X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic%2FcicParser3.ml;h=02d22b3216b0bf631f2be796689f627a775534be;hb=1c7fb836e2af4f2f3d18afd0396701f2094265ff;hp=72882a186513e62dba5aa9f9dc263d7c9240cefa;hpb=37f08b2aba9f17d9d609ca0f57d607f437a3d3fc;p=helm.git diff --git a/helm/ocaml/cic/cicParser3.ml b/helm/ocaml/cic/cicParser3.ml index 72882a186..02d22b321 100644 --- a/helm/ocaml/cic/cicParser3.ml +++ b/helm/ocaml/cic/cicParser3.ml @@ -41,19 +41,12 @@ exception IllFormedXml of int;; -(* The list of tokens of the current section path. *) -(* Used to resolve relative URIs *) -let current_sp = ref [];; - -(* The uri of the object been parsed *) -let current_uri = ref (UriManager.uri_of_string "cic:/.xml");; - (* Utility functions to map a markup attribute to something useful *) let cic_attr_of_xml_attr = function Pxp_types.Value s -> Cic.Name s - | Pxp_types.Implied_value -> Cic.Anonimous + | Pxp_types.Implied_value -> Cic.Anonymous | _ -> raise (IllFormedXml 1) let cic_sort_of_xml_attr = @@ -89,7 +82,7 @@ let binder_of_xml_attr = class virtual cic_term = object (self) - (* fields and methods ever required by markup *) + (* fields and methods always required by markup *) val mutable node = (None : cic_term Pxp_document.node option) method clone = {< >} @@ -103,7 +96,8 @@ class virtual cic_term = (* a method that returns the internal representation of the tree (term) *) (* rooted in this node *) - method virtual to_cic_term : Cic.annterm + method virtual to_cic_term : + (UriManager.uri * Cic.annterm) list -> Cic.annterm end ;; @@ -113,7 +107,7 @@ class eltype_not_of_cic = inherit cic_term - method to_cic_term = raise (IllFormedXml 6) + method to_cic_term _ = raise (IllFormedXml 6) end ;; @@ -124,10 +118,11 @@ class eltype_transparent = inherit cic_term - method to_cic_term = + method to_cic_term exp_named_subst = + assert (exp_named_subst = []) ; let n = self#node in match n#sub_nodes with - [ t ] -> t#extension#to_cic_term + [ t ] -> t#extension#to_cic_term [] | _ -> raise (IllFormedXml 7) end ;; @@ -139,7 +134,8 @@ class eltype_fix = inherit cic_term - method to_cic_term = + method to_cic_term exp_named_subst = + assert (exp_named_subst = []) ; let n = self#node in let nofun = int_of_xml_attr (n#attribute "noFun") and id = string_of_xml_attr (n#attribute "id") @@ -149,16 +145,17 @@ class eltype_fix = (function f when f#node_type = Pxp_document.T_element "FixFunction" -> let name = string_of_xml_attr (f#attribute "name") + and id = string_of_xml_attr (f#attribute "id") and recindex = int_of_xml_attr (f#attribute "recIndex") and (ty, body) = match f#sub_nodes with [t ; b] when t#node_type = Pxp_document.T_element "type" && b#node_type = Pxp_document.T_element "body" -> - (t#extension#to_cic_term, b#extension#to_cic_term) + (t#extension#to_cic_term [], b#extension#to_cic_term []) | _ -> raise (IllFormedXml 14) in - (name, recindex, ty, body) + (id, name, recindex, ty, body) | _ -> raise (IllFormedXml 13) ) sons in @@ -171,7 +168,8 @@ class eltype_cofix = inherit cic_term - method to_cic_term = + method to_cic_term exp_named_subst = + assert (exp_named_subst = []) ; let n = self#node in let nofun = int_of_xml_attr (n#attribute "noFun") and id = string_of_xml_attr (n#attribute "id") @@ -181,15 +179,16 @@ class eltype_cofix = (function f when f#node_type = Pxp_document.T_element "CofixFunction" -> let name = string_of_xml_attr (f#attribute "name") + and id = string_of_xml_attr (f#attribute "id") and (ty, body) = match f#sub_nodes with [t ; b] when t#node_type = Pxp_document.T_element "type" && b#node_type = Pxp_document.T_element "body" -> - (t#extension#to_cic_term, b#extension#to_cic_term) + (t#extension#to_cic_term [], b#extension#to_cic_term []) | _ -> raise (IllFormedXml 16) in - (name, ty, body) + (id, name, ty, body) | _ -> raise (IllFormedXml 15) ) sons in @@ -202,7 +201,8 @@ class eltype_implicit = inherit cic_term - method to_cic_term = + method to_cic_term exp_named_subst = + assert (exp_named_subst = []) ; let n = self#node in let id = string_of_xml_attr (n#attribute "id") in Cic.AImplicit id @@ -214,12 +214,14 @@ class eltype_rel = inherit cic_term - method to_cic_term = + method to_cic_term exp_named_subst = + assert (exp_named_subst = []) ; let n = self#node in let value = int_of_xml_attr (n#attribute "value") and binder = binder_of_xml_attr (n#attribute "binder") - and id = string_of_xml_attr (n#attribute "id") in - Cic.ARel (id,value,binder) + and id = string_of_xml_attr (n#attribute "id") + and idref = string_of_xml_attr (n#attribute "idref") in + Cic.ARel (id,idref,value,binder) end ;; @@ -228,7 +230,8 @@ class eltype_meta = inherit cic_term - method to_cic_term = + method to_cic_term exp_named_subst = + assert (exp_named_subst = []) ; let n = self#node in let value = int_of_xml_attr (n#attribute "no") and id = string_of_xml_attr (n#attribute "id") @@ -239,7 +242,7 @@ class eltype_meta = (function substitution -> match substitution#sub_nodes with [] -> None - | [he] -> Some he#extension#to_cic_term + | [he] -> Some (he#extension#to_cic_term []) | _ -> raise (IllFormedXml 20) ) sons in @@ -252,27 +255,13 @@ class eltype_var = inherit cic_term - method to_cic_term = + method to_cic_term exp_named_subst = + assert (exp_named_subst = []) ; let n = self#node in - let name = string_of_xml_attr (n#attribute "relUri") + let uri = uri_of_xml_attr (n#attribute "uri") and xid = string_of_xml_attr (n#attribute "id") in - match Str.split (Str.regexp ",") name with - [index; id] -> - let get_prefix n = - let rec aux = - function - (0,_) -> "/" - | (n,he::tl) when n > 0 -> "/" ^ he ^ aux (n - 1, tl) - | _ -> raise (IllFormedXml 19) - in - aux (List.length !current_sp - n,!current_sp) - in - Cic.AVar - (xid, - (UriManager.uri_of_string - ("cic:" ^ get_prefix (int_of_string index) ^ id ^ ".var")) - ) - | _ -> raise (IllFormedXml 18) +(*CSC: BIG BUG: [] MUST BE REPLACED WITH THE PARSED EXPLICIT NAMED SUBSTITUTION *) + Cic.AVar (xid,uri,[]) end ;; @@ -281,14 +270,15 @@ class eltype_apply = inherit cic_term - method to_cic_term = + method to_cic_term exp_named_subst = + assert (exp_named_subst = []) ; let n = self#node in let children = n#sub_nodes and id = string_of_xml_attr (n#attribute "id") in if List.length children < 2 then raise (IllFormedXml 8) else Cic.AAppl - (id,List.map (fun x -> x#extension#to_cic_term) children) + (id,List.map (fun x -> x#extension#to_cic_term []) children) end ;; @@ -297,7 +287,8 @@ class eltype_cast = inherit cic_term - method to_cic_term = + method to_cic_term exp_named_subst = + assert (exp_named_subst = []) ; let n = self#node in let sons = n#sub_nodes and id = string_of_xml_attr (n#attribute "id") in @@ -305,8 +296,8 @@ class eltype_cast = [te ; ty] when te#node_type = Pxp_document.T_element "term" && ty#node_type = Pxp_document.T_element "type" -> - let term = te#extension#to_cic_term - and typ = ty#extension#to_cic_term in + let term = te#extension#to_cic_term [] + and typ = ty#extension#to_cic_term [] in Cic.ACast (id,term,typ) | _ -> raise (IllFormedXml 9) end @@ -317,7 +308,8 @@ class eltype_sort = inherit cic_term - method to_cic_term = + method to_cic_term exp_named_subst = + assert (exp_named_subst = []) ; let n = self#node in let sort = cic_sort_of_xml_attr (n#attribute "value") and id = string_of_xml_attr (n#attribute "id") in @@ -325,30 +317,17 @@ class eltype_sort = end ;; -class eltype_abst = - object (self) - - inherit cic_term - - method to_cic_term = - let n = self#node in - let value = uri_of_xml_attr (n#attribute "uri") - and id = string_of_xml_attr (n#attribute "id") in - Cic.AAbst (id,value) - end -;; - class eltype_const = object (self) inherit cic_term - method to_cic_term = + method to_cic_term exp_named_subst = let module U = UriManager in let n = self#node in let value = uri_of_xml_attr (n#attribute "uri") and id = string_of_xml_attr (n#attribute "id") in - Cic.AConst (id,value, U.relative_depth !current_uri value 0) + Cic.AConst (id,value, exp_named_subst) end ;; @@ -357,14 +336,14 @@ class eltype_mutind = inherit cic_term - method to_cic_term = + method to_cic_term exp_named_subst = let module U = UriManager in let n = self#node in let name = uri_of_xml_attr (n#attribute "uri") and noType = int_of_xml_attr (n#attribute "noType") and id = string_of_xml_attr (n#attribute "id") in Cic.AMutInd - (id,name, U.relative_depth !current_uri name 0, noType) + (id,name, noType, exp_named_subst) end ;; @@ -373,7 +352,7 @@ class eltype_mutconstruct = inherit cic_term - method to_cic_term = + method to_cic_term exp_named_subst = let module U = UriManager in let n = self#node in let name = uri_of_xml_attr (n#attribute "uri") @@ -381,8 +360,7 @@ class eltype_mutconstruct = and noConstr = int_of_xml_attr (n#attribute "noConstr") and id = string_of_xml_attr (n#attribute "id") in Cic.AMutConstruct - (id, name, U.relative_depth !current_uri name 0, - noType, noConstr) + (id, name, noType, noConstr, exp_named_subst) end ;; @@ -391,19 +369,25 @@ class eltype_prod = inherit cic_term - method to_cic_term = + method to_cic_term exp_named_subst = + assert (exp_named_subst = []) ; let n = self#node in - let sons = n#sub_nodes - and id = string_of_xml_attr (n#attribute "id") in - match sons with - [s ; t] when - s#node_type = Pxp_document.T_element "source" && - t#node_type = Pxp_document.T_element "target" -> - let name = cic_attr_of_xml_attr (t#attribute "binder") - and source = s#extension#to_cic_term - and target = t#extension#to_cic_term in - Cic.AProd (id,name,source,target) - | _ -> raise (IllFormedXml 10) + let sons = n#sub_nodes in + let rec get_decls_and_target = + function + [t] when t#node_type = Pxp_document.T_element "target" -> + [],t#extension#to_cic_term [] + | s::tl when s#node_type = Pxp_document.T_element "decl" -> + let decls,target = get_decls_and_target tl in + let id = string_of_xml_attr (s#attribute "id") in + let binder = cic_attr_of_xml_attr (s#attribute "binder") in + (id,binder,s#extension#to_cic_term [])::decls, target + | _ -> raise (IllFormedXml 10) + in + let decls,target = get_decls_and_target sons in + List.fold_right + (fun (id,b,s) t -> Cic.AProd (id,b,s,t)) + decls target end ;; @@ -412,7 +396,8 @@ class eltype_mutcase = inherit cic_term - method to_cic_term = + method to_cic_term exp_named_subst = + assert (exp_named_subst = []) ; let module U = UriManager in let n = self#node in let sons = n#sub_nodes @@ -423,12 +408,12 @@ class eltype_mutcase = te#node_type = Pxp_document.T_element "inductiveTerm" -> let ci = uri_of_xml_attr (n#attribute "uriType") and typeno = int_of_xml_attr (n#attribute "noType") - and inductiveType = ty#extension#to_cic_term - and inductiveTerm = te#extension#to_cic_term - and lpattern= List.map (fun x -> x#extension#to_cic_term) patterns + and inductiveType = ty#extension#to_cic_term [] + and inductiveTerm = te#extension#to_cic_term [] + and lpattern = + List.map (fun x -> x#extension#to_cic_term []) patterns in - Cic.AMutCase (id,ci,U.relative_depth !current_uri ci 0, - typeno,inductiveType,inductiveTerm,lpattern) + Cic.AMutCase (id,ci, typeno,inductiveType,inductiveTerm,lpattern) | _ -> raise (IllFormedXml 11) end ;; @@ -438,19 +423,25 @@ class eltype_lambda = inherit cic_term - method to_cic_term = + method to_cic_term exp_named_subst = + assert (exp_named_subst = []) ; let n = self#node in - let sons = n#sub_nodes - and id = string_of_xml_attr (n#attribute "id") in - match sons with - [s ; t] when - s#node_type = Pxp_document.T_element "source" && - t#node_type = Pxp_document.T_element "target" -> - let name = cic_attr_of_xml_attr (t#attribute "binder") - and source = s#extension#to_cic_term - and target = t#extension#to_cic_term in - Cic.ALambda (id,name,source,target) - | _ -> raise (IllFormedXml 12) + let sons = n#sub_nodes in + let rec get_decls_and_target = + function + [t] when t#node_type = Pxp_document.T_element "target" -> + [],t#extension#to_cic_term [] + | s::tl when s#node_type = Pxp_document.T_element "decl" -> + let decls,target = get_decls_and_target tl in + let id = string_of_xml_attr (s#attribute "id") in + let binder = cic_attr_of_xml_attr (s#attribute "binder") in + (id,binder,s#extension#to_cic_term [])::decls, target + | _ -> raise (IllFormedXml 12) + in + let decls,target = get_decls_and_target sons in + List.fold_right + (fun (id,b,s) t -> Cic.ALambda (id,b,s,t)) + decls target end ;; @@ -459,22 +450,64 @@ class eltype_letin = inherit cic_term - method to_cic_term = + method to_cic_term exp_named_subst = + assert (exp_named_subst = []) ; let n = self#node in - let sons = n#sub_nodes - and id = string_of_xml_attr (n#attribute "id") in - match sons with - [s ; t] when - s#node_type = Pxp_document.T_element "term" && - t#node_type = Pxp_document.T_element "letintarget" -> - let name = cic_attr_of_xml_attr (t#attribute "binder") - and source = s#extension#to_cic_term - and target = t#extension#to_cic_term in - Cic.ALetIn (id,name,source,target) - | _ -> raise (IllFormedXml 12) + let sons = n#sub_nodes in + let rec get_defs_and_target = + function + [t] when t#node_type = Pxp_document.T_element "target" -> + [],t#extension#to_cic_term [] + | s::tl when s#node_type = Pxp_document.T_element "def" -> + let defs,target = get_defs_and_target tl in + let id = string_of_xml_attr (s#attribute "id") in + let binder = cic_attr_of_xml_attr (s#attribute "binder") in + (id,binder,s#extension#to_cic_term [])::defs, target + | _ -> raise (IllFormedXml 12) + in + let defs,target = get_defs_and_target sons in + List.fold_right + (fun (id,b,s) t -> Cic.ALetIn (id,b,s,t)) + defs target + end +;; + +class eltype_instantiate = + object (self) + + inherit cic_term + + method to_cic_term exp_named_subst = + assert (exp_named_subst = []) ; + let n = self#node in +(* CSC: this optional attribute should be parsed and reflected in Cic.annterm + and id = string_of_xml_attr (n#attribute "id") +*) + match n#sub_nodes with + t::l -> + let baseUri = + UriManager.buri_of_uri (uri_of_xml_attr (t#attribute "uri")) in + let exp_named_subst = + List.map + (function + n when n#node_type = Pxp_document.T_element "arg" -> + let relUri = string_of_xml_attr (n#attribute "relUri") in + let uri = UriManager.uri_of_string (baseUri ^ "/" ^ relUri) in + let arg = + match n#sub_nodes with + [ t ] -> t#extension#to_cic_term [] + | _ -> raise (IllFormedXml 7) + in + (uri, arg) + | _ -> raise (IllFormedXml 7) + ) l + in + t#extension#to_cic_term exp_named_subst + | _ -> raise (IllFormedXml 7) end ;; + (* The definition of domspec, an hashtable that maps each node type to the *) (* object that must be linked to it. Used by markup. *) @@ -495,17 +528,18 @@ let domspec = "LETIN", (new D.element_impl (new eltype_letin)) ; "APPLY", (new D.element_impl (new eltype_apply)) ; "CONST", (new D.element_impl (new eltype_const)) ; - "ABST", (new D.element_impl (new eltype_abst)) ; "MUTIND", (new D.element_impl (new eltype_mutind)) ; "MUTCONSTRUCT", (new D.element_impl (new eltype_mutconstruct)) ; "MUTCASE", (new D.element_impl (new eltype_mutcase)) ; "FIX", (new D.element_impl (new eltype_fix)) ; "COFIX", (new D.element_impl (new eltype_cofix)) ; + "instantiate", (new D.element_impl (new eltype_instantiate)) ; "arity", (new D.element_impl (new eltype_transparent)) ; "term", (new D.element_impl (new eltype_transparent)) ; "type", (new D.element_impl (new eltype_transparent)) ; "body", (new D.element_impl (new eltype_transparent)) ; - "source", (new D.element_impl (new eltype_transparent)) ; + "decl", (new D.element_impl (new eltype_transparent)) ; + "def", (new D.element_impl (new eltype_transparent)) ; "target", (new D.element_impl (new eltype_transparent)) ; "letintarget", (new D.element_impl (new eltype_transparent)) ; "patternsType", (new D.element_impl (new eltype_transparent)) ;