Unification enhanchement:

 (?1 t) vs (h t)     used to return    ?1 := \lambda x.h x
                     it now returns    ?1 := h

Note: both heuristics are not complete. E.g.:

(H ?1 (?1 t)) vs (H h (h t))                 used to fail (now succeeds)
(H ?1 (?1 t)) vs (H (\lambda x.h x) (h t))   used to succeed (now fails)

diff --git a/helm/ocaml/cic_unification/cicUnification.ml b/helm/ocaml/cic_unification/cicUnification.ml
index 27150461fb0038ba4c5e7d81f8ff0562d0dc2de3..d8a078997a04ca3e9a1d8de75db88d4da96b90e2 100644 (file)
--- a/helm/ocaml/cic_unification/cicUnification.ml
+++ b/helm/ocaml/cic_unification/cicUnification.ml
@@ -77,6 +77,37 @@ let rec deref subst t =
     | t -> t
 ;; 
 
+exception WrongShape;;
+let eta_reduce after_beta_expansion after_beta_expansion_body
+     before_beta_expansion
+ =
+ try
+  match before_beta_expansion,after_beta_expansion_body with
+     Cic.Appl l, Cic.Appl l' ->
+      let rec all_but_last check_last =
+       function
+          [] -> assert false
+        | [Cic.Rel 1] -> []
+        | [_] -> if check_last then raise WrongShape else []
+        | he::tl -> he::(all_but_last check_last tl)
+      in
+       let all_but_last check_last l =
+        match all_but_last check_last l with
+           [] -> assert false
+         | [he] -> he
+         | l -> Cic.Appl l
+       in
+       let t = CicSubstitution.subst (Cic.Rel (-1)) (all_but_last true l') in
+       let all_but_last = all_but_last false l in
+        (* here we should test alpha-equivalence; however we know by
+           construction that here alpha_equivalence is equivalent to = *)
+        if t = all_but_last then
+         all_but_last
+        else
+         after_beta_expansion
+   | _,_ -> after_beta_expansion
+ with
+  WrongShape -> after_beta_expansion
 
 let rec beta_expand test_equality_only metasenv subst context t arg ugraph =
  let module S = CicSubstitution in
@@ -220,10 +251,11 @@ let rec beta_expand test_equality_only metasenv subst context t arg ugraph =
   let argty,ugraph1 = type_of_aux' metasenv subst context arg ugraph in
   let fresh_name =
    FreshNamesGenerator.mk_fresh_name ~subst
-    metasenv context (Cic.Name "Heta") ~typ:argty
+    metasenv context (Cic.Name "Hbeta") ~typ:argty
   in
    let subst,metasenv,t',ugraph2 = aux metasenv subst 0 context t ugraph1 in
-   subst, metasenv, C.Lambda (fresh_name,argty,t'), ugraph2
+   let t'' = eta_reduce (C.Lambda (fresh_name,argty,t')) t' t in
+   subst, metasenv, t'', ugraph2
 
 
 and beta_expand_many test_equality_only metasenv subst context t args ugraph =