1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
|
default Order dec
$include <prelude.sail>
/* Test returning an existential with a mixed boolean/integer
constraint */
val foo : forall ('n : Int) ('b : Bool).
(bool('b), int('n)) -> {'m, 'b & 'm == 'n | not('b) & 'm == 3. int('m)}
function foo(b, n) = {
if b then n else 3
}
/* We now allow type synonyms for kinds other that Type */
type implies('p: Bool, 'q: Bool) -> Bool = not('p) | 'q
infixr 1 -->
type operator -->('p: Bool, 'q: Bool) -> Bool = implies('p, 'q)
infix 1 <-->
type operator <-->('p: Bool, 'q: Bool) -> Bool = ('p --> 'q) & ('q --> 'p)
val my_not = pure {coq: "negb", _: "not"} : forall ('p : Bool). bool('p) -> {('q : Bool), 'p <--> not('q). bool('q)}
/* This example mimics 32-bit ARM instructions where a flag in the
function argument restricts a type variable in a specific branch of
the code */
val test : forall ('n : Int) ('b : Bool), 0 <= 'n <= 15 & implies('b, 'n <= 14).
(bool('b), int('n)) -> unit
function test(cond, n) = {
if cond then {
_prove(constraint('n <= 14))
} else {
_not_prove(constraint('n <= 14));
_prove(constraint('n <= 15))
};
if my_not(cond) then {
_not_prove(constraint('n <= 14));
_prove(constraint('n <= 15))
} else {
_prove(constraint('n <= 14))
}
}
|
