From 5061952d0632ba8bc77be5cab11fab2f36e1e26f Mon Sep 17 00:00:00 2001
From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Tue, 30 Sep 2008 16:44:58 +0000
Subject: [PATCH] ...

---
 .../components/ng_kernel/oCic2NCic.ml         | 31 ++++++++++++++++---
 .../components/ng_kernel/oCic2NCic.mli        |  1 +
 .../components/ng_refiner/oMeta2nMeta.ml      | 10 ++++++
 3 files changed, 37 insertions(+), 5 deletions(-)
 create mode 100644 helm/software/components/ng_refiner/oMeta2nMeta.ml

diff --git a/helm/software/components/ng_kernel/oCic2NCic.ml b/helm/software/components/ng_kernel/oCic2NCic.ml
index 0ead3ff2f..0854b624f 100644
--- a/helm/software/components/ng_kernel/oCic2NCic.ml
+++ b/helm/software/components/ng_kernel/oCic2NCic.ml
@@ -504,10 +504,6 @@ and height_of_term ?(h=ref 0) t =
    1 + !h
 ;;
 
-(* 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 *)
-let convert_term uri t = 
   (* k=true if we are converting a term to be pushed in a ctx or if we are
             converting the type of a fix;
      k=false if we are converting a term to be put in the body of a fix;
@@ -765,7 +761,12 @@ let convert_term uri t =
        match ens with
           [] -> he,objs
         | _::_ -> NCic.Appl (he::ens),objs
-  in
+;;
+
+(* 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 *)
+let convert_term uri t = 
    aux false [] [] 0 uri t
 ;;
 
@@ -843,3 +844,23 @@ let convert_obj uri obj =
 (*prerr_endline ("H(" ^ UriManager.string_of_uri uri ^ ") = " ^ string_of_int * (get_height uri));*)
   fixpoints @ [obj]
 ;;
+
+let convert_context uri =
+  let name_of = function Cic.Name s -> s | _ -> "_" in
+  List.fold_right
+    (function 
+    | (Some (s, Cic.Decl t) as e) -> fun (nc,auxc,oc) ->
+       let t, _ = aux true oc auxc 0 uri t in
+       (name_of s, NCic.Decl t) :: nc, 
+       Ce (lazy ((name_of s, NCic.Decl t),[])) :: auxc,  e :: oc
+    | (Some (Cic.Name s, Cic.Def (t,ty)) as e) -> fun (nc,auxc,oc) ->
+       let t, _ = aux true oc auxc 0 uri t in
+       let t, _ = aux true oc auxc 0 uri ty in
+       (name_of s, NCic.Def (t,ty)) :: nc, 
+       Ce (lazy ((name_of s, NCic.Def (t,ty)),[])) :: auxc,  e :: oc
+    | None -> ...
+;;
+
+let convert_term uri ctx t = 
+   aux false [] [] 0 uri t
+;;
diff --git a/helm/software/components/ng_kernel/oCic2NCic.mli b/helm/software/components/ng_kernel/oCic2NCic.mli
index 7ee5cb11d..02ee706ef 100644
--- a/helm/software/components/ng_kernel/oCic2NCic.mli
+++ b/helm/software/components/ng_kernel/oCic2NCic.mli
@@ -16,3 +16,4 @@ val nuri_of_ouri: UriManager.uri -> NUri.uri
 val reference_of_ouri: UriManager.uri -> NReference.spec -> NReference.reference
 
 val convert_obj: UriManager.uri -> Cic.obj -> NCic.obj list
+val convert_term: UriManager.uri -> Cic.term -> NCic.term * NCic.obj list
diff --git a/helm/software/components/ng_refiner/oMeta2nMeta.ml b/helm/software/components/ng_refiner/oMeta2nMeta.ml
new file mode 100644
index 000000000..4993e482a
--- /dev/null
+++ b/helm/software/components/ng_refiner/oMeta2nMeta.ml
@@ -0,0 +1,10 @@
+let convert_metasenv uri = 
+  let new_metasenv, fixpoints =
+    List.fold_left
+      (fun (nm,fty) (i, ctx, ty) ->
+         let new_ty, fix_ty = OCic2NCic.convert_term uri ty in
+
+  in
+  assert (fixpoints = []);
+  new_metasenv
+;;
-- 
2.39.2