summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/monomorphise.ml5
-rw-r--r--src/pretty_print.mli2
-rw-r--r--src/pretty_print_lem.ml327
-rw-r--r--src/process_file.ml14
-rw-r--r--src/process_file.mli2
-rw-r--r--src/sail.ml4
6 files changed, 176 insertions, 178 deletions
diff --git a/src/monomorphise.ml b/src/monomorphise.ml
index 8e254e9f..8730b019 100644
--- a/src/monomorphise.ml
+++ b/src/monomorphise.ml
@@ -1691,11 +1691,10 @@ let rewrite_size_parameters env (Defs defs) =
let sizes_funcl fsizes (FCL_aux (FCL_Funcl (id,pexp),(l,_))) =
let sizes = size_vars pexp in
let pat,guard,exp,pannot = destruct_pexp pexp in
- (* TODO: what, if anything, should sequential be? *)
let visible_tyvars =
KidSet.union
- (Pretty_print_lem.lem_tyvars_of_typ false true (pat_typ_of pat))
- (Pretty_print_lem.lem_tyvars_of_typ false true (typ_of exp))
+ (Pretty_print_lem.lem_tyvars_of_typ (pat_typ_of pat))
+ (Pretty_print_lem.lem_tyvars_of_typ (typ_of exp))
in
let expose_tyvars = KidSet.diff sizes visible_tyvars in
let parameters = match pat with
diff --git a/src/pretty_print.mli b/src/pretty_print.mli
index d411815f..c01e0b93 100644
--- a/src/pretty_print.mli
+++ b/src/pretty_print.mli
@@ -58,4 +58,4 @@ val pat_to_string : 'a pat -> string
(* Prints on formatter the defs as Lem Ast nodes *)
val pp_lem_defs : Format.formatter -> tannot defs -> unit
-val pp_defs_lem : bool -> bool -> (out_channel * string list) -> (out_channel * string list) -> tannot defs -> string -> unit
+val pp_defs_lem : (out_channel * string list) -> (out_channel * string list) -> tannot defs -> string -> unit
diff --git a/src/pretty_print_lem.ml b/src/pretty_print_lem.ml
index c76be843..48eed31a 100644
--- a/src/pretty_print_lem.ml
+++ b/src/pretty_print_lem.ml
@@ -60,6 +60,9 @@ open Pretty_print_common
* PPrint-based sail-to-lem pprinter
****************************************************************************)
+let opt_sequential = ref false
+let opt_mwords = ref false
+
let print_to_from_interp_value = ref false
let langlebar = string "<|"
let ranglebar = string "|>"
@@ -195,8 +198,8 @@ let rec orig_nexp (Nexp_aux (nexp, l)) =
(* Returns the set of type variables that will appear in the Lem output,
which may be smaller than those in the Sail type. May need to be
updated with doc_typ_lem *)
-let rec lem_nexps_of_typ sequential mwords (Typ_aux (t,_)) =
- let trec = lem_nexps_of_typ sequential mwords in
+let rec lem_nexps_of_typ (Typ_aux (t,_)) =
+ let trec = lem_nexps_of_typ in
match t with
| Typ_id _ -> NexpSet.empty
| Typ_var kid -> NexpSet.singleton (orig_nexp (nvar kid))
@@ -210,75 +213,75 @@ let rec lem_nexps_of_typ sequential mwords (Typ_aux (t,_)) =
Typ_arg_aux (Typ_arg_order ord, _);
Typ_arg_aux (Typ_arg_typ elem_typ, _)]) ->
let m = nexp_simp m in
- if mwords && is_bit_typ elem_typ && not (is_nexp_constant m) then
+ if !opt_mwords && is_bit_typ elem_typ && not (is_nexp_constant m) then
NexpSet.singleton (orig_nexp m)
else trec elem_typ
(* NexpSet.union
- (if mwords then tyvars_of_nexp (nexp_simp m) else NexpSet.empty)
+ (if !opt_mwords then tyvars_of_nexp (nexp_simp m) else NexpSet.empty)
(trec elem_typ) *)
| Typ_app(Id_aux (Id "register", _), [Typ_arg_aux (Typ_arg_typ etyp, _)]) ->
- if sequential then trec etyp else NexpSet.empty
+ if !opt_sequential then trec etyp else NexpSet.empty
| Typ_app(Id_aux (Id "range", _),_)
| Typ_app(Id_aux (Id "implicit", _),_)
| Typ_app(Id_aux (Id "atom", _), _) -> NexpSet.empty
| Typ_app (_,tas) ->
- List.fold_left (fun s ta -> NexpSet.union s (lem_nexps_of_typ_arg sequential mwords ta))
+ List.fold_left (fun s ta -> NexpSet.union s (lem_nexps_of_typ_arg ta))
NexpSet.empty tas
| Typ_exist (kids,_,t) ->
let s = trec t in
List.fold_left (fun s k -> NexpSet.remove k s) s (List.map nvar kids)
-and lem_nexps_of_typ_arg sequential mwords (Typ_arg_aux (ta,_)) =
+and lem_nexps_of_typ_arg (Typ_arg_aux (ta,_)) =
match ta with
| Typ_arg_nexp nexp -> NexpSet.singleton (nexp_simp (orig_nexp nexp))
- | Typ_arg_typ typ -> lem_nexps_of_typ sequential mwords typ
+ | Typ_arg_typ typ -> lem_nexps_of_typ typ
| Typ_arg_order _ -> NexpSet.empty
-let lem_tyvars_of_typ sequential mwords typ =
+let lem_tyvars_of_typ typ =
NexpSet.fold (fun nexp ks -> KidSet.union ks (tyvars_of_nexp nexp))
- (lem_nexps_of_typ sequential mwords typ) KidSet.empty
+ (lem_nexps_of_typ typ) KidSet.empty
(* When making changes here, check whether they affect lem_tyvars_of_typ *)
let doc_typ_lem, doc_atomic_typ_lem =
(* following the structure of parser for precedence *)
- let rec typ sequential mwords ty = fn_typ sequential mwords true ty
- and typ' sequential mwords ty = fn_typ sequential mwords false ty
- and fn_typ (sequential : bool) (mwords : bool) atyp_needed ((Typ_aux (t, _)) as ty) = match t with
+ let rec typ ty = fn_typ true ty
+ and typ' ty = fn_typ false ty
+ and fn_typ atyp_needed ((Typ_aux (t, _)) as ty) = match t with
| Typ_fn(arg,ret,efct) ->
(*let exc_typ = string "string" in*)
let ret_typ =
if effectful efct
- then separate space [string "_M";(*parens exc_typ;*) fn_typ sequential mwords true ret]
- else separate space [fn_typ sequential mwords false ret] in
- let tpp = separate space [tup_typ sequential mwords true arg; arrow;ret_typ] in
+ then separate space [string "_M";(*parens exc_typ;*) fn_typ true ret]
+ else separate space [fn_typ false ret] in
+ let tpp = separate space [tup_typ true arg; arrow;ret_typ] in
(* once we have proper excetions we need to know what the exceptions type is *)
if atyp_needed then parens tpp else tpp
- | _ -> tup_typ sequential mwords atyp_needed ty
- and tup_typ sequential mwords atyp_needed ((Typ_aux (t, _)) as ty) = match t with
+ | _ -> tup_typ atyp_needed ty
+ and tup_typ atyp_needed ((Typ_aux (t, _)) as ty) = match t with
| Typ_tup typs ->
- 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
+ parens (separate_map (space ^^ star ^^ space) (app_typ false) typs)
+ | _ -> app_typ atyp_needed ty
+ and app_typ atyp_needed ((Typ_aux (t, l)) as ty) = match t with
| Typ_app(Id_aux (Id "vector", _), [
Typ_arg_aux (Typ_arg_nexp n, _);
Typ_arg_aux (Typ_arg_nexp m, _);
Typ_arg_aux (Typ_arg_order ord, _);
Typ_arg_aux (Typ_arg_typ elem_typ, _)]) ->
let tpp = match elem_typ with
- | Typ_aux (Typ_id (Id_aux (Id "bit",_)),_) when mwords ->
+ | Typ_aux (Typ_id (Id_aux (Id "bit",_)),_) when !opt_mwords ->
string "bitvector " ^^ doc_nexp_lem (nexp_simp m)
(* (match nexp_simp m with
| (Nexp_aux(Nexp_constant i,_)) -> string "bitvector ty" ^^ doc_int i
| (Nexp_aux(Nexp_var _, _)) -> separate space [string "bitvector"; doc_nexp m]
| _ -> raise (Reporting_basic.err_unreachable l
"cannot pretty-print bitvector type with non-constant length")) *)
- | _ -> string "vector" ^^ space ^^ typ sequential mwords elem_typ in
+ | _ -> string "vector" ^^ space ^^ typ elem_typ in
if atyp_needed then parens tpp else tpp
| Typ_app(Id_aux (Id "register", _), [Typ_arg_aux (Typ_arg_typ etyp, _)]) ->
(* TODO: Better distinguish register names and contents? *)
(* fn_typ regtypes atyp_needed etyp *)
let tpp =
- if sequential
- then string "register_ref regstate " ^^ typ sequential mwords etyp
+ if !opt_sequential
+ then string "register_ref regstate " ^^ typ etyp
else string "register" in
if atyp_needed then parens tpp else tpp
| Typ_app(Id_aux (Id "range", _),_) ->
@@ -288,10 +291,10 @@ let doc_typ_lem, doc_atomic_typ_lem =
| Typ_app(Id_aux (Id "atom", _), [Typ_arg_aux(Typ_arg_nexp n,_)]) ->
(string "integer")
| Typ_app(id,args) ->
- let tpp = (doc_id_lem_type id) ^^ space ^^ (separate_map space (doc_typ_arg_lem sequential mwords) args) in
+ let tpp = (doc_id_lem_type id) ^^ space ^^ (separate_map space doc_typ_arg_lem args) in
if atyp_needed then parens tpp else tpp
- | _ -> atomic_typ sequential mwords atyp_needed ty
- and atomic_typ sequential mwords atyp_needed ((Typ_aux (t, l)) as ty) = match t with
+ | _ -> atomic_typ atyp_needed ty
+ and atomic_typ atyp_needed ((Typ_aux (t, l)) as ty) = match t with
| Typ_id (Id_aux (Id "bool",_)) -> string "bool"
| Typ_id (Id_aux (Id "bit",_)) -> string "bitU"
| Typ_id (id) ->
@@ -302,11 +305,11 @@ let doc_typ_lem, doc_atomic_typ_lem =
| Typ_app _ | Typ_tup _ | Typ_fn _ ->
(* exhaustiveness matters here to avoid infinite loops
* if we add a new Typ constructor *)
- let tpp = typ sequential mwords ty in
+ let tpp = typ ty in
if atyp_needed then parens tpp else tpp
| Typ_exist (kids,_,ty) -> begin
- let tpp = typ sequential mwords ty in
- let visible_vars = lem_tyvars_of_typ sequential mwords ty in
+ let tpp = typ ty in
+ let visible_vars = lem_tyvars_of_typ ty in
match List.filter (fun kid -> KidSet.mem kid visible_vars) kids with
| [] -> if atyp_needed then parens tpp else tpp
| bad -> raise (Reporting_basic.err_general l
@@ -314,8 +317,8 @@ let doc_typ_lem, doc_atomic_typ_lem =
String.concat ", " (List.map string_of_kid bad) ^
" escape into Lem"))
end
- and doc_typ_arg_lem sequential mwords (Typ_arg_aux(t,_)) = match t with
- | Typ_arg_typ t -> app_typ sequential mwords true t
+ and doc_typ_arg_lem (Typ_arg_aux(t,_)) = match t with
+ | Typ_arg_typ t -> app_typ true t
| Typ_arg_nexp n -> doc_nexp_lem (nexp_simp n)
| Typ_arg_order o -> empty
in typ', atomic_typ
@@ -325,36 +328,37 @@ let doc_typ_lem, doc_atomic_typ_lem =
length argument are checked for variables, and the latter only if it is
a bitvector; for other types of vectors, the length is not pretty-printed
in the type, and the start index is never pretty-printed in vector types. *)
-let rec contains_t_pp_var mwords (Typ_aux (t,a) as typ) = match t with
+let rec contains_t_pp_var (Typ_aux (t,a) as typ) = match t with
| Typ_id _ -> false
| Typ_var _ -> true
| Typ_exist _ -> true
- | Typ_fn (t1,t2,_) -> contains_t_pp_var mwords t1 || contains_t_pp_var mwords t2
- | Typ_tup ts -> List.exists (contains_t_pp_var mwords) ts
+ | Typ_fn (t1,t2,_) -> contains_t_pp_var t1 || contains_t_pp_var t2
+ | Typ_tup ts -> List.exists contains_t_pp_var ts
| Typ_app (c,targs) ->
if Ast_util.is_number typ then false
else if is_bitvector_typ typ then
let (_,length,_,_) = vector_typ_args_of typ in
let length = nexp_simp length in
not (is_nexp_constant length ||
- (mwords && match length with Nexp_aux (Nexp_var _,_) -> true | _ -> false))
- else List.exists (contains_t_arg_pp_var mwords) targs
-and contains_t_arg_pp_var mwords (Typ_arg_aux (targ, _)) = match targ with
- | Typ_arg_typ t -> contains_t_pp_var mwords t
+ (!opt_mwords &&
+ match length with Nexp_aux (Nexp_var _,_) -> true | _ -> false))
+ else List.exists contains_t_arg_pp_var targs
+and contains_t_arg_pp_var (Typ_arg_aux (targ, _)) = match targ with
+ | Typ_arg_typ t -> contains_t_pp_var t
| Typ_arg_nexp nexp -> not (is_nexp_constant (nexp_simp nexp))
| _ -> false
-let doc_tannot_lem sequential mwords eff typ =
- if contains_t_pp_var mwords typ then empty
+let doc_tannot_lem eff typ =
+ if contains_t_pp_var typ then empty
else
- let ta = doc_typ_lem sequential mwords typ in
+ let ta = doc_typ_lem typ in
if eff then string " : _M " ^^ parens ta
else string " : " ^^ ta
(* doc_lit_lem gets as an additional parameter the type information from the
* expression around it: that's a hack, but how else can we distinguish between
* undefined values of different types ? *)
-let doc_lit_lem sequential mwords in_pat (L_aux(lit,l)) a =
+let doc_lit_lem in_pat (L_aux(lit,l)) a =
match lit with
| L_unit -> utf8string "()"
| L_zero -> utf8string "B0"
@@ -377,8 +381,8 @@ let doc_lit_lem sequential mwords in_pat (L_aux(lit,l)) a =
| Typ_app (Id_aux (Id "register", _),_) -> utf8string "UndefinedRegister 0"
| Typ_id (Id_aux (Id "string", _)) -> utf8string "\"\""
| _ ->
- let ta = if contains_t_pp_var mwords typ then empty
- else doc_tannot_lem sequential mwords false typ in
+ let ta = if contains_t_pp_var typ then empty
+ else doc_tannot_lem false typ in
parens
((utf8string "(failwith \"undefined value of unsupported type\")") ^^ ta))
| _ -> utf8string "(failwith \"undefined value of unsupported type\")")
@@ -442,19 +446,19 @@ let rec typeclass_nexps (Typ_aux(t,_)) = match t with
| Typ_app _ -> NexpSet.empty
| Typ_exist (kids,_,t) -> NexpSet.empty (* todo *)
-let doc_typclasses_lem mwords t =
- if mwords then
+let doc_typclasses_lem t =
+ if !opt_mwords then
let nexps = typeclass_nexps t in
if NexpSet.is_empty nexps then (empty, NexpSet.empty) else
(separate_map comma_sp (fun nexp -> string "Size " ^^ doc_nexp_lem nexp) (NexpSet.elements nexps) ^^ string " => ", nexps)
else (empty, NexpSet.empty)
-let doc_typschm_lem sequential mwords quants (TypSchm_aux(TypSchm_ts(tq,t),_)) =
- let pt = doc_typ_lem sequential mwords t in
+let doc_typschm_lem quants (TypSchm_aux(TypSchm_ts(tq,t),_)) =
+ let pt = doc_typ_lem t in
if quants
then
- let nexps_used = lem_nexps_of_typ sequential mwords t in
- let ptyc, nexps_sizes = doc_typclasses_lem mwords t in
+ let nexps_used = lem_nexps_of_typ t in
+ let ptyc, nexps_sizes = doc_typclasses_lem t in
let nexps_to_include = NexpSet.union nexps_used nexps_sizes in
if NexpSet.is_empty nexps_to_include
then pt
@@ -468,44 +472,44 @@ let is_ctor env id = match Env.lookup_id id env with
(*Note: vector concatenation, literal vectors, indexed vectors, and record should
be removed prior to pp. The latter two have never yet been seen
*)
-let rec doc_pat_lem sequential mwords apat_needed (P_aux (p,(l,annot)) as pa) = match p with
+let rec doc_pat_lem apat_needed (P_aux (p,(l,annot)) as pa) = match p with
| P_app(id, ((_ :: _) as pats)) ->
let ppp = doc_unop (doc_id_lem_ctor id)
- (parens (separate_map comma (doc_pat_lem sequential mwords true) pats)) in
+ (parens (separate_map comma (doc_pat_lem true) pats)) in
if apat_needed then parens ppp else ppp
| P_app(id,[]) -> doc_id_lem_ctor id
- | P_lit lit -> doc_lit_lem sequential mwords true lit annot
+ | P_lit lit -> doc_lit_lem true lit annot
| P_wild -> underscore
| P_id id ->
begin match id with
| Id_aux (Id "None",_) -> string "Nothing" (* workaround temporary issue *)
| _ -> 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_var(p,kid) -> doc_pat_lem true p
+ | P_as(p,id) -> parens (separate space [doc_pat_lem 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
+ doc_pat_lem 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
- else parens (doc_op colon doc_p (doc_typ_lem sequential mwords typ))
+ let doc_p = doc_pat_lem true p in
+ if contains_t_pp_var typ then doc_p
+ else parens (doc_op colon doc_p (doc_typ_lem typ))
| P_vector pats ->
let ppp =
(separate space)
- [string "Vector";brackets (separate_map semi (doc_pat_lem sequential mwords true) pats);underscore;underscore] in
+ [string "Vector";brackets (separate_map semi (doc_pat_lem true) pats);underscore;underscore] in
if apat_needed then parens ppp else ppp
| P_vector_concat pats ->
raise (Reporting_basic.err_unreachable l
"vector concatenation patterns should have been removed before pretty-printing")
| P_tup pats ->
(match pats with
- | [p] -> doc_pat_lem sequential mwords apat_needed p
- | _ -> parens (separate_map comma_sp (doc_pat_lem sequential mwords false) pats))
- | P_list pats -> brackets (separate_map semi (doc_pat_lem sequential mwords false) pats) (*Never seen but easy in lem*)
- | P_cons (p,p') -> doc_op (string "::") (doc_pat_lem sequential mwords true p) (doc_pat_lem sequential mwords true p')
+ | [p] -> doc_pat_lem apat_needed p
+ | _ -> parens (separate_map comma_sp (doc_pat_lem false) pats))
+ | P_list pats -> brackets (separate_map semi (doc_pat_lem false) pats) (*Never seen but easy in lem*)
+ | P_cons (p,p') -> doc_op (string "::") (doc_pat_lem true p) (doc_pat_lem true p')
| P_record (_,_) -> empty (* TODO *)
let rec typ_needs_printed (Typ_aux (t,_) as typ) = match t with
@@ -537,11 +541,11 @@ let typ_id_of (Typ_aux (typ, l)) = match typ with
let prefix_recordtype = true
let report = Reporting_basic.err_unreachable
let doc_exp_lem, doc_let_lem =
- let rec top_exp sequential mwords (early_ret : bool) (aexp_needed : bool)
+ let rec top_exp (early_ret : bool) (aexp_needed : bool)
(E_aux (e, (l,annot)) as full_exp) =
- let expY = top_exp sequential mwords early_ret true in
- let expN = top_exp sequential mwords early_ret false in
- let expV = top_exp sequential mwords early_ret in
+ let expY = top_exp early_ret true in
+ let expN = top_exp early_ret false in
+ let expV = top_exp early_ret in
let liftR doc =
if early_ret && effectful (effect_of full_exp)
then separate space [string "liftR"; parens (doc)]
@@ -563,10 +567,10 @@ let doc_exp_lem, doc_let_lem =
doc_id_lem id in
liftR ((prefix 2 1)
(string "write_reg_field_range")
- (align (doc_lexp_deref_lem sequential mwords early_ret le ^/^
+ (align (doc_lexp_deref_lem early_ret le ^/^
field_ref ^/^ expY e2 ^/^ expY e3 ^/^ expY e)))
| _ ->
- let deref = doc_lexp_deref_lem sequential mwords early_ret le in
+ let deref = doc_lexp_deref_lem early_ret le in
liftR ((prefix 2 1)
(string "write_reg_range")
(align (deref ^/^ expY e2 ^/^ expY e3) ^/^ expY e)))
@@ -583,10 +587,10 @@ let doc_exp_lem, doc_let_lem =
let call = if is_bitvector_typ (Env.base_typ_of (env_of full_exp) (typ_of_annot fannot)) then "write_reg_field_bit" else "write_reg_field_pos" in
liftR ((prefix 2 1)
(string call)
- (align (doc_lexp_deref_lem sequential mwords early_ret le ^/^
+ (align (doc_lexp_deref_lem early_ret le ^/^
field_ref ^/^ expY e2 ^/^ expY e)))
| LEXP_aux (_, lannot) ->
- let deref = doc_lexp_deref_lem sequential mwords early_ret le in
+ let deref = doc_lexp_deref_lem 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))
@@ -600,10 +604,10 @@ let doc_exp_lem, doc_let_lem =
string "set_field"*) in
liftR ((prefix 2 1)
(string "write_reg_field")
- (doc_lexp_deref_lem sequential mwords early_ret le ^^ space ^^
+ (doc_lexp_deref_lem early_ret le ^^ space ^^
field_ref ^/^ expY e))
| _ ->
- liftR ((prefix 2 1) (string "write_reg") (doc_lexp_deref_lem sequential mwords early_ret le ^/^ expY e)))
+ liftR ((prefix 2 1) (string "write_reg") (doc_lexp_deref_lem 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")
@@ -619,7 +623,7 @@ let doc_exp_lem, doc_let_lem =
| E_for(id,exp1,exp2,exp3,(Ord_aux(order,_)),exp4) ->
raise (report l "E_for should have been removed till now")
| E_let(leb,e) ->
- let epp = let_exp sequential mwords early_ret leb ^^ space ^^ string "in" ^^ hardline ^^ expN e in
+ let epp = let_exp early_ret leb ^^ space ^^ string "in" ^^ hardline ^^ expN e in
if aexp_needed then parens epp else epp
| E_app(f,args) ->
begin match f with
@@ -674,13 +678,13 @@ let doc_exp_lem, doc_let_lem =
| [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
+ if contains_t_pp_var (typ_of exp) ||
+ contains_t_pp_var (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
+ doc_atomic_typ_lem false (typ_of full_exp);
+ doc_atomic_typ_lem 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
@@ -710,7 +714,7 @@ let doc_exp_lem, doc_let_lem =
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 (Env.base_typ_of (env_of full_exp) t)
- then (align epp ^^ (doc_tannot_lem sequential mwords (effectful eff) t), true)
+ then (align epp ^^ (doc_tannot_lem (effectful eff) t), true)
else (epp, aexp_needed) in
liftR (if aexp_needed then parens (align taepp) else taepp)
end
@@ -732,7 +736,7 @@ let doc_exp_lem, doc_let_lem =
let field_f = doc_id_lem tid ^^ underscore ^^ doc_id_lem id ^^ dot ^^ string "get_field" in
let (ta,aexp_needed) =
if typ_needs_printed t
- then (doc_tannot_lem sequential mwords (effectful eff) t, true)
+ then (doc_tannot_lem (effectful eff) t, true)
else (empty, aexp_needed) in
let epp = field_f ^^ space ^^ (expY fexp) in
if aexp_needed then parens (align epp ^^ ta) else (epp ^^ ta)
@@ -755,11 +759,11 @@ let doc_exp_lem, doc_let_lem =
if has_effect eff BE_rreg then
let epp = separate space [string "read_reg";doc_id_lem id] in
if is_bitvector_typ base_typ
- then liftR (parens (epp ^^ doc_tannot_lem sequential mwords true base_typ))
+ then liftR (parens (epp ^^ doc_tannot_lem true base_typ))
else liftR epp
else if is_ctor env id then doc_id_lem_ctor id
else doc_id_lem id
- | E_lit lit -> doc_lit_lem sequential mwords false lit annot
+ | E_lit lit -> doc_lit_lem false lit annot
| E_cast(typ,e) ->
expV aexp_needed e
| E_tuple exps ->
@@ -773,7 +777,7 @@ let doc_exp_lem, doc_let_lem =
| _ -> raise (report l ("cannot get record type from annot " ^ string_of_annot annot ^ " of exp " ^ string_of_exp full_exp)) in
let epp = anglebars (space ^^ (align (separate_map
(semi_sp ^^ break 1)
- (doc_fexp sequential mwords early_ret recordtyp) fexps)) ^^ space) in
+ (doc_fexp early_ret recordtyp) fexps)) ^^ space) in
if aexp_needed then parens epp else epp
| E_record_update(e,(FES_aux(FES_Fexps(fexps,_),_))) ->
let recordtyp = match annot with
@@ -782,7 +786,7 @@ let doc_exp_lem, doc_let_lem =
when Env.is_record tid env ->
tid
| _ -> raise (report l ("cannot get record type from annot " ^ string_of_annot annot ^ " of exp " ^ string_of_exp full_exp)) in
- anglebars (doc_op (string "with") (expY e) (separate_map semi_sp (doc_fexp sequential mwords early_ret recordtyp) fexps))
+ anglebars (doc_op (string "with") (expY e) (separate_map semi_sp (doc_fexp early_ret recordtyp) fexps))
| E_vector exps ->
let t = Env.base_typ_of (env_of full_exp) (typ_of full_exp) in
let (start, len, order, etyp) =
@@ -808,9 +812,9 @@ let doc_exp_lem, doc_let_lem =
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
+ if is_bit_typ etyp && !opt_mwords then
let bepp = string "vec_to_bvec" ^^ space ^^ parens (align epp) in
- (bepp ^^ doc_tannot_lem sequential mwords false t, true)
+ (bepp ^^ doc_tannot_lem false t, true)
else (epp,aexp_needed) in
if aexp_needed then parens (align epp) else epp
| E_vector_update(v,e1,e2) ->
@@ -841,7 +845,7 @@ let doc_exp_lem, doc_let_lem =
let epp =
group ((separate space [string "match"; only_integers e; string "with"]) ^/^
- (separate_map (break 1) (doc_case sequential mwords early_ret) pexps) ^/^
+ (separate_map (break 1) (doc_case early_ret) pexps) ^/^
(string "end")) in
if aexp_needed then parens (align epp) else align epp
| E_exit e -> liftR (separate space [string "exit"; expY e;])
@@ -861,67 +865,67 @@ let doc_exp_lem, doc_let_lem =
(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
+ doc_pat_lem 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]
| 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
+ | Nexp_aux (Nexp_constant i, _) -> doc_lit_lem false (L_aux (L_num i, l)) annot
| _ ->
raise (Reporting_basic.err_unreachable l
"pretty-printing non-constant sizeof expressions to Lem not supported"))
| E_return r ->
- let ret_monad = if sequential then " : MR regstate" else " : MR" in
+ let ret_monad = if !opt_sequential then " : MR regstate" else " : MR" in
let ta =
- if contains_t_pp_var mwords (typ_of full_exp) || contains_t_pp_var mwords (typ_of r)
+ if contains_t_pp_var (typ_of full_exp) || contains_t_pp_var (typ_of r)
then empty
else separate space
[string ret_monad;
- parens (doc_typ_lem sequential mwords (typ_of full_exp));
- parens (doc_typ_lem sequential mwords (typ_of r))] in
+ parens (doc_typ_lem (typ_of full_exp));
+ parens (doc_typ_lem (typ_of r))] in
align (parens (string "early_return" ^//^ expV true r ^//^ ta))
| 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")
- and let_exp sequential mwords early_ret (LB_aux(lb,_)) = match lb with
+ and let_exp early_ret (LB_aux(lb,_)) = match lb with
| LB_val(pat,e) ->
prefix 2 1
- (separate space [string "let"; doc_pat_lem sequential mwords true pat; equals])
- (top_exp sequential mwords early_ret false e)
+ (separate space [string "let"; doc_pat_lem true pat; equals])
+ (top_exp early_ret false e)
- and doc_fexp sequential mwords early_ret recordtyp (FE_aux(FE_Fexp(id,e),_)) =
+ and doc_fexp early_ret recordtyp (FE_aux(FE_Fexp(id,e),_)) =
let fname =
if prefix_recordtype
then (string (string_of_id recordtyp ^ "_")) ^^ doc_id_lem id
else doc_id_lem id in
- group (doc_op equals fname (top_exp sequential mwords early_ret true e))
+ group (doc_op equals fname (top_exp early_ret true e))
- and doc_case sequential mwords early_ret = function
+ and doc_case early_ret = function
| Pat_aux(Pat_exp(pat,e),_) ->
- group (prefix 3 1 (separate space [pipe; doc_pat_lem sequential mwords false pat;arrow])
- (group (top_exp sequential mwords early_ret false e)))
+ group (prefix 3 1 (separate space [pipe; doc_pat_lem false pat;arrow])
+ (group (top_exp early_ret false e)))
| Pat_aux(Pat_when(_,_,_),(l,_)) ->
raise (Reporting_basic.err_unreachable l
"guarded pattern expression should have been rewritten before pretty-printing")
- and doc_lexp_deref_lem sequential mwords early_ret ((LEXP_aux(lexp,(l,annot))) as le) = match lexp with
+ and doc_lexp_deref_lem 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])
+ parens (separate empty [doc_lexp_deref_lem early_ret le;dot;doc_id_lem id])
| 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)
+ | LEXP_tup lexps -> parens (separate_map comma_sp (doc_lexp_deref_lem early_ret) lexps)
| _ ->
raise (Reporting_basic.err_unreachable l ("doc_lexp_deref_lem: Unsupported lexp"))
(* expose doc_exp_lem and doc_let *)
in top_exp, let_exp
(*TODO Upcase and downcase type and constructors as needed*)
-let doc_type_union_lem sequential mwords (Tu_aux(typ_u,_)) = match typ_u with
+let doc_type_union_lem (Tu_aux(typ_u,_)) = match typ_u with
| Tu_ty_id(typ,id) -> separate space [pipe; doc_id_lem_ctor id; string "of";
- parens (doc_typ_lem sequential mwords typ)]
+ parens (doc_typ_lem typ)]
| Tu_id id -> separate space [pipe; doc_id_lem_ctor id]
let rec doc_range_lem (BF_aux(r,_)) = match r with
@@ -929,17 +933,17 @@ let rec doc_range_lem (BF_aux(r,_)) = match r with
| BF_range(i1,i2) -> parens (doc_op comma (doc_int i1) (doc_int i2))
| BF_concat(ir1,ir2) -> (doc_range ir1) ^^ comma ^^ (doc_range ir2)
-let doc_typdef_lem sequential mwords (TD_aux(td, (l, annot))) = match td with
+let doc_typdef_lem (TD_aux(td, (l, annot))) = match td with
| TD_abbrev(id,nm,(TypSchm_aux (TypSchm_ts (typq, _), _) as typschm)) ->
doc_op equals
(separate space [string "type"; doc_id_lem_type id; doc_typquant_items_lem None typq])
- (doc_typschm_lem sequential mwords false typschm)
+ (doc_typschm_lem false typschm)
| TD_record(id,nm,typq,fs,_) ->
let fname fid = if prefix_recordtype
then concat [doc_id_lem id;string "_";doc_id_lem_type fid;]
else doc_id_lem_type fid in
let f_pp (typ,fid) =
- concat [fname fid;space;colon;space;doc_typ_lem sequential mwords typ; semi] in
+ concat [fname fid;space;colon;space;doc_typ_lem typ; semi] in
let rectyp = match typq with
| TypQ_aux (TypQ_tq qs, _) ->
let quant_item = function
@@ -956,7 +960,7 @@ let doc_typdef_lem sequential mwords (TD_aux(td, (l, annot))) = match td with
mk_typ (Typ_app (Id_aux (Id "field_ref", Parse_ast.Unknown),
[mk_typ_arg (Typ_arg_typ rectyp);
mk_typ_arg (Typ_arg_typ ftyp)])) in
- let rfannot = doc_tannot_lem sequential mwords false reftyp in
+ let rfannot = doc_tannot_lem false reftyp in
let get, set =
string "rec_val" ^^ dot ^^ fname fid,
anglebars (space ^^ string "rec_val with " ^^
@@ -985,7 +989,7 @@ let doc_typdef_lem sequential mwords (TD_aux(td, (l, annot))) = match td with
doc_op equals
(separate space [string "type"; doc_id_lem_type id; doc_typquant_items_lem None typq])
((*doc_typquant_lem typq*) (anglebars (space ^^ align fs_doc ^^ space))) ^^ hardline ^^
- if sequential && string_of_id id = "regstate" then empty
+ if !opt_sequential && string_of_id id = "regstate" then empty
else separate_map hardline doc_field fs
| TD_variant(id,nm,typq,ar,_) ->
(match id with
@@ -999,7 +1003,7 @@ let doc_typdef_lem sequential mwords (TD_aux(td, (l, annot))) = match td with
| Id_aux ((Id "diafp"),_) -> empty *)
| Id_aux ((Id "option"),_) -> empty
| _ ->
- let ar_doc = group (separate_map (break 1) (doc_type_union_lem sequential mwords) ar) in
+ let ar_doc = group (separate_map (break 1) doc_type_union_lem ar) in
let typ_pp =
(doc_op equals)
(concat [string "type"; space; doc_id_lem_type id; space; doc_typquant_items_lem None typq])
@@ -1176,13 +1180,13 @@ let doc_typdef_lem sequential mwords (TD_aux(td, (l, annot))) = match td with
let ord = Ord_aux ((if dir_b then Ord_inc else Ord_dec), Parse_ast.Unknown) in
let size = if dir_b then add_big_int (sub_big_int i2 i1) unit_big_int else add_big_int (sub_big_int i1 i2) unit_big_int in
let vtyp = vector_typ (nconstant i1) (nconstant size) ord bit_typ in
- let tannot = doc_tannot_lem sequential mwords false vtyp in
+ let tannot = doc_tannot_lem false vtyp in
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
doc_op equals
(concat [string "type";space;doc_id_lem id])
- (doc_typ_lem sequential mwords vtyp)
+ (doc_typ_lem vtyp)
^^ hardline ^^
doc_op equals
(concat [string "let";space;string "cast_";doc_id_lem id;space;string "reg"])
@@ -1203,17 +1207,17 @@ let doc_rec_lem (Rec_aux(r,_)) = match r with
| Rec_nonrec -> space
| Rec_rec -> space ^^ string "rec" ^^ space
-let doc_tannot_opt_lem sequential mwords (Typ_annot_opt_aux(t,_)) = match t with
- | Typ_annot_opt_some(tq,typ) -> (*doc_typquant_lem tq*) (doc_typ_lem sequential mwords typ)
+let doc_tannot_opt_lem (Typ_annot_opt_aux(t,_)) = match t with
+ | Typ_annot_opt_some(tq,typ) -> (*doc_typquant_lem tq*) (doc_typ_lem typ)
-let doc_fun_body_lem sequential mwords exp =
+let doc_fun_body_lem exp =
let early_ret =contains_early_return exp in
- let doc_exp = doc_exp_lem sequential mwords early_ret false exp in
+ let doc_exp = doc_exp_lem early_ret false exp in
if early_ret
then align (string "catch_early_return" ^//^ parens (doc_exp))
else doc_exp
-let doc_funcl_lem sequential mwords (FCL_aux(FCL_Funcl(id,pexp),_)) =
+let doc_funcl_lem (FCL_aux(FCL_Funcl(id,pexp),_)) =
let pat,guard,exp,(l,_) = destruct_pexp pexp in
let _ = match guard with
| None -> ()
@@ -1221,8 +1225,8 @@ let doc_funcl_lem sequential mwords (FCL_aux(FCL_Funcl(id,pexp),_)) =
raise (Reporting_basic.err_unreachable l
"guarded pattern expression should have been rewritten before pretty-printing")
in
- group (prefix 3 1 ((doc_pat_lem sequential mwords false pat) ^^ space ^^ arrow)
- (doc_fun_body_lem sequential mwords exp))
+ group (prefix 3 1 ((doc_pat_lem false pat) ^^ space ^^ arrow)
+ (doc_fun_body_lem exp))
let get_id = function
| [] -> failwith "FD_function with empty list"
@@ -1230,7 +1234,7 @@ let get_id = function
module StringSet = Set.Make(String)
-let doc_fundef_rhs_lem sequential mwords (FD_aux(FD_function(r, typa, efa, funcls),fannot) as fd) =
+let doc_fundef_rhs_lem (FD_aux(FD_function(r, typa, efa, funcls),fannot) as fd) =
match funcls with
| [] -> failwith "FD_function with empty function list"
| [FCL_aux(FCL_Funcl(id,pexp),_)] ->
@@ -1244,25 +1248,24 @@ let doc_fundef_rhs_lem sequential mwords (FD_aux(FD_function(r, typa, efa, funcl
(prefix 2 1)
((separate space)
[doc_id_lem id;
- (doc_pat_lem sequential mwords true pat);
+ (doc_pat_lem true pat);
equals])
- (doc_fun_body_lem sequential mwords exp)
+ (doc_fun_body_lem exp)
| _ ->
let clauses =
(separate_map (break 1))
- (fun fcl -> separate space [pipe;doc_funcl_lem sequential mwords fcl]) funcls in
+ (fun fcl -> separate space [pipe;doc_funcl_lem fcl]) funcls in
(prefix 2 1)
((separate space) [doc_id_lem (id_of_fundef fd);equals;string "function"])
(clauses ^/^ string "end")
-let doc_mutrec_lem sequential mwords = function
+let doc_mutrec_lem = function
| [] -> failwith "DEF_internal_mutrec with empty function list"
| fundefs ->
string "let rec " ^^
- separate_map (hardline ^^ string "and ")
- (doc_fundef_rhs_lem sequential mwords) fundefs
+ separate_map (hardline ^^ string "and ") doc_fundef_rhs_lem fundefs
-let rec doc_fundef_lem sequential mwords (FD_aux(FD_function(r, typa, efa, fcls),fannot) as fd) =
+let rec doc_fundef_lem (FD_aux(FD_function(r, typa, efa, fcls),fannot) as fd) =
match fcls with
| [] -> failwith "FD_function with empty function list"
| FCL_aux (FCL_Funcl(id,_),_) :: _
@@ -1298,7 +1301,7 @@ let rec doc_fundef_lem sequential mwords (FD_aux(FD_function(r, typa, efa, fcls)
,annot) in
let auxiliary_functions =
auxiliary_functions ^^ hardline ^^ hardline ^^
- doc_fundef_lem sequential mwords (FD_aux (FD_function(r,typa,efa,[fcl]),fannot)) in
+ doc_fundef_lem (FD_aux (FD_function(r,typa,efa,[fcl]),fannot)) in
(* Bind complex patterns to names so that we can pass them to the
auxiliary function *)
let name_pat idx (P_aux (p,a)) = match p with
@@ -1310,13 +1313,13 @@ let rec doc_fundef_lem sequential mwords (FD_aux(FD_function(r, typa, efa, fcls)
let named_pat = P_aux (P_app (Id_aux (Id ctor,l),named_argspat),pannot) in
let doc_arg idx (P_aux (p,(l,a))) = match p with
| P_as (pat,id) -> doc_id_lem id
- | P_lit lit -> doc_lit_lem sequential mwords false lit a
+ | P_lit lit -> doc_lit_lem false lit a
| P_id id -> doc_id_lem id
| _ -> string ("arg" ^ string_of_int idx) in
let clauses =
clauses ^^ (break 1) ^^
(separate space
- [pipe;doc_pat_lem sequential mwords false named_pat;arrow;
+ [pipe;doc_pat_lem false named_pat;arrow;
string aux_fname;
parens (separate comma (List.mapi doc_arg named_argspat))]) in
(already_used_fnames,auxiliary_functions,clauses)
@@ -1328,15 +1331,15 @@ let rec doc_fundef_lem sequential mwords (FD_aux(FD_function(r, typa, efa, fcls)
(clauses ^/^ string "end")
| FCL_aux (FCL_Funcl(id,_),annot) :: _
when not (Env.is_extern id (env_of_annot annot) "lem") ->
- string "let" ^^ (doc_rec_lem r) ^^ (doc_fundef_rhs_lem sequential mwords fd)
+ string "let" ^^ (doc_rec_lem r) ^^ (doc_fundef_rhs_lem fd)
| _ -> empty
-let doc_dec_lem sequential (DEC_aux (reg, ((l, _) as annot))) =
+let doc_dec_lem (DEC_aux (reg, ((l, _) as annot))) =
match reg with
| DEC_reg(typ,id) ->
- if sequential then empty
+ if !opt_sequential then empty
else
let env = env_of_annot annot in
(match typ with
@@ -1365,12 +1368,12 @@ let doc_dec_lem sequential (DEC_aux (reg, ((l, _) as annot))) =
| DEC_alias(id,alspec) -> empty
| DEC_typ_alias(typ,id,alspec) -> empty
-let doc_spec_lem sequential mwords (VS_aux (valspec,annot)) =
+let doc_spec_lem (VS_aux (valspec,annot)) =
match valspec with
| VS_val_spec (typschm,id,ext,_) when ext "lem" = None ->
(* let (TypSchm_aux (TypSchm_ts (tq, typ), _)) = typschm in
- if contains_t_pp_var mwords typ then empty else *)
- separate space [string "val"; doc_id_lem id; string ":";doc_typschm_lem sequential mwords true typschm] ^/^ hardline
+ if contains_t_pp_var typ then empty else *)
+ separate space [string "val"; doc_id_lem id; string ":";doc_typschm_lem true typschm] ^/^ hardline
(* | VS_val_spec (_,_,Some _,_) -> empty *)
| _ -> empty
@@ -1392,7 +1395,7 @@ let is_field_accessor regtypes fdef =
(access = "get" || access = "set") && is_field_of regtyp field
| _ -> false
-let doc_regtype_fields sequential mwords (tname, (n1, n2, fields)) =
+let doc_regtype_fields (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
@@ -1414,7 +1417,7 @@ let doc_regtype_fields sequential mwords (tname, (n1, n2, fields)) =
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
+ let rfannot = doc_tannot_lem false reftyp in
doc_op equals
(concat [string "let "; parens (concat [string tname; underscore; doc_id_lem fid; rfannot])])
(concat [
@@ -1426,36 +1429,36 @@ let doc_regtype_fields sequential mwords (tname, (n1, n2, fields)) =
in
separate_map hardline doc_field fields
-let rec doc_def_lem sequential mwords regtypes def =
+let rec doc_def_lem 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)
+ | DEF_spec v_spec -> (empty,doc_spec_lem v_spec)
| DEF_fixity _ -> (empty,empty)
| DEF_overload _ -> (empty,empty)
- | DEF_type t_def -> (group (doc_typdef_lem sequential mwords t_def) ^/^ hardline,empty)
- | DEF_reg_dec dec -> (group (doc_dec_lem sequential dec),empty)
+ | DEF_type t_def -> (group (doc_typdef_lem t_def) ^/^ hardline,empty)
+ | DEF_reg_dec dec -> (group (doc_dec_lem dec),empty)
| DEF_default df -> (empty,empty)
| DEF_fundef fdef ->
- let doc_fdef = group (doc_fundef_lem sequential mwords fdef) ^/^ hardline in
+ let doc_fdef = group (doc_fundef_lem 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)
+ (empty, doc_mutrec_lem fundefs ^/^ hardline)
+ | DEF_val lbind -> (empty,group (doc_let_lem false lbind) ^/^ hardline)
| DEF_scattered sdef -> failwith "doc_def_lem: shoulnd't have DEF_scattered at this point"
| DEF_kind _ -> (empty,empty)
| DEF_comm (DC_comm s) -> (empty,comment (string s))
| DEF_comm (DC_comm_struct d) ->
- let (typdefs,vdefs) = doc_def_lem sequential mwords regtypes d in
+ let (typdefs,vdefs) = doc_def_lem regtypes d in
(empty,comment (typdefs ^^ hardline ^^ vdefs))
-let doc_defs_lem sequential mwords (Defs defs) =
+let doc_defs_lem (Defs 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
+ let field_refs = separate_map hardline doc_regtype_fields regtypes in
+ let (typdefs,valdefs) = List.split (List.map (doc_def_lem regtypes) defs) in
(separate empty typdefs ^^ field_refs, separate empty valdefs)
let find_registers (Defs defs) =
@@ -1470,7 +1473,7 @@ let find_registers (Defs defs) =
| _ -> acc
) [] defs
-let doc_regstate_lem mwords registers =
+let doc_regstate_lem registers =
let l = Parse_ast.Unknown in
let annot = (l, None) in
let regstate = match registers with
@@ -1494,17 +1497,17 @@ let doc_regstate_lem mwords registers =
| _ ->
let initreg (typ, id, env) =
let annot typ = Some (env, typ, no_effect) in
- let initval = undefined_of_typ mwords l annot typ in
+ let initval = undefined_of_typ !opt_mwords l annot typ in
FE_aux (FE_Fexp (id, initval), (l, annot typ)) in
E_aux (
E_record (FES_aux (FES_Fexps (List.map initreg registers, false), annot)),
(l, Some (Env.empty, mk_id_typ (mk_id "regstate"), no_effect)))
in
- doc_op equals (string "let initial_regstate") (doc_exp_lem true mwords false false exp)
+ doc_op equals (string "let initial_regstate") (doc_exp_lem false false exp)
else empty
in
concat [
- doc_typdef_lem true mwords (TD_aux (regstate, annot)); hardline;
+ doc_typdef_lem (TD_aux (regstate, annot)); hardline;
hardline;
string "type _MR 'a 'r = MR regstate 'a 'r"; hardline;
string "type _M 'a = M regstate 'a"
@@ -1534,10 +1537,10 @@ let doc_register_refs_lem registers =
string " write_to = (fun s v -> (<| s with "; field; string " = v |>)) |>"] in
separate_map hardline doc_register_ref registers
-let pp_defs_lem sequential mwords (types_file,types_modules) (defs_file,defs_modules) d top_line =
+let pp_defs_lem (types_file,types_modules) (defs_file,defs_modules) d top_line =
(* let regtypes = find_regtypes d in *)
- let (typdefs,valdefs) = doc_defs_lem sequential mwords d in
- let regstate_def, initregstate_def = doc_regstate_lem mwords (find_registers d) in
+ let (typdefs,valdefs) = doc_defs_lem d in
+ let regstate_def, initregstate_def = doc_regstate_lem (find_registers d) in
let register_refs = doc_register_refs_lem (find_registers d) in
(print types_file)
(concat
@@ -1558,7 +1561,7 @@ let pp_defs_lem sequential mwords (types_file,types_modules) (defs_file,defs_mod
else empty;
typdefs; hardline;
hardline;
- if sequential then
+ if !opt_sequential then
concat [regstate_def; hardline;
hardline;
register_refs]
diff --git a/src/process_file.ml b/src/process_file.ml
index 68e5786e..44f2e832 100644
--- a/src/process_file.ml
+++ b/src/process_file.ml
@@ -49,8 +49,6 @@
(**************************************************************************)
let opt_new_parser = ref false
-let opt_lem_sequential = ref false
-let opt_lem_mwords = ref false
type out_type =
| Lem_ast_out
@@ -130,7 +128,7 @@ let opt_dmono_analysis = ref 0
let opt_auto_mono = ref false
let monomorphise_ast locs type_env ast =
- let ast = Monomorphise.monomorphise (!opt_lem_mwords) (!opt_auto_mono) (!opt_dmono_analysis)
+ let ast = Monomorphise.monomorphise (!Pretty_print_lem.opt_mwords) (!opt_auto_mono) (!opt_dmono_analysis)
locs type_env ast in
let () = if !opt_ddump_raw_mono_ast then Pretty_print.pp_defs stdout ast else () in
let ienv = Type_check.Env.no_casts Type_check.initial_env in
@@ -159,10 +157,10 @@ let generated_line f =
let output_lem filename libs defs =
let generated_line = generated_line filename in
- let seq_suffix = if !opt_lem_sequential then "_sequential" else "" in
+ let seq_suffix = if !Pretty_print_lem.opt_sequential then "_sequential" else "" in
let types_module = (filename ^ "_embed_types" ^ seq_suffix) in
- let monad_module = if !opt_lem_sequential then "State" else "Prompt" in
- let operators_module = if !opt_lem_mwords then "Sail_operators_mwords" else "Sail_operators" in
+ let monad_module = if !Pretty_print_lem.opt_sequential then "State" else "Prompt" in
+ let operators_module = if !Pretty_print_lem.opt_mwords then "Sail_operators_mwords" else "Sail_operators" in
let libs = List.map (fun lib -> lib ^ seq_suffix) libs in
let base_imports = [
"Pervasives_extra";
@@ -175,7 +173,7 @@ let output_lem filename libs defs =
open_output_with_check_unformatted (filename ^ "_embed_types" ^ seq_suffix ^ ".lem") in
let ((o,_, _) as ext_o) =
open_output_with_check_unformatted (filename ^ "_embed" ^ seq_suffix ^ ".lem") in
- (Pretty_print.pp_defs_lem !opt_lem_sequential !opt_lem_mwords
+ (Pretty_print.pp_defs_lem
(ot, base_imports)
(o, base_imports @ (String.capitalize types_module :: libs))
defs generated_line);
@@ -233,7 +231,7 @@ let rewrite rewriters defs =
raise (Reporting_basic.err_typ l (Type_check.string_of_type_error err))
let rewrite_ast = rewrite [("initial", Rewriter.rewrite_defs)]
-let rewrite_undefined = rewrite [("undefined", fun x -> Rewrites.rewrite_undefined !opt_lem_mwords x)]
+let rewrite_undefined = rewrite [("undefined", fun x -> Rewrites.rewrite_undefined !Pretty_print_lem.opt_mwords x)]
let rewrite_ast_lem = rewrite Rewrites.rewrite_defs_lem
let rewrite_ast_ocaml = rewrite Rewrites.rewrite_defs_ocaml
let rewrite_ast_sil = rewrite Rewrites.rewrite_defs_sil
diff --git a/src/process_file.mli b/src/process_file.mli
index f99bdf54..a9b9cf1f 100644
--- a/src/process_file.mli
+++ b/src/process_file.mli
@@ -63,8 +63,6 @@ val load_file_no_check : Ast.order -> string -> unit Ast.defs
val load_file : Ast.order -> Type_check.Env.t -> string -> Type_check.tannot Ast.defs * Type_check.Env.t
val opt_new_parser : bool ref
-val opt_lem_sequential : bool ref
-val opt_lem_mwords : bool ref
val opt_just_check : bool ref
val opt_ddump_tc_ast : bool ref
val opt_ddump_rewrite_ast : ((string * int) option) ref
diff --git a/src/sail.ml b/src/sail.ml
index aecbcbec..d922afe9 100644
--- a/src/sail.ml
+++ b/src/sail.ml
@@ -93,10 +93,10 @@ let options = Arg.align ([
Arg.String (fun l -> opt_libs_lem := l::!opt_libs_lem),
"<filename> provide additional library to open in Lem output");
( "-lem_sequential",
- Arg.Set Process_file.opt_lem_sequential,
+ Arg.Set Pretty_print_lem.opt_sequential,
" use sequential state monad for Lem output");
( "-lem_mwords",
- Arg.Set Process_file.opt_lem_mwords,
+ Arg.Set Pretty_print_lem.opt_mwords,
" use native machine word library for Lem output");
( "-mono-split",
Arg.String (fun s ->
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-09 21:00:28 +0000