From 35e102fec6bad146fee425f299a93520e657e7c2 Mon Sep 17 00:00:00 2001
From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Mon, 7 Apr 2008 22:00:51 +0000
Subject: [PATCH] Cooking implemented (not tested yet).

---
 .../components/ng_kernel/oCic2NCic.ml         | 64 +++++++++++++++----
 1 file changed, 51 insertions(+), 13 deletions(-)

diff --git a/helm/software/components/ng_kernel/oCic2NCic.ml b/helm/software/components/ng_kernel/oCic2NCic.ml
index 095b967a4..cd90fbdf5 100644
--- a/helm/software/components/ng_kernel/oCic2NCic.ml
+++ b/helm/software/components/ng_kernel/oCic2NCic.ml
@@ -146,7 +146,7 @@ let convert_term uri t =
             fl tys ([],fixpoints_tys,0)
         in
         let obj = 
-          NUri.nuri_of_ouri buri,0,[],[],
+          NUri.nuri_of_ouri buri,max_int,[],[],
             NCic.Fixpoint (true, fl, (`Generated, `Definition)) 
         in
         splat_args ctx
@@ -202,18 +202,20 @@ let convert_term uri t =
         (match l with
         | (NCic.Appl l1)::l2 -> NCic.Appl (l1@l2), fixpoints
         | _ -> NCic.Appl l, fixpoints)
-    | Cic.Const (curi, _) -> 
+    | Cic.Const (curi, ens) -> 
+       aux_ens octx ctx n_fix uri ens
         (match fst(CicEnvironment.get_obj CicUniv.oblivion_ugraph curi) with
         | Cic.Constant (_,Some _,_,_,_) ->
-               NCic.Const (Ref.reference_of_ouri curi Ref.Def),[]
+               NCic.Const (Ref.reference_of_ouri curi Ref.Def)
         | Cic.Constant (_,None,_,_,_) ->
-               NCic.Const (Ref.reference_of_ouri curi Ref.Decl),[]
+               NCic.Const (Ref.reference_of_ouri curi Ref.Decl)
         | _ -> assert false)
-    | Cic.MutInd (curi, tyno, _) -> 
-        NCic.Const (Ref.reference_of_ouri curi (Ref.Ind tyno)),[]
-    | Cic.MutConstruct (curi, tyno, consno, _) -> 
-        NCic.Const (Ref.reference_of_ouri curi 
-        (Ref.Con (tyno,consno))),[]
+    | Cic.MutInd (curi, tyno, ens) -> 
+       aux_ens octx ctx n_fix uri ens
+        (NCic.Const (Ref.reference_of_ouri curi (Ref.Ind tyno)))
+    | 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) ->
         let r = Ref.reference_of_ouri curi (Ref.Ind tyno) in
         let oty, fixpoints_oty = aux octx ctx n_fix uri oty in
@@ -227,31 +229,67 @@ let convert_term uri t =
         in
         NCic.Match (r,oty,t,branches), fixpoints_oty @ fixpoints_t @ fixpoints
     | Cic.Implicit _ | Cic.Meta _ | Cic.Var _ -> assert false
+  and aux_ens octx ctx n_fix uri ens he =
+   match ens with
+      [] -> he,[]
+    | _::_ ->
+      let ens,objs =
+       List.fold_right
+        (fun (_,t) (l,objs) ->
+          let t,o = aux octx ctx n_fix uri t in
+           t::l, o@objs
+        ) ens ([],[])
+      in
+       NCic.Appl (he::ens),objs
   in
    aux [] [] 0 uri t
 ;;
 
+let cook vars t =
+ let t = CicSubstitution.lift (List.length vars) t in
+ snd (List.fold_right
+  (fun uri (n,t) ->
+    let t = CicSubstitution.subst_vars [uri,Cic.Rel 1] t in
+    let bo,ty =
+     match fst (CicEnvironment.get_obj CicUniv.oblivion_ugraph uri) with
+        Cic.Variable (_,bo,ty,_,_) -> bo,ty
+      | _ -> assert false in
+    let id = Cic.Name (UriManager.name_of_uri uri) in
+    let t =
+     match bo,ty with
+        None,ty -> Cic.Lambda (id,ty,t)
+      | Some bo,ty -> Cic.LetIn (id,bo,ty,t)
+    in
+     n+1,t
+  ) vars (1,t))
+;;
+
 let convert_obj_aux uri = function
- | Cic.Constant (name, None, ty, _, _) ->
+ | Cic.Constant (name, None, ty, vars, _) ->
+     let ty = cook vars ty in
      let nty, fixpoints = convert_term uri ty in
      assert(fixpoints = []);
      NCic.Constant ([], name, None, nty, (`Provided,`Theorem,`Regular)),
      fixpoints
- | Cic.Constant (name, Some bo, ty, _, _) ->
+ | Cic.Constant (name, Some bo, ty, vars, _) ->
+     let bo = cook vars bo in
+     let ty = cook vars ty in
      let nbo, fixpoints_bo = convert_term uri bo in
      let nty, fixpoints_ty = convert_term uri ty in
      assert(fixpoints_ty = []);
      NCic.Constant ([], name, Some nbo, nty, (`Provided,`Theorem,`Regular)),
      fixpoints_bo @ fixpoints_ty
- | Cic.InductiveDefinition (itl,_,leftno,_) -> 
+ | Cic.InductiveDefinition (itl,vars,leftno,_) -> 
      let ind = let _,x,_,_ = List.hd itl in x in
      let itl, fix_itl = 
        List.fold_right
          (fun (name, _, ty, cl) (itl,acc) ->
+            let ty = cook vars ty in
             let ty, fix_ty = convert_term uri ty in
             let cl, fix_cl = 
               List.fold_right
                (fun (name, ty) (cl,acc) -> 
+                 let ty = cook vars ty in
                  let ty, fix_ty = convert_term uri ty in
                  ([], name, ty)::cl, acc @ fix_ty)
                cl ([],[])
@@ -259,7 +297,7 @@ let convert_obj_aux uri = function
             ([], name, ty, cl)::itl, fix_ty @ fix_cl @ acc)
          itl ([],[])
      in
-     NCic.Inductive (ind, leftno, itl, (`Provided, `Regular)),
+     NCic.Inductive(ind, leftno + List.length vars, itl, (`Provided, `Regular)),
      fix_itl
  | Cic.Variable _ 
  | Cic.CurrentProof _ -> assert false
-- 
2.39.2