diff options
| -rw-r--r-- | src/ast_util.ml | 39 | ||||
| -rw-r--r-- | src/ast_util.mli | 3 | ||||
| -rw-r--r-- | src/pretty_print_lem.ml | 52 |
3 files changed, 93 insertions, 1 deletions
diff --git a/src/ast_util.ml b/src/ast_util.ml index daaf5725..2cc9d5a5 100644 --- a/src/ast_util.ml +++ b/src/ast_util.ml @@ -618,8 +618,15 @@ let rec simplify_nexp (Nexp_aux (nexp, l)) = rewrap (Nexp_constant (op i1 i2)) | n1, n2 -> rewrap (c n1 n2)) in match nexp with + | Nexp_times (Nexp_aux (Nexp_constant 1,_),n') + | Nexp_times (n',Nexp_aux (Nexp_constant 1,_)) + -> n' | Nexp_times (n1, n2) -> try_binop ( * ) n1 n2 (fun n1 n2 -> Nexp_times (n1, n2)) | Nexp_sum (n1, n2) -> try_binop ( + ) n1 n2 (fun n1 n2 -> Nexp_sum (n1, n2)) + | Nexp_minus (n', Nexp_aux (Nexp_constant 0,_)) -> n' + (* A vector range x['n-1 .. 0] can result in the size "('n-1) - -1" *) + | Nexp_minus (Nexp_aux (Nexp_minus (n', Nexp_aux (Nexp_constant 1,_)),_), + Nexp_aux (Nexp_constant (-1),_)) -> n' | Nexp_minus (n1, n2) -> try_binop ( - ) n1 n2 (fun n1 n2 -> Nexp_minus (n1, n2)) (* | Nexp_exp n -> (match simplify_nexp n with @@ -709,3 +716,35 @@ let has_effect (Effect_aux (eff,_)) searched_for = match eff with | Effect_var _ -> raise (Reporting_basic.err_unreachable Parse_ast.Unknown "has_effect called on effect variable") + +let rec tyvars_of_nexp (Nexp_aux (nexp,_)) = + match nexp with + | Nexp_id _ + | Nexp_constant _ -> KidSet.empty + | Nexp_var kid -> KidSet.singleton kid + | Nexp_times (n1,n2) + | Nexp_sum (n1,n2) + | Nexp_minus (n1,n2) -> KidSet.union (tyvars_of_nexp n1) (tyvars_of_nexp n2) + | Nexp_exp n + | Nexp_neg n -> tyvars_of_nexp n + +let rec tyvars_of_typ (Typ_aux (t,_)) = + match t with + | Typ_wild + | Typ_id _ -> KidSet.empty + | Typ_var kid -> KidSet.singleton kid + | Typ_fn (t1,t2,_) -> KidSet.union (tyvars_of_typ t1) (tyvars_of_typ t2) + | Typ_tup ts -> + List.fold_left (fun s t -> KidSet.union s (tyvars_of_typ t)) + KidSet.empty ts + | Typ_app (_,tas) -> + List.fold_left (fun s ta -> KidSet.union s (tyvars_of_typ_arg ta)) + KidSet.empty tas + | Typ_exist (kids,_,t) -> + let s = tyvars_of_typ t in + List.fold_left (fun s k -> KidSet.remove k s) s kids +and tyvars_of_typ_arg (Typ_arg_aux (ta,_)) = + match ta with + | Typ_arg_nexp nexp -> tyvars_of_nexp nexp + | Typ_arg_typ typ -> tyvars_of_typ typ + | Typ_arg_order _ -> KidSet.empty diff --git a/src/ast_util.mli b/src/ast_util.mli index 7ab7807a..7e4c9fa0 100644 --- a/src/ast_util.mli +++ b/src/ast_util.mli @@ -225,3 +225,6 @@ val vector_typ_args_of : typ -> nexp * nexp * order * typ val is_order_inc : order -> bool val has_effect : effect -> base_effect_aux -> bool + +val tyvars_of_nexp : nexp -> KidSet.t +val tyvars_of_typ : typ -> KidSet.t diff --git a/src/pretty_print_lem.ml b/src/pretty_print_lem.ml index ac766e89..c03d4040 100644 --- a/src/pretty_print_lem.ml +++ b/src/pretty_print_lem.ml @@ -156,6 +156,45 @@ let doc_nexp_lem (Nexp_aux (nexp, l) as full_nexp) = match nexp with | _ -> raise (Reporting_basic.err_unreachable l ("cannot pretty-print non-atomic nexp \"" ^ string_of_nexp full_nexp ^ "\"")) +(* 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_tyvars_of_typ sequential mwords (Typ_aux (t,_)) = + let trec = lem_tyvars_of_typ sequential mwords in + match t with + | Typ_wild + | Typ_id _ -> KidSet.empty + | Typ_var kid -> KidSet.singleton kid + | Typ_fn (t1,t2,_) -> KidSet.union (trec t1) (trec t2) + | Typ_tup ts -> + List.fold_left (fun s t -> KidSet.union s (trec t)) + KidSet.empty ts + | 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, _)]) -> + KidSet.union + (if mwords then tyvars_of_nexp (simplify_nexp m) else KidSet.empty) + (trec elem_typ) + | Typ_app(Id_aux (Id "register", _), [Typ_arg_aux (Typ_arg_typ etyp, _)]) -> + if sequential then trec etyp else KidSet.empty + | Typ_app(Id_aux (Id "range", _),_) + | Typ_app(Id_aux (Id "implicit", _),_) + | Typ_app(Id_aux (Id "atom", _), _) -> KidSet.empty + | Typ_app (_,tas) -> + List.fold_left (fun s ta -> KidSet.union s (lem_tyvars_of_typ_arg sequential mwords ta)) + KidSet.empty tas + | Typ_exist (kids,_,t) -> + let s = trec t in + List.fold_left (fun s k -> KidSet.remove k s) s kids +and lem_tyvars_of_typ_arg sequential mwords (Typ_arg_aux (ta,_)) = + match ta with + | Typ_arg_nexp nexp -> tyvars_of_nexp nexp + | Typ_arg_typ typ -> lem_tyvars_of_typ sequential mwords typ + | Typ_arg_order _ -> 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 @@ -210,7 +249,7 @@ let doc_typ_lem, doc_atomic_typ_lem = let tpp = (doc_id_lem_type id) ^^ space ^^ (separate_map space (doc_typ_arg_lem sequential mwords) 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, _)) as ty) = match t with + and atomic_typ sequential mwords 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) -> @@ -224,12 +263,23 @@ let doc_typ_lem, doc_atomic_typ_lem = * if we add a new Typ constructor *) let tpp = typ sequential mwords 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 + 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 + ("Existential type variable(s) " ^ + 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 | Typ_arg_nexp n -> doc_nexp_lem (simplify_nexp n) | 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 |