Skip to content

Commit 5624f69

Browse files
oskarabrahamssonoskarabrahamsson
committed
Add Set module to basis
This commit adds a new Set module to basis. The module is based on the same balanced map as Map.map, but is translated in a separate theory (SetProg) to avoid clashes with translator theorem names for values with identical (unqualified) names within the theory.
1 parent edb9197 commit 5624f69

10 files changed

+332
-15
lines changed

‎basis/HashtableProgScript.sml

+2-2
Original file line numberDiff line numberDiff line change
@@ -3,10 +3,10 @@
33
*)
44
open preamble
55
ml_translatorLib ml_progLib basisFunctionsLib
6-
MapProgTheory
6+
SetProgTheory
77

88
val _ = new_theory "HashtableProg"
9-
val _ = translation_extends "MapProg"
9+
val _ = translation_extends "SetProg"
1010
val () = ml_prog_update(open_module "Hashtable");
1111

1212
(*Local structure:

‎basis/MapProgScript.sml

+29-11
Original file line numberDiff line numberDiff line change
@@ -31,32 +31,42 @@ val _ = translate balanceL_def;
3131
val _ = translate balanceR_def;
3232
val _ = translate deleteFindMax_def;
3333

34-
val deleteFindmax_side_thm = Q.prove (
35-
`!m. m ≠ Tip ⇒ deletefindmax_side m`,
34+
Theorem deleteFindmax_side_thm[local]:
35+
!m. m ≠ Tip ⇒ deletefindmax_side m
36+
Proof
3637
ho_match_mp_tac deleteFindMax_ind >>
3738
ONCE_REWRITE_TAC [theorem "deletefindmax_side_def"] >>
3839
rw [] >>
3940
ONCE_REWRITE_TAC [theorem "deletefindmax_side_def"] >>
4041
rw [] >>
41-
metis_tac []) |> update_precondition;
42+
metis_tac []
43+
QED
44+
val _ = update_precondition deleteFindmax_side_thm;
4245

4346
val _ = translate deleteFindMin_def;
4447

45-
val deleteFindmin_side_thm = Q.prove (
46-
`!m. m ≠ Tip ⇒ deletefindmin_side m`,
48+
Theorem deleteFindmin_side_thm[local]:
49+
!m. m ≠ Tip ⇒ deletefindmin_side m
50+
Proof
4751
ho_match_mp_tac deleteFindMin_ind >>
4852
ONCE_REWRITE_TAC [theorem "deletefindmin_side_def"] >>
4953
rw [] >>
5054
ONCE_REWRITE_TAC [theorem "deletefindmin_side_def"] >>
5155
rw [] >>
52-
metis_tac []) |> update_precondition;
56+
metis_tac []
57+
QED
58+
val _ = update_precondition deleteFindmin_side_thm;
5359

5460
val _ = translate glue_def;
5561

56-
val glue_side_thm = Q.prove (
57-
`!m n. glue_side m n`,
62+
Theorem glue_side_thm[local]:
63+
!m n. glue_side m n
64+
Proof
5865
rw [fetch "-" "glue_side_def"] >>
59-
metis_tac [deleteFindmin_side_thm, deleteFindmax_side_thm, balanced_map_distinct]) |> update_precondition;
66+
metis_tac [deleteFindmin_side_thm, deleteFindmax_side_thm,
67+
balanced_map_distinct]
68+
QED
69+
val _ = update_precondition glue_side_thm;
6070

6171
val _ = translate trim_help_greater_def;
6272
val _ = translate trim_help_lesser_def;
@@ -113,10 +123,13 @@ val _ = ml_prog_update (open_module "Map");
113123

114124
(* provides the Map.map name for the map type *)
115125
val _ = ml_prog_update (add_dec
116-
``Dtabbrev unknown_loc ["'a";"'b"] "map" (Atapp [Atvar "'a"; Atvar "'b"] (Short "map"))`` I);
126+
``Dtabbrev unknown_loc ["'a";"'b"] "map"
127+
(Atapp [Atvar "'a"; Atvar "'b"] (Short "map"))`` I);
117128

118129
val _ = next_ml_names := ["lookup"];
119130
val _ = translate mlmapTheory.lookup_def;
131+
val _ = next_ml_names := ["member"];
132+
val _ = translate mlmapTheory.member_def;
120133
val _ = next_ml_names := ["insert"];
121134
val _ = translate mlmapTheory.insert_def;
122135
val _ = next_ml_names := ["delete"];
@@ -127,6 +140,8 @@ val _ = next_ml_names := ["size"];
127140
val _ = translate mlmapTheory.size_def;
128141
val _ = next_ml_names := ["empty"];
129142
val _ = translate mlmapTheory.empty_def;
143+
val _ = next_ml_names := ["singleton"];
144+
val _ = translate mlmapTheory.singleton_def;
130145
val _ = next_ml_names := ["union"];
131146
val _ = translate mlmapTheory.union_def;
132147
val _ = next_ml_names := ["unionWith"];
@@ -155,12 +170,15 @@ val _ = next_ml_names := ["filterWithKey"];
155170
val _ = translate mlmapTheory.filterWithKey_def;
156171
val _ = next_ml_names := ["filter"];
157172
val _ = translate mlmapTheory.filter_def;
173+
val _ = next_ml_names := ["compare"];
174+
val _ = translate mlmapTheory.compare_def;
158175

159176
val _ = ml_prog_update (close_module NONE);
160177

161178
(* this is here so that the type name is accessible without the full name *)
162179
val _ = ml_prog_update (add_dec
163-
``Dtabbrev unknown_loc ["'a";"'b"] "map" (Atapp [Atvar "'a"; Atvar "'b"] (Short "map"))`` I);
180+
``Dtabbrev unknown_loc ["'a";"'b"] "map"
181+
(Atapp [Atvar "'a"; Atvar "'b"] (Short "map"))`` I);
164182

165183
val _ = ml_prog_update close_local_block;
166184

‎basis/README.md

+4
Original file line numberDiff line numberDiff line change
@@ -77,6 +77,10 @@ forcing a full GC to run, a function for producing debug output.
7777
[RuntimeProofScript.sml](RuntimeProofScript.sml):
7878
Proof about the exit function in the Runtime module.
7979

80+
[SetProgScript.sml](SetProgScript.sml):
81+
This module contains CakeML code implementing a functional set type
82+
using a self-balancing binary tree.
83+
8084
[StringProgScript.sml](StringProgScript.sml):
8185
Module about the built-in string tyoe.
8286

‎basis/SetProgScript.sml

+163
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,163 @@
1+
(*
2+
This module contains CakeML code implementing a functional set type
3+
using a self-balancing binary tree.
4+
*)
5+
open preamble
6+
ml_translatorLib ml_translatorTheory ml_progLib
7+
balanced_mapTheory MapProgTheory basisFunctionsLib
8+
9+
val _ = new_theory "SetProg"
10+
11+
val _ = translation_extends "MapProg";
12+
13+
val _ = ml_prog_update open_local_block;
14+
15+
val _ = (use_full_type_names := false);
16+
val _ = register_type ``:'a mlset$mlset``;
17+
val _ = (use_full_type_names := true);
18+
19+
val _ = next_ml_names := ["size", "singleton"];
20+
val _ = translate size_def;
21+
val _ = translate singleton_def;
22+
23+
(* Helpers *)
24+
25+
val _ = translate FOLDL;
26+
val _ = translate ratio_def;
27+
val _ = translate delta_def;
28+
val _ = translate balanceL_def;
29+
val _ = translate balanceR_def;
30+
val _ = translate deleteFindMax_def;
31+
32+
Theorem deleteFindmax_side_thm[local]:
33+
!m. m ≠ Tip ⇒ deletefindmax_side m
34+
Proof
35+
ho_match_mp_tac deleteFindMax_ind >>
36+
ONCE_REWRITE_TAC [theorem "deletefindmax_side_def"] >>
37+
rw [] >>
38+
ONCE_REWRITE_TAC [theorem "deletefindmax_side_def"] >>
39+
rw [] >>
40+
metis_tac []
41+
QED
42+
val _ = update_precondition deleteFindmax_side_thm;
43+
44+
val _ = translate deleteFindMin_def;
45+
46+
Theorem deleteFindmin_side_thm[local]:
47+
!m. m ≠ Tip ⇒ deletefindmin_side m
48+
Proof
49+
ho_match_mp_tac deleteFindMin_ind >>
50+
ONCE_REWRITE_TAC [theorem "deletefindmin_side_def"] >>
51+
rw [] >>
52+
ONCE_REWRITE_TAC [theorem "deletefindmin_side_def"] >>
53+
rw [] >>
54+
metis_tac []
55+
QED
56+
val _ = update_precondition deleteFindmin_side_thm;
57+
58+
val _ = translate glue_def;
59+
60+
Theorem glue_side_thm[local]:
61+
!m n. glue_side m n
62+
Proof
63+
rw [fetch "-" "glue_side_def"] >>
64+
metis_tac [deleteFindmin_side_thm, deleteFindmax_side_thm,
65+
balanced_map_distinct]
66+
QED
67+
val _ = update_precondition glue_side_thm;
68+
69+
val _ = translate trim_help_greater_def;
70+
val _ = translate trim_help_lesser_def;
71+
val _ = translate trim_help_middle_def;
72+
val _ = translate trim_def;
73+
val _ = translate insertMin_def;
74+
val _ = translate insertMax_def;
75+
val _ = translate bin_def;
76+
val _ = translate link_def;
77+
val _ = translate link2_def;
78+
val _ = translate filterLt_help_def;
79+
val _ = translate filterLt_def;
80+
val _ = translate filterGt_help_def;
81+
val _ = translate filterGt_def;
82+
val _ = translate insertR_def;
83+
val _ = translate hedgeUnion_def;
84+
val _ = next_ml_names := ["lookup"];
85+
val _ = translate lookup_def;
86+
val _ = translate hedgeUnionWithKey_def;
87+
val _ = translate splitLookup_def;
88+
val _ = translate submap'_def;
89+
90+
(* Exported functions *)
91+
val _ = next_ml_names :=
92+
["null", "member", "empty", "insert", "delete", "union", "foldrWithKey",
93+
"toAscList", "compare", "isSubmapOfBy", "isSubmapOf", "fromList",
94+
"filterWithKey", "all", "exists"];
95+
val _ = translate null_def;
96+
val _ = translate member_def;
97+
val _ = translate empty_def;
98+
val _ = translate insert_def;
99+
val _ = translate delete_def;
100+
val _ = translate union_def;
101+
val _ = translate foldrWithKey_def;
102+
val _ = translate toAscList_def;
103+
val _ = translate compare_def;
104+
val _ = translate isSubmapOfBy_def;
105+
val _ = translate isSubmapOf_def;
106+
val _ = translate fromList_def;
107+
val _ = translate filterWithKey_def;
108+
val _ = translate every_def;
109+
val _ = translate exists_def;
110+
111+
val _ = ml_prog_update open_local_in_block;
112+
113+
val _ = ml_prog_update (open_module "Set");
114+
115+
(* provides the Set.set name for the set type *)
116+
val _ = ml_prog_update (add_dec
117+
``Dtabbrev unknown_loc ["'a"] "set" (Atapp [Atvar "'a"] (Short "mlset"))`` I);
118+
119+
val _ = next_ml_names := ["singleton"];
120+
val _ = translate mlsetTheory.singleton_def;
121+
val _ = next_ml_names := ["member"];
122+
val _ = translate mlsetTheory.member_def;
123+
val _ = next_ml_names := ["delete"];
124+
val _ = translate mlsetTheory.delete_def;
125+
val _ = next_ml_names := ["union"];
126+
val _ = translate mlsetTheory.union_def;
127+
val _ = next_ml_names := ["isSubset"];
128+
val _ = translate mlsetTheory.isSubset_def;
129+
val _ = next_ml_names := ["compare"];
130+
val _ = translate mlsetTheory.compare_def;
131+
val _ = next_ml_names := ["all"];
132+
val _ = translate mlsetTheory.all_def;
133+
val _ = next_ml_names := ["exists"];
134+
val _ = translate mlsetTheory.exists_def;
135+
val _ = next_ml_names := ["translate"];
136+
val _ = translate mlsetTheory.translate_def;
137+
val _ = next_ml_names := ["map"];
138+
val _ = translate mlsetTheory.map_def;
139+
val _ = next_ml_names := ["filter"];
140+
val _ = translate mlsetTheory.filter_def;
141+
val _ = next_ml_names := ["fromList"];
142+
val _ = translate mlsetTheory.fromList_def;
143+
val _ = next_ml_names := ["toList"];
144+
val _ = translate mlsetTheory.toList_def;
145+
val _ = next_ml_names := ["null"];
146+
val _ = translate mlsetTheory.null_def;
147+
val _ = next_ml_names := ["size"];
148+
val _ = translate mlsetTheory.size_def;
149+
val _ = next_ml_names := ["fold"];
150+
val _ = translate mlsetTheory.fold_def;
151+
val _ = next_ml_names := ["empty"];
152+
val _ = translate mlsetTheory.empty_def;
153+
val _ = next_ml_names := ["insert"];
154+
val _ = translate mlsetTheory.insert_def;
155+
156+
val _ = ml_prog_update (close_module NONE);
157+
158+
val _ = ml_prog_update (add_dec
159+
``Dtabbrev unknown_loc ["'a"] "set" (Atapp [Atvar "'a"] (Short "mlset"))`` I);
160+
161+
val _ = ml_prog_update close_local_block;
162+
163+
val _ = export_theory ();

‎basis/dependency-order

+1
Original file line numberDiff line numberDiff line change
@@ -23,6 +23,7 @@ Word8
2323
Word8Array
2424
Array
2525
Map
26+
Set
2627
Hashtable
2728
CommandLine
2829
Double

‎basis/pure/README.md

+5
Original file line numberDiff line numberDiff line change
@@ -31,6 +31,11 @@ Types and pure functions for pretty printing
3131
[mlratScript.sml](mlratScript.sml):
3232
Pure functions for the Rat module.
3333

34+
[mlsetScript.sml](mlsetScript.sml):
35+
Pure functions for the Set module.
36+
This file defines a wrapper around the balanced_map type. See
37+
$HOLDIR/examples/balanced_bst/osetScript.sml.
38+
3439
[mlstringLib.sml](mlstringLib.sml):
3540
More ML functions for manipulating HOL terms involving mlstrings.
3641

‎basis/pure/mlmapScript.sml

+13
Original file line numberDiff line numberDiff line change
@@ -102,6 +102,19 @@ Definition exists_def:
102102
exists f (Map cmp t) = balanced_map$exists f t
103103
End
104104

105+
Definition member_def:
106+
member k (Map cmp t) = balanced_map$member cmp k t
107+
End
108+
109+
Definition singleton_def:
110+
singleton cmp k v = Map cmp (balanced_map$singleton k v)
111+
End
112+
113+
Definition compare_def:
114+
compare vcmp (Map cmp m1) (Map _ m2) =
115+
balanced_map$compare cmp vcmp m1 m2
116+
End
117+
105118
(* definitions for proofs *)
106119

107120
Definition map_ok_def:

0 commit comments

Comments
 (0)