fix_outty fixed in order to perform eta-expansion when the term is not

a sequence of lambdas.

diff --git a/helm/software/components/ng_kernel/oCic2NCic.ml b/helm/software/components/ng_kernel/oCic2NCic.ml
index af9642e3f1657eeb47e6d0f2b12d73b717018eb1..d67089146171479ee83dac24f8429ff738668d8a 100644 (file)
--- a/helm/software/components/ng_kernel/oCic2NCic.ml
+++ b/helm/software/components/ng_kernel/oCic2NCic.ml
@@ -61,6 +61,8 @@ let splat_args ctx t n_fix =
    NCic.Appl (t:: aux (List.length ctx))
 ;;
 
+exception Nothing_to_do;;
+
 let fix_outty curi tyno t context outty =
  let leftno,rightno =
   match fst (CicEnvironment.get_obj CicUniv.oblivion_ugraph curi) with
@@ -80,22 +82,29 @@ prerr_endline ("LEFTNO: " ^ string_of_int leftno ^ "  " ^ CicPp.ppterm arity);*)
        leftno, count_prods leftno [] arity
    | _ -> assert false in
  let ens,args =
-  match fst (CicTypeChecker.type_of_aux' [] context t CicUniv.oblivion_ugraph)
-  with
+  let tty,_= CicTypeChecker.type_of_aux' [] context t CicUniv.oblivion_ugraph in
+  match CicReduction.whd context tty with
      Cic.MutInd (_,_,ens) -> ens,[]
    | Cic.Appl (Cic.MutInd (_,_,ens)::args) ->
       ens,fst (HExtlib.split_nth leftno args)
    | _ -> assert false
  in
-  let rec aux n irl context outty =
-   match n, CicReduction.whd context outty with
-      0, (Cic.Lambda _ as t) -> t
-    | 0, t ->
+  let rec aux n irl context outsort =
+   match n, CicReduction.whd context outsort with
+      0, Cic.Prod _ -> raise Nothing_to_do
+    | 0, _ ->
        let ty = Cic.MutInd (curi,tyno,ens) in
-       let args = args @ irl in
-       let ty = if args = [] then ty else Cic.Appl (ty::args) in
-        Cic.Lambda (Cic.Anonymous, ty, CicSubstitution.lift 1 t)
-    | n, Cic.Lambda (name,so,ty) ->
+       let ty =
+        if args = [] && irl = [] then ty
+        else
+         Cic.Appl (ty::(List.map (CicSubstitution.lift rightno) args)@irl) in
+       let he = CicSubstitution.lift (rightno + 1) outty in
+       let t =
+        if irl = [] then he
+        else Cic.Appl (he::List.map (CicSubstitution.lift 1) irl)
+       in
+        Cic.Lambda (Cic.Anonymous, ty, t)
+    | n, Cic.Prod (name,so,ty) ->
        let ty' =
         aux (n - 1) (Cic.Rel n::irl) (Some (name, Cic.Decl so)::context) ty
        in
@@ -103,9 +112,12 @@ prerr_endline ("LEFTNO: " ^ string_of_int leftno ^ "  " ^ CicPp.ppterm arity);*)
     | _,_ -> assert false
   in
 (*prerr_endline ("RIGHTNO = " ^ string_of_int rightno ^ " OUTTY = " ^ CicPp.ppterm outty);*)
-   let outty' = aux rightno [] context outty in
+   let outsort =
+    fst (CicTypeChecker.type_of_aux' [] context outty CicUniv.oblivion_ugraph)
+   in
+    try aux rightno [] context outsort
+    with Nothing_to_do -> outty
 (*prerr_endline (CicPp.ppterm outty ^ " <==> " ^ CicPp.ppterm outty');*)
-    if outty' = outty then outty else outty'
 ;;
 
 (* we are lambda-lifting also variables that do not occur *)