C.ARel (id,idref,n,b) ->
let sort = Hashtbl.find ids_to_inner_sorts id in
X.xml_empty "REL"
- ["value",(string_of_int n) ; "binder",b ; "id",id ; "idref",idref ;
- "sort",sort]
+ [None,"value",(string_of_int n) ; None,"binder",b ; None,"id",id ;
+ None,"idref",idref ; None,"sort",sort]
| C.AVar (id,uri,exp_named_subst) ->
let sort = Hashtbl.find ids_to_inner_sorts id in
aux_subst uri
- (X.xml_empty "VAR" ["uri",U.string_of_uri uri;"id",id;"sort",sort])
+ (X.xml_empty "VAR"
+ [None,"uri",U.string_of_uri uri;None,"id",id;None,"sort",sort])
exp_named_subst
| C.AMeta (id,n,l) ->
let sort = Hashtbl.find ids_to_inner_sorts id in
- X.xml_nempty "META" ["no",(string_of_int n) ; "id",id ; "sort",sort]
+ X.xml_nempty "META"
+ [None,"no",(string_of_int n) ; None,"id",id ; None,"sort",sort]
(List.fold_left
(fun i t ->
match t with
| C.Set -> "Set"
| C.Type -> "Type"
in
- X.xml_empty "SORT" ["value",(string_of_sort s) ; "id",id]
+ X.xml_empty "SORT" [None,"value",(string_of_sort s) ; None,"id",id]
| C.AImplicit _ -> raise NotImplemented
| C.AProd (last_id,_,_,_) as prods ->
let rec eat_prods =
in
let prods,t = eat_prods prods in
let sort = Hashtbl.find ids_to_inner_sorts last_id in
- X.xml_nempty "PROD" ["type",sort]
+ X.xml_nempty "PROD" [None,"type",sort]
[< List.fold_left
(fun i (id,binder,s) ->
let sort =
Hashtbl.find ids_to_inner_sorts (Cic2acic.source_id_of_id id)
in
let attrs =
- ("id",id)::("type",sort)::
+ (None,"id",id)::(None,"type",sort)::
match binder with
C.Anonymous -> []
- | C.Name b -> ["binder",b]
+ | C.Name b -> [None,"binder",b]
in
[< i ; X.xml_nempty "decl" attrs (aux s) >]
) [< >] prods ;
>]
| C.ACast (id,v,t) ->
let sort = Hashtbl.find ids_to_inner_sorts id in
- X.xml_nempty "CAST" ["id",id ; "sort",sort]
+ X.xml_nempty "CAST" [None,"id",id ; None,"sort",sort]
[< X.xml_nempty "term" [] (aux v) ;
X.xml_nempty "type" [] (aux t)
>]
in
let lambdas,t = eat_lambdas lambdas in
let sort = Hashtbl.find ids_to_inner_sorts last_id in
- X.xml_nempty "LAMBDA" ["sort",sort]
+ X.xml_nempty "LAMBDA" [None,"sort",sort]
[< List.fold_left
(fun i (id,binder,s) ->
let sort =
Hashtbl.find ids_to_inner_sorts (Cic2acic.source_id_of_id id)
in
let attrs =
- ("id",id)::("type",sort)::
+ (None,"id",id)::(None,"type",sort)::
match binder with
C.Anonymous -> []
- | C.Name b -> ["binder",b]
+ | C.Name b -> [None,"binder",b]
in
[< i ; X.xml_nempty "decl" attrs (aux s) >]
) [< >] lambdas ;
in
let letins,t = eat_letins letins in
let sort = Hashtbl.find ids_to_inner_sorts last_id in
- X.xml_nempty "LETIN" ["sort",sort]
+ X.xml_nempty "LETIN" [None,"sort",sort]
[< List.fold_left
(fun i (id,binder,s) ->
let sort = Hashtbl.find ids_to_inner_sorts id in
let attrs =
- ("id",id)::("sort",sort)::
+ (None,"id",id)::(None,"sort",sort)::
match binder with
C.Anonymous -> []
- | C.Name b -> ["binder",b]
+ | C.Name b -> [None,"binder",b]
in
[< i ; X.xml_nempty "def" attrs (aux s) >]
) [< >] letins ;
>]
| C.AAppl (id,li) ->
let sort = Hashtbl.find ids_to_inner_sorts id in
- X.xml_nempty "APPLY" ["id",id ; "sort",sort]
+ X.xml_nempty "APPLY" [None,"id",id ; None,"sort",sort]
[< (List.fold_right (fun x i -> [< (aux x) ; i >]) li [<>])
>]
| C.AConst (id,uri,exp_named_subst) ->
let sort = Hashtbl.find ids_to_inner_sorts id in
aux_subst uri
(X.xml_empty "CONST"
- ["uri", (U.string_of_uri uri) ; "id",id ; "sort",sort]
+ [None,"uri",(U.string_of_uri uri) ; None,"id",id ; None,"sort",sort]
) exp_named_subst
| C.AMutInd (id,uri,i,exp_named_subst) ->
aux_subst uri
(X.xml_empty "MUTIND"
- ["uri", (U.string_of_uri uri) ;
- "noType",(string_of_int i) ;
- "id",id]
+ [None, "uri", (U.string_of_uri uri) ;
+ None, "noType", (string_of_int i) ;
+ None, "id", id]
) exp_named_subst
| C.AMutConstruct (id,uri,i,j,exp_named_subst) ->
let sort = Hashtbl.find ids_to_inner_sorts id in
aux_subst uri
(X.xml_empty "MUTCONSTRUCT"
- ["uri", (U.string_of_uri uri) ;
- "noType",(string_of_int i) ; "noConstr",(string_of_int j) ;
- "id",id ; "sort",sort]
+ [None,"uri", (U.string_of_uri uri) ;
+ None,"noType",(string_of_int i) ;
+ None,"noConstr",(string_of_int j) ;
+ None,"id",id ; None,"sort",sort]
) exp_named_subst
| C.AMutCase (id,uri,typeno,ty,te,patterns) ->
let sort = Hashtbl.find ids_to_inner_sorts id in
X.xml_nempty "MUTCASE"
- ["uriType",(U.string_of_uri uri) ;
- "noType", (string_of_int typeno) ;
- "id", id ; "sort",sort]
+ [None,"uriType",(U.string_of_uri uri) ;
+ None,"noType", (string_of_int typeno) ;
+ None,"id", id ; None,"sort",sort]
[< X.xml_nempty "patternsType" [] [< (aux ty) >] ;
X.xml_nempty "inductiveTerm" [] [< (aux te) >] ;
List.fold_right
| C.AFix (id, no, funs) ->
let sort = Hashtbl.find ids_to_inner_sorts id in
X.xml_nempty "FIX"
- ["noFun", (string_of_int no) ; "id",id ; "sort",sort]
+ [None,"noFun", (string_of_int no) ; None,"id",id ; None,"sort",sort]
[< List.fold_right
(fun (id,fi,ai,ti,bi) i ->
[< X.xml_nempty "FixFunction"
- ["id",id ; "name", fi ; "recIndex", (string_of_int ai)]
+ [None,"id",id ; None,"name", fi ;
+ None,"recIndex", (string_of_int ai)]
[< X.xml_nempty "type" [] [< aux ti >] ;
X.xml_nempty "body" [] [< aux bi >]
>] ;
| C.ACoFix (id,no,funs) ->
let sort = Hashtbl.find ids_to_inner_sorts id in
X.xml_nempty "COFIX"
- ["noFun", (string_of_int no) ; "id",id ; "sort",sort]
+ [None,"noFun", (string_of_int no) ; None,"id",id ; None,"sort",sort]
[< List.fold_right
(fun (id,fi,ti,bi) i ->
- [< X.xml_nempty "CofixFunction" ["id",id ; "name", fi]
+ [< X.xml_nempty "CofixFunction" [None,"id",id ; None,"name", fi]
[< X.xml_nempty "type" [] [< aux ti >] ;
X.xml_nempty "body" [] [< aux bi >]
>] ;
target
else
Xml.xml_nempty "instantiate"
- (match id with None -> [] | Some id -> ["id",id])
+ (match id with None -> [] | Some id -> [None,"id",id])
[< target ;
List.fold_left
(fun i (uri,arg) ->
in
find_relUri buri_frags uri_frags
in
- [< i ; Xml.xml_nempty "arg" ["relUri", relUri] (aux arg) >]
+ [< i ; Xml.xml_nempty "arg" [None,"relUri", relUri] (aux arg) >]
) [<>] subst
>]
in
(*CSC: Should the CurrentProof also have the list of variables it depends on? *)
(*CSC: I think so. Not implemented yet. *)
X.xml_nempty "CurrentProof"
- ["of",UriManager.string_of_uri uri ; "id", id]
+ [None,"of",UriManager.string_of_uri uri ; None,"id", id]
[< List.fold_left
(fun i (cid,n,canonical_context,t) ->
[< i ;
X.xml_nempty "Conjecture"
- ["id", cid ; "no",(string_of_int n)]
+ [None,"id",cid ; None,"no",(string_of_int n)]
[< List.fold_left
(fun i (hid,t) ->
[< (match t with
Some (n,C.ADecl t) ->
X.xml_nempty "Decl"
(match n with
- C.Name n' -> ["id",hid;"name",n']
- | C.Anonymous -> ["id",hid])
+ C.Name n' ->
+ [None,"id",hid;None,"name",n']
+ | C.Anonymous -> [None,"id",hid])
(print_term ids_to_inner_sorts t)
| Some (n,C.ADef t) ->
X.xml_nempty "Def"
(match n with
- C.Name n' -> ["id",hid;"name",n']
- | C.Anonymous -> ["id",hid])
+ C.Name n' ->
+ [None,"id",hid;None,"name",n']
+ | C.Anonymous -> [None,"id",hid])
(print_term ids_to_inner_sorts t)
- | None -> X.xml_empty "Hidden" ["id",hid]
+ | None -> X.xml_empty "Hidden" [None,"id",hid]
) ;
i
>]
X.xml_nempty "body" [] (print_term ids_to_inner_sorts bo) >]
in
let xml_for_current_proof_type =
- X.xml_nempty "ConstantType" ["name",n ; "params",params' ; "id", id]
+ X.xml_nempty "ConstantType"
+ [None,"name",n ; None,"params",params' ; None,"id", id]
(print_term ids_to_inner_sorts ty)
in
let xmlbo =
X.xml_cdata
("<!DOCTYPE ConstantBody SYSTEM \"" ^ dtdname ^ "\">\n") ;
X.xml_nempty "ConstantBody"
- ["for",UriManager.string_of_uri uri ; "params",params' ;
- "id", id]
+ [None,"for",UriManager.string_of_uri uri ;
+ None,"params",params' ; None,"id", id]
[< print_term ids_to_inner_sorts bo >]
>]
in
[< X.xml_cdata "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n" ;
X.xml_cdata ("<!DOCTYPE ConstantType SYSTEM \""^ dtdname ^ "\">\n");
X.xml_nempty "ConstantType"
- ["name",n ; "params",params' ; "id", id]
+ [None,"name",n ; None,"params",params' ; None,"id", id]
[< print_term ids_to_inner_sorts ty >]
>]
in
[< X.xml_cdata "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n" ;
X.xml_cdata ("<!DOCTYPE Variable SYSTEM \"" ^ dtdname ^ "\">\n");
X.xml_nempty "Variable"
- ["name",n ; "params",params' ; "id", id]
+ [None,"name",n ; None,"params",params' ; None,"id", id]
[< xmlbo ;
X.xml_nempty "type" [] (print_term ids_to_inner_sorts ty)
>]
X.xml_cdata
("<!DOCTYPE InductiveDefinition SYSTEM \"" ^ dtdname ^ "\">\n") ;
X.xml_nempty "InductiveDefinition"
- ["noParams",string_of_int nparams ;
- "id",id ;
- "params",params']
+ [None,"noParams",string_of_int nparams ;
+ None,"id",id ;
+ None,"params",params']
[< (List.fold_left
(fun i (id,typename,finite,arity,cons) ->
[< i ;
X.xml_nempty "InductiveType"
- ["id",id ; "name",typename ;
- "inductive",(string_of_bool finite)
+ [None,"id",id ; None,"name",typename ;
+ None,"inductive",(string_of_bool finite)
]
[< X.xml_nempty "arity" []
(print_term ids_to_inner_sorts arity) ;
(fun i (name,lc) ->
[< i ;
X.xml_nempty "Constructor"
- ["name",name]
+ [None,"name",name]
(print_term ids_to_inner_sorts lc)
>]) [<>] cons
)
[< X.xml_cdata "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n" ;
X.xml_cdata
("<!DOCTYPE InnerTypes SYSTEM \"" ^ dtdname ^ "\">\n") ;
- X.xml_nempty "InnerTypes" ["of",UriManager.string_of_uri curi]
+ X.xml_nempty "InnerTypes" [None,"of",UriManager.string_of_uri curi]
(Hashtbl.fold
(fun id {C2A.annsynthesized = synty ; C2A.annexpected = expty} x ->
[< x ;
- X.xml_nempty "TYPE" ["of",id]
+ X.xml_nempty "TYPE" [None,"of",id]
[< X.xml_nempty "synthesized" []
[< print_term ids_to_inner_sorts synty >] ;
match expty with
projects / helm.git / blobdiff