Model.Config

1module Model.Config
2
3family ModelWord32 : Type 0
4constructor ModelWord32Value
5field unrestricted modelWord32Byte0 : Byte
6field unrestricted modelWord32Byte1 : Byte
7field unrestricted modelWord32Byte2 : Byte
8field unrestricted modelWord32Byte3 : Byte
9
10end-family
11
12family ModelBoolean : Type 0
13constructor ModelFalse
14constructor ModelTrue
15
16end-family
17
18def modelWord32 =
19  (lambda unrestricted byte0 : Byte .
20    (lambda unrestricted byte1 : Byte .
21      (lambda unrestricted byte2 : Byte .
22        (lambda unrestricted byte3 : Byte .
23          (constructor ModelWord32 ModelWord32Value byte0 byte1 byte2 byte3)))))
24
25def modelWord32Bytes =
26  (lambda unrestricted value : (family ModelWord32) .
27    (eliminate
28      ModelWord32
29      (lambda unrestricted motiveValue : (family ModelWord32) . Bytes)
30      value
31      (branch
32        ModelWord32Value
33        byte0
34        byte1
35        byte2
36        byte3
37        .
38        (bytes-cons byte0 (bytes-cons byte1 (bytes-cons byte2 (bytes-cons byte3 b"")))))))
39
40def modelWord32One =
41  (constructor ModelWord32 ModelWord32Value (byte 1) (byte 0) (byte 0) (byte 0))
42
43def modelWord32Four =
44  (constructor ModelWord32 ModelWord32Value (byte 4) (byte 0) (byte 0) (byte 0))
45
46def modelWord32Sixteen =
47  (constructor ModelWord32 ModelWord32Value (byte 16) (byte 0) (byte 0) (byte 0))
48
49def modelWord32SixtyFour =
50  (constructor ModelWord32 ModelWord32Value (byte 64) (byte 0) (byte 0) (byte 0))
51
52def modelWord32TwoHundredFiftySix =
53  (constructor ModelWord32 ModelWord32Value (byte 0) (byte 1) (byte 0) (byte 0))
54
55def modelWord32OneThousandTwentyFour =
56  (constructor ModelWord32 ModelWord32Value (byte 0) (byte 4) (byte 0) (byte 0))
57
58def modelWord32FourThousandNinetySix =
59  (constructor ModelWord32 ModelWord32Value (byte 0) (byte 16) (byte 0) (byte 0))
60
61def modelWord32TenThousandTwoHundredForty =
62  (constructor ModelWord32 ModelWord32Value (byte 0) (byte 40) (byte 0) (byte 0))
63
64def modelWord32TwelveThousandTwoHundredEightyEight =
65  (constructor ModelWord32 ModelWord32Value (byte 0) (byte 48) (byte 0) (byte 0))