extracted/state.ml

   1 open Preamble
   2
   3 open Jmeq
   4
   5 open Russell
   6
   7 open Bool
   8
   9 open Nat
  10
  11 open List
  12
  13 open Setoids
  14
  15 open Relations
  16
  17 open Hints_declaration
  18
  19 open Core_notation
  20
  21 open Pts
  22
  23 open Logic
  24
  25 open Types
  26
  27 open Monad
  28
  29 (** val state_monad : Monad.setoidMonadProps **)
  30 let state_monad =
  31   Monad.makeSetoidMonadProps (fun _ x s -> { Types.fst = s; Types.snd = x })
  32     (fun _ _ m f s -> let { Types.fst = s'; Types.snd = x } = m s in f x s')
  33
  34 (** val state_get : 'a1 Monad.smax_def__o__monad **)
  35 let state_get =
  36   Obj.magic (fun s -> { Types.fst = s; Types.snd = s })
  37
  38 (** val state_set : 'a1 -> Types.unit0 Monad.smax_def__o__monad **)
  39 let state_set s =
  40   Obj.magic (fun x -> { Types.fst = s; Types.snd = Types.It })
  41
  42 (** val state_run : 'a1 -> 'a2 Monad.smax_def__o__monad -> 'a2 **)
  43 let state_run s c =
  44   (Obj.magic c s).Types.snd
  45
  46 (** val state_update :
  47     ('a1 -> 'a1) -> Types.unit0 Monad.smax_def__o__monad **)
  48 let state_update f =
  49   Obj.magic (fun s -> { Types.fst = (f s); Types.snd = Types.It })
  50
  51 (** val state_pred : Monad.monadPred **)
  52 let state_pred =
  53   Monad.Mk_MonadPred
  54
  55 (** val stateRel : Monad.monadRel **)
  56 let stateRel =
  57   Monad.Mk_MonadRel
  58