From 2ef7c31074720997bbc519e44e34c076677ab282 Mon Sep 17 00:00:00 2001 From: Thomas Bauereiss Date: Thu, 14 Dec 2017 16:48:05 +0000 Subject: Make sequential and mwords global variables in Lem pretty-printer --- src/monomorphise.ml | 5 +- src/pretty_print.mli | 2 +- src/pretty_print_lem.ml | 327 ++++++++++++++++++++++++------------------------ src/process_file.ml | 14 +-- src/process_file.mli | 2 - src/sail.ml | 4 +- 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), " 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 -> -- cgit v1.2.3 From 1c16fa04954387521ff8a21b68fb5bca3f27a29e Mon Sep 17 00:00:00 2001 From: Thomas Bauereiss Date: Thu, 14 Dec 2017 16:21:14 +0000 Subject: Un-tuple function arguments when pretty-printing to Lem This makes Lem prefer plain "definition" when generating Isabelle output for functions, which is processed by Isabelle much faster than "fun"/"function" definitions. This change is not complete yet, because the Sail library functions still need to be changed to not use tupled arguments (possibly as part of a bigger refactoring of the library). For now, external functions are special-cased in the pretty-printer and get tupled arguments. --- src/pretty_print_lem.ml | 107 ++++++++++++++++++++++++++++++------------------ 1 file changed, 67 insertions(+), 40 deletions(-) diff --git a/src/pretty_print_lem.ml b/src/pretty_print_lem.ml index 48eed31a..b0b76ac1 100644 --- a/src/pretty_print_lem.ml +++ b/src/pretty_print_lem.ml @@ -247,12 +247,15 @@ let doc_typ_lem, doc_atomic_typ_lem = 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 true ret] + then separate space [string "_M"; fn_typ true ret] else separate space [fn_typ false ret] in - let tpp = separate space [tup_typ true arg; arrow;ret_typ] in + let arg_typs = match arg with + | Typ_aux (Typ_tup typs, _) -> + List.map (app_typ true) typs + | _ -> [tup_typ true arg] in + let tpp = separate (space ^^ arrow ^^ space) (arg_typs @ [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 atyp_needed ty @@ -702,13 +705,17 @@ let doc_exp_lem, doc_let_lem = parens (separate_map comma (expV false) args) in if aexp_needed then parens (align epp) else epp | _ -> - let call = match annot with + let call, is_extern = match annot with | Some (env, _, _) when Env.is_extern f env "lem" -> - string (Env.get_extern f env "lem") - | _ -> doc_id_lem f in - let argspp = match args with - | [arg] -> expV true arg - | args -> parens (align (separate_map (comma ^^ break 0) (expV false) args)) in + string (Env.get_extern f env "lem"), true + | _ -> doc_id_lem f, false in + let argspp = + (* TODO Update Sail library functions to not use tupled arguments, + then remove the special case here *) + if is_extern then + parens (align (separate_map (comma ^^ break 0) (expV true) args)) + else + align (separate_map (break 1) (expV true) args) in let epp = align (call ^//^ argspp) in let (taepp,aexp_needed) = let t = (*Env.base_typ_of (env_of full_exp)*) (typ_of full_exp) in @@ -1203,6 +1210,43 @@ let doc_typdef_lem (TD_aux(td, (l, annot))) = match td with break 0 ^^ brackets (align doc_rids)])) | _ -> raise (Reporting_basic.err_unreachable l "register with non-constant indices") +let args_of_typ l env typ = + let typs = match typ with + | Typ_aux (Typ_tup typs, _) -> typs + | typ -> [typ] in + let arg i typ = + let id = mk_id ("arg" ^ string_of_int i) in + P_aux (P_id id, (l, Some (env, typ, no_effect))), + E_aux (E_id id, (l, Some (env, typ, no_effect))) in + List.split (List.mapi arg typs) + +let rec untuple_args_pat (P_aux (paux, ((l, _) as annot)) as pat) = + let env = env_of_annot annot in + let id = (fun body -> body) in + match paux with + | P_tup [] -> + let annot = (l, Some (Env.empty, unit_typ, no_effect)) in + [P_aux (P_lit (mk_lit L_unit), annot)], id + | P_tup pats -> pats, id + | P_wild -> + begin + match pat_typ_of pat with + | Typ_aux (Typ_tup typs, _) -> + let wild typ = P_aux (P_wild, (l, Some (env, typ, no_effect))) in + List.map wild typs, id + | _ -> [pat], id + end + | P_lit _ | P_id _ | P_var _ | P_app _ | P_record _ + | P_vector _ | P_vector_concat _ | P_list _ | P_cons _ -> + [pat], id + | P_typ (_, pat) -> untuple_args_pat pat + | P_as _ -> + let argpats, argexps = args_of_typ l env (pat_typ_of pat) in + let argexp = E_aux (E_tuple argexps, annot) in + let bindargs (E_aux (_, bannot) as body) = + E_aux (E_let (LB_aux (LB_val (pat, argexp), annot), body), bannot) in + argpats, bindargs + let doc_rec_lem (Rec_aux(r,_)) = match r with | Rec_nonrec -> space | Rec_rec -> space ^^ string "rec" ^^ space @@ -1219,14 +1263,16 @@ let doc_fun_body_lem exp = let doc_funcl_lem (FCL_aux(FCL_Funcl(id,pexp),_)) = let pat,guard,exp,(l,_) = destruct_pexp pexp in + let pats, bind = untuple_args_pat pat in + let patspp = separate_map space (doc_pat_lem true) pats in let _ = match guard with | None -> () | _ -> raise (Reporting_basic.err_unreachable l - "guarded pattern expression should have been rewritten before pretty-printing") - in - group (prefix 3 1 ((doc_pat_lem false pat) ^^ space ^^ arrow) - (doc_fun_body_lem exp)) + "guarded pattern expression should have been rewritten before pretty-printing") in + group (prefix 3 1 + (separate space [doc_id_lem id; patspp; equals]) + (doc_fun_body_lem (bind exp))) let get_id = function | [] -> failwith "FD_function with empty list" @@ -1235,29 +1281,7 @@ let get_id = function module StringSet = Set.Make(String) 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),_)] -> - let pat,guard,exp,(l,_) = destruct_pexp pexp in - let _ = match guard with - | None -> () - | _ -> - raise (Reporting_basic.err_unreachable l - "guarded pattern expression should have been rewritten before pretty-printing") - in - (prefix 2 1) - ((separate space) - [doc_id_lem id; - (doc_pat_lem true pat); - equals]) - (doc_fun_body_lem exp) - | _ -> - let clauses = - (separate_map (break 1)) - (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") + separate_map (hardline ^^ string "and ") doc_funcl_lem funcls let doc_mutrec_lem = function | [] -> failwith "DEF_internal_mutrec with empty function list" @@ -1294,10 +1318,12 @@ let rec doc_fundef_lem (FD_aux(FD_function(r, typa, efa, fcls),fannot) as fd) = if StringSet.mem candidate already_used then pick_name_not_clashing_with already_used (candidate ^ "'") else candidate in + let unit_pat = P_aux (P_lit (mk_lit L_unit), (l, Some (Env.empty, unit_typ, no_effect))) in let aux_fname = pick_name_not_clashing_with already_used_fnames (string_of_id id ^ "_" ^ ctor) in + let aux_args = if argspat = [] then unit_pat else P_aux (P_tup argspat,pannot) in let already_used_fnames = StringSet.add aux_fname already_used_fnames in let fcl = FCL_aux (FCL_Funcl (Id_aux (Id aux_fname,l), - Pat_aux (Pat_exp (P_aux (P_tup argspat,pannot),exp),(pexp_l,None))) + Pat_aux (Pat_exp (aux_args,exp),(pexp_l,None))) ,annot) in let auxiliary_functions = auxiliary_functions ^^ hardline ^^ hardline ^^ @@ -1311,6 +1337,7 @@ let rec doc_fundef_lem (FD_aux(FD_function(r, typa, efa, fcls),fannot) as fd) = | _ -> P_aux (P_as (P_aux (p,a), Id_aux (Id ("arg" ^ string_of_int idx),l)),a) in let named_argspat = List.mapi name_pat argspat in let named_pat = P_aux (P_app (Id_aux (Id ctor,l),named_argspat),pannot) in + let named_args = if argspat = [] then [unit_pat] else named_argspat 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 false lit a @@ -1321,7 +1348,7 @@ let rec doc_fundef_lem (FD_aux(FD_function(r, typa, efa, fcls),fannot) as fd) = (separate space [pipe;doc_pat_lem false named_pat;arrow; string aux_fname; - parens (separate comma (List.mapi doc_arg named_argspat))]) in + separate space (List.mapi doc_arg named_args)]) in (already_used_fnames,auxiliary_functions,clauses) ) (StringSet.empty,empty,empty) fcls in @@ -1424,8 +1451,8 @@ let doc_regtype_fields (tname, (n1, n2, fields)) = 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]) + space; space; space; string (" get_field = get_" ^ tname ^ "_" ^ string_of_id fid ^ ";"); hardline; + space; space; space; string (" set_field = set_" ^ tname ^ "_" ^ string_of_id fid ^ " "); ranglebar]) in separate_map hardline doc_field fields -- cgit v1.2.3 From 5cd77a145b886e614d4b5cb46e53d42736cc6865 Mon Sep 17 00:00:00 2001 From: Brian Campbell Date: Mon, 18 Dec 2017 14:28:02 +0000 Subject: Handle multiple -lem_lib options --- src/process_file.ml | 6 +++--- src/process_file.mli | 2 +- src/sail.ml | 2 +- 3 files changed, 5 insertions(+), 5 deletions(-) diff --git a/src/process_file.ml b/src/process_file.ml index 44f2e832..a1ce00ff 100644 --- a/src/process_file.ml +++ b/src/process_file.ml @@ -52,7 +52,7 @@ let opt_new_parser = ref false type out_type = | Lem_ast_out - | Lem_out of string option + | Lem_out of string list option let get_lexbuf f = let in_chan = open_in f in @@ -201,8 +201,8 @@ let output1 libpath out_arg filename defs = end | Lem_out None -> output_lem f' [] defs - | Lem_out (Some lib) -> - output_lem f' [lib] defs + | Lem_out (Some libs) -> + output_lem f' libs defs let output libpath out_arg files = List.iter diff --git a/src/process_file.mli b/src/process_file.mli index a9b9cf1f..17088d36 100644 --- a/src/process_file.mli +++ b/src/process_file.mli @@ -73,7 +73,7 @@ val opt_auto_mono : bool ref type out_type = | Lem_ast_out - | Lem_out of string option (* If present, the string is a file to open in the lem backend*) + | Lem_out of string list option (* If present, the strings are files to open in the lem backend*) val output : string -> (* The path to the library *) diff --git a/src/sail.ml b/src/sail.ml index d922afe9..93669c9d 100644 --- a/src/sail.ml +++ b/src/sail.ml @@ -234,7 +234,7 @@ let main() = then let ast_lem = rewrite_ast_lem ast in if !(opt_libs_lem) = [] then output "" (Lem_out None) [out_name,ast_lem] - else output "" (Lem_out (Some (List.hd !opt_libs_lem))) [out_name,ast_lem] + else output "" (Lem_out (Some (!opt_libs_lem))) [out_name,ast_lem] else ()); end -- cgit v1.2.3 From fb12f81bc8c682439a440e3939c7ae029d91fd5e Mon Sep 17 00:00:00 2001 From: Brian Campbell Date: Mon, 18 Dec 2017 14:32:09 +0000 Subject: Clean up last commit --- src/process_file.ml | 6 ++---- src/process_file.mli | 2 +- src/sail.ml | 4 +--- 3 files changed, 4 insertions(+), 8 deletions(-) diff --git a/src/process_file.ml b/src/process_file.ml index a1ce00ff..83cfd8a3 100644 --- a/src/process_file.ml +++ b/src/process_file.ml @@ -52,7 +52,7 @@ let opt_new_parser = ref false type out_type = | Lem_ast_out - | Lem_out of string list option + | Lem_out of string list let get_lexbuf f = let in_chan = open_in f in @@ -199,9 +199,7 @@ let output1 libpath out_arg filename defs = Pretty_print.pp_lem_defs o defs; close_output_with_check ext_o end - | Lem_out None -> - output_lem f' [] defs - | Lem_out (Some libs) -> + | Lem_out libs -> output_lem f' libs defs let output libpath out_arg files = diff --git a/src/process_file.mli b/src/process_file.mli index 17088d36..88c9b9fb 100644 --- a/src/process_file.mli +++ b/src/process_file.mli @@ -73,7 +73,7 @@ val opt_auto_mono : bool ref type out_type = | Lem_ast_out - | Lem_out of string list option (* If present, the strings are files to open in the lem backend*) + | Lem_out of string list (* If present, the strings are files to open in the lem backend*) val output : string -> (* The path to the library *) diff --git a/src/sail.ml b/src/sail.ml index 93669c9d..9bb7cfcb 100644 --- a/src/sail.ml +++ b/src/sail.ml @@ -232,9 +232,7 @@ let main() = else ()); (if !(opt_print_lem) then let ast_lem = rewrite_ast_lem ast in - if !(opt_libs_lem) = [] - then output "" (Lem_out None) [out_name,ast_lem] - else output "" (Lem_out (Some (!opt_libs_lem))) [out_name,ast_lem] + output "" (Lem_out (!opt_libs_lem)) [out_name,ast_lem] else ()); end -- cgit v1.2.3 From dfd6d278deb29e5fd39e3246a52bb0999451a47c Mon Sep 17 00:00:00 2001 From: Thomas Bauereiss Date: Tue, 19 Dec 2017 11:28:48 +0000 Subject: Fix a bug in untupling function arguments for Lem Was missing the case where the tuple of arguments is bound against a single variable using P_id (not P_as). Now replaces that with the expected number of argument variables, and rebinds the single variable in the body, as for the other cases. --- src/pretty_print_lem.ml | 31 +++++++++++++------------------ 1 file changed, 13 insertions(+), 18 deletions(-) diff --git a/src/pretty_print_lem.ml b/src/pretty_print_lem.ml index b0b76ac1..96f312fb 100644 --- a/src/pretty_print_lem.ml +++ b/src/pretty_print_lem.ml @@ -1222,30 +1222,25 @@ let args_of_typ l env typ = let rec untuple_args_pat (P_aux (paux, ((l, _) as annot)) as pat) = let env = env_of_annot annot in - let id = (fun body -> body) in - match paux with - | P_tup [] -> + let (Typ_aux (taux, _)) = typ_of_annot annot in + let identity = (fun body -> body) in + match paux, taux with + | P_tup [], _ -> let annot = (l, Some (Env.empty, unit_typ, no_effect)) in - [P_aux (P_lit (mk_lit L_unit), annot)], id - | P_tup pats -> pats, id - | P_wild -> - begin - match pat_typ_of pat with - | Typ_aux (Typ_tup typs, _) -> - let wild typ = P_aux (P_wild, (l, Some (env, typ, no_effect))) in - List.map wild typs, id - | _ -> [pat], id - end - | P_lit _ | P_id _ | P_var _ | P_app _ | P_record _ - | P_vector _ | P_vector_concat _ | P_list _ | P_cons _ -> - [pat], id - | P_typ (_, pat) -> untuple_args_pat pat - | P_as _ -> + [P_aux (P_lit (mk_lit L_unit), annot)], identity + | P_tup pats, _ -> pats, identity + | P_wild, Typ_tup typs -> + let wild typ = P_aux (P_wild, (l, Some (env, typ, no_effect))) in + List.map wild typs, identity + | P_typ (_, pat), _ -> untuple_args_pat pat + | P_as _, Typ_tup _ | P_id _, Typ_tup _ -> let argpats, argexps = args_of_typ l env (pat_typ_of pat) in let argexp = E_aux (E_tuple argexps, annot) in let bindargs (E_aux (_, bannot) as body) = E_aux (E_let (LB_aux (LB_val (pat, argexp), annot), body), bannot) in argpats, bindargs + | _, _ -> + [pat], identity let doc_rec_lem (Rec_aux(r,_)) = match r with | Rec_nonrec -> space -- cgit v1.2.3 From 5c0b807f89b99b1f7adb2a2f6aebdea52a8bdd80 Mon Sep 17 00:00:00 2001 From: Thomas Bauereiss Date: Tue, 19 Dec 2017 11:40:49 +0000 Subject: Add rewriting step for numeral patterns Pattern matching against literal numbers is not well supported by Lem or Isabelle. This rewriting step turns them into guarded patterns (which can be picked up by the guarded pattern rewriting to if-expressions). --- src/rewrites.ml | 47 ++++++++++++++++++++++++++++++++++++++++------- 1 file changed, 40 insertions(+), 7 deletions(-) diff --git a/src/rewrites.ml b/src/rewrites.ml index 424931c3..a42335b9 100644 --- a/src/rewrites.ml +++ b/src/rewrites.ml @@ -1028,6 +1028,12 @@ let bitwise_and_exp exp1 exp2 = let andid = Id_aux (Id "and_bool", gen_loc l) in annot_exp (E_app(andid,[exp1;exp2])) l (env_of exp1) bool_typ +let compose_guard_opt g1 g2 = match g1, g2 with + | Some g1, Some g2 -> Some (bitwise_and_exp g1 g2) + | Some g1, None -> Some g1 + | None, Some g2 -> Some g2 + | None, None -> None + let rec contains_bitvector_pat (P_aux (pat,annot)) = match pat with | P_lit _ | P_wild | P_id _ -> false | P_as (pat,_) | P_typ (_,pat) -> contains_bitvector_pat pat @@ -1122,13 +1128,7 @@ let remove_bitvector_pat (P_aux (_, (l, _)) as pat) = annot_exp (E_let (letbind,body)) l env (typ_of body)) in (letexp, letbind) in - let compose_guards guards = - let conj g1 g2 = match g1, g2 with - | Some g1, Some g2 -> Some (bitwise_and_exp g1 g2) - | Some g1, None -> Some g1 - | None, Some g2 -> Some g2 - | None, None -> None in - List.fold_right conj guards None in + let compose_guards guards = List.fold_right compose_guard_opt guards None in let flatten_guards_decls gd = let (guards,decls,letbinds) = Util.split3 gd in @@ -1294,6 +1294,38 @@ let rewrite_defs_remove_bitvector_pats (Defs defs) = Defs (List.flatten (List.map rewrite_def defs)) (* )) *) +(* Rewrite literal number patterns to guarded patterns + Those numeral patterns are not handled very well by Lem (or Isabelle) + *) +let rewrite_defs_remove_numeral_pats = + let p_lit = function + | L_aux (L_num n, l) -> + let id = fresh_id "l__" Parse_ast.Unknown in + let annot_exp e_aux typ = E_aux (e_aux, simple_annot l typ) in + let guard = + annot_exp (E_app_infix ( + annot_exp (E_id id) (atom_typ (nconstant n)), + mk_id "==", + simple_num l n + )) bool_typ in + (Some guard, P_id id) + | lit -> (None, P_lit lit) in + let guard_pat = + fold_pat { (compute_pat_alg None compose_guard_opt) with p_lit = p_lit } in + let pat_aux (pexp_aux, a) = + let pat,guard,exp,a = destruct_pexp (Pat_aux (pexp_aux, a)) in + let guard',pat = guard_pat pat in + match compose_guard_opt guard guard' with + | Some g -> Pat_aux (Pat_when (pat, g, exp), a) + | None -> Pat_aux (Pat_exp (pat, exp), a) in + let exp_alg = { id_exp_alg with pat_aux = pat_aux } in + let rewrite_exp _ = fold_exp exp_alg in + let rewrite_funcl (FCL_aux (FCL_Funcl (id, pexp), annot)) = + FCL_aux (FCL_Funcl (id, fold_pexp exp_alg pexp), annot) in + let rewrite_fun _ (FD_aux (FD_function (r_o, t_o, e_o, funcls), a)) = + FD_aux (FD_function (r_o, t_o, e_o, List.map rewrite_funcl funcls), a) in + rewrite_defs_base + { rewriters_base with rewrite_exp = rewrite_exp; rewrite_fun = rewrite_fun } (* Remove pattern guards by rewriting them to if-expressions within the pattern expression. *) @@ -2921,6 +2953,7 @@ let rewrite_defs_lem = [ (* ("simple_assignments", rewrite_simple_assignments); *) ("remove_vector_concat", rewrite_defs_remove_vector_concat); ("remove_bitvector_pats", rewrite_defs_remove_bitvector_pats); + ("remove_numeral_pats", rewrite_defs_remove_numeral_pats); ("guarded_pats", rewrite_defs_guarded_pats); ("exp_lift_assign", rewrite_defs_exp_lift_assign); ("register_ref_writes", rewrite_register_ref_writes); -- cgit v1.2.3 From b938fd99a9f16d4bb2ef1c483574a2850aa6e640 Mon Sep 17 00:00:00 2001 From: Thomas Bauereiss Date: Tue, 19 Dec 2017 11:53:23 +0000 Subject: Support user-defined exceptions in Lem shallow embedding The type-checker already supports a user-defined "exception" type that can be used in throw and try-catch expressions. This patch adds support for that to the Lem shallow embedding by adapting the existing exception mechanisms of the state and prompt monads. User-defined exceptions are distinguished from builtin exception cases. For example, the state monad uses type ex 'e = | Exit | Assert of string | Throw of 'e to distinguish between calls to "exit", failed assertions, and user-defined exceptions, respectively. Early return is also handled using the exception mechanism, by lifting to a monad with "either 'r exception" as the exception type, where 'r is the expected return type and "exception" is the user-defined exception type. --- mips_new_tc/mips_extras_embed.lem | 28 ++--- mips_new_tc/mips_extras_embed_sequential.lem | 26 ++-- src/ast_util.ml | 8 ++ src/ast_util.mli | 1 + src/gen_lib/prompt.lem | 149 ++++++++++++----------- src/gen_lib/state.lem | 174 +++++++++++++++------------ src/lem_interp/sail_impl_base.lem | 27 ++--- src/monomorphise.ml | 2 +- src/pretty_print_lem.ml | 52 +++++--- src/rewriter.ml | 5 +- src/rewrites.ml | 8 ++ 11 files changed, 276 insertions(+), 204 deletions(-) diff --git a/mips_new_tc/mips_extras_embed.lem b/mips_new_tc/mips_extras_embed.lem index 82f208f6..bda70274 100644 --- a/mips_new_tc/mips_extras_embed.lem +++ b/mips_new_tc/mips_extras_embed.lem @@ -4,10 +4,10 @@ open import Sail_impl_base open import Sail_values open import Prompt -val MEMr : forall 'a 'b. Bitvector 'a, Bitvector 'b => ('a * integer) -> M 'b -val MEMr_reserve : forall 'a 'b. Bitvector 'a, Bitvector 'b => ('a * integer) -> M 'b -val MEMr_tag : forall 'a 'b. Bitvector 'a, Bitvector 'b => ('a * integer) -> M 'b -val MEMr_tag_reserve : forall 'a 'b. Bitvector 'a, Bitvector 'b => ('a * integer) -> M 'b +val MEMr : forall 'a 'b 'e. Bitvector 'a, Bitvector 'b => ('a * integer) -> M 'b 'e +val MEMr_reserve : forall 'a 'b 'e. Bitvector 'a, Bitvector 'b => ('a * integer) -> M 'b 'e +val MEMr_tag : forall 'a 'b 'e. Bitvector 'a, Bitvector 'b => ('a * integer) -> M 'b 'e +val MEMr_tag_reserve : forall 'a 'b 'e. Bitvector 'a, Bitvector 'b => ('a * integer) -> M 'b 'e let MEMr (addr,size) = read_mem false Read_plain addr size let MEMr_reserve (addr,size) = read_mem false Read_reserve addr size @@ -16,10 +16,10 @@ let MEMr_tag (addr,size) = read_mem false Read_plain addr size let MEMr_tag_reserve (addr,size) = read_mem false Read_reserve addr size -val MEMea : forall 'a. Bitvector 'a => ('a * integer) -> M unit -val MEMea_conditional : forall 'a. Bitvector 'a => ('a * integer) -> M unit -val MEMea_tag : forall 'a. Bitvector 'a => ('a * integer) -> M unit -val MEMea_tag_conditional : forall 'a. Bitvector 'a => ('a * integer) -> M unit +val MEMea : forall 'a 'e. Bitvector 'a => ('a * integer) -> M unit 'e +val MEMea_conditional : forall 'a 'e. Bitvector 'a => ('a * integer) -> M unit 'e +val MEMea_tag : forall 'a 'e. Bitvector 'a => ('a * integer) -> M unit 'e +val MEMea_tag_conditional : forall 'a 'e. Bitvector 'a => ('a * integer) -> M unit 'e let MEMea (addr,size) = write_mem_ea Write_plain addr size let MEMea_conditional (addr,size) = write_mem_ea Write_conditional addr size @@ -28,10 +28,10 @@ let MEMea_tag (addr,size) = write_mem_ea Write_plain addr size let MEMea_tag_conditional (addr,size) = write_mem_ea Write_conditional addr size -val MEMval : forall 'a 'b. Bitvector 'a, Bitvector 'b => ('a * integer * 'b) -> M unit -val MEMval_conditional : forall 'a 'b. Bitvector 'a, Bitvector 'b => ('a * integer * 'b) -> M bool -val MEMval_tag : forall 'a 'b. Bitvector 'a, Bitvector 'b => ('a * integer * 'b) -> M unit -val MEMval_tag_conditional : forall 'a 'b. Bitvector 'a, Bitvector 'b => ('a * integer * 'b) -> M bool +val MEMval : forall 'a 'b 'e. Bitvector 'a, Bitvector 'b => ('a * integer * 'b) -> M unit 'e +val MEMval_conditional : forall 'a 'b 'e. Bitvector 'a, Bitvector 'b => ('a * integer * 'b) -> M bool 'e +val MEMval_tag : forall 'a 'b 'e. Bitvector 'a, Bitvector 'b => ('a * integer * 'b) -> M unit 'e +val MEMval_tag_conditional : forall 'a 'b 'e. Bitvector 'a, Bitvector 'b => ('a * integer * 'b) -> M bool 'e let MEMval (_,_,v) = write_mem_val v >>= fun _ -> return () let MEMval_conditional (_,_,v) = write_mem_val v >>= fun b -> return (if b then true else false) @@ -39,9 +39,9 @@ let MEMval_tag (_,_,v) = write_mem_val v >>= fun _ -> return () let MEMval_tag_conditional (_,_,v) = write_mem_val v >>= fun b -> return (if b then true else false) (* TODO *) -val TAGw : (vector bitU * vector bitU) -> M unit +val TAGw : forall 'e. (vector bitU * vector bitU) -> M unit 'e let TAGw (addr, tag) = failwith "TAGw not implemented" -val MEM_sync : unit -> M unit +val MEM_sync : forall 'e. unit -> M unit 'e let MEM_sync () = barrier Barrier_Isync diff --git a/mips_new_tc/mips_extras_embed_sequential.lem b/mips_new_tc/mips_extras_embed_sequential.lem index c32f297e..b50052dc 100644 --- a/mips_new_tc/mips_extras_embed_sequential.lem +++ b/mips_new_tc/mips_extras_embed_sequential.lem @@ -5,10 +5,10 @@ open import Sail_values open import Sail_operators_mwords open import State -val MEMr : forall 'regs 'a 'b. Bitvector 'a, Bitvector 'b => ('a * integer) -> M 'regs 'b -val MEMr_reserve : forall 'regs 'a 'b. Bitvector 'a, Bitvector 'b => ('a * integer) -> M 'regs 'b -val MEMr_tag : forall 'regs 'a 'b. Bitvector 'a, Bitvector 'b => ('a * integer) -> M 'regs (bool * 'b) -val MEMr_tag_reserve : forall 'regs 'a 'b. Bitvector 'a, Bitvector 'b => ('a * integer) -> M 'regs (bool * 'b) +val MEMr : forall 'regs 'a 'b 'e. Bitvector 'a, Bitvector 'b => ('a * integer) -> M 'regs 'b 'e +val MEMr_reserve : forall 'regs 'a 'b 'e. Bitvector 'a, Bitvector 'b => ('a * integer) -> M 'regs 'b 'e +val MEMr_tag : forall 'regs 'a 'b 'e. Bitvector 'a, Bitvector 'b => ('a * integer) -> M 'regs (bool * 'b) 'e +val MEMr_tag_reserve : forall 'regs 'a 'b 'e. Bitvector 'a, Bitvector 'b => ('a * integer) -> M 'regs (bool * 'b) 'e let MEMr (addr,size) = read_mem false Read_plain addr size let MEMr_reserve (addr,size) = read_mem false Read_reserve addr size @@ -24,10 +24,10 @@ let MEMr_tag_reserve (addr,size) = return (bitU_to_bool t, v) -val MEMea : forall 'regs 'a. Bitvector 'a => ('a * integer) -> M 'regs unit -val MEMea_conditional : forall 'regs 'a. Bitvector 'a => ('a * integer) -> M 'regs unit -val MEMea_tag : forall 'regs 'a. Bitvector 'a => ('a * integer) -> M 'regs unit -val MEMea_tag_conditional : forall 'regs 'a. Bitvector 'a => ('a * integer) -> M 'regs unit +val MEMea : forall 'regs 'a 'e. Bitvector 'a => ('a * integer) -> M 'regs unit 'e +val MEMea_conditional : forall 'regs 'a 'e. Bitvector 'a => ('a * integer) -> M 'regs unit 'e +val MEMea_tag : forall 'regs 'a 'e. Bitvector 'a => ('a * integer) -> M 'regs unit 'e +val MEMea_tag_conditional : forall 'regs 'a 'e. Bitvector 'a => ('a * integer) -> M 'regs unit 'e let MEMea (addr,size) = write_mem_ea Write_plain addr size let MEMea_conditional (addr,size) = write_mem_ea Write_conditional addr size @@ -36,16 +36,16 @@ let MEMea_tag (addr,size) = write_mem_ea Write_plain addr size let MEMea_tag_conditional (addr,size) = write_mem_ea Write_conditional addr size -val MEMval : forall 'regs 'a 'b. Bitvector 'a, Bitvector 'b => ('a * integer * 'b) -> M 'regs unit -val MEMval_conditional : forall 'regs 'a 'b. Bitvector 'a, Bitvector 'b => ('a * integer * 'b) -> M 'regs bool -val MEMval_tag : forall 'regs 'a 'b. Bitvector 'a, Bitvector 'b => ('a * integer * bool * 'b) -> M 'regs unit -val MEMval_tag_conditional : forall 'regs 'a 'b. Bitvector 'a, Bitvector 'b => ('a * integer * bool * 'b) -> M 'regs bool +val MEMval : forall 'regs 'a 'b 'e. Bitvector 'a, Bitvector 'b => ('a * integer * 'b) -> M 'regs unit 'e +val MEMval_conditional : forall 'regs 'a 'b 'e. Bitvector 'a, Bitvector 'b => ('a * integer * 'b) -> M 'regs bool 'e +val MEMval_tag : forall 'regs 'a 'b 'e. Bitvector 'a, Bitvector 'b => ('a * integer * bool * 'b) -> M 'regs unit 'e +val MEMval_tag_conditional : forall 'regs 'a 'b 'e. Bitvector 'a, Bitvector 'b => ('a * integer * bool * 'b) -> M 'regs bool 'e let MEMval (_,size,v) = write_mem_val v >>= fun _ -> return () let MEMval_conditional (_,size,v) = write_mem_val v >>= fun b -> return (if b then true else false) let MEMval_tag (_,size,t,v) = write_mem_val v >>= fun _ -> write_tag (bool_to_bitU t) >>= fun _ -> return () let MEMval_tag_conditional (_,size,t,v) = write_mem_val v >>= fun b -> write_tag (bool_to_bitU t) >>= fun _ -> return (if b then true else false) -val MEM_sync : forall 'regs. unit -> M 'regs unit +val MEM_sync : forall 'regs 'e. unit -> M 'regs unit 'e let MEM_sync () = barrier Barrier_MIPS_SYNC diff --git a/src/ast_util.ml b/src/ast_util.ml index 2fd43db5..4ceb3e7f 100644 --- a/src/ast_util.ml +++ b/src/ast_util.ml @@ -679,6 +679,14 @@ let id_of_fundef (FD_aux (FD_function (_, _, _, funcls), (l, _))) = | Some id -> id | None -> raise (Reporting_basic.err_typ l "funcl list is empty") +let id_of_type_def_aux = function + | TD_abbrev (id, _, _) + | TD_record (id, _, _, _, _) + | TD_variant (id, _, _, _, _) + | TD_enum (id, _, _, _) + | TD_register (id, _, _, _) -> id +let id_of_type_def (TD_aux (td_aux, _)) = id_of_type_def_aux td_aux + module BE = struct type t = base_effect let compare be1 be2 = String.compare (string_of_base_effect be1) (string_of_base_effect be2) diff --git a/src/ast_util.mli b/src/ast_util.mli index a45ca4e9..68955387 100644 --- a/src/ast_util.mli +++ b/src/ast_util.mli @@ -192,6 +192,7 @@ val string_of_letbind : 'a letbind -> string val string_of_index_range : index_range -> string val id_of_fundef : 'a fundef -> id +val id_of_type_def : 'a type_def -> id val id_of_kid : kid -> id val kid_of_id : id -> kid diff --git a/src/gen_lib/prompt.lem b/src/gen_lib/prompt.lem index 4646ef6f..77a39096 100644 --- a/src/gen_lib/prompt.lem +++ b/src/gen_lib/prompt.lem @@ -2,13 +2,12 @@ open import Pervasives_extra open import Sail_impl_base open import Sail_values -type MR 'a 'r = outcome_r 'a 'r -type M 'a = outcome 'a +type M 'a 'e = outcome 'a 'e -val return : forall 'a 'r. 'a -> MR 'a 'r +val return : forall 'a 'e. 'a -> M 'a 'e let return a = Done a -val bind : forall 'a 'b 'r. MR 'a 'r -> ('a -> MR 'b 'r) -> MR 'b 'r +val bind : forall 'a 'b 'e. M 'a 'e -> ('a -> M 'b 'e) -> M 'b 'e let rec bind m f = match m with | Done a -> f a | Read_mem descr k -> Read_mem descr (fun v -> let (o,opt) = k v in (bind o f,opt)) @@ -22,61 +21,73 @@ let rec bind m f = match m with | Escape descr -> Escape descr | Fail descr -> Fail descr | Error descr -> Error descr - | Return a -> Return a + | Exception e -> Exception e | Internal descr o_s -> Internal descr (let (o,opt) = o_s in (bind o f ,opt)) end let inline (>>=) = bind -val (>>) : forall 'b 'r. MR unit 'r -> MR 'b 'r -> MR 'b 'r -let inline (>>) m n = m >>= fun _ -> n +val (>>) : forall 'b 'e. M unit 'e -> M 'b 'e -> M 'b 'e +let inline (>>) m n = m >>= fun (_ : unit) -> n -val exit : forall 'a 'b. 'b -> M 'a -let exit s = Fail Nothing +val exit : forall 'a 'e. unit -> M 'a 'e +let exit () = Fail Nothing -val assert_exp : bool -> string -> M unit +val assert_exp : forall 'e. bool -> string -> M unit 'e let assert_exp exp msg = if exp then Done () else Fail (Just msg) -val early_return : forall 'r. 'r -> MR unit 'r -let early_return r = Return r +val throw : forall 'a 'e. 'e -> M 'a 'e +let throw e = Exception e -val liftR : forall 'a 'r. M 'a -> MR 'a 'r -let rec liftR m = match m with +val try_catch : forall 'a 'e1 'e2. M 'a 'e1 -> ('e1 -> M 'a 'e2) -> M 'a 'e2 +let rec try_catch m h = match m with | Done a -> Done a - | Read_mem descr k -> Read_mem descr (fun v -> let (o,opt) = k v in (liftR o,opt)) - | Read_reg descr k -> Read_reg descr (fun v -> let (o,opt) = k v in (liftR o,opt)) - | Write_memv descr k -> Write_memv descr (fun v -> let (o,opt) = k v in (liftR o,opt)) - | Excl_res k -> Excl_res (fun v -> let (o,opt) = k v in (liftR o,opt)) - | Write_ea descr o_s -> Write_ea descr (let (o,opt) = o_s in (liftR o,opt)) - | Barrier descr o_s -> Barrier descr (let (o,opt) = o_s in (liftR o,opt)) - | Footprint o_s -> Footprint (let (o,opt) = o_s in (liftR o,opt)) - | Write_reg descr o_s -> Write_reg descr (let (o,opt) = o_s in (liftR o,opt)) - | Internal descr o_s -> Internal descr (let (o,opt) = o_s in (liftR o,opt)) + | Read_mem descr k -> Read_mem descr (fun v -> let (o,opt) = k v in (try_catch o h,opt)) + | Read_reg descr k -> Read_reg descr (fun v -> let (o,opt) = k v in (try_catch o h,opt)) + | Write_memv descr k -> Write_memv descr (fun v -> let (o,opt) = k v in (try_catch o h,opt)) + | Excl_res k -> Excl_res (fun v -> let (o,opt) = k v in (try_catch o h,opt)) + | Write_ea descr o_s -> Write_ea descr (let (o,opt) = o_s in (try_catch o h,opt)) + | Barrier descr o_s -> Barrier descr (let (o,opt) = o_s in (try_catch o h,opt)) + | Footprint o_s -> Footprint (let (o,opt) = o_s in (try_catch o h,opt)) + | Write_reg descr o_s -> Write_reg descr (let (o,opt) = o_s in (try_catch o h,opt)) | Escape descr -> Escape descr | Fail descr -> Fail descr | Error descr -> Error descr - | Return _ -> Error "uncaught early return" + | Exception e -> h e + | Internal descr o_s -> Internal descr (let (o,opt) = o_s in (try_catch o h ,opt)) end -val catch_early_return : forall 'a 'r. MR 'a 'a -> M 'a -let rec catch_early_return m = match m with - | Done a -> Done a - | Read_mem descr k -> Read_mem descr (fun v -> let (o,opt) = k v in (catch_early_return o,opt)) - | Read_reg descr k -> Read_reg descr (fun v -> let (o,opt) = k v in (catch_early_return o,opt)) - | Write_memv descr k -> Write_memv descr (fun v -> let (o,opt) = k v in (catch_early_return o,opt)) - | Excl_res k -> Excl_res (fun v -> let (o,opt) = k v in (catch_early_return o,opt)) - | Write_ea descr o_s -> Write_ea descr (let (o,opt) = o_s in (catch_early_return o,opt)) - | Barrier descr o_s -> Barrier descr (let (o,opt) = o_s in (catch_early_return o,opt)) - | Footprint o_s -> Footprint (let (o,opt) = o_s in (catch_early_return o,opt)) - | Write_reg descr o_s -> Write_reg descr (let (o,opt) = o_s in (catch_early_return o,opt)) - | Internal descr o_s -> Internal descr (let (o,opt) = o_s in (catch_early_return o,opt)) - | Escape descr -> Escape descr - | Fail descr -> Fail descr - | Error descr -> Error descr - | Return a -> Done a -end - -val read_mem : forall 'a 'b. Bitvector 'a, Bitvector 'b => bool -> read_kind -> 'a -> integer -> M 'b +(* For early return, we abuse exceptions by throwing and catching + the return value. The exception type is "either 'r 'e", where "Right e" + represents a proper exception and "Left r" an early return of value "r". *) +type MR 'a 'r 'e = M 'a (either 'r 'e) + +val early_return : forall 'a 'r 'e. 'r -> MR 'a 'r 'e +let early_return r = throw (Left r) + +val catch_early_return : forall 'a 'e. MR 'a 'a 'e -> M 'a 'e +let catch_early_return m = + try_catch m + (function + | Left a -> return a + | Right e -> throw e + end) + +(* Lift to monad with early return by wrapping exceptions *) +val liftR : forall 'a 'r 'e. M 'a 'e -> MR 'a 'r 'e +let liftR m = try_catch m (fun e -> throw (Right e)) + +(* Catch exceptions in the presence of early returns *) +val try_catchR : forall 'a 'r 'e1 'e2. MR 'a 'r 'e1 -> ('e1 -> MR 'a 'r 'e2) -> MR 'a 'r 'e2 +let try_catchR m h = + try_catch m + (function + | Left r -> throw (Left r) + | Right e -> h e + end) + + +val read_mem : forall 'a 'b 'e. Bitvector 'a, Bitvector 'b => bool -> read_kind -> 'a -> integer -> M 'b 'e let read_mem dir rk addr sz = let addr = address_lifted_of_bitv (bits_of addr) in let sz = natFromInteger sz in @@ -85,24 +96,24 @@ let read_mem dir rk addr sz = (Done bitv,Nothing) in Read_mem (rk,addr,sz) k -val excl_result : unit -> M bool +val excl_result : forall 'e. unit -> M bool 'e let excl_result () = let k successful = (return successful,Nothing) in Excl_res k -val write_mem_ea : forall 'a. Bitvector 'a => write_kind -> 'a -> integer -> M unit +val write_mem_ea : forall 'a 'e. Bitvector 'a => write_kind -> 'a -> integer -> M unit 'e let write_mem_ea wk addr sz = let addr = address_lifted_of_bitv (bits_of addr) in let sz = natFromInteger sz in Write_ea (wk,addr,sz) (Done (),Nothing) -val write_mem_val : forall 'a. Bitvector 'a => 'a -> M bool +val write_mem_val : forall 'a 'e. Bitvector 'a => 'a -> M bool 'e let write_mem_val v = let v = external_mem_value (bits_of v) in let k successful = (return successful,Nothing) in Write_memv v k -val read_reg_aux : forall 'a. Bitvector 'a => reg_name -> M 'a +val read_reg_aux : forall 'a 'e. Bitvector 'a => reg_name -> M 'a 'e let read_reg_aux reg = let k reg_value = let v = of_bits (internal_reg_value reg_value) in @@ -124,7 +135,7 @@ let read_reg_bitfield reg regfield = let reg_deref = read_reg -val write_reg_aux : forall 'a. Bitvector 'a => reg_name -> 'a -> M unit +val write_reg_aux : forall 'a 'e. Bitvector 'a => reg_name -> 'a -> M unit 'e let write_reg_aux reg_name v = let regval = external_reg_value reg_name (bits_of v) in Write_reg (reg_name,regval) (Done (), Nothing) @@ -150,29 +161,29 @@ 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 +val barrier : forall 'e. barrier_kind -> M unit 'e let barrier bk = Barrier bk (Done (), Nothing) -val footprint : M unit +val footprint : forall 'e. M unit 'e let footprint = Footprint (Done (),Nothing) -val iter_aux : forall 'regs 'e 'a. integer -> (integer -> 'a -> MR unit 'e) -> list 'a -> MR unit 'e +val iter_aux : forall 'a 'e. integer -> (integer -> 'a -> M unit 'e) -> list 'a -> M 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 +val iteri : forall 'a 'e. (integer -> 'a -> M unit 'e) -> list 'a -> M 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 +val iter : forall 'a 'e. ('a -> M unit 'e) -> list 'a -> M 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 +val foreachM_inc : forall 'vars 'e. (integer * integer * integer) -> 'vars -> + (integer -> 'vars -> M 'vars 'e) -> M 'vars 'e let rec foreachM_inc (i,stop,by) vars body = if (by > 0 && i <= stop) || (by < 0 && stop <= i) then @@ -181,8 +192,8 @@ let rec foreachM_inc (i,stop,by) vars body = else return vars -val foreachM_dec : forall 'vars 'r. (integer * integer * integer) -> 'vars -> - (integer -> 'vars -> MR 'vars 'r) -> MR 'vars 'r +val foreachM_dec : forall 'vars 'e. (integer * integer * integer) -> 'vars -> + (integer -> 'vars -> M 'vars 'e) -> M 'vars 'e let rec foreachM_dec (i,stop,by) vars body = if (by > 0 && i >= stop) || (by < 0 && stop >= i) then @@ -194,21 +205,21 @@ val while_PP : forall 'vars. 'vars -> ('vars -> bool) -> ('vars -> 'vars) -> 'va let rec while_PP vars cond body = if cond vars then while_PP (body vars) cond body else vars -val while_PM : forall 'vars 'r. 'vars -> ('vars -> bool) -> - ('vars -> MR 'vars 'r) -> MR 'vars 'r +val while_PM : forall 'vars 'e. 'vars -> ('vars -> bool) -> + ('vars -> M 'vars 'e) -> M 'vars 'e let rec while_PM vars cond body = if cond vars then body vars >>= fun vars -> while_PM vars cond body else return vars -val while_MP : forall 'vars 'r. 'vars -> ('vars -> MR bool 'r) -> - ('vars -> 'vars) -> MR 'vars 'r +val while_MP : forall 'vars 'e. 'vars -> ('vars -> M bool 'e) -> + ('vars -> 'vars) -> M 'vars 'e let rec while_MP vars cond body = cond vars >>= fun cond_val -> if cond_val then while_MP (body vars) cond body else return vars -val while_MM : forall 'vars 'r. 'vars -> ('vars -> MR bool 'r) -> - ('vars -> MR 'vars 'r) -> MR 'vars 'r +val while_MM : forall 'vars 'e. 'vars -> ('vars -> M bool 'e) -> + ('vars -> M 'vars 'e) -> M 'vars 'e let rec while_MM vars cond body = cond vars >>= fun cond_val -> if cond_val then @@ -220,21 +231,21 @@ let rec until_PP vars cond body = let vars = body vars in if (cond vars) then vars else until_PP (body vars) cond body -val until_PM : forall 'vars 'r. 'vars -> ('vars -> bool) -> - ('vars -> MR 'vars 'r) -> MR 'vars 'r +val until_PM : forall 'vars 'e. 'vars -> ('vars -> bool) -> + ('vars -> M 'vars 'e) -> M 'vars 'e let rec until_PM vars cond body = body vars >>= fun vars -> if (cond vars) then return vars else until_PM vars cond body -val until_MP : forall 'vars 'r. 'vars -> ('vars -> MR bool 'r) -> - ('vars -> 'vars) -> MR 'vars 'r +val until_MP : forall 'vars 'e. 'vars -> ('vars -> M bool 'e) -> + ('vars -> 'vars) -> M 'vars 'e let rec until_MP vars cond body = let vars = body vars in cond vars >>= fun cond_val -> if cond_val then return vars else until_MP vars cond body -val until_MM : forall 'vars 'r. 'vars -> ('vars -> MR bool 'r) -> - ('vars -> MR 'vars 'r) -> MR 'vars 'r +val until_MM : forall 'vars 'e. 'vars -> ('vars -> M bool 'e) -> + ('vars -> M 'vars 'e) -> M 'vars 'e let rec until_MM vars cond body = body vars >>= fun vars -> cond vars >>= fun cond_val -> diff --git a/src/gen_lib/state.lem b/src/gen_lib/state.lem index fa0fcd24..f9011323 100644 --- a/src/gen_lib/state.lem +++ b/src/gen_lib/state.lem @@ -23,55 +23,79 @@ let init_state regs = 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) - -(* By default, we use strings to distinguish between different types of exceptions *) -type M 'regs 'a = ME 'regs 'a string +type ex 'e = + | Exit + | Assert of string + | Throw of 'e -(* For early return, we abuse exceptions by throwing and catching - the return value. The exception type is "either 'r string", where "Right e" - represents a proper exception and "Left r" an early return of value "r". *) -type MR 'regs 'a 'r = ME 'regs 'a (either 'r string) +type result 'a 'e = + | Value of 'a + | Exception of (ex 'e) -val liftR : forall 'a 'r 'regs. M 'regs 'a -> MR 'regs 'a 'r -let liftR m s = List.map (function - | (Left a, s') -> (Left a, s') - | (Right e, s') -> (Right (Right e), s') - end) (m s) +(* State, nondeterminism and exception monad with result value type 'a + and exception type 'e. *) +type M 'regs 'a 'e = sequential_state 'regs -> list (result 'a 'e * sequential_state 'regs) -val return : forall 'regs 'a 'e. 'a -> ME 'regs 'a 'e -let return a s = [(Left a,s)] +val return : forall 'regs 'a 'e. 'a -> M 'regs 'a 'e +let return a s = [(Value a,s)] -val bind : forall 'regs 'a 'b 'e. ME 'regs 'a 'e -> ('a -> ME 'regs 'b 'e) -> ME 'regs 'b 'e +val bind : forall 'regs 'a 'b 'e. M 'regs 'a 'e -> ('a -> M 'regs 'b 'e) -> M 'regs 'b 'e let bind m f (s : sequential_state 'regs) = List.concatMap (function - | (Left a, s') -> f a s' - | (Right e, s') -> [(Right e, s')] + | (Value a, s') -> f a s' + | (Exception e, s') -> [(Exception e, s')] end) (m s) let inline (>>=) = bind -val (>>): forall 'regs 'b 'e. ME 'regs unit 'e -> ME 'regs 'b 'e -> ME 'regs 'b 'e -let inline (>>) m n = m >>= fun _ -> n +val (>>): forall 'regs 'b 'e. M 'regs unit 'e -> M 'regs 'b 'e -> M 'regs 'b 'e +let inline (>>) m n = m >>= fun (_ : unit) -> n -val exit : forall 'regs 'e 'a. 'e -> M 'regs 'a -let exit _ s = [(Right "exit", s)] +val throw : forall 'regs 'a 'e. 'e -> M 'regs 'a 'e +let throw e s = [(Exception (Throw e), s)] -val assert_exp : forall 'regs. bool -> string -> M 'regs unit -let assert_exp exp msg s = if exp then [(Left (), s)] else [(Right msg, s)] +val try_catch : forall 'regs 'a 'e1 'e2. M 'regs 'a 'e1 -> ('e1 -> M 'regs 'a 'e2) -> M 'regs 'a 'e2 +let try_catch m h s = + List.concatMap (function + | (Value a, s') -> return a s' + | (Exception (Throw e), s') -> h e s' + | (Exception Exit, s') -> [(Exception Exit, s')] + | (Exception (Assert msg), s') -> [(Exception (Assert msg), s')] + end) (m s) -val early_return : forall 'regs 'a 'r. 'r -> MR 'regs 'a 'r -let early_return r s = [(Right (Left r), s)] +val exit : forall 'regs 'e 'a. unit -> M 'regs 'a 'e +let exit () s = [(Exception Exit, s)] -val catch_early_return : forall 'regs 'a. MR 'regs 'a 'a -> M 'regs 'a -let catch_early_return m s = - List.map +val assert_exp : forall 'regs 'e. bool -> string -> M 'regs unit 'e +let assert_exp exp msg s = if exp then [(Value (), s)] else [(Exception (Assert msg), s)] + +(* For early return, we abuse exceptions by throwing and catching + the return value. The exception type is "either 'r 'e", where "Right e" + represents a proper exception and "Left r" an early return of value "r". *) +type MR 'regs 'a 'r 'e = M 'regs 'a (either 'r 'e) + +val early_return : forall 'regs 'a 'r 'e. 'r -> MR 'regs 'a 'r 'e +let early_return r = throw (Left r) + +val catch_early_return : forall 'regs 'a 'e. MR 'regs 'a 'a 'e -> M 'regs 'a 'e +let catch_early_return m = + try_catch m + (function + | Left a -> return a + | Right e -> throw e + end) + +(* Lift to monad with early return by wrapping exceptions *) +val liftR : forall 'a 'r 'regs 'e. M 'regs 'a 'e -> MR 'regs 'a 'r 'e +let liftR m = try_catch m (fun e -> throw (Right e)) + +(* Catch exceptions in the presence of early returns *) +val try_catchR : forall 'regs 'a 'r 'e1 'e2. MR 'regs 'a 'r 'e1 -> ('e1 -> MR 'regs 'a 'r 'e2) -> MR 'regs 'a 'r 'e2 +let try_catchR m h = + try_catch m (function - | (Right (Left a), s') -> (Left a, s') - | (Right (Right e), s') -> (Right e, s') - | (Left a, s') -> (Left a, s') - end) (m s) + | Left r -> throw (Left r) + | Right e -> h e + end) val range : integer -> integer -> list integer let rec range i j = @@ -103,20 +127,20 @@ let is_exclusive = function end -val read_mem : forall 'regs 'a 'b. Bitvector 'a, Bitvector 'b => bool -> read_kind -> 'a -> integer -> M 'regs 'b +val read_mem : forall 'regs 'a 'b 'e. Bitvector 'a, Bitvector 'b => bool -> read_kind -> 'a -> integer -> M 'regs 'b 'e let read_mem dir read_kind addr sz state = let addr = unsigned addr in let addrs = range addr (addr+sz-1) in let memory_value = List.map (fun addr -> Map_extra.find addr state.memstate) addrs in let value = of_bits (Sail_values.internal_mem_value dir memory_value) in if is_exclusive read_kind - then [(Left value, <| state with last_exclusive_operation_was_load = true |>)] - else [(Left value, state)] + then [(Value value, <| state with last_exclusive_operation_was_load = true |>)] + else [(Value value, state)] (* caps are aligned at 32 bytes *) let cap_alignment = (32 : integer) -val read_tag : forall 'regs 'a. Bitvector 'a => bool -> read_kind -> 'a -> M 'regs bitU +val read_tag : forall 'regs 'a 'e. Bitvector 'a => bool -> read_kind -> 'a -> M 'regs bitU 'e let read_tag dir read_kind addr state = let addr = (unsigned addr) / cap_alignment in let tag = match (Map.lookup addr state.tagstate) with @@ -124,20 +148,20 @@ let read_tag dir read_kind addr state = | Nothing -> B0 end in if is_exclusive read_kind - then [(Left tag, <| state with last_exclusive_operation_was_load = true |>)] - else [(Left tag, state)] + then [(Value tag, <| state with last_exclusive_operation_was_load = true |>)] + else [(Value tag, state)] -val excl_result : forall 'regs. unit -> M 'regs bool +val excl_result : forall 'regs 'e. unit -> M 'regs bool 'e let excl_result () state = let success = - (Left true, <| state with last_exclusive_operation_was_load = false |>) in - (Left false, state) :: if state.last_exclusive_operation_was_load then [success] else [] + (Value true, <| state with last_exclusive_operation_was_load = false |>) in + (Value false, state) :: if state.last_exclusive_operation_was_load then [success] else [] -val write_mem_ea : forall 'regs 'a. Bitvector 'a => write_kind -> 'a -> integer -> M 'regs unit +val write_mem_ea : forall 'regs 'a 'e. Bitvector 'a => write_kind -> 'a -> integer -> M 'regs unit 'e let write_mem_ea write_kind addr sz state = - [(Left (), <| state with write_ea = Just (write_kind,unsigned addr,sz) |>)] + [(Value (), <| state with write_ea = Just (write_kind,unsigned addr,sz) |>)] -val write_mem_val : forall 'a 'regs 'b. Bitvector 'a => 'a -> M 'regs bool +val write_mem_val : forall 'a 'regs 'b 'e. Bitvector 'a => 'a -> M 'regs bool 'e let write_mem_val v state = let (write_kind,addr,sz) = match state.write_ea with | Nothing -> failwith "write ea has not been announced yet" @@ -147,27 +171,27 @@ let write_mem_val v state = let addresses_with_value = List.zip addrs v in let memstate = List.foldl (fun mem (addr,v) -> Map.insert addr v mem) state.memstate addresses_with_value in - [(Left true, <| state with memstate = memstate |>)] + [(Value true, <| state with memstate = memstate |>)] -val write_tag : forall 'regs. bitU -> M 'regs bool +val write_tag : forall 'regs 'e. bitU -> M 'regs bool 'e let write_tag t state = let (write_kind,addr,sz) = match state.write_ea with | Nothing -> failwith "write ea has not been announced yet" | Just write_ea -> write_ea end in let taddr = addr / cap_alignment in let tagstate = Map.insert taddr t state.tagstate in - [(Left true, <| state with tagstate = tagstate |>)] + [(Value true, <| state with tagstate = tagstate |>)] -val read_reg : forall 'regs 'a. register_ref 'regs 'a -> M 'regs 'a +val read_reg : forall 'regs 'a 'e. register_ref 'regs 'a -> M 'regs 'a 'e let read_reg reg state = let v = reg.read_from state.regstate in - [(Left v,state)] + [(Value v,state)] (*let read_reg_range reg i j state = let v = slice (get_reg state (name_of_reg reg)) i j in - [(Left (vec_to_bvec v),state)] + [(Value (vec_to_bvec v),state)] let read_reg_bit reg i state = let v = access (get_reg state (name_of_reg reg)) i in - [(Left v,state)] + [(Value v,state)] let read_reg_field reg regfield = let (i,j) = register_field_indices reg regfield in read_reg_range reg i j @@ -177,17 +201,17 @@ let read_reg_bitfield reg regfield = let reg_deref = read_reg -val write_reg : forall 'regs 'a. register_ref 'regs 'a -> 'a -> M 'regs unit +val write_reg : forall 'regs 'a 'e. register_ref 'regs 'a -> 'a -> M 'regs unit 'e let write_reg reg v state = - [(Left (), <| state with regstate = reg.write_to state.regstate v |>)] + [(Value (), <| 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 +val update_reg : forall 'regs 'a 'b 'e. register_ref 'regs 'a -> ('a -> 'b -> 'a) -> 'b -> M 'regs unit 'e let update_reg reg f v state = let current_value = get_reg state reg in let new_value = f current_value v in - [(Left (), set_reg state reg new_value)] + [(Value (), set_reg state reg new_value)] let write_reg_field reg regfield = update_reg reg regfield.set_field @@ -219,26 +243,26 @@ let update_reg_field_bit regfield i reg_val bit = regfield.set_field reg_val new_field_value let write_reg_field_bit reg regfield i = update_reg reg (update_reg_field_bit regfield i) -val barrier : forall 'regs. barrier_kind -> M 'regs unit +val barrier : forall 'regs 'e. barrier_kind -> M 'regs unit 'e let barrier _ = return () -val footprint : forall 'regs. M 'regs unit +val footprint : forall 'regs 'e. M 'regs unit 'e 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 +val iter_aux : forall 'regs 'e 'a. integer -> (integer -> 'a -> M 'regs unit 'e) -> list 'a -> M '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 +val iteri : forall 'regs 'e 'a. (integer -> 'a -> M 'regs unit 'e) -> list 'a -> M '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 +val iter : forall 'regs 'e 'a. ('a -> M 'regs unit 'e) -> list 'a -> M '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 + (integer -> 'vars -> M 'regs 'vars 'e) -> M 'regs 'vars 'e let rec foreachM_inc (i,stop,by) vars body = if (by > 0 && i <= stop) || (by < 0 && stop <= i) then @@ -248,7 +272,7 @@ 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 + (integer -> 'vars -> M 'regs 'vars 'e) -> M 'regs 'vars 'e let rec foreachM_dec (i,stop,by) vars body = if (by > 0 && i >= stop) || (by < 0 && stop >= i) then @@ -261,20 +285,20 @@ let rec while_PP vars cond body = if cond vars then while_PP (body vars) cond body else vars val while_PM : forall 'regs 'vars 'e. 'vars -> ('vars -> bool) -> - ('vars -> ME 'regs 'vars 'e) -> ME 'regs 'vars 'e + ('vars -> M 'regs 'vars 'e) -> M 'regs 'vars 'e let rec while_PM vars cond body = if cond vars then body vars >>= fun vars -> while_PM vars cond body else return vars -val while_MP : forall 'regs 'vars 'e. 'vars -> ('vars -> ME 'regs bool 'e) -> - ('vars -> 'vars) -> ME 'regs 'vars 'e +val while_MP : forall 'regs 'vars 'e. 'vars -> ('vars -> M 'regs bool 'e) -> + ('vars -> 'vars) -> M 'regs 'vars 'e let rec while_MP vars cond body = cond vars >>= fun cond_val -> if cond_val then while_MP (body vars) cond body else return vars -val while_MM : forall 'regs 'vars 'e. 'vars -> ('vars -> ME 'regs bool 'e) -> - ('vars -> ME 'regs 'vars 'e) -> ME 'regs 'vars 'e +val while_MM : forall 'regs 'vars 'e. 'vars -> ('vars -> M 'regs bool 'e) -> + ('vars -> M 'regs 'vars 'e) -> M 'regs 'vars 'e let rec while_MM vars cond body = cond vars >>= fun cond_val -> if cond_val then @@ -287,20 +311,20 @@ let rec until_PP vars cond body = if (cond vars) then vars else until_PP (body vars) cond body val until_PM : forall 'regs 'vars 'e. 'vars -> ('vars -> bool) -> - ('vars -> ME 'regs 'vars 'e) -> ME 'regs 'vars 'e + ('vars -> M 'regs 'vars 'e) -> M 'regs 'vars 'e let rec until_PM vars cond body = body vars >>= fun vars -> if (cond vars) then return vars else until_PM vars cond body -val until_MP : forall 'regs 'vars 'e. 'vars -> ('vars -> ME 'regs bool 'e) -> - ('vars -> 'vars) -> ME 'regs 'vars 'e +val until_MP : forall 'regs 'vars 'e. 'vars -> ('vars -> M 'regs bool 'e) -> + ('vars -> 'vars) -> M 'regs 'vars 'e let rec until_MP vars cond body = let vars = body vars in cond vars >>= fun cond_val -> if cond_val then return vars else until_MP vars cond body -val until_MM : forall 'regs 'vars 'e. 'vars -> ('vars -> ME 'regs bool 'e) -> - ('vars -> ME 'regs 'vars 'e) -> ME 'regs 'vars 'e +val until_MM : forall 'regs 'vars 'e. 'vars -> ('vars -> M 'regs bool 'e) -> + ('vars -> M 'regs 'vars 'e) -> M 'regs 'vars 'e let rec until_MM vars cond body = body vars >>= fun vars -> cond vars >>= fun cond_val -> diff --git a/src/lem_interp/sail_impl_base.lem b/src/lem_interp/sail_impl_base.lem index 421219da..368f7505 100644 --- a/src/lem_interp/sail_impl_base.lem +++ b/src/lem_interp/sail_impl_base.lem @@ -905,36 +905,35 @@ end (* the address_lifted types should go away here and be replaced by address *) type with_aux 'o = 'o * maybe ((unit -> (string * string)) * ((list (reg_name * register_value)) -> list event)) -type outcome_r 'a 'r = +type outcome 'a 'e = (* Request to read memory, value is location to read, integer is size to read, followed by registers that were used in computing that size *) - | Read_mem of (read_kind * address_lifted * nat) * (memory_value -> with_aux (outcome_r 'a 'r)) + | Read_mem of (read_kind * address_lifted * nat) * (memory_value -> with_aux (outcome 'a 'e)) (* Tell the system a write is imminent, at address lifted, of size nat *) - | Write_ea of (write_kind * address_lifted * nat) * (with_aux (outcome_r 'a 'r)) + | Write_ea of (write_kind * address_lifted * nat) * (with_aux (outcome 'a 'e)) (* Request the result of store-exclusive *) - | Excl_res of (bool -> with_aux (outcome_r 'a 'r)) + | Excl_res of (bool -> with_aux (outcome 'a 'e)) (* Request to write memory at last signalled address. Memory value should be 8 times the size given in ea signal *) - | Write_memv of memory_value * (bool -> with_aux (outcome_r 'a 'r)) + | Write_memv of memory_value * (bool -> with_aux (outcome 'a 'e)) (* Request a memory barrier *) - | Barrier of barrier_kind * with_aux (outcome_r 'a 'r) + | Barrier of barrier_kind * with_aux (outcome 'a 'e) (* Tell the system to dynamically recalculate dependency footprint *) - | Footprint of with_aux (outcome_r 'a 'r) + | Footprint of with_aux (outcome 'a 'e) (* Request to read register, will track dependency when mode.track_values *) - | Read_reg of reg_name * (register_value -> with_aux (outcome_r 'a 'r)) + | Read_reg of reg_name * (register_value -> with_aux (outcome 'a 'e)) (* Request to write register *) - | Write_reg of (reg_name * register_value) * with_aux (outcome_r 'a 'r) + | Write_reg of (reg_name * register_value) * with_aux (outcome 'a 'e) | Escape of maybe string (*Result of a failed assert with possible error message to report*) | Fail of maybe string - (* Early return with value of type 'r *) - | Return of 'r - | Internal of (maybe string * maybe (unit -> string)) * with_aux (outcome_r 'a 'r) + (* Exception of type 'e *) + | Exception of 'e + | Internal of (maybe string * maybe (unit -> string)) * with_aux (outcome 'a 'e) | Done of 'a | Error of string -type outcome 'a = outcome_r 'a unit -type outcome_s 'a = with_aux (outcome 'a) +type outcome_s 'a 'e = with_aux (outcome 'a 'e) (* first string : output of instruction_stack_to_string second string: output of local_variables_to_string *) diff --git a/src/monomorphise.ml b/src/monomorphise.ml index 8730b019..0cbeda49 100644 --- a/src/monomorphise.ml +++ b/src/monomorphise.ml @@ -102,7 +102,7 @@ let rec subst_nc substs (NC_aux (nc,l) as n_constraint) = begin match KBindings.find kid substs with | Nexp_aux (Nexp_constant i,_) -> - if List.mem i is then re NC_true else re NC_false + if List.exists (fun j -> Big_int.eq_big_int i j) is then re NC_true else re NC_false | nexp -> raise (Reporting_basic.err_general l ("Unable to substitute " ^ string_of_nexp nexp ^ diff --git a/src/pretty_print_lem.ml b/src/pretty_print_lem.ml index 96f312fb..6a3d1293 100644 --- a/src/pretty_print_lem.ml +++ b/src/pretty_print_lem.ml @@ -249,12 +249,12 @@ let doc_typ_lem, doc_atomic_typ_lem = | Typ_fn(arg,ret,efct) -> let ret_typ = if effectful efct - then separate space [string "_M"; fn_typ true ret] + then separate space [string "M"; fn_typ true ret] else separate space [fn_typ false ret] in let arg_typs = match arg with | Typ_aux (Typ_tup typs, _) -> - List.map (app_typ true) typs - | _ -> [tup_typ true arg] in + List.map (app_typ false) typs + | _ -> [tup_typ false arg] in let tpp = separate (space ^^ arrow ^^ space) (arg_typs @ [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 @@ -355,7 +355,7 @@ let doc_tannot_lem eff typ = if contains_t_pp_var typ then empty else let ta = doc_typ_lem typ in - if eff then string " : _M " ^^ parens ta + if eff then string " : M " ^^ parens ta else string " : " ^^ ta (* doc_lit_lem gets as an additional parameter the type information from the @@ -685,7 +685,7 @@ let doc_exp_lem, doc_let_lem = contains_t_pp_var (typ_of full_exp) then aexp_needed, epp else - let tannot = separate space [string "_MR"; + let tannot = separate space [string "MR"; 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 @@ -855,7 +855,20 @@ let doc_exp_lem, doc_let_lem = (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;]) + | E_try (e, pexps) -> + if effectful (effect_of e) then + let try_catch = if early_ret then "try_catchR" else "try_catch" in + let epp = + group ((separate space [string try_catch; expY e; string "(function "]) ^/^ + (separate_map (break 1) (doc_case early_ret) pexps) ^/^ + (string "end)")) in + if aexp_needed then parens (align epp) else align epp + else + raise (Reporting_basic.err_todo l "Warning: try-block around pure expression") + | E_throw e -> + let epp = liftR (separate space [string "throw"; expY e]) in + if aexp_needed then parens (align epp) else align epp + | E_exit e -> liftR (separate space [string "exit"; expY e]) | E_assert (e1,e2) -> let epp = liftR (separate space [string "assert_exp"; expY e1; expY e2]) in if aexp_needed then parens (align epp) else align epp @@ -1495,6 +1508,12 @@ let find_registers (Defs defs) = | _ -> acc ) [] defs +let find_exc_typ (Defs defs) = + let is_exc_typ_def = function + | DEF_type td -> string_of_id (id_of_type_def td) = "exception" + | _ -> false in + if List.exists is_exc_typ_def defs then "exception" else "unit" + let doc_regstate_lem registers = let l = Parse_ast.Unknown in let annot = (l, None) in @@ -1528,12 +1547,7 @@ let doc_regstate_lem registers = doc_op equals (string "let initial_regstate") (doc_exp_lem false false exp) else empty in - concat [ - 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" - ], + doc_typdef_lem (TD_aux (regstate, annot)), initregstate let doc_register_refs_lem registers = @@ -1564,6 +1578,7 @@ let pp_defs_lem (types_file,types_modules) (defs_file,defs_modules) d top_line = 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 + let exc_typ = find_exc_typ d in (print types_file) (concat [string "(*" ^^ (string top_line) ^^ string "*)";hardline; @@ -1585,10 +1600,17 @@ let pp_defs_lem (types_file,types_modules) (defs_file,defs_modules) d top_line = hardline; if !opt_sequential then concat [regstate_def; hardline; - hardline; - register_refs] + hardline; + string ("type MR 'a 'r = State.MR regstate 'a 'r " ^ exc_typ); hardline; + string ("type M 'a = State.M regstate 'a " ^ exc_typ); hardline; + hardline; + register_refs + ] else - concat [string "type _MR 'a 'r = MR 'a 'r"; hardline; string "type _M 'a = M 'a"; hardline] + concat [ + string ("type MR 'a 'r = Prompt.MR 'a 'r " ^ exc_typ); hardline; + string ("type M 'a = Prompt.M 'a " ^ exc_typ); hardline + ] ]); (print defs_file) (concat diff --git a/src/rewriter.ml b/src/rewriter.ml index 88fb17a5..31bcb577 100644 --- a/src/rewriter.ml +++ b/src/rewriter.ml @@ -130,12 +130,11 @@ let fix_eff_exp (E_aux (e,((l,_) as annot))) = match snd annot with | E_record_update(e,fexps) -> union_effects (effect_of e) (effect_of_fexps fexps) | E_field (e,_) -> effect_of e - | E_case (e,pexps) -> + | E_case (e,pexps) | E_try (e,pexps) -> List.fold_left union_effects (effect_of e) (List.map effect_of_pexp pexps) | E_let (lb,e) -> union_effects (effect_of_lb lb) (effect_of e) | E_assign (lexp,e) -> union_effects (effect_of_lexp lexp) (effect_of e) - | E_exit e -> union_effects eff (effect_of e) - | E_return e -> union_effects eff (effect_of e) + | E_exit e | E_return e | E_throw e -> union_effects eff (effect_of e) | E_sizeof _ | E_sizeof_internal _ | E_constraint _ -> no_effect | E_assert (c,m) -> union_effects eff (union_eff_exps [c; m]) | E_comment _ | E_comment_struc _ -> no_effect diff --git a/src/rewrites.ml b/src/rewrites.ml index a42335b9..32ffe54a 100644 --- a/src/rewrites.ml +++ b/src/rewrites.ml @@ -2378,6 +2378,11 @@ let rewrite_defs_letbind_effects = n_exp_name exp1 (fun exp1 -> n_pexpL newreturn pexps (fun pexps -> k (rewrap (E_case (exp1,pexps))))) + | E_try (exp1,pexps) -> + let newreturn = effectful exp1 || List.exists effectful_pexp pexps in + n_exp_name exp1 (fun exp1 -> + n_pexpL newreturn pexps (fun pexps -> + k (rewrap (E_try (exp1,pexps))))) | E_let (lb,body) -> n_lb lb (fun lb -> rewrap (E_let (lb,n_exp body k))) @@ -2416,6 +2421,9 @@ let rewrite_defs_letbind_effects = | E_return exp' -> n_exp_name exp' (fun exp' -> k (rewrap (E_return exp'))) + | E_throw exp' -> + n_exp_name exp' (fun exp' -> + k (rewrap (E_throw exp'))) | E_internal_plet _ -> failwith "E_internal_plet should not be here yet" in let rewrite_fun _ (FD_aux (FD_function(recopt,tannotopt,effectopt,funcls),fdannot)) = -- cgit v1.2.3 From 6f3bf52cef2bd210fbad96f189bf3d6e13872fdb Mon Sep 17 00:00:00 2001 From: Alasdair Armstrong Date: Mon, 8 Jan 2018 17:03:19 +0000 Subject: Potential fix for bug where different quantifer order in existentials will break alpha-equivalence. --- src/type_check.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/type_check.ml b/src/type_check.ml index 5bd633ee..d03673d9 100644 --- a/src/type_check.ml +++ b/src/type_check.ml @@ -1583,7 +1583,7 @@ let rec alpha_equivalent env typ1 typ2 = let kids = List.map (fun kid -> (kid, new_kid ())) kids in let nc = List.fold_left (fun nc (kid, nk) -> nc_subst_nexp kid (Nexp_var nk) nc) nc kids in let typ = List.fold_left (fun nc (kid, nk) -> typ_subst_nexp kid (Nexp_var nk) nc) typ kids in - Typ_exist (List.map snd kids, nc, typ) + Typ_exist (List.sort Kid.compare (List.map snd kids), nc, typ) | Typ_app (id, args) -> Typ_app (id, List.map relabel_arg args) in -- cgit v1.2.3 From ffcf8a814cdd23eaff9286835478afb66fbb0029 Mon Sep 17 00:00:00 2001 From: Alasdair Armstrong Date: Mon, 8 Jan 2018 19:19:17 +0000 Subject: Improved fix for alpha-equivalence re-ordering issue --- src/type_check.ml | 37 ++++++++++++++++++++++++++++++++++++- 1 file changed, 36 insertions(+), 1 deletion(-) diff --git a/src/type_check.ml b/src/type_check.ml index d03673d9..dee17fee 100644 --- a/src/type_check.ml +++ b/src/type_check.ml @@ -1569,6 +1569,39 @@ let uv_nexp_constraint env (kid, uvar) = | U_nexp nexp -> Env.add_constraint (nc_eq (nvar kid) nexp) env | _ -> env +(* The kid_order function takes a set of Int-kinded kids, and returns + a list of those kids in the order they appear in a type, as well as + a set containing all the kids that did not occur in the type. We + only care about Int-kinded kids because those are the only type + that can appear in an existential. *) + +let rec kid_order_nexp kids (Nexp_aux (aux, l) as nexp) = + match aux with + | Nexp_var kid when KidSet.mem kid kids -> ([kid], KidSet.remove kid kids) + | Nexp_var _ | Nexp_id _ | Nexp_constant _ -> ([], kids) + | Nexp_exp nexp | Nexp_neg nexp -> kid_order_nexp kids nexp + | Nexp_times (nexp1, nexp2) | Nexp_sum (nexp1, nexp2) | Nexp_minus (nexp1, nexp2) -> + let (ord, kids) = kid_order_nexp kids nexp1 in + let (ord', kids) = kid_order_nexp kids nexp2 in + (ord @ ord', kids) + | Nexp_app (id, nexps) -> + List.fold_left (fun (ord, kids) nexp -> let (ord', kids) = kid_order_nexp kids nexp in (ord @ ord', kids)) ([], kids) nexps + +let rec kid_order kids (Typ_aux (aux, l) as typ) = + match aux with + | Typ_var kid when KidSet.mem kid kids -> ([kid], KidSet.remove kid kids) + | Typ_id _ | Typ_var _ -> ([], kids) + | Typ_tup typs -> + List.fold_left (fun (ord, kids) typ -> let (ord', kids) = kid_order kids typ in (ord @ ord', kids)) ([], kids) typs + | Typ_app (_, args) -> + List.fold_left (fun (ord, kids) arg -> let (ord', kids) = kid_order_arg kids arg in (ord @ ord', kids)) ([], kids) args + | Typ_fn _ | Typ_exist _ -> typ_error l ("Existential or function type cannot appear within existential type: " ^ string_of_typ typ) +and kid_order_arg kids (Typ_arg_aux (aux, l) as arg) = + match aux with + | Typ_arg_typ typ -> kid_order kids typ + | Typ_arg_nexp nexp -> kid_order_nexp kids nexp + | Typ_arg_order _ -> ([], kids) + let rec alpha_equivalent env typ1 typ2 = let counter = ref 0 in let new_kid () = let kid = mk_kid ("alpha#" ^ string_of_int !counter) in (incr counter; kid) in @@ -1583,7 +1616,9 @@ let rec alpha_equivalent env typ1 typ2 = let kids = List.map (fun kid -> (kid, new_kid ())) kids in let nc = List.fold_left (fun nc (kid, nk) -> nc_subst_nexp kid (Nexp_var nk) nc) nc kids in let typ = List.fold_left (fun nc (kid, nk) -> typ_subst_nexp kid (Nexp_var nk) nc) typ kids in - Typ_exist (List.sort Kid.compare (List.map snd kids), nc, typ) + let kids = List.map snd kids in + let (kids, _) = kid_order (KidSet.of_list kids) typ in + Typ_exist (kids, nc, typ) | Typ_app (id, args) -> Typ_app (id, List.map relabel_arg args) in -- cgit v1.2.3