helm/interface/cicParser2.ml

   1 (******************************************************************************)
   2 (*                                                                            *)
   3 (*                               PROJECT HELM                                 *)
   4 (*                                                                            *)
   5 (*                Claudio Sacerdoti Coen <sacerdot@@cs.unibo.it>              *)
   6 (*                                 24/01/2000                                 *)
   7 (*                                                                            *)
   8 (* This module is the objects level of a parser for cic objects from xml      *)
   9 (* files to the internal representation. It uses the module cicParser3        *)
  10 (* cicParser3 (terms level) and it is used only through cicParser2 (top       *)
  11 (* level).                                                                    *)
  12 (*                                                                            *)
  13 (******************************************************************************)
  14
  15 exception IllFormedXml of int;;
  16 exception NotImplemented;;
  17
  18 (* Utility functions that transform a Pxp attribute into something useful *)
  19
  20 (* mk_absolute_uris "n1: v1 ... vn n2 : u1 ... un ...."      *)
  21 (* returns [(n1,[absolute_uri_for_v1 ; ... ; absolute_uri_for_vn]) ; (n2,...) *)
  22 let mk_absolute_uris s =
  23  let l = (Str.split (Str.regexp ":") s) in
  24   let absolute_of_relative n v =
  25    let module P3 = CicParser3 in
  26     let rec mkburi =
  27      function
  28         (0,_) -> "/"
  29       | (n,he::tl) when n > 0 ->
  30          "/" ^ he ^ mkburi (n - 1, tl)
  31       | _ -> raise (IllFormedXml 12)
  32     in
  33      let m = List.length !P3.current_sp - (int_of_string n) in
  34       let buri = mkburi (m, !P3.current_sp) in
  35        UriManager.uri_of_string ("cic:" ^ buri ^ v ^ ".var")
  36   in
  37    let rec absolutize =
  38     function
  39        [] -> []
  40      | [no ; vs] ->
  41         let vars = (Str.split (Str.regexp " ") vs) in
  42          [(int_of_string no, List.map (absolute_of_relative no) vars)]
  43      | no::vs::tl ->
  44         let vars = (Str.split (Str.regexp " ") vs) in
  45          let rec add_prefix =
  46           function
  47              [no2] -> ([], no2)
  48            | he::tl ->
  49               let (pvars, no2) = add_prefix tl in
  50                ((absolute_of_relative no he)::pvars, no2)
  51            | _ -> raise (IllFormedXml 11)
  52          in
  53           let (pvars, no2) = add_prefix vars in
  54            (int_of_string no, pvars)::(absolutize (no2::tl))
  55      | _ -> raise (IllFormedXml 10)
  56    in
  57     (* last parameter must be applied first *)
  58     absolutize l
  59 ;;
  60
  61 let option_uri_list_of_attr a1 a2 =
  62  let module T = Pxp_types in
  63   let parameters =
  64    match a1 with
  65       T.Value s -> mk_absolute_uris s
  66     | _ -> raise (IllFormedXml 0)
  67   in
  68    match a2 with
  69       T.Value "POSSIBLE" -> Cic.Possible parameters
  70     | T.Implied_value -> Cic.Actual parameters
  71     | _ -> raise (IllFormedXml 0)
  72 ;;
  73
  74 let uri_list_of_attr a =
  75  let module T = Pxp_types in
  76   match a with
  77      T.Value s -> mk_absolute_uris s
  78    | _ -> raise (IllFormedXml 0)
  79 ;;
  80
  81 let string_of_attr a =
  82  let module T = Pxp_types in
  83   match a with
  84      T.Value s -> s
  85    | _ -> raise (IllFormedXml 0)
  86 ;;
  87
  88 let int_of_attr a =
  89  int_of_string (string_of_attr a)
  90 ;;
  91
  92 let bool_of_attr a =
  93  bool_of_string (string_of_attr a)
  94 ;;
  95
  96 (* Other utility functions *)
  97
  98 let get_content n =
  99  match n#sub_nodes with
 100     [ t ] -> t
 101   | _     -> raise (IllFormedXml 1)
 102 ;;
 103
 104 let register_id id node =
 105  if !CicParser3.process_annotations then
 106   match !CicParser3.ids_to_targets with
 107      None -> assert false
 108    | Some ids_to_targets ->
 109       Hashtbl.add ids_to_targets id (Cic.Object node)
 110 ;;
 111
 112 (* Functions that, given the list of sons of a node of the cic dom (objects   *)
 113 (* level), retrieve the internal representation associated to the node.       *)
 114 (* Everytime a cic term subtree is found, it is translated to the internal    *)
 115 (* representation using the method to_cic_term defined in cicParser3.         *)
 116 (* Each function raise IllFormedXml if something goes wrong, but this should  *)
 117 (* be impossible due to the presence of the dtd                               *)
 118 (* The functions should really be obvious looking at their name and the cic   *)
 119 (* dtd                                                                        *)
 120
 121 (* called when a CurrentProof is found *)
 122 let get_conjs_value_type l =
 123  let rec rget (c, v, t) l =
 124   let module D = Pxp_document in
 125    match l with
 126       [] -> (c, v, t)
 127     | conj::tl when conj#node_type = D.T_element "Conjecture" ->
 128        let no = int_of_attr (conj#attribute "no")
 129        and typ = (get_content conj)#extension#to_cic_term in
 130         rget ((no, typ)::c, v, t) tl
 131     | value::tl when value#node_type = D.T_element "body" ->
 132        let v' = (get_content value)#extension#to_cic_term in
 133         (match v with
 134             None -> rget (c, Some v', t) tl
 135           | _    -> raise (IllFormedXml 2)
 136         )
 137     | typ::tl when typ#node_type = D.T_element "type" ->
 138        let t' = (get_content typ)#extension#to_cic_term in
 139         (match t with
 140             None -> rget (c, v, Some t') tl
 141           | _    -> raise (IllFormedXml 3)
 142         )
 143     | _ -> raise (IllFormedXml 4)
 144  in
 145   match rget ([], None, None) l with
 146      (c, Some v, Some t) -> (c, v, t)
 147    | _ -> raise (IllFormedXml 5)
 148 ;;
 149
 150 (* used only by get_inductive_types; called one time for each inductive  *)
 151 (* definitions in a block of inductive definitions                       *)
 152 let get_names_arity_constructors l =
 153  let rec rget (a,c) l =
 154   let module D = Pxp_document in
 155    match l with
 156       [] -> (a, c)
 157     | arity::tl when arity#node_type = D.T_element "arity" ->
 158        let a' = (get_content arity)#extension#to_cic_term in
 159         rget (Some a',c) tl
 160     | con::tl when con#node_type = D.T_element "Constructor" ->
 161        let id = string_of_attr (con#attribute "name")
 162        and ty = (get_content con)#extension#to_cic_term in
 163          rget (a,(id,ty,ref None)::c) tl
 164     | _ -> raise (IllFormedXml 9)
 165  in
 166   match rget (None,[]) l with
 167      (Some a, c) -> (a, List.rev c)
 168    | _ -> raise (IllFormedXml 8)
 169 ;;
 170
 171 (* called when an InductiveDefinition is found *)
 172 let rec get_inductive_types =
 173  function
 174     []     -> []
 175   | he::tl ->
 176      let tyname    = string_of_attr (he#attribute "name")
 177      and inductive = bool_of_attr   (he#attribute "inductive")
 178      and (arity,cons) =
 179       get_names_arity_constructors (he#sub_nodes)
 180      in
 181       (tyname,inductive,arity,cons)::(get_inductive_types tl) (*CSC 0 a caso *)
 182 ;;
 183
 184 (* This is the main function and also the only one used directly from *)
 185 (* cicParser. Given the root of the dom tree, it returns the internal *)
 186 (* representation of the cic object described in the tree             *)
 187 (* It uses the previous functions and the to_cic_term method defined  *)
 188 (* in cicParser3 (used for subtrees that encode cic terms)            *)
 189 let rec get_term n =
 190  let module D = Pxp_document in
 191  let module C = Cic in
 192   let ntype = n # node_type in
 193   match ntype with
 194     D.T_element "Definition" ->
 195       let id = string_of_attr (n # attribute "name")
 196       and params =
 197        option_uri_list_of_attr (n#attribute "params") (n#attribute "paramMode")
 198       and (value, typ) =
 199        let sons = n#sub_nodes in
 200         match sons with
 201           [v ; t] when
 202             v#node_type = D.T_element "body" &&
 203             t#node_type = D.T_element "type" ->
 204              let v' = get_content v
 205              and t' = get_content t in
 206               (v'#extension#to_cic_term, t'#extension#to_cic_term)
 207         | _ -> raise (IllFormedXml 6)
 208       and xid = string_of_attr (n#attribute "id") in
 209        let res = C.ADefinition (xid, ref None, id, value, typ, params) in
 210         register_id xid res ;
 211         res
 212   | D.T_element "Axiom" ->
 213       let id = string_of_attr (n # attribute "name")
 214       and params = uri_list_of_attr (n # attribute "params")
 215       and typ =
 216        (get_content (get_content n))#extension#to_cic_term
 217       and xid = string_of_attr (n#attribute "id") in
 218        let res = C.AAxiom (xid, ref None, id, typ, params) in
 219         register_id xid res ;
 220         res
 221   | D.T_element "CurrentProof" ->
 222      let name = string_of_attr (n#attribute "name")
 223      and xid = string_of_attr (n#attribute "id") in
 224      let sons = n#sub_nodes in
 225       let (conjs, value, typ) = get_conjs_value_type sons in
 226        let res = C.ACurrentProof (xid, ref None, name, conjs, value, typ) in
 227         register_id xid res ;
 228         res
 229   | D.T_element "InductiveDefinition" ->
 230      let sons = n#sub_nodes
 231      and xid = string_of_attr (n#attribute "id") in
 232       let inductiveTypes = get_inductive_types sons
 233       and params = uri_list_of_attr (n#attribute "params")
 234       and nparams = int_of_attr (n#attribute "noParams") in
 235        let res =
 236         C.AInductiveDefinition (xid, ref None, inductiveTypes, params, nparams)
 237        in
 238         register_id xid res ;
 239         res
 240   | D.T_element "Variable" ->
 241      let name = string_of_attr (n#attribute "name")
 242      and xid = string_of_attr (n#attribute "id")
 243      and (body, typ) =
 244       let sons = n#sub_nodes in
 245        match sons with
 246           [b ; t] when
 247             b#node_type = D.T_element "body" &&
 248             t#node_type = D.T_element "type" ->
 249              let b' = get_content b
 250              and t' = get_content t in
 251               (Some (b'#extension#to_cic_term), t'#extension#to_cic_term)
 252         | [t] when t#node_type = D.T_element "type" ->
 253              let t' = get_content t in
 254               (None, t'#extension#to_cic_term)
 255         | _ -> raise (IllFormedXml 6)
 256      in
 257       let res = C.AVariable (xid,ref None,name,body,typ) in
 258        register_id xid res ;
 259        res
 260   | D.T_element _
 261   | D.T_data
 262   | _ ->
 263      raise (IllFormedXml 7)
 264 ;;