aboutsummaryrefslogtreecommitdiff
path: root/vernac
diff options
context:
space:
mode:
Diffstat (limited to 'vernac')
-rw-r--r--vernac/auto_ind_decl.ml2
-rw-r--r--vernac/class.ml13
-rw-r--r--vernac/comProgramFixpoint.ml4
-rw-r--r--vernac/egramcoq.ml133
-rw-r--r--vernac/egramcoq.mli3
-rw-r--r--vernac/egramml.ml9
-rw-r--r--vernac/egramml.mli2
-rw-r--r--vernac/g_vernac.mlg26
-rw-r--r--vernac/himsg.ml31
-rw-r--r--vernac/lemmas.ml18
-rw-r--r--vernac/metasyntax.ml368
-rw-r--r--vernac/metasyntax.mli2
-rw-r--r--vernac/obligations.ml2
-rw-r--r--vernac/ppvernac.ml31
-rw-r--r--vernac/proof_using.ml10
-rw-r--r--vernac/record.ml14
-rw-r--r--vernac/topfmt.ml124
-rw-r--r--vernac/vernacentries.ml132
-rw-r--r--vernac/vernacentries.mli30
-rw-r--r--vernac/vernacexpr.ml5
20 files changed, 675 insertions, 284 deletions
diff --git a/vernac/auto_ind_decl.ml b/vernac/auto_ind_decl.ml
index ee578669c2..e33aa38173 100644
--- a/vernac/auto_ind_decl.ml
+++ b/vernac/auto_ind_decl.ml
@@ -355,7 +355,7 @@ let destruct_ind sigma c =
then avoid should be
[| lb_An ... lb _A1 (resp. bl_An ... bl_A1)
eq_An .... eq_A1 An ... A1 |]
-so from Ai we can find the the correct eq_Ai bl_ai or lb_ai
+so from Ai we can find the correct eq_Ai bl_ai or lb_ai
*)
(* used in the leib -> bool side*)
let do_replace_lb mode lb_scheme_key aavoid narg p q =
diff --git a/vernac/class.ml b/vernac/class.ml
index e425e6474d..614b2181d9 100644
--- a/vernac/class.ml
+++ b/vernac/class.ml
@@ -73,7 +73,7 @@ let check_reference_arity ref =
let check_arity = function
| CL_FUN | CL_SORT -> ()
| CL_CONST cst -> check_reference_arity (ConstRef cst)
- | CL_PROJ cst -> check_reference_arity (ConstRef cst)
+ | CL_PROJ p -> check_reference_arity (ConstRef (Projection.Repr.constant p))
| CL_SECVAR id -> check_reference_arity (VarRef id)
| CL_IND kn -> check_reference_arity (IndRef kn)
@@ -92,8 +92,8 @@ let uniform_cond sigma ctx lt =
let class_of_global = function
| ConstRef sp ->
- if Environ.is_projection sp (Global.env ())
- then CL_PROJ sp else CL_CONST sp
+ (match Recordops.find_primitive_projection sp with
+ | Some p -> CL_PROJ p | None -> CL_CONST sp)
| IndRef sp -> CL_IND sp
| VarRef id -> CL_SECVAR id
| ConstructRef _ as c ->
@@ -143,8 +143,8 @@ let get_target t ind =
CL_FUN
else
match pi1 (find_class_type Evd.empty (EConstr.of_constr t)) with
- | CL_CONST p when Environ.is_projection p (Global.env ()) ->
- CL_PROJ p
+ | CL_CONST p when Recordops.is_primitive_projection p ->
+ CL_PROJ (Option.get @@ Recordops.find_primitive_projection p)
| x -> x
let strength_of_cl = function
@@ -165,7 +165,8 @@ let get_strength stre ref cls clt =
let ident_key_of_class = function
| CL_FUN -> "Funclass"
| CL_SORT -> "Sortclass"
- | CL_CONST sp | CL_PROJ sp -> Label.to_string (Constant.label sp)
+ | CL_CONST sp -> Label.to_string (Constant.label sp)
+ | CL_PROJ sp -> Label.to_string (Projection.Repr.label sp)
| CL_IND (sp,_) -> Label.to_string (MutInd.label sp)
| CL_SECVAR id -> Id.to_string id
diff --git a/vernac/comProgramFixpoint.ml b/vernac/comProgramFixpoint.ml
index eef7afbfba..102a98f046 100644
--- a/vernac/comProgramFixpoint.ml
+++ b/vernac/comProgramFixpoint.ml
@@ -187,7 +187,9 @@ let build_wellfounded (recname,pl,n,bl,arityc,body) poly r measure notation =
let sigma, def =
let sigma, h_a_term = Evarutil.new_global sigma (delayed_force fix_sub_ref) in
let sigma, h_e_term = Evarutil.new_evar env sigma
- ~src:(Loc.tag @@ Evar_kinds.QuestionMark (Evar_kinds.Define false,Anonymous)) wf_proof in
+ ~src:(Loc.tag @@ Evar_kinds.QuestionMark {
+ Evar_kinds.default_question_mark with Evar_kinds.qm_obligation=Evar_kinds.Define false;
+ }) wf_proof in
sigma, mkApp (h_a_term, [| argtyp ; wf_rel ; h_e_term; prop |])
in
let sigma, def = Typing.solve_evars env sigma def in
diff --git a/vernac/egramcoq.ml b/vernac/egramcoq.ml
index 3281b75aaa..16101396cf 100644
--- a/vernac/egramcoq.ml
+++ b/vernac/egramcoq.ml
@@ -54,6 +54,17 @@ let default_pattern_levels =
let default_constr_levels = (default_levels, default_pattern_levels)
+let find_levels levels = function
+ | InConstrEntry -> levels, String.Map.find "constr" levels
+ | InCustomEntry s ->
+ try levels, String.Map.find s levels
+ with Not_found ->
+ String.Map.add s ([],[]) levels, ([],[])
+
+let save_levels levels custom lev =
+ let s = match custom with InConstrEntry -> "constr" | InCustomEntry s -> s in
+ String.Map.add s lev levels
+
(* At a same level, LeftA takes precedence over RightA and NoneA *)
(* In case, several associativity exists for a level, we make two levels, *)
(* first LeftA, then RightA and NoneA together *)
@@ -125,24 +136,24 @@ let rec list_mem_assoc_triple x = function
let register_empty_levels accu forpat levels =
let rec filter accu = function
| [] -> ([], accu)
- | n :: rem ->
+ | (where,n) :: rem ->
let rem, accu = filter accu rem in
- let (clev, plev) = accu in
+ let accu, (clev, plev) = find_levels accu where in
let levels = if forpat then plev else clev in
if not (list_mem_assoc_triple n levels) then
let nlev, ans = find_position_gen levels true None (Some n) in
let nlev = if forpat then (clev, nlev) else (nlev, plev) in
- ans :: rem, nlev
+ (where, ans) :: rem, save_levels accu where nlev
else rem, accu
in
filter accu levels
-let find_position accu forpat assoc level =
- let (clev, plev) = accu in
+let find_position accu custom forpat assoc level =
+ let accu, (clev, plev) = find_levels accu custom in
let levels = if forpat then plev else clev in
let nlev, ans = find_position_gen levels false assoc level in
let nlev = if forpat then (clev, nlev) else (nlev, plev) in
- (ans, nlev)
+ (ans, save_levels accu custom nlev)
(**************************************************************************)
(*
@@ -231,7 +242,7 @@ type (_, _) entry =
| TTName : ('self, lname) entry
| TTReference : ('self, qualid) entry
| TTBigint : ('self, Constrexpr.raw_natural_number) entry
-| TTConstr : prod_info * 'r target -> ('r, 'r) entry
+| TTConstr : notation_entry * prod_info * 'r target -> ('r, 'r) entry
| TTConstrList : prod_info * Tok.t list * 'r target -> ('r, 'r list) entry
| TTPattern : int -> ('self, cases_pattern_expr) entry
| TTOpenBinderList : ('self, local_binder_expr list) entry
@@ -239,17 +250,58 @@ type (_, _) entry =
type _ any_entry = TTAny : ('s, 'r) entry -> 's any_entry
+let constr_custom_entry : (string, Constrexpr.constr_expr) entry_command =
+ create_entry_command "constr" (fun s st -> [s], st)
+let pattern_custom_entry : (string, Constrexpr.cases_pattern_expr) entry_command =
+ create_entry_command "pattern" (fun s st -> [s], st)
+
+let custom_entry_locality = Summary.ref ~name:"LOCAL-CUSTOM-ENTRY" String.Set.empty
+(** If the entry is present then local *)
+
+let create_custom_entry ~local s =
+ if List.mem s ["constr";"pattern";"ident";"global";"binder";"bigint"] then
+ user_err Pp.(quote (str s) ++ str " is a reserved entry name.");
+ let sc = "constr:"^s in
+ let sp = "pattern:"^s in
+ let _ = extend_entry_command constr_custom_entry sc in
+ let _ = extend_entry_command pattern_custom_entry sp in
+ let () = if local then custom_entry_locality := String.Set.add s !custom_entry_locality in
+ ()
+
+let find_custom_entry s =
+ let sc = "constr:"^s in
+ let sp = "pattern:"^s in
+ try (find_custom_entry constr_custom_entry sc, find_custom_entry pattern_custom_entry sp)
+ with Not_found -> user_err Pp.(str "Undeclared custom entry: " ++ str s ++ str ".")
+
+let locality_of_custom_entry s = String.Set.mem s !custom_entry_locality
+
(* This computes the name of the level where to add a new rule *)
-let interp_constr_entry_key : type r. r target -> int -> r Entry.t * int option =
- fun forpat level -> match forpat with
+let interp_constr_entry_key : type r. _ -> r target -> int -> r Entry.t * int option =
+ fun custom forpat level ->
+ match custom with
+ | InCustomEntry s ->
+ (let (entry_for_constr, entry_for_patttern) = find_custom_entry s in
+ match forpat with
+ | ForConstr -> entry_for_constr, Some level
+ | ForPattern -> entry_for_patttern, Some level)
+ | InConstrEntry ->
+ match forpat with
| ForConstr ->
if level = 200 then Constr.binder_constr, None
else Constr.operconstr, Some level
| ForPattern -> Constr.pattern, Some level
-let target_entry : type s. s target -> s Entry.t = function
-| ForConstr -> Constr.operconstr
-| ForPattern -> Constr.pattern
+let target_entry : type s. notation_entry -> s target -> s Entry.t = function
+| InConstrEntry ->
+ (function
+ | ForConstr -> Constr.operconstr
+ | ForPattern -> Constr.pattern)
+| InCustomEntry s ->
+ let (entry_for_constr, entry_for_patttern) = find_custom_entry s in
+ function
+ | ForConstr -> entry_for_constr
+ | ForPattern -> entry_for_patttern
let is_self from e = match e with
| (NumLevel n, BorderProd (Right, _ (* Some(NonA|LeftA) *))) -> false
@@ -273,11 +325,11 @@ let make_sep_rules = function
let r = mkrule (List.rev tkl) in
Arules [r]
-let symbol_of_target : type s. _ -> _ -> _ -> s target -> (s, s) symbol = fun p assoc from forpat ->
- if is_binder_level from p then Aentryl (target_entry forpat, "200")
+let symbol_of_target : type s. _ -> _ -> _ -> _ -> s target -> (s, s) symbol = fun custom p assoc from forpat ->
+ if custom = InConstrEntry && is_binder_level from p then Aentryl (target_entry InConstrEntry forpat, "200")
else if is_self from p then Aself
else
- let g = target_entry forpat in
+ let g = target_entry custom forpat in
let lev = adjust_level assoc from p in
begin match lev with
| None -> Aentry g
@@ -286,11 +338,11 @@ let symbol_of_target : type s. _ -> _ -> _ -> s target -> (s, s) symbol = fun p
end
let symbol_of_entry : type s r. _ -> _ -> (s, r) entry -> (s, r) symbol = fun assoc from typ -> match typ with
-| TTConstr (p, forpat) -> symbol_of_target p assoc from forpat
+| TTConstr (s, p, forpat) -> symbol_of_target s p assoc from forpat
| TTConstrList (typ', [], forpat) ->
- Alist1 (symbol_of_target typ' assoc from forpat)
+ Alist1 (symbol_of_target InConstrEntry typ' assoc from forpat)
| TTConstrList (typ', tkl, forpat) ->
- Alist1sep (symbol_of_target typ' assoc from forpat, make_sep_rules tkl)
+ Alist1sep (symbol_of_target InConstrEntry typ' assoc from forpat, make_sep_rules tkl)
| TTPattern p -> Aentryl (Constr.pattern, string_of_int p)
| TTClosedBinderList [] -> Alist1 (Aentry Constr.binder)
| TTClosedBinderList tkl -> Alist1sep (Aentry Constr.binder, make_sep_rules tkl)
@@ -303,9 +355,8 @@ let interp_entry forpat e = match e with
| ETProdName -> TTAny TTName
| ETProdReference -> TTAny TTReference
| ETProdBigint -> TTAny TTBigint
-| ETProdConstr p -> TTAny (TTConstr (p, forpat))
+| ETProdConstr (s,p) -> TTAny (TTConstr (s, p, forpat))
| ETProdPattern p -> TTAny (TTPattern p)
-| ETProdOther _ -> assert false (** not used *)
| ETProdConstrList (p, tkl) -> TTAny (TTConstrList (p, tkl, forpat))
| ETProdBinderList ETBinderOpen -> TTAny TTOpenBinderList
| ETProdBinderList (ETBinderClosed tkl) -> TTAny (TTClosedBinderList tkl)
@@ -420,21 +471,23 @@ let target_to_bool : type r. r target -> bool = function
| ForConstr -> false
| ForPattern -> true
-let prepare_empty_levels forpat (pos,p4assoc,name,reinit) =
+let prepare_empty_levels forpat (where,(pos,p4assoc,name,reinit)) =
let empty = (pos, [(name, p4assoc, [])]) in
- if forpat then ExtendRule (Constr.pattern, reinit, empty)
- else ExtendRule (Constr.operconstr, reinit, empty)
-
-let rec pure_sublevels : type a b c. int option -> (a, b, c) rule -> int list = fun level r -> match r with
-| Stop -> []
-| Next (rem, Aentryl (_, i)) ->
- let i = int_of_string i in
- let rem = pure_sublevels level rem in
- begin match level with
- | Some j when Int.equal i j -> rem
- | _ -> i :: rem
- end
-| Next (rem, _) -> pure_sublevels level rem
+ ExtendRule (target_entry where forpat, reinit, empty)
+
+let rec pure_sublevels' custom assoc from forpat level = function
+| [] -> []
+| GramConstrNonTerminal (e,_) :: rem ->
+ let rem = pure_sublevels' custom assoc from forpat level rem in
+ let push where p rem =
+ match symbol_of_target custom p assoc from forpat with
+ | Aentryl (_,i) when level <> Some (int_of_string i) -> (where,int_of_string i) :: rem
+ | _ -> rem in
+ (match e with
+ | ETProdPattern i -> push InConstrEntry (NumLevel i,InternalProd) rem
+ | ETProdConstr (s,p) -> push s p rem
+ | _ -> rem)
+| (GramConstrTerminal _ | GramConstrListMark _) :: rem -> pure_sublevels' custom assoc from forpat level rem
let make_act : type r. r target -> _ -> r gen_eval = function
| ForConstr -> fun notation loc env ->
@@ -445,17 +498,17 @@ let make_act : type r. r target -> _ -> r gen_eval = function
CAst.make ~loc @@ CPatNotation (notation, env, [])
let extend_constr state forpat ng =
- let n,_,_ = ng.notgram_level in
+ let custom,n,_,_ = ng.notgram_level in
let assoc = ng.notgram_assoc in
- let (entry, level) = interp_constr_entry_key forpat n in
+ let (entry, level) = interp_constr_entry_key custom forpat n in
let fold (accu, state) pt =
let AnyTyRule r = make_ty_rule assoc n forpat pt in
let symbs = ty_erase r in
- let pure_sublevels = pure_sublevels level symbs in
+ let pure_sublevels = pure_sublevels' custom assoc n forpat level pt in
let isforpat = target_to_bool forpat in
let needed_levels, state = register_empty_levels state isforpat pure_sublevels in
- let (pos,p4assoc,name,reinit), state = find_position state isforpat assoc level in
- let empty_rules = List.map (prepare_empty_levels isforpat) needed_levels in
+ let (pos,p4assoc,name,reinit), state = find_position state custom isforpat assoc level in
+ let empty_rules = List.map (prepare_empty_levels forpat) needed_levels in
let empty = { constrs = []; constrlists = []; binders = []; binderlists = [] } in
let act = ty_eval r (make_act forpat ng.notgram_notation) empty in
let rule = (name, p4assoc, [Rule (symbs, act)]) in
@@ -468,7 +521,7 @@ let constr_levels = GramState.field ()
let extend_constr_notation ng state =
let levels = match GramState.get state constr_levels with
- | None -> default_constr_levels
+ | None -> String.Map.add "constr" default_constr_levels String.Map.empty
| Some lev -> lev
in
(* Add the notation in constr *)
diff --git a/vernac/egramcoq.mli b/vernac/egramcoq.mli
index b0341e6a17..3a6f8ae015 100644
--- a/vernac/egramcoq.mli
+++ b/vernac/egramcoq.mli
@@ -17,3 +17,6 @@
val extend_constr_grammar : Notation_gram.one_notation_grammar -> unit
(** Add a term notation rule to the parsing system. *)
+
+val create_custom_entry : local:bool -> string -> unit
+val locality_of_custom_entry : string -> bool
diff --git a/vernac/egramml.ml b/vernac/egramml.ml
index 048d4d93a0..c5dedc880e 100644
--- a/vernac/egramml.ml
+++ b/vernac/egramml.ml
@@ -64,6 +64,15 @@ let make_rule f prod =
let act = ty_eval ty_rule f in
Extend.Rule (symb, act)
+let rec proj_symbol : type a b c. (a, b, c) ty_user_symbol -> (a, b, c) genarg_type = function
+| TUentry a -> ExtraArg a
+| TUentryl (a,l) -> ExtraArg a
+| TUopt(o) -> OptArg (proj_symbol o)
+| TUlist1 l -> ListArg (proj_symbol l)
+| TUlist1sep (l,_) -> ListArg (proj_symbol l)
+| TUlist0 l -> ListArg (proj_symbol l)
+| TUlist0sep (l,_) -> ListArg (proj_symbol l)
+
(** Vernac grammar extensions *)
let vernac_exts = ref []
diff --git a/vernac/egramml.mli b/vernac/egramml.mli
index a5ee036db5..c4f4fcfaa4 100644
--- a/vernac/egramml.mli
+++ b/vernac/egramml.mli
@@ -26,6 +26,8 @@ val extend_vernac_command_grammar :
val get_extend_vernac_rule : Vernacexpr.extend_name -> vernac_expr grammar_prod_item list
+val proj_symbol : ('a, 'b, 'c) Extend.ty_user_symbol -> ('a, 'b, 'c) Genarg.genarg_type
+
(** Utility function reused in Egramcoq : *)
val make_rule :
diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg
index a35a1998d3..74516e320c 100644
--- a/vernac/g_vernac.mlg
+++ b/vernac/g_vernac.mlg
@@ -59,7 +59,7 @@ let make_bullet s =
| '*' -> Star n
| _ -> assert false
-let parse_compat_version ?(allow_old = true) = let open Flags in function
+let parse_compat_version = let open Flags in function
| "8.8" -> Current
| "8.7" -> V8_7
| "8.6" -> V8_6
@@ -1087,6 +1087,11 @@ GRAMMAR EXTEND Gram
r = red_expr ->
{ VernacDeclareReduction (s,r) }
+(* factorized here, though relevant for syntax extensions *)
+
+ | IDENT "Declare"; IDENT "Custom"; IDENT "Entry"; s = IDENT ->
+ { VernacDeclareCustomEntry s }
+
] ];
END
@@ -1153,6 +1158,9 @@ GRAMMAR EXTEND Gram
;
syntax_modifier:
[ [ "at"; IDENT "level"; n = natural -> { SetLevel n }
+ | "in"; IDENT "custom"; x = IDENT -> { SetCustomEntry (x,None) }
+ | "in"; IDENT "custom"; x = IDENT; "at"; IDENT "level"; n = natural ->
+ { SetCustomEntry (x,Some n) }
| IDENT "left"; IDENT "associativity" -> { SetAssoc LeftA }
| IDENT "right"; IDENT "associativity" -> { SetAssoc RightA }
| IDENT "no"; IDENT "associativity" -> { SetAssoc NonA }
@@ -1166,23 +1174,27 @@ GRAMMAR EXTEND Gram
| { CAst.v = k }, Some s -> SetFormat(k,s)
| s, None -> SetFormat ("text",s) end }
| x = IDENT; ","; l = LIST1 [id = IDENT -> { id } ] SEP ","; "at";
- lev = level -> { SetItemLevel (x::l,lev) }
- | x = IDENT; "at"; lev = level -> { SetItemLevel ([x],lev) }
- | x = IDENT; "at"; lev = level; b = constr_as_binder_kind -> { SetItemLevelAsBinder ([x],b,Some lev) }
- | x = IDENT; b = constr_as_binder_kind -> { SetItemLevelAsBinder ([x],b,None) }
+ lev = level -> { SetItemLevel (x::l,None,Some lev) }
+ | x = IDENT; "at"; lev = level -> { SetItemLevel ([x],None,Some lev) }
+ | x = IDENT; "at"; lev = level; b = constr_as_binder_kind ->
+ { SetItemLevel ([x],Some b,Some lev) }
+ | x = IDENT; b = constr_as_binder_kind -> { SetItemLevel ([x],Some b,None) }
| x = IDENT; typ = syntax_extension_type -> { SetEntryType (x,typ) }
] ]
;
syntax_extension_type:
- [ [ IDENT "ident" -> { ETName } | IDENT "global" -> { ETReference }
+ [ [ IDENT "ident" -> { ETIdent } | IDENT "global" -> { ETGlobal }
| IDENT "bigint" -> { ETBigint }
| IDENT "binder" -> { ETBinder true }
- | IDENT "constr"; n = OPT at_level; b = constr_as_binder_kind -> { ETConstrAsBinder (b,n) }
+ | IDENT "constr" -> { ETConstr (InConstrEntry,None,None) }
+ | IDENT "constr"; n = OPT at_level; b = OPT constr_as_binder_kind -> { ETConstr (InConstrEntry,b,n) }
| IDENT "pattern" -> { ETPattern (false,None) }
| IDENT "pattern"; "at"; IDENT "level"; n = natural -> { ETPattern (false,Some n) }
| IDENT "strict"; IDENT "pattern" -> { ETPattern (true,None) }
| IDENT "strict"; IDENT "pattern"; "at"; IDENT "level"; n = natural -> { ETPattern (true,Some n) }
| IDENT "closed"; IDENT "binder" -> { ETBinder false }
+ | IDENT "custom"; x = IDENT; n = OPT at_level; b = OPT constr_as_binder_kind ->
+ { ETConstr (InCustomEntry x,b,n) }
] ]
;
at_level:
diff --git a/vernac/himsg.ml b/vernac/himsg.ml
index 534e58f9c9..a4650cfd92 100644
--- a/vernac/himsg.ml
+++ b/vernac/himsg.ml
@@ -194,12 +194,6 @@ let rec pr_disjunction pr = function
| a::l -> pr a ++ str "," ++ spc () ++ pr_disjunction pr l
| [] -> assert false
-let pr_puniverses f env (c,u) =
- f env c ++
- (if Flags.is_universe_polymorphism () && not (Univ.Instance.is_empty u) then
- str"(*" ++ Univ.Instance.pr UnivNames.pr_with_global_universes u ++ str"*)"
- else mt())
-
let explain_elim_arity env sigma ind sorts c pj okinds =
let open EConstr in
let env = make_all_name_different env sigma in
@@ -262,7 +256,7 @@ let explain_ill_formed_branch env sigma c ci actty expty =
let pa, pe = pr_explicit env sigma (simp actty) (simp expty) in
strbrk "In pattern-matching on term" ++ brk(1,1) ++ pc ++
spc () ++ strbrk "the branch for constructor" ++ spc () ++
- quote (pr_puniverses pr_constructor env ci) ++
+ quote (pr_pconstructor env sigma ci) ++
spc () ++ str "has type" ++ brk(1,1) ++ pa ++ spc () ++
str "which should be" ++ brk(1,1) ++ pe ++ str "."
@@ -520,11 +514,15 @@ let pr_trailing_ne_context_of env sigma =
then str "."
else (str " in environment:"++ pr_context_unlimited env sigma)
-let rec explain_evar_kind env sigma evk ty = function
+let rec explain_evar_kind env sigma evk ty =
+ let open Evar_kinds in
+ function
| Evar_kinds.NamedHole id ->
strbrk "the existential variable named " ++ Id.print id
- | Evar_kinds.QuestionMark _ ->
+ | Evar_kinds.QuestionMark {qm_record_field=None} ->
strbrk "this placeholder of type " ++ ty
+ | Evar_kinds.QuestionMark {qm_record_field=Some {fieldname; recordname}} ->
+ str "field " ++ (Printer.pr_constant env fieldname) ++ str " of record " ++ (Printer.pr_inductive env recordname)
| Evar_kinds.CasesType false ->
strbrk "the type of this pattern-matching problem"
| Evar_kinds.CasesType true ->
@@ -681,6 +679,11 @@ let explain_unsatisfied_constraints env sigma cst =
Univ.pr_constraints (Termops.pr_evd_level sigma) cst ++
spc () ++ str "(maybe a bugged tactic)."
+let explain_undeclared_universe env sigma l =
+ strbrk "Undeclared universe: " ++
+ Termops.pr_evd_level sigma l ++
+ spc () ++ str "(maybe a bugged tactic)."
+
let explain_type_error env sigma err =
let env = make_all_name_different env sigma in
match err with
@@ -718,6 +721,8 @@ let explain_type_error env sigma err =
explain_wrong_case_info env ind ci
| UnsatisfiedConstraints cst ->
explain_unsatisfied_constraints env sigma cst
+ | UndeclaredUniverse l ->
+ explain_undeclared_universe env sigma l
let pr_position (cl,pos) =
let clpos = match cl with
@@ -1229,12 +1234,7 @@ let explain_wrong_numarg_inductive env ind n =
str " expects " ++ decline_string n "argument" ++ str "."
let explain_unused_clause env pats =
-(* Without localisation
- let s = if List.length pats > 1 then "s" else "" in
- (str ("Unused clause with pattern"^s) ++ spc () ++
- hov 0 (pr_sequence pr_cases_pattern pats) ++ str ")")
-*)
- str "This clause is redundant."
+ str "Pattern \"" ++ hov 0 (prlist_with_sep pr_comma pr_cases_pattern pats) ++ strbrk "\" is redundant in this clause."
let explain_non_exhaustive env pats =
str "Non exhaustive pattern-matching: no clause found for " ++
@@ -1306,6 +1306,7 @@ let map_ptype_error f = function
| IllTypedRecBody (n, na, jv, t) ->
IllTypedRecBody (n, na, Array.map (on_judgment f) jv, Array.map f t)
| UnsatisfiedConstraints g -> UnsatisfiedConstraints g
+| UndeclaredUniverse l -> UndeclaredUniverse l
let explain_reduction_tactic_error = function
| Tacred.InvalidAbstraction (env,sigma,c,(env',e)) ->
diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml
index ce74f2344a..880a11becd 100644
--- a/vernac/lemmas.ml
+++ b/vernac/lemmas.ml
@@ -71,17 +71,13 @@ let adjust_guardness_conditions const = function
List.interval 0 (List.length ((lam_assum c))))
lemma_guard (Array.to_list fixdefs) in
*)
- let add c cb e =
- let exists c e =
- try ignore(Environ.lookup_constant c e); true
- with Not_found -> false in
- if exists c e then e else Environ.add_constant c cb e in
- let env = List.fold_left (fun env { eff } ->
- match eff with
- | SEsubproof (c, cb,_) -> add c cb env
- | SEscheme (l,_) ->
- List.fold_left (fun e (_,c,cb,_) -> add c cb e) env l)
- env (Safe_typing.side_effects_of_private_constants eff) in
+ let fold env eff =
+ try
+ let _ = Environ.lookup_constant eff.seff_constant env in
+ env
+ with Not_found -> Environ.add_constant eff.seff_constant eff.seff_body env
+ in
+ let env = List.fold_left fold env (Safe_typing.side_effects_of_private_constants eff) in
let indexes =
search_guard env
possible_indexes fixdecls in
diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml
index 33e6229b29..d66a121437 100644
--- a/vernac/metasyntax.ml
+++ b/vernac/metasyntax.ml
@@ -283,20 +283,30 @@ let error_not_same_scope x y =
(**********************************************************************)
(* Build pretty-printing rules *)
+let pr_notation_entry = function
+ | InConstrEntry -> str "constr"
+ | InCustomEntry s -> str "custom " ++ str s
+
let prec_assoc = function
| RightA -> (L,E)
| LeftA -> (E,L)
| NonA -> (L,L)
-let precedence_of_position_and_level from = function
+let precedence_of_position_and_level from_level = function
| NumLevel n, BorderProd (_,None) -> n, Prec n
| NumLevel n, BorderProd (b,Some a) ->
n, let (lp,rp) = prec_assoc a in if b == Left then lp else rp
| NumLevel n, InternalProd -> n, Prec n
- | NextLevel, _ -> from, L
-
-let precedence_of_entry_type from = function
- | ETConstr x | ETConstrAsBinder (_,x) -> precedence_of_position_and_level from x
+ | NextLevel, _ -> from_level, L
+
+let precedence_of_entry_type (from_custom,from_level) = function
+ | ETConstr (custom,_,x) when notation_entry_eq custom from_custom ->
+ precedence_of_position_and_level from_level x
+ | ETConstr (custom,_,(NumLevel n,_)) -> n, Prec n
+ | ETConstr (custom,_,(NextLevel,_)) ->
+ user_err (strbrk "\"next level\" is only for sub-expressions in the same entry as where the notation is (" ++
+ quote (pr_notation_entry custom) ++ strbrk " is different from " ++
+ quote (pr_notation_entry from_custom) ++ str ").")
| ETPattern (_,n) -> let n = match n with None -> 0 | Some n -> n in n, Prec n
| _ -> 0, E (* should not matter *)
@@ -367,15 +377,14 @@ let unparsing_metavar i from typs =
let x = List.nth typs (i-1) in
let prec = snd (precedence_of_entry_type from x) in
match x with
- | ETConstr _ | ETConstrAsBinder _ | ETReference | ETBigint ->
+ | ETConstr _ | ETGlobal | ETBigint ->
UnpMetaVar (i,prec)
| ETPattern _ ->
UnpBinderMetaVar (i,prec)
- | ETName ->
- UnpBinderMetaVar (i,Prec 0)
+ | ETIdent ->
+ UnpBinderMetaVar (i,prec)
| ETBinder isopen ->
assert false
- | ETOther _ -> failwith "TODO"
(* Heuristics for building default printing rules *)
@@ -561,11 +570,10 @@ let hunks_of_format (from,(vars,typs)) symfmt =
(**********************************************************************)
(* Build parsing rules *)
-let assoc_of_type n (_,typ) = precedence_of_entry_type n typ
+let assoc_of_type from n (_,typ) = precedence_of_entry_type (from,n) typ
let is_not_small_constr = function
ETProdConstr _ -> true
- | ETProdOther("constr","binder_constr") -> true
| _ -> false
let rec define_keywords_aux = function
@@ -595,9 +603,9 @@ let distribute a ll = List.map (fun l -> a @ l) ll
t;sep;t;...;t;sep;t;...;t;sep;t (p+n times)
t;sep;t;...;t;sep;t;...;t;sep;t;LIST1(t,sep) *)
-let expand_list_rule typ tkl x n p ll =
+let expand_list_rule s typ tkl x n p ll =
let camlp5_message_name = Some (add_suffix x ("_"^string_of_int n)) in
- let main = GramConstrNonTerminal (ETProdConstr typ, camlp5_message_name) in
+ let main = GramConstrNonTerminal (ETProdConstr (s,typ), camlp5_message_name) in
let tks = List.map (fun x -> GramConstrTerminal x) tkl in
let rec aux i hds ll =
if i < p then aux (i+1) (main :: tks @ hds) ll
@@ -613,7 +621,7 @@ let expand_list_rule typ tkl x n p ll =
let is_constr_typ typ x etyps =
match List.assoc x etyps with
- | ETConstr typ' | ETConstrAsBinder (_,typ') -> typ = typ'
+ | ETConstr (_,_,typ') -> typ = typ'
| _ -> false
let include_possible_similar_trailing_pattern typ etyps sl l =
@@ -627,13 +635,12 @@ let include_possible_similar_trailing_pattern typ etyps sl l =
try_aux 0 l
let prod_entry_type = function
- | ETName -> ETProdName
- | ETReference -> ETProdReference
+ | ETIdent -> ETProdName
+ | ETGlobal -> ETProdReference
| ETBigint -> ETProdBigint
| ETBinder _ -> assert false (* See check_binder_type *)
- | ETConstr p | ETConstrAsBinder (_,p) -> ETProdConstr p
+ | ETConstr (s,_,p) -> ETProdConstr (s,p)
| ETPattern (_,n) -> ETProdPattern (match n with None -> 0 | Some n -> n)
- | ETOther (s,t) -> ETProdOther (s,t)
let make_production etyps symbols =
let rec aux = function
@@ -651,9 +658,9 @@ let make_production etyps symbols =
| Break _ -> []
| _ -> anomaly (Pp.str "Found a non terminal token in recursive notation separator.")) sl) in
match List.assoc x etyps with
- | ETConstr typ ->
+ | ETConstr (s,_,typ) ->
let p,l' = include_possible_similar_trailing_pattern typ etyps sl l in
- expand_list_rule typ tkl x 1 p (aux l')
+ expand_list_rule s typ tkl x 1 p (aux l')
| ETBinder o ->
check_open_binder o sl x;
let typ = if o then (assert (tkl = []); ETBinderOpen) else ETBinderClosed tkl in
@@ -675,8 +682,7 @@ let rec find_symbols c_current c_next c_last = function
(x,c_next)::(find_symbols c_next c_next c_last sl')
let border = function
- | (_,ETConstr(_,BorderProd (_,a))) :: _ -> a
- | (_,(ETConstrAsBinder(_,(_,BorderProd (_,a))))) :: _ -> a
+ | (_,(ETConstr(_,_,(_,BorderProd (_,a))))) :: _ -> a
| _ -> None
let recompute_assoc typs =
@@ -698,23 +704,24 @@ let pr_arg_level from (lev,typ) =
| (n,_) -> str "Unknown level" in
Ppvernac.pr_set_entry_type (fun _ -> (*TO CHECK*) mt()) typ ++
(match typ with
- | ETConstr _ | ETConstrAsBinder _ | ETPattern _ -> spc () ++ pplev lev
+ | ETConstr _ | ETPattern _ -> spc () ++ pplev lev
| _ -> mt ())
-let pr_level ntn (from,args,typs) =
- str "at level " ++ int from ++ spc () ++ str "with arguments" ++ spc() ++
- prlist_with_sep pr_comma (pr_arg_level from) (List.combine args typs)
+let pr_level ntn (from,fromlevel,args,typs) =
+ (match from with InConstrEntry -> mt () | InCustomEntry s -> str "in " ++ str s ++ spc()) ++
+ str "at level " ++ int fromlevel ++ spc () ++ str "with arguments" ++ spc() ++
+ prlist_with_sep pr_comma (pr_arg_level fromlevel) (List.combine args typs)
let error_incompatible_level ntn oldprec prec =
user_err
- (str "Notation " ++ qstring ntn ++ str " is already defined" ++ spc() ++
+ (str "Notation " ++ pr_notation ntn ++ str " is already defined" ++ spc() ++
pr_level ntn oldprec ++
spc() ++ str "while it is now required to be" ++ spc() ++
pr_level ntn prec ++ str ".")
let error_parsing_incompatible_level ntn ntn' oldprec prec =
user_err
- (str "Notation " ++ qstring ntn ++ str " relies on a parsing rule for " ++ qstring ntn' ++ spc() ++
+ (str "Notation " ++ pr_notation ntn ++ str " relies on a parsing rule for " ++ pr_notation ntn' ++ spc() ++
str " which is already defined" ++ spc() ++
pr_level ntn oldprec ++
spc() ++ str "while it is now required to be" ++ spc() ++
@@ -738,7 +745,7 @@ type syntax_extension_obj = locality_flag * syntax_extension
let check_and_extend_constr_grammar ntn rule =
try
let ntn_for_grammar = rule.notgram_notation in
- if String.equal ntn ntn_for_grammar then raise Not_found;
+ if notation_eq ntn ntn_for_grammar then raise Not_found;
let prec = rule.notgram_level in
let oldprec = Notgram_ops.level_of_notation ntn_for_grammar in
if not (Notgram_ops.level_eq prec oldprec) then error_parsing_incompatible_level ntn ntn_for_grammar oldprec prec;
@@ -760,7 +767,7 @@ let cache_one_syntax_extension se =
if not onlyprint then List.iter (check_and_extend_constr_grammar ntn) se.synext_notgram.notgram_rules;
(* Declare the notation rule *)
declare_notation_rule ntn
- ~extra:se.synext_extra (se.synext_unparsing, pi1 prec) se.synext_notgram
+ ~extra:se.synext_extra (se.synext_unparsing, let (_,lev,_,_) = prec in lev) se.synext_notgram
end
let cache_syntax_extension (_, (_, sy)) =
@@ -797,7 +804,9 @@ module NotationMods = struct
type notation_modifier = {
assoc : gram_assoc option;
level : int option;
+ custom : notation_entry;
etyps : (Id.t * simple_constr_prod_entry_key) list;
+ subtyps : (Id.t * production_level) list;
(* common to syn_data below *)
only_parsing : bool;
@@ -810,7 +819,9 @@ type notation_modifier = {
let default = {
assoc = None;
level = None;
+ custom = InConstrEntry;
etyps = [];
+ subtyps = [];
only_parsing = false;
only_printing = false;
compat = None;
@@ -821,53 +832,75 @@ let default = {
end
let interp_modifiers modl = let open NotationMods in
- let rec interp acc = function
- | [] -> acc
+ let rec interp subtyps acc = function
+ | [] -> subtyps, acc
| SetEntryType (s,typ) :: l ->
let id = Id.of_string s in
if Id.List.mem_assoc id acc.etyps then
user_err ~hdr:"Metasyntax.interp_modifiers"
(str s ++ str " is already assigned to an entry or constr level.");
- interp { acc with etyps = (id,typ) :: acc.etyps; } l
- | SetItemLevel ([],n) :: l ->
- interp acc l
- | SetItemLevelAsBinder ([],_,_) :: l ->
- interp acc l
- | SetItemLevel (s::idl,n) :: l ->
+ interp subtyps { acc with etyps = (id,typ) :: acc.etyps; } l
+ | SetItemLevel ([],bko,n) :: l ->
+ interp subtyps acc l
+ | SetItemLevel (s::idl,bko,n) :: l ->
let id = Id.of_string s in
if Id.List.mem_assoc id acc.etyps then
user_err ~hdr:"Metasyntax.interp_modifiers"
(str s ++ str " is already assigned to an entry or constr level.");
- let typ = ETConstr (Some n) in
- interp { acc with etyps = (id,typ)::acc.etyps; } (SetItemLevel (idl,n)::l)
- | SetItemLevelAsBinder (s::idl,bk,n) :: l ->
- let id = Id.of_string s in
- if Id.List.mem_assoc id acc.etyps then
- user_err ~hdr:"Metasyntax.interp_modifiers"
- (str s ++ str " is already assigned to an entry or constr level.");
- let typ = ETConstrAsBinder (bk,n) in
- interp { acc with etyps = (id,typ)::acc.etyps; } (SetItemLevelAsBinder (idl,bk,n)::l)
+ interp ((id,bko,n)::subtyps) acc (SetItemLevel (idl,bko,n)::l)
| SetLevel n :: l ->
- interp { acc with level = Some n; } l
+ (match acc.custom with
+ | InCustomEntry s ->
+ if acc.level <> None then
+ user_err (str ("isolated \"at level " ^ string_of_int n ^ "\" unexpected."))
+ else
+ user_err (str ("use \"in custom " ^ s ^ " at level " ^ string_of_int n ^
+ "\"") ++ spc () ++ str "rather than" ++ spc () ++
+ str ("\"at level " ^ string_of_int n ^ "\"") ++
+ spc () ++ str "isolated.")
+ | InConstrEntry ->
+ if acc.level <> None then
+ user_err (str "A level is already assigned.");
+ interp subtyps { acc with level = Some n; } l)
+ | SetCustomEntry (s,n) :: l ->
+ if acc.level <> None then
+ (if n = None then
+ user_err (str ("use \"in custom " ^ s ^ " at level " ^
+ string_of_int (Option.get acc.level) ^
+ "\"") ++ spc () ++ str "rather than" ++ spc () ++
+ str ("\"at level " ^
+ string_of_int (Option.get acc.level) ^ "\"") ++
+ spc () ++ str "isolated.")
+ else
+ user_err (str ("isolated \"at level " ^ string_of_int (Option.get acc.level) ^ "\" unexpected.")));
+ if acc.custom <> InConstrEntry then
+ user_err (str "Entry is already assigned to custom " ++ str s ++ (match acc.level with None -> mt () | Some lev -> str " at level " ++ int lev) ++ str ".");
+ interp subtyps { acc with custom = InCustomEntry s; level = n } l
| SetAssoc a :: l ->
if not (Option.is_empty acc.assoc) then user_err Pp.(str "An associativity is given more than once.");
- interp { acc with assoc = Some a; } l
+ interp subtyps { acc with assoc = Some a; } l
| SetOnlyParsing :: l ->
- interp { acc with only_parsing = true; } l
+ interp subtyps { acc with only_parsing = true; } l
| SetOnlyPrinting :: l ->
- interp { acc with only_printing = true; } l
+ interp subtyps { acc with only_printing = true; } l
| SetCompatVersion v :: l ->
- interp { acc with compat = Some v; } l
+ interp subtyps { acc with compat = Some v; } l
| SetFormat ("text",s) :: l ->
if not (Option.is_empty acc.format) then user_err Pp.(str "A format is given more than once.");
- interp { acc with format = Some s; } l
- | SetFormat (k,{CAst.v=s}) :: l ->
- interp { acc with extra = (k,s)::acc.extra; } l
- in interp default modl
+ interp subtyps { acc with format = Some s; } l
+ | SetFormat (k,s) :: l ->
+ interp subtyps { acc with extra = (k,s.CAst.v)::acc.extra; } l
+ in
+ let subtyps,mods = interp [] default modl in
+ (* interpret item levels wrt to main entry *)
+ let extra_etyps = List.map (fun (id,bko,n) -> (id,ETConstr (mods.custom,bko,n))) subtyps in
+ { mods with etyps = extra_etyps@mods.etyps }
let check_infix_modifiers modifiers =
- let t = (interp_modifiers modifiers).NotationMods.etyps in
- if not (List.is_empty t) then
+ let mods = interp_modifiers modifiers in
+ let t = mods.NotationMods.etyps in
+ let u = mods.NotationMods.subtyps in
+ if not (List.is_empty t) || not (List.is_empty u) then
user_err Pp.(str "Explicit entry level or type unexpected in infix notation.")
let check_useless_entry_types recvars mainvars etyps =
@@ -908,21 +941,18 @@ let get_compat_version mods =
(* Compute precedences from modifiers (or find default ones) *)
-let set_entry_type etyps (x,typ) =
+let set_entry_type from etyps (x,typ) =
let typ = try
match List.assoc x etyps, typ with
- | ETConstr (Some n), (_,BorderProd (left,_)) ->
- ETConstr (n,BorderProd (left,None))
- | ETConstr (Some n), (_,InternalProd) -> ETConstr (n,InternalProd)
- | ETConstrAsBinder (bk, Some n), (_,BorderProd (left,_)) ->
- ETConstrAsBinder (bk, (n,BorderProd (left,None)))
- | ETConstrAsBinder (bk, Some n), (_,InternalProd) ->
- ETConstrAsBinder (bk, (n,InternalProd))
+ | ETConstr (s,bko,Some n), (_,BorderProd (left,_)) ->
+ ETConstr (s,bko,(n,BorderProd (left,None)))
+ | ETConstr (s,bko,Some n), (_,InternalProd) ->
+ ETConstr (s,bko,(n,InternalProd))
| ETPattern (b,n), _ -> ETPattern (b,n)
- | (ETName | ETBigint | ETReference | ETBinder _ | ETOther _ as x), _ -> x
- | ETConstr None, _ -> ETConstr typ
- | ETConstrAsBinder (bk,None), _ -> ETConstrAsBinder (bk,typ)
- with Not_found -> ETConstr typ
+ | (ETIdent | ETBigint | ETGlobal | ETBinder _ as x), _ -> x
+ | ETConstr (s,bko,None), _ -> ETConstr (s,bko,typ)
+ with Not_found ->
+ ETConstr (from,None,typ)
in (x,typ)
let join_auxiliary_recursive_types recvars etyps =
@@ -942,8 +972,8 @@ let join_auxiliary_recursive_types recvars etyps =
let internalization_type_of_entry_type = function
| ETBinder _ -> NtnInternTypeOnlyBinder
- | ETConstr _ | ETConstrAsBinder _ | ETBigint | ETReference
- | ETName | ETPattern _ | ETOther _ -> NtnInternTypeAny
+ | ETConstr _ | ETBigint | ETGlobal
+ | ETIdent | ETPattern _ -> NtnInternTypeAny
let set_internalization_type typs =
List.map (fun (_, e) -> internalization_type_of_entry_type e) typs
@@ -954,20 +984,28 @@ let make_internalization_vars recvars mainvars typs =
maintyps @ extratyps
let make_interpretation_type isrec isonlybinding = function
- | ETConstr _ ->
- if isrec then NtnTypeConstrList else
- if isonlybinding then
- (* Parsed as constr, but interpreted as a binder: default is to parse it as an ident only *)
- NtnTypeBinder (NtnBinderParsedAsConstr AsIdent)
- else NtnTypeConstr
- | ETConstrAsBinder (bk,_) -> NtnTypeBinder (NtnBinderParsedAsConstr bk)
- | ETName -> NtnTypeBinder NtnParsedAsIdent
+ (* Parsed as constr list *)
+ | ETConstr (_,None,_) when isrec -> NtnTypeConstrList
+ (* Parsed as constr, but interpreted as a binder: default is to parse it as an ident only *)
+ | ETConstr (_,Some bk,_) -> NtnTypeBinder (NtnBinderParsedAsConstr bk)
+ | ETConstr (_,None,_) when isonlybinding -> NtnTypeBinder (NtnBinderParsedAsConstr AsIdent)
+ (* Parsed as constr, interpreted as constr *)
+ | ETConstr (_,None,_) -> NtnTypeConstr
+ (* Others *)
+ | ETIdent -> NtnTypeBinder NtnParsedAsIdent
| ETPattern (ppstrict,_) -> NtnTypeBinder (NtnParsedAsPattern ppstrict) (* Parsed as ident/pattern, primarily interpreted as binder; maybe strict at printing *)
- | ETBigint | ETReference | ETOther _ -> NtnTypeConstr
+ | ETBigint | ETGlobal -> NtnTypeConstr
| ETBinder _ ->
if isrec then NtnTypeBinderList
else anomaly Pp.(str "Type binder is only for use in recursive notations for binders.")
+let subentry_of_constr_prod_entry = function
+ | ETConstr (InCustomEntry s,_,(NumLevel n,_)) -> InCustomEntryLevel (s,n)
+ (* level and use of parentheses for coercion is hard-wired for "constr";
+ we don't remember the level *)
+ | ETConstr (InConstrEntry,_,_) -> InConstrEntrySomeLevel
+ | _ -> InConstrEntrySomeLevel
+
let make_interpretation_vars recvars allvars typs =
let eq_subscope (sc1, l1) (sc2, l2) =
Option.equal String.equal sc1 sc2 &&
@@ -983,7 +1021,9 @@ let make_interpretation_vars recvars allvars typs =
let mainvars =
Id.Map.filter (fun x _ -> not (Id.List.mem x useless_recvars)) allvars in
Id.Map.mapi (fun x (isonlybinding, sc) ->
- (sc, make_interpretation_type (Id.List.mem_assoc x recvars) isonlybinding (Id.List.assoc x typs))) mainvars
+ let typ = Id.List.assoc x typs in
+ ((subentry_of_constr_prod_entry typ,sc),
+ make_interpretation_type (Id.List.mem_assoc x recvars) isonlybinding typ)) mainvars
let check_rule_productivity l =
if List.for_all (function NonTerminal _ | Break _ -> true | _ -> false) l then
@@ -1009,17 +1049,42 @@ let warn_non_reversible_notation =
str " not occur in the right-hand side." ++ spc() ++
strbrk "The notation will not be used for printing as it is not reversible.")
-let is_not_printable onlyparse reversibility = function
-| NVar _ ->
- if not onlyparse then warn_notation_bound_to_variable ();
- true
+let make_custom_entry custom level =
+ match custom with
+ | InConstrEntry -> InConstrEntrySomeLevel
+ | InCustomEntry s -> InCustomEntryLevel (s,level)
+
+type entry_coercion_kind =
+ | IsEntryCoercion of notation_entry_level
+ | IsEntryGlobal of string * int
+ | IsEntryIdent of string * int
+
+let is_coercion = function
+ | Some (custom,n,_,[e]) ->
+ (match e, custom with
+ | ETConstr _, _ ->
+ let customkey = make_custom_entry custom n in
+ let subentry = subentry_of_constr_prod_entry e in
+ if notation_entry_level_eq subentry customkey then None
+ else Some (IsEntryCoercion subentry)
+ | ETGlobal, InCustomEntry s -> Some (IsEntryGlobal (s,n))
+ | ETIdent, InCustomEntry s -> Some (IsEntryIdent (s,n))
+ | _ -> None)
+ | Some _ -> assert false
+ | None -> None
+
+let printability level onlyparse reversibility = function
+| NVar _ when reversibility = APrioriReversible ->
+ let coe = is_coercion level in
+ if not onlyparse && coe = None then
+ warn_notation_bound_to_variable ();
+ true, coe
| _ ->
- if not onlyparse && reversibility <> APrioriReversible then
+ (if not onlyparse && reversibility <> APrioriReversible then
(warn_non_reversible_notation reversibility; true)
- else onlyparse
+ else onlyparse),None
-
-let find_precedence lev etyps symbols onlyprint =
+let find_precedence custom lev etyps symbols onlyprint =
let first_symbol =
let rec aux = function
| Break _ :: t -> aux t
@@ -1043,10 +1108,9 @@ let find_precedence lev etyps symbols onlyprint =
else [],Option.get lev
else
user_err Pp.(str "The level of the leftmost non-terminal cannot be changed.") in
- (try match List.assoc x etyps with
- | ETConstr _ -> test ()
- | ETConstrAsBinder (_,Some _) -> test ()
- | (ETName | ETBigint | ETReference) ->
+ (try match List.assoc x etyps, custom with
+ | ETConstr (s,_,Some _), s' when s = s' -> test ()
+ | (ETIdent | ETBigint | ETGlobal), _ ->
begin match lev with
| None ->
([Feedback.msg_info ?loc:None ,strbrk "Setting notation at level 0."],0)
@@ -1055,7 +1119,7 @@ let find_precedence lev etyps symbols onlyprint =
| _ ->
user_err Pp.(str "A notation starting with an atomic expression must be at level 0.")
end
- | (ETPattern _ | ETBinder _ | ETOther _ | ETConstrAsBinder _) ->
+ | (ETPattern _ | ETBinder _ | ETConstr _), _ ->
(* Give a default ? *)
if Option.is_empty lev then
user_err Pp.(str "Need an explicit level.")
@@ -1073,7 +1137,7 @@ let find_precedence lev etyps symbols onlyprint =
[],Option.get lev
let check_curly_brackets_notation_exists () =
- try let _ = Notgram_ops.level_of_notation "{ _ }" in ()
+ try let _ = Notgram_ops.level_of_notation (InConstrEntrySomeLevel,"{ _ }") in ()
with Not_found ->
user_err Pp.(str "Notations involving patterns of the form \"{ _ }\" are treated \n\
specially and require that the notation \"{ _ }\" is already reserved.")
@@ -1103,7 +1167,7 @@ let remove_curly_brackets l =
module SynData = struct
- type subentry_types = (Id.t * (production_level * production_position) constr_entry_key_gen) list
+ type subentry_types = (Id.t * constr_entry_key) list
(* XXX: Document *)
type syn_data = {
@@ -1137,7 +1201,7 @@ module SynData = struct
end
-let find_subentry_types n assoc etyps symbols =
+let find_subentry_types from n assoc etyps symbols =
let innerlevel = NumLevel 200 in
let typs =
find_symbols
@@ -1145,11 +1209,21 @@ let find_subentry_types n assoc etyps symbols =
(innerlevel,InternalProd)
(NumLevel n,BorderProd(Right,assoc))
symbols in
- let sy_typs = List.map (set_entry_type etyps) typs in
- let prec = List.map (assoc_of_type n) sy_typs in
+ let sy_typs = List.map (set_entry_type from etyps) typs in
+ let prec = List.map (assoc_of_type from n) sy_typs in
sy_typs, prec
-let compute_syntax_data df modifiers =
+let check_locality_compatibility local custom i_typs =
+ if not local then
+ let subcustom = List.map_filter (function _,ETConstr (InCustomEntry s,_,_) -> Some s | _ -> None) i_typs in
+ let allcustoms = match custom with InCustomEntry s -> s::subcustom | _ -> subcustom in
+ List.iter (fun s ->
+ if Egramcoq.locality_of_custom_entry s then
+ user_err (strbrk "Notation has to be declared local as it depends on custom entry " ++ str s ++
+ strbrk " which is local."))
+ (List.uniquize allcustoms)
+
+let compute_syntax_data local df modifiers =
let open SynData in
let open NotationMods in
let mods = interp_modifiers modifiers in
@@ -1162,25 +1236,28 @@ let compute_syntax_data df modifiers =
let _ = check_binder_type recvars mods.etyps in
(* Notations for interp and grammar *)
- let ntn_for_interp = make_notation_key symbols in
- let symbols_for_grammar = remove_curly_brackets symbols in
+ let msgs,n = find_precedence mods.custom mods.level mods.etyps symbols onlyprint in
+ let custom = make_custom_entry mods.custom n in
+ let ntn_for_interp = make_notation_key custom symbols in
+ let symbols_for_grammar =
+ if custom = InConstrEntrySomeLevel then remove_curly_brackets symbols else symbols in
let need_squash = not (List.equal Notation.symbol_eq symbols symbols_for_grammar) in
- let ntn_for_grammar = if need_squash then make_notation_key symbols_for_grammar else ntn_for_interp in
- if not onlyprint then check_rule_productivity symbols_for_grammar;
- let msgs,n = find_precedence mods.level mods.etyps symbols onlyprint in
+ let ntn_for_grammar = if need_squash then make_notation_key custom symbols_for_grammar else ntn_for_interp in
+ if mods.custom = InConstrEntry && not onlyprint then check_rule_productivity symbols_for_grammar;
(* To globalize... *)
let etyps = join_auxiliary_recursive_types recvars mods.etyps in
let sy_typs, prec =
- find_subentry_types n assoc etyps symbols in
+ find_subentry_types mods.custom n assoc etyps symbols in
let sy_typs_for_grammar, prec_for_grammar =
if need_squash then
- find_subentry_types n assoc etyps symbols_for_grammar
+ find_subentry_types mods.custom n assoc etyps symbols_for_grammar
else
sy_typs, prec in
let i_typs = set_internalization_type sy_typs in
+ check_locality_compatibility local mods.custom sy_typs;
let pa_sy_data = (sy_typs_for_grammar,symbols_for_grammar) in
let pp_sy_data = (sy_typs,symbols) in
- let sy_fulldata = (ntn_for_grammar,(n,prec_for_grammar,List.map snd sy_typs_for_grammar),need_squash) in
+ let sy_fulldata = (ntn_for_grammar,(mods.custom,n,prec_for_grammar,List.map snd sy_typs_for_grammar),need_squash) in
let df' = ((Lib.library_dp(),Lib.current_dirpath true),df) in
let i_data = ntn_for_interp, df' in
@@ -1199,15 +1276,15 @@ let compute_syntax_data df modifiers =
mainvars;
intern_typs = i_typs;
- level = (n,prec,List.map snd sy_typs);
+ level = (mods.custom,n,prec,List.map snd sy_typs);
pa_syntax_data = pa_sy_data;
pp_syntax_data = pp_sy_data;
not_data = sy_fulldata;
}
-let compute_pure_syntax_data df mods =
+let compute_pure_syntax_data local df mods =
let open SynData in
- let sd = compute_syntax_data df mods in
+ let sd = compute_syntax_data local df mods in
let msgs =
if sd.only_parsing then
(Feedback.msg_warning ?loc:None,
@@ -1222,6 +1299,7 @@ type notation_obj = {
notobj_local : bool;
notobj_scope : scope_name option;
notobj_interp : interpretation;
+ notobj_coercion : entry_coercion_kind option;
notobj_onlyparse : bool;
notobj_onlyprint : bool;
notobj_compat : Flags.compat_version option;
@@ -1243,7 +1321,13 @@ let open_notation i (_, nobj) =
let () = Notation.declare_notation_interpretation ntn scope pat df ~onlyprint in
(* Declare the uninterpretation *)
if not nobj.notobj_onlyparse then
- Notation.declare_uninterpretation (NotationRule (scope, ntn)) pat
+ Notation.declare_uninterpretation (NotationRule (scope, ntn)) pat;
+ (* Declare a possible coercion *)
+ (match nobj.notobj_coercion with
+ | Some (IsEntryCoercion entry) -> Notation.declare_entry_coercion ntn entry
+ | Some (IsEntryGlobal (entry,n)) -> Notation.declare_custom_entry_has_global entry n
+ | Some (IsEntryIdent (entry,n)) -> Notation.declare_custom_entry_has_ident entry n
+ | None -> ())
end
let cache_notation o =
@@ -1301,7 +1385,7 @@ let recover_notation_syntax ntn =
raise NoSyntaxRule
let recover_squash_syntax sy =
- let sq = recover_notation_syntax "{ _ }" in
+ let sq = recover_notation_syntax (InConstrEntrySomeLevel,"{ _ }") in
sy :: sq.synext_notgram.notgram_rules
(**********************************************************************)
@@ -1336,8 +1420,9 @@ let make_pp_rule level (typs,symbols) fmt =
(* let make_syntax_rules i_typs (ntn,prec,need_squash) sy_data fmt extra onlyprint compat = *)
let make_syntax_rules (sd : SynData.syn_data) = let open SynData in
let ntn_for_grammar, prec_for_grammar, need_squash = sd.not_data in
+ let custom,level,_,_ = sd.level in
let pa_rule = make_pa_rule prec_for_grammar sd.pa_syntax_data ntn_for_grammar need_squash in
- let pp_rule = make_pp_rule (pi1 sd.level) sd.pp_syntax_data sd.format in {
+ let pp_rule = make_pp_rule (custom,level) sd.pp_syntax_data sd.format in {
synext_level = sd.level;
synext_notation = fst sd.info;
synext_notgram = { notgram_onlyprinting = sd.only_printing; notgram_rules = pa_rule };
@@ -1355,7 +1440,7 @@ let to_map l =
let add_notation_in_scope local df env c mods scope =
let open SynData in
- let sd = compute_syntax_data df mods in
+ let sd = compute_syntax_data local df mods in
(* Prepare the interpretation *)
(* Prepare the parsing and printing rules *)
let sy_rules = make_syntax_rules sd in
@@ -1367,13 +1452,14 @@ let add_notation_in_scope local df env c mods scope =
let (acvars, ac, reversibility) = interp_notation_constr env nenv c in
let interp = make_interpretation_vars sd.recvars acvars (fst sd.pa_syntax_data) in
let map (x, _) = try Some (x, Id.Map.find x interp) with Not_found -> None in
- let onlyparse = is_not_printable sd.only_parsing reversibility ac in
+ let onlyparse,coe = printability (Some sd.level) sd.only_parsing reversibility ac in
let notation = {
notobj_local = local;
notobj_scope = scope;
notobj_interp = (List.map_filter map i_vars, ac);
(** Order is important here! *)
notobj_onlyparse = onlyparse;
+ notobj_coercion = coe;
notobj_onlyprint = sd.only_printing;
notobj_compat = sd.compat;
notobj_notation = sd.info;
@@ -1387,16 +1473,17 @@ let add_notation_in_scope local df env c mods scope =
let add_notation_interpretation_core local df env ?(impls=empty_internalization_env) c scope onlyparse onlyprint compat =
let (recvars,mainvars,symbs) = analyze_notation_tokens ~onlyprint df in
(* Recover types of variables and pa/pp rules; redeclare them if needed *)
- let i_typs, onlyprint = if not (is_numeral symbs) then begin
- let sy = recover_notation_syntax (make_notation_key symbs) in
+ let level, i_typs, onlyprint = if not (is_numeral symbs) then begin
+ let sy = recover_notation_syntax (make_notation_key InConstrEntrySomeLevel symbs) in
let () = Lib.add_anonymous_leaf (inSyntaxExtension (local,sy)) in
(** If the only printing flag has been explicitly requested, put it back *)
let onlyprint = onlyprint || sy.synext_notgram.notgram_onlyprinting in
- pi3 sy.synext_level, onlyprint
- end else [], false in
+ let _,_,_,typs = sy.synext_level in
+ Some sy.synext_level, typs, onlyprint
+ end else None, [], false in
(* Declare interpretation *)
let path = (Lib.library_dp(), Lib.current_dirpath true) in
- let df' = (make_notation_key symbs, (path,df)) in
+ let df' = (make_notation_key InConstrEntrySomeLevel symbs, (path,df)) in
let i_vars = make_internalization_vars recvars mainvars (List.map internalization_type_of_entry_type i_typs) in
let nenv = {
ninterp_var_type = to_map i_vars;
@@ -1405,13 +1492,14 @@ let add_notation_interpretation_core local df env ?(impls=empty_internalization_
let (acvars, ac, reversibility) = interp_notation_constr env ~impls nenv c in
let interp = make_interpretation_vars recvars acvars (List.combine mainvars i_typs) in
let map (x, _) = try Some (x, Id.Map.find x interp) with Not_found -> None in
- let onlyparse = is_not_printable onlyparse reversibility ac in
+ let onlyparse,coe = printability level onlyparse reversibility ac in
let notation = {
notobj_local = local;
notobj_scope = scope;
notobj_interp = (List.map_filter map i_vars, ac);
(** Order is important here! *)
notobj_onlyparse = onlyparse;
+ notobj_coercion = coe;
notobj_onlyprint = onlyprint;
notobj_compat = compat;
notobj_notation = df';
@@ -1422,7 +1510,7 @@ let add_notation_interpretation_core local df env ?(impls=empty_internalization_
(* Notations without interpretation (Reserved Notation) *)
let add_syntax_extension local ({CAst.loc;v=df},mods) = let open SynData in
- let psd = compute_pure_syntax_data df mods in
+ let psd = compute_pure_syntax_data local df mods in
let sy_rules = make_syntax_rules {psd with compat = None} in
Flags.if_verbose (List.iter (fun (f,x) -> f x)) psd.msgs;
Lib.add_anonymous_leaf (inSyntaxExtension(local,sy_rules))
@@ -1462,7 +1550,7 @@ let add_notation local env c ({CAst.loc;v=df},modifiers) sc =
let add_notation_extra_printing_rule df k v =
let notk =
let _,_, symbs = analyze_notation_tokens ~onlyprint:true df in
- make_notation_key symbs in
+ make_notation_key InConstrEntrySomeLevel symbs in
add_notation_extra_printing_rule notk k v
(* Infix notations *)
@@ -1546,7 +1634,35 @@ let add_syntactic_definition env ident (vars,c) local onlyparse =
List.map map vars, reversibility, pat
in
let onlyparse = match onlyparse with
- | None when (is_not_printable false reversibility pat) -> Some Flags.Current
+ | None when fst (printability None false reversibility pat) -> Some Flags.Current
| p -> p
in
Syntax_def.declare_syntactic_definition local ident onlyparse (vars,pat)
+
+(**********************************************************************)
+(* Declaration of custom entry *)
+
+let load_custom_entry _ _ = ()
+
+let open_custom_entry _ (_,(local,s)) =
+ Egramcoq.create_custom_entry ~local s
+
+let cache_custom_entry o =
+ load_custom_entry 1 o;
+ open_custom_entry 1 o
+
+let subst_custom_entry (subst,x) = x
+
+let classify_custom_entry (local,s as o) =
+ if local then Dispose else Substitute o
+
+let inCustomEntry : locality_flag * string -> obj =
+ declare_object {(default_object "CUSTOM-ENTRIES") with
+ cache_function = cache_custom_entry;
+ open_function = open_custom_entry;
+ load_function = load_custom_entry;
+ subst_function = subst_custom_entry;
+ classify_function = classify_custom_entry}
+
+let declare_custom_entry local s =
+ Lib.add_anonymous_leaf (inCustomEntry (local,s))
diff --git a/vernac/metasyntax.mli b/vernac/metasyntax.mli
index f6de75b079..73bee7121b 100644
--- a/vernac/metasyntax.mli
+++ b/vernac/metasyntax.mli
@@ -60,3 +60,5 @@ val pr_grammar : string -> Pp.t
val check_infix_modifiers : syntax_modifier list -> unit
val with_syntax_protection : ('a -> 'b) -> 'a -> 'b
+
+val declare_custom_entry : locality_flag -> string -> unit
diff --git a/vernac/obligations.ml b/vernac/obligations.ml
index 1f401b4e15..14d7642328 100644
--- a/vernac/obligations.ml
+++ b/vernac/obligations.ml
@@ -220,7 +220,7 @@ let eterm_obligations env name evm fs ?status t ty =
in
let loc, k = evar_source id evm in
let status = match k with
- | Evar_kinds.QuestionMark (o,_) -> o
+ | Evar_kinds.QuestionMark { Evar_kinds.qm_obligation=o } -> o
| _ -> match status with
| Some o -> o
| None -> Evar_kinds.Define (not (Program.get_proofs_transparency ()))
diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml
index e5547d9b75..93e4e89a12 100644
--- a/vernac/ppvernac.ml
+++ b/vernac/ppvernac.ml
@@ -97,25 +97,27 @@ open Pputils
let sep = fun _ -> spc()
let sep_v2 = fun _ -> str"," ++ spc()
+ let pr_notation_entry = function
+ | InConstrEntry -> keyword "constr"
+ | InCustomEntry s -> keyword "custom" ++ spc () ++ str s
+
let pr_at_level = function
| NumLevel n -> keyword "at" ++ spc () ++ keyword "level" ++ spc () ++ int n
| NextLevel -> keyword "at" ++ spc () ++ keyword "next" ++ spc () ++ keyword "level"
let pr_constr_as_binder_kind = let open Notation_term in function
- | AsIdent -> keyword "as ident"
- | AsIdentOrPattern -> keyword "as pattern"
- | AsStrictPattern -> keyword "as strict pattern"
+ | AsIdent -> spc () ++ keyword "as ident"
+ | AsIdentOrPattern -> spc () ++ keyword "as pattern"
+ | AsStrictPattern -> spc () ++ keyword "as strict pattern"
let pr_strict b = if b then str "strict " else mt ()
let pr_set_entry_type pr = function
- | ETName -> str"ident"
- | ETReference -> str"global"
+ | ETIdent -> str"ident"
+ | ETGlobal -> str"global"
| ETPattern (b,None) -> pr_strict b ++ str"pattern"
| ETPattern (b,Some n) -> pr_strict b ++ str"pattern" ++ spc () ++ pr_at_level (NumLevel n)
- | ETConstr lev -> str"constr" ++ pr lev
- | ETOther (_,e) -> str e
- | ETConstrAsBinder (bk,lev) -> pr lev ++ spc () ++ pr_constr_as_binder_kind bk
+ | ETConstr (s,bko,lev) -> pr_notation_entry s ++ pr lev ++ pr_opt pr_constr_as_binder_kind bko
| ETBigint -> str "bigint"
| ETBinder true -> str "binder"
| ETBinder false -> str "closed binder"
@@ -378,12 +380,11 @@ open Pputils
let pr_thm_token k = keyword (Kindops.string_of_theorem_kind k)
let pr_syntax_modifier = function
- | SetItemLevel (l,n) ->
- prlist_with_sep sep_v2 str l ++ spc () ++ pr_at_level n
- | SetItemLevelAsBinder (l,bk,n) ->
- prlist_with_sep sep_v2 str l ++
- spc() ++ pr_at_level_opt n ++ spc() ++ pr_constr_as_binder_kind bk
+ | SetItemLevel (l,bko,n) ->
+ prlist_with_sep sep_v2 str l ++ spc () ++ pr_at_level_opt n ++
+ pr_opt pr_constr_as_binder_kind bko
| SetLevel n -> pr_at_level (NumLevel n)
+ | SetCustomEntry (s,n) -> keyword "in" ++ spc() ++ keyword "custom" ++ spc() ++ str s ++ (match n with None -> mt () | Some n -> pr_at_level (NumLevel n))
| SetAssoc LeftA -> keyword "left associativity"
| SetAssoc RightA -> keyword "right associativity"
| SetAssoc NonA -> keyword "no associativity"
@@ -674,6 +675,10 @@ open Pputils
return (
keyword "Format Notation " ++ qs s ++ spc () ++ qs k ++ spc() ++ qs v
)
+ | VernacDeclareCustomEntry s ->
+ return (
+ keyword "Declare Custom Entry " ++ str s
+ )
(* Gallina *)
| VernacDefinition ((discharge,kind),id,b) -> (* A verifier... *)
diff --git a/vernac/proof_using.ml b/vernac/proof_using.ml
index 74e53bef18..3e2bd98720 100644
--- a/vernac/proof_using.ml
+++ b/vernac/proof_using.ml
@@ -18,14 +18,6 @@ module NamedDecl = Context.Named.Declaration
let known_names = Summary.ref [] ~name:"proofusing-nameset"
-let in_nameset =
- let open Libobject in
- declare_object { (default_object "proofusing-nameset") with
- cache_function = (fun (_,x) -> known_names := x :: !known_names);
- classify_function = (fun _ -> Dispose);
- discharge_function = (fun _ -> None)
- }
-
let rec close_fwd e s =
let s' =
List.fold_left (fun s decl ->
@@ -73,7 +65,7 @@ let process_expr env e ty =
let s = Id.Set.union v_ty (process_expr env e ty) in
Id.Set.elements s
-let name_set id expr = Lib.add_anonymous_leaf (in_nameset (id,expr))
+let name_set id expr = known_names := (id,expr) :: !known_names
let minimize_hyps env ids =
let rec aux ids =
diff --git a/vernac/record.ml b/vernac/record.ml
index 7a8ce7d25a..6b5c538df2 100644
--- a/vernac/record.ml
+++ b/vernac/record.ml
@@ -324,12 +324,16 @@ let declare_projections indsp ctx ?(kind=StructureComponent) binder_name coers u
| Name fid -> try
let kn, term =
if is_local_assum decl && primitive then
- (** Already defined in the kernel silently *)
- let gr = Nametab.locate (Libnames.qualid_of_ident fid) in
- let kn = destConstRef gr in
+ let p = Projection.Repr.make indsp
+ ~proj_npars:mib.mind_nparams
+ ~proj_arg:i
+ (Label.of_id fid)
+ in
+ (** Already defined by declare_mind silently *)
+ let kn = Projection.Repr.constant p in
Declare.definition_message fid;
- UnivNames.register_universe_binders gr ubinders;
- kn, mkProj (Projection.make kn false,mkRel 1)
+ UnivNames.register_universe_binders (ConstRef kn) ubinders;
+ kn, mkProj (Projection.make p false,mkRel 1)
else
let ccl = subst_projection fid subst ti in
let body = match decl with
diff --git a/vernac/topfmt.ml b/vernac/topfmt.ml
index 609dac69aa..f842ca5ead 100644
--- a/vernac/topfmt.ml
+++ b/vernac/topfmt.ml
@@ -181,6 +181,10 @@ let default_tag_map () = let open Terminal in [
; "tactic.keyword" , make ~bold:true ()
; "tactic.primitive" , make ~fg_color:`LIGHT_GREEN ()
; "tactic.string" , make ~fg_color:`LIGHT_RED ()
+ ; "diff.added" , make ~bg_color:(`RGB(0,141,0)) ~underline:true ()
+ ; "diff.removed" , make ~bg_color:(`RGB(170,0,0)) ~underline:true ()
+ ; "diff.added.bg" , make ~bg_color:(`RGB(0,91,0)) ()
+ ; "diff.removed.bg" , make ~bg_color:(`RGB(91,0,0)) ()
]
let tag_map = ref CString.Map.empty
@@ -198,72 +202,103 @@ let parse_color_config file =
let dump_tags () = CString.Map.bindings !tag_map
+let empty = Terminal.make ()
+let default_style = Terminal.reset_style
+
+let get_style tag =
+ try CString.Map.find tag !tag_map
+ with Not_found -> empty;;
+
+let get_open_seq tags =
+ let style = List.fold_left (fun a b -> Terminal.merge a (get_style b)) default_style tags in
+ Terminal.eval (Terminal.diff default_style style);;
+
+let get_close_seq tags =
+ let style = List.fold_left (fun a b -> Terminal.merge a (get_style b)) default_style tags in
+ Terminal.eval (Terminal.diff style default_style);;
+
+let diff_tag_stack = ref [] (* global, just like std_ft *)
+
(** Not thread-safe. We should put a lock somewhere if we print from
different threads. Do we? *)
let make_style_stack () =
(** Default tag is to reset everything *)
- let empty = Terminal.make () in
- let default_tag = Terminal.({
- fg_color = Some `DEFAULT;
- bg_color = Some `DEFAULT;
- bold = Some false;
- italic = Some false;
- underline = Some false;
- negative = Some false;
- prefix = None;
- suffix = None;
- })
- in
let style_stack = ref [] in
let peek () = match !style_stack with
- | [] -> default_tag (** Anomalous case, but for robustness *)
+ | [] -> default_style (** Anomalous case, but for robustness *)
| st :: _ -> st
in
- let push tag =
- let style =
- try CString.Map.find tag !tag_map
- with | Not_found -> empty
- in
- (** Use the merging of the latest tag and the one being currently pushed.
- This may be useful if for instance the latest tag changes the background and
- the current one the foreground, so that the two effects are additioned. *)
+ let open_tag tag =
+ let (tpfx, ttag) = split_tag tag in
+ if tpfx = end_pfx then "" else
+ let style = get_style ttag in
+ (** Merge the current settings and the style being pushed. This allows
+ restoring the previous settings correctly in a pop when both set the same
+ attribute. Example: current settings have red FG, the pushed style has
+ green FG. When popping the style, we should set red FG, not default FG. *)
let style = Terminal.merge (peek ()) style in
+ let diff = Terminal.diff (peek ()) style in
style_stack := style :: !style_stack;
- Terminal.eval style
+ if tpfx = start_pfx then diff_tag_stack := ttag :: !diff_tag_stack;
+ Terminal.eval diff
in
- let pop _ = match !style_stack with
- | [] -> (** Something went wrong, we fallback *)
- Terminal.eval default_tag
- | _ :: rem -> style_stack := rem;
- Terminal.eval (peek ())
+ let close_tag tag =
+ let (tpfx, _) = split_tag tag in
+ if tpfx = start_pfx then "" else begin
+ if tpfx = end_pfx then diff_tag_stack := (try List.tl !diff_tag_stack with tl -> []);
+ match !style_stack with
+ | [] -> (** Something went wrong, we fallback *)
+ Terminal.eval default_style
+ | cur :: rem -> style_stack := rem;
+ if cur = (peek ()) then "" else
+ if rem = [] then Terminal.reset else
+ Terminal.eval (Terminal.diff cur (peek ()))
+ end
in
let clear () = style_stack := [] in
- push, pop, clear
+ open_tag, close_tag, clear
let make_printing_functions () =
- let empty = Terminal.make () in
let print_prefix ft tag =
- let style =
- try CString.Map.find tag !tag_map
- with | Not_found -> empty
- in
- match style.Terminal.prefix with Some s -> Format.pp_print_string ft s | None -> ()
- in
+ let (tpfx, ttag) = split_tag tag in
+ if tpfx <> end_pfx then
+ let style = get_style ttag in
+ match style.Terminal.prefix with Some s -> Format.pp_print_string ft s | None -> () in
+
let print_suffix ft tag =
- let style =
- try CString.Map.find tag !tag_map
- with | Not_found -> empty
- in
- match style.Terminal.suffix with Some s -> Format.pp_print_string ft s | None -> ()
- in
+ let (tpfx, ttag) = split_tag tag in
+ if tpfx <> start_pfx then
+ let style = get_style ttag in
+ match style.Terminal.suffix with Some s -> Format.pp_print_string ft s | None -> () in
+
print_prefix, print_suffix
+let init_output_fns () =
+ let reopen_highlight = ref "" in
+ let open Format in
+ let fns = Format.pp_get_formatter_out_functions !std_ft () in
+ let newline () =
+ if !diff_tag_stack <> [] then begin
+ let close = get_close_seq !diff_tag_stack in
+ fns.out_string close 0 (String.length close);
+ reopen_highlight := get_open_seq (List.rev !diff_tag_stack);
+ end;
+ fns.out_string "\n" 0 1 in
+ let string s off n =
+ if !reopen_highlight <> "" && String.trim (String.sub s off n) <> "" then begin
+ fns.out_string !reopen_highlight 0 (String.length !reopen_highlight);
+ reopen_highlight := ""
+ end;
+ fns.out_string s off n in
+ let new_fns = { fns with out_string = string; out_newline = newline } in
+ Format.pp_set_formatter_out_functions !std_ft new_fns;;
+
let init_terminal_output ~color =
- let push_tag, pop_tag, clear_tag = make_style_stack () in
+ let open_tag, close_tag, clear_tag = make_style_stack () in
let print_prefix, print_suffix = make_printing_functions () in
let tag_handler ft = {
- Format.mark_open_tag = push_tag;
- Format.mark_close_tag = pop_tag;
+ Format.mark_open_tag = open_tag;
+ Format.mark_close_tag = close_tag;
Format.print_open_tag = print_prefix ft;
Format.print_close_tag = print_suffix ft;
} in
@@ -271,6 +306,7 @@ let init_terminal_output ~color =
(* Use 0-length markers *)
begin
std_logger_cleanup := clear_tag;
+ init_output_fns ();
Format.pp_set_mark_tags !std_ft true;
Format.pp_set_mark_tags !err_ft true
end
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index b6bc76a2ed..e1c9712135 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -431,6 +431,10 @@ let vernac_notation ~atts =
let local = enforce_module_locality atts.locality in
Metasyntax.add_notation local (Global.env())
+let vernac_custom_entry ~atts s =
+ let local = enforce_module_locality atts.locality in
+ Metasyntax.declare_custom_entry local s
+
(***********)
(* Gallina *)
@@ -1501,8 +1505,8 @@ let _ =
{ optdepr = false;
optname = "kernel term sharing";
optkey = ["Kernel"; "Term"; "Sharing"];
- optread = (fun () -> !CClosure.share);
- optwrite = (fun b -> CClosure.share := b) }
+ optread = (fun () -> (Global.typing_flags ()).Declarations.share_reduction);
+ optwrite = (fun b -> Global.set_reduction_sharing b) }
let _ =
declare_bool_option
@@ -1983,8 +1987,9 @@ let vernac_subproof gln =
match gln with
| None -> Proof.focus subproof_cond () 1 p
| Some (Goal_select.SelectNth n) -> Proof.focus subproof_cond () n p
+ | Some (Goal_select.SelectId id) -> Proof.focus_id subproof_cond () id p
| _ -> user_err ~hdr:"bracket_selector"
- (str "Brackets only support the single numbered goal selector."))
+ (str "Brackets do not support multi-goal selectors."))
let vernac_end_subproof () =
Proof_global.simple_with_current_proof (fun _ p ->
@@ -2096,6 +2101,8 @@ let interp ?proof ~atts ~st c =
vernac_notation ~atts c infpl sc
| VernacNotationAddFormat(n,k,v) ->
Metasyntax.add_notation_extra_printing_rule n k v
+ | VernacDeclareCustomEntry s ->
+ vernac_custom_entry ~atts s
(* Gallina *)
| VernacDefinition ((discharge,kind),lid,d) ->
@@ -2224,6 +2231,7 @@ let check_vernac_supports_locality c l =
| Some _, (
VernacOpenCloseScope _
| VernacSyntaxExtension _ | VernacInfix _ | VernacNotation _
+ | VernacDeclareCustomEntry _
| VernacDefinition _ | VernacFixpoint _ | VernacCoFixpoint _
| VernacAssumption _ | VernacStartTheoremProof _
| VernacCoercion _ | VernacIdentityCoercion _
@@ -2436,3 +2444,121 @@ let interp ?verbosely ?proof ~st cmd =
let exn = CErrors.push exn in
Vernacstate.invalidate_cache ();
iraise exn
+
+(** VERNAC EXTEND registering *)
+
+open Genarg
+open Extend
+
+type classifier = Genarg.raw_generic_argument list -> vernac_classification
+
+type (_, _) ty_sig =
+| TyNil : (atts:atts -> st:Vernacstate.t -> Vernacstate.t, Vernacexpr.vernac_classification) ty_sig
+| TyTerminal : string * ('r, 's) ty_sig -> ('r, 's) ty_sig
+| TyNonTerminal :
+ string option * ('a, 'b, 'c) Extend.ty_user_symbol * ('r, 's) ty_sig -> ('a -> 'r, 'a -> 's) ty_sig
+
+type ty_ml = TyML : bool * ('r, 's) ty_sig * 'r * 's option -> ty_ml
+
+let type_error () = CErrors.anomaly (Pp.str "Ill-typed VERNAC EXTEND")
+
+let rec untype_classifier : type r s. (r, s) ty_sig -> s -> classifier = function
+| TyNil -> fun f args ->
+ begin match args with
+ | [] -> f
+ | _ :: _ -> type_error ()
+ end
+| TyTerminal (_, ty) -> fun f args -> untype_classifier ty f args
+| TyNonTerminal (_, tu, ty) -> fun f args ->
+ begin match args with
+ | [] -> type_error ()
+ | Genarg.GenArg (Rawwit tag, v) :: args ->
+ match Genarg.genarg_type_eq tag (Egramml.proj_symbol tu) with
+ | None -> type_error ()
+ | Some Refl -> untype_classifier ty (f v) args
+ end
+
+(** Stupid GADTs forces us to duplicate the definition just for typing *)
+let rec untype_command : type r s. (r, s) ty_sig -> r -> plugin_args vernac_command = function
+| TyNil -> fun f args ->
+ begin match args with
+ | [] -> f
+ | _ :: _ -> type_error ()
+ end
+| TyTerminal (_, ty) -> fun f args -> untype_command ty f args
+| TyNonTerminal (_, tu, ty) -> fun f args ->
+ begin match args with
+ | [] -> type_error ()
+ | Genarg.GenArg (Rawwit tag, v) :: args ->
+ match Genarg.genarg_type_eq tag (Egramml.proj_symbol tu) with
+ | None -> type_error ()
+ | Some Refl -> untype_command ty (f v) args
+ end
+
+let rec untype_user_symbol : type s a b c. (a, b, c) Extend.ty_user_symbol -> (s, a) Extend.symbol = function
+| TUlist1 l -> Alist1 (untype_user_symbol l)
+| TUlist1sep (l, s) -> Alist1sep (untype_user_symbol l, Atoken (CLexer.terminal s))
+| TUlist0 l -> Alist0 (untype_user_symbol l)
+| TUlist0sep (l, s) -> Alist0sep (untype_user_symbol l, Atoken (CLexer.terminal s))
+| TUopt o -> Aopt (untype_user_symbol o)
+| TUentry a -> Aentry (Pcoq.genarg_grammar (ExtraArg a))
+| TUentryl (a, i) -> Aentryl (Pcoq.genarg_grammar (ExtraArg a), string_of_int i)
+
+let rec untype_grammar : type r s. (r, s) ty_sig -> vernac_expr Egramml.grammar_prod_item list = function
+| TyNil -> []
+| TyTerminal (tok, ty) -> Egramml.GramTerminal tok :: untype_grammar ty
+| TyNonTerminal (id, tu, ty) ->
+ let t = Option.map (fun _ -> rawwit (Egramml.proj_symbol tu)) id in
+ let symb = untype_user_symbol tu in
+ Egramml.GramNonTerminal (Loc.tag (t, symb)) :: untype_grammar ty
+
+let _ = untype_classifier, untype_command, untype_grammar, untype_user_symbol
+
+let classifiers : classifier array String.Map.t ref = ref String.Map.empty
+
+let get_vernac_classifier (name, i) args =
+ (String.Map.find name !classifiers).(i) args
+
+let declare_vernac_classifier name f =
+ classifiers := String.Map.add name f !classifiers
+
+let vernac_extend ~command ?classifier ?entry ext =
+ let get_classifier (TyML (_, ty, _, cl)) = match cl with
+ | Some cl -> untype_classifier ty cl
+ | None ->
+ match classifier with
+ | Some cl -> fun _ -> cl command
+ | None ->
+ let e = match entry with
+ | None -> "COMMAND"
+ | Some e -> Pcoq.Gram.Entry.name e
+ in
+ let msg = Printf.sprintf "\
+ Vernac entry \"%s\" misses a classifier. \
+ A classifier is a function that returns an expression \
+ of type vernac_classification (see Vernacexpr). You can: \n\
+ - Use '... EXTEND %s CLASSIFIED AS QUERY ...' if the \
+ new vernacular command does not alter the system state;\n\
+ - Use '... EXTEND %s CLASSIFIED AS SIDEFF ...' if the \
+ new vernacular command alters the system state but not the \
+ parser nor it starts a proof or ends one;\n\
+ - Use '... EXTEND %s CLASSIFIED BY f ...' to specify \
+ a global function f. The function f will be called passing\
+ \"%s\" as the only argument;\n\
+ - Add a specific classifier in each clause using the syntax:\n\
+ '[...] => [ f ] -> [...]'.\n\
+ Specific classifiers have precedence over global \
+ classifiers. Only one classifier is called."
+ command e e e command
+ in
+ CErrors.user_err (Pp.strbrk msg)
+ in
+ let cl = Array.map_of_list get_classifier ext in
+ let iter i (TyML (depr, ty, f, _)) =
+ let f = untype_command ty f in
+ let r = untype_grammar ty in
+ let () = vinterp_add depr (command, i) f in
+ Egramml.extend_vernac_command_grammar (command, i) entry r
+ in
+ let () = declare_vernac_classifier command cl in
+ List.iteri iter ext
diff --git a/vernac/vernacentries.mli b/vernac/vernacentries.mli
index 79f9c05ad8..fb2a30bac7 100644
--- a/vernac/vernacentries.mli
+++ b/vernac/vernacentries.mli
@@ -42,3 +42,33 @@ val universe_polymorphism_option_name : string list
(** Elaborate a [atts] record out of a list of flags.
Also returns whether polymorphism is explicitly (un)set. *)
val attributes_of_flags : Vernacexpr.vernac_flags -> Vernacinterp.atts -> bool option * Vernacinterp.atts
+
+(** {5 VERNAC EXTEND} *)
+
+type classifier = Genarg.raw_generic_argument list -> Vernacexpr.vernac_classification
+
+type (_, _) ty_sig =
+| TyNil : (atts:Vernacinterp.atts -> st:Vernacstate.t -> Vernacstate.t, Vernacexpr.vernac_classification) ty_sig
+| TyTerminal : string * ('r, 's) ty_sig -> ('r, 's) ty_sig
+| TyNonTerminal :
+ string option *
+ ('a, 'b, 'c) Extend.ty_user_symbol * ('r, 's) ty_sig ->
+ ('a -> 'r, 'a -> 's) ty_sig
+
+type ty_ml = TyML : bool (** deprecated *) * ('r, 's) ty_sig * 'r * 's option -> ty_ml
+
+(** Wrapper to dynamically extend vernacular commands. *)
+val vernac_extend :
+ command:string ->
+ ?classifier:(string -> Vernacexpr.vernac_classification) ->
+ ?entry:Vernacexpr.vernac_expr Pcoq.Entry.t ->
+ ty_ml list -> unit
+
+(** {5 STM classifiers} *)
+
+val get_vernac_classifier :
+ Vernacexpr.extend_name -> classifier
+
+(** Low-level API, not for casual user. *)
+val declare_vernac_classifier :
+ string -> classifier array -> unit
diff --git a/vernac/vernacexpr.ml b/vernac/vernacexpr.ml
index e97cac818a..8fb74e6d78 100644
--- a/vernac/vernacexpr.ml
+++ b/vernac/vernacexpr.ml
@@ -211,9 +211,9 @@ type proof_expr =
ident_decl * (local_binder_expr list * constr_expr)
type syntax_modifier =
- | SetItemLevel of string list * Extend.production_level
- | SetItemLevelAsBinder of string list * Notation_term.constr_as_binder_kind * Extend.production_level option
+ | SetItemLevel of string list * Notation_term.constr_as_binder_kind option * Extend.production_level option
| SetLevel of int
+ | SetCustomEntry of string * int option
| SetAssoc of Extend.gram_assoc
| SetEntryType of string * Extend.simple_constr_prod_entry_key
| SetOnlyParsing
@@ -333,6 +333,7 @@ type nonrec vernac_expr =
constr_expr * (lstring * syntax_modifier list) *
scope_name option
| VernacNotationAddFormat of string * string * string
+ | VernacDeclareCustomEntry of string
(* Gallina *)
| VernacDefinition of (Decl_kinds.discharge * Decl_kinds.definition_object_kind) * name_decl * definition_expr
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-05 01:16:18 +0000