Last change
on this file 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  

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  

Note: See
TracBrowser
for help on using the repository browser.