exception ImpossiblePossible;;
exception NotImplemented;;
-let dtdname = "http://localhost:8081/getdtd?uri=cic.dtd";;
+let dtdname ~ask_dtd_to_the_getter dtd =
+ if ask_dtd_to_the_getter then
+ Configuration.getter_url ^ "getdtd?uri=" ^ dtd
+ else
+ "http://mowgli.cs.unibo.it/dtd/" ^ dtd
+;;
let param_attribute_of_params params =
String.concat " " (List.map UriManager.string_of_uri params)
X.xml_nempty "PROD" ["type",sort]
[< List.fold_left
(fun i (id,binder,s) ->
- let sort = Hashtbl.find ids_to_inner_sorts id in
+ let sort =
+ Hashtbl.find ids_to_inner_sorts (Cic2acic.source_id_of_id id)
+ in
let attrs =
("id",id)::("type",sort)::
match binder with
X.xml_nempty "LAMBDA" ["sort",sort]
[< List.fold_left
(fun i (id,binder,s) ->
- let sort = Hashtbl.find ids_to_inner_sorts id in
+ let sort =
+ Hashtbl.find ids_to_inner_sorts (Cic2acic.source_id_of_id id)
+ in
let attrs =
("id",id)::("type",sort)::
match binder with
aux
;;
-exception NotImplemented;;
-
-let print_object uri ~ids_to_inner_sorts =
- let rec aux =
- let module C = Cic in
- let module X = Xml in
- let module U = UriManager in
- function
+let print_object uri ~ids_to_inner_sorts ~ask_dtd_to_the_getter obj =
+ let module C = Cic in
+ let module X = Xml in
+ let module U = UriManager in
+ let dtdname = dtdname ~ask_dtd_to_the_getter "cic.dtd" in
+ match obj with
C.ACurrentProof (id,idbody,n,conjectures,bo,ty,params) ->
let params' = param_attribute_of_params params in
let xml_for_current_proof_body =
(print_term ids_to_inner_sorts t)
>]
>])
- [<>] (List.rev conjectures) ;
+ [<>] conjectures ;
X.xml_nempty "body" [] (print_term ids_to_inner_sorts bo) >]
in
let xml_for_current_proof_type =
in
let xmlbo =
[< X.xml_cdata "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n" ;
- X.xml_cdata ("<!DOCTYPE CurrentProof SYSTEM \""^dtdname ^"\">\n");
+ X.xml_cdata ("<!DOCTYPE CurrentProof SYSTEM \""^ dtdname ^ "\">\n");
xml_for_current_proof_body
>] in
let xmlty =
[< X.xml_cdata "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n" ;
- X.xml_cdata
- ("<!DOCTYPE ConstantType SYSTEM \"" ^ dtdname ^ "\">\n");
+ X.xml_cdata ("<!DOCTYPE ConstantType SYSTEM \""^ dtdname ^ "\">\n");
xml_for_current_proof_type
>]
in
in
let xmlty =
[< X.xml_cdata "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n" ;
- X.xml_cdata ("<!DOCTYPE ConstantType SYSTEM \""^dtdname ^"\">\n");
+ X.xml_cdata ("<!DOCTYPE ConstantType SYSTEM \""^ dtdname ^ "\">\n");
X.xml_nempty "ConstantType"
["name",n ; "params",params' ; "id", id]
[< print_term ids_to_inner_sorts ty >]
>]
in
xmlty, xmlbo
- | _ -> raise NotImplemented
- in
- aux
+ | C.AVariable (id,n,bo,ty,params) ->
+ let params' = param_attribute_of_params params in
+ let xmlbo =
+ match bo with
+ None -> [< >]
+ | Some bo ->
+ X.xml_nempty "body" [] [< print_term ids_to_inner_sorts bo >]
+ in
+ let aobj =
+ [< 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]
+ [< xmlbo ;
+ X.xml_nempty "type" [] (print_term ids_to_inner_sorts ty)
+ >]
+ >]
+ in
+ aobj, None
+ | C.AInductiveDefinition (id,tys,params,nparams) ->
+ let params' = param_attribute_of_params params in
+ [< X.xml_cdata "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n" ;
+ X.xml_cdata
+ ("<!DOCTYPE InductiveDefinition SYSTEM \"" ^ dtdname ^ "\">\n") ;
+ X.xml_nempty "InductiveDefinition"
+ ["noParams",string_of_int nparams ;
+ "id",id ;
+ "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)
+ ]
+ [< X.xml_nempty "arity" []
+ (print_term ids_to_inner_sorts arity) ;
+ (List.fold_left
+ (fun i (name,lc) ->
+ [< i ;
+ X.xml_nempty "Constructor"
+ ["name",name]
+ (print_term ids_to_inner_sorts lc)
+ >]) [<>] cons
+ )
+ >]
+ >]
+ ) [< >] tys
+ )
+ >]
+ >], None
;;
-let print_inner_types curi ~ids_to_inner_sorts ~ids_to_inner_types =
+let
+ print_inner_types curi ~ids_to_inner_sorts ~ids_to_inner_types
+ ~ask_dtd_to_the_getter
+=
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 ids_to_inner_sorts synty ;
- match expty with
- None -> [<>]
- | Some expty' -> print_term ids_to_inner_sorts expty'
+ let dtdname = dtdname ~ask_dtd_to_the_getter "cictypes.dtd" in
+ [< 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]
+ (Hashtbl.fold
+ (fun id {C2A.annsynthesized = synty ; C2A.annexpected = expty} x ->
+ [< x ;
+ X.xml_nempty "TYPE" ["of",id]
+ [< X.xml_nempty "synthesized" []
+ [< print_term ids_to_inner_sorts synty >] ;
+ match expty with
+ None -> [<>]
+ | Some expty' -> X.xml_nempty "expected" [] [< print_term ids_to_inner_sorts expty' >]
+ >]
>]
- >]
- ) ids_to_inner_types [<>]
- )
+ ) ids_to_inner_types [<>]
+ )
+ >]
;;
projects / helm.git / blobdiff