Merge sail2 into monads

1 files changed, 38 insertions, 4 deletions

diff --git a/src/rewrites.ml b/src/rewrites.ml
index 0ad4c56e..8894f2c8 100644
--- a/src/rewrites.ml
+++ b/src/rewrites.ml
@@ -4763,6 +4763,35 @@ let minimise_recursive_functions (Defs defs) =
     | d -> d
   in Defs (List.map rewrite_def defs)
 
+let move_termination_measures (Defs defs) =
+  let scan_for id defs =
+    let rec aux = function
+      | [] -> None
+      | (DEF_measure (id',pat,exp))::t ->
+         if Id.compare id id' == 0 then Some (pat,exp) else aux t
+      | (DEF_fundef (FD_aux (FD_function (_,_,_,FCL_aux (FCL_Funcl (id',_),_)::_),_)))::_
+      | (DEF_spec (VS_aux (VS_val_spec (_,id',_,_),_))::_)
+        when Id.compare id id' == 0 -> None
+      | _::t -> aux t
+    in aux defs
+  in
+  let rec aux acc = function
+    | [] -> List.rev acc
+    | (DEF_fundef (FD_aux (FD_function (r,ty,e,fs),(l,f_ann))) as d)::t -> begin
+       let id = match fs with
+         | [] -> assert false (* TODO *)
+         | (FCL_aux (FCL_Funcl (id,_),_))::_ -> id
+       in
+       match scan_for id t with
+       | None -> aux (d::acc) t
+       | Some (pat,exp) ->
+          let r = Rec_aux (Rec_measure (pat,exp), Generated l) in
+          aux (DEF_fundef (FD_aux (FD_function (r,ty,e,fs),(l,f_ann)))::acc) t
+      end
+    | (DEF_measure _)::t -> aux acc t
+    | h::t -> aux (h::acc) t
+  in Defs (aux [] defs)
+
 (* Make recursive functions with a measure use the measure as an
    explicit recursion limit, enforced by an assertion. *)
 let rewrite_explicit_measure (Defs defs) =
@@ -4806,8 +4835,8 @@ let rewrite_explicit_measure (Defs defs) =
     | exception Not_found -> [vs]
   in
   (* Add extra argument and assertion to each funcl, and rewrite recursive calls *)
-  let rewrite_funcl (FCL_aux (FCL_Funcl (id,pexp),ann) as fcl) =
-    let loc = Parse_ast.Generated (fst ann) in
+  let rewrite_funcl (FCL_aux (FCL_Funcl (id,pexp),fcl_ann) as fcl) =
+    let loc = Parse_ast.Generated (fst fcl_ann) in
     let P_aux (pat,pann),guard,body,ann = destruct_pexp pexp in
     let extra_pat = P_aux (P_id limit,(loc,empty_tannot)) in
     let pat = match pat with
@@ -4839,7 +4868,7 @@ let rewrite_explicit_measure (Defs defs) =
         } body
     in
     let body = E_aux (E_block [assert_exp; body],(loc,empty_tannot)) in
-    FCL_aux (FCL_Funcl (rec_id id, construct_pexp (P_aux (pat,pann),guard,body,ann)),ann)
+    FCL_aux (FCL_Funcl (rec_id id, construct_pexp (P_aux (pat,pann),guard,body,ann)),fcl_ann)
   in
   let rewrite_function (FD_aux (FD_function (r,t,e,fcls),ann) as fd) =
     let loc = Parse_ast.Generated (fst ann) in
@@ -4881,6 +4910,7 @@ let rewrite_explicit_measure (Defs defs) =
              | [wpat] -> wpat
              | _ -> P_aux (P_tup wpats,(loc,empty_tannot))
            in
+           let measure_exp = E_aux (E_cast (int_typ, measure_exp),(loc,empty_tannot)) in
            let wbody = E_aux (E_app (rec_id id,wexps@[measure_exp]),(loc,empty_tannot)) in
            let wrapper =
              FCL_aux (FCL_Funcl (id, Pat_aux (Pat_exp (wpat,wbody),(loc,empty_tannot))),(loc,empty_tannot))
@@ -5029,10 +5059,15 @@ let rewrite_defs_coq = [
   ("exp_lift_assign", rewrite_defs_exp_lift_assign);
   (* ("constraint", rewrite_constraint); *)
   (* ("remove_assert", rewrite_defs_remove_assert); *)
+  ("move_termination_measures", move_termination_measures);
   ("top_sort_defs", top_sort_defs);
   ("trivial_sizeof", rewrite_trivial_sizeof);
   ("sizeof", rewrite_sizeof);
   ("early_return", rewrite_defs_early_return);
+  (* merge funcls before adding the measure argument so that it doesn't
+     disappear into an internal pattern match *)
+  ("merge function clauses", merge_funcls);
+  ("recheck_defs_without_effects", recheck_defs_without_effects);
   ("make_cases_exhaustive", MakeExhaustive.rewrite);
   ("rewrite_explicit_measure", rewrite_explicit_measure);
   ("recheck_defs_without_effects", recheck_defs_without_effects);
@@ -5043,7 +5078,6 @@ let rewrite_defs_coq = [
   ("internal_lets", rewrite_defs_internal_lets);
   ("remove_superfluous_letbinds", rewrite_defs_remove_superfluous_letbinds);
   ("remove_superfluous_returns", rewrite_defs_remove_superfluous_returns);
-  ("merge function clauses", merge_funcls);
   ("recheck_defs", recheck_defs)
   ]