diff options
| -rw-r--r-- | proofs/proof.ml | 2 | ||||
| -rw-r--r-- | proofs/proofview.ml | 216 | ||||
| -rw-r--r-- | proofs/proofview.mli | 2 | ||||
| -rw-r--r-- | proofs/proofview_monad.ml | 98 | ||||
| -rw-r--r-- | proofs/proofview_monad.mli | 49 |
5 files changed, 216 insertions, 151 deletions
diff --git a/proofs/proof.ml b/proofs/proof.ml index 53b73097f..8d43513f2 100644 --- a/proofs/proof.ml +++ b/proofs/proof.ml @@ -318,7 +318,7 @@ let initial_goals p = Proofview.initial_goals p.entry let run_tactic env tac pr = let sp = pr.proofview in - let (_,tacticced_proofview,(status,(to_shelve,give_up))) = Proofview.apply env tac sp in + let (_,tacticced_proofview,(status,to_shelve,give_up)) = Proofview.apply env tac sp in let shelf = Proofview.in_proofview tacticced_proofview begin fun sigma -> let pre_shelf = pr.shelf@(Evd.future_goals sigma)@to_shelve in diff --git a/proofs/proofview.ml b/proofs/proofview.ml index dd1515918..34d53c3f2 100644 --- a/proofs/proofview.ml +++ b/proofs/proofview.ml @@ -22,10 +22,86 @@ open Pp open Util +open Proofview_monad (* Type of proofviews. *) -type proofview = Proofview_monad.proofview -open Proofview_monad +type proofview = { solution : Evd.evar_map; comb : Goal.goal list } + +(** Parameters of the logic monads *) +module P = struct + + type s = proofview * Environ.env + + type e = unit + (* spiwack: nothing read-only anymore but it's free so I'll leave a place holder. *) + + (** Status (safe/unsafe) * shelved goals * given up *) + type w = bool * Evar.t list * Evar.t list + + let wunit = true , [] , [] + let wprod (b1,s1,g1) (b2,s2,g2) = b1 && b2 , s1@s2 , g1@g2 + +end + +(** Definition of the tactic monad *) +module Proof = Logical(P) + +(** Lenses to access to components of the states *) +module Pv = struct + + type t = proofview + + let get : t Proof.t = Proof.(map fst get) + let set (p:t) : unit Proof.t = Proof.modify (fun (_,e) -> (p,e)) + let modify (f:t->t) : unit Proof.t = Proof.modify (fun (p,e) -> (f p,e)) + +end + +module Comb = struct + + type t = Evar.t list + + let get : t Proof.t = Proof.map (fun {comb} -> comb) Pv.get + let set (c:Evar.t list) : unit Proof.t = Pv.modify (fun pv -> { pv with comb = c }) + let modify (f:Evar.t list -> Evar.t list) : unit Proof.t = + Pv.modify (fun pv -> { pv with comb = f pv.comb }) + +end + +module Env = struct + + type t = Environ.env + + let get : t Proof.t = Proof.(map snd get) + let set (e:t) : unit Proof.t = Proof.modify (fun (p,_) -> (p,e)) + let modify (f:t->t) : unit Proof.t = Proof.modify (fun (p,e) -> (p,f e)) + +end + +module Status = struct + + type t = bool + + let put (s:t) : unit Proof.t = Proof.put (s,[],[]) + +end + +module Shelf = struct + + type t = Evar.t list + + let put (sh:t) : unit Proof.t = Proof.put (true,sh,[]) + +end + +module Giveup = struct + + type t = Evar.t list + + let put (gs:t) : unit Proof.t = Proof.put (true,[],gs) + +end + type entry = (Term.constr * Term.types) list @@ -235,7 +311,6 @@ let unfocus c sp = - report unsafe status, shelved goals and given up goals - access and change the current [proofview] - backtrack on previous changes of the proofview *) -module Proof = Proofview_monad.Logical type +'a tactic = 'a Proof.t type 'a case = @@ -244,8 +319,10 @@ type 'a case = (* Applies a tactic to the current proofview. *) let apply env t sp = - let (((next_r,next_state),status)) = Proofview_monad.NonLogical.run (Proof.run t env sp) in - next_r , next_state , status + let (next_r,(next_state,_),status) = + Proofview_monad.NonLogical.run (Proof.run t () (sp,env)) + in + next_r,next_state,status (*** tacticals ***) @@ -344,12 +421,12 @@ let tclFOCUS_gen nosuchgoal i j t = (* spiwack: convenience notations, waiting for ocaml 3.12 *) let (>>=) = Proof.bind in let (>>) = Proof.seq in - Proof.get >>= fun initial -> + Pv.get >>= fun initial -> try let (focused,context) = focus i j initial in - Proof.set focused >> + Pv.set focused >> t >>= fun result -> - Proof.modify (fun next -> unfocus context next) >> + Pv.modify (fun next -> unfocus context next) >> Proof.ret result with IndexOutOfRange -> nosuchgoal @@ -359,15 +436,15 @@ let tclTRYFOCUS i j t = tclFOCUS_gen (tclUNIT ()) i j t let tclFOCUSID id t = let (>>=) = Proof.bind in let (>>) = Proof.seq in - Proof.get >>= fun initial -> + Pv.get >>= fun initial -> let rec aux n = function | [] -> tclZERO (NoSuchGoals 1) | g::l -> if Names.Id.equal (Evd.evar_ident g initial.solution) id then let (focused,context) = focus n n initial in - Proof.set focused >> + Pv.set focused >> t >>= fun result -> - Proof.modify (fun next -> unfocus context next) >> + Pv.modify (fun next -> unfocus context next) >> Proof.ret result else aux (n+1) l in @@ -430,15 +507,10 @@ let list_iter2 l1 l2 s i = | reraise -> tclZERO reraise end -(* A variant of [Proof.set] specialized on the comb. Doesn't change - the underlying "solution" (i.e. [evar_map]) *) -let set_comb c = - Proof.modify (fun step -> { step with comb = c }) - let on_advance g ~solved ~adv = (* spiwack: convenience notations, waiting for ocaml 3.12 *) let (>>=) = Proof.bind in - Proof.get >>= fun step -> + Pv.get >>= fun step -> match advance step.solution g with | None -> solved (* If [first] has been solved by side effect: do nothing. *) | Some g -> adv g @@ -452,17 +524,17 @@ let list_iter_goal s i = (* spiwack: convenience notations, waiting for ocaml 3.12 *) let (>>=) = Proof.bind in let (>>) = Proof.seq in - Proof.get >>= fun initial -> + Pv.get >>= fun initial -> list_iter initial.comb (s,[]) begin fun goal ((r,subgoals) as cur) -> on_advance goal ~solved: ( Proof.ret cur ) ~adv: begin fun goal -> - set_comb [goal] >> + Comb.set [goal] >> i goal r >>= fun r -> - Proof.map (fun step -> (r, step.comb :: subgoals)) Proof.get + Proof.map (fun step -> (r, step.comb :: subgoals)) Pv.get end end >>= fun (r,subgoals) -> - set_comb (List.flatten (List.rev subgoals)) >> + Comb.set (List.flatten (List.rev subgoals)) >> Proof.ret r (* spiwack: essentially a copy/paste of the above… *) @@ -471,17 +543,17 @@ let list_iter_goal2 l s i = (* spiwack: convenience notations, waiting for ocaml 3.12 *) let (>>=) = Proof.bind in let (>>) = Proof.seq in - Proof.get >>= fun initial -> + Pv.get >>= fun initial -> list_iter2 initial.comb l (s,[]) begin fun goal a ((r,subgoals) as cur) -> on_advance goal ~solved: ( Proof.ret cur ) ~adv: begin fun goal -> - set_comb [goal] >> + Comb.set [goal] >> i goal a r >>= fun r -> - Proof.map (fun step -> (r, step.comb :: subgoals)) Proof.get + Proof.map (fun step -> (r, step.comb :: subgoals)) Pv.get end end >>= fun (r,subgoals) -> - set_comb (List.flatten (List.rev subgoals)) >> + Comb.set (List.flatten (List.rev subgoals)) >> Proof.ret r (* spiwack: we use an parametrised function to generate the dispatch @@ -493,14 +565,14 @@ let tclDISPATCHGEN f join tacs = match tacs with | [] -> begin - Proof.get >>= fun initial -> + Pv.get >>= fun initial -> match initial.comb with | [] -> tclUNIT (join []) | _ -> tclZERO (SizeMismatch (List.length initial.comb,0)) end | [tac] -> begin - Proof.get >>= fun initial -> + Pv.get >>= fun initial -> match initial.comb with | [goal] -> on_advance goal @@ -543,7 +615,7 @@ let extend_to_list startxs rx endxs l = let tclEXTEND tacs1 rtac tacs2 = (* spiwack: convenience notations, waiting for ocaml 3.12 *) let (>>=) = Proof.bind in - Proof.get >>= fun step -> + Pv.get >>= fun step -> try let tacs = extend_to_list tacs1 rtac tacs2 step.comb in tclDISPATCH tacs @@ -558,14 +630,14 @@ let tclEXTEND tacs1 rtac tacs2 = let tclINDEPENDENT tac = (* spiwack: convenience notations, waiting for ocaml 3.12 *) let (>>=) = Proof.bind in - Proof.get >>= fun initial -> + Pv.get >>= fun initial -> match initial.comb with | [] -> tclUNIT () | [_] -> tac | _ -> list_iter_goal () (fun _ () -> tac) let tclNEWGOALS gls = - Proof.modify begin fun step -> + Pv.modify begin fun step -> let map gl = advance step.solution gl in let gls = List.map_filter map gls in { step with comb = step.comb @ gls } @@ -580,9 +652,9 @@ let goal_equal evars1 gl1 evars2 gl2 = let tclPROGRESS t = (* spiwack: convenience notations, waiting for ocaml 3.12 *) let (>>=) = Proof.bind in - Proof.get >>= fun initial -> + Pv.get >>= fun initial -> t >>= fun res -> - Proof.get >>= fun final -> + Pv.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) @@ -593,16 +665,16 @@ let tclPROGRESS t = tclZERO (Errors.UserError ("Proofview.tclPROGRESS" , Pp.str"Failed to progress.")) let tclEVARMAP = - Proof.map (fun initial -> initial.solution) Proof.get + Proof.map (fun initial -> initial.solution) Pv.get -let tclENV = Proof.current +let tclENV = Env.get let tclEFFECTS eff = Proof.bind (Proof.ret ()) (fun () -> (* The Global.env should be taken at exec time *) Proof.seq - (Proof.update (Global.env ())) - (Proof.modify (fun initial -> emit_side_effects eff initial))) + (Env.set (Global.env ())) + (Pv.modify (fun initial -> emit_side_effects eff initial))) exception Timeout let _ = Errors.register_handler begin function @@ -620,13 +692,12 @@ let tclTIMEOUT n t = 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)) + (Proofview_monad.NonLogical.timeout n (Proof.run t () initial)) (fun r -> Proofview_monad.NonLogical.ret (Util.Inl r)) end begin function @@ -637,7 +708,7 @@ let tclTIMEOUT n t = | e -> Proofview_monad.NonLogical.raise e end end >>= function - | Util.Inl ((res,s),m) -> + | Util.Inl (res,s,m) -> Proof.set s >> Proof.put m >> Proof.ret res @@ -670,17 +741,16 @@ let tclTIME s t = tclOR (tclUNIT x) (fun e -> aux (n+1) (k e)) in aux 0 t -let mark_as_unsafe = - Proof.put (false,([],[])) +let mark_as_unsafe = Status.put false (* Shelves all the goals under focus. *) let shelve = (* spiwack: convenience notations, waiting for ocaml 3.12 *) let (>>=) = Proof.bind in let (>>) = Proof.seq in - Proof.get >>= fun initial -> - Proof.set {initial with comb=[]} >> - Proof.put (true,(initial.comb,[])) + Pv.get >>= fun initial -> + Pv.set {initial with comb=[]} >> + Shelf.put initial.comb (* [contained_in_info e evi] checks whether the evar [e] appears in @@ -716,14 +786,14 @@ let shelve_unifiable = (* spiwack: convenience notations, waiting for ocaml 3.12 *) let (>>=) = Proof.bind in let (>>) = Proof.seq in - Proof.get >>= fun initial -> + Pv.get >>= fun initial -> let (u,n) = partition_unifiable initial.solution initial.comb in - Proof.set {initial with comb=n} >> - Proof.put (true,(u,[])) + Pv.set {initial with comb=n} >> + Shelf.put u let check_no_dependencies = let (>>=) = Proof.bind in - Proof.get >>= fun initial -> + Pv.get >>= fun initial -> let (u,n) = partition_unifiable initial.solution initial.comb in match u with | [] -> tclUNIT () @@ -745,9 +815,10 @@ let give_up = (* spiwack: convenience notations, waiting for ocaml 3.12 *) let (>>=) = Proof.bind in let (>>) = Proof.seq in - Proof.get >>= fun initial -> - Proof.set {initial with comb=[]} >> - Proof.put (false,([],initial.comb)) + Pv.get >>= fun initial -> + Pv.set {initial with comb=[]} >> + mark_as_unsafe >> + Giveup.put initial.comb (** [goodmod p m] computes the representative of [p] modulo [m] in the interval [[0,m-1]].*) @@ -761,16 +832,16 @@ let goodmod p m = let cycle n = (* spiwack: convenience notations, waiting for ocaml 3.12 *) let (>>=) = Proof.bind in - Proof.get >>= fun initial -> + Pv.get >>= fun initial -> let l = List.length initial.comb in let n' = goodmod n l in let (front,rear) = List.chop n' initial.comb in - Proof.set {initial with comb=rear@front} + Pv.set {initial with comb=rear@front} let swap i j = (* spiwack: convenience notations, waiting for ocaml 3.12 *) let (>>=) = Proof.bind in - Proof.get >>= fun initial -> + Pv.get >>= fun initial -> let l = List.length initial.comb 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 @@ -782,18 +853,18 @@ let swap i j = | _ -> x end 0 initial.comb in - Proof.set {initial with comb} + Pv.set {initial with comb} let revgoals = (* spiwack: convenience notations, waiting for ocaml 3.12 *) let (>>=) = Proof.bind in - Proof.get >>= fun initial -> - Proof.set {initial with comb=List.rev initial.comb} + Pv.get >>= fun initial -> + Pv.set {initial with comb=List.rev initial.comb} let numgoals = (* spiwack: convenience notations, waiting for ocaml 3.12 *) let (>>=) = Proof.bind in - Proof.get >>= fun { comb } -> + Pv.get >>= fun { comb } -> Proof.ret (List.length comb) (*** Commands ***) @@ -826,7 +897,7 @@ module V82 = struct expectingly preserving the semantics of <= 8.2 tactics *) (* spiwack: convenience notations, waiting for ocaml 3.12 *) let (>>=) = Proof.bind in - Proof.get >>= fun ps -> + Pv.get >>= fun ps -> try let tac gl evd = let glsigma = @@ -841,7 +912,7 @@ module V82 = struct in let (goalss,evd) = Evd.Monad.List.map tac initgoals initevd in let sgs = List.flatten goalss in - Proof.set { solution = evd; comb = sgs; } + Pv.set { solution = evd; comb = sgs; } with e when catchable_exception e -> let e = Errors.push e in tclZERO e @@ -850,7 +921,7 @@ module V82 = struct (* normalises the evars in the goals, and stores the result in solution. *) let nf_evar_goals = - Proof.modify begin fun ps -> + Pv.modify begin fun ps -> let map g s = Goal.V82.nf_evar s g in let (goals,evd) = Evd.Monad.List.map map ps.comb ps.solution in { solution = evd; comb = goals; } @@ -858,13 +929,13 @@ module V82 = struct (* A [Proofview.tactic] version of [Refiner.tclEVARS] *) let tclEVARS evd = - Proof.modify (fun ps -> { ps with solution = evd }) + Pv.modify (fun ps -> { ps with solution = evd }) let tclEVARSADVANCE evd = - Proof.modify (fun ps -> { solution = evd; comb = undefined evd ps.comb }) + Pv.modify (fun ps -> { solution = evd; comb = undefined evd ps.comb }) let tclEVARUNIVCONTEXT ctx = - Proof.modify (fun ps -> { ps with solution = Evd.set_universe_context ps.solution ctx }) + Pv.modify (fun ps -> { ps with solution = Evd.set_universe_context ps.solution ctx }) let has_unresolved_evar pv = Evd.has_undefined pv.solution @@ -916,8 +987,7 @@ module V82 = struct let e = Backtrace.app_backtrace ~src ~dst:e in raise e - let put_status b = - Proof.put (b,([],[])) + let put_status = Status.put let catchable_exception = catchable_exception @@ -959,7 +1029,7 @@ module Goal = struct let nf_enter f = list_iter_goal () begin fun goal () -> - Proof.current >>= fun env -> + Env.get >>= fun env -> tclEVARMAP >>= fun sigma -> try let (gl, sigma) = nf_gmake env sigma goal in @@ -970,7 +1040,7 @@ module Goal = struct end let normalize { self } = - Proof.current >>= fun env -> + Env.get >>= fun env -> tclEVARMAP >>= fun sigma -> let (gl,sigma) = nf_gmake env sigma self in tclTHEN (V82.tclEVARS sigma) (tclUNIT gl) @@ -981,7 +1051,7 @@ module Goal = struct let enter f = list_iter_goal () begin fun goal () -> - Proof.current >>= fun env -> + Env.get >>= fun env -> tclEVARMAP >>= fun sigma -> try f (gmake env sigma goal) with e when catchable_exception e -> @@ -990,8 +1060,8 @@ module Goal = struct end let goals = - Proof.current >>= fun env -> - Proof.get >>= fun step -> + Env.get >>= fun env -> + Pv.get >>= fun step -> let sigma = step.solution in let map goal = match advance sigma goal with @@ -1062,7 +1132,7 @@ struct (** Select the goals *) let comb = undefined sigma (List.rev evs) in let sigma = List.fold_left mark_as_goal sigma comb in - Proof.set { solution = Evd.reset_future_goals sigma; comb; } + Pv.set { solution = Evd.reset_future_goals sigma; comb; } end (** Useful definitions *) @@ -1085,7 +1155,7 @@ end module NonLogical = Proofview_monad.NonLogical -let tclLIFT = Proofview_monad.Logical.lift +let tclLIFT = Proof.lift let tclCHECKINTERRUPT = tclLIFT (NonLogical.make Control.check_for_interrupt) diff --git a/proofs/proofview.mli b/proofs/proofview.mli index d822f933b..45a0c9484 100644 --- a/proofs/proofview.mli +++ b/proofs/proofview.mli @@ -133,7 +133,7 @@ type 'a case = case it is [false]. *) val apply : Environ.env -> 'a tactic -> proofview -> 'a * proofview - * (bool*(Goal.goal list*Goal.goal list)) + * (bool*Goal.goal list*Goal.goal list) (*** tacticals ***) diff --git a/proofs/proofview_monad.ml b/proofs/proofview_monad.ml index 9be26ab2b..784b7d7f3 100644 --- a/proofs/proofview_monad.ml +++ b/proofs/proofview_monad.ml @@ -13,21 +13,6 @@ and a logical layer which handles backtracking, proof manipulation, and any other effect which needs to backtrack. *) -(** {6 States of the logical monad} *) - -type proofview = { solution : Evd.evar_map; comb : Goal.goal list } - -(** Read/write *) -type logicalState = proofview - -(** Write only. Must be a monoid. - - Status (safe/unsafe) * ( shelved goals * given up ). *) -type logicalMessageType = bool*(Goal.goal list*Goal.goal list) - -(** Read only *) -type logicalEnvironment = Environ.env - (** {6 Exceptions} *) @@ -154,22 +139,34 @@ type ('a, 'b) list_view = | Nil of exn | Cons of 'a * 'b -module Logical = -struct +module type Param = sig - type rt = logicalEnvironment - type wt = logicalMessageType - type st = logicalState + (** Read only *) + type e - type state = { - rstate : rt; - wstate : wt; - sstate : st; - } + (** Write only *) + type w - let empty = (true, ([], [])) + (** [w] must be a monoid *) + val wunit : w + val wprod : w -> w -> w - let merge (b1, (l1, k1)) (b2, (l2, k2)) = (b1 && b2, (l1 @ l2, k1 @ k2)) + (** Read-write *) + type s + +end + + +module Logical (P:Param) = +struct + + (** All three of environment, writer and state are coded as a single + state-passing-style monad.*) + type state = { + rstate : P.e; + wstate : P.w; + sstate : P.s; + } (** Double-continuation backtracking monads are reasonable folklore for "search" implementations (including the Tac interactive @@ -190,7 +187,7 @@ struct the impredicative encoding of the following stream type: [type 'a _iolist' = Nil of exn | Cons of 'a*'a iolist' - and 'a iolist = 'a _iolist NonLogical.t] + and 'a iolist = 'a _iolist NonLogical.t] Using impredicative encoding avoids intermediate allocation and is, empirically, very efficient in Ocaml. It also has the @@ -206,66 +203,61 @@ struct ('a -> (exn -> 'r NonLogical.t) -> 'r NonLogical.t) -> 'r NonLogical.t } - type 'a tactic = state -> ('a * state) iolist + type 'a t = state -> ('a * state) iolist - type 'a t = 'a tactic - - let zero e : 'a tactic = (); fun s -> + let zero e : 'a t = (); fun s -> { iolist = fun nil cons -> nil e } - let plus m1 m2 : 'a tactic = (); fun s -> + 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 ret x : 'a tactic = (); fun s -> + let ret x : 'a t = (); fun s -> { iolist = fun nil cons -> cons (x, s) nil } - let bind (m : 'a tactic) (f : 'a -> 'b tactic) : 'b tactic = (); fun s -> + let bind (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 seq (m : unit tactic) (f : 'a tactic) : 'a tactic = (); fun s -> + let seq (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 map (f : 'a -> 'b) (m : 'a tactic) : 'b tactic = (); fun s -> + 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 ignore (m : 'a tactic) : unit tactic = (); fun s -> + 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 lift (m : 'a NonLogical.t) : 'a tactic = (); fun s -> + let lift (m : 'a NonLogical.t) : 'a t = (); fun s -> { iolist = fun nil cons -> NonLogical.bind m (fun x -> cons (x, s) nil) } (** State related *) - let get : st tactic = (); fun s -> + let get : P.s t = (); fun s -> { iolist = fun nil cons -> cons (s.sstate, s) nil } - let set (sstate : st) : unit tactic = (); fun s -> + let set (sstate : P.s) : unit t = (); fun s -> { iolist = fun nil cons -> cons ((), { s with sstate }) nil } - let modify (f : st -> st) : unit tactic = (); fun s -> + let modify (f : P.s -> P.s) : unit t = (); fun s -> { iolist = fun nil cons -> cons ((), { s with sstate = f s.sstate }) nil } - let current : rt tactic = (); fun s -> + let current : P.e t = (); fun s -> { iolist = fun nil cons -> cons (s.rstate, s) nil } - let update (rstate : rt) : unit tactic = (); fun s -> - { iolist = fun nil cons -> cons ((), { s with rstate }) nil } - - let put (w : wt) : unit tactic = (); fun s -> - { iolist = fun nil cons -> cons ((), { s with wstate = merge w s.wstate }) nil } + let put (w : P.w) : unit t = (); fun s -> + { iolist = fun nil cons -> cons ((), { s with wstate = P.wprod s.wstate w }) nil } (** List observation *) - let once (m : 'a tactic) : 'a tactic = (); fun s -> + 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 break (f : exn -> bool) (m : 'a tactic) : 'a tactic = (); fun s -> + let break (f : exn -> bool) (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 -> if f e then nil e else next e)) @@ -284,7 +276,7 @@ struct NonLogical.bind m next } - let split (m : 'a tactic) : ('a, exn -> 'a t) list_view tactic = (); fun s -> + let split (m : 'a t) : ('a, exn -> 'a t) list_view t = (); fun s -> let m = m s in let rnil e = NonLogical.ret (Nil e) in let rcons p l = NonLogical.ret (Cons (p, l)) in @@ -297,10 +289,10 @@ struct end } let run m r s = - let s = { wstate = empty; rstate = r; sstate = s } in + let s = { wstate = P.wunit; rstate = r; sstate = s } in let m = m s in let nil e = NonLogical.raise (TacticFailure e) in - let cons (x, s) _ = NonLogical.ret ((x, s.sstate), s.wstate) in + let cons (x, s) _ = NonLogical.ret (x, s.sstate, s.wstate) in m.iolist nil cons end diff --git a/proofs/proofview_monad.mli b/proofs/proofview_monad.mli index e1d9b4fa1..675b4c768 100644 --- a/proofs/proofview_monad.mli +++ b/proofs/proofview_monad.mli @@ -13,21 +13,6 @@ and a logical layer which handles backtracking, proof manipulation, and any other effect which needs to backtrack. *) -(** {6 States of the logical monad} *) - -type proofview = { solution : Evd.evar_map; comb : Goal.goal list } - -(** Read/write *) -type logicalState = proofview - -(** Read only *) -type logicalEnvironment = Environ.env - -(** Write only. Must be a monoid. - - Status (safe/unsafe) * ( shelved goals * given up ). *) -type logicalMessageType = bool * ( Goal.goal list * Goal.goal list ) - (** {6 Exceptions} *) @@ -119,7 +104,26 @@ type ('a, 'b) list_view = | Nil of exn | Cons of 'a * 'b -module Logical : sig +(** The monad is parametrised in the types of state, environment and + writer. *) +module type Param = sig + + (** Read only *) + type e + + (** Write only *) + type w + + (** [w] must be a monoid *) + val wunit : w + val wprod : w -> w -> w + + (** Read-write *) + type s + +end + +module Logical (P:Param) : sig type +'a t @@ -129,12 +133,11 @@ module Logical : sig val ignore : 'a t -> unit t val seq : unit t -> 'a t -> 'a t - val set : logicalState -> unit t - val get : logicalState t - val modify : (logicalState -> logicalState) -> unit t - val put : logicalMessageType -> unit t - val current : logicalEnvironment t - val update : logicalEnvironment -> unit t + val set : P.s -> unit t + val get : P.s t + val modify : (P.s -> P.s) -> unit t + val put : P.w -> unit t + val current : P.e t val zero : exn -> 'a t val plus : 'a t -> (exn -> 'a t) -> 'a t @@ -144,5 +147,5 @@ module Logical : sig val lift : 'a NonLogical.t -> 'a t - val run : 'a t -> logicalEnvironment -> logicalState -> (('a*logicalState)*logicalMessageType) NonLogical.t + val run : 'a t -> P.e -> P.s -> ('a * P.s * P.w) NonLogical.t end |