-
(* Copyright (C) 2000, HELM Team.
*
* This file is part of HELM, an Hypertextual, Electronic
let dtdname = "http://localhost:8081/getdtd?url=cic.dtd";;
(*CSC ottimizzazione: al posto di curi cdepth (vedi codice) *)
-let print_term curi ids_to_inner_sorts =
+let print_term curi ~ids_to_inner_sorts =
let rec aux =
let module C = Cic in
let module X = Xml in
["relUri",(string_of_int (cdepth - vdepth)) ^ "," ^
(U.name_of_uri uri) ;
"id",id ; "sort",sort]
- | C.AMeta (id,n) ->
+ | C.AMeta (id,n,l) ->
let sort = Hashtbl.find ids_to_inner_sorts id in
- X.xml_empty "META" ["no",(string_of_int n) ; "id",id ; "sort",sort]
+ 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_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) ->
let sort = Hashtbl.find ids_to_inner_sorts xid in
X.xml_nempty "LETIN" ["id",xid ; "sort",sort]
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"
["uri", (U.string_of_uri uri) ;
exception NotImplemented;;
(*CSC ottimizzazione: al posto di curi cdepth (vedi codice) *)
-let print_object curi ids_to_inner_sorts =
+let print_object curi ~ids_to_inner_sorts =
let rec aux =
let module C = Cic in
let module X = Xml in
C.ACurrentProof (id,n,conjectures,bo,ty) ->
X.xml_nempty "CurrentProof" ["name",n ; "id", id]
[< List.fold_left
- (fun i (n,t) ->
+ (fun i (cid,n,canonical_context,t) ->
[< i ;
- X.xml_nempty "Conjecture" ["no",(string_of_int n)]
- (print_term curi ids_to_inner_sorts t)
+ 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) ;
in
aux
;;
+
+let print_inner_types curi ~ids_to_inner_sorts ~ids_to_inner_types =
+ let module C2A = Cic2acic in
+ let module X = Xml in
+ X.xml_nempty "InnerTypes" ["of",UriManager.string_of_uri curi]
+ (Hashtbl.fold
+ (fun id {C2A.annsynthesized = synty ; C2A.annexpected = expty} x ->
+ [< x ;
+ X.xml_nempty "TYPE" ["of",id]
+ [< print_term curi ids_to_inner_sorts synty ;
+ match expty with
+ None -> [<>]
+ | Some expty' -> print_term curi ids_to_inner_sorts expty'
+ >]
+ >]
+ ) ids_to_inner_types [<>]
+ )
+;;