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 =
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 =
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
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
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
+ 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
- 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
;;
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
- Cic.AMeta (id,value)
+ 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
- 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
;;
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
;;
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 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
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
;;
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
;;
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 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
;;
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
;;
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
- 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
;;
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
;;
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. *)
"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