From 93427ac75ded2d7a06256f3c19b167c6c2e97830 Mon Sep 17 00:00:00 2001 From: gabrielhdt Date: Fri, 17 Dec 2021 11:15:08 +0100 Subject: [PATCH 1/2] 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 000000000..655647773 --- /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 ce5530862..ebe8bb987 100644 --- a/tests/dune +++ b/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) diff --git a/tests/meta.ml b/tests/meta.ml new file mode 100644 index 000000000..10779262f --- /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 r = + Scope.scope_rule true 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 + +let () = + let open Alcotest in + run "Meta" + [ ( "standard" + , [ ("no rewriting with signature's rules", `Quick, no_rewrite) + ; ("rewrite symbol", `Quick, simple_rewrite) + ] ) + ] From 81146a0da8bded217745eaadd2da1a89b3cf53d8 Mon Sep 17 00:00:00 2001 From: gabrielhdt Date: Sun, 19 Dec 2021 19:07:57 +0100 Subject: [PATCH 2/2] Allow to rewrite constants --- src/handle/command.ml | 4 ++-- src/parsing/scope.ml | 49 +++++++++++++++++++++++++++++++------------ src/parsing/scope.mli | 14 ++++++++++--- tests/meta.ml | 22 +++++++++++++++---- tests/rewriting.ml | 2 +- 5 files changed, 68 insertions(+), 23 deletions(-) diff --git a/src/handle/command.ml b/src/handle/command.ml index e304e0136..84fb4efe4 100644 --- a/src/handle/command.ml +++ b/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; diff --git a/src/parsing/scope.ml b/src/parsing/scope.ml index 1a752600d..4804fd576 100644 --- a/src/parsing/scope.ml +++ b/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). *) diff --git a/src/parsing/scope.mli b/src/parsing/scope.mli index 8228bc1ce..9a8a41875 100644 --- a/src/parsing/scope.mli +++ b/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 diff --git a/tests/meta.ml b/tests/meta.ml index 10779262f..bc4f0bcdd 100644 --- a/tests/meta.ml +++ b/tests/meta.ml @@ -36,16 +36,14 @@ let or_true_true = (** Unit tests functions *) let no_rewrite () = - let no_rewrite = - Tool.Meta.rewrite_with bool_sig [] or_true_true - in + 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 true bool_sig_st (Pos.none (lhs, rhs)) + 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 = @@ -57,11 +55,27 @@ let simple_rewrite () = 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) ] ) ] diff --git a/tests/rewriting.ml b/tests/rewriting.ml index 43ba2d24b..743a53d9c 100644 --- a/tests/rewriting.ml +++ b/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. *)