rewrite tactic: improve matches (fix #1026) (#1027)

src/core/term.ml

@@ -430,7 +430,7 @@ let is_unset : meta -> bool = fun m -> !(m.meta_value) = None
 let is_symb : sym -> term -> bool = fun s t ->
   match unfold t with Symb(r) -> r == s | _ -> false
 
-(** Total order on terms. *)
+(** Total order on terms modulo alpha-conversion. *)
 let cmp : term cmp =
   let rec cmp t t' =
     match unfold t, unfold t' with

src/handle/rewrite.ml

@@ -157,22 +157,19 @@ let matches : term -> term -> bool =
     match l with
     | [] -> ()
     | (p,t)::l ->
+      if Term.cmp p t = 0 then eq l else begin
       let hp, ps, k = get_args_len p and ht, ts, n = get_args_len t in
       if Logger.log_enabled() then
         log_rewr "matches %a %a ≡ %a %a"
           term hp (D.list term) ps term ht (D.list term) ts;
       match hp with
-      | Wild -> assert false
-      | Meta _ -> assert false
-      | Patt _ -> assert false
-      | TEnv _ -> assert false
-      | Plac _ -> assert false
-      | Appl _ -> assert false
-      | Prod _ -> assert false
-      | Abst _ -> assert false
-      | LLet _ -> assert false
-      | Type -> assert false
-      | Kind -> assert false
+      | Wild -> assert false (* used in user syntax only *)
+      | Patt _ -> assert false (* used in rules only *)
+      | TEnv _ -> assert false (* used in rules only *)
+      | Plac _ -> assert false (* used in scoping only *)
+      | Appl _ -> assert false (* not possible after get_args_len *)
+      | Type -> assert false (* not possible because of typing *)
+      | Kind -> assert false (* not possible because of typing *)
       | TRef r ->
         if k > n then raise Not_equal;
         let ts1, ts2 = List.cut ts (n-k) in
@@ -181,7 +178,12 @@ let matches : term -> term -> bool =
           log_rewr (Color.red "<TRef> ≔ %a") term u;
         r := Some u;
         eq (List.fold_left2 (fun l pi ti -> (pi,ti)::l) l ps ts2)
-      | _ ->
+      | Meta _
+      | Prod _
+      | Abst _
+      | LLet _
+      | Symb _
+      | Vari _ ->
         if k <> n then raise Not_equal;
         let add_args l =
           List.fold_left2 (fun l pi ti -> (pi,ti)::l) l ps ts in
@@ -191,6 +193,7 @@ let matches : term -> term -> bool =
         | _ ->
           if Logger.log_enabled() then log_rewr "distinct heads";
           raise Not_equal
+      end
   in
   fun p t ->
     try

tests/OK/1026.lp

@@ -0,0 +1,31 @@
+symbol Prop: TYPE;
+symbol π: Prop → TYPE;
+symbol Set: TYPE;
+constant symbol τ: Set → TYPE;
+builtin "T" ≔ τ;
+builtin "P" ≔ π;
+
+symbol = [a:Set] : τ a → τ a → Prop;
+
+notation = infix 10;
+
+constant symbol eq_refl [a:Set] (x:τ a) : π (x = x);
+constant symbol ind_eq [a:Set] [x y:τ a] : π (x = y) → Π p, π (p y) → π (p x);
+
+builtin "eq"    ≔ =;
+builtin "refl"  ≔ eq_refl;
+builtin "eqind" ≔ ind_eq;
+
+symbol set: Set;
+symbol cset [T]: (τ T → Prop) → τ set;
+
+symbol T: Set;
+symbol P: τ T → Prop;
+symbol U: τ set;
+symbol Q: τ set → Prop;
+symbol th: π (cset (λ x, P x) = U) → π (Q U) → π (Q (cset (λ x, P x))) ≔
+begin
+  assume h1 h2;
+  rewrite h1;
+  apply h2;
+end;