Conjectures and Hypotheses inside every conjecture and in the sequents now

[helm.git] / helm / gTopLevel / cic2acic.ml

diff --git a/helm/gTopLevel/cic2acic.ml b/helm/gTopLevel/cic2acic.ml
index d7688499c7cbfe497d6e30485cf3341cef98b1d1..ffe9dbd4db98f0e1abe90fc2851b84484c3680c8 100644 (file)
--- a/helm/gTopLevel/cic2acic.ml
+++ b/helm/gTopLevel/cic2acic.ml
@@ -205,14 +205,16 @@ let acic_of_cic_context metasenv context t =
 
 exception Found of (Cic.name * Cic.context_entry) list;;
 
-exception NotImplemented;;
-
 let acic_object_of_cic_object obj =
  let module C = Cic 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
   let ids_to_inner_types = Hashtbl.create 503 in
+  let ids_to_conjectures = Hashtbl.create 11 in
+  let ids_to_hypotheses = Hashtbl.create 127 in
+  let hypotheses_seed = ref 0 in
+  let conjectures_seed = ref 0 in
   let seed = ref 0 in
   let acic_term_of_cic_term_context' =
    acic_of_cic_context' seed ids_to_terms ids_to_father_ids ids_to_inner_sorts
@@ -230,34 +232,43 @@ let acic_object_of_cic_object obj =
     | C.CurrentProof (id,conjectures,bo,ty) ->
        let aconjectures =
         List.map
-         (function (i,canonical_context,term) ->
-           let acanonical_context =
-            let rec aux =
-             function
-                [] -> []
-              | (Some (n,C.Decl t))::tl ->
-                  let at =
-                   acic_term_of_cic_term_context' conjectures tl t
-                  in
-                   Some (n,C.ADecl at)::(aux tl)
-              | (Some (n,C.Def t))::tl ->
-                  let at =
-                   acic_term_of_cic_term_context' conjectures tl t
-                  in
-                   Some (n,C.ADef at)::(aux tl)
-               | None::tl -> None::(aux tl)
-            in
-             aux canonical_context
-           in
-            let aterm =
-             acic_term_of_cic_term_context' conjectures canonical_context term
+         (function (i,canonical_context,term) as conjecture ->
+           let cid = "c" ^ string_of_int !conjectures_seed in
+            Hashtbl.add ids_to_conjectures cid conjecture ;
+            incr conjectures_seed ;
+            let acanonical_context =
+             let rec aux =
+              function
+                 [] -> []
+               | hyp::tl ->
+                  let hid = "h" ^ string_of_int !hypotheses_seed in
+                   Hashtbl.add ids_to_hypotheses hid hyp ;
+                   incr hypotheses_seed ;
+                   match hyp with
+                      (Some (n,C.Decl t)) ->
+                        let at =
+                         acic_term_of_cic_term_context' conjectures tl t
+                        in
+                         (hid,Some (n,C.ADecl at))::(aux tl)
+                    | (Some (n,C.Def t)) ->
+                        let at =
+                         acic_term_of_cic_term_context' conjectures tl t
+                        in
+                         (hid,Some (n,C.ADef at))::(aux tl)
+                    | None -> (hid,None)::(aux tl)
+             in
+              aux canonical_context
             in
-             (i, acanonical_context,aterm)
+             let aterm =
+              acic_term_of_cic_term_context' conjectures canonical_context term
+             in
+              (cid,i,acanonical_context,aterm)
          ) conjectures in
        let abo = acic_term_of_cic_term_context' conjectures [] bo in
        let aty = acic_term_of_cic_term_context' conjectures [] ty in
         C.ACurrentProof ("mettereaposto",id,aconjectures,abo,aty)
     | C.InductiveDefinition (tys,params,paramsno) -> raise NotImplemented
    in
-    aobj,ids_to_terms,ids_to_father_ids,ids_to_inner_sorts,ids_to_inner_types
+    aobj,ids_to_terms,ids_to_father_ids,ids_to_inner_sorts,ids_to_inner_types,
+     ids_to_conjectures,ids_to_hypotheses
 ;;