diff options
Diffstat (limited to 'parsing')
35 files changed, 616 insertions, 138 deletions
diff --git a/parsing/.cvsignore b/parsing/.cvsignore index ffeaac2ef..a2e50565c 100644 --- a/parsing/.cvsignore +++ b/parsing/.cvsignore @@ -1,7 +1,6 @@ lexer.ml *.ppo pcoq.ml -extend.ml g_prim.ml q_coqast.ml g_basevernac.ml diff --git a/parsing/ast.ml b/parsing/ast.ml index 46fb041a7..a41e627e6 100755 --- a/parsing/ast.ml +++ b/parsing/ast.ml @@ -11,6 +11,7 @@ open Pp open Util open Names +open Libnames open Coqast open Tacexpr open Genarg @@ -111,15 +112,6 @@ type act = | ActCase of act * (pat * act) list | ActCaseList of act * (pat * act) list -(* -type act = - | Aast of typed_ast - | Aastlist of patlist - | Acase of act * (Coqast.t * act) list - | Atypedcase of act * (typed_ast * act) list - | Acaselist of act * (patlist * act) list -*) - (* values associated to variables *) type typed_ast = | AstListNode of Coqast.t list @@ -139,7 +131,7 @@ let rec print_ast ast = match ast with | Num(_,n) -> int n | Str(_,s) -> qs s - | Path(_,sl) -> str (string_of_path sl) + | Path(_,sl) -> str (string_of_kn sl) | Id (_,s) -> str "{" ++ str s ++ str "}" | Nvar(_,s) -> str (string_of_id s) | Nmeta(_,s) -> str s @@ -226,8 +218,8 @@ let coerce_to_id a = match coerce_to_var a with (loc ast,"Ast.coerce_to_id", str"This expression should be a simple identifier") -let coerce_qualid_to_id (loc,qid) = match Nametab.repr_qualid qid with - | dir, id when dir = Nameops.empty_dirpath -> id +let coerce_qualid_to_id (loc,qid) = match repr_qualid qid with + | dir, id when dir = empty_dirpath -> id | _ -> user_err_loc (loc, "Ast.coerce_qualid_to_id", str"This expression should be a simple identifier") @@ -749,3 +741,27 @@ and caselist vars etyp (pl,a) = (AstListPat apl,aa) let to_act_check_vars = act_of_ast + +let rec subst_astpat subst = function + | Pquote a -> Pquote (subst_ast subst a) + | Pmeta _ as p -> p + | Pnode (s,pl) -> Pnode (s,subst_astpatlist subst pl) + | Pslam (ido,p) -> Pslam (ido,subst_astpat subst p) + | Pmeta_slam (s,p) -> Pmeta_slam (s,subst_astpat subst p) + +and subst_astpatlist subst = function + | Pcons (p,pl) -> Pcons (subst_astpat subst p, subst_astpatlist subst pl) + | (Plmeta _ | Pnil) as pl -> pl + +let subst_pat subst = function + | AstListPat pl -> AstListPat (subst_astpatlist subst pl) + | PureAstPat p -> PureAstPat (subst_astpat subst p) + +let rec subst_act subst = function + | Act p -> Act (subst_pat subst p) + | ActCase (a,l) -> + ActCase (subst_act subst a, + List.map (fun (p,a) -> subst_pat subst p, subst_act subst a) l) + | ActCaseList (a,l) -> + ActCaseList (subst_act subst a, + List.map (fun (p,a) -> subst_pat subst p, subst_act subst a) l) diff --git a/parsing/ast.mli b/parsing/ast.mli index 4a9048256..07dbd06f2 100755 --- a/parsing/ast.mli +++ b/parsing/ast.mli @@ -11,6 +11,7 @@ (*i*) open Pp open Names +open Libnames open Coqast open Genarg (*i*) @@ -30,13 +31,13 @@ val nvar : identifier -> Coqast.t val ide : string -> Coqast.t val num : int -> Coqast.t val string : string -> Coqast.t -val path : section_path -> Coqast.t +val path : kernel_name -> Coqast.t val dynamic : Dyn.t -> Coqast.t val set_loc : Coqast.loc -> Coqast.t -> Coqast.t -val path_section : Coqast.loc -> section_path -> Coqast.t -val section_path : section_path -> section_path +val path_section : Coqast.loc -> kernel_name -> Coqast.t +val section_path : kernel_name -> kernel_name (* ast destructors *) val num_of_ast : Coqast.t -> int @@ -100,7 +101,7 @@ val coerce_to_var : Coqast.t -> Coqast.t val coerce_to_id : Coqast.t -> identifier -val coerce_qualid_to_id : Nametab.qualid Util.located -> identifier +val coerce_qualid_to_id : qualid Util.located -> identifier val coerce_reference_to_id : Tacexpr.reference_expr -> identifier @@ -151,3 +152,6 @@ val to_pat : entry_env -> Coqast.t -> (astpat * entry_env) val eval_act : Coqast.loc -> env -> act -> typed_ast val to_act_check_vars : entry_env -> ast_action_type -> grammar_action -> act + +val subst_astpat : Names.substitution -> astpat -> astpat +val subst_act : Names.substitution -> act -> act diff --git a/parsing/astmod.ml b/parsing/astmod.ml new file mode 100644 index 000000000..acf0de62e --- /dev/null +++ b/parsing/astmod.ml @@ -0,0 +1,147 @@ +(***********************************************************************) +(* 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 *) +(***********************************************************************) + +(* $Id$ *) + +open Pp +open Util +open Names +open Entries +open Libnames +open Coqast +open Astterm + +let rec make_mp mp = function + [] -> mp + | h::tl -> make_mp (MPdot(mp, label_of_id h)) tl + +(* +(* Since module components are not put in the nametab we try to locate +the module prefix *) +exception BadRef + +let lookup_qualid (modtype:bool) qid = + let rec make_mp mp = function + [] -> mp + | h::tl -> make_mp (MPdot(mp, label_of_id h)) tl + in + let rec find_module_prefix dir n = + if n<0 then raise Not_found; + let dir',dir'' = list_chop n dir in + let id',dir''' = + match dir'' with + | hd::tl -> hd,tl + | _ -> anomaly "This list should not be empty!" + in + let qid' = make_qualid dir' id' in + try + match Nametab.locate qid' with + | ModRef mp -> mp,dir''' + | _ -> raise BadRef + with + Not_found -> find_module_prefix dir (pred n) + in + try Nametab.locate qid + with Not_found -> + let (dir,id) = repr_qualid qid in + let pref_mp,dir' = find_module_prefix dir (List.length dir - 1) in + let mp = + List.fold_left (fun mp id -> MPdot (mp, label_of_id id)) pref_mp dir' + in + if modtype then + ModTypeRef (make_ln mp (label_of_id id)) + else + ModRef (MPdot (mp,label_of_id id)) + +*) + +(* Search for the head of [qid] in [binders]. + If found, returns the module_path/kernel_name created from the dirpath + and the basename. Searches Nametab otherwise. +*) + +let lookup_module binders qid = + try + let dir,id = repr_qualid qid in + (* dirpath in natural order *) + let idl = List.rev (id::repr_dirpath dir) in + let top_mp = MPbound (fst (List.assoc (List.hd idl) binders)) in + make_mp top_mp (List.tl idl) + with + Not_found -> Nametab.locate_module qid + +let lookup_modtype binders qid = + try + let dir,id = repr_qualid qid in + (* dirpath in natural order *) + match List.rev (repr_dirpath dir) with + | hd::tl -> + let top_mp = MPbound (fst (List.assoc hd binders)) in + let mp = make_mp top_mp tl in + make_kn mp empty_dirpath (label_of_id id) + | [] -> raise Not_found + (* may-be a module, but not a module type!*) + with + Not_found -> Nametab.locate_modtype qid + +let transl_modtype binders = function + | Node(loc,"MODTYPEQID",qid_ast) -> begin match qid_ast with + | [Node (loc, "QUALID", astl)] -> + let qid = interp_qualid astl in begin + try + MTEident (lookup_modtype binders qid) + with + | Not_found -> + Modops.error_not_a_modtype (*loc*) (string_of_qualid qid) + end + | _ -> anomaly "QUALID expected" + end + | _ -> anomaly "TODO: transl_modtype: I can handle qualid module types only" + + +let transl_binder binders (idl,mty_ast) = + let mte = transl_modtype binders mty_ast in + let add_one binders id = + if List.mem_assoc id binders then + error "Two identical module binders..." + else + let mbid = make_mbid (Lib.module_dp()) (string_of_id id) in + (id,(mbid,mte))::binders + in + List.fold_left add_one binders idl + +let transl_binders = List.fold_left transl_binder + + +let rec transl_modexpr binders = function + | Node(loc,"MODEXPRQID",qid_ast) -> begin match qid_ast with + | [Node (loc, "QUALID", astl)] -> + let qid = interp_qualid astl in begin + try + MEident (lookup_module binders qid) + with + | Not_found -> + Modops.error_not_a_module (*loc*) (string_of_qualid qid) + end + | _ -> anomaly "QUALID expected" + end + | Node(_,"MODEXPRAPP",[ast1;ast2]) -> + let me1 = transl_modexpr binders ast1 in + let me2 = transl_modexpr binders ast2 in + MEapply(me1,me2) + | Node(_,"MODEXPRAPP",_) -> + anomaly "transl_modexpr: MODEXPRAPP must have two arguments" + | _ -> anomaly "transl_modexpr: I can handle MODEXPRQID or MODEXPRAPP only..." + + +let interp_module_decl evd env args_ast mty_ast_o mexpr_ast_o = + let binders = transl_binders [] args_ast in + let mty_o = option_app (transl_modtype binders) mty_ast_o in + let mexpr_o = option_app (transl_modexpr binders) mexpr_ast_o in + (List.rev binders, mty_o, mexpr_o) + diff --git a/parsing/astmod.mli b/parsing/astmod.mli new file mode 100644 index 000000000..158f40e89 --- /dev/null +++ b/parsing/astmod.mli @@ -0,0 +1,30 @@ +(***********************************************************************) +(* 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 *) +(***********************************************************************) + +(*i $Id$ i*) + +(*i*) +open Names +open Declarations +open Environ +open Entries +open Evd +(*i*) + +(* Module expressions and module types are interpreted relatively to + eventual functor or funsig arguments. *) + +val interp_module_decl : evar_map -> env -> + (identifier list * Coqast.t) list -> + Coqast.t option -> + Coqast.t option + -> + (identifier * (mod_bound_id * module_type_entry)) list * + module_type_entry option * + module_expr option + diff --git a/parsing/astterm.ml b/parsing/astterm.ml index 0985d309f..89025de4f 100644 --- a/parsing/astterm.ml +++ b/parsing/astterm.ml @@ -19,6 +19,7 @@ open Termops open Environ open Evd open Reductionops +open Libnames open Impargs open Declare open Rawterm @@ -122,7 +123,7 @@ let add_glob loc ref = in let s = string_of_dirpath (find_module dir) in i*) - let sp = Nametab.sp_of_global (Global.env ()) ref in + let sp = Nametab.sp_of_global None ref in let id = let _,id = repr_path sp in string_of_id id in let dp = string_of_dirpath (Declare.library_part ref) in dump_string (Printf.sprintf "R%d %s.%s\n" (fst loc) dp id) @@ -229,14 +230,15 @@ let maybe_constructor allow_var env = function if !dump then add_glob loc (ConstructRef c); ConstrPat (loc,c) - | Path(loc,sp) -> - (match absolute_reference sp with - | ConstructRef c as r -> - if !dump then add_glob loc (ConstructRef c); - ConstrPat (loc,c) - | _ -> - error ("Unknown absolute constructor name: "^(string_of_path sp))) - + | Path(loc,kn) -> + (let dir,id = decode_kn kn in + let sp = make_path dir id in + match absolute_reference sp with + | ConstructRef c as r -> + if !dump then add_glob loc (ConstructRef c); + ConstrPat (loc,c) + | _ -> + error ("Unknown absolute constructor name: "^(string_of_path sp))) | Node(loc,("CONST"|"SECVAR"|"EVAR"|"MUTIND"|"SYNCONST" as key), l) -> user_err_loc (loc,"ast_to_pattern", (str "Found a pattern involving global references which are not constructors" @@ -622,7 +624,7 @@ let ast_of_syndef loc sp = Node (loc, "SYNCONST", [path_section loc sp]) let ast_of_extended_ref_loc loc = function | TrueGlobal ref -> ast_of_ref_loc loc ref - | SyntacticDef sp -> ast_of_syndef loc sp + | SyntacticDef kn -> ast_of_syndef loc kn let ast_of_extended_ref = ast_of_extended_ref_loc dummy_loc diff --git a/parsing/astterm.mli b/parsing/astterm.mli index 3074ff665..3a871cd53 100644 --- a/parsing/astterm.mli +++ b/parsing/astterm.mli @@ -14,6 +14,7 @@ open Term open Sign open Evd open Environ +open Libnames open Rawterm open Pattern (*i*) @@ -25,7 +26,7 @@ val constrIn : constr -> Coqast.t val constrOut : Coqast.t -> constr (* Interprets global names, including syntactic defs and section variables *) -val interp_global_constr : env -> Nametab.qualid Util.located -> constr +val interp_global_constr : env -> qualid Util.located -> constr val interp_rawconstr : evar_map -> env -> Coqast.t -> rawconstr val interp_rawconstr_gen : @@ -81,13 +82,13 @@ val interp_constrpattern : bound idents in grammar or pretty-printing rules) *) val globalize_constr : Coqast.t -> Coqast.t val globalize_ast : Coqast.t -> Coqast.t -val globalize_qualid : Nametab.qualid Util.located -> Coqast.t +val globalize_qualid : qualid Util.located -> Coqast.t -val ast_of_extended_ref_loc : loc -> Nametab.extended_global_reference -> Coqast.t +val ast_of_extended_ref_loc : loc -> Libnames.extended_global_reference -> Coqast.t (* This transforms args of a qualid keyword into a qualified ident *) (* it does no relocation *) -val interp_qualid : Coqast.t list -> Nametab.qualid +val interp_qualid : Coqast.t list -> qualid (*i Translation rules from V6 to V7: diff --git a/parsing/coqast.ml b/parsing/coqast.ml index 9b65bdfb1..e9b9e3c14 100644 --- a/parsing/coqast.ml +++ b/parsing/coqast.ml @@ -10,6 +10,7 @@ (*i*) open Names +open Libnames (*i*) type loc = int * int @@ -23,7 +24,7 @@ type t = | Num of loc * int | Str of loc * string | Id of loc * string - | Path of loc * section_path + | Path of loc * kernel_name | Dynamic of loc * Dyn.t type the_coq_ast = t @@ -62,7 +63,7 @@ module Hast = Hashcons.Make( type u = (the_coq_ast -> the_coq_ast) * ((loc -> loc) * (string -> string) - * (identifier -> identifier) * (section_path -> section_path)) + * (identifier -> identifier) * (kernel_name -> kernel_name)) let hash_sub (hast,(hloc,hstr,hid,hsp)) = function | Node(l,s,al) -> Node(hloc l, hstr s, List.map hast al) | Nmeta(l,s) -> Nmeta(hloc l, hstr s) @@ -98,6 +99,32 @@ let hcons_ast (hstr,hid,hpath) = let hast = Hashcons.recursive_hcons Hast.f (hloc,hstr,hid,hpath) in (hast,hloc) +let rec subst_ast subst ast = match ast with + | Node (l,s,astl) -> + let astl' = Util.list_smartmap (subst_ast subst) astl in + if astl' == astl then ast else + Node (l,s,astl') + | Slam (l,ido,ast1) -> + let ast1' = subst_ast subst ast1 in + if ast1' == ast1 then ast else + Slam (l,ido,ast1') + | Smetalam (l,s,ast1) -> + let ast1' = subst_ast subst ast1 in + if ast1' == ast1 then ast else + Smetalam (l,s,ast1') + | Path (loc,kn) -> + let kn' = Names.subst_kn subst kn in + if kn' == kn then ast else + Path(loc,kn') + | Nmeta _ + | Nvar _ -> ast + | Num _ + | Str _ + | Id _ + | Dynamic _ -> ast + + + (* type 'vernac_ast raw_typed_ast = | PureAstNode of t diff --git a/parsing/coqast.mli b/parsing/coqast.mli index b5ad45c74..a304aa06b 100644 --- a/parsing/coqast.mli +++ b/parsing/coqast.mli @@ -10,6 +10,7 @@ (*i*) open Names +open Libnames (*i*) (* Abstract syntax trees. *) @@ -25,7 +26,7 @@ type t = | Num of loc * int | Str of loc * string | Id of loc * string - | Path of loc * section_path + | Path of loc * kernel_name | Dynamic of loc * Dyn.t (* returns the list of metas occuring in the ast *) @@ -38,9 +39,11 @@ val subst_meta : (int * t) list -> t -> t (* hash-consing function *) val hcons_ast: (string -> string) * (Names.identifier -> Names.identifier) - * (section_path -> section_path) + * (kernel_name -> kernel_name) -> (t -> t) * (loc -> loc) +val subst_ast: Names.substitution -> t -> t + (* val map_tactic_expr : (t -> t) -> (tactic_expr -> tactic_expr) -> tactic_expr -> tactic_expr val fold_tactic_expr : diff --git a/parsing/coqlib.ml b/parsing/coqlib.ml index 07e439af8..52311d188 100644 --- a/parsing/coqlib.ml +++ b/parsing/coqlib.ml @@ -11,6 +11,7 @@ open Util open Names open Term +open Libnames open Declare open Pattern open Nametab @@ -26,6 +27,9 @@ let logic_type_module = make_dir ["Coq";"Init";"Logic_Type"] let datatypes_module = make_dir ["Coq";"Init";"Datatypes"] let arith_module = make_dir ["Coq";"Arith";"Arith"] +(* TODO: temporary hack *) +let make_path dir id = Libnames.encode_kn dir id + let nat_path = make_path datatypes_module (id_of_string "nat") let glob_nat = IndRef (nat_path,0) diff --git a/parsing/coqlib.mli b/parsing/coqlib.mli index 0b5bb0ec5..8eedab050 100644 --- a/parsing/coqlib.mli +++ b/parsing/coqlib.mli @@ -10,6 +10,7 @@ (*i*) open Names +open Libnames open Nametab open Term open Pattern @@ -21,8 +22,8 @@ open Pattern (*s Global references *) (* Modules *) -val logic_module : Names.dir_path -val logic_type_module : Names.dir_path +val logic_module : dir_path +val logic_type_module : dir_path (* Natural numbers *) val glob_nat : global_reference diff --git a/parsing/egrammar.ml b/parsing/egrammar.ml index 97cfd77b1..d665ad575 100644 --- a/parsing/egrammar.ml +++ b/parsing/egrammar.ml @@ -24,6 +24,10 @@ type all_grammar_command = (string * (string * grammar_production list) * Tacexpr.raw_tactic_expr) list +let subst_all_grammar_command subst = function + | AstGrammar gc -> AstGrammar (subst_grammar_command subst gc) + | TacticGrammar g -> TacticGrammar g (* TODO ... *) + let (grammar_state : all_grammar_command list ref) = ref [] (* Interpretation of the right hand side of grammar rules *) diff --git a/parsing/egrammar.mli b/parsing/egrammar.mli index e7d2cde12..9f9e34846 100644 --- a/parsing/egrammar.mli +++ b/parsing/egrammar.mli @@ -38,3 +38,6 @@ val extend_tactic_grammar : val extend_vernac_command_grammar : string -> (string * grammar_tactic_production list) list -> unit + +val subst_all_grammar_command : + Names.substitution -> all_grammar_command -> all_grammar_command diff --git a/parsing/esyntax.ml b/parsing/esyntax.ml index 608868ca6..b3d027802 100644 --- a/parsing/esyntax.ml +++ b/parsing/esyntax.ml @@ -10,6 +10,8 @@ open Pp open Util +open Names +open Libnames open Coqast open Ast open Extend @@ -195,14 +197,14 @@ let make_hunks (lp,rp) s e1 e2 = let build_syntax (ref,e1,e2,assoc) = let sp = match ref with - | TrueGlobal r -> Nametab.sp_of_global (Global.env()) r - | SyntacticDef sp -> sp in + | TrueGlobal r -> Nametab.sp_of_global None r + | SyntacticDef kn -> Nametab.sp_of_syntactic_definition kn in let rec find_symbol = function | [] -> let s = match ref with | TrueGlobal r -> - string_of_qualid (shortest_qualid_of_global (Global.env()) r) - | SyntacticDef sp -> string_of_path sp in + string_of_qualid (shortest_qualid_of_global None r) + | SyntacticDef _ -> string_of_path sp in UNP_BOX (PpHOVB 0, [RO "("; RO s; UNP_BRK (1, 1); PH (meta_pattern e1, None, E); UNP_BRK (1, 1); PH (meta_pattern e2, None, E); RO ")"]) diff --git a/parsing/esyntax.mli b/parsing/esyntax.mli index 5ddadb5bc..8e3445ed7 100644 --- a/parsing/esyntax.mli +++ b/parsing/esyntax.mli @@ -42,7 +42,7 @@ module Ppprim : val add : string * t -> unit end -val declare_infix_symbol : Names.section_path -> string -> unit +val declare_infix_symbol : Libnames.section_path -> string -> unit (* Generic printing functions *) val token_printer: std_printer -> std_printer diff --git a/parsing/extend.ml b/parsing/extend.ml index bc4ad211b..7c4c400eb 100644 --- a/parsing/extend.ml +++ b/parsing/extend.ml @@ -50,6 +50,16 @@ type raw_grammar_rule = string * grammar_production list * grammar_action type raw_grammar_entry = string * ast_action_type * grammar_associativity * raw_grammar_rule list +let subst_grammar_rule subst gr = + { gr with gr_action = subst_act subst gr.gr_action } + +let subst_grammar_entry subst ge = + { ge with gl_rules = List.map (subst_grammar_rule subst) ge.gl_rules } + +let subst_grammar_command subst gc = + { gc with gc_entries = List.map (subst_grammar_entry subst) gc.gc_entries } + + (*s Terminal symbols interpretation *) let is_ident_not_keyword s = @@ -177,9 +187,28 @@ type 'pat unparsing_hunk = | UNP_TBRK of int * int | UNP_TAB | UNP_FNL - | UNP_INFIX of Nametab.extended_global_reference * string * string * + | UNP_INFIX of Libnames.extended_global_reference * string * string * (parenRelation * parenRelation) +let rec subst_hunk subst_pat subst hunk = match hunk with + | PH (pat,so,pr) -> + let pat' = subst_pat subst pat in + if pat'==pat then hunk else + PH (pat',so,pr) + | RO _ -> hunk + | UNP_BOX (ppbox, hunkl) -> + let hunkl' = list_smartmap (subst_hunk subst_pat subst) hunkl in + if hunkl' == hunkl then hunk else + UNP_BOX (ppbox, hunkl') + | UNP_BRK _ + | UNP_TBRK _ + | UNP_TAB + | UNP_FNL -> hunk + | UNP_INFIX (ref,s1,s2,prs) -> + let ref' = Libnames.subst_ext subst ref in + if ref' == ref then hunk else + UNP_INFIX (ref',s1,s2,prs) + (* Checks if the precedence of the parent printer (None means the highest precedence), and the child's one, follow the given relation. *) @@ -213,10 +242,29 @@ type 'pat syntax_entry = { syn_astpat : 'pat; syn_hunks : 'pat unparsing_hunk list } +let subst_syntax_entry subst_pat subst sentry = + let syn_astpat' = subst_pat subst sentry.syn_astpat in + let syn_hunks' = list_smartmap (subst_hunk subst_pat subst) sentry.syn_hunks + in + if syn_astpat' == sentry.syn_astpat + && syn_hunks' == sentry.syn_hunks then sentry + else + { sentry with + syn_astpat = syn_astpat' ; + syn_hunks = syn_hunks' ; + } + type 'pat syntax_command = { sc_univ : string; sc_entries : 'pat syntax_entry list } +let subst_syntax_command subst_pat subst scomm = + let sc_entries' = + list_smartmap (subst_syntax_entry subst_pat subst) scomm.sc_entries + in + if sc_entries' == scomm.sc_entries then scomm else + { scomm with sc_entries = sc_entries' } + type syntax_rule = string * Coqast.t * Coqast.t unparsing_hunk list type syntax_entry_ast = precedence * syntax_rule list diff --git a/parsing/extend.mli b/parsing/extend.mli index e80f011d3..8734e3452 100644 --- a/parsing/extend.mli +++ b/parsing/extend.mli @@ -1,3 +1,15 @@ +(***********************************************************************) +(* 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 *) +(***********************************************************************) + +(*i $Id$ i*) + +(*i*) + open Pp open Ast open Coqast @@ -42,6 +54,9 @@ val terminal : string -> string * string val rename_command : string -> string +val subst_grammar_command : + Names.substitution -> grammar_command -> grammar_command + (*s Pretty-print. *) (* Dealing with precedences *) @@ -67,9 +82,14 @@ type 'pat unparsing_hunk = | UNP_TBRK of int * int | UNP_TAB | UNP_FNL - | UNP_INFIX of Nametab.extended_global_reference * string * string * + | UNP_INFIX of Libnames.extended_global_reference * string * string * (parenRelation * parenRelation) +(*val subst_unparsing_hunk : + Names.substitution -> (Names.substitution -> 'pat -> 'pat) -> + 'pat unparsing_hunk -> 'pat unparsing_hunk +*) + (* Checks if the precedence of the parent printer (None means the highest precedence), and the child's one, follow the given relation. *) @@ -86,10 +106,19 @@ type 'pat syntax_entry = { syn_astpat : 'pat; syn_hunks : 'pat unparsing_hunk list } +val subst_syntax_entry : + (Names.substitution -> 'pat -> 'pat) -> + Names.substitution -> 'pat syntax_entry -> 'pat syntax_entry + + type 'pat syntax_command = { sc_univ : string; sc_entries : 'pat syntax_entry list } +val subst_syntax_command : + (Names.substitution -> 'pat -> 'pat) -> + Names.substitution -> 'pat syntax_command -> 'pat syntax_command + type syntax_rule = string * Coqast.t * Coqast.t unparsing_hunk list type syntax_entry_ast = precedence * syntax_rule list diff --git a/parsing/g_module.ml4 b/parsing/g_module.ml4 new file mode 100644 index 000000000..01e7256ef --- /dev/null +++ b/parsing/g_module.ml4 @@ -0,0 +1,81 @@ +(***********************************************************************) +(* 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 *) +(***********************************************************************) + +(*i camlp4deps: "parsing/grammar.cma" i*) + +(* $Id$ *) + +open Pp +open Ast +open Pcoq +open Prim +open Module +open Util + +(* Grammar rules for module expressions and types *) + +GEXTEND Gram + GLOBAL: ne_binders_list module_expr + module_type; + + ident: + [ [ id = Prim.var -> id ] ] + ; + + ident_comma_list_tail: + [ [ ","; idl = LIST0 ident SEP "," -> idl + | -> [] ] ] + ; + + qualid: + [ [ id = Prim.var; l = fields -> <:ast< (QUALID $id ($LIST $l)) >> + | id = Prim.var -> <:ast< (QUALID $id) >> + ] ] + ; + fields: + [ [ id = FIELD; l = fields -> <:ast< ($VAR $id) >> :: l + | id = FIELD -> [ <:ast< ($VAR $id) >> ] + ] ] + ; + + vardecls: (* This is interpreted by Pcoq.abstract_binder *) + [ [ id = ident; idl = ident_comma_list_tail; + ":"; mty = module_type -> + <:ast< (BINDER $mty $id ($LIST $idl)) >> ] ] + ; + + ne_vardecls_list: + [ [ id = vardecls; ";"; idl = ne_vardecls_list -> id :: idl + | id = vardecls -> [id] ] ] + ; + + rawbinders: + [ [ "["; bl = ne_vardecls_list; "]" -> bl ] ] + ; + + ne_binders_list: + [ [ bl = rawbinders; bll = ne_binders_list -> bl @ bll + | bl = rawbinders -> bl ] ] + ; + + module_expr: + [ [ qid = qualid -> <:ast< (MODEXPRQID $qid) >> + | me1 = module_expr; me2 = module_expr -> + <:ast< (MODEXPRAPP $me1 $me2) >> + | "("; me = module_expr; ")" -> + me +(* ... *) + ] ] + ; + + module_type: + [ [ qid = qualid -> <:ast< (MODTYPEQID $qid) >> +(* ... *) + ] ] + ; +END diff --git a/parsing/g_prim.ml4 b/parsing/g_prim.ml4 index 51696ad03..d279499ab 100644 --- a/parsing/g_prim.ml4 +++ b/parsing/g_prim.ml4 @@ -15,6 +15,7 @@ camlp4o pa_ifdef.cmo pa_extend.cmo pr_o.cmo pr_extend.cmo -quotify -DQuotify -im open Coqast open Pcoq open Names +open Libnames ifdef Quotify then open Qast @@ -26,7 +27,7 @@ open Prim ifdef Quotify then module Prelude = struct let local_id_of_string s = Apply ("Names","id_of_string", [s]) -let local_make_dirpath l = Qast.Apply ("Nametab","make_dirpath",[l]) +let local_make_dirpath l = Qast.Apply ("Names","make_dirpath",[l]) let local_make_posint s = s let local_make_negint s = Apply ("Pervasives","~-", [s]) let local_make_qualid l id' = @@ -34,7 +35,7 @@ let local_make_qualid l id' = let local_make_short_qualid id = Qast.Apply ("Nametab","make_short_qualid",[id]) let local_make_path l id' = - Qast.Apply ("Names","make_path", [local_make_dirpath l;id']) + Qast.Apply ("Libnames","encode_kn", [local_make_dirpath l;id']) let local_make_binding loc a b = match a with | Qast.Node ("Nvar", [_;id]) -> @@ -56,7 +57,7 @@ let local_make_qualid l id' = make_qualid (local_make_dirpath l) id' let local_make_short_qualid id = make_short_qualid id let local_make_posint = int_of_string let local_make_negint n = - int_of_string n -let local_make_path l a = make_path (local_make_dirpath l) a +let local_make_path l a = encode_kn (local_make_dirpath l) a let local_make_binding loc a b = match a with | Nvar (_,id) -> Slam(loc,Some id,b) diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index 243f72bf1..c9a0d69c7 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -297,10 +297,46 @@ ident_comma_list_tail: [ [ (* Sections *) IDENT "Section"; id = ident -> VernacBeginSection id - | IDENT "Chapter"; id = ident -> VernacBeginSection id - | IDENT "Module"; id = ident -> - warning "Module is currently unsupported"; VernacNop - | IDENT "End"; id = ident -> VernacEndSection id + | IDENT "Chapter"; id = ident -> VernacBeginSection id ] ] +(* | IDENT "Module"; id = ident -> + warning "Module is currently unsupported"; VernacNop *) + ; + + module_vardecls: (* This is interpreted by Pcoq.abstract_binder *) + [ [ id = ident; idl = ident_comma_list_tail; + ":"; mty = Module.module_type -> + (id::idl,mty) ] ] + ; + module_binders: + [ [ "["; bl = LIST1 module_vardecls SEP ";"; "]" -> bl ] ] + ; + module_binders_list: + [ [ bls = LIST0 module_binders -> List.flatten bls ] ] + ; + of_module_type: + [ [ ":"; mty = Module.module_type -> mty ] ] + ; + is_module_type: + [ [ ":="; mty = Module.module_type -> mty ] ] + ; + is_module_expr: + [ [ ":="; mexpr = Module.module_expr -> mexpr ] ] + ; + gallina_ext: + [ [ + (* Interactive module declaration *) + IDENT "Module"; id = ident; bl = module_binders_list; + mty_o = OPT of_module_type; mexpr_o = OPT is_module_expr -> + VernacDeclareModule id bl mty_o mexpr_o + + | IDENT "Module"; "Type"; id = ident; + bl = module_binders_list; mty_o = OPT is_module_type -> + VernacDeclareModuleType id bl mty_o + + (* This end a Section a Module or a Module Type *) + + | IDENT "End"; id = ident -> VernacEndSegment id + (* Transparent and Opaque *) | IDENT "Transparent"; l = LIST1 qualid -> VernacSetOpacity (false, l) @@ -333,13 +369,13 @@ ident_comma_list_tail: VernacIdentityCoercion (Declare.make_strength_0 (), f, s, t) | IDENT "Identity"; IDENT "Coercion"; f = Prim.ident; ":"; s = class_rawexpr; ">->"; t = class_rawexpr -> - VernacIdentityCoercion (Nametab.NeverDischarge, f, s, t) + VernacIdentityCoercion (Libnames.NeverDischarge, f, s, t) | IDENT "Coercion"; IDENT "Local"; qid = qualid; ":"; s = class_rawexpr; ">->"; t = class_rawexpr -> VernacCoercion (Declare.make_strength_0 (), qid, s, t) | IDENT "Coercion"; qid = qualid; ":"; s = class_rawexpr; ">->"; t = class_rawexpr -> - VernacCoercion (Nametab.NeverDischarge, qid, s, t) + VernacCoercion (Libnames.NeverDischarge, qid, s, t) | IDENT "Class"; IDENT "Local"; c = qualid -> Pp.warning "Class is obsolete"; VernacNop | IDENT "Class"; c = qualid -> diff --git a/parsing/genarg.mli b/parsing/genarg.mli index 70e67330e..2991d237a 100644 --- a/parsing/genarg.mli +++ b/parsing/genarg.mli @@ -11,7 +11,7 @@ open Util open Names open Term -open Nametab +open Libnames open Rawterm type 'a or_var = ArgArg of 'a | ArgVar of loc * identifier @@ -82,7 +82,7 @@ val rawwit_pre_ident : (string,'co,'ta) abstract_argument_type val wit_pre_ident : (string,'co,'ta) abstract_argument_type val rawwit_qualid : (qualid located,constr_ast,'ta) abstract_argument_type -val wit_qualid : (Nametab.global_reference,constr,'ta) abstract_argument_type +val wit_qualid : (global_reference,constr,'ta) abstract_argument_type val rawwit_quant_hyp : (quantified_hypothesis,'co,'ta) abstract_argument_type val wit_quant_hyp : (quantified_hypothesis,'co,'ta) abstract_argument_type @@ -99,7 +99,7 @@ val wit_casted_open_constr : (open_constr,constr,'ta) abstract_argument_type val rawwit_constr_with_bindings : (constr_ast with_bindings,constr_ast,'ta) abstract_argument_type val wit_constr_with_bindings : (constr with_bindings,constr,'ta) abstract_argument_type -val rawwit_red_expr : ((constr_ast,Nametab.qualid or_metanum) red_expr_gen,constr_ast,'ta) abstract_argument_type +val rawwit_red_expr : ((constr_ast,qualid or_metanum) red_expr_gen,constr_ast,'ta) abstract_argument_type val wit_red_expr : ((constr,Closure.evaluable_global_reference) red_expr_gen,constr,'ta) abstract_argument_type (* TODO: transformer tactic en extra arg *) diff --git a/parsing/pcoq.ml4 b/parsing/pcoq.ml4 index d26613b10..2d444fcbb 100644 --- a/parsing/pcoq.ml4 +++ b/parsing/pcoq.ml4 @@ -222,6 +222,7 @@ let create_univ s = let uprim = create_univ "prim" let uconstr = create_univ "constr" +let umodule = create_univ "module" let utactic = create_univ "tactic" let uvernac = create_univ "vernac" @@ -398,6 +399,18 @@ module Constr = end +module Module = + struct + let gec = make_entry umodule inPureAstType + let gec_list = make_entry umodule inAstListType + + let ident = gec "ident" + let qualid = gec_list "qualid" + let ne_binders_list = gec_list "ne_binders_list" + let module_expr = gec "module_expr" + let module_type = gec "module_type" + end + module Tactic = struct let gec = make_entry utactic inPureAstType diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli index 61e2f9771..628f4035e 100644 --- a/parsing/pcoq.mli +++ b/parsing/pcoq.mli @@ -102,7 +102,7 @@ module Prim : sig open Util open Names - open Nametab + open Libnames val preident : string Gram.Entry.e val ident : identifier Gram.Entry.e val rawident : identifier located Gram.Entry.e @@ -150,6 +150,13 @@ module Constr : val ne_binders_list : Coqast.t list Gram.Entry.e end +module Module : + sig + val ne_binders_list : Coqast.t list Gram.Entry.e + val module_expr : Coqast.t Gram.Entry.e + val module_type : Coqast.t Gram.Entry.e + end + module Tactic : sig open Rawterm @@ -168,7 +175,7 @@ module Tactic : module Vernac_ : sig open Util - open Nametab + open Libnames val thm_token : theorem_kind Gram.Entry.e val class_rawexpr : class_rawexpr Gram.Entry.e val gallina : vernac_expr Gram.Entry.e diff --git a/parsing/ppconstr.ml b/parsing/ppconstr.ml index ad120fe19..fbee5ff27 100644 --- a/parsing/ppconstr.ml +++ b/parsing/ppconstr.ml @@ -16,33 +16,34 @@ open Pp open Nametab open Names open Nameops +open Libnames open Coqast open Extend open Util let dfltpr ast = (str"#GENTERM " ++ print_ast ast);; -let pr_global ref = pr_global_env (Global.env()) ref +let pr_global ref = pr_global_env None ref -let global_const_name sp = - try pr_global (ConstRef sp) +let global_const_name kn = + try pr_global (ConstRef kn) with Not_found -> (* May happen in debug *) - (str ("CONST("^(string_of_path sp)^")")) + (str ("CONST("^(string_of_kn kn)^")")) let global_var_name id = try pr_global (VarRef id) with Not_found -> (* May happen in debug *) (str ("SECVAR("^(string_of_id id)^")")) -let global_ind_name (sp,tyi) = - try pr_global (IndRef (sp,tyi)) +let global_ind_name (kn,tyi) = + try pr_global (IndRef (kn,tyi)) with Not_found -> (* May happen in debug *) - (str ("IND("^(string_of_path sp)^","^(string_of_int tyi)^")")) + (str ("IND("^(string_of_kn kn)^","^(string_of_int tyi)^")")) -let global_constr_name ((sp,tyi),i) = - try pr_global (ConstructRef ((sp,tyi),i)) +let global_constr_name ((kn,tyi),i) = + try pr_global (ConstructRef ((kn,tyi),i)) with Not_found -> (* May happen in debug *) - (str ("CONSTRUCT("^(string_of_path sp)^","^(string_of_int tyi) + (str ("CONSTRUCT("^(string_of_kn kn)^","^(string_of_int tyi) ^","^(string_of_int i)^")")) let globpr gt = match gt with @@ -89,7 +90,7 @@ let pr_constr = gentermpr let pr_pattern = gentermpr -let pr_qualid qid = str (Nametab.string_of_qualid qid) +let pr_qualid qid = str (string_of_qualid qid) open Rawterm diff --git a/parsing/ppconstr.mli b/parsing/ppconstr.mli index d9b8b6ea5..04225ef7a 100644 --- a/parsing/ppconstr.mli +++ b/parsing/ppconstr.mli @@ -14,7 +14,7 @@ open Pp open Environ open Term -open Nametab +open Libnames open Pcoq open Rawterm open Extend diff --git a/parsing/pptactic.ml b/parsing/pptactic.ml index 80cdf953b..8fa2326c4 100644 --- a/parsing/pptactic.ml +++ b/parsing/pptactic.ml @@ -245,9 +245,9 @@ open Closure let pr_evaluable_reference = function | EvalVarRef id -> pr_id id - | EvalConstRef sp -> pr_global (Nametab.ConstRef sp) + | EvalConstRef sp -> pr_global (Libnames.ConstRef sp) -let pr_inductive ind = pr_global (Nametab.IndRef ind) +let pr_inductive ind = pr_global (Libnames.IndRef ind) let rec pr_generic prtac x = match Genarg.genarg_tag x with diff --git a/parsing/prettyp.ml b/parsing/prettyp.ml index c7da75c36..6554659f3 100644 --- a/parsing/prettyp.ml +++ b/parsing/prettyp.ml @@ -25,6 +25,7 @@ open Declare open Impargs open Libobject open Printer +open Libnames open Nametab let print_basename sp = pr_global (ConstRef sp) @@ -291,20 +292,20 @@ let print_constant with_values sep sp = let print_inductive sp = (print_mutual sp ++ fnl ()) -let print_syntactic_def sep sp = - let id = basename sp in - let c = Syntax_def.search_syntactic_definition sp in - (str" Syntactic Definition " ++ pr_id id ++ str sep ++ pr_rawterm c ++ fnl ()) +let print_syntactic_def sep kn = + let _,_,l = repr_kn kn in + let c = Syntax_def.search_syntactic_definition kn in + (str" Syntactic Definition " ++ pr_lab l ++ str sep ++ pr_rawterm c ++ fnl ()) -let print_leaf_entry with_values sep (sp,lobj) = +let print_leaf_entry with_values sep ((sp,kn as oname),lobj) = let tag = object_tag lobj in - match (sp,tag) with + match (oname,tag) with | (_,"VARIABLE") -> print_section_variable (basename sp) | (_,("CONSTANT"|"PARAMETER")) -> - print_constant with_values sep sp + print_constant with_values sep kn | (_,"INDUCTIVE") -> - print_inductive sp + print_inductive kn | (_,"AUTOHINT") -> (* (str" Hint Marker" ++ fnl ())*) (mt ()) @@ -312,7 +313,7 @@ let print_leaf_entry with_values sep (sp,lobj) = (* (str" Grammar Marker" ++ fnl ())*) (mt ()) | (_,"SYNTAXCONSTANT") -> - print_syntactic_def sep sp + print_syntactic_def sep kn | (_,"PPSYNTAX") -> (* (str" Syntax Marker" ++ fnl ())*) (mt ()) @@ -340,15 +341,20 @@ let print_leaf_entry with_values sep (sp,lobj) = let rec print_library_entry with_values ent = let sep = if with_values then " = " else " : " in + let pr_name (sp,_) = pr_id (basename sp) in match ent with - | (sp,Lib.Leaf lobj) -> - (print_leaf_entry with_values sep (sp,lobj)) - | (sp,Lib.OpenedSection (dir,_)) -> - (str " >>>>>>> Section " ++ pr_id (basename sp) ++ fnl ()) - | (sp,Lib.ClosedSection _) -> - (str " >>>>>>> Closed Section " ++ pr_id (basename sp) ++ fnl ()) - | (_,Lib.Module dir) -> - (str " >>>>>>> Module " ++ pr_dirpath dir ++ fnl ()) + | (oname,Lib.Leaf lobj) -> + (print_leaf_entry with_values sep (oname,lobj)) + | (oname,Lib.OpenedSection (dir,_)) -> + (str " >>>>>>> Section " ++ pr_name oname ++ fnl ()) + | (oname,Lib.ClosedSection _) -> + (str " >>>>>>> Closed Section " ++ pr_name oname ++ fnl ()) + | (_,Lib.CompilingModule (dir,_)) -> + (str " >>>>>>> Library " ++ pr_dirpath dir ++ fnl ()) + | (oname,Lib.OpenedModule _) -> + (str " >>>>>>> Module " ++ pr_name oname ++ fnl ()) + | (oname,Lib.OpenedModtype _) -> + (str " >>>>>>> Module Type " ++ pr_name oname ++ fnl ()) | (_,Lib.FrozenState _) -> (mt ()) @@ -385,9 +391,9 @@ let read_sec_context (loc,qid) = with Not_found -> user_err_loc (loc,"read_sec_context", str "Unknown section") in let rec get_cxt in_cxt = function - | ((sp,Lib.OpenedSection (dir',_)) as hd)::rest -> + | ((_,Lib.OpenedSection ((dir',_),_)) as hd)::rest -> if dir = dir' then (hd::in_cxt) else get_cxt (hd::in_cxt) rest - | ((sp,Lib.ClosedSection (_,_,ctxt)) as hd)::rest -> + | ((_,Lib.ClosedSection (_,_,ctxt)) as hd)::rest -> error "Cannot print the contents of a closed section" | [] -> [] | hd::rest -> get_cxt (hd::in_cxt) rest @@ -414,15 +420,15 @@ let print_eval red_fun env {uj_val=trm;uj_type=typ} = let print_name (loc,qid) = try let sp = Nametab.locate_obj qid in - let (sp,lobj) = - let (sp,entry) = - List.find (fun en -> (fst en) = sp) (Lib.contents_after None) + let (oname,lobj) = + let (oname,entry) = + List.find (fun en -> (fst (fst en)) = sp) (Lib.contents_after None) in match entry with - | Lib.Leaf obj -> (sp,obj) + | Lib.Leaf obj -> (oname,obj) | _ -> raise Not_found in - print_leaf_entry true " = " (sp,lobj) + print_leaf_entry true " = " (oname,lobj) with Not_found -> try match Nametab.locate qid with @@ -438,8 +444,8 @@ let print_name (loc,qid) = (print_named_decl (str,c,typ)) with Not_found -> try - let sp = Syntax_def.locate_syntactic_definition qid in - print_syntactic_def " = " sp + let kn = Nametab.locate_syntactic_definition qid in + print_syntactic_def " = " kn with Not_found -> user_err_loc (loc,"print_name",pr_qualid qid ++ spc () ++ str "not a defined object") @@ -468,9 +474,9 @@ let print_local_context () = let env = Lib.contents_after None in let rec print_var_rec = function | [] -> (mt ()) - | (sp,Lib.Leaf lobj)::rest -> + | (oname,Lib.Leaf lobj)::rest -> if "VARIABLE" = object_tag lobj then - let (d,_) = get_variable (basename sp) in + let (d,_) = get_variable (basename (fst oname)) in (print_var_rec rest ++ print_named_decl d) else @@ -478,16 +484,18 @@ let print_local_context () = | _::rest -> print_var_rec rest and print_last_const = function - | (sp,Lib.Leaf lobj)::rest -> + | (oname,Lib.Leaf lobj)::rest -> (match object_tag lobj with | "CONSTANT" | "PARAMETER" -> + let kn = snd oname in let {const_body=val_0;const_type=typ} = - Global.lookup_constant sp in - (print_last_const rest ++ - print_basename sp ++str" = " ++ + Global.lookup_constant kn in + (print_last_const rest ++ + print_basename kn ++str" = " ++ print_typed_body (val_0,typ)) | "INDUCTIVE" -> - (print_last_const rest ++print_mutual sp ++ fnl ()) + let kn = snd oname in + (print_last_const rest ++print_mutual kn ++ fnl ()) | "VARIABLE" -> (mt ()) | _ -> print_last_const rest) | _ -> (mt ()) diff --git a/parsing/prettyp.mli b/parsing/prettyp.mli index 4a65492ae..4f3c1269e 100644 --- a/parsing/prettyp.mli +++ b/parsing/prettyp.mli @@ -16,6 +16,7 @@ open Sign open Term open Environ open Reductionops +open Libnames open Nametab (*i*) @@ -26,21 +27,21 @@ val assumptions_for_print : name list -> Termops.names_context val print_closed_sections : bool ref val print_impl_args : int list -> std_ppcmds val print_context : bool -> Lib.library_segment -> std_ppcmds -val print_library_entry : bool -> (section_path * Lib.node) -> std_ppcmds +val print_library_entry : bool -> (object_name * Lib.node) -> std_ppcmds val print_full_context : unit -> std_ppcmds val print_full_context_typ : unit -> std_ppcmds -val print_sec_context : Nametab.qualid located -> std_ppcmds -val print_sec_context_typ : Nametab.qualid located -> std_ppcmds +val print_sec_context : qualid located -> std_ppcmds +val print_sec_context_typ : qualid located -> std_ppcmds val print_judgment : env -> unsafe_judgment -> std_ppcmds val print_safe_judgment : env -> Safe_typing.judgment -> std_ppcmds val print_eval : reduction_function -> env -> unsafe_judgment -> std_ppcmds (* This function is exported for the graphical user-interface pcoq *) -val build_inductive : section_path -> int -> +val build_inductive : mutual_inductive -> int -> global_reference * rel_context * types * identifier array * types array -val print_mutual : section_path -> std_ppcmds -val print_name : Nametab.qualid located -> std_ppcmds -val print_opaque_name : Nametab.qualid located -> std_ppcmds +val print_mutual : mutual_inductive -> std_ppcmds +val print_name : qualid located -> std_ppcmds +val print_opaque_name : qualid located -> std_ppcmds val print_local_context : unit -> std_ppcmds (*i diff --git a/parsing/printer.ml b/parsing/printer.ml index a3ce32047..5867d8143 100644 --- a/parsing/printer.ml +++ b/parsing/printer.ml @@ -21,6 +21,7 @@ open Declare open Coqast open Ast open Termast +open Libnames open Extend open Nametab open Ppconstr diff --git a/parsing/printer.mli b/parsing/printer.mli index 17b6341fd..48ee955cc 100644 --- a/parsing/printer.mli +++ b/parsing/printer.mli @@ -11,6 +11,7 @@ (*i*) open Pp open Names +open Libnames open Term open Sign open Environ diff --git a/parsing/q_coqast.ml4 b/parsing/q_coqast.ml4 index debe3ba93..6b7eb89a3 100644 --- a/parsing/q_coqast.ml4 +++ b/parsing/q_coqast.ml4 @@ -8,6 +8,8 @@ (* $Id$ *) +open Names +open Libnames open Q_util let dummy_loc = (0,0) @@ -71,13 +73,13 @@ let rec mlexpr_of_ast = function | Coqast.Num loc i -> <:expr< Coqast.Num loc $int:string_of_int i$ >> | Coqast.Id loc id -> <:expr< Coqast.Id loc $str:id$ >> | Coqast.Str loc str -> <:expr< Coqast.Str loc $str:str$ >> - | Coqast.Path loc qid -> - let l,a = Names.repr_path qid in + | Coqast.Path loc kn -> + let l,a = Libnames.decode_kn kn in let mlexpr_of_modid id = - <:expr< Names.id_of_string $str:Names.string_of_id id$ >> in - let e = List.map mlexpr_of_modid (Names.repr_dirpath l) in + <:expr< Names.id_of_string $str:string_of_id id$ >> in + let e = List.map mlexpr_of_modid (repr_dirpath l) in let e = expr_list_of_var_list e in - <:expr< Coqast.Path loc (Names.make_path (Names.make_dirpath $e$) + <:expr< Coqast.Path loc (Libnames.encode_kn (Names.make_dirpath $e$) (Names.id_of_string $str:Names.string_of_id a$)) >> | Coqast.Dynamic _ _ -> failwith "Q_Coqast: dynamic: not implemented" @@ -121,8 +123,8 @@ let mlexpr_of_dirpath dir = <:expr< Names.make_dirpath $mlexpr_of_list mlexpr_of_ident l$ >> let mlexpr_of_qualid qid = - let (dir, id) = Nametab.repr_qualid qid in - <:expr< Nametab.make_qualid $mlexpr_of_dirpath dir$ $mlexpr_of_ident id$ >> + let (dir, id) = repr_qualid qid in + <:expr< make_qualid $mlexpr_of_dirpath dir$ $mlexpr_of_ident id$ >> let mlexpr_of_reference = function | Tacexpr.RQualid (loc,qid) -> <:expr< Tacexpr.RQualid loc $mlexpr_of_qualid qid$ >> diff --git a/parsing/search.ml b/parsing/search.ml index 1d5619969..78e549e13 100644 --- a/parsing/search.ml +++ b/parsing/search.ml @@ -22,6 +22,7 @@ open Astterm open Environ open Pattern open Printer +open Libnames open Nametab (* The functions print_constructors and crible implement the behavior needed @@ -49,9 +50,9 @@ let rec head_const c = match kind_of_term c with let crible (fn : global_reference -> env -> constr -> unit) ref = let env = Global.env () in - let imported = Library.opened_modules() in + let imported = Library.opened_libraries() in let const = constr_of_reference ref in - let crible_rec sp lobj = + let crible_rec (sp,_) lobj = match object_tag lobj with | "VARIABLE" -> (try @@ -60,26 +61,28 @@ let crible (fn : global_reference -> env -> constr -> unit) ref = with Not_found -> (* we are in a section *) ()) | "CONSTANT" | "PARAMETER" -> - let {const_type=typ} = Global.lookup_constant sp in - if (head_const typ) = const then fn (ConstRef sp) env typ + let kn=locate_constant (qualid_of_sp sp) in + let {const_type=typ} = Global.lookup_constant kn in + if (head_const typ) = const then fn (ConstRef kn) env typ | "INDUCTIVE" -> - let mib = Global.lookup_mind sp in - let arities = + let kn=locate_mind (qualid_of_sp sp) in + let mib = Global.lookup_mind kn in +(* let arities = array_map_to_list (fun mip -> (Name mip.mind_typename, None, mip.mind_nf_arity)) - mib.mind_packets in + mib.mind_packets in*) (match kind_of_term const with - | Ind ((sp',tyi) as indsp) -> - if sp=sp' then - print_constructors indsp fn env mib.mind_packets.(tyi) + | Ind ((kn',tyi) as ind) -> + if kn=kn' then + print_constructors ind fn env mib.mind_packets.(tyi) | _ -> ()) | _ -> () in - try - Library.iter_all_segments false crible_rec - with Not_found -> - errorlabstrm "search" + try + Declaremods.iter_all_segments false crible_rec + with Not_found -> + errorlabstrm "search" (pr_global ref ++ spc () ++ str "not declared") (* Fine Search. By Yves Bertot. *) @@ -104,9 +107,9 @@ let plain_display ref a c = msg (hov 2 (pr ++ str":" ++ spc () ++ pc) ++ fnl ()) let filter_by_module (module_list:dir_path list) (accept:bool) - (ref:global_reference) (env:env) _ = + (ref:global_reference) _ _ = try - let sp = sp_of_global env ref in + let sp = sp_of_global None ref in let sl = dirpath sp in let rec filter_aux = function | m :: tl -> (not (is_dirpath_prefix_of m sl)) && (filter_aux tl) @@ -117,9 +120,9 @@ let filter_by_module (module_list:dir_path list) (accept:bool) false let gref_eq = - IndRef (make_path Coqlib.logic_module (id_of_string "eq"), 0) + IndRef (Libnames.encode_kn Coqlib.logic_module (id_of_string "eq"), 0) let gref_eqT = - IndRef (make_path Coqlib.logic_type_module (id_of_string "eqT"), 0) + IndRef (Libnames.encode_kn Coqlib.logic_type_module (id_of_string "eqT"), 0) let mk_rewrite_pattern1 eq pattern = PApp (PRef eq, [| PMeta None; pattern; PMeta None |]) diff --git a/parsing/search.mli b/parsing/search.mli index 111858733..d1f6bccd4 100644 --- a/parsing/search.mli +++ b/parsing/search.mli @@ -13,6 +13,7 @@ open Names open Term open Environ open Pattern +open Libnames open Nametab (*s Search facilities. *) diff --git a/parsing/termast.ml b/parsing/termast.ml index 95e4b5163..d30e03903 100644 --- a/parsing/termast.ml +++ b/parsing/termast.ml @@ -18,6 +18,7 @@ open Termops open Inductive open Sign open Environ +open Libnames open Declare open Impargs open Coqast diff --git a/parsing/termast.mli b/parsing/termast.mli index fb0762446..c6e94fe16 100644 --- a/parsing/termast.mli +++ b/parsing/termast.mli @@ -14,6 +14,7 @@ open Term open Termops open Sign open Environ +open Libnames open Nametab open Rawterm open Pattern @@ -36,7 +37,7 @@ val ast_of_existential : env -> existential -> Coqast.t val ast_of_constructor : env -> constructor -> Coqast.t val ast_of_inductive : env -> inductive -> Coqast.t val ast_of_ref : global_reference -> Coqast.t -val ast_of_qualid : Nametab.qualid -> Coqast.t +val ast_of_qualid : qualid -> Coqast.t (* For debugging *) val print_implicits : bool ref |