summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/gen_lib/prompt.lem8
-rw-r--r--src/gen_lib/sail_operators.lem2
-rw-r--r--src/gen_lib/sail_values.lem9
-rw-r--r--src/gen_lib/state.lem13
-rw-r--r--src/ocaml_backend.ml90
-rw-r--r--src/pretty_print_lem.ml28
-rw-r--r--src/pretty_print_lem_ast.ml15
-rw-r--r--src/process_file.ml1
-rw-r--r--src/process_file.mli1
-rw-r--r--src/rewriter.ml330
-rw-r--r--src/rewriter.mli3
-rw-r--r--src/sail.ml6
-rw-r--r--src/spec_analysis.ml1
-rw-r--r--src/type_check.ml37
-rw-r--r--src/type_check.mli1
15 files changed, 336 insertions, 209 deletions
diff --git a/src/gen_lib/prompt.lem b/src/gen_lib/prompt.lem
index f5ac8fc5..23f81f0e 100644
--- a/src/gen_lib/prompt.lem
+++ b/src/gen_lib/prompt.lem
@@ -158,7 +158,7 @@ let footprint = Footprint (Done (),Nothing)
val foreachM_inc : forall 'vars 'r. (integer * integer * integer) -> 'vars ->
(integer -> 'vars -> MR 'vars 'r) -> MR 'vars 'r
let rec foreachM_inc (i,stop,by) vars body =
- if i <= stop
+ if (by > 0 && i <= stop) || (by < 0 && stop <= i)
then
body i vars >>= fun vars ->
foreachM_inc (i + by,stop,by) vars body
@@ -167,11 +167,11 @@ let rec foreachM_inc (i,stop,by) vars body =
val foreachM_dec : forall 'vars 'r. (integer * integer * integer) -> 'vars ->
(integer -> 'vars -> MR 'vars 'r) -> MR 'vars 'r
-let rec foreachM_dec (i,stop,by) vars body =
- if i >= stop
+let rec foreachM_dec (stop,i,by) vars body =
+ if (by > 0 && i >= stop) || (by < 0 && stop >= i)
then
body i vars >>= fun vars ->
- foreachM_dec (i - by,stop,by) vars body
+ foreachM_dec (stop,i - by,by) vars body
else return vars
val while_PP : forall 'vars. bool -> 'vars -> ('vars -> bool) -> ('vars -> 'vars) -> 'vars
diff --git a/src/gen_lib/sail_operators.lem b/src/gen_lib/sail_operators.lem
index 30c7325e..d9bf8454 100644
--- a/src/gen_lib/sail_operators.lem
+++ b/src/gen_lib/sail_operators.lem
@@ -144,7 +144,7 @@ let to_bin n = List.reverse (to_bin_aux n)
val pad_zero : list bitU -> integer -> list bitU
let rec pad_zero bits n =
- if n = 0 then bits else pad_zero (B0 :: bits) (n -1)
+ if n <= 0 then bits else pad_zero (B0 :: bits) (n -1)
let rec add_one_bit_ignore_overflow_aux bits = match bits with
diff --git a/src/gen_lib/sail_values.lem b/src/gen_lib/sail_values.lem
index 906b35a8..45b73ab5 100644
--- a/src/gen_lib/sail_values.lem
+++ b/src/gen_lib/sail_values.lem
@@ -167,6 +167,7 @@ let get_dir (Vector _ _ ord) = ord
let get_start (Vector _ s _) = s
let get_elems (Vector elems _ _) = elems
let length (Vector bs _ _) = integerFromNat (length bs)
+let vector_length = length
instance forall 'a. Show 'a => (Show (vector 'a))
let show = showVector
@@ -565,17 +566,17 @@ let internal_mem_value direction bytes =
val foreach_inc : forall 'vars. (integer * integer * integer) -> 'vars ->
(integer -> 'vars -> 'vars) -> 'vars
let rec foreach_inc (i,stop,by) vars body =
- if i <= stop
+ if (by > 0 && i <= stop) || (by < 0 && stop <= i)
then let vars = body i vars in
foreach_inc (i + by,stop,by) vars body
else vars
val foreach_dec : forall 'vars. (integer * integer * integer) -> 'vars ->
(integer -> 'vars -> 'vars) -> 'vars
-let rec foreach_dec (i,stop,by) vars body =
- if i >= stop
+let rec foreach_dec (stop,i,by) vars body =
+ if (by > 0 && i >= stop) || (by < 0 && stop >= i)
then let vars = body i vars in
- foreach_dec (i - by,stop,by) vars body
+ foreach_dec (stop,i - by,by) vars body
else vars
let assert' b msg_opt =
diff --git a/src/gen_lib/state.lem b/src/gen_lib/state.lem
index 1b03c81e..1ca25b74 100644
--- a/src/gen_lib/state.lem
+++ b/src/gen_lib/state.lem
@@ -63,8 +63,9 @@ let catch_early_return m s =
end) (m s)
val range : integer -> integer -> list integer
-let rec range i j =
- if i = j then [i]
+let rec range i j =
+ if j < i then []
+ else if i = j then [i]
else i :: range (i+1) j
val get_reg : forall 'regs 'a. sequential_state 'regs -> register_ref 'regs 'a -> 'a
@@ -218,7 +219,7 @@ let footprint s = return () s
val foreachM_inc : forall 'regs 'vars 'e. (integer * integer * integer) -> 'vars ->
(integer -> 'vars -> ME 'regs 'vars 'e) -> ME 'regs 'vars 'e
let rec foreachM_inc (i,stop,by) vars body =
- if i <= stop
+ if (by > 0 && i <= stop) || (by < 0 && stop <= i)
then
body i vars >>= fun vars ->
foreachM_inc (i + by,stop,by) vars body
@@ -227,11 +228,11 @@ let rec foreachM_inc (i,stop,by) vars body =
val foreachM_dec : forall 'regs 'vars 'e. (integer * integer * integer) -> 'vars ->
(integer -> 'vars -> ME 'regs 'vars 'e) -> ME 'regs 'vars 'e
-let rec foreachM_dec (i,stop,by) vars body =
- if i >= stop
+let rec foreachM_dec (stop,i,by) vars body =
+ if (by > 0 && i >= stop) || (by < 0 && stop >= i)
then
body i vars >>= fun vars ->
- foreachM_dec (i - by,stop,by) vars body
+ foreachM_dec (stop,i - by,by) vars body
else return vars
val while_PP : forall 'vars. bool -> 'vars -> ('vars -> bool) -> ('vars -> 'vars) -> 'vars
diff --git a/src/ocaml_backend.ml b/src/ocaml_backend.ml
index dc8c056e..74fb6e4c 100644
--- a/src/ocaml_backend.ml
+++ b/src/ocaml_backend.ml
@@ -5,12 +5,14 @@ open Type_check
type ctx =
{ register_inits : tannot exp list;
- externs : id Bindings.t
+ externs : id Bindings.t;
+ val_specs : typ Bindings.t
}
let empty_ctx =
{ register_inits = [];
- externs = Bindings.empty
+ externs = Bindings.empty;
+ val_specs = Bindings.empty
}
let zchar c =
@@ -47,7 +49,10 @@ let ocaml_typ_id ctx = function
| id when Id.compare id (mk_id "list") = 0 -> string "list"
| id when Id.compare id (mk_id "bit") = 0 -> string "bit"
| id when Id.compare id (mk_id "int") = 0 -> string "big_int"
+ | id when Id.compare id (mk_id "nat") = 0 -> string "big_int"
| id when Id.compare id (mk_id "bool") = 0 -> string "bool"
+ | id when Id.compare id (mk_id "unit") = 0 -> string "unit"
+ | id when Id.compare id (mk_id "real") = 0 -> string "Num.num"
| id -> zencode ctx id
let rec ocaml_typ ctx (Typ_aux (typ_aux, _)) =
@@ -84,6 +89,7 @@ let ocaml_lit (L_aux (lit_aux, _)) =
| L_num n -> parens (string "big_int_of_int" ^^ space ^^ string (string_of_int n))
| L_undef -> failwith "undefined should have been re-written prior to ocaml backend"
| L_string str -> dquotes (string (String.escaped str))
+ | L_real str -> parens (string "Num.num_of_string" ^^ space ^^ dquotes (string (String.escaped str)))
| _ -> string "LIT"
let rec ocaml_pat ctx (P_aux (pat_aux, _) as pat) =
@@ -110,10 +116,10 @@ let rec ocaml_exp ctx (E_aux (exp_aux, _) as exp) =
| E_app (f, [x]) when Env.is_union_constructor f (env_of exp) -> zencode_upper ctx f ^^ space ^^ ocaml_atomic_exp ctx x
| E_app (f, [x]) -> zencode ctx f ^^ space ^^ ocaml_atomic_exp ctx x
| E_app (f, xs) when Env.is_union_constructor f (env_of exp) ->
- zencode_upper ctx f ^^ space ^^ parens (separate_map (comma ^^ space) (ocaml_exp ctx) xs)
+ zencode_upper ctx f ^^ space ^^ parens (separate_map (comma ^^ space) (ocaml_atomic_exp ctx) xs)
| E_app (f, xs) ->
- zencode ctx f ^^ space ^^ parens (separate_map (comma ^^ space) (ocaml_exp ctx) xs)
- | E_vector_subrange (exp1, exp2, exp3) -> string "subrange" ^^ space ^^ parens (separate_map (comma ^^ space) (ocaml_exp ctx) [exp1; exp2; exp3])
+ zencode ctx f ^^ space ^^ parens (separate_map (comma ^^ space) (ocaml_atomic_exp ctx) xs)
+ | E_vector_subrange (exp1, exp2, exp3) -> string "subrange" ^^ space ^^ parens (separate_map (comma ^^ space) (ocaml_atomic_exp ctx) [exp1; exp2; exp3])
| E_return exp -> separate space [string "r.return"; ocaml_atomic_exp ctx exp]
| E_assert (exp, _) -> separate space [string "assert"; ocaml_atomic_exp ctx exp]
| E_cast (_, exp) -> ocaml_exp ctx exp
@@ -140,8 +146,19 @@ let rec ocaml_exp ctx (E_aux (exp_aux, _) as exp) =
^/^ ocaml_exp ctx exp
| E_internal_let (lexp, exp1, exp2) ->
separate space [string "let"; ocaml_atomic_lexp ctx lexp;
- equals; string "ref"; ocaml_atomic_exp ctx exp1; string "in"]
+ equals; string "ref"; parens (ocaml_atomic_exp ctx exp1 ^^ space ^^ colon ^^ space ^^ ocaml_typ ctx (Rewriter.simple_typ (typ_of exp1))); string "in"]
^/^ ocaml_exp ctx exp2
+ | E_loop (Until, cond, body) ->
+ let loop_body =
+ (ocaml_atomic_exp ctx body ^^ semi)
+ ^/^
+ separate space [string "if"; ocaml_atomic_exp ctx cond;
+ string "then loop ()";
+ string "else ()"]
+ in
+ (string "let rec loop () =" ^//^ loop_body)
+ ^/^ string "in"
+ ^/^ string "loop ()"
| E_loop (While, cond, body) ->
let loop_body =
separate space [string "if"; ocaml_atomic_exp ctx cond;
@@ -152,11 +169,22 @@ let rec ocaml_exp ctx (E_aux (exp_aux, _) as exp) =
^/^ string "in"
^/^ string "loop ()"
| E_lit _ | E_list _ | E_id _ | E_tuple _ -> ocaml_atomic_exp ctx exp
+ | E_for (id, exp_from, exp_to, exp_step, _, exp_body) ->
+ let loop_var = separate space [string "let"; zencode ctx id; equals; string "ref"; ocaml_atomic_exp ctx exp_from; string "in"] in
+ let loop_mod = string "add_big_int" ^^ space ^^ zencode ctx id ^^ space ^^ ocaml_atomic_exp ctx exp_step in
+ let loop_body =
+ separate space [string "if"; zencode ctx id; string "<="; ocaml_atomic_exp ctx exp_to]
+ ^/^ separate space [string "then";
+ parens (ocaml_atomic_exp ctx exp_body ^^ semi ^^ space ^^ string "loop" ^^ space ^^ parens loop_mod)]
+ ^/^ string "else ()"
+ in
+ (string ("let rec loop " ^ zencode_string (string_of_id id) ^ " =") ^//^ loop_body)
+ ^/^ string "in"
+ ^/^ (string "loop" ^^ space ^^ ocaml_atomic_exp ctx exp_from)
| _ -> string ("EXP(" ^ string_of_exp exp ^ ")")
and ocaml_letbind ctx (LB_aux (lb_aux, _)) =
match lb_aux with
| LB_val (pat, exp) -> separate space [ocaml_pat ctx pat; equals; ocaml_atomic_exp ctx exp]
- | _ -> failwith "Ocaml: Explicit letbind found"
and ocaml_pexps ctx = function
| [pexp] -> ocaml_pexp ctx pexp
| pexp :: pexps -> ocaml_pexp ctx pexp ^/^ ocaml_pexps ctx pexps
@@ -166,7 +194,7 @@ and ocaml_pexp ctx = function
separate space [bar; ocaml_pat ctx pat; string "->"]
^//^ group (ocaml_exp ctx exp)
| Pat_aux (Pat_when (pat, wh, exp), _) ->
- separate space [bar; ocaml_pat ctx pat; string "when"; ocaml_atomic_exp ctx exp; string "->"]
+ separate space [bar; ocaml_pat ctx pat; string "when"; ocaml_atomic_exp ctx wh; string "->"]
^//^ group (ocaml_exp ctx exp)
and ocaml_block ctx = function
| [exp] -> ocaml_exp ctx exp
@@ -182,7 +210,8 @@ and ocaml_atomic_exp ctx (E_aux (exp_aux, _) as exp) =
match Env.lookup_id id (env_of exp) with
| Local (Immutable, _) | Unbound -> zencode ctx id
| Enum _ | Union _ -> zencode_upper ctx id
- | Register _ | Local (Mutable, _) -> bang ^^ zencode ctx id
+ | Register _ -> parens (string ("trace \"REG: " ^ string_of_id id ^ "\";") ^^ space ^^ bang ^^ zencode ctx id)
+ | Local (Mutable, _) -> bang ^^ zencode ctx id
end
| E_list exps -> enclose lbracket rbracket (separate_map (semi ^^ space) (ocaml_exp ctx) exps)
| E_tuple exps -> parens (separate_map (comma ^^ space) (ocaml_exp ctx) exps)
@@ -234,15 +263,25 @@ let rec ocaml_funcl_matches ctx = function
| [clause] -> ocaml_funcl_match ctx clause
| (clause :: clauses) -> ocaml_funcl_match ctx clause ^/^ ocaml_funcl_matches ctx clauses
+let first_function = ref true
+
+let function_header () =
+ if !first_function
+ then (first_function := false; string "let rec")
+ else string "and"
+
let ocaml_funcls ctx = function
| [] -> failwith "Ocaml: empty function"
| [FCL_aux (FCL_Funcl (id, pat, exp),_)] ->
- separate space [string "let rec"; zencode ctx id; ocaml_pat ctx pat; equals; string "with_return (fun r ->"]
+ let Typ_aux (Typ_fn (typ1, typ2, _), _) = Bindings.find id ctx.val_specs in
+ let annot_pat = parens (ocaml_pat ctx pat ^^ space ^^ colon ^^ space ^^ ocaml_typ ctx typ1) in
+ let dbg = string ("trace_call \"Calling: " ^ string_of_id id ^ "\";") in
+ separate space [function_header (); zencode ctx id; annot_pat; colon; ocaml_typ ctx typ2; equals; dbg; string "with_return (fun r ->"]
^//^ ocaml_exp ctx exp
^^ rparen
| funcls ->
let id = funcls_id funcls in
- separate space [string "let rec"; zencode ctx id; equals; string "function"]
+ separate space [function_header (); zencode ctx id; equals; string "function"]
^//^ ocaml_funcl_matches ctx funcls
let ocaml_fundef ctx (FD_aux (FD_function (_, _, _, funcls), _)) =
@@ -303,15 +342,35 @@ let get_externs (Defs defs) =
let ocaml_def_end = string ";;" ^^ twice hardline
+let nf_group doc =
+ first_function := true;
+ group doc
+
let ocaml_def ctx def = match def with
- | DEF_reg_dec ds -> group (ocaml_dec_spec ctx ds) ^^ ocaml_def_end
- | DEF_fundef fd -> group (ocaml_fundef ctx fd) ^^ ocaml_def_end
- | DEF_type td -> group (ocaml_typedef ctx td) ^^ ocaml_def_end
+ | DEF_reg_dec ds -> nf_group (ocaml_dec_spec ctx ds) ^^ ocaml_def_end
+ | DEF_fundef fd -> group (ocaml_fundef ctx fd) ^^ twice hardline
+ | DEF_type td -> nf_group (ocaml_typedef ctx td) ^^ ocaml_def_end
+ | DEF_val lb -> nf_group (string "let" ^^ space ^^ ocaml_letbind ctx lb) ^^ ocaml_def_end
| _ -> empty
+let val_spec_typs (Defs defs) =
+ let typs = ref (Bindings.empty) in
+ let val_spec_typ (VS_aux (vs_aux, _)) =
+ match vs_aux with
+ | VS_val_spec (TypSchm_aux (TypSchm_ts (_, typ), _), id, _, _) -> typs := Bindings.add id typ !typs
+ in
+ let rec vs_typs = function
+ | DEF_spec vs :: defs -> val_spec_typ vs; vs_typs defs
+ | _ :: defs -> vs_typs defs
+ | [] -> []
+ in
+ vs_typs defs;
+ !typs
+
let ocaml_defs (Defs defs) =
let ctx = { register_inits = get_initialize_registers defs;
- externs = get_externs (Defs defs)
+ externs = get_externs (Defs defs);
+ val_specs = val_spec_typs (Defs defs)
}
in
let empty_reg_init =
@@ -333,6 +392,7 @@ let ocaml_main spec =
^//^ (string "Random.self_init ();"
^/^ string "load_elf ();"
^/^ string "initialize_registers ();"
+ ^/^ string "Printexc.record_backtrace true;"
^/^ string "zmain ()")
]
diff --git a/src/pretty_print_lem.ml b/src/pretty_print_lem.ml
index a890e039..0cb95db1 100644
--- a/src/pretty_print_lem.ml
+++ b/src/pretty_print_lem.ml
@@ -62,7 +62,7 @@ let is_number_char c =
c = '0' || c = '1' || c = '2' || c = '3' || c = '4' || c = '5' ||
c = '6' || c = '7' || c = '8' || c = '9'
-let fix_id remove_tick name = match name with
+let rec fix_id remove_tick name = match name with
| "assert"
| "lsl"
| "lsr"
@@ -82,7 +82,9 @@ let fix_id remove_tick name = match name with
| "integer"
-> name ^ "'"
| _ ->
- if name.[0] = '\'' then
+ if String.contains name '#' then
+ fix_id remove_tick (String.concat "_" (Util.split_on_char '#' name))
+ else if name.[0] = '\'' then
let var = String.sub name 1 (String.length name - 1) in
if remove_tick then var else (var ^ "'")
else if is_number_char(name.[0]) then
@@ -285,9 +287,9 @@ let doc_lit_lem sequential mwords in_pat (L_aux(lit,l)) a =
| Typ_app (Id_aux (Id "register", _),_) -> utf8string "UndefinedRegister 0"
| Typ_id (Id_aux (Id "string", _)) -> utf8string "\"\""
| _ ->
+ let ta = if contains_t_pp_var typ then empty else doc_tannot_lem sequential mwords false typ in
parens
- ((utf8string "(failwith \"undefined value of unsupported type\")") ^^
- (doc_tannot_lem sequential mwords false typ)))
+ ((utf8string "(failwith \"undefined value of unsupported type\")") ^^ ta))
| _ -> utf8string "(failwith \"undefined value of unsupported type\")")
| L_string s -> utf8string ("\"" ^ s ^ "\"")
| L_real s ->
@@ -1058,7 +1060,15 @@ let doc_exp_lem, doc_let_lem =
raise (Reporting_basic.err_unreachable l
"pretty-printing non-constant sizeof expressions to Lem not supported"))
| E_return r ->
- align (string "early_return" ^//^ expV true r)
+ let ret_monad = if sequential then " : MR regstate" else " : MR" in
+ let ta =
+ if contains_t_pp_var (typ_of full_exp) || contains_t_pp_var (typ_of r)
+ then empty
+ else separate space
+ [string ret_monad;
+ parens (doc_typ_lem sequential mwords (typ_of full_exp));
+ parens (doc_typ_lem sequential mwords (typ_of r))] in
+ align (parens (string "early_return" ^//^ expV true r ^//^ ta))
| E_constraint _ | E_comment _ | E_comment_struc _ -> empty
| E_internal_cast _ | E_internal_exp _ | E_sizeof_internal _ | E_internal_exp_user _ ->
raise (Reporting_basic.err_unreachable l
@@ -1110,9 +1120,10 @@ let rec doc_range_lem (BF_aux(r,_)) = match r with
| BF_concat(ir1,ir2) -> (doc_range ir1) ^^ comma ^^ (doc_range ir2)
let doc_typdef_lem sequential mwords (TD_aux(td, (l, annot))) = match td with
- | TD_abbrev(id,nm,typschm) ->
- doc_op equals (concat [string "type"; space; doc_id_lem_type id])
- (doc_typschm_lem sequential mwords false typschm)
+ | TD_abbrev(id,nm,(TypSchm_aux (TypSchm_ts (typq, _), _) as typschm)) ->
+ doc_op equals
+ (separate space [string "type"; doc_id_lem_type id; doc_typquant_items_lem typq])
+ (doc_typschm_lem sequential mwords false typschm)
| TD_record(id,nm,typq,fs,_) ->
let fname fid = if prefix_recordtype
then concat [doc_id_lem id;string "_";doc_id_lem_type fid;]
@@ -1575,6 +1586,7 @@ let rec doc_def_lem sequential mwords def =
(* let _ = Pretty_print_sail.pp_defs stderr (Defs [def]) in *)
match def with
| DEF_spec v_spec -> (empty,doc_spec_lem sequential mwords v_spec)
+ | DEF_fixity _ -> (empty,empty)
| DEF_overload _ -> (empty,empty)
| DEF_type t_def -> (group (doc_typdef_lem sequential mwords t_def) ^/^ hardline,empty)
| DEF_reg_dec dec -> (group (doc_dec_lem sequential dec),empty)
diff --git a/src/pretty_print_lem_ast.ml b/src/pretty_print_lem_ast.ml
index 2e464a08..2232b4de 100644
--- a/src/pretty_print_lem_ast.ml
+++ b/src/pretty_print_lem_ast.ml
@@ -234,6 +234,17 @@ let pp_lem_nexp ppf n = base ppf (pp_format_nexp_lem n)
let pp_lem_ord ppf o = base ppf (pp_format_ord_lem o)
let pp_lem_effects ppf e = base ppf (pp_format_effects_lem e)
let pp_lem_beffect ppf be = base ppf (pp_format_base_effect_lem be)
+let pp_lem_loop ppf l =
+ let l_str = match l with
+ | While -> "While"
+ | Until -> "Until" in
+ base ppf l_str
+let pp_lem_prec ppf p =
+ let p_str = match p with
+ | Infix -> "Infix"
+ | InfixL -> "InfixL"
+ | InfixR -> "InfixR" in
+ base ppf p_str
let pp_lem_nexp_constraint ppf nc = base ppf (pp_format_nexp_constraint_lem nc)
@@ -380,6 +391,9 @@ and pp_lem_exp ppf (E_aux(e,(l,annot))) =
fprintf ppf "@[<0>(E_aux (E_for %a %a %a %a %a @ @[<1> %a @]) (%a, %a))@]"
pp_lem_id id pp_lem_exp exp1 pp_lem_exp exp2 pp_lem_exp exp3
pp_lem_ord order pp_lem_exp exp4 pp_lem_l l pp_annot annot
+ | E_loop(loop,cond,body) ->
+ fprintf ppf "@[<0>(E_aux (E_loop %a %a @ @[<1> %a @]) (%a, %a))@]"
+ pp_lem_loop loop pp_lem_exp cond pp_lem_exp body pp_lem_l l pp_annot annot
| E_vector(exps) -> fprintf ppf "@[<0>(E_aux (%a [%a]) (%a, %a))@]"
kwd "E_vector" (list_pp pp_semi_lem_exp pp_lem_exp) exps pp_lem_l l pp_annot annot
| E_vector_access(v,e) ->
@@ -634,6 +648,7 @@ let pp_lem_def ppf d =
| DEF_val(lbind) -> fprintf ppf "(DEF_val %a);@\n" pp_lem_let lbind
| DEF_reg_dec(dec) -> fprintf ppf "(DEF_reg_dec %a);@\n" pp_lem_dec dec
| DEF_comm d -> fprintf ppf ""
+ | DEF_fixity (prec, n, id) -> fprintf ppf "(DEF_fixity %a %s %a);@\n" pp_lem_prec prec (lemnum string_of_int n) pp_lem_id id
| _ -> raise (Reporting_basic.err_unreachable Parse_ast.Unknown "initial_check didn't remove all scattered Defs")
let pp_lem_defs ppf (Defs(defs)) =
diff --git a/src/process_file.ml b/src/process_file.ml
index d35ccf5e..18df5047 100644
--- a/src/process_file.ml
+++ b/src/process_file.ml
@@ -259,5 +259,6 @@ let rewrite rewriters defs =
exit 1
let rewrite_ast = rewrite [("initial", Rewriter.rewrite_defs)]
+let rewrite_undefined = rewrite [("undefined", Rewriter.rewrite_undefined)]
let rewrite_ast_lem = rewrite Rewriter.rewrite_defs_lem
let rewrite_ast_ocaml = rewrite Rewriter.rewrite_defs_ocaml
diff --git a/src/process_file.mli b/src/process_file.mli
index c477d185..fae38100 100644
--- a/src/process_file.mli
+++ b/src/process_file.mli
@@ -45,6 +45,7 @@ val convert_ast : Ast.order -> Parse_ast.defs -> unit Ast.defs
val check_ast: unit Ast.defs -> Type_check.tannot Ast.defs * Type_check.Env.t
val monomorphise_ast : ((string * int) * string) list -> Type_check.tannot Ast.defs -> Type_check.tannot Ast.defs * Type_check.Env.t
val rewrite_ast: Type_check.tannot Ast.defs -> Type_check.tannot Ast.defs
+val rewrite_undefined: Type_check.tannot Ast.defs -> Type_check.tannot Ast.defs
val rewrite_ast_lem : Type_check.tannot Ast.defs -> Type_check.tannot Ast.defs
val rewrite_ast_ocaml : Type_check.tannot Ast.defs -> Type_check.tannot Ast.defs
diff --git a/src/rewriter.ml b/src/rewriter.ml
index bcc4e60a..60beadac 100644
--- a/src/rewriter.ml
+++ b/src/rewriter.ml
@@ -76,12 +76,18 @@ let effect_of_pexp (Pat_aux (pexp,(_,a))) = match a with
let effect_of_lb (LB_aux (_,(_,a))) = effect_of_annot a
let get_loc_exp (E_aux (_,(l,_))) = l
+let gen_loc l = Parse_ast.Generated l
-let simple_annot l typ = (Parse_ast.Generated l, Some (Env.empty, typ, no_effect))
+let simple_annot l typ = (gen_loc l, Some (Env.empty, typ, no_effect))
let simple_num l n = E_aux (
- E_lit (L_aux (L_num n, Parse_ast.Generated l)),
- simple_annot (Parse_ast.Generated l)
- (atom_typ (Nexp_aux (Nexp_constant n, Parse_ast.Generated l))))
+ E_lit (L_aux (L_num n, gen_loc l)),
+ simple_annot (gen_loc l)
+ (atom_typ (Nexp_aux (Nexp_constant n, gen_loc l))))
+let annot_exp_effect e_aux l env typ effect = E_aux (e_aux, (l, Some (env, typ, effect)))
+let annot_exp e_aux l env typ = annot_exp_effect e_aux l env typ no_effect
+let annot_pat p_aux l env typ = P_aux (p_aux, (l, Some (env, typ, no_effect)))
+let annot_letbind (p_aux, exp) l env typ =
+ LB_aux (LB_val (annot_pat p_aux l env typ, exp), (l, Some (env, typ, effect_of exp)))
let rec small (E_aux (exp,_)) = match exp with
| E_id _
@@ -103,15 +109,15 @@ let reset_fresh_name_counter () =
let fresh_id pre l =
let current = fresh_name () in
- Id_aux (Id (pre ^ string_of_int current), Parse_ast.Generated l)
+ Id_aux (Id (pre ^ string_of_int current), gen_loc l)
let fresh_id_exp pre ((l,annot)) =
let id = fresh_id pre l in
- E_aux (E_id id, (Parse_ast.Generated l, annot))
+ E_aux (E_id id, (gen_loc l, annot))
let fresh_id_pat pre ((l,annot)) =
let id = fresh_id pre l in
- P_aux (P_id id, (Parse_ast.Generated l, annot))
+ P_aux (P_id id, (gen_loc l, annot))
let union_eff_exps es =
List.fold_left union_effects no_effect (List.map effect_of es)
@@ -237,7 +243,8 @@ let effectful_effs = function
) effs
| _ -> true
-let effectful eaux = effectful_effs (effect_of eaux)
+let effectful eaux = effectful_effs (effect_of (propagate_exp_effect eaux))
+let effectful_pexp pexp = effectful_effs (snd (propagate_pexp_effect pexp))
let updates_vars_effs = function
| Effect_aux (Effect_set effs, _) ->
@@ -349,9 +356,9 @@ let vector_string_to_bit_list l lit =
| L_bin s_bin -> explode s_bin
| _ -> raise (Reporting_basic.err_unreachable l "s_bin given non vector literal") in
- List.map (function '0' -> L_aux (L_zero, Parse_ast.Generated l)
- | '1' -> L_aux (L_one,Parse_ast.Generated l)
- | _ -> raise (Reporting_basic.err_unreachable (Parse_ast.Generated l) "binary had non-zero or one")) s_bin
+ List.map (function '0' -> L_aux (L_zero, gen_loc l)
+ | '1' -> L_aux (L_one,gen_loc l)
+ | _ -> raise (Reporting_basic.err_unreachable (gen_loc l) "binary had non-zero or one")) s_bin
let rewrite_pat rewriters (P_aux (pat,(l,annot))) =
let rewrap p = P_aux (p,(l,annot)) in
@@ -1079,7 +1086,7 @@ let rewrite_sizeof (Defs defs) =
when string_of_id atom = "atom" ->
[nexp, E_id id]
| Typ_app (vector, _) when string_of_id vector = "vector" ->
- let id_length = Id_aux (Id "length", Parse_ast.Generated l) in
+ let id_length = Id_aux (Id "length", gen_loc l) in
(try
(match Env.get_val_spec id_length (env_of_annot annot) with
| _ ->
@@ -1115,7 +1122,8 @@ let rewrite_sizeof (Defs defs) =
(* Rewrite calls to functions which have had parameters added to pass values
of type-level variables; these are added as sizeof expressions first, and
then further rewritten as above. *)
- let e_app_aux param_map ((exp, exp_orig), ((l, Some (env, _, _)) as annot)) =
+ let e_app_aux param_map ((exp, exp_orig), ((l, _) as annot)) =
+ let env = env_of_annot annot in
let full_exp = E_aux (exp, annot) in
let orig_exp = E_aux (exp_orig, annot) in
match exp with
@@ -1143,7 +1151,7 @@ let rewrite_sizeof (Defs defs) =
(* If the type variable is Not_found then it was probably
introduced by a P_var pattern, so it likely exists as
a variable in scope. It can't be an existential because the assert rules that out. *)
- | None -> E_aux (E_id (id_of_kid (orig_kid kid)), simple_annot l (atom_typ (nvar (orig_kid kid))))
+ | None -> annot_exp (E_id (id_of_kid (orig_kid kid))) l env (atom_typ (nvar (orig_kid kid)))
| _ ->
raise (Reporting_basic.err_unreachable l
("failed to infer nexp for type variable " ^ string_of_kid kid ^
@@ -1415,6 +1423,7 @@ let remove_vector_concat_pat pat =
(* build a let-expression of the form "let child = root[i..j] in body" *)
let letbind_vec typ_opt (rootid,rannot) (child,cannot) (i,j) =
let (l,_) = cannot in
+ let env = env_of_annot rannot in
let rootname = string_of_id rootid in
let childname = string_of_id child in
@@ -1434,7 +1443,7 @@ let remove_vector_concat_pat pat =
| None -> P_aux (P_id child,cannot) in
let letbind = fix_eff_lb (LB_aux (LB_val (id_pat,subv),cannot)) in
(letbind,
- (fun body -> fix_eff_exp (E_aux (E_let (letbind,body), simple_annot l (typ_of body)))),
+ (fun body -> fix_eff_exp (annot_exp (E_let (letbind,body)) l env (typ_of body))),
(rootname,childname)) in
let p_aux = function
@@ -1562,7 +1571,7 @@ let remove_vector_concat_pat pat =
let typ = Env.base_typ_of env (typ_of_annot annot) in
let eff = effect_of_annot (snd annot) in
let (l,_) = annot in
- let wild _ = P_aux (P_wild,(Parse_ast.Generated l, Some (env, bit_typ, eff))) in
+ let wild _ = P_aux (P_wild,(gen_loc l, Some (env, bit_typ, eff))) in
if is_vector_typ typ then
match p, vector_typ_args_of typ with
| P_vector ps,_ -> acc @ ps
@@ -1751,10 +1760,17 @@ and fpat_to_fexp (FP_aux (FP_Fpat (id,pat),(l,annot))) =
FE_aux (FE_Fexp (id, pat_to_exp pat),(l,annot))
let case_exp e t cs =
- let pexp (pat,body,annot) = Pat_aux (Pat_exp (pat,body),annot) in
- let ps = List.map pexp cs in
- (* let efr = union_effs (List.map effect_of_pexp ps) in *)
- fix_eff_exp (E_aux (E_case (e,ps), (get_loc_exp e, Some (env_of e, t, no_effect))))
+ let l = get_loc_exp e in
+ let env = env_of e in
+ let annot = (get_loc_exp e, Some (env_of e, t, no_effect)) in
+ match cs with
+ | [(P_aux (P_id id, pannot) as pat, body, _)] ->
+ fix_eff_exp (annot_exp (E_let (LB_aux (LB_val (pat, e), pannot), body)) l env t)
+ | _ ->
+ let pexp (pat,body,annot) = Pat_aux (Pat_exp (pat,body),annot) in
+ let ps = List.map pexp cs in
+ (* let efr = union_effs (List.map effect_of_pexp ps) in *)
+ fix_eff_exp (annot_exp (E_case (e,ps)) l env t)
let rewrite_guarded_clauses l cs =
let rec group clauses =
@@ -1800,7 +1816,7 @@ let rewrite_guarded_clauses l cs =
if equiv_pats current_pat pat'
then if_exp current_pat (c' :: cs)
else case_exp (pat_to_exp current_pat) (typ_of body') (group (c' :: cs)) in
- fix_eff_exp (E_aux (E_if (exp,body,else_exp), simple_annot (fst annot) (typ_of body)))
+ fix_eff_exp (annot_exp (E_if (exp,body,else_exp)) (fst annot) (env_of exp) (typ_of body))
| None -> body)
| [(pat,guard,body,annot)] -> body
| [] ->
@@ -1810,8 +1826,8 @@ let rewrite_guarded_clauses l cs =
let bitwise_and_exp exp1 exp2 =
let (E_aux (_,(l,_))) = exp1 in
- let andid = Id_aux (Id "bool_and", Parse_ast.Generated l) in
- E_aux (E_app(andid,[exp1;exp2]), simple_annot l bool_typ)
+ let andid = Id_aux (Id "bool_and", gen_loc l) in
+ annot_exp (E_app(andid,[exp1;exp2])) l (env_of exp1) bool_typ
let rec contains_bitvector_pat (P_aux (pat,annot)) = match pat with
| P_lit _ | P_wild | P_id _ -> false
@@ -1833,6 +1849,8 @@ let contains_bitvector_pexp = function
let remove_bitvector_pat pat =
+ let env = try pat_env_of pat with _ -> Env.empty in
+
(* first introduce names for bitvector patterns *)
let name_bitvector_roots =
{ p_lit = (fun lit -> P_lit lit)
@@ -1868,23 +1886,20 @@ let remove_bitvector_pat pat =
bindings for the bits bound by P_id or P_as patterns *)
(* Helper functions for generating guard expressions *)
- let access_bit_exp (rootid,rannot) l idx =
- let root : tannot exp = E_aux (E_id rootid,rannot) in
+ let access_bit_exp rootid l typ idx =
+ let root = annot_exp (E_id rootid) l env typ in
(* FIXME *)
- E_aux (E_vector_access (root,simple_num l idx), simple_annot l bit_typ) in
+ annot_exp (E_vector_access (root, simple_num l idx)) l env bit_typ in
(*let env = env_of_annot rannot in
let t = Env.base_typ_of env (typ_of_annot rannot) in
let (_, _, ord, _) = vector_typ_args_of t in
let access_id = if is_order_inc ord then "bitvector_access_inc" else "bitvector_access_dec" in
E_aux (E_app (mk_id access_id, [root; simple_num l idx]), simple_annot l bit_typ) in*)
- let test_bit_exp rootid l t idx exp =
- let rannot = simple_annot l t in
- let elem = access_bit_exp (rootid,rannot) l idx in
- let eqid = Id_aux (Id "eq", Parse_ast.Generated l) in
- let eqannot = simple_annot l bool_typ in
- let eqexp : tannot exp = E_aux (E_app(eqid,[elem;exp]), eqannot) in
- Some (eqexp) in
+ let test_bit_exp rootid l typ idx exp =
+ let rannot = (l, Some (env_of exp, typ, no_effect)) in
+ let elem = access_bit_exp rootid l typ idx in
+ Some (annot_exp (E_app (mk_id "eq", [elem; exp])) l env bool_typ) in
let test_subvec_exp rootid l typ i j lits =
let (start, length, ord, _) = vector_typ_args_of typ in
@@ -1903,25 +1918,24 @@ let remove_bitvector_pat pat =
then E_id rootid
else*)
E_vector_subrange (
- E_aux (E_id rootid, simple_annot l typ),
+ annot_exp (E_id rootid) l env typ,
simple_num l i,
simple_num l j) in
(* let subrange_id = if is_order_inc ord then "bitvector_subrange_inc" else "bitvector_subrange_dec" in
E_app (mk_id subrange_id, [E_aux (E_id rootid, simple_annot l typ); simple_num l i; simple_num l j]) in *)
- E_aux (E_app(
- Id_aux (Id "eq_vec", Parse_ast.Generated l),
- [E_aux (subvec_exp, simple_annot l typ');
- E_aux (E_vector lits, simple_annot l typ')]),
- simple_annot l bool_typ) in
+ annot_exp (E_app(
+ Id_aux (Id "eq_vec", gen_loc l),
+ [annot_exp subvec_exp l env typ';
+ annot_exp (E_vector lits) l env typ'])) l env bool_typ in
let letbind_bit_exp rootid l typ idx id =
let rannot = simple_annot l typ in
- let elem = access_bit_exp (rootid,rannot) l idx in
- let e = P_aux (P_id id, simple_annot l bit_typ) in
- let letbind = LB_aux (LB_val (e,elem), simple_annot l bit_typ) in
+ let elem = access_bit_exp rootid l typ idx in
+ let e = annot_pat (P_id id) l env bit_typ in
+ let letbind = LB_aux (LB_val (e,elem), (l, Some (env, bit_typ, no_effect))) in
let letexp = (fun body ->
let (E_aux (_,(_,bannot))) = body in
- E_aux (E_let (letbind,body), (Parse_ast.Generated l, bannot))) in
+ annot_exp (E_let (letbind,body)) l env (typ_of body)) in
(letexp, letbind) in
let compose_guards guards =
@@ -1946,7 +1960,7 @@ let remove_bitvector_pat pat =
| pat :: ps' ->
(match pat with
| P_aux (P_lit lit, (l,annot)) ->
- let e = E_aux (E_lit lit, (Parse_ast.Generated l, annot)) in
+ let e = E_aux (E_lit lit, (gen_loc l, annot)) in
let current' = (match current with
| Some (l,i,j,lits) -> Some (l,i,idx,lits @ [e])
| None -> Some (l,idx,idx,[e])) in
@@ -2243,7 +2257,7 @@ let rewrite_exp_lift_assign_intro rewriters ((E_aux (exp,((l,_) as annot))) as f
when lexp_is_local_intro le (env_of full_exp) && not (lexp_is_effectful le) ->
let (le', re') = rewrite_local_lexp le in
let e' = re' (rewrite_base e) in
- let block = E_aux (E_block [], simple_annot l unit_typ) in
+ let block = annot_exp (E_block []) l (env_of full_exp) unit_typ in
fix_eff_exp (E_aux (E_internal_let(le', e', block), annot))
| _ -> rewrite_base full_exp
@@ -2328,13 +2342,13 @@ let rewrite_defs_early_return =
match es with
| [E_aux (e, _)] -> e
| _ :: _ when is_return (Util.last es) ->
- let (E_aux (_, annot) as e) = Util.last es in
+ let (E_aux (_, annot) as e) = get_return (Util.last es) in
E_return (E_aux (E_block (Util.butlast es @ [get_return e]), annot))
| _ -> E_block es in
let e_if (e1, e2, e3) =
if is_return e2 && is_return e3 then
- let (E_aux (_, annot)) = e2 in
+ let (E_aux (_, annot)) = get_return e2 in
E_return (E_aux (E_if (e1, get_return e2, get_return e3), annot))
else E_if (e1, e2, e3) in
@@ -2344,7 +2358,7 @@ let rewrite_defs_early_return =
let get_return_pexp (Pat_aux (pexp, a)) = match pexp with
| Pat_exp (p, e) -> Pat_aux (Pat_exp (p, get_return e), a)
| Pat_when (p, g, e) -> Pat_aux (Pat_when (p, g, get_return e), a) in
- let annot = match pes with
+ let annot = match List.map get_return_pexp pes with
| Pat_aux (Pat_exp (_, E_aux (_, annot)), _) :: _ -> annot
| Pat_aux (Pat_when (_, _, E_aux (_, annot)), _) :: _ -> annot
| [] -> (Parse_ast.Unknown, None) in
@@ -2526,6 +2540,26 @@ let rewrite_undefined =
let rewrite_exp_undefined = { id_exp_alg with e_aux = (fun (exp, annot) -> rewrite_e_aux (E_aux (exp, annot))) } in
rewrite_defs_base { rewriters_base with rewrite_exp = (fun _ -> fold_exp rewrite_exp_undefined) }
+let rec simple_typ (Typ_aux (typ_aux, l) as typ) = Typ_aux (simple_typ_aux typ_aux, l)
+and simple_typ_aux = function
+ | Typ_wild -> Typ_wild
+ | Typ_id id -> Typ_id id
+ | Typ_app (id, [_; _; _; Typ_arg_aux (Typ_arg_typ typ, l)]) when Id.compare id (mk_id "vector") = 0 ->
+ Typ_app (mk_id "list", [Typ_arg_aux (Typ_arg_typ (simple_typ typ), l)])
+ | Typ_app (id, [_]) when Id.compare id (mk_id "atom") = 0 ->
+ Typ_id (mk_id "int")
+ | Typ_app (id, [_; _]) when Id.compare id (mk_id "range") = 0 ->
+ Typ_id (mk_id "int")
+ | Typ_app (id, args) -> Typ_app (id, List.concat (List.map simple_typ_arg args))
+ | Typ_fn (typ1, typ2, effs) -> Typ_fn (simple_typ typ1, simple_typ typ2, effs)
+ | Typ_tup typs -> Typ_tup (List.map simple_typ typs)
+ | Typ_exist (_, _, Typ_aux (typ, l)) -> simple_typ_aux typ
+ | typ_aux -> typ_aux
+and simple_typ_arg (Typ_arg_aux (typ_arg_aux, l)) =
+ match typ_arg_aux with
+ | Typ_arg_typ typ -> [Typ_arg_aux (Typ_arg_typ (simple_typ typ), l)]
+ | _ -> []
+
(* This pass aims to remove all the Num quantifiers from the specification. *)
let rewrite_simple_types (Defs defs) =
let is_simple = function
@@ -2537,26 +2571,6 @@ let rewrite_simple_types (Defs defs) =
| TypQ_no_forall -> TypQ_aux (TypQ_no_forall, annot)
| TypQ_tq quants -> TypQ_aux (TypQ_tq (List.filter (fun q -> is_simple q) quants), annot)
in
- let rec simple_typ (Typ_aux (typ_aux, l) as typ) = Typ_aux (simple_typ_aux typ_aux, l)
- and simple_typ_aux = function
- | Typ_wild -> Typ_wild
- | Typ_id id -> Typ_id id
- | Typ_app (id, [_; _; _; Typ_arg_aux (Typ_arg_typ typ, l)]) when Id.compare id (mk_id "vector") = 0 ->
- Typ_app (mk_id "list", [Typ_arg_aux (Typ_arg_typ (simple_typ typ), l)])
- | Typ_app (id, [_]) when Id.compare id (mk_id "atom") = 0 ->
- Typ_id (mk_id "int")
- | Typ_app (id, [_; _]) when Id.compare id (mk_id "range") = 0 ->
- Typ_id (mk_id "int")
- | Typ_app (id, args) -> Typ_app (id, List.concat (List.map simple_typ_arg args))
- | Typ_fn (typ1, typ2, effs) -> Typ_fn (simple_typ typ1, simple_typ typ2, effs)
- | Typ_tup typs -> Typ_tup (List.map simple_typ typs)
- | Typ_exist (_, _, Typ_aux (typ, l)) -> simple_typ_aux typ
- | typ_aux -> typ_aux
- and simple_typ_arg (Typ_arg_aux (typ_arg_aux, l)) =
- match typ_arg_aux with
- | Typ_arg_typ typ -> [Typ_arg_aux (Typ_arg_typ (simple_typ typ), l)]
- | _ -> []
- in
let simple_typschm (TypSchm_aux (TypSchm_ts (typq, typ), annot)) =
TypSchm_aux (TypSchm_ts (simple_typquant typq, simple_typ typ), annot)
in
@@ -2621,7 +2635,7 @@ let rewrite_tuple_vector_assignments defs =
let i = match simplify_nexp start with
| (Nexp_aux (Nexp_constant i, _)) -> i
| _ -> if is_order_inc ord then 0 else List.length lexps - 1 in
- let l = Parse_ast.Generated (fst annot) in
+ let l = gen_loc (fst annot) in
let exp' =
if small exp then strip_exp exp
else mk_exp (E_id (mk_id "split_vec")) in
@@ -2699,14 +2713,19 @@ let rewrite_simple_assignments defs =
let rewrite_defs_remove_blocks =
let letbind_wild v body =
+ let l = get_loc_exp v in
+ let env = env_of v in
+ let typ = typ_of v in
+ annot_exp (E_let (annot_letbind (P_wild, v) l env typ, body)) l env (typ_of body) in
+ (* let pat = annot_pat P_wild l env typ in
let (E_aux (_,(l,tannot))) = v in
let annot_pat = (simple_annot l (typ_of v)) in
- let annot_lb = (Parse_ast.Generated l, tannot) in
- let annot_let = (Parse_ast.Generated l, Some (env_of body, typ_of body, union_eff_exps [v;body])) in
- E_aux (E_let (LB_aux (LB_val (P_aux (P_wild,annot_pat),v),annot_lb),body),annot_let) in
+ let annot_lb = (gen_loc l, tannot) in
+ let annot_let = (gen_loc l, Some (env_of body, typ_of body, union_eff_exps [v;body])) in
+ E_aux (E_let (LB_aux (LB_val (P_aux (P_wild,annot_pat),v),annot_lb),body),annot_let) in *)
let rec f l = function
- | [] -> E_aux (E_lit (L_aux (L_unit,Parse_ast.Generated l)), (simple_annot l unit_typ))
+ | [] -> E_aux (E_lit (L_aux (L_unit,gen_loc l)), (simple_annot l unit_typ))
| [e] -> e (* check with Kathy if that annotation is fine *)
| e :: es -> letbind_wild e (f l es) in
@@ -2733,27 +2752,15 @@ let letbind (v : 'a exp) (body : 'a exp -> 'a exp) : 'a exp =
let (E_aux (_,(l,annot))) = v in
match annot with
| Some (env, Typ_aux (Typ_id tid, _), eff) when string_of_id tid = "unit" ->
- let e = E_aux (E_lit (L_aux (L_unit,Parse_ast.Generated l)),(simple_annot l unit_typ)) in
- let body = body e in
+ let body = body (annot_exp (E_lit (mk_lit L_unit)) l env unit_typ) in
let body_typ = try typ_of body with _ -> unit_typ in
- let annot_pat = simple_annot l unit_typ in
- let annot_lb = annot_pat in
- let annot_let = (Parse_ast.Generated l, Some (env, body_typ, union_eff_exps [v;body])) in
- let pat = P_aux (P_wild,annot_pat) in
-
- E_aux (E_let (LB_aux (LB_val (pat,v),annot_lb),body),annot_let)
+ let lb = annot_letbind (P_wild, v) l env unit_typ in
+ propagate_exp_effect (annot_exp (E_let (lb, body)) l env body_typ)
| Some (env, typ, eff) ->
let id = fresh_id "w__" l in
- let annot_pat = simple_annot l typ in
- let e_id = E_aux (E_id id, (Parse_ast.Generated l, Some (env, typ, no_effect))) in
- let body = body e_id in
- let body_typ = try typ_of body with _ -> unit_typ in
-
- let annot_lb = annot_pat in
- let annot_let = (Parse_ast.Generated l, Some (env, body_typ, union_eff_exps [v;body])) in
- let pat = P_aux (P_id id,annot_pat) in
-
- E_aux (E_let (LB_aux (LB_val (pat,v),annot_lb),body),annot_let)
+ let lb = annot_letbind (P_id id, v) l env typ in
+ let body = body (annot_exp (E_id id) l env typ) in
+ propagate_exp_effect (annot_exp (E_let (lb, body)) l env (typ_of body))
| None ->
raise (Reporting_basic.err_unreachable l "no type information")
@@ -2853,8 +2860,8 @@ let rewrite_defs_letbind_effects =
let (E_aux (_,(l,tannot))) = exp in
let exp =
if newreturn then
- let typ = try typ_of exp with _ -> unit_typ in
- E_aux (E_internal_return exp, simple_annot l typ)
+ (* let typ = try typ_of exp with _ -> unit_typ in *)
+ annot_exp (E_internal_return exp) l (env_of exp) (typ_of exp)
else
exp in
(* n_exp_term forces an expression to be translated into a form
@@ -2947,10 +2954,7 @@ let rewrite_defs_letbind_effects =
n_exp_name exp1 (fun exp1 ->
k (rewrap (E_field (exp1,id))))
| E_case (exp1,pexps) ->
- let newreturn =
- List.fold_left
- (fun b pexp -> b || (try effectful_effs (effect_of_pexp pexp) with _ -> false))
- false pexps in
+ let newreturn = List.exists effectful_pexp pexps in
n_exp_name exp1 (fun exp1 ->
n_pexpL newreturn pexps (fun pexps ->
k (rewrap (E_case (exp1,pexps)))))
@@ -2995,10 +2999,8 @@ let rewrite_defs_letbind_effects =
| E_internal_plet _ -> failwith "E_internal_plet should not be here yet" in
let rewrite_fun _ (FD_aux (FD_function(recopt,tannotopt,effectopt,funcls),fdannot)) =
- let newreturn =
- List.fold_left
- (fun b (FCL_aux (FCL_Funcl(id,pat,exp),(_,annot))) ->
- b || (try effectful exp with _ -> false)) false funcls in
+ let effectful_funcl (FCL_aux (FCL_Funcl(_, _, exp), _)) = effectful exp in
+ let newreturn = List.exists effectful_funcl funcls in
let rewrite_funcl (FCL_aux (FCL_Funcl(id,pat,exp),annot)) =
let _ = reset_fresh_name_counter () in
FCL_aux (FCL_Funcl (id,pat,n_exp_term newreturn exp),annot)
@@ -3110,27 +3112,25 @@ let swaptyp typ (l,tannot) = match tannot with
let mktup l es =
match es with
- | [] -> E_aux (E_lit (L_aux (L_unit,Parse_ast.Generated l)),(simple_annot l unit_typ))
+ | [] -> annot_exp (E_lit (mk_lit L_unit)) (gen_loc l) Env.empty unit_typ
| [e] -> e
- | e :: _ ->
- let effs =
- List.fold_left (fun acc e -> union_effects acc (effect_of e)) no_effect es in
+ | e :: _ ->
let typ = mk_typ (Typ_tup (List.map typ_of es)) in
- E_aux (E_tuple es,(Parse_ast.Generated l, Some (env_of e, typ, effs)))
+ propagate_exp_effect (annot_exp (E_tuple es) (gen_loc l) (env_of e) typ)
let mktup_pat l es =
match es with
- | [] -> P_aux (P_wild,(simple_annot l unit_typ))
+ | [] -> annot_pat P_wild (gen_loc l) Env.empty unit_typ
| [E_aux (E_id id,_) as exp] ->
- P_aux (P_id id,(simple_annot l (typ_of exp)))
- | _ ->
+ annot_pat (P_id id) (gen_loc l) (env_of exp) (typ_of exp)
+ | exp :: _ ->
let typ = mk_typ (Typ_tup (List.map typ_of es)) in
let pats = List.map (function
| (E_aux (E_id id,_) as exp) ->
- P_aux (P_id id,(simple_annot l (typ_of exp)))
+ annot_pat (P_id id) (gen_loc l) (env_of exp) (typ_of exp)
| exp ->
- P_aux (P_wild,(simple_annot l (typ_of exp)))) es in
- P_aux (P_tup pats,(simple_annot l typ))
+ annot_pat P_wild (gen_loc l) (env_of exp) (typ_of exp)) es in
+ annot_pat (P_tup pats) (gen_loc l) (env_of exp) typ
type 'a updated_term =
@@ -3139,6 +3139,8 @@ type 'a updated_term =
let rec rewrite_var_updates ((E_aux (expaux,((l,_) as annot))) as exp) =
+ let env = env_of exp in
+
let rec add_vars overwrite ((E_aux (expaux,annot)) as exp) vars =
match expaux with
| E_let (lb,exp) ->
@@ -3163,7 +3165,7 @@ let rec rewrite_var_updates ((E_aux (expaux,((l,_) as annot))) as exp) =
| _ -> raise (Reporting_basic.err_unreachable l
"add_vars: trying to overwrite a non-unit expression in tail-position")
else
- let typ' = Typ_aux (Typ_tup [typ_of exp;typ_of vars], Parse_ast.Generated l) in
+ let typ' = Typ_aux (Typ_tup [typ_of exp;typ_of vars], gen_loc l) in
E_aux (E_tuple [exp;vars],swaptyp typ' annot) in
let rewrite (E_aux (expaux,((el,_) as annot))) (P_aux (_,(pl,pannot)) as pat) =
@@ -3192,7 +3194,7 @@ let rec rewrite_var_updates ((E_aux (expaux,((l,_) as annot))) as exp) =
| true, Ord_aux (Ord_dec,_) -> "foreachM_dec"
| _ -> raise (Reporting_basic.err_unreachable el
"Could not determine foreach combinator") in
- let funcl = Id_aux (Id fname,Parse_ast.Generated el) in
+ let funcl = Id_aux (Id fname,gen_loc el) in
let loopvar =
(* Don't bother with creating a range type annotation, since the
Lem pretty-printing does not use it. *)
@@ -3211,13 +3213,12 @@ let rec rewrite_var_updates ((E_aux (expaux,((l,_) as annot))) as exp) =
let t = {t = Tapp ("range",match order with
| Ord_aux (Ord_inc,_) -> [bf;tt]
| Ord_aux (Ord_dec,_) -> [tf;bt])} in *)
- E_aux (E_id id, simple_annot l int_typ) in
+ annot_exp (E_id id) l env int_typ in
let v = E_aux (E_app (funcl,[loopvar;mktup el [exp1;exp2;exp3];exp4;vartuple]),
- (Parse_ast.Generated el, annot4)) in
+ (gen_loc el, annot4)) in
let pat =
if overwrite then mktup_pat el vars
- else P_aux (P_tup [pat; mktup_pat pl vars],
- simple_annot pl (typ_of v)) in
+ else annot_pat (P_tup [pat; mktup_pat pl vars]) pl env (typ_of v) in
Added_vars (v,pat)
| E_loop(loop,cond,body) ->
let vars = List.map (fun (var,(l,t)) -> E_aux (E_id var,(l,t))) (find_updated_vars body) in
@@ -3230,17 +3231,15 @@ let rec rewrite_var_updates ((E_aux (expaux,((l,_) as annot))) as exp) =
| false, true -> "while_PM"
| true, false -> "while_MP"
| true, true -> "while_MM" in
- let funcl = Id_aux (Id fname,Parse_ast.Generated el) in
+ let funcl = Id_aux (Id fname,gen_loc el) in
let is_while =
match loop with
- | While -> E_aux (E_lit (mk_lit L_true), simple_annot el bool_typ)
- | Until -> E_aux (E_lit (mk_lit L_false), simple_annot el bool_typ) in
- let v = E_aux (E_app (funcl,[is_while;cond;body;vartuple]),
- (Parse_ast.Generated el, bannot)) in
+ | While -> annot_exp (E_lit (mk_lit L_true)) (gen_loc el) env bool_typ
+ | Until -> annot_exp (E_lit (mk_lit L_false)) (gen_loc el) env bool_typ in
+ let v = E_aux (E_app (funcl,[is_while;cond;body;vartuple]), (gen_loc el, bannot)) in
let pat =
if overwrite then mktup_pat el vars
- else P_aux (P_tup [pat; mktup_pat pl vars],
- simple_annot pl (typ_of v)) in
+ else annot_pat (P_tup [pat; mktup_pat pl vars]) pl env (typ_of v) in
Added_vars (v,pat)
| E_if (c,e1,e2) ->
let vars = List.map (fun (var,(l,t)) -> E_aux (E_id var,(l,t)))
@@ -3255,11 +3254,10 @@ let rec rewrite_var_updates ((E_aux (expaux,((l,_) as annot))) as exp) =
let env = env_of_annot annot in
let typ = typ_of e1 in
let eff = union_eff_exps [e1;e2] in
- let v = E_aux (E_if (c,e1,e2), (Parse_ast.Generated el, Some (env, typ, eff))) in
+ let v = E_aux (E_if (c,e1,e2), (gen_loc el, Some (env, typ, eff))) in
let pat =
if overwrite then mktup_pat el vars
- else P_aux (P_tup [pat; mktup_pat pl vars],
- (simple_annot pl (typ_of v))) in
+ else annot_pat (P_tup [pat; mktup_pat pl vars]) pl env (typ_of v) in
Added_vars (v,pat)
| E_case (e1,ps) ->
(* after rewrite_defs_letbind_effects e1 needs no rewriting *)
@@ -3277,10 +3275,19 @@ let rec rewrite_var_updates ((E_aux (expaux,((l,_) as annot))) as exp) =
Same_vars (E_aux (E_case (e1,ps),annot))
else
let vartuple = mktup el vars in
- let typ =
- let (Pat_aux ((Pat_exp (_,first)|Pat_when (_,_,first)),_)) = List.hd ps in
- typ_of first in
- let (ps,typ,effs) =
+ let rewrite_pexp (Pat_aux (pexp, (l, _))) = match pexp with
+ | Pat_exp (pat, exp) ->
+ let exp = rewrite_var_updates (add_vars overwrite exp vartuple) in
+ let pannot = (l, Some (env_of exp, typ_of exp, effect_of exp)) in
+ Pat_aux (Pat_exp (pat, exp), pannot)
+ | Pat_when _ ->
+ raise (Reporting_basic.err_unreachable l
+ "Guarded patterns should have been rewritten already") in
+ let typ = match ps with
+ | Pat_aux ((Pat_exp (_,first)|Pat_when (_,_,first)),_) :: _ -> typ_of first
+ | _ -> unit_typ in
+ let v = propagate_exp_effect (annot_exp (E_case (e1, List.map rewrite_pexp ps)) pl env typ) in
+ (* let (ps,typ,effs) =
let f (acc,typ,effs) (Pat_aux (Pat_exp (p,e),pannot)) =
let etyp = typ_of e in
let () = assert (string_of_typ etyp = string_of_typ typ) in
@@ -3290,11 +3297,10 @@ let rec rewrite_var_updates ((E_aux (expaux,((l,_) as annot))) as exp) =
let pat' = Pat_aux (Pat_exp (p,e),pannot) in
(acc @ [pat'],typ,effs) in
List.fold_left f ([],typ,no_effect) ps in
- let v = E_aux (E_case (e1,ps), (Parse_ast.Generated pl, Some (env_of_annot annot, typ, effs))) in
+ let v = E_aux (E_case (e1,ps), (gen_loc pl, Some (env_of_annot annot, typ, effs))) in *)
let pat =
if overwrite then mktup_pat el vars
- else P_aux (P_tup [pat; mktup_pat pl vars],
- (simple_annot pl (typ_of v))) in
+ else annot_pat (P_tup [pat; mktup_pat pl vars]) pl env (typ_of v) in
Added_vars (v,pat)
| E_assign (lexp,vexp) ->
let effs = match effect_of_annot (snd annot) with
@@ -3307,23 +3313,21 @@ let rec rewrite_var_updates ((E_aux (expaux,((l,_) as annot))) as exp) =
else
(match lexp with
| LEXP_aux (LEXP_id id,annot) ->
- let pat = P_aux (P_id id, simple_annot pl (typ_of vexp)) in
+ let pat = annot_pat (P_id id) pl env (typ_of vexp) in
Added_vars (vexp,pat)
| LEXP_aux (LEXP_cast (_,id),annot) ->
- let pat = P_aux (P_id id, simple_annot pl (typ_of vexp)) in
+ let pat = annot_pat (P_id id) pl env (typ_of vexp) in
Added_vars (vexp,pat)
| LEXP_aux (LEXP_vector (LEXP_aux (LEXP_id id,((l2,_) as annot2)),i),((l1,_) as annot)) ->
- let eid = E_aux (E_id id, simple_annot l2 (typ_of_annot annot2)) in
- let vexp = E_aux (E_vector_update (eid,i,vexp),
- simple_annot l1 (typ_of_annot annot)) in
- let pat = P_aux (P_id id, simple_annot pl (typ_of vexp)) in
+ let eid = annot_exp (E_id id) l2 env (typ_of_annot annot2) in
+ let vexp = annot_exp (E_vector_update (eid,i,vexp)) l1 env (typ_of_annot annot) in
+ let pat = annot_pat (P_id id) pl env (typ_of vexp) in
Added_vars (vexp,pat)
| LEXP_aux (LEXP_vector_range (LEXP_aux (LEXP_id id,((l2,_) as annot2)),i,j),
((l,_) as annot)) ->
- let eid = E_aux (E_id id, simple_annot l2 (typ_of_annot annot2)) in
- let vexp = E_aux (E_vector_update_subrange (eid,i,j,vexp),
- simple_annot l (typ_of_annot annot)) in
- let pat = P_aux (P_id id, simple_annot pl (typ_of vexp)) in
+ let eid = annot_exp (E_id id) l2 env (typ_of_annot annot2) in
+ let vexp = annot_exp (E_vector_update_subrange (eid,i,j,vexp)) l env (typ_of_annot annot) in
+ let pat = annot_pat (P_id id) pl env (typ_of vexp) in
Added_vars (vexp,pat)
| _ -> Same_vars (E_aux (E_assign (lexp,vexp),annot)))
| _ ->
@@ -3334,32 +3338,35 @@ let rec rewrite_var_updates ((E_aux (expaux,((l,_) as annot))) as exp) =
match expaux with
| E_let (lb,body) ->
let body = rewrite_var_updates body in
- let (eff,lb) = match lb with
- | LB_aux (LB_val (pat,v),lbannot) ->
- (match rewrite v pat with
- | Added_vars (v,pat) ->
- let (E_aux (_,(l,_))) = v in
- let lbannot = (simple_annot l (typ_of v)) in
- (effect_of v,LB_aux (LB_val (pat,v),lbannot))
- | Same_vars v -> (effect_of v,LB_aux (LB_val (pat,v),lbannot))) in
- let tannot = Some (env_of_annot annot, typ_of body, union_effects eff (effect_of body)) in
- E_aux (E_let (lb,body),(Parse_ast.Generated l,tannot))
+ let (LB_aux (LB_val (pat, v), lbannot)) = lb in
+ let lb = match rewrite v pat with
+ | Added_vars (v, P_aux (pat, _)) ->
+ annot_letbind (pat, v) (get_loc_exp v) env (typ_of v)
+ | Same_vars v -> LB_aux (LB_val (pat, v),lbannot) in
+ propagate_exp_effect (annot_exp (E_let (lb, body)) l env (typ_of body))
| E_internal_let (lexp,v,body) ->
(* Rewrite E_internal_let into E_let and call recursively *)
let id = match lexp with
| LEXP_aux (LEXP_id id,_) -> id
- | LEXP_aux (LEXP_cast (_,id),_) -> id in
- let env = env_of_annot annot in
+ | LEXP_aux (LEXP_cast (_,id),_) -> id
+ | _ ->
+ raise (Reporting_basic.err_unreachable l
+ "E_internal_let with a lexp that is not a variable") in
+ let pat = annot_pat (P_id id) l env (typ_of v) in
+ let lb = annot_letbind (P_id id, v) l env (typ_of v) in
+ let exp = propagate_exp_effect (annot_exp (E_let (lb, body)) l env (typ_of body)) in
+ rewrite_var_updates exp
+ (* let env = env_of_annot annot in
let vtyp = typ_of v in
let veff = effect_of v in
let bodyenv = env_of body in
let bodytyp = typ_of body in
let bodyeff = effect_of body in
let pat = P_aux (P_id id, (simple_annot l vtyp)) in
- let lbannot = (Parse_ast.Generated l, Some (env, vtyp, veff)) in
+ let lbannot = (gen_loc l, Some (env, vtyp, veff)) in
let lb = LB_aux (LB_val (pat,v),lbannot) in
- let exp = E_aux (E_let (lb,body),(Parse_ast.Generated l, Some (bodyenv, bodytyp, union_effects veff bodyeff))) in
- rewrite_var_updates exp
+ let exp = E_aux (E_let (lb,body),(gen_loc l, Some (bodyenv, bodytyp, union_effects veff bodyeff))) in
+ rewrite_var_updates exp *)
| E_internal_plet (pat,v,body) ->
failwith "rewrite_var_updates: E_internal_plet shouldn't be introduced yet"
(* There are no expressions that have effects or variable updates in
@@ -3509,7 +3516,8 @@ let rewrite_defs_lem = [
let rewrite_defs_ocaml = [
(* ("top_sort_defs", top_sort_defs); *)
- ("undefined", rewrite_undefined);
+ (* ("undefined", rewrite_undefined); *)
+ ("tuple_vector_assignments", rewrite_tuple_vector_assignments);
("tuple_assignments", rewrite_tuple_assignments);
("simple_assignments", rewrite_simple_assignments);
("remove_vector_concat", rewrite_defs_remove_vector_concat);
diff --git a/src/rewriter.mli b/src/rewriter.mli
index 1c3e8fae..73337de4 100644
--- a/src/rewriter.mli
+++ b/src/rewriter.mli
@@ -56,9 +56,12 @@ type 'a rewriters = { rewrite_exp : 'a rewriters -> 'a exp -> 'a exp;
val rewrite_exp : tannot rewriters -> tannot exp -> tannot exp
val rewrite_defs : tannot defs -> tannot defs
+val rewrite_undefined : tannot defs -> tannot defs
val rewrite_defs_ocaml : (string * (tannot defs -> tannot defs)) list (*Perform rewrites to exclude AST nodes not supported for ocaml out*)
val rewrite_defs_lem : (string * (tannot defs -> tannot defs)) list (*Perform rewrites to exclude AST nodes not supported for lem out*)
+val simple_typ : typ -> typ
+
(* the type of interpretations of pattern-matching expressions *)
type ('a,'pat,'pat_aux,'fpat,'fpat_aux) pat_alg =
{ p_lit : lit -> 'pat_aux
diff --git a/src/sail.ml b/src/sail.ml
index ca121a79..9c447f36 100644
--- a/src/sail.ml
+++ b/src/sail.ml
@@ -170,7 +170,11 @@ let main() =
| locs -> monomorphise_ast locs ast
in
- let ast = rewrite_ast ast in
+ let ast =
+ if !Initial_check.opt_undefined_gen then
+ rewrite_undefined (rewrite_ast ast)
+ else rewrite_ast ast in
+
let out_name = match !opt_file_out with
| None -> fst (List.hd parsed)
| Some f -> f ^ ".sail" in
diff --git a/src/spec_analysis.ml b/src/spec_analysis.ml
index 2e368c53..c896f07a 100644
--- a/src/spec_analysis.ml
+++ b/src/spec_analysis.ml
@@ -534,6 +534,7 @@ let fv_of_def consider_var consider_scatter_as_one all_defs = function
| DEF_fundef fdef -> fv_of_fun consider_var fdef
| DEF_val lebind -> ((fun (b,u,_) -> (b,u)) (fv_of_let consider_var mt mt mt lebind))
| DEF_spec vspec -> fv_of_vspec consider_var vspec
+ | DEF_fixity _ -> mt,mt
| DEF_overload (id,ids) -> init_env (string_of_id id), List.fold_left (fun ns id -> Nameset.add (string_of_id id) ns) mt ids
| DEF_default def -> mt,mt
| DEF_scattered sdef -> fv_of_scattered consider_var consider_scatter_as_one all_defs sdef
diff --git a/src/type_check.ml b/src/type_check.ml
index 3b13abb8..58de77e1 100644
--- a/src/type_check.ml
+++ b/src/type_check.ml
@@ -2027,16 +2027,15 @@ let rec check_exp env (E_aux (exp_aux, (l, ())) as exp : unit exp) (Typ_aux (typ
| E_throw exp, _ ->
let checked_exp = crule check_exp env exp exc_typ in
annot_exp_effect (E_throw checked_exp) typ (mk_effect [BE_escape])
+ | E_internal_let (lexp, bind, exp), _ ->
+ let E_aux (E_assign (lexp, bind), _), env = bind_assignment env lexp bind in
+ let checked_exp = crule check_exp env exp typ in
+ annot_exp (E_internal_let (lexp, bind, checked_exp)) typ
| E_vector vec, _ ->
- begin
- let (start, len, ord, vtyp) = destruct_vec_typ l env typ in
- let checked_items = List.map (fun i -> crule check_exp env i vtyp) vec in
- match nexp_simp len with
- | Nexp_aux (Nexp_constant lenc, _) ->
- if List.length vec = lenc then annot_exp (E_vector checked_items) typ
- else typ_error l "List length didn't match" (* FIXME: improve error message *)
- | _ -> typ_error l "Cannot check list constant against non-constant length vector type"
- end
+ let (start, len, ord, vtyp) = destruct_vec_typ l env typ in
+ let checked_items = List.map (fun i -> crule check_exp env i vtyp) vec in
+ if prove env (nc_eq (nconstant (List.length vec)) (nexp_simp len)) then annot_exp (E_vector checked_items) typ
+ else typ_error l "List length didn't match" (* FIXME: improve error message *)
| E_lit (L_aux (L_undef, _) as lit), _ ->
annot_exp_effect (E_lit lit) typ (mk_effect [BE_undef])
(* This rule allows registers of type t to be passed by name with type register<t>*)
@@ -2981,6 +2980,11 @@ and propagate_exp_effect_aux = function
let p_lexp = propagate_lexp_effect lexp in
let p_exp = propagate_exp_effect exp in
E_assign (p_lexp, p_exp), union_effects (effect_of p_exp) (effect_of_lexp p_lexp)
+ | E_internal_let (lexp, bind, exp) ->
+ let p_lexp = propagate_lexp_effect lexp in
+ let p_bind = propagate_exp_effect bind in
+ let p_exp = propagate_exp_effect exp in
+ E_internal_let (p_lexp, p_bind, p_exp), union_effects (effect_of_lexp p_lexp) (collect_effects [p_bind; p_exp])
| E_sizeof nexp -> E_sizeof nexp, no_effect
| E_constraint nc -> E_constraint nc, no_effect
| E_exit exp ->
@@ -2999,6 +3003,21 @@ and propagate_exp_effect_aux = function
| E_field (exp, id) ->
let p_exp = propagate_exp_effect exp in
E_field (p_exp, id), effect_of p_exp
+ | E_internal_let (lexp, exp, body) ->
+ let p_lexp = propagate_lexp_effect lexp in
+ let p_exp = propagate_exp_effect exp in
+ let p_body = propagate_exp_effect body in
+ E_internal_let (p_lexp, p_exp, p_body),
+ union_effects (effect_of_lexp p_lexp) (collect_effects [p_exp; p_body])
+ | E_internal_plet (pat, exp, body) ->
+ let p_pat = propagate_pat_effect pat in
+ let p_exp = propagate_exp_effect exp in
+ let p_body = propagate_exp_effect body in
+ E_internal_plet (p_pat, p_exp, p_body),
+ union_effects (effect_of_pat p_pat) (collect_effects [p_exp; p_body])
+ | E_internal_return exp ->
+ let p_exp = propagate_exp_effect exp in
+ E_internal_return p_exp, effect_of p_exp
| exp_aux -> typ_error Parse_ast.Unknown ("Unimplemented: Cannot propagate effect in expression "
^ string_of_exp (E_aux (exp_aux, (Parse_ast.Unknown, None))))
diff --git a/src/type_check.mli b/src/type_check.mli
index b6b5e75e..ff9eb74e 100644
--- a/src/type_check.mli
+++ b/src/type_check.mli
@@ -241,6 +241,7 @@ val unify : l -> Env.t -> typ -> typ -> uvar KBindings.t * kid list * n_constrai
val instantiation_of : tannot exp -> uvar KBindings.t
val propagate_exp_effect : tannot exp -> tannot exp
+val propagate_pexp_effect : tannot pexp -> tannot pexp * effect
(* Fully type-check an AST
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-10 01:14:29 +0000