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
|
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
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
/-- Type quantifiers: n : Int -/
def foo (n : Int) : SailM (Bool × (BitVec 1) × Int × Nat × (BitVec 3)) := do
(pure ((← (undefined_bool ())), (← (undefined_bit ())), (← (undefined_int ())), (← (undefined_nat
())), (← (undefined_bitvector 3))))
/-- Type quantifiers: n : Int -/
def bar (n : Int) : SailM (Vector Int 4) := do
(undefined_vector 4 n)
def initialize_registers (_ : Unit) : Unit :=
()
def sail_model_init (x_0 : Unit) : Unit :=
(initialize_registers ())
end Out.Functions
|
