diff options
| -rw-r--r-- | lib/mono_rewrites.sail | 2 | ||||
| -rw-r--r-- | src/monomorphise.ml | 20 |
2 files changed, 11 insertions, 11 deletions
diff --git a/lib/mono_rewrites.sail b/lib/mono_rewrites.sail index 93ad3db5..8259ec47 100644 --- a/lib/mono_rewrites.sail +++ b/lib/mono_rewrites.sail @@ -63,7 +63,7 @@ function slice_slice_concat (xs, i, l, ys, i', l') = { extzv(xs) << l' | extzv(ys) } -val slice_zeros_concat : forall 'n 'p 'q 'r, 'r == 'p + 'q & 'n >= 0 & 'p >= 0 & 'q >= 0 & 'r >= 0. +val slice_zeros_concat : forall 'n 'p 'q 'r, 'r == 'p + 'q & 'n >= 0 & /*'p >= 0 & 'q >= 0 &*/ 'r >= 0. (bits('n), int, atom('p), atom('q)) -> bits('r) effect pure function slice_zeros_concat (xs, i, l, l') = { diff --git a/src/monomorphise.ml b/src/monomorphise.ml index 2124c11e..51de5a25 100644 --- a/src/monomorphise.ml +++ b/src/monomorphise.ml @@ -3687,6 +3687,7 @@ let rewrite_app env typ (id,args) = | Some c -> E_cast (vector_typ (nconstant c) order bittyp, exp) | None -> e in + let rewrap e = E_aux (e, (Unknown, empty_tannot)) in if is_append id then let is_subrange = is_id env (Id "vector_subrange") in let is_slice = is_id env (Id "slice") in @@ -3846,36 +3847,34 @@ let rewrite_app env typ (id,args) = E_aux (E_app (zeros1, [len1]),_)]),_)):: ([] | [_;E_aux (E_id (Id_aux (Id "unsigned",_)),_)]) when is_subrange subrange1 && is_zeros zeros1 && is_append append1 - -> E_app (mk_id "place_subrange", - [vector1; start1; end1; len1]) + -> try_cast_to_typ (rewrap (E_app (mk_id "place_subrange", [vector1; start1; end1; len1]))) | (E_aux (E_app (append1, [E_aux (E_app (slice1, [vector1; start1; length1]), _); E_aux (E_app (zeros1, [length2]),_)]),_)):: ([] | [_;E_aux (E_id (Id_aux (Id "unsigned",_)),_)]) when is_slice slice1 && is_zeros zeros1 && is_append append1 - -> E_app (mk_id "place_slice", - [vector1; start1; length1; length2]) + -> try_cast_to_typ (rewrap (E_app (mk_id "place_slice", [vector1; start1; length1; length2]))) (* If we've already rewritten to slice_slice_concat or subrange_subrange_concat, we can just drop the zero extension because those functions can do it themselves *) | (E_aux (E_cast (_, (E_aux (E_app (Id_aux ((Id "slice_slice_concat" | Id "subrange_subrange_concat"),_) as op, args),_))),_)):: ([] | [_;E_aux (E_id (Id_aux (Id "unsigned",_)),_)]) - -> E_app (op, args) + -> try_cast_to_typ (rewrap (E_app (op, args))) | (E_aux (E_app (Id_aux ((Id "slice_slice_concat" | Id "subrange_subrange_concat"),_) as op, args),_)):: ([] | [_;E_aux (E_id (Id_aux (Id "unsigned",_)),_)]) - -> E_app (op, args) + -> try_cast_to_typ (rewrap (E_app (op, args))) | [E_aux (E_app (slice1, [vector1; start1; length1]),_)] when is_slice slice1 && not (is_constant length1) -> - E_app (mk_id "zext_slice", [vector1; start1; length1]) + try_cast_to_typ (rewrap (E_app (mk_id "zext_slice", [vector1; start1; length1]))) | [E_aux (E_app (ones, [len1]),_); _ (* unnecessary ZeroExtend length *)] when is_ones ones -> - E_app (mk_id "zext_ones", [len1]) + try_cast_to_typ (rewrap (E_app (mk_id "zext_ones", [len1]))) | _ -> E_app (id,args) @@ -4308,9 +4307,10 @@ let rewrite_toplevel_nexps (Defs defs) = | A_typ typ -> A_aux (A_typ (aux typ),l) | A_order _ -> ta_full | A_nexp nexp -> - match find_nexp env nexp_map nexp with + (match find_nexp env nexp_map nexp with | (kid,_) -> A_aux (A_nexp (nvar kid),l) - | exception Not_found -> ta_full + | exception Not_found -> ta_full) + | _ -> ta_full in aux typ in let rewrite_one_exp nexp_map (e,ann) = |