aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--bootstrap/Monads.v605
-rw-r--r--dev/printers.mllib4
-rw-r--r--proofs/monads.ml496
-rw-r--r--proofs/proof_errors.ml12
-rw-r--r--proofs/proof_errors.mli18
-rw-r--r--proofs/proofs.mllib4
-rw-r--r--proofs/proofview.ml196
-rw-r--r--proofs/proofview.mli7
-rw-r--r--proofs/proofview_gen.ml377
-rw-r--r--proofs/proofview_monad.ml1
-rw-r--r--proofs/proofview_monad.mli81
-rw-r--r--tactics/tacticals.ml2
-rw-r--r--tactics/tactics.ml7
-rw-r--r--toplevel/cerrors.ml3
14 files changed, 1218 insertions, 595 deletions
diff --git a/bootstrap/Monads.v b/bootstrap/Monads.v
new file mode 100644
index 0000000000..26583b0be5
--- /dev/null
+++ b/bootstrap/Monads.v
@@ -0,0 +1,605 @@
+(* -*- coq-prog-args: ("-emacs-U" "-impredicative-set") -*- *)
+
+(* arnaud: on ne doit pas en avoir besoin normalement. *)
+
+Reserved Notation "'do' M x ':=' e 'in' u" (at level 200, M at level 0, x ident, e at level 200, u at level 200).
+(*Reserved Notation "'do' e ; u" (at level 200, e at level 200, u at level 200).*)
+
+(*** Unit ***)
+
+Extract Inductive unit => unit [
+ "()"
+].
+Notation "()" := tt.
+
+(*** Bool ***)
+Extract Inductive bool => bool [
+ "true"
+ "false"
+].
+
+(*** List ***)
+Extract Inductive list => list [
+ "[]"
+ "(::)"
+].
+
+(*** Prod ***)
+Extract Inductive prod => "(*)" [
+ "(,)"
+].
+
+(*** Sum ***)
+Print sum.
+Extract Inductive sum => "Util.union" [
+ "Util.Inl"
+ "Util.Inr"
+].
+
+(*** Exceptions ***)
+
+Parameter Exception : Set.
+Extract Inlined Constant Exception => exn.
+
+Parameter tactic_failure : Exception -> Exception.
+Extract Inlined Constant tactic_failure => "(fun e -> Proof_errors.TacticFailure e)".
+
+(*** Monoids ***)
+
+Module Monoid.
+
+Record T (M:Set) := {
+ zero : M;
+ prod : M -> M -> M
+}.
+
+End Monoid.
+
+(*** Monads and related interfaces ***)
+(* spiwack: the interfaces are presented in a mixin style.
+ I haven't tested other presentation, it just felt
+ convenient when I started *)
+
+Record Monad (T:Set->Set) := {
+ ret : forall{A:Set}, A->T A;
+ bind : forall{A B:Set}, T A -> (A -> T B) -> T B;
+ ignore : forall{A:Set}, T A -> T unit;
+ seq : forall{A:Set}, T unit -> T A -> T A
+}.
+
+Notation "'do' M x ':=' e 'in' u" := (bind _ M e (fun x => u)).
+
+Record State (S:Set) (T:Set->Set) := {
+ set : S -> T unit;
+ get : T S
+}.
+
+(* spiwack: Environment and Writer are given distinct interfaces from
+ State (rather than state beeing the composition of these) because I
+ don't really know how to combine the three together. However, we
+ might want to be able to arrange things so that we can say "I have a
+ number of things I can get, and a number of things I can set, some
+ of which can be got, and the other being monoids, then I have a
+ monad". I have yet to find how to do that though.*)
+Record Environment (E:Set) (T:Set->Set) := { current : T E }.
+
+Record Writer (M:Set) (T:Set->Set) := {
+ put : M -> T unit
+}.
+
+Record Logic (T:Set -> Set) := {
+ (* [zero] is usually argument free, but Coq likes to explain errors,
+ hence error messages should be carried around. *)
+ zero : forall {A}, Exception -> T A;
+ plus : forall {A}, T A -> (Exception -> T A) -> T A;
+ (** [split x] runs [x] until it either fails with [zero e] or finds
+ a result [a]. In the former case it returns [Inr e], otherwise
+ it returns [Inl (a,y)] where [y] can be run to get more results
+ from [x]. It is a variant of prolog's cut. *)
+ split : forall {A}, T A -> T ((A * (Exception -> T A)) + Exception)%type
+}.
+(** Writing (+) for plus and (>>=) for bind, we shall require that
+
+ x+(y+z) = (x+y)+z
+
+ zero+x = x
+
+ x+zero = x
+
+ (x+y)>>=k = (x>>=k)+(y>>=k) *)
+(* The [T] argument represents the "global" effect: it is not
+ backtracked when backtracking occurs at a [plus]. *)
+(* spiwack: hence, [T] will not be instanciated with a state monad
+ representing the proofs, we will use a surrounding state transformer
+ to that effect. [T] is meant to be instantiated with [IO]. *)
+
+
+Module Id.
+
+ Definition M : Monad (fun A => A) := {|
+ ret := fun _ x => x;
+ bind := fun _ _ x k => k x;
+ ignore := fun _ x => ();
+ seq := fun _ x k => k
+ |}.
+
+End Id.
+
+Module IOBase.
+
+ Parameter T : Set -> Set.
+ Extract Constant T "'a" => "unit -> 'a".
+ Parameter Ref : Set -> Set.
+ Extract Constant Ref "'a" => "'a Pervasives.ref".
+
+ Parameter ret : forall (A:Set), A -> T A.
+ Extract Constant ret => "fun a () -> a".
+ Extraction Implicit ret [A].
+ Parameter bind : forall A B, T A -> (A->T B) -> T B.
+ Extract Constant bind => "fun a k () -> k (a ()) ()".
+ Extraction Implicit bind [A B].
+ Parameter ignore : forall A, T A -> T unit.
+ Extract Constant ignore => "fun a () -> ignore (a ())".
+ Extraction Implicit ignore [A].
+ Parameter seq : forall A, T unit -> T A -> T A.
+ Extract Constant seq => "fun a k () -> a (); k ()".
+ Extraction Implicit seq [A].
+
+ Parameter ref : forall (A:Set), A -> T (Ref A).
+ Extract Constant ref => "fun a () -> Pervasives.ref a".
+ Extraction Implicit ref [A].
+ Parameter set : forall A, Ref A -> A -> T unit.
+ Extract Constant set => "fun r a () -> Pervasives.(:=) r a".
+ Extraction Implicit set [A].
+ Parameter get : forall A, Ref A -> T A.
+ Extract Constant get => "fun r () -> Pervasives.(!) r".
+ Extraction Implicit get [A].
+
+ Parameter raise : forall A, Exception -> T A.
+ Extract Constant raise => "fun e () -> raise (Proof_errors.Exception e)".
+ Extraction Implicit raise [A].
+ Parameter catch : forall A, T A -> (Exception -> T A) -> T A.
+ Extract Constant catch => "fun s h () -> try s () with Proof_errors.Exception e -> h e ()".
+ Extraction Implicit catch [A].
+
+ Parameter Int : Set.
+ Extract Constant Int => int.
+ Parameter timeout: forall A, Int -> T A -> T A.
+ Extract Constant timeout => "fun n t () ->
+ let timeout_handler _ = Pervasives.raise (Proof_errors.Exception Proof_errors.Timeout) in
+ let psh = Sys.signal Sys.sigalrm (Sys.Signal_handle timeout_handler) in
+ Pervasives.ignore (Unix.alarm n);
+ let restore_timeout () =
+ Pervasives.ignore (Unix.alarm 0);
+ Sys.set_signal Sys.sigalrm psh
+ in
+ try
+ let res = t () in
+ restore_timeout ();
+ res
+ with
+ | e -> restore_timeout (); Pervasives.raise e
+ ".
+ Extraction Implicit timeout [A].
+
+End IOBase.
+
+(* spiwack: IO is split in two modules to avoid moot dependencies and
+ useless extracted code. *)
+Module IO.
+
+ Record S (Ref:Set->Set) (T:Set->Set) : Set := {
+ ref : forall {A:Set}, A -> T (Ref A);
+ set : forall {A:Set}, Ref A -> A -> T unit;
+ get : forall {A:Set}, Ref A -> T A;
+
+ raise : forall {A:Set}, Exception -> T A;
+ catch : forall {A:Set}, T A -> (Exception -> T A) -> T A;
+ timeout : forall {A:Set}, IOBase.Int -> T A -> T A
+ }.
+
+ Definition T : Set -> Set := IOBase.T.
+ Definition Ref : Set -> Set := IOBase.Ref.
+
+ Definition M : Monad T := {|
+ ret := IOBase.ret;
+ bind := IOBase.bind;
+ ignore := IOBase.ignore;
+ seq := IOBase.seq
+ |}.
+
+ Definition IO : S Ref T := {|
+ ref := IOBase.ref;
+ set := IOBase.set;
+ get := IOBase.get;
+
+ raise := IOBase.raise;
+ catch := IOBase.catch;
+ timeout := IOBase.timeout
+ |}.
+
+End IO.
+
+Module State.
+(** State monad transformer, adapted from Haskell' StateT *)
+
+Section Common.
+
+ Variables (S:Set) (T₀:Set->Set) (M:Monad T₀).
+
+ Definition T (A:Set):= S -> T₀ (A*S)%type.
+
+ Definition F : Monad T := {|
+ ret A x s := ret _ M (x,s);
+ bind A B x k s :=
+ do M x := x s in
+ let '(x,s) := x in
+ k x s;
+ ignore A x s :=
+ do M x := x s in
+ let '(_,s) := x in
+ ret _ M ((),s);
+ seq A x k s :=
+ do M x := x s in
+ let '((),s) := x in
+ k s
+ |}.
+
+ Definition State : State S T := {|
+ set := (fun (x s:S) => ret _ M ((),x)) : S -> T unit ;
+ get := fun (s:S) => ret _ M (s,s)
+ |}.
+
+ Definition lift : forall {A}, T₀ A -> T A := fun _ x s =>
+ do M x := x in
+ ret _ M (x,s)
+ .
+
+ Definition run : forall {A}, T A -> S -> T₀ (A*S) := fun _ x => x.
+
+ Variable (L:Logic T₀).
+
+
+ Definition Logic : Logic T := {|
+ zero A e := lift (zero _ L e);
+ plus A x y s := plus _ L (x s) (fun e => y e s);
+ split A x s :=
+ do M x := split _ L (x s) in
+ match x return T₀ (((A*(Exception->T A))+Exception)*S) with
+ | inr e => ret _ M (inr e,s)
+ | inl ((a,s),y) =>
+ let y e (_:S) := y e in
+ ret _ M (inl (a,y) , s)
+ end
+ |}.
+
+End Common.
+
+End State.
+
+
+Module Environment.
+(** An environment monad transformer, like Haskell's ReaderT *)
+
+Section Common.
+
+ Variable (E:Set) (T₀:Set->Set) (M:Monad T₀).
+
+ Definition T (A:Set) := E -> T₀ A.
+
+ Definition F : Monad T := {|
+ ret A x e := ret _ M x;
+ bind A B x k e :=
+ do M x := x e in
+ k x e;
+ ignore A x e := ignore _ M (x e);
+ seq A x k e := seq _ M (x e) (k e)
+ |}.
+
+ Definition Environment : Environment E T := {|
+ current e := ret _ M e
+ |}.
+
+
+ Variable (L:Logic T₀).
+
+
+ Definition Logic : Logic T := {|
+ zero A e env := zero _ L e;
+ plus A x y env := plus _ L (x env) (fun e => y e env);
+ split A x env :=
+ do M x := split _ L (x env) in
+ match x return T₀ ((A*(Exception->T A))+Exception) with
+ | inr e => ret _ M (inr e)
+ | inl (a,y) =>
+ let y e (_:E) := y e in
+ ret _ M (inl (a,y))
+ end
+ |}.
+
+
+ Definition lift {A:Set} (x:T₀ A) : T A := fun _ => x.
+
+ Definition run {A:Set} (x:T A) (e:E) : T₀ A := x e.
+
+End Common.
+
+End Environment.
+
+Module Writer.
+(** A "Writer" monad transformer, that is the canonical monad associated
+ to a monoid. Adaptated from Haskell's WriterT *)
+
+Section Common.
+
+ Variables (C:Set) (m:Monoid.T C) (T₀:Set->Set) (M:Monad T₀).
+
+ Definition T (A:Set) := T₀ (A*C)%type.
+
+ Definition F : Monad T := {|
+ ret A x := ret _ M (x,Monoid.zero _ m);
+ bind A B x k :=
+ do M x := x in
+ let '(x,c) := x in
+ do M y := k x in
+ let '(y,c') := y in
+ ret _ M (y,Monoid.prod _ m c c');
+ ignore A x :=
+ do M x := x in
+ let '(_,c) := x in
+ ret _ M ((),c);
+ seq A x k :=
+ do M x := x in
+ let '((),c) := x in
+ do M y := k in
+ let '(y,c') := y in
+ ret _ M (y,Monoid.prod _ m c c')
+ |}.
+
+ Definition Writer : Writer C T := {|
+ put := fun (x:C) => ret _ M ((),x) : T unit
+ |}.
+
+ Definition lift {A} (x:T₀ A) : T A :=
+ do M x := x in
+ ret _ M (x, Monoid.zero _ m)
+ .
+
+ Definition run {A} (x:T A) : T₀ (A*C)%type := x.
+
+ Variable (L:Logic T₀).
+
+ Definition Logic : Logic T := {|
+ zero A e := lift (zero _ L e);
+ plus A x y := plus _ L x y;
+ split A x :=
+ do M x := split _ L x in
+ match x return T ((A*(Exception -> T A)) + Exception) with
+ | inr e => ret _ M (inr e, Monoid.zero _ m)
+ | inl ((a,c),y) =>
+ ret _ M (inl (a,y), c)
+ end
+ |}.
+
+End Common.
+
+End Writer.
+
+
+Module Logic.
+
+(* Double-continuation backtracking monads are reasonable folklore for
+ "search" implementations (including Tac interactive prover's
+ tactics). Yet it's quite hard to wrap your head around these. I
+ recommand reading a few times the "Backtracking, Interleaving, and
+ Terminating Monad Transformers" paper by O. Kiselyov, C. Chen,
+ D. Fridman. The peculiar shape of the monadic type is reminiscent
+ of that of the continuation monad transformer.
+
+ The paper also contains the rational for the [split] abstraction.
+
+ An explanation of how to derive such a monad from mathematical
+ principles can be found in "Kan Extensions for Program
+ Optimisation" by Ralf Hinze.
+
+ One way to think of the [Logic] functor is to imagine ['a
+ Logic(X).t] to represent list of ['a] with an exception at the
+ bottom (leaving the monad-transforming issues aside, as they don't
+ really work well with lists). Each of the element is a valid
+ result, sequentialising with a [f:'a -> 'b t] is done by applying
+ [f] to each element and then flatten the list, [plus] is
+ concatenation, and [split] is pattern-matching. *)
+(* spiwack: I added the primitives from [IO] directly in the [Logic]
+ signature for convenience. It doesn't really make sense, strictly
+ speaking, as they are somewhat deconnected from the semantics of
+ [Logic], but without an appropriate language for composition (some
+ kind of mixins?) I would be going nowhere with a gazillion
+ functors. *)
+
+Section Common.
+
+ Variables (T₀:Set->Set) (M:Monad T₀).
+
+ Definition FK (R:Set) : Set := Exception -> R.
+ Definition SK (A R:Set) : Set := A -> FK R -> R.
+ Definition T (A:Set) : Set := forall (R:Set), SK A (T₀ R) -> FK (T₀ R) -> T₀ R.
+ (* spiwack: the implementation is an adaptation of the aforementionned
+ "Backtracking, Interleaving, and Terminating Monad Transformers"
+ paper *)
+ (* spiwack: [fk] stands for failure continuation, and [sk] for success
+ continuation. *)
+
+ Definition F : Monad T := {|
+ ret A x R sk fk := sk x fk;
+ bind A B x k R sk fk :=
+ x _ (fun a fk => k a _ sk fk) fk;
+ ignore A x R sk fk :=
+ x _ (fun _ fk => sk () fk) fk;
+ seq A x k R sk fk :=
+ x _ (fun _ fk => k _ sk fk) fk
+ |}.
+
+ Definition lift {A} (x:T₀ A) : T A := fun _ sk fk =>
+ do M x := x in
+ sk x fk
+ .
+
+ Definition _zero {A:Set} (e:Exception) : T A := fun _ _ fk => fk e.
+ Definition _plus {A:Set} (x:T A) (y:Exception -> T A) : T A := fun _ sk fk =>
+ x _ sk (fun e => y e _ sk fk)
+ .
+
+ (* For [reflect] and [split] see the "Backtracking, Interleaving,
+ and Terminating Monad Transformers" paper *)
+ Definition reflect {A:Set} (x:(A*(Exception -> T A)) + Exception) : T A :=
+ match x with
+ | inr e => _zero e
+ | inl (a,x) => _plus (ret _ F a) x
+ end
+ .
+
+ Definition lower {A:Set} (x:T A) : T₀ ((A*(Exception -> T A)) + Exception) :=
+ let fk e := ret _ M (inr e) in
+ let lift_fk fk e := do F y := lift (fk e) in reflect y in
+ let sk a fk := ret _ M (inl (a, lift_fk fk)) in
+ x _ sk fk
+ .
+
+ Definition Logic : Logic T := {|
+ zero := @_zero;
+ plus := @_plus;
+ split A x := lift (lower x)
+ |}.
+
+ Variable (Ref:Set->Set) (IO:IO.S Ref T₀).
+
+ Definition run {A:Set} (x:T A) : T₀ A :=
+ let sk (a:A) _ : T₀ A := ret _ M a in
+ let fk e : T₀ A := IO.raise _ _ IO (tactic_failure e) in
+ x _ sk fk
+ .
+
+End Common.
+
+End Logic.
+
+
+(*** Extraction **)
+
+Parameters (constr types evar_map goal env seffs:Set).
+Extract Inlined Constant constr => "Term.constr".
+Extract Inlined Constant types => "Term.types".
+Extract Inlined Constant evar_map => "Evd.evar_map".
+Extract Inlined Constant goal => "Goal.goal".
+Extract Inlined Constant env => "Environ.env".
+
+Record proofview := {
+ initial : list (constr*types);
+ solution : evar_map;
+ comb : list goal
+}.
+
+Definition LogicalState := proofview.
+Definition LogicalMessageType := bool.
+Definition LogicalEnvironment := env.
+Definition LogicalMessage : Monoid.T LogicalMessageType := {|
+ Monoid.zero := true;
+ Monoid.prod x y := andb x y
+|}.
+
+Definition NonLogicalType := IO.T.
+Definition NonLogicalMonad : Monad NonLogicalType := IO.M.
+Definition NonLogicalIO : IO.S IO.Ref NonLogicalType := IO.IO.
+
+Definition LogicalType := Eval compute in State.T LogicalState (Environment.T LogicalEnvironment (Writer.T LogicalMessageType (Logic.T NonLogicalType))).
+Definition LogicalMonadBase := Logic.F NonLogicalType.
+Definition LogicalMonadWriter := Writer.F _ LogicalMessage _ LogicalMonadBase.
+Definition LogicalMonadEnv := Environment.F LogicalEnvironment _ LogicalMonadWriter.
+Definition LogicalMonad : Monad LogicalType := State.F LogicalState _ LogicalMonadEnv.
+Definition LogicalStateM : State LogicalState LogicalType := State.State LogicalState _ LogicalMonadEnv.
+Definition LogicalReader : Environment LogicalEnvironment _ := Environment.Environment LogicalEnvironment _ LogicalMonadWriter.
+Definition LogicalWriter : Writer LogicalMessageType _ := Writer.Writer LogicalMessageType _ (Logic.F NonLogicalType).
+Definition LogicalLogic : Logic LogicalType := State.Logic _ _ LogicalMonadEnv (Environment.Logic _ _ LogicalMonadWriter (Writer.Logic _ LogicalMessage _ LogicalMonadBase (Logic.Logic _ NonLogicalMonad))).
+
+Module NonLogical.
+
+ Definition t (a:Set) := Eval compute in NonLogicalType a.
+ Definition ref (a:Set) := Eval compute in IO.Ref a.
+
+ Definition ret {a:Set} (x:a) : t a := Eval compute in ret _ NonLogicalMonad x.
+ Extraction Implicit ret [a].
+ Definition bind {a b:Set} (x:t a) (k:a-> t b) : t b := Eval compute in bind _ NonLogicalMonad x k.
+ Extraction Implicit bind [a b].
+
+ Definition ignore {a:Set} (x:t a) : t unit := Eval compute in ignore _ NonLogicalMonad x.
+ Extraction Implicit ignore [a].
+ Definition seq {a:Set} (x:t unit) (k:t a) : t a := Eval compute in seq _ NonLogicalMonad x k.
+ Extraction Implicit seq [a].
+
+ Definition new_ref {a:Set} (x:a) : t (ref a) := Eval compute in IO.ref _ _ NonLogicalIO x.
+ Extraction Implicit new_ref [a].
+ Definition set {a:Set} (r:ref a) (x:a) : t unit := Eval compute in IO.set _ _ NonLogicalIO r x.
+ Extraction Implicit set [a].
+ Definition get {a:Set} (r:ref a) : t a := Eval compute in IO.get _ _ NonLogicalIO r.
+ Extraction Implicit get [a].
+
+ Definition raise {a:Set} (e:Exception) : t a := Eval compute in IO.raise _ _ NonLogicalIO e.
+ Extraction Implicit raise [a].
+ Definition catch {a:Set} (s:t a) (h:Exception -> t a) : t a := Eval compute in IO.catch _ _ NonLogicalIO s h.
+ Extraction Implicit catch [a].
+ Definition timeout {a:Set} n (x:t a) : t a := Eval compute in IO.timeout _ _ NonLogicalIO n x.
+ Extraction Implicit timeout [a].
+
+ (* /!\ The extracted code for [run] performs effects. /!\ *)
+ Parameter run : forall a:Set, t a -> a.
+ Extract Constant run => "fun x -> try x () with Proof_errors.Exception e -> Pervasives.raise e".
+ Extraction Implicit run [a].
+
+End NonLogical.
+
+Module Logical.
+
+ Definition t (a:Set) := Eval compute in LogicalType a.
+
+ Definition ret {a:Set} (x:a) : t a := Eval compute in ret _ LogicalMonad x.
+ Extraction Implicit ret [a].
+ Definition bind {a b:Set} (x:t a) (k:a-> t b) : t b := Eval compute in bind _ LogicalMonad x k.
+ Extraction Implicit bind [a b].
+ Definition ignore {a:Set} (x:t a) : t unit := Eval compute in ignore _ LogicalMonad x.
+ Extraction Implicit ignore [a].
+ Definition seq {a:Set} (x:t unit) (k:t a) : t a := Eval compute in seq _ LogicalMonad x k.
+ Extraction Implicit seq [a].
+
+ Definition set (s:LogicalState) : t unit := Eval compute in set _ _ LogicalStateM s.
+ Definition get : t LogicalState := Eval compute in get _ _ LogicalStateM.
+ Print Environment.lift.
+ Definition put (m:LogicalMessageType) : t unit := Eval compute in State.lift _ _ LogicalMonadEnv (Environment.lift _ _ (put _ _ LogicalWriter m)).
+ Definition current : t LogicalEnvironment := Eval compute in State.lift _ _ LogicalMonadEnv (current _ _ LogicalReader).
+
+ Definition zero {a:Set} (e:Exception) : t a := Eval compute in zero _ LogicalLogic e.
+ Extraction Implicit zero [a].
+ Definition plus {a:Set} (x:t a) (y:Exception -> t a) : t a := Eval compute in plus _ LogicalLogic x y.
+ Extraction Implicit plus [a].
+ Definition split {a:Set} (x:t a) : t ((a*(Exception -> t a))+Exception) := Eval compute in split _ LogicalLogic x.
+ Extraction Implicit split [a].
+ Definition lift {a:Set} (x:NonLogical.t a) : t a := Eval compute in
+ State.lift _ _ LogicalMonadEnv (Environment.lift _ _ (Writer.lift _ LogicalMessage _ LogicalMonadBase (Logic.lift _ NonLogicalMonad x))).
+ Extraction Implicit lift [a].
+
+ Definition run {a:Set} (x:t a) (e:LogicalEnvironment) (s:LogicalState) : NonLogical.t ((a*LogicalState)*LogicalMessageType) := Eval compute in
+ Logic.run _ NonLogicalMonad _ NonLogicalIO (Writer.run _ _ (Environment.run _ _ (State.run _ _ x s) e))
+ .
+ Extraction Implicit run [a].
+
+End Logical.
+
+
+Set Extraction Conservative Types.
+Set Extraction File Comment "
+This file has been generated by extraction of bootstrap/Monad.v.
+It shouldn't be modified directly. To regenerate it run
+coqtop -batch -impredicative-set bootstrap/Monad.v in Coq's source
+directory.
+".
+
+Extraction "proofs/proofview_gen.ml" NonLogical Logical.
diff --git a/dev/printers.mllib b/dev/printers.mllib
index c14d72def1..1410cc7a0b 100644
--- a/dev/printers.mllib
+++ b/dev/printers.mllib
@@ -157,7 +157,9 @@ Logic
Refiner
Clenv
Evar_refiner
-Monads
+Proof_errors
+Proofview_gen
+Proofview_monad
Proofview
Proof
Proof_global
diff --git a/proofs/monads.ml b/proofs/monads.ml
deleted file mode 100644
index 803715a450..0000000000
--- a/proofs/monads.ml
+++ /dev/null
@@ -1,496 +0,0 @@
-module type Type = sig
- type t
-end
-
-module type S = sig
- type +'a t
-
- val return : 'a -> 'a t
- val bind : 'a t -> ('a -> 'b t) -> 'b t
- val seq : unit t -> 'a t -> 'a t
- val ignore : 'a t -> unit t
-(* spiwack: these will suffice for now, if we would use monads more
- globally, then I would add map/join/List.map and such functions,
- plus default implementations *)
-end
-
-module type State = sig
- type s (* type of the state *)
- include S
-
- val set : s -> unit t
- val get : s t
-end
-
-module type Writer = sig
- type m (* type of the messages *)
- include S
-
- val put : m -> unit t
-end
-
-module type IO = sig
- include S
-
- type 'a ref
-
- val ref : 'a -> 'a ref t
- val (:=) : 'a ref -> 'a -> unit t
- val (!) : 'a ref -> 'a t
-
- val raise : exn -> 'a t
- val catch : 'a t -> (exn -> 'a t) -> 'a t
-
- (** In the basic IO monad, [timeout n x] acts as [x] unless it runs for more than [n]
- seconds in which case it raises [IO.Timeout]. *)
- val timeout : int -> 'a t -> 'a t
-end
-
-module IO : sig
- include IO
-
- (** To help distinguish between exceptions raised by the [IO] monad
- from the one used natively by Coq, the former are wrapped in
- [Exception]. *)
- exception Exception of exn
- (** This exception is used to signal abortion in [timeout] functions. *)
- exception Timeout
- (** runs the suspension for its effects *)
- val run : 'a t -> 'a
-end = struct
- type 'a t = unit -> 'a
-
- let run x = x ()
-
- let return x () = x
- let bind x k () = k (x ()) ()
- let seq x k () = x (); k ()
- let ignore x () = ignore (x ())
-
- type 'a ref = 'a Pervasives.ref
-
- let ref x () = Pervasives.ref x
- let (:=) r x () = Pervasives.(:=) r x
- let (!) r () = Pervasives.(!) r
-
- exception Exception of exn
- let raise e () = raise (Exception e)
- let catch s h () =
- try s ()
- with Exception e -> h e ()
-
- exception Timeout
- let timeout n t () =
- let timeout_handler _ = Pervasives.raise (Exception Timeout) in
- let psh = Sys.signal Sys.sigalrm (Sys.Signal_handle timeout_handler) in
- Pervasives.ignore (Unix.alarm n);
- let restore_timeout () =
- Pervasives.ignore (Unix.alarm 0);
- Sys.set_signal Sys.sigalrm psh
- in
- try
- let res = t () in
- restore_timeout ();
- res
- with
- | e -> restore_timeout (); Pervasives.raise e
-
- let _ = Errors.register_handler begin function
- | Timeout -> Errors.errorlabstrm "Monads.IO.timeout" (Pp.str"Timeout!")
- | Exception e -> Errors.print e
- | _ -> Pervasives.raise Errors.Unhandled
- end
-end
-
-(* State monad transformer, adapted from Haskell's StateT *)
-module State (X:Type) (T:S) : sig
- (* spiwack: it is not essential that both ['a result] and ['a t] be
- private (or either, for that matter). I just hope it will help
- catch more programming errors. *)
- type +'a result = private { result : 'a ; state : X.t }
- include State with type s = X.t and type +'a t = private X.t -> 'a result T.t
- (* a function version of the coercion from the private type ['a t].*)
- val run : 'a t -> s -> 'a result T.t
- val lift : 'a T.t -> 'a t
-end = struct
- type s = X.t
- type 'a result = { result : 'a ; state : s }
- type 'a t = s -> 'a result T.t
-
- let run x = x
- (*spiwack: convenience notation, waiting for ocaml 3.12 *)
- let (>>=) = T.bind
- let return x s = T.return { result=x ; state=s }
- let bind x k s =
- x s >>= fun { result=a ; state=s } ->
- k a s
- let ignore x s =
- x s >>= fun x' ->
- T.return { x' with result=() }
- let seq x t s =
- (x s) >>= fun x' ->
- t x'.state
- let lift x s =
- x >>= fun a ->
- T.return { result=a ; state=s }
-
- let set s _ =
- T.return { result=() ; state=s }
- let get s =
- T.return { result=s ; state=s }
-end
-
-module type Monoid = sig
- type t
-
- val zero : t
- val ( * ) : t -> t -> t
-end
-
-module Writer (M:Monoid) (T:S) : sig
- include Writer with type +'a t = private ('a*M.t) T.t and type m = M.t
-
- val lift : 'a T.t -> 'a t
- (* The coercion from private ['a t] in function form. *)
- val run : 'a t -> ('a*m) T.t
-end = struct
-
- type 'a t = ('a*M.t) T.t
- type m = M.t
-
- let run x = x
-
- (*spiwack: convenience notation, waiting for ocaml 3.12 *)
- let (>>=) = T.bind
-
- let bind x k =
- x >>= fun (a,m) ->
- k a >>= fun (r,m') ->
- T.return (r,M.( * ) m m')
-
- let seq x k =
- x >>= fun ((),m) ->
- k >>= fun (r,m') ->
- T.return (r,M.( * ) m m')
-
- let return x =
- T.return (x,M.zero)
-
- let ignore x =
- x >>= fun (_,m) ->
- T.return ((),m)
-
- let lift x =
- x >>= fun r ->
- T.return (r,M.zero)
-
- let put m =
- T.return ((),m)
-end
-
-(* Double-continuation backtracking monads are reasonable folklore for
- "search" implementations (including Tac interactive prover's
- tactics). Yet it's quite hard to wrap your head around these. I
- recommand reading a few times the "Backtracking, Interleaving, and
- Terminating Monad Transformers" paper by O. Kiselyov, C. Chen,
- D. Fridman. The peculiar shape of the monadic type is reminiscent
- of that of the continuation monad transformer.
-
- The paper also contains the rational for the [split] abstraction.
-
- An explanation of how to derive such a monad from mathematical
- principles can be found in "Kan Extensions for Program
- Optimisation" by Ralf Hinze.
-
- One way to think of the [Logic] functor is to imagine ['a
- Logic(X).t] to represent list of ['a] with an exception at the
- bottom (leaving the monad-transforming issues aside, as they don't
- really work well with lists). Each of the element is a valid
- result, sequentialising with a [f:'a -> 'b t] is done by applying
- [f] to each element and then flatten the list, [plus] is
- concatenation, and [split] is pattern-matching. *)
-(* spiwack: I added the primitives from [IO] directly in the [Logic]
- signature for convenience. It doesn't really make sense, strictly
- speaking, as they are somewhat deconnected from the semantics of
- [Logic], but without an appropriate language for composition (some
- kind of mixins?) I would be going nowhere with a gazillion
- functors. *)
-module type Logic = sig
- include IO
-
- (* [zero] is usually argument free, but Coq likes to explain errors,
- hence error messages should be carried around. *)
- val zero : exn -> 'a t
- val plus : 'a t -> (exn -> 'a t) -> 'a t
-(** Writing (+) for plus and (>>=) for bind, we shall require that
-
- x+(y+z) = (x+y)+z
-
- zero+x = x
-
- x+zero = x
-
- (x+y)>>=k = (x>>=k)+(y>>=k) *)
-
- (** [split x] runs [x] until it either fails with [zero e] or finds
- a result [a]. In the former case it returns [Inr e], otherwise
- it returns [Inl (a,y)] where [y] can be run to get more results
- from [x]. It is a variant of prolog's cut. *)
- val split : 'a t -> ('a * (exn -> 'a t) , exn ) Util.union t
-end
-(* The [T] argument represents the "global" effect: it is not
- backtracked when backtracking occurs at a [plus]. *)
-(* spiwack: hence, [T] will not be instanciated with a state monad
- representing the proofs, we will use a surrounding state transformer
- to that effect. In fact at the time I'm writing this comment, I have
- no immediate use for [T]. We might, however, consider instantiating it
- with a "writer" monad around [Pp] to implement [idtac "msg"] for
- instance. *)
-module Logic (T:IO) : sig
- include Logic
-
- (** [run x] raises [e] if [x] is [zero e]. *)
- val run : 'a t -> 'a T.t
-
- val lift : 'a T.t -> 'a t
-end = struct
-(* spiwack: the implementation is an adaptation of the aforementionned
- "Backtracking, Interleaving, and Terminating Monad Transformers"
- paper *)
- (* spiwack: [fk] stands for failure continuation, and [sk] for success
- continuation. *)
- type +'r fk = exn -> 'r
- type (-'a,'r) sk = 'a -> 'r fk -> 'r
- type 'a t = { go : 'r. ('a,'r T.t) sk -> 'r T.t fk -> 'r T.t }
-
- let return x = { go = fun sk fk ->
- sk x fk
- }
- let bind x k = { go = fun sk fk ->
- x.go (fun a fk -> (k a).go sk fk) fk
- }
- let ignore x = { go = fun sk fk ->
- x.go (fun _ fk -> sk () fk) fk
- }
- let seq x t = { go = fun sk fk ->
- x.go (fun () fk -> t.go sk fk) fk
- }
-
- let zero e = { go = fun _ fk -> fk e }
-
- let plus x y = { go = fun sk fk ->
- x.go sk (fun e -> (y e).go sk fk)
- }
-
- let lift x = { go = fun sk fk ->
- T.bind x (fun a -> sk a fk)
- }
-
- let run x =
- let sk a _ = T.return a in
- let fk e = raise e in
- x.go sk fk
-
- (* For [reflect] and [split] see the "Backtracking, Interleaving,
- and Terminating Monad Transformers" paper *)
- let reflect : ('a*(exn -> 'a t) , exn) Util.union -> 'a t = function
- | Util.Inr e -> zero e
- | Util.Inl (a,x) -> plus (return a) x
-
- let lower x =
- let fk e = T.return (Util.Inr e) in
- let sk a fk = T.return (Util.Inl (a,fun e -> bind (lift (fk e)) reflect)) in
- x.go sk fk
-
- let split x =
- lift (lower x)
-
- (*** IO ***)
-
- type 'a ref = 'a T.ref
- let ref x = lift (T.ref x)
- let (:=) r x = lift (T.(:=) r x)
- let (!) r = lift (T.(!) r)
-
- let raise e = lift (T.raise e)
- let catch t h =
- let h' e = lower (h e) in
- bind (lift (T.catch (lower t) h')) reflect
-
- (** [timeout n x] can have several success. It succeeds as long as,
- individually, each of the past successes run in less than [n]
- seconds.
- In case of timeout if fails with [zero Timeout]. *)
- let rec timeout n x =
- (* spiwack: adds a [T.return] in front of [x] in order to force
- [lower] to go into [T] before running [x]. The problem is that
- in a continuation-passing monad transformer, the monadic
- operations don't make use of the underlying ones. Hence, when
- going back to a lower monad, much computation can be done
- before returning (and running the lower monad). It is
- undesirable for timeout, obviously. *)
- let x = seq (lift (T.return ())) x in
- let x' =
- (* spiwack: this could be a [T.map] if provided *)
- T.bind (lower x) begin function
- | Util.Inr _ as e -> T.return e
- | Util.Inl (a,h) -> T.return (Util.Inl (a, fun e -> timeout n (h e)))
- end
- in
- (* spiwack: we report timeouts as resumable failures. *)
- bind (catch (lift (T.timeout n x')) begin function
- | IO.Timeout -> zero IO.Timeout
- | e -> raise e
- end) reflect
-end
-
-
-(* [State(X)(T:Logic)] can be lifted to [Logic] by backtracking on state on [plus].*)
-module StateLogic(X:Type)(T:Logic) : sig
- (* spiwack: some duplication from interfaces as we need ocaml 3.12
- to substitute inside signatures. *)
- type s = X.t
- type +'a result = private { result : 'a ; state : s }
- include Logic with type +'a t = private X.t -> 'a result T.t
-
- val set : s -> unit t
- val get : s t
-
- val lift : 'a T.t -> 'a t
- val run : 'a t -> s -> 'a result T.t
-end = struct
-
- module S = State(X)(T)
- include S
-
- let zero e = lift (T.zero e)
- let plus x y =
- (* spiwack: convenience notation, waiting for ocaml 3.12 *)
- let (>>=) = bind in
- let (>>) = seq in
- get >>= fun initial ->
- lift begin
- (T.plus (run x initial) (fun e -> run (y e) initial))
- end >>= fun { result = a ; state = final } ->
- set final >>
- return a
- (* spiwack: the definition of [plus] is essentially [plus x y = fun s
- -> T.plus (run x s) (run y s)]. But the [private] annotation
- prevents us from writing that. Maybe I should remove [private]
- around [+'a t] (it would be unnecessary to remove that of ['a
- result]) after all. I'll leave it like that for now. *)
-
- let split x =
- (* spiwack: convenience notation, waiting for ocaml 3.12 *)
- let (>>=) = bind in
- let (>>) = seq in
- get >>= fun initial ->
- lift (T.split (run x initial)) >>= function
- | Util.Inr _ as e -> return e
- | Util.Inl (a,y) ->
- let y' e =
- lift (y e) >>= fun b ->
- set b.state >>
- return b.result
- in
- set a.state >>
- return (Util.Inl(a.result,y'))
-
-
- (*** IO ***)
-
- type 'a ref = 'a T.ref
- let ref x = lift (T.ref x)
- let (:=) r x = lift (T.(:=) r x)
- let (!) r = lift (T.(!) r)
-
- let raise e = lift (T.raise e)
- let catch t h =
- (* spiwack: convenience notation, waiting for ocaml 3.12 *)
- let (>>=) = bind in
- let (>>) = seq in
- get >>= fun initial ->
- let h' e = run (h e) initial in
- lift (T.catch (run t initial) h') >>= fun a ->
- set a.state >>
- return a.result
-
- exception Timeout
- let timeout n t =
- (* spiwack: convenience notation, waiting for ocaml 3.12 *)
- let (>>=) = bind in
- let (>>) = seq in
- get >>= fun initial ->
- lift (T.timeout n (run t initial)) >>= fun a ->
- set a.state >>
- return a.result
-end
-
-(* [Writer(M)(T:Logic)] can be lifted to [Logic] by backtracking on state on [plus].*)
-module WriterLogic(M:Monoid)(T:Logic) : sig
- (* spiwack: some duplication from interfaces as we need ocaml 3.12
- to substitute inside signatures. *)
- type m = M.t
- include Logic with type +'a t = private ('a*m) T.t
-
- val put : m -> unit t
-
- val lift : 'a T.t -> 'a t
- val run : 'a t -> ('a*m) T.t
-end = struct
- module W = Writer(M)(T)
- include W
-
- let zero e = lift (T.zero e)
- let plus x y =
- (* spiwack: convenience notation, waiting for ocaml 3.12 *)
- let (>>=) = bind in
- let (>>) = seq in
- lift begin
- (T.plus (run x) (fun e -> run (y e)))
- end >>= fun (r,m) ->
- put m >>
- return r
-
- let split x =
- (* spiwack: convenience notation, waiting for ocaml 3.12 *)
- let (>>=) = bind in
- let (>>) = seq in
- lift (T.split (run x)) >>= function
- | Util.Inr _ as e -> return e
- | Util.Inl ((a,m),y) ->
- let y' e =
- lift (y e) >>= fun (b,m) ->
- put m >>
- return b
- in
- put m >>
- return (Util.Inl(a,y'))
-
-
- (*** IO ***)
-
- type 'a ref = 'a T.ref
- let ref x = lift (T.ref x)
- let (:=) r x = lift (T.(:=) r x)
- let (!) r = lift (T.(!) r)
-
- let raise e = lift (T.raise e)
- let catch t h =
- (* spiwack: convenience notation, waiting for ocaml 3.12 *)
- let (>>=) = bind in
- let (>>) = seq in
- let h' e = run (h e) in
- lift (T.catch (run t) h') >>= fun (a,m) ->
- put m >>
- return a
-
- exception Timeout
- let timeout n t =
- (* spiwack: convenience notation, waiting for ocaml 3.12 *)
- let (>>=) = bind in
- let (>>) = seq in
- lift (T.timeout n (run t)) >>= fun (a,m) ->
- put m >>
- return a
-end
diff --git a/proofs/proof_errors.ml b/proofs/proof_errors.ml
new file mode 100644
index 0000000000..e543b0c8fd
--- /dev/null
+++ b/proofs/proof_errors.ml
@@ -0,0 +1,12 @@
+exception Exception of exn
+exception Timeout
+exception TacticFailure of exn
+
+let _ = Errors.register_handler begin function
+ | Timeout -> Errors.errorlabstrm "Some timeout function" (Pp.str"Timeout!")
+ | Exception e -> Errors.print e
+ | TacticFailure e -> Errors.print e
+ | _ -> Pervasives.raise Errors.Unhandled
+end
+
+
diff --git a/proofs/proof_errors.mli b/proofs/proof_errors.mli
new file mode 100644
index 0000000000..dd21d539c9
--- /dev/null
+++ b/proofs/proof_errors.mli
@@ -0,0 +1,18 @@
+(** This small files declares the exceptions needed by Proofview_gen,
+ as Coq's extraction cannot produce exception declarations. *)
+
+(** To help distinguish between exceptions raised by the IO monad from
+ the one used natively by Coq, the former are wrapped in
+ [Exception]. It is only used internally so that [catch] blocks of
+ the IO monad would only catch exceptions raised by the [raise]
+ function of the IO monad, and not for instance, by system
+ interrupts. Also used in [Proofview] to avoid capturing exception
+ from the IO monad ([Proofview] catches errors in its compatibility
+ layer, and when lifting goal-level expressions). *)
+exception Exception of exn
+(** This exception is used to signal abortion in [timeout] functions. *)
+exception Timeout
+(** This exception is used by the tactics to signal failure by lack of
+ successes, rather than some other exceptions (like system
+ interrupts). *)
+exception TacticFailure of exn
diff --git a/proofs/proofs.mllib b/proofs/proofs.mllib
index 19f289316f..4a7efb029c 100644
--- a/proofs/proofs.mllib
+++ b/proofs/proofs.mllib
@@ -1,7 +1,9 @@
Goal
Evar_refiner
-Monads
Proof_type
+Proof_errors
+Proofview_gen
+Proofview_monad
Proofview
Proof
Proof_global
diff --git a/proofs/proofview.ml b/proofs/proofview.ml
index eed792fd7f..9496b51ea8 100644
--- a/proofs/proofview.ml
+++ b/proofs/proofview.ml
@@ -23,11 +23,8 @@
open Util
(* Type of proofviews. *)
-type proofview = {
- initial : (Term.constr * Term.types) list;
- solution : Evd.evar_map;
- comb : Goal.goal list;
- }
+type proofview = Proofview_monad.proofview
+open Proofview_monad
let proofview p =
p.comb , p.solution
@@ -188,79 +185,68 @@ let unfocus c sp =
- access the environment,
- access and change the current [proofview]
- backtrack on previous changes of the proofview *)
-(* spiwack: it seems lighter, for now, to deal with the environment here rather than in [Monads]. *)
-
-module ProofState = struct
- type t = proofview
-end
-module MessageType = struct
- type t = bool (* [false] if an unsafe tactic has been used. *)
-
- let zero = true
- let ( * ) s1 s2 = s1 && s2
-end
-module Backtrack = Monads.Logic(Monads.IO)
-module Message = Monads.WriterLogic(MessageType)(Backtrack)
-module Proof = Monads.StateLogic(ProofState)(Message)
-
-type +'a tactic = Environ.env -> 'a Proof.t
+module Proof = Proofview_monad.Logical
+type +'a tactic = 'a Proof.t
(* Applies a tactic to the current proofview. *)
let apply env t sp =
- let (next,status) = Monads.IO.run (Backtrack.run (Message.run (Proof.run (t env) sp))) in
- next.Proof.result , next.Proof.state , status
+ let (((next_r,next_state),status)) = Proofview_monad.NonLogical.run (Proof.run t env sp) in
+ next_r , next_state , status
(*** tacticals ***)
+let rec catchable_exception = function
+ | Proof_errors.Exception _ -> false
+ | e -> Errors.noncritical e
+
+
(* Unit of the tactic monad *)
-let tclUNIT a _ = Proof.return a
+let tclUNIT a = (Proof.ret a:'a Proof.t)
(* Bind operation of the tactic monad *)
-let tclBIND t k env =
- Proof.bind (t env) (fun a -> k a env)
+let tclBIND = Proof.bind
(* Interpretes the ";" (semicolon) of Ltac.
As a monadic operation, it's a specialized "bind"
on unit-returning tactic (meaning "there is no value to bind") *)
-let tclTHEN t1 t2 env =
- Proof.seq (t1 env) (t2 env)
+let tclTHEN = Proof.seq
(* [tclIGNORE t] has the same operational content as [t],
but drops the value at the end. *)
-let tclIGNORE tac env = Proof.ignore (tac env)
+let tclIGNORE = Proof.ignore
(* [tclOR t1 t2 = 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]. No interleaving at this point. *)
-let tclOR t1 t2 env =
- Proof.plus (t1 env) (fun e -> t2 e env)
+let tclOR t1 t2 =
+ Proof.plus t1 t2
(* [tclZERO e] always fails with error message [e]*)
-let tclZERO e _ = Proof.zero e
+let tclZERO = Proof.zero
(* [tclORELSE t1 t2] behaves like [t1] if [t1] succeeds at least once
or [t2] if [t1] fails. *)
-let tclORELSE t1 t2 env =
+let tclORELSE t1 t2 =
(* spiwack: convenience notations, waiting for ocaml 3.12 *)
let (>>=) = Proof.bind in
- Proof.split (t1 env) >>= function
- | Util.Inr e -> t2 e env
- | Util.Inl (a,t1') -> Proof.plus (Proof.return a) t1'
+ Proof.split t1 >>= function
+ | Util.Inr e -> t2 e
+ | Util.Inl (a,t1') -> Proof.plus (Proof.ret 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 env =
+let tclIFCATCH a s f =
(* spiwack: convenience notations, waiting for ocaml 3.12 *)
let (>>=) = Proof.bind in
- Proof.split (a env) >>= function
- | Util.Inr e -> f e env
- | Util.Inl (x,a') -> Proof.plus (s x env) (fun e -> (a' e) >>= fun x' -> (s x' env))
+ Proof.split a >>= function
+ | Util.Inr e -> f e
+ | Util.Inl (x,a') -> Proof.plus (s x) (fun e -> (a' e) >>= fun x' -> (s x'))
(* Focuses a tactic at a range of subgoals, found by their indices. *)
(* arnaud: bug if 0 goals ! *)
-let tclFOCUS i j t env =
+let tclFOCUS i j t =
(* spiwack: convenience notations, waiting for ocaml 3.12 *)
let (>>=) = Proof.bind in
let (>>) = Proof.seq in
@@ -268,14 +254,14 @@ let tclFOCUS i j t env =
try
let (focused,context) = focus i j initial in
Proof.set focused >>
- t (env) >>= fun result ->
+ t >>= fun result ->
Proof.get >>= fun next ->
Proof.set (unfocus context next) >>
- Proof.return result
+ Proof.ret result
with e ->
(* spiwack: a priori the only possible exceptions are that of focus,
of course I haven't made them algebraic yet. *)
- tclZERO e env
+ tclZERO e
(* Dispatch tacticals are used to apply a different tactic to each goal under
consideration. They come in two flavours:
@@ -299,27 +285,27 @@ end
both lists are being concatenated.
[join] and [null] need be some sort of comutative monoid. *)
-let rec tclDISPATCHGEN null join tacs env =
+let rec tclDISPATCHGEN null join tacs =
(* spiwack: convenience notations, waiting for ocaml 3.12 *)
let (>>=) = Proof.bind in
let (>>) = Proof.seq in
Proof.get >>= fun initial ->
match tacs,initial.comb with
- | [], [] -> tclUNIT null env
+ | [], [] -> tclUNIT null
| t::tacs , first::goals ->
begin match Goal.advance initial.solution first with
- | None -> Proof.return null (* If [first] has been solved by side effect: do nothing. *)
+ | None -> Proof.ret null (* If [first] has been solved by side effect: do nothing. *)
| Some first ->
Proof.set {initial with comb=[first]} >>
- t env
+ t
end >>= fun y ->
Proof.get >>= fun step ->
Proof.set {step with comb=goals} >>
- tclDISPATCHGEN null join tacs env >>= fun x ->
+ tclDISPATCHGEN null join tacs >>= fun x ->
Proof.get >>= fun step' ->
Proof.set {step' with comb=step.comb@step'.comb} >>
- Proof.return (join y x)
- | _ , _ -> tclZERO SizeMismatch env
+ Proof.ret (join y x)
+ | _ , _ -> tclZERO SizeMismatch
let unitK () () = ()
let tclDISPATCH = tclDISPATCHGEN () unitK
@@ -343,12 +329,12 @@ let extend_to_list =
let ne = List.length endxs in
let n = List.length l in
startxs@(copy (n-ne-ns) rx endxs)
-let tclEXTEND tacs1 rtac tacs2 env =
+let tclEXTEND tacs1 rtac tacs2 =
(* spiwack: convenience notations, waiting for ocaml 3.12 *)
let (>>=) = Proof.bind in
Proof.get >>= fun step ->
let tacs = extend_to_list tacs1 rtac tacs2 step.comb in
- tclDISPATCH tacs env
+ tclDISPATCH tacs
(* No backtracking can happen here, hence, as opposed to the dispatch tacticals,
@@ -367,44 +353,79 @@ let sensitive_on_proofview s env step =
{ step with
solution = new_defs;
comb = List.flatten combed_subgoals; }
- let tclSENSITIVE s env =
+let tclSENSITIVE s =
(* spiwack: convenience notations, waiting for ocaml 3.12 *)
let (>>=) = Proof.bind in
+ Proof.current >>= fun env ->
Proof.get >>= fun step ->
try
let next = sensitive_on_proofview s env step in
Proof.set next
- with e when Errors.noncritical e ->
- tclZERO e env
+ with e when catchable_exception e ->
+ tclZERO e
-let tclPROGRESS t env =
+let tclPROGRESS t =
(* spiwack: convenience notations, waiting for ocaml 3.12 *)
let (>>=) = Proof.bind in
Proof.get >>= fun initial ->
- t env >>= fun res ->
+ t >>= fun res ->
Proof.get >>= fun final ->
let test =
Evd.progress_evar_map initial.solution final.solution &&
not (Util.List.for_all2eq (fun i f -> Goal.equal initial.solution i final.solution f) initial.comb final.comb)
in
if test then
- tclUNIT res env
+ tclUNIT res
else
- tclZERO (Errors.UserError ("Proofview.tclPROGRESS" , Pp.str"Failed to progress.")) env
+ tclZERO (Errors.UserError ("Proofview.tclPROGRESS" , Pp.str"Failed to progress."))
-let tclEVARMAP _ =
+let tclEVARMAP =
(* spiwack: convenience notations, waiting for ocaml 3.12 *)
let (>>=) = Proof.bind in
Proof.get >>= fun initial ->
- Proof.return (initial.solution)
+ Proof.ret (initial.solution)
-let tclENV env =
- Proof.return env
+let tclENV = Proof.current
-let tclTIMEOUT n t env = Proof.timeout n (t env)
+exception Timeout
+let _ = Errors.register_handler begin function
+ | Timeout -> Errors.errorlabstrm "Proofview.tclTIMEOUT" (Pp.str"Tactic timeout!")
+ | _ -> Pervasives.raise Errors.Unhandled
+end
-let mark_as_unsafe env =
- Proof.lift (Message.put false)
+let tclTIMEOUT n t =
+ (* spiwack: convenience notations, waiting for ocaml 3.12 *)
+ let (>>=) = Proof.bind in
+ let (>>) = Proof.seq 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 (Proofview_monad.NonLogical.ret ()) >> t in
+ Proof.current >>= fun env ->
+ Proof.get >>= fun initial ->
+ Proof.lift begin
+ Proofview_monad.NonLogical.catch
+ begin
+ Proofview_monad.NonLogical.bind
+ (Proofview_monad.NonLogical.timeout n (Proof.run t env initial))
+ (fun r -> Proofview_monad.NonLogical.ret (Util.Inl r))
+ end
+ begin function
+ | Proof_errors.Timeout -> Proofview_monad.NonLogical.ret (Util.Inr Timeout)
+ | Proof_errors.TacticFailure e -> Proofview_monad.NonLogical.ret (Util.Inr e)
+ | e -> Proofview_monad.NonLogical.raise e
+ end
+ end >>= function
+ | Util.Inl ((res,s),m) ->
+ Proof.set s >>
+ Proof.put m >>
+ Proof.ret res
+ | Util.Inr e -> tclZERO e
+
+let mark_as_unsafe =
+ Proof.put false
(*** Commands ***)
@@ -430,7 +451,7 @@ module Notations = struct
end >= fun l' ->
tclUNIT (List.flatten l')
let (<*>) = tclTHEN
- let (<+>) t1 t2 = tclOR t2 (fun _ -> t2)
+ let (<+>) t1 t2 = tclOR t1 (fun _ -> t2)
end
open Notations
@@ -446,7 +467,7 @@ let rec list_map f = function
module V82 = struct
type tac = Goal.goal Evd.sigma -> Goal.goal list Evd.sigma
- let tactic tac env =
+ 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 *)
@@ -467,8 +488,8 @@ module V82 = struct
let (goalss,evd) = Goal.list_map tac initgoals initevd in
let sgs = List.flatten goalss in
Proof.set { ps with solution=evd ; comb=sgs; }
- with e when Errors.noncritical e ->
- tclZERO e env
+ with e when catchable_exception e ->
+ tclZERO e
let has_unresolved_evar pv =
Evd.has_undefined pv.solution
@@ -515,14 +536,16 @@ module V82 = struct
solution = Evar_refiner.instantiate_pf_com evk com pv.solution }
let of_tactic t gls =
- let init = { solution = gls.Evd.sigma ; comb = [gls.Evd.it] ; initial = [] } in
- let (_,final,_) = apply (Goal.V82.env gls.Evd.sigma gls.Evd.it) t init in
- { Evd.sigma = final.solution ; it = final.comb }
+ try
+ let init = { solution = gls.Evd.sigma ; comb = [gls.Evd.it] ; initial = [] } in
+ let (_,final,_) = apply (Goal.V82.env gls.Evd.sigma gls.Evd.it) t init in
+ { Evd.sigma = final.solution ; it = final.comb }
+ with Proof_errors.TacticFailure e -> raise e
- let put_status b _env =
- Proof.lift (Message.put b)
+ let put_status b =
+ Proof.put b
- let catchable_exception = Errors.noncritical
+ let catchable_exception = catchable_exception
end
@@ -530,10 +553,11 @@ module Goal = struct
type 'a u = 'a list
- let lift s env =
+ let lift s =
(* spiwack: convenience notations, waiting for ocaml 3.12 *)
let (>>=) = Proof.bind in
let (>>) = Proof.seq in
+ Proof.current >>= fun env ->
Proof.get >>= fun step ->
try
let (res,sigma) =
@@ -542,22 +566,12 @@ module Goal = struct
end step.comb step.solution
in
Proof.set { step with solution=sigma } >>
- Proof.return res
- with e when Errors.noncritical e ->
- tclZERO e env
+ Proof.ret res
+ with e when catchable_exception e ->
+ tclZERO e
let return x = lift (Goal.return x)
let concl = lift Goal.concl
let hyps = lift Goal.hyps
let env = lift Goal.env
end
-
-
-
-
-
-
-
-
-
-
diff --git a/proofs/proofview.mli b/proofs/proofview.mli
index a2a5746933..136a44332e 100644
--- a/proofs/proofview.mli
+++ b/proofs/proofview.mli
@@ -194,10 +194,9 @@ val tclEVARMAP : Evd.evar_map tactic
environment is returned by {!Proofview.Goal.env}. *)
val tclENV : Environ.env tactic
-(** [tclTIMEOUT n t] can have several success. It succeeds as long as,
- individually, each of the past successes run in less than [n]
- seconds.
- In case of timeout if fails with [tclZERO Timeout]. *)
+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
(** [mark_as_unsafe] signals that the current tactic is unsafe. *)
diff --git a/proofs/proofview_gen.ml b/proofs/proofview_gen.ml
new file mode 100644
index 0000000000..577aa2ddb0
--- /dev/null
+++ b/proofs/proofview_gen.ml
@@ -0,0 +1,377 @@
+(* This file has been generated by extraction
+ of bootstrap/Monad.v. It shouldn't be
+ modified directly. To regenerate it run
+ coqtop -batch -impredicative-set
+ bootstrap/Monad.v in Coq's source
+ directory. *)
+
+type __ = Obj.t
+let __ = let rec f _ = Obj.repr f in Obj.repr f
+
+module IOBase =
+ struct
+ type 'a coq_T = unit -> 'a
+
+ type 'a coq_Ref = 'a Pervasives.ref
+
+ (** val ret : 'a1 -> 'a1 coq_T **)
+
+ let ret = fun a () -> a
+
+ (** val bind :
+ 'a1 coq_T -> ('a1 -> 'a2 coq_T) -> 'a2
+ coq_T **)
+
+ let bind = fun a k () -> k (a ()) ()
+
+ (** val ignore :
+ 'a1 coq_T -> unit coq_T **)
+
+ let ignore = fun a () -> ignore (a ())
+
+ (** val seq :
+ unit coq_T -> 'a1 coq_T -> 'a1 coq_T **)
+
+ let seq = fun a k () -> a (); k ()
+
+ (** val ref : 'a1 -> 'a1 coq_Ref coq_T **)
+
+ let ref = fun a () -> Pervasives.ref a
+
+ (** val set :
+ 'a1 coq_Ref -> 'a1 -> unit coq_T **)
+
+ let set = fun r a () -> Pervasives.(:=) r a
+
+ (** val get : 'a1 coq_Ref -> 'a1 coq_T **)
+
+ let get = fun r () -> Pervasives.(!) r
+
+ (** val raise : exn -> 'a1 coq_T **)
+
+ let raise = fun e () -> raise (Proof_errors.Exception e)
+
+ (** val catch :
+ 'a1 coq_T -> (exn -> 'a1 coq_T) -> 'a1
+ coq_T **)
+
+ let catch = fun s h () -> try s () with Proof_errors.Exception e -> h e ()
+
+ type coq_Int = int
+
+ (** val timeout :
+ coq_Int -> 'a1 coq_T -> 'a1 coq_T **)
+
+ let timeout = fun n t () ->
+ let timeout_handler _ = Pervasives.raise (Proof_errors.Exception Proof_errors.Timeout) in
+ let psh = Sys.signal Sys.sigalrm (Sys.Signal_handle timeout_handler) in
+ Pervasives.ignore (Unix.alarm n);
+ let restore_timeout () =
+ Pervasives.ignore (Unix.alarm 0);
+ Sys.set_signal Sys.sigalrm psh
+ in
+ try
+ let res = t () in
+ restore_timeout ();
+ res
+ with
+ | e -> restore_timeout (); Pervasives.raise e
+
+ end
+
+type proofview = { initial : (Term.constr*Term.types)
+ list;
+ solution : Evd.evar_map;
+ comb : Goal.goal list }
+
+type logicalState = proofview
+
+type logicalMessageType = bool
+
+type logicalEnvironment = Environ.env
+
+module NonLogical =
+ struct
+ type 'a t = 'a IOBase.coq_T
+
+ type 'a ref = 'a IOBase.coq_Ref
+
+ (** val ret : 'a1 -> 'a1 t **)
+
+ let ret x =
+ IOBase.ret x
+
+ (** val bind :
+ 'a1 t -> ('a1 -> 'a2 t) -> 'a2 t **)
+
+ let bind x k =
+ IOBase.bind x k
+
+ (** val ignore : 'a1 t -> unit t **)
+
+ let ignore x =
+ IOBase.ignore x
+
+ (** val seq : unit t -> 'a1 t -> 'a1 t **)
+
+ let seq x k =
+ IOBase.seq x k
+
+ (** val new_ref : 'a1 -> 'a1 ref t **)
+
+ let new_ref x =
+ IOBase.ref x
+
+ (** val set : 'a1 ref -> 'a1 -> unit t **)
+
+ let set r x =
+ IOBase.set r x
+
+ (** val get : 'a1 ref -> 'a1 t **)
+
+ let get r =
+ IOBase.get r
+
+ (** val raise : exn -> 'a1 t **)
+
+ let raise e =
+ IOBase.raise e
+
+ (** val catch :
+ 'a1 t -> (exn -> 'a1 t) -> 'a1 t **)
+
+ let catch s h =
+ IOBase.catch s h
+
+ (** val timeout :
+ IOBase.coq_Int -> 'a1 t -> 'a1 t **)
+
+ let timeout n x =
+ IOBase.timeout n x
+
+ (** val run : 'a1 t -> 'a1 **)
+
+ let run = fun x -> try x () with Proof_errors.Exception e -> Pervasives.raise e
+ end
+
+module Logical =
+ struct
+ type 'a t =
+ proofview -> Environ.env -> __ ->
+ ((('a*proofview)*bool) -> (exn -> __
+ IOBase.coq_T) -> __ IOBase.coq_T) -> (exn
+ -> __ IOBase.coq_T) -> __ IOBase.coq_T
+
+ (** val ret :
+ 'a1 -> proofview -> Environ.env -> __
+ -> ((('a1*proofview)*bool) -> (exn ->
+ 'a2 IOBase.coq_T) -> 'a2 IOBase.coq_T)
+ -> (exn -> 'a2 IOBase.coq_T) -> 'a2
+ IOBase.coq_T **)
+
+ let ret x s e r sk fk =
+ sk ((x,s),true) fk
+
+ (** val bind :
+ 'a1 t -> ('a1 -> 'a2 t) -> proofview ->
+ Environ.env -> __ ->
+ ((('a2*proofview)*bool) -> (exn -> 'a3
+ IOBase.coq_T) -> 'a3 IOBase.coq_T) ->
+ (exn -> 'a3 IOBase.coq_T) -> 'a3
+ IOBase.coq_T **)
+
+ let bind x k s e r sk fk =
+ Obj.magic x s e __ (fun a fk0 ->
+ let x0,c = a in
+ let x1,s0 = x0 in
+ Obj.magic k x1 s0 e __ (fun a0 fk1 ->
+ let y,c' = a0 in
+ sk (y,(if c then c' else false)) fk1)
+ fk0) fk
+
+ (** val ignore :
+ 'a1 t -> proofview -> Environ.env -> __
+ -> (((unit*proofview)*bool) -> (exn ->
+ 'a2 IOBase.coq_T) -> 'a2 IOBase.coq_T)
+ -> (exn -> 'a2 IOBase.coq_T) -> 'a2
+ IOBase.coq_T **)
+
+ let ignore x s e r sk fk =
+ Obj.magic x s e __ (fun a fk0 ->
+ let x0,c = a in
+ let sk0 = fun a0 fk1 ->
+ let y,c' = a0 in
+ sk (y,(if c then c' else false)) fk1
+ in
+ let a0,s0 = x0 in
+ sk0 (((),s0),true) fk0) fk
+
+ (** val seq :
+ unit t -> 'a1 t -> proofview ->
+ Environ.env -> __ ->
+ ((('a1*proofview)*bool) -> (exn -> 'a2
+ IOBase.coq_T) -> 'a2 IOBase.coq_T) ->
+ (exn -> 'a2 IOBase.coq_T) -> 'a2
+ IOBase.coq_T **)
+
+ let seq x k s e r sk fk =
+ Obj.magic x s e __ (fun a fk0 ->
+ let x0,c = a in
+ let u,s0 = x0 in
+ Obj.magic k s0 e __ (fun a0 fk1 ->
+ let y,c' = a0 in
+ sk (y,(if c then c' else false)) fk1)
+ fk0) fk
+
+ (** val set :
+ logicalState -> proofview ->
+ Environ.env -> __ ->
+ (((unit*proofview)*bool) -> (exn -> 'a1
+ IOBase.coq_T) -> 'a1 IOBase.coq_T) ->
+ (exn -> 'a1 IOBase.coq_T) -> 'a1
+ IOBase.coq_T **)
+
+ let set s s0 e r sk fk =
+ sk (((),s),true) fk
+
+ (** val get :
+ proofview -> Environ.env -> __ ->
+ (((logicalState*proofview)*bool) ->
+ (exn -> 'a1 IOBase.coq_T) -> 'a1
+ IOBase.coq_T) -> (exn -> 'a1
+ IOBase.coq_T) -> 'a1 IOBase.coq_T **)
+
+ let get s e r sk fk =
+ sk ((s,s),true) fk
+
+ (** val put :
+ logicalMessageType -> proofview ->
+ Environ.env -> __ ->
+ (((unit*proofview)*bool) -> (exn -> 'a1
+ IOBase.coq_T) -> 'a1 IOBase.coq_T) ->
+ (exn -> 'a1 IOBase.coq_T) -> 'a1
+ IOBase.coq_T **)
+
+ let put m s e r sk fk =
+ sk (((),s),m) fk
+
+ (** val current :
+ proofview -> Environ.env -> __ ->
+ (((logicalEnvironment*proofview)*bool)
+ -> (exn -> 'a1 IOBase.coq_T) -> 'a1
+ IOBase.coq_T) -> (exn -> 'a1
+ IOBase.coq_T) -> 'a1 IOBase.coq_T **)
+
+ let current s e r sk fk =
+ sk ((e,s),true) fk
+
+ (** val zero :
+ exn -> proofview -> Environ.env -> __
+ -> ((('a1*proofview)*bool) -> (exn ->
+ 'a2 IOBase.coq_T) -> 'a2 IOBase.coq_T)
+ -> (exn -> 'a2 IOBase.coq_T) -> 'a2
+ IOBase.coq_T **)
+
+ let zero e s e0 r sk fk =
+ fk e
+
+ (** val plus :
+ 'a1 t -> (exn -> 'a1 t) -> proofview ->
+ Environ.env -> __ ->
+ ((('a1*proofview)*bool) -> (exn -> 'a2
+ IOBase.coq_T) -> 'a2 IOBase.coq_T) ->
+ (exn -> 'a2 IOBase.coq_T) -> 'a2
+ IOBase.coq_T **)
+
+ let plus x y s env r sk fk =
+ Obj.magic x s env __ sk (fun e ->
+ Obj.magic y e s env __ sk fk)
+
+ (** val split :
+ 'a1 t -> proofview -> Environ.env -> __
+ -> (((('a1*(exn -> 'a1 t), exn)
+ Util.union*proofview)*bool) -> (exn ->
+ 'a2 IOBase.coq_T) -> 'a2 IOBase.coq_T)
+ -> (exn -> 'a2 IOBase.coq_T) -> 'a2
+ IOBase.coq_T **)
+
+ let split x s e r sk fk =
+ IOBase.bind
+ (Obj.magic x s e __ (fun a fk0 ->
+ IOBase.ret (Util.Inl
+ (a,(fun e0 _ sk0 fk1 ->
+ IOBase.bind (fk0 e0) (fun x0 ->
+ match x0 with
+ | Util.Inl p ->
+ let a0,x1 = p in
+ sk0 a0 (fun e1 ->
+ x1 e1 __ sk0 fk1)
+ | Util.Inr e1 -> fk1 e1)))))
+ (fun e0 -> IOBase.ret (Util.Inr e0)))
+ (fun x0 ->
+ let sk0 = fun a fk0 ->
+ let sk0 = fun a0 fk1 ->
+ let x1,c = a0 in
+ let sk0 = fun a1 fk2 ->
+ let y,c' = a1 in
+ sk (y,(if c then c' else false))
+ fk2
+ in
+ (match x1 with
+ | Util.Inl p ->
+ let p0,y = p in
+ let a1,s0 = p0 in
+ sk0 (((Util.Inl
+ (a1,(fun e0 x2 ->
+ y e0))),s0),true) fk1
+ | Util.Inr e0 ->
+ sk0 (((Util.Inr e0),s),true) fk1)
+ in
+ let x1,c = a in
+ let sk1 = fun a0 fk1 ->
+ let y,c' = a0 in
+ sk0 (y,(if c then c' else false))
+ fk1
+ in
+ (match x1 with
+ | Util.Inl p ->
+ let a0,y = p in
+ sk1 ((Util.Inl (a0,(fun e0 x2 ->
+ y e0))),true) fk0
+ | Util.Inr e0 ->
+ sk1 ((Util.Inr e0),true) fk0)
+ in
+ (match x0 with
+ | Util.Inl p ->
+ let p0,y = p in
+ let a,c = p0 in
+ sk0 ((Util.Inl (a,y)),c) fk
+ | Util.Inr e0 ->
+ sk0 ((Util.Inr e0),true) fk))
+
+ (** val lift :
+ 'a1 NonLogical.t -> proofview ->
+ Environ.env -> __ ->
+ ((('a1*proofview)*bool) -> (exn -> 'a2
+ IOBase.coq_T) -> 'a2 IOBase.coq_T) ->
+ (exn -> 'a2 IOBase.coq_T) -> 'a2
+ IOBase.coq_T **)
+
+ let lift x s e r sk fk =
+ IOBase.bind x (fun x0 ->
+ sk ((x0,s),true) fk)
+
+ (** val run :
+ 'a1 t -> logicalEnvironment ->
+ logicalState ->
+ (('a1*logicalState)*logicalMessageType)
+ NonLogical.t **)
+
+ let run x e s =
+ Obj.magic x s e __ (fun a x0 ->
+ IOBase.ret a) (fun e0 ->
+ IOBase.raise
+ ((fun e -> Proof_errors.TacticFailure e)
+ e0))
+ end
+
diff --git a/proofs/proofview_monad.ml b/proofs/proofview_monad.ml
new file mode 100644
index 0000000000..ebbb040877
--- /dev/null
+++ b/proofs/proofview_monad.ml
@@ -0,0 +1 @@
+include Proofview_gen
diff --git a/proofs/proofview_monad.mli b/proofs/proofview_monad.mli
new file mode 100644
index 0000000000..02550aebc0
--- /dev/null
+++ b/proofs/proofview_monad.mli
@@ -0,0 +1,81 @@
+(* This is an interface for the code extracted from bootstrap/Monad.v.
+ The relevant comments are overthere. *)
+
+
+type proofview = { initial : (Term.constr * Term.types) list;
+ solution : Evd.evar_map; comb : Goal.goal list }
+
+type logicalState = proofview
+
+type logicalEnvironment = Environ.env
+
+type logicalMessageType = bool
+
+
+
+module NonLogical : sig
+
+ type +'a t
+ type 'a ref
+
+ val ret : 'a -> 'a t
+ val bind : 'a t -> ('a -> 'b t) -> 'b t
+ val ignore : 'a t -> unit t
+ val seq : unit t -> 'a t -> 'a t
+
+ val new_ref : 'a -> 'a ref t
+ val set : 'a ref -> 'a -> unit t
+ val get : 'a ref -> 'a t
+
+ val raise : exn -> 'a t
+ val catch : 'a t -> (exn -> 'a t) -> 'a t
+ val timeout : int -> 'a t -> 'a t
+
+
+ (* [run] performs effects. *)
+ val run : 'a t -> 'a
+
+end
+
+
+module Logical : sig
+
+ type +'a t
+
+ val ret : 'a -> 'a t
+ val bind : 'a t -> ('a -> 'b t) -> 'b t
+ val ignore : 'a t -> unit t
+ val seq : unit t -> 'a t -> 'a t
+
+ val set : logicalState -> unit t
+ val get : logicalState t
+ val put : logicalMessageType -> unit t
+ val current : logicalEnvironment t
+
+ val zero : exn -> 'a t
+ val plus : 'a t -> (exn -> 'a t) -> 'a t
+ val split : 'a t -> (('a*(exn->'a t),exn) Util.union) t
+
+ val lift : 'a NonLogical.t -> 'a t
+
+ val run : 'a t -> logicalEnvironment -> logicalState -> (('a*logicalState)*logicalMessageType) NonLogical.t
+end
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index 816415b48a..2553b9bf93 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -512,7 +512,7 @@ module New = struct
Proofview.tclOR
(Proofview.tclTIMEOUT n t)
begin function
- | Monads.IO.Timeout as e -> Proofview.tclZERO (Refiner.FailError (0,lazy (Errors.print e)))
+ | Proofview.Timeout as e -> Proofview.tclZERO (Refiner.FailError (0,lazy (Errors.print e)))
| e -> Proofview.tclZERO e
end
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index f6983cba39..3e37ea998a 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -3758,6 +3758,7 @@ let abstract_subproof id tac gl =
with Uninstantiated_evar _ ->
error "\"abstract\" cannot handle existentials." in
(* spiwack: the [abstract] tacticals loses the "unsafe status" information *)
+ try
let (const,_) = Pfedit.build_constant_by_tactic id secsign concl
(Tacticals.New.tclCOMPLETE (Tacticals.New.tclTHEN (Tacticals.New.tclDO (List.length sign) intro) tac)) in
let cd = Entries.DefinitionEntry const in
@@ -3772,6 +3773,12 @@ let abstract_subproof id tac gl =
exact_no_check
(applist (lem,List.rev (instance_from_named_context sign)))
gl
+ with Proof_errors.TacticFailure e ->
+ (* if the tactic [tac] fails, it reports a [TacticFailure e],
+ which is an error irrelevant to the proof system (in fact it
+ means that [e] comes from [tac] failing to yield enough
+ success). Hence it reraises [e]. *)
+ raise e
let tclABSTRACT name_op tac gl =
let s = match name_op with
diff --git a/toplevel/cerrors.ml b/toplevel/cerrors.ml
index b9468a298c..96ade04103 100644
--- a/toplevel/cerrors.ml
+++ b/toplevel/cerrors.ml
@@ -57,7 +57,7 @@ let wrap_vernac_error exn strm =
let e = EvaluatedError (hov 0 (str "Error:" ++ spc () ++ strm), None) in
Exninfo.copy exn e
-let process_vernac_interp_error exn = match exn with
+let rec process_vernac_interp_error exn = match exn with
| Univ.UniverseInconsistency (o,u,v,p) ->
let pr_rel r =
match r with
@@ -114,6 +114,7 @@ let process_vernac_interp_error exn = match exn with
if Int.equal i 0 then str "." else str " (level " ++ int i ++ str").")
| AlreadyDeclared msg ->
wrap_vernac_error exn (msg ++ str ".")
+ | Proof_errors.TacticFailure e -> process_vernac_interp_error e
| exc ->
exc
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-03 22:27:47 +0000