From 6b449a61d1572779c39f9313f7725ae9a9b3e32c Mon Sep 17 00:00:00 2001
From: gabrielhdt <gabrielhondet@gmail.com>
Date: Fri, 17 Dec 2021 11:15:08 +0100
Subject: [PATCH] Add starting point to DkMeta

Introduce a function that allows to rewrite a term with a specific
set of rewrite rules. In particular, it may be used to implement tactics
that transform terms.
---
 src/tool/meta.ml | 22 ++++++++++++++++
 tests/dune       |  2 +-
 tests/meta.ml    | 67 ++++++++++++++++++++++++++++++++++++++++++++++++
 3 files changed, 90 insertions(+), 1 deletion(-)
 create mode 100644 src/tool/meta.ml
 create mode 100644 tests/meta.ml

diff --git a/src/tool/meta.ml b/src/tool/meta.ml
new file mode 100644
index 0000000000..953cb30dc1
--- /dev/null
+++ b/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
diff --git a/tests/dune b/tests/dune
index 3d1bf8bf82..cd624eaa6e 100644
--- a/tests/dune
+++ b/tests/dune
@@ -1,5 +1,5 @@
 (tests
- (names ok_ko rewriting purity)
+ (names ok_ko rewriting purity meta)
  (deps
   (glob_files OK/*.lp)
   (glob_files OK/*.dk)
diff --git a/tests/meta.ml b/tests/meta.ml
new file mode 100644
index 0000000000..9ae79433c9
--- /dev/null
+++ b/tests/meta.ml
@@ -0,0 +1,67 @@
+(** 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 Pos.{ elt = r; _ } =
+    Scope.scope_rule true bool_sig_st (Pos.none (lhs, rhs))
+  in
+  let r = (r.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
+
+let () =
+  let open Alcotest in
+  run "Meta"
+    [ ( "standard"
+      , [ ("no rewriting with signature's rules", `Quick, no_rewrite)
+        ; ("rewrite symbol", `Quick, simple_rewrite)
+        ] )
+    ]