From 9043add656177eeac1491a73d2f3ab92bec0013c Mon Sep 17 00:00:00 2001 From: Benjamin Barenblat Date: Sat, 29 Dec 2018 14:31:27 -0500 Subject: Imported Upstream version 8.8.2 --- engine/proofview.ml | 366 ++++++++++++++++++++++++++++++---------------------- 1 file changed, 210 insertions(+), 156 deletions(-) (limited to 'engine/proofview.ml') diff --git a/engine/proofview.ml b/engine/proofview.ml index c0187976..22271dd0 100644 --- a/engine/proofview.ml +++ b/engine/proofview.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* i+1) solution 0 in let new_el = List.map (fun (t,ty) -> nf t, nf ty) el in let pruned_solution = Evd.drop_all_defined solution in let apply_subst_einfo _ ei = Evd.({ ei with - evar_concl = nf ei.evar_concl; - evar_hyps = Environ.map_named_val nf ei.evar_hyps; - evar_candidates = Option.map (List.map nf) ei.evar_candidates }) in + evar_concl = nf0 ei.evar_concl; + evar_hyps = Environ.map_named_val nf0 ei.evar_hyps; + evar_candidates = Option.map (List.map nf0) ei.evar_candidates }) in let new_solution = Evd.raw_map_undefined apply_subst_einfo pruned_solution in let new_size = Evd.fold (fun _ _ i -> i+1) new_solution 0 in Feedback.msg_info (Pp.str (Printf.sprintf "Evars: %d -> %d\n" size new_size)); @@ -54,7 +58,7 @@ let compact el ({ solution } as pv) = type telescope = | TNil of Evd.evar_map - | TCons of Environ.env * Evd.evar_map * Term.types * (Evd.evar_map -> Term.constr -> telescope) + | TCons of Environ.env * Evd.evar_map * EConstr.types * (Evd.evar_map -> EConstr.constr -> telescope) let typeclass_resolvable = Evd.Store.field () @@ -63,18 +67,16 @@ let dependent_init = for type classes. *) let store = Evd.Store.set Evd.Store.empty typeclass_resolvable () in (* Goals don't have a source location. *) - let src = (Loc.ghost,Evar_kinds.GoalEvar) in + let src = Loc.tag @@ Evar_kinds.GoalEvar in (* Main routine *) let rec aux = function | TNil sigma -> [], { solution = sigma; comb = []; shelf = [] } | TCons (env, sigma, typ, t) -> - let sigma = Sigma.Unsafe.of_evar_map sigma in - let Sigma (econstr, sigma, _) = Evarutil.new_evar env sigma ~src ~store typ in - let sigma = Sigma.to_evar_map sigma in + let (sigma, econstr) = Evarutil.new_evar env sigma ~src ~store typ in + let (gl, _) = EConstr.destEvar sigma econstr in let ret, { solution = sol; comb = comb } = aux (t sigma econstr) in - let (gl, _) = Term.destEvar econstr in let entry = (econstr, typ) :: ret in - entry, { solution = sol; comb = gl :: comb; shelf = [] } + entry, { solution = sol; comb = with_empty_state gl :: comb; shelf = [] } in fun t -> let entry, v = aux t in @@ -110,7 +112,7 @@ let partial_proof entry pv = CList.map (return_constr pv) (CList.map fst entry) (* First component is a reverse list of the goals which come before and second component is the list of the goals which go after (in the expected order). *) -type focus_context = Evar.t list * Evar.t list +type focus_context = goal_with_state list * goal_with_state list (** Returns a stylised view of a focus_context for use by, for @@ -120,11 +122,12 @@ type focus_context = Evar.t list * Evar.t list new nearly identical function everytime. Hence the generic name. *) (* In this version: the goals in the context, as a "zipper" (the first list is in reversed order). *) -let focus_context f = f +let focus_context (left,right) = + (List.map drop_state left, List.map drop_state right) (** This (internal) function extracts a sublist between two indices, and returns this sublist together with its context: if it returns - [(a,(b,c))] then [a] is the sublist and (rev b)@a@c is the + [(a,(b,c))] then [a] is the sublist and [(rev b) @ a @ c] is the original list. The focused list has lenght [j-i-1] and contains the goals from number [i] to number [j] (both included) the first goal of the list being numbered [1]. [focus_sublist i j l] raises @@ -149,17 +152,35 @@ let unfocus_sublist (left,right) s = proofview. It returns the focused proofview, and a context for the focus stack. *) let focus i j sp = - let (new_comb, context) = focus_sublist i j sp.comb in - ( { sp with comb = new_comb } , context ) + let (new_comb, (left, right)) = focus_sublist i j sp.comb in + ( { sp with comb = new_comb } , (left, right) ) + +let cleared_alias evd g = + let evk = drop_state g in + let state = get_state g in + Option.map (fun g -> goal_with_state g state) (Evarutil.advance evd evk) (** [undefined defs l] is the list of goals in [l] which are still - unsolved (after advancing cleared goals). *) -let undefined defs l = CList.map_filter (Evarutil.advance defs) l + unsolved (after advancing cleared goals). Note that order matters. *) +let undefined_evars defs l = + List.fold_right (fun evk l -> + match Evarutil.advance defs evk with + | Some evk -> List.add_set Evar.equal evk l + | None -> l) l [] +let goal_with_state_equal x y = Evar.equal (drop_state x) (drop_state y) +let undefined defs l = + List.fold_right (fun evk l -> + match cleared_alias defs evk with + | Some evk -> List.add_set goal_with_state_equal evk l + | None -> l) l [] (** Unfocuses a proofview with respect to a context. *) -let unfocus c sp = - { sp with comb = undefined sp.solution (unfocus_sublist c sp.comb) } +let unfocus (left, right) sp = + { sp with comb = undefined sp.solution (unfocus_sublist (left, right) sp.comb) } +let with_empty_state = Proofview_monad.with_empty_state +let drop_state = Proofview_monad.drop_state +let goal_with_state = Proofview_monad.goal_with_state (** {6 The tactic monad} *) @@ -286,7 +307,7 @@ let tclONCE = Proof.once exception MoreThanOneSuccess let _ = CErrors.register_handler begin function - | MoreThanOneSuccess -> CErrors.error "This tactic has more than one success." + | MoreThanOneSuccess -> CErrors.user_err Pp.(str "This tactic has more than one success.") | _ -> raise CErrors.Unhandled end @@ -332,7 +353,7 @@ exception NoSuchGoals of int (* This hook returns a string to be appended to the usual message. Primarily used to add a suggestion about the right bullet to use to focus the next goal, if applicable. *) -let nosuchgoals_hook:(int -> std_ppcmds) ref = ref (fun n -> mt ()) +let nosuchgoals_hook:(int -> Pp.t) ref = ref (fun n -> mt ()) let set_nosuchgoals_hook f = nosuchgoals_hook := f @@ -341,7 +362,7 @@ let set_nosuchgoals_hook f = nosuchgoals_hook := f let _ = CErrors.register_handler begin function | NoSuchGoals n -> let suffix = !nosuchgoals_hook n in - CErrors.errorlabstrm "" + CErrors.user_err (str "No such " ++ str (String.plural n "goal") ++ str "." ++ pr_non_empty_arg (fun x -> x) suffix) | _ -> raise CErrors.Unhandled @@ -402,7 +423,8 @@ let tclFOCUSID id t = try let ev = Evd.evar_key id initial.solution in try - let n = CList.index Evar.equal ev initial.comb in + let comb = CList.map drop_state initial.comb in + let n = CList.index Evar.equal ev comb in (* goal is already under focus *) let (focused,context) = focus n n initial in Pv.set focused >> @@ -411,7 +433,7 @@ let tclFOCUSID id t = return result with Not_found -> (* otherwise, save current focus and work purely on the shelve *) - Comb.set [ev] >> + Comb.set [with_empty_state ev] >> t >>= fun result -> Comb.set initial.comb >> return result @@ -421,13 +443,13 @@ let tclFOCUSID id t = exception SizeMismatch of int*int let _ = CErrors.register_handler begin function - | SizeMismatch (i,_) -> + | SizeMismatch (i,j) -> let open Pp in let errmsg = str"Incorrect number of goals" ++ spc() ++ - str"(expected "++int i++str(String.plural i " tactic") ++ str")." + str"(expected "++int i++str(String.plural i " tactic") ++ str", was given "++ int j++str")." in - CErrors.errorlabstrm "" errmsg + CErrors.user_err errmsg | _ -> raise CErrors.Unhandled end @@ -441,7 +463,7 @@ let iter_goal i = Comb.get >>= fun initial -> Proof.List.fold_left begin fun (subgoals as cur) goal -> Solution.get >>= fun step -> - match Evarutil.advance step goal with + match cleared_alias step goal with | None -> return cur | Some goal -> Comb.set [goal] >> @@ -451,6 +473,25 @@ let iter_goal i = Solution.get >>= fun evd -> Comb.set CList.(undefined evd (flatten (rev subgoals))) +(** List iter but allocates a list of results *) +let map_goal i = + let rev = List.rev in (* hem... Proof masks List... *) + let open Proof in + Comb.get >>= fun initial -> + Proof.List.fold_left begin fun (acc, subgoals as cur) goal -> + Solution.get >>= fun step -> + match cleared_alias step goal with + | None -> return cur + | Some goal -> + Comb.set [goal] >> + i goal >>= fun res -> + Proof.map (fun comb -> comb :: subgoals) Comb.get >>= fun x -> + return (res :: acc, x) + end ([],[]) initial >>= fun (results_rev, subgoals) -> + Solution.get >>= fun evd -> + Comb.set CList.(undefined evd (flatten (rev subgoals))) >> + return (rev results_rev) + (** A variant of [Monad.List.fold_left2] where the first list is the list of focused goals. The argument tactic is executed in a focus comprising only of the current goal, a goal which has been solved @@ -465,7 +506,7 @@ let fold_left2_goal i s l = in Proof.List.fold_left2 err begin fun ((r,subgoals) as cur) goal a -> Solution.get >>= fun step -> - match Evarutil.advance step goal with + match cleared_alias step goal with | None -> return cur | Some goal -> Comb.set [goal] >> @@ -509,7 +550,7 @@ let tclDISPATCHGEN0 join tacs = let open Proof in Pv.get >>= function | { comb=[goal] ; solution } -> - begin match Evarutil.advance solution goal with + begin match cleared_alias solution goal with | None -> tclUNIT (join []) | Some _ -> Proof.map (fun res -> join [res]) tac end @@ -531,8 +572,8 @@ let tclDISPATCHL tacs = tclDISPATCHGEN CList.rev tacs (** [extend_to_list startxs rx endxs l] builds a list - [startxs@[rx,...,rx]@endxs] of the same length as [l]. Raises - [SizeMismatch] if [startxs@endxs] is already longer than [l]. *) + [startxs @ [rx,...,rx] @ endxs] of the same length as [l]. Raises + [SizeMismatch] if [startxs @ endxs] is already longer than [l]. *) let extend_to_list startxs rx endxs l = (* spiwack: I use [l] essentially as a natural number *) let rec duplicate acc = function @@ -583,7 +624,15 @@ let tclINDEPENDENT tac = let tac = InfoL.tag (Info.DBranch) tac in InfoL.tag (Info.Dispatch) (iter_goal (fun _ -> tac)) - +let tclINDEPENDENTL tac = + let open Proof in + Pv.get >>= fun initial -> + match initial.comb with + | [] -> tclUNIT [] + | [_] -> tac >>= fun x -> return [x] + | _ -> + let tac = InfoL.tag (Info.DBranch) tac in + InfoL.tag (Info.Dispatch) (map_goal (fun _ -> tac)) (** {7 Goal manipulation} *) @@ -593,42 +642,70 @@ let shelve = Comb.get >>= fun initial -> Comb.set [] >> InfoL.leaf (Info.Tactic (fun () -> Pp.str"shelve")) >> - Shelf.modify (fun gls -> gls @ initial) + Shelf.modify (fun gls -> gls @ CList.map drop_state initial) let shelve_goals l = let open Proof in Comb.get >>= fun initial -> - let comb = CList.filter (fun g -> not (CList.mem g l)) initial in + let comb = CList.filter (fun g -> not (CList.mem (drop_state g) l)) initial in Comb.set comb >> InfoL.leaf (Info.Tactic (fun () -> Pp.str"shelve_goals")) >> Shelf.modify (fun gls -> gls @ l) -(** [contained_in_info e evi] checks whether the evar [e] appears in - the hypotheses, the conclusion or the body of the evar_info - [evi]. Note: since we want to use it on goals, the body is actually - supposed to be empty. *) -let contained_in_info sigma e evi = - Evar.Set.mem e (Evd.evars_of_filtered_evar_info (Evarutil.nf_evar_info sigma evi)) - (** [depends_on sigma src tgt] checks whether the goal [src] appears as an existential variable in the definition of the goal [tgt] in [sigma]. *) let depends_on sigma src tgt = let evi = Evd.find sigma tgt in - contained_in_info sigma src evi + Evar.Set.mem src (Evd.evars_of_filtered_evar_info (Evarutil.nf_evar_info sigma evi)) + +let unifiable_delayed g l = + CList.exists (fun (tgt, lazy evs) -> not (Evar.equal g tgt) && Evar.Set.mem g evs) l + +let free_evars sigma l = + let cache = Evarutil.create_undefined_evars_cache () in + let map ev = + (** Computes the set of evars appearing in the hypotheses, the conclusion or + the body of the evar_info [evi]. Note: since we want to use it on goals, + the body is actually supposed to be empty. *) + let evi = Evd.find sigma ev in + let fevs = lazy (Evarutil.filtered_undefined_evars_of_evar_info ~cache sigma evi) in + (ev, fevs) + in + List.map map l + +let free_evars_with_state sigma l = + let cache = Evarutil.create_undefined_evars_cache () in + let map ev = + (** Computes the set of evars appearing in the hypotheses, the conclusion or + the body of the evar_info [evi]. Note: since we want to use it on goals, + the body is actually supposed to be empty. *) + let ev = drop_state ev in + let evi = Evd.find sigma ev in + let fevs = lazy (Evarutil.filtered_undefined_evars_of_evar_info ~cache sigma evi) in + (ev, fevs) + in + List.map map l + (** [unifiable sigma g l] checks whether [g] appears in another subgoal of [l]. The list [l] may contain [g], but it does not affect the result. *) +let unifiable_delayed_with_state sigma g l = + let g = drop_state g in + unifiable_delayed g l + let unifiable sigma g l = - CList.exists (fun tgt -> not (Evar.equal g tgt) && depends_on sigma g tgt) l + let l = free_evars sigma l in + unifiable_delayed g l (** [partition_unifiable sigma l] partitions [l] into a pair [(u,n)] where [u] is composed of the unifiable goals, i.e. the goals on whose definition other goals of [l] depend, and [n] are the non-unifiable goals. *) let partition_unifiable sigma l = - CList.partition (fun g -> unifiable sigma g l) l + let fevs = free_evars_with_state sigma l in + CList.partition (fun g -> unifiable_delayed_with_state sigma g fevs) l (** Shelves the unifiable goals under focus, i.e. the goals which appear in other goals under focus (the unfocused goals are not @@ -639,7 +716,7 @@ let shelve_unifiable = let (u,n) = partition_unifiable initial.solution initial.comb in Comb.set n >> InfoL.leaf (Info.Tactic (fun () -> Pp.str"shelve_unifiable")) >> - Shelf.modify (fun gls -> gls @ u) + Shelf.modify (fun gls -> gls @ CList.map drop_state u) (** [guard_no_unifiable] returns the list of unifiable goals if some goals are unifiable (see {!shelve_unifiable}) in the current focus. *) @@ -650,13 +727,14 @@ let guard_no_unifiable = match u with | [] -> tclUNIT None | gls -> - let l = CList.map (fun g -> Evd.dependent_evar_ident g initial.solution) gls in + let l = CList.map (fun g -> Evd.dependent_evar_ident (drop_state g) initial.solution) gls in let l = CList.map (fun id -> Names.Name id) l in tclUNIT (Some l) (** [unshelve l p] adds all the goals in [l] at the end of the focused goals of p *) let unshelve l p = + let l = List.map with_empty_state l in (* advance the goals in case of clear *) let l = undefined p.solution l in { p with comb = p.comb@l } @@ -666,6 +744,12 @@ let mark_in_evm ~goal evd content = let info = if goal then { info with Evd.evar_source = match info.Evd.evar_source with + (* Two kinds for goal evars: + - GoalEvar (morally not dependent) + - VarInstance (morally dependent of some name). + This is a heuristic for naming these evars. *) + | loc, (Evar_kinds.QuestionMark (_,Names.Name id) | + Evar_kinds.ImplicitArg (_,(_,Some id),_)) -> loc, Evar_kinds.VarInstance id | _, (Evar_kinds.VarInstance _ | Evar_kinds.GoalEvar) as x -> x | loc,_ -> loc,Evar_kinds.GoalEvar } else info @@ -684,12 +768,13 @@ let with_shelf tac = tac >>= fun ans -> Pv.get >>= fun npv -> let { shelf = gls; solution = sigma } = npv in + (* The pending future goals are necessarily coming from V82.tactic *) + (* and thus considered as to shelve, as in Proof.run_tactic *) let gls' = Evd.future_goals sigma in - 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 + let fgoals = Evd.save_future_goals solution in + let sigma = Evd.restore_future_goals sigma fgoals in (* Ensure we mark and return only unsolved goals *) - let gls' = undefined sigma (CList.rev_append gls' gls) in + let gls' = undefined_evars 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) @@ -771,7 +856,7 @@ let give_up = Comb.set [] >> mark_as_unsafe >> InfoL.leaf (Info.Tactic (fun () -> Pp.str"give_up")) >> - Giveup.put initial + Giveup.put (CList.map drop_state initial) @@ -812,8 +897,8 @@ module Progress = struct (** Equality function on goals *) let goal_equal evars1 gl1 evars2 gl2 = - let evi1 = Evd.find evars1 gl1 in - let evi2 = Evd.find evars2 gl2 in + let evi1 = Evd.find evars1 (drop_state gl1) in + let evi2 = Evd.find evars2 (drop_state gl2) in eq_evar_info evars1 evars2 evi1 evi2 end @@ -828,22 +913,20 @@ let tclPROGRESS t = let quick_test = initial.solution == final.solution && initial.comb == final.comb in - let exhaustive_test = + let test = + quick_test || Util.List.for_all2eq begin fun i f -> Progress.goal_equal initial.solution i final.solution f end initial.comb final.comb in - let test = - quick_test || exhaustive_test - in if not test then tclUNIT res else - tclZERO (CErrors.UserError ("Proofview.tclPROGRESS" , Pp.str"Failed to progress.")) + tclZERO (CErrors.UserError (Some "Proofview.tclPROGRESS" , Pp.str"Failed to progress.")) exception Timeout let _ = CErrors.register_handler begin function - | Timeout -> CErrors.errorlabstrm "Proofview.tclTIMEOUT" (Pp.str"Tactic timeout!") + | Timeout -> CErrors.user_err ~hdr:"Proofview.tclTIMEOUT" (Pp.str"Tactic timeout!") | _ -> Pervasives.raise CErrors.Unhandled end @@ -929,6 +1012,15 @@ module Unsafe = struct let tclSETGOALS = Comb.set + let tclGETSHELF = Shelf.get + + let tclSETSHELF = Shelf.set + + let tclPUTSHELF to_shelve = + tclBIND tclGETSHELF (fun shelf -> tclSETSHELF (to_shelve@shelf)) + + let tclPUTGIVENUP = Giveup.put + let tclEVARSADVANCE evd = Pv.modify (fun ps -> { ps with solution = evd; comb = undefined evd ps.comb }) @@ -978,64 +1070,68 @@ let catchable_exception = function module Goal = struct - type ('a, 'r) t = { + type t = { env : Environ.env; sigma : Evd.evar_map; - concl : Term.constr ; + concl : EConstr.constr ; + state : StateStore.t; self : Evar.t ; (* for compatibility with old-style definitions *) } - type ('a, 'b) enter = - { enter : 'r. ('a, 'r) t -> 'b } - - let assume (gl : ('a, 'r) t) = (gl :> ([ `NF ], 'r) t) + let assume (gl : t) = (gl : t) - let env { env=env } = env - let sigma { sigma=sigma } = Sigma.Unsafe.of_evar_map sigma - let hyps { env=env } = Environ.named_context env - let concl { concl=concl } = concl - let extra { sigma=sigma; self=self } = goal_extra sigma self + let print { sigma; self } = { Evd.it = self; sigma } - let raw_concl { concl=concl } = concl + let state { state=state } = state + let env {env} = env + let sigma {sigma} = sigma + let hyps {env} = EConstr.named_context env + let concl {concl} = concl + let extra {sigma; self} = goal_extra sigma self - let gmake_with info env sigma goal = + let gmake_with info env sigma goal state = { env = Environ.reset_with_named_context (Evd.evar_filtered_hyps info) env ; sigma = sigma ; - concl = Evd.evar_concl info ; + concl = EConstr.of_constr (Evd.evar_concl info); + state = state ; self = goal } let nf_gmake env sigma goal = + let state = get_state goal in + let goal = drop_state goal in let info = Evarutil.nf_evar_info sigma (Evd.find sigma goal) in let sigma = Evd.add sigma goal info in - gmake_with info env sigma goal , sigma + gmake_with info env sigma goal state , sigma let nf_enter f = InfoL.tag (Info.Dispatch) begin iter_goal begin fun goal -> - Env.get >>= fun env -> + tclENV >>= fun env -> tclEVARMAP >>= fun sigma -> try let (gl, sigma) = nf_gmake env sigma goal in - tclTHEN (Unsafe.tclEVARS sigma) (InfoL.tag (Info.DBranch) (f.enter gl)) + tclTHEN (Unsafe.tclEVARS sigma) (InfoL.tag (Info.DBranch) (f gl)) with e when catchable_exception e -> let (e, info) = CErrors.push e in tclZERO ~info e end end - let normalize { self } = + let normalize { self; state } = Env.get >>= fun env -> tclEVARMAP >>= fun sigma -> - let (gl,sigma) = nf_gmake env sigma self in + let (gl,sigma) = nf_gmake env sigma (goal_with_state self state) in tclTHEN (Unsafe.tclEVARS sigma) (tclUNIT gl) let gmake env sigma goal = + let state = get_state goal in + let goal = drop_state goal in let info = Evd.find sigma goal in - gmake_with info env sigma goal + gmake_with info env sigma goal state let enter f = - let f gl = InfoL.tag (Info.DBranch) (f.enter gl) in + let f gl = InfoL.tag (Info.DBranch) (f gl) in InfoL.tag (Info.Dispatch) begin iter_goal begin fun goal -> Env.get >>= fun env -> @@ -1047,66 +1143,25 @@ module Goal = struct end end - exception NotExactlyOneSubgoal - let _ = CErrors.register_handler begin function - | NotExactlyOneSubgoal -> - CErrors.errorlabstrm "" (Pp.str"Not exactly one subgoal.") - | _ -> raise CErrors.Unhandled - end - - let enter_one f = + let enter_one ?(__LOC__=__LOC__) f = let open Proof in Comb.get >>= function | [goal] -> begin Env.get >>= fun env -> tclEVARMAP >>= fun sigma -> - try f.enter (gmake env sigma goal) + try f (gmake env sigma goal) with e when catchable_exception e -> let (e, info) = CErrors.push e in tclZERO ~info e end - | _ -> tclZERO NotExactlyOneSubgoal - - type ('a, 'b) s_enter = - { s_enter : 'r. ('a, 'r) t -> ('b, 'r) Sigma.sigma } - - let s_enter f = - InfoL.tag (Info.Dispatch) begin - iter_goal begin fun goal -> - Env.get >>= fun env -> - tclEVARMAP >>= fun sigma -> - try - let gl = gmake env sigma goal in - let Sigma (tac, sigma, _) = f.s_enter gl in - let sigma = Sigma.to_evar_map sigma in - tclTHEN (Unsafe.tclEVARS sigma) (InfoL.tag (Info.DBranch) tac) - with e when catchable_exception e -> - let (e, info) = CErrors.push e in - tclZERO ~info e - end - end - - let nf_s_enter f = - InfoL.tag (Info.Dispatch) begin - iter_goal begin fun goal -> - Env.get >>= fun env -> - tclEVARMAP >>= fun sigma -> - try - let (gl, sigma) = nf_gmake env sigma goal in - let Sigma (tac, sigma, _) = f.s_enter gl in - let sigma = Sigma.to_evar_map sigma in - tclTHEN (Unsafe.tclEVARS sigma) (InfoL.tag (Info.DBranch) tac) - with e when catchable_exception e -> - let (e, info) = CErrors.push e in - tclZERO ~info e - end - end + | _ -> + CErrors.anomaly Pp.(str __LOC__ ++ str " enter_one") let goals = Pv.get >>= fun step -> let sigma = step.solution in let map goal = - match Evarutil.advance sigma goal with + match cleared_alias sigma goal with | None -> None (** ppedrot: Is this check really necessary? *) | Some goal -> let gl = @@ -1125,8 +1180,6 @@ module Goal = struct (* compatibility *) let goal { self=self } = self - let lift (gl : ('a, 'r) t) _ = (gl :> ('a, 's) t) - end @@ -1161,25 +1214,29 @@ let tclCHECKINTERRUPT = module V82 = struct type tac = Evar.t Evd.sigma -> Evar.t list Evd.sigma - let tactic tac = + let tactic ?(nf_evars=true) tac = (* spiwack: we ignore the dependencies between goals here, expectingly preserving the semantics of <= 8.2 tactics *) (* spiwack: convenience notations, waiting for ocaml 3.12 *) let open Proof in Pv.get >>= fun ps -> try - let tac gl evd = + let tac g_w_s evd = + let g, w = drop_state g_w_s, get_state g_w_s in let glsigma = - tac { Evd.it = gl ; sigma = evd; } in + tac { Evd.it = g ; sigma = evd; } in let sigma = glsigma.Evd.sigma in - let g = glsigma.Evd.it in + let g = CList.map (fun g -> goal_with_state g w) glsigma.Evd.it in ( g, sigma ) in (* Old style tactics expect the goals normalized with respect to evars. *) - let (initgoals,initevd) = - Evd.Monad.List.map (fun g s -> goal_nf_evar s g) ps.comb ps.solution + let (initgoals_w_state, initevd) = + Evd.Monad.List.map (fun g_w_s s -> + let g, w = drop_state g_w_s, get_state g_w_s in + let g, s = if nf_evars then goal_nf_evar s g else g, s in + goal_with_state g w, s) ps.comb ps.solution in - let (goalss,evd) = Evd.Monad.List.map tac initgoals initevd in + let (goalss,evd) = Evd.Monad.List.map tac initgoals_w_state initevd in let sgs = CList.flatten goalss in let sgs = undefined evd sgs in InfoL.leaf (Info.Tactic (fun () -> Pp.str"")) >> @@ -1194,8 +1251,9 @@ module V82 = struct let nf_evar_goals = Pv.modify begin fun ps -> let map g s = goal_nf_evar s g in - let (goals,evd) = Evd.Monad.List.map map ps.comb ps.solution in - { ps with solution = evd; comb = goals; } + let comb = CList.map drop_state ps.comb in + let (_goals,evd) = Evd.Monad.List.map map comb ps.solution in + { ps with solution = evd; } end let has_unresolved_evar pv = @@ -1205,30 +1263,30 @@ module V82 = struct let grab pv = let undef = Evd.undefined_map pv.solution in let goals = CList.rev_map fst (Evar.Map.bindings undef) in - { pv with comb = goals } + { pv with comb = List.map with_empty_state goals } (* Returns the open goals of the proofview together with the evar_map to interpret them. *) let goals { comb = comb ; solution = solution; } = - { Evd.it = comb ; sigma = solution } + { Evd.it = List.map drop_state comb ; sigma = solution } let top_goals initial { solution=solution; } = - let goals = CList.map (fun (t,_) -> fst (Term.destEvar t)) initial in + let goals = CList.map (fun (t,_) -> fst (Constr.destEvar (EConstr.Unsafe.to_constr t))) initial in { Evd.it = goals ; sigma=solution; } let top_evars initial = let evars_of_initial (c,_) = - Evar.Set.elements (Evd.evars_of_term c) + Evar.Set.elements (Evd.evars_of_term (EConstr.Unsafe.to_constr c)) in CList.flatten (CList.map evars_of_initial initial) let of_tactic t gls = try - let init = { shelf = []; solution = gls.Evd.sigma ; comb = [gls.Evd.it] } in + let init = { shelf = []; solution = gls.Evd.sigma ; comb = [with_empty_state gls.Evd.it] } in let (_,final,_,_) = apply (goal_env gls.Evd.sigma gls.Evd.it) t init in - { Evd.sigma = final.solution ; it = final.comb } + { Evd.sigma = final.solution ; it = CList.map drop_state final.comb } with Logic_monad.TacticFailure e as src -> let (_, info) = CErrors.push src in iraise (e, info) @@ -1250,8 +1308,4 @@ module Notations = struct let (>>=) = tclBIND let (<*>) = tclTHEN let (<+>) t1 t2 = tclOR t1 (fun _ -> t2) - type ('a, 'b) enter = ('a, 'b) Goal.enter = - { enter : 'r. ('a, 'r) Goal.t -> 'b } - type ('a, 'b) s_enter = ('a, 'b) Goal.s_enter = - { s_enter : 'r. ('a, 'r) Goal.t -> ('b, 'r) Sigma.sigma } end -- cgit v1.2.3