forked from CakeML/cakeml
-
Notifications
You must be signed in to change notification settings - Fork 0
/
UnsafeProgScript.sml
35 lines (27 loc) · 1.12 KB
/
UnsafeProgScript.sml
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
(*
This module defines functions for accessing CakeML's unsafe
array primitives, i.e. primitives that crash if the index is
out of bounds. This is not part of the basis.
This script defines four functions:
Unsafe.sub -- unsafe version of Array.sub
Unsafe.update -- unsafe version of Array.update
Unsafe.w8sub -- unsafe version of Word8Array.sub
Unsafe.w8update -- unsafe version of Word8Array.update
*)
open preamble ml_translatorLib ml_progLib basisFunctionsLib
basisProgTheory
val _ = new_theory"UnsafeProg"
val _ = translation_extends"basisProg"
val () = ml_prog_update (open_module "Unsafe");
val () = append_decs
``[mk_binop "sub" Asub_unsafe;
Dlet unknown_loc (Pvar "update")
(Fun "x" (Fun "y" (Fun "z"
(App Aupdate_unsafe [Var (Short "x"); Var (Short "y"); Var (Short "z")])))) ]``;
val () = append_decs
``[mk_binop "w8sub" Aw8sub_unsafe;
Dlet unknown_loc (Pvar "w8update")
(Fun "x" (Fun "y" (Fun "z"
(App Aw8update_unsafe [Var (Short "x"); Var (Short "y"); Var (Short "z")])))) ]``;
val _ = ml_prog_update (close_module NONE);
val _ = export_theory ()