More forms converting from parse_ast to ast; also removed some annot aux homs for terms that only need locations and not full annotations

11 files changed, 304 insertions, 48 deletions

diff --git a/language/l2.ott b/language/l2.ott
index a20f14ee..8949f098 100644
--- a/language/l2.ott
+++ b/language/l2.ott
@@ -375,7 +375,7 @@ grammar
 
 nexp_constraint :: 'NC_' ::=
   {{ com constraint over kind $[[Nat]]$ }}
-  {{ aux _ annot }} {{ auxparam 'a }}
+  {{ aux _ l }}
   | nexp = nexp'                                :: :: fixed
   | nexp >= nexp'                               :: :: bounded_ge
   | nexp '<=' nexp'                             :: :: bounded_le
@@ -392,20 +392,20 @@ kinded_id :: 'KOpt_' ::=
 
 quant_item :: 'QI_' ::=
   {{ com Either a kinded identifier or a nexp constraint for a typquant }}
-  {{ aux _ annot }} {{ auxparam 'a }}
+  {{ aux _ l }}
   | kinded_id 	  	 	       	      :: :: id {{ com An optionally kinded identifier }}
   | nexp_constraint			      :: :: const {{ com A constraint for this type }}
 
 typquant :: 'TypQ_' ::= 
   {{ com type quantifiers and constraints}}
-  {{ aux _ annot }} {{ auxparam 'a }}
+  {{ aux _ l }}
   | forall quant_item1 , ... , quant_itemn . :: :: tq {{ texlong }}
 % WHY ARE CONSTRAINTS HERE AND NOT IN THE KIND LANGUAGE
   |                           ::  ::  no_forall     {{ com sugar, omitting quantifier and constraints }}
 
 typschm :: 'TypSchm_' ::=
   {{ com type scheme  }}
-  {{ aux _ annot }} {{ auxparam 'a }}
+  {{ aux _ l }}
   |  typquant typ                                                       :: :: ts
 
 
diff --git a/src/_build/reporting_basic.ml b/src/_build/reporting_basic.ml
index a0d53ab0..b3880598 100644
--- a/src/_build/reporting_basic.ml
+++ b/src/_build/reporting_basic.ml
@@ -162,7 +162,7 @@ exception Fatal_error of error
 let err_todo l m = Fatal_error (Err_todo (l, m))
 let err_unreachable l m = Fatal_error (Err_unreachable (l, m))
 let err_general l m = Fatal_error (Err_general (l, m))
-
+let err_typ l m = Fatal_error (Err_type (l,m))
 
 let report_error e = 
   let (m1, verb_pos, pos_l, m2) = dest_err e in
diff --git a/src/_build/reporting_basic.mli b/src/_build/reporting_basic.mli
index 8074695b..462d2394 100644
--- a/src/_build/reporting_basic.mli
+++ b/src/_build/reporting_basic.mli
@@ -97,6 +97,9 @@ val err_general : Parse_ast.l -> string -> exn
 (** [err_unreachable l m] is an abreviatiation for [Fatal_error (Err_unreachable (b, l, m))] *)
 val err_unreachable : Parse_ast.l -> string -> exn
 
+(** [err_typ l m] is an abreviatiation for [Fatal_error (Err_type (l, m))] *)
+val err_typ : Parse_ast.l -> string -> exn
+
 (** Report error should only be used by main to print the error in the end. Everywhere else,
     raising a [Fatal_error] exception is recommended. *)
 val report_error : error -> 'a
diff --git a/src/ast.ml b/src/ast.ml
index 1987056d..356248ac 100644
--- a/src/ast.ml
+++ b/src/ast.ml
@@ -64,7 +64,7 @@ kinded_id_aux =  (* optionally kind-annotated identifier *)
 
 
 type 
-'a nexp_constraint_aux =  (* constraint over kind $_$ *)
+nexp_constraint_aux =  (* constraint over kind $_$ *)
    NC_fixed of nexp * nexp
  | NC_bounded_ge of nexp * nexp
  | NC_bounded_le of nexp * nexp
@@ -88,8 +88,8 @@ kinded_id =
 
 
 type 
-'a nexp_constraint = 
-   NC_aux of 'a nexp_constraint_aux * 'a annot
+nexp_constraint = 
+   NC_aux of nexp_constraint_aux * l
 
 
 type 
@@ -98,9 +98,9 @@ efct =
 
 
 type 
-'a quant_item_aux =  (* Either a kinded identifier or a nexp constraint for a typquant *)
+quant_item_aux =  (* Either a kinded identifier or a nexp constraint for a typquant *)
    QI_id of kinded_id (* An optionally kinded identifier *)
- | QI_const of 'a nexp_constraint (* A constraint for this type *)
+ | QI_const of nexp_constraint (* A constraint for this type *)
 
 
 type 
@@ -117,8 +117,8 @@ order_aux =  (* vector order specifications, of kind $_$ *)
 
 
 type 
-'a quant_item = 
-   QI_aux of 'a quant_item_aux * 'a annot
+quant_item = 
+   QI_aux of quant_item_aux * l
 
 
 type 
@@ -132,8 +132,8 @@ order =
 
 
 type 
-'a typquant_aux =  (* type quantifiers and constraints *)
-   TypQ_tq of ('a quant_item) list
+typquant_aux =  (* type quantifiers and constraints *)
+   TypQ_tq of (quant_item) list
  | TypQ_no_forall (* sugar, omitting quantifier and constraints *)
 
 
@@ -172,8 +172,8 @@ and typ_arg =
 
 
 type 
-'a typquant = 
-   TypQ_aux of 'a typquant_aux * 'a annot
+typquant = 
+   TypQ_aux of typquant_aux * l
 
 
 type 
@@ -182,8 +182,8 @@ lit =
 
 
 type 
-'a typschm_aux =  (* type scheme *)
-   TypSchm_ts of 'a typquant * typ
+typschm_aux =  (* type scheme *)
+   TypSchm_ts of typquant * typ
 
 
 type 
@@ -212,13 +212,13 @@ and 'a fpat =
 
 
 type 
-'a typschm = 
-   TypSchm_aux of 'a typschm_aux * 'a annot
+typschm = 
+   TypSchm_aux of typschm_aux * l
 
 
 type 
 'a letbind_aux =  (* Let binding *)
-   LB_val_explicit of 'a typschm * 'a pat * 'a exp (* value binding, explicit type ('a pat must be total) *)
+   LB_val_explicit of typschm * 'a pat * 'a exp (* value binding, explicit type ('a pat must be total) *)
  | LB_val_implicit of 'a pat * 'a exp (* value binding, implicit type ('a pat must be total) *)
 
 and 'a letbind = 
@@ -298,7 +298,7 @@ rec_opt_aux =  (* Optional recursive annotation for functions *)
 
 type 
 'a tannot_opt_aux =  (* Optional type annotation for functions *)
-   Typ_annot_opt_some of 'a typquant * typ
+   Typ_annot_opt_some of typquant * typ
 
 
 type 
@@ -344,14 +344,14 @@ type
 
 type 
 'a val_spec_aux =  (* Value type specification *)
-   VS_val_spec of 'a typschm * id
+   VS_val_spec of typschm * id
 
 
 type 
 'a type_def_aux =  (* Type definition body *)
-   TD_abbrev of id * naming_scheme_opt * 'a typschm (* type abbreviation *)
- | TD_record of id * naming_scheme_opt * 'a typquant * ((typ * id)) list * bool (* struct type definition *)
- | TD_variant of id * naming_scheme_opt * 'a typquant * ((typ * id)) list * bool (* union type definition *)
+   TD_abbrev of id * naming_scheme_opt * typschm (* type abbreviation *)
+ | TD_record of id * naming_scheme_opt * typquant * ((typ * id)) list * bool (* struct type definition *)
+ | TD_variant of id * naming_scheme_opt * typquant * ((typ * id)) list * bool (* union type definition *)
  | TD_enum of id * naming_scheme_opt * (id) list * bool (* enumeration type definition *)
  | TD_register of id * nexp * nexp * ((index_range * id)) list (* register mutable bitfield type definition *)
 
@@ -364,7 +364,7 @@ type
 type 
 'a default_typing_spec_aux =  (* Default kinding or typing assumption *)
    DT_kind of base_kind * id
- | DT_typ of 'a typschm * id
+ | DT_typ of typschm * id
 
 
 type 
@@ -397,14 +397,14 @@ type
  | DEF_reg_dec of typ * id (* register declaration *)
  | DEF_scattered_function of rec_opt * 'a tannot_opt * 'a effects_opt * id (* scattered function definition header *)
  | DEF_scattered_funcl of 'a funcl (* scattered function definition clause *)
- | DEF_scattered_variant of id * naming_scheme_opt * 'a typquant (* scattered union definition header *)
+ | DEF_scattered_variant of id * naming_scheme_opt * typquant (* scattered union definition header *)
  | DEF_scattered_unioncl of id * typ * id (* scattered union definition member *)
  | DEF_scattered_end of id (* scattered definition end *)
 
 
 type 
 'a ctor_def_aux =  (* Datatype constructor definition clause *)
-   CT_ct of id * 'a typschm
+   CT_ct of id * typschm
 
 
 type 
diff --git a/src/initial_check.ml b/src/initial_check.ml
index 8f474f26..d36999ec 100644
--- a/src/initial_check.ml
+++ b/src/initial_check.ml
@@ -1,7 +1,242 @@
 open Type_internal
 open Ast
 
-type 'a envs = 'a * Nameset.t * kind Kindmap.t * t Typmap.t
+type kind = Type_internal.kind
+type typ = Type_internal.t
 
-let rec to_ast (bound_names : Nameset.t) (kind_env : kind Kindmap.t) (typ_env : t Typmap.t) partial_defs defs =
-  (Defs [])
+type envs = Nameset.t * kind Envmap.t * t Envmap.t
+type 'a envs_out = 'a * envs
+
+let id_to_string (Id_aux(id,l)) =
+  match id with | Id(x) | DeIid(x) -> x
+
+(*placeholder, write in type_internal*)
+let kind_to_string _ = " kind pp place holder "
+
+let typ_error l msg opt_id opt_kind =
+  raise (Reporting_basic.err_typ 
+           l
+           (msg ^
+              (match opt_id, opt_kind with
+              | Some(id),Some(kind) -> (id_to_string id) ^ " of " ^ (kind_to_string kind)
+              | Some(id),None -> ": " ^ (id_to_string id)
+              | None,Some(kind) -> " " ^ (kind_to_string kind)
+              | None,None -> "")))
+                
+let to_ast_id (Parse_ast.Id_aux(id,l)) =
+    Id_aux( (match id with
+             | Parse_ast.Id(x) -> Id(x)
+             | Parse_ast.DeIid(x) -> DeIid(x)) , l)
+
+let to_ast_kind (k_env : kind Envmap.t) (Parse_ast.K_aux(Parse_ast.K_kind(klst),l)) : (Ast.kind * kind) =
+  let to_ast_basic_kind (Parse_ast.BK_aux(k,l')) =
+    match k with
+    | Parse_ast.BK_type -> BK_aux(BK_type,l'), { k = K_Typ}
+    | Parse_ast.BK_nat -> BK_aux(BK_nat,l'), { k = K_Nat }
+    | Parse_ast.BK_order -> BK_aux(BK_order,l'), { k = K_Ord }
+    | Parse_ast.BK_effects -> BK_aux(BK_effects,l'), { k = K_Efct }
+  in
+  match klst with
+  | [] -> raise (Reporting_basic.err_unreachable l "Kind with empty kindlist encountered")
+  | [k] -> let k_ast,k_typ = to_ast_basic_kind k in
+           K_aux(K_kind([k_ast]),l), k_typ
+  | ks -> let k_pairs = List.map to_ast_basic_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
+
+let rec to_ast_typ (k_env : kind Envmap.t) (t: Parse_ast.atyp) : Ast.typ =
+  match t with
+  | Parse_ast.ATyp_aux(t,l) ->
+    Typ_aux( (match t with 
+              | Parse_ast.ATyp_id(id) -> 
+                let id = to_ast_id id in
+                let mk = Envmap.apply k_env (id_to_string id) in
+                (match mk with
+                | Some(k) -> (match k.k with
+                              | K_Typ -> Typ_var id
+                              | K_infer -> k.k <- K_Typ; Typ_var id
+                              | _ -> typ_error l "Required a variable with kind Type, encountered " (Some id) (Some k))
+                | None -> typ_error l "Encountered an unbound variable" (Some id) None)
+              | Parse_ast.ATyp_wild -> Typ_wild
+              | Parse_ast.ATyp_fn(arg,ret,efct) -> Typ_fn( (to_ast_typ k_env arg),
+                                                           (to_ast_typ k_env ret),
+                                                           (to_ast_effects k_env efct))
+              | Parse_ast.ATyp_tup(typs) -> Typ_tup( List.map (to_ast_typ k_env) typs)
+              | Parse_ast.ATyp_app(pid,typs) -> 
+                let id = to_ast_id pid in 
+                let k = Envmap.apply k_env (id_to_string id) in
+                (match k with 
+                | Some({k = K_Lam(args,t)}) -> Typ_app(id,(List.map2 (fun k a -> (to_ast_typ_arg k_env k a)) args typs))
+                | None -> typ_error l "Required a type constructor, encountered an unbound variable" (Some id) None
+                | _ -> typ_error l "Required a type constructor, encountered a base kind variable" (Some id) None)
+              | _ -> typ_error l "Required an item of kind Type, encountered an illegal form for this kind" None None
+    ), l)
+
+and to_ast_nexp (k_env : kind Envmap.t) (n: Parse_ast.atyp) : Ast.nexp =
+  match n with
+  | Parse_ast.ATyp_aux(t,l) ->
+    (match t with
+    | Parse_ast.ATyp_id(id) ->                 
+                let id = to_ast_id id in
+                let mk = Envmap.apply k_env (id_to_string id) in
+                (match mk with
+                | Some(k) -> Nexp_aux((match k.k with
+                                      | K_Nat -> Nexp_id id
+                                      | K_infer -> k.k <- K_Nat; Nexp_id id
+                                      | _ -> typ_error l "Required a variable with kind Nat, encountered " (Some id) (Some k)),l)
+                | None -> typ_error l "Encountered an unbound variable" (Some id) None)
+    | Parse_ast.ATyp_constant(i) -> Nexp_aux(Nexp_constant(i),l)
+    | Parse_ast.ATyp_sum(t1,t2) ->
+      let n1 = to_ast_nexp k_env t1 in
+      let n2 = to_ast_nexp k_env t2 in
+      Nexp_aux(Nexp_sum(n1,n2),l)
+    | Parse_ast.ATyp_exp(t1) -> Nexp_aux(Nexp_exp(to_ast_nexp k_env t1),l)
+    | Parse_ast.ATyp_tup(typs) ->
+      let rec times_loop (typs : Parse_ast.atyp list) (one_ok : bool) : nexp =
+        (match typs,one_ok with
+        | [],_ | [_],false -> raise (Reporting_basic.err_unreachable l "to_ast_nexp has ATyp_tup with empty list or list with one element")
+        | [t],true -> to_ast_nexp k_env t
+        | (t1::typs),_ -> let n1 = to_ast_nexp k_env t1 in
+                          let n2 = times_loop typs true in 
+                          (Nexp_aux((Nexp_times(n1,n2)),l)))  (*TODO This needs just a portion of the l, think about adding a way to split*)
+      in
+      times_loop typs false
+    | _ -> typ_error l "Requred an item of kind Nat, encountered an illegal form for this kind" None None)
+    
+and to_ast_order (k_env : kind Envmap.t) (o: Parse_ast.atyp) : Ast.order =
+  match o with
+  | Parse_ast.ATyp_aux(t,l) ->
+    Ord_aux( (match t with
+               | Parse_ast.ATyp_id(id) -> 
+                let id = to_ast_id id in
+                let mk = Envmap.apply k_env (id_to_string id) in
+                (match mk with
+                | Some(k) -> (match k.k with
+                              | K_Ord -> Ord_id id
+                              | K_infer -> k.k <- K_Ord; Ord_id id
+                              | _ -> typ_error l "Required a variable with kind Order, encountered " (Some id) (Some k))
+                | None -> typ_error l "Encountered an unbound variable" (Some id) None)
+               | Parse_ast.ATyp_inc -> Ord_inc
+               | Parse_ast.ATyp_dec -> Ord_dec
+               | _ -> typ_error l "Requred an item of kind Order, encountered an illegal form for this kind" None None
+    ), l)
+
+and to_ast_effects (k_env : kind Envmap.t) (e : Parse_ast.atyp) : Ast.effects =
+  match e with
+  | Parse_ast.ATyp_aux(t,l) ->
+    Effects_aux( (match t with
+               | Parse_ast.ATyp_efid(id) ->  
+                let id = to_ast_id id in
+                let mk = Envmap.apply k_env (id_to_string id) in
+                (match mk with
+                | Some(k) -> (match k.k with
+                              | K_Efct -> Effects_var id
+                              | K_infer -> k.k <- K_Efct; Effects_var id
+                              | _ -> typ_error l "Required a variable with kind Effect, encountered " (Some id) (Some k))
+                | None -> typ_error l "Encountered an unbound variable" (Some id) None)
+               | Parse_ast.ATyp_set(effects) ->
+                 Effects_set( List.map 
+                             (fun efct -> match efct with
+                             | Parse_ast.Effect_aux(e,l) ->
+                               Effect_aux((match e with 
+                               | Parse_ast.Effect_rreg -> Effect_rreg
+                               | Parse_ast.Effect_wreg -> Effect_wreg
+                               | Parse_ast.Effect_rmem -> Effect_rmem
+                               | Parse_ast.Effect_wmem -> Effect_wmem
+                               | Parse_ast.Effect_undef -> Effect_undef
+                               | Parse_ast.Effect_unspec -> Effect_unspec
+                               | Parse_ast.Effect_nondet -> Effect_nondet),l))
+                             effects)
+               | _ -> typ_error l "Required an item of kind Effects, encountered an illegal form for this kind" None None
+    ), l)
+
+and to_ast_typ_arg (k_env : kind Envmap.t) (kind : kind) (arg : Parse_ast.atyp) : Ast.typ_arg =
+  let l = (match arg with Parse_ast.ATyp_aux(_,l) -> l) in
+  Typ_arg_aux (  
+    (match kind.k with 
+    | K_Typ -> Typ_arg_typ (to_ast_typ k_env arg)
+    | K_Nat  -> Typ_arg_nexp (to_ast_nexp k_env arg)
+    | K_Ord -> Typ_arg_order (to_ast_order k_env arg)
+    | K_Efct -> Typ_arg_effects (to_ast_effects k_env arg)
+    | _ -> raise (Reporting_basic.err_unreachable l "To_ast_typ_arg received Lam kind or infer kind")),
+    l)
+
+let to_ast_nexp_constraint (k_env : kind Envmap.t) (c : Parse_ast.nexp_constraint) : nexp_constraint =
+  match c with 
+  | Parse_ast.NC_aux(nc,l) ->
+    NC_aux( (match nc with
+             | Parse_ast.NC_fixed(t1,t2) -> 
+               let n1 = to_ast_nexp k_env t1 in
+               let n2 = to_ast_nexp k_env t2 in
+               NC_fixed(n1,n2)
+             | Parse_ast.NC_bounded_ge(t1,t2) ->
+               let n1 = to_ast_nexp k_env t1 in
+               let n2 = to_ast_nexp k_env t2 in
+               NC_bounded_ge(n1,n2)
+             | Parse_ast.NC_bounded_le(t1,t2) ->
+               let n1 = to_ast_nexp k_env t1 in
+               let n2 = to_ast_nexp k_env t2 in
+               NC_bounded_le(n1,n2)
+             | Parse_ast.NC_nat_set_bounded(id,bounds) ->
+               NC_nat_set_bounded(to_ast_id id, bounds)
+    ), l)               
+
+let to_ast_typquant (k_env: kind Envmap.t) (tq : Parse_ast.typquant) : typquant * kind Envmap.t =
+  assert false
+
+let to_ast_typschm (k_env : kind Envmap.t) (tschm : Parse_ast.typschm) : Ast.typschm =
+  match tschm with
+  | Parse_ast.TypSchm_aux(ts,l) -> 
+    (match ts with | Parse_ast.TypSchm_ts(tquant,t) ->
+      let tq,k_env = to_ast_typquant k_env tquant in
+      let typ = to_ast_typ k_env t in
+      TypSchm_aux(TypSchm_ts(tq,typ),l))
+
+(*
+type 
+def_aux =  (* Top-level definition *)
+   DEF_type of type_def (* type definition *)
+ | DEF_fundef of fundef (* function definition *)
+ | DEF_val of letbind (* value definition *)
+ | DEF_spec of val_spec (* top-level type constraint *)
+ | DEF_default of default_typing_spec (* default kind and type assumptions *)
+ | DEF_reg_dec of atyp * id (* register declaration *)
+ | DEF_scattered_function of rec_opt * tannot_opt * effects_opt * id (* scattered function definition header *)
+ | DEF_scattered_funcl of funcl (* scattered function definition clause *)
+ | DEF_scattered_variant of id * naming_scheme_opt * typquant (* scattered union definition header *)
+ | DEF_scattered_unioncl of id * atyp * id (* scattered union definition member *)
+ | DEF_scattered_end of id (* scattered definition end *)
+
+
+type 
+def = 
+   DEF_aux of def_aux * l *)
+
+let to_ast_def (names, k_env, t_env) partial_defs def : ((tannot def) option) envs_out * (tannot def) list = 
+  match def with
+  | Parse_ast.DEF_aux(d,l) ->
+    (match d with
+    | Parse_ast.DEF_type(t_def) -> assert false
+    | Parse_ast.DEF_fundef(f_def) -> assert false
+    | Parse_ast.DEF_val(lbind) -> assert false
+    | Parse_ast.DEF_spec(val_spec) -> assert false
+    | Parse_ast.DEF_default(typ_spec) -> assert false
+    )
+
+
+let rec to_ast_defs_helper envs partial_defs = function
+  | [] -> ([],envs,partial_defs)
+  | d::ds  -> let ((d', envs), partial_defs) = to_ast_def envs partial_defs d in
+              match d' with
+              | Some def -> let (defs, envs, p_defs) = to_ast_defs_helper envs partial_defs ds in 
+                            (def::defs,envs, partial_defs)
+              | None -> to_ast_defs_helper envs partial_defs ds
+                
+
+let to_ast (bound_names : Nameset.t) (kind_env : kind Envmap.t) (typ_env : t Envmap.t) (Parse_ast.Defs(defs)) =
+  let defs,_,partial_defs = to_ast_defs_helper (bound_names,kind_env,typ_env) [] defs in
+  (* (Defs defs) *) (*TODO there will be type defs in partial defs that need to replace "placeholders" in the def list *)
+  (Defs [ ] ) (* Until not all forms return assert false *)
diff --git a/src/initial_check.mli b/src/initial_check.mli
index 39b955b5..03b34e78 100644
--- a/src/initial_check.mli
+++ b/src/initial_check.mli
@@ -1,14 +1,10 @@
 
-open Type_internal
 open Ast
+open Type_internal
+type kind = Type_internal.kind
+type typ = Type_internal.t
 
-type 'a envs = 'a * Nameset.t * kind Kindmap.t * t Typmap.t
+type envs = Nameset.t * kind Envmap.t * typ Envmap.t
+type 'a envs_out = 'a * envs
 
-val to_ast : Nameset.t -> kind Kindmap.t -> t Typmap.t -> tannot def list -> Parse_ast.defs -> tannot defs
-(*val to_ast_def : nameset -> kind kindmap -> t typmap -> tannot def list -> Parse_ast.defs -> (annot def) envs * annot def list
-val to_ast_fun : nameset -> kind kindmap -> t typmap -> Parse_ast.fundef -> (annot fundef) envs
-val to_ast_expr : nameset -> kind kindmap -> t typmap -> Parse_ast.exp -> (annot exp) envs
-val to_ast_targ : nameset -> kind kindmap -> t typmap -> Parse_ast.atyp -> (annot typ_arg) envs
-val to_ast_typ : nameset -> kind kindmap -> t typmap -> Parse_ast.atyp -> (annot typ) envs
-val to_ast_nexp : nameset -> kind kindmap -> t typmap -> Parse_ast.atyp -> (annot nexp) envs
-*)
+val to_ast : Nameset.t -> kind Envmap.t -> typ Envmap.t -> Parse_ast.defs -> tannot defs
diff --git a/src/process_file.ml b/src/process_file.ml
index 8c996c14..d3b5604b 100644
--- a/src/process_file.ml
+++ b/src/process_file.ml
@@ -70,7 +70,7 @@ let parse_file (f : string) : Parse_ast.defs =
           raise (Reporting_basic.Fatal_error (Reporting_basic.Err_lex (p, s)))
 
 let convert_ast (defs : Parse_ast.defs) : Type_internal.tannot Ast.defs =
-  Initial_check.to_ast Nameset.empty Kindmap.empty Typmap.empty [] defs
+  Initial_check.to_ast Nameset.empty Envmap.empty Envmap.empty defs
 
 (* type instances = Types.instance list Types.Pfmap.t
 
diff --git a/src/reporting_basic.ml b/src/reporting_basic.ml
index a0d53ab0..b3880598 100644
--- a/src/reporting_basic.ml
+++ b/src/reporting_basic.ml
@@ -162,7 +162,7 @@ exception Fatal_error of error
 let err_todo l m = Fatal_error (Err_todo (l, m))
 let err_unreachable l m = Fatal_error (Err_unreachable (l, m))
 let err_general l m = Fatal_error (Err_general (l, m))
-
+let err_typ l m = Fatal_error (Err_type (l,m))
 
 let report_error e = 
   let (m1, verb_pos, pos_l, m2) = dest_err e in
diff --git a/src/reporting_basic.mli b/src/reporting_basic.mli
index 8074695b..462d2394 100644
--- a/src/reporting_basic.mli
+++ b/src/reporting_basic.mli
@@ -97,6 +97,9 @@ val err_general : Parse_ast.l -> string -> exn
 (** [err_unreachable l m] is an abreviatiation for [Fatal_error (Err_unreachable (b, l, m))] *)
 val err_unreachable : Parse_ast.l -> string -> exn
 
+(** [err_typ l m] is an abreviatiation for [Fatal_error (Err_type (l, m))] *)
+val err_typ : Parse_ast.l -> string -> exn
+
 (** Report error should only be used by main to print the error in the end. Everywhere else,
     raising a [Fatal_error] exception is recommended. *)
 val report_error : error -> 'a
diff --git a/src/type_internal.ml b/src/type_internal.ml
index 8b68934e..c4d6ecbc 100644
--- a/src/type_internal.ml
+++ b/src/type_internal.ml
@@ -1,4 +1,4 @@
-module Kindmap = Finite_map.Fmap_map(String)
+module Envmap = Finite_map.Fmap_map(String)
 module Nameset' = Set.Make(String)
 module Nameset = struct
   include Nameset'
@@ -8,7 +8,15 @@ module Nameset = struct
       (Nameset'.elements nameset)
 end
 
-module Typmap = Finite_map.Fmap_map(String)
+type kind = { mutable k : k_aux }
+and k_aux =
+  | K_Typ
+  | K_Nat
+  | K_Ord
+  | K_Efct
+  | K_Val
+  | K_Lam of kind list * kind
+  | K_infer
 
 type t = { mutable t : t_aux }
 and t_aux =
@@ -55,3 +63,4 @@ type nexp_range =
   | In of Parse_ast.l * nexp * nexp list
 
 type tannot = (t * nexp_range list) option
+
diff --git a/src/type_internal.mli b/src/type_internal.mli
index cfa12a75..1857b007 100644
--- a/src/type_internal.mli
+++ b/src/type_internal.mli
@@ -1,10 +1,20 @@
-module Kindmap : Finite_map.Fmap with type k = string
-module Typmap : Finite_map.Fmap with type k = string
+module Envmap : Finite_map.Fmap with type k = string
 module Nameset : sig
   include Set.S with type elt = string
   val pp : Format.formatter -> t -> unit
 end
 
+
+type kind = { mutable k : k_aux }
+and k_aux =
+  | K_Typ
+  | K_Nat
+  | K_Ord
+  | K_Efct
+  | K_Val
+  | K_Lam of kind list * kind
+  | K_infer
+
 type t_uvar
 type n_uvar
 type e_uvar