diff options
40 files changed, 487 insertions, 259 deletions
@@ -1,4 +1,4 @@ -Changes beyong V8.6 +Changes beyond V8.6 =================== Tactics diff --git a/configure.ml b/configure.ml index 7e125d87c..c3ba953de 100644 --- a/configure.ml +++ b/configure.ml @@ -430,7 +430,7 @@ let dll = if os_type_win32 then ".dll" else ".so" let vcs = let git_dir = try Sys.getenv "GIT_DIR" with Not_found -> ".git" in - if dir_exists git_dir then "git" + if Sys.file_exists git_dir then "git" else if Sys.file_exists ".svn/entries" then "svn" else if dir_exists "{arch}" then "gnuarch" else "none" diff --git a/engine/ftactic.ml b/engine/ftactic.ml index 588709873..aeaaea7e4 100644 --- a/engine/ftactic.ml +++ b/engine/ftactic.ml @@ -29,13 +29,28 @@ let bind (type a) (type b) (m : a t) (f : a -> b t) : b t = m >>= function | Uniform x -> (** We dispatch the uniform result on each goal under focus, as we know that the [m] argument was actually dependent. *) - Proofview.Goal.goals >>= fun l -> - let ans = List.map (fun _ -> x) l in + Proofview.Goal.goals >>= fun goals -> + let ans = List.map (fun g -> (g,x)) goals in Proofview.tclUNIT ans - | Depends l -> Proofview.tclUNIT l + | Depends l -> + Proofview.Goal.goals >>= fun goals -> + Proofview.tclUNIT (List.combine goals l) + in + (* After the tactic has run, some goals which were previously + produced may have been solved by side effects. The values + attached to such goals must be discarded, otherwise the list of + result would not have the same length as the list of focused + goals, which is an invariant of the [Ftactic] module. It is the + reason why a goal is attached to each result above. *) + let filter (g,x) = + g >>= fun g -> + Proofview.Goal.unsolved g >>= function + | true -> Proofview.tclUNIT (Some x) + | false -> Proofview.tclUNIT None in Proofview.tclDISPATCHL (List.map f l) >>= fun l -> - Proofview.tclUNIT (Depends (List.concat l)) + Proofview.Monad.List.map_filter filter (List.concat l) >>= fun filtered -> + Proofview.tclUNIT (Depends filtered) let goals = Proofview.Goal.goals >>= fun l -> Proofview.tclUNIT (Depends l) let set_sigma r = diff --git a/engine/proofview.ml b/engine/proofview.ml index 1ebc857d8..d7fb65126 100644 --- a/engine/proofview.ml +++ b/engine/proofview.ml @@ -685,6 +685,21 @@ let unshelve l p = let l = undefined p.solution l in { p with comb = p.comb@l } +let mark_in_evm ~goal evd content = + let info = Evd.find evd content in + let info = + if goal then + { info with Evd.evar_source = match info.Evd.evar_source with + | _, (Evar_kinds.VarInstance _ | Evar_kinds.GoalEvar) as x -> x + | loc,_ -> loc,Evar_kinds.GoalEvar } + else info + in + let info = match Evd.Store.get info.Evd.evar_extra typeclass_resolvable with + | None -> { info with Evd.evar_extra = Evd.Store.set info.Evd.evar_extra typeclass_resolvable () } + | Some () -> info + in + Evd.add evd content info + let with_shelf tac = let open Proof in Pv.get >>= fun pv -> @@ -697,8 +712,11 @@ let with_shelf tac = let fgoals = Evd.future_goals solution in let pgoal = Evd.principal_future_goal solution in let sigma = Evd.restore_future_goals sigma fgoals pgoal in - Pv.set { npv with shelf; solution = sigma } >> - tclUNIT (CList.rev_append gls' gls, ans) + (* Ensure we mark and return only unsolved goals *) + let gls' = undefined sigma (CList.rev_append gls' gls) in + let sigma = CList.fold_left (mark_in_evm ~goal:false) sigma gls' in + let npv = { npv with shelf; solution = sigma } in + Pv.set npv >> tclUNIT (gls', ans) (** [goodmod p m] computes the representative of [p] modulo [m] in the interval [[0,m-1]].*) @@ -929,6 +947,8 @@ module Unsafe = struct { step with comb = step.comb @ gls } end + let tclSETENV = Env.set + let tclGETGOALS = Comb.get let tclSETGOALS = Comb.set @@ -943,20 +963,13 @@ module Unsafe = struct { p with solution = Evd.reset_future_goals p.solution } let mark_as_goal evd content = - let info = Evd.find evd content in - let info = - { info with Evd.evar_source = match info.Evd.evar_source with - | _, (Evar_kinds.VarInstance _ | Evar_kinds.GoalEvar) as x -> x - | loc,_ -> loc,Evar_kinds.GoalEvar } - in - let info = match Evd.Store.get info.Evd.evar_extra typeclass_resolvable with - | None -> { info with Evd.evar_extra = Evd.Store.set info.Evd.evar_extra typeclass_resolvable () } - | Some () -> info - in - Evd.add evd content info + mark_in_evm ~goal:true evd content let advance = advance + let mark_as_unresolvable p gl = + { p with solution = mark_in_evm ~goal:false p.solution gl } + let typeclass_resolvable = typeclass_resolvable end @@ -1129,6 +1142,10 @@ module Goal = struct in tclUNIT (CList.map_filter map step.comb) + let unsolved { self=self } = + tclEVARMAP >>= fun sigma -> + tclUNIT (not (Option.is_empty (advance sigma self))) + (* compatibility *) let goal { self=self } = self diff --git a/engine/proofview.mli b/engine/proofview.mli index bc68f11ff..725445251 100644 --- a/engine/proofview.mli +++ b/engine/proofview.mli @@ -326,8 +326,9 @@ val unshelve : Goal.goal list -> proofview -> proofview (** [depends_on g1 g2 sigma] checks if g1 occurs in the type/ctx of g2 *) val depends_on : Evd.evar_map -> Goal.goal -> Goal.goal -> bool -(** [with_shelf tac] executes [tac] and returns its result together with the set - of goals shelved by [tac]. The current shelf is unchanged. *) +(** [with_shelf tac] executes [tac] and returns its result together with + the set of goals shelved by [tac]. The current shelf is unchanged + and the returned list contains only unsolved goals. *) val with_shelf : 'a tactic -> (Goal.goal list * 'a) tactic (** If [n] is positive, [cycle n] puts the [n] first goal last. If [n] @@ -409,6 +410,9 @@ module Unsafe : sig (** Like {!tclEVARS} but also checks whether goals have been solved. *) val tclEVARSADVANCE : Evd.evar_map -> unit tactic + (** Set the global environment of the tactic *) + val tclSETENV : Environ.env -> unit tactic + (** [tclNEWGOALS gls] adds the goals [gls] to the ones currently being proved, appending them to the list of focused goals. If a goal is already solved, it is not added. *) @@ -431,6 +435,9 @@ module Unsafe : sig and makes it unresolvable for type classes. *) val mark_as_goal : Evd.evar_map -> Evar.t -> Evd.evar_map + (** Make an evar unresolvable for type classes. *) + val mark_as_unresolvable : proofview -> Evar.t -> proofview + (** [advance sigma g] returns [Some g'] if [g'] is undefined and is the current avatar of [g] (for instance [g] was changed by [clear] into [g']). It returns [None] if [g] has been (partially) @@ -518,6 +525,10 @@ module Goal : sig FIXME: encapsulate the level in an existential type. *) val goals : ([ `LZ ], 'r) t tactic list tactic + (** [unsolved g] is [true] if [g] is still unsolved in the current + proof state. *) + val unsolved : ('a, 'r) t -> bool tactic + (** Compatibility: avoid if possible *) val goal : ([ `NF ], 'r) t -> Evar.t diff --git a/interp/constrextern.ml b/interp/constrextern.ml index f7fcbb4ee..4aff82403 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -481,7 +481,7 @@ let explicitize loc inctx impl (cf,f) args = (!print_implicits && !print_implicits_explicit_args) || (is_needed_for_correct_partial_application tail imp) || (!print_implicits_defensive && - (not (is_inferable_implicit inctx n imp) || !Flags.beautify_file) && + (not (is_inferable_implicit inctx n imp) || !Flags.beautify) && is_significant_implicit (Lazy.force a)) in if visible then diff --git a/interp/topconstr.ml b/interp/topconstr.ml index eb564f3b3..b455381ea 100644 --- a/interp/topconstr.ml +++ b/interp/topconstr.ml @@ -22,8 +22,7 @@ open Constrexpr_ops let asymmetric_patterns = ref (false) let _ = Goptions.declare_bool_option { Goptions.optsync = true; Goptions.optdepr = false; - Goptions.optname = - "Constructors in patterns require all their arguments but no parameters instead of explicit parameters and arguments"; + Goptions.optname = "no parameters in constructors"; Goptions.optkey = ["Asymmetric";"Patterns"]; Goptions.optread = (fun () -> !asymmetric_patterns); Goptions.optwrite = (fun a -> asymmetric_patterns:=a); diff --git a/kernel/entries.mli b/kernel/entries.mli index b736b2113..77081947e 100644 --- a/kernel/entries.mli +++ b/kernel/entries.mli @@ -98,7 +98,12 @@ type module_entry = | MExpr of module_params_entry * module_struct_entry * module_struct_entry option -type seff_env = [ `Nothing | `Opaque of Constr.t * Univ.universe_context_set ] + +type seff_env = + [ `Nothing + (* The proof term and its universes. + Same as the constant_body's but not in an ephemeron *) + | `Opaque of Constr.t * Univ.universe_context_set ] type side_eff = | SEsubproof of constant * Declarations.constant_body * seff_env diff --git a/lib/monad.ml b/lib/monad.ml index a1714a41b..2e55e9698 100644 --- a/lib/monad.ml +++ b/lib/monad.ml @@ -64,6 +64,9 @@ module type ListS = sig its second argument in a tail position. *) val iter : ('a -> unit t) -> 'a list -> unit t + (** Like the regular {!CList.map_filter}. The monadic effects are threaded left*) + val map_filter : ('a -> 'b option t) -> 'a list -> 'b list t + (** {6 Two-list iterators} *) @@ -138,6 +141,14 @@ module Make (M:Def) : S with type +'a t = 'a M.t = struct | a::b::l -> f a >> f b >> iter f l + let rec map_filter f = function + | [] -> return [] + | a::l -> + f a >>= function + | None -> map_filter f l + | Some b -> + map_filter f l >>= fun filtered -> + return (b::filtered) let rec fold_left2 r f x l1 l2 = match l1,l2 with diff --git a/lib/monad.mli b/lib/monad.mli index c8655efa0..f7de71f53 100644 --- a/lib/monad.mli +++ b/lib/monad.mli @@ -66,6 +66,9 @@ module type ListS = sig its second argument in a tail position. *) val iter : ('a -> unit t) -> 'a list -> unit t + (** Like the regular {!CList.map_filter}. The monadic effects are threaded left*) + val map_filter : ('a -> 'b option t) -> 'a list -> 'b list t + (** {6 Two-list iterators} *) @@ -77,17 +77,6 @@ open Pp_control \end{description} *) -let comments = ref [] - -let rec split_com comacc acc pos = function - [] -> comments := List.rev acc; comacc - | ((b,e),c as com)::coms -> - (* Take all comments that terminates before pos, or begin exactly - at pos (used to print comments attached after an expression) *) - if e<=pos || pos=b then split_com (c::comacc) acc pos coms - else split_com comacc (com::acc) pos coms - - type block_type = | Pp_hbox of int | Pp_vbox of int @@ -111,7 +100,7 @@ type 'a ppcmd_token = | Ppcmd_open_box of block_type | Ppcmd_close_box | Ppcmd_close_tbox - | Ppcmd_comment of int + | Ppcmd_comment of string list | Ppcmd_open_tag of Tag.t | Ppcmd_close_tag @@ -177,7 +166,7 @@ let tab () = Glue.atom(Ppcmd_set_tab) let fnl () = Glue.atom(Ppcmd_force_newline) let pifb () = Glue.atom(Ppcmd_print_if_broken) let ws n = Glue.atom(Ppcmd_white_space n) -let comment n = Glue.atom(Ppcmd_comment n) +let comment l = Glue.atom(Ppcmd_comment l) (* derived commands *) let mt () = Glue.empty @@ -321,8 +310,7 @@ let pp_dirs ?pp_tag ft = com_brk ft; Format.pp_force_newline ft () | Ppcmd_print_if_broken -> com_if ft (Lazy.from_fun(fun()->Format.pp_print_if_newline ft ())) - | Ppcmd_comment i -> - let coms = split_com [] [] i !comments in + | Ppcmd_comment coms -> (* Format.pp_open_hvbox ft 0;*) List.iter (pr_com ft) coms(*; Format.pp_close_box ft ()*) diff --git a/lib/pp.mli b/lib/pp.mli index 3bd560812..f607e99db 100644 --- a/lib/pp.mli +++ b/lib/pp.mli @@ -23,8 +23,7 @@ val ws : int -> std_ppcmds val mt : unit -> std_ppcmds val ismt : std_ppcmds -> bool -val comment : int -> std_ppcmds -val comments : ((int * int) * string) list ref +val comment : string list -> std_ppcmds (** {6 Manipulation commands} *) diff --git a/ltac/g_rewrite.ml4 b/ltac/g_rewrite.ml4 index 3168898a3..b1c4f58eb 100644 --- a/ltac/g_rewrite.ml4 +++ b/ltac/g_rewrite.ml4 @@ -63,8 +63,17 @@ let glob_strategy ist s = map_strategy (Tacintern.intern_constr ist) (fun c -> c let subst_strategy s str = str let pr_strategy _ _ _ (s : strategy) = Pp.str "<strategy>" -let pr_raw_strategy _ _ _ (s : raw_strategy) = Pp.str "<strategy>" -let pr_glob_strategy _ _ _ (s : glob_strategy) = Pp.str "<strategy>" +let pr_raw_strategy prc prlc _ (s : raw_strategy) = + let prr = Pptactic.pr_red_expr (prc, prlc, Pputils.pr_or_by_notation Libnames.pr_reference, prc) in + Rewrite.pr_strategy prc prr s +let pr_glob_strategy prc prlc _ (s : glob_strategy) = + let prr = Pptactic.pr_red_expr + (Ppconstr.pr_constr_expr, + Ppconstr.pr_lconstr_expr, + Pputils.pr_or_by_notation Libnames.pr_reference, + Ppconstr.pr_constr_expr) + in + Rewrite.pr_strategy prc prr s ARGUMENT EXTEND rewstrategy PRINTED BY pr_strategy diff --git a/ltac/rewrite.ml b/ltac/rewrite.ml index a332e2871..217f5f42e 100644 --- a/ltac/rewrite.ml +++ b/ltac/rewrite.ml @@ -1703,6 +1703,40 @@ let rec map_strategy (f : 'a -> 'a2) (g : 'b -> 'b2) : ('a,'b) strategy_ast -> ( | StratEval r -> StratEval (g r) | StratFold c -> StratFold (f c) +let pr_ustrategy = function +| Subterms -> str "subterms" +| Subterm -> str "subterm" +| Innermost -> str "innermost" +| Outermost -> str "outermost" +| Bottomup -> str "bottomup" +| Topdown -> str "topdown" +| Progress -> str "progress" +| Try -> str "try" +| Any -> str "any" +| Repeat -> str "repeat" + +let paren p = str "(" ++ p ++ str ")" + +let rec pr_strategy prc prr = function +| StratId -> str "id" +| StratFail -> str "fail" +| StratRefl -> str "refl" +| StratUnary (s, str) -> + pr_ustrategy s ++ spc () ++ paren (pr_strategy prc prr str) +| StratBinary (Choice, str1, str2) -> + str "choice" ++ spc () ++ paren (pr_strategy prc prr str1) ++ spc () ++ + paren (pr_strategy prc prr str2) +| StratBinary (Compose, str1, str2) -> + pr_strategy prc prr str1 ++ str ";" ++ spc () ++ pr_strategy prc prr str2 +| StratConstr (c, true) -> prc c +| StratConstr (c, false) -> str "<-" ++ spc () ++ prc c +| StratTerms cl -> str "terms" ++ spc () ++ pr_sequence prc cl +| StratHints (old, id) -> + let cmd = if old then "old_hints" else "hints" in + str cmd ++ spc () ++ str id +| StratEval r -> str "eval" ++ spc () ++ prr r +| StratFold c -> str "fold" ++ spc () ++ prc c + let rec strategy_of_ast = function | StratId -> Strategies.id | StratFail -> Strategies.fail diff --git a/ltac/rewrite.mli b/ltac/rewrite.mli index f448c8543..35c448351 100644 --- a/ltac/rewrite.mli +++ b/ltac/rewrite.mli @@ -62,6 +62,9 @@ val strategy_of_ast : (glob_constr_and_expr, raw_red_expr) strategy_ast -> strat val map_strategy : ('a -> 'b) -> ('c -> 'd) -> ('a, 'c) strategy_ast -> ('b, 'd) strategy_ast +val pr_strategy : ('a -> Pp.std_ppcmds) -> ('b -> Pp.std_ppcmds) -> + ('a, 'b) strategy_ast -> Pp.std_ppcmds + (** Entry point for user-level "rewrite_strat" *) val cl_rewrite_clause_strat : strategy -> Id.t option -> unit Proofview.tactic diff --git a/parsing/cLexer.ml4 b/parsing/cLexer.ml4 index f19759470..a7b413f57 100644 --- a/parsing/cLexer.ml4 +++ b/parsing/cLexer.ml4 @@ -340,34 +340,46 @@ let comm_loc bp = match !comment_begin with | None -> comment_begin := Some bp | _ -> () -let current = Buffer.create 8192 -let between_com = ref true - -type com_state = int option * string * bool -let restore_com_state (o,s,b) = +let comments = ref [] +let current_comment = Buffer.create 8192 +let between_commands = ref true + +let rec split_comments comacc acc pos = function + [] -> comments := List.rev acc; comacc + | ((b,e),c as com)::coms -> + (* Take all comments that terminates before pos, or begin exactly + at pos (used to print comments attached after an expression) *) + if e<=pos || pos=b then split_comments (c::comacc) acc pos coms + else split_comments comacc (com::acc) pos coms + +let extract_comments pos = split_comments [] [] pos !comments + +type comments_state = int option * string * bool * ((int * int) * string) list +let restore_comments_state (o,s,b,c) = comment_begin := o; - Buffer.clear current; Buffer.add_string current s; - between_com := b -let dflt_com = (None,"",true) -let com_state () = - let s = (!comment_begin, Buffer.contents current, !between_com) in - restore_com_state dflt_com; s + Buffer.clear current_comment; Buffer.add_string current_comment s; + between_commands := b; + comments := c +let default_comments_state = (None,"",true,[]) +let comments_state () = + let s = (!comment_begin, Buffer.contents current_comment, !between_commands, !comments) in + restore_comments_state default_comments_state; s -let real_push_char c = Buffer.add_char current c +let real_push_char c = Buffer.add_char current_comment c (* Add a char if it is between two commands, if it is a newline or if the last char is not a space itself. *) let push_char c = if - !between_com || List.mem c ['\n';'\r'] || + !between_commands || List.mem c ['\n';'\r'] || (List.mem c [' ';'\t']&& - (Int.equal (Buffer.length current) 0 || - not (let s = Buffer.contents current in + (Int.equal (Buffer.length current_comment) 0 || + not (let s = Buffer.contents current_comment in List.mem s.[String.length s - 1] [' ';'\t';'\n';'\r']))) then real_push_char c -let push_string s = Buffer.add_string current s +let push_string s = Buffer.add_string current_comment s let null_comment s = let rec null i = @@ -375,12 +387,12 @@ let null_comment s = null (String.length s - 1) let comment_stop ep = - let current_s = Buffer.contents current in - if !Flags.xml_export && Buffer.length current > 0 && - (!between_com || not(null_comment current_s)) then + let current_s = Buffer.contents current_comment in + if !Flags.xml_export && Buffer.length current_comment > 0 && + (!between_commands || not(null_comment current_s)) then Hook.get f_xml_output_comment current_s; - (if Flags.do_beautify() && Buffer.length current > 0 && - (!between_com || not(null_comment current_s)) then + (if Flags.do_beautify() && Buffer.length current_comment > 0 && + (!between_commands || not(null_comment current_s)) then let bp = match !comment_begin with Some bp -> bp | None -> @@ -389,10 +401,10 @@ let comment_stop ep = ++ str current_s ++str"' ending at " ++ int ep); ep-1 in - Pp.comments := ((bp,ep),current_s) :: !Pp.comments); - Buffer.clear current; + comments := ((bp,ep),current_s) :: !comments); + Buffer.clear current_comment; comment_begin := None; - between_com := false + between_commands := false (* Does not unescape!!! *) let rec comm_string loc bp = parser @@ -548,16 +560,16 @@ let rec next_token loc = parser bp | KEYWORD ("." | "...") -> if not (blank_or_eof s) then err (set_loc_pos loc bp (ep+1)) Undefined_token; - between_com := true; + between_commands := true; | _ -> () in (t, set_loc_pos loc bp ep) | [< ' ('-'|'+'|'*' as c); s >] -> - let t,new_between_com = - if !between_com then process_sequence loc bp c s, true + let t,new_between_commands = + if !between_commands then process_sequence loc bp c s, true else process_chars loc bp c s,false in - comment_stop bp; between_com := new_between_com; t + comment_stop bp; between_commands := new_between_commands; t | [< ''?'; s >] ep -> let t = parse_after_qmark loc bp s in comment_stop bp; (t, set_loc_pos loc ep bp) @@ -590,9 +602,9 @@ let rec next_token loc = parser bp (try find_keyword loc id s with Not_found -> IDENT id), set_loc_pos loc bp ep | AsciiChar | Utf8Token ((Unicode.Symbol | Unicode.IdentPart), _) -> let t = process_chars loc bp (Stream.next s) s in - let new_between_com = match t with - (KEYWORD ("{"|"}"),_) -> !between_com | _ -> false in - comment_stop bp; between_com := new_between_com; t + let new_between_commands = match t with + (KEYWORD ("{"|"}"),_) -> !between_commands | _ -> false in + comment_stop bp; between_commands := new_between_commands; t | EmptyStream -> comment_stop bp; (EOI, set_loc_pos loc bp (bp+1)) diff --git a/parsing/cLexer.mli b/parsing/cLexer.mli index 3b4891d9a..3ad49eb74 100644 --- a/parsing/cLexer.mli +++ b/parsing/cLexer.mli @@ -34,12 +34,12 @@ type frozen_t val freeze : unit -> frozen_t val unfreeze : frozen_t -> unit -type com_state -val com_state: unit -> com_state -val restore_com_state: com_state -> unit - val xml_output_comment : (string -> unit) Hook.t +(* Retrieve the comments lexed at a given location of the stream + currently being processeed *) +val extract_comments : int -> string list + val terminal : string -> Tok.t (** The lexer of Coq: *) diff --git a/parsing/compat.ml4 b/parsing/compat.ml4 index 389c34fa5..58b74da26 100644 --- a/parsing/compat.ml4 +++ b/parsing/compat.ml4 @@ -138,12 +138,21 @@ module type LexerSig = sig exception E of t val to_string : t -> string end + type comments_state + val default_comments_state : comments_state + val comments_state : unit -> comments_state + val restore_comments_state : comments_state -> unit end ELSE -module type LexerSig = - Camlp4.Sig.Lexer with module Loc = CompatLoc and type Token.t = Tok.t +module type LexerSig = sig + include Camlp4.Sig.Lexer with module Loc = CompatLoc and type Token.t = Tok.t + type comments_state + val default_comments_state : comments_state + val comments_state : unit -> comments_state + val restore_comments_state : comments_state -> unit +end END @@ -162,10 +171,13 @@ module type GrammarSig = sig string option * Gramext.g_assoc option * production_rule list type extend_statment = Gramext.position option * single_extend_statment list + type coq_parsable + val parsable : char Stream.t -> coq_parsable val action : 'a -> action val entry_create : string -> 'a entry - val entry_parse : 'a entry -> parsable -> 'a + val entry_parse : 'a entry -> coq_parsable -> 'a val entry_print : Format.formatter -> 'a entry -> unit + val with_parsable : coq_parsable -> ('a -> 'b) -> 'a -> 'b val srules' : production_rule list -> symbol val parse_tokens_after_filter : 'a entry -> Tok.t Stream.t -> 'a end @@ -181,14 +193,33 @@ module GrammarMake (L:LexerSig) : GrammarSig = struct string option * Gramext.g_assoc option * production_rule list type extend_statment = Gramext.position option * single_extend_statment list + type coq_parsable = parsable * L.comments_state ref + let parsable c = + let state = ref L.default_comments_state in (parsable c, state) let action = Gramext.action let entry_create = Entry.create - let entry_parse e p = - try Entry.parse e p + let entry_parse e (p,state) = + L.restore_comments_state !state; + try + let c = Entry.parse e p in + state := L.comments_state (); + L.restore_comments_state L.default_comments_state; + c with Exc_located (loc,e) -> + L.restore_comments_state L.default_comments_state; let loc' = Loc.get_loc (Exninfo.info e) in let loc = match loc' with None -> to_coqloc loc | Some loc -> loc in Loc.raise ~loc e + let with_parsable (p,state) f x = + L.restore_comments_state !state; + try + let a = f x in + state := L.comments_state (); + L.restore_comments_state L.default_comments_state; + a + with e -> + L.restore_comments_state L.default_comments_state; + raise e let entry_print ft x = Entry.print ft x let srules' = Gramext.srules @@ -202,12 +233,13 @@ module type GrammarSig = sig with module Loc = CompatLoc and type Token.t = Tok.t type 'a entry = 'a Entry.t type action = Action.t - type parsable - val parsable : char Stream.t -> parsable + type coq_parsable + val parsable : char Stream.t -> coq_parsable val action : 'a -> action val entry_create : string -> 'a entry - val entry_parse : 'a entry -> parsable -> 'a + val entry_parse : 'a entry -> coq_parsable -> 'a val entry_print : Format.formatter -> 'a entry -> unit + val with_parsable : coq_parsable -> ('a -> 'b) -> 'a -> 'b val srules' : production_rule list -> symbol end @@ -217,13 +249,31 @@ module GrammarMake (L:LexerSig) : GrammarSig = struct include Camlp4.Struct.Grammar.Static.Make (L) type 'a entry = 'a Entry.t type action = Action.t - type parsable = char Stream.t - let parsable s = s + type comments_state = int option * string * bool * ((int * int) * string) list + type coq_parsable = char Stream.t * L.comments_state ref + let parsable s = let state = ref L.default_comments_state in (s, state) let action = Action.mk let entry_create = Entry.mk - let entry_parse e s = - try parse e (*FIXME*)CompatLoc.ghost s - with Exc_located (loc,e) -> raise_coq_loc loc e + let entry_parse e (s,state) = + L.restore_comments_state !state; + try + let c = parse e (*FIXME*)CompatLoc.ghost s in + state := L.comments_state (); + L.restore_comments_state L.default_comments_state; + c + with Exc_located (loc,e) -> + L.restore_comments_state L.default_comments_state; + raise_coq_loc loc e + let with_parsable (p,state) f x = + L.restore_comments_state !state; + try + let a = f x in + state := L.comments_state (); + L.restore_comments_state L.default_comments_state; + a + with e -> + L.restore_comments_state L.default_comments_state; + raise e let entry_print ft x = Entry.print ft x let srules' = srules (entry_create "dummy") end diff --git a/pretyping/cases.ml b/pretyping/cases.ml index 0d30b3e4c..02fb515b0 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -1870,22 +1870,16 @@ let inh_conv_coerce_to_tycon loc env evdref j tycon = (* We put the tycon inside the arity signature, possibly discovering dependencies. *) -let add_subst c len (rel_subst,var_subst) = - match kind_of_term c with - | Rel n -> (n,len) :: rel_subst, var_subst - | Var id -> rel_subst, (id,len) :: var_subst - | _ -> assert false - let prepare_predicate_from_arsign_tycon env sigma loc tomatchs arsign c = let nar = List.fold_left (fun n sign -> Context.Rel.nhyps sign + n) 0 arsign in - let (rel_subst,var_subst), len = + let subst, len = List.fold_right2 (fun (tm, tmtype) sign (subst, len) -> let signlen = List.length sign in match kind_of_term tm with - | Rel _ | Var _ when dependent tm c + | Rel n when dependent tm c && Int.equal signlen 1 (* The term to match is not of a dependent type itself *) -> - (add_subst tm len subst, len - signlen) - | Rel _ | Var _ when signlen > 1 (* The term is of a dependent type, + ((n, len) :: subst, len - signlen) + | Rel n when signlen > 1 (* The term is of a dependent type, maybe some variable in its type appears in the tycon. *) -> (match tmtype with NotInd _ -> (subst, len - signlen) @@ -1894,36 +1888,28 @@ let prepare_predicate_from_arsign_tycon env sigma loc tomatchs arsign c = List.fold_left (fun (subst, len) arg -> match kind_of_term arg with - | Rel _ | Var _ when dependent arg c -> - (add_subst arg len subst, pred len) + | Rel n when dependent arg c -> + ((n, len) :: subst, pred len) | _ -> (subst, pred len)) (subst, len) realargs in let subst = - if dependent tm c && List.for_all (fun c -> isRel c || isVar c) realargs - then add_subst tm len subst else subst + if dependent tm c && List.for_all isRel realargs + then (n, len) :: subst else subst in (subst, pred len)) | _ -> (subst, len - signlen)) - (List.rev tomatchs) arsign (([],[]), nar) + (List.rev tomatchs) arsign ([], nar) in let rec predicate lift c = match kind_of_term c with | Rel n when n > lift -> (try (* Make the predicate dependent on the matched variable *) - let idx = Int.List.assoc (n - lift) rel_subst in + let idx = Int.List.assoc (n - lift) subst in mkRel (idx + lift) with Not_found -> - (* A variable that is not matched, lift over the arsign *) + (* A variable that is not matched, lift over the arsign. *) mkRel (n + nar)) - | Var id -> - (try - (* Make the predicate dependent on the matched variable *) - let idx = Id.List.assoc id var_subst in - mkRel (idx + lift) - with Not_found -> - (* A variable that is not matched *) - c) | _ -> map_constr_with_binders succ predicate lift c in @@ -1944,39 +1930,38 @@ let prepare_predicate_from_arsign_tycon env sigma loc tomatchs arsign c = let prepare_predicate loc typing_fun env sigma tomatchs arsign tycon pred = let preds = - match pred with + match pred, tycon with (* No return clause *) - | None -> - let sigma,t = - match tycon with - | Some t -> sigma, t - | None -> - (* No type constraint: we first create a generic evar type constraint *) - let src = (loc, Evar_kinds.CasesType false) in - let sigma = Sigma.Unsafe.of_evar_map sigma in - let Sigma ((t, _), sigma, _) = new_type_evar env sigma univ_flexible_alg ~src in - let sigma = Sigma.to_evar_map sigma in - sigma, t in - (* First strategy: we build an "inversion" predicate, also replacing the *) - (* dependencies with existential variables *) + | None, Some t when not (noccur_with_meta 0 max_int t) -> + (* If the tycon is not closed w.r.t real variables, we try *) + (* two different strategies *) + (* First strategy: we build an "inversion" predicate *) let sigma1,pred1 = build_inversion_problem loc env sigma tomatchs t in (* Optional second strategy: we abstract the tycon wrt to the dependencies *) let p2 = prepare_predicate_from_arsign_tycon env sigma loc tomatchs arsign t in - (* Third strategy: we take the type constraint as it is; of course we could *) - (* need something inbetween, abstracting some but not all of the dependencies *) - (* the "inversion" strategy deals with that but unification may not be *) - (* powerful enough so strategy 2 and 3 helps; moreover, inverting does not *) - (* work (yet) when a constructor has a type not precise enough for the inversion *) - (* see log message for details *) - let pred3 = lift (List.length (List.flatten arsign)) t in (match p2 with - | Some (sigma2,pred2) when not (Constr.equal pred2 pred3) -> - [sigma1, pred1; sigma2, pred2; sigma, pred3] - | _ -> - [sigma1, pred1; sigma, pred3]) + | Some (sigma2,pred2) -> [sigma1, pred1; sigma2, pred2] + | None -> [sigma1, pred1]) + | None, _ -> + (* No dependent type constraint, or no constraints at all: *) + (* we use two strategies *) + let sigma,t = match tycon with + | Some t -> sigma,t + | None -> + let sigma = Sigma.Unsafe.of_evar_map sigma in + let Sigma ((t, _), sigma, _) = + new_type_evar env sigma univ_flexible_alg ~src:(loc, Evar_kinds.CasesType false) in + let sigma = Sigma.to_evar_map sigma in + sigma, t + in + (* First strategy: we build an "inversion" predicate *) + let sigma1,pred1 = build_inversion_problem loc env sigma tomatchs t in + (* Second strategy: we use the evar or tycon as a non dependent pred *) + let pred2 = lift (List.length (List.flatten arsign)) t in + [sigma1, pred1; sigma, pred2] (* Some type annotation *) - | Some rtntyp -> + | Some rtntyp, _ -> (* We extract the signature of the arity *) let envar = List.fold_right push_rel_context arsign env in let sigma, newt = new_sort_variable univ_flexible_alg sigma in diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml index fa5a70899..c94650f1e 100644 --- a/printing/ppconstr.ml +++ b/printing/ppconstr.ml @@ -129,7 +129,7 @@ end) = struct str "`" ++ str hd ++ c ++ str tl let pr_com_at n = - if Flags.do_beautify() && not (Int.equal n 0) then comment n + if Flags.do_beautify() && not (Int.equal n 0) then comment (CLexer.extract_comments n) else mt() let pr_with_comments loc pp = pr_located (fun x -> x) (loc,pp) diff --git a/printing/pputils.ml b/printing/pputils.ml index 33382fe83..491688913 100644 --- a/printing/pputils.ml +++ b/printing/pputils.ml @@ -17,7 +17,11 @@ open Genredexpr let pr_located pr (loc, x) = if Flags.do_beautify () && loc <> Loc.ghost then let (b, e) = Loc.unloc loc in - Pp.comment b ++ pr x ++ Pp.comment e + (* Side-effect: order matters *) + let before = Pp.comment (CLexer.extract_comments b) in + let x = pr x in + let after = Pp.comment (CLexer.extract_comments e) in + before ++ x ++ after else pr x let pr_or_var pr = function diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml index 7c00106e2..5d7249aff 100644 --- a/printing/ppvernac.ml +++ b/printing/ppvernac.ml @@ -261,7 +261,7 @@ module Make let pr_decl_notation prc ((loc,ntn),c,scopt) = fnl () ++ keyword "where " ++ qs ntn ++ str " := " - ++ Flags.without_option Flags.beautify_file prc c ++ + ++ Flags.without_option Flags.beautify prc c ++ pr_opt (fun sc -> str ": " ++ str sc) scopt let pr_binders_arg = @@ -381,7 +381,7 @@ module Make | Some pl -> str"@{" ++ prlist_with_sep spc pr_lident pl ++ str"}" let pr_rec_definition ((((loc,id),pl),ro,bl,type_,def),ntn) = - let pr_pure_lconstr c = Flags.without_option Flags.beautify_file pr_lconstr c in + let pr_pure_lconstr c = Flags.without_option Flags.beautify pr_lconstr c in let annot = pr_guard_annot pr_lconstr_expr bl ro in pr_id id ++ pr_univs pl ++ pr_binders_arg bl ++ annot ++ pr_type_option (fun c -> spc() ++ pr_lconstr_expr c) type_ @@ -676,7 +676,7 @@ module Make | VernacNotation (_,c,((_,s),l),opt) -> return ( hov 2 (keyword "Notation" ++ spc() ++ qs s ++ - str " :=" ++ Flags.without_option Flags.beautify_file pr_constrarg c ++ pr_syntax_modifiers l ++ + str " :=" ++ Flags.without_option Flags.beautify pr_constrarg c ++ pr_syntax_modifiers l ++ (match opt with | None -> mt() | Some sc -> str" :" ++ spc() ++ str sc)) @@ -758,7 +758,7 @@ module Make let pr_constructor (coe,(id,c)) = hov 2 (pr_lident id ++ str" " ++ (if coe then str":>" else str":") ++ - Flags.without_option Flags.beautify_file pr_spc_lconstr c) + Flags.without_option Flags.beautify pr_spc_lconstr c) in let pr_constructor_list b l = match l with | Constructors [] -> mt() diff --git a/proofs/proof.ml b/proofs/proof.ml index 16278b456..0a3b08c04 100644 --- a/proofs/proof.ml +++ b/proofs/proof.ml @@ -351,7 +351,14 @@ let run_tactic env tac pr = Proofview.apply env tac sp in let sigma = Proofview.return proofview in - let shelf = (undef sigma pr.shelf)@retrieved@(undef sigma to_shelve) in + let to_shelve = undef sigma to_shelve in + let shelf = (undef sigma pr.shelf)@retrieved@to_shelve in + let proofview = + List.fold_left + Proofview.Unsafe.mark_as_unresolvable + proofview + to_shelve + in let given_up = pr.given_up@give_up in let proofview = Proofview.Unsafe.reset_future_goals proofview in { pr with proofview ; shelf ; given_up },(status,info_trace) diff --git a/proofs/refine.ml b/proofs/refine.ml index ecc461f78..d4920e505 100644 --- a/proofs/refine.ml +++ b/proofs/refine.ml @@ -53,6 +53,23 @@ let typecheck_proof c concl env sigma = let (pr_constrv,pr_constr) = Hook.make ~default:(fun _env _sigma _c -> Pp.str"<constr>") () +(* Get the side-effect's constant declarations to update the monad's + * environmnent *) +let add_if_undefined kn cb env = + try ignore(Environ.lookup_constant kn env); env + with Not_found -> Environ.add_constant kn cb env + +(* Add the side effects to the monad's environment, if not already done. *) +let add_side_effect env = function + | { Entries.eff = Entries.SEsubproof (kn, cb, eff_env) } -> + add_if_undefined kn cb env + | { Entries.eff = Entries.SEscheme (l,_) } -> + List.fold_left (fun env (_,kn,cb,eff_env) -> + add_if_undefined kn cb env) env l + +let add_side_effects env effects = + List.fold_left (fun env eff -> add_side_effect env eff) env effects + let make_refine_enter ?(unsafe = true) f = { enter = fun gl -> let gl = Proofview.Goal.assume gl in @@ -68,6 +85,10 @@ let make_refine_enter ?(unsafe = true) f = let ((v,c), sigma) = Sigma.run (Evd.reset_future_goals sigma) f in let evs = Evd.future_goals sigma in let evkmain = Evd.principal_future_goal sigma in + (** Redo the effects in sigma in the monad's env *) + let privates_csts = Evd.eval_side_effects sigma in + let sideff = Safe_typing.side_effects_of_private_constants privates_csts in + let env = add_side_effects env sideff in (** Check that the introduced evars are well-typed *) let fold accu ev = typecheck_evar ev env accu in let sigma = if unsafe then sigma else CList.fold_left fold sigma evs in @@ -96,6 +117,7 @@ let make_refine_enter ?(unsafe = true) f = let sigma = CList.fold_left Proofview.Unsafe.mark_as_goal sigma comb in let trace () = Pp.(hov 2 (str"simple refine"++spc()++ Hook.get pr_constrv env sigma c)) in Proofview.Trace.name_tactic trace (Proofview.tclUNIT v) >>= fun v -> + Proofview.Unsafe.tclSETENV (Environ.reset_context env) <*> Proofview.Unsafe.tclEVARS sigma <*> Proofview.Unsafe.tclSETGOALS comb <*> Proofview.tclUNIT v diff --git a/tactics/auto.ml b/tactics/auto.ml index 1cb71da69..c66fad651 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -374,7 +374,7 @@ and my_find_search_delta db_list local_db hdc concl = in List.map (fun x -> (Some flags,x)) l) (local_db::db_list) -and tac_of_hint dbg db_list local_db concl (flags, ({pat=p; code=t;poly=poly})) = +and tac_of_hint dbg db_list local_db concl (flags, ({pat=p; code=t;poly=poly;db=dbname})) = let tactic = function | Res_pf (c,cl) -> unify_resolve_gen poly flags (c,cl) | ERes_pf _ -> Proofview.V82.tactic (fun gl -> error "eres_pf") @@ -393,7 +393,14 @@ and tac_of_hint dbg db_list local_db concl (flags, ({pat=p; code=t;poly=poly})) | Extern tacast -> conclPattern concl p tacast in - tclLOG dbg (fun () -> pr_hint t) (run_hint t tactic) + let pr_hint () = + let origin = match dbname with + | None -> mt () + | Some n -> str " (in " ++ str n ++ str ")" + in + pr_hint t ++ origin + in + tclLOG dbg pr_hint (run_hint t tactic) and trivial_resolve dbg mod_delta db_list local_db cl = try diff --git a/tactics/auto.mli b/tactics/auto.mli index 1689bd73c..3ee96353f 100644 --- a/tactics/auto.mli +++ b/tactics/auto.mli @@ -16,8 +16,6 @@ open Decl_kinds open Hints open Tactypes -val priority : ('a * full_hint) list -> ('a * full_hint) list - val default_search_depth : int ref val auto_flags_of_state : transparent_state -> Unification.unify_flags diff --git a/tactics/hints.ml b/tactics/hints.ml index ac945de3c..7dc40079e 100644 --- a/tactics/hints.ml +++ b/tactics/hints.ml @@ -111,6 +111,7 @@ type 'a with_metadata = { poly : polymorphic; (** Is the hint polymorpic and hence should be refreshed at each application *) pat : constr_pattern option; (* A pattern for the concl of the Goal *) name : hints_path_atom; (* A potential name to refer to the hint *) + db : string option; (** The database from which the hint comes *) code : 'a; (* the tactic to apply when the concl matches pat *) } @@ -413,7 +414,35 @@ let rec subst_hints_path subst hp = if p' == p && q' == q then hp else PathOr (p', q') | _ -> hp -module Hint_db = struct +type hint_db_name = string + +module Hint_db : +sig +type t +val empty : ?name:hint_db_name -> transparent_state -> bool -> t +val find : global_reference -> t -> search_entry +val map_none : t -> full_hint list +val map_all : global_reference -> t -> full_hint list +val map_existential : (global_reference * constr array) -> constr -> t -> full_hint list +val map_eauto : (global_reference * constr array) -> constr -> t -> full_hint list +val map_auto : (global_reference * constr array) -> constr -> t -> full_hint list +val add_one : env -> evar_map -> hint_entry -> t -> t +val add_list : env -> evar_map -> hint_entry list -> t -> t +val remove_one : global_reference -> t -> t +val remove_list : global_reference list -> t -> t +val iter : (global_reference option -> hint_mode array list -> full_hint list -> unit) -> t -> unit +val use_dn : t -> bool +val transparent_state : t -> transparent_state +val set_transparent_state : t -> transparent_state -> t +val add_cut : hints_path -> t -> t +val add_mode : global_reference -> hint_mode array -> t -> t +val cut : t -> hints_path +val unfolds : t -> Id.Set.t * Cset.t +val fold : (global_reference option -> hint_mode array list -> full_hint list -> 'a -> 'a) -> + t -> 'a -> 'a + +end = +struct type t = { hintdb_state : Names.transparent_state; @@ -424,20 +453,22 @@ module Hint_db = struct hintdb_map : search_entry Constr_map.t; (* A list of unindexed entries starting with an unfoldable constant or with no associated pattern. *) - hintdb_nopat : (global_reference option * stored_data) list + hintdb_nopat : (global_reference option * stored_data) list; + hintdb_name : string option; } let next_hint_id db = let h = db.hintdb_max_id in { db with hintdb_max_id = succ db.hintdb_max_id }, h - let empty st use_dn = { hintdb_state = st; + let empty ?name st use_dn = { hintdb_state = st; hintdb_cut = PathEmpty; hintdb_unfolds = (Id.Set.empty, Cset.empty); hintdb_max_id = 0; use_dn = use_dn; hintdb_map = Constr_map.empty; - hintdb_nopat = [] } + hintdb_nopat = []; + hintdb_name = name; } let find key db = try Constr_map.find key db.hintdb_map @@ -505,7 +536,7 @@ module Hint_db = struct | _ -> false let addkv gr id v db = - let idv = id, v in + let idv = id, { v with db = db.hintdb_name } in let k = match gr with | Some gr -> if db.use_dn && is_transparent_gr db.hintdb_state gr && is_unfold v.code.obj then None else Some gr @@ -609,8 +640,6 @@ type hint_db = Hint_db.t type hint_db_table = hint_db Hintdbmap.t ref -type hint_db_name = string - (** Initially created hint databases, for typeclasses and rewrite *) let typeclasses_db = "typeclass_instances" @@ -687,6 +716,7 @@ let make_exact_entry env sigma pri poly ?(name=PathAny) (c, cty, ctx) = poly = poly; pat = Some pat; name = name; + db = None; code = with_uid (Give_exact (c, cty, ctx)); }) let make_apply_entry env sigma (eapply,hnf,verbose) pri poly ?(name=PathAny) (c, cty, ctx) = @@ -707,6 +737,7 @@ let make_apply_entry env sigma (eapply,hnf,verbose) pri poly ?(name=PathAny) (c, poly = poly; pat = Some pat; name = name; + db = None; code = with_uid (Res_pf(c,cty,ctx)); }) else begin if not eapply then failwith "make_apply_entry"; @@ -718,6 +749,7 @@ let make_apply_entry env sigma (eapply,hnf,verbose) pri poly ?(name=PathAny) (c, poly = poly; pat = Some pat; name = name; + db = None; code = with_uid (ERes_pf(c,cty,ctx)); }) end | _ -> failwith "make_apply_entry" @@ -802,6 +834,7 @@ let make_unfold eref = poly = false; pat = None; name = PathHints [g]; + db = None; code = with_uid (Unfold_nth eref) }) let make_extern pri pat tacast = @@ -811,6 +844,7 @@ let make_extern pri pat tacast = poly = false; pat = pat; name = PathAny; + db = None; code = with_uid (Extern tacast) }) let make_mode ref m = @@ -834,6 +868,7 @@ let make_trivial env sigma poly ?(name=PathAny) r = poly = poly; pat = Some (Patternops.pattern_of_constr env ce.evd (clenv_type ce)); name = name; + db = None; code= with_uid (Res_pf_THEN_trivial_fail(c,t,ctx)) }) @@ -847,7 +882,7 @@ let make_trivial env sigma poly ?(name=PathAny) r = let get_db dbname = try searchtable_map dbname - with Not_found -> Hint_db.empty empty_transparent_state false + with Not_found -> Hint_db.empty ~name:dbname empty_transparent_state false let add_hint dbname hintlist = let check (_, h) = @@ -907,7 +942,7 @@ type hint_obj = { let load_autohint _ (kn, h) = let name = h.hint_name in match h.hint_action with - | CreateDB (b, st) -> searchtable_add (name, Hint_db.empty st b) + | CreateDB (b, st) -> searchtable_add (name, Hint_db.empty ~name st b) | AddTransparency (grs, b) -> add_transparency name grs b | AddHints hints -> add_hint name hints | RemoveHints grs -> remove_hint name grs diff --git a/tactics/hints.mli b/tactics/hints.mli index 9a3817203..48351a317 100644 --- a/tactics/hints.mli +++ b/tactics/hints.mli @@ -46,11 +46,14 @@ type hints_path_atom = (* For forward hints, their names is the list of projections *) | PathAny +type hint_db_name = string + type 'a with_metadata = private { pri : int; (** A number between 0 and 4, 4 = lower priority *) poly : polymorphic; (** Is the hint polymorpic and hence should be refreshed at each application *) pat : constr_pattern option; (** A pattern for the concl of the Goal *) name : hints_path_atom; (** A potential name to refer to the hint *) + db : hint_db_name option; code : 'a; (** the tactic to apply when the concl matches pat *) } @@ -80,7 +83,7 @@ val pp_hint_mode : hint_mode -> Pp.std_ppcmds module Hint_db : sig type t - val empty : transparent_state -> bool -> t + val empty : ?name:hint_db_name -> transparent_state -> bool -> t val find : global_reference -> t -> search_entry val map_none : t -> full_hint list @@ -116,8 +119,6 @@ module Hint_db : val unfolds : t -> Id.Set.t * Cset.t end -type hint_db_name = string - type hint_db = Hint_db.t type hnf = bool diff --git a/test-suite/bugs/closed/4416.v b/test-suite/bugs/closed/4416.v new file mode 100644 index 000000000..b97a8ce64 --- /dev/null +++ b/test-suite/bugs/closed/4416.v @@ -0,0 +1,3 @@ +Goal exists x, x. +unshelve refine (ex_intro _ _ _); match goal with _ => refine (_ _) end. +(* Error: Incorrect number of goals (expected 2 tactics). *)
\ No newline at end of file diff --git a/test-suite/bugs/closed/4863.v b/test-suite/bugs/closed/4863.v new file mode 100644 index 000000000..e884355fd --- /dev/null +++ b/test-suite/bugs/closed/4863.v @@ -0,0 +1,32 @@ +Require Import Classes.DecidableClass. + +Inductive Foo : Set := +| foo1 | foo2. + +Instance Decidable_sumbool : forall P, {P}+{~P} -> Decidable P. +Proof. + intros P H. + refine (Build_Decidable _ (if H then true else false) _). + intuition congruence. +Qed. + +Hint Extern 100 ({?A = ?B}+{~ ?A = ?B}) => abstract (abstract (abstract (decide equality))) : typeclass_instances. + +Goal forall (a b : Foo), {a=b}+{a<>b}. +intros. +abstract (abstract (decide equality)). (*abstract works here*) +Qed. + +Check ltac:(abstract (exact I)) : True. + +Goal forall (a b : Foo), Decidable (a=b) * Decidable (a=b). +intros. +split. typeclasses eauto. typeclasses eauto. Qed. + +Goal forall (a b : Foo), Decidable (a=b) * Decidable (a=b). +intros. +split. +refine _. +refine _. +Defined. +(*fails*) diff --git a/test-suite/bugs/closed/5123.v b/test-suite/bugs/closed/5123.v new file mode 100644 index 000000000..bcde510ee --- /dev/null +++ b/test-suite/bugs/closed/5123.v @@ -0,0 +1,33 @@ +(* IN 8.5pl2 and 8.6 (4da2131), the following shows different typeclass resolution behaviors following an unshelve tactical vs. an Unshelve command: *) + +(*Pose an open constr to prevent immediate typeclass resolution in holes:*) +Tactic Notation "opose" open_constr(x) "as" ident(H) := pose x as H. + +Inductive vect A : nat -> Type := +| vnil : vect A 0 +| vcons : forall (h:A) (n:nat), vect A n -> vect A (S n). + +Class Eqdec A := eqdec : forall a b : A, {a=b}+{a<>b}. + +Require Bool. + +Instance Bool_eqdec : Eqdec bool := Bool.bool_dec. + +Context `{vect_sigT_eqdec : forall A : Type, Eqdec A -> Eqdec {a : nat & vect A a}}. + +Typeclasses eauto := debug. + +Goal True. + unshelve opose (@vect_sigT_eqdec _ _ _ _) as H. + all:cycle 2. + eapply existT. (*BUG: Why does this do typeclass resolution in the evar?*) + Focus 5. +Abort. + +Goal True. + opose (@vect_sigT_eqdec _ _ _ _) as H. + Unshelve. + all:cycle 3. + eapply existT. (*This does no typeclass resultion, which is correct.*) + Focus 5. +Abort.
\ No newline at end of file diff --git a/test-suite/success/Case13.v b/test-suite/success/Case13.v index 356a67efe..8f95484cf 100644 --- a/test-suite/success/Case13.v +++ b/test-suite/success/Case13.v @@ -87,41 +87,3 @@ Check fun (x : E) => match x with c => e c end. Inductive C' : bool -> Set := c' : C' true. Inductive E' (b : bool) : Set := e' :> C' b -> E' b. Check fun (x : E' true) => match x with c' => e' true c' end. - -(* Check use of the no-dependency strategy when a type constraint is - given (and when the "inversion-and-dependencies-as-evars" strategy - is not strong enough because of a constructor with a type whose - pattern structure is not refined enough for it to be captured by - the inversion predicate) *) - -Inductive K : bool -> bool -> Type := F : K true true | G x : K x x. - -Check fun z P Q (y:K true z) (H1 H2:P y) (f:forall y, P y -> Q y z) => - match y with - | F => f y H1 - | G _ => f y H2 - end : Q y z. - -(* Check use of the maximal-dependency-in-variable strategy even when - no explicit type constraint is given (and when the - "inversion-and-dependencies-as-evars" strategy is not strong enough - because of a constructor with a type whose pattern structure is not - refined enough for it to be captured by the inversion predicate) *) - -Check fun z P Q (y:K true z) (H1 H2:P y) (f:forall y z, P y -> Q y z) => - match y with - | F => f y true H1 - | G b => f y b H2 - end. - -(* Check use of the maximal-dependency-in-variable strategy for "Var" - variables *) - -Goal forall z P Q (y:K true z) (H1 H2:P y) (f:forall y z, P y -> Q y z), Q y z. -intros z P Q y H1 H2 f. -Show. -refine (match y with - | F => f y true H1 - | G b => f y b H2 - end). -Qed. diff --git a/test-suite/success/Typeclasses.v b/test-suite/success/Typeclasses.v index dfa438d90..3eaa04144 100644 --- a/test-suite/success/Typeclasses.v +++ b/test-suite/success/Typeclasses.v @@ -5,7 +5,7 @@ Record Equ (A : Type) (R : A -> A -> Prop). Definition equiv {A} R (e : Equ A R) := R. Record Refl (A : Type) (R : A -> A -> Prop). Axiom equ_refl : forall A R (e : Equ A R), Refl _ (@equiv A R e). -Hint Extern 0 (Refl _ _) => unshelve class_apply @equ_refl; [|shelve|] : foo. +Hint Extern 0 (Refl _ _) => unshelve class_apply @equ_refl; [shelve|] : foo. Variable R : nat -> nat -> Prop. Lemma bas : Equ nat R. diff --git a/theories/FSets/FSetDecide.v b/theories/FSets/FSetDecide.v index ad067eb3d..1db6a71e8 100644 --- a/theories/FSets/FSetDecide.v +++ b/theories/FSets/FSetDecide.v @@ -357,17 +357,8 @@ the above form: | _ => idtac end. - (** [if t then t1 else t2] executes [t] and, if it does not - fail, then [t1] will be applied to all subgoals - produced. If [t] fails, then [t2] is executed. *) - Tactic Notation - "if" tactic(t) - "then" tactic(t1) - "else" tactic(t2) := - first [ t; first [ t1 | fail 2 ] | t2 ]. - Ltac abstract_term t := - if (is_var t) then fail "no need to abstract a variable" + tryif (is_var t) then fail "no need to abstract a variable" else (let x := fresh "x" in set (x := t) in *; try clearbody x). Ltac abstract_elements := @@ -478,11 +469,11 @@ the above form: repeat ( match goal with | H : context [ @Logic.eq ?T ?x ?y ] |- _ => - if (change T with E.t in H) then fail - else if (change T with t in H) then fail + tryif (change T with E.t in H) then fail + else tryif (change T with t in H) then fail else clear H | H : ?P |- _ => - if prop (FSet_Prop P) holds by + tryif prop (FSet_Prop P) holds by (auto 100 with FSet_Prop) then fail else clear H @@ -747,7 +738,7 @@ the above form: | H: (In ?x ?r) -> False |- (E.eq ?y ?x) -> False => contradict H; fsetdec_body | H: ?P -> False |- ?Q -> False => - if prop (FSet_elt_Prop P) holds by + tryif prop (FSet_elt_Prop P) holds by (auto 100 with FSet_Prop) then (contradict H; fsetdec_body) else fsetdec_body diff --git a/theories/MSets/MSetDecide.v b/theories/MSets/MSetDecide.v index f2555791b..9c622fd78 100644 --- a/theories/MSets/MSetDecide.v +++ b/theories/MSets/MSetDecide.v @@ -357,17 +357,8 @@ the above form: | _ => idtac end. - (** [if t then t1 else t2] executes [t] and, if it does not - fail, then [t1] will be applied to all subgoals - produced. If [t] fails, then [t2] is executed. *) - Tactic Notation - "if" tactic(t) - "then" tactic(t1) - "else" tactic(t2) := - first [ t; first [ t1 | fail 2 ] | t2 ]. - Ltac abstract_term t := - if (is_var t) then fail "no need to abstract a variable" + tryif (is_var t) then fail "no need to abstract a variable" else (let x := fresh "x" in set (x := t) in *; try clearbody x). Ltac abstract_elements := @@ -478,11 +469,11 @@ the above form: repeat ( match goal with | H : context [ @Logic.eq ?T ?x ?y ] |- _ => - if (change T with E.t in H) then fail - else if (change T with t in H) then fail + tryif (change T with E.t in H) then fail + else tryif (change T with t in H) then fail else clear H | H : ?P |- _ => - if prop (MSet_Prop P) holds by + tryif prop (MSet_Prop P) holds by (auto 100 with MSet_Prop) then fail else clear H @@ -747,7 +738,7 @@ the above form: | H: (In ?x ?r) -> False |- (E.eq ?y ?x) -> False => contradict H; fsetdec_body | H: ?P -> False |- ?Q -> False => - if prop (MSet_elt_Prop P) holds by + tryif prop (MSet_elt_Prop P) holds by (auto 100 with MSet_Prop) then (contradict H; fsetdec_body) else fsetdec_body diff --git a/theories/Structures/OrdersFacts.v b/theories/Structures/OrdersFacts.v index 6f8fc1b32..0115d8a54 100644 --- a/theories/Structures/OrdersFacts.v +++ b/theories/Structures/OrdersFacts.v @@ -434,14 +434,14 @@ Lemma eqb_compare x y : (x =? y) = match compare x y with Eq => true | _ => false end. Proof. apply eq_true_iff_eq. rewrite eqb_eq, <- compare_eq_iff. -destruct compare; now split. +now destruct compare. Qed. Lemma ltb_compare x y : (x <? y) = match compare x y with Lt => true | _ => false end. Proof. apply eq_true_iff_eq. rewrite ltb_lt, <- compare_lt_iff. -destruct compare; now split. +now destruct compare. Qed. Lemma leb_compare x y : diff --git a/toplevel/coqloop.ml b/toplevel/coqloop.ml index 69d68bd35..71e1f9593 100644 --- a/toplevel/coqloop.ml +++ b/toplevel/coqloop.ml @@ -23,7 +23,7 @@ type input_buffer = { mutable str : string; (* buffer of already read characters *) mutable len : int; (* number of chars in the buffer *) mutable bols : int list; (* offsets in str of beginning of lines *) - mutable tokens : Gram.parsable; (* stream of tokens *) + mutable tokens : Gram.coq_parsable; (* stream of tokens *) mutable start : int } (* stream count of the first char of the buffer *) (* Double the size of the buffer. *) @@ -274,9 +274,9 @@ let rec discard_to_dot () = | End_of_input -> raise End_of_input | e when CErrors.noncritical e -> () -let read_sentence () = +let read_sentence input = try - let (loc, _ as r) = Vernac.parse_sentence (top_buffer.tokens, None) in + let (loc, _ as r) = Vernac.parse_sentence input in CWarnings.set_current_loc loc; r with reraise -> let reraise = CErrors.push reraise in @@ -298,7 +298,8 @@ let do_vernac () = if !print_emacs then top_stderr (str (top_buffer.prompt())); resynch_buffer top_buffer; try - Vernac.eval_expr (read_sentence ()) + let input = (top_buffer.tokens, None) in + Vernac.eval_expr input (read_sentence input) with | End_of_input | CErrors.Quit -> top_stderr (fnl ()); raise CErrors.Quit diff --git a/toplevel/coqloop.mli b/toplevel/coqloop.mli index 00554da30..e40353e0f 100644 --- a/toplevel/coqloop.mli +++ b/toplevel/coqloop.mli @@ -18,7 +18,7 @@ type input_buffer = { mutable str : string; (** buffer of already read characters *) mutable len : int; (** number of chars in the buffer *) mutable bols : int list; (** offsets in str of begining of lines *) - mutable tokens : Pcoq.Gram.parsable; (** stream of tokens *) + mutable tokens : Pcoq.Gram.coq_parsable; (** stream of tokens *) mutable start : int } (** stream count of the first char of the buffer *) (** The input buffer of stdin. *) diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml index 07bccb532..a37859c9c 100644 --- a/toplevel/vernac.ml +++ b/toplevel/vernac.ml @@ -124,34 +124,37 @@ let set_formatter_translator() = Format.set_formatter_output_functions out (fun () -> flush ch); Format.set_max_boxes max_int -let pr_new_syntax loc ocom = +let pr_new_syntax_in_context loc ocom = let loc = Loc.unloc loc in if !beautify_file then set_formatter_translator(); let fs = States.freeze ~marshallable:`No in + (* Side-effect: order matters *) + let before = comment (CLexer.extract_comments (fst loc)) in let com = match ocom with | Some com -> Ppvernac.pr_vernac com | None -> mt() in + let after = comment (CLexer.extract_comments (snd loc)) in if !beautify_file then - Feedback.msg_notice (hov 0 (comment (fst loc) ++ com ++ comment (snd loc))) + Pp.msg_with !Pp_control.std_ft (hov 0 (before ++ com ++ after)) else Feedback.msg_info (hov 4 (str"New Syntax:" ++ fnl() ++ (hov 0 com))); States.unfreeze fs; Format.set_formatter_out_channel stdout +let pr_new_syntax (po,_) loc ocom = + (* Reinstall the context of parsing which includes the bindings of comments to locations *) + Pcoq.Gram.with_parsable po (pr_new_syntax_in_context loc) ocom + let save_translator_coqdoc () = (* translator state *) let ch = !chan_beautify in - let cl = !Pp.comments in - let cs = CLexer.com_state() in (* end translator state *) let coqdocstate = CLexer.location_table () in - ch,cl,cs,coqdocstate + ch,coqdocstate -let restore_translator_coqdoc (ch,cl,cs,coqdocstate) = +let restore_translator_coqdoc (ch,coqdocstate) = if !Flags.beautify_file then close_out !chan_beautify; chan_beautify := ch; - Pp.comments := cl; - CLexer.restore_com_state cs; CLexer.restore_location_table coqdocstate (* For coqtop -time, we display the position in the file, @@ -182,7 +185,7 @@ let print_cmd_header loc com = Pp.pp_with !Pp_control.std_ft (pp_cmd_header loc com); Format.pp_print_flush !Pp_control.std_ft () -let rec vernac_com checknav (loc,com) = +let rec vernac_com input checknav (loc,com) = let interp = function | VernacLoad (verbosely, fname) -> let fname = Envars.expand_path_macros ~warn:(fun x -> Feedback.msg_warning (str x)) fname in @@ -194,7 +197,6 @@ let rec vernac_com checknav (loc,com) = if !Flags.beautify_file then begin chan_beautify := open_out (f^beautify_suffix); - Pp.comments := [] end; begin try @@ -214,13 +216,11 @@ let rec vernac_com checknav (loc,com) = in try checknav loc com; - if do_beautify () then pr_new_syntax loc (Some com); + if do_beautify () then pr_new_syntax input loc (Some com); (* XXX: This is not 100% correct if called from an IDE context *) if !Flags.time then print_cmd_header loc com; let com = if !Flags.time then VernacTime (loc,com) else com in - let a = CLexer.com_state () in - interp com; - CLexer.restore_com_state a + interp com with reraise -> let (reraise, info) = CErrors.push reraise in Format.set_formatter_out_channel stdout; @@ -240,7 +240,7 @@ and read_vernac_file verbosely s = while true do let loc_ast = parse_sentence input in CWarnings.set_current_loc (fst loc_ast); - vernac_com checknav loc_ast; + vernac_com input checknav loc_ast; done with any -> (* whatever the exception *) let (e, info) = CErrors.push any in @@ -249,7 +249,7 @@ and read_vernac_file verbosely s = match e with | End_of_input -> if do_beautify () then - pr_new_syntax (Loc.make_loc (max_int,max_int)) None + pr_new_syntax input (Loc.make_loc (max_int,max_int)) None | reraise -> iraise (disable_drop e, info) @@ -264,7 +264,7 @@ let checknav loc ast = if is_deep_navigation_vernac ast then user_error loc "Navigation commands forbidden in nested commands" -let eval_expr loc_ast = vernac_com checknav loc_ast +let eval_expr input loc_ast = vernac_com input checknav loc_ast (* XML output hooks *) let (f_xml_start_library, xml_start_library) = Hook.make ~default:ignore () diff --git a/toplevel/vernac.mli b/toplevel/vernac.mli index 7bfddd947..2fd86ddc2 100644 --- a/toplevel/vernac.mli +++ b/toplevel/vernac.mli @@ -11,7 +11,7 @@ (** Read a vernac command on the specified input (parse only). Raises [End_of_file] if EOF (or Ctrl-D) is reached. *) -val parse_sentence : Pcoq.Gram.parsable * in_channel option -> +val parse_sentence : Pcoq.Gram.coq_parsable * in_channel option -> Loc.t * Vernacexpr.vernac_expr (** Reads and executes vernac commands from a stream. @@ -21,7 +21,7 @@ exception End_of_input val just_parsing : bool ref -val eval_expr : Loc.t * Vernacexpr.vernac_expr -> unit +val eval_expr : Pcoq.Gram.coq_parsable * in_channel option -> Loc.t * Vernacexpr.vernac_expr -> unit (** Set XML hooks *) val xml_start_library : (unit -> unit) Hook.t |