-
(* Copyright (C) 2000, HELM Team.
*
* This file is part of HELM, an Hypertextual, Electronic
exception ImpossiblePossible;;
exception NotImplemented;;
-let dtdname = "http://localhost:8081/getdtd?url=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)
+;;
(*CSC ottimizzazione: al posto di curi cdepth (vedi codice) *)
-let print_term curi ids_to_inner_sorts =
+let print_term ~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) ->
+ 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 ; "sort",sort]
- | C.AVar (id,uri) ->
- let vdepth = U.depth_of_uri uri
- 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 ; "sort",sort]
+ ["value",(string_of_int n) ; "binder",b ; "id",id ; "idref",idref ;
+ "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])
+ 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]
in
X.xml_empty "SORT" ["value",(string_of_sort s) ; "id",id]
| C.AImplicit _ -> raise NotImplemented
- | C.AProd (id,C.Anonimous,s,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) ->
- 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.AProd (last_id,_,_,_) as prods ->
+ let rec eat_prods =
+ function
+ C.AProd (id,n,s,t) ->
+ let prods,t' = eat_prods t in
+ (id,n,s)::prods,t'
+ | t -> [],t
+ 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]
+ [< 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)::
+ match binder with
+ C.Anonymous -> []
+ | C.Name b -> ["binder",b]
+ in
+ [< i ; X.xml_nempty "decl" attrs (aux s) >]
+ ) [< >] prods ;
+ X.xml_nempty "target" [] (aux t)
+ >]
| 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 "term" [] (aux v) ;
X.xml_nempty "type" [] (aux t)
>]
- | C.ALambda (id,C.Anonimous,s,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) ->
- 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) ->
+ | C.ALambda (last_id,_,_,_) as lambdas ->
+ let rec eat_lambdas =
+ function
+ C.ALambda (id,n,s,t) ->
+ let lambdas,t' = eat_lambdas t in
+ (id,n,s)::lambdas,t'
+ | t -> [],t
+ 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]
+ [< 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)::
+ match binder with
+ C.Anonymous -> []
+ | C.Name b -> ["binder",b]
+ in
+ [< i ; X.xml_nempty "decl" attrs (aux s) >]
+ ) [< >] lambdas ;
+ X.xml_nempty "target" [] (aux t)
+ >]
+ | C.ALetIn (xid,C.Anonymous,s,t) ->
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]
- [< X.xml_nempty "term" [] (aux s) ;
- X.xml_nempty "letintarget" ["binder",id] (aux t)
- >]
+ | C.ALetIn (last_id,C.Name _,_,_) as letins ->
+ let rec eat_letins =
+ function
+ C.ALetIn (id,n,s,t) ->
+ let letins,t' = eat_letins t in
+ (id,n,s)::letins,t'
+ | t -> [],t
+ 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]
+ [< List.fold_left
+ (fun i (id,binder,s) ->
+ let sort = Hashtbl.find ids_to_inner_sorts id in
+ let attrs =
+ ("id",id)::("sort",sort)::
+ match binder with
+ C.Anonymous -> []
+ | C.Name b -> ["binder",b]
+ in
+ [< i ; X.xml_nempty "def" attrs (aux s) >]
+ ) [< >] letins ;
+ X.xml_nempty "target" [] (aux t)
+ >]
| C.AAppl (id,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,_) ->
+ | C.AConst (id,uri,exp_named_subst) ->
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) ;
- "noType",(string_of_int i) ;
- "id",id]
- | C.AMutConstruct (id,uri,_,i,j) ->
+ aux_subst uri
+ (X.xml_empty "CONST"
+ ["uri", (U.string_of_uri uri) ; "id",id ; "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]
+ ) exp_named_subst
+ | C.AMutConstruct (id,uri,i,j,exp_named_subst) ->
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) ->
+ 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]
+ ) 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) ;
X.xml_nempty "FIX"
["noFun", (string_of_int no) ; "id",id ; "sort",sort]
[< List.fold_right
- (fun (fi,ai,ti,bi) i ->
+ (fun (id,fi,ai,ti,bi) i ->
[< X.xml_nempty "FixFunction"
- ["name", fi; "recIndex", (string_of_int ai)]
+ ["id",id ; "name", fi ; "recIndex", (string_of_int ai)]
[< X.xml_nempty "type" [] [< aux ti >] ;
X.xml_nempty "body" [] [< aux bi >]
>] ;
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]
+ (fun (id,fi,ti,bi) i ->
+ [< X.xml_nempty "CofixFunction" ["id",id ; "name", fi]
[< X.xml_nempty "type" [] [< aux ti >] ;
X.xml_nempty "body" [] [< aux bi >]
>] ;
>]
) funs [<>]
>]
- in
- aux
+ and aux_subst buri target subst =
+(*CSC: I have now no way to assign an ID to the explicit named substitution *)
+ let id = None in
+ if subst = [] then
+ target
+ else
+ Xml.xml_nempty "instantiate"
+ (match id with None -> [] | Some id -> ["id",id])
+ [< target ;
+ List.fold_left
+ (fun i (uri,arg) ->
+ let relUri =
+ let buri_frags =
+ Str.split (Str.regexp "/") (UriManager.string_of_uri buri) in
+ let uri_frags =
+ Str.split (Str.regexp "/") (UriManager.string_of_uri uri) in
+ let rec find_relUri buri_frags uri_frags =
+ match buri_frags,uri_frags with
+ [_], _ -> String.concat "/" uri_frags
+ | he1::tl1, he2::tl2 ->
+ assert (he1 = he2) ;
+ find_relUri tl1 tl2
+ | _,_ -> assert false (* uri is not relative to buri *)
+ in
+ find_relUri buri_frags uri_frags
+ in
+ [< i ; Xml.xml_nempty "arg" ["relUri", relUri] (aux arg) >]
+ ) [<>] subst
+ >]
+ 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 (n,canonical_context,t) ->
- [< i ;
- X.xml_nempty "Conjecture" ["no",(string_of_int n)]
- [< List.fold_left
- (fun i t ->
- [< (match t with
- Some (n,C.ADecl t) ->
- X.xml_nempty "Decl"
- (match n with
- C.Name n' -> ["name",n']
- | C.Anonimous -> [])
- (print_term curi ids_to_inner_sorts t)
- | Some (n,C.ADef t) ->
- X.xml_nempty "Def"
- (match n with
- C.Name n' -> ["name",n']
- | C.Anonimous -> [])
- (print_term curi ids_to_inner_sorts t)
- | None -> X.xml_empty "Hidden" []
- ) ;
- 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 ""
+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 =
+(*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]
+ [< 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.Anonymous -> ["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])
+ (print_term ids_to_inner_sorts t)
+ | None -> X.xml_empty "Hidden" ["id",hid]
+ ) ;
+ i
+ >]
+ ) [< >] canonical_context ;
+ X.xml_nempty "Goal" []
+ (print_term ids_to_inner_sorts t)
+ >]
+ >])
+ [<>] conjectures ;
+ 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]
+ (print_term ids_to_inner_sorts ty)
+ in
+ let xmlbo =
+ [< X.xml_cdata "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\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");
+ xml_for_current_proof_type
+ >]
+ in
+ xmlty, Some xmlbo
+ | C.AConstant (id,idbody,n,bo,ty,params) ->
+ let params' = param_attribute_of_params params in
+ let xmlbo =
+ match bo with
+ None -> None
+ | Some bo ->
+ Some
+ [< X.xml_cdata
+ "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n" ;
+ X.xml_cdata
+ ("<!DOCTYPE ConstantBody SYSTEM \"" ^ dtdname ^ "\">\n") ;
+ X.xml_nempty "ConstantBody"
+ ["for",UriManager.string_of_uri uri ; "params",params' ;
+ "id", id]
+ [< print_term ids_to_inner_sorts bo >]
+ >]
+ 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_nempty "ConstantType"
+ ["name",n ; "params",params' ; "id", id]
+ [< print_term ids_to_inner_sorts ty >]
+ >]
+ in
+ xmlty, xmlbo
+ | 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
- 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
+ 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 ty x ->
- [< x ;
- X.xml_nempty "TYPE" ["of",id]
- (print_term curi ids_to_inner_sorts ty)
- >]
- ) ids_to_inner_types [<>]
- )
+ 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 [<>]
+ )
+ >]
;;
projects / helm.git / blobdiff