summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/ast_util.ml14
-rw-r--r--src/ast_util.mli1
-rw-r--r--src/gen_lib/prompt.lem19
-rw-r--r--src/gen_lib/sail_values.lem4
-rw-r--r--src/gen_lib/state.lem25
-rw-r--r--src/initial_check.mli2
-rw-r--r--src/lem_interp/sail_impl_base.lem11
-rw-r--r--src/pretty_print_lem.ml698
-rw-r--r--src/pretty_print_lem_ast.ml3
-rw-r--r--src/pretty_print_sail2.ml21
-rw-r--r--src/rewriter.ml665
-rw-r--r--src/spec_analysis.ml4
-rw-r--r--src/type_check.ml134
-rw-r--r--src/type_check.mli2
-rw-r--r--src/util.mli2
15 files changed, 749 insertions, 856 deletions
diff --git a/src/ast_util.ml b/src/ast_util.ml
index d26e12ed..7d2d320b 100644
--- a/src/ast_util.ml
+++ b/src/ast_util.ml
@@ -612,8 +612,8 @@ let rec string_of_exp (E_aux (exp, _)) =
| E_comment _ -> "INTERNAL COMMENT"
| E_comment_struc _ -> "INTERNAL COMMENT STRUC"
| E_internal_let _ -> "INTERNAL LET"
- | E_internal_return _ -> "INTERNAL RETURN"
- | E_internal_plet _ -> "INTERNAL PLET"
+ | E_internal_return exp -> "internal_return (" ^ string_of_exp exp ^ ")"
+ | E_internal_plet (pat, exp, body) -> "internal_plet " ^ string_of_pat pat ^ " = " ^ string_of_exp exp ^ " in " ^ string_of_exp body
| _ -> "INTERNAL"
and string_of_fexp (FE_aux (FE_Fexp (field, exp), _)) =
string_of_id field ^ " = " ^ string_of_exp exp
@@ -704,6 +704,14 @@ let rec lexp_to_exp (LEXP_aux (lexp_aux, annot) as le) =
| LEXP_field (lexp, id) -> rewrap (E_field (lexp_to_exp lexp, id))
| LEXP_memory (id, exps) -> rewrap (E_app (id, exps))
+let destruct_range (Typ_aux (typ_aux, _)) =
+ match typ_aux with
+ | Typ_app (f, [Typ_arg_aux (Typ_arg_nexp n, _)])
+ when string_of_id f = "atom" -> Some (n, n)
+ | Typ_app (f, [Typ_arg_aux (Typ_arg_nexp n1, _); Typ_arg_aux (Typ_arg_nexp n2, _)])
+ when string_of_id f = "range" -> Some (n1, n2)
+ | _ -> None
+
let rec is_number (Typ_aux (t,_)) =
match t with
| Typ_id (Id_aux (Id "int", _))
@@ -819,6 +827,8 @@ let rec undefined_of_typ mwords l annot (Typ_aux (typ_aux, _) as typ) =
wrap (E_app (mk_id "undefined_bitvector",
undefined_of_typ_args mwords l annot start @
undefined_of_typ_args mwords l annot size)) typ
+ | Typ_app (atom, [Typ_arg_aux (Typ_arg_nexp i, _)]) when string_of_id atom = "atom" ->
+ wrap (E_sizeof i) typ
| Typ_app (id, args) ->
wrap (E_app (prepend_id "undefined_" id,
List.concat (List.map (undefined_of_typ_args mwords l annot) args))) typ
diff --git a/src/ast_util.mli b/src/ast_util.mli
index 2059bb7f..7e22a6e7 100644
--- a/src/ast_util.mli
+++ b/src/ast_util.mli
@@ -248,6 +248,7 @@ val is_bitvector_typ : typ -> bool
val typ_app_args_of : typ -> string * typ_arg_aux list * Ast.l
val vector_typ_args_of : typ -> nexp * nexp * order * typ
+val destruct_range : typ -> (nexp * nexp) option
val is_order_inc : order -> bool
diff --git a/src/gen_lib/prompt.lem b/src/gen_lib/prompt.lem
index 8ef9dd9b..4646ef6f 100644
--- a/src/gen_lib/prompt.lem
+++ b/src/gen_lib/prompt.lem
@@ -148,7 +148,7 @@ let write_reg_field_pos reg regfield i v =
write_reg_field_range reg regfield i i [v]
let write_reg_field_bit = write_reg_field_pos
-
+let write_reg_ref (reg, v) = write_reg reg v
val barrier : barrier_kind -> M unit
let barrier bk = Barrier bk (Done (), Nothing)
@@ -158,6 +158,19 @@ val footprint : M unit
let footprint = Footprint (Done (),Nothing)
+val iter_aux : forall 'regs 'e 'a. integer -> (integer -> 'a -> MR unit 'e) -> list 'a -> MR unit 'e
+let rec iter_aux i f xs = match xs with
+ | x :: xs -> f i x >> iter_aux (i + 1) f xs
+ | [] -> return ()
+ end
+
+val iteri : forall 'regs 'e 'a. (integer -> 'a -> MR unit 'e) -> list 'a -> MR unit 'e
+let iteri f xs = iter_aux 0 f xs
+
+val iter : forall 'regs 'e 'a. ('a -> MR unit 'e) -> list 'a -> MR unit 'e
+let iter f xs = iteri (fun _ x -> f x) xs
+
+
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 =
@@ -170,11 +183,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 (stop,i,by) vars body =
+let rec foreachM_dec (i,stop,by) vars body =
if (by > 0 && i >= stop) || (by < 0 && stop >= i)
then
body i vars >>= fun vars ->
- foreachM_dec (stop,i - by,by) vars body
+ foreachM_dec (i - by,stop,by) vars body
else return vars
val while_PP : forall 'vars. 'vars -> ('vars -> bool) -> ('vars -> 'vars) -> 'vars
diff --git a/src/gen_lib/sail_values.lem b/src/gen_lib/sail_values.lem
index bd18cf81..98ac2522 100644
--- a/src/gen_lib/sail_values.lem
+++ b/src/gen_lib/sail_values.lem
@@ -619,10 +619,10 @@ let rec foreach_inc (i,stop,by) vars body =
val foreach_dec : forall 'vars. (integer * integer * integer) -> 'vars ->
(integer -> 'vars -> 'vars) -> 'vars
-let rec foreach_dec (stop,i,by) vars body =
+let rec foreach_dec (i,stop,by) vars body =
if (by > 0 && i >= stop) || (by < 0 && stop >= i)
then let vars = body i vars in
- foreach_dec (stop,i - by,by) vars body
+ foreach_dec (i - by,stop,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 69b9e301..a089f8c5 100644
--- a/src/gen_lib/state.lem
+++ b/src/gen_lib/state.lem
@@ -15,6 +15,14 @@ type sequential_state 'regs =
write_ea : maybe (write_kind * integer * integer);
last_exclusive_operation_was_load : bool|>
+val init_state : forall 'regs. 'regs -> sequential_state 'regs
+let init_state regs =
+ <| regstate = regs;
+ memstate = Map.empty;
+ tagstate = Map.empty;
+ write_ea = Nothing;
+ last_exclusive_operation_was_load = false |>
+
(* State, nondeterminism and exception monad with result type 'a
and exception type 'e. *)
type ME 'regs 'a 'e = sequential_state 'regs -> list ((either 'a 'e) * sequential_state 'regs)
@@ -176,6 +184,8 @@ val write_reg : forall 'regs 'a. register_ref 'regs 'a -> 'a -> M 'regs unit
let write_reg reg v state =
[(Left (), <| state with regstate = reg.write_to state.regstate v |>)]
+let write_reg_ref (reg, v) = write_reg reg v
+
val update_reg : forall 'regs 'a 'b. register_ref 'regs 'a -> ('a -> 'b -> 'a) -> 'b -> M 'regs unit
let update_reg reg f v state =
let current_value = get_reg state reg in
@@ -218,6 +228,17 @@ let barrier _ = return ()
val footprint : forall 'regs. M 'regs unit
let footprint s = return () s
+val iter_aux : forall 'regs 'e 'a. integer -> (integer -> 'a -> ME 'regs unit 'e) -> list 'a -> ME 'regs unit 'e
+let rec iter_aux i f xs = match xs with
+ | x :: xs -> f i x >> iter_aux (i + 1) f xs
+ | [] -> return ()
+ end
+
+val iteri : forall 'regs 'e 'a. (integer -> 'a -> ME 'regs unit 'e) -> list 'a -> ME 'regs unit 'e
+let iteri f xs = iter_aux 0 f xs
+
+val iter : forall 'regs 'e 'a. ('a -> ME 'regs unit 'e) -> list 'a -> ME 'regs unit 'e
+let iter f xs = iteri (fun _ x -> f x) xs
val foreachM_inc : forall 'regs 'vars 'e. (integer * integer * integer) -> 'vars ->
(integer -> 'vars -> ME 'regs 'vars 'e) -> ME 'regs 'vars 'e
@@ -231,11 +252,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 (stop,i,by) vars body =
+let rec foreachM_dec (i,stop,by) vars body =
if (by > 0 && i >= stop) || (by < 0 && stop >= i)
then
body i vars >>= fun vars ->
- foreachM_dec (stop,i - by,by) vars body
+ foreachM_dec (i - by,stop,by) vars body
else return vars
val while_PP : forall 'vars. 'vars -> ('vars -> bool) -> ('vars -> 'vars) -> 'vars
diff --git a/src/initial_check.mli b/src/initial_check.mli
index feb9cb83..2a6b8349 100644
--- a/src/initial_check.mli
+++ b/src/initial_check.mli
@@ -48,3 +48,5 @@ val opt_undefined_gen : bool ref
val process_ast : order -> Parse_ast.defs -> unit defs
val val_spec_ids : 'a defs -> IdSet.t
+
+val val_spec_of_string : order -> id -> string -> unit def
diff --git a/src/lem_interp/sail_impl_base.lem b/src/lem_interp/sail_impl_base.lem
index eb2e1a4e..c7c6cd20 100644
--- a/src/lem_interp/sail_impl_base.lem
+++ b/src/lem_interp/sail_impl_base.lem
@@ -643,7 +643,7 @@ instance (Ord write_kind)
let (>=) = write_kindGreaterEq
end
-(* Barrier comparison that uses less memory in Isabelle/HOL
+(* Barrier comparison that uses less memory in Isabelle/HOL *)
let ~{ocaml} barrier_number = function
| Barrier_Sync -> (0 : natural)
| Barrier_LwSync -> 1
@@ -660,15 +660,15 @@ let ~{ocaml} barrier_number = function
| Barrier_MIPS_SYNC -> 12
end
- let ~{ocaml} barrier_kindCompare bk1 bk2 =
+let ~{ocaml} barrier_kindCompare bk1 bk2 =
let n1 = barrier_number bk1 in
let n2 = barrier_number bk2 in
if n1 < n2 then LT
else if n1 = n2 then EQ
else GT
-*)
+let inline {ocaml} barrier_kindCompare = defaultCompare
-let ~{ocaml} barrier_kindCompare bk1 bk2 =
+(*let ~{ocaml} barrier_kindCompare bk1 bk2 =
match (bk1, bk2) with
| (Barrier_Sync, Barrier_Sync) -> EQ
| (Barrier_Sync, _) -> LT
@@ -722,8 +722,7 @@ let ~{ocaml} barrier_kindCompare bk1 bk2 =
(* | (Barrier_MIPS_SYNC, _) -> LT
| (_, Barrier_MIPS_SYNC) -> GT *)
- end
-let inline {ocaml} barrier_kindCompare = defaultCompare
+ end*)
let ~{ocaml} barrier_kindLess b1 b2 = barrier_kindCompare b1 b2 = LT
let ~{ocaml} barrier_kindLessEq b1 b2 = barrier_kindCompare b1 b2 <> GT
diff --git a/src/pretty_print_lem.ml b/src/pretty_print_lem.ml
index 2855adbc..f5f58d14 100644
--- a/src/pretty_print_lem.ml
+++ b/src/pretty_print_lem.ml
@@ -248,8 +248,7 @@ let doc_typ_lem, doc_atomic_typ_lem =
| _ -> tup_typ sequential mwords atyp_needed ty
and tup_typ sequential mwords atyp_needed ((Typ_aux (t, _)) as ty) = match t with
| Typ_tup typs ->
- let tpp = separate_map (space ^^ star ^^ space) (app_typ sequential mwords false) typs in
- if atyp_needed then parens tpp else tpp
+ parens (separate_map (space ^^ star ^^ space) (app_typ sequential mwords false) typs)
| _ -> app_typ sequential mwords atyp_needed ty
and app_typ sequential mwords atyp_needed ((Typ_aux (t, l)) as ty) = match t with
| Typ_app(Id_aux (Id "vector", _), [
@@ -476,6 +475,12 @@ let rec doc_pat_lem sequential mwords apat_needed (P_aux (p,(l,annot)) as pa) =
| _ -> doc_id_lem id end
| P_var(p,kid) -> doc_pat_lem sequential mwords true p
| P_as(p,id) -> parens (separate space [doc_pat_lem sequential mwords true p; string "as"; doc_id_lem id])
+ | P_typ(Typ_aux (Typ_tup typs, _), P_aux (P_tup pats, _)) ->
+ (* Isabelle does not seem to like type-annotated tuple patterns;
+ it gives a syntax error. Avoid this by annotating the tuple elements instead *)
+ let doc_elem typ (P_aux (_, annot) as pat) =
+ doc_pat_lem sequential mwords true (P_aux (P_typ (typ, pat), annot)) in
+ parens (separate comma_sp (List.map2 doc_elem typs pats))
| P_typ(typ,p) ->
let doc_p = doc_pat_lem sequential mwords true p in
if contains_t_pp_var mwords typ then doc_p
@@ -507,9 +512,13 @@ and typ_needs_printed_arg (Typ_arg_aux (targ, _)) = match targ with
| _ -> false
let contains_early_return exp =
+ let e_app (f, args) =
+ let rets, args = List.split args in
+ (List.fold_left (||) (string_of_id f = "early_return") rets,
+ E_app (f, args)) in
fst (fold_exp
{ (Rewriter.compute_exp_alg false (||))
- with e_return = (fun (_, r) -> (true, E_return r)) } exp)
+ with e_return = (fun (_, r) -> (true, E_return r)); e_app = e_app } exp)
let typ_id_of (Typ_aux (typ, l)) = match typ with
| Typ_id id -> id
@@ -570,27 +579,11 @@ let doc_exp_lem, doc_let_lem =
(align (doc_lexp_deref_lem sequential mwords early_ret le ^/^
field_ref ^/^ expY e2 ^/^ expY e)))
| LEXP_aux (_, lannot) ->
- (match le with
- | LEXP_aux (_, (_, Some (_, Typ_aux (Typ_app (vector, [_; _; _; Typ_arg_aux (Typ_arg_typ etyp, _)]), _), _)))
- when is_reftyp etyp && string_of_id vector = "vector" ->
- (* Special case vectors of register references *)
- let deref =
- parens (separate space [
- string "access";
- expY (lexp_to_exp le);
- expY e2
- ]) in
- liftR ((prefix 2 1) (string "write_reg") (deref ^/^ expY e))
- | _ ->
- let deref = doc_lexp_deref_lem sequential mwords early_ret le in
- let call = if is_bitvector_typ (Env.base_typ_of (env_of full_exp) (typ_of_annot lannot)) then "write_reg_bit" else "write_reg_pos" in
- liftR ((prefix 2 1) (string call)
- (deref ^/^ expY e2 ^/^ expY e)))
+ let deref = doc_lexp_deref_lem sequential mwords early_ret le in
+ let call = if is_bitvector_typ (Env.base_typ_of (env_of full_exp) (typ_of_annot lannot)) then "write_reg_bit" else "write_reg_pos" in
+ liftR ((prefix 2 1) (string call)
+ (deref ^/^ expY e2 ^/^ expY e))
)
- (* | LEXP_field (le,id) when is_bit_typ t ->
- liftR ((prefix 2 1)
- (string "write_reg_bitfield")
- (doc_lexp_deref_lem sequential mwords early_ret le ^^ space ^^ string_lit(doc_id_lem id) ^/^ expY e)) *)
| LEXP_field ((LEXP_aux (_, lannot) as le),id) ->
let field_ref =
doc_id_lem (typ_id_of (typ_of_annot lannot)) ^^
@@ -602,34 +595,11 @@ let doc_exp_lem, doc_let_lem =
(string "write_reg_field")
(doc_lexp_deref_lem sequential mwords early_ret le ^^ space ^^
field_ref ^/^ expY e))
- (* | (LEXP_id id | LEXP_cast (_,id)), t, Alias alias_info ->
- (match alias_info with
- | Alias_field(reg,field) ->
- let f = match t with
- | (Tid "bit" | Tabbrev (_,{t=Tid "bit"})) ->
- string "write_reg_bitfield"
- | _ -> string "write_reg_field" in
- (prefix 2 1)
- f
- (separate space [string reg;string_lit(string field);expY e])
- | Alias_pair(reg1,reg2) ->
- string "write_two_regs" ^^ space ^^ string reg1 ^^ space ^^
- string reg2 ^^ space ^^ expY e) *)
| _ ->
liftR ((prefix 2 1) (string "write_reg") (doc_lexp_deref_lem sequential mwords early_ret le ^/^ expY e)))
| E_vector_append(le,re) ->
raise (Reporting_basic.err_unreachable l
"E_vector_append should have been rewritten before pretty-printing")
- (* let t = Env.base_typ_of (env_of full_exp) (typ_of full_exp) in
- let (call,ta,aexp_needed) =
- if is_bitvector_typ t then
- if not (contains_t_pp_var mwords t)
- then ("bitvector_concat", doc_tannot_lem sequential mwords false t, true)
- else ("bitvector_concat", empty, aexp_needed)
- else ("vector_concat",empty,aexp_needed) in
- let epp =
- align (group (separate space [string call;expY le;expY re])) ^^ ta in
- if aexp_needed then parens epp else epp *)
| E_cons(le,re) -> doc_op (group (colon^^colon)) (expY le) (expY re)
| E_if(c,t,e) ->
let (E_aux (_,(_,cannot))) = c in
@@ -647,80 +617,68 @@ let doc_exp_lem, doc_let_lem =
| E_app(f,args) ->
begin match f with
(* temporary hack to make the loop body a function of the temporary variables *)
- | Id_aux ((Id (("foreach_inc" | "foreach_dec" |
- "foreachM_inc" | "foreachM_dec" ) as loopf),_)) ->
- let [id;indices;body;e5] = args in
- let varspp = match e5 with
- | E_aux (E_tuple vars,_) ->
- let vars = List.map (fun (E_aux (E_id id,_)) -> doc_id_lem id) vars in
- begin match vars with
- | [v] -> v
- | _ -> parens (separate comma vars) end
- | E_aux (E_id id,_) ->
- doc_id_lem id
- | E_aux (E_lit (L_aux (L_unit,_)),_) ->
- string "_" in
- parens (
- (prefix 2 1)
- ((separate space) [string loopf;group (expY indices);expY e5])
- (parens
- (prefix 1 1 (separate space [string "fun";expY id;varspp;arrow]) (expN body))
- )
- )
- | Id_aux ((Id (("while_PP" | "while_PM" |
- "while_MP" | "while_MM" |
- "until_PP" | "until_PM" |
- "until_MP" | "until_MM") as loopf),_)) ->
- let [cond;body;e5] = args in
- let varspp = match e5 with
- | E_aux (E_tuple vars,_) ->
- let vars = List.map (fun (E_aux (E_id id,_)) -> doc_id_lem id) vars in
- begin match vars with
- | [v] -> v
- | _ -> parens (separate comma vars) end
- | E_aux (E_id id,_) ->
- doc_id_lem id
- | E_aux (E_lit (L_aux (L_unit,_)),_) ->
- string "_" in
- parens (
- (prefix 2 1)
- ((separate space) [string loopf; expY e5])
- ((prefix 0 1)
- (parens (prefix 1 1 (separate space [string "fun";varspp;arrow]) (expN cond)))
- (parens (prefix 1 1 (separate space [string "fun";varspp;arrow]) (expN body))))
- )
- (* | Id_aux (Id "append",_) ->
- let [e1;e2] = args in
- let epp = align (expY e1 ^^ space ^^ string "++" ^//^ expY e2) in
- if aexp_needed then parens (align epp) else epp
- | Id_aux (Id "slice_raw",_) ->
- let [e1;e2;e3] = args in
- let t1 = typ_of e1 in
- let eff1 = effect_of e1 in
- let call = if is_bitvector_typ t1 then "bvslice_raw" else "slice_raw" in
- let epp = separate space [string call;expY e1;expY e2;expY e3] in
- let (taepp,aexp_needed) =
- let t = Env.base_typ_of (env_of full_exp) (typ_of full_exp) in
- let eff = effect_of full_exp in
- if typ_needs_printed t && not (contains_t_pp_var mwords t)
- then (align epp ^^ (doc_tannot_lem sequential mwords (effectful eff) t), true)
- else (epp, aexp_needed) in
- if aexp_needed then parens (align taepp) else taepp*)
- | Id_aux (Id "length",_) ->
- (* Another temporary hack: The sizeof rewriting introduces calls to
- "length", and the disambiguation between the length function on
- bitvectors and vectors of other element types should be done by
- the type checker, but type checking after rewriting steps is
- currently broken. *)
- let [arg] = args in
- let targ = typ_of arg in
- let call = if (*mwords &&*) is_bitvector_typ targ then "bitvector_length" else "vector_length" in
- let epp = separate space [string call;expY arg] in
- if aexp_needed then parens (align epp) else epp
- (*)| Id_aux (Id "bool_not", _) ->
- let [a] = args in
- let epp = align (string "~" ^^ expY a) in
- if aexp_needed then parens (align epp) else epp *)
+ | Id_aux (Id "foreach", _) ->
+ begin
+ match args with
+ | [exp1; exp2; exp3; ord_exp; vartuple; body] ->
+ let loopvar, body = match body with
+ | E_aux (E_let (LB_aux (LB_val (
+ P_aux (P_typ (_, P_aux (P_var (P_aux (P_id id, _), _), _)), _), _), _), body), _) -> id, body
+ | _ -> raise (Reporting_basic.err_unreachable l ("Unable to find loop variable in " ^ string_of_exp body)) in
+ let combinator = match effectful (effect_of body), ord_exp with
+ | false, E_aux (E_lit (L_aux (L_false, _)), _) -> "foreach_dec"
+ | false, E_aux (E_lit (L_aux (L_true, _)), _) -> "foreach_inc"
+ | true, E_aux (E_lit (L_aux (L_false, _)), _) -> "foreachM_dec"
+ | true, E_aux (E_lit (L_aux (L_true, _)), _) -> "foreachM_inc"
+ | _ -> raise (Reporting_basic.err_unreachable l "Unable to figure out loop combinator") in
+ let indices_pp = parens (separate_map comma expY [exp1; exp2; exp3]) in
+ parens (
+ (prefix 2 1)
+ ((separate space) [string combinator; indices_pp; expY vartuple])
+ (parens
+ (prefix 1 1 (separate space [string "fun"; doc_id_lem loopvar; expY vartuple; arrow]) (expN body))
+ )
+ )
+ | _ -> raise (Reporting_basic.err_unreachable l
+ "Unexpected number of arguments for loop combinator")
+ end
+ | Id_aux (Id (("while" | "until") as combinator), _) ->
+ begin
+ match args with
+ | [cond; varstuple; body] ->
+ let csuffix = match effectful (effect_of cond), effectful (effect_of body) with
+ | false, false -> "_PP"
+ | false, true -> "_PM"
+ | true, false -> "_MP"
+ | true, true -> "_MM" in
+ parens (
+ (prefix 2 1)
+ ((separate space) [string (combinator ^ csuffix); expY varstuple])
+ ((prefix 0 1)
+ (parens (prefix 1 1 (separate space [string "fun"; expY varstuple; arrow]) (expN cond)))
+ (parens (prefix 1 1 (separate space [string "fun"; expY varstuple; arrow]) (expN body))))
+ )
+ | _ -> raise (Reporting_basic.err_unreachable l
+ "Unexpected number of arguments for loop combinator")
+ end
+ | Id_aux (Id "early_return", _) ->
+ begin
+ match args with
+ | [exp] ->
+ let epp = separate space [string "early_return"; expY exp] in
+ let aexp_needed, tepp =
+ if contains_t_pp_var mwords (typ_of exp) ||
+ contains_t_pp_var mwords (typ_of full_exp) then
+ aexp_needed, epp
+ else
+ let tannot = separate space [string "_MR";
+ doc_atomic_typ_lem sequential mwords false (typ_of full_exp);
+ doc_atomic_typ_lem sequential mwords false (typ_of exp)] in
+ true, doc_op colon epp tannot in
+ if aexp_needed then parens tepp else tepp
+ | _ -> raise (Reporting_basic.err_unreachable l
+ "Unexpected number of arguments for early_return builtin")
+ end
| _ ->
begin match annot with
| Some (env, _, _) when (is_ctor env f) ->
@@ -751,68 +709,11 @@ let doc_exp_lem, doc_let_lem =
end
end
| E_vector_access (v,e) ->
- let vtyp = Env.base_typ_of (env_of v) (typ_of v) in
- let (start, len, ord, etyp) = vector_typ_args_of vtyp in
- let ord_suffix = if is_order_inc ord then "_inc" else "_dec" in
- let bit_prefix = if is_bitvector_typ vtyp then "bit" else "" in
- let call = bit_prefix ^ "vector_access" ^ ord_suffix in
- let start_idx = match nexp_simp (start) with
- | Nexp_aux (Nexp_constant i, _) -> expN (simple_num l i)
- | _ ->
- let nc = nc_eq start (nminus len (nint 1)) in
- if prove (env_of full_exp) nc
- then string (bit_prefix ^ "vector_length") ^^ space ^^ expY v
- else raise (Reporting_basic.err_unreachable l
- ("cannot pretty print expression " ^ (string_of_exp full_exp) ^
- " with non-constant start index")) in
- let epp = string call ^^ space ^^ parens (separate comma_sp [start_idx;expY v;expY e]) in
- if aexp_needed then parens (align epp) else epp
- (* raise (Reporting_basic.err_unreachable l
- "E_vector_access should have been rewritten before pretty-printing") *)
- (* let eff = effect_of full_exp in
- let epp =
- if has_effect eff BE_rreg then
- separate space [string "read_reg_bit";expY v;expY e]
- else
- let tv = typ_of v in
- let call = if is_bitvector_typ tv then "bvaccess" else "access" in
- separate space [string call;expY v;expY e] in
- if aexp_needed then parens (align epp) else epp*)
+ raise (Reporting_basic.err_unreachable l
+ "E_vector_access should have been rewritten before pretty-printing")
| E_vector_subrange (v,e1,e2) ->
- let vtyp = Env.base_typ_of (env_of v) (typ_of v) in
- let (start, len, ord, etyp) = vector_typ_args_of vtyp in
- let ord_suffix = if is_order_inc ord then "_inc" else "_dec" in
- let bit_prefix = if is_bitvector_typ vtyp then "bit" else "" in
- let call = bit_prefix ^ "vector_subrange" ^ ord_suffix in
- let start_idx = match nexp_simp (start) with
- | Nexp_aux (Nexp_constant i, _) -> expN (simple_num l i)
- | _ ->
- let nc = nc_eq start (nminus len (nint 1)) in
- if prove (env_of full_exp) nc
- then string (bit_prefix ^ "vector_length") ^^ space ^^ expY v
- else raise (Reporting_basic.err_unreachable l
- ("cannot pretty print expression " ^ (string_of_exp full_exp) ^
- " with non-constant start index")) in
- let epp = string call ^^ space ^^ parens (separate comma_sp [start_idx;expY v;expY e1;expY e2]) in
- if aexp_needed then parens (align epp) else epp
- (* raise (Reporting_basic.err_unreachable l
- "E_vector_subrange should have been rewritten before pretty-printing") *)
- (* let t = Env.base_typ_of (env_of full_exp) (typ_of full_exp) in
- let eff = effect_of full_exp in
- let (epp,aexp_needed) =
- if has_effect eff BE_rreg then
- let epp = align (string "read_reg_range" ^^ space ^^ expY v ^//^ expY e1 ^//^ expY e2) in
- if typ_needs_printed t && not (contains_t_pp_var mwords t)
- then (epp ^^ doc_tannot_lem sequential mwords true t, true)
- else (epp, aexp_needed)
- else
- if is_bitvector_typ t then
- let bepp = string "bvslice" ^^ space ^^ expY v ^//^ expY e1 ^//^ expY e2 in
- if not (contains_t_pp_var mwords t)
- then (bepp ^^ doc_tannot_lem sequential mwords false t, true)
- else (bepp, aexp_needed)
- else (string "slice" ^^ space ^^ expY v ^//^ expY e1 ^//^ expY e2, aexp_needed) in
- if aexp_needed then parens (align epp) else epp *)
+ raise (Reporting_basic.err_unreachable l
+ "E_vector_subrange should have been rewritten before pretty-printing")
| E_field((E_aux(_,(l,fannot)) as fexp),id) ->
let ft = typ_of_annot (l,fannot) in
(match fannot with
@@ -851,73 +752,11 @@ let doc_exp_lem, doc_let_lem =
else liftR epp
else if is_ctor env id then doc_id_lem_ctor id
else doc_id_lem id
- (*| Base((_,t),Alias alias_info,_,eff,_,_) ->
- (match alias_info with
- | Alias_field(reg,field) ->
- let call = match t.t with
- | Tid "bit" | Tabbrev (_,{t=Tid "bit"}) -> "read_reg_bitfield"
- | _ -> "read_reg_field" in
- let ta =
- if typ_needs_printed t && not (contains_t_pp_var mwords t)
- then doc_tannot_lem sequential mwords true t else empty in
- let epp = separate space [string call;string reg;string_lit(string field)] ^^ ta in
- if aexp_needed then parens (align epp) else epp
- | Alias_pair(reg1,reg2) ->
- let (call,ta) =
- if has_effect eff BE_rreg then
- let ta =
- if typ_needs_printed t && not (contains_t_pp_var mwords t)
- then doc_tannot_lem sequential mwords true t else empty in
- ("read_two_regs", ta)
- else
- ("RegisterPair", empty) in
- let epp = separate space [string call;string reg1;string reg2] ^^ ta in
- if aexp_needed then parens (align epp) else epp
- | Alias_extract(reg,start,stop) ->
- let epp =
- if start = stop then
- separate space [string "read_reg_bit";string reg;doc_int start]
- else
- let ta =
- if typ_needs_printed t && not (contains_t_pp_var mwords t)
- then doc_tannot_lem sequential mwords true t else empty in
- separate space [string "read_reg_range";string reg;doc_int start;doc_int stop] ^^ ta in
- if aexp_needed then parens (align epp) else epp
- )*)
| E_lit lit -> doc_lit_lem sequential mwords false lit annot
| E_cast(typ,e) ->
- expV aexp_needed e (*
- (match annot with
- | Base((_,t),External _,_,_,_,_) ->
- (* TODO: Does this case still exist with the new type checker? *)
- let epp = string "read_reg" ^^ space ^^ expY e in
- if typ_needs_printed t && not (contains_t_pp_var mwords t)
- then parens (epp ^^ doc_tannot_lem sequential mwords true t) else epp
- | Base((_,t),_,_,_,_,_) ->
- (match typ with
- | Typ_app (Id_aux (Id "vector",_), [Typ_arg_aux (Typ_arg_nexp(Nexp_aux (Nexp_constant i,_)),_);_;_;_]) ->
- let call =
- if is_bitvector_typ t then "set_bitvector_start"
- else "set_vector_start" in
- let epp = (concat [string call;space;string (string_of_int i)]) ^//^
- expY e in
- if aexp_needed then parens epp else epp
- (*
- | Typ_var (Kid_aux (Var "length",_)) ->
- (* TODO: Does this case still exist with the new type checker? *)
- let call =
- if is_bitvector_typ t then "set_bitvector_start_to_length"
- else "set_vector_start_to_length" in
- let epp = (string call) ^//^ expY e in
- if aexp_needed then parens epp else epp
- *)
- | _ ->
- expV aexp_needed e)) (*(parens (doc_op colon (group (expY e)) (doc_typ_lem typ)))) *)
- *)
+ expV aexp_needed e
| E_tuple exps ->
- (match exps with (*
- | [e] -> expV aexp_needed e *)
- | _ -> parens (separate_map comma expN exps))
+ parens (separate_map comma expN exps)
| E_record(FES_aux(FES_Fexps(fexps,_),_)) ->
let recordtyp = match annot with
| Some (env, Typ_aux (Typ_id tid,_), _)
@@ -930,7 +769,6 @@ let doc_exp_lem, doc_let_lem =
(doc_fexp sequential mwords early_ret recordtyp) fexps)) ^^ space) in
if aexp_needed then parens epp else epp
| E_record_update(e,(FES_aux(FES_Fexps(fexps,_),_))) ->
- (* let (E_aux (_, (_, eannot))) = e in *)
let recordtyp = match annot with
| Some (env, Typ_aux (Typ_id tid,_), _)
| Some (env, Typ_aux (Typ_app (tid, _), _), _)
@@ -944,77 +782,43 @@ let doc_exp_lem, doc_let_lem =
if is_vector_typ t then vector_typ_args_of t
else raise (Reporting_basic.err_unreachable l
"E_vector of non-vector type") in
- (*match annot with
- | Base((_,t),_,_,_,_,_) ->
- match t.t with
- | Tapp("vector", [TA_nexp start; TA_nexp len; TA_ord order; TA_typ etyp])
- | Tabbrev(_,{t= Tapp("vector", [TA_nexp start; TA_nexp len; TA_ord order; TA_typ etyp])}) ->*)
- let dir,dir_out = if is_order_inc order then (true,"true") else (false, "false") in
- let start = match nexp_simp start with
- | Nexp_aux (Nexp_constant i, _) -> string_of_big_int i
- | _ -> if dir then "0" else string_of_int (List.length exps) in
- let expspp =
- match exps with
- | [] -> empty
- | e :: es ->
- let (expspp,_) =
- List.fold_left
- (fun (pp,count) e ->
- (pp ^^ semi ^^ (if count = 20 then break 0 else empty) ^^
- expN e),
- if count = 20 then 0 else count + 1)
- (expN e,0) es in
- align (group expspp) in
- let epp =
- group (separate space [string "Vector"; brackets expspp;string start;string dir_out]) in
- let (epp,aexp_needed) =
- if is_bit_typ etyp && mwords then
- let bepp = string "vec_to_bvec" ^^ space ^^ parens (align epp) in
- (bepp ^^ doc_tannot_lem sequential mwords false t, true)
- else (epp,aexp_needed) in
- if aexp_needed then parens (align epp) else epp
- (* *)
- | E_vector_update(v,e1,e2) ->
- let t = typ_of v in
- let (start, len, ord, _) = vector_typ_args_of (Env.base_typ_of (env_of full_exp) t) in
- let ord_suffix = if is_order_inc ord then "_inc" else "_dec" in
- let bit_prefix = if is_bitvector_typ t then "bit" else "" in
- let call = bit_prefix ^ "vector_update_pos" ^ ord_suffix in
- let start_idx = match nexp_simp (start) with
- | Nexp_aux (Nexp_constant i, _) -> expN (simple_num l i)
- | _ ->
- let nc = nc_eq start (nminus len (nint 1)) in
- if prove (env_of full_exp) nc
- then string (bit_prefix ^ "vector_length") ^^ space ^^ expY v
- else raise (Reporting_basic.err_unreachable l
- ("cannot pretty print expression " ^ (string_of_exp full_exp) ^
- " with non-constant start index")) in
- let epp = string call ^^ space ^^ parens (separate comma_sp [start_idx;expY v;expY e1;expY e2]) in
- if aexp_needed then parens (align epp) else epp
- | E_vector_update_subrange(v,e1,e2,e3) ->
- let t = typ_of v in
- let (start, len, ord, _) = vector_typ_args_of (Env.base_typ_of (env_of full_exp) t) in
- let ord_suffix = if is_order_inc ord then "_inc" else "_dec" in
- let bit_prefix = if is_bitvector_typ t then "bit" else "" in
- let call = bit_prefix ^ "vector_update_subrange" ^ ord_suffix in
- let start_idx = match nexp_simp (start) with
- | Nexp_aux (Nexp_constant i, _) -> expN (simple_num l i)
- | _ ->
- let nc = nc_eq start (nminus len (nint 1)) in
- if prove (env_of full_exp) nc
- then string (bit_prefix ^ "vector_length") ^^ space ^^ expY v
- else raise (Reporting_basic.err_unreachable l
- ("cannot pretty print expression " ^ (string_of_exp full_exp) ^
- " with non-constant start index")) in
+ let dir,dir_out = if is_order_inc order then (true,"true") else (false, "false") in
+ let start = match nexp_simp start with
+ | Nexp_aux (Nexp_constant i, _) -> string_of_big_int i
+ | _ -> if dir then "0" else string_of_int (List.length exps) in
+ let expspp =
+ match exps with
+ | [] -> empty
+ | e :: es ->
+ let (expspp,_) =
+ List.fold_left
+ (fun (pp,count) e ->
+ (pp ^^ semi ^^ (if count = 20 then break 0 else empty) ^^
+ expN e),
+ if count = 20 then 0 else count + 1)
+ (expN e,0) es in
+ align (group expspp) in
let epp =
- align (string call ^//^
- parens (separate comma_sp
- [start_idx; group (expY v); group (expY e1); group (expY e2); group (expY e3)])) in
+ group (separate space [string "Vector"; brackets expspp;string start;string dir_out]) in
+ let (epp,aexp_needed) =
+ if is_bit_typ etyp && mwords then
+ let bepp = string "vec_to_bvec" ^^ space ^^ parens (align epp) in
+ (bepp ^^ doc_tannot_lem sequential mwords false t, true)
+ else (epp,aexp_needed) in
if aexp_needed then parens (align epp) else epp
+ | E_vector_update(v,e1,e2) ->
+ raise (Reporting_basic.err_unreachable l
+ "E_vector_update should have been rewritten before pretty-printing")
+ | E_vector_update_subrange(v,e1,e2,e3) ->
+ raise (Reporting_basic.err_unreachable l
+ "E_vector_update should have been rewritten before pretty-printing")
| E_list exps ->
brackets (separate_map semi (expN) exps)
| E_case(e,pexps) ->
- let only_integers e =
+ let only_integers e = expY e in
+ (*
+ (* This is a hack, incomplete. It's because lem does not allow
+ pattern-matching on integers *)
let typ = typ_of e in
if Ast_util.is_number typ then
let e_pp = expY e in
@@ -1026,10 +830,8 @@ let doc_exp_lem, doc_let_lem =
let e_pp = expY e in
align (string "toNaturalFiveTup" ^//^ e_pp)
| _ -> expY e)
- in
+ in*)
- (* This is a hack, incomplete. It's because lem does not allow
- pattern-matching on integers *)
let epp =
group ((separate space [string "match"; only_integers e; string "with"]) ^/^
(separate_map (break 1) (doc_case sequential mwords early_ret) pexps) ^/^
@@ -1040,117 +842,22 @@ let doc_exp_lem, doc_let_lem =
let epp = liftR (separate space [string "assert_exp"; expY e1; expY e2]) in
if aexp_needed then parens (align epp) else align epp
| E_app_infix (e1,id,e2) ->
- (* TODO: Should have been removed by the new type checker; check with Alasdair *)
raise (Reporting_basic.err_unreachable l
"E_app_infix should have been rewritten before pretty-printing")
- (*match annot with
- | Base((_,t),External(Some name),_,_,_,_) ->
- let argpp arg =
- let (E_aux (_,(_,Base((_,t),_,_,_,_,_)))) = arg in
- match t.t with
- | Tapp("vector",_) ->
- let call =
- if is_bitvector_typ t then "reset_bitvector_start"
- else "reset_vector_start" in
- parens (concat [string call;space;expY arg])
- | _ -> expY arg in
- let epp =
- let aux name = align (argpp e1 ^^ space ^^ string name ^//^ argpp e2) in
- let aux2 name = align (string name ^//^ argpp e1 ^/^ argpp e2) in
- align
- (match name with
- | "power" -> aux2 "pow"
-
- | "bitwise_and_bit" -> aux "&."
- | "bitwise_or_bit" -> aux "|."
- | "bitwise_xor_bit" -> aux "+."
- | "add" -> aux "+"
- | "minus" -> aux "-"
- | "multiply" -> aux "*"
-
- | "quot" -> aux2 "quot"
- | "quot_signed" -> aux2 "quot"
- | "modulo" -> aux2 "modulo"
- | "add_vec" -> aux2 "add_VVV"
- | "add_vec_signed" -> aux2 "addS_VVV"
- | "add_overflow_vec" -> aux2 "addO_VVV"
- | "add_overflow_vec_signed" -> aux2 "addSO_VVV"
- | "minus_vec" -> aux2 "minus_VVV"
- | "minus_overflow_vec" -> aux2 "minusO_VVV"
- | "minus_overflow_vec_signed" -> aux2 "minusSO_VVV"
- | "multiply_vec" -> aux2 "mult_VVV"
- | "multiply_vec_signed" -> aux2 "multS_VVV"
- | "mult_overflow_vec" -> aux2 "multO_VVV"
- | "mult_overflow_vec_signed" -> aux2 "multSO_VVV"
- | "quot_vec" -> aux2 "quot_VVV"
- | "quot_vec_signed" -> aux2 "quotS_VVV"
- | "quot_overflow_vec" -> aux2 "quotO_VVV"
- | "quot_overflow_vec_signed" -> aux2 "quotSO_VVV"
- | "mod_vec" -> aux2 "mod_VVV"
-
- | "add_vec_range" -> aux2 "add_VIV"
- | "add_vec_range_signed" -> aux2 "addS_VIV"
- | "minus_vec_range" -> aux2 "minus_VIV"
- | "mult_vec_range" -> aux2 "mult_VIV"
- | "mult_vec_range_signed" -> aux2 "multS_VIV"
- | "mod_vec_range" -> aux2 "minus_VIV"
-
- | "add_range_vec" -> aux2 "add_IVV"
- | "add_range_vec_signed" -> aux2 "addS_IVV"
- | "minus_range_vec" -> aux2 "minus_IVV"
- | "mult_range_vec" -> aux2 "mult_IVV"
- | "mult_range_vec_signed" -> aux2 "multS_IVV"
-
- | "add_range_vec_range" -> aux2 "add_IVI"
- | "add_range_vec_range_signed" -> aux2 "addS_IVI"
- | "minus_range_vec_range" -> aux2 "minus_IVI"
-
- | "add_vec_range_range" -> aux2 "add_VII"
- | "add_vec_range_range_signed" -> aux2 "addS_VII"
- | "minus_vec_range_range" -> aux2 "minus_VII"
- | "add_vec_vec_range" -> aux2 "add_VVI"
- | "add_vec_vec_range_signed" -> aux2 "addS_VVI"
-
- | "add_vec_bit" -> aux2 "add_VBV"
- | "add_vec_bit_signed" -> aux2 "addS_VBV"
- | "add_overflow_vec_bit_signed" -> aux2 "addSO_VBV"
- | "minus_vec_bit_signed" -> aux2 "minus_VBV"
- | "minus_overflow_vec_bit" -> aux2 "minusO_VBV"
- | "minus_overflow_vec_bit_signed" -> aux2 "minusSO_VBV"
-
- | _ ->
- string name ^//^ parens (expN e1 ^^ comma ^/^ expN e2)) in
- let (epp,aexp_needed) =
- if typ_needs_printed t && not (contains_t_pp_var mwords t)
- then (parens epp ^^ doc_tannot_lem sequential mwords false t, true)
- else (epp, aexp_needed) in
- if aexp_needed then parens (align epp) else epp
- | _ ->
- let epp =
- align (doc_id_lem id ^//^ parens (expN e1 ^^ comma ^/^ expN e2)) in
- if aexp_needed then parens (align epp) else epp*)
| E_internal_let(lexp, eq_exp, in_exp) ->
- raise (report l "E_internal_lets should have been removed till now")
- (* (separate
- space
- [string "let internal";
- (match lexp with (LEXP_aux ((LEXP_id id | LEXP_cast (_,id)),_)) -> doc_id_lem id);
- coloneq;
- exp eq_exp;
- string "in"]) ^/^
- exp in_exp *)
+ raise (report l "E_internal_lets should have been removed before pretty-printing")
| E_internal_plet (pat,e1,e2) ->
let epp =
let b = match e1 with E_aux (E_if _,_) -> true | _ -> false in
match pat with
- | P_aux (P_wild,_) ->
+ | P_aux (P_wild,_) | P_aux (P_typ (_, P_aux (P_wild, _)), _) ->
(separate space [expV b e1; string ">>"]) ^^ hardline ^^ expN e2
| _ ->
(separate space [expV b e1; string ">>= fun";
doc_pat_lem sequential mwords true pat;arrow]) ^^ hardline ^^ expN e2 in
if aexp_needed then parens (align epp) else epp
| E_internal_return (e1) ->
- separate space [string "return"; expY e1;]
+ separate space [string "return"; expY e1]
| E_sizeof nexp ->
(match nexp_simp nexp with
| Nexp_aux (Nexp_constant i, _) -> doc_lit_lem sequential mwords false (L_aux (L_num i, l)) annot
@@ -1167,7 +874,8 @@ let doc_exp_lem, doc_let_lem =
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_constraint _ -> string "true"
+ | 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
"unsupported internal expression encountered while pretty-printing")
@@ -1195,14 +903,11 @@ let doc_exp_lem, doc_let_lem =
and doc_lexp_deref_lem sequential mwords early_ret ((LEXP_aux(lexp,(l,annot))) as le) = match lexp with
| LEXP_field (le,id) ->
parens (separate empty [doc_lexp_deref_lem sequential mwords early_ret le;dot;doc_id_lem id])
- | LEXP_vector(le,e) ->
- parens ((separate space) [string "access";doc_lexp_deref_lem sequential mwords early_ret le;
- top_exp sequential mwords early_ret true e])
| LEXP_id id -> doc_id_lem id
| LEXP_cast (typ,id) -> doc_id_lem id
| LEXP_tup lexps -> parens (separate_map comma_sp (doc_lexp_deref_lem sequential mwords early_ret) lexps)
| _ ->
- raise (Reporting_basic.err_unreachable l ("doc_lexp_deref_lem: Shouldn't happen"))
+ raise (Reporting_basic.err_unreachable l ("doc_lexp_deref_lem: Unsupported lexp"))
(* expose doc_exp_lem and doc_let *)
in top_exp, let_exp
@@ -1289,7 +994,6 @@ let doc_typdef_lem sequential mwords (TD_aux(td, (l, annot))) = match td with
| _ ->
let ar_doc = group (separate_map (break 1) (doc_type_union_lem sequential mwords) ar) in
let typ_pp =
-
(doc_op equals)
(concat [string "type"; space; doc_id_lem_type id; space; doc_typquant_items_lem None typq])
((*doc_typquant_lem typq*) ar_doc) in
@@ -1469,33 +1173,6 @@ let doc_typdef_lem sequential mwords (TD_aux(td, (l, annot))) = match td with
let doc_rid (r,id) = parens (separate comma_sp [string_lit (doc_id_lem id);
doc_range_lem r;]) in
let doc_rids = group (separate_map (semi ^^ (break 1)) doc_rid rs) in
- let doc_field (fr, fid) =
- let i, j = match fr with
- | BF_aux (BF_single i, _) -> (i, i)
- | BF_aux (BF_range (i, j), _) -> (i, j)
- | _ -> raise (Reporting_basic.err_unreachable l "unsupported field type") in
- let fsize = if dir_b then add_big_int (sub_big_int j i) unit_big_int else add_big_int (sub_big_int i j) unit_big_int in
- let ftyp = vector_typ (nconstant i) (nconstant fsize) ord bit_typ in
- let reftyp =
- mk_typ (Typ_app (Id_aux (Id "field_ref", Parse_ast.Unknown),
- [mk_typ_arg (Typ_arg_typ (mk_id_typ id));
- mk_typ_arg (Typ_arg_typ ftyp)])) in
- let rfannot = doc_tannot_lem sequential mwords false reftyp in
- let id_exp id = E_aux (E_id (mk_id id), simple_annot l vtyp) in
- let get, set =
- E_aux (E_vector_subrange (id_exp "reg", simple_num l i, simple_num l j), simple_annot l ftyp),
- E_aux (E_vector_update_subrange (id_exp "reg", simple_num l i, simple_num l j, id_exp "v"), simple_annot l ftyp) in
- (* "bitvector_subrange" ^ dir_suffix ^ " (" ^ string_of_int i1 ^ ", reg, " ^ string_of_int i ^ ", " ^ string_of_int j ^ ")",
- "bitvector_update_subrange" ^ dir_suffix ^ " (" ^ string_of_int i1 ^ ", reg, " ^ string_of_int i ^ ", " ^ string_of_int j ^ ", v)" in *)
- doc_op equals
- (concat [string "let "; parens (concat [doc_id_lem id; underscore; doc_id_lem fid; rfannot])])
- (concat [
- space; langlebar; string " field_name = \"" ^^ doc_id_lem fid ^^ string "\";"; hardline;
- space; space; space; string (" field_start = " ^ string_of_big_int i ^ ";"); hardline;
- space; space; space; string (" field_is_inc = " ^ dir ^ ";"); hardline;
- space; space; space; string " get_field = (fun reg -> " ^^ doc_exp_lem sequential mwords false false get ^^ string ");"; hardline;
- space; space; space; string " set_field = (fun reg v -> " ^^ doc_exp_lem sequential mwords false false set ^^ string ") "; ranglebar])
- in
doc_op equals
(concat [string "type";space;doc_id_lem id])
(doc_typ_lem sequential mwords vtyp)
@@ -1508,34 +1185,11 @@ let doc_typdef_lem sequential mwords (TD_aux(td, (l, annot))) = match td with
(concat [string "let";space;string "cast_to_";doc_id_lem id;space;string "reg"])
(string "reg")
^^ hardline ^^
- (* if sequential then *)
- (* string " = <|" (*; parens (string "reg" ^^ tannot) *)]) ^^ hardline ^^
- string (" get_field = (fun reg -> " ^ get ^ ");") ^^ hardline ^^
- string (" set_field = (fun reg v -> " ^ set ^") |>") *)
- (* doc_op equals
- (concat [string "let set_"; doc_id_lem id; underscore; doc_id_lem fid;
- space; parens (separate comma_sp [parens (string "reg" ^^ tannot); string "v"])]) (string set) *)
- (* in *)
- (* doc_op equals
- (concat [string "let";space;string "build_";doc_id_lem id;space;string "regname"])
- (string "Register" ^^ space ^^
- align (separate space [string "regname"; doc_int size; doc_int i1; dir;
- break 0 ^^ brackets (align doc_rids)]))
- ^^ hardline ^^ *)
- separate_map hardline doc_field rs
- ^^ hardline ^^
- (* else *)
- (*let doc_rfield (_,id) =
- (doc_op equals)
- (string "let" ^^ space ^^ doc_id_lem id)
- (string "Register_field" ^^ space ^^ string_lit(doc_id_lem id)) in*)
doc_op equals
(concat [string "let";space;string "build_";doc_id_lem id;space;string "regname"])
(string "Register" ^^ space ^^
align (separate space [string "regname"; doc_int size; doc_int i1; string dir;
break 0 ^^ brackets (align doc_rids)]))
- (*^^ hardline ^^
- separate_map hardline doc_field rs*)
| _ -> raise (Reporting_basic.err_unreachable l "register with non-constant indices")
@@ -1692,7 +1346,59 @@ let doc_spec_lem sequential mwords (VS_aux (valspec,annot)) =
(* | VS_val_spec (_,_,Some _,_) -> empty *)
| _ -> empty
-let rec doc_def_lem sequential mwords def =
+let find_regtypes defs =
+ List.fold_left
+ (fun acc def ->
+ match def with
+ | DEF_type (TD_aux(TD_register (Id_aux (Id tname, _), n1, n2, fields),_)) ->
+ (tname, (n1, n2, fields)) :: acc
+ | _ -> acc
+ ) [] defs
+
+let is_field_accessor regtypes fdef =
+ let is_field_of regtyp field =
+ List.exists (fun (tname, (_, _, fields)) -> tname = regtyp &&
+ List.exists (fun (_, fid) -> string_of_id fid = field) fields) regtypes in
+ match Util.split_on_char '_' (string_of_id (id_of_fundef fdef)) with
+ | [access; regtyp; field] ->
+ (access = "get" || access = "set") && is_field_of regtyp field
+ | _ -> false
+
+let doc_regtype_fields sequential mwords (tname, (n1, n2, fields)) =
+ let i1, i2 = match n1, n2 with
+ | Nexp_aux(Nexp_constant i1,_),Nexp_aux(Nexp_constant i2,_) -> i1, i2
+ | _ -> raise (Reporting_basic.err_typ Parse_ast.Unknown
+ ("Non-constant indices in register type " ^ tname)) in
+ let dir_b = i1 < i2 in
+ let dir = (if dir_b then "true" else "false") in
+ let doc_field (fr, fid) =
+ let i, j = match fr with
+ | BF_aux (BF_single i, _) -> (i, i)
+ | BF_aux (BF_range (i, j), _) -> (i, j)
+ | _ -> raise (Reporting_basic.err_unreachable Parse_ast.Unknown
+ ("Unsupported type in field " ^ string_of_id fid ^ " of " ^ tname)) in
+ let fsize = succ_big_int (abs_big_int (sub_big_int i j)) in
+ (* TODO Assumes normalised, decreasing bitvector slices; however, since
+ start indices or indexing order do not appear in Lem type annotations,
+ this does not matter. *)
+ let ftyp = vector_typ (nconstant (pred_big_int fsize)) (nconstant fsize) dec_ord bit_typ in
+ let reftyp =
+ mk_typ (Typ_app (Id_aux (Id "field_ref", Parse_ast.Unknown),
+ [mk_typ_arg (Typ_arg_typ (mk_id_typ (mk_id tname)));
+ mk_typ_arg (Typ_arg_typ ftyp)])) in
+ let rfannot = doc_tannot_lem sequential mwords false reftyp in
+ doc_op equals
+ (concat [string "let "; parens (concat [string tname; underscore; doc_id_lem fid; rfannot])])
+ (concat [
+ space; langlebar; string " field_name = \"" ^^ doc_id_lem fid ^^ string "\";"; hardline;
+ space; space; space; string (" field_start = " ^ string_of_big_int i ^ ";"); hardline;
+ space; space; space; string (" field_is_inc = " ^ dir ^ ";"); hardline;
+ space; space; space; string (" get_field = (fun reg -> get_" ^ tname ^ "_" ^ string_of_id fid ^ "(reg));"); hardline;
+ space; space; space; string (" set_field = (fun reg v -> set_" ^ tname ^ "_" ^ string_of_id fid ^ "(reg, v)) "); ranglebar])
+ in
+ separate_map hardline doc_field fields
+
+let rec doc_def_lem sequential mwords regtypes 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)
@@ -1702,7 +1408,9 @@ let rec doc_def_lem sequential mwords def =
| DEF_reg_dec dec -> (group (doc_dec_lem sequential dec),empty)
| DEF_default df -> (empty,empty)
- | DEF_fundef f_def -> (empty,group (doc_fundef_lem sequential mwords f_def) ^/^ hardline)
+ | DEF_fundef fdef ->
+ let doc_fdef = group (doc_fundef_lem sequential mwords fdef) ^/^ hardline in
+ if is_field_accessor regtypes fdef then (doc_fdef, empty) else (empty, doc_fdef)
| DEF_internal_mutrec fundefs ->
(empty, doc_mutrec_lem sequential mwords fundefs ^/^ hardline)
| DEF_val lbind -> (empty,group (doc_let_lem sequential mwords false lbind) ^/^ hardline)
@@ -1712,21 +1420,15 @@ let rec doc_def_lem sequential mwords def =
| DEF_comm (DC_comm s) -> (empty,comment (string s))
| DEF_comm (DC_comm_struct d) ->
- let (typdefs,vdefs) = doc_def_lem sequential mwords d in
+ let (typdefs,vdefs) = doc_def_lem sequential mwords regtypes d in
(empty,comment (typdefs ^^ hardline ^^ vdefs))
let doc_defs_lem sequential mwords (Defs defs) =
- let (typdefs,valdefs) = List.split (List.map (doc_def_lem sequential mwords) defs) in
- (separate empty typdefs,separate empty valdefs)
-
-let find_regtypes (Defs defs) =
- List.fold_left
- (fun acc def ->
- match def with
- | DEF_type (TD_aux(TD_register (Id_aux (Id tname, _),_,_,_),_)) -> tname :: acc
- | _ -> acc
- ) [] defs
+ let regtypes = find_regtypes defs in
+ let field_refs = separate_map hardline (doc_regtype_fields sequential mwords) regtypes in
+ let (typdefs,valdefs) = List.split (List.map (doc_def_lem sequential mwords regtypes) defs) in
+ (separate empty typdefs ^^ field_refs, separate empty valdefs)
let find_registers (Defs defs) =
List.fold_left
@@ -1776,6 +1478,7 @@ let doc_regstate_lem mwords registers =
concat [
doc_typdef_lem true mwords (TD_aux (regstate, annot)); hardline;
hardline;
+ string "type _MR 'a 'r = MR regstate 'a 'r"; hardline;
string "type _M 'a = M regstate 'a"
],
initregstate
@@ -1832,30 +1535,8 @@ let pp_defs_lem sequential mwords (types_file,types_modules) (defs_file,defs_mod
hardline;
register_refs]
else
- concat [string "type _M 'a = M 'a"; hardline]
+ concat [string "type _MR 'a 'r = MR 'a 'r"; hardline; string "type _M 'a = M 'a"; hardline]
]);
- (* (print types_seq_file)
- (concat
- [string "(*" ^^ (string top_line) ^^ string "*)";hardline;
- (separate_map hardline)
- (fun lib -> separate space [string "open import";string lib]) types_seq_modules;hardline;
- if !print_to_from_interp_value
- then
- concat
- [(separate_map hardline)
- (fun lib -> separate space [string " import";string lib]) ["Interp";"Interp_ast"];
- string "open import Deep_shallow_convert";
- hardline;
- hardline;
- string "module SI = Interp"; hardline;
- string "module SIA = Interp_ast"; hardline;
- hardline]
- else empty;
- typdefs_seq; hardline;
- hardline;
- regstate_def; hardline;
- hardline;
- register_refs]); *)
(print defs_file)
(concat
[string "(*" ^^ (string top_line) ^^ string "*)";hardline;
@@ -1865,10 +1546,3 @@ let pp_defs_lem sequential mwords (types_file,types_modules) (defs_file,defs_mod
valdefs;
hardline;
initregstate_def]);
- (* (print state_file)
- (concat
- [string "(*" ^^ (string top_line) ^^ string "*)";hardline;
- (separate_map hardline)
- (fun lib -> separate space [string "open import";string lib]) state_modules;hardline;
- hardline;
- valdefs_seq]); *)
diff --git a/src/pretty_print_lem_ast.ml b/src/pretty_print_lem_ast.ml
index a91a6f08..4cb7bef2 100644
--- a/src/pretty_print_lem_ast.ml
+++ b/src/pretty_print_lem_ast.ml
@@ -616,7 +616,7 @@ let pp_lem_dec ppf (DEC_aux(reg,(l,annot))) =
fprintf ppf "@[<0>(DEC_aux (DEC_typ_alias %a %a %a) (%a, %a))@]"
pp_lem_typ typ pp_lem_id id pp_lem_aspec alias_spec pp_lem_l l pp_annot annot
-let pp_lem_def ppf d =
+let rec pp_lem_def ppf d =
match d with
| DEF_default(df) -> fprintf ppf "(DEF_default %a);@\n" pp_lem_default df
| DEF_spec(v_spec) -> fprintf ppf "(DEF_spec %a);@\n" pp_lem_spec v_spec
@@ -628,6 +628,7 @@ let pp_lem_def ppf d =
| 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_big_int n) pp_lem_id id
+ | DEF_internal_mutrec f_defs -> List.iter (fun f_def -> pp_lem_def ppf (DEF_fundef f_def)) f_defs
| _ -> 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/pretty_print_sail2.ml b/src/pretty_print_sail2.ml
index e354fe58..59413653 100644
--- a/src/pretty_print_sail2.ml
+++ b/src/pretty_print_sail2.ml
@@ -183,17 +183,29 @@ let rec doc_exp (E_aux (e_aux, _) as exp) =
group (separate space [string "if"; doc_exp if_exp; string "then"; doc_exp then_exp; string "else"; doc_exp else_exp])
| E_list exps -> string "[|" ^^ separate_map (comma ^^ space) doc_exp exps ^^ string "|]"
| E_cons (exp1, exp2) -> string "E_cons"
- | E_record fexps -> string "E_record"
+ | E_record fexps -> string "<|" ^^ doc_fexps fexps ^^ string "|>"
| E_loop (While, cond, exp) ->
separate space [string "while"; doc_exp cond; string "do"; doc_exp exp]
| E_loop (Until, cond, exp) ->
separate space [string "repeat"; doc_exp exp; string "until"; doc_exp cond]
- | E_record_update (exp, fexps) -> string "E_record_update"
+ | E_record_update (exp, fexps) -> separate space [string "<|"; doc_exp exp; string "with"; doc_fexps fexps; string "|>"]
| E_vector_append (exp1, exp2) -> separate space [doc_atomic_exp exp1; string "@"; doc_atomic_exp exp2]
| E_case (exp, pexps) ->
separate space [string "match"; doc_exp exp; doc_pexps pexps]
| E_let (LB_aux (LB_val (pat, binding), _), exp) ->
separate space [string "let"; doc_pat pat; equals; doc_exp binding; string "in"; doc_exp exp]
+ | E_internal_let (lexp, exp1, exp2) ->
+ let le =
+ prefix 2 1
+ (separate space [string "internal_let"; doc_lexp lexp; equals])
+ (doc_exp exp1) in
+ doc_op (string "in") le (doc_exp exp2)
+ | E_internal_plet (pat, exp1, exp2) ->
+ let le =
+ prefix 2 1
+ (separate space [string "internal_plet"; doc_pat pat; equals])
+ (doc_exp exp1) in
+ doc_op (string "in") le (doc_exp exp2)
| E_assign (lexp, exp) ->
separate space [doc_lexp lexp; equals; doc_exp exp]
| E_for (id, exp1, exp2, exp3, order, exp4) ->
@@ -216,6 +228,7 @@ let rec doc_exp (E_aux (e_aux, _) as exp) =
| E_throw exp -> assert false
| E_try (exp, pexps) -> assert false
| E_return exp -> string "return" ^^ parens (doc_exp exp)
+ | E_internal_return exp -> string "internal_return" ^^ parens (doc_exp exp)
| E_app (id, [exp]) when Id.compare (mk_id "pow2") id == 0 ->
separate space [string "2"; string "^"; doc_atomic_exp exp]
| _ -> doc_atomic_exp exp
@@ -268,6 +281,9 @@ and doc_pexp (Pat_aux (pat_aux, _)) =
| Pat_exp (pat, exp) -> separate space [doc_pat pat; string "=>"; doc_exp exp]
| Pat_when (pat, wh, exp) ->
separate space [doc_pat pat; string "if"; doc_exp wh; string "=>"; doc_exp exp]
+and doc_fexps (FES_aux (FES_Fexps (fexps, _), _)) = separate_map (semi ^^ space) doc_fexp fexps
+and doc_fexp (FE_aux (FE_Fexp (id, exp), _)) =
+ doc_op (string "=") (doc_id id) (doc_exp exp)
and doc_letbind (LB_aux (lb_aux, _)) =
match lb_aux with
| LB_val (pat, exp) ->
@@ -377,6 +393,7 @@ let rec doc_def def = group (match def with
| DEF_type t_def -> doc_typdef t_def
| DEF_kind k_def -> doc_kind_def k_def
| DEF_fundef f_def -> doc_fundef f_def
+ | DEF_internal_mutrec f_defs -> separate_map hardline doc_fundef f_defs
| DEF_val lbind -> string "let" ^^ space ^^ doc_letbind lbind
| DEF_reg_dec dec -> doc_dec dec
| DEF_scattered sdef -> doc_scattered sdef
diff --git a/src/rewriter.ml b/src/rewriter.ml
index fd1479a7..002d7630 100644
--- a/src/rewriter.ml
+++ b/src/rewriter.ml
@@ -78,6 +78,8 @@ 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 gen_vs (id, spec) = Initial_check.val_spec_of_string dec_ord (mk_id id) spec
+
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, gen_loc l)),
@@ -246,18 +248,6 @@ let effectful_effs = function
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, _) ->
- List.exists
- (fun (BE_aux (be,_)) ->
- match be with
- | BE_lset -> true
- | _ -> false
- ) effs
- | _ -> true
-
-let updates_vars eaux = updates_vars_effs (effect_of eaux)
-
let id_to_string (Id_aux(id,l)) =
match id with
| Id(s) -> s
@@ -535,7 +525,8 @@ let rewrite_exp rewriters (E_aux (exp,(l,annot))) =
raise (Reporting_basic.err_unreachable l
("Internal_exp_user given unexpected types " ^ (t_to_string tu) ^ ", " ^ (t_to_string ti))))
| _ -> raise (Reporting_basic.err_unreachable l ("Internal_exp_user given none Base annot")))*)
- | E_internal_let _ -> raise (Reporting_basic.err_unreachable l "Internal let found before it should have been introduced")
+ | E_internal_let (lexp, e1, e2) ->
+ rewrap (E_internal_let (rewriters.rewrite_lexp rewriters lexp, rewriters.rewrite_exp rewriters e1, rewriters.rewrite_exp rewriters e2))
| E_internal_return _ -> raise (Reporting_basic.err_unreachable l "Internal return found before it should have been introduced")
| E_internal_plet _ -> raise (Reporting_basic.err_unreachable l " Internal plet found before it should have been introduced")
| _ -> rewrap exp
@@ -1306,16 +1297,25 @@ let rewrite_sizeof (Defs defs) =
let exp' = fold_exp { id_exp_alg with e_sizeof = e_sizeof kid_nmap } exp in
FCL_aux (FCL_Funcl (id, rewrite_pat pat, exp'), annot) in
let funcls = List.map rewrite_funcl_params funcls in
- (nvars, FD_aux (FD_function (rec_opt,tannot,eff,funcls),annot)) in
+ let fd = FD_aux (FD_function (rec_opt,tannot,eff,funcls),annot) in
+ let params_map =
+ if KidSet.is_empty nvars then params_map else
+ Bindings.add (id_of_fundef fd) nvars params_map in
+ (params_map, FD_aux (FD_function (rec_opt,tannot,eff,funcls),annot)) in
let rewrite_sizeof_def (params_map, defs) = function
- | DEF_fundef fd as def ->
- let (nvars, fd') = rewrite_sizeof_fun params_map fd in
- let id = id_of_fundef fd in
- let params_map' =
- if KidSet.is_empty nvars then params_map
- else Bindings.add id nvars params_map in
+ | DEF_fundef fd ->
+ let (params_map', fd') = rewrite_sizeof_fun params_map fd in
(params_map', defs @ [DEF_fundef fd'])
+ | DEF_internal_mutrec fds ->
+ let rewrite_fd (params_map, fds) fd =
+ let (params_map', fd') = rewrite_sizeof_fun params_map fd in
+ (params_map', fds @ [fd']) in
+ (* TODO Split rewrite_sizeof_fun into an analysis and a rewrite pass,
+ so that we can call the analysis until a fixpoint is reached and then
+ rewrite the mutually recursive functions *)
+ let (params_map', fds') = List.fold_left rewrite_fd (params_map, []) fds in
+ (params_map', defs @ [DEF_internal_mutrec fds'])
| DEF_val (LB_aux (lb, annot)) ->
begin
let lb' = match lb with
@@ -1354,11 +1354,18 @@ let rewrite_sizeof (Defs defs) =
let (params_map, defs) = List.fold_left rewrite_sizeof_def
(Bindings.empty, []) defs in
let defs = List.map (rewrite_sizeof_valspec params_map) defs in
- Defs defs
- (* FIXME: Won't re-check due to flow typing and E_constraint re-write before E_sizeof re-write.
- Requires the typechecker to be more smart about different representations for valid flow typing constraints.
fst (check initial_env (Defs defs))
- *)
+
+let rewrite_defs_remove_assert defs =
+ let e_assert ((E_aux (eaux, (l, _)) as exp), str) = match eaux with
+ | E_constraint _ ->
+ E_assert (exp, str)
+ | _ ->
+ E_assert (E_aux (E_lit (mk_lit L_true), simple_annot l bool_typ), str) in
+ rewrite_defs_base
+ { rewriters_base with
+ rewrite_exp = (fun _ -> fold_exp { id_exp_alg with e_assert = e_assert}) }
+ defs
let remove_vector_concat_pat pat =
@@ -1874,7 +1881,7 @@ let contains_bitvector_pexp = function
(* Rewrite bitvector patterns to guarded patterns *)
-let remove_bitvector_pat pat =
+let remove_bitvector_pat (P_aux (_, (l, _)) as pat) =
let env = try pat_env_of pat with _ -> Env.empty in
@@ -1906,54 +1913,39 @@ let remove_bitvector_pat pat =
; fP_aux = (fun (fpat,annot) -> FP_aux (fpat,annot))
; fP_Fpat = (fun (id,p) -> FP_Fpat (id,p false))
} in
- let pat = (fold_pat name_bitvector_roots pat) false in
+ let pat, env = bind_pat env
+ (strip_pat ((fold_pat name_bitvector_roots pat) false))
+ (pat_typ_of pat) in
(* Then collect guard expressions testing whether the literal bits of a
bitvector pattern match those of a given bitvector, and collect let
bindings for the bits bound by P_id or P_as patterns *)
(* Helper functions for generating guard expressions *)
+ let mk_exp e_aux = E_aux (e_aux, (l, ())) in
+ let mk_num_exp i = mk_lit_exp (L_num i) in
+ let check_eq_exp l r =
+ let exp = mk_exp (E_app_infix (l, Id_aux (DeIid "==", Parse_ast.Unknown), r)) in
+ check_exp env exp bool_typ in
+
let access_bit_exp rootid l typ idx =
- let root = annot_exp (E_id rootid) l env typ in
- (* FIXME *)
- 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 access_aux = E_vector_access (mk_exp (E_id rootid), mk_num_exp idx) in
+ check_exp env (mk_exp access_aux) bit_typ 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
+ Some (check_eq_exp (strip_exp elem) (strip_exp exp)) in
let test_subvec_exp rootid l typ i j lits =
let (start, length, ord, _) = vector_typ_args_of typ in
- let length' = nint (List.length lits) in
- let start' =
- if is_order_inc ord then nint 0
- else nminus length' (nint 1) in
- let typ' = vector_typ start' length' ord bit_typ in
let subvec_exp =
match start, length with
| Nexp_aux (Nexp_constant s, _), Nexp_aux (Nexp_constant l, _)
when eq_big_int s i && eq_big_int l (big_int_of_int (List.length lits)) ->
- E_id rootid
+ mk_exp (E_id rootid)
| _ ->
- (*if vec_start t = i && vec_length t = List.length lits
- then E_id rootid
- else*)
- E_vector_subrange (
- 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 *)
- 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
+ mk_exp (E_vector_subrange (mk_exp (E_id rootid), mk_num_exp i, mk_num_exp j)) in
+ check_eq_exp subvec_exp (mk_exp (E_vector (List.map strip_exp lits))) in
let letbind_bit_exp rootid l typ idx id =
let rannot = simple_annot l typ in
@@ -2099,7 +2091,6 @@ let rewrite_exp_remove_bitvector_pat rewriters (E_aux (exp,(l,annot)) as full_ex
let rewrite_fun_remove_bitvector_pat
rewriters (FD_aux (FD_function(recopt,tannotopt,effectopt,funcls),(l,fdannot))) =
let _ = reset_fresh_name_counter () in
- (* TODO Can there be clauses with different id's in one FD_function? *)
let funcls = match funcls with
| (FCL_aux (FCL_Funcl(id,_,_),_) :: _) ->
let clause (FCL_aux (FCL_Funcl(_,pat,exp),annot)) =
@@ -2108,7 +2099,7 @@ let rewrite_fun_remove_bitvector_pat
(pat,guard,exp,annot) in
let cs = rewrite_guarded_clauses l (List.map clause funcls) in
List.map (fun (pat,exp,annot) -> FCL_aux (FCL_Funcl(id,pat,exp),annot)) cs
- | _ -> funcls (* TODO is the empty list possible here? *) in
+ | _ -> funcls in
FD_aux (FD_function(recopt,tannotopt,effectopt,funcls),(l,fdannot))
let rewrite_defs_remove_bitvector_pats (Defs defs) =
@@ -2171,6 +2162,10 @@ let id_is_local_var id env = match Env.lookup_id id env with
| Local _ -> true
| _ -> false
+let id_is_unbound id env = match Env.lookup_id id env with
+ | Unbound -> true
+ | _ -> false
+
let rec lexp_is_local (LEXP_aux (lexp, _)) env = match lexp with
| LEXP_memory _ -> false
| LEXP_id id
@@ -2180,10 +2175,6 @@ let rec lexp_is_local (LEXP_aux (lexp, _)) env = match lexp with
| LEXP_vector_range (lexp,_,_)
| LEXP_field (lexp,_) -> lexp_is_local lexp env
-let id_is_unbound id env = match Env.lookup_id id env with
- | Unbound -> true
- | _ -> false
-
let rec lexp_is_local_intro (LEXP_aux (lexp, _)) env = match lexp with
| LEXP_memory _ -> false
| LEXP_id id
@@ -2197,21 +2188,49 @@ let lexp_is_effectful (LEXP_aux (_, (_, annot))) = match annot with
| Some (_, _, eff) -> effectful_effs eff
| _ -> false
-let rec rewrite_local_lexp ((LEXP_aux(lexp,((l,_) as annot))) as le) =
- match lexp with
- | LEXP_id _ | LEXP_cast (_, _) | LEXP_tup _ -> (le, (fun exp -> exp))
- | LEXP_vector (lexp, e) ->
- let (lhs, rhs) = rewrite_local_lexp lexp in
- (lhs, (fun exp -> rhs (E_aux (E_vector_update (lexp_to_exp lexp, e, exp), annot))))
- | LEXP_vector_range (lexp, e1, e2) ->
- let (lhs, rhs) = rewrite_local_lexp lexp in
- (lhs, (fun exp -> rhs (E_aux (E_vector_update_subrange (lexp_to_exp lexp, e1, e2, exp), annot))))
- | LEXP_field (lexp, id) ->
- let (lhs, rhs) = rewrite_local_lexp lexp in
- let (LEXP_aux (_, recannot)) = lexp in
- let field_update exp = FES_aux (FES_Fexps ([FE_aux (FE_Fexp (id, exp), annot)], false), annot) in
- (lhs, (fun exp -> rhs (E_aux (E_record_update (lexp_to_exp lexp, field_update exp), recannot))))
- | _ -> raise (Reporting_basic.err_unreachable l ("Unsupported lexp: " ^ string_of_lexp le))
+let rec rewrite_lexp_to_rhs (do_rewrite : tannot lexp -> bool) ((LEXP_aux(lexp,((l,_) as annot))) as le) =
+ if do_rewrite le then
+ match lexp with
+ | LEXP_id _ | LEXP_cast (_, _) | LEXP_tup _ -> (le, (fun exp -> exp))
+ | LEXP_vector (lexp, e) ->
+ let (lhs, rhs) = rewrite_lexp_to_rhs do_rewrite lexp in
+ (lhs, (fun exp -> rhs (E_aux (E_vector_update (lexp_to_exp lexp, e, exp), annot))))
+ | LEXP_vector_range (lexp, e1, e2) ->
+ let (lhs, rhs) = rewrite_lexp_to_rhs do_rewrite lexp in
+ (lhs, (fun exp -> rhs (E_aux (E_vector_update_subrange (lexp_to_exp lexp, e1, e2, exp), annot))))
+ | LEXP_field (lexp, id) ->
+ begin
+ let (lhs, rhs) = rewrite_lexp_to_rhs do_rewrite lexp in
+ let (LEXP_aux (_, lannot)) = lexp in
+ let env = env_of_annot lannot in
+ match Env.expand_synonyms env (typ_of_annot lannot) with
+ | Typ_aux (Typ_app (Id_aux (Id "register", _), [Typ_arg_aux (Typ_arg_typ (Typ_aux (Typ_id regtyp_id, _)), _)]), _)
+ | Typ_aux (Typ_id regtyp_id, _) when Env.is_regtyp regtyp_id env ->
+ let base, top, ranges = Env.get_regtyp regtyp_id env in
+ let range, _ =
+ try List.find (fun (_, fid) -> Id.compare fid id = 0) ranges with
+ | Not_found ->
+ raise (Reporting_basic.err_typ l ("Field " ^ string_of_id id ^ " doesn't exist for register type " ^ string_of_id regtyp_id))
+ in
+ let lexp_exp = E_aux (E_app (mk_id ("cast_" ^ string_of_id regtyp_id), [lexp_to_exp lexp]), (l, None)) in
+ let n, m = match range with
+ | BF_aux (BF_single n, _) -> n, n
+ | BF_aux (BF_range (n, m), _) -> n, m
+ | _ -> raise (Reporting_basic.err_unreachable l ("Unsupported lexp: " ^ string_of_lexp le)) in
+ let rhs' exp = rhs (E_aux (E_vector_update_subrange (lexp_exp, simple_num l n, simple_num l m, exp), lannot)) in
+ (lhs, rhs')
+ | Typ_aux (Typ_id rectyp_id, _) | Typ_aux (Typ_app (rectyp_id, _), _) when Env.is_record rectyp_id env ->
+ let field_update exp = FES_aux (FES_Fexps ([FE_aux (FE_Fexp (id, exp), annot)], false), annot) in
+ (lhs, (fun exp -> rhs (E_aux (E_record_update (lexp_to_exp lexp, field_update exp), lannot))))
+ | _ -> raise (Reporting_basic.err_unreachable l ("Unsupported lexp: " ^ string_of_lexp le))
+ end
+ | _ -> raise (Reporting_basic.err_unreachable l ("Unsupported lexp: " ^ string_of_lexp le))
+ else (le, (fun exp -> exp))
+
+let updates_vars exp =
+ let e_assign ((_, lexp), (u, exp)) =
+ (u || lexp_is_local lexp (env_of exp), E_assign (lexp, exp)) in
+ fst (fold_exp { (compute_exp_alg false (||)) with e_assign = e_assign } exp)
(*Expects to be called after rewrite_defs; thus the following should not appear:
internal_exp of any form
@@ -2229,7 +2248,7 @@ let rewrite_exp_lift_assign_intro rewriters ((E_aux (exp,((l,_) as annot))) as f
| [] -> []
| (E_aux(E_assign(le,e), ((l, Some (env,typ,eff)) as annot)) as exp)::exps
when lexp_is_local_intro le env && not (lexp_is_effectful le) ->
- let (le', re') = rewrite_local_lexp le in
+ let (le', re') = rewrite_lexp_to_rhs (fun _ -> true) le in
let e' = re' (rewrite_base e) in
let exps' = walker exps in
let effects = union_eff_exps exps' in
@@ -2279,13 +2298,15 @@ let rewrite_exp_lift_assign_intro rewriters ((E_aux (exp,((l,_) as annot))) as f
(E_aux(E_if(c',t',e'),(Parse_ast.Generated l, annot))::exps',eff_union_exps (c'::t'::e'::exps')) new_vars)*)
| e::exps -> (rewrite_rec e)::(walker exps)
in
- rewrap (E_block (walker exps))
+ check_exp (env_of full_exp)
+ (E_aux (E_block (List.map strip_exp (walker exps)), (l, ()))) (typ_of full_exp)
| E_assign(le,e)
when lexp_is_local_intro le (env_of full_exp) && not (lexp_is_effectful le) ->
- let (le', re') = rewrite_local_lexp le in
+ let (le', re') = rewrite_lexp_to_rhs (fun _ -> true) le in
let e' = re' (rewrite_base e) 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))
+ check_exp (env_of full_exp)
+ (strip_exp (E_aux (E_internal_let(le', e', block), annot))) (typ_of full_exp)
| _ -> rewrite_base full_exp
let rewrite_lexp_lift_assign_intro rewriters ((LEXP_aux(lexp,annot)) as le) =
@@ -2309,6 +2330,79 @@ let rewrite_defs_exp_lift_assign defs = rewrite_defs_base
rewrite_def = rewrite_def;
rewrite_defs = rewrite_defs_base} defs
+
+(* Rewrite assignments to register references into calls to a builtin function
+ "write_reg_ref" (in the Lem shallow embedding). For example, if GPR is a
+ vector of register references, then
+ GPR[i] := exp;
+ becomes
+ write_reg_ref (vector_access (GPR, i)) exp
+ *)
+let rewrite_register_ref_writes (Defs defs) =
+ let (Defs write_reg_spec) = fst (check Env.empty (Defs (List.map gen_vs
+ [("write_reg_ref", "forall ('a : Type). (register('a), 'a) -> unit effect {wreg}")]))) in
+ let lexp_ref_exp (LEXP_aux (_, annot) as lexp) =
+ try
+ let exp = infer_exp (env_of_annot annot) (strip_exp (lexp_to_exp lexp)) in
+ if is_reftyp (typ_of exp) then Some exp else None
+ with | _ -> None in
+ let e_assign (lexp, exp) =
+ let (lhs, rhs) = rewrite_lexp_to_rhs (fun le -> lexp_ref_exp le = None) lexp in
+ match lexp_ref_exp lhs with
+ | Some (E_aux (_, annot) as lhs_exp) ->
+ let lhs = LEXP_aux (LEXP_memory (mk_id "write_reg_ref", [lhs_exp]), annot) in
+ E_assign (lhs, rhs exp)
+ | None -> E_assign (lexp, exp) in
+ let rewrite_exp _ = fold_exp { id_exp_alg with e_assign = e_assign } in
+
+ let generate_field_accessors l env id n1 n2 fields =
+ let i1, i2 = match n1, n2 with
+ | Nexp_aux(Nexp_constant i1, _),Nexp_aux(Nexp_constant i2, _) -> i1, i2
+ | _ -> raise (Reporting_basic.err_typ l
+ ("Non-constant indices in register type " ^ string_of_id id)) in
+ let dir_b = i1 < i2 in
+ let dir = (if dir_b then "true" else "false") in
+ let ord = Ord_aux ((if dir_b then Ord_inc else Ord_dec), Parse_ast.Unknown) in
+ let size = if dir_b then succ_big_int (sub_big_int i2 i1) else succ_big_int (sub_big_int i1 i2) in
+ let rtyp = mk_id_typ id in
+ let vtyp = vector_typ (nconstant i1) (nconstant size) ord bit_typ in
+ let accessors (fr, fid) =
+ let i, j = match fr with
+ | BF_aux (BF_single i, _) -> (i, i)
+ | BF_aux (BF_range (i, j), _) -> (i, j)
+ | _ -> raise (Reporting_basic.err_unreachable l "unsupported field type") in
+ let mk_num_exp i = mk_lit_exp (L_num i) in
+ let reg_pat, reg_env = bind_pat env (mk_pat (P_typ (rtyp, mk_pat (P_id (mk_id "reg"))))) rtyp in
+ let inferred_get = infer_exp reg_env (mk_exp (E_vector_subrange
+ (mk_exp (E_id (mk_id "reg")), mk_num_exp i, mk_num_exp j))) in
+ let ftyp = typ_of inferred_get in
+ let v_pat, v_env = bind_pat reg_env (mk_pat (P_typ (ftyp, mk_pat (P_id (mk_id "v"))))) ftyp in
+ let inferred_set = infer_exp v_env (mk_exp (E_vector_update_subrange
+ (mk_exp (E_id (mk_id "reg")), mk_num_exp i, mk_num_exp j, mk_exp (E_id (mk_id "v"))))) in
+ let set_args = P_aux (P_tup [reg_pat; v_pat], (l, Some (env, tuple_typ [rtyp; ftyp], no_effect))) in
+ let fsuffix = "_" ^ string_of_id id ^ "_" ^ string_of_id fid in
+ let rec_opt = Rec_aux (Rec_nonrec, l) in
+ let tannot ret_typ = Typ_annot_opt_aux (Typ_annot_opt_some (TypQ_aux (TypQ_tq [], l), ret_typ), l) in
+ let eff_opt = Effect_opt_aux (Effect_opt_pure, l) in
+ let mk_funcl id pat exp = FCL_aux (FCL_Funcl (mk_id id, pat, exp), (l, None)) in
+ let mk_fundef id pat exp ret_typ = DEF_fundef (FD_aux (FD_function (rec_opt, tannot ret_typ, eff_opt, [mk_funcl id pat exp]), (l, None))) in
+ [mk_fundef ("get" ^ fsuffix) reg_pat inferred_get ftyp;
+ mk_fundef ("set" ^ fsuffix) set_args inferred_set (typ_of inferred_set)] in
+ List.concat (List.map accessors fields) in
+
+ let rewriters = { rewriters_base with rewrite_exp = rewrite_exp } in
+ let rec rewrite ds = match ds with
+ | (DEF_type (TD_aux (TD_register (id, n1, n2, fields), (l, Some (env, _, _)))) as d) :: ds ->
+ let (Defs d), env = check env (Defs [d]) in
+ d @ (generate_field_accessors l env id n1 n2 fields) @ rewrite ds
+ | d::ds -> (rewriters.rewrite_def rewriters d)::(rewrite ds)
+ | [] -> [] in
+ Defs (rewrite (write_reg_spec @ defs))
+
+ (* rewrite_defs_base { rewriters_base with rewrite_exp = rewrite_exp }
+ (Defs (write_reg_spec @ defs)) *)
+
+
(*let rewrite_exp_separate_ints rewriters ((E_aux (exp,((l,_) as annot))) as full_exp) =
(*let tparms,t,tag,nexps,eff,cum_eff,bounds = match annot with
| Base((tparms,t),tag,nexps,eff,cum_eff,bounds) -> tparms,t,tag,nexps,eff,cum_eff,bounds
@@ -2356,7 +2450,14 @@ let rewrite_defs_separate_numbs defs = rewrite_defs_base
rewrite_def = rewrite_def;
rewrite_defs = rewrite_defs_base} defs*)
-let rewrite_defs_early_return =
+(* Remove redundant return statements, and translate remaining ones into an
+ (effectful) call to builtin function "early_return" (in the Lem shallow
+ embedding).
+
+ TODO: Maybe separate generic removal of redundant returns, and Lem-specific
+ rewriting of early returns
+ *)
+let rewrite_defs_early_return (Defs defs) =
let is_return (E_aux (exp, _)) = match exp with
| E_return _ -> true
| _ -> false in
@@ -2394,13 +2495,15 @@ let rewrite_defs_early_return =
else E_case (e, pes) in
let e_aux (exp, (l, annot)) =
- let full_exp = fix_eff_exp (E_aux (exp, (l, annot))) in
- match annot with
- | Some (env, typ, eff) when is_return full_exp ->
+ let full_exp = propagate_exp_effect (E_aux (exp, (l, annot))) in
+ let env = env_of full_exp in
+ match full_exp with
+ | E_aux (E_return exp, (l, Some (env, typ, eff))) ->
(* Add escape effect annotation, since we use the exception mechanism
of the state monad to implement early return in the Lem backend *)
let annot' = Some (env, typ, union_effects eff (mk_effect [BE_escape])) in
- E_aux (exp, (l, annot'))
+ let exp' = annot_exp (E_cast (typ_of exp, exp)) l env (typ_of exp) in
+ E_aux (E_app (mk_id "early_return", [exp']), (l, annot'))
| _ -> full_exp in
let rewrite_funcl_early_return _ (FCL_aux (FCL_Funcl (id, pat, exp), a)) =
@@ -2423,7 +2526,12 @@ let rewrite_defs_early_return =
FD_aux (FD_function (rec_opt, tannot_opt, effect_opt,
List.map (rewrite_funcl_early_return rewriters) funcls), a) in
- rewrite_defs_base { rewriters_base with rewrite_fun = rewrite_fun_early_return }
+ let (Defs early_ret_spec) = fst (check Env.empty (Defs [gen_vs
+ ("early_return", "forall ('a : Type) ('b : Type). 'a -> 'b effect {escape}")])) in
+
+ rewrite_defs_base
+ { rewriters_base with rewrite_fun = rewrite_fun_early_return }
+ (Defs (early_ret_spec @ defs))
(* Propagate effects of functions, if effect checking and propagation
have not been performed already by the type checker. *)
@@ -2497,6 +2605,11 @@ let rewrite_fix_val_specs (Defs defs) =
Rec_aux (Rec_rec, Parse_ast.Unknown)
else recopt
in
+ let tannotopt = match tannotopt, funcls with
+ | Typ_annot_opt_aux (Typ_annot_opt_some (typq, typ), l),
+ FCL_aux (FCL_Funcl (_, _, exp), _) :: _ ->
+ Typ_annot_opt_aux (Typ_annot_opt_some (typq, rewrite_typ_nexp_ids (env_of exp) typ), l)
+ | _ -> tannotopt in
(val_specs, FD_aux (FD_function (recopt, tannotopt, effopt, funcls), a)) in
let rec rewrite_fundefs (val_specs, fundefs) =
@@ -2784,7 +2897,7 @@ let rewrite_simple_assignments defs =
let env = env_of_annot annot in
match e_aux with
| E_assign (lexp, exp) ->
- let (lexp, rhs) = rewrite_local_lexp lexp in
+ let (lexp, rhs) = rewrite_lexp_to_rhs (fun _ -> true) lexp in
let assign = mk_exp (E_assign (strip_lexp lexp, strip_exp (rhs exp))) in
check_exp env assign unit_typ
| _ -> E_aux (e_aux, annot)
@@ -2801,13 +2914,9 @@ let rewrite_defs_remove_blocks =
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 = (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 wild = P_typ (typ, annot_pat P_wild l env typ) in
+ let e_aux = E_let (annot_letbind (wild, v) l env typ, body) in
+ propagate_exp_effect (annot_exp e_aux l env (typ_of body)) in
let rec f l = function
| [] -> E_aux (E_lit (L_aux (L_unit,gen_loc l)), (simple_annot l unit_typ))
@@ -2839,11 +2948,13 @@ let letbind (v : 'a exp) (body : 'a exp -> 'a exp) : 'a exp =
| Some (env, Typ_aux (Typ_id tid, _), eff) when string_of_id tid = "unit" ->
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 lb = annot_letbind (P_wild, v) l env unit_typ in
+ let wild = P_typ (typ_of v, annot_pat P_wild l env (typ_of v)) in
+ let lb = annot_letbind (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 lb = annot_letbind (P_id id, v) l env typ in
+ let pat = P_typ (typ_of v, annot_pat (P_id id) l env (typ_of v)) in
+ let lb = annot_letbind (pat, 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 ->
@@ -3058,8 +3169,8 @@ let rewrite_defs_letbind_effects =
k (rewrap (E_assign (lexp,exp1)))))
| E_exit exp' -> k (E_aux (E_exit (n_exp_term (effectful exp') exp'),annot))
| E_assert (exp1,exp2) ->
- n_exp exp1 (fun exp1 ->
- n_exp exp2 (fun exp2 ->
+ n_exp_name exp1 (fun exp1 ->
+ n_exp_name exp2 (fun exp2 ->
k (rewrap (E_assert (exp1,exp2)))))
| E_internal_cast (annot',exp') ->
n_exp_name exp' (fun exp' ->
@@ -3114,7 +3225,7 @@ let rewrite_defs_letbind_effects =
; rewrite_defs = rewrite_defs_base
}
-let rewrite_defs_effectful_let_expressions =
+let rewrite_defs_internal_lets =
let rec pat_of_local_lexp (LEXP_aux (lexp, ((l, _) as annot))) = match lexp with
| LEXP_id id -> P_aux (P_id id, annot)
@@ -3124,26 +3235,31 @@ let rewrite_defs_effectful_let_expressions =
let e_let (lb,body) =
match lb with
- | LB_aux (LB_val (P_aux (P_wild, _), E_aux (E_assign ((LEXP_aux (_, annot) as le), exp), _)), _)
+ | LB_aux (LB_val (P_aux ((P_wild | P_typ (_, P_aux (P_wild, _))), _),
+ E_aux (E_assign ((LEXP_aux (_, annot) as le), exp), (l, _))), _)
when lexp_is_local le (env_of_annot annot) && not (lexp_is_effectful le) ->
- (* Rewrite assignments to local variables into let bindings *)
- let (lhs, rhs) = rewrite_local_lexp le in
- E_let (LB_aux (LB_val (pat_of_local_lexp lhs, rhs exp), annot), body)
+ (* Rewrite assignments to local variables into let bindings *)
+ let (lhs, rhs) = rewrite_lexp_to_rhs (fun _ -> true) le in
+ let (LEXP_aux (_, lannot)) = lhs in
+ let ltyp = typ_of_annot lannot in
+ let rhs = annot_exp (E_cast (ltyp, rhs exp)) l (env_of_annot lannot) ltyp in
+ E_let (LB_aux (LB_val (pat_of_local_lexp lhs, rhs), annot), body)
| LB_aux (LB_val (pat,exp'),annot') ->
if effectful exp'
then E_internal_plet (pat,exp',body)
else E_let (lb,body) in
let e_internal_let = fun (lexp,exp1,exp2) ->
- match lexp with
- | LEXP_aux (LEXP_id id,annot)
- | LEXP_aux (LEXP_cast (_,id),annot) ->
- if effectful exp1 then
- E_internal_plet (P_aux (P_id id,annot),exp1,exp2)
- else
- let lb = LB_aux (LB_val (P_aux (P_id id,annot), exp1), annot) in
- E_let (lb, exp2)
+ let paux, annot = match lexp with
+ | LEXP_aux (LEXP_id id, annot) ->
+ (P_id id, annot)
+ | LEXP_aux (LEXP_cast (typ, id), annot) ->
+ (P_typ (typ, P_aux (P_id id, annot)), annot)
| _ -> failwith "E_internal_let with unexpected lexp" in
+ if effectful exp1 then
+ E_internal_plet (P_aux (paux, annot), exp1, exp2)
+ else
+ E_let (LB_aux (LB_val (P_aux (paux, annot), exp1), annot), exp2) in
let alg = { id_exp_alg with e_let = e_let; e_internal_let = e_internal_let } in
rewrite_defs_base
@@ -3170,56 +3286,31 @@ let eqidtyp (id1,_) (id2,_) =
name1 = name2
let find_introduced_vars exp =
- let e_aux ((ids,e_aux),annot) =
- let ids = match e_aux, annot with
- | E_internal_let (LEXP_aux (LEXP_id id, _), _, _), (_, Some (env, _, _))
- | E_internal_let (LEXP_aux (LEXP_cast (_, id), _), _, _), (_, Some (env, _, _))
- when id_is_unbound id env -> IdSet.add id ids
- | _ -> ids in
- (ids, E_aux (e_aux, annot)) in
+ let lEXP_aux ((ids, lexp), annot) =
+ let ids = match lexp with
+ | LEXP_id id | LEXP_cast (_, id)
+ when id_is_unbound id (env_of_annot annot) -> IdSet.add id ids
+ | _ -> ids in
+ (ids, LEXP_aux (lexp, annot)) in
fst (fold_exp
- { (compute_exp_alg IdSet.empty IdSet.union) with e_aux = e_aux } exp)
+ { (compute_exp_alg IdSet.empty IdSet.union) with lEXP_aux = lEXP_aux } exp)
let find_updated_vars exp =
let intros = find_introduced_vars exp in
- let e_aux ((ids,e_aux),annot) =
- let ids = match e_aux, annot with
- | E_assign (LEXP_aux (LEXP_id id, _), _), (_, Some (env, _, _))
- | E_assign (LEXP_aux (LEXP_cast (_, id), _), _), (_, Some (env, _, _))
- when id_is_local_var id env && not (IdSet.mem id intros) ->
- (id, annot) :: ids
- | _ -> ids in
- (ids, E_aux (e_aux, annot)) in
+ let lEXP_aux ((ids, lexp), annot) =
+ let ids = match lexp with
+ | LEXP_id id | LEXP_cast (_, id)
+ when id_is_local_var id (env_of_annot annot) && not (IdSet.mem id intros) ->
+ (id, annot) :: ids
+ | _ -> ids in
+ (ids, LEXP_aux (lexp, annot)) in
dedup eqidtyp (fst (fold_exp
- { (compute_exp_alg [] (@)) with e_aux = e_aux } exp))
+ { (compute_exp_alg [] (@)) with lEXP_aux = lEXP_aux } exp))
let swaptyp typ (l,tannot) = match tannot with
| Some (env, typ', eff) -> (l, Some (env, typ, eff))
| _ -> raise (Reporting_basic.err_unreachable l "swaptyp called with empty type annotation")
-let mktup l es =
- match es with
- | [] -> annot_exp (E_lit (mk_lit L_unit)) (gen_loc l) Env.empty unit_typ
- | [e] -> e
- | e :: _ ->
- let typ = mk_typ (Typ_tup (List.map typ_of es)) in
- propagate_exp_effect (annot_exp (E_tuple es) (gen_loc l) (env_of e) typ)
-
-let mktup_pat l es =
- match es with
- | [] -> annot_pat P_wild (gen_loc l) Env.empty unit_typ
- | [E_aux (E_id id,_) as 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) ->
- annot_pat (P_id id) (gen_loc l) (env_of exp) (typ_of exp)
- | exp ->
- 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 =
| Added_vars of 'a exp * 'a pat
| Same_vars of 'a exp
@@ -3254,9 +3345,33 @@ let rec rewrite_var_updates ((E_aux (expaux,((l,_) as annot))) as exp) =
else
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) =
- let overwrite = match typ_of_annot annot with
+
+ let mk_varstup l es =
+ let exp_to_pat (E_aux (eaux, annot) as exp) = match eaux with
+ | E_lit lit ->
+ P_aux (P_lit lit, annot)
+ | E_id id ->
+ annot_pat (P_id id) l (env_of exp) (typ_of exp)
+ | _ -> raise (Reporting_basic.err_unreachable l
+ ("Failed to extract pattern from expression " ^ string_of_exp exp)) in
+ match es with
+ | [] ->
+ annot_exp (E_lit (mk_lit L_unit)) (gen_loc l) Env.empty unit_typ,
+ annot_pat P_wild (gen_loc l) Env.empty unit_typ
+ | [e] ->
+ let e = infer_exp (env_of e) (strip_exp e) in
+ e, annot_pat (P_typ (typ_of e, exp_to_pat e)) l (env_of e) (typ_of e)
+ | e :: _ ->
+ let infer_e e = infer_exp (env_of e) (strip_exp e) in
+ let es = List.map infer_e es in
+ let pats = List.map exp_to_pat es in
+ let typ = tuple_typ (List.map typ_of es) in
+ annot_exp (E_tuple es) l (env_of e) typ,
+ annot_pat (P_typ (typ, annot_pat (P_tup pats) l (env_of e) typ)) l (env_of e) typ in
+
+ let rewrite (E_aux (expaux,((el,_) as annot)) as full_exp) (P_aux (_,(pl,pannot)) as pat) =
+ let env = env_of_annot annot in
+ let overwrite = match typ_of full_exp with
| Typ_aux (Typ_id (Id_aux (Id "unit", _)), _) -> true
| _ -> false in
match expaux with
@@ -3271,62 +3386,44 @@ let rec rewrite_var_updates ((E_aux (expaux,((l,_) as annot))) as exp) =
expects. In (Lem) pretty-printing, this turned into an anonymous
function and passed to foreach*. *)
let vars = List.map (fun (var,(l,t)) -> E_aux (E_id var,(l,t))) (find_updated_vars exp4) in
- let vartuple = mktup el vars in
- let exp4 = rewrite_var_updates (add_vars overwrite exp4 vartuple) in
- let (E_aux (_,(_,annot4))) = exp4 in
- let fname = match effectful exp4,order with
- | false, Ord_aux (Ord_inc,_) -> "foreach_inc"
- | false, Ord_aux (Ord_dec,_) -> "foreach_dec"
- | true, Ord_aux (Ord_inc,_) -> "foreachM_inc"
- | 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,gen_loc el) in
- let loopvar =
- (* Don't bother with creating a range type annotation, since the
- Lem pretty-printing does not use it. *)
- (* let (bf,tf) = match typ_of exp1 with
- | {t = Tapp ("atom",[TA_nexp f])} -> (TA_nexp f,TA_nexp f)
- | {t = Tapp ("reg", [TA_typ {t = Tapp ("atom",[TA_nexp f])}])} -> (TA_nexp f,TA_nexp f)
- | {t = Tapp ("range",[TA_nexp bf;TA_nexp tf])} -> (TA_nexp bf,TA_nexp tf)
- | {t = Tapp ("reg", [TA_typ {t = Tapp ("range",[TA_nexp bf;TA_nexp tf])}])} -> (TA_nexp bf,TA_nexp tf)
- | {t = Tapp (name,_)} -> failwith (name ^ " shouldn't be here") in
- let (bt,tt) = match typ_of exp2 with
- | {t = Tapp ("atom",[TA_nexp t])} -> (TA_nexp t,TA_nexp t)
- | {t = Tapp ("atom",[TA_typ {t = Tapp ("atom", [TA_nexp t])}])} -> (TA_nexp t,TA_nexp t)
- | {t = Tapp ("range",[TA_nexp bt;TA_nexp tt])} -> (TA_nexp bt,TA_nexp tt)
- | {t = Tapp ("atom",[TA_typ {t = Tapp ("range",[TA_nexp bt;TA_nexp tt])}])} -> (TA_nexp bt,TA_nexp tt)
- | {t = Tapp (name,_)} -> failwith (name ^ " shouldn't be here") in
- let t = {t = Tapp ("range",match order with
- | Ord_aux (Ord_inc,_) -> [bf;tt]
- | Ord_aux (Ord_dec,_) -> [tf;bt])} 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]),
- (gen_loc el, annot4)) in
+ let varstuple, varspat = mk_varstup el vars in
+ let varstyp = typ_of varstuple in
+ let exp4 = rewrite_var_updates (add_vars overwrite exp4 varstuple) in
+ let ord_exp, lower, upper = match destruct_range (typ_of exp1), destruct_range (typ_of exp2) with
+ | None, _ | _, None ->
+ raise (Reporting_basic.err_unreachable el "Could not determine loop bounds")
+ | Some (l1, u1), Some (l2, u2) ->
+ if is_order_inc order
+ then (annot_exp (E_lit (mk_lit L_true)) el env bool_typ, l1, u2)
+ else (annot_exp (E_lit (mk_lit L_false)) el env bool_typ, l2, u1) in
+ let lvar_kid = mk_kid ("loop_" ^ string_of_id id) in
+ let lvar_nc = nc_and (nc_lteq lower (nvar lvar_kid)) (nc_lteq (nvar lvar_kid) upper) in
+ let lvar_typ = mk_typ (Typ_exist ([lvar_kid], lvar_nc, atom_typ (nvar lvar_kid))) in
+ let lvar_pat = P_typ (lvar_typ, annot_pat (P_var (
+ annot_pat (P_id id) el env (atom_typ (nvar lvar_kid)),
+ lvar_kid)) el env lvar_typ) in
+ let lb = annot_letbind (lvar_pat, exp1) el env lvar_typ in
+ let body = annot_exp (E_let (lb, exp4)) el env (typ_of exp4) in
+ let v = annot_exp (E_app (mk_id "foreach", [exp1; exp2; exp3; ord_exp; varstuple; body])) el env (typ_of body) in
let pat =
- if overwrite then mktup_pat el vars
- else annot_pat (P_tup [pat; mktup_pat pl vars]) pl env (typ_of v) in
+ if overwrite then varspat
+ else annot_pat (P_tup [pat; varspat]) 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
- let vartuple = mktup el vars in
- (* let cond = rewrite_var_updates (add_vars false cond vartuple) in *)
- let body = rewrite_var_updates (add_vars overwrite body vartuple) in
+ let varstuple, varspat = mk_varstup el vars in
+ let varstyp = typ_of varstuple in
+ (* let cond = rewrite_var_updates (add_vars false cond varstuple) in *)
+ let body = rewrite_var_updates (add_vars overwrite body varstuple) in
let (E_aux (_,(_,bannot))) = body in
- let fname = match loop, effectful cond, effectful body with
- | While, false, false -> "while_PP"
- | While, false, true -> "while_PM"
- | While, true, false -> "while_MP"
- | While, true, true -> "while_MM"
- | Until, false, false -> "until_PP"
- | Until, false, true -> "until_PM"
- | Until, true, false -> "until_MP"
- | Until, true, true -> "until_MM" in
+ let fname = match loop with
+ | While -> "while"
+ | Until -> "until" in
let funcl = Id_aux (Id fname,gen_loc el) in
- let v = E_aux (E_app (funcl,[cond;body;vartuple]), (gen_loc el, bannot)) in
+ let v = E_aux (E_app (funcl,[cond;varstuple;body]), (gen_loc el, bannot)) in
let pat =
- if overwrite then mktup_pat el vars
- else annot_pat (P_tup [pat; mktup_pat pl vars]) pl env (typ_of v) in
+ if overwrite then varspat
+ else annot_pat (P_tup [pat; varspat]) 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)))
@@ -3334,17 +3431,18 @@ let rec rewrite_var_updates ((E_aux (expaux,((l,_) as annot))) as exp) =
if vars = [] then
(Same_vars (E_aux (E_if (c,rewrite_var_updates e1,rewrite_var_updates e2),annot)))
else
- let vartuple = mktup el vars in
- let e1 = rewrite_var_updates (add_vars overwrite e1 vartuple) in
- let e2 = rewrite_var_updates (add_vars overwrite e2 vartuple) in
+ let varstuple, varspat = mk_varstup el vars in
+ let varstyp = typ_of varstuple in
+ let e1 = rewrite_var_updates (add_vars overwrite e1 varstuple) in
+ let e2 = rewrite_var_updates (add_vars overwrite e2 varstuple) in
(* after rewrite_defs_letbind_effects c has no variable updates *)
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), (gen_loc el, Some (env, typ, eff))) in
let pat =
- if overwrite then mktup_pat el vars
- else annot_pat (P_tup [pat; mktup_pat pl vars]) pl env (typ_of v) in
+ if overwrite then varspat
+ else annot_pat (P_tup [pat; varspat]) pl env (typ_of v) in
Added_vars (v,pat)
| E_case (e1,ps) ->
(* after rewrite_defs_letbind_effects e1 needs no rewriting *)
@@ -3361,10 +3459,11 @@ let rec rewrite_var_updates ((E_aux (expaux,((l,_) as annot))) as exp) =
Pat_aux (Pat_when (p,g,rewrite_var_updates e),a)) ps in
Same_vars (E_aux (E_case (e1,ps),annot))
else
- let vartuple = mktup el vars in
+ let varstuple, varspat = mk_varstup el vars in
+ let varstyp = typ_of varstuple in
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 exp = rewrite_var_updates (add_vars overwrite exp varstuple) in
let pannot = (l, Some (env_of exp, typ_of exp, effect_of exp)) in
Pat_aux (Pat_exp (pat, exp), pannot)
| Pat_when _ ->
@@ -3374,36 +3473,26 @@ let rec rewrite_var_updates ((E_aux (expaux,((l,_) as annot))) as exp) =
| 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
- let e = rewrite_var_updates (add_vars overwrite e vartuple) in
- let pannot = simple_annot pl (typ_of e) in
- let effs = union_effects effs (effect_of e) in
- 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), (gen_loc pl, Some (env_of_annot annot, typ, effs))) in *)
let pat =
- if overwrite then mktup_pat el vars
- else annot_pat (P_tup [pat; mktup_pat pl vars]) pl env (typ_of v) in
+ if overwrite then varspat
+ else annot_pat (P_tup [pat; varspat]) pl env (typ_of v) in
Added_vars (v,pat)
| E_assign (lexp,vexp) ->
- let effs = match effect_of_annot (snd annot) with
- | Effect_aux (Effect_set effs, _) -> effs
+ let mk_id_pat id = match Env.lookup_id id env with
+ | Local (_, typ) ->
+ annot_pat (P_typ (typ, annot_pat (P_id id) pl env typ)) pl env typ
| _ ->
- raise (Reporting_basic.err_unreachable l
- "assignment without effects annotation") in
+ raise (Reporting_basic.err_unreachable pl
+ ("Failed to look up type of variable " ^ string_of_id id)) in
if effectful exp then
Same_vars (E_aux (E_assign (lexp,vexp),annot))
else
(match lexp with
| LEXP_aux (LEXP_id id,annot) ->
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 = annot_pat (P_id id) pl env (typ_of vexp) in
+ Added_vars (vexp, mk_id_pat id)
+ | LEXP_aux (LEXP_cast (typ,id),annot) ->
+ let pat = annot_pat (P_typ (typ, annot_pat (P_id id) pl env (typ_of vexp))) pl env typ in
Added_vars (vexp,pat)
| LEXP_aux (LEXP_vector (LEXP_aux (LEXP_id id,((l2,_) as annot2)),i),((l1,_) as annot)) ->
let eid = annot_exp (E_id id) l2 env (typ_of_annot annot2) in
@@ -3433,27 +3522,17 @@ let rec rewrite_var_updates ((E_aux (expaux,((l,_) as annot))) as exp) =
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
+ let paux, typ = match lexp with
+ | LEXP_aux (LEXP_id id, _) ->
+ P_id id, typ_of v
+ | LEXP_aux (LEXP_cast (typ, id), _) ->
+ P_typ (typ, annot_pat (P_id id) l env (typ_of v)), typ
| _ ->
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 lb = annot_letbind (paux, v) l env typ 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 = (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),(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
@@ -3497,17 +3576,17 @@ let rewrite_defs_remove_superfluous_letbinds =
| E_let (lb,exp2) ->
begin match lb,exp2 with
(* 'let x = EXP1 in x' can be replaced with 'EXP1' *)
- | LB_aux (LB_val (P_aux (P_id (Id_aux (id,_)),_),exp1),_),
- E_aux (E_id (Id_aux (id',_)),_)
- | LB_aux (LB_val (P_aux (P_id (Id_aux (id,_)),_),exp1),_),
- E_aux (E_cast (_,E_aux (E_id (Id_aux (id',_)),_)),_)
- when id = id' ->
+ | LB_aux (LB_val (P_aux (P_id id, _), exp1), _),
+ E_aux (E_id id', _)
+ | LB_aux (LB_val (P_aux (P_id id, _), exp1), _),
+ E_aux (E_cast (_,E_aux (E_id id', _)), _)
+ when Id.compare id id' == 0 && id_is_unbound id (env_of_annot annot) ->
exp1
(* "let x = EXP1 in return x" can be replaced with 'return (EXP1)', at
least when EXP1 is 'small' enough *)
- | LB_aux (LB_val (P_aux (P_id (Id_aux (id,_)),_),exp1),_),
- E_aux (E_internal_return (E_aux (E_id (Id_aux (id',_)),_)),_)
- when id = id' && small exp1 ->
+ | LB_aux (LB_val (P_aux (P_id id, _), exp1), _),
+ E_aux (E_internal_return (E_aux (E_id id', _)), _)
+ when Id.compare id id' == 0 && small exp1 && id_is_unbound id (env_of_annot annot) ->
let (E_aux (_,e1annot)) = exp1 in
E_aux (E_internal_return (exp1),e1annot)
| _ -> E_aux (exp,annot)
@@ -3532,21 +3611,44 @@ let rewrite_defs_remove_superfluous_returns =
| Typ_aux (Typ_id (Id_aux (Id "unit", _)), _) -> true
| _ -> false in
+ let untyp_pat = function
+ | P_aux (P_typ (typ, pat), _) -> pat, Some typ
+ | pat -> pat, None in
+
+ let uncast_internal_return = function
+ | E_aux (E_internal_return (E_aux (E_cast (typ, exp), _)), a) ->
+ E_aux (E_internal_return exp, a), Some typ
+ | exp -> exp, None in
+
let e_aux (exp,annot) = match exp with
- | E_internal_plet (pat,exp1,exp2) when effectful exp1 ->
- begin match pat,exp2 with
- | P_aux (P_lit (L_aux (lit,_)),_),
- E_aux (E_internal_return (E_aux (E_lit (L_aux (lit',_)),_)),_)
- when lit = lit' ->
- exp1
- | P_aux (P_wild,pannot),
- E_aux (E_internal_return (E_aux (E_lit (L_aux (L_unit,_)),_)),_)
- when has_unittype exp1 ->
- exp1
- | P_aux (P_id (Id_aux (id,_)),_),
- E_aux (E_internal_return (E_aux (E_id (Id_aux (id',_)),_)),_)
- when id = id' ->
- exp1
+ | E_let (LB_aux (LB_val (pat, exp1), _), exp2)
+ | E_internal_plet (pat, exp1, exp2)
+ when effectful exp1 ->
+ begin match untyp_pat pat, uncast_internal_return exp2 with
+ | (P_aux (P_lit (L_aux (lit,_)),_), ptyp),
+ (E_aux (E_internal_return (E_aux (E_lit (L_aux (lit',_)),_)), a), etyp)
+ when lit = lit' ->
+ begin
+ match ptyp, etyp with
+ | Some typ, _ | _, Some typ -> E_aux (E_cast (typ, exp1), a)
+ | None, None -> exp1
+ end
+ | (P_aux (P_wild,pannot), ptyp),
+ (E_aux (E_internal_return (E_aux (E_lit (L_aux (L_unit,_)),_)), a), etyp)
+ when has_unittype exp1 ->
+ begin
+ match ptyp, etyp with
+ | Some typ, _ | _, Some typ -> E_aux (E_cast (typ, exp1), a)
+ | None, None -> exp1
+ end
+ | (P_aux (P_id id,_), ptyp),
+ (E_aux (E_internal_return (E_aux (E_id id',_)), a), etyp)
+ when Id.compare id id' == 0 && id_is_unbound id (env_of_annot annot) ->
+ begin
+ match ptyp, etyp with
+ | Some typ, _ | _, Some typ -> E_aux (E_cast (typ, exp1), a)
+ | None, None -> exp1
+ end
| _ -> E_aux (exp,annot)
end
| _ -> E_aux (exp,annot) in
@@ -3563,7 +3665,11 @@ let rewrite_defs_remove_superfluous_returns =
}
-let rewrite_defs_remove_e_assign =
+let rewrite_defs_remove_e_assign (Defs defs) =
+ let (Defs loop_specs) = fst (check Env.empty (Defs (List.map gen_vs
+ [("foreach", "forall ('vars : Type). (int, int, int, bool, 'vars, 'vars) -> 'vars");
+ ("while", "forall ('vars : Type). (bool, 'vars, 'vars) -> 'vars");
+ ("until", "forall ('vars : Type). (bool, 'vars, 'vars) -> 'vars")]))) in
let rewrite_exp _ e =
replace_memwrite_e_assign (remove_reference_types (rewrite_var_updates e)) in
rewrite_defs_base
@@ -3574,32 +3680,35 @@ let rewrite_defs_remove_e_assign =
; rewrite_fun = rewrite_fun
; rewrite_def = rewrite_def
; rewrite_defs = rewrite_defs_base
- }
+ } (Defs (loop_specs @ defs))
let recheck_defs defs = fst (check initial_env defs)
let rewrite_defs_lem = [
- ("top_sort_defs", top_sort_defs);
("tuple_vector_assignments", rewrite_tuple_vector_assignments);
("tuple_assignments", rewrite_tuple_assignments);
(* ("simple_assignments", rewrite_simple_assignments); *)
- ("constraint", rewrite_constraint);
- ("trivial_sizeof", rewrite_trivial_sizeof);
- ("sizeof", rewrite_sizeof);
("remove_vector_concat", rewrite_defs_remove_vector_concat);
("remove_bitvector_pats", rewrite_defs_remove_bitvector_pats);
("guarded_pats", rewrite_defs_guarded_pats);
- (* ("recheck_defs", recheck_defs); *)
+ ("exp_lift_assign", rewrite_defs_exp_lift_assign);
+ ("register_ref_writes", rewrite_register_ref_writes);
+ ("recheck_defs", recheck_defs);
+ (* ("constraint", rewrite_constraint); *)
+ (* ("remove_assert", rewrite_defs_remove_assert); *)
+ ("top_sort_defs", top_sort_defs);
+ ("trivial_sizeof", rewrite_trivial_sizeof);
+ ("sizeof", rewrite_sizeof);
("early_return", rewrite_defs_early_return);
("nexp_ids", rewrite_defs_nexp_ids);
("fix_val_specs", rewrite_fix_val_specs);
- ("exp_lift_assign", rewrite_defs_exp_lift_assign);
("remove_blocks", rewrite_defs_remove_blocks);
("letbind_effects", rewrite_defs_letbind_effects);
("remove_e_assign", rewrite_defs_remove_e_assign);
- ("effectful_let_expressions", rewrite_defs_effectful_let_expressions);
+ ("internal_lets", rewrite_defs_internal_lets);
("remove_superfluous_letbinds", rewrite_defs_remove_superfluous_letbinds);
- ("remove_superfluous_returns", rewrite_defs_remove_superfluous_returns)
+ ("remove_superfluous_returns", rewrite_defs_remove_superfluous_returns);
+ ("recheck_defs", recheck_defs)
]
let rewrite_defs_ocaml = [
diff --git a/src/spec_analysis.ml b/src/spec_analysis.ml
index bdbc031a..424481b5 100644
--- a/src/spec_analysis.ml
+++ b/src/spec_analysis.ml
@@ -334,6 +334,10 @@ let rec fv_of_exp consider_var bound used set (E_aux (e,(_,tannot))) : (Nameset.
| E_let(lebind,e) ->
let b,u,s = fv_of_let consider_var bound used set lebind in
fv_of_exp consider_var b u s e
+ | E_internal_let (lexp, exp1, exp2) ->
+ let b,u,s = fv_of_lexp consider_var bound used set lexp in
+ let _,used,set = fv_of_exp consider_var bound used set exp1 in
+ fv_of_exp consider_var b used set exp2
| E_assign(lexp,e) ->
let b,u,s = fv_of_lexp consider_var bound used set lexp in
let _,used,set = fv_of_exp consider_var bound u s e in
diff --git a/src/type_check.ml b/src/type_check.ml
index 2260416d..1782a11b 100644
--- a/src/type_check.ml
+++ b/src/type_check.ml
@@ -133,14 +133,6 @@ let orig_kid (Kid_aux (Var v, l) as kid) =
with
| Not_found -> kid
-let is_range (Typ_aux (typ_aux, _)) =
- match typ_aux with
- | Typ_app (f, [Typ_arg_aux (Typ_arg_nexp n, _)])
- when string_of_id f = "atom" -> Some (n, n)
- | Typ_app (f, [Typ_arg_aux (Typ_arg_nexp n1, _); Typ_arg_aux (Typ_arg_nexp n2, _)])
- when string_of_id f = "range" -> Some (n1, n2)
- | _ -> None
-
let is_list (Typ_aux (typ_aux, _)) =
match typ_aux with
| Typ_app (f, [Typ_arg_aux (Typ_arg_typ typ, _)])
@@ -921,7 +913,7 @@ end = struct
rewrap (Typ_app (id, List.map aux_arg targs))
| Typ_id id when is_regtyp id env ->
let base, top, ranges = get_regtyp id env in
- let len = sub_big_int (abs_big_int (sub_big_int top base)) unit_big_int in
+ let len = succ_big_int (abs_big_int (sub_big_int top base)) in
vector_typ (nconstant base) (nconstant len) (get_default_order env) bit_typ
(* TODO registers with non-default order? non-bitvector registers? *)
| t -> rewrap t
@@ -1808,34 +1800,30 @@ let destruct_atom (Typ_aux (typ_aux, _)) =
exception Not_a_constraint;;
-let rec assert_nexp env exp =
- match destruct_atom_nexp env (typ_of exp) with
- | Some nexp -> nexp
- | None -> raise Not_a_constraint
+let rec assert_nexp env exp = destruct_atom_nexp env (typ_of exp)
let rec assert_constraint env (E_aux (exp_aux, _) as exp) =
match exp_aux with
+ | E_constraint nc ->
+ Some nc
| E_app (op, [x; y]) when string_of_id op = "or_bool" ->
- nc_or (assert_constraint env x) (assert_constraint env y)
+ option_binop nc_or (assert_constraint env x) (assert_constraint env y)
| E_app (op, [x; y]) when string_of_id op = "and_bool" ->
- nc_and (assert_constraint env x) (assert_constraint env y)
+ option_binop nc_and (assert_constraint env x) (assert_constraint env y)
| E_app (op, [x; y]) when string_of_id op = "gteq_atom" ->
- nc_gteq (assert_nexp env x) (assert_nexp env y)
+ option_binop nc_gteq (assert_nexp env x) (assert_nexp env y)
| E_app (op, [x; y]) when string_of_id op = "lteq_atom" ->
- nc_lteq (assert_nexp env x) (assert_nexp env y)
+ option_binop nc_lteq (assert_nexp env x) (assert_nexp env y)
| E_app (op, [x; y]) when string_of_id op = "gt_atom" ->
- nc_gt (assert_nexp env x) (assert_nexp env y)
+ option_binop nc_gt (assert_nexp env x) (assert_nexp env y)
| E_app (op, [x; y]) when string_of_id op = "lt_atom" ->
- nc_lt (assert_nexp env x) (assert_nexp env y)
+ option_binop nc_lt (assert_nexp env x) (assert_nexp env y)
| E_app (op, [x; y]) when string_of_id op = "eq_atom" ->
- nc_eq (assert_nexp env x) (assert_nexp env y)
+ option_binop nc_eq (assert_nexp env x) (assert_nexp env y)
| E_app (op, [x; y]) when string_of_id op = "neq_atom" ->
- nc_neq (assert_nexp env x) (assert_nexp env y)
+ option_binop nc_neq (assert_nexp env x) (assert_nexp env y)
| _ ->
- begin
- typ_debug ("Unable to construct a constraint for expression " ^ string_of_exp exp);
- raise Not_a_constraint
- end
+ None
type flow_constraint =
| Flow_lteq of big_int * nexp
@@ -1907,7 +1895,7 @@ let rec infer_flow env (E_aux (exp_aux, (l, _)) as exp) =
| Some (c, nexp) -> [(v, Flow_gteq (c, nexp))], []
| _ -> [], []
end
- | _ -> try [], [assert_constraint env exp] with Not_a_constraint -> [], []
+ | _ -> [], option_these [assert_constraint env exp]
let rec add_flows b flows env =
match flows with
@@ -2000,26 +1988,17 @@ let rec check_exp env (E_aux (exp_aux, (l, ())) as exp : unit exp) (Typ_aux (typ
| (E_aux (E_assign (lexp, bind), _) :: exps) ->
let texp, env = bind_assignment env lexp bind in
texp :: check_block l env exps typ
- | ((E_aux (E_assert (E_aux (E_constraint nc, _), assert_msg), _) as exp) :: exps) ->
- typ_print ("Adding constraint " ^ string_of_n_constraint nc ^ " for assert");
- let inferred_exp = irule infer_exp env exp in
- add_effect inferred_exp (mk_effect [BE_escape]) :: check_block l (Env.add_constraint nc env) exps typ
| ((E_aux (E_assert (constr_exp, assert_msg), _) as exp) :: exps) ->
- begin
- try
- let constr_exp = crule check_exp env constr_exp bool_typ in
- let nc = assert_constraint env constr_exp in
- let cexp = annot_exp (E_constraint nc) bool_typ in
- let checked_msg = crule check_exp env assert_msg string_typ in
- let texp = annot_exp_effect (E_assert (cexp, checked_msg)) unit_typ (mk_effect [BE_escape]) in
- texp :: check_block l (Env.add_constraint nc env) exps typ
- with
- | Not_a_constraint ->
- let constr_exp = crule check_exp env constr_exp bool_typ in
- let checked_msg = crule check_exp env assert_msg string_typ in
- let texp = annot_exp_effect (E_assert (constr_exp, checked_msg)) unit_typ (mk_effect [BE_escape]) in
- texp :: check_block l env exps typ
- end
+ let constr_exp = crule check_exp env constr_exp bool_typ in
+ let checked_msg = crule check_exp env assert_msg string_typ in
+ let cexp, env = match assert_constraint env constr_exp with
+ | Some nc ->
+ typ_print ("Adding constraint " ^ string_of_n_constraint nc ^ " for assert");
+ annot_exp (E_constraint nc) bool_typ, Env.add_constraint nc env
+ | None ->
+ constr_exp, env in
+ let texp = annot_exp_effect (E_assert (cexp, checked_msg)) unit_typ (mk_effect [BE_escape]) in
+ texp :: check_block l env exps typ
| (exp :: exps) ->
let texp = crule check_exp env exp (mk_typ (Typ_id (mk_id "unit"))) in
texp :: check_block l env exps typ
@@ -2163,6 +2142,27 @@ let rec check_exp env (E_aux (exp_aux, (l, ())) as exp : unit exp) (Typ_aux (typ
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_internal_return exp, _ ->
+ let checked_exp = crule check_exp env exp typ in
+ annot_exp (E_internal_return checked_exp) typ
+ | E_internal_plet (pat, bind, body), _ ->
+ let bind_exp, ptyp = match pat with
+ | P_aux (P_typ (ptyp, _), _) ->
+ Env.wf_typ env ptyp;
+ let checked_bind = crule check_exp env bind ptyp in
+ checked_bind, ptyp
+ | _ ->
+ let inferred_bind = irule infer_exp env bind in
+ inferred_bind, typ_of inferred_bind in
+ let tpat, env = bind_pat env pat ptyp in
+ (* Propagate constraint assertions on the lhs of monadic binds to the rhs *)
+ let env = match bind_exp with
+ | E_aux (E_assert (E_aux (E_constraint nc, _), _), _) ->
+ typ_print ("Adding constraint " ^ string_of_n_constraint nc ^ " for assert");
+ Env.add_constraint nc env
+ | _ -> env in
+ let checked_body = crule check_exp env body typ in
+ annot_exp (E_internal_plet (tpat, bind_exp, checked_body)) typ
| E_vector vec, _ ->
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
@@ -2785,7 +2785,7 @@ and infer_exp env (E_aux (exp_aux, (l, ())) as exp) =
let inferred_f = irule infer_exp env f in
let inferred_t = irule infer_exp env t in
let checked_step = crule check_exp env step int_typ in
- match is_range (typ_of inferred_f), is_range (typ_of inferred_t) with
+ match destruct_range (typ_of inferred_f), destruct_range (typ_of inferred_t) with
| None, _ -> typ_error l ("Type of " ^ string_of_exp f ^ " in foreach must be a range")
| _, None -> typ_error l ("Type of " ^ string_of_exp t ^ " in foreach must be a range")
(* | Some (l1, l2), Some (u1, u2) when prove env (nc_lteq l2 u1) ->
@@ -2842,6 +2842,39 @@ and infer_exp env (E_aux (exp_aux, (l, ())) as exp) =
let checked_test = crule check_exp env test bool_typ in
let checked_msg = crule check_exp env msg string_typ in
annot_exp_effect (E_assert (checked_test, checked_msg)) unit_typ (mk_effect [BE_escape])
+ | E_internal_return exp ->
+ let inferred_exp = irule infer_exp env exp in
+ annot_exp (E_internal_return inferred_exp) (typ_of inferred_exp)
+ | E_internal_plet (pat, bind, body) ->
+ let bind_exp, ptyp = match pat with
+ | P_aux (P_typ (ptyp, _), _) ->
+ Env.wf_typ env ptyp;
+ let checked_bind = crule check_exp env bind ptyp in
+ checked_bind, ptyp
+ | _ ->
+ let inferred_bind = irule infer_exp env bind in
+ inferred_bind, typ_of inferred_bind in
+ let tpat, env = bind_pat env pat ptyp in
+ (* Propagate constraint assertions on the lhs of monadic binds to the rhs *)
+ let env = match bind_exp with
+ | E_aux (E_assert (E_aux (E_constraint nc, _), _), _) ->
+ typ_print ("Adding constraint " ^ string_of_n_constraint nc ^ " for assert");
+ Env.add_constraint nc env
+ | _ -> env in
+ let inferred_body = irule infer_exp env body in
+ annot_exp (E_internal_plet (tpat, bind_exp, inferred_body)) (typ_of inferred_body)
+ | E_let (LB_aux (letbind, (let_loc, _)), exp) ->
+ let bind_exp, pat, ptyp = match letbind with
+ | LB_val (P_aux (P_typ (ptyp, _), _) as pat, bind) ->
+ Env.wf_typ env ptyp;
+ let checked_bind = crule check_exp env bind ptyp in
+ checked_bind, pat, ptyp
+ | LB_val (pat, bind) ->
+ let inferred_bind = irule infer_exp env bind in
+ inferred_bind, pat, typ_of inferred_bind in
+ let tpat, env = bind_pat env pat ptyp in
+ let inferred_exp = irule infer_exp env exp in
+ annot_exp (E_let (LB_aux (LB_val (tpat, bind_exp), (let_loc, None)), inferred_exp)) (typ_of inferred_exp)
| _ -> typ_error l ("Cannot infer type of: " ^ string_of_exp exp)
and infer_funapp l env f xs ret_ctx_typ = fst (infer_funapp' l env f (Env.get_val_spec f env) xs ret_ctx_typ)
@@ -3496,7 +3529,7 @@ let check_typedef env (TD_aux (tdef, (l, _))) =
[DEF_type (TD_aux (tdef, (l, None)))], env
| TD_enum(id, nmscm, ids, _) ->
[DEF_type (TD_aux (tdef, (l, None)))], Env.add_enum id ids env
- | TD_register(id, base, top, ranges) -> [DEF_type (TD_aux (tdef, (l, None)))], check_register env id base top ranges
+ | TD_register(id, base, top, ranges) -> [DEF_type (TD_aux (tdef, (l, Some (env, unit_typ, no_effect))))], check_register env id base top ranges
let check_kinddef env (KD_aux (kdef, (l, _))) =
let kd_err () = raise (Reporting_basic.err_unreachable Parse_ast.Unknown "Unimplemented kind def") in
@@ -3513,6 +3546,13 @@ let rec check_def env def =
| DEF_type tdef -> check_typedef env tdef
| DEF_fixity (prec, n, op) -> [DEF_fixity (prec, n, op)], env
| DEF_fundef fdef -> check_fundef env fdef
+ | DEF_internal_mutrec fdefs ->
+ let defs = List.concat (List.map (fun fdef -> fst (check_fundef env fdef)) fdefs) in
+ let split_fundef (defs, fdefs) def = match def with
+ | DEF_fundef fdef -> (defs, fdefs @ [fdef])
+ | _ -> (defs @ [def], fdefs) in
+ let (defs, fdefs) = List.fold_left split_fundef ([], []) defs in
+ (defs @ [DEF_internal_mutrec fdefs]), env
| DEF_val letdef -> check_letdef env letdef
| DEF_spec vs -> check_val_spec env vs
| DEF_default default -> check_default env default
diff --git a/src/type_check.mli b/src/type_check.mli
index 99385b31..5ed55843 100644
--- a/src/type_check.mli
+++ b/src/type_check.mli
@@ -195,6 +195,8 @@ val prove : Env.t -> n_constraint -> bool
val subtype_check : Env.t -> typ -> typ -> bool
+val bind_pat : Env.t -> unit pat -> typ -> tannot pat * Env.t
+
(* Partial functions: The expressions and patterns passed to these
functions must be guaranteed to have tannots of the form Some (env,
typ) for these to work. *)
diff --git a/src/util.mli b/src/util.mli
index 38af1fc2..ac87cab8 100644
--- a/src/util.mli
+++ b/src/util.mli
@@ -84,7 +84,7 @@ val option_default : 'a -> 'a option -> 'a
(** [option_binop f (Some x) (Some y)] returns [Some (f x y)],
and in all other cases, [option_binop] returns [None]. *)
-val option_binop : ('a -> 'a -> 'a) -> 'a option -> 'a option -> 'a option
+val option_binop : ('a -> 'a -> 'b) -> 'a option -> 'a option -> 'b option
(** [option_get_exn exn None] throws the exception [exn],
whereas [option_get_exn exn (Some x)] returns [x]. *)
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-09 23:00:13 +0000