From 02744ec842e0ac8b978feb519247d434ebbe8d67 Mon Sep 17 00:00:00 2001
From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Sun, 20 Jul 2003 15:53:12 +0000
Subject: [PATCH] Cic2acic is now responsible of eta-fixing the objects (using
 the Eta_fix module).

---
 helm/ocaml/cic_omdoc/.depend     |  4 +--
 helm/ocaml/cic_omdoc/cic2acic.ml | 44 ++++++++++++++++++++++++--------
 2 files changed, 36 insertions(+), 12 deletions(-)

diff --git a/helm/ocaml/cic_omdoc/.depend b/helm/ocaml/cic_omdoc/.depend
index 5dfc55b8a..9e8bfadb7 100644
--- a/helm/ocaml/cic_omdoc/.depend
+++ b/helm/ocaml/cic_omdoc/.depend
@@ -5,8 +5,8 @@ eta_fixing.cmo: eta_fixing.cmi
 eta_fixing.cmx: eta_fixing.cmi 
 doubleTypeInference.cmo: doubleTypeInference.cmi 
 doubleTypeInference.cmx: doubleTypeInference.cmi 
-cic2acic.cmo: doubleTypeInference.cmi cic2acic.cmi 
-cic2acic.cmx: doubleTypeInference.cmx cic2acic.cmi 
+cic2acic.cmo: doubleTypeInference.cmi eta_fixing.cmi cic2acic.cmi 
+cic2acic.cmx: doubleTypeInference.cmx eta_fixing.cmx cic2acic.cmi 
 content.cmo: content.cmi 
 content.cmx: content.cmi 
 contentPp.cmo: content.cmi contentPp.cmi 
diff --git a/helm/ocaml/cic_omdoc/cic2acic.ml b/helm/ocaml/cic_omdoc/cic2acic.ml
index a3cdfbb78..b8679dc62 100644
--- a/helm/ocaml/cic_omdoc/cic2acic.ml
+++ b/helm/ocaml/cic_omdoc/cic2acic.ml
@@ -298,6 +298,7 @@ let acic_of_cic_context metasenv context idrefs t =
 
 let acic_object_of_cic_object obj =
  let module C = Cic in
+ let module E = Eta_fixing in
   let ids_to_terms = Hashtbl.create 503 in
   let ids_to_father_ids = Hashtbl.create 503 in
   let ids_to_inner_sorts = Hashtbl.create 503 in
@@ -314,24 +315,45 @@ let acic_object_of_cic_object obj =
    let aobj =
     match obj with
       C.Constant (id,Some bo,ty,params) ->
-       let abo = acic_term_of_cic_term' bo (Some ty) in
-       let aty = acic_term_of_cic_term' ty None in
+       let bo' = E.eta_fix [] bo in
+       let ty' = E.eta_fix [] ty in
+       let abo = acic_term_of_cic_term' bo' (Some ty') in
+       let aty = acic_term_of_cic_term' ty' None in
         C.AConstant
-         ("mettereaposto",Some "mettereaposto2",id,Some abo,aty, params)
+         ("mettereaposto",Some "mettereaposto2",id,Some abo,aty,params)
     | C.Constant (id,None,ty,params) ->
-       let aty = acic_term_of_cic_term' ty None in
+       let ty' = E.eta_fix [] ty in
+       let aty = acic_term_of_cic_term' ty' None in
         C.AConstant
-         ("mettereaposto",None,id,None,aty, params)
+         ("mettereaposto",None,id,None,aty,params)
     | C.Variable (id,bo,ty,params) ->
+       let ty' = E.eta_fix [] ty in
        let abo =
         match bo with
            None -> None
-         | Some bo -> Some (acic_term_of_cic_term' bo (Some ty))
+         | Some bo ->
+            let bo' = E.eta_fix [] bo in
+             Some (acic_term_of_cic_term' bo' (Some ty'))
        in
-       let aty = acic_term_of_cic_term' ty None in
+       let aty = acic_term_of_cic_term' ty' None in
         C.AVariable
          ("mettereaposto",id,abo,aty, params)
     | C.CurrentProof (id,conjectures,bo,ty,params) ->
+       let conjectures' =
+        List.map
+         (function (i,canonical_context,term) ->
+           let canonical_context' =
+            List.map
+             (function
+                 None -> None
+               | Some (n, C.Decl t)-> Some (n, C.Decl (E.eta_fix conjectures t))
+               | Some (n, C.Def t) -> Some (n, C.Def (E.eta_fix conjectures t))
+             ) canonical_context
+           in
+           let term' = E.eta_fix conjectures term in
+            (i,canonical_context',term')
+         ) conjectures
+       in
        let aconjectures =
         List.map
          (function (i,canonical_context,term) as conjecture ->
@@ -377,10 +399,12 @@ let acic_object_of_cic_object obj =
                canonical_context idrefs' term None
              in
               (cid,i,(List.rev revacanonical_context),aterm)
-         ) conjectures in
+         ) conjectures' in
+       let bo' = E.eta_fix conjectures' bo in
+       let ty' = E.eta_fix conjectures' ty in
        let abo =
-        acic_term_of_cic_term_context' conjectures [] [] bo (Some ty) in
-       let aty = acic_term_of_cic_term_context' conjectures [] [] ty None in
+        acic_term_of_cic_term_context' conjectures' [] [] bo' (Some ty') in
+       let aty = acic_term_of_cic_term_context' conjectures' [] [] ty' None in
         C.ACurrentProof
          ("mettereaposto","mettereaposto2",id,aconjectures,abo,aty,params)
     | C.InductiveDefinition (tys,params,paramsno) ->
-- 
2.39.2