Initial revision

[helm.git] / helm / ocaml / cic / cicParser2.ml

diff --git a/helm/ocaml/cic/cicParser2.ml b/helm/ocaml/cic/cicParser2.ml
index 562f79bba66150b0e5aea5c2e2c5cd5a5feaf856..154b294ce7daff797cbd3d27fa1f0e85292332e4 100644 (file)
--- a/helm/ocaml/cic/cicParser2.ml
+++ b/helm/ocaml/cic/cicParser2.ml
@@ -118,6 +118,15 @@ let bool_of_attr a =
  bool_of_string (string_of_attr a)
 ;;
 
+let name_of_attr a =
+ let module T = Pxp_types in
+ let module C = Cic in
+  match a with
+     T.Value s -> C.Name s
+   | T.Implied_value -> C.Anonimous
+   | _ -> raise (IllFormedXml 0)
+;;
+
 (* Other utility functions *)
 
 let get_content n =
@@ -126,14 +135,6 @@ let get_content n =
   | _     -> raise (IllFormedXml 1)
 ;;
 
-let register_id id node =
- if !CicParser3.process_annotations then
-  match !CicParser3.ids_to_targets with
-     None -> assert false
-   | Some ids_to_targets ->
-      Hashtbl.add ids_to_targets id (Cic.Object node)
-;;
-
 (* Functions that, given the list of sons of a node of the cic dom (objects   *)
 (* level), retrieve the internal representation associated to the node.       *)
 (* Everytime a cic term subtree is found, it is translated to the internal    *)
@@ -150,9 +151,33 @@ let get_conjs_value_type l =
    match l with
       [] -> (c, v, t)
     | conj::tl when conj#node_type = D.T_element "Conjecture" ->
-       let no = int_of_attr (conj#attribute "no")
-       and typ = (get_content conj)#extension#to_cic_term in
-        rget ((no, typ)::c, v, t) tl
+       let no = int_of_attr (conj#attribute "no") in
+       let xid = string_of_attr (conj#attribute "id") in
+       let typ,canonical_context =
+        match List.rev (conj#sub_nodes) with
+           [] -> raise (IllFormedXml 13)
+         | typ::canonical_context ->
+            (get_content typ)#extension#to_cic_term,
+            List.map
+             (function n ->
+               match n#node_type with
+                  D.T_element "Decl" ->
+                   let name = name_of_attr (n#attribute "name") in
+                   let hid = string_of_attr (n#attribute "id") in
+                   let term = (get_content n)#extension#to_cic_term in
+                    hid,Some (name,Cic.ADecl term)
+                | D.T_element "Def" ->
+                   let name = name_of_attr (n#attribute "name") in
+                   let hid = string_of_attr (n#attribute "id") in
+                   let term = (get_content n)#extension#to_cic_term in
+                    hid,Some (name,Cic.ADef term)
+                | D.T_element "Hidden" ->
+                   let hid = string_of_attr (n#attribute "id") in
+                    hid,None
+                | _ -> raise (IllFormedXml 14)
+             ) canonical_context
+       in
+        rget ((xid, no, canonical_context, typ)::c, v, t) tl
     | value::tl when value#node_type = D.T_element "body" ->
        let v' = (get_content value)#extension#to_cic_term in
         (match v with
@@ -168,7 +193,7 @@ let get_conjs_value_type l =
     | _ -> raise (IllFormedXml 4)
  in
   match rget ([], None, None) l with
-     (c, Some v, Some t) -> (c, v, t)
+     (revc, Some v, Some t) -> (List.rev revc, v, t)
    | _ -> raise (IllFormedXml 5)
 ;;
 
@@ -231,37 +256,27 @@ let rec get_term n =
               (v'#extension#to_cic_term, t'#extension#to_cic_term)
         | _ -> raise (IllFormedXml 6)
       and xid = string_of_attr (n#attribute "id") in
-       let res = C.ADefinition (xid, ref None, id, value, typ, params) in
-        register_id xid res ;
-        res
+       C.ADefinition (xid, id, value, typ, params)
   | D.T_element "Axiom" ->
       let id = string_of_attr (n # attribute "name")
       and params = uri_list_of_attr (n # attribute "params")
       and typ = 
        (get_content (get_content n))#extension#to_cic_term
       and xid = string_of_attr (n#attribute "id") in
-       let res = C.AAxiom (xid, ref None, id, typ, params) in
-        register_id xid res ;
-        res
+       C.AAxiom (xid, id, typ, params)
   | D.T_element "CurrentProof" ->
      let name = string_of_attr (n#attribute "name")
      and xid = string_of_attr (n#attribute "id") in
      let sons = n#sub_nodes in
       let (conjs, value, typ) = get_conjs_value_type sons in
-       let res = C.ACurrentProof (xid, ref None, name, conjs, value, typ) in
-        register_id xid res ;
-        res
+       C.ACurrentProof (xid, name, conjs, value, typ)
   | D.T_element "InductiveDefinition" ->
      let sons = n#sub_nodes
      and xid = string_of_attr (n#attribute "id") in
       let inductiveTypes = get_inductive_types sons
       and params = uri_list_of_attr (n#attribute "params")
       and nparams = int_of_attr (n#attribute "noParams") in
-       let res =
-        C.AInductiveDefinition (xid, ref None, inductiveTypes, params, nparams)
-       in
-        register_id xid res ;
-        res
+       C.AInductiveDefinition (xid, inductiveTypes, params, nparams)
   | D.T_element "Variable" ->
      let name = string_of_attr (n#attribute "name")
      and xid = string_of_attr (n#attribute "id")
@@ -279,9 +294,7 @@ let rec get_term n =
               (None, t'#extension#to_cic_term)
         | _ -> raise (IllFormedXml 6)
      in
-      let res = C.AVariable (xid,ref None,name,body,typ) in
-       register_id xid res ;
-       res
+      C.AVariable (xid,name,body,typ)
   | D.T_element _
   | D.T_data
   | _ ->