diff options
34 files changed, 326 insertions, 233 deletions
diff --git a/interp/coqlib.ml b/interp/coqlib.ml index d38ef592f..6879dc965 100644 --- a/interp/coqlib.ml +++ b/interp/coqlib.ml @@ -15,7 +15,7 @@ open Term open Libnames open Pattern open Nametab -open Syntax_def +open Smartlocate (************************************************************************) (* Generic functions to find Coq objects *) diff --git a/interp/genarg.ml b/interp/genarg.ml index 8724b0bfd..c6dc12164 100644 --- a/interp/genarg.ml +++ b/interp/genarg.ml @@ -47,7 +47,11 @@ type argument_type = type 'a and_short_name = 'a * identifier located option type 'a or_by_notation = | AN of 'a - | ByNotation of loc * string * Notation.delimiters option + | ByNotation of (loc * string * Notation.delimiters option) + +let loc_of_or_by_notation f = function + | AN c -> f c + | ByNotation (loc,s,_) -> loc type rawconstr_and_expr = rawconstr * constr_expr option type open_constr_expr = unit * constr_expr diff --git a/interp/genarg.mli b/interp/genarg.mli index 9072456c3..e6747db17 100644 --- a/interp/genarg.mli +++ b/interp/genarg.mli @@ -21,7 +21,9 @@ type 'a and_short_name = 'a * identifier located option type 'a or_by_notation = | AN of 'a - | ByNotation of loc * string * Notation.delimiters option + | ByNotation of (loc * string * Notation.delimiters option) + +val loc_of_or_by_notation : ('a -> loc) -> 'a or_by_notation -> loc (* In globalize tactics, we need to keep the initial [constr_expr] to recompute*) (* in the environment by the effective calls to Intro, Inversion, etc *) diff --git a/interp/interp.mllib b/interp/interp.mllib index 234487bc9..991cfac57 100644 --- a/interp/interp.mllib +++ b/interp/interp.mllib @@ -4,7 +4,8 @@ Ppextend Notation Dumpglob Genarg -Syntax_def +Syntax_def +Smartlocate Reserve Impargs Implicit_quantifiers diff --git a/interp/notation.ml b/interp/notation.ml index 08936759d..58c28149d 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -536,7 +536,7 @@ let decompose_notation_key s = let tok = match String.sub s n (pos-n) with | "_" -> NonTerminal (id_of_string "_") - | s -> Terminal s in + | s -> Terminal (drop_simple_quotes s) in decomp_ntn (tok::dirs) (pos+1) in decomp_ntn [] 0 @@ -650,15 +650,16 @@ let interp_notation_as_global_reference loc test ntn sc = | [] -> error_notation_not_reference loc ntn | _ -> error_ambiguous_notation loc ntn -let locate_notation prraw ntn = +let locate_notation prraw ntn scope = let ntns = factorize_entries (browse_notation false ntn !scope_map) in + let scopes = Option.fold_right push_scope scope !scope_stack in if ntns = [] then str "Unknown notation" else t (str "Notation " ++ tab () ++ str "Scope " ++ tab () ++ fnl () ++ prlist (fun (ntn,l) -> - let scope = find_default ntn !scope_stack in + let scope = find_default ntn scopes in prlist (fun (sc,r,(_,df)) -> hov 0 ( diff --git a/interp/notation.mli b/interp/notation.mli index 21d3ae1a0..57e0deb10 100644 --- a/interp/notation.mli +++ b/interp/notation.mli @@ -167,7 +167,8 @@ val decompose_notation_key : notation -> symbol list (* Prints scopes (expect a pure aconstr printer *) val pr_scope : (rawconstr -> std_ppcmds) -> scope_name -> std_ppcmds val pr_scopes : (rawconstr -> std_ppcmds) -> std_ppcmds -val locate_notation : (rawconstr -> std_ppcmds) -> notation -> std_ppcmds +val locate_notation : (rawconstr -> std_ppcmds) -> notation -> + scope_name option -> std_ppcmds val pr_visibility: (rawconstr -> std_ppcmds) -> scope_name option -> std_ppcmds diff --git a/interp/smartlocate.ml b/interp/smartlocate.ml new file mode 100644 index 000000000..07ae87fa0 --- /dev/null +++ b/interp/smartlocate.ml @@ -0,0 +1,62 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(* Created by Hugo Herbelin from code formerly dispatched in + syntax_def.ml or tacinterp.ml, Sep 2009 *) + +(* This file provides high-level name globalization functions *) + +(* $Id:$ *) + +(* *) +open Pp +open Util +open Names +open Libnames +open Genarg +open Syntax_def +open Topconstr + +let global_of_extended_global = function + | TrueGlobal ref -> ref + | SynDef kn -> + match search_syntactic_definition dummy_loc kn with + | [],ARef ref -> ref + | _ -> raise Not_found + +let locate_global_with_alias (loc,qid) = + let ref = Nametab.locate_extended qid in + try global_of_extended_global ref + with Not_found -> + user_err_loc (loc,"",pr_qualid qid ++ + str " is bound to a notation that does not denote a reference") + +let global_inductive_with_alias r = + match locate_global_with_alias (qualid_of_reference r) with + | IndRef ind -> ind + | ref -> + user_err_loc (loc_of_reference r,"global_inductive", + pr_reference r ++ spc () ++ str "is not an inductive type") + +let global_with_alias r = + let (loc,qid as lqid) = qualid_of_reference r in + try locate_global_with_alias lqid + with Not_found -> Nametab.error_global_not_found_loc loc qid + +let smart_global = function + | AN r -> + global_with_alias r + | ByNotation (loc,ntn,sc) -> + Notation.interp_notation_as_global_reference loc (fun _ -> true) ntn sc + +let smart_global_inductive = function + | AN r -> + global_inductive_with_alias r + | ByNotation (loc,ntn,sc) -> + destIndRef + (Notation.interp_notation_as_global_reference loc isIndRef ntn sc) diff --git a/interp/smartlocate.mli b/interp/smartlocate.mli new file mode 100644 index 000000000..682484f57 --- /dev/null +++ b/interp/smartlocate.mli @@ -0,0 +1,37 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(* $Id:$ *) + +open Util +open Names +open Libnames +open Genarg + +(* [locate_global_with_alias] locates global reference possibly following + a notation if this notation has a role of aliasing; raise Not_found + if not bound in the global env; raise an error if bound to a + syntactic def that does not denote a reference *) + +val locate_global_with_alias : qualid located -> global_reference + +(* Extract a global_reference from a reference that can be an "alias" *) +val global_of_extended_global : extended_global_reference -> global_reference + +(* Locate a reference taking into account possible "alias" notations *) +val global_with_alias : reference -> global_reference + +(* The same for inductive types *) +val global_inductive_with_alias : reference -> inductive + +(* Locate a reference taking into account notations and "aliases" *) +val smart_global : reference or_by_notation -> global_reference + +(* The same for inductive types *) +val smart_global_inductive : reference or_by_notation -> inductive + diff --git a/interp/syntax_def.ml b/interp/syntax_def.ml index 1619bad27..e58bb000a 100644 --- a/interp/syntax_def.ml +++ b/interp/syntax_def.ml @@ -81,29 +81,3 @@ let declare_syntactic_definition local id onlyparse pat = let search_syntactic_definition loc kn = out_pat (KNmap.find kn !syntax_table) - -let global_of_extended_global = function - | TrueGlobal ref -> ref - | SynDef kn -> - match search_syntactic_definition dummy_loc kn with - | [],ARef ref -> ref - | _ -> raise Not_found - -let locate_global_with_alias (loc,qid) = - let ref = Nametab.locate_extended qid in - try global_of_extended_global ref - with Not_found -> - user_err_loc (loc,"",pr_qualid qid ++ - str " is bound to a notation that does not denote a reference") - -let global_inductive_with_alias r = - match locate_global_with_alias (qualid_of_reference r) with - | IndRef ind -> ind - | ref -> - user_err_loc (loc_of_reference r,"global_inductive", - pr_reference r ++ spc () ++ str "is not an inductive type") - -let global_with_alias r = - let (loc,qid as lqid) = qualid_of_reference r in - try locate_global_with_alias lqid - with Not_found -> Nametab.error_global_not_found_loc loc qid diff --git a/interp/syntax_def.mli b/interp/syntax_def.mli index fb0c3c9f2..3ba78e91d 100644 --- a/interp/syntax_def.mli +++ b/interp/syntax_def.mli @@ -25,19 +25,3 @@ val declare_syntactic_definition : bool -> identifier -> bool -> syndef_interpretation -> unit val search_syntactic_definition : loc -> kernel_name -> syndef_interpretation - -(* [locate_global_with_alias] locates global reference possibly following - a notation if this notation has a role of aliasing; raise Not_found - if not bound in the global env; raise an error if bound to a - syntactic def that does not denote a reference *) - -val locate_global_with_alias : qualid located -> global_reference - -(* Extract a global_reference from a reference that can be an "alias" *) -val global_of_extended_global : extended_global_reference -> global_reference - -(* Locate a reference taking into account possible "alias" notations *) -val global_with_alias : reference -> global_reference - -(* The same for inductive types *) -val global_inductive_with_alias : reference -> inductive diff --git a/lib/util.ml b/lib/util.ml index 549c40e30..b161b966e 100644 --- a/lib/util.ml +++ b/lib/util.ml @@ -99,6 +99,10 @@ let strip s = let a = lstrip_rec 0 and b = rstrip_rec (n-1) in String.sub s a (b-a+1) +let drop_simple_quotes s = + let n = String.length s in + if n > 2 & s.[0] = '\'' & s.[n-1] = '\'' then String.sub s 1 (n-2) else s + (* substring searching... *) (* gdzie = where, co = what *) diff --git a/lib/util.mli b/lib/util.mli index 84762bade..5e32a1b0e 100644 --- a/lib/util.mli +++ b/lib/util.mli @@ -83,6 +83,7 @@ val is_blank : char -> bool val explode : string -> string list val implode : string list -> string val strip : string -> string +val drop_simple_quotes : string -> string val string_index_from : string -> int -> string -> int val string_string_contains : where:string -> what:string -> bool val plural : int -> string -> string diff --git a/library/libnames.ml b/library/libnames.ml index c7d484d1e..0404d7cd8 100644 --- a/library/libnames.ml +++ b/library/libnames.ml @@ -23,6 +23,14 @@ type global_reference = | ConstructRef of constructor let isVarRef = function VarRef _ -> true | _ -> false +let isConstRef = function ConstRef _ -> true | _ -> false +let isIndRef = function IndRef _ -> true | _ -> false +let isConstructRef = function ConstructRef _ -> true | _ -> false + +let destVarRef = function VarRef ind -> ind | _ -> failwith "destVarRef" +let destConstRef = function ConstRef ind -> ind | _ -> failwith "destConstRef" +let destIndRef = function IndRef ind -> ind | _ -> failwith "destIndRef" +let destConstructRef = function ConstructRef ind -> ind | _ -> failwith "destConstructRef" let subst_constructor subst ((kn,i),j as ref) = let kn' = subst_kn subst kn in diff --git a/library/libnames.mli b/library/libnames.mli index 92dd9cb28..b93ee87ee 100644 --- a/library/libnames.mli +++ b/library/libnames.mli @@ -24,6 +24,14 @@ type global_reference = | ConstructRef of constructor val isVarRef : global_reference -> bool +val isConstRef : global_reference -> bool +val isIndRef : global_reference -> bool +val isConstructRef : global_reference -> bool + +val destVarRef : global_reference -> variable +val destConstRef : global_reference -> constant +val destIndRef : global_reference -> inductive +val destConstructRef : global_reference -> constructor val subst_constructor : substitution -> constructor -> constructor * constr val subst_global : substitution -> global_reference -> global_reference * constr diff --git a/library/nametab.mli b/library/nametab.mli index 5367bfdd8..774b148a5 100755 --- a/library/nametab.mli +++ b/library/nametab.mli @@ -21,12 +21,12 @@ open Libnames There are three classes of names: 1a- internal kernel names: [kernel_name], [constant], [inductive], - [module_path] + [module_path], [dir_path] 1b- other internal names: [global_reference], [syndef_name], [extended_global_reference], [global_dir_reference], ... - 2- full, non ambiguous user names: [full_path] and [dir_path] + 2- full, non ambiguous user names: [full_path] 3- non necessarily full, possibly ambiguous user names: [reference] and [qualid] diff --git a/parsing/g_prim.ml4 b/parsing/g_prim.ml4 index 0e91fddbd..168e532a8 100644 --- a/parsing/g_prim.ml4 +++ b/parsing/g_prim.ml4 @@ -37,7 +37,7 @@ GEXTEND Gram GLOBAL: bigint natural integer identref name ident var preident fullyqualid qualid reference dirpath - ne_string string pattern_ident pattern_identref; + ne_string string pattern_ident pattern_identref by_notation smart_global; preident: [ [ s = IDENT -> s ] ] ; @@ -84,6 +84,13 @@ GEXTEND Gram | id = ident -> Ident (loc,id) ] ] ; + by_notation: + [ [ s = ne_string; sc = OPT ["%"; key = IDENT -> key ] -> (loc,s,sc) ] ] + ; + smart_global: + [ [ c = reference -> Genarg.AN c + | ntn = by_notation -> Genarg.ByNotation ntn ] ] + ; qualid: [ [ qid = basequalid -> loc, qid ] ] ; diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4 index 875b9dc07..846246ed0 100644 --- a/parsing/g_tactic.ml4 +++ b/parsing/g_tactic.ml4 @@ -215,11 +215,6 @@ GEXTEND Gram | c1 = constr; "at"; occs = occs_nums; "with"; c2 = constr -> (Some (occs,c1), c2) ] ] ; - smart_global: - [ [ c = global -> AN c - | s = ne_string; sc = OPT ["%"; key = IDENT -> key ] -> - ByNotation (loc,s,sc) ] ] - ; occs_nums: [ [ nl = LIST1 nat_or_var -> no_occurrences_expr_but nl | "-"; n = nat_or_var; nl = LIST0 int_or_var -> diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index 9940a1378..272737cc6 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -306,11 +306,11 @@ GEXTEND Gram | id = identref; ":="; kind = scheme_kind -> (Some id,kind) ] ] ; scheme_kind: - [ [ IDENT "Induction"; "for"; ind = global; + [ [ IDENT "Induction"; "for"; ind = smart_global; IDENT "Sort"; s = sort-> InductionScheme(true,ind,s) - | IDENT "Minimality"; "for"; ind = global; + | IDENT "Minimality"; "for"; ind = smart_global; IDENT "Sort"; s = sort-> InductionScheme(false,ind,s) - | IDENT "Equality"; "for" ; ind = global -> EqualityScheme(ind) ] ] + | IDENT "Equality"; "for" ; ind = smart_global -> EqualityScheme(ind) ] ] ; (* Various Binders *) (* @@ -465,17 +465,20 @@ GEXTEND Gram gallina_ext: [ [ (* Transparent and Opaque *) - IDENT "Transparent"; l = LIST1 global -> + IDENT "Transparent"; l = LIST1 smart_global -> VernacSetOpacity (use_non_locality (),[Conv_oracle.transparent,l]) - | IDENT "Opaque"; l = LIST1 global -> + | IDENT "Opaque"; l = LIST1 smart_global -> VernacSetOpacity (use_non_locality (),[Conv_oracle.Opaque, l]) | IDENT "Strategy"; l = - LIST1 [ lev=strategy_level; "["; q=LIST1 global; "]" -> (lev,q)] -> + LIST1 [ lev=strategy_level; "["; q=LIST1 smart_global; "]" -> (lev,q)] -> VernacSetOpacity (use_locality (),l) (* Canonical structure *) | IDENT "Canonical"; IDENT "Structure"; qid = global -> - VernacCanonical qid - | IDENT "Canonical"; IDENT "Structure"; qid = global; d = def_body -> + VernacCanonical (AN qid) + | IDENT "Canonical"; IDENT "Structure"; ntn = by_notation -> + VernacCanonical (ByNotation ntn) + | IDENT "Canonical"; IDENT "Structure"; qid = global; + d = def_body -> let s = coerce_reference_to_id qid in VernacDefinition ((Global,false,CanonicalStructure),(dummy_loc,s),d, @@ -496,10 +499,16 @@ GEXTEND Gram VernacIdentityCoercion (use_locality_exp (), f, s, t) | IDENT "Coercion"; IDENT "Local"; qid = global; ":"; s = class_rawexpr; ">->"; t = class_rawexpr -> - VernacCoercion (enforce_locality_exp (), qid, s, t) + VernacCoercion (enforce_locality_exp (), AN qid, s, t) + | IDENT "Coercion"; IDENT "Local"; ntn = by_notation; ":"; + s = class_rawexpr; ">->"; t = class_rawexpr -> + VernacCoercion (enforce_locality_exp (), ByNotation ntn, s, t) | IDENT "Coercion"; qid = global; ":"; s = class_rawexpr; ">->"; t = class_rawexpr -> - VernacCoercion (use_locality_exp (), qid, s, t) + VernacCoercion (use_locality_exp (), AN qid, s, t) + | IDENT "Coercion"; ntn = by_notation; ":"; s = class_rawexpr; ">->"; + t = class_rawexpr -> + VernacCoercion (use_locality_exp (), ByNotation ntn, s, t) | IDENT "Context"; c = binders_let -> VernacContext c @@ -530,7 +539,7 @@ GEXTEND Gram | IDENT "Existing"; IDENT "Instance"; is = identref -> VernacDeclareInstance is (* Implicit *) - | IDENT "Implicit"; IDENT "Arguments"; qid = global; + | IDENT "Implicit"; IDENT "Arguments"; qid = smart_global; pos = OPT [ "["; l = LIST0 implicit_name; "]" -> List.map (fun (id,b,f) -> (ExplByName id,b,f)) l ] -> VernacDeclareImplicits (use_section_locality (),qid,pos) @@ -601,13 +610,13 @@ GEXTEND Gram (* Printing (careful factorization of entries) *) | IDENT "Print"; p = printable -> VernacPrint p - | IDENT "Print"; qid = global -> VernacPrint (PrintName qid) + | IDENT "Print"; qid = smart_global -> VernacPrint (PrintName qid) | IDENT "Print"; IDENT "Module"; "Type"; qid = global -> VernacPrint (PrintModuleType qid) | IDENT "Print"; IDENT "Module"; qid = global -> VernacPrint (PrintModule qid) | IDENT "Inspect"; n = natural -> VernacPrint (PrintInspect n) - | IDENT "About"; qid = global -> VernacPrint (PrintAbout qid) + | IDENT "About"; qid = smart_global -> VernacPrint (PrintAbout qid) (* Searching the environment *) | IDENT "Search"; c = constr_pattern; l = in_or_out_modules -> @@ -674,7 +683,7 @@ GEXTEND Gram fun g -> VernacCheckMayEval (None, g, c) ] ] ; printable: - [ [ IDENT "Term"; qid = global -> PrintName qid + [ [ IDENT "Term"; qid = smart_global -> PrintName qid | IDENT "All" -> PrintFullContext | IDENT "Section"; s = global -> PrintSectionContext s | IDENT "Grammar"; ent = IDENT -> @@ -690,40 +699,36 @@ GEXTEND Gram | IDENT "Graph" -> PrintGraph | IDENT "Classes" -> PrintClasses | IDENT "TypeClasses" -> PrintTypeClasses - | IDENT "Instances"; qid = global -> PrintInstances qid + | IDENT "Instances"; qid = smart_global -> PrintInstances qid | IDENT "Ltac"; qid = global -> PrintLtac qid | IDENT "Coercions" -> PrintCoercions | IDENT "Coercion"; IDENT "Paths"; s = class_rawexpr; t = class_rawexpr -> PrintCoercionPaths (s,t) | IDENT "Canonical"; IDENT "Projections" -> PrintCanonicalConversions | IDENT "Tables" -> PrintTables -(* Obsolete: was used for cooking V6.3 recipes ?? - | IDENT "Proof"; qid = global -> PrintOpaqueName qid -*) | IDENT "Hint" -> PrintHintGoal - | IDENT "Hint"; qid = global -> PrintHint qid + | IDENT "Hint"; qid = smart_global -> PrintHint qid | IDENT "Hint"; "*" -> PrintHintDb | IDENT "HintDb"; s = IDENT -> PrintHintDbName s | "Rewrite"; IDENT "HintDb"; s = IDENT -> PrintRewriteHintDbName s | IDENT "Scopes" -> PrintScopes | IDENT "Scope"; s = IDENT -> PrintScope s | IDENT "Visibility"; s = OPT IDENT -> PrintVisibility s - | IDENT "Implicit"; qid = global -> PrintImplicit qid + | IDENT "Implicit"; qid = smart_global -> PrintImplicit qid | IDENT "Universes"; fopt = OPT ne_string -> PrintUniverses fopt - | IDENT "Assumptions"; qid = global -> PrintAssumptions (false, qid) - | IDENT "Opaque"; IDENT "Dependencies"; qid = global -> PrintAssumptions (true, qid) ] ] + | IDENT "Assumptions"; qid = smart_global -> PrintAssumptions (false, qid) + | IDENT "Opaque"; IDENT "Dependencies"; qid = smart_global -> PrintAssumptions (true, qid) ] ] ; class_rawexpr: [ [ IDENT "Funclass" -> FunClass | IDENT "Sortclass" -> SortClass - | qid = global -> RefClass qid ] ] + | qid = smart_global -> RefClass qid ] ] ; locatable: - [ [ qid = global -> LocateTerm qid + [ [ qid = smart_global -> LocateTerm qid | IDENT "File"; f = ne_string -> LocateFile f | IDENT "Library"; qid = global -> LocateLibrary qid - | IDENT "Module"; qid = global -> LocateModule qid - | s = ne_string -> LocateNotation s ] ] + | IDENT "Module"; qid = global -> LocateModule qid ] ] ; option_value: [ [ n = integer -> IntValue n @@ -805,7 +810,7 @@ GEXTEND Gram | IDENT "Bind"; IDENT "Scope"; sc = IDENT; "with"; refl = LIST1 class_rawexpr -> VernacBindScope (sc,refl) - | IDENT "Arguments"; IDENT "Scope"; qid = global; + | IDENT "Arguments"; IDENT "Scope"; qid = smart_global; "["; scl = LIST0 opt_scope; "]" -> VernacArgumentsScope (use_non_locality (),qid,scl) diff --git a/parsing/pcoq.ml4 b/parsing/pcoq.ml4 index 1c9e1e46b..6b5d03d91 100644 --- a/parsing/pcoq.ml4 +++ b/parsing/pcoq.ml4 @@ -273,6 +273,8 @@ module Prim = let bigint = Gram.Entry.create "Prim.bigint" let string = gec_gen rawwit_string "string" let reference = make_gen_entry uprim rawwit_ref "reference" + let by_notation = Gram.Entry.create "by_notation" + let smart_global = Gram.Entry.create "smart_global" (* parsed like ident but interpreted as a term *) let var = gec_gen rawwit_var "var" diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli index f356ae07e..cfd05f4f7 100644 --- a/parsing/pcoq.mli +++ b/parsing/pcoq.mli @@ -182,6 +182,8 @@ module Prim : val qualid : qualid located Gram.Entry.e val fullyqualid : identifier list located Gram.Entry.e val reference : reference Gram.Entry.e + val by_notation : (loc * string * string option) Gram.Entry.e + val smart_global : reference or_by_notation Gram.Entry.e val dirpath : dir_path Gram.Entry.e val ne_string : string Gram.Entry.e val var : identifier located Gram.Entry.e diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml index 656c38497..26fa53550 100644 --- a/parsing/ppvernac.ml +++ b/parsing/ppvernac.ml @@ -50,6 +50,8 @@ let pr_lname = function (loc,Name id) -> pr_lident (loc,id) | lna -> pr_located pr_name lna +let pr_smart_global = pr_or_by_notation pr_reference + let pr_ltac_id = Libnames.pr_reference let pr_module = Libnames.pr_reference @@ -164,7 +166,7 @@ let pr_explanation (e,b,f) = let pr_class_rawexpr = function | FunClass -> str"Funclass" | SortClass -> str"Sortclass" - | RefClass qid -> pr_reference qid + | RefClass qid -> pr_smart_global qid let pr_option_ref_value = function | QualidRefValue id -> pr_reference id @@ -304,7 +306,7 @@ let pr_onescheme (idop,schem) = | None -> spc () ) ++ hov 0 ((if dep then str"Induction for" else str"Minimality for") - ++ spc() ++ pr_reference ind) ++ spc() ++ + ++ spc() ++ pr_smart_global ind) ++ spc() ++ hov 0 (str"Sort" ++ spc() ++ pr_rawsort s) | EqualityScheme ind -> (match idop with @@ -312,7 +314,7 @@ let pr_onescheme (idop,schem) = | None -> spc() ) ++ hov 0 (str"Equality for") - ++ spc() ++ pr_reference ind + ++ spc() ++ pr_smart_global ind let begin_of_inductive = function [] -> 0 @@ -321,7 +323,7 @@ let begin_of_inductive = function let pr_class_rawexpr = function | FunClass -> str"Funclass" | SortClass -> str"Sortclass" - | RefClass qid -> pr_reference qid + | RefClass qid -> pr_smart_global qid let pr_assumption_token many = function | (Local,Logical) -> @@ -508,7 +510,8 @@ let rec pr_vernac = function | VernacArgumentsScope (local,q,scl) -> let pr_opt_scope = function | None -> str"_" | Some sc -> str sc in - str"Arguments Scope" ++ spc() ++ pr_non_locality local ++ pr_reference q + str"Arguments Scope" ++ spc() ++ pr_non_locality local ++ + pr_smart_global q ++ spc() ++ str"[" ++ prlist_with_sep sep pr_opt_scope scl ++ str"]" | VernacInfix (local,(s,mv),q,sn) -> (* A Verifier *) hov 0 (hov 0 (str"Infix " ++ pr_locality local @@ -541,7 +544,7 @@ let rec pr_vernac = function | None -> mt() | Some r -> str"Eval" ++ spc() ++ - pr_red_expr (pr_constr, pr_lconstr, pr_or_by_notation pr_reference) r ++ + pr_red_expr (pr_constr, pr_lconstr, pr_smart_global) r ++ str" in" ++ spc() in let pr_def_body = function | DefineBody (bl,red,body,d) -> @@ -690,12 +693,12 @@ let rec pr_vernac = function | VernacImport (f,l) -> (if f then str"Export" else str"Import") ++ spc() ++ prlist_with_sep sep pr_import_module l - | VernacCanonical q -> str"Canonical Structure" ++ spc() ++ pr_reference q + | VernacCanonical q -> str"Canonical Structure" ++ spc() ++ pr_smart_global q | VernacCoercion (s,id,c1,c2) -> hov 1 ( str"Coercion" ++ (match s with | Local -> spc() ++ str"Local" ++ spc() | Global -> spc()) ++ - pr_reference id ++ spc() ++ str":" ++ spc() ++ pr_class_rawexpr c1 ++ + pr_smart_global id ++ spc() ++ str":" ++ spc() ++ pr_class_rawexpr c1 ++ spc() ++ str">->" ++ spc() ++ pr_class_rawexpr c2) | VernacIdentityCoercion (s,id,c1,c2) -> hov 1 ( @@ -831,10 +834,10 @@ let rec pr_vernac = function prlist_with_sep spc pr_id ids ++ str" :=" ++ pr_constrarg c ++ pr_syntax_modifiers (if onlyparsing then [SetOnlyParsing] else [])) | VernacDeclareImplicits (local,q,None) -> - hov 2 (str"Implicit Arguments" ++ spc() ++ pr_reference q) + hov 2 (str"Implicit Arguments" ++ spc() ++ pr_smart_global q) | VernacDeclareImplicits (local,q,Some imps) -> hov 1 (str"Implicit Arguments " ++ pr_non_locality local ++ - spc() ++ pr_reference q ++ spc() ++ + spc() ++ pr_smart_global q ++ spc() ++ str"[" ++ prlist_with_sep sep pr_explanation imps ++ str"]") | VernacReserve (idl,c) -> hov 1 (str"Implicit Type" ++ @@ -843,10 +846,10 @@ let rec pr_vernac = function pr_lconstr c) | VernacSetOpacity(b,[k,l]) when k=Conv_oracle.transparent -> hov 1 (str"Transparent" ++ pr_non_locality b ++ - spc() ++ prlist_with_sep sep pr_reference l) + spc() ++ prlist_with_sep sep pr_smart_global l) | VernacSetOpacity(b,[Conv_oracle.Opaque,l]) -> hov 1 (str"Opaque" ++ pr_non_locality b ++ - spc() ++ prlist_with_sep sep pr_reference l) + spc() ++ prlist_with_sep sep pr_smart_global l) | VernacSetOpacity (local,l) -> let pr_lev = function Conv_oracle.Opaque -> str"opaque" @@ -855,7 +858,7 @@ let rec pr_vernac = function | Conv_oracle.Level n -> int n in let pr_line (l,q) = hov 2 (pr_lev l ++ spc() ++ - str"[" ++ prlist_with_sep sep pr_reference q ++ str"]") in + str"[" ++ prlist_with_sep sep pr_smart_global q ++ str"]") in hov 1 (pr_locality local ++ str"Strategy" ++ spc() ++ hv 0 (prlist_with_sep sep pr_line l)) | VernacUnsetOption (l,na) -> @@ -870,7 +873,7 @@ let rec pr_vernac = function let pr_mayeval r c = match r with | Some r0 -> hov 2 (str"Eval" ++ spc() ++ - pr_red_expr (pr_constr,pr_lconstr,pr_or_by_notation pr_reference) r0 ++ + pr_red_expr (pr_constr,pr_lconstr,pr_smart_global) r0 ++ spc() ++ str"in" ++ spc () ++ pr_constr c) | None -> hov 2 (str"Check" ++ spc() ++ pr_constr c) in @@ -891,41 +894,39 @@ let rec pr_vernac = function | PrintGraph -> str"Print Graph" | PrintClasses -> str"Print Classes" | PrintTypeClasses -> str"Print TypeClasses" - | PrintInstances qid -> str"Print Instances" ++ spc () ++ pr_reference qid + | PrintInstances qid -> str"Print Instances" ++ spc () ++ pr_smart_global qid | PrintLtac qid -> str"Print Ltac" ++ spc() ++ pr_reference qid | PrintCoercions -> str"Print Coercions" | PrintCoercionPaths (s,t) -> str"Print Coercion Paths" ++ spc() ++ pr_class_rawexpr s ++ spc() ++ pr_class_rawexpr t | PrintCanonicalConversions -> str"Print Canonical Structures" | PrintTables -> str"Print Tables" - | PrintOpaqueName qid -> str"Print Term" ++ spc() ++ pr_reference qid | PrintHintGoal -> str"Print Hint" - | PrintHint qid -> str"Print Hint" ++ spc() ++ pr_reference qid + | PrintHint qid -> str"Print Hint" ++ spc() ++ pr_smart_global qid | PrintHintDb -> str"Print Hint *" | PrintHintDbName s -> str"Print HintDb" ++ spc() ++ str s | PrintRewriteHintDbName s -> str"Print Rewrite HintDb" ++ spc() ++ str s | PrintUniverses fopt -> str"Dump Universes" ++ pr_opt str fopt - | PrintName qid -> str"Print" ++ spc() ++ pr_reference qid + | PrintName qid -> str"Print" ++ spc() ++ pr_smart_global qid | PrintModuleType qid -> str"Print Module Type" ++ spc() ++ pr_reference qid | PrintModule qid -> str"Print Module" ++ spc() ++ pr_reference qid | PrintInspect n -> str"Inspect" ++ spc() ++ int n | PrintScopes -> str"Print Scopes" | PrintScope s -> str"Print Scope" ++ spc() ++ str s | PrintVisibility s -> str"Print Visibility" ++ pr_opt str s - | PrintAbout qid -> str"About" ++ spc() ++ pr_reference qid - | PrintImplicit qid -> str"Print Implicit" ++ spc() ++ pr_reference qid + | PrintAbout qid -> str"About" ++ spc() ++ pr_smart_global qid + | PrintImplicit qid -> str"Print Implicit" ++ spc() ++ pr_smart_global qid (* spiwack: command printing all the axioms and section variables used in a term *) | PrintAssumptions (b,qid) -> (if b then str"Print Assumptions" else str"Print Opaque Dependencies") - ++spc()++pr_reference qid + ++ spc() ++ pr_smart_global qid in pr_printable p | VernacSearch (sea,sea_r) -> pr_search sea sea_r pr_constr_pattern_expr | VernacLocate loc -> let pr_locate =function - | LocateTerm qid -> pr_reference qid + | LocateTerm qid -> pr_smart_global qid | LocateFile f -> str"File" ++ spc() ++ qs f | LocateLibrary qid -> str"Library" ++ spc () ++ pr_module qid | LocateModule qid -> str"Module" ++ spc () ++ pr_module qid - | LocateNotation s -> qs s in str"Locate" ++ spc() ++ pr_locate loc | VernacComments l -> hov 2 diff --git a/parsing/prettyp.ml b/parsing/prettyp.ml index 9e6ff72d3..0518da327 100644 --- a/parsing/prettyp.ml +++ b/parsing/prettyp.ml @@ -619,8 +619,7 @@ let print_sec_context sec = let print_sec_context_typ sec = print_context false None (read_sec_context sec) -let print_name ref = - match locate_any_name ref with +let print_any_name = function | Term (ConstRef sp) -> print_constant_with_infos sp | Term (IndRef (sp,_)) -> print_inductive sp | Term (ConstructRef ((sp,_),_)) -> print_inductive sp @@ -639,6 +638,14 @@ let print_name ref = errorlabstrm "print_name" (pr_qualid qid ++ spc () ++ str "not a defined object.") +let print_name = function + | Genarg.ByNotation (loc,ntn,sc) -> + print_any_name + (Term (Notation.interp_notation_as_global_reference loc (fun _ -> true) + ntn sc)) + | Genarg.AN ref -> + print_any_name (locate_any_name ref) + let print_opaque_name qid = let env = Global.env () in match global qid with @@ -657,8 +664,7 @@ let print_opaque_name qid = let (_,c,ty) = lookup_named id env in print_named_decl (id,c,ty) -let print_about ref = - let k = locate_any_name ref in +let print_about_any k = begin match k with | Term ref -> print_ref false ref ++ fnl () ++ print_name_infos ref ++ @@ -670,8 +676,16 @@ let print_about ref = ++ hov 0 (str "Expands to: " ++ pr_located_qualid k) +let print_about = function + | Genarg.ByNotation (loc,ntn,sc) -> + print_about_any + (Term (Notation.interp_notation_as_global_reference loc (fun _ -> true) + ntn sc)) + | Genarg.AN ref -> + print_about_any (locate_any_name ref) + let print_impargs ref = - let ref = Nametab.global ref in + let ref = Smartlocate.smart_global ref in let impl = implicits_of_global ref in let has_impl = List.filter is_status_implicit impl <> [] in (* Need to reduce since implicits are computed with products flattened *) diff --git a/parsing/prettyp.mli b/parsing/prettyp.mli index 88b0a80ec..ba1977e89 100644 --- a/parsing/prettyp.mli +++ b/parsing/prettyp.mli @@ -18,6 +18,7 @@ open Environ open Reductionops open Libnames open Nametab +open Genarg (*i*) (* A Pretty-Printer for the Calculus of Inductive Constructions. *) @@ -40,10 +41,10 @@ val print_eval : (* This function is exported for the graphical user-interface pcoq *) val build_inductive : mutual_inductive -> int -> global_reference * rel_context * types * identifier array * types array -val print_name : reference -> std_ppcmds +val print_name : reference or_by_notation -> std_ppcmds val print_opaque_name : reference -> std_ppcmds -val print_about : reference -> std_ppcmds -val print_impargs : reference -> std_ppcmds +val print_about : reference or_by_notation -> std_ppcmds +val print_impargs : reference or_by_notation -> std_ppcmds (*i val print_extracted_name : identifier -> std_ppcmds diff --git a/plugins/interface/xlate.ml b/plugins/interface/xlate.ml index 4d4eff56f..be7472a48 100644 --- a/plugins/interface/xlate.ml +++ b/plugins/interface/xlate.ml @@ -217,10 +217,14 @@ let reference_to_ct_ID = function | Ident (_,id) -> CT_ident (Names.string_of_id id) | Qualid (_,qid) -> CT_ident (Libnames.string_of_qualid qid) +let loc_smart_global_to_ct_ID = function + | AN ref -> reference_to_ct_ID ref + | ByNotation _ -> xlate_error "smart_global to do" + let xlate_class = function | FunClass -> CT_ident "FUNCLASS" | SortClass -> CT_ident "SORTCLASS" - | RefClass qid -> loc_qualid_to_ct_ID qid + | RefClass qid -> loc_smart_global_to_ct_ID qid let id_to_pattern_var ctid = match ctid with @@ -1837,7 +1841,7 @@ let rec xlate_vernac = CT_strategy(CT_level_list (List.map (fun (l,q) -> (level_to_ct_LEVEL l, - CT_id_list(List.map loc_qualid_to_ct_ID q))) l)) + CT_id_list(List.map loc_smart_global_to_ct_ID q))) l)) | VernacUndo n -> CT_undo (CT_coerce_INT_to_INT_OPT (CT_int n)) | VernacShow (ShowGoal nopt) -> CT_show_goal (xlate_int_opt nopt) | VernacShow ShowNode -> CT_show_node @@ -1860,8 +1864,7 @@ let rec xlate_vernac = | VernacPrint p -> (match p with PrintFullContext -> CT_print_all - | PrintName id -> CT_print_id (loc_qualid_to_ct_ID id) - | PrintOpaqueName id -> CT_print_opaqueid (loc_qualid_to_ct_ID id) + | PrintName id -> CT_print_id (loc_smart_global_to_ct_ID id) | PrintSectionContext id -> CT_print_section (loc_qualid_to_ct_ID id) | PrintModules -> CT_print_modules | PrintGrammar name -> CT_print_grammar CT_grammar_none @@ -1871,7 +1874,7 @@ let rec xlate_vernac = | PrintRewriteHintDbName id -> CT_print_rewrite_hintdb (CT_ident id) | PrintHint id -> - CT_print_hint (CT_coerce_ID_to_ID_OPT (loc_qualid_to_ct_ID id)) + CT_print_hint (CT_coerce_ID_to_ID_OPT (loc_smart_global_to_ct_ID id)) | PrintHintGoal -> CT_print_hint ctv_ID_OPT_NONE | PrintLoadPath None -> CT_print_loadpath | PrintLoadPath _ -> xlate_error "TODO: Print LoadPath dir" @@ -1903,8 +1906,8 @@ let rec xlate_vernac = (match id_opt with Some id -> CT_coerce_ID_to_ID_OPT(CT_ident id) | None -> ctv_ID_OPT_NONE) - | PrintAbout qid -> CT_print_about(loc_qualid_to_ct_ID qid) - | PrintImplicit qid -> CT_print_implicit(loc_qualid_to_ct_ID qid)) + | PrintAbout qid -> CT_print_about(loc_smart_global_to_ct_ID qid) + | PrintImplicit qid -> CT_print_implicit(loc_smart_global_to_ct_ID qid)) | VernacBeginSection (_,id) -> CT_coerce_SECTION_BEGIN_to_COMMAND (CT_section (xlate_ident id)) | VernacEndSegment (_,id) -> CT_section_end (xlate_ident id) @@ -2007,12 +2010,12 @@ let rec xlate_vernac = | (Some (_,id), InductionScheme (depstr, inde, sort)) -> CT_scheme_spec (xlate_ident id, xlate_dep depstr, - CT_coerce_ID_to_FORMULA (loc_qualid_to_ct_ID inde), + CT_coerce_ID_to_FORMULA (loc_smart_global_to_ct_ID inde), xlate_sort sort) | (None, InductionScheme (depstr, inde, sort)) -> CT_scheme_spec (xlate_ident (id_of_string ""), xlate_dep depstr, - CT_coerce_ID_to_FORMULA (loc_qualid_to_ct_ID inde), + CT_coerce_ID_to_FORMULA (loc_smart_global_to_ct_ID inde), xlate_sort sort) | (_, EqualityScheme _) -> xlate_error "TODO: Scheme Equality" in CT_ind_scheme @@ -2064,7 +2067,7 @@ let rec xlate_vernac = | VernacOpenCloseScope(true, false, s) -> CT_local_close_scope(CT_ident s) | VernacOpenCloseScope(false, false, s) -> CT_close_scope(CT_ident s) | VernacArgumentsScope(true, qid, l) -> - CT_arguments_scope(loc_qualid_to_ct_ID qid, + CT_arguments_scope(loc_smart_global_to_ct_ID qid, CT_id_opt_list (List.map (fun x -> @@ -2077,7 +2080,7 @@ let rec xlate_vernac = | VernacBindScope(id, a::l) -> let xlate_class_rawexpr = function FunClass -> CT_ident "Funclass" | SortClass -> CT_ident "Sortclass" - | RefClass qid -> loc_qualid_to_ct_ID qid in + | RefClass qid -> loc_smart_global_to_ct_ID qid in CT_bind_scope(CT_ident id, CT_id_ne_list(xlate_class_rawexpr a, List.map xlate_class_rawexpr l)) @@ -2124,7 +2127,7 @@ let rec xlate_vernac = (* Cannot decide whether it is a global or a Local but at toplevel *) | Global -> CT_coerce_NONE_to_LOCAL_OPT CT_none | Local -> CT_local in - CT_coercion (local_opt, id_opt, loc_qualid_to_ct_ID id1, + CT_coercion (local_opt, id_opt, loc_smart_global_to_ct_ID id1, xlate_class id2, xlate_class id3) | VernacIdentityCoercion (s, (_,id1), id2, id3) -> @@ -2157,7 +2160,7 @@ let rec xlate_vernac = CT_scomments(CT_scomment_content_list (List.map xlate_comment l)) | VernacDeclareImplicits(true, id, opt_positions) -> CT_implicits - (reference_to_ct_ID id, + (loc_smart_global_to_ct_ID id, match opt_positions with None -> CT_coerce_NONE_to_ID_LIST_OPT CT_none | Some l -> @@ -2175,11 +2178,10 @@ let rec xlate_vernac = List.map (fun (_,x) -> xlate_ident x) l), xlate_formula f) | VernacReserve([], _) -> assert false - | VernacLocate(LocateTerm id) -> CT_locate(reference_to_ct_ID id) + | VernacLocate(LocateTerm id) -> CT_locate(loc_smart_global_to_ct_ID id) | VernacLocate(LocateLibrary id) -> CT_locate_lib(reference_to_ct_ID id) | VernacLocate(LocateModule _) -> xlate_error "TODO: Locate Module" | VernacLocate(LocateFile s) -> CT_locate_file(CT_string s) - | VernacLocate(LocateNotation s) -> CT_locate_notation(CT_string s) | VernacTime(v) -> CT_time(xlate_vernac v) | VernacTimeout(n,v) -> CT_timeout(CT_int n,xlate_vernac v) | VernacSetOption (_,["Implicit"; "Arguments"], BoolValue true)->CT_user_vernac (CT_ident "IMPLICIT_ARGS_ON", CT_varg_list[]) diff --git a/plugins/setoid_ring/newring.ml4 b/plugins/setoid_ring/newring.ml4 index 6d1ed511b..14d10e54f 100644 --- a/plugins/setoid_ring/newring.ml4 +++ b/plugins/setoid_ring/newring.ml4 @@ -623,7 +623,7 @@ let interp_cst_tac env sigma rk kind (zero,one,add,mul,opp) cst_tac = match cst_tac with Some (CstTac t) -> Tacinterp.glob_tactic t | Some (Closed lc) -> - closed_term_ast (List.map Syntax_def.global_with_alias lc) + closed_term_ast (List.map Smartlocate.global_with_alias lc) | None -> (match rk, opp, kind with Abstract, None, _ -> @@ -667,7 +667,7 @@ let interp_power env pow = match tac with | CstTac t -> Tacinterp.glob_tactic t | Closed lc -> - closed_term_ast (List.map Syntax_def.global_with_alias lc) in + closed_term_ast (List.map Smartlocate.global_with_alias lc) in let spec = make_hyp env (ic spec) in (tac, lapp coq_Some [|carrier; spec|]) diff --git a/tactics/auto.ml b/tactics/auto.ml index c62824d4b..394626f24 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -34,6 +34,7 @@ open Clenv open Hiddentac open Libnames open Nametab +open Smartlocate open Libobject open Library open Printer @@ -533,7 +534,7 @@ type hints_entry = let interp_hints h = let f = Constrintern.interp_constr Evd.empty (Global.env()) in let fr r = - let gr = Syntax_def.global_with_alias r in + let gr = global_with_alias r in let r' = evaluable_of_global_reference (Global.env()) gr in Dumpglob.add_glob (loc_of_reference r) gr; r' in @@ -1118,7 +1119,7 @@ let superauto n to_add argl = tclTRY (tclCOMPLETE (search_superauto n to_add argl)) let interp_to_add gl r = - let r = Syntax_def.locate_global_with_alias (qualid_of_reference r) in + let r = locate_global_with_alias (qualid_of_reference r) in let id = basename_of_global r in (next_ident_away id (pf_ids_of_hyps gl), constr_of_global r) diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index 5df025c1a..28173b7a3 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -26,6 +26,7 @@ open Names open Nameops open Libnames open Nametab +open Smartlocate open Pfedit open Proof_type open Refiner @@ -365,17 +366,7 @@ let intern_or_var ist = function | ArgVar locid -> ArgVar (intern_hyp ist locid) | ArgArg _ as x -> x -let loc_of_by_notation f = function - | AN c -> f c - | ByNotation (loc,s,_) -> loc - -let destIndRef = function IndRef ind -> ind | _ -> failwith "destIndRef" - -let intern_inductive_or_by_notation = function - | AN r -> Nametab.global_inductive r - | ByNotation (loc,ntn,sc) -> - destIndRef (Notation.interp_notation_as_global_reference loc - (function IndRef ind -> true | _ -> false) ntn sc) +let intern_inductive_or_by_notation = smart_global_inductive let intern_inductive ist = function | AN (Ident (loc,id)) when find_var id ist -> ArgVar (loc,id) diff --git a/toplevel/command.ml b/toplevel/command.ml index 82fd9bc1a..80de34458 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -46,6 +46,7 @@ open Goptions open Mod_subst open Evd open Decls +open Smartlocate let rec abstract_constr_expr c = function | [] -> c @@ -930,8 +931,8 @@ requested let l1,l2 = split_scheme q in ( match t with | InductionScheme (x,y,z) -> - let ind = mkInd (Nametab.global_inductive y) in - let sort_of_ind = family_of_sort (Typing.sort_of env Evd.empty ind) + let ind = smart_global_inductive y in + let sort_of_ind = Retyping.get_sort_family_of env Evd.empty (mkInd ind) in let z' = family_of_sort (interp_sort z) in let suffix = ( @@ -955,8 +956,8 @@ in | InSet -> "_rec_nodep" | InType -> "_rect_nodep") ) in - let newid = (string_of_id (coerce_reference_to_id y))^suffix in - let newref = (dummy_loc,id_of_string newid) in + let newid = add_suffix (basename_of_global (IndRef ind)) suffix in + let newref = (dummy_loc,newid) in ((newref,x,y,z)::l1),l2 | EqualityScheme x -> l1,(x::l2) ) @@ -969,7 +970,7 @@ let build_induction_scheme lnamedepindsort = let lrecspec = List.map (fun (_,dep,indid,sort) -> - let ind = Nametab.global_inductive indid in + let ind = smart_global_inductive indid in let (mib,mip) = Global.lookup_inductive ind in (ind,mib,mip,dep,interp_elimination_sort sort)) lnamedepindsort @@ -998,7 +999,7 @@ tried to declare different schemes at once *) else ( if ischeme <> [] then build_induction_scheme ischeme; List.iter ( fun indname -> - let ind = Nametab.global_inductive indname + let ind = smart_global_inductive indname in declare_eq_scheme (fst ind); try make_eq_decidability ind diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml index adf3e93a4..54cbc0ae3 100644 --- a/toplevel/metasyntax.ml +++ b/toplevel/metasyntax.ml @@ -240,8 +240,6 @@ let parse_format (loc,str) = type symbol_token = WhiteSpace of int | String of string -(* Decompose the notation string into tokens *) - let split_notation_string str = let push_token beg i l = if beg = i then l else @@ -307,10 +305,6 @@ let rec interp_list_parser hd = function (* Find non-terminal tokens of notation *) -let unquote_notation_token s = - let n = String.length s in - if n > 2 & s.[0] = '\'' & s.[n-1] = '\'' then String.sub s 1 (n-2) else s - let is_normal_token str = try let _ = Lexer.check_ident str in true with Lexer.Error _ -> false @@ -321,26 +315,18 @@ let quote_notation_token x = if (n > 0 & norm) or (n > 2 & x.[0] = '\'') then "'"^x^"'" else x -let rec raw_analyse_notation_tokens = function - | [] -> [], [] - | String ".." :: sl -> - let (vars,l) = raw_analyse_notation_tokens sl in - (list_add_set ldots_var vars, NonTerminal ldots_var :: l) +let rec raw_analyze_notation_tokens = function + | [] -> [] + | String ".." :: sl -> NonTerminal ldots_var :: raw_analyze_notation_tokens sl | String "_" :: _ -> error "_ must be quoted." | String x :: sl when is_normal_token x -> Lexer.check_ident x; - let id = Names.id_of_string x in - let (vars,l) = raw_analyse_notation_tokens sl in - if List.mem id vars then - error ("Variable "^x^" occurs more than once."); - (id::vars, NonTerminal id :: l) + NonTerminal (Names.id_of_string x) :: raw_analyze_notation_tokens sl | String s :: sl -> Lexer.check_keyword s; - let (vars,l) = raw_analyse_notation_tokens sl in - (vars, Terminal (unquote_notation_token s) :: l) + Terminal (drop_simple_quotes s) :: raw_analyze_notation_tokens sl | WhiteSpace n :: sl -> - let (vars,l) = raw_analyse_notation_tokens sl in - (vars, Break n :: l) + Break n :: raw_analyze_notation_tokens sl let is_numeral symbs = match List.filter (function Break _ -> false | _ -> true) symbs with @@ -349,8 +335,23 @@ let is_numeral symbs = | _ -> false -let analyse_notation_tokens l = - let vars,l = raw_analyse_notation_tokens l in +let rec get_notation_vars = function + | [] -> [] + | NonTerminal id :: sl -> + let vars = get_notation_vars sl in + if List.mem id vars then + if id <> ldots_var then + error ("Variable "^string_of_id id^" occurs more than once.") + else + vars + else + id::vars + | (Terminal _ | Break _) :: sl -> get_notation_vars sl + | SProdList _ :: _ -> assert false + +let analyze_notation_tokens l = + let l = raw_analyze_notation_tokens l in + let vars = get_notation_vars l in let extrarecvars,recvars,l = interp_list_parser [] l in (if extrarecvars = [] then [], [], vars, l else extrarecvars, recvars, list_subtract vars recvars, l) @@ -538,7 +539,7 @@ let hunks_of_format (from,(vars,typs)) symfmt = when s' = String.make (String.length s') ' ' -> let symbs, l = aux (symbs,fmt) in symbs, u :: l | Terminal s :: symbs, (UnpTerminal s') :: fmt - when s = unquote_notation_token s' -> + when s = drop_simple_quotes s' -> let symbs, l = aux (symbs,fmt) in symbs, UnpTerminal s :: l | NonTerminal s :: symbs, UnpTerminal s' :: fmt when s = id_of_string s' -> let i = list_index s vars in @@ -829,7 +830,7 @@ let compute_syntax_data (df,modifiers) = (* Notation defaults to NONA *) let assoc = match assoc with None -> Some Gramext.NonA | a -> a in let toks = split_notation_string df in - let (extrarecvars,recvars,vars,symbols) = analyse_notation_tokens toks in + let (extrarecvars,recvars,vars,symbols) = analyze_notation_tokens toks in let ntn_for_interp = make_notation_key symbols in let symbols' = remove_curly_brackets symbols in let need_squash = (symbols <> symbols') in @@ -962,7 +963,7 @@ let add_notation_in_scope local df c mods scope = let add_notation_interpretation_core local df names c scope onlyparse = let dfs = split_notation_string df in - let (extrarecvars,recvars,vars,symbs) = analyse_notation_tokens dfs in + let (extrarecvars,recvars,vars,symbs) = analyze_notation_tokens dfs in (* Redeclare pa/pp rules *) if not (is_numeral symbs) then begin let sy_rules = recover_notation_syntax (make_notation_key symbs) in @@ -1016,19 +1017,6 @@ let add_infix local (inf,modifiers) pr sc = add_notation local c (df,modifiers) sc (**********************************************************************) -(* Miscellaneous *) - -let standardize_locatable_notation ntn = - let unquote = function - | String s -> [unquote_notation_token s] - | _ -> [] in - if String.contains ntn ' ' then - String.concat " " - (List.flatten (List.map unquote (split_notation_string ntn))) - else - unquote_notation_token ntn - -(**********************************************************************) (* Delimiters and classes bound to scopes *) type scope_command = ScopeDelim of string | ScopeClasses of Classops.cl_typ diff --git a/toplevel/metasyntax.mli b/toplevel/metasyntax.mli index 29dbcb4da..7ebb81867 100644 --- a/toplevel/metasyntax.mli +++ b/toplevel/metasyntax.mli @@ -53,10 +53,6 @@ val add_syntax_extension : val print_grammar : string -> unit -(* Removes quotes in a notation *) - -val standardize_locatable_notation : string -> string - (* Evaluate whether a notation is not printable *) val is_not_printable : aconstr -> bool diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 739193f51..887d5a616 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -44,7 +44,7 @@ type pcoq_hook = { solve : int -> unit; abort : string -> unit; search : searchable -> dir_path list * bool -> unit; - print_name : reference -> unit; + print_name : reference Genarg.or_by_notation -> unit; print_check : Environ.env -> Environ.unsafe_judgment -> unit; print_eval : Reductionops.reduction_function -> Environ.env -> Evd.evar_map -> constr_expr -> Environ.unsafe_judgment -> unit; @@ -59,7 +59,7 @@ let set_pcoq_hook f = pcoq := Some f let cl_of_qualid = function | FunClass -> Classops.CL_FUN | SortClass -> Classops.CL_SORT - | RefClass r -> Class.class_of_global (global_with_alias r) + | RefClass r -> Class.class_of_global (Smartlocate.smart_global r) (*******************) (* "Show" commands *) @@ -278,9 +278,9 @@ let print_located_module r = str "No module is referred to by name ") ++ pr_qualid qid in msgnl msg -let global_with_alias r = - let gr = global_with_alias r in - Dumpglob.add_glob (loc_of_reference r) gr; +let smart_global r = + let gr = Smartlocate.smart_global r in + Dumpglob.add_glob (Genarg.loc_of_or_by_notation loc_of_reference r) gr; gr (**********) @@ -296,7 +296,7 @@ let vernac_bind_scope sc cll = let vernac_open_close_scope = Notation.open_close_scope let vernac_arguments_scope local r scl = - Notation.declare_arguments_scope local (global_with_alias r) scl + Notation.declare_arguments_scope local (smart_global r) scl let vernac_infix = Metasyntax.add_infix @@ -596,14 +596,14 @@ let vernac_require import _ qidl = (* Coercions and canonical structures *) let vernac_canonical r = - Recordops.declare_canonical_structure (global_with_alias r) + Recordops.declare_canonical_structure (smart_global r) let vernac_coercion stre ref qids qidt = let target = cl_of_qualid qidt in let source = cl_of_qualid qids in - let ref' = global_with_alias ref in + let ref' = smart_global ref in Class.try_add_new_coercion_with_target ref' stre source target; - if_verbose message ((string_of_reference ref) ^ " is now a coercion") + if_verbose msgnl (pr_global ref' ++ str " is now a coercion") let vernac_identity_coercion stre id qids qidt = let target = cl_of_qualid qidt in @@ -764,10 +764,10 @@ let vernac_syntactic_definition lid = let vernac_declare_implicits local r = function | Some imps -> - Impargs.declare_manual_implicits local (global_with_alias r) ~enriching:false + Impargs.declare_manual_implicits local (smart_global r) ~enriching:false (List.map (fun (ex,b,f) -> ex, (b,true,f)) imps) | None -> - Impargs.declare_implicits local (global_with_alias r) + Impargs.declare_implicits local (smart_global r) let vernac_reserve idl c = let t = Constrintern.interp_type Evd.empty (Global.env()) c in @@ -975,7 +975,7 @@ let _ = let vernac_set_opacity local str = let glob_ref r = - match global_with_alias r with + match smart_global r with | ConstRef sp -> EvalConstRef sp | VarRef id -> EvalVarRef id | _ -> error @@ -1064,11 +1064,10 @@ let vernac_print = function | PrintName qid -> if !pcoq <> None then (Option.get !pcoq).print_name qid else msg (print_name qid) - | PrintOpaqueName qid -> msg (print_opaque_name qid) | PrintGraph -> ppnl (Prettyp.print_graph()) | PrintClasses -> ppnl (Prettyp.print_classes()) | PrintTypeClasses -> ppnl (Prettyp.print_typeclasses()) - | PrintInstances c -> ppnl (Prettyp.print_instances (global c)) + | PrintInstances c -> ppnl (Prettyp.print_instances (smart_global c)) | PrintLtac qid -> ppnl (Tacinterp.print_ltac (snd (qualid_of_reference qid))) | PrintCoercions -> ppnl (Prettyp.print_coercions()) | PrintCoercionPaths (cls,clt) -> @@ -1076,7 +1075,7 @@ let vernac_print = function | PrintCanonicalConversions -> ppnl (Prettyp.print_canonical_projections ()) | PrintUniverses None -> pp (Univ.pr_universes (Global.universes ())) | PrintUniverses (Some s) -> dump_universes s - | PrintHint r -> Auto.print_hint_ref (global_with_alias r) + | PrintHint r -> Auto.print_hint_ref (smart_global r) | PrintHintGoal -> Auto.print_applicable_hint () | PrintHintDbName s -> Auto.print_hint_db_by_name s | PrintRewriteHintDbName s -> Autorewrite.print_rewrite_hintdb s @@ -1091,7 +1090,7 @@ let vernac_print = function | PrintImplicit qid -> msg (print_impargs qid) (*spiwack: prints all the axioms and section variables used by a term *) | PrintAssumptions (o,r) -> - let cstr = constr_of_global (global_with_alias r) in + let cstr = constr_of_global (smart_global r) in let nassumptions = Environ.assumptions (Conv_oracle.get_transp_state ()) ~add_opaque:o cstr (Global.env ()) in msg (Printer.pr_assumptionset (Global.env ()) nassumptions) @@ -1144,13 +1143,14 @@ let vernac_search s r = Search.search_about (List.map (on_snd interp_search_about_item) sl) r let vernac_locate = function - | LocateTerm qid -> msgnl (print_located_qualid qid) + | LocateTerm (Genarg.AN qid) -> msgnl (print_located_qualid qid) + | LocateTerm (Genarg.ByNotation (_,ntn,sc)) -> + ppnl + (Notation.locate_notation + (Constrextern.without_symbols pr_lrawconstr) ntn sc) | LocateLibrary qid -> print_located_library qid | LocateModule qid -> print_located_module qid | LocateFile f -> locate_file f - | LocateNotation ntn -> - ppnl (Notation.locate_notation (Constrextern.without_symbols pr_lrawconstr) - (Metasyntax.standardize_locatable_notation ntn)) (********************) (* Proof management *) diff --git a/toplevel/vernacentries.mli b/toplevel/vernacentries.mli index 6cbb53617..300ff44f8 100644 --- a/toplevel/vernacentries.mli +++ b/toplevel/vernacentries.mli @@ -38,7 +38,7 @@ type pcoq_hook = { solve : int -> unit; abort : string -> unit; search : searchable -> dir_path list * bool -> unit; - print_name : Libnames.reference -> unit; + print_name : Libnames.reference Genarg.or_by_notation -> unit; print_check : Environ.env -> Environ.unsafe_judgment -> unit; print_eval : Reductionops.reduction_function -> Environ.env -> Evd.evar_map -> constr_expr -> Environ.unsafe_judgment -> unit; diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml index e563f6687..080acc7fc 100644 --- a/toplevel/vernacexpr.ml +++ b/toplevel/vernacexpr.ml @@ -30,7 +30,7 @@ type lname = name located type lstring = string type lreference = reference -type class_rawexpr = FunClass | SortClass | RefClass of reference +type class_rawexpr = FunClass | SortClass | RefClass of reference or_by_notation type printable = | PrintTables @@ -44,18 +44,17 @@ type printable = | PrintModuleType of reference | PrintMLLoadPath | PrintMLModules - | PrintName of reference - | PrintOpaqueName of reference + | PrintName of reference or_by_notation | PrintGraph | PrintClasses | PrintTypeClasses - | PrintInstances of reference + | PrintInstances of reference or_by_notation | PrintLtac of reference | PrintCoercions | PrintCoercionPaths of class_rawexpr * class_rawexpr | PrintCanonicalConversions | PrintUniverses of string option - | PrintHint of reference + | PrintHint of reference or_by_notation | PrintHintGoal | PrintHintDbName of string | PrintRewriteHintDbName of string @@ -63,9 +62,9 @@ type printable = | PrintScopes | PrintScope of string | PrintVisibility of string option - | PrintAbout of reference - | PrintImplicit of reference - | PrintAssumptions of bool * reference + | PrintAbout of reference or_by_notation + | PrintImplicit of reference or_by_notation + | PrintAssumptions of bool * reference or_by_notation type search_about_item = | SearchSubPattern of constr_pattern_expr @@ -78,11 +77,10 @@ type searchable = | SearchAbout of (bool * search_about_item) list type locatable = - | LocateTerm of reference + | LocateTerm of reference or_by_notation | LocateLibrary of reference | LocateModule of reference | LocateFile of string - | LocateNotation of notation type goable = | GoTo of int @@ -188,8 +186,8 @@ type proof_end = | Proved of opacity_flag * (lident * theorem_kind option) option type scheme = - | InductionScheme of bool * lreference * sort_expr - | EqualityScheme of lreference + | InductionScheme of bool * reference or_by_notation * sort_expr + | EqualityScheme of reference or_by_notation type vernac_expr = (* Control *) @@ -204,7 +202,8 @@ type vernac_expr = | VernacOpenCloseScope of (locality_flag * bool * scope_name) | VernacDelimiters of scope_name * lstring | VernacBindScope of scope_name * class_rawexpr list - | VernacArgumentsScope of locality_flag * lreference * scope_name option list + | VernacArgumentsScope of locality_flag * reference or_by_notation * + scope_name option list | VernacInfix of locality_flag * (lstring * syntax_modifier list) * constr_expr * scope_name option | VernacNotation of @@ -232,8 +231,9 @@ type vernac_expr = | VernacRequire of export_flag option * specif_flag option * lreference list | VernacImport of export_flag * lreference list - | VernacCanonical of lreference - | VernacCoercion of locality * lreference * class_rawexpr * class_rawexpr + | VernacCanonical of reference or_by_notation + | VernacCoercion of locality * reference or_by_notation * + class_rawexpr * class_rawexpr | VernacIdentityCoercion of locality * lident * class_rawexpr * class_rawexpr @@ -297,11 +297,11 @@ type vernac_expr = | VernacHints of locality_flag * lstring list * hints_expr | VernacSyntacticDefinition of identifier located * (identifier list * constr_expr) * locality_flag * onlyparsing_flag - | VernacDeclareImplicits of locality_flag * lreference * + | VernacDeclareImplicits of locality_flag * reference or_by_notation * (explicitation * bool * bool) list option | VernacReserve of lident list * constr_expr | VernacSetOpacity of - locality_flag * (Conv_oracle.level * lreference list) list + locality_flag * (Conv_oracle.level * reference or_by_notation list) list | VernacUnsetOption of bool option * Goptions.option_name | VernacSetOption of bool option * Goptions.option_name * option_value | VernacAddOption of Goptions.option_name * option_ref_value list diff --git a/toplevel/whelp.ml4 b/toplevel/whelp.ml4 index b844f03ca..b7db4b431 100644 --- a/toplevel/whelp.ml4 +++ b/toplevel/whelp.ml4 @@ -217,7 +217,7 @@ END VERNAC COMMAND EXTEND Whelp | [ "Whelp" "Locate" string(s) ] -> [ whelp_locate s ] | [ "Whelp" "Locate" preident(s) ] -> [ whelp_locate s ] -| [ "Whelp" "Elim" global(r) ] -> [ whelp_elim (global_inductive_with_alias r) ] +| [ "Whelp" "Elim" global(r) ] -> [ whelp_elim (Smartlocate.global_inductive_with_alias r) ] | [ "Whelp" whelp_constr_request(req) constr(c) ] -> [ whelp_constr_expr req c] END |