forked from CakeML/cakeml
-
Notifications
You must be signed in to change notification settings - Fork 0
/
simple_bstProgScript.sml
71 lines (56 loc) · 1.76 KB
/
simple_bstProgScript.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
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
(*
Using the CakeML translator to produce a verified deep embedding of the
simple BST implementation.
*)
open preamble
ml_progLib ml_translatorLib
simple_bstTheory
val _ = new_theory "simple_bstProg";
(*
To translate a HOL function to CakeML, call translate on its definition. For
example, let us start by translating the singleton function from
simple_bstTheory.
The necessary datatypes (('a,'b) btree in this case) will be automatically
translated first.
The result is a certificate theorem indicating that the CakeML value
(singleton_v) that results from running the generated code for declaring the
CakeML version of the singleton function refines the HOL function singleton.
*)
val res = translate singleton_def;
(*
The translator maintains state, containing the entire current translated program.
For each top-level declaration in this program, the translator also defines a
constant representing the state of the CakeML semantics after this
As a side effect of calling translate, the program is appended to the state.
Let us look at the code in the current program.
*)
(* TODO: this is too cumbersome! *)
fun get_current_prog() =
let
val state = get_ml_prog_state()
val state_thm =
state |> ml_progLib.remove_snocs
|> ml_progLib.clean_state
|> get_thm
val current_prog =
state_thm
|> concl
|> strip_comb |> #2
|> el 3
in current_prog end
(*
get_current_prog()
*)
(*
To print in concrete syntax:
astPP.enable_astPP();
To remove this pretty-printing:
astPP.disable_astPP();
*)
val res = translate insert_def;
val res = translate lookup_def;
(*
val res = translate member_def;
*)
(* TODO: use of certificate theorem to show something about the generated code? *)
val _ = export_theory();