blob: 5e7768531b22830358ebb6993bb9e5b481b16662 (
plain)
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
|
(************************************************************)
(* Support for toFromInterp *)
(************************************************************)
open Sail_lib;;
open Value;;
type vector_order =
| Order_inc
| Order_dec
let zunitFromInterpValue v = match v with
| V_unit -> ()
| _ -> failwith "invalid interpreter value for unit"
let zunitToInterpValue () = V_unit
let unitFromInterpValue = zunitFromInterpValue
let unitToInterpValue = zunitToInterpValue
let zatomFromInterpValue typq_'n v = match v with
| V_int i when typq_'n = i -> i
| _ -> failwith "invalid interpreter value for atom"
let zatomToInterpValue typq_'n v =
assert (typq_'n = v);
V_int v
let atomFromInterpValue = zatomFromInterpValue
let atomToInterpValue = zatomToInterpValue
let zintFromInterpValue v = match v with
| V_int i -> i
| _ -> failwith "invalid interpreter value for int"
let zintToInterpValue v = V_int v
let intFromInterpValue = zintFromInterpValue
let intToInterpValue = zintToInterpValue
let znatFromInterpValue v = match v with
| V_int i when i >= Big_int.zero -> i
| _ -> failwith "invalid interpreter value for nat"
let znatToInterpValue v =
assert (v >= Big_int.zero);
V_int v
let natFromInterpValue = znatFromInterpValue
let natToInterpValue = znatToInterpValue
let zboolFromInterpValue v = match v with
| V_bool b -> b
| _ -> failwith "invalid interpreter value for bool"
let zboolToInterpValue v = V_bool v
let boolFromInterpValue = zboolFromInterpValue
let boolToInterpValue = zboolToInterpValue
let zstringFromInterpValue v = match v with
| V_string s -> s
| _ -> failwith "invalid interpreter value for string"
let zstringToInterpValue v = V_string v
let stringFromInterpValue = zstringFromInterpValue
let stringToInterpValue = zstringToInterpValue
let zlistFromInterpValue typq_'a v = match v with
| V_list vs -> List.map typq_'a vs
| _ -> failwith "invalid interpreter value for list"
let zlistToInterpValue typq_'a v = V_list (List.map typq_'a v)
let listFromInterpValue = zlistFromInterpValue
let listToInterpValue = zlistToInterpValue
let zvectorFromInterpValue typq_'n typq_'ord typq_'a v = match v with
| V_vector vs ->
assert (Big_int.of_int (List.length vs) = typq_'n);
List.map typq_'a vs
| _ -> failwith "invalid interpreter value for vector"
let zvectorToInterpValue typq_'n typq_'ord typq_'a v =
assert (Big_int.of_int (List.length v) = typq_'n);
V_vector (List.map typq_'a v)
let vectorFromInterpValue = zvectorFromInterpValue
let vectorToInterpValue = zvectorToInterpValue
let zbitFromInterpValue v = match v with
| V_bit b -> b
| _ -> failwith "invalid interpreter value for bit"
let zbitToInterpValue v = V_bit v
let bitFromInterpValue = zbitFromInterpValue
let bitToInterpValue = zbitToInterpValue
|
