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.

Author: gabrielhdt

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 utils ok_ko rewriting)
+ (names utils ok_ko rewriting meta)
  (deps
   (glob_files OK/*.lp)
   (glob_files OK/*.dk)

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)
+        ] )
+    ]