diff options
Diffstat (limited to 'vernac')
| -rw-r--r-- | vernac/class.ml | 13 | ||||
| -rw-r--r-- | vernac/comProgramFixpoint.ml | 4 | ||||
| -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 |
7 files changed, 109 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/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 |