- 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)