+++ /dev/null
-(* Copyright (C) 2000, HELM Team.
- *
- * This file is part of HELM, an Hypertextual, Electronic
- * Library of Mathematics, developed at the Computer Science
- * Department, University of Bologna, Italy.
- *
- * HELM is free software; you can redistribute it and/or
- * modify it under the terms of the GNU General Public License
- * as published by the Free Software Foundation; either version 2
- * of the License, or (at your option) any later version.
- *
- * HELM is distributed in the hope that it will be useful,
- * but WITHOUT ANY WARRANTY; without even the implied warranty of
- * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
- * GNU General Public License for more details.
- *
- * You should have received a copy of the GNU General Public License
- * along with HELM; if not, write to the Free Software
- * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
- * MA 02111-1307, USA.
- *
- * For details, see the HELM World-Wide-Web page,
- * http://cs.unibo.it/helm/.
- *)
-
-(******************************************************************************)
-(* *)
-(* PROJECT HELM *)
-(* *)
-(* Claudio Sacerdoti Coen <sacerdot@cs.unibo.it> *)
-(* 24/01/2000 *)
-(* *)
-(* This module is the terms level of a parser for cic objects from xml *)
-(* files to the internal representation. It is used by the module cicParser2 *)
-(* (objects level). It defines an extension of the standard dom using the *)
-(* object-oriented extension machinery of markup: an object with a method *)
-(* to_cic_term that returns the internal representation of the subtree is *)
-(* added to each node of the dom tree *)
-(* *)
-(******************************************************************************)
-
-exception IllFormedXml of int;;
-
-(* 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.Anonymous
- | _ -> raise (IllFormedXml 1)
-
-let cic_sort_of_xml_attr =
- function
- Pxp_types.Value "Prop" -> Cic.Prop
- | Pxp_types.Value "Set" -> Cic.Set
- | Pxp_types.Value "Type" -> Cic.Type
- | _ -> raise (IllFormedXml 2)
-
-let int_of_xml_attr =
- function
- Pxp_types.Value n -> int_of_string n
- | _ -> raise (IllFormedXml 3)
-
-let uri_of_xml_attr =
- function
- Pxp_types.Value s -> UriManager.uri_of_string s
- | _ -> raise (IllFormedXml 4)
-
-let string_of_xml_attr =
- function
- Pxp_types.Value s -> s
- | _ -> raise (IllFormedXml 5)
-
-let binder_of_xml_attr =
- function
- Pxp_types.Value s -> s
- | _ -> raise (IllFormedXml 17)
-;;
-
-(* the "interface" of the class linked to each node of the dom tree *)
-
-class virtual cic_term =
- object (self)
-
- (* fields and methods always required by markup *)
- val mutable node = (None : cic_term Pxp_document.node option)
-
- method clone = {< >}
- method node =
- match node with
- None ->
- assert false
- | Some n -> n
- method set_node n =
- node <- Some n
-
- (* a method that returns the internal representation of the tree (term) *)
- (* rooted in this node *)
- method virtual to_cic_term :
- (UriManager.uri * Cic.annterm) list -> Cic.annterm
- end
-;;
-
-(* the class of the objects linked to nodes that are not roots of cic terms *)
-class eltype_not_of_cic =
- object (self)
-
- inherit cic_term
-
- method to_cic_term _ = raise (IllFormedXml 6)
- end
-;;
-
-(* the class of the objects linked to nodes whose content is a cic term *)
-(* (syntactic sugar xml entities) e.g. <type> ... </type> *)
-class eltype_transparent =
- object (self)
-
- inherit 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 []
- | _ -> raise (IllFormedXml 7)
- end
-;;
-
-(* A class for each cic node type *)
-
-class eltype_fix =
- object (self)
-
- inherit 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")
- and functions =
- let sons = n#sub_nodes in
- List.map
- (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 [])
- | _ -> raise (IllFormedXml 14)
- in
- (id, name, recindex, ty, body)
- | _ -> raise (IllFormedXml 13)
- ) sons
- in
- Cic.AFix (id, nofun, functions)
- end
-;;
-
-class eltype_cofix =
- object (self)
-
- inherit 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")
- and functions =
- let sons = n#sub_nodes in
- List.map
- (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 [])
- | _ -> raise (IllFormedXml 16)
- in
- (id, name, ty, body)
- | _ -> raise (IllFormedXml 15)
- ) sons
- in
- Cic.ACoFix (id, nofun, functions)
- end
-;;
-
-class eltype_implicit =
- object (self)
-
- inherit 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
- end
-;;
-
-class eltype_rel =
- object (self)
-
- inherit 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")
- and idref = string_of_xml_attr (n#attribute "idref") in
- Cic.ARel (id,idref,value,binder)
- end
-;;
-
-class eltype_meta =
- object (self)
-
- inherit 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")
- in
- let local_context =
- let sons = n#sub_nodes in
- List.map
- (function substitution ->
- match substitution#sub_nodes with
- [] -> None
- | [he] -> Some (he#extension#to_cic_term [])
- | _ -> raise (IllFormedXml 20)
- ) sons
- in
- Cic.AMeta (id,value,local_context)
- end
-;;
-
-class eltype_var =
- object (self)
-
- inherit cic_term
-
- method to_cic_term exp_named_subst =
- assert (exp_named_subst = []) ;
- let n = self#node in
- let uri = uri_of_xml_attr (n#attribute "uri")
- and xid = string_of_xml_attr (n#attribute "id") in
-(*CSC: BIG BUG: [] MUST BE REPLACED WITH THE PARSED EXPLICIT NAMED SUBSTITUTION *)
- Cic.AVar (xid,uri,[])
- end
-;;
-
-class eltype_apply =
- object (self)
-
- inherit 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)
- end
-;;
-
-class eltype_cast =
- object (self)
-
- inherit 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
- [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
- Cic.ACast (id,term,typ)
- | _ -> raise (IllFormedXml 9)
- end
-;;
-
-class eltype_sort =
- object (self)
-
- inherit 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
- Cic.ASort (id,sort)
- end
-;;
-
-class eltype_const =
- object (self)
-
- inherit 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, exp_named_subst)
- end
-;;
-
-class eltype_mutind =
- object (self)
-
- inherit 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, noType, exp_named_subst)
- end
-;;
-
-class eltype_mutconstruct =
- object (self)
-
- inherit 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 noConstr = int_of_xml_attr (n#attribute "noConstr")
- and id = string_of_xml_attr (n#attribute "id") in
- Cic.AMutConstruct
- (id, name, noType, noConstr, exp_named_subst)
- end
-;;
-
-class eltype_prod =
- object (self)
-
- inherit cic_term
-
- method to_cic_term exp_named_subst =
- assert (exp_named_subst = []) ;
- let n = self#node in
- 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
-;;
-
-class eltype_mutcase =
- object (self)
-
- inherit 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
- and id = string_of_xml_attr (n#attribute "id") in
- match sons with
- ty::te::patterns when
- ty#node_type = Pxp_document.T_element "patternsType" &&
- 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
- in
- Cic.AMutCase (id,ci, typeno,inductiveType,inductiveTerm,lpattern)
- | _ -> raise (IllFormedXml 11)
- end
-;;
-
-class eltype_lambda =
- object (self)
-
- inherit cic_term
-
- method to_cic_term exp_named_subst =
- assert (exp_named_subst = []) ;
- let n = self#node in
- 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
-;;
-
-class eltype_letin =
- object (self)
-
- inherit cic_term
-
- method to_cic_term exp_named_subst =
- assert (exp_named_subst = []) ;
- let n = self#node in
- 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. *)
-
-let domspec =
- let module D = Pxp_document in
- D.make_spec_from_alist
- ~data_exemplar: (new D.data_impl (new eltype_not_of_cic))
- ~default_element_exemplar: (new D.element_impl (new eltype_not_of_cic))
- ~element_alist:
- [ "REL", (new D.element_impl (new eltype_rel)) ;
- "VAR", (new D.element_impl (new eltype_var)) ;
- "META", (new D.element_impl (new eltype_meta)) ;
- "SORT", (new D.element_impl (new eltype_sort)) ;
- "IMPLICIT", (new D.element_impl (new eltype_implicit)) ;
- "CAST", (new D.element_impl (new eltype_cast)) ;
- "PROD", (new D.element_impl (new eltype_prod)) ;
- "LAMBDA", (new D.element_impl (new eltype_lambda)) ;
- "LETIN", (new D.element_impl (new eltype_letin)) ;
- "APPLY", (new D.element_impl (new eltype_apply)) ;
- "CONST", (new D.element_impl (new eltype_const)) ;
- "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)) ;
- "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)) ;
- "inductiveTerm", (new D.element_impl (new eltype_transparent)) ;
- "pattern", (new D.element_impl (new eltype_transparent))
- ]
- ()
-;;
projects / helm.git / blobdiff