Term transformation helper function

src/handle/command.ml

@@ -136,7 +136,7 @@ let handle_modifiers : p_modifier list -> prop * expo * match_strat =
 let handle_rule : sig_state -> p_rule -> sym = fun ss r ->
   Console.out 3 (Color.cya "%a") Pos.pp r.pos;
   Console.out 4 "%a" (Pretty.rule "rule") r;
-  let pr = scope_rule false ss r in
+  let pr = scope_rule ss r in
   let sym = pr.elt.pr_sym in
   if !(sym.sym_def) <> None then
     fatal pr.pos "No rewriting rule can be given on the defined symbol %a."
@@ -227,7 +227,7 @@ let get_proof_data : compiler -> sig_state -> p_command -> cmd_output =
       (add_notation ss sym n, None, None)
   | P_unif_rule(h) ->
       (* Approximately same processing as rules without SR checking. *)
-      let pur = scope_rule true ss h in
+      let pur = scope_unif_rule ss h in
       let urule = Scope.rule_of_pre_rule pur in
       Sign.add_rule ss.signature Unif_rule.equiv urule;
       Tree.update_dtree Unif_rule.equiv;

src/parsing/scope.ml

@@ -641,10 +641,22 @@ let rule_of_pre_rule : pre_rule loc -> rule =
   ; xvars_nb = pr_xvars_nb
   ; rule_pos }
 
-(** [scope_rule ur ss r] turns a parser-level rewriting rule [r], or a
-    unification rule if [ur] is true, into a pre-rewriting rule. *)
-let scope_rule : bool -> sig_state -> p_rule -> pre_rule loc =
-  fun ur ss { elt = (p_lhs, p_rhs); pos } ->
+(** The status of rewrite rules. *)
+type rule_status =
+  | Regular (** Regular LPMT rewrite rule *)
+  | Unif
+    (** Unification rule: rewrite a unification problem into another
+        unification problem. *)
+  | Meta
+    (** Meta rewrite rule: such rewrite rules are allowed to rewrite
+        constant symbols *)
+
+(** [scope_rule rst ss r] turns a parser-level rewriting rule [r] into
+    a pre-rewriting rule. Argument [rst] specifies the nature of the
+    rewrite rulea unification rule if [rst] is [Unif], *)
+let scope_rule : rule_status -> sig_state -> p_rule -> pre_rule loc =
+  fun rst ss r ->
+  let (p_lhs, p_rhs) = r.elt in
   (* Compute the set of pattern variables on both sides. *)
   let (pvs_lhs, nl) = patt_vars p_lhs in
   (* NOTE to reject non-left-linear rules check [nl = []] here. *)
@@ -680,8 +692,10 @@ let scope_rule : bool -> sig_state -> p_rule -> pre_rule loc =
     let (h, args) = get_args pr_lhs in
     match h with
     | Symb(s) ->
-        if is_constant s then fatal p_lhs.pos "Constant LHS head symbol.";
-        if s.sym_expo = Protec && ss.signature.sign_path <> s.sym_path then
+        if rst <> Meta && is_constant s then
+          fatal p_lhs.pos "Constant LHS head symbol.";
+        if rst <> Meta && s.sym_expo = Protec &&
+           ss.signature.sign_path <> s.sym_path then
           fatal p_lhs.pos "Cannot define rules on foreign protected symbols.";
         (s, args)
     | _ -> fatal p_lhs.pos "No head symbol in LHS."
@@ -698,10 +712,12 @@ let scope_rule : bool -> sig_state -> p_rule -> pre_rule loc =
     let htbl_vars = Hashtbl.create (Hashtbl.length lhs_indices) in
     let fn k i = Hashtbl.add htbl_vars k pr_vars.(i) in
     Hashtbl.iter fn lhs_indices;
-    if ur then
-      M_URHS{ m_urhs_data = htbl_vars ; m_urhs_vars_nb = Array.length pr_vars
-            ; m_urhs_xvars = [] }
-    else
+    match rst with
+    | Unif ->
+        M_URHS{ m_urhs_data = htbl_vars;
+                m_urhs_vars_nb = Array.length pr_vars;
+                m_urhs_xvars = [] }
+    | Regular | Meta ->
       M_RHS{ m_rhs_prv = is_private pr_sym; m_rhs_data = htbl_vars;
              m_rhs_new_metas = new_problem() }
   in
@@ -715,7 +731,8 @@ let scope_rule : bool -> sig_state -> p_rule -> pre_rule loc =
       in
       Array.init lhs_size fn
     in
-    if ur then (* Unification rule. *)
+    match rst with
+    | Unif ->
       (* We scope the RHS and retrieve variables not occurring in the LHS. *)
       let xvars =
         match mode with
@@ -734,11 +751,17 @@ let scope_rule : bool -> sig_state -> p_rule -> pre_rule loc =
       (* We put everything together to build the pre-rule. *)
       { pr_sym ; pr_lhs ; pr_vars ; pr_rhs ; pr_arities
       ; pr_names ; pr_xvars_nb }
-    else (* Rewrite rule. *)
+    | Regular | Meta ->
       { pr_sym ; pr_lhs ; pr_vars ; pr_rhs ; pr_arities
       ; pr_names ; pr_xvars_nb=0 }
   in
-  Pos.make pos prerule
+  Pos.make r.pos prerule
+
+let scope_unif_rule : sig_state -> p_rule -> pre_rule loc = scope_rule Unif
+
+let scope_meta_rule : sig_state -> p_rule -> pre_rule loc = scope_rule Meta
+
+let scope_rule : sig_state -> p_rule -> pre_rule loc = scope_rule Regular
 
 (** [scope_pattern ss env t] turns a parser-level term [t] into an actual term
     that will correspond to selection pattern (rewrite tactic). *)

src/parsing/scope.mli

@@ -51,9 +51,17 @@ type pre_rule =
 (** [rule_of_pre_rule r] converts a pre-rewrite rule into a rewrite rule. *)
 val rule_of_pre_rule : pre_rule loc -> rule
 
-(** [scope_rule ur ss r] turns a parser-level rewriting rule [r], or a
-    unification rule if [ur] is true, into a pre-rewriting rule. *)
-val scope_rule : bool -> sig_state -> p_rule -> pre_rule loc
+(** [scope_rule ss r] turns a parser-level rewriting rule [r] into a
+    pre-rewriting rule. *)
+val scope_rule : sig_state -> p_rule -> pre_rule loc
+
+(** [scope_unif_rule ss r] turns a parser-level unification rule [r] into a
+    pre-rewriting rule. *)
+val scope_unif_rule : sig_state -> p_rule -> pre_rule loc
+
+(** [scope_meta_rule ss r] turns a parser-level meta rewriting rule [r]
+    into a pre-rewriting rule. *)
+val scope_meta_rule : sig_state -> p_rule -> pre_rule loc
 
 (** [scope_rw_patt ss env t] turns a parser-level rewrite tactic specification
     [s] into an actual rewrite specification (possibly containing variables of

src/tool/meta.ml

@@ -0,0 +1,22 @@
+open Core
+open Timed
+open Lplib
+open Extra
+
+let rewrite_with (sign : Sign.t) (rules : (Term.sym * Term.rule) list) :
+    Term.term -> Term.term =
+  let exec t =
+    (* Remove rules and definitions from {b!all} signatures *)
+    let strip_sym _ s =
+      s.Term.sym_rules := [];
+      s.Term.sym_def := None;
+      Tree.update_dtree s
+    in
+    Common.Path.Map.iter
+      (fun _ s -> StrMap.iter strip_sym !(s.Sign.sign_symbols))
+      Timed.(!Sign.loaded);
+    (* Add a set of custom rules *)
+    List.iter (fun (s, r) -> Sign.add_rule sign s r) rules;
+    Eval.snf [] t
+  in
+  pure_apply exec

tests/dune

@@ -1,5 +1,5 @@
 (tests
- (names ok_ko rewriting purity kernel)
+ (names ok_ko rewriting purity meta kernel)
  (deps
   (glob_files OK/*.lp)
   (glob_files OK/*.dk)

tests/meta.ml

@@ -0,0 +1,81 @@
+(** Test the Meta module. *)
+open Common
+
+open Handle
+open Parsing
+open Core
+
+let term : Term.term Alcotest.testable =
+  ( module struct
+    type t = Term.term
+
+    let pp = Print.pp_term
+    let equal = Rewrite.eq
+  end )
+
+let scope_term ss t =
+  Scope.scope_term true ss [] (Term.new_problem ()) (Fun.const None)
+    (Fun.const None) t
+
+let () = Library.set_lib_root (Some "/tmp")
+
+(** The signature of [OK/bool.lp] *)
+let bool_sig = Compile.Pure.compile_file "OK/bool.lp"
+
+(** The signature state with [OK/bool.lp] opened. *)
+let bool_sig_st =
+  let open Core in
+  let ss = Sig_state.of_sign bool_sig in
+  Sig_state.open_sign ss bool_sig
+
+(** The term [bool_or true true] *)
+let or_true_true =
+  Syntax.P.(appl_list (iden "bool_or") [ iden "true"; iden "true" ])
+  |> scope_term bool_sig_st
+
+(** Unit tests functions *)
+
+let no_rewrite () =
+  let no_rewrite = Tool.Meta.rewrite_with bool_sig [] or_true_true in
+  Alcotest.(check term) "same term" or_true_true no_rewrite
+
+let simple_rewrite () =
+  let lhs = Syntax.P.iden "bool_or" in
+  let rhs = Syntax.P.iden "bool_and" in
+  let r =
+    Scope.scope_rule bool_sig_st (Pos.none (lhs, rhs))
+  in
+  let r = (r.Pos.elt.pr_sym, Scope.rule_of_pre_rule r) in
+  let rewritten =
+    Tool.Meta.rewrite_with bool_sig [ r ] or_true_true
+  in
+  let and_true_true =
+    Syntax.P.(appl_list (iden "bool_and") [ iden "true"; iden "true" ])
+    |> scope_term bool_sig_st
+  in
+  Alcotest.(check term) "same term" and_true_true rewritten
+
+(* Meta rewrite rules can rewrite symbols noted "constant". *)
+let rewrite_constant () =
+  let lhs = Syntax.P.iden "true" in (* [true] is constant *)
+  let rhs = Syntax.P.iden "false" in
+  let r =
+    Scope.scope_meta_rule bool_sig_st (Pos.none (lhs, rhs))
+  in
+  let r = (r.Pos.elt.pr_sym, Scope.rule_of_pre_rule r) in
+  let or_false_false =
+    Syntax.P.(appl_list (iden "bool_or") [ iden "false"; iden "false" ])
+    |> scope_term bool_sig_st
+  in
+  let rewritten = Tool.Meta.rewrite_with bool_sig [ r ] or_true_true in
+  Alcotest.check term "same term" or_false_false rewritten
+
+let () =
+  let open Alcotest in
+  run "Meta"
+    [ ( "standard"
+      , [ ("no rewriting with signature's rules", `Quick, no_rewrite)
+        ; ("rewrite symbol", `Quick, simple_rewrite)
+        ; ("rewrite constant", `Quick, rewrite_constant)
+        ] )
+    ]

tests/rewriting.ml

@@ -32,7 +32,7 @@ let sig_state, a = add_sym sig_state "A"
 let parse_rule s =
   let r = Parser.Lp.parse_string "rewrite_test rule" s |> Stream.next in
   let r = match r.elt with Syntax.P_rules [r] -> r | _ -> assert false in
-  Scope.scope_rule false sig_state r |> Scope.rule_of_pre_rule
+  Scope.scope_rule sig_state r |> Scope.rule_of_pre_rule
 
 let arrow_matching () =
   (* Matching on a product. *)