X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FgTopLevel%2Fcic2Xml.ml;h=ad1d1f8818fb244190075feb9b0223e5db4c77ad;hb=c929e791b0eca1e75694a663a2f6ada9f0ff9534;hp=69203731169f48a6f0a38a4f9fe0b055e6c2c860;hpb=2329c7fd13fb6c88f9f82ccad6b25a67c9ce7acf;p=helm.git diff --git a/helm/gTopLevel/cic2Xml.ml b/helm/gTopLevel/cic2Xml.ml index 692037311..ad1d1f881 100644 --- a/helm/gTopLevel/cic2Xml.ml +++ b/helm/gTopLevel/cic2Xml.ml @@ -31,23 +31,35 @@ exception NotImplemented;; let dtdname = "http://localhost:8081/getdtd?url=cic.dtd";; (*CSC ottimizzazione: al posto di curi cdepth (vedi codice) *) -let print_term curi = +let print_term curi ids_to_inner_sorts = let rec aux = let module C = Cic in let module X = Xml in let module U = UriManager in function C.ARel (id,n,b) -> - X.xml_empty "REL" ["value",(string_of_int n);"binder",b;"id",id] + let sort = Hashtbl.find ids_to_inner_sorts id in + X.xml_empty "REL" + ["value",(string_of_int n) ; "binder",b ; "id",id ; "sort",sort] | C.AVar (id,uri) -> let vdepth = U.depth_of_uri uri - and cdepth = U.depth_of_uri curi in + and cdepth = U.depth_of_uri curi + and sort = Hashtbl.find ids_to_inner_sorts id in X.xml_empty "VAR" ["relUri",(string_of_int (cdepth - vdepth)) ^ "," ^ (U.name_of_uri uri) ; - "id",id] - | C.AMeta (id,n) -> - X.xml_empty "META" ["no",(string_of_int n) ; "id",id] + "id",id ; "sort",sort] + | 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] + (List.fold_left + (fun i t -> + match t with + Some t' -> + [< i ; X.xml_nempty "substitution" [] (aux t') >] + | None -> + [< i ; X.xml_empty "substitution" [] >] + ) [< >] l) | C.ASort (id,s) -> let string_of_sort = function @@ -58,43 +70,52 @@ let print_term curi = X.xml_empty "SORT" ["value",(string_of_sort s) ; "id",id] | C.AImplicit _ -> raise NotImplemented | C.AProd (id,C.Anonimous,s,t) -> - X.xml_nempty "PROD" ["id",id] - [< X.xml_nempty "source" [] (aux s) ; - X.xml_nempty "target" [] (aux t) - >] + let ty = Hashtbl.find ids_to_inner_sorts id in + X.xml_nempty "PROD" ["id",id ; "type",ty] + [< X.xml_nempty "source" [] (aux s) ; + X.xml_nempty "target" [] (aux t) + >] | C.AProd (xid,C.Name id,s,t) -> - X.xml_nempty "PROD" ["id",xid] - [< X.xml_nempty "source" [] (aux s) ; - X.xml_nempty "target" ["binder",id] (aux t) - >] + let ty = Hashtbl.find ids_to_inner_sorts xid in + X.xml_nempty "PROD" ["id",xid ; "type",ty] + [< X.xml_nempty "source" [] (aux s) ; + X.xml_nempty "target" ["binder",id] (aux t) + >] | C.ACast (id,v,t) -> - X.xml_nempty "CAST" ["id",id] - [< X.xml_nempty "term" [] (aux v) ; - X.xml_nempty "type" [] (aux t) - >] + let sort = Hashtbl.find ids_to_inner_sorts id in + X.xml_nempty "CAST" ["id",id ; "sort",sort] + [< X.xml_nempty "term" [] (aux v) ; + X.xml_nempty "type" [] (aux t) + >] | C.ALambda (id,C.Anonimous,s,t) -> - X.xml_nempty "LAMBDA" ["id",id] - [< X.xml_nempty "source" [] (aux s) ; - X.xml_nempty "target" [] (aux t) - >] + let sort = Hashtbl.find ids_to_inner_sorts id in + X.xml_nempty "LAMBDA" ["id",id ; "sort",sort] + [< X.xml_nempty "source" [] (aux s) ; + X.xml_nempty "target" [] (aux t) + >] | C.ALambda (xid,C.Name id,s,t) -> - X.xml_nempty "LAMBDA" ["id",xid] - [< X.xml_nempty "source" [] (aux s) ; - X.xml_nempty "target" ["binder",id] (aux t) - >] + let sort = Hashtbl.find ids_to_inner_sorts xid in + X.xml_nempty "LAMBDA" ["id",xid ; "sort",sort] + [< X.xml_nempty "source" [] (aux s) ; + X.xml_nempty "target" ["binder",id] (aux t) + >] | C.ALetIn (xid,C.Anonimous,s,t) -> - assert false (*CSC: significa che e' sbagliato il tipo di LetIn!!!*) + assert false | C.ALetIn (xid,C.Name id,s,t) -> - X.xml_nempty "LETIN" ["id",xid] - [< X.xml_nempty "term" [] (aux s) ; - X.xml_nempty "letintarget" ["binder",id] (aux t) - >] + let sort = Hashtbl.find ids_to_inner_sorts xid in + X.xml_nempty "LETIN" ["id",xid ; "sort",sort] + [< X.xml_nempty "term" [] (aux s) ; + X.xml_nempty "letintarget" ["binder",id] (aux t) + >] | C.AAppl (id,li) -> - X.xml_nempty "APPLY" ["id",id] - [< (List.fold_right (fun x i -> [< (aux x) ; i >]) li [<>]) - >] + let sort = Hashtbl.find ids_to_inner_sorts id in + X.xml_nempty "APPLY" ["id",id ; "sort",sort] + [< (List.fold_right (fun x i -> [< (aux x) ; i >]) li [<>]) + >] | C.AConst (id,uri,_) -> - X.xml_empty "CONST" ["uri", (U.string_of_uri uri) ; "id",id] + let sort = Hashtbl.find ids_to_inner_sorts id in + X.xml_empty "CONST" + ["uri", (U.string_of_uri uri) ; "id",id ; "sort",sort] | C.AAbst (id,uri) -> raise NotImplemented | C.AMutInd (id,uri,_,i) -> X.xml_empty "MUTIND" @@ -102,46 +123,127 @@ let print_term curi = "noType",(string_of_int i) ; "id",id] | C.AMutConstruct (id,uri,_,i,j) -> - X.xml_empty "MUTCONSTRUCT" - ["uri", (U.string_of_uri uri) ; - "noType",(string_of_int i) ; "noConstr",(string_of_int j) ; - "id",id] + let sort = Hashtbl.find ids_to_inner_sorts id in + X.xml_empty "MUTCONSTRUCT" + ["uri", (U.string_of_uri uri) ; + "noType",(string_of_int i) ; "noConstr",(string_of_int j) ; + "id",id ; "sort",sort] | C.AMutCase (id,uri,_,typeno,ty,te,patterns) -> - X.xml_nempty "MUTCASE" - ["uriType",(U.string_of_uri uri) ; - "noType", (string_of_int typeno) ; - "id", id] - [< X.xml_nempty "patternsType" [] [< (aux ty) >] ; - X.xml_nempty "inductiveTerm" [] [< (aux te) >] ; - List.fold_right - (fun x i -> [< X.xml_nempty "pattern" [] [< aux x >] ; i>]) - 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] + [< X.xml_nempty "patternsType" [] [< (aux ty) >] ; + X.xml_nempty "inductiveTerm" [] [< (aux te) >] ; + List.fold_right + (fun x i -> [< X.xml_nempty "pattern" [] [< aux x >] ; i>]) + patterns [<>] + >] | C.AFix (id, no, funs) -> - X.xml_nempty "FIX" ["noFun", (string_of_int no) ; "id",id] - [< List.fold_right - (fun (fi,ai,ti,bi) i -> - [< X.xml_nempty "FixFunction" - ["name", fi; "recIndex", (string_of_int ai)] - [< X.xml_nempty "type" [] [< aux ti >] ; - X.xml_nempty "body" [] [< aux bi >] - >] ; - i - >] - ) funs [<>] - >] + let sort = Hashtbl.find ids_to_inner_sorts id in + X.xml_nempty "FIX" + ["noFun", (string_of_int no) ; "id",id ; "sort",sort] + [< List.fold_right + (fun (fi,ai,ti,bi) i -> + [< X.xml_nempty "FixFunction" + ["name", fi; "recIndex", (string_of_int ai)] + [< X.xml_nempty "type" [] [< aux ti >] ; + X.xml_nempty "body" [] [< aux bi >] + >] ; + i + >] + ) funs [<>] + >] | C.ACoFix (id,no,funs) -> - X.xml_nempty "COFIX" ["noFun", (string_of_int no) ; "id",id] - [< List.fold_right - (fun (fi,ti,bi) i -> - [< X.xml_nempty "CofixFunction" ["name", fi] - [< X.xml_nempty "type" [] [< aux ti >] ; - X.xml_nempty "body" [] [< aux bi >] - >] ; - i - >] - ) funs [<>] - >] + let sort = Hashtbl.find ids_to_inner_sorts id in + X.xml_nempty "COFIX" + ["noFun", (string_of_int no) ; "id",id ; "sort",sort] + [< List.fold_right + (fun (fi,ti,bi) i -> + [< X.xml_nempty "CofixFunction" ["name", fi] + [< X.xml_nempty "type" [] [< aux ti >] ; + X.xml_nempty "body" [] [< aux bi >] + >] ; + i + >] + ) funs [<>] + >] in aux ;; + +exception NotImplemented;; + +(*CSC ottimizzazione: al posto di curi cdepth (vedi codice) *) +let print_object curi ids_to_inner_sorts = + let rec aux = + let module C = Cic in + let module X = Xml in + let module U = UriManager in + function + C.ACurrentProof (id,n,conjectures,bo,ty) -> + X.xml_nempty "CurrentProof" ["name",n ; "id", id] + [< List.fold_left + (fun i (cid,n,canonical_context,t) -> + [< i ; + X.xml_nempty "Conjecture" + ["id", cid ; "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.Anonimous -> ["id",hid]) + (print_term curi 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.Anonimous -> ["id",hid]) + (print_term curi ids_to_inner_sorts t) + | None -> X.xml_empty "Hidden" ["id",hid] + ) ; + i + >] + ) [< >] canonical_context ; + X.xml_nempty "Goal" [] + (print_term curi ids_to_inner_sorts t) + >] + >]) + [<>] conjectures ; + X.xml_nempty "body" [] (print_term curi ids_to_inner_sorts bo) ; + X.xml_nempty "type" [] (print_term curi ids_to_inner_sorts ty) >] + | C.ADefinition (id,n,bo,ty,C.Actual params) -> + let params' = + List.fold_right + (fun (_,x) i -> + List.fold_right + (fun x i -> + U.string_of_uri x ^ match i with "" -> "" | i' -> " " ^ i' + ) x "" ^ match i with "" -> "" | i' -> " " ^ i' + ) params "" + in + X.xml_nempty "Definition" ["name",n ; "params",params' ; "id", id] + [< X.xml_nempty "body" [] (print_term curi ids_to_inner_sorts bo) ; + X.xml_nempty "type" [] (print_term curi ids_to_inner_sorts ty) >] + | C.ADefinition _ -> assert false + | _ -> raise NotImplemented + in + aux +;; + +let print_inner_types curi ids_to_inner_sorts ids_to_inner_types = + let module X = Xml in + X.xml_nempty "InnerTypes" ["of",UriManager.string_of_uri curi] + (Hashtbl.fold + (fun id ty x -> + [< x ; + X.xml_nempty "TYPE" ["of",id] + (print_term curi ids_to_inner_sorts ty) + >] + ) ids_to_inner_types [<>] + ) +;;