aboutsummaryrefslogtreecommitdiffhomepage
path: root/proofs/proofview_monad.ml
diff options
context:
space:
mode:
Diffstat (limited to 'proofs/proofview_monad.ml')
-rw-r--r--proofs/proofview_monad.ml217
1 files changed, 1 insertions, 216 deletions
diff --git a/proofs/proofview_monad.ml b/proofs/proofview_monad.ml
index f6ba5341e..ebbb04087 100644
--- a/proofs/proofview_monad.ml
+++ b/proofs/proofview_monad.ml
@@ -1,216 +1 @@
-module NonLogical =
-struct
-type 'a t = unit -> 'a
-
-type 'a ref = 'a Pervasives.ref
-
-let ret = fun a -> (); fun () -> a
-
-let bind = fun a k -> (); fun () -> k (a ()) ()
-
-let ignore = fun a -> (); fun () -> ignore (a ())
-
-let seq = fun a k -> (); fun () -> a (); k ()
-
-let new_ref = fun a -> (); fun () -> Pervasives.ref a
-
-let set = fun r a -> (); fun () -> Pervasives.(:=) r a
-
-let get = fun r -> (); fun () -> Pervasives.(!) r
-
-let raise = fun e -> (); fun () -> raise (Proof_errors.Exception e)
-
-let catch = fun s h -> (); fun () -> try s () with Proof_errors.Exception e -> h e ()
-
-let read_line = fun () -> try Pervasives.read_line () with e -> raise e ()
-
-let print_char = fun c -> (); fun () -> print_char c
-
-let print = fun s -> (); fun () -> try Pp.pp s; Pp.pp_flush () with e -> raise e ()
-
-let timeout = fun n t -> (); fun () ->
- 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
-
-let run = fun x -> try x () with Proof_errors.Exception e -> Pervasives.raise e
-
-end
-
-
-type ('a, 'b) list_view =
-| Nil of exn
-| Cons of 'a * 'b
-
-type proofview = { initial : (Term.constr*Term.types) list; solution : Evd.evar_map; comb : Goal.goal list }
-
-type logicalState = proofview
-
-type logicalMessageType = bool * (Goal.goal list * Goal.goal list)
-
-type logicalEnvironment = Environ.env
-
-type message = logicalMessageType
-type environment = logicalEnvironment
-type state = logicalState
-
-module Logical =
-struct
-
-type 'a ioT = 'a NonLogical.t
-
-type 'a logicT = { logic : 'r. ('a -> (exn -> 'r ioT) -> 'r ioT) -> (exn -> 'r ioT) -> 'r ioT }
-
-type 'a writerT = { writer : 'r. ('a -> message -> 'r logicT) -> 'r logicT }
-
-type 'a readerT = { reader : 'r. ('a -> 'r writerT) -> environment -> 'r writerT }
-
-type 'a stateT = { state : 'r. ('a -> state -> 'r readerT) -> state -> 'r readerT }
-
-type 'a t = 'a stateT
-
-let empty_message = (true, ([], []))
-
-let ret x = { state = fun k s -> k x s }
-
-let bind m f = { state = fun k s -> m.state (fun x s -> (f x).state k s) s }
-
-let ignore m = { state = fun k s -> m.state (fun _ s -> k () s) s }
-
-let seq m n =
- { state = fun k s -> m.state (fun () s -> n.state k s) s }
-
-let set s =
- { state = fun k _ -> k () s }
-
-let get = { state = fun k s -> k s s }
-
-let current = { state = fun k s -> { reader = fun kr e -> (k e s).reader kr e } }
-
-let join (b1, (l1, r1)) (b2, (l2, r2)) =
- (b1 && b2, (List.append l1 l2, List.append r1 r2))
-
-let put msg =
- { state = fun k s ->
- let m = k () s in
- { reader = fun kr e ->
- let m = m.reader kr e in
- { writer = fun kw -> m.writer
- (fun x nmsg -> kw x (join msg nmsg))
- }
- }
- }
-
-let zero err =
- { state = fun k s ->
- { reader = fun kr e ->
- { writer = fun kw ->
- { logic = fun sk fk -> fk err }
- }
- }
- }
-
-let plus m f =
- { state = fun k s ->
- let m = m.state k s in
- { reader = fun kr e ->
- let m = m.reader kr e in
- { writer = fun kw ->
- let m = m.writer kw in
- { logic = fun sk fk ->
- let plus_fk err = ((((f err).state k s).reader kr e).writer kw).logic sk fk in
- m.logic sk plus_fk
- }
- }
- }
- }
-
-let srun_state x s = { reader = fun kr _ -> kr (x, s) }
-let srun_reader x = { writer = fun kw -> kw x empty_message }
-let srun_writer x msg = { logic = fun sk fk -> sk (x, msg) fk }
-
-let srun_logic_sk x fk =
- let next err =
- let ans = fk err in { logic = fun sk fk ->
- NonLogical.bind ans (function
- | Nil err -> fk err
- | Cons (y, n) -> sk x (fun err -> (n err).logic sk fk))
- } in
- let ans = Cons (x, next) in
- NonLogical.ret ans
-
-let srun_logic_fk err = NonLogical.ret (Nil err)
-
-let split_next k s kr e kw sk fk = (); function
-| Nil _ as x ->
- let m = k x s in
- let m = m.reader kr e in
- let m = m.writer kw in
- m.logic sk fk
-| Cons (((x, s), msg), next) ->
- let next err =
- let next = next err in {
- state = fun k s -> {
- reader = fun kr e -> {
- writer = fun kw -> {
- logic = fun sk fk ->
- let sk ((x, s), msg) fk =
- let kw x nmsg = kw x (join msg nmsg) in
- (((k x s).reader kr e).writer kw).logic sk fk
- in
- next.logic sk fk
- }
- }
- }
- } in
- let m = k (Cons (x, next)) s in
- let m = m.reader kr e in
- let m = m.writer (fun x nmsg -> kw x (join msg nmsg)) in
- m.logic sk fk
-
-let split m =
- { state = fun k s ->
- let m = m.state srun_state s in
- { reader = fun kr e ->
- let m = m.reader srun_reader e in
- { writer = fun kw ->
- let m = m.writer srun_writer in
- { logic = fun sk fk ->
- let m = m.logic srun_logic_sk srun_logic_fk in
- NonLogical.bind m (split_next k s kr e kw sk fk)
- }
- }
- }
- }
-
-let lift m =
- { state = fun k s ->
- { reader = fun kr e ->
- { writer = fun kw ->
- { logic = fun sk fk ->
- let lift x = (((k x s).reader kr e).writer kw).logic sk fk in
- NonLogical.bind m lift
- }
- }
- }
- }
-
-let run m e s =
- let m = m.state srun_state s in
- let m = m.reader srun_reader e in
- let m = m.writer srun_writer in
- let run_fk err = NonLogical.raise (Proof_errors.TacticFailure err) in
- let run_sk x _ = NonLogical.ret x in
- m.logic run_sk run_fk
-
-end
+include Proofview_gen
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-11 16:10:43 +0000