diff options
| -rw-r--r-- | contrib/xml/cooking.ml | 41 | ||||
| -rw-r--r-- | contrib/xml/xmlcommand.ml | 12 |
2 files changed, 26 insertions, 27 deletions
diff --git a/contrib/xml/cooking.ml b/contrib/xml/cooking.ml index 19420ff46..10c8d80ef 100644 --- a/contrib/xml/cooking.ml +++ b/contrib/xml/cooking.ml @@ -57,32 +57,31 @@ let get_params_from_type vl t = in let pl = List.rev (rget t []) in string_of_vars_list pl - (*List.fold_right - (fun x i -> x ^ match i with "" -> "" | i' -> " " ^ i') pl ""*) ;; (* add_cooking_information csp vl *) (* when csp is the section path of the most cooked object co *) (* and vl is the list of variables possibly occuring in co *) (* returns the list of variables actually occurring in co *) -let add_cooking_information csp vl = -(* - let module CT = Constrtypes in +let add_cooking_information sp vl = + let module D = Declarations in + let module G = Global in let module N = Names in - let clobj = Lib.map_leaf (N.objsp_of csp) in - let ctag = Libobject.object_tag clobj in - match ctag with - "CONSTANT" -> - let (ccmap, _, _) = Environ.outConstant clobj in - let {CT.cONSTBODY=cval0 ; - CT.cONSTTYPE=ctyp} = Listmap.map ccmap N.CCI - in - get_params_from_type vl ctyp - | "MUTUALINDUCTIVE" -> - let (cmap, _) = Environ.outMutualInductive clobj in - let {CT.mINDPACKETS=packs} = Listmap.map cmap N.CCI in - let {CT.mINDARITY=arity} = packs.(0) in - get_params_from_type vl arity - | _ -> Std.anomaly "Cooking of an uncoockable term required" -*) "" + let module T = Term in + let module X = Xml in + try + let {D.const_body=val0 ; D.const_type = typ} = G.lookup_constant sp in + let typ = T.body_of_type typ in + get_params_from_type vl typ + with + Not_found -> + try + let {D.mind_packets=packs ; D.mind_nparams=nparams} = + G.lookup_mind sp + in + let {D.mind_nf_arity=arity} = packs.(0) in + let arity = T.body_of_type arity in + get_params_from_type vl arity + with + Not_found -> Util.anomaly "Cooking of an uncoockable term required" ;; diff --git a/contrib/xml/xmlcommand.ml b/contrib/xml/xmlcommand.ml index 1206892cf..6364d258c 100644 --- a/contrib/xml/xmlcommand.ml +++ b/contrib/xml/xmlcommand.ml @@ -15,7 +15,7 @@ (* CONFIGURATION PARAMETERS *) let dtdname = "http://localhost:8081/getdtd?url=cic.dtd";; -let verbose = ref false;; (* always set to true during a "Print XML All" *) +let verbose = ref true;; (* always set to true during a "Print XML All" *) @@ -62,7 +62,7 @@ let print_if_verbose s = if !verbose then print_string s;; let ext_of_tag = function "CONSTANT" -> "con" - | "MUTUALINDUCTIVE" -> "ind" + | "INDUCTIVE" -> "ind" | "VARIABLE" -> "var" | _ -> "err" (* uninteresting thing that won't be printed *) ;; @@ -75,7 +75,7 @@ let tag_of_sp sp = with Not_found -> try - let _ = G.lookup_mind sp in "MUTUALINDUCTIVE" + let _ = G.lookup_mind sp in "INDUCTIVE" with Not_found -> (* We could only hope it is a variable *) @@ -88,6 +88,7 @@ let tag_of_sp sp = 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 @@ -95,7 +96,7 @@ let could_have_namesakes o sp = (* namesake = omonimo in italian *) | D.NeverDischarge -> true (* a non-local one *) ) | "VARIABLE" -> false (* variables are local, so no namesakes *) - | "MUTUALINDUCTIVE" -> true (* mutual inductive types are never local *) + | "INDUCTIVE" -> true (* mutual inductive types are never local *) | _ -> false (* uninteresting thing that won't be printed*) ;; @@ -622,14 +623,13 @@ let print_object o id sp dn fv = D.Cooked c -> print_definition id c typ fv | D.Recipe _ -> Util.anomaly "trying to print a recipe" end - | "MUTUALINDUCTIVE" -> + | "INDUCTIVE" -> (*CSC: QUI CI SONO ANCHE LE VARIABILI, CREDO, CHIAMATE mind_hyps *) let {D.mind_packets=packs ; D.mind_nparams=nparams} = G.lookup_mind sp in print_mutual_inductive packs fv nparams | "VARIABLE" -> - (*CHE COSA E' IL PRIMO ARGOMENTO?*) let (_,typ) = G.lookup_named id in add_to_pvars (N.string_of_id id) ; print_variable id (T.body_of_type typ) |