diff options
Diffstat (limited to 'vernac')
| -rw-r--r-- | vernac/class.ml | 13 | ||||
| -rw-r--r-- | vernac/comProgramFixpoint.ml | 4 | ||||
| -rw-r--r-- | vernac/egramml.ml | 9 | ||||
| -rw-r--r-- | vernac/egramml.mli | 2 | ||||
| -rw-r--r-- | vernac/himsg.ml | 23 | ||||
| -rw-r--r-- | vernac/obligations.ml | 2 | ||||
| -rw-r--r-- | vernac/proof_using.ml | 10 | ||||
| -rw-r--r-- | vernac/record.ml | 14 | ||||
| -rw-r--r-- | vernac/topfmt.ml | 124 | ||||
| -rw-r--r-- | vernac/vernacentries.ml | 118 | ||||
| -rw-r--r-- | vernac/vernacentries.mli | 30 |
11 files changed, 268 insertions, 81 deletions
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/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/himsg.ml b/vernac/himsg.ml index 534e58f9c9..b9c47ff475 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 -> @@ -1229,12 +1227,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 " ++ 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/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..653f8b26e0 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -2436,3 +2436,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 |