X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic%2FcicParser2.ml;h=b641c649ecd485ca20ad4c8e85d031d94e184eaa;hb=acf29bdbdcdc6ad8c2d9d27e8a47500981b605cd;hp=562f79bba66150b0e5aea5c2e2c5cd5a5feaf856;hpb=5a92117eeff70048d29e91ba24e113155d956e1b;p=helm.git

diff --git a/helm/ocaml/cic/cicParser2.ml b/helm/ocaml/cic/cicParser2.ml
index 562f79bba..b641c649e 100644
--- a/helm/ocaml/cic/cicParser2.ml
+++ b/helm/ocaml/cic/cicParser2.ml
@@ -40,66 +40,19 @@
 exception IllFormedXml of int;;
 exception NotImplemented;;
 
-(* Utility functions that transform a Pxp attribute into something useful *)
-
-(* mk_absolute_uris "n1: v1 ... vn n2 : u1 ... un ...."      *)
-(* returns [(n1,[absolute_uri_for_v1 ; ... ; absolute_uri_for_vn]) ; (n2,...) *)
-let mk_absolute_uris s =
- let l = (Str.split (Str.regexp ":") s) in
-  let absolute_of_relative n v =
-   let module P3 = CicParser3 in
-    let rec mkburi =
-     function
-        (0,_) -> "/"
-      | (n,he::tl) when n > 0 ->
-         "/" ^ he ^ mkburi (n - 1, tl)
-      | _ -> raise (IllFormedXml 12)
-    in
-     let m = List.length !P3.current_sp - (int_of_string n) in
-      let buri = mkburi (m, !P3.current_sp) in
-       UriManager.uri_of_string ("cic:" ^ buri ^ v ^ ".var")
-  in
-   let rec absolutize =
-    function
-       [] -> []
-     | [no ; vs] ->
-        let vars = (Str.split (Str.regexp " ") vs) in
-         [(int_of_string no, List.map (absolute_of_relative no) vars)]
-     | no::vs::tl -> 
-        let vars = (Str.split (Str.regexp " ") vs) in
-         let rec add_prefix =
-          function
-             [no2] -> ([], no2)
-           | he::tl ->
-              let (pvars, no2) = add_prefix tl in
-               ((absolute_of_relative no he)::pvars, no2)
-           | _ -> raise (IllFormedXml 11)
-         in
-          let (pvars, no2) = add_prefix vars in
-           (int_of_string no, pvars)::(absolutize (no2::tl))
-     | _ -> raise (IllFormedXml 10)
-   in
-    (* last parameter must be applied first *)
-    absolutize l
-;;
+  (* TODO ZACK implement attributes parsing from XML. ATM, parsing always
+  * returns the empty list of attributes reported here *)
+let obj_attributes = []
+let get_obj_attributes (n: 'a Pxp_document.node) =
+  obj_attributes
 
-let option_uri_list_of_attr a1 a2 =
- let module T = Pxp_types in
-  let parameters =
-   match a1 with
-      T.Value s -> mk_absolute_uris s
-    | _ -> raise (IllFormedXml 0)
-  in
-   match a2 with
-      T.Value "POSSIBLE" -> Cic.Possible parameters
-    | T.Implied_value -> Cic.Actual parameters
-    | _ -> raise (IllFormedXml 0)
-;;
+(* Utility functions that transform a Pxp attribute into something useful *)
 
 let uri_list_of_attr a =
  let module T = Pxp_types in
   match a with
-     T.Value s -> mk_absolute_uris s
+     T.Value s ->
+      List.map UriManager.uri_of_string (Str.split (Str.regexp " ") s)
    | _ -> raise (IllFormedXml 0)
 ;;
 
@@ -118,6 +71,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.Anonymous
+   | _ -> raise (IllFormedXml 0)
+;;
+
 (* Other utility functions *)
 
 let get_content n =
@@ -126,14 +88,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    *)
@@ -144,31 +98,46 @@ let register_id id node =
 (* dtd                                                                        *)
 
 (* called when a CurrentProof is found *)
-let get_conjs_value_type l =
- let rec rget (c, v, t) l =
+let get_conjs_value l =
+ let rec rget (c, v) l =
   let module D = Pxp_document in
    match l with
-      [] -> (c, v, t)
+      [] -> (c, v)
     | 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 id = 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 ->
+               let id = string_of_attr (n#attribute "id") in
+                match n#node_type with
+                   D.T_element "Decl" ->
+                    let name = name_of_attr (n#attribute "name") in
+                    let term = (get_content n)#extension#to_cic_term [] in
+                     id, Some (name,Cic.ADecl term)
+                 | D.T_element "Def" ->
+                    let name = name_of_attr (n#attribute "name") in
+                    let term = (get_content n)#extension#to_cic_term [] in
+                     id, Some (name,Cic.ADef term)
+                 | D.T_element "Hidden" -> id, None
+                 | _ -> raise (IllFormedXml 14)
+             ) canonical_context
+       in
+        rget ((id, no, canonical_context, typ)::c, v) tl
     | value::tl when value#node_type = D.T_element "body" ->
-       let v' = (get_content value)#extension#to_cic_term in
+       let v' = (get_content value)#extension#to_cic_term [] in
         (match v with
-            None -> rget (c, Some v', t) tl
+            None -> rget (c, Some v') tl
           | _    -> raise (IllFormedXml 2)
         )
-    | typ::tl when typ#node_type = D.T_element "type" ->
-       let t' = (get_content typ)#extension#to_cic_term in
-        (match t with
-            None -> rget (c, v, Some t') tl
-          | _    -> raise (IllFormedXml 3)
-        )
     | _ -> raise (IllFormedXml 4)
  in
-  match rget ([], None, None) l with
-     (c, Some v, Some t) -> (c, v, t)
+  match rget ([], None) l with
+     (revc, Some v) -> (List.rev revc, v)
    | _ -> raise (IllFormedXml 5)
 ;;
 
@@ -180,12 +149,12 @@ let get_names_arity_constructors l =
    match l with
       [] -> (a, c)
     | arity::tl when arity#node_type = D.T_element "arity" ->
-       let a' = (get_content arity)#extension#to_cic_term in
+       let a' = (get_content arity)#extension#to_cic_term [] in
         rget (Some a',c) tl
     | con::tl when con#node_type = D.T_element "Constructor" ->
        let id = string_of_attr (con#attribute "name")
-       and ty = (get_content con)#extension#to_cic_term in
-         rget (a,(id,ty,ref None)::c) tl
+       and ty = (get_content con)#extension#to_cic_term [] in
+         rget (a,(id,ty)::c) tl
     | _ -> raise (IllFormedXml 9)
  in
   match rget (None,[]) l with
@@ -200,10 +169,11 @@ let rec get_inductive_types =
   | he::tl ->
      let tyname    = string_of_attr (he#attribute "name")
      and inductive = bool_of_attr   (he#attribute "inductive")
+     and xid = string_of_attr (he#attribute "id")
      and (arity,cons) =
       get_names_arity_constructors (he#sub_nodes)
      in
-      (tyname,inductive,arity,cons)::(get_inductive_types tl) (*CSC 0 a caso *)
+      (xid,tyname,inductive,arity,cons)::(get_inductive_types tl)
 ;;
 
 (* This is the main function and also the only one used directly from *)
@@ -211,59 +181,61 @@ let rec get_inductive_types =
 (* representation of the cic object described in the tree             *)
 (* It uses the previous functions and the to_cic_term method defined  *)
 (* in cicParser3 (used for subtrees that encode cic terms)            *)
-let rec get_term n =
+let rec get_term (n : CicParser3.cic_term Pxp_document.node) nbody
+=
+ let module U = UriManager in
  let module D = Pxp_document in
  let module C = Cic in
-  let ntype = n # node_type in
+  let obj_attrs = get_obj_attributes n in
+  let ntype = n#node_type in
   match ntype with
-    D.T_element "Definition" ->
-      let id = string_of_attr (n # attribute "name")
-      and params =
-       option_uri_list_of_attr (n#attribute "params") (n#attribute "paramMode")
-      and (value, typ) = 
-       let sons = n#sub_nodes in
-        match sons with
-          [v ; t] when
-            v#node_type = D.T_element "body" &&
-            t#node_type = D.T_element "type" ->
-             let v' = get_content v
-             and t' = get_content t in
-              (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
-  | 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
-  | 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
+    D.T_element "ConstantType" ->
+      let name = string_of_attr (n # attribute "name") in
+      let params = uri_list_of_attr (n#attribute "params") in
+      let xid = string_of_attr (n#attribute "id") in
+      let typ = (get_content n)#extension#to_cic_term [] in
+       (match nbody with
+           None ->
+            (* Axiom *)
+            C.AConstant (xid, None, name, None, typ, params, obj_attrs)
+         | Some nbody' ->
+            let nbodytype = nbody'#node_type in
+            match nbodytype with
+             D.T_element "ConstantBody" ->
+(*CSC: the attribute "for" is ignored and not checked
+              let for_ = string_of_attr (nbody'#attribute "for") in
+*)
+              let paramsbody = uri_list_of_attr (nbody'#attribute "params") in
+              let xidbody = string_of_attr (nbody'#attribute "id") in
+              let value = (get_content nbody')#extension#to_cic_term [] in
+               if paramsbody = params then
+                C.AConstant (xid, Some xidbody, name, Some value, typ, params,
+                  obj_attrs)
+               else
+                raise (IllFormedXml 6)
+           | D.T_element "CurrentProof" ->
+(*CSC: the attribute "of" is ignored and not checked
+              let for_ = string_of_attr (nbody'#attribute "of") in
+*)
+              let xidbody = string_of_attr (nbody'#attribute "id") in
+              let sons = nbody'#sub_nodes in
+               let (conjs, value) = get_conjs_value sons in
+                C.ACurrentProof (xid, xidbody, name, conjs, value, typ, params,
+                  obj_attrs)
+           | D.T_element _
+           | D.T_data
+           | _ -> raise (IllFormedXml 6)
+       )
   | 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, obj_attrs)
   | D.T_element "Variable" ->
      let name = string_of_attr (n#attribute "name")
+     and params = uri_list_of_attr (n#attribute "params")
      and xid = string_of_attr (n#attribute "id")
      and (body, typ) = 
       let sons = n#sub_nodes in
@@ -273,17 +245,14 @@ let rec get_term n =
             t#node_type = D.T_element "type" ->
              let b' = get_content b
              and t' = get_content t in
-              (Some (b'#extension#to_cic_term), t'#extension#to_cic_term)
+              (Some (b'#extension#to_cic_term []), t'#extension#to_cic_term [])
         | [t] when t#node_type = D.T_element "type" ->
              let t' = get_content t in
-              (None, t'#extension#to_cic_term)
+              (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,params,obj_attrs)
   | D.T_element _
   | D.T_data
-  | _ ->
-     raise (IllFormedXml 7)
+  | _ -> raise (IllFormedXml 7)
 ;;