more translation from parse_ast to ast

1 files changed, 131 insertions, 19 deletions

diff --git a/src/initial_check.ml b/src/initial_check.ml
index d36999ec..a2f3f64c 100644
--- a/src/initial_check.ml
+++ b/src/initial_check.ml
@@ -13,6 +13,8 @@ let id_to_string (Id_aux(id,l)) =
 (*placeholder, write in type_internal*)
 let kind_to_string _ = " kind pp place holder "
 
+let typquant_to_quantids k_env typquant = []
+
 let typ_error l msg opt_id opt_kind =
   raise (Reporting_basic.err_typ 
            l
@@ -28,19 +30,19 @@ let to_ast_id (Parse_ast.Id_aux(id,l)) =
              | Parse_ast.Id(x) -> Id(x)
              | Parse_ast.DeIid(x) -> DeIid(x)) , l)
 
+let to_ast_base_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 }
+
 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] -> let k_ast,k_typ = to_ast_base_kind k in
            K_aux(K_kind([k_ast]),l), k_typ
-  | ks -> let k_pairs = List.map to_ast_basic_kind ks in
+  | ks -> let k_pairs = List.map to_ast_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
@@ -185,7 +187,52 @@ let to_ast_nexp_constraint (k_env : kind Envmap.t) (c : Parse_ast.nexp_constrain
     ), l)               
 
 let to_ast_typquant (k_env: kind Envmap.t) (tq : Parse_ast.typquant) : typquant * kind Envmap.t =
-  assert false
+  let opt_kind_to_ast k_env local_names (Parse_ast.KOpt_aux(ki,l)) =
+    let id, key, kind, ktyp =
+      match ki with
+      | Parse_ast.KOpt_none(id) ->
+	let id = to_ast_id id in
+	let key = id_to_string id 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
+	id,key,kind, ktyp
+      | Parse_ast.KOpt_kind(k,id) ->
+	let id = to_ast_id id in
+	let key = id_to_string id in
+	let kind,ktyp = to_ast_kind k_env k in
+	id,key,Some(kind),Some(ktyp)
+    in
+    if (Nameset.mem key local_names)
+    then typ_error l "Encountered duplicate name in type scheme" (Some id) None
+    else 
+      let local_names = Nameset.add key local_names in
+      let kopt,k_env = (match kind,ktyp with
+        | Some(k),Some(kt) -> KOpt_kind(k,id), (Envmap.insert k_env (key,kt))
+	| None, Some(kt) -> KOpt_none(id), (Envmap.insert k_env (key,kt))
+	| _ -> raise (Reporting_basic.err_unreachable l "Envmap in dom true but apply gives None")) in
+      KOpt_aux(kopt,l),k_env,local_names
+  in
+  match tq with
+  | Parse_ast.TypQ_aux(tqa,l) ->
+    (match tqa with
+    | Parse_ast.TypQ_no_forall -> TypQ_aux(TypQ_no_forall,l), k_env
+    | Parse_ast.TypQ_tq(qlist) ->
+      let rec to_ast_q_items k_env local_names = function
+	| [] -> [],k_env
+	| q::qs -> (match q with
+	            | Parse_ast.QI_aux(qi,l) ->
+		      (match qi with
+		      | Parse_ast.QI_const(n_const) -> 
+			let c = QI_aux(QI_const(to_ast_nexp_constraint k_env n_const),l) in
+			let qis,k_env = to_ast_q_items k_env local_names qs in
+			(c::qis),k_env
+		      | Parse_ast.QI_id(kid) ->
+			let kid,k_env,local_names = opt_kind_to_ast k_env local_names kid in
+			let c = QI_aux(QI_id(kid),l) in
+			let qis,k_env = to_ast_q_items k_env local_names qs in
+			(c::qis),k_env))	
+      in
+      let lst,k_env = to_ast_q_items k_env Nameset.empty qlist in
+      TypQ_aux(TypQ_tq(lst),l), k_env)
 
 let to_ast_typschm (k_env : kind Envmap.t) (tschm : Parse_ast.typschm) : Ast.typschm =
   match tschm with
@@ -195,7 +242,67 @@ let to_ast_typschm (k_env : kind Envmap.t) (tschm : Parse_ast.typschm) : Ast.typ
       let typ = to_ast_typ k_env t in
       TypSchm_aux(TypSchm_ts(tq,typ),l))
 
+let to_ast_default (names, k_env, t_env) (default : Parse_ast.default_typing_spec) : (tannot default_typing_spec) envs_out =
+  match default with
+  | Parse_ast.DT_aux(df,l) ->
+    (match df with 
+    | Parse_ast.DT_kind(bk,id) ->
+      let k,k_typ = to_ast_base_kind bk in
+      let id = to_ast_id id in
+      let key = id_to_string id in
+      DT_aux(DT_kind(k,id),(l,None)),(names,(Envmap.insert k_env (key,k_typ)),t_env)
+    | Parse_ast.DT_typ(typschm,id) ->
+      let tps = to_ast_typschm k_env typschm in
+      DT_aux(DT_typ(tps,to_ast_id id),(l,None)),(names,k_env,t_env) (* Does t_env need to be updated here in this pass? *)
+    )
+
+let to_ast_spec (names,k_env,t_env) (val_:Parse_ast.val_spec) : (tannot val_spec) envs_out =
+  match val_ with
+  | Parse_ast.VS_aux(vs,l) ->
+    (match vs with
+    | Parse_ast.VS_val_spec(ts,id) ->
+      VS_aux(VS_val_spec(to_ast_typschm k_env ts,to_ast_id id),(l,None)),(names,k_env,t_env)) (*Do names and t_env need updating this pass? *)
+
+let to_ast_namescm name_scm_opt = assert false
+
+let to_ast_typedef (names,k_env,t_env) (td:Parse_ast.type_def) : (tannot type_def) envs_out =
+  match td with
+  | Parse_ast.TD_aux(td,l) ->
+  (match td with 
+  | Parse_ast.TD_abbrev(id,name_scm_opt,typschm) ->
+    let id = to_ast_id id in
+    let name_scm_opt = to_ast_namescm name_scm_opt in
+    let key = id_to_string id in
+    let typschm = to_ast_typschm k_env typschm in
+(*    match typschm with 
+    | TypSchm_aux(TypSchm_no_forall,_) -> 
+      TD_aux(TD_abbrev(id,name_scm_opt,typschm),(l,None)),(names,Envmap.insert (key,{k = K_Typ}) k_env,t_env) 
+    | TypSchm_aux(TypSchm_ts(tq,typ), _) *)
+      assert false
+  | Parse_ast.TD_record(id,name_scm_opt,typq,fields,_) -> assert false
+  | Parse_ast.TD_variant(id,name_scm_opt,typq,arms,_) -> assert false
+  | Parse_ast.TD_enum(id,name_scm_opt,enums,_) -> assert false
+  | Parse_ast.TD_register(id,t1,t2,ranges) -> assert false)
+
+(*
+
+type 
+type_def = 
+   TD_aux of type_def_aux * l
+
+type 
+type_def_aux =  (* Type definition body *)
+   TD_abbrev of id * naming_scheme_opt * typschm (* type abbreviation *)
+ | TD_record of id * naming_scheme_opt * typquant * ((atyp * id)) list * bool (* struct type definition *)
+ | TD_variant of id * naming_scheme_opt * typquant * ((atyp * id)) list * bool (* union type definition *)
+ | TD_enum of id * naming_scheme_opt * (id) list * bool (* enumeration type definition *)
+ | TD_register of id * atyp * atyp * ((index_range * id)) list (* register mutable bitfield type definition *)
+
+
+*)
+
 (*
+
 type 
 def_aux =  (* Top-level definition *)
    DEF_type of type_def (* type definition *)
@@ -209,21 +316,26 @@ def_aux =  (* Top-level definition *)
  | 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 = 
+  let envs = (names,k_env,t_env) in
   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
+    | Parse_ast.DEF_spec(val_spec) -> 
+      let vs,envs = to_ast_spec envs val_spec in
+      ((Some(DEF_aux(DEF_spec(vs),(l,None)))),envs),partial_defs
+    | Parse_ast.DEF_default(typ_spec) -> 
+      let default,envs = to_ast_default envs typ_spec in
+      ((Some(DEF_aux(DEF_default(default),(l,None)))),envs),partial_defs
+    | Parse_ast.DEF_reg_dec(typ,id) ->
+      let t = to_ast_typ k_env typ in
+      let id = to_ast_id id in
+      ((Some(DEF_aux(DEF_reg_dec(t,id),(l,None)))),envs),partial_defs (*If tracking types here, update tenv and None*)
     )
 
 
@@ -236,7 +348,7 @@ let rec to_ast_defs_helper envs partial_defs = function
               | 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
+let to_ast (default_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 (default_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 *)