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
|
import Out.Sail.Sail
import Out.Sail.BitVec
open PreSail
set_option maxHeartbeats 1_000_000_000
set_option maxRecDepth 1_000_000
set_option linter.unusedVariables false
set_option match.ignoreUnusedAlts true
open Sail
structure rectangle where
width : Int
height : Int
deriving BEq, Inhabited, Repr
structure circle where
radius : Int
deriving BEq, Inhabited, Repr
inductive shape where
| Rectangle (_ : rectangle)
| Circle (_ : circle)
deriving Inhabited, BEq, Repr
/-- Type quantifiers: k_a : Type -/
inductive my_option (k_a : Type) where
| MySome (_ : k_a)
| MyNone (_ : Unit)
deriving Inhabited, BEq, Repr
abbrev Register := PEmpty
abbrev RegisterType : Register -> Type := PEmpty.elim
abbrev exception := Unit
abbrev SailM := PreSailM RegisterType trivialChoiceSource exception
XXXXXXXXX
import Out.Sail.Sail
import Out.Sail.BitVec
import Out.Sail.IntRange
import Out.Defs
import Out.Specialization
import Out.FakeReal
set_option maxHeartbeats 1_000_000_000
set_option maxRecDepth 1_000_000
set_option linter.unusedVariables false
set_option match.ignoreUnusedAlts true
open Sail
namespace Out.Functions
open shape
open my_option
def undefined_rectangle (_ : Unit) : SailM rectangle := do
(pure { width := (← (undefined_int ()))
height := (← (undefined_int ())) })
def undefined_circle (_ : Unit) : SailM circle := do
(pure { radius := (← (undefined_int ())) })
/-- Type quantifiers: k_a : Type -/
def is_none (opt : (my_option k_a)) : Bool :=
match opt with
| .MySome _ => false
| .MyNone () => true
/-- Type quantifiers: k_a : Type -/
def use_is_none (opt : (my_option k_a)) : Bool :=
(is_none opt)
def initialize_registers (_ : Unit) : Unit :=
()
def sail_model_init (x_0 : Unit) : Unit :=
(initialize_registers ())
end Out.Functions
|
