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
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"
"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 [<>]
+ )
+;;
projects / helm.git / blobdiff