aboutsummaryrefslogtreecommitdiff
path: root/contrib/xml/xmlcommand.ml4
diff options
context:
space:
mode:
Diffstat (limited to 'contrib/xml/xmlcommand.ml4')
-rw-r--r--contrib/xml/xmlcommand.ml41037
1 files changed, 1037 insertions, 0 deletions
diff --git a/contrib/xml/xmlcommand.ml4 b/contrib/xml/xmlcommand.ml4
new file mode 100644
index 0000000000..7b6303130b
--- /dev/null
+++ b/contrib/xml/xmlcommand.ml4
@@ -0,0 +1,1037 @@
+(***********************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
+(* \VV/ *************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(***********************************************************************)
+(******************************************************************************)
+(* *)
+(* PROJECT HELM *)
+(* *)
+(* A module to print Coq objects in XML *)
+(* *)
+(* Claudio Sacerdoti Coen <sacerdot@cs.unibo.it> *)
+(* 06/12/2000 *)
+(* *)
+(******************************************************************************)
+
+
+(* CONFIGURATION PARAMETERS *)
+
+let dtdname = "http://www.cs.unibo.it/helm/dtd/cic.dtd";;
+let typesdtdname = "http://www.cs.unibo.it/helm/dtd/cictypes.dtd";;
+let verbose = ref false;; (* always set to true during a "Print XML All" *)
+
+(* UTILITY FUNCTIONS *)
+
+let print_if_verbose s = if !verbose then print_string s;;
+
+type tag =
+ Constant
+ | Inductive
+ | Variable
+;;
+
+(* Next exception is used only inside print_object and tag_of_string_tag *)
+exception Uninteresting;;
+
+let tag_of_string_tag =
+ function
+ "CONSTANT"
+ | "PARAMETER" -> Constant
+ | "INDUCTIVE" -> Inductive
+ | "VARIABLE" -> Variable
+ | _ -> raise Uninteresting
+;;
+
+let ext_of_tag =
+ function
+ Constant -> "con"
+ | Inductive -> "ind"
+ | Variable -> "var"
+;;
+
+(* Internally, for Coq V7, params of inductive types are associated *)
+(* not to the whole block of mutual inductive (as it was in V6) but to *)
+(* each member of the block; but externally, all params are required *)
+(* to be the same; the following function checks that the parameters *)
+(* of each inductive of a same block are all the same, then returns *)
+(* this number; it fails otherwise *)
+let extract_nparams pack =
+ let module D = Declarations in
+ let module U = Util in
+ let module S = Sign in
+
+ let {D.mind_nparams=nparams0} = pack.(0) in
+ let arity0 = pack.(0).D.mind_user_arity in
+ let params0, _ = S.decompose_prod_n_assum nparams0 arity0 in
+ for i = 1 to Array.length pack - 1 do
+ let {D.mind_nparams=nparamsi} = pack.(i) in
+ let arityi = pack.(i).D.mind_user_arity in
+ let paramsi, _ = S.decompose_prod_n_assum nparamsi arityi in
+ if params0 <> paramsi then U.error "Cannot convert a block of inductive definitions with parameters specific to each inductive to a block of mutual inductive definitions with parameters global to the whole block"
+ done;
+ nparams0
+
+(* could_have_namesakes sp = true iff o is an object that could be cooked and *)
+(* than that could exists in cooked form with the same name in a super *)
+(* section of the actual section *)
+let could_have_namesakes o sp = (* namesake = omonimo in italian *)
+ let module D = Declare in
+ let tag = Libobject.object_tag o in
+ print_if_verbose ("Object tag: " ^ tag ^ "\n") ;
+ match tag with
+ "CONSTANT" ->
+ (match D.constant_strength sp with
+ | D.DischargeAt _ -> false (* a local definition *)
+ | D.NotDeclare -> false (* not a definition *)
+ | D.NeverDischarge -> true (* a non-local one *)
+ )
+ | "PARAMETER" (* axioms and *)
+ | "INDUCTIVE" -> true (* mutual inductive types are never local *)
+ | "VARIABLE" -> false (* variables are local, so no namesakes *)
+ | _ -> false (* uninteresting thing that won't be printed*)
+;;
+
+
+(* uri_of_path sp is a broken (wrong) uri pointing to the object whose *)
+(* section path is sp *)
+let uri_of_path sp tag =
+ let module N = Names in
+ let module No = Nameops in
+ let ext_of_sp sp = ext_of_tag tag in
+ let dir0 = No.extend_dirpath (No.dirpath sp) (No.basename sp) in
+ let dir = List.map N.string_of_id (List.rev (N.repr_dirpath dir0)) in
+ "cic:/" ^ (String.concat "/" dir) ^ "." ^ (ext_of_sp sp)
+;;
+
+let string_of_sort =
+ let module T = Term in
+ function
+ T.Prop(T.Pos) -> "Set"
+ | T.Prop(T.Null) -> "Prop"
+ | T.Type(_) -> "Type"
+;;
+
+let string_of_name =
+ let module N = Names in
+ function
+ N.Name id -> N.string_of_id id
+ | _ -> Util.anomaly "this should not happen"
+;;
+
+(* A SIMPLE DATA STRUCTURE AND SOME FUNCTIONS TO MANAGE THE CURRENT *)
+(* ENVIRONMENT (= [l1, ..., ln] WHERE li IS THE LIST OF VARIABLES *)
+(* DECLARED IN THE i-th SUPER-SECTION OF THE CURRENT SECTION *)
+
+(*CSC: commento sbagliato ed obsoleto *)
+(* list of variables availables in the actual section *)
+let pvars = ref ([[]] : string list list);;
+let cumenv = ref Environ.empty_env;;
+
+let string_of_vars_list =
+ let add_prefix n s = string_of_int n ^ ": " ^ s in
+ let rec aux =
+ function
+ [n,v] -> (n,v)
+ | (n,v)::tl ->
+ let (k,s) = aux tl in
+ if k = n then (k, v ^ " " ^ s) else (n, v ^ " " ^ add_prefix k s)
+ | [] -> assert false
+ in
+ function
+ [] -> ""
+ | vl -> let (k,s) = aux vl in add_prefix k s
+;;
+
+(*
+let string_of_pvars pvars hyps =
+ let rec aux =
+ function
+ [] -> (0, "")
+ | he::tl ->
+ let (n,s) = aux tl in
+ (n + 1,
+ string_of_int n ^ ": " ^ (String.concat " ") (List.rev he) ^
+ match s with "" -> "" | _ -> " " ^ s
+ )
+ in
+ snd (aux (List.rev pvars))
+;;
+*)
+
+let string_of_pvars pvars hyps =
+ let find_depth pvars v =
+ let rec aux n =
+ function
+ [] -> assert false
+(* (-1,"?") For Print XML *)
+(*
+print_string "\nPVARS:" ;
+List.iter (List.iter print_string) pvars ;
+print_string "\nHYPS:" ;
+List.iter print_string hyps ;
+print_string "\n" ;
+flush stdout ;
+assert false
+*)
+ | l::_ when List.mem v l -> (n,v)
+ | _::tl -> aux (n+1) tl
+ in
+ aux 0 pvars
+ in
+ string_of_vars_list (List.map (find_depth pvars) (List.rev hyps))
+;;
+
+type variables_type =
+ Definition of string * Term.constr * Term.types
+ | Assumption of string * Term.constr
+;;
+
+let add_to_pvars x =
+ let module E = Environ in
+ let v =
+ match x with
+ Definition (v, bod, typ) ->
+ cumenv :=
+ E.push_named_decl (Names.id_of_string v, Some bod, typ) !cumenv ;
+ v
+ | Assumption (v, typ) ->
+ cumenv :=
+ E.push_named_decl (Names.id_of_string v, None, typ) !cumenv ;
+ v
+ in
+ match !pvars with
+ [] -> assert false
+ | (he::tl) -> pvars := (v::he)::tl
+;;
+
+let get_depth_of_var v =
+ let rec aux n =
+ function
+ [] -> None
+ | (he::tl) -> if List.mem v he then Some n else aux (n + 1) tl
+ in
+ aux 0 !pvars
+;;
+
+(* FUNCTIONS TO CREATE IDENTIFIERS *)
+
+(* seed to create the next identifier *)
+let next_id_cic = ref 0;;
+let next_id_types = ref 0;;
+
+(* reset_ids () reset the identifier seed to 0 *)
+let reset_ids () =
+ next_id_cic := 0 ;
+ next_id_types := 0
+;;
+
+(* get_next_id () returns fresh identifier *)
+let get_next_id =
+ function
+ `T ->
+ let res =
+ "t" ^ string_of_int !next_id_types
+ in
+ incr next_id_types ;
+ res
+ | `I ->
+ let res =
+ "i" ^ string_of_int !next_id_cic
+ in
+ incr next_id_cic ;
+ res
+;;
+
+type innersort =
+ InnerProp of Term.constr (* the constr is the type of the term *)
+ | InnerSet
+ | InnerType
+;;
+
+(* FUNCTION TO PRINT A SINGLE TERM OF CIC *)
+(* print_term t l where t is a term of Cic returns a stream of XML tokens *)
+(* suitable to be printed via the pretty printer Xml.pp. l is the list of *)
+(* bound names *)
+let print_term inner_types l env csr =
+ let module N = Names in
+ let module E = Environ in
+ let module T = Term in
+ let module X = Xml in
+ let module R = Retyping in
+ let rec names_to_ids =
+ function
+ [] -> []
+ | (N.Name id)::l -> id::(names_to_ids l)
+ | _ -> names_to_ids l
+ in
+
+ let inner_type_display env term =
+ let type_of_term =
+ Reduction.nf_betaiota (R.get_type_of env (Evd.empty) term)
+ in
+ match R.get_sort_family_of env (Evd.empty) type_of_term with
+ T.InProp -> InnerProp type_of_term
+ | T.InSet -> InnerSet
+ | T.InType -> InnerType
+ in
+
+(*WHICH FORCE FUNCTION DEPENDS ON THE ORDERING YOU WANT
+ let rec force =
+ parser
+ [< 'he ; tl >] -> let tl = (force tl) in [< 'he ; tl >]
+ | [< >] -> [<>]
+ in
+*)
+ let force x = x in
+
+ let rec term_display idradix in_lambda l env cstr =
+ let next_id = get_next_id idradix in
+ let add_sort_attribute do_output_type l' =
+ let xmlinnertype = inner_type_display env cstr in
+ match xmlinnertype with
+ InnerProp type_of_term ->
+ if do_output_type & idradix = `I then
+ begin
+ let pp_cmds = term_display `T false l env type_of_term in
+ inner_types := (next_id, pp_cmds)::!inner_types ;
+ end ;
+ ("sort","Prop")::l'
+ | InnerSet -> ("sort","Set")::l'
+ | InnerType -> ("sort","Type")::l'
+ in
+ let add_type_attribute l' =
+ ("type", string_of_sort (R.get_sort_of env (Evd.empty) cstr))::l'
+ in
+ (* kind_of_term helps doing pattern matching hiding the lower level of *)
+ (* coq coding of terms (the one of the logical framework) *)
+ match T.kind_of_term cstr with
+ T.Rel n ->
+ let id =
+ match List.nth l (n - 1) with
+ N.Name id -> id
+ | N.Anonymous -> Nameops.make_ident "_" None
+ in
+ X.xml_empty "REL"
+ (add_sort_attribute false
+ ["value",(string_of_int n) ;
+ "binder",(N.string_of_id id) ;
+ "id", next_id])
+ | T.Var id ->
+ let depth =
+ match get_depth_of_var (N.string_of_id id) with
+ None -> "?" (* when printing via Show XML Proof or Print XML id *)
+ (* no infos about variables uri are known *)
+(*V7 posso usare nametab, forse*)
+ | Some n -> string_of_int n
+ in
+ X.xml_empty "VAR"
+ (add_sort_attribute false
+ ["relUri",depth ^ "," ^ (N.string_of_id id) ;
+ "id", next_id])
+ | T.Meta n ->
+ X.xml_empty "META"
+ (add_sort_attribute false ["no",(string_of_int n) ; "id", next_id])
+ | T.Sort s ->
+ X.xml_empty "SORT" ["value",(string_of_sort s) ; "id", next_id]
+ | T.Cast (t1,t2) ->
+ X.xml_nempty "CAST" (add_sort_attribute false ["id", next_id])
+(force
+ [< X.xml_nempty "term" [] (term_display idradix false l env t1) ;
+ X.xml_nempty "type" [] (term_display idradix false l env t2)
+ >]
+)
+ | T.LetIn (nid,s,t,d)->
+ let nid' = Nameops.next_name_away nid (names_to_ids l) in
+ X.xml_nempty "LETIN" (add_sort_attribute true ["id", next_id])
+(force
+ [< X.xml_nempty "term" [] (term_display idradix false l env s) ;
+ X.xml_nempty "letintarget" ["binder",(N.string_of_id nid')]
+ (term_display idradix false
+ ((N.Name nid')::l)
+ (E.push_rel (N.Name nid', Some s, t) env)
+ d
+ )
+ >]
+)
+ | T.Prod (N.Name _ as nid, t1, t2) ->
+ let nid' = Nameops.next_name_away nid (names_to_ids l) in
+ X.xml_nempty "PROD" (add_type_attribute ["id", next_id])
+(force
+ [< X.xml_nempty "source" [] (term_display idradix false l env t1) ;
+ X.xml_nempty "target"
+ (if idradix = `T &&
+ T.noccurn 1 t2
+ then []
+ else ["binder",(N.string_of_id nid')])
+ (term_display idradix false
+ ((N.Name nid')::l)
+ (E.push_rel (N.Name nid', None, t1) env)
+ t2
+ )
+ >]
+)
+ | T.Prod (N.Anonymous as nid, t1, t2) ->
+ X.xml_nempty "PROD" (add_type_attribute ["id", next_id])
+(force
+ [< X.xml_nempty "source" [] (term_display idradix false l env t1) ;
+ X.xml_nempty "target" []
+ (term_display idradix false
+ (nid::l)
+ (E.push_rel (nid, None, t1) env)
+ t2
+ )
+ >]
+)
+ | T.Lambda (N.Name _ as nid, t1, t2) ->
+ let nid' = Nameops.next_name_away nid (names_to_ids l) in
+ X.xml_nempty "LAMBDA" (add_sort_attribute (not in_lambda) ["id",next_id])
+(force
+ [< X.xml_nempty "source" [] (term_display idradix false l env t1) ;
+ X.xml_nempty "target" ["binder",(N.string_of_id nid')]
+ (term_display idradix true
+ ((N.Name nid')::l)
+ (E.push_rel (N.Name nid', None, t1) env)
+ t2
+ )
+ >]
+)
+ | T.Lambda (N.Anonymous as nid, t1, t2) ->
+ X.xml_nempty "LAMBDA" (add_sort_attribute (not in_lambda) ["id", next_id])
+(force
+ [< X.xml_nempty "source" [] (term_display idradix false l env t1) ;
+ X.xml_nempty "target" []
+ (term_display idradix true
+ (nid::l)
+ (E.push_rel (nid, None, t1) env)
+ t2
+ )
+ >]
+)
+ | T.App (h,t) ->
+ X.xml_nempty "APPLY" (add_sort_attribute true ["id", next_id])
+(force
+ [< (term_display idradix false l env h) ;
+ (Array.fold_right
+ (fun x i -> [< (term_display idradix false l env x); i >]) t [<>])
+ >]
+)
+ | T.Const sp ->
+ X.xml_empty "CONST"
+ (add_sort_attribute false
+ ["uri",(uri_of_path sp Constant) ; "id", next_id])
+ | T.Ind (sp,i) ->
+ X.xml_empty "MUTIND"
+ ["uri",(uri_of_path sp Inductive) ;
+ "noType",(string_of_int i) ;
+ "id", next_id]
+ | T.Construct ((sp,i),j) ->
+ X.xml_empty "MUTCONSTRUCT"
+ (add_sort_attribute false
+ ["uri",(uri_of_path sp Inductive) ;
+ "noType",(string_of_int i) ;
+ "noConstr",(string_of_int j) ;
+ "id", next_id])
+ | T.Case ({T.ci_ind=(sp,i)},ty,term,a) ->
+ let (uri, typeno) = (uri_of_path sp Inductive),i in
+ X.xml_nempty "MUTCASE"
+ (add_sort_attribute true
+ ["uriType",uri ; "noType",(string_of_int typeno) ; "id",next_id])
+(force
+ [< X.xml_nempty "patternsType" []
+ [< (term_display idradix false l env ty) >] ;
+ X.xml_nempty "inductiveTerm" []
+ [< (term_display idradix false l env term)>];
+ Array.fold_right
+ (fun x i ->
+ [< X.xml_nempty "pattern" []
+ [<term_display idradix false l env x >] ; i>]
+ ) a [<>]
+ >]
+)
+ | T.Fix ((ai,i),((f,t,b) as rec_decl)) ->
+ X.xml_nempty "FIX"
+ (add_sort_attribute true ["noFun", (string_of_int i) ; "id",next_id])
+(force
+ [< Array.fold_right
+ (fun (fi,ti,bi,ai) i ->
+ [< X.xml_nempty "FixFunction"
+ ["name", (string_of_name fi); "recIndex", (string_of_int ai)]
+ [< X.xml_nempty "type" []
+ [< term_display idradix false l env ti >] ;
+ X.xml_nempty "body" [] [<
+ term_display idradix false
+ ((Array.to_list f)@l)
+ (E.push_rec_types rec_decl env)
+ bi
+ >]
+ >] ;
+ i
+ >]
+ )
+ (Array.mapi (fun j x -> (x,t.(j),b.(j),ai.(j)) ) f )
+ [<>]
+ >]
+)
+ | T.CoFix (i,((f,t,b) as rec_decl)) ->
+ X.xml_nempty "COFIX"
+ (add_sort_attribute true ["noFun", (string_of_int i) ; "id",next_id])
+(force
+ [< Array.fold_right
+ (fun (fi,ti,bi) i ->
+ [< X.xml_nempty "CofixFunction" ["name", (string_of_name fi)]
+ [< X.xml_nempty "type" []
+ [< term_display idradix false l env ti >] ;
+ X.xml_nempty "body" [] [<
+ term_display idradix false
+ ((Array.to_list f)@l)
+ (E.push_rec_types rec_decl env)
+ bi
+ >]
+ >] ;
+ i
+ >]
+ )
+ (Array.mapi (fun j x -> (x,t.(j),b.(j)) ) f ) [<>]
+ >]
+)
+ | T.Evar _ ->
+ Util.anomaly "Evar node in a term!!!"
+ in
+ (*CSC: ad l vanno andrebbero aggiunti i nomi da non *)
+ (*CSC: mascherare (costanti? variabili?) *)
+ term_display `I false l env csr
+;;
+
+(* FUNCTIONS TO PRINT A SINGLE OBJECT OF COQ *)
+
+(* print_current_proof term type id conjectures *)
+(* where term is the term of the proof in progress p *)
+(* and type is the type of p *)
+(* and id is the identifier (name) of p *)
+(* and conjectures is the list of conjectures (cic terms) *)
+(* returns a stream of XML tokens suitable to be pretty printed via Xml.pp *)
+let print_current_proof c typ id mv inner_types =
+ let module X = Xml in
+ let env = (Safe_typing.env_of_safe_env (Global.safe_env ())) in
+ [< X.xml_cdata "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n" ;
+ X.xml_cdata ("<!DOCTYPE CurrentProof SYSTEM \"" ^ dtdname ^ "\">\n\n") ;
+ X.xml_nempty "CurrentProof" ["name",id ; "id", get_next_id `I]
+ [< List.fold_right
+ (fun (j,t) i ->
+ [< X.xml_nempty "Conjecture" ["no",(string_of_int j)]
+ [< print_term inner_types [] env t >] ; i >])
+ mv [<>] ;
+ X.xml_nempty "body" [] [< print_term inner_types [] env c >] ;
+ X.xml_nempty "type" [] [< print_term inner_types [] env typ >]
+ >]
+ >]
+;;
+
+(* print_axiom id type params *)
+(* where type is the type of an axiom a *)
+(* and id is the identifier (name) of a *)
+(* and params is the list of formal params for a *)
+(* returns a stream of XML tokens suitable to be pretty printed via Xml.pp *)
+let print_axiom id typ fv hyps env inner_types =
+ let module X = Xml in
+ let module N = Names in
+ [< X.xml_cdata "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n" ;
+ X.xml_cdata ("<!DOCTYPE Axiom SYSTEM \"" ^ dtdname ^ "\">\n\n") ;
+ X.xml_nempty "Axiom"
+ ["name",(N.string_of_id id) ;
+ "id", get_next_id `I ;
+ "params",(string_of_pvars fv hyps)]
+ [< X.xml_nempty "type" [] (print_term inner_types [] env typ) >]
+ >]
+;;
+
+(* print_definition id term type params hyps *)
+(* where id is the identifier (name) of a definition d *)
+(* and term is the term (body) of d *)
+(* and type is the type of d *)
+(* and params is the list of formal params for d *)
+(* returns a stream of XML tokens suitable to be pretty printed via Xml.pp *)
+let print_definition id c typ fv hyps env inner_types =
+ let module X = Xml in
+ let module N = Names in
+ [< X.xml_cdata "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n" ;
+ X.xml_cdata ("<!DOCTYPE Definition SYSTEM \"" ^ dtdname ^ "\">\n\n") ;
+ X.xml_nempty "Definition"
+ ["name",(N.string_of_id id) ;
+ "id", get_next_id `I ;
+ "params",(string_of_pvars fv hyps)]
+ [< X.xml_nempty "body" [] (print_term inner_types [] env c) ;
+ X.xml_nempty "type" [] (print_term inner_types [] env typ) >]
+ >]
+;;
+
+(* print_variable id type *)
+(* where id is the identifier (name) of a variable v *)
+(* and type is the type of v *)
+(* returns a stream of XML tokens suitable to be pretty printed via Xml.pp *)
+let print_variable id body typ env inner_types =
+ let module X = Xml in
+ let module N = Names in
+ [< X.xml_cdata "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n" ;
+ X.xml_cdata ("<!DOCTYPE Variable SYSTEM \"" ^ dtdname ^ "\">\n\n") ;
+ X.xml_nempty "Variable" ["name",(N.string_of_id id); "id", get_next_id `I]
+ [< (match body with
+ None -> [<>]
+ | Some body ->
+ X.xml_nempty "body" [] (print_term inner_types [] env body)
+ ) ;
+ X.xml_nempty "type" [] (print_term inner_types [] env typ)
+ >]
+ >]
+;;
+
+(* print_mutual_inductive_packet p *)
+(* where p is a mutual inductive packet (an inductive definition in a block *)
+(* of mutual inductive definitions) *)
+(* returns a stream of XML tokens suitable to be pretty printed via Xml.pp *)
+(* Used only by print_mutual_inductive *)
+let print_mutual_inductive_packet inner_types names env finite p =
+ let module D = Declarations in
+ let module N = Names in
+ let module T = Term in
+ let module X = Xml in
+ let {D.mind_consnames=consnames ;
+ D.mind_typename=typename ;
+ D.mind_nf_lc=lc ;
+ D.mind_nf_arity=arity} = p
+ in
+ [< X.xml_nempty "InductiveType"
+ ["name",(N.string_of_id typename) ;
+ "inductive",(string_of_bool finite)
+ ]
+ [<
+ X.xml_nempty "arity" []
+ (print_term inner_types [] env (T.body_of_type arity)) ;
+ (Array.fold_right
+ (fun (name,lc) i ->
+ [< X.xml_nempty "Constructor" ["name",(N.string_of_id name)]
+ (print_term inner_types names env lc) ;
+ i
+ >])
+ (Array.mapi (fun j x -> (x,T.body_of_type lc.(j)) ) consnames )
+ [<>]
+ )
+ >]
+ >]
+;;
+
+(* print_mutual_inductive packs params nparams *)
+(* where packs is the list of inductive definitions in the block of *)
+(* mutual inductive definitions b *)
+(* and params is the list of formal params for b *)
+(* and nparams is the number of "parameters" in the arity of the *)
+(* mutual inductive types *)
+(* returns a stream of XML tokens suitable to be pretty printed via Xml.pp *)
+let print_mutual_inductive finite packs fv hyps env inner_types =
+ let module D = Declarations in
+ let module E = Environ in
+ let module X = Xml in
+ let module N = Names in
+ let nparams = extract_nparams packs in
+ let names =
+ List.map
+ (fun p -> let {D.mind_typename=typename} = p in N.Name(typename))
+ (Array.to_list packs)
+ in
+ let env =
+ List.fold_right
+ (fun {D.mind_typename=typename ; D.mind_nf_arity=arity} env ->
+ E.push_rel (N.Name typename, None, arity) env)
+ (Array.to_list packs)
+ env
+ in
+ [< X.xml_cdata "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n" ;
+ X.xml_cdata ("<!DOCTYPE InductiveDefinition SYSTEM \"" ^
+ dtdname ^ "\">\n\n") ;
+ X.xml_nempty "InductiveDefinition"
+ ["noParams",string_of_int nparams ;
+ "id",get_next_id `I ;
+ "params",(string_of_pvars fv hyps)]
+ [< (Array.fold_right
+ (fun x i ->
+ [< print_mutual_inductive_packet
+ inner_types names env finite x ; i >]
+ ) packs [< >]
+ )
+ >]
+ >]
+;;
+
+let string_list_of_named_context_list =
+ List.map
+ (function (n,_,_) -> Names.string_of_id n)
+;;
+
+let types_filename_of_filename =
+ function
+ Some f -> Some (f ^ ".types")
+ | None -> None
+;;
+
+let pp_cmds_of_inner_types inner_types target_uri =
+ let module X = Xml in
+ let rec stream_of_list =
+ function
+ [] -> [<>]
+ | he::tl -> [< he ; stream_of_list tl >]
+ in
+ [< X.xml_cdata "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n" ;
+ X.xml_cdata ("<!DOCTYPE InnerTypes SYSTEM \"" ^ typesdtdname ^ "\">\n\n");
+ X.xml_nempty "InnerTypes" ["of",target_uri]
+ (stream_of_list
+ (List.map
+ (function
+ (id,type_pp_cmds) -> X.xml_nempty "TYPE" ["of",id] type_pp_cmds)
+ (List.rev inner_types)
+ ))
+ >]
+;;
+
+(* print id dest *)
+(* where sp is the qualified identifier (section path) of a *)
+(* definition/theorem, variable or inductive definition *)
+(* and dest is either None (for stdout) or (Some filename) *)
+(* pretty prints via Xml.pp the object whose identifier is id on dest *)
+(* Note: it is printed only (and directly) the most cooked available *)
+(* form of the definition (all the parameters are *)
+(* lambda-abstracted, but the object can still refer to variables) *)
+let print qid fn =
+ let module D = Declarations in
+ let module G = Global in
+ let module N = Names in
+ let module Nt = Nametab in
+ let module T = Term in
+ let module X = Xml in
+ let (_,id) = Nt.repr_qualid qid in
+ let glob_ref = Nametab.locate qid in
+ let env = (Safe_typing.env_of_safe_env (G.safe_env ())) in
+ reset_ids () ;
+ let inner_types = ref [] in
+ let sp,tag,pp_cmds =
+ match glob_ref with
+ Nt.VarRef id ->
+ let sp = Declare.find_section_variable id in
+ let (_,body,typ) = G.lookup_named id in
+ sp,Variable,print_variable id body (T.body_of_type typ) env inner_types
+ | Nt.ConstRef sp ->
+ let {D.const_body=val0 ; D.const_type = typ ; D.const_hyps = hyps} =
+ G.lookup_constant sp in
+ let hyps = string_list_of_named_context_list hyps in
+ let typ = T.body_of_type typ in
+ sp,Constant,
+ begin
+ match val0 with
+ None -> print_axiom id typ [] hyps env inner_types
+ | Some c -> print_definition id c typ [] hyps env inner_types
+ end
+ | Nt.IndRef (sp,_) ->
+ let {D.mind_packets=packs ;
+ D.mind_hyps=hyps;
+ D.mind_finite=finite} = G.lookup_mind sp in
+ let hyps = string_list_of_named_context_list hyps in
+ sp,Inductive,
+ print_mutual_inductive finite packs [] hyps env inner_types
+ | Nt.ConstructRef _ ->
+ Util.anomaly ("print: this should not happen")
+ in
+ Xml.pp pp_cmds fn ;
+ Xml.pp (pp_cmds_of_inner_types !inner_types (uri_of_path sp tag))
+ (types_filename_of_filename fn)
+;;
+
+(* show dest *)
+(* where dest is either None (for stdout) or (Some filename) *)
+(* pretty prints via Xml.pp the proof in progress on dest *)
+let show fn =
+ let pftst = Pfedit.get_pftreestate () in
+ let str = Names.string_of_id (Pfedit.get_current_proof_name ()) in
+ let pf = Tacmach.proof_of_pftreestate pftst in
+ let typ = (Proof_trees.goal_of_proof pf).Evd.evar_concl in
+ let val0,mv = Tacmach.extract_open_pftreestate pftst in
+ reset_ids () ;
+ let inner_types = ref [] in
+ Xml.pp
+ (print_current_proof val0 typ str mv inner_types)
+ fn ;
+ Xml.pp (pp_cmds_of_inner_types !inner_types ("?" ^ str ^ "?"))
+ (types_filename_of_filename fn)
+;;
+
+(* FUNCTIONS TO PRINT AN ENTIRE SECTION OF COQ *)
+
+(* list of (name, uncooked sp, most cooked sp, uncooked leaf object, *)
+(* list of possible variables, directory name) *)
+(* used to collect informations on the uncooked and most cooked forms *)
+(* of objects that could be cooked (have namesakes) *)
+let printed = ref [];;
+
+(* makes a filename from a directory name, a section path and an extension *)
+let mkfilename dn sp ext =
+ let dir_list_of_dirpath s =
+ let rec aux n =
+ try
+ let pos = String.index_from s n '/' in
+ let head = String.sub s n (pos - n) in
+ head::(aux (pos + 1))
+ with
+ Not_found -> [String.sub s n (String.length s - n)]
+ in
+ aux 0
+ in
+ let rec join_dirs cwd =
+ function
+ [] -> assert false
+ | [he] -> "/" ^ he
+ | he::tail ->
+ let newcwd = cwd ^ "/" ^ he in
+ (try
+ Unix.mkdir newcwd 0o775
+ with _ -> () (* Let's ignore the errors on mkdir *)
+ ) ;
+ "/" ^ he ^ join_dirs newcwd tail
+ in
+ let module L = Library in
+ let module S = System in
+ let module N = Names in
+ let module No = Nameops in
+ match dn with
+ None -> None
+ | Some basedir ->
+ let dir0 = No.extend_dirpath (No.dirpath sp) (No.basename sp) in
+ let dir = List.map N.string_of_id (List.rev (N.repr_dirpath dir0)) in
+ Some (basedir ^ join_dirs basedir dir ^ "." ^ ext)
+;;
+
+(* print_object leaf_object id section_path directory_name formal_vars *)
+(* where leaf_object is a leaf object *)
+(* and id is the identifier (name) of the definition/theorem *)
+(* or of the inductive definition o *)
+(* and section_path is the section path of o *)
+(* and directory_name is the base directory in which putting the print *)
+(* and formal_vars is the list of parameters (variables) of o *)
+(* pretty prints via Xml.pp the object o in the right directory deduced *)
+(* from directory_name and section_path *)
+(* Note: it is printed only the uncooked available form of the object plus *)
+(* the list of parameters of the object deduced from it's most cooked *)
+(* form *)
+let print_object lobj id sp dn fv env =
+ let module D = Declarations in
+ let module E = Environ in
+ let module G = Global in
+ let module N = Names in
+ let module T = Term in
+ let module X = Xml in
+ let strtag = Libobject.object_tag lobj in
+ try
+ let tag = tag_of_string_tag strtag in
+ reset_ids () ;
+ let inner_types = ref [] in
+ let pp_cmds =
+ match strtag with
+ "CONSTANT" (* = Definition, Theorem *)
+ | "PARAMETER" (* = Axiom *) ->
+ let {D.const_body=val0 ; D.const_type = typ ; D.const_hyps = hyps} =
+ G.lookup_constant sp
+ in
+ let hyps = string_list_of_named_context_list hyps in
+ let typ = T.body_of_type typ in
+ begin
+ match val0 with
+ None -> print_axiom id typ fv hyps env inner_types
+ | Some c -> print_definition id c typ fv hyps env inner_types
+ end
+ | "INDUCTIVE" ->
+ let
+ {D.mind_packets=packs ;
+ D.mind_hyps = hyps;
+ D.mind_finite = finite
+ } = G.lookup_mind sp
+ in
+ let hyps = string_list_of_named_context_list hyps in
+ print_mutual_inductive finite packs fv hyps env inner_types
+ | "VARIABLE" ->
+ let (_,(_,varentry,_)) = Declare.out_variable lobj in
+ begin
+ match varentry with
+ Declare.SectionLocalDef (body,optt) ->
+ let typ = match optt with
+ | None -> Retyping.get_type_of env Evd.empty body
+ | Some t -> t in
+ add_to_pvars (Definition (N.string_of_id id, body, typ)) ;
+ print_variable id (Some body) typ env inner_types
+ | Declare.SectionLocalAssum typ ->
+ add_to_pvars (Assumption (N.string_of_id id, typ)) ;
+ print_variable id None (T.body_of_type typ) env inner_types
+ end
+ | "CLASS"
+ | "COERCION"
+ | _ -> raise Uninteresting
+ and fileext () = ext_of_tag tag in
+ let fn = (mkfilename dn sp (fileext ())) in
+ Xml.pp pp_cmds fn ;
+ Xml.pp (pp_cmds_of_inner_types !inner_types (uri_of_path sp tag))
+ (types_filename_of_filename fn)
+ with
+ Uninteresting -> ()
+;;
+
+(* print_library_segment state bprintleaf directory_name *)
+(* where state is a list of (section-path, node) *)
+(* and bprintleaf is true iff the leaf objects should be printed *)
+(* and directory_name is the name of the base directory in which to print *)
+(* the files *)
+(* print via print_node all the nodes (leafs excluded if bprintleaf is false) *)(* in state *)
+let rec print_library_segment state bprintleaf dn =
+ List.iter
+ (function (sp, node) ->
+ print_if_verbose ("Print_library_segment: " ^ Names.string_of_path sp ^ "\n") ;
+ print_node node (Nameops.basename sp) sp bprintleaf dn ;
+ print_if_verbose "\n"
+ ) (List.rev state)
+(* print_node node id section_path bprintleaf directory_name *)
+(* prints a single node (and all it's subnodes via print_library_segment *)
+and print_node n id sp bprintleaf dn =
+ let module L = Lib in
+ match n with
+ L.Leaf o ->
+ print_if_verbose "LEAF\n" ;
+ if bprintleaf then
+ begin
+ if not (List.mem id !printed) then
+ (* this is an uncooked term or a local (with no namesakes) term *)
+ begin
+try
+ if could_have_namesakes o sp then
+ begin
+ (* this is an uncooked term *)
+ print_if_verbose ("OK, stampo solo questa volta " ^ Names.string_of_id id ^ "\n") ;
+ print_object o id sp dn !pvars !cumenv ;
+ printed := id::!printed
+ end
+ else
+ begin
+ (* this is a local term *)
+ print_if_verbose ("OK, stampo " ^ Names.string_of_id id ^ "\n") ;
+ print_object o id sp dn !pvars !cumenv
+ end
+with _ -> print_if_verbose ("EXCEPTION RAISED!!!\n");
+ end
+ else
+ begin
+ (* update the least cooked sp *)
+ print_if_verbose ("Suppongo gia' stampato " ^ Names.string_of_id id ^ "\n")
+ end
+ end
+ | L.OpenedSection (dir,_) ->
+ let id = snd (Nameops.split_dirpath dir) in
+ print_if_verbose ("OpenDir " ^ Names.string_of_id id ^ "\n")
+ | L.ClosedSection (_,dir,state) ->
+ let id = snd (Nameops.split_dirpath dir) in
+ print_if_verbose("ClosedDir " ^ Names.string_of_id id ^ "\n") ;
+ if bprintleaf then
+ begin
+ (* open a new scope *)
+ pvars := []::!pvars ;
+ print_library_segment state bprintleaf dn ;
+ (* close the scope *)
+ match !pvars with
+ [] -> assert false
+ | he::tl -> pvars := tl
+ end ;
+ print_if_verbose "/ClosedDir\n"
+ | L.Module s ->
+ print_if_verbose ("Module " ^ (Names.string_of_dirpath s) ^ "\n")
+ | L.FrozenState _ ->
+ print_if_verbose ("FrozenState\n")
+;;
+
+(* print_closed_section module_name node directory_name *)
+(* where module_name is the name of a module *)
+(* and node is the library segment of the module *)
+(* and directory_name is the base directory in which to put the xml files *)
+(* prints all the leaf objects of the tree rooted in node using *)
+(* print_library_segment on all its sons *)
+let print_closed_section s ls dn =
+ let module L = Lib in
+ printed := [] ;
+ pvars := [[]] ;
+ cumenv := Safe_typing.env_of_safe_env (Global.safe_env ()) ;
+ print_if_verbose ("Module " ^ s ^ ":\n") ;
+ print_library_segment ls true dn ;
+ print_if_verbose "\n/Module\n" ;
+;;
+
+(* printModule identifier directory_name *)
+(* where identifier is the name of a module (section) d *)
+(* and directory_name is the directory in which to root all the xml files *)
+(* prints all the xml files and directories corresponding to the subsections *)
+(* and terms of the module d *)
+(* Note: the terms are printed in their uncooked form plus the informations *)
+(* on the parameters of their most cooked form *)
+let printModule qid dn =
+ let module L = Library in
+ let module N = Nametab in
+ let module X = Xml in
+
+ let (_,dir_path,_) = L.locate_qualified_library qid in
+
+ let str = N.string_of_qualid qid in
+ let ls = L.module_segment (Some dir_path) in
+ print_if_verbose ("MODULE_BEGIN " ^ str ^ " " ^
+ (L.module_full_filename dir_path) ^ "\n") ;
+ print_closed_section str (List.rev ls) dn ;
+ print_if_verbose ("MODULE_END " ^ str ^ " " ^
+ (L.module_full_filename dir_path) ^ "\n")
+;;
+
+(* printSection identifier directory_name *)
+(* where identifier is the name of a closed section d *)
+(* and directory_name is the directory in which to root all the xml files *)
+(* prints all the xml files and directories corresponding to the subsections *)
+(* and terms of the closed section d *)
+(* Note: the terms are printed in their uncooked form plus the informations *)
+(* on the parameters of their most cooked form *)
+let printSection id dn =
+ let module L = Library in
+ let module N = Names in
+ let module No = Nameops in
+ let module X = Xml in
+ let sp = Lib.make_path id in
+ let ls =
+ let rec find_closed_section =
+ function
+ [] -> raise Not_found
+ | (_,Lib.ClosedSection (_,dir,ls))::_ when snd (No.split_dirpath dir) = id
+ -> ls
+ | _::t -> find_closed_section t
+ in
+ print_string ("Searching " ^ Names.string_of_path sp ^ "\n") ;
+ find_closed_section (Lib.contents_after None)
+ in
+ let str = N.string_of_id id in
+ print_if_verbose ("SECTION_BEGIN " ^ str ^ " " ^ N.string_of_path sp ^ "\n");
+ print_closed_section str ls dn ;
+ print_if_verbose ("SECTION_END " ^ str ^ " " ^ N.string_of_path sp ^ "\n")
+;;
+
+(* print All () prints what is the structure of the current environment of *)
+(* Coq. No terms are printed. Useful only for debugging *)
+let printAll () =
+ let state = Library.module_segment None in
+ let oldverbose = !verbose in
+ verbose := true ;
+ print_library_segment state false None ;
+(*
+ let ml = Library.loaded_modules () in
+ List.iter (function i -> printModule (Names.id_of_string i) None) ml ;
+*)
+ verbose := oldverbose
+;;
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 18:20:59 +0000