From d14df293d2696f00a8de137bea9fe3a89e0bdeb0 Mon Sep 17 00:00:00 2001 From: letouzey Date: Wed, 19 Dec 2001 11:42:11 +0000 Subject: reparation du make depend et du .depend git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2334 85f007b7-540e-0410-9357-904b9bb8a0f7 --- contrib/xml/xmlcommand.ml | 1037 --------------------------------------------- 1 file changed, 1037 deletions(-) delete mode 100644 contrib/xml/xmlcommand.ml (limited to 'contrib/xml/xmlcommand.ml') diff --git a/contrib/xml/xmlcommand.ml b/contrib/xml/xmlcommand.ml deleted file mode 100644 index 7b6303130b..0000000000 --- a/contrib/xml/xmlcommand.ml +++ /dev/null @@ -1,1037 +0,0 @@ -(***********************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* *) -(* 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" [] - [] ; 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 "\n" ; - X.xml_cdata ("\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 "\n" ; - X.xml_cdata ("\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 "\n" ; - X.xml_cdata ("\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 "\n" ; - X.xml_cdata ("\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 "\n" ; - X.xml_cdata ("\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 "\n" ; - X.xml_cdata ("\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 -;; -- cgit v1.2.3