fix inverse (#1316)

Author: fblanqui

src/core/inverse.ml

@@ -98,20 +98,6 @@ let prod_graph : sym -> (sym * sym * sym * bool) list = fun s ->
 (** cached version of [prod_graph]. *)
 let prod_graph : sym -> (sym * sym * sym * bool) list = cache prod_graph
 
-(** [inverse_prod s s'] returns [(s0,s1,s2,b)] if [s] has a rule of the form
-   [s (s0 _ _) ↪ Π x:s1 _, s2 r] with [b=true] iff [x] occurs in [r], and
-   either [s1] has a rule of the form [s1 (s3 ...) ↪ s' ...] or [s1 == s'].
-@raise [Not_found] otherwise. *)
-let inverse_prod : sym -> sym -> sym * sym * sym * bool = fun s s' ->
-  match prod_graph s with
-  | [] -> raise Not_found
-  | [x] -> x
-  | graph ->
-  let f (_,s1,_,_) =
-    try let _ = inverse_const s1 s' in true with Not_found -> false in
-  try List.find f graph
-  with Not_found -> List.find (fun (_,s1,_,_) -> s1 == s') graph
-
 (** [inverse s v] tries to compute a term [u] such that [s(u)] reduces to [v].
 @raise [Not_found] otherwise. *)
 let rec inverse : sym -> term -> term = fun s v ->
@@ -120,22 +106,24 @@ let rec inverse : sym -> term -> term = fun s v ->
   | Symb s', [t] when s' == s -> t
   | Symb s', ts -> add_args (mk_Symb (inverse_const s s')) ts
   | Prod(a,b), _ ->
-      let s0,s1,s2,occ =
-        match get_args a with
-        | Symb s', _ -> inverse_prod s s'
-        | _ -> raise Not_found
-      in
-      let t1 = inverse s1 a in
-      let t2 =
-        let x, b = unbind b in
-        let b = inverse s2 b in
-        if occ then mk_Abst (a, bind_var x b) else b
+      let x, b = unbind b in
+      let f (s0,s1,s2,occ) =
+        try
+          let t1 = inverse s1 a in
+          let t2 = inverse s2 b in
+          let t2 = if occ then mk_Abst (a, bind_var x t2) else t2 in
+          Some (add_args (mk_Symb s0) [t1;t2])
+        with Not_found -> None
       in
-      add_args (mk_Symb s0) [t1;t2]
+      begin
+        match List.find_map f (prod_graph s) with
+        | None -> raise Not_found
+        | Some t -> t
+      end
   | _ -> raise Not_found
 
 let inverse : sym -> term -> term = fun s v ->
   let t = inverse s v in let v' = mk_Appl(mk_Symb s,t) in
   if Eval.eq_modulo [] v' v then t
-  else (if Logger.log_enabled() then log "%a ≢ %a@" term v' term v;
+  else (if Logger.log_enabled() then log "%a ≢ %a" term v' term v;
         raise Not_found)

tests/OK/1313.lp

@@ -0,0 +1,3 @@
+require open tests.OK.HOL tests.OK.Eq tests.OK.Epsilon tests.OK.Impred;
+
+symbol test_KO : π ((ε) [ι] = (ε) [ι]);

tests/OK/Epsilon.lp

@@ -0,0 +1,4 @@
+require open tests.OK.FOL tests.OK.HOL tests.OK.Impred;
+
+symbol ε [a:Set] : (τ a → Prop) → τ a;
+symbol εᵢ [a:Set] (p:τ a → Prop) : π (∃ p) → π (p (ε p));

tests/export_raw_dk.sh

@@ -60,7 +60,7 @@ do
         # proofs
         why3*|tutorial|try|tautologies|rewrite*|remove|natproofs|have|generalize|foo|comment_in_qid|apply|anonymous|admit|change);;
         # "open"
-        triangular|power-fact|postfix|perf_rw_*|not-eager|nonLeftLinear2|natural|Nat|lpparse2|logic|List|FOL|Eq|doc|Bool|arity_var|arity_diff|922|262_pair_ex_2|215|1141|Tactic|Option|String|HOL|Impred|PropExt|Classic|Comp|Pos|Z|1217|1151|B1|B2|C1|C2|C3);;
+        triangular|power-fact|postfix|perf_rw_*|not-eager|nonLeftLinear2|natural|Nat|lpparse2|logic|List|FOL|Eq|doc|Bool|arity_var|arity_diff|922|262_pair_ex_2|215|1141|Tactic|Option|String|HOL|Impred|PropExt|Classic|Comp|Pos|Z|1217|1151|B1|B2|C1|C2|C3|Epsilon|1313);;
         # "inductive"
         strictly_positive_*|inductive|989|904|830|341);;
         # underscore in query