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
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
|
(**************************************************************************)
(* Sail *)
(* *)
(* Copyright (c) 2013-2017 *)
(* Kathyrn Gray *)
(* Shaked Flur *)
(* Stephen Kell *)
(* Gabriel Kerneis *)
(* Robert Norton-Wright *)
(* Christopher Pulte *)
(* Peter Sewell *)
(* Alasdair Armstrong *)
(* Brian Campbell *)
(* Thomas Bauereiss *)
(* Anthony Fox *)
(* Jon French *)
(* Dominic Mulligan *)
(* Stephen Kell *)
(* Mark Wassell *)
(* *)
(* All rights reserved. *)
(* *)
(* This software was developed by the University of Cambridge Computer *)
(* Laboratory as part of the Rigorous Engineering of Mainstream Systems *)
(* (REMS) project, funded by EPSRC grant EP/K008528/1. *)
(* *)
(* Redistribution and use in source and binary forms, with or without *)
(* modification, are permitted provided that the following conditions *)
(* are met: *)
(* 1. Redistributions of source code must retain the above copyright *)
(* notice, this list of conditions and the following disclaimer. *)
(* 2. Redistributions in binary form must reproduce the above copyright *)
(* notice, this list of conditions and the following disclaimer in *)
(* the documentation and/or other materials provided with the *)
(* distribution. *)
(* *)
(* THIS SOFTWARE IS PROVIDED BY THE AUTHOR AND CONTRIBUTORS ``AS IS'' *)
(* AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED *)
(* TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A *)
(* PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHOR OR *)
(* CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, *)
(* SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT *)
(* LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF *)
(* USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND *)
(* ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, *)
(* OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT *)
(* OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF *)
(* SUCH DAMAGE. *)
(**************************************************************************)
module Big_int = Nat_big_num
type bit = B0 | B1
type value =
| V_vector of value list
| V_list of value list
| V_int of Big_int.num
| V_bool of bool
| V_bit of bit
| V_tuple of value list
| V_unit
| V_string of string
| V_ctor of string * value list
let rec string_of_value = function
| V_vector _ -> "VEC"
| V_bool true -> "true"
| V_bool false -> "false"
| V_bit B0 -> "bitzero"
| V_bit B1 -> "bitone"
| V_int n -> Big_int.to_string n
| V_tuple vals -> "(" ^ Util.string_of_list ", " string_of_value vals ^ ")"
| V_list vals -> "[" ^ Util.string_of_list ", " string_of_value vals ^ "]"
| V_unit -> "()"
| V_string str -> "\"" ^ str ^ "\""
| V_ctor (str, vals) -> str ^ "(" ^ Util.string_of_list ", " string_of_value vals ^ ")"
let eq_value v1 v2 = string_of_value v1 = string_of_value v2
let coerce_bit = function
| V_bit b -> b
| _ -> assert false
let coerce_ctor = function
| V_ctor (str, vals) -> (str, vals)
| _ -> assert false
let coerce_bool = function
| V_bool b -> b
| _ -> assert false
let and_bool = function
| [v1; v2] -> V_bool (coerce_bool v1 && coerce_bool v2)
| _ -> assert false
let or_bool = function
| [v1; v2] -> V_bool (coerce_bool v1 || coerce_bool v2)
| _ -> assert false
let print = function
| [v] -> print_endline (string_of_value v |> Util.red |> Util.clear); V_unit
| _ -> assert false
let tuple_value (vs : value list) : value = V_tuple vs
let coerce_tuple = function
| V_tuple vs -> vs
| _ -> assert false
let coerce_listlike = function
| V_tuple vs -> vs
| V_list vs -> vs
| _ -> assert false
let coerce_cons = function
| V_list (v :: vs) -> Some (v, vs)
| V_list [] -> None
| _ -> assert false
let unit_value = V_unit
module StringMap = Map.Make(String)
let primops =
List.fold_left
(fun r (x, y) -> StringMap.add x y r)
StringMap.empty
[ ("and_bool", and_bool);
("or_bool", or_bool);
("print_endline", print);
]
|
