X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_transformations%2Fcic2Xml.ml;h=d945cc82f63d54b2e931424c625dacd9707ba383;hb=6f65a2e518d723ea722b23bfd9fa0162ff8be457;hp=564493cb83e9d9d2ae42908e3970b21fbb5107be;hpb=f7b2e35a7bdadb4fdf0e640428e694703ddf67a5;p=helm.git diff --git a/helm/ocaml/cic_transformations/cic2Xml.ml b/helm/ocaml/cic_transformations/cic2Xml.ml index 564493cb8..d945cc82f 100644 --- a/helm/ocaml/cic_transformations/cic2Xml.ml +++ b/helm/ocaml/cic_transformations/cic2Xml.ml @@ -49,16 +49,18 @@ let print_term ~ids_to_inner_sorts = 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 @@ -74,7 +76,7 @@ let print_term ~ids_to_inner_sorts = | 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 = @@ -86,17 +88,17 @@ let print_term ~ids_to_inner_sorts = 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 ; @@ -104,7 +106,7 @@ let print_term ~ids_to_inner_sorts = >] | 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) >] @@ -118,17 +120,17 @@ let print_term ~ids_to_inner_sorts = 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 ; @@ -146,15 +148,15 @@ let print_term ~ids_to_inner_sorts = 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 ; @@ -162,36 +164,37 @@ let print_term ~ids_to_inner_sorts = >] | 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 @@ -201,11 +204,12 @@ let print_term ~ids_to_inner_sorts = | 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 >] >] ; @@ -216,10 +220,10 @@ let print_term ~ids_to_inner_sorts = | 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 >] >] ; @@ -234,7 +238,7 @@ let print_term ~ids_to_inner_sorts = 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) -> @@ -253,7 +257,7 @@ let print_term ~ids_to_inner_sorts = 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 @@ -272,28 +276,30 @@ let print_object uri ~ids_to_inner_sorts ~ask_dtd_to_the_getter obj = (*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 >] @@ -306,7 +312,8 @@ let print_object uri ~ids_to_inner_sorts ~ask_dtd_to_the_getter obj = 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 = @@ -333,8 +340,8 @@ let print_object uri ~ids_to_inner_sorts ~ask_dtd_to_the_getter obj = X.xml_cdata ("\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 @@ -342,7 +349,7 @@ let print_object uri ~ids_to_inner_sorts ~ask_dtd_to_the_getter obj = [< X.xml_cdata "\n" ; X.xml_cdata ("\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 @@ -359,7 +366,7 @@ let print_object uri ~ids_to_inner_sorts ~ask_dtd_to_the_getter obj = [< X.xml_cdata "\n" ; X.xml_cdata ("\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) >] @@ -372,15 +379,15 @@ let print_object uri ~ids_to_inner_sorts ~ask_dtd_to_the_getter obj = X.xml_cdata ("\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) ; @@ -388,7 +395,7 @@ let print_object uri ~ids_to_inner_sorts ~ask_dtd_to_the_getter obj = (fun i (name,lc) -> [< i ; X.xml_nempty "Constructor" - ["name",name] + [None,"name",name] (print_term ids_to_inner_sorts lc) >]) [<>] cons ) @@ -410,11 +417,11 @@ let [< X.xml_cdata "\n" ; X.xml_cdata ("\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