source: extracted/state.ml @ 2717

Last change on this file since 2717 was 2717, checked in by sacerdot, 7 years ago

Extracted code for the whole compiler.
The space cost model is not there yet.

I have fixed by hand the few extraction problems
(i.e. composed coercions not extracted and type
definitions with wrong syntax).

I have also changed all axioms to be implemented
so that they do not fail at initialization time.

File size: 1.1 KB
Line 
1open Preamble
2
3open Jmeq
4
5open Russell
6
7open Bool
8
9open Nat
10
11open List
12
13open Setoids
14
15open Relations
16
17open Hints_declaration
18
19open Core_notation
20
21open Pts
22
23open Logic
24
25open Types
26
27open Monad
28
29(** val state_monad : Monad.setoidMonadProps **)
30let 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 **)
35let 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 **)
39let 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 **)
43let 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 **)
48let state_update f =
49  Obj.magic (fun s -> { Types.fst = (f s); Types.snd = Types.It })
50
51(** val state_pred : Monad.monadPred **)
52let state_pred =
53  Monad.Mk_MonadPred
54
55(** val stateRel : Monad.monadRel **)
56let stateRel =
57  Monad.Mk_MonadRel
58
Note: See TracBrowser for help on using the repository browser.