diff options
Diffstat (limited to 'src/initial_check.ml')
| -rw-r--r-- | src/initial_check.ml | 573 |
1 files changed, 343 insertions, 230 deletions
diff --git a/src/initial_check.ml b/src/initial_check.ml index 632e70ca..d5502d63 100644 --- a/src/initial_check.ml +++ b/src/initial_check.ml @@ -48,14 +48,45 @@ (* SUCH DAMAGE. *) (**************************************************************************) -open Type_internal open Ast +open Util +open Ast_util +module Big_int = Nat_big_num -type kind = Type_internal.kind -type typ = Type_internal.t +let opt_undefined_gen = ref false +let opt_magic_hash = ref false + +module Envmap = Finite_map.Fmap_map(String) +module Nameset' = Set.Make(String) +module Nameset = struct + include Nameset' + let pp ppf nameset = + Format.fprintf ppf "{@[%a@]}" + (Pp.lst ",@ " Pp.pp_str) + (Nameset'.elements nameset) +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 + +let rec kind_to_string kind = match kind.k with + | K_Nat -> "Nat" + | K_Typ -> "Type" + | K_Ord -> "Order" + | K_Efct -> "Effect" + | K_infer -> "Infer" + | K_Val -> "Val" + | K_Lam (kinds,kind) -> "Lam [" ^ string_of_list ", " kind_to_string kinds ^ "] -> " ^ (kind_to_string kind) (*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 * order +type envs = Nameset.t * kind Envmap.t * order type 'a envs_out = 'a * envs let id_to_string (Id_aux(id,l)) = @@ -94,11 +125,22 @@ let typ_error l msg opt_id opt_var opt_kind = | None,Some(v),None -> ": " ^ (var_to_string v) | None,None,Some(kind) -> " " ^ (kind_to_string kind) | _ -> ""))) - -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 string_of_parse_id_aux = function + | Parse_ast.Id v -> v + | Parse_ast.DeIid v -> v + +let string_contains str char = + try (String.index str char; true) with + | Not_found -> false + +let to_ast_id (Parse_ast.Id_aux(id, l)) = + if string_contains (string_of_parse_id_aux id) '#' && not (!opt_magic_hash) + then typ_error l "Identifier contains hash character" None None None + else Id_aux ((match id with + | Parse_ast.Id(x) -> Id(x) + | Parse_ast.DeIid(x) -> DeIid(x)), + l) let to_ast_var (Parse_ast.Kid_aux(Parse_ast.Var v,l)) = Kid_aux(Var v,l) @@ -107,7 +149,6 @@ let to_ast_base_kind (Parse_ast.BK_aux(k,l')) = | 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_effect -> BK_aux(BK_effect,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) = match klst with @@ -126,16 +167,8 @@ let rec to_ast_typ (k_env : kind Envmap.t) (def_ord : order) (t: Parse_ast.atyp) 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_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) - | Parse_ast.ATyp_var(v) -> + | Parse_ast.ATyp_id(id) -> Typ_id (to_ast_id id) + | Parse_ast.ATyp_var(v) -> let v = to_ast_var v in let mk = Envmap.apply k_env (var_to_string v) in (match mk with @@ -152,12 +185,12 @@ let rec to_ast_typ (k_env : kind Envmap.t) (def_ord : order) (t: Parse_ast.atyp) let make_r bot top = match bot,top with | Parse_ast.ATyp_aux(Parse_ast.ATyp_constant b,_),Parse_ast.ATyp_aux(Parse_ast.ATyp_constant t,l) -> - Parse_ast.ATyp_aux(Parse_ast.ATyp_constant ((t-b)+1),l) + Parse_ast.ATyp_aux(Parse_ast.ATyp_constant (Big_int.add (Big_int.sub t b) (Big_int.of_int 1)),l) | bot,(Parse_ast.ATyp_aux(_,l) as top) -> Parse_ast.ATyp_aux((Parse_ast.ATyp_sum ((Parse_ast.ATyp_aux (Parse_ast.ATyp_sum (top, - Parse_ast.ATyp_aux(Parse_ast.ATyp_constant 1,Parse_ast.Unknown)), + Parse_ast.ATyp_aux(Parse_ast.ATyp_constant (Big_int.of_int 1),Parse_ast.Unknown)), Parse_ast.Unknown)), (Parse_ast.ATyp_aux ((Parse_ast.ATyp_neg bot),Parse_ast.Unknown)))), l) in let base = to_ast_nexp k_env b in @@ -173,9 +206,9 @@ let rec to_ast_typ (k_env : kind Envmap.t) (def_ord : order) (t: Parse_ast.atyp) | Parse_ast.ATyp_app(Parse_ast.Id_aux(Parse_ast.Id "vector_sugar_r",il), [b;r;ord;ti]) -> let make_sub_one t = match t with - | Parse_ast.ATyp_aux(Parse_ast.ATyp_constant t,_) -> Parse_ast.ATyp_aux(Parse_ast.ATyp_constant (t-1),l) + | Parse_ast.ATyp_aux(Parse_ast.ATyp_constant t,_) -> Parse_ast.ATyp_aux(Parse_ast.ATyp_constant (Big_int.sub t (Big_int.of_int 1)),l) | t -> (Parse_ast.ATyp_aux - (Parse_ast.ATyp_sum (t, Parse_ast.ATyp_aux(Parse_ast.ATyp_constant (-1),Parse_ast.Unknown)), + (Parse_ast.ATyp_sum (t, Parse_ast.ATyp_aux(Parse_ast.ATyp_constant (Big_int.negate (Big_int.of_int 1)),Parse_ast.Unknown)), Parse_ast.Unknown)) in let (base,rise) = match def_ord with | Ord_aux(Ord_inc,dl) -> (to_ast_nexp k_env b), (to_ast_nexp k_env r) @@ -197,53 +230,40 @@ let rec to_ast_typ (k_env : kind Envmap.t) (def_ord : order) (t: Parse_ast.atyp) 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) + | Parse_ast.ATyp_exist (kids, nc, atyp) -> + let kids = List.map to_ast_var kids in + let k_env = List.fold_left Envmap.insert k_env (List.map (fun kid -> (var_to_string kid, {k=K_Nat})) kids) in + let exist_typ = to_ast_typ k_env def_ord atyp in + Typ_exist (kids, to_ast_nexp_constraint k_env nc, exist_typ) | _ -> typ_error l "Required an item of kind Type, encountered an illegal form for this kind" None None None ), l) and to_ast_nexp (k_env : kind Envmap.t) (n: Parse_ast.atyp) : Ast.nexp = - (*let _ = Printf.eprintf "to_ast_nexp\n" in*) match n with | Parse_ast.ATyp_aux(t,l) -> (match t with - | Parse_ast.ATyp_id(i) -> - let i = to_ast_id i in - let v = id_to_string i in - let mk = Envmap.apply k_env v 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 an identifier with kind Nat, encountered " (Some i) None (Some k)),l) - | None -> typ_error l "Encountered an unbound variable" (Some i) None None) - | Parse_ast.ATyp_var(v) -> - let v = to_ast_var v in - let mk = Envmap.apply k_env (var_to_string v) in - (*let _ = - Envmap.iter (fun v' k -> Printf.eprintf "%s -> %s, %s =? %b\n" - v' (kind_to_string k) (var_to_string v) ((var_to_string v) = v') ) k_env 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) - | 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_neg(t1) -> Nexp_aux(Nexp_neg(to_ast_nexp k_env t1),l) - | Parse_ast.ATyp_times(t1,t2) -> - let n1 = to_ast_nexp k_env t1 in - let n2 = to_ast_nexp k_env t2 in - Nexp_aux(Nexp_times(n1,n2),l) - | Parse_ast.ATyp_minus(t1,t2) -> - let n1 = to_ast_nexp k_env t1 in - let n2 = to_ast_nexp k_env t2 in - Nexp_aux(Nexp_minus(n1,n2),l) - | _ -> typ_error l "Requred an item of kind Nat, encountered an illegal form for this kind" None None None) - + | Parse_ast.ATyp_id i -> Nexp_aux (Nexp_id (to_ast_id i), l) + | Parse_ast.ATyp_var v -> Nexp_aux (Nexp_var (to_ast_var v), l) + | 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_neg t1 -> Nexp_aux(Nexp_neg(to_ast_nexp k_env t1),l) + | Parse_ast.ATyp_times (t1, t2) -> + let n1 = to_ast_nexp k_env t1 in + let n2 = to_ast_nexp k_env t2 in + Nexp_aux (Nexp_times (n1, n2), l) + | Parse_ast.ATyp_minus (t1, t2) -> + let n1 = to_ast_nexp k_env t1 in + let n2 = to_ast_nexp k_env t2 in + Nexp_aux (Nexp_minus (n1, n2), l) + | Parse_ast.ATyp_app (id, ts) -> + let nexps = List.map (to_ast_nexp k_env) ts in + Nexp_aux (Nexp_app (to_ast_id id, nexps), l) + | _ -> typ_error l "Required an item of kind Nat, encountered an illegal form for this kind" None None None) + and to_ast_order (k_env : kind Envmap.t) (def_ord : order) (o: Parse_ast.atyp) : Ast.order = match o with | Parse_ast.ATyp_aux(t,l) -> @@ -271,10 +291,7 @@ and to_ast_effects (k_env : kind Envmap.t) (e : Parse_ast.atyp) : Ast.effect = let v = to_ast_var v in 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)) + | Some k -> 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) | Parse_ast.ATyp_set(effects) -> Effect_set( List.map @@ -307,18 +324,21 @@ and to_ast_typ_arg (k_env : kind Envmap.t) (def_ord : order) (kind : kind) (arg | K_Typ -> Typ_arg_typ (to_ast_typ k_env def_ord arg) | K_Nat -> Typ_arg_nexp (to_ast_nexp k_env arg) | K_Ord -> Typ_arg_order (to_ast_order k_env def_ord arg) - | K_Efct -> Typ_arg_effect (to_ast_effects k_env arg) - | _ -> raise (Reporting_basic.err_unreachable l "To_ast_typ_arg received Lam kind or infer kind")), + | _ -> raise (Reporting_basic.err_unreachable l ("To_ast_typ_arg received Lam kind or infer kind: " ^ kind_to_string kind))), l) -let to_ast_nexp_constraint (k_env : kind Envmap.t) (c : Parse_ast.n_constraint) : n_constraint = - match c with +and to_ast_nexp_constraint (k_env : kind Envmap.t) (c : Parse_ast.n_constraint) : n_constraint = + match c with | Parse_ast.NC_aux(nc,l) -> NC_aux( (match nc with - | Parse_ast.NC_fixed(t1,t2) -> + | Parse_ast.NC_equal(t1,t2) -> let n1 = to_ast_nexp k_env t1 in let n2 = to_ast_nexp k_env t2 in - NC_fixed(n1,n2) + NC_equal(n1,n2) + | Parse_ast.NC_not_equal(t1,t2) -> + let n1 = to_ast_nexp k_env t1 in + let n2 = to_ast_nexp k_env t2 in + NC_not_equal(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 @@ -327,9 +347,15 @@ let to_ast_nexp_constraint (k_env : kind Envmap.t) (c : Parse_ast.n_constraint) 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_var id, bounds) - ), l) + | Parse_ast.NC_set(id,bounds) -> + NC_set(to_ast_var id, bounds) + | Parse_ast.NC_or (nc1, nc2) -> + NC_or (to_ast_nexp_constraint k_env nc1, to_ast_nexp_constraint k_env nc2) + | Parse_ast.NC_and (nc1, nc2) -> + NC_and (to_ast_nexp_constraint k_env nc1, to_ast_nexp_constraint k_env nc2) + | Parse_ast.NC_true -> NC_true + | Parse_ast.NC_false -> NC_false + ), l) (* Transforms a typquant while building first the kind environment of declared variables, and also the kind environment in context *) let to_ast_typquant (k_env: kind Envmap.t) (tq : Parse_ast.typquant) : typquant * kind Envmap.t * kind Envmap.t = @@ -400,10 +426,11 @@ let to_ast_lit (Parse_ast.L_aux(lit,l)) : lit = | Parse_ast.L_num(i) -> L_num(i) | Parse_ast.L_hex(h) -> L_hex(h) | Parse_ast.L_bin(b) -> L_bin(b) + | Parse_ast.L_real r -> L_real r | Parse_ast.L_string(s) -> L_string(s)) ,l) -let rec to_ast_pat (k_env : kind Envmap.t) (def_ord : order) (Parse_ast.P_aux(pat,l) : Parse_ast.pat) : tannot pat = +let rec to_ast_pat (k_env : kind Envmap.t) (def_ord : order) (Parse_ast.P_aux(pat,l) : Parse_ast.pat) : unit pat = P_aux( (match pat with | Parse_ast.P_lit(lit) -> P_lit(to_ast_lit lit) @@ -411,6 +438,7 @@ let rec to_ast_pat (k_env : kind Envmap.t) (def_ord : order) (Parse_ast.P_aux(pa | Parse_ast.P_as(pat,id) -> P_as(to_ast_pat k_env def_ord pat,to_ast_id id) | Parse_ast.P_typ(typ,pat) -> P_typ(to_ast_typ k_env def_ord typ,to_ast_pat k_env def_ord pat) | Parse_ast.P_id(id) -> P_id(to_ast_id id) + | Parse_ast.P_var (pat, kid) -> P_var (to_ast_pat k_env def_ord pat, to_ast_var kid) | Parse_ast.P_app(id,pats) -> if pats = [] then P_id (to_ast_id id) @@ -418,27 +446,24 @@ let rec to_ast_pat (k_env : kind Envmap.t) (def_ord : order) (Parse_ast.P_aux(pa | Parse_ast.P_record(fpats,_) -> P_record(List.map (fun (Parse_ast.FP_aux(Parse_ast.FP_Fpat(id,fp),l)) -> - FP_aux(FP_Fpat(to_ast_id id, to_ast_pat k_env def_ord fp),(l,NoTyp))) + FP_aux(FP_Fpat(to_ast_id id, to_ast_pat k_env def_ord fp),(l,()))) fpats, false) | Parse_ast.P_vector(pats) -> P_vector(List.map (to_ast_pat k_env def_ord) pats) - | Parse_ast.P_vector_indexed(ipats) -> P_vector_indexed(List.map (fun (i,pat) -> i,to_ast_pat k_env def_ord pat) ipats) | Parse_ast.P_vector_concat(pats) -> P_vector_concat(List.map (to_ast_pat k_env def_ord) pats) | Parse_ast.P_tup(pats) -> P_tup(List.map (to_ast_pat k_env def_ord) pats) | Parse_ast.P_list(pats) -> P_list(List.map (to_ast_pat k_env def_ord) pats) - ), (l,NoTyp)) + | Parse_ast.P_cons(pat1, pat2) -> P_cons (to_ast_pat k_env def_ord pat1, to_ast_pat k_env def_ord pat2) + ), (l,())) -let rec to_ast_letbind (k_env : kind Envmap.t) (def_ord : order) (Parse_ast.LB_aux(lb,l) : Parse_ast.letbind) : tannot letbind = +let rec to_ast_letbind (k_env : kind Envmap.t) (def_ord : order) (Parse_ast.LB_aux(lb,l) : Parse_ast.letbind) : unit letbind = LB_aux( (match lb with - | Parse_ast.LB_val_explicit(typschm,pat,exp) -> - let typsch, k_env, _ = to_ast_typschm k_env def_ord typschm in - LB_val_explicit(typsch,to_ast_pat k_env def_ord pat, to_ast_exp k_env def_ord exp) - | Parse_ast.LB_val_implicit(pat,exp) -> - LB_val_implicit(to_ast_pat k_env def_ord pat, to_ast_exp k_env def_ord exp) - ), (l,NoTyp)) - -and to_ast_exp (k_env : kind Envmap.t) (def_ord : order) (Parse_ast.E_aux(exp,l) : Parse_ast.exp) : tannot exp = + | Parse_ast.LB_val(pat,exp) -> + LB_val(to_ast_pat k_env def_ord pat, to_ast_exp k_env def_ord exp) + ), (l,())) + +and to_ast_exp (k_env : kind Envmap.t) (def_ord : order) (Parse_ast.E_aux(exp,l) : Parse_ast.exp) : unit exp = E_aux( (match exp with | Parse_ast.E_block(exps) -> @@ -460,20 +485,10 @@ and to_ast_exp (k_env : kind Envmap.t) (def_ord : order) (Parse_ast.E_aux(exp,l) | Parse_ast.E_if(e1,e2,e3) -> E_if(to_ast_exp k_env def_ord e1, to_ast_exp k_env def_ord e2, to_ast_exp k_env def_ord e3) | Parse_ast.E_for(id,e1,e2,e3,atyp,e4) -> E_for(to_ast_id id,to_ast_exp k_env def_ord e1, to_ast_exp k_env def_ord e2, - to_ast_exp k_env def_ord e3,to_ast_order k_env def_ord atyp, to_ast_exp k_env def_ord e4) - | Parse_ast.E_vector(exps) -> - (match to_ast_iexps false k_env def_ord exps with - | Some([]) -> E_vector([]) - | Some(iexps) -> E_vector_indexed(iexps, - Def_val_aux(Def_val_empty,(l,NoTyp))) - | None -> E_vector(List.map (to_ast_exp k_env def_ord) exps)) - | Parse_ast.E_vector_indexed(iexps,Parse_ast.Def_val_aux(default,dl)) -> - (match to_ast_iexps true k_env def_ord iexps with - | Some(iexps) -> E_vector_indexed (iexps, - Def_val_aux((match default with - | Parse_ast.Def_val_empty -> Def_val_empty - | Parse_ast.Def_val_dec e -> Def_val_dec (to_ast_exp k_env def_ord e)),(dl,NoTyp))) - | _ -> raise (Reporting_basic.err_unreachable l "to_ast_iexps didn't throw error")) + to_ast_exp k_env def_ord e3,to_ast_order k_env def_ord atyp, to_ast_exp k_env def_ord e4) + | Parse_ast.E_loop (Parse_ast.While, e1, e2) -> E_loop (While, to_ast_exp k_env def_ord e1, to_ast_exp k_env def_ord e2) + | Parse_ast.E_loop (Parse_ast.Until, e1, e2) -> E_loop (Until, to_ast_exp k_env def_ord e1, to_ast_exp k_env def_ord e2) + | Parse_ast.E_vector(exps) -> E_vector(List.map (to_ast_exp k_env def_ord) exps) | Parse_ast.E_vector_access(vexp,exp) -> E_vector_access(to_ast_exp k_env def_ord vexp, to_ast_exp k_env def_ord exp) | Parse_ast.E_vector_subrange(vex,exp1,exp2) -> E_vector_subrange(to_ast_exp k_env def_ord vex, to_ast_exp k_env def_ord exp1, to_ast_exp k_env def_ord exp2) @@ -485,22 +500,28 @@ and to_ast_exp (k_env : kind Envmap.t) (def_ord : order) (Parse_ast.E_aux(exp,l) | Parse_ast.E_vector_append(e1,e2) -> E_vector_append(to_ast_exp k_env def_ord e1,to_ast_exp k_env def_ord e2) | Parse_ast.E_list(exps) -> E_list(List.map (to_ast_exp k_env def_ord) exps) | Parse_ast.E_cons(e1,e2) -> E_cons(to_ast_exp k_env def_ord e1, to_ast_exp k_env def_ord e2) - | Parse_ast.E_record _ -> raise (Reporting_basic.err_unreachable l "parser generated an E_record") + | Parse_ast.E_record fexps -> + (match to_ast_fexps true k_env def_ord fexps with + | Some fexps -> E_record fexps + | None -> raise (Reporting_basic.err_unreachable l "to_ast_fexps with true returned none")) | Parse_ast.E_record_update(exp,fexps) -> (match to_ast_fexps true k_env def_ord fexps with | Some(fexps) -> E_record_update(to_ast_exp k_env def_ord exp, fexps) | _ -> raise (Reporting_basic.err_unreachable l "to_ast_fexps with true returned none")) | Parse_ast.E_field(exp,id) -> E_field(to_ast_exp k_env def_ord exp, to_ast_id id) | Parse_ast.E_case(exp,pexps) -> E_case(to_ast_exp k_env def_ord exp, List.map (to_ast_case k_env def_ord) pexps) + | Parse_ast.E_try (exp, pexps) -> E_try (to_ast_exp k_env def_ord exp, List.map (to_ast_case k_env def_ord) pexps) | Parse_ast.E_let(leb,exp) -> E_let(to_ast_letbind k_env def_ord leb, to_ast_exp k_env def_ord exp) | Parse_ast.E_assign(lexp,exp) -> E_assign(to_ast_lexp k_env def_ord lexp, to_ast_exp k_env def_ord exp) | Parse_ast.E_sizeof(nexp) -> E_sizeof(to_ast_nexp k_env nexp) + | Parse_ast.E_constraint nc -> E_constraint (to_ast_nexp_constraint k_env nc) | Parse_ast.E_exit exp -> E_exit(to_ast_exp k_env def_ord exp) + | Parse_ast.E_throw exp -> E_throw (to_ast_exp k_env def_ord exp) | Parse_ast.E_return exp -> E_return(to_ast_exp k_env def_ord exp) | Parse_ast.E_assert(cond,msg) -> E_assert(to_ast_exp k_env def_ord cond, to_ast_exp k_env def_ord msg) - ), (l,NoTyp)) + ), (l,())) -and to_ast_lexp (k_env : kind Envmap.t) (def_ord : order) (Parse_ast.E_aux(exp,l) : Parse_ast.exp) : tannot lexp = +and to_ast_lexp (k_env : kind Envmap.t) (def_ord : order) (Parse_ast.E_aux(exp,l) : Parse_ast.exp) : unit lexp = LEXP_aux( (match exp with | Parse_ast.E_id(id) -> LEXP_id(to_ast_id id) @@ -528,15 +549,17 @@ and to_ast_lexp (k_env : kind Envmap.t) (def_ord : order) (Parse_ast.E_aux(exp,l LEXP_vector_range(to_ast_lexp k_env def_ord vexp, to_ast_exp k_env def_ord exp1, to_ast_exp k_env def_ord exp2) | Parse_ast.E_field(fexp,id) -> LEXP_field(to_ast_lexp k_env def_ord fexp, to_ast_id id) | _ -> typ_error l "Only identifiers, cast identifiers, vector accesses, vector slices, and fields can be on the lefthand side of an assignment" None None None) - , (l,NoTyp)) + , (l,())) -and to_ast_case (k_env : kind Envmap.t) (def_ord : order) (Parse_ast.Pat_aux(pex,l) : Parse_ast.pexp) : tannot pexp = +and to_ast_case (k_env : kind Envmap.t) (def_ord : order) (Parse_ast.Pat_aux(pex,l) : Parse_ast.pexp) : unit pexp = match pex with - | Parse_ast.Pat_exp(pat,exp) -> Pat_aux(Pat_exp(to_ast_pat k_env def_ord pat, to_ast_exp k_env def_ord exp),(l,NoTyp)) + | Parse_ast.Pat_exp(pat,exp) -> Pat_aux(Pat_exp(to_ast_pat k_env def_ord pat, to_ast_exp k_env def_ord exp),(l,())) + | Parse_ast.Pat_when(pat,guard,exp) -> + Pat_aux (Pat_when (to_ast_pat k_env def_ord pat, to_ast_exp k_env def_ord guard, to_ast_exp k_env def_ord exp), (l, ())) -and to_ast_fexps (fail_on_error:bool) (k_env:kind Envmap.t) (def_ord:order) (exps : Parse_ast.exp list) : tannot fexps option = +and to_ast_fexps (fail_on_error:bool) (k_env:kind Envmap.t) (def_ord:order) (exps : Parse_ast.exp list) : unit fexps option = match exps with - | [] -> Some(FES_aux(FES_Fexps([],false), (Parse_ast.Unknown,NoTyp))) + | [] -> Some(FES_aux(FES_Fexps([],false), (Parse_ast.Unknown,()))) | fexp::exps -> let maybe_fexp,maybe_error = to_ast_record_try k_env def_ord fexp in (match maybe_fexp,maybe_error with | Some(fexp),None -> @@ -549,12 +572,12 @@ and to_ast_fexps (fail_on_error:bool) (k_env:kind Envmap.t) (def_ord:order) (exp else None | _ -> None) -and to_ast_record_try (k_env:kind Envmap.t) (def_ord:order) (Parse_ast.E_aux(exp,l):Parse_ast.exp): tannot fexp option * (l * string) option = +and to_ast_record_try (k_env:kind Envmap.t) (def_ord:order) (Parse_ast.E_aux(exp,l):Parse_ast.exp): unit fexp option * (l * string) option = match exp with | Parse_ast.E_app_infix(left,op,r) -> (match left, op with | Parse_ast.E_aux(Parse_ast.E_id(id),li), Parse_ast.Id_aux(Parse_ast.Id("="),leq) -> - Some(FE_aux(FE_Fexp(to_ast_id id, to_ast_exp k_env def_ord r), (l,NoTyp))),None + Some(FE_aux(FE_Fexp(to_ast_id id, to_ast_exp k_env def_ord r), (l,()))),None | Parse_ast.E_aux(_,li) , Parse_ast.Id_aux(Parse_ast.Id("="),leq) -> None,Some(li,"Expected an identifier to begin this field assignment") | Parse_ast.E_aux(Parse_ast.E_id(id),li), Parse_ast.Id_aux(_,leq) -> @@ -564,32 +587,7 @@ and to_ast_record_try (k_env:kind Envmap.t) (def_ord:order) (Parse_ast.E_aux(exp | _ -> None,Some(l, "Expected a field assignment to be identifier = expression") -and to_ast_iexps (fail_on_error:bool) (k_env:kind Envmap.t) (def_ord:order) (exps:Parse_ast.exp list):(int * tannot exp) list option = - match exps with - | [] -> Some([]) - | iexp::exps -> (match to_iexp_try k_env def_ord iexp with - | Some(iexp),None -> - (match to_ast_iexps fail_on_error k_env def_ord exps with - | Some(iexps) -> Some(iexp::iexps) - | _ -> None) - | None,Some(l,msg) -> - if fail_on_error - then typ_error l msg None None None - else None - | _ -> None) -and to_iexp_try (k_env:kind Envmap.t) (def_ord:order) (Parse_ast.E_aux(exp,l): Parse_ast.exp): ((int * tannot exp) option * (l*string) option) = - match exp with - | Parse_ast.E_app_infix(left,op,r) -> - (match left,op with - | Parse_ast.E_aux(Parse_ast.E_lit(Parse_ast.L_aux (Parse_ast.L_num i,ll)),cl), Parse_ast.Id_aux(Parse_ast.Id("="),leq) -> - Some(i,to_ast_exp k_env def_ord r),None - | Parse_ast.E_aux(_,li), Parse_ast.Id_aux (Parse_ast.Id("="),leq) -> - None,(Some(li,"Expected a constant number to begin this indexed vector assignemnt")) - | Parse_ast.E_aux(_,cl), Parse_ast.Id_aux(_,leq) -> - None,(Some(leq,"Expected an indexed vector assignment constant = expression"))) - | _ -> None,(Some(l,"Expected an indexed vector assignment: constant = expression")) - -let to_ast_default (names, k_env, default_order) (default : Parse_ast.default_typing_spec) : (tannot default_spec) envs_out = +let to_ast_default (names, k_env, default_order) (default : Parse_ast.default_typing_spec) : default_spec envs_out = match default with | Parse_ast.DT_aux(df,l) -> (match df with @@ -612,21 +610,13 @@ let to_ast_default (names, k_env, default_order) (default : Parse_ast.default_ty DT_aux(DT_order default_order,l),(names,k_env,default_order) | _ -> typ_error l "Inc and Dec must have kind Order" None None None)) -let to_ast_spec (names,k_env,default_order) (val_:Parse_ast.val_spec) : (tannot val_spec) envs_out = +let to_ast_spec (names,k_env,default_order) (val_:Parse_ast.val_spec) : (unit val_spec) envs_out = match val_ with | Parse_ast.VS_aux(vs,l) -> (match vs with - | Parse_ast.VS_val_spec(ts,id) -> - (*let _ = Printf.eprintf "to_ast_spec called for internal spec: for %s\n" (id_to_string (to_ast_id id)) in*) - let typsch,_,_ = to_ast_typschm k_env default_order ts in - VS_aux(VS_val_spec(typsch,to_ast_id id),(l,NoTyp)),(names,k_env,default_order) - | Parse_ast.VS_extern_spec(ts,id,s) -> + | Parse_ast.VS_val_spec(ts,id,ext,is_cast) -> let typsch,_,_ = to_ast_typschm k_env default_order ts in - VS_aux(VS_extern_spec(typsch,to_ast_id id,s),(l,NoTyp)),(names,k_env,default_order) - | Parse_ast.VS_extern_no_rename(ts,id) -> - let typsch,_,_ = to_ast_typschm k_env default_order ts in - VS_aux(VS_extern_no_rename(typsch,to_ast_id id),(l,NoTyp)),(names,k_env,default_order)) - + VS_aux(VS_val_spec(typsch,to_ast_id id,ext,is_cast),(l,())),(names,k_env,default_order)) let to_ast_namescm (Parse_ast.Name_sect_aux(ns,l)) = Name_sect_aux( @@ -653,7 +643,7 @@ let to_ast_type_union k_env default_order (Parse_ast.Tu_aux(tu,l)) = | _ -> Tu_aux(Tu_ty_id(typ, to_ast_id id), l)) | Parse_ast.Tu_id id -> (Tu_aux(Tu_id(to_ast_id id),l)) -let to_ast_typedef (names,k_env,def_ord) (td:Parse_ast.type_def) : (tannot type_def) envs_out = +let to_ast_typedef (names,k_env,def_ord) (td:Parse_ast.type_def) : (unit type_def) envs_out = match td with | Parse_ast.TD_aux(td,l) -> (match td with @@ -661,7 +651,7 @@ let to_ast_typedef (names,k_env,def_ord) (td:Parse_ast.type_def) : (tannot type_ let id = to_ast_id id in let key = id_to_string id in let typschm,k_env,_ = to_ast_typschm k_env def_ord typschm in - let td_abrv = TD_aux(TD_abbrev(id,to_ast_namescm name_scm_opt,typschm),(l,NoTyp)) in + let td_abrv = TD_aux(TD_abbrev(id,to_ast_namescm name_scm_opt,typschm),(l,())) in let typ = (match typschm with | TypSchm_aux(TypSchm_ts(tq,typ), _) -> begin match (typquant_to_quantkinds k_env tq) with @@ -674,7 +664,7 @@ let to_ast_typedef (names,k_env,def_ord) (td:Parse_ast.type_def) : (tannot type_ let key = id_to_string id in let typq,k_env,_ = to_ast_typquant k_env typq in let fields = List.map (fun (atyp,id) -> (to_ast_typ k_env def_ord atyp),(to_ast_id id)) fields in (* Add check that all arms have unique names locally *) - let td_rec = TD_aux(TD_record(id,to_ast_namescm name_scm_opt,typq,fields,false),(l,NoTyp)) in + let td_rec = TD_aux(TD_record(id,to_ast_namescm name_scm_opt,typq,fields,false),(l,())) in let typ = (match (typquant_to_quantkinds k_env typq) with | [ ] -> {k = K_Typ} | typs -> {k = K_Lam(typs,{k=K_Typ})}) in @@ -684,7 +674,7 @@ let to_ast_typedef (names,k_env,def_ord) (td:Parse_ast.type_def) : (tannot type_ let key = id_to_string id in let typq,k_env,_ = to_ast_typquant k_env typq in let arms = List.map (to_ast_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_ast_namescm name_scm_opt,typq,arms,false),(l,NoTyp)) in + let td_var = TD_aux(TD_variant(id,to_ast_namescm name_scm_opt,typq,arms,false),(l,())) in let typ = (match (typquant_to_quantkinds k_env typq) with | [ ] -> {k = K_Typ} | typs -> {k = K_Lam(typs,{k=K_Typ})}) in @@ -694,7 +684,7 @@ let to_ast_typedef (names,k_env,def_ord) (td:Parse_ast.type_def) : (tannot type_ let key = id_to_string id in let enums = List.map to_ast_id enums in let keys = List.map id_to_string enums in - let td_enum = TD_aux(TD_enum(id,to_ast_namescm name_scm_opt,enums,false),(l,NoTyp)) in (* Add check that all enums have unique names *) + let td_enum = TD_aux(TD_enum(id,to_ast_namescm name_scm_opt,enums,false),(l,())) 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) | Parse_ast.TD_register(id,t1,t2,ranges) -> @@ -703,9 +693,9 @@ let to_ast_typedef (names,k_env,def_ord) (td:Parse_ast.type_def) : (tannot type_ let n1 = to_ast_nexp k_env t1 in let n2 = to_ast_nexp k_env t2 in let ranges = List.map (fun (range,id) -> (to_ast_range range),to_ast_id id) ranges in - TD_aux(TD_register(id,n1,n2,ranges),(l,NoTyp)), (names,Envmap.insert k_env (key, {k=K_Typ}),def_ord)) + TD_aux(TD_register(id,n1,n2,ranges),(l,())), (names,Envmap.insert k_env (key, {k=K_Typ}),def_ord)) -let to_ast_kdef (names,k_env,def_ord) (td:Parse_ast.kind_def) : (tannot kind_def) envs_out = +let to_ast_kdef (names,k_env,def_ord) (td:Parse_ast.kind_def) : (unit kind_def) envs_out = match td with | Parse_ast.KD_aux(td,l) -> (match td with @@ -714,67 +704,17 @@ let to_ast_kdef (names,k_env,def_ord) (td:Parse_ast.kind_def) : (tannot kind_def let key = id_to_string id in let (kind,k) = to_ast_kind k_env kind in (match k.k with - | K_Typ | K_Lam _ -> - let typschm,k_env,_ = to_ast_typschm k_env def_ord typschm in - let kd_abrv = KD_aux(KD_abbrev(kind,id,to_ast_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) | K_Nat -> let kd_nabrv = (match typschm with | Parse_ast.TypSchm_aux(Parse_ast.TypSchm_ts(Parse_ast.TypQ_aux(tq,_),atyp),_) -> (match tq with | Parse_ast.TypQ_no_forall -> - KD_aux(KD_nabbrev(kind,id,to_ast_namescm name_scm_opt, to_ast_nexp k_env atyp), (l,NoTyp)) + KD_aux(KD_nabbrev(kind,id,to_ast_namescm name_scm_opt, to_ast_nexp k_env atyp), (l,())) | _ -> typ_error l "Def with kind Nat cannot have universal quantification" None None None)) in kd_nabrv,(names,Envmap.insert k_env (key, k),def_ord) | _ -> assert false - ) - | Parse_ast.KD_record(kind,id,name_scm_opt,typq,fields,_) -> - let id = to_ast_id id in - let key = id_to_string id in - let (kind,k) = to_ast_kind k_env kind in - let typq,k_env,_ = to_ast_typquant k_env typq in - let fields = List.map (fun (atyp,id) -> (to_ast_typ k_env def_ord atyp),(to_ast_id id)) fields in (* Add check that all arms have unique names locally *) - let kd_rec = KD_aux(KD_record(kind,id,to_ast_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) - | Parse_ast.KD_variant(kind,id,name_scm_opt,typq,arms,_) -> - let id = to_ast_id id in - let key = id_to_string id in - let kind,k = to_ast_kind k_env kind in - let typq,k_env,_ = to_ast_typquant k_env typq in - let arms = List.map (to_ast_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_ast_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) - | Parse_ast.KD_enum(kind,id,name_scm_opt,enums,_) -> - let id = to_ast_id id in - let key = id_to_string id in - let kind,k = to_ast_kind k_env kind in - let enums = List.map to_ast_id enums in - let keys = List.map id_to_string enums in - let kd_enum = KD_aux(KD_enum(kind,id,to_ast_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) - | Parse_ast.KD_register(kind,id,t1,t2,ranges) -> - let id = to_ast_id id in - let key = id_to_string id in - let kind,k = to_ast_kind k_env kind in - let n1 = to_ast_nexp k_env t1 in - let n2 = to_ast_nexp k_env t2 in - let ranges = List.map (fun (range,id) -> (to_ast_range range),to_ast_id 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)) - + )) let to_ast_rec (Parse_ast.Rec_aux(r,l): Parse_ast.rec_opt) : rec_opt = Rec_aux((match r with @@ -784,7 +724,8 @@ let to_ast_rec (Parse_ast.Rec_aux(r,l): Parse_ast.rec_opt) : rec_opt = let to_ast_tannot_opt (k_env:kind Envmap.t) (def_ord:order) (Parse_ast.Typ_annot_opt_aux(tp,l)):tannot_opt * kind Envmap.t * kind Envmap.t= match tp with - | Parse_ast.Typ_annot_opt_none -> raise (Reporting_basic.err_unreachable l "Parser generated typ annot opt none") + | Parse_ast.Typ_annot_opt_none -> + Typ_annot_opt_aux (Typ_annot_opt_none, l), k_env, Envmap.empty | Parse_ast.Typ_annot_opt_some(tq,typ) -> let typq,k_env,k_local = to_ast_typquant k_env tq in Typ_annot_opt_aux(Typ_annot_opt_some(typq,to_ast_typ k_env def_ord typ),l),k_env,k_local @@ -794,25 +735,25 @@ let to_ast_effects_opt (k_env : kind Envmap.t) (Parse_ast.Effect_opt_aux(e,l)) : | Parse_ast.Effect_opt_pure -> Effect_opt_aux(Effect_opt_pure,l) | Parse_ast.Effect_opt_effect(typ) -> Effect_opt_aux(Effect_opt_effect(to_ast_effects k_env typ),l) -let to_ast_funcl (names,k_env,def_ord) (Parse_ast.FCL_aux(fcl,l) : Parse_ast.funcl) : (tannot funcl) = +let to_ast_funcl (names,k_env,def_ord) (Parse_ast.FCL_aux(fcl,l) : Parse_ast.funcl) : (unit funcl) = (*let _ = Printf.eprintf "to_ast_funcl\n" in*) match fcl with - | Parse_ast.FCL_Funcl(id,pat,exp) -> - FCL_aux(FCL_Funcl(to_ast_id id, to_ast_pat k_env def_ord pat, to_ast_exp k_env def_ord exp),(l,NoTyp)) + | Parse_ast.FCL_Funcl(id,pexp) -> + FCL_aux(FCL_Funcl(to_ast_id id, to_ast_case k_env def_ord pexp),(l,())) -let to_ast_fundef (names,k_env,def_ord) (Parse_ast.FD_aux(fd,l):Parse_ast.fundef) : (tannot fundef) envs_out = +let to_ast_fundef (names,k_env,def_ord) (Parse_ast.FD_aux(fd,l):Parse_ast.fundef) : (unit fundef) envs_out = match fd with | Parse_ast.FD_function(rec_opt,tannot_opt,effects_opt,funcls) -> (*let _ = Printf.eprintf "to_ast_fundef\n" in*) let tannot_opt, k_env,_ = to_ast_tannot_opt k_env def_ord tannot_opt in - FD_aux(FD_function(to_ast_rec rec_opt, tannot_opt, to_ast_effects_opt k_env effects_opt, List.map (to_ast_funcl (names, k_env, def_ord)) funcls), (l,NoTyp)), (names,k_env,def_ord) + FD_aux(FD_function(to_ast_rec rec_opt, tannot_opt, to_ast_effects_opt k_env effects_opt, List.map (to_ast_funcl (names, k_env, def_ord)) funcls), (l,())), (names,k_env,def_ord) type def_progress = No_def | Def_place_holder of id * Parse_ast.l - | Finished of tannot def + | Finished of unit def -type partial_def = ((tannot def) * bool) ref * kind Envmap.t +type partial_def = ((unit 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 @@ -826,17 +767,17 @@ let to_ast_alias_spec k_env def_ord (Parse_ast.E_aux(e,le)) = AL_aux( (match e with | Parse_ast.E_field(Parse_ast.E_aux(Parse_ast.E_id id,li), field) -> - AL_subreg(RI_aux(RI_id (to_ast_id id),(li,NoTyp)),to_ast_id field) + AL_subreg(RI_aux(RI_id (to_ast_id id),(li,())),to_ast_id field) | Parse_ast.E_vector_access(Parse_ast.E_aux(Parse_ast.E_id id,li),range) -> - AL_bit(RI_aux(RI_id (to_ast_id id),(li,NoTyp)),to_ast_exp k_env def_ord range) + AL_bit(RI_aux(RI_id (to_ast_id id),(li,())),to_ast_exp k_env def_ord range) | Parse_ast.E_vector_subrange(Parse_ast.E_aux(Parse_ast.E_id id,li),base,stop) -> - AL_slice(RI_aux(RI_id (to_ast_id id),(li,NoTyp)),to_ast_exp k_env def_ord base,to_ast_exp k_env def_ord stop) + AL_slice(RI_aux(RI_id (to_ast_id id),(li,())),to_ast_exp k_env def_ord base,to_ast_exp k_env def_ord stop) | Parse_ast.E_vector_append(Parse_ast.E_aux(Parse_ast.E_id first,lf), Parse_ast.E_aux(Parse_ast.E_id second,ls)) -> - AL_concat(RI_aux(RI_id (to_ast_id first),(lf,NoTyp)), - RI_aux(RI_id (to_ast_id second),(ls,NoTyp))) + AL_concat(RI_aux(RI_id (to_ast_id first),(lf,())), + RI_aux(RI_id (to_ast_id second),(ls,()))) | _ -> raise (Reporting_basic.err_unreachable le "Found an expression not supported by parser in to_ast_alias_spec") - ), (le,NoTyp)) + ), (le,())) let to_ast_dec (names,k_env,def_ord) (Parse_ast.DEC_aux(regdec,l)) = DEC_aux( @@ -847,11 +788,20 @@ let to_ast_dec (names,k_env,def_ord) (Parse_ast.DEC_aux(regdec,l)) = DEC_alias(to_ast_id id,to_ast_alias_spec k_env def_ord e) | Parse_ast.DEC_typ_alias(typ,id,e) -> DEC_typ_alias(to_ast_typ k_env def_ord typ,to_ast_id id,to_ast_alias_spec k_env def_ord e) - ),(l,NoTyp)) - + ),(l,())) + +let to_ast_prec = function + | Parse_ast.Infix -> Infix + | Parse_ast.InfixL -> InfixL + | Parse_ast.InfixR -> InfixR + let to_ast_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 + | Parse_ast.DEF_overload(id,ids) -> + ((Finished(DEF_overload(to_ast_id id, List.map to_ast_id ids))),envs),partial_defs + | Parse_ast.DEF_fixity (prec, n, op) -> + ((Finished(DEF_fixity (to_ast_prec prec, n, to_ast_id op)),envs),partial_defs) | Parse_ast.DEF_kind(k_def) -> let kd,envs = to_ast_kdef envs k_def in ((Finished(DEF_kind(kd))),envs),partial_defs @@ -877,16 +827,16 @@ let to_ast_def (names, k_env, def_ord) partial_defs def : def_progress envs_out (match sd with | Parse_ast.SD_scattered_function(rec_opt, tannot_opt, effects_opt, id) -> let rec_opt = to_ast_rec rec_opt in - let tannot,k_env',k_local = to_ast_tannot_opt k_env def_ord tannot_opt in + let unit,k_env',k_local = to_ast_tannot_opt k_env def_ord tannot_opt in let effects_opt = to_ast_effects_opt k_env' effects_opt in let id = to_ast_id id 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 + | None -> let partial_def = ref ((DEF_fundef(FD_aux(FD_function(rec_opt,unit,effects_opt,[]),(l,())))),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) | Parse_ast.SD_scattered_funcl(funcl) -> (match funcl with - | Parse_ast.FCL_aux(Parse_ast.FCL_Funcl(id,_,_),_) -> + | Parse_ast.FCL_aux(Parse_ast.FCL_Funcl(id,_),_) -> let id = to_ast_id id in (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 @@ -909,7 +859,7 @@ let to_ast_def (names, k_env, def_ord) partial_defs def : def_progress envs_out | [ ] -> {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 + | None -> let partial_def = ref ((DEF_type(TD_aux(TD_variant(id,name,typq,[],false),(l,())))),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) | Parse_ast.SD_scattered_unioncl(id,tu) -> @@ -956,7 +906,15 @@ let rec to_ast_defs_helper envs partial_defs = function then (fst !d) :: defs, envs, partial_defs else typ_error l "Scattered type definition never ended" (Some id) None None)) +let rec remove_mutrec = function + | [] -> [] + | Parse_ast.DEF_internal_mutrec fundefs :: defs -> + List.map (fun fdef -> Parse_ast.DEF_fundef fdef) fundefs @ remove_mutrec defs + | def :: defs -> + def :: remove_mutrec defs + let to_ast (default_names : Nameset.t) (kind_env : kind Envmap.t) (def_ord : order) (Parse_ast.Defs(defs)) = + let defs = remove_mutrec defs in let defs,(_,k_env,def_ord),partial_defs = to_ast_defs_helper (default_names,kind_env,def_ord) [] defs in List.iter (fun (id,(d,k)) -> @@ -965,3 +923,158 @@ let to_ast (default_names : Nameset.t) (kind_env : kind Envmap.t) (def_ord : ord | (_, true) -> ())) partial_defs; (Defs defs),k_env,def_ord + +let initial_kind_env = + Envmap.from_list [ + ("bool", {k = K_Typ}); + ("nat", {k = K_Typ}); + ("int", {k = K_Typ}); + ("uint8", {k = K_Typ}); + ("uint16", {k= K_Typ}); + ("uint32", {k=K_Typ}); + ("uint64", {k=K_Typ}); + ("unit", {k = K_Typ}); + ("bit", {k = K_Typ}); + ("string", {k = K_Typ}); + ("real", {k = K_Typ}); + ("list", {k = K_Lam( [{k = K_Typ}], {k = K_Typ})}); + ("reg", {k = K_Lam( [{k = K_Typ}], {k= K_Typ})}); + ("register", {k = K_Lam( [{k = K_Typ}], {k= K_Typ})}); + ("range", {k = K_Lam( [ {k = K_Nat}; {k= K_Nat}], {k = K_Typ}) }); + ("vector", {k = K_Lam( [ {k = K_Nat}; {k = K_Nat}; {k= K_Ord} ; {k=K_Typ}], {k=K_Typ}) } ); + ("atom", {k = K_Lam( [ {k=K_Nat} ], {k=K_Typ})}); + ("option", { k = K_Lam( [{k=K_Typ}], {k=K_Typ}) }); + ("implicit", {k = K_Lam( [{k = K_Nat}], {k=K_Typ})} ); + ("itself", {k = K_Lam( [ {k=K_Nat} ], {k=K_Typ})}); + ] + +let exp_of_string order str = + let exp = Parser2.exp_eof Lexer2.token (Lexing.from_string str) in + to_ast_exp initial_kind_env order exp + +let typschm_of_string order str = + let typschm = Parser2.typschm_eof Lexer2.token (Lexing.from_string str) in + let (typschm, _, _) = to_ast_typschm initial_kind_env order typschm in + typschm + +let val_spec_of_string order id str = mk_val_spec (VS_val_spec (typschm_of_string order str, id, (fun _ -> Some (string_of_id id)), false)) + +let val_spec_ids (Defs defs) = + let val_spec_id (VS_aux (vs_aux, _)) = + match vs_aux with + | VS_val_spec (_, id, _, _) -> id + in + let rec vs_ids = function + | DEF_spec vs :: defs -> val_spec_id vs :: vs_ids defs + | def :: defs -> vs_ids defs + | [] -> [] + in + IdSet.of_list (vs_ids defs) + +let quant_item_param = function + | QI_aux (QI_id kopt, _) when is_nat_kopt kopt -> [prepend_id "atom_" (id_of_kid (kopt_kid kopt))] + | QI_aux (QI_id kopt, _) when is_typ_kopt kopt -> [prepend_id "typ_" (id_of_kid (kopt_kid kopt))] + | _ -> [] +let quant_item_typ = function + | QI_aux (QI_id kopt, _) when is_nat_kopt kopt -> [atom_typ (nvar (kopt_kid kopt))] + | QI_aux (QI_id kopt, _) when is_typ_kopt kopt -> [mk_typ (Typ_var (kopt_kid kopt))] + | _ -> [] +let quant_item_arg = function + | QI_aux (QI_id kopt, _) when is_nat_kopt kopt -> [mk_typ_arg (Typ_arg_nexp (nvar (kopt_kid kopt)))] + | QI_aux (QI_id kopt, _) when is_typ_kopt kopt -> [mk_typ_arg (Typ_arg_typ (mk_typ (Typ_var (kopt_kid kopt))))] + | _ -> [] +let undefined_typschm id typq = + let qis = quant_items typq in + if qis = [] then + mk_typschm typq (mk_typ (Typ_fn (unit_typ, mk_typ (Typ_id id), mk_effect [BE_undef]))) + else + let arg_typ = mk_typ (Typ_tup (List.concat (List.map quant_item_typ qis))) in + let ret_typ = app_typ id (List.concat (List.map quant_item_arg qis)) in + mk_typschm typq (mk_typ (Typ_fn (arg_typ, ret_typ, mk_effect [BE_undef]))) + +let generate_undefineds vs_ids (Defs defs) = + let gen_vs id str = + if (IdSet.mem id vs_ids) then [] else [val_spec_of_string dec_ord id str] + in + let undefined_builtins = List.concat + [gen_vs (mk_id "internal_pick") "forall ('a:Type). list('a) -> 'a effect {undef}"; + gen_vs (mk_id "undefined_bool") "unit -> bool effect {undef}"; + gen_vs (mk_id "undefined_bit") "unit -> bit effect {undef}"; + gen_vs (mk_id "undefined_int") "unit -> int effect {undef}"; + gen_vs (mk_id "undefined_nat") "unit -> nat effect {undef}"; + gen_vs (mk_id "undefined_real") "unit -> real effect {undef}"; + gen_vs (mk_id "undefined_string") "unit -> string effect {undef}"; + gen_vs (mk_id "undefined_list") "forall ('a:Type). 'a -> list('a) effect {undef}"; + gen_vs (mk_id "undefined_range") "forall 'n 'm. (atom('n), atom('m)) -> range('n,'m) effect {undef}"; + (* FIXME: How to handle inc/dec order correctly? *) + gen_vs (mk_id "undefined_vector") "forall 'n 'm ('a:Type). (atom('n), atom('m), 'a) -> vector('n, 'm, dec,'a) effect {undef}"; + (* Only used with lem_mwords *) + gen_vs (mk_id "undefined_bitvector") "forall 'n 'm. (atom('n), atom('m)) -> vector('n, 'm, dec,bit) effect {undef}"; + gen_vs (mk_id "undefined_unit") "unit -> unit effect {undef}"] + in + let undefined_tu = function + | Tu_aux (Tu_id id, _) -> mk_exp (E_id id) + | Tu_aux (Tu_ty_id (typ, id), _) -> mk_exp (E_app (id, [mk_lit_exp L_undef])) + in + let undefined_td = function + | TD_enum (id, _, ids, _) when not (IdSet.mem (prepend_id "undefined_" id) vs_ids) -> + let typschm = typschm_of_string dec_ord ("unit -> " ^ string_of_id id ^ " effect {undef}") in + [mk_val_spec (VS_val_spec (typschm, prepend_id "undefined_" id, (fun _ -> None), false)); + mk_fundef [mk_funcl (prepend_id "undefined_" id) + (mk_pat (P_lit (mk_lit L_unit))) + (mk_exp (E_app (mk_id "internal_pick", + [mk_exp (E_list (List.map (fun id -> mk_exp (E_id id)) ids))])))]] + | TD_record (id, _, typq, fields, _) when not (IdSet.mem (prepend_id "undefined_" id) vs_ids) -> + let pat = mk_pat (P_tup (quant_items typq |> List.map quant_item_param |> List.concat |> List.map (fun id -> mk_pat (P_id id)))) in + [mk_val_spec (VS_val_spec (undefined_typschm id typq, prepend_id "undefined_" id, (fun _ -> None), false)); + mk_fundef [mk_funcl (prepend_id "undefined_" id) + pat + (mk_exp (E_record (mk_fexps (List.map (fun (_, id) -> mk_fexp id (mk_lit_exp L_undef)) fields))))]] + | TD_variant (id, _, typq, tus, _) when not (IdSet.mem (prepend_id "undefined_" id) vs_ids) -> + let pat = mk_pat (P_tup (quant_items typq |> List.map quant_item_param |> List.concat |> List.map (fun id -> mk_pat (P_id id)))) in + [mk_val_spec (VS_val_spec (undefined_typschm id typq, prepend_id "undefined_" id, (fun _ -> None), false)); + mk_fundef [mk_funcl (prepend_id "undefined_" id) + pat + (mk_exp (E_app (mk_id "internal_pick", + [mk_exp (E_list (List.map undefined_tu tus))])))]] + | _ -> [] + in + let rec undefined_defs = function + | DEF_type (TD_aux (td_aux, _)) as def :: defs -> + def :: undefined_td td_aux @ undefined_defs defs + | def :: defs -> + def :: undefined_defs defs + | [] -> [] + in + Defs (undefined_builtins @ undefined_defs defs) + +let rec get_registers = function + | DEF_reg_dec (DEC_aux (DEC_reg (typ, id), _)) :: defs -> (typ, id) :: get_registers defs + | def :: defs -> get_registers defs + | [] -> [] + +let generate_initialize_registers vs_ids (Defs defs) = + let regs = get_registers defs in + let initialize_registers = + if IdSet.mem (mk_id "initialize_registers") vs_ids || regs = [] then [] + else + [val_spec_of_string dec_ord (mk_id "initialize_registers") "unit -> unit effect {undef, wreg}"; + mk_fundef [mk_funcl (mk_id "initialize_registers") + (mk_pat (P_lit (mk_lit L_unit))) + (mk_exp (E_block (List.map (fun (typ, id) -> mk_exp (E_assign (mk_lexp (LEXP_cast (typ, id)), mk_lit_exp L_undef))) regs)))]] + in + Defs (defs @ initialize_registers) + +let incremental_k_env = ref initial_kind_env + +let process_ast order defs = + let ast, k_env, _= to_ast Nameset.empty !incremental_k_env order defs in + incremental_k_env := k_env; + if not !opt_undefined_gen + then ast + else + begin + let vs_ids = val_spec_ids ast in + let ast = generate_undefineds vs_ids ast in + generate_initialize_registers vs_ids ast + end |