aboutsummaryrefslogtreecommitdiffhomepage
path: root/proofs
diff options
context:
space:
mode:
authorGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2016-03-20 19:38:36 +0100
committerGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2016-03-20 19:48:38 +0100
commitea4e09c26747fa9c49882580a72139fe748a0d64 (patch)
tree40364a6bb2100e102bc16e465b6d6289b1340314 /proofs
parent93a77f3cb8ee36072f93b4c0ace6f0f9c19f51a3 (diff)
Moving Proofview to pretyping/.
Diffstat (limited to 'proofs')
-rw-r--r--proofs/proofs.mllib1
-rw-r--r--proofs/proofview.ml1204
-rw-r--r--proofs/proofview.mli586
3 files changed, 0 insertions, 1791 deletions
diff --git a/proofs/proofs.mllib b/proofs/proofs.mllib
index 236d47932..9130a186b 100644
--- a/proofs/proofs.mllib
+++ b/proofs/proofs.mllib
@@ -4,7 +4,6 @@ Evar_refiner
Proof_using
Proof_errors
Logic
-Proofview
Refine
Proof
Proof_global
diff --git a/proofs/proofview.ml b/proofs/proofview.ml
deleted file mode 100644
index 20be02e76..000000000
--- a/proofs/proofview.ml
+++ /dev/null
@@ -1,1204 +0,0 @@
-(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
-(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
-(************************************************************************)
-
-
-(** This files defines the basic mechanism of proofs: the [proofview]
- type is the state which tactics manipulate (a global state for
- existential variables, together with the list of goals), and the type
- ['a tactic] is the (abstract) type of tactics modifying the proof
- state and returning a value of type ['a]. *)
-
-open Pp
-open Util
-open Proofview_monad
-open Sigma.Notations
-open Context.Named.Declaration
-
-(** Main state of tactics *)
-type proofview = Proofview_monad.proofview
-
-type entry = (Term.constr * Term.types) list
-
-(** Returns a stylised view of a proofview for use by, for instance,
- ide-s. *)
-(* spiwack: the type of [proofview] will change as we push more
- refined functions to ide-s. This would be better than spawning a
- new nearly identical function everytime. Hence the generic name. *)
-(* In this version: returns the list of focused goals together with
- the [evar_map] context. *)
-let proofview p =
- p.comb , p.solution
-
-let compact el ({ solution } as pv) =
- let nf = Evarutil.nf_evar solution in
- let size = Evd.fold (fun _ _ i -> 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
- 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
- msg_info (Pp.str (Printf.sprintf "Evars: %d -> %d\n" size new_size));
- new_el, { pv with solution = new_solution; }
-
-
-(** {6 Starting and querying a proof view} *)
-
-type telescope =
- | TNil of Evd.evar_map
- | TCons of Environ.env * Evd.evar_map * Term.types * (Evd.evar_map -> Term.constr -> telescope)
-
-let dependent_init =
- (* Goals are created with a store which marks them as unresolvable
- for type classes. *)
- let store = Typeclasses.set_resolvable Evd.Store.empty false in
- (* Goals don't have a source location. *)
- let src = (Loc.ghost,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 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 = [] }
- in
- fun t ->
- let entry, v = aux t in
- (* The created goal are not to be shelved. *)
- let solution = Evd.reset_future_goals v.solution in
- entry, { v with solution }
-
-let init =
- let rec aux sigma = function
- | [] -> TNil sigma
- | (env,g)::l -> TCons (env,sigma,g,(fun sigma _ -> aux sigma l))
- in
- fun sigma l -> dependent_init (aux sigma l)
-
-let initial_goals initial = initial
-
-let finished = function
- | {comb = []} -> true
- | _ -> false
-
-let return { solution=defs } = defs
-
-let return_constr { solution = defs } c = Evarutil.nf_evar defs c
-
-let partial_proof entry pv = CList.map (return_constr pv) (CList.map fst entry)
-
-
-(** {6 Focusing commands} *)
-
-(** A [focus_context] represents the part of the proof view which has
- been removed by a focusing action, it can be used to unfocus later
- on. *)
-(* 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
-
-
-(** Returns a stylised view of a focus_context for use by, for
- instance, ide-s. *)
-(* spiwack: the type of [focus_context] will change as we push more
- refined functions to ide-s. This would be better than spawning a
- 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
-
-(** 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
- 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
- [IndexOutOfRange] if [i > length l], or [j > length l] or [j <
- i]. *)
-let focus_sublist i j l =
- let (left,sub_right) = CList.goto (i-1) l in
- let (sub, right) =
- try CList.chop (j-i+1) sub_right
- with Failure _ -> raise CList.IndexOutOfRange
- in
- (sub, (left,right))
-
-(** Inverse operation to the previous one. *)
-let unfocus_sublist (left,right) s =
- CList.rev_append left (s@right)
-
-
-(** [focus i j] focuses a proofview on the goals from index [i] to
- index [j] (inclusive, goals are indexed from [1]). I.e. goals
- number [i] to [j] become the only focused goals of the returned
- 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 )
-
-
-(** [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)
- solved. *)
-(* spiwack: [advance] is probably performance critical, and the good
- behaviour of its definition may depend sensitively to the actual
- definition of [Evd.find]. Currently, [Evd.find] starts looking for
- a value in the heap of undefined variable, which is small. Hence in
- the most common case, where [advance] is applied to an unsolved
- goal ([advance] is used to figure if a side effect has modified the
- goal) it terminates quickly. *)
-let rec advance sigma g =
- let open Evd in
- let evi = Evd.find sigma g in
- match evi.evar_body with
- | Evar_empty -> Some g
- | Evar_defined v ->
- if Option.default false (Store.get evi.evar_extra Evarutil.cleared) then
- let (e,_) = Term.destEvar v in
- advance sigma e
- else
- None
-
-(** [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 (advance defs) l
-
-(** Unfocuses a proofview with respect to a context. *)
-let unfocus c sp =
- { sp with comb = undefined sp.solution (unfocus_sublist c sp.comb) }
-
-
-(** {6 The tactic monad} *)
-
-(** - Tactics are objects which apply a transformation to all the
- subgoals of the current view at the same time. By opposition to
- the old vision of applying it to a single goal. It allows tactics
- such as [shelve_unifiable], tactics to reorder the focused goals,
- or global automation tactic for dependent subgoals (instantiating
- an evar has influences on the other goals of the proof in
- progress, not being able to take that into account causes the
- current eauto tactic to fail on some instances where it could
- succeed). Another benefit is that it is possible to write tactics
- that can be executed even if there are no focused goals.
- - Tactics form a monad ['a tactic], in a sense a tactic can be
- seen as a function (without argument) which returns a value of
- type 'a and modifies the environment (in our case: the view).
- Tactics of course have arguments, but these are given at the
- meta-level as OCaml functions. Most tactics in the sense we are
- used to return [()], that is no really interesting values. But
- some might pass information around. The tactics seen in Coq's
- Ltac are (for now at least) only [unit tactic], the return values
- are kept for the OCaml toolkit. The operation or the monad are
- [Proofview.tclUNIT] (which is the "return" of the tactic monad)
- [Proofview.tclBIND] (which is the "bind") and [Proofview.tclTHEN]
- (which is a specialized bind on unit-returning tactics).
- - Tactics have support for full-backtracking. Tactics can be seen
- having multiple success: if after returning the first success a
- failure is encountered, the tactic can backtrack and use a second
- success if available. The state is backtracked to its previous
- value, except the non-logical state defined in the {!NonLogical}
- module below.
-*)
-(* spiwack: as far as I'm aware this doesn't really relate to
- F. Kirchner and C. Muñoz. *)
-
-module Proof = Logical
-
-(** type of tactics:
-
- tactics can
- - access the environment,
- - report unsafe status, shelved goals and given up goals
- - access and change the current [proofview]
- - backtrack on previous changes of the proofview *)
-type +'a tactic = 'a Proof.t
-
-(** Applies a tactic to the current proofview. *)
-let apply env t sp =
- let open Logic_monad in
- let ans = Proof.repr (Proof.run t false (sp,env)) in
- let ans = Logic_monad.NonLogical.run ans in
- match ans with
- | Nil (e, info) -> iraise (TacticFailure e, info)
- | Cons ((r, (state, _), status, info), _) ->
- let (status, gaveup) = status in
- let status = (status, state.shelf, gaveup) in
- let state = { state with shelf = [] } in
- r, state, status, Trace.to_tree info
-
-
-
-(** {7 Monadic primitives} *)
-
-(** Unit of the tactic monad. *)
-let tclUNIT = Proof.return
-
-(** Bind operation of the tactic monad. *)
-let tclBIND = Proof.(>>=)
-
-(** Interpretes the ";" (semicolon) of Ltac. As a monadic operation,
- it's a specialized "bind". *)
-let tclTHEN = Proof.(>>)
-
-(** [tclIGNORE t] has the same operational content as [t], but drops
- the returned value. *)
-let tclIGNORE = Proof.ignore
-
-module Monad = Proof
-
-
-
-(** {7 Failure and backtracking} *)
-
-
-(** [tclZERO e] fails with exception [e]. It has no success. *)
-let tclZERO ?info e =
- let info = match info with
- | None -> Exninfo.null
- | Some info -> info
- in
- Proof.zero (e, info)
-
-(** [tclOR t1 t2] behaves like [t1] as long as [t1] succeeds. Whenever
- the successes of [t1] have been depleted and it failed with [e],
- then it behaves as [t2 e]. In other words, [tclOR] inserts a
- backtracking point. *)
-let tclOR = Proof.plus
-
-(** [tclORELSE t1 t2] is equal to [t1] if [t1] has at least one
- success or [t2 e] if [t1] fails with [e]. It is analogous to
- [try/with] handler of exception in that it is not a backtracking
- point. *)
-let tclORELSE t1 t2 =
- let open Logic_monad in
- let open Proof in
- split t1 >>= function
- | Nil e -> t2 e
- | Cons (a,t1') -> plus (return a) t1'
-
-(** [tclIFCATCH a s f] is a generalisation of {!tclORELSE}: if [a]
- succeeds at least once then it behaves as [tclBIND a s] otherwise,
- if [a] fails with [e], then it behaves as [f e]. *)
-let tclIFCATCH a s f =
- let open Logic_monad in
- let open Proof in
- split a >>= function
- | Nil e -> f e
- | Cons (x,a') -> plus (s x) (fun e -> (a' e) >>= fun x' -> (s x'))
-
-(** [tclONCE t] behave like [t] except it has at most one success:
- [tclONCE t] stops after the first success of [t]. If [t] fails
- with [e], [tclONCE t] also fails with [e]. *)
-let tclONCE = Proof.once
-
-exception MoreThanOneSuccess
-let _ = Errors.register_handler begin function
- | MoreThanOneSuccess -> Errors.error "This tactic has more than one success."
- | _ -> raise Errors.Unhandled
-end
-
-(** [tclEXACTLY_ONCE e t] succeeds as [t] if [t] has exactly one
- success. Otherwise it fails. The tactic [t] is run until its first
- success, then a failure with exception [e] is simulated. It [t]
- yields another success, then [tclEXACTLY_ONCE e t] fails with
- [MoreThanOneSuccess] (it is a user error). Otherwise,
- [tclEXACTLY_ONCE e t] succeeds with the first success of
- [t]. Notice that the choice of [e] is relevant, as the presence of
- further successes may depend on [e] (see {!tclOR}). *)
-let tclEXACTLY_ONCE e t =
- let open Logic_monad in
- let open Proof in
- split t >>= function
- | Nil (e, info) -> tclZERO ~info e
- | Cons (x,k) ->
- Proof.split (k (e, Exninfo.null)) >>= function
- | Nil _ -> tclUNIT x
- | _ -> tclZERO MoreThanOneSuccess
-
-
-(** [tclCASE t] wraps the {!Proofview_monad.Logical.split} primitive. *)
-type 'a case =
-| Fail of iexn
-| Next of 'a * (iexn -> 'a tactic)
-let tclCASE t =
- let open Logic_monad in
- let map = function
- | Nil e -> Fail e
- | Cons (x, t) -> Next (x, t)
- in
- Proof.map map (Proof.split t)
-
-let tclBREAK = Proof.break
-
-
-
-(** {7 Focusing tactics} *)
-
-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 set_nosuchgoals_hook f = nosuchgoals_hook := f
-
-
-
-(* This uses the hook above *)
-let _ = Errors.register_handler begin function
- | NoSuchGoals n ->
- let suffix = !nosuchgoals_hook n in
- Errors.errorlabstrm ""
- (str "No such " ++ str (String.plural n "goal") ++ str "." ++ suffix)
- | _ -> raise Errors.Unhandled
-end
-
-(** [tclFOCUS_gen nosuchgoal i j t] applies [t] in a context where
- only the goals numbered [i] to [j] are focused (the rest of the goals
- is restored at the end of the tactic). If the range [i]-[j] is not
- valid, then it [tclFOCUS_gen nosuchgoal i j t] is [nosuchgoal]. *)
-let tclFOCUS_gen nosuchgoal i j t =
- let open Proof in
- Pv.get >>= fun initial ->
- try
- let (focused,context) = focus i j initial in
- Pv.set focused >>
- t >>= fun result ->
- Pv.modify (fun next -> unfocus context next) >>
- return result
- with CList.IndexOutOfRange -> nosuchgoal
-
-let tclFOCUS i j t = tclFOCUS_gen (tclZERO (NoSuchGoals (j+1-i))) i j t
-let tclTRYFOCUS i j t = tclFOCUS_gen (tclUNIT ()) i j t
-
-(** Like {!tclFOCUS} but selects a single goal by name. *)
-let tclFOCUSID id t =
- let open Proof in
- Pv.get >>= fun initial ->
- try
- let ev = Evd.evar_key id initial.solution in
- try
- let n = CList.index Evar.equal ev initial.comb in
- (* goal is already under focus *)
- let (focused,context) = focus n n initial in
- Pv.set focused >>
- t >>= fun result ->
- Pv.modify (fun next -> unfocus context next) >>
- return result
- with Not_found ->
- (* otherwise, save current focus and work purely on the shelve *)
- Comb.set [ev] >>
- t >>= fun result ->
- Comb.set initial.comb >>
- return result
- with Not_found -> tclZERO (NoSuchGoals 1)
-
-(** {7 Dispatching on goals} *)
-
-exception SizeMismatch of int*int
-let _ = Errors.register_handler begin function
- | SizeMismatch (i,_) ->
- let open Pp in
- let errmsg =
- str"Incorrect number of goals" ++ spc() ++
- str"(expected "++int i++str(String.plural i " tactic") ++ str")."
- in
- Errors.errorlabstrm "" errmsg
- | _ -> raise Errors.Unhandled
-end
-
-(** A variant of [Monad.List.iter] where we iter over the focused list
- of goals. The argument tactic is executed in a focus comprising
- only of the current goal, a goal which has been solved by side
- effect is skipped. The generated subgoals are concatenated in
- order. *)
-let iter_goal i =
- let open Proof in
- Comb.get >>= fun initial ->
- Proof.List.fold_left begin fun (subgoals as cur) goal ->
- Solution.get >>= fun step ->
- match advance step goal with
- | None -> return cur
- | Some goal ->
- Comb.set [goal] >>
- i goal >>
- Proof.map (fun comb -> comb :: subgoals) Comb.get
- end [] initial >>= fun subgoals ->
- Solution.get >>= fun evd ->
- Comb.set CList.(undefined evd (flatten (rev subgoals)))
-
-(** 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
- by side effect is skipped. The generated subgoals are concatenated
- in order. *)
-let fold_left2_goal i s l =
- let open Proof in
- Pv.get >>= fun initial ->
- let err =
- return () >>= fun () -> (* Delay the computation of list lengths. *)
- tclZERO (SizeMismatch (CList.length initial.comb,CList.length l))
- in
- Proof.List.fold_left2 err begin fun ((r,subgoals) as cur) goal a ->
- Solution.get >>= fun step ->
- match advance step goal with
- | None -> return cur
- | Some goal ->
- Comb.set [goal] >>
- i goal a r >>= fun r ->
- Proof.map (fun comb -> (r, comb :: subgoals)) Comb.get
- end (s,[]) initial.comb l >>= fun (r,subgoals) ->
- Solution.get >>= fun evd ->
- Comb.set CList.(undefined evd (flatten (rev subgoals))) >>
- return r
-
-(** Dispatch tacticals are used to apply a different tactic to each
- goal under focus. They come in two flavours: [tclDISPATCH] takes a
- list of [unit tactic]-s and build a [unit tactic]. [tclDISPATCHL]
- takes a list of ['a tactic] and returns an ['a list tactic].
-
- They both work by applying each of the tactic in a focus
- restricted to the corresponding goal (starting with the first
- goal). In the case of [tclDISPATCHL], the tactic returns a list of
- the same size as the argument list (of tactics), each element
- being the result of the tactic executed in the corresponding goal.
-
- When the length of the tactic list is not the number of goal,
- raises [SizeMismatch (g,t)] where [g] is the number of available
- goals, and [t] the number of tactics passed.
-
- [tclDISPATCHGEN join tacs] generalises both functions as the
- successive results of [tacs] are stored in reverse order in a
- list, and [join] is used to convert the result into the expected
- form. *)
-let tclDISPATCHGEN0 join tacs =
- match tacs with
- | [] ->
- begin
- let open Proof in
- Comb.get >>= function
- | [] -> tclUNIT (join [])
- | comb -> tclZERO (SizeMismatch (CList.length comb,0))
- end
- | [tac] ->
- begin
- let open Proof in
- Pv.get >>= function
- | { comb=[goal] ; solution } ->
- begin match advance solution goal with
- | None -> tclUNIT (join [])
- | Some _ -> Proof.map (fun res -> join [res]) tac
- end
- | {comb} -> tclZERO (SizeMismatch(CList.length comb,1))
- end
- | _ ->
- let iter _ t cur = Proof.map (fun y -> y :: cur) t in
- let ans = fold_left2_goal iter [] tacs in
- Proof.map join ans
-
-let tclDISPATCHGEN join tacs =
- let branch t = InfoL.tag (Info.DBranch) t in
- let tacs = CList.map branch tacs in
- InfoL.tag (Info.Dispatch) (tclDISPATCHGEN0 join tacs)
-
-let tclDISPATCH tacs = tclDISPATCHGEN Pervasives.ignore tacs
-
-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]. *)
-let extend_to_list startxs rx endxs l =
- (* spiwack: I use [l] essentially as a natural number *)
- let rec duplicate acc = function
- | [] -> acc
- | _::rest -> duplicate (rx::acc) rest
- in
- let rec tail to_match rest =
- match rest, to_match with
- | [] , _::_ -> raise (SizeMismatch(0,0)) (* placeholder *)
- | _::rest , _::to_match -> tail to_match rest
- | _ , [] -> duplicate endxs rest
- in
- let rec copy pref rest =
- match rest,pref with
- | [] , _::_ -> raise (SizeMismatch(0,0)) (* placeholder *)
- | _::rest, a::pref -> a::(copy pref rest)
- | _ , [] -> tail endxs rest
- in
- copy startxs l
-
-(** [tclEXTEND b r e] is a variant of {!tclDISPATCH}, where the [r]
- tactic is "repeated" enough time such that every goal has a tactic
- assigned to it ([b] is the list of tactics applied to the first
- goals, [e] to the last goals, and [r] is applied to every goal in
- between). *)
-let tclEXTEND tacs1 rtac tacs2 =
- let open Proof in
- Comb.get >>= fun comb ->
- try
- let tacs = extend_to_list tacs1 rtac tacs2 comb in
- tclDISPATCH tacs
- with SizeMismatch _ ->
- tclZERO (SizeMismatch(
- CList.length comb,
- (CList.length tacs1)+(CList.length tacs2)))
-(* spiwack: failure occurs only when the number of goals is too
- small. Hence we can assume that [rtac] is replicated 0 times for
- any error message. *)
-
-(** [tclEXTEND [] tac []]. *)
-let tclINDEPENDENT tac =
- let open Proof in
- Pv.get >>= fun initial ->
- match initial.comb with
- | [] -> tclUNIT ()
- | [_] -> tac
- | _ ->
- let tac = InfoL.tag (Info.DBranch) tac in
- InfoL.tag (Info.Dispatch) (iter_goal (fun _ -> tac))
-
-
-
-(** {7 Goal manipulation} *)
-
-(** Shelves all the goals under focus. *)
-let shelve =
- let open Proof in
- Comb.get >>= fun initial ->
- Comb.set [] >>
- InfoL.leaf (Info.Tactic (fun () -> Pp.str"shelve")) >>
- Shelf.modify (fun gls -> gls @ initial)
-
-
-(** [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
-
-(** [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 sigma g l =
- CList.exists (fun tgt -> not (Evar.equal g tgt) && depends_on sigma g tgt) 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
-
-(** Shelves the unifiable goals under focus, i.e. the goals which
- appear in other goals under focus (the unfocused goals are not
- considered). *)
-let shelve_unifiable =
- let open Proof in
- Pv.get >>= fun initial ->
- 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)
-
-(** [guard_no_unifiable] returns the list of unifiable goals if some
- goals are unifiable (see {!shelve_unifiable}) in the current focus. *)
-let guard_no_unifiable =
- let open Proof in
- Pv.get >>= fun initial ->
- let (u,n) = partition_unifiable initial.solution initial.comb in
- 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 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 =
- (* advance the goals in case of clear *)
- let l = undefined p.solution l in
- { p with comb = p.comb@l }
-
-let with_shelf tac =
- let open Proof in
- Pv.get >>= fun pv ->
- let { shelf; solution } = pv in
- Pv.set { pv with shelf = []; solution = Evd.reset_future_goals solution } >>
- tac >>= fun ans ->
- Pv.get >>= fun npv ->
- let { shelf = gls; solution = sigma } = npv in
- 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
- Pv.set { npv with shelf; solution = sigma } >>
- tclUNIT (CList.rev_append gls' gls, ans)
-
-(** [goodmod p m] computes the representative of [p] modulo [m] in the
- interval [[0,m-1]].*)
-let goodmod p m =
- let p' = p mod m in
- (* if [n] is negative [n mod l] is negative of absolute value less
- than [l], so [(n mod l)+l] is the representative of [n] in the
- interval [[0,l-1]].*)
- if p' < 0 then p'+m else p'
-
-let cycle n =
- let open Proof in
- InfoL.leaf (Info.Tactic (fun () -> Pp.(str"cycle "++int n))) >>
- Comb.modify begin fun initial ->
- let l = CList.length initial in
- let n' = goodmod n l in
- let (front,rear) = CList.chop n' initial in
- rear@front
- end
-
-let swap i j =
- let open Proof in
- InfoL.leaf (Info.Tactic (fun () -> Pp.(hov 2 (str"swap"++spc()++int i++spc()++int j)))) >>
- Comb.modify begin fun initial ->
- let l = CList.length initial in
- let i = if i>0 then i-1 else i and j = if j>0 then j-1 else j in
- let i = goodmod i l and j = goodmod j l in
- CList.map_i begin fun k x ->
- match k with
- | k when Int.equal k i -> CList.nth initial j
- | k when Int.equal k j -> CList.nth initial i
- | _ -> x
- end 0 initial
- end
-
-let revgoals =
- let open Proof in
- InfoL.leaf (Info.Tactic (fun () -> Pp.str"revgoals")) >>
- Comb.modify CList.rev
-
-let numgoals =
- let open Proof in
- Comb.get >>= fun comb ->
- return (CList.length comb)
-
-
-
-(** {7 Access primitives} *)
-
-let tclEVARMAP = Solution.get
-
-let tclENV = Env.get
-
-
-
-(** {7 Put-like primitives} *)
-
-
-let emit_side_effects eff x =
- { x with solution = Evd.emit_side_effects eff x.solution }
-
-let tclEFFECTS eff =
- let open Proof in
- return () >>= fun () -> (* The Global.env should be taken at exec time *)
- Env.set (Global.env ()) >>
- Pv.modify (fun initial -> emit_side_effects eff initial)
-
-let mark_as_unsafe = Status.put false
-
-(** Gives up on the goal under focus. Reports an unsafe status. Proofs
- with given up goals cannot be closed. *)
-let give_up =
- let open Proof in
- Comb.get >>= fun initial ->
- Comb.set [] >>
- mark_as_unsafe >>
- InfoL.leaf (Info.Tactic (fun () -> Pp.str"give_up")) >>
- Giveup.put initial
-
-
-
-(** {7 Control primitives} *)
-
-
-module Progress = struct
-
- let eq_constr = Evarutil.eq_constr_univs_test
-
- (** equality function on hypothesis contexts *)
- let eq_named_context_val sigma1 sigma2 ctx1 ctx2 =
- let open Environ in
- let c1 = named_context_of_val ctx1 and c2 = named_context_of_val ctx2 in
- let eq_named_declaration d1 d2 =
- match d1, d2 with
- | LocalAssum (i1,t1), LocalAssum (i2,t2) ->
- Names.Id.equal i1 i2 && eq_constr sigma1 sigma2 t1 t2
- | LocalDef (i1,c1,t1), LocalDef (i2,c2,t2) ->
- Names.Id.equal i1 i2 && eq_constr sigma1 sigma2 c1 c2
- && eq_constr sigma1 sigma2 t1 t2
- | _ ->
- false
- in List.equal eq_named_declaration c1 c2
-
- let eq_evar_body sigma1 sigma2 b1 b2 =
- let open Evd in
- match b1, b2 with
- | Evar_empty, Evar_empty -> true
- | Evar_defined t1, Evar_defined t2 -> eq_constr sigma1 sigma2 t1 t2
- | _ -> false
-
- let eq_evar_info sigma1 sigma2 ei1 ei2 =
- let open Evd in
- eq_constr sigma1 sigma2 ei1.evar_concl ei2.evar_concl &&
- eq_named_context_val sigma1 sigma2 (ei1.evar_hyps) (ei2.evar_hyps) &&
- eq_evar_body sigma1 sigma2 ei1.evar_body ei2.evar_body
-
- (** 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
- eq_evar_info evars1 evars2 evi1 evi2
-
-end
-
-let tclPROGRESS t =
- let open Proof in
- Pv.get >>= fun initial ->
- t >>= fun res ->
- Pv.get >>= fun final ->
- (* [*_test] test absence of progress. [quick_test] is approximate
- whereas [exhaustive_test] is complete. *)
- let quick_test =
- initial.solution == final.solution && initial.comb == final.comb
- in
- let exhaustive_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 (Errors.UserError ("Proofview.tclPROGRESS" , Pp.str"Failed to progress."))
-
-exception Timeout
-let _ = Errors.register_handler begin function
- | Timeout -> Errors.errorlabstrm "Proofview.tclTIMEOUT" (Pp.str"Tactic timeout!")
- | _ -> Pervasives.raise Errors.Unhandled
-end
-
-let tclTIMEOUT n t =
- let open Proof in
- (* spiwack: as one of the monad is a continuation passing monad, it
- doesn't force the computation to be threaded inside the underlying
- (IO) monad. Hence I force it myself by asking for the evaluation of
- a dummy value first, lest [timeout] be called when everything has
- already been computed. *)
- let t = Proof.lift (Logic_monad.NonLogical.return ()) >> t in
- Proof.get >>= fun initial ->
- Proof.current >>= fun envvar ->
- Proof.lift begin
- Logic_monad.NonLogical.catch
- begin
- let open Logic_monad.NonLogical in
- timeout n (Proof.repr (Proof.run t envvar initial)) >>= fun r ->
- match r with
- | Logic_monad.Nil e -> return (Util.Inr e)
- | Logic_monad.Cons (r, _) -> return (Util.Inl r)
- end
- begin let open Logic_monad.NonLogical in function (e, info) ->
- match e with
- | Logic_monad.Timeout -> return (Util.Inr (Timeout, info))
- | Logic_monad.TacticFailure e ->
- return (Util.Inr (e, info))
- | e -> Logic_monad.NonLogical.raise ~info e
- end
- end >>= function
- | Util.Inl (res,s,m,i) ->
- Proof.set s >>
- Proof.put m >>
- Proof.update (fun _ -> i) >>
- return res
- | Util.Inr (e, info) -> tclZERO ~info e
-
-let tclTIME s t =
- let pr_time t1 t2 n msg =
- let msg =
- if n = 0 then
- str msg
- else
- str (msg ^ " after ") ++ int n ++ str (String.plural n " backtracking")
- in
- msg_info(str "Tactic call" ++ pr_opt str s ++ str " ran for " ++
- System.fmt_time_difference t1 t2 ++ str " " ++ surround msg) in
- let rec aux n t =
- let open Proof in
- tclUNIT () >>= fun () ->
- let tstart = System.get_time() in
- Proof.split t >>= let open Logic_monad in function
- | Nil (e, info) ->
- begin
- let tend = System.get_time() in
- pr_time tstart tend n "failure";
- tclZERO ~info e
- end
- | Cons (x,k) ->
- let tend = System.get_time() in
- pr_time tstart tend n "success";
- tclOR (tclUNIT x) (fun e -> aux (n+1) (k e))
- in aux 0 t
-
-
-
-(** {7 Unsafe primitives} *)
-
-module Unsafe = struct
-
- let tclEVARS evd =
- Pv.modify (fun ps -> { ps with solution = evd })
-
- let tclNEWGOALS gls =
- Pv.modify begin fun step ->
- let gls = undefined step.solution gls in
- { step with comb = step.comb @ gls }
- end
-
- let tclGETGOALS = Comb.get
-
- let tclSETGOALS = Comb.set
-
- let tclEVARSADVANCE evd =
- Pv.modify (fun ps -> { ps with solution = evd; comb = undefined evd ps.comb })
-
- let tclEVARUNIVCONTEXT ctx =
- Pv.modify (fun ps -> { ps with solution = Evd.set_universe_context ps.solution ctx })
-
- let reset_future_goals p =
- { 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 = Typeclasses.mark_unresolvable info in
- Evd.add evd content info
-
- let advance = advance
-
-end
-
-module UnsafeRepr = Proof.Unsafe
-
-let (>>=) = tclBIND
-let (<*>) = tclTHEN
-let (<+>) t1 t2 = tclOR t1 (fun _ -> t2)
-
-(** {6 Goal-dependent tactics} *)
-
-let goal_env evars gl =
- let evi = Evd.find evars gl in
- Evd.evar_filtered_env evi
-
-let goal_nf_evar sigma gl =
- let evi = Evd.find sigma gl in
- let evi = Evarutil.nf_evar_info sigma evi in
- let sigma = Evd.add sigma gl evi in
- (gl, sigma)
-
-let goal_extra evars gl =
- let evi = Evd.find evars gl in
- evi.Evd.evar_extra
-
-
-let catchable_exception = function
- | Logic_monad.Exception _ -> false
- | e -> Errors.noncritical e
-
-
-module Goal = struct
-
- type ('a, 'r) t = {
- env : Environ.env;
- sigma : Evd.evar_map;
- concl : Term.constr ;
- 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 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 raw_concl { concl=concl } = concl
-
-
- let gmake_with info env sigma goal =
- { env = Environ.reset_with_named_context (Evd.evar_filtered_hyps info) env ;
- sigma = sigma ;
- concl = Evd.evar_concl info ;
- self = goal }
-
- let nf_gmake env sigma goal =
- 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
-
- let nf_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
- tclTHEN (Unsafe.tclEVARS sigma) (InfoL.tag (Info.DBranch) (f.enter gl))
- with e when catchable_exception e ->
- let (e, info) = Errors.push e in
- tclZERO ~info e
- end
- end
-
- let normalize { self } =
- Env.get >>= fun env ->
- tclEVARMAP >>= fun sigma ->
- let (gl,sigma) = nf_gmake env sigma self in
- tclTHEN (Unsafe.tclEVARS sigma) (tclUNIT gl)
-
- let gmake env sigma goal =
- let info = Evd.find sigma goal in
- gmake_with info env sigma goal
-
- let enter f =
- let f gl = InfoL.tag (Info.DBranch) (f.enter gl) in
- InfoL.tag (Info.Dispatch) begin
- iter_goal begin fun goal ->
- Env.get >>= fun env ->
- tclEVARMAP >>= fun sigma ->
- try f (gmake env sigma goal)
- with e when catchable_exception e ->
- let (e, info) = Errors.push e in
- tclZERO ~info e
- end
- end
-
- 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) = Errors.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) = Errors.push e in
- tclZERO ~info e
- end
- end
-
- let goals =
- Pv.get >>= fun step ->
- let sigma = step.solution in
- let map goal =
- match advance sigma goal with
- | None -> None (** ppedrot: Is this check really necessary? *)
- | Some goal ->
- let gl =
- Env.get >>= fun env ->
- tclEVARMAP >>= fun sigma ->
- tclUNIT (gmake env sigma goal)
- in
- Some gl
- in
- tclUNIT (CList.map_filter map step.comb)
-
- (* compatibility *)
- let goal { self=self } = self
-
- let lift (gl : ('a, 'r) t) _ = (gl :> ('a, 's) t)
-
-end
-
-
-
-(** {6 Trace} *)
-
-module Trace = struct
-
- let record_info_trace = InfoL.record_trace
-
- let log m = InfoL.leaf (Info.Msg m)
- let name_tactic m t = InfoL.tag (Info.Tactic m) t
-
- let pr_info ?(lvl=0) info =
- assert (lvl >= 0);
- Info.(print (collapse lvl info))
-
-end
-
-
-
-(** {6 Non-logical state} *)
-
-module NonLogical = Logic_monad.NonLogical
-
-let tclLIFT = Proof.lift
-
-let tclCHECKINTERRUPT =
- tclLIFT (NonLogical.make Control.check_for_interrupt)
-
-
-
-
-
-(*** Compatibility layer with <= 8.2 tactics ***)
-module V82 = struct
- type tac = Evar.t Evd.sigma -> Evar.t list Evd.sigma
-
- let tactic 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 glsigma =
- tac { Evd.it = gl ; sigma = evd; } in
- let sigma = glsigma.Evd.sigma in
- let g = 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
- in
- let (goalss,evd) = Evd.Monad.List.map tac initgoals initevd in
- let sgs = CList.flatten goalss in
- let sgs = undefined evd sgs in
- InfoL.leaf (Info.Tactic (fun () -> Pp.str"<unknown>")) >>
- Pv.set { ps with solution = evd; comb = sgs; }
- with e when catchable_exception e ->
- let (e, info) = Errors.push e in
- tclZERO ~info e
-
-
- (* normalises the evars in the goals, and stores the result in
- solution. *)
- 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; }
- end
-
- let has_unresolved_evar pv =
- Evd.has_undefined pv.solution
-
- (* Main function in the implementation of Grab Existential Variables.*)
- 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 }
-
-
-
- (* 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 }
-
- let top_goals initial { solution=solution; } =
- let goals = CList.map (fun (t,_) -> fst (Term.destEvar 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)
- 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 (_,final,_,_) = apply (goal_env gls.Evd.sigma gls.Evd.it) t init in
- { Evd.sigma = final.solution ; it = final.comb }
- with Logic_monad.TacticFailure e as src ->
- let (_, info) = Errors.push src in
- iraise (e, info)
-
- let put_status = Status.put
-
- let catchable_exception = catchable_exception
-
- let wrap_exceptions f =
- try f ()
- with e when catchable_exception e ->
- let (e, info) = Errors.push e in tclZERO ~info e
-
-end
-
-(** {7 Notations} *)
-
-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
diff --git a/proofs/proofview.mli b/proofs/proofview.mli
deleted file mode 100644
index 6bc2e9a0e..000000000
--- a/proofs/proofview.mli
+++ /dev/null
@@ -1,586 +0,0 @@
-(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
-(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
-(************************************************************************)
-
-(** This files defines the basic mechanism of proofs: the [proofview]
- type is the state which tactics manipulate (a global state for
- existential variables, together with the list of goals), and the type
- ['a tactic] is the (abstract) type of tactics modifying the proof
- state and returning a value of type ['a]. *)
-
-open Util
-open Term
-
-(** Main state of tactics *)
-type proofview
-
-(** Returns a stylised view of a proofview for use by, for instance,
- ide-s. *)
-(* spiwack: the type of [proofview] will change as we push more
- refined functions to ide-s. This would be better than spawning a
- new nearly identical function everytime. Hence the generic name. *)
-(* In this version: returns the list of focused goals together with
- the [evar_map] context. *)
-val proofview : proofview -> Goal.goal list * Evd.evar_map
-
-
-(** {6 Starting and querying a proof view} *)
-
-(** Abstract representation of the initial goals of a proof. *)
-type entry
-
-(** Optimize memory consumption *)
-val compact : entry -> proofview -> entry * proofview
-
-(** Initialises a proofview, the main argument is a list of
- environments (including a [named_context] which are used as
- hypotheses) pair with conclusion types, creating accordingly many
- initial goals. Because a proof does not necessarily starts in an
- empty [evar_map] (indeed a proof can be triggered by an incomplete
- pretyping), [init] takes an additional argument to represent the
- initial [evar_map]. *)
-val init : Evd.evar_map -> (Environ.env * Term.types) list -> entry * proofview
-
-(** A [telescope] is a list of environment and conclusion like in
- {!init}, except that each element may depend on the previous
- goals. The telescope passes the goals in the form of a
- [Term.constr] which represents the goal as an [evar]. The
- [evar_map] is threaded in state passing style. *)
-type telescope =
- | TNil of Evd.evar_map
- | TCons of Environ.env * Evd.evar_map * Term.types * (Evd.evar_map -> Term.constr -> telescope)
-
-(** Like {!init}, but goals are allowed to be dependent on one
- another. Dependencies between goals is represented with the type
- [telescope] instead of [list]. Note that the first [evar_map] of
- the telescope plays the role of the [evar_map] argument in
- [init]. *)
-val dependent_init : telescope -> entry * proofview
-
-(** [finished pv] is [true] if and only if [pv] is complete. That is,
- if it has an empty list of focused goals. There could still be
- unsolved subgoaled, but they would then be out of focus. *)
-val finished : proofview -> bool
-
-(** Returns the current [evar] state. *)
-val return : proofview -> Evd.evar_map
-
-val partial_proof : entry -> proofview -> constr list
-val initial_goals : entry -> (constr * types) list
-
-
-
-(** {6 Focusing commands} *)
-
-(** A [focus_context] represents the part of the proof view which has
- been removed by a focusing action, it can be used to unfocus later
- on. *)
-type focus_context
-
-(** Returns a stylised view of a focus_context for use by, for
- instance, ide-s. *)
-(* spiwack: the type of [focus_context] will change as we push more
- refined functions to ide-s. This would be better than spawning a
- 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). *)
-val focus_context : focus_context -> Goal.goal list * Goal.goal list
-
-(** [focus i j] focuses a proofview on the goals from index [i] to
- index [j] (inclusive, goals are indexed from [1]). I.e. goals
- number [i] to [j] become the only focused goals of the returned
- proofview. It returns the focused proofview, and a context for
- the focus stack. *)
-val focus : int -> int -> proofview -> proofview * focus_context
-
-(** Unfocuses a proofview with respect to a context. *)
-val unfocus : focus_context -> proofview -> proofview
-
-
-(** {6 The tactic monad} *)
-
-(** - Tactics are objects which apply a transformation to all the
- subgoals of the current view at the same time. By opposition to
- the old vision of applying it to a single goal. It allows tactics
- such as [shelve_unifiable], tactics to reorder the focused goals,
- or global automation tactic for dependent subgoals (instantiating
- an evar has influences on the other goals of the proof in
- progress, not being able to take that into account causes the
- current eauto tactic to fail on some instances where it could
- succeed). Another benefit is that it is possible to write tactics
- that can be executed even if there are no focused goals.
- - Tactics form a monad ['a tactic], in a sense a tactic can be
- seen as a function (without argument) which returns a value of
- type 'a and modifies the environment (in our case: the view).
- Tactics of course have arguments, but these are given at the
- meta-level as OCaml functions. Most tactics in the sense we are
- used to return [()], that is no really interesting values. But
- some might pass information around. The tactics seen in Coq's
- Ltac are (for now at least) only [unit tactic], the return values
- are kept for the OCaml toolkit. The operation or the monad are
- [Proofview.tclUNIT] (which is the "return" of the tactic monad)
- [Proofview.tclBIND] (which is the "bind") and [Proofview.tclTHEN]
- (which is a specialized bind on unit-returning tactics).
- - Tactics have support for full-backtracking. Tactics can be seen
- having multiple success: if after returning the first success a
- failure is encountered, the tactic can backtrack and use a second
- success if available. The state is backtracked to its previous
- value, except the non-logical state defined in the {!NonLogical}
- module below.
-*)
-
-
-(** The abstract type of tactics *)
-type +'a tactic
-
-(** Applies a tactic to the current proofview. Returns a tuple
- [a,pv,(b,sh,gu)] where [a] is the return value of the tactic, [pv]
- is the updated proofview, [b] a boolean which is [true] if the
- tactic has not done any action considered unsafe (such as
- admitting a lemma), [sh] is the list of goals which have been
- shelved by the tactic, and [gu] the list of goals on which the
- tactic has given up. In case of multiple success the first one is
- selected. If there is no success, fails with
- {!Logic_monad.TacticFailure}*)
-val apply : Environ.env -> 'a tactic -> proofview -> 'a
- * proofview
- * (bool*Goal.goal list*Goal.goal list)
- * Proofview_monad.Info.tree
-
-(** {7 Monadic primitives} *)
-
-(** Unit of the tactic monad. *)
-val tclUNIT : 'a -> 'a tactic
-
-(** Bind operation of the tactic monad. *)
-val tclBIND : 'a tactic -> ('a -> 'b tactic) -> 'b tactic
-
-(** Interprets the ";" (semicolon) of Ltac. As a monadic operation,
- it's a specialized "bind". *)
-val tclTHEN : unit tactic -> 'a tactic -> 'a tactic
-
-(** [tclIGNORE t] has the same operational content as [t], but drops
- the returned value. *)
-val tclIGNORE : 'a tactic -> unit tactic
-
-(** Generic monadic combinators for tactics. *)
-module Monad : Monad.S with type +'a t = 'a tactic
-
-(** {7 Failure and backtracking} *)
-
-(** [tclZERO e] fails with exception [e]. It has no success. *)
-val tclZERO : ?info:Exninfo.info -> exn -> 'a tactic
-
-(** [tclOR t1 t2] behaves like [t1] as long as [t1] succeeds. Whenever
- the successes of [t1] have been depleted and it failed with [e],
- then it behaves as [t2 e]. In other words, [tclOR] inserts a
- backtracking point. *)
-val tclOR : 'a tactic -> (iexn -> 'a tactic) -> 'a tactic
-
-(** [tclORELSE t1 t2] is equal to [t1] if [t1] has at least one
- success or [t2 e] if [t1] fails with [e]. It is analogous to
- [try/with] handler of exception in that it is not a backtracking
- point. *)
-val tclORELSE : 'a tactic -> (iexn -> 'a tactic) -> 'a tactic
-
-(** [tclIFCATCH a s f] is a generalisation of {!tclORELSE}: if [a]
- succeeds at least once then it behaves as [tclBIND a s] otherwise,
- if [a] fails with [e], then it behaves as [f e]. *)
-val tclIFCATCH : 'a tactic -> ('a -> 'b tactic) -> (iexn -> 'b tactic) -> 'b tactic
-
-(** [tclONCE t] behave like [t] except it has at most one success:
- [tclONCE t] stops after the first success of [t]. If [t] fails
- with [e], [tclONCE t] also fails with [e]. *)
-val tclONCE : 'a tactic -> 'a tactic
-
-(** [tclEXACTLY_ONCE e t] succeeds as [t] if [t] has exactly one
- success. Otherwise it fails. The tactic [t] is run until its first
- success, then a failure with exception [e] is simulated. It [t]
- yields another success, then [tclEXACTLY_ONCE e t] fails with
- [MoreThanOneSuccess] (it is a user error). Otherwise,
- [tclEXACTLY_ONCE e t] succeeds with the first success of
- [t]. Notice that the choice of [e] is relevant, as the presence of
- further successes may depend on [e] (see {!tclOR}). *)
-exception MoreThanOneSuccess
-val tclEXACTLY_ONCE : exn -> 'a tactic -> 'a tactic
-
-(** [tclCASE t] splits [t] into its first success and a
- continuation. It is the most general primitive to control
- backtracking. *)
-type 'a case =
- | Fail of iexn
- | Next of 'a * (iexn -> 'a tactic)
-val tclCASE : 'a tactic -> 'a case tactic
-
-(** [tclBREAK p t] is a generalization of [tclONCE t]. Instead of
- stopping after the first success, it succeeds like [t] until a
- failure with an exception [e] such that [p e = Some e'] is raised. At
- which point it drops the remaining successes, failing with [e'].
- [tclONCE t] is equivalent to [tclBREAK (fun e -> Some e) t]. *)
-val tclBREAK : (iexn -> iexn option) -> 'a tactic -> 'a tactic
-
-
-(** {7 Focusing tactics} *)
-
-(** [tclFOCUS i j t] applies [t] after focusing on the goals number
- [i] to [j] (see {!focus}). The rest of the goals is restored after
- the tactic action. If the specified range doesn't correspond to
- existing goals, fails with [NoSuchGoals] (a user error). this
- exception is caught at toplevel with a default message + a hook
- message that can be customized by [set_nosuchgoals_hook] below.
- This hook is used to add a suggestion about bullets when
- applicable. *)
-exception NoSuchGoals of int
-val set_nosuchgoals_hook: (int -> Pp.std_ppcmds) -> unit
-
-val tclFOCUS : int -> int -> 'a tactic -> 'a tactic
-
-(** [tclFOCUSID x t] applies [t] on a (single) focused goal like
- {!tclFOCUS}. The goal is found by its name rather than its
- number.*)
-val tclFOCUSID : Names.Id.t -> 'a tactic -> 'a tactic
-
-(** [tclTRYFOCUS i j t] behaves like {!tclFOCUS}, except that if the
- specified range doesn't correspond to existing goals, behaves like
- [tclUNIT ()] instead of failing. *)
-val tclTRYFOCUS : int -> int -> unit tactic -> unit tactic
-
-
-(** {7 Dispatching on goals} *)
-
-(** Dispatch tacticals are used to apply a different tactic to each
- goal under focus. They come in two flavours: [tclDISPATCH] takes a
- list of [unit tactic]-s and build a [unit tactic]. [tclDISPATCHL]
- takes a list of ['a tactic] and returns an ['a list tactic].
-
- They both work by applying each of the tactic in a focus
- restricted to the corresponding goal (starting with the first
- goal). In the case of [tclDISPATCHL], the tactic returns a list of
- the same size as the argument list (of tactics), each element
- being the result of the tactic executed in the corresponding goal.
-
- When the length of the tactic list is not the number of goal,
- raises [SizeMismatch (g,t)] where [g] is the number of available
- goals, and [t] the number of tactics passed. *)
-exception SizeMismatch of int*int
-val tclDISPATCH : unit tactic list -> unit tactic
-val tclDISPATCHL : 'a tactic list -> 'a list tactic
-
-(** [tclEXTEND b r e] is a variant of {!tclDISPATCH}, where the [r]
- tactic is "repeated" enough time such that every goal has a tactic
- assigned to it ([b] is the list of tactics applied to the first
- goals, [e] to the last goals, and [r] is applied to every goal in
- between). *)
-val tclEXTEND : unit tactic list -> unit tactic -> unit tactic list -> unit tactic
-
-(** [tclINDEPENDENT tac] runs [tac] on each goal successively, from
- the first one to the last one. Backtracking in one goal is
- independent of backtracking in another. It is equivalent to
- [tclEXTEND [] tac []]. *)
-val tclINDEPENDENT : unit tactic -> unit tactic
-
-
-(** {7 Goal manipulation} *)
-
-(** Shelves all the goals under focus. The goals are placed on the
- shelf for later use (or being solved by side-effects). *)
-val shelve : unit tactic
-
-(** Shelves the unifiable goals under focus, i.e. the goals which
- appear in other goals under focus (the unfocused goals are not
- considered). *)
-val shelve_unifiable : unit tactic
-
-(** [guard_no_unifiable] returns the list of unifiable goals if some
- goals are unifiable (see {!shelve_unifiable}) in the current focus. *)
-val guard_no_unifiable : Names.Name.t list option tactic
-
-(** [unshelve l p] adds all the goals in [l] at the end of the focused
- goals of p *)
-val unshelve : Goal.goal list -> proofview -> proofview
-
-(** [with_shelf tac] executes [tac] and returns its result together with the set
- of goals shelved by [tac]. The current shelf is unchanged. *)
-val with_shelf : 'a tactic -> (Goal.goal list * 'a) tactic
-
-(** If [n] is positive, [cycle n] puts the [n] first goal last. If [n]
- is negative, then it puts the [n] last goals first.*)
-val cycle : int -> unit tactic
-
-(** [swap i j] swaps the position of goals number [i] and [j]
- (negative numbers can be used to address goals from the end. Goals
- are indexed from [1]. For simplicity index [0] corresponds to goal
- [1] as well, rather than raising an error. *)
-val swap : int -> int -> unit tactic
-
-(** [revgoals] reverses the list of focused goals. *)
-val revgoals : unit tactic
-
-(** [numgoals] returns the number of goals under focus. *)
-val numgoals : int tactic
-
-
-(** {7 Access primitives} *)
-
-(** [tclEVARMAP] doesn't affect the proof, it returns the current
- [evar_map]. *)
-val tclEVARMAP : Evd.evar_map tactic
-
-(** [tclENV] doesn't affect the proof, it returns the current
- environment. It is not the environment of a particular goal,
- rather the "global" environment of the proof. The goal-wise
- environment is obtained via {!Proofview.Goal.env}. *)
-val tclENV : Environ.env tactic
-
-
-(** {7 Put-like primitives} *)
-
-(** [tclEFFECTS eff] add the effects [eff] to the current state. *)
-val tclEFFECTS : Safe_typing.private_constants -> unit tactic
-
-(** [mark_as_unsafe] declares the current tactic is unsafe. *)
-val mark_as_unsafe : unit tactic
-
-(** Gives up on the goal under focus. Reports an unsafe status. Proofs
- with given up goals cannot be closed. *)
-val give_up : unit tactic
-
-
-(** {7 Control primitives} *)
-
-(** [tclPROGRESS t] checks the state of the proof after [t]. It it is
- identical to the state before, then [tclePROGRESS t] fails, otherwise
- it succeeds like [t]. *)
-val tclPROGRESS : 'a tactic -> 'a tactic
-
-(** Checks for interrupts *)
-val tclCHECKINTERRUPT : unit tactic
-
-exception Timeout
-(** [tclTIMEOUT n t] can have only one success.
- In case of timeout if fails with [tclZERO Timeout]. *)
-val tclTIMEOUT : int -> 'a tactic -> 'a tactic
-
-(** [tclTIME s t] displays time for each atomic call to t, using s as an
- identifying annotation if present *)
-val tclTIME : string option -> 'a tactic -> 'a tactic
-
-(** {7 Unsafe primitives} *)
-
-(** The primitives in the [Unsafe] module should be avoided as much as
- possible, since they can make the proof state inconsistent. They are
- nevertheless helpful, in particular when interfacing the pretyping and
- the proof engine. *)
-module Unsafe : sig
-
- (** [tclEVARS sigma] replaces the current [evar_map] by [sigma]. If
- [sigma] has new unresolved [evar]-s they will not appear as
- goal. If goals have been solved in [sigma] they will still
- appear as unsolved goals. *)
- val tclEVARS : Evd.evar_map -> unit tactic
-
- (** Like {!tclEVARS} but also checks whether goals have been solved. *)
- val tclEVARSADVANCE : Evd.evar_map -> 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. *)
- val tclNEWGOALS : Goal.goal list -> unit tactic
-
- (** [tclSETGOALS gls] sets goals [gls] as the goals being under focus. If a
- goal is already solved, it is not set. *)
- val tclSETGOALS : Goal.goal list -> unit tactic
-
- (** [tclGETGOALS] returns the list of goals under focus. *)
- val tclGETGOALS : Goal.goal list tactic
-
- (** Sets the evar universe context. *)
- val tclEVARUNIVCONTEXT : Evd.evar_universe_context -> unit tactic
-
- (** Clears the future goals store in the proof view. *)
- val reset_future_goals : proofview -> proofview
-
- (** Give an evar the status of a goal (changes its source location
- and makes it unresolvable for type classes. *)
- val mark_as_goal : Evd.evar_map -> Evar.t -> Evd.evar_map
-
- (** [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)
- solved. *)
- val advance : Evd.evar_map -> Evar.t -> Evar.t option
-end
-
-(** This module gives access to the innards of the monad. Its use is
- restricted to very specific cases. *)
-module UnsafeRepr :
-sig
- type state = Proofview_monad.Logical.Unsafe.state
- val repr : 'a tactic -> ('a, state, state, iexn) Logic_monad.BackState.t
- val make : ('a, state, state, iexn) Logic_monad.BackState.t -> 'a tactic
-end
-
-(** {6 Goal-dependent tactics} *)
-
-module Goal : sig
-
- (** Type of goals.
-
- The first parameter type is a phantom argument indicating whether the data
- contained in the goal has been normalized w.r.t. the current sigma. If it
- is the case, it is flagged [ `NF ]. You may still access the un-normalized
- data using {!assume} if you known you do not rely on the assumption of
- being normalized, at your own risk.
-
- The second parameter is a stage indicating where the goal belongs. See
- module {!Sigma}.
- *)
- type ('a, 'r) t
-
- (** Assume that you do not need the goal to be normalized. *)
- val assume : ('a, 'r) t -> ([ `NF ], 'r) t
-
- (** Normalises the argument goal. *)
- val normalize : ('a, 'r) t -> ([ `NF ], 'r) t tactic
-
- (** [concl], [hyps], [env] and [sigma] given a goal [gl] return
- respectively the conclusion of [gl], the hypotheses of [gl], the
- environment of [gl] (i.e. the global environment and the
- hypotheses) and the current evar map. *)
- val concl : ([ `NF ], 'r) t -> Term.constr
- val hyps : ([ `NF ], 'r) t -> Context.Named.t
- val env : ('a, 'r) t -> Environ.env
- val sigma : ('a, 'r) t -> 'r Sigma.t
- val extra : ('a, 'r) t -> Evd.Store.t
-
- (** Returns the goal's conclusion even if the goal is not
- normalised. *)
- val raw_concl : ('a, 'r) t -> Term.constr
-
- type ('a, 'b) enter =
- { enter : 'r. ('a, 'r) t -> 'b }
-
- (** [nf_enter t] applies the goal-dependent tactic [t] in each goal
- independently, in the manner of {!tclINDEPENDENT} except that
- the current goal is also given as an argument to [t]. The goal
- is normalised with respect to evars. *)
- val nf_enter : ([ `NF ], unit tactic) enter -> unit tactic
-
- (** Like {!nf_enter}, but does not normalize the goal beforehand. *)
- val enter : ([ `LZ ], unit tactic) enter -> unit tactic
-
- type ('a, 'b) s_enter =
- { s_enter : 'r. ('a, 'r) t -> ('b, 'r) Sigma.sigma }
-
- (** A variant of {!enter} allows to work with a monotonic state. The evarmap
- returned by the argument is put back into the current state before firing
- the returned tactic. *)
- val s_enter : ([ `LZ ], unit tactic) s_enter -> unit tactic
-
- (** Like {!s_enter}, but normalizes the goal beforehand. *)
- val nf_s_enter : ([ `NF ], unit tactic) s_enter -> unit tactic
-
- (** Recover the list of current goals under focus, without evar-normalization.
- FIXME: encapsulate the level in an existential type. *)
- val goals : ([ `LZ ], 'r) t tactic list tactic
-
- (** Compatibility: avoid if possible *)
- val goal : ([ `NF ], 'r) t -> Evar.t
-
- (** Every goal is valid at a later stage. FIXME: take a later evarmap *)
- val lift : ('a, 'r) t -> ('r, 's) Sigma.le -> ('a, 's) t
-
-end
-
-
-(** {6 Trace} *)
-
-module Trace : sig
-
- (** [record_info_trace t] behaves like [t] except the [info] trace
- is stored. *)
- val record_info_trace : 'a tactic -> 'a tactic
-
- val log : Proofview_monad.lazy_msg -> unit tactic
- val name_tactic : Proofview_monad.lazy_msg -> 'a tactic -> 'a tactic
-
- val pr_info : ?lvl:int -> Proofview_monad.Info.tree -> Pp.std_ppcmds
-
-end
-
-
-(** {6 Non-logical state} *)
-
-(** The [NonLogical] module allows the execution of effects (including
- I/O) in tactics (non-logical side-effects are not discarded at
- failures). *)
-module NonLogical : module type of Logic_monad.NonLogical
-
-(** [tclLIFT c] is a tactic which behaves exactly as [c]. *)
-val tclLIFT : 'a NonLogical.t -> 'a tactic
-
-
-(**/**)
-
-(*** Compatibility layer with <= 8.2 tactics ***)
-module V82 : sig
- type tac = Evar.t Evd.sigma -> Evar.t list Evd.sigma
- val tactic : tac -> unit tactic
-
- (* normalises the evars in the goals, and stores the result in
- solution. *)
- val nf_evar_goals : unit tactic
-
- val has_unresolved_evar : proofview -> bool
-
- (* Main function in the implementation of Grab Existential Variables.
- Resets the proofview's goals so that it contains all unresolved evars
- (in chronological order of insertion). *)
- val grab : proofview -> proofview
-
- (* Returns the open goals of the proofview together with the evar_map to
- interpret them. *)
- val goals : proofview -> Evar.t list Evd.sigma
-
- val top_goals : entry -> proofview -> Evar.t list Evd.sigma
-
- (* returns the existential variable used to start the proof *)
- val top_evars : entry -> Evd.evar list
-
- (* Caution: this function loses quite a bit of information. It
- should be avoided as much as possible. It should work as
- expected for a tactic obtained from {!V82.tactic} though. *)
- val of_tactic : 'a tactic -> tac
-
- (* marks as unsafe if the argument is [false] *)
- val put_status : bool -> unit tactic
-
- (* exception for which it is deemed to be safe to transmute into
- tactic failure. *)
- val catchable_exception : exn -> bool
-
- (* transforms every Ocaml (catchable) exception into a failure in
- the monad. *)
- val wrap_exceptions : (unit -> 'a tactic) -> 'a tactic
-end
-
-(** {7 Notations} *)
-
-module Notations : sig
-
- (** {!tclBIND} *)
- val (>>=) : 'a tactic -> ('a -> 'b tactic) -> 'b tactic
- (** {!tclTHEN} *)
- val (<*>) : unit tactic -> 'a tactic -> 'a tactic
- (** {!tclOR}: [t1+t2] = [tclOR t1 (fun _ -> t2)]. *)
- val (<+>) : 'a tactic -> 'a tactic -> 'a tactic
-
- 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