Add local rewrite rules for compute

src/transform/compute.ml

@@ -35,12 +35,14 @@ let meta_begin_compute_context =
            transformation@ 'compute_in_context'."
 *)
 
+let rule_label = Ident.create_label "rewrite"
+
 let collect_rule_decl prs e d =
   match d.Decl.d_node with
     | Decl.Dtype _ | Decl.Ddata _ | Decl.Dparam _ | Decl.Dind  _
     | Decl.Dlogic _ -> e
     | Decl.Dprop(_, pr, t) ->
-      if Decl.Spr.mem pr prs then
+      if Decl.Spr.mem pr prs || Ident.Slab.mem rule_label t.t_label then
         try add_rule t e
         with NotARewriteRule msg ->
           Warning.emit "proposition %a cannot be turned into a rewrite rule: %s"

src/transform/reduction_engine.ml

@@ -519,6 +519,7 @@ and reduce_match st u ~orig tbl sigma cont =
 
 
 and reduce_eval st t ~orig sigma rem =
+  let orig = t_label_copy orig t in
   match t.t_node with
   | Tvar v ->
     begin
@@ -533,13 +534,13 @@ and reduce_eval st t ~orig sigma rem =
           Format.eprintf "Tvar not found: %a@." Pretty.print_vs v;
           assert false
         *)
-        { value_stack = Term (t_label_copy orig t) :: st ;
+        { value_stack = Term orig :: st ;
           cont_stack = rem;
         }
     end
   | Tif(t1,t2,t3) ->
     { value_stack = st;
-      cont_stack = (Keval(t1,sigma),t1) :: (Kif(t2,t3,sigma),t) :: rem;
+      cont_stack = (Keval(t1,sigma),t1) :: (Kif(t2,t3,sigma),orig) :: rem;
     }
   | Tlet(t1,tb) ->
     let v,t2 = t_open_bound tb in
@@ -574,7 +575,7 @@ and reduce_eval st t ~orig sigma rem =
       cont_stack = List.rev_append args ((Kapp(ls,t.t_ty),orig) :: rem);
     }
   | Ttrue | Tfalse | Tconst _ ->
-    { value_stack = Term (t_label_copy orig t) :: st;
+    { value_stack = Term orig :: st;
       cont_stack = rem;
     }
 

tests/test_rewrite.mlw

+
+
+module M
+
+  predicate (-->) (x y:'a) = "rewrite" x = y
+
+  use import int.Int
+
+  goal g0 :
+     forall x:int. ("rewrite" x = 42) -> x+1 = 42+1
+
+  goal g :
+     forall x:int. x --> 42 -> x+1 = 42
+
+end