...

diff --git a/helm/software/components/ng_refiner/nCicUnification.ml b/helm/software/components/ng_refiner/nCicUnification.ml
index fa3ba4988477dd0aa777a462b5e350a65eee9f5c..98b06f94e689d5d138d610eb130809512f8e2f78 100644 (file)
--- a/helm/software/components/ng_refiner/nCicUnification.ml
+++ b/helm/software/components/ng_refiner/nCicUnification.ml
@@ -45,6 +45,8 @@ let eta_reduce after_beta_expansion after_beta_expansion_body
  try
   match before_beta_expansion,after_beta_expansion_body with
   | NCic.Appl l1, NCic.Appl l2 ->
+      NCicUtils.does_not_occur 0 1 (NCic.Appl (List.tail (List.rev l2)))
+      ...
       let rec all_but_last check_last = function
         | [] -> assert false
         | [NCic.Rel 1] -> []
@@ -57,42 +59,49 @@ let eta_reduce after_beta_expansion after_beta_expansion_body
         | [he] -> he
         | l -> NCic.Appl l
       in
-      let t = 
-        NCicSubstitution.subst (NCic.Sort NCic.Prop) (all_but_last true l2) in
-      let all_but_last = all_but_last false l in
+      let impossible_term = NCic.Rel ~-1 in
+      let t = NCicSubstitution.subst impossible_term (all_but_last true l2) in
+      let all_but_last = all_but_last false l1 in
       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 num test_equality_only metasenv subst context t arg =
-  let rec aux (n,context as k) (metasenv, subst as acc) t' =
+let rec beta_expand num test_eq_only swap metasenv subst context t arg =
+  let rec aux (n,context,test_eq_only as k) (metasenv, subst as acc) t' =
    try
     let metasenv, subst =
-     unify (* test_equality_only *) metasenv subst context
+     unify test_eq_only metasenv subst context
       (NCicSubstitution.lift n arg) t'
     in
      (metasenv, subst), C.Rel (1 + n)
    with Uncertain _ | UnificationFailure _ ->
        match t' with
-       | NCic.Rel m  -> 
-           (metasenv, subst), if m <= n then NCic.Rel m else NCic.Rel (m+1)
+       | NCic.Rel m orig -> 
+           (metasenv, subst), if m <= n then orig else NCic.Rel (m+1)
        (* andrea: in general, beta_expand can create badly typed
         terms. This happens quite seldom in practice, UNLESS we
         iterate on the local context. For this reason, we renounce
         to iterate and just lift *)
        | NCic.Meta (i,(shift,lc)) ->
            (metasenv,subst), NCic.Meta (i,(shift+1,lc))
+       | NCic.Prod (name, src, tgt) as orig ->
+           let (metasenv, subst), src1 = aux (n,context,true) acc src in 
+           let k = n+1, (name, NCic.Decl src) :: context, test_eq_only in
+           let (metasenv,subst), tgt1 = aux k (metasenv, subst) tgt in 
+           if src == src1 && tgt == tgt1 then orig else
+           NCic.Prod (name, src1, tgt1)
        | t -> 
            NCicUntrusted.map_term_fold_a 
-             (fun e (n,ctx) -> n+i,e::ctx) k aux acc t
+             (fun e (n,ctx) -> n+1,e::ctx) k aux acc t
 
   in
   let argty = NCicTypeChecker.typeof ~metasenv ~subst context arg in
   let fresh_name = "Hbeta" ^ string_of_int num in
-  let (metasenv,subst), t = aux (0, context) (metasenv, subst) t in
-  let t = eta_reduce (C.Lambda (fresh_name,argty,t)) t t in
-  metasenv, subst, t
+  let (metasenv,subst,_), t1 = 
+    aux (0, context, test_eq_only) (metasenv, subst) t in
+  let t2 = eta_reduce (C.Lambda (fresh_name,argty,t1)) t1 t in
+  metasenv, subst, t2
 
 and beta_expand_many test_equality_only metasenv subst context t args ugraph =
   let _, subst, metasenv, hd =
@@ -231,7 +240,7 @@ and unify metasenv subst context t1 t2 =
            (* we verify that none of the args is a Meta, 
               since beta expanding w.r.t a metavariable makes no sense  *)
               let subst, metasenv, beta_expanded =
-                beta_expand_many 
+                beta_expand_many (* passare swap *)
                   test_equality_only metasenv subst context t2 args ugraph 
               in
                 aux test_eq_only metasenv subst context