+++ /dev/null
-(* Copyright (C) 2000-2004, HELM Team.
- *
- * This file is part of HELM, an Hypertextual, Electronic
- * Library of Mathematics, developed at the Computer Science
- * Department, University of Bologna, Italy.
- *
- * HELM is free software; you can redistribute it and/or
- * modify it under the terms of the GNU General Public License
- * as published by the Free Software Foundation; either version 2
- * of the License, or (at your option) any later version.
- *
- * HELM is distributed in the hope that it will be useful,
- * but WITHOUT ANY WARRANTY; without even the implied warranty of
- * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
- * GNU General Public License for more details.
- *
- * You should have received a copy of the GNU General Public License
- * along with HELM; if not, write to the Free Software
- * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
- * MA 02111-1307, USA.
- *
- * For details, see the HELM World-Wide-Web page,
- * http://helm.cs.unibo.it/
- *)
-
-(*CSC codice cut & paste da cicPp e xmlcommand *)
-
-exception ImpossiblePossible;;
-exception NotImplemented;;
-
-let dtdname ~ask_dtd_to_the_getter dtd =
- if ask_dtd_to_the_getter then
- Helm_registry.get "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 ~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,idref,n,b) ->
- let sort = Hashtbl.find ids_to_inner_sorts id in
- X.xml_empty "REL"
- [None,"value",(string_of_int n) ; None,"binder",b ; None,"id",id ;
- None,"idref",idref ; None,"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"
- [None,"uri",U.string_of_uri uri;None,"id",id;None,"sort",sort])
- exp_named_subst
- | C.AMeta (id,n,l) ->
- let sort = Hashtbl.find ids_to_inner_sorts id in
- X.xml_nempty "META"
- [None,"no",(string_of_int n) ; None,"id",id ; None,"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
- C.Prop -> "Prop"
- | C.Set -> "Set"
- | C.Type _ -> "Type" (* TASSI *)
- | C.CProp -> "CProp"
- in
- X.xml_empty "SORT" [None,"value",(string_of_sort s) ; None,"id",id]
- | C.AImplicit _ -> raise NotImplemented
- | 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" [None,"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 =
- (None,"id",id)::(None,"type",sort)::
- match binder with
- C.Anonymous -> []
- | C.Name b -> [None,"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" [None,"id",id ; None,"sort",sort]
- [< X.xml_nempty "term" [] (aux v) ;
- X.xml_nempty "type" [] (aux 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" [None,"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 =
- (None,"id",id)::(None,"type",sort)::
- match binder with
- C.Anonymous -> []
- | C.Name b -> [None,"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 (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" [None,"sort",sort]
- [< List.fold_left
- (fun i (id,binder,s) ->
- let sort = Hashtbl.find ids_to_inner_sorts id in
- let attrs =
- (None,"id",id)::(None,"sort",sort)::
- match binder with
- C.Anonymous -> []
- | C.Name b -> [None,"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" [None,"id",id ; None,"sort",sort]
- [< (List.fold_right (fun x i -> [< (aux x) ; i >]) li [<>])
- >]
- | C.AConst (id,uri,exp_named_subst) ->
- let sort = Hashtbl.find ids_to_inner_sorts id in
- aux_subst uri
- (X.xml_empty "CONST"
- [None,"uri",(U.string_of_uri uri) ; None,"id",id ; None,"sort",sort]
- ) exp_named_subst
- | C.AMutInd (id,uri,i,exp_named_subst) ->
- aux_subst uri
- (X.xml_empty "MUTIND"
- [None, "uri", (U.string_of_uri uri) ;
- None, "noType", (string_of_int i) ;
- None, "id", id]
- ) exp_named_subst
- | C.AMutConstruct (id,uri,i,j,exp_named_subst) ->
- let sort = Hashtbl.find ids_to_inner_sorts id in
- aux_subst uri
- (X.xml_empty "MUTCONSTRUCT"
- [None,"uri", (U.string_of_uri uri) ;
- None,"noType",(string_of_int i) ;
- None,"noConstr",(string_of_int j) ;
- None,"id",id ; None,"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"
- [None,"uriType",(U.string_of_uri uri) ;
- None,"noType", (string_of_int typeno) ;
- None,"id", id ; None,"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) ->
- let sort = Hashtbl.find ids_to_inner_sorts id in
- X.xml_nempty "FIX"
- [None,"noFun", (string_of_int no) ; None,"id",id ; None,"sort",sort]
- [< List.fold_right
- (fun (id,fi,ai,ti,bi) i ->
- [< X.xml_nempty "FixFunction"
- [None,"id",id ; None,"name", fi ;
- None,"recIndex", (string_of_int ai)]
- [< X.xml_nempty "type" [] [< aux ti >] ;
- X.xml_nempty "body" [] [< aux bi >]
- >] ;
- i
- >]
- ) funs [<>]
- >]
- | C.ACoFix (id,no,funs) ->
- let sort = Hashtbl.find ids_to_inner_sorts id in
- X.xml_nempty "COFIX"
- [None,"noFun", (string_of_int no) ; None,"id",id ; None,"sort",sort]
- [< List.fold_right
- (fun (id,fi,ti,bi) i ->
- [< X.xml_nempty "CofixFunction" [None,"id",id ; None,"name", fi]
- [< X.xml_nempty "type" [] [< aux ti >] ;
- X.xml_nempty "body" [] [< aux bi >]
- >] ;
- i
- >]
- ) funs [<>]
- >]
- 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 -> [None,"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" [None,"relUri", relUri] (aux arg) >]
- ) [<>] subst
- >]
- in
- aux
-;;
-
-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"
- [None,"of",UriManager.string_of_uri uri ; None,"id", id]
- [< List.fold_left
- (fun i (cid,n,canonical_context,t) ->
- [< i ;
- X.xml_nempty "Conjecture"
- [None,"id",cid ; None,"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' ->
- [None,"id",hid;None,"name",n']
- | C.Anonymous -> [None,"id",hid])
- (print_term ids_to_inner_sorts t)
- | Some (n,C.ADef t) ->
- X.xml_nempty "Def"
- (match n with
- C.Name n' ->
- [None,"id",hid;None,"name",n']
- | C.Anonymous -> [None,"id",hid])
- (print_term ids_to_inner_sorts t)
- | None -> X.xml_empty "Hidden" [None,"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"
- [None,"name",n ; None,"params",params' ; None,"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"
- [None,"for",UriManager.string_of_uri uri ;
- None,"params",params' ; None,"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"
- [None,"name",n ; None,"params",params' ; None,"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"
- [None,"name",n ; None,"params",params' ; None,"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"
- [None,"noParams",string_of_int nparams ;
- None,"id",id ;
- None,"params",params']
- [< (List.fold_left
- (fun i (id,typename,finite,arity,cons) ->
- [< i ;
- X.xml_nempty "InductiveType"
- [None,"id",id ; None,"name",typename ;
- None,"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"
- [None,"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
- ~ask_dtd_to_the_getter
-=
- let module C2A = Cic2acic in
- let module X = Xml in
- 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" [None,"of",UriManager.string_of_uri curi]
- (Hashtbl.fold
- (fun id {C2A.annsynthesized = synty ; C2A.annexpected = expty} x ->
- [< x ;
- X.xml_nempty "TYPE" [None,"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