diff options
Diffstat (limited to 'contrib/xml')
-rw-r--r-- | contrib/xml/xmlcommand.ml | 273 |
1 files changed, 1 insertions, 272 deletions
diff --git a/contrib/xml/xmlcommand.ml b/contrib/xml/xmlcommand.ml index 63f7bfce2..ace8a7435 100644 --- a/contrib/xml/xmlcommand.ml +++ b/contrib/xml/xmlcommand.ml @@ -19,7 +19,7 @@ (* CONFIGURATION PARAMETERS *) -let verbose = ref false;; (* always set to true during a "Print XML All" *) +let verbose = ref false;; (* HOOKS *) let print_proof_tree, set_print_proof_tree = @@ -557,277 +557,6 @@ let show fn = show_pftreestate fn (kind,pftst) id ;; -(* -(* 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 = -(*CSC: - 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 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 (join_dirs basedir dir ^ "." ^ ext) -*) match dn with None -> None | Some _ -> Some "/tmp/nonloso" -;; - -(* print_coq_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_coq_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 -(*CSC: GROSSO BUG: env e' l'environment cumulativo in cui aggiungiamo passo passo tutte le variabili. Qui, invece, non lo stiamo piu' usando per nulla. Quindi la prima variabile che incontreremo non verra' trovata ;-(((( Direi che l'environment vada passato fino alla print_object che a sua volta lo passera' a chi di dovere (ovvero sia a Cic2Acic che a DoubleTypeInference *) - let strtag = Libobject.object_tag lobj in - try - let tag = tag_of_string_tag strtag in - let obj = - match strtag with - "CONSTANT" (* = Definition, Theorem, Axiom *) - let {D.const_body=val0 ; D.const_type = typ ; D.const_hyps = hyps} = - G.lookup_constant sp - in - mk_constant_obj id val0 typ fv hyps - | "INDUCTIVE" -> - let - {D.mind_packets=packs ; - D.mind_hyps = hyps; - D.mind_finite = finite - } = G.lookup_mind sp - in - mk_inductive_obj sp packs fv hyps finite - | "VARIABLE" -> - let (_,(_,varentry,_)) = Declare.out_variable lobj in - begin - match varentry with - Declare.SectionLocalDef (body,optt,opaq) -> - 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)) ; - mk_variable_obj id (Some body) typ - | Declare.SectionLocalAssum typ -> - add_to_pvars (Assumption (N.string_of_id id, typ)) ; - mk_variable_obj id None (T.body_of_type typ) - end - | "CLASS" - | "COERCION" - | _ -> raise Uninteresting - in - let fileext () = ext_of_tag tag in - let fn = mkfilename dn sp (fileext ()) in - print_object (uri_of_path sp tag) obj Evd.empty None 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 -(*CSC: pezza quando i .vo sono magri -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_coq_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_coq_object o id sp dn !pvars !cumenv - end -(*CSC: pezza quando i .vo sono magri -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 *) - let (_,section_name) = Nameops.split_dirpath dir in - pvars := (section_name,[])::!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 := [Names.id_of_string "",[]] ; - 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 (loc,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 -;; -*) - - -(*CSC: Ask Hugo for a better solution *) -(* -let ref_of_kernel_name kn = - let module N = Names in - let module Ln = Libnames in - let (modpath,_,label) = N.repr_kn kn in - match modpath with - N.MPself _ -> Ln.Qualid (Ln.qualid_of_sp (Nametab.sp_of_global None kn)) - | _ -> - Util.anomaly ("ref_of_kernel_name: the module path is not MPself") -;; -*) (* Let's register the callbacks *) let xml_library_root = |