Removed inital_check_full_ast

3 files changed, 1 insertions, 825 deletions

diff --git a/src/initial_check_full_ast.ml b/src/initial_check_full_ast.ml
deleted file mode 100644
index b2781350..00000000
--- a/src/initial_check_full_ast.ml
+++ /dev/null
@@ -1,820 +0,0 @@
-(**************************************************************************)
-(*     Sail                                                               *)
-(*                                                                        *)
-(*  Copyright (c) 2013-2017                                               *)
-(*    Kathyrn Gray                                                        *)
-(*    Shaked Flur                                                         *)
-(*    Stephen Kell                                                        *)
-(*    Gabriel Kerneis                                                     *)
-(*    Robert Norton-Wright                                                *)
-(*    Christopher Pulte                                                   *)
-(*    Peter Sewell                                                        *)
-(*                                                                        *)
-(*  All rights reserved.                                                  *)
-(*                                                                        *)
-(*  This software was developed by the University of Cambridge Computer   *)
-(*  Laboratory as part of the Rigorous Engineering of Mainstream Systems  *)
-(*  (REMS) project, funded by EPSRC grant EP/K008528/1.                   *)
-(*                                                                        *)
-(*  Redistribution and use in source and binary forms, with or without    *)
-(*  modification, are permitted provided that the following conditions    *)
-(*  are met:                                                              *)
-(*  1. Redistributions of source code must retain the above copyright     *)
-(*     notice, this list of conditions and the following disclaimer.      *)
-(*  2. Redistributions in binary form must reproduce the above copyright  *)
-(*     notice, this list of conditions and the following disclaimer in    *)
-(*     the documentation and/or other materials provided with the         *)
-(*     distribution.                                                      *)
-(*                                                                        *)
-(*  THIS SOFTWARE IS PROVIDED BY THE AUTHOR AND CONTRIBUTORS ``AS IS''    *)
-(*  AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED     *)
-(*  TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A       *)
-(*  PARTICULAR PURPOSE ARE DISCLAIMED.  IN NO EVENT SHALL THE AUTHOR OR   *)
-(*  CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,          *)
-(*  SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT      *)
-(*  LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF      *)
-(*  USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND   *)
-(*  ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY,    *)
-(*  OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT    *)
-(*  OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF    *)
-(*  SUCH DAMAGE.                                                          *)
-(**************************************************************************)
-
-open Type_internal
-open Ast
-open Type_internal
-
-(*Envs is a tuple of used names (currently unused), map from id to kind, default order for vector types and literal vectors *)
-type envs = Nameset.t * kind Envmap.t * Ast.order 
-type 'a envs_out = 'a * envs
-
-let id_to_string (Id_aux(id,l)) =
-  match id with | Id(x) | DeIid(x) -> x
-
-let var_to_string (Kid_aux(Var v,l)) = v
-
-let typquant_to_quantkinds k_env typquant = 
-  match typquant with
-  | TypQ_aux(tq,_) ->
-    (match tq with
-    | TypQ_no_forall -> []
-    | TypQ_tq(qlist) ->
-      List.fold_right
-        (fun (QI_aux(qi,_)) rst ->
-          match qi with
-          | QI_const _ -> rst
-          | QI_id(ki) -> begin
-            match ki with 
-            | KOpt_aux(KOpt_none(v),l) | KOpt_aux(KOpt_kind(_,v),l) -> 
-              (match Envmap.apply k_env (var_to_string v) with
-              | Some(typ) -> typ::rst
-              | None -> raise (Reporting_basic.err_unreachable l "Envmap didn't get an entry during typschm processing"))
-          end)
-        qlist
-        [])
-
-let typ_error l msg opt_id opt_var opt_kind =
-  let full_msg = (msg ^
-                  (match opt_id, opt_var, opt_kind with
-                   | Some(id),None,Some(kind) -> (id_to_string id) ^ " of " ^ (kind_to_string kind)
-                   | Some(id),None,None -> ": " ^ (id_to_string id)
-                   | None,Some(v),Some(kind) -> (var_to_string v) ^ " of " ^ (kind_to_string kind)
-                   | None,Some(v),None -> ": " ^ (var_to_string v)
-                   | None,None,Some(kind) -> " " ^ (kind_to_string kind)
-                   | _ -> "")) in
-  Reporting_basic.report_error (Reporting_basic.Err_type(l, full_msg))
-                
-let to_base_kind (BK_aux(k,l')) =
-  match k with
-  | BK_type -> BK_aux(BK_type,l'), { k = K_Typ}
-  | BK_nat -> BK_aux(BK_nat,l'), { k = K_Nat }
-  | BK_order -> BK_aux(BK_order,l'), { k = K_Ord }
-  | BK_effect -> BK_aux(BK_effect,l'), { k = K_Efct }
-
-let to_kind (k_env : kind Envmap.t) (K_aux(K_kind(klst),l)) : (Ast.kind * kind) =
-  match klst with
-  | [] -> raise (Reporting_basic.err_unreachable l "Kind with empty kindlist encountered")
-  | [k] -> let k_ast,k_typ = to_base_kind k in
-           K_aux(K_kind([k_ast]),l), k_typ
-  | ks -> let k_pairs = List.map to_base_kind ks in
-          let reverse_typs = List.rev (List.map snd k_pairs) in
-          let ret,args = List.hd reverse_typs, List.rev (List.tl reverse_typs) in
-          match ret.k with
-          | K_Typ -> K_aux(K_kind(List.map fst k_pairs), l), { k = K_Lam(args,ret) }
-          | _ -> typ_error l "Type constructor must have an -> kind ending in Type" None None None
-
-let rec typ_to_string (Typ_aux(t,_)) = match t with
-  | Typ_id i -> id_to_string i
-  | Typ_var (Kid_aux (Var i,_)) -> i
-  | _ -> "bigger than var"
-
-and nexp_to_string (Nexp_aux(n,_)) = match n with
-  | Nexp_id i -> id_to_string i
-  | Nexp_var (Kid_aux (Var i,_)) -> i
-  | _ -> "nexp bigger than var"
-
-let rec to_typ (k_env : kind Envmap.t) (def_ord : Ast.order) (t: Ast.typ) : Ast.typ =
-  match t with
-  | Typ_aux(t,l) ->
-    Typ_aux( (match t with 
-              | Typ_id(id) -> 
-                let mk = Envmap.apply k_env (id_to_string id) in
-                (match mk with
-                 | Some(k) ->
-                   (match k.k with
-                    | K_Typ -> Typ_id id
-                    | K_infer -> k.k <- K_Typ; Typ_id id
-                    | _ -> typ_error l "Required an identifier with kind Type, encountered " (Some id) None (Some k))
-                 | None -> typ_error l "Encountered an unbound type identifier" (Some id) None None)
-              | Typ_var(v) -> 
-                let mk = Envmap.apply k_env (var_to_string v) in
-                (match mk with
-                 | Some(k) -> (match k.k with
-                     | K_Typ -> Typ_var v
-                     | K_infer -> k.k <- K_Typ; Typ_var v
-                     | _ -> typ_error l "Required a variable with kind Type, encountered " None (Some v) (Some k))
-                | None -> typ_error l "Encountered an unbound variable" None (Some v) None)
-              | Typ_fn(arg,ret,efct) -> Typ_fn( (to_typ k_env def_ord arg),
-                                                (to_typ k_env def_ord ret),
-                                                (to_effects k_env efct))
-              | Typ_tup(typs) -> Typ_tup( List.map (to_typ k_env def_ord) typs)
-              | Typ_app(id,typs) ->
-                let k = Envmap.apply k_env (id_to_string id) in
-                (match k with 
-                 | Some({k = K_Lam(args,t)}) -> 
-                   if ((List.length args) = (List.length typs))
-                   then
-                     Typ_app(id,(List.map2 (fun k a -> (to_typ_arg k_env def_ord k a)) args typs))
-                   else typ_error l "Type constructor given incorrect number of arguments" (Some id) None None
-                 | None ->
-                   typ_error l "Required a type constructor, encountered an unbound identifier" (Some id) None None
-                 | _ -> typ_error l "Required a type constructor, encountered a base kind variable" (Some id) None None)
-              | _ ->
-                typ_error l "Required an item of kind Type, encountered an illegal form for this kind" None None None
-      ), l)
-
-and to_nexp (k_env : kind Envmap.t) (n: Ast.nexp) : Ast.nexp =
-  match n with
-  | Nexp_aux(t,l) ->
-    (match t with
-     | Nexp_id i ->
-       let mk = Envmap.apply k_env (id_to_string i) in
-       (match mk with
-        | Some(k) -> Nexp_aux((match k.k with
-            | K_Nat -> Nexp_id i
-            | K_infer -> k.k <- K_Nat; Nexp_id i
-            | _ -> typ_error l "Required a variable with kind Nat, encountered " (Some i) None (Some k)),l)
-       | None -> typ_error l "Encountered an unbound variable" (Some i) None None)       
-    | Nexp_var(v) ->                
-      let mk = Envmap.apply k_env (var_to_string v) in
-      (match mk with
-       | Some(k) -> Nexp_aux((match k.k with
-           | K_Nat -> Nexp_var v
-           | K_infer -> k.k <- K_Nat; Nexp_var v
-           | _ -> typ_error l "Required a variable with kind Nat, encountered " None (Some v) (Some k)),l)
-       | None -> typ_error l "Encountered an unbound variable" None (Some v) None)
-    | Nexp_constant(i) -> Nexp_aux(Nexp_constant(i),l)
-    | Nexp_sum(t1,t2) ->
-      let n1 = to_nexp k_env t1 in
-      let n2 = to_nexp k_env t2 in
-      Nexp_aux(Nexp_sum(n1,n2),l)
-    | Nexp_exp(t1) -> Nexp_aux(Nexp_exp(to_nexp k_env t1),l)
-    | Nexp_neg(t1) -> Nexp_aux(Nexp_neg(to_nexp k_env t1),l)
-    | Nexp_times(t1,t2) ->
-      let n1 = to_nexp k_env t1 in
-      let n2 = to_nexp k_env t2 in
-      Nexp_aux(Nexp_times(n1,n2),l)
-    | Nexp_minus(t1,t2) ->
-      let n1 = to_nexp k_env t1 in
-      let n2 = to_nexp k_env t2 in
-      Nexp_aux(Nexp_minus(n1,n2),l))
-    
-and to_order (k_env : kind Envmap.t) (def_ord : Ast.order) (o: Ast.order) : Ast.order =
-  match o with
-  | Ord_aux(t,l) ->
-    (match t with
-      | Ord_var(v) -> 
-        let mk = Envmap.apply k_env (var_to_string v) in
-        (match mk with
-         | Some(k) -> (match k.k with
-             | K_Ord -> Ord_aux(Ord_var v, l)
-             | K_infer -> k.k <- K_Ord; Ord_aux(Ord_var v,l)
-             | _ -> typ_error l "Required a variable with kind Order, encountered " None (Some v) (Some k))
-         | None -> typ_error l "Encountered an unbound variable" None (Some v) None)
-      | Ord_inc -> Ord_aux(Ord_inc,l)
-      | Ord_dec -> Ord_aux(Ord_dec,l)
-    )
-
-and to_effects (k_env : kind Envmap.t) (e : Ast.effect) : Ast.effect =
-  match e with
-  | Effect_aux(t,l) ->
-    Effect_aux( (match t with
-        | Effect_var(v) ->  
-          let mk = Envmap.apply k_env (var_to_string v) in
-          (match mk with
-           | Some(k) -> (match k.k with
-               | K_Efct -> Effect_var v
-               | K_infer -> k.k <- K_Efct; Effect_var v
-               | _ -> typ_error l "Required a variable with kind Effect, encountered " None (Some v) (Some k))
-           | None -> typ_error l "Encountered an unbound variable" None (Some v) None)
-        | Effect_set(effects) -> Effect_set(effects)
-    ), l)
-
-and to_typ_arg (k_env : kind Envmap.t) (def_ord : Ast.order) (kind : kind) (arg : Ast.typ_arg) : Ast.typ_arg =
-  let l,ta = (match arg with Typ_arg_aux(ta,l) -> l,ta) in
-  Typ_arg_aux (  
-    (match kind.k,ta with 
-    | K_Typ,Typ_arg_typ t     -> Typ_arg_typ (to_typ k_env def_ord t)
-    | K_Nat,Typ_arg_nexp n    -> Typ_arg_nexp (to_nexp k_env n)
-    | K_Ord,Typ_arg_order o   -> Typ_arg_order (to_order k_env def_ord o)
-    | K_Efct,Typ_arg_effect e -> Typ_arg_effect (to_effects k_env e)
-    | (K_Lam _ | K_infer | K_Val),_ -> 
-      raise (Reporting_basic.err_unreachable l "To_ast_typ_arg received Lam kind or infer kind")
-    | _ ->
-      let tn_str = 
-        (match ta with
-         | Typ_arg_typ t -> typ_to_string t
-         | Typ_arg_nexp n -> nexp_to_string n
-         | _ -> "order or effect") in
-      typ_error l ("Kind declaration and kind of type argument, " ^ tn_str ^ " don't match here")
-        None None (Some kind)), 
-    l)
-
-let to_nexp_constraint (k_env : kind Envmap.t) (c : n_constraint) : n_constraint =
-  match c with 
-  | NC_aux(nc,l) ->
-    NC_aux( (match nc with
-             | NC_fixed(t1,t2) -> 
-               let n1 = to_nexp k_env t1 in
-               let n2 = to_nexp k_env t2 in
-               NC_fixed(n1,n2)
-             | NC_bounded_ge(t1,t2) ->
-               let n1 = to_nexp k_env t1 in
-               let n2 = to_nexp k_env t2 in
-               NC_bounded_ge(n1,n2)
-             | NC_bounded_le(t1,t2) ->
-               let n1 = to_nexp k_env t1 in
-               let n2 = to_nexp k_env t2 in
-               NC_bounded_le(n1,n2)
-             | NC_nat_set_bounded(id,bounds) ->
-               NC_nat_set_bounded(id, bounds)
-    ), l)               
-
-(* Transforms a typquant while building first the kind environment of declared variables, and also the kind environment in context *)
-let to_typquant (k_env: kind Envmap.t) (tq : typquant) : typquant * kind Envmap.t * kind Envmap.t =
-  let opt_kind_to_ast k_env local_names local_env (KOpt_aux(ki,l)) =
-    let v, key, kind, ktyp =
-      match ki with
-      | KOpt_none(v) ->
-        let key = var_to_string v in
-        let kind,ktyp =
-          if (Envmap.in_dom key k_env) then None,(Envmap.apply k_env key)
-          else None,(Some{ k = K_infer }) in
-        v,key,kind, ktyp
-      | KOpt_kind(k,v) ->
-        let key = var_to_string v in
-        let kind,ktyp = to_kind k_env k in
-        v,key,Some(kind),Some(ktyp)
-    in
-    if (Nameset.mem key local_names)
-    then typ_error l "Encountered duplicate name in type scheme" None (Some v) None
-    else 
-      let local_names = Nameset.add key local_names in
-      let kopt,k_env,k_env_local = (match kind,ktyp with
-        | Some(k),Some(kt) -> KOpt_kind(k,v), (Envmap.insert k_env (key,kt)), (Envmap.insert local_env (key,kt))
-        | None, Some(kt) -> KOpt_none(v), (Envmap.insert k_env (key,kt)), (Envmap.insert local_env (key,kt))
-        | _ -> raise (Reporting_basic.err_unreachable l "Envmap in dom is true but apply gives None")) in
-      KOpt_aux(kopt,l),k_env,local_names,k_env_local
-  in
-  match tq with
-  | TypQ_aux(tqa,l) ->
-    (match tqa with
-    | TypQ_no_forall -> TypQ_aux(TypQ_no_forall,l), k_env, Envmap.empty
-    | TypQ_tq(qlist) ->
-      let rec to_q_items k_env local_names local_env = function
-        | [] -> [],k_env,local_env
-        | q::qs ->
-          (match q with
-           | QI_aux(qi,l) ->
-             (match qi with
-              | QI_const(n_const) -> 
-                let c = QI_aux(QI_const(to_nexp_constraint k_env n_const),l) in
-                        let qis,k_env,local_env = to_q_items k_env local_names local_env qs in
-                        (c::qis),k_env,local_env
-                      | QI_id(kid) ->
-                        let kid,k_env,local_names,local_env = opt_kind_to_ast k_env local_names local_env kid in
-                        let c = QI_aux(QI_id(kid),l) in
-                        let qis,k_env,local_env = to_q_items k_env local_names local_env qs in
-                        (c::qis),k_env,local_env))      
-      in
-      let lst,k_env,local_env = to_q_items k_env Nameset.empty Envmap.empty qlist in
-      TypQ_aux(TypQ_tq(lst),l), k_env, local_env)
-
-let to_typschm (k_env:kind Envmap.t) (def_ord:Ast.order) (tschm:Ast.typschm)
-  :Ast.typschm * kind Envmap.t * kind Envmap.t =
-  match tschm with
-  | TypSchm_aux(ts,l) -> 
-    (match ts with | TypSchm_ts(tquant,t) ->
-      let tq,k_env,local_env = to_typquant k_env tquant in
-      let typ = to_typ k_env def_ord t in
-      TypSchm_aux(TypSchm_ts(tq,typ),l),k_env,local_env)
-
-let rec to_pat (k_env : kind Envmap.t) (def_ord : Ast.order) (P_aux(pat,(l,_)) : tannot pat) : tannot pat = 
-  P_aux(
-    (match pat with 
-    | P_lit(lit) -> P_lit(lit)
-    | P_wild -> P_wild
-    | P_as(pat,id) -> P_as(to_pat k_env def_ord pat, id)
-    | P_typ(typ,pat) -> P_typ(to_typ k_env def_ord typ,to_pat k_env def_ord pat)
-    | P_id(id) -> P_id(id)
-    | P_app(id,pats) ->
-      if pats = [] 
-      then P_id (id)
-      else P_app(id, List.map (to_pat k_env def_ord) pats)
-    | P_record(fpats,_) -> 
-      P_record(List.map 
-                 (fun (FP_aux(FP_Fpat(id,fp),(l,_))) -> 
-                      FP_aux(FP_Fpat(id, to_pat k_env def_ord fp),(l,NoTyp)))
-                 fpats, false)
-    | P_vector(pats) -> P_vector(List.map (to_pat k_env def_ord) pats)
-    | P_vector_indexed(ipats) -> P_vector_indexed(List.map (fun (i,pat) -> i,to_pat k_env def_ord pat) ipats)
-    | P_vector_concat(pats) -> P_vector_concat(List.map (to_pat k_env def_ord) pats)
-    | P_tup(pats) -> P_tup(List.map (to_pat k_env def_ord) pats)
-    | P_list(pats) -> P_list(List.map (to_pat k_env def_ord) pats)
-    ), (l,NoTyp))
-
-
-let rec to_letbind (k_env : kind Envmap.t) (def_ord : Ast.order) (LB_aux(lb,(l,_)) : tannot letbind) : tannot letbind =
-  LB_aux(
-    (match lb with
-    | LB_val_explicit(typschm,pat,exp) ->
-      let typsch, k_env, _  = to_typschm k_env def_ord typschm in
-      LB_val_explicit(typsch,to_pat k_env def_ord pat, to_exp k_env def_ord exp)
-    | LB_val_implicit(pat,exp) ->
-      LB_val_implicit(to_pat k_env def_ord pat, to_exp k_env def_ord exp)
-    ), (l,NoTyp))
-
-and to_exp (k_env : kind Envmap.t) (def_ord : Ast.order) (E_aux(exp,(l,_)) :  exp) : exp = 
-  E_aux(
-    (match exp with
-    | E_block(exps) -> E_block(List.map (to_exp k_env def_ord) exps)
-    | E_nondet(exps) -> E_nondet(List.map (to_exp k_env def_ord) exps)
-    | E_id(id) -> E_id(id)
-    | E_lit(lit) -> E_lit(lit)
-    | E_cast(typ,exp) -> E_cast(to_typ k_env def_ord typ, to_exp k_env def_ord exp)
-    | E_app(f,args) -> 
-      (match List.map (to_exp k_env def_ord) args with
-        | [] -> E_app(f, [])
-        | [E_aux(E_tuple(exps),_)] -> E_app(f, exps)
-        | exps -> E_app(f, exps))
-    | E_app_infix(left,op,right) -> 
-      E_app_infix(to_exp k_env def_ord left, op, to_exp k_env def_ord right)
-    | E_tuple(exps) -> E_tuple(List.map (to_exp k_env def_ord) exps)
-    | E_if(e1,e2,e3) -> E_if(to_exp k_env def_ord e1, to_exp k_env def_ord e2, to_exp k_env def_ord e3)
-    | E_for(id,e1,e2,e3,atyp,e4) -> 
-      E_for(id,to_exp k_env def_ord e1, to_exp k_env def_ord e2,
-            to_exp k_env def_ord e3,to_order k_env def_ord atyp, to_exp k_env def_ord e4)
-    | E_vector(exps) -> E_vector(List.map (to_exp k_env def_ord) exps)
-    | E_vector_indexed(iexps,Def_val_aux(default,(dl,_))) -> 
-      E_vector_indexed (to_iexps true k_env def_ord iexps, 
-                        Def_val_aux((match default with
-                            | Def_val_empty -> Def_val_empty
-                            | Def_val_dec e -> Def_val_dec (to_exp k_env def_ord e)),(dl,NoTyp)))
-    | E_vector_access(vexp,exp) -> E_vector_access(to_exp k_env def_ord vexp, to_exp k_env def_ord exp)
-    | E_vector_subrange(vex,exp1,exp2) -> 
-      E_vector_subrange(to_exp k_env def_ord vex, to_exp k_env def_ord exp1, to_exp k_env def_ord exp2)
-    | E_vector_update(vex,exp1,exp2) -> 
-      E_vector_update(to_exp k_env def_ord vex, to_exp k_env def_ord exp1, to_exp k_env def_ord exp2)
-    | E_vector_update_subrange(vex,e1,e2,e3) -> 
-      E_vector_update_subrange(to_exp k_env def_ord vex, to_exp k_env def_ord e1, 
-                               to_exp k_env def_ord e2, to_exp k_env def_ord e3)
-    | E_vector_append(e1,e2) -> E_vector_append(to_exp k_env def_ord e1,to_exp k_env def_ord e2)
-    | E_list(exps) -> E_list(List.map (to_exp k_env def_ord) exps)
-    | E_cons(e1,e2) -> E_cons(to_exp k_env def_ord e1, to_exp k_env def_ord e2)
-    | E_record(fexps) ->
-      (match to_fexps true k_env def_ord fexps with
-       | Some(fexps) -> E_record(fexps)
-       | None -> raise (Reporting_basic.err_unreachable l "to_fexps with true returned none"))
-    | E_record_update(exp,fexps) -> 
-      (match to_fexps true k_env def_ord fexps with
-      | Some(fexps) -> E_record_update(to_exp k_env def_ord exp, fexps)
-      | _ -> raise (Reporting_basic.err_unreachable l "to_fexps with true returned none"))
-    | E_field(exp,id) -> E_field(to_exp k_env def_ord exp, id)
-    | E_case(exp,pexps) -> E_case(to_exp k_env def_ord exp, List.map (to_case k_env def_ord) pexps)
-    | E_let(leb,exp) -> E_let(to_letbind k_env def_ord leb, to_exp k_env def_ord exp)
-    | E_assign(lexp,exp) -> E_assign(to_lexp k_env def_ord lexp, to_exp k_env def_ord exp)
-    | E_sizeof(nexp) -> E_sizeof(to_nexp k_env nexp)
-    | E_exit exp -> E_exit(to_exp k_env def_ord exp)
-    | E_return exp -> E_return(to_exp k_env def_ord exp)
-    | E_assert(cond,msg) -> E_assert(to_exp k_env def_ord cond, to_exp k_env def_ord msg)
-    | E_comment s -> E_comment s
-    | E_comment_struc e -> E_comment_struc e
-    | _ -> raise (Reporting_basic.err_unreachable l "to_exp given internal node")
-    ), (l,NoTyp))
-
-and to_lexp (k_env : kind Envmap.t) (def_ord : Ast.order) (LEXP_aux(exp,(l,_)) : tannot lexp) : tannot lexp = 
-  LEXP_aux(
-    (match exp with
-    | LEXP_id(id) -> LEXP_id(id)
-    | LEXP_memory(f,args) -> 
-      (match List.map (to_exp k_env def_ord) args with
-       | [] -> LEXP_memory(f,[])
-       | [E_aux(E_tuple exps,_)] -> LEXP_memory(f,exps)
-       | args -> LEXP_memory(f, args))
-    | LEXP_cast(typ,id) ->
-      LEXP_cast(to_typ k_env def_ord typ, id)
-    | LEXP_tup tups ->
-       let ltups = List.map (to_lexp k_env def_ord) tups in
-       let is_ok_in_tup (LEXP_aux (le,(l,_))) =
-         match le with
-         | LEXP_id _ | LEXP_cast _ | LEXP_vector _ | LEXP_field _ | LEXP_vector_range _ | LEXP_tup _ -> ()
-         | LEXP_memory _  ->
-           typ_error l "only identifiers, fields, and vectors may be set in a tuple" None None None in
-       List.iter is_ok_in_tup ltups;
-       LEXP_tup(ltups)
-    | LEXP_vector(vexp,exp) -> LEXP_vector(to_lexp k_env def_ord vexp, to_exp k_env def_ord exp)
-    | LEXP_vector_range(vexp,exp1,exp2) -> 
-      LEXP_vector_range(to_lexp k_env def_ord vexp, to_exp k_env def_ord exp1, to_exp k_env def_ord exp2)
-    | LEXP_field(fexp,id) -> LEXP_field(to_lexp k_env def_ord fexp, id))
-  , (l,NoTyp))
-
-and to_case (k_env : kind Envmap.t) (def_ord : Ast.order) (Pat_aux(pex,(l,_)) : tannot pexp) : tannot pexp =
-  match pex with 
-  | Pat_exp(pat,exp) -> Pat_aux(Pat_exp(to_pat k_env def_ord pat, to_exp k_env def_ord exp),(l,NoTyp))
-
-and to_fexps (fail_on_error:bool) (k_env:kind Envmap.t) (def_ord:Ast.order) (FES_aux (FES_Fexps(fexps,_),(l,_)))
-  : tannot fexps option =
-  let wrap fs = FES_aux (FES_Fexps(fs,false),(l,NoTyp)) in
-  match fexps with
-  | [] -> if fail_on_error then typ_error l "Record or record update must include fields" None None None
-    else None
-  | fexp::exps ->
-    match fexp with
-    | FE_aux(FE_Fexp(id,exp),(fl,_)) ->
-      (match (to_fexps false k_env def_ord (wrap exps)) with
-       | Some(FES_aux(FES_Fexps(fexps,_),(l,_))) ->
-         Some(wrap(fexp::fexps))
-       | None ->
-         Some(wrap([fexp])))
-
-and to_iexps (fail_on_error:bool) (k_env:kind Envmap.t) (def_ord:Ast.order) (iexps: (int * exp) list)
-  :(int * exp) list =
-  match iexps with
-  | [] -> []
-  | (i,exp)::exps ->
-    (i, to_exp k_env def_ord exp)::to_iexps fail_on_error k_env def_ord exps
-      
-let to_default (names, k_env, default_order) (default : tannot default_spec) : (tannot default_spec) envs_out =
-  match default with
-  | DT_aux(df,l) ->
-    (match df with 
-    | DT_kind(bk,v) ->
-      let k,k_typ = to_base_kind bk in
-      let key = var_to_string v in
-      DT_aux(DT_kind(k,v),l),(names,(Envmap.insert k_env (key,k_typ)),default_order)
-    | DT_typ(typschm,id) ->
-      let tps,_,_ = to_typschm k_env default_order typschm in
-      DT_aux(DT_typ(tps,id),l),(names,k_env,default_order)
-    | DT_order(o) ->
-      (match o with
-       | Ord_aux(Ord_inc,lo) ->
-         let default_order = Ord_aux(Ord_inc,lo) in
-         DT_aux(DT_order default_order,l),(names,k_env,default_order)
-       | Ord_aux(Ord_dec,lo) ->
-         let default_order = Ord_aux(Ord_dec,lo) in
-         DT_aux(DT_order default_order,l),(names,k_env,default_order)
-       | _ -> typ_error l "Default order must be Inc or Dec" None None None))
-
-let to_spec (names,k_env,default_order) (val_: tannot val_spec) : (tannot val_spec) envs_out =
-  match val_ with
-  | VS_aux(vs,(l,_)) ->
-    (match vs with
-    | VS_val_spec(ts,id) ->
-      let typsch,_,_ = to_typschm k_env default_order ts in
-      VS_aux(VS_val_spec(typsch, id),(l,NoTyp)),(names,k_env,default_order)
-    | VS_extern_spec(ts,id,s) ->
-      let typsch,_,_ = to_typschm k_env default_order ts in
-      VS_aux(VS_extern_spec(typsch,id,s),(l,NoTyp)),(names,k_env,default_order)
-    | VS_extern_no_rename(ts,id) ->
-      let typsch,_,_ = to_typschm k_env default_order ts in
-       VS_aux(VS_extern_no_rename(typsch,id),(l,NoTyp)),(names,k_env,default_order))
-    
-let to_namescm ns = ns
-
-let rec to_range (BF_aux(r,l)) = (* TODO add check that ranges are sensible for some definition of sensible *)
-  BF_aux(
-    (match r with
-    | BF_single(i) -> BF_single(i)
-    | BF_range(i1,i2) -> BF_range(i1,i2)
-    | BF_concat(ir1,ir2) -> BF_concat( to_range ir1, to_range ir2)),
-    l)
-
-let to_type_union k_env default_order (Tu_aux(tu,l)) =
-  match tu with
-    | Tu_ty_id(atyp,id) -> (Tu_aux(Tu_ty_id ((to_typ k_env default_order atyp),id),l))
-    | Tu_id id -> (Tu_aux(Tu_id(id),l)) 
-
-let to_typedef (names,k_env,def_ord) (td: tannot type_def) : (tannot type_def) envs_out =
-  match td with
-  |TD_aux(td,(l,_)) ->
-  (match td with 
-  | TD_abbrev(id,name_scm_opt,typschm) ->
-    let key = id_to_string id in
-    let typschm,k_env,_ = to_typschm k_env def_ord typschm in
-    let td_abrv = TD_aux(TD_abbrev(id,to_namescm name_scm_opt,typschm),(l,NoTyp)) in
-    let typ = (match typschm with 
-      | TypSchm_aux(TypSchm_ts(tq,typ), _) ->
-        begin match (typquant_to_quantkinds k_env tq) with
-        | [] -> {k = K_Typ}
-        | typs -> {k= K_Lam(typs,{k=K_Typ})}
-        end) in
-    td_abrv,(names,Envmap.insert k_env (key,typ),def_ord)
-  | TD_record(id,name_scm_opt,typq,fields,_) -> 
-    let key = id_to_string id in
-    let typq,k_env,_ = to_typquant k_env typq in
-    let fields = List.map (fun (atyp,id) -> (to_typ k_env def_ord atyp),id) fields in (* Add check that all arms have unique names locally *)
-    let td_rec = TD_aux(TD_record(id,to_namescm name_scm_opt,typq,fields,false),(l,NoTyp)) in
-    let typ = (match (typquant_to_quantkinds k_env typq) with
-      | [ ] -> {k = K_Typ}
-      | typs -> {k = K_Lam(typs,{k=K_Typ})}) in
-    td_rec, (names,Envmap.insert k_env (key,typ), def_ord)
-  | TD_variant(id,name_scm_opt,typq,arms,_) ->
-    let key = id_to_string id in
-    let typq,k_env,_ = to_typquant k_env typq in
-    let arms = List.map (to_type_union k_env def_ord) arms in (* Add check that all arms have unique names *)
-    let td_var = TD_aux(TD_variant(id,to_namescm name_scm_opt,typq,arms,false),(l,NoTyp)) in
-    let typ = (match (typquant_to_quantkinds k_env typq) with
-      | [ ] -> {k = K_Typ}
-      | typs -> {k = K_Lam(typs,{k=K_Typ})}) in
-    td_var, (names,Envmap.insert k_env (key,typ), def_ord)
-  | TD_enum(id,name_scm_opt,enums,_) -> 
-    let key = id_to_string id in
-    let keys = List.map id_to_string enums in
-    let td_enum = TD_aux(TD_enum(id,to_namescm name_scm_opt,enums,false),(l,NoTyp)) in (* Add check that all enums have unique names *)
-    let k_env = List.fold_right (fun k k_env -> Envmap.insert k_env (k,{k=K_Nat})) keys (Envmap.insert k_env (key,{k=K_Typ})) in
-    td_enum, (names,k_env,def_ord)
-  | TD_register(id,t1,t2,ranges) -> 
-    let key = id_to_string id in
-    let n1 = to_nexp k_env t1 in
-    let n2 = to_nexp k_env t2 in
-    let ranges = List.map (fun (range,id) -> (to_range range),id) ranges in
-    TD_aux(TD_register(id,n1,n2,ranges),(l,NoTyp)), (names,Envmap.insert k_env (key, {k=K_Typ}),def_ord))
-
-let to_kinddef (names,k_env,def_ord) (kd: tannot kind_def) : (tannot kind_def) envs_out =
-  match kd with
-  |KD_aux(td,(l,_)) ->
-    (match td with 
-     | KD_abbrev(kind,id,name_scm_opt,typschm) ->
-       let key = id_to_string id in
-       let _,k = to_kind k_env kind in
-       (match k.k with
-        | K_Typ | K_Lam _ ->
-          let typschm,k_env,_ = to_typschm k_env def_ord typschm in
-          let kd_abrv = KD_aux(KD_abbrev(kind,id,to_namescm name_scm_opt,typschm),(l,NoTyp)) in
-          let typ = (match typschm with 
-              | TypSchm_aux(TypSchm_ts(tq,typ), _) ->
-                begin match (typquant_to_quantkinds k_env tq) with
-                  | [] -> {k = K_Typ}
-                  | typs -> {k= K_Lam(typs,{k=K_Typ})}
-                end) in
-          kd_abrv,(names,Envmap.insert k_env (key,typ),def_ord)
-        | _ -> typ_error l "Def abbreviation with type scheme had declared kind other than Type" None None (Some k))
-     | KD_nabbrev(kind,id,name_scm_opt,nexp) ->
-       let key = id_to_string id in
-       let _,k = to_kind k_env kind in
-       (match k.k with
-        | K_Nat ->
-          let nexp = to_nexp k_env nexp in
-          let kd_nabrv = KD_aux(KD_nabbrev(kind,id,to_namescm name_scm_opt, nexp),(l,NoTyp)) in
-          kd_nabrv,(names,Envmap.insert k_env (key,k),def_ord)
-        | _ -> typ_error l "Def abbreviation binding a number declared with kind other than Nat" None None (Some k))
-     | KD_record(kind,id,name_scm_opt,typq,fields,_) -> 
-       let key = id_to_string id in
-       let _,k = to_kind k_env kind in
-       let typq,k_env,_ = to_typquant k_env typq in
-       (match k.k with
-        | K_Typ | K_Lam _ ->
-          let fields = List.map (fun (atyp,id) -> (to_typ k_env def_ord atyp),id) fields in (* Add check that all arms have unique names locally *)
-          let kd_rec = KD_aux(KD_record(kind,id,to_namescm name_scm_opt,typq,fields,false),(l,NoTyp)) in
-          let typ = (match (typquant_to_quantkinds k_env typq) with
-              | [ ] -> {k = K_Typ}
-              | typs -> {k = K_Lam(typs,{k=K_Typ})}) in
-          kd_rec, (names,Envmap.insert k_env (key,typ), def_ord)
-        | _ -> typ_error l "Def abbreviation binding a record has kind other than Type" None None (Some k))
-     | KD_variant(kind,id,name_scm_opt,typq,arms,_) ->
-       let key = id_to_string id in
-       let _,k = to_kind k_env kind in
-       let typq,k_env,_ = to_typquant k_env typq in
-       (match k.k with
-        | K_Typ | K_Lam _ ->
-          let arms = List.map (to_type_union k_env def_ord) arms in (* Add check that all arms have unique names *)
-          let kd_var = KD_aux(KD_variant(kind,id,to_namescm name_scm_opt,typq,arms,false),(l,NoTyp)) in
-          let typ = (match (typquant_to_quantkinds k_env typq) with
-              | [ ] -> {k = K_Typ}
-              | typs -> {k = K_Lam(typs,{k=K_Typ})}) in
-          kd_var, (names,Envmap.insert k_env (key,typ), def_ord)
-        | _ -> typ_error l "Def abbreviation binding a variant has kind other than Type" None None (Some k))
-     | KD_enum(kind,id,name_scm_opt,enums,_) -> 
-       let key = id_to_string id in
-       let keys = List.map id_to_string enums in
-       let _,k= to_kind k_env kind in
-       (match k.k with
-        | K_Typ ->
-          let kd_enum = KD_aux(KD_enum(kind,id,to_namescm name_scm_opt,enums,false),(l,NoTyp)) in (* Add check that all enums have unique names *)
-          let k_env = List.fold_right (fun k k_env -> Envmap.insert k_env (k,{k=K_Nat})) keys (Envmap.insert k_env (key,{k=K_Typ})) in
-          kd_enum, (names,k_env,def_ord)
-        | _ -> typ_error l "Def abbreviation binding an enum has kind other than Type" None None (Some k))
-     | KD_register(kind,id,t1,t2,ranges) -> 
-       let key = id_to_string id in
-       let n1 = to_nexp k_env t1 in
-       let n2 = to_nexp k_env t2 in
-       let _,k = to_kind k_env kind in
-       match k.k with
-       | K_Typ ->
-         let ranges = List.map (fun (range,id) -> (to_range range),id) ranges in
-         KD_aux(KD_register(kind,id,n1,n2,ranges),(l,NoTyp)), (names,Envmap.insert k_env (key, {k=K_Typ}),def_ord)
-       | _ -> typ_error l "Def abbreviation binding a register type has kind other than Type" None None (Some k))
-
-
-let to_tannot_opt (k_env:kind Envmap.t) (def_ord:Ast.order) (Typ_annot_opt_aux(tp,l))
-  :tannot_opt * kind Envmap.t * kind Envmap.t=
-  match tp with
-  | Typ_annot_opt_some(tq,typ) ->
-    let typq,k_env,k_local = to_typquant k_env tq in
-    Typ_annot_opt_aux(Typ_annot_opt_some(typq,to_typ k_env def_ord typ),l),k_env,k_local
-
-let to_effects_opt (k_env : kind Envmap.t) (Effect_opt_aux(e,l)) : effect_opt =
-  match e with
-  | Effect_opt_pure -> Effect_opt_aux(Effect_opt_pure,l)
-  | Effect_opt_effect(typ) -> Effect_opt_aux(Effect_opt_effect(to_effects k_env typ),l)
-
-let to_funcl (names,k_env,def_ord) (FCL_aux(fcl,(l,_)) : tannot funcl) : (tannot funcl) =
-  match fcl with
-  | FCL_Funcl(id,pat,exp) -> 
-    FCL_aux(FCL_Funcl(id, to_pat k_env def_ord pat, to_exp k_env def_ord exp),(l,NoTyp))
-
-let to_fundef  (names,k_env,def_ord) (FD_aux(fd,(l,_)): tannot fundef) : (tannot fundef) envs_out = 
-  match fd with
-  | FD_function(rec_opt,tannot_opt,effects_opt,funcls) -> 
-    let tannot_opt, k_env,_ = to_tannot_opt k_env def_ord tannot_opt in
-    FD_aux(FD_function(rec_opt, tannot_opt, to_effects_opt k_env effects_opt,
-                       List.map (to_funcl (names, k_env, def_ord)) funcls), (l,NoTyp)), (names,k_env,def_ord)
-    
-type def_progress =
-    No_def
-  | Def_place_holder of id * Parse_ast.l
-  | Finished of tannot def
-
-type partial_def = ((tannot def) * bool) ref * kind Envmap.t
-
-let rec def_in_progress (id : id) (partial_defs : (id * partial_def) list) : partial_def option =
-  match partial_defs with
-  | [] -> None
-  | (n,pd)::defs -> 
-    (match n,id with
-    | Id_aux(Id(n),_), Id_aux(Id(i),_) -> if (n = i) then Some(pd) else def_in_progress id defs
-    | _,_ -> def_in_progress id defs)
-
-let to_alias_spec k_env def_ord (AL_aux(ae,(le,_))) = 
-  AL_aux(
-    (match ae with
-      | AL_subreg(reg, field) -> AL_subreg(reg, field)
-      | AL_bit(reg,range) -> AL_bit(reg,to_exp k_env def_ord range)
-      | AL_slice(reg,base,stop) ->
-        AL_slice(reg,to_exp k_env def_ord base,to_exp k_env def_ord stop)
-      | AL_concat(first,second) -> AL_concat(first,second)
-    ), (le,NoTyp))
-
-let to_dec (names,k_env,def_ord) (DEC_aux(regdec,(l,_))) =
-  DEC_aux(
-    (match regdec with
-      | DEC_reg(typ,id) ->
-        DEC_reg(to_typ k_env def_ord typ,id)
-      | DEC_alias(id,ae) ->
-        DEC_alias(id,to_alias_spec k_env def_ord ae)
-      | DEC_typ_alias(typ,id,ae) ->
-        DEC_typ_alias(to_typ k_env def_ord typ,id,to_alias_spec k_env def_ord ae)
-    ),(l,NoTyp))
-      
-let to_def (names, k_env, def_ord) partial_defs def : def_progress envs_out * (id * partial_def) list = 
-  let envs = (names,k_env,def_ord) in
-  match def with
-  | DEF_kind(k_def) ->
-    let kd,envs = to_kinddef envs k_def in
-    ((Finished(DEF_kind(kd))),envs),partial_defs
-  | DEF_type(t_def) -> 
-    let td,envs = to_typedef envs t_def in
-    ((Finished(DEF_type(td))),envs),partial_defs
-  | DEF_fundef(f_def) -> 
-    let fd,envs = to_fundef envs f_def in
-    ((Finished(DEF_fundef(fd))),envs),partial_defs
-  | DEF_val(lbind) -> 
-    let lb = to_letbind k_env def_ord lbind in
-    ((Finished(DEF_val(lb))),envs),partial_defs
-  | DEF_spec(val_spec) -> 
-    let vs,envs = to_spec envs val_spec in
-    ((Finished(DEF_spec(vs))),envs),partial_defs
-  | DEF_default(typ_spec) -> 
-    let default,envs = to_default envs typ_spec in
-    ((Finished(DEF_default(default))),envs),partial_defs
-  | DEF_comm c-> ((Finished(DEF_comm c)),envs),partial_defs
-  | DEF_reg_dec(dec) ->
-    let d = to_dec envs dec in
-    ((Finished(DEF_reg_dec(d))),envs),partial_defs
-  | DEF_scattered(SD_aux(sd,(l,_))) ->
-    (match sd with
-    | SD_scattered_function(rec_opt, tannot_opt, effects_opt, id) ->
-      let tannot,k_env',k_local = to_tannot_opt k_env def_ord tannot_opt in
-      let effects_opt = to_effects_opt k_env' effects_opt in
-      (match (def_in_progress id partial_defs) with
-       | None ->
-         let partial_def = ref ((DEF_fundef(FD_aux(FD_function(rec_opt,tannot,effects_opt,[]),(l,NoTyp)))),false) in
-         (No_def,envs),((id,(partial_def,k_local))::partial_defs)
-       | Some(d,k) ->
-         typ_error l
-           "Scattered function definition header name already in use by scattered definition" (Some id) None None)
-    | SD_scattered_funcl(funcl) -> 
-      (match funcl with
-       | FCL_aux(FCL_Funcl(id,_,_),_) -> 
-         (match (def_in_progress id partial_defs) with
-          | None ->
-            typ_error l
-              "Scattered function definition clause does not match any exisiting function definition headers"
-              (Some id) None None
-          | Some(d,k) ->
-            (match !d with
-             | DEF_fundef(FD_aux(FD_function(r,t,e,fcls),fl)),false -> 
-               let funcl = to_funcl (names,Envmap.union k k_env,def_ord) funcl in 
-               d:= DEF_fundef(FD_aux(FD_function(r,t,e,fcls@[funcl]),fl)),false;
-               (No_def,envs),partial_defs
-             | _,true -> typ_error l "Scattered funciton definition clauses extends ended defintion" (Some id) None None
-             | _ -> typ_error l
-                      "Scattered function definition clause matches an existing scattered type definition header"
-                      (Some id) None None)))
-    | SD_scattered_variant(id,naming_scheme_opt,typquant) -> 
-      let name = to_namescm naming_scheme_opt in
-      let typq, k_env',_ = to_typquant k_env typquant in
-      let kind = (match (typquant_to_quantkinds k_env' typq) with
-        | [ ] -> {k = K_Typ}
-        | typs -> {k = K_Lam(typs,{k=K_Typ})}) in
-      (match (def_in_progress id partial_defs) with
-       | None -> let partial_def = ref ((DEF_type(TD_aux(TD_variant(id,name,typq,[],false),(l,NoTyp)))),false) in
-         (Def_place_holder(id,l),
-          (names,Envmap.insert k_env ((id_to_string id),kind),def_ord)),(id,(partial_def,k_env'))::partial_defs
-       | Some(d,k) ->
-         typ_error l "Scattered type definition header name already in use by scattered definition" (Some id) None None)
-    | SD_scattered_unioncl(id,tu) -> 
-      (match (def_in_progress id partial_defs) with
-       | None -> typ_error l
-                   "Scattered type definition clause does not match any existing type definition headers"
-                   (Some id) None None
-       | Some(d,k) ->
-         (match !d with
-          | DEF_type(TD_aux(TD_variant(id,name,typq,arms,false),tl)), false -> 
-            d:= DEF_type(TD_aux(TD_variant(id,name,typq,arms@[to_type_union k def_ord tu],false),tl)),false;
-            (No_def,envs),partial_defs
-          | _,true -> typ_error l "Scattered type definition clause extends ended definition" (Some id) None None
-          | _ -> typ_error l
-                   "Scattered type definition clause matches an existing scattered function definition header"
-                   (Some id) None None))
-    | SD_scattered_end(id) ->
-      (match (def_in_progress id partial_defs) with
-      | None -> typ_error l "Scattered definition end does not match any open scattered definitions" (Some id) None None
-      | Some(d,k) ->
-        (match !d with
-        | (DEF_type(_) as def),false ->
-          d:= (def,true);
-          (No_def,envs),partial_defs
-        | (DEF_fundef(_) as def),false ->
-          d:= (def,true);
-          ((Finished def), envs),partial_defs
-        | _, true -> 
-          typ_error l "Scattered definition ended multiple times" (Some id) None None
-        | _ -> raise (Reporting_basic.err_unreachable l "Something in partial_defs other than fundef and type"))))
-    
-let rec to_defs_helper envs partial_defs = function
-  | [] -> ([],envs,partial_defs)
-  | d::ds  -> let ((d', envs), partial_defs) = to_def envs partial_defs d in
-              let (defs,envs,partial_defs) = to_defs_helper envs partial_defs ds in
-              (match d' with
-              | Finished def -> (def::defs,envs, partial_defs)
-              | No_def -> defs,envs,partial_defs
-              | Def_place_holder(id,l) -> 
-                (match (def_in_progress id partial_defs) with
-                 | None ->
-                   raise
-                     (Reporting_basic.err_unreachable l "Id stored in place holder not retrievable from partial defs")
-                 | Some(d,k) -> 
-                   if (snd !d) 
-                   then (fst !d) :: defs, envs, partial_defs
-                   else typ_error l "Scattered type definition never ended" (Some id) None None))                
-
-let to_checked_ast (default_names : Nameset.t) (kind_env : kind Envmap.t) (def_ord : Ast.order) (Defs(defs)) =
-  let defs,(_,k_env,def_ord),partial_defs = to_defs_helper (default_names,kind_env,def_ord) [] defs in
-  List.iter 
-    (fun (id,(d,k)) -> 
-      (match !d with
-      | (d,false) -> typ_error Parse_ast.Unknown "Scattered definition never ended" (Some id) None None
-      | (_, true) -> ()))
-    partial_defs;
-  (Defs defs),k_env,def_ord
diff --git a/src/process_file.ml b/src/process_file.ml
index 2425a9bb..cecc4f81 100644
--- a/src/process_file.ml
+++ b/src/process_file.ml
@@ -57,7 +57,7 @@ let get_lexbuf fn =
 
 let parse_file (f : string) : Parse_ast.defs =
   let scanbuf = get_lexbuf f in
-  let type_names = 
+  let type_names =
     try
       Pre_parser.file Pre_lexer.token scanbuf
     with
@@ -85,9 +85,6 @@ let parse_file (f : string) : Parse_ast.defs =
 let convert_ast (defs : Parse_ast.defs) : (Type_internal.tannot Ast.defs * kind Envmap.t * Ast.order)=
   Initial_check.to_ast Nameset.empty Type_internal.initial_kind_env (Ast.Ord_aux(Ast.Ord_inc,Parse_ast.Unknown)) defs
 
-let initi_check_ast (defs : Type_internal.tannot Ast.defs) : (Type_internal.tannot Ast.defs * kind Envmap.t * Ast.order)=
-  Initial_check_full_ast.to_checked_ast Nameset.empty Type_internal.initial_kind_env (Ast.Ord_aux(Ast.Ord_inc,Parse_ast.Unknown)) defs
-
 let opt_new_typecheck = ref false
 let opt_just_check = ref false
 let opt_ddump_tc_ast = ref false
diff --git a/src/process_file.mli b/src/process_file.mli
index aa8d3265..6cbc6e48 100644
--- a/src/process_file.mli
+++ b/src/process_file.mli
@@ -42,7 +42,6 @@
 
 val parse_file : string -> Parse_ast.defs
 val convert_ast : Parse_ast.defs -> Type_internal.tannot Ast.defs * Type_internal.kind Type_internal.Envmap.t * Ast.order
-val initi_check_ast : Type_internal.tannot Ast.defs -> Type_internal.tannot Ast.defs * Type_internal.kind Type_internal.Envmap.t * Ast.order
 val check_ast: Type_internal.tannot Ast.defs -> Type_internal.kind Type_internal.Envmap.t -> Ast.order -> Type_internal.tannot Ast.defs * Type_check.envs
 val rewrite_ast: Type_internal.tannot Ast.defs -> Type_internal.tannot Ast.defs
 val rewrite_ast_lem : Type_internal.tannot Ast.defs -> Type_internal.tannot Ast.defs