Tentative (and bad!) fix of outtypes in non-dependent eliminations.

The fix does not work since there is no guarantee in Coq that the outtype
is made of a sequence of Lambdas (and indeed it is not for automatically
generated elimiantion principles). Thus I need to perform recursion on the
type of the outtype and I also need to perform some eta-expansion to insert
the additional lambda in the right position :-(

diff --git a/helm/software/components/ng_kernel/oCic2NCic.ml b/helm/software/components/ng_kernel/oCic2NCic.ml
index d758c2ca686e99c55d9bde8e86d1cdd737e58fc4..af9642e3f1657eeb47e6d0f2b12d73b717018eb1 100644 (file)
--- a/helm/software/components/ng_kernel/oCic2NCic.ml
+++ b/helm/software/components/ng_kernel/oCic2NCic.ml
@@ -61,6 +61,53 @@ let splat_args ctx t n_fix =
    NCic.Appl (t:: aux (List.length ctx))
 ;;
 
+let fix_outty curi tyno t context outty =
+ let leftno,rightno =
+  match fst (CicEnvironment.get_obj CicUniv.oblivion_ugraph curi) with
+     Cic.InductiveDefinition (tyl,_,leftno,_) ->
+      let _,_,arity,_ = List.nth tyl tyno in
+      let rec count_prods leftno context arity =
+       match leftno, CicReduction.whd context arity with
+          0, Cic.Sort _ -> 0
+        | 0, Cic.Prod (name,so,ty) ->
+           1 + count_prods 0 (Some (name, Cic.Decl so)::context) ty
+        | n, Cic.Prod (name,so,ty) ->
+           count_prods (leftno - 1) (Some (name, Cic.Decl so)::context) ty
+        | _,_ -> assert false
+      in
+(*prerr_endline (UriManager.string_of_uri curi);
+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
+     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 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' =
+        aux (n - 1) (Cic.Rel n::irl) (Some (name, Cic.Decl so)::context) ty
+       in
+        Cic.Lambda (name,so,ty')
+    | _,_ -> assert false
+  in
+(*prerr_endline ("RIGHTNO = " ^ string_of_int rightno ^ " OUTTY = " ^ CicPp.ppterm outty);*)
+   let outty' = aux rightno [] context outty in
+(*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 *)
 (* ctx does not distinguish successive blocks of cofix, since there may be no
  *   lambda separating them *)
@@ -216,9 +263,10 @@ let convert_term uri t =
     | Cic.MutConstruct (curi, tyno, consno, ens) -> 
        aux_ens octx ctx n_fix uri ens
         (NCic.Const (Ref.reference_of_ouri curi (Ref.Con (tyno,consno))))
-    | Cic.MutCase (curi, tyno, oty, t, branches) ->
+    | Cic.MutCase (curi, tyno, outty, t, branches) ->
+        let outty = fix_outty curi tyno t octx outty in
         let r = Ref.reference_of_ouri curi (Ref.Ind tyno) in
-        let oty, fixpoints_oty = aux octx ctx n_fix uri oty in
+        let outty, fixpoints_outty = aux octx ctx n_fix uri outty in
         let t, fixpoints_t = aux octx ctx n_fix uri t in
         let branches, fixpoints =
           List.fold_right 
@@ -227,7 +275,7 @@ let convert_term uri t =
                (t::l,fixpoints@acc))
              branches ([],[])
         in
-        NCic.Match (r,oty,t,branches), fixpoints_oty @ fixpoints_t @ fixpoints
+        NCic.Match (r,outty,t,branches), fixpoints_outty@fixpoints_t@fixpoints
     | Cic.Implicit _ | Cic.Meta _ | Cic.Var _ -> assert false
   and aux_ens octx ctx n_fix uri ens he =
    match ens with