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
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
|
(** CakeML driver *)
printer "cakeml"
module BuiltIn
syntax type int "int"
end
module HighOrd
syntax type (->) "%1 -> %2"
syntax val ( @ ) "%1 %2"
end
module option.Option
syntax type option "%1 option"
syntax val None "NONE"
syntax val Some "SOME %1"
end
module Bool
syntax type bool "bool"
syntax val True "true"
syntax val False "false"
end
module bool.Ite
syntax val ite "(if %1 then %2 else %3)"
end
module bool.Bool
syntax val andb "%1 andalso %2"
syntax val orb "%1 orelse %2"
syntax val xorb "%1 <> %2"
syntax val notb "not %1"
syntax val implb "not %1 orelse %2"
end
module list.List
syntax type list "%1 list"
syntax val Nil "[]"
syntax val Cons "%1 :: %2"
syntax val is_nil "%1 = []"
end
module list.Length
syntax val length "List.length %1"
end
module Ref
syntax type ref "%1 ref"
syntax val contents "!%1"
syntax val ref "ref %1"
end
module ref.Ref
syntax val (!_) "!%1"
syntax val (:=) "%1 := %2"
end
module ref.Refint
syntax val incr "%1 := !%1 + 1"
syntax val decr "%1 := !%1 - 1"
syntax val (+=) "%1 := !%1 + %2"
syntax val (-=) "%1 := !%1 - %2"
syntax val ( *= ) "%1 := !%1 * %2"
end
module int.Int
syntax val zero "0"
syntax val one "1"
syntax val (<) "%1 < %2"
syntax val (<=) "%1 <= %2"
syntax val (>) "%1 > %2"
syntax val (>=) "%1 >= %2"
syntax val (=) "%1 = %2"
syntax val (+) "%1 + %2"
syntax val (-) "%1 - %2"
syntax val ( * ) "%1 * %2"
syntax val (-_) "~%1"
end
module int.EuclideanDivision
syntax val div "%1 div %2"
syntax val mod "%1 mod %2"
end
(* not implemented in CakeML *)
(* module int.ComputerDivision *)
(* syntax val div "quot (%1, %2)" *)
(* syntax val mod "%1 rem %2" *)
(* end *)
module array.Array
syntax type array "%1 array"
(* syntax exception OutOfBounds "Why3__Array.OutOfBounds" *) (* FIXME *)
syntax val ([]) "Array.sub %1 %2"
syntax val ([]<-) "Array.update %1 %2 %3"
syntax val length "Array.length %1"
syntax val defensive_get "Array.sub %1 %2"
syntax val defensive_set "Array.update %1 %2 %3"
syntax val make "Array.array %1 %2"
syntax val empty "Array.arrayEmpty %1"
(* syntax val append "Array.append %1 %2" *)
(* syntax val sub "Array.sub %1 (Z.to_int %2) (Z.to_int %3)" *)
(* syntax val copy "Array.copy %1" *)
(* syntax val fill "Array.fill %1 (Z.to_int %2) (Z.to_int %3) %4" *)
(* syntax val blit "Array.blit %1 (Z.to_int %2) %3 (Z.to_int %4) (Z.to_int %5)" *)
end
(* module mach.int.Int *)
(* syntax val ( / ) "Z.div %1 %2" *)
(* syntax val ( % ) "Z.rem %1 %2" *)
(* end *)
|
