From e88e0b2140bdd2d194a52bc09f8338b5667d0f92 Mon Sep 17 00:00:00 2001 From: herbelin Date: Thu, 14 Nov 2002 18:37:54 +0000 Subject: Réforme de l'interprétation des termes : - Le parsing se fait maintenant via "constr_expr" au lieu de "Coqast.t" - "Coqast.t" reste pour l'instant pour le pretty-printing. Un deuxième pretty-printer dans ppconstr.ml est basé sur "constr_expr". - Nouveau répertoire "interp" qui hérite de la partie interprétation qui se trouvait avant dans "parsing" (constrintern.ml remplace astterm.ml; constrextern.ml est l'équivalent de termast.ml pour le nouveau printer; topconstr.ml; contient la définition de "constr_expr"; modintern.ml remplace astmod.ml) - Libnames.reference tend à remplacer Libnames.qualid git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3235 85f007b7-540e-0410-9357-904b9bb8a0f7 --- contrib/xml/cic2acic.ml | 2 +- contrib/xml/xmlcommand.ml | 43 ++++++++++++++++++++++++------------------- contrib/xml/xmlcommand.mli | 2 +- contrib/xml/xmlentries.ml4 | 4 ++-- 4 files changed, 28 insertions(+), 23 deletions(-) (limited to 'contrib/xml') diff --git a/contrib/xml/cic2acic.ml b/contrib/xml/cic2acic.ml index 19dfc940ae..1cd33f53c4 100644 --- a/contrib/xml/cic2acic.ml +++ b/contrib/xml/cic2acic.ml @@ -249,7 +249,7 @@ print_endline "PASSATO" ; flush stdout ; let subst,residual_args,uninst_vars = let variables,basedir = try - let g = Declare.reference_of_constr h in + let g = Libnames.reference_of_constr h in let sp = match g with Libnames.ConstructRef ((induri,_),_) diff --git a/contrib/xml/xmlcommand.ml b/contrib/xml/xmlcommand.ml index 151d4582b9..07df70a0c0 100644 --- a/contrib/xml/xmlcommand.ml +++ b/contrib/xml/xmlcommand.ml @@ -393,7 +393,7 @@ let mk_inductive_obj sp packs variables hyps finite = (* 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 as locqid) fn = +let print r fn = let module D = Declarations in let module De = Declare in let module G = Global in @@ -402,14 +402,16 @@ let print (_,qid as locqid) fn = let module T = Term in let module X = Xml in let module Ln = Libnames in - let (_,id) = Libnames.repr_qualid qid in + let (_,id) = Ln.repr_qualid (snd (Ln.qualid_of_reference r)) in let glob_ref = (*CSC: ask Hugo why Nametab.global does not work with variables and *) (*CSC: we have to do this hugly try ... with *) try - Nt.global locqid + Nt.global r with - _ -> let (_,id) = Ln.repr_qualid qid in Ln.VarRef id + _ -> + let (_,id) = Ln.repr_qualid (snd (Ln.qualid_of_reference r)) in + Ln.VarRef id in (* Variables are the identifiers of the variables in scope *) let variables = search_variables () in @@ -761,14 +763,17 @@ let filename_of_path ?(keep_sections=false) xml_library_root kn tag = ;; (*CSC: Ask Hugo for a better solution *) -let qualid_of_kernel_name kn = +(* +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 _ -> Libnames.make_qualid (Lib.cwd ()) (N.id_of_label label) + N.MPself _ -> Ln.Qualid (Ln.qualid_of_sp (Nametab.sp_of_global None kn)) | _ -> - Util.anomaly ("qualid_of_kernel_name: the module path is not MPself") + Util.anomaly ("ref_of_kernel_name: the module path is not MPself") ;; +*) (* Let's register the callbacks *) let xml_library_root = @@ -787,37 +792,37 @@ let _ = let _ = Declare.set_xml_declare_variable - (function kn -> + (function (sp,kn) -> let filename = filename_of_path ~keep_sections:true xml_library_root kn Cic2acic.Variable in - let qualid = qualid_of_kernel_name kn in let dummy_location = -1,-1 in - print (dummy_location,qualid) filename) + let ref = Libnames.Qualid (dummy_location,Libnames.qualid_of_sp sp) in + print ref filename) ;; let _ = Declare.set_xml_declare_constant - (function kn -> + (function (sp,kn) -> let filename = filename_of_path xml_library_root kn Cic2acic.Constant in - let qualid = qualid_of_kernel_name kn in + let dummy_location = -1,-1 in + let ref = Libnames.Qualid (dummy_location,Libnames.qualid_of_sp sp) in match !proof_to_export with None -> - let dummy_location = -1,-1 in - print (dummy_location,qualid) filename + print ref filename | Some pftreestate -> (* It is a proof. Let's export it starting from the proof-tree *) (* I saved in the Pfedit.set_xml_cook_proof callback. *) - show_pftreestate filename pftreestate - (Names.id_of_label (Names.label kn)) ; + show_pftreestate filename pftreestate + (Names.id_of_label (Names.label kn)) ; proof_to_export := None) ;; let _ = Declare.set_xml_declare_inductive - (function kn -> + (function (sp,kn) -> let filename = filename_of_path xml_library_root kn Cic2acic.Inductive in - let qualid = qualid_of_kernel_name kn in let dummy_location = -1,-1 in - print (dummy_location,qualid) filename) + let ref = Libnames.Qualid (dummy_location,Libnames.qualid_of_sp sp) in + print ref filename) ;; diff --git a/contrib/xml/xmlcommand.mli b/contrib/xml/xmlcommand.mli index 4690e21c19..6e43be9c20 100644 --- a/contrib/xml/xmlcommand.mli +++ b/contrib/xml/xmlcommand.mli @@ -28,7 +28,7 @@ (* 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) *) -val print : Libnames.qualid Util.located -> string option -> unit +val print : Libnames.reference -> string option -> unit (* show dest *) (* where dest is either None (for stdout) or (Some filename) *) diff --git a/contrib/xml/xmlentries.ml4 b/contrib/xml/xmlentries.ml4 index fbb9944d37..6988f789ee 100644 --- a/contrib/xml/xmlentries.ml4 +++ b/contrib/xml/xmlentries.ml4 @@ -81,14 +81,14 @@ let _ = (wit_diskname, pr_diskname) VERNAC COMMAND EXTEND Xml -| [ "Print" "XML" filename(fn) qualid(id) ] -> [ Xmlcommand.print id fn ] +| [ "Print" "XML" filename(fn) global(id) ] -> [ Xmlcommand.print id fn ] | [ "Show" "XML" filename(fn) "Proof" ] -> [ Xmlcommand.show fn ] (* | [ "Print" "XML" "All" ] -> [ Xmlcommand.printAll () ] -| [ "Print" "XML" "Module" diskname(dn) qualid(id) ] -> +| [ "Print" "XML" "Module" diskname(dn) global(id) ] -> [ Xmlcommand.printLibrary id dn ] | [ "Print" "XML" "Section" diskname(dn) ident(id) ] -> -- cgit v1.2.3