From bab7c8bff9fd6dd42e4fa9908303d2d8ad3c33fc Mon Sep 17 00:00:00 2001 From: Brian Campbell Date: Fri, 3 Nov 2017 15:33:20 +0000 Subject: Make nexp_simp a little smarter --- src/ast_util.ml | 3 +++ 1 file changed, 3 insertions(+) (limited to 'src') diff --git a/src/ast_util.ml b/src/ast_util.ml index 707ec93c..7d366803 100644 --- a/src/ast_util.ml +++ b/src/ast_util.ml @@ -198,6 +198,9 @@ and nexp_simp_aux = function let (Nexp_aux (n2_simp, _) as n2) = nexp_simp n2 in match n1_simp, n2_simp with | Nexp_constant c1, Nexp_constant c2 -> Nexp_constant (c1 - c2) + (* A vector range x['n-1 .. 0] can result in the size "('n-1) - -1" *) + | Nexp_minus (Nexp_aux (n,_), Nexp_aux (Nexp_constant c1,_)), Nexp_constant c2 + when c1 = -c2 -> n | _, _ -> Nexp_minus (n1, n2) end | nexp -> nexp -- cgit v1.2.3 From b93a5387d0565d0bfc452146e7335fc4b46110fa Mon Sep 17 00:00:00 2001 From: Brian Campbell Date: Fri, 3 Nov 2017 15:33:59 +0000 Subject: Make sure simple parameter sizes appear in Lem mwords output --- src/pretty_print_lem.ml | 48 +++++++++++++++++++++++++----------------------- 1 file changed, 25 insertions(+), 23 deletions(-) (limited to 'src') diff --git a/src/pretty_print_lem.ml b/src/pretty_print_lem.ml index 7a29579b..b9ef1aec 100644 --- a/src/pretty_print_lem.ml +++ b/src/pretty_print_lem.ml @@ -316,32 +316,33 @@ let doc_typ_lem, doc_atomic_typ_lem = | Typ_arg_order o -> empty in typ', atomic_typ - (* Check for variables in types that would be pretty-printed. In particular, in case of vector types, only the element type and the 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 (Typ_aux (t,a) as typ) = match t with +let rec contains_t_pp_var mwords (Typ_aux (t,a) as typ) = match t with | Typ_wild -> true | Typ_id _ -> false | Typ_var _ -> true | Typ_exist _ -> true - | 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_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_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 - not (is_nexp_constant (nexp_simp length)) - 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 + 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 | 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 typ then empty + if contains_t_pp_var mwords typ then empty else let ta = doc_typ_lem sequential mwords typ in if eff then string " : _M " ^^ parens ta @@ -373,7 +374,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 typ then empty else doc_tannot_lem sequential mwords false typ in + let ta = if contains_t_pp_var mwords typ then empty + else doc_tannot_lem sequential mwords false typ in parens ((utf8string "(failwith \"undefined value of unsupported type\")") ^^ ta)) | _ -> utf8string "(failwith \"undefined value of unsupported type\")") @@ -480,7 +482,7 @@ let rec doc_pat_lem sequential mwords apat_needed (P_aux (p,(l,annot)) as pa) = | P_as(p,id) -> parens (separate space [doc_pat_lem sequential mwords true p; string "as"; doc_id_lem id]) | P_typ(typ,p) -> let doc_p = doc_pat_lem sequential mwords true p in - if contains_t_pp_var typ then doc_p + if contains_t_pp_var mwords typ then doc_p else parens (doc_op colon doc_p (doc_typ_lem sequential mwords typ)) | P_vector pats -> let ppp = @@ -625,7 +627,7 @@ let doc_exp_lem, doc_let_lem = (* let t = Env.base_typ_of (env_of full_exp) (typ_of full_exp) in let (call,ta,aexp_needed) = if is_bitvector_typ t then - if not (contains_t_pp_var t) + if not (contains_t_pp_var mwords t) then ("bitvector_concat", doc_tannot_lem sequential mwords false t, true) else ("bitvector_concat", empty, aexp_needed) else ("vector_concat",empty,aexp_needed) in @@ -704,7 +706,7 @@ let doc_exp_lem, doc_let_lem = let (taepp,aexp_needed) = let t = Env.base_typ_of (env_of full_exp) (typ_of full_exp) in let eff = effect_of full_exp in - if typ_needs_printed t && not (contains_t_pp_var t) + if typ_needs_printed t && not (contains_t_pp_var mwords t) then (align epp ^^ (doc_tannot_lem sequential mwords (effectful eff) t), true) else (epp, aexp_needed) in if aexp_needed then parens (align taepp) else taepp*) @@ -804,13 +806,13 @@ let doc_exp_lem, doc_let_lem = let (epp,aexp_needed) = if has_effect eff BE_rreg then let epp = align (string "read_reg_range" ^^ space ^^ expY v ^//^ expY e1 ^//^ expY e2) in - if typ_needs_printed t && not (contains_t_pp_var t) + if typ_needs_printed t && not (contains_t_pp_var mwords t) then (epp ^^ doc_tannot_lem sequential mwords true t, true) else (epp, aexp_needed) else if is_bitvector_typ t then let bepp = string "bvslice" ^^ space ^^ expY v ^//^ expY e1 ^//^ expY e2 in - if not (contains_t_pp_var t) + if not (contains_t_pp_var mwords t) then (bepp ^^ doc_tannot_lem sequential mwords false t, true) else (bepp, aexp_needed) else (string "slice" ^^ space ^^ expY v ^//^ expY e1 ^//^ expY e2, aexp_needed) in @@ -860,7 +862,7 @@ let doc_exp_lem, doc_let_lem = | Tid "bit" | Tabbrev (_,{t=Tid "bit"}) -> "read_reg_bitfield" | _ -> "read_reg_field" in let ta = - if typ_needs_printed t && not (contains_t_pp_var t) + if typ_needs_printed t && not (contains_t_pp_var mwords t) then doc_tannot_lem sequential mwords true t else empty in let epp = separate space [string call;string reg;string_lit(string field)] ^^ ta in if aexp_needed then parens (align epp) else epp @@ -868,7 +870,7 @@ let doc_exp_lem, doc_let_lem = let (call,ta) = if has_effect eff BE_rreg then let ta = - if typ_needs_printed t && not (contains_t_pp_var t) + if typ_needs_printed t && not (contains_t_pp_var mwords t) then doc_tannot_lem sequential mwords true t else empty in ("read_two_regs", ta) else @@ -881,7 +883,7 @@ let doc_exp_lem, doc_let_lem = separate space [string "read_reg_bit";string reg;doc_int start] else let ta = - if typ_needs_printed t && not (contains_t_pp_var t) + if typ_needs_printed t && not (contains_t_pp_var mwords t) then doc_tannot_lem sequential mwords true t else empty in separate space [string "read_reg_range";string reg;doc_int start;doc_int stop] ^^ ta in if aexp_needed then parens (align epp) else epp @@ -893,7 +895,7 @@ let doc_exp_lem, doc_let_lem = | Base((_,t),External _,_,_,_,_) -> (* TODO: Does this case still exist with the new type checker? *) let epp = string "read_reg" ^^ space ^^ expY e in - if typ_needs_printed t && not (contains_t_pp_var t) + if typ_needs_printed t && not (contains_t_pp_var mwords t) then parens (epp ^^ doc_tannot_lem sequential mwords true t) else epp | Base((_,t),_,_,_,_,_) -> (match typ with @@ -1123,7 +1125,7 @@ let doc_exp_lem, doc_let_lem = | _ -> string name ^//^ parens (expN e1 ^^ comma ^/^ expN e2)) in let (epp,aexp_needed) = - if typ_needs_printed t && not (contains_t_pp_var t) + if typ_needs_printed t && not (contains_t_pp_var mwords t) then (parens epp ^^ doc_tannot_lem sequential mwords false t, true) else (epp, aexp_needed) in if aexp_needed then parens (align epp) else epp @@ -1162,7 +1164,7 @@ let doc_exp_lem, doc_let_lem = | E_return r -> let ret_monad = if sequential then " : MR regstate" else " : MR" in let ta = - if contains_t_pp_var (typ_of full_exp) || contains_t_pp_var (typ_of r) + if contains_t_pp_var mwords (typ_of full_exp) || contains_t_pp_var mwords (typ_of r) then empty else separate space [string ret_monad; @@ -1549,7 +1551,7 @@ 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_fun_body_lem sequential mwords exp = - let early_ret = contains_early_return exp in + let early_ret =contains_early_return exp in let doc_exp = doc_exp_lem sequential mwords early_ret false exp in if early_ret then align (string "catch_early_return" ^//^ parens (doc_exp)) @@ -1689,7 +1691,7 @@ let doc_spec_lem sequential mwords (VS_aux (valspec,annot)) = match valspec with | VS_val_spec (typschm,id,None,_) -> (* let (TypSchm_aux (TypSchm_ts (tq, typ), _)) = typschm in - if contains_t_pp_var typ then empty else *) + 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 | VS_val_spec (_,_,Some _,_) -> empty -- cgit v1.2.3