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
|
val internal_pick = monadic {_: "internal_pick"}: forall ('a : Type).
list('a) -> 'a
val undefined_int = monadic {_: "undefined_int"}: unit -> int
default Order dec
val mult_atom = pure {ocaml: "mult", interpreter: "mult", lem: "integerMult", c: "mult_int", coq: "Z.mul"}: forall 'n 'm.
(int('n), int('m)) -> int('n * 'm)
$sail_internal
enum e2 = {GHI, JKL}
val undefined_e2 : unit -> e2
function undefined_e2 () = internal_pick([|GHI, JKL|])
struct s1 = {fA : int, fB : e2}
val undefined_s1 : unit -> s1
function undefined_s1 () = struct { fA = undefined_int(), fB = undefined_e2() }
struct s3 = {fE : s1, fF : int}
val undefined_s3 : unit -> s3
function undefined_s3 () = struct { fE = undefined_s1(), fF = undefined_int() }
val f : int -> int
function f x = mult_atom(2, x)
val k : int -> int
function k x = {
var s : s3 = undefined_s3();
s = { s with fF = x };
f(s.fF)
}
|
