Allow to rewrite constants

Author: gabrielhdt

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).elt in
+      let pur = (scope_unif_rule ss h).elt 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

@@ -628,9 +628,20 @@ let rule_of_pre_rule : pre_rule -> rule =
   ; vars = pr_vars
   ; xvars_nb = pr_xvars_nb }
 
-(** [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 r ->
+(** 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
@@ -667,8 +678,10 @@ let scope_rule : bool -> sig_state -> p_rule -> pre_rule loc = fun ur ss r ->
     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."
@@ -685,10 +698,11 @@ let scope_rule : bool -> sig_state -> p_rule -> pre_rule loc = fun ur ss r ->
     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
+    match rst with
+    | Unif ->
+        M_URHS{ m_urhs_data = htbl_vars ; m_urhs_vars_nb = Array.length pr_vars
             ; m_urhs_xvars = [] }
-    else
+    | Regular | Meta ->
       M_RHS{ m_rhs_prv = is_private sym; m_rhs_data = htbl_vars;
              m_rhs_new_metas = new_problem() }
   in
@@ -702,7 +716,8 @@ let scope_rule : bool -> sig_state -> p_rule -> pre_rule loc = fun ur ss r ->
       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
@@ -721,12 +736,18 @@ let scope_rule : bool -> sig_state -> p_rule -> pre_rule loc = fun ur ss r ->
       (* We put everything together to build the pre-rule. *)
       { pr_sym = sym ; pr_lhs ; pr_vars ; pr_rhs ; pr_arities
       ; pr_names = lhs_names ; pr_xvars_nb }
-    else (* Rewrite rule. *)
+    | Regular | Meta ->
       { pr_sym = sym ; pr_lhs ; pr_vars ; pr_rhs ; pr_arities
       ; pr_names = lhs_names ; pr_xvars_nb=0 }
   in
   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). *)
 let scope_pattern : sig_state -> env -> p_term -> term = fun ss env t ->

src/parsing/scope.mli

@@ -48,9 +48,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 -> 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

tests/meta.ml

@@ -36,32 +36,44 @@ 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 Pos.{ elt = r; _ } =
-    Scope.scope_rule true bool_sig_st (Pos.none (lhs, rhs))
+    Scope.scope_meta_rule 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 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 Pos.{ elt = r; _ } =
+    Scope.scope_meta_rule bool_sig_st (Pos.none (lhs, rhs))
+  in
+  let r = (r.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).elt |> Scope.rule_of_pre_rule
+  (Scope.scope_rule sig_state r).elt |> Scope.rule_of_pre_rule
 
 let arrow_matching () =
   (* Matching on a product. *)