source: extracted/bind_new.mli @ 2746

Last change on this file since 2746 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: 2.2 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
29type ('b, 'e) bind_new =
30| Bret of 'e
31| Bnew of ('b -> ('b, 'e) bind_new)
32
33val bind_new_rect_Type4 :
34  ('a2 -> 'a3) -> (('a1 -> ('a1, 'a2) bind_new) -> ('a1 -> 'a3) -> 'a3) ->
35  ('a1, 'a2) bind_new -> 'a3
36
37val bind_new_rect_Type3 :
38  ('a2 -> 'a3) -> (('a1 -> ('a1, 'a2) bind_new) -> ('a1 -> 'a3) -> 'a3) ->
39  ('a1, 'a2) bind_new -> 'a3
40
41val bind_new_rect_Type2 :
42  ('a2 -> 'a3) -> (('a1 -> ('a1, 'a2) bind_new) -> ('a1 -> 'a3) -> 'a3) ->
43  ('a1, 'a2) bind_new -> 'a3
44
45val bind_new_rect_Type1 :
46  ('a2 -> 'a3) -> (('a1 -> ('a1, 'a2) bind_new) -> ('a1 -> 'a3) -> 'a3) ->
47  ('a1, 'a2) bind_new -> 'a3
48
49val bind_new_rect_Type0 :
50  ('a2 -> 'a3) -> (('a1 -> ('a1, 'a2) bind_new) -> ('a1 -> 'a3) -> 'a3) ->
51  ('a1, 'a2) bind_new -> 'a3
52
53val bind_new_inv_rect_Type4 :
54  ('a1, 'a2) bind_new -> ('a2 -> __ -> 'a3) -> (('a1 -> ('a1, 'a2) bind_new)
55  -> ('a1 -> __ -> 'a3) -> __ -> 'a3) -> 'a3
56
57val bind_new_inv_rect_Type3 :
58  ('a1, 'a2) bind_new -> ('a2 -> __ -> 'a3) -> (('a1 -> ('a1, 'a2) bind_new)
59  -> ('a1 -> __ -> 'a3) -> __ -> 'a3) -> 'a3
60
61val bind_new_inv_rect_Type2 :
62  ('a1, 'a2) bind_new -> ('a2 -> __ -> 'a3) -> (('a1 -> ('a1, 'a2) bind_new)
63  -> ('a1 -> __ -> 'a3) -> __ -> 'a3) -> 'a3
64
65val bind_new_inv_rect_Type1 :
66  ('a1, 'a2) bind_new -> ('a2 -> __ -> 'a3) -> (('a1 -> ('a1, 'a2) bind_new)
67  -> ('a1 -> __ -> 'a3) -> __ -> 'a3) -> 'a3
68
69val bind_new_inv_rect_Type0 :
70  ('a1, 'a2) bind_new -> ('a2 -> __ -> 'a3) -> (('a1 -> ('a1, 'a2) bind_new)
71  -> ('a1 -> __ -> 'a3) -> __ -> 'a3) -> 'a3
72
73val bind_new_discr : ('a1, 'a2) bind_new -> ('a1, 'a2) bind_new -> __
74
75val bind_new_jmdiscr : ('a1, 'a2) bind_new -> ('a1, 'a2) bind_new -> __
76
77val bnews :
78  Nat.nat -> ('a1 List.list -> ('a1, 'a2) bind_new) -> ('a1, 'a2) bind_new
79
80val bnews_strong :
81  Nat.nat -> ('a1 List.list -> __ -> ('a1, 'a2) bind_new) -> ('a1, 'a2)
82  bind_new
83
84val bbind :
85  ('a1, 'a2) bind_new -> ('a2 -> ('a1, 'a3) bind_new) -> ('a1, 'a3) bind_new
86
87val bindNew : Monad.monadProps
88
89open State
90
91val bcompile :
92  'a2 Monad.smax_def__o__monad -> ('a2, 'a3) bind_new -> 'a3
93  Monad.smax_def__o__monad
94
Note: See TracBrowser for help on using the repository browser.