diff options
Diffstat (limited to 'proofs/logic_monad.ml')
-rw-r--r-- | proofs/logic_monad.ml | 133 |
1 files changed, 64 insertions, 69 deletions
diff --git a/proofs/logic_monad.ml b/proofs/logic_monad.ml index d509670e..e3caa886 100644 --- a/proofs/logic_monad.ml +++ b/proofs/logic_monad.ml @@ -94,10 +94,6 @@ struct let print_char = fun c -> (); fun () -> print_char c - (** {!Pp.pp}. The buffer is also flushed. *) - let print = fun s -> (); fun () -> try Pp.msg_info s; Pp.pp_flush () with e -> - let (e, info) = Errors.push e in raise ~info e () - let timeout = fun n t -> (); fun () -> Control.timeout n t (Exception Timeout) @@ -107,6 +103,13 @@ struct let (e, info) = Errors.push e in Util.iraise (Exception e, info) + (** Use the current logger. The buffer is also flushed. *) + let print_debug s = make (fun _ -> Pp.msg_info s;Pp.pp_flush ()) + let print_info s = make (fun _ -> Pp.msg_info s;Pp.pp_flush ()) + let print_warning s = make (fun _ -> Pp.msg_warning s;Pp.pp_flush ()) + let print_error s = make (fun _ -> Pp.msg_error s;Pp.pp_flush ()) + let print_notice s = make (fun _ -> Pp.msg_notice s;Pp.pp_flush ()) + let run = fun x -> try x () with Exception e as src -> let (src, info) = Errors.push src in @@ -184,7 +187,7 @@ struct shape of the monadic type is reminiscent of that of the continuation monad transformer. - The paper also contains the rational for the [split] abstraction. + The paper also contains the rationale for the [split] abstraction. An explanation of how to derive such a monad from mathematical principles can be found in "Kan Extensions for Program @@ -208,118 +211,110 @@ struct type rich_exn = Exninfo.iexn type 'a iolist = - { iolist : 'r. (rich_exn -> 'r NonLogical.t) -> - ('a -> (rich_exn -> 'r NonLogical.t) -> 'r NonLogical.t) -> - 'r NonLogical.t } + { iolist : 'r. state -> (rich_exn -> 'r NonLogical.t) -> + ('a -> state -> (rich_exn -> 'r NonLogical.t) -> 'r NonLogical.t) -> + 'r NonLogical.t } include Monad.Make(struct - type 'a t = state -> ('a * state) iolist - let return x : 'a t = (); fun s -> - { iolist = fun nil cons -> cons (x, s) nil } + type 'a t = 'a iolist + + let return x = + { iolist = fun s nil cons -> cons x s nil } - let (>>=) (m : 'a t) (f : 'a -> 'b t) : 'b t = (); fun s -> - let m = m s in - { iolist = fun nil cons -> - m.iolist nil (fun (x, s) next -> (f x s).iolist next cons) } + let (>>=) m f = + { iolist = fun s nil cons -> + m.iolist s nil (fun x s next -> (f x).iolist s next cons) } - let (>>) (m : unit t) (f : 'a t) : 'a t = (); fun s -> - let m = m s in - { iolist = fun nil cons -> - m.iolist nil (fun ((), s) next -> (f s).iolist next cons) } + let (>>) m f = + { iolist = fun s nil cons -> + m.iolist s nil (fun () s next -> f.iolist s next cons) } - let map (f : 'a -> 'b) (m : 'a t) : 'b t = (); fun s -> - let m = m s in - { iolist = fun nil cons -> m.iolist nil (fun (x, s) next -> cons (f x, s) next) } + let map f m = + { iolist = fun s nil cons -> m.iolist s nil (fun x s next -> cons (f x) s next) } end) - let zero e : 'a t = (); fun s -> - { iolist = fun nil cons -> nil e } + let zero e = + { iolist = fun _ nil cons -> nil e } - let plus m1 m2 : 'a t = (); fun s -> - let m1 = m1 s in - { iolist = fun nil cons -> m1.iolist (fun e -> (m2 e s).iolist nil cons) cons } + let plus m1 m2 = + { iolist = fun s nil cons -> m1.iolist s (fun e -> (m2 e).iolist s nil cons) cons } - let ignore (m : 'a t) : unit t = (); fun s -> - let m = m s in - { iolist = fun nil cons -> m.iolist nil (fun (_, s) next -> cons ((), s) next) } + let ignore m = + { iolist = fun s nil cons -> m.iolist s nil (fun _ s next -> cons () s next) } - let lift (m : 'a NonLogical.t) : 'a t = (); fun s -> - { iolist = fun nil cons -> NonLogical.(m >>= fun x -> cons (x, s) nil) } + let lift m = + { iolist = fun s nil cons -> NonLogical.(m >>= fun x -> cons x s nil) } (** State related *) - let get : P.s t = (); fun s -> - { iolist = fun nil cons -> cons (s.sstate, s) nil } + let get = + { iolist = fun s nil cons -> cons s.sstate s nil } - let set (sstate : P.s) : unit t = (); fun s -> - { iolist = fun nil cons -> cons ((), { s with sstate }) nil } + let set (sstate : P.s) = + { iolist = fun s nil cons -> cons () { s with sstate } nil } - let modify (f : P.s -> P.s) : unit t = (); fun s -> - { iolist = fun nil cons -> cons ((), { s with sstate = f s.sstate }) nil } + let modify (f : P.s -> P.s) = + { iolist = fun s nil cons -> cons () { s with sstate = f s.sstate } nil } - let current : P.e t = (); fun s -> - { iolist = fun nil cons -> cons (s.rstate, s) nil } + let current = + { iolist = fun s nil cons -> cons s.rstate s nil } - let local (type a) (e:P.e) (m:a t) : a t = (); fun s -> - let m = m { s with rstate = e } in - { iolist = fun nil cons -> - m.iolist nil (fun (x,s') next -> cons (x,{s' with rstate=s.rstate}) next) } + let local e m = + { iolist = fun s nil cons -> + m.iolist { s with rstate = e } nil + (fun x s' next -> cons x {s' with rstate = s.rstate} next) } - let put (w : P.w) : unit t = (); fun s -> - { iolist = fun nil cons -> cons ((), { s with wstate = P.wprod s.wstate w }) nil } + let put w = + { iolist = fun s nil cons -> cons () { s with wstate = P.wprod s.wstate w } nil } - let update (f : P.u -> P.u) : unit t = (); fun s -> - { iolist = fun nil cons -> cons ((), { s with ustate = f s.ustate }) nil } + let update (f : P.u -> P.u) = + { iolist = fun s nil cons -> cons () { s with ustate = f s.ustate } nil } (** List observation *) - let once (m : 'a t) : 'a t = (); fun s -> - let m = m s in - { iolist = fun nil cons -> m.iolist nil (fun x _ -> cons x nil) } + let once m = + { iolist = fun s nil cons -> m.iolist s nil (fun x s _ -> cons x s nil) } - let break (f : rich_exn -> rich_exn option) (m : 'a t) : 'a t = (); fun s -> - let m = m s in - { iolist = fun nil cons -> - m.iolist nil (fun x next -> cons x (fun e -> match f e with None -> next e | Some e -> nil e)) + let break f m = + { iolist = fun s nil cons -> + m.iolist s nil (fun x s next -> cons x s (fun e -> match f e with None -> next e | Some e -> nil e)) } (** For [reflect] and [split] see the "Backtracking, Interleaving, and Terminating Monad Transformers" paper. *) type 'a reified = ('a, rich_exn -> 'a reified) list_view NonLogical.t - let rec reflect (m : 'a reified) : 'a iolist = - { iolist = fun nil cons -> + let rec reflect (m : ('a * state) reified) : 'a iolist = + { iolist = fun s0 nil cons -> let next = function | Nil e -> nil e - | Cons (x, l) -> cons x (fun e -> (reflect (l e)).iolist nil cons) + | Cons ((x, s), l) -> cons x s (fun e -> (reflect (l e)).iolist s0 nil cons) in NonLogical.(m >>= next) } - let split (m : 'a t) : ('a, rich_exn -> 'a t) list_view t = (); fun s -> - let m = m s in + let split m : ('a, rich_exn -> 'a t) list_view t = let rnil e = NonLogical.return (Nil e) in - let rcons p l = NonLogical.return (Cons (p, l)) in - { iolist = fun nil cons -> + let rcons p s l = NonLogical.return (Cons ((p, s), l)) in + { iolist = fun s nil cons -> let open NonLogical in - m.iolist rnil rcons >>= begin function - | Nil e -> cons (Nil e, s) nil + m.iolist s rnil rcons >>= begin function + | Nil e -> cons (Nil e) s nil | Cons ((x, s), l) -> - let l e = (); fun _ -> reflect (l e) in - cons (Cons (x, l), s) nil + let l e = reflect (l e) in + cons (Cons (x, l)) s nil end } let run m r s = let s = { wstate = P.wunit; ustate = P.uunit; rstate = r; sstate = s } in - let m = m s in let rnil e = NonLogical.return (Nil e) in - let rcons (x, s) l = + let rcons x s l = let p = (x, s.sstate, s.wstate, s.ustate) in NonLogical.return (Cons (p, l)) in - m.iolist rnil rcons + m.iolist s rnil rcons let repr x = x |