unif: test equality first

src/core/eval.ml

@@ -102,7 +102,7 @@ module Config = struct
       configuration [cfg]. *)
   let rec unfold : t -> term -> term = fun cfg a ->
     match Term.unfold a with
-    | Vari x as a->
+    | Vari x as a ->
       begin match VarMap.find_opt x cfg.varmap with
         | None -> a
         | Some v -> unfold cfg v
@@ -501,17 +501,18 @@ let hnf = time_reducer hnf
 
 (** [eq_modulo c a b] tests the convertibility of [a] and [b] in context
     [c]. WARNING: may have side effects in TRef's introduced by whnf. *)
-let eq_modulo : ctxt -> term -> term -> bool = fun c ->
-  eq_modulo whnf (Config.make c)
+let eq_modulo : ?tags:rw_tag list -> ctxt -> term -> term -> bool =
+  fun ?tags c -> eq_modulo whnf (Config.make ?tags c)
 
 let eq_modulo =
-  let open Stdlib in let r = ref false in fun c t u ->
-  Debug.(record_time Rewriting (fun () -> r := eq_modulo c t u)); !r
+  let open Stdlib in let r = ref false in fun ?tags c t u ->
+  Debug.(record_time Rewriting (fun () -> r := eq_modulo ?tags c t u)); !r
 
 (** [pure_eq_modulo c a b] tests the convertibility of [a] and [b] in context
     [c] with no side effects. *)
-let pure_eq_modulo : ctxt -> term -> term -> bool = fun c a b ->
-  Timed.pure_test (fun (c,a,b) -> eq_modulo c a b) (c,a,b)
+let pure_eq_modulo : ?tags:rw_tag list -> ctxt -> term -> term -> bool =
+  fun ?tags c a b ->
+  Timed.pure_test (fun (c,a,b) -> eq_modulo ?tags c a b) (c,a,b)
 
 (** [whnf c t] computes a whnf of [t], unfolding the variables defined in the
    context [c], and using user-defined rewrite rules if [~rewrite]. *)

src/core/eval.mli

@@ -51,11 +51,11 @@ val whnf : ?tags:rw_tag list -> ctxt -> term -> term
 
 (** [eq_modulo c a b] tests the convertibility of [a] and [b] in context
     [c]. *)
-val eq_modulo : ctxt -> term -> term -> bool
+val eq_modulo : ?tags:rw_tag list -> ctxt -> term -> term -> bool
 
 (** [pure_eq_modulo c a b] tests the convertibility of [a] and [b] in context
    [c] with no side effects. *)
-val pure_eq_modulo : ctxt -> term -> term -> bool
+val pure_eq_modulo : ?tags:rw_tag list -> ctxt -> term -> term -> bool
 
 (** [snf ~dtree c t] computes a snf of [t], unfolding the variables defined in
     the context [c]. The function [dtree] maps symbols to dtrees. *)

src/core/unif.ml

@@ -354,7 +354,7 @@ let sym_sym_whnf :
       | Some (t, u) -> add_constr p (c,t,u)
       | None -> inverse p c t2 s2 ts2 t1
 
-(** [solve_noexn p] tries to simplify the constraints of [p].
+(** [solve p] tries to simplify the constraints of [p].
 @raise [Unsolvable] if it finds a constraint that cannot be satisfied.
 Otherwise, [p.to_solve] is empty but [p.unsolved] may still contain
 constraints that could not be simplified. *)
@@ -372,9 +372,12 @@ let solve : problem -> unit = fun p ->
   p := {!p with to_solve};
 
   (* We first try without normalizing wrt user-defined rules. *)
-  let t1 = Eval.whnf ~tags:[`NoRw; `NoExpand] c t1
-  and t2 = Eval.whnf ~tags:[`NoRw; `NoExpand] c t2 in
+  let tags = [`NoRw; `NoExpand] in
+  let t1 = Eval.whnf ~tags c t1 and t2 = Eval.whnf ~tags c t2 in
   if Logger.log_enabled () then log_unif (gre "solve %a") constr (c,t1,t2);
+  if Eval.pure_eq_modulo ~tags c t1 t2 then
+    (if Logger.log_enabled () then log_unif "equivalent terms")
+  else
   let h1, ts1 = get_args t1 and h2, ts2 = get_args t2 in
 
   match h1, h2 with

src/tool/sr.ml

@@ -92,7 +92,8 @@ let symb_to_tenv
             (* A symbol may also come from a metavariable that appeared in the
                type of a metavariable that was replaced by a symbol. We do not
                have concrete examples of that happening yet. *)
-            fatal pos "Introduced symbol [%s] cannot be removed." f.sym_name
+            fatal pos "Bug. Introduced symbol [%s] cannot be removed. \
+                       Please contact the developers." f.sym_name
           in
           let (ts1, ts2) = List.cut ts arities.(i) in
           (_TEnv (_TE_Vari vars.(i)) (Array.of_list ts1), ts2)
@@ -149,6 +150,7 @@ let check_rule : Scope.pre_rule Pos.loc -> rule = fun ({pos; elt} as pr) ->
     end;
   (* Replace [Patt] nodes of LHS with corresponding elements of [vars]. *)
   let lhs_vars = _Appl_Symb s (List.map (patt_to_tenv vars) lhs) in
+  (* Replace [vars] by fresh metas. *)
   let p = new_problem() in
   let metas =
     let f i _ =
@@ -158,7 +160,6 @@ let check_rule : Scope.pre_rule Pos.loc -> rule = fun ({pos; elt} as pr) ->
       LibMeta.fresh p (build_meta_type p arity) arity
     in Array.mapi f vars
   in
-  (* Substitute them in the LHS and in the RHS. *)
   let lhs_with_metas, rhs_with_metas =
     let lhs_rhs = Bindlib.box_pair lhs_vars pr_rhs in
     let b = Bindlib.unbox (Bindlib.bind_mvar vars lhs_rhs) in

tests/OK/1006.lp

@@ -0,0 +1,11 @@
+constant symbol Set : TYPE;
+injective symbol τ : Set → TYPE; builtin "T" ≔ τ;
+
+symbol mys : TYPE;
+symbol myop :  mys →  mys →   mys;
+
+symbol testfun : Π (Func : Set) (Hom : τ Func → Set) (Comp : Π [F : τ Func]  , τ (Hom F)) ,
+ mys;
+
+rule (myop (@testfun $Func $Hom $Comp ) (@testfun $Func $Hom $Comp    ) )
+    ↪  (@testfun $Func $Hom $Comp ) ;