exception IllFormedXml of int;;
-(* The hashtable from the current identifiers to the object or the terms *)
-let ids_to_targets = ref None;;
-
-(* 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");;
-
-(* True if annotation really matter *)
-let process_annotations = ref false;;
-
(* 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 =
function
Pxp_types.Value "Prop" -> Cic.Prop
| Pxp_types.Value "Set" -> Cic.Set
- | Pxp_types.Value "Type" -> Cic.Type
+ | Pxp_types.Value "Type" -> Cic.Type (CicUniv.fresh ()) (* TASSI: sure? *)
| _ -> raise (IllFormedXml 2)
let int_of_xml_attr =
let binder_of_xml_attr =
function
- Pxp_types.Value s -> if !process_annotations then Some s else None
+ Pxp_types.Value s -> s
| _ -> raise (IllFormedXml 17)
;;
-let register_id id node =
- if !process_annotations then
- match !ids_to_targets with
- None -> assert false
- | Some ids_to_targets ->
- Hashtbl.add ids_to_targets id (Cic.Term node)
-;;
-
(* the "interface" of the class linked to each node of the dom tree *)
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 = {< >}
(* 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
;;
inherit cic_term
- method to_cic_term = raise (IllFormedXml 6)
+ method to_cic_term _ = raise (IllFormedXml 6)
end
;;
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
;;
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")
(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
- let res = Cic.AFix (id, ref None, nofun, functions) in
- register_id id res ;
- res
+ Cic.AFix (id, nofun, functions)
end
;;
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")
(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
- let res = Cic.ACoFix (id, ref None, nofun, functions) in
- register_id id res ;
- res
+ Cic.ACoFix (id, nofun, functions)
end
;;
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
- let res = Cic.AImplicit (id, ref None) in
- register_id id res ;
- res
+ Cic.AImplicit (id, None)
end
;;
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
- let res = Cic.ARel (id,ref None,value,binder) in
- register_id id res ;
- res
+ 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
;;
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") in
- let res = Cic.AMeta (id,ref None,value) in
- register_id id res ;
- res
+ 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
;;
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
- let res =
- Cic.AVar
- (xid,ref None,
- (UriManager.uri_of_string
- ("cic:" ^ get_prefix (int_of_string index) ^ id ^ ".var"))
- )
- in
- register_id id res ;
- res
- | _ -> raise (IllFormedXml 18)
+(*CSC: BIG BUG: [] MUST BE REPLACED WITH THE PARSED EXPLICIT NAMED SUBSTITUTION *)
+ Cic.AVar (xid,uri,[])
end
;;
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
- let res =
- Cic.AAppl
- (id,ref None,List.map (fun x -> x#extension#to_cic_term) children)
- in
- register_id id res ;
- res
+ Cic.AAppl
+ (id,List.map (fun x -> x#extension#to_cic_term []) children)
end
;;
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
[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 res = Cic.ACast (id,ref None,term,typ) in
- register_id id res ;
- res
+ let term = te#extension#to_cic_term []
+ and typ = ty#extension#to_cic_term [] in
+ Cic.ACast (id,term,typ)
| _ -> raise (IllFormedXml 9)
end
;;
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
- let res = Cic.ASort (id,ref None,sort) in
- register_id id res ;
- res
- 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
- let res = Cic.AAbst (id,ref None,value) in
- register_id id res ;
- res
+ Cic.ASort (id,sort)
end
;;
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
- let res =
- Cic.AConst (id,ref None,value, U.relative_depth !current_uri value 0)
- in
- register_id id res ;
- res
+ Cic.AConst (id,value, exp_named_subst)
end
;;
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
- let res =
- Cic.AMutInd
- (id,ref None,name, U.relative_depth !current_uri name 0, noType)
- in
- register_id id res ;
- res
+ Cic.AMutInd
+ (id,name, noType, exp_named_subst)
end
;;
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 noConstr = int_of_xml_attr (n#attribute "noConstr")
and id = string_of_xml_attr (n#attribute "id") in
- let res =
- Cic.AMutConstruct
- (id, ref None, name, U.relative_depth !current_uri name 0,
- noType, noConstr)
- in
- register_id id res ;
- res
+ Cic.AMutConstruct
+ (id, name, noType, noConstr, exp_named_subst)
end
;;
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
- let res = Cic.AProd (id,ref None,name,source,target) in
- register_id id res ;
- res
- | _ -> 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
;;
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
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
- let res =
- Cic.AMutCase (id,ref None,ci,U.relative_depth !current_uri ci 0,
- typeno,inductiveType,inductiveTerm,lpattern)
- in
- register_id id res ;
- res
+ Cic.AMutCase (id,ci, typeno,inductiveType,inductiveTerm,lpattern)
| _ -> raise (IllFormedXml 11)
end
;;
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
- let res = Cic.ALambda (id,ref None,name,source,target) in
- register_id id res ;
- res
- | _ -> 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
;;
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
- let res = Cic.ALetIn (id,ref None,name,source,target) in
- register_id id res ;
- res
- | _ -> 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. *)
"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)) ;
projects / helm.git / blobdiff