1structure patricia_castsLib :> patricia_castsLib =
2struct
3
4(* interactive use:
5  app load ["patriciaLib", "patricia_castsSyntax"];
6*)
7
8open HolKernel Parse boolLib bossLib Q computeLib patriciaLib
9     patriciaTheory patricia_castsTheory patriciaSyntax patricia_castsSyntax;
10
11(* ------------------------------------------------------------------------- *)
12
13val emit_mesg = !Feedback.emit_MESG;
14val _ = Feedback.emit_MESG := false;
15
16val m = apropos;
17
18val ERR = mk_HOL_ERR "patricia_casts";
19
20(* ------------------------------------------------------------------------- *)
21
22fun dest_word_ptree t =
23let val sz = fcpLib.index_to_num (fst (dest_word_ptree_type (type_of t)))
24in
25  (sz, dest_ptree (dest_some_ptree t))
26end;
27
28fun mk_word_ptree (n, t) =
29  if every_leaf (fn k => fn _ =>
30                   (k = Arbnum.zero) orelse
31                   (Arbnum.<(Arbnum.log2 k, n))) t
32  then
33    mk_some_ptree(fcpLib.index_type n, mk_ptree t)
34  else
35    raise ERR "mk_word_ptree"
36              "At least one key is larger than the required word length.";
37
38(* ------------------------------------------------------------------------- *)
39
40val the_ptree_compset =
41  new_compset [THE_PTREE_def, THE_PTREE_SOME_PTREE, WordEmpty_def];
42
43val THE_PTREE_CONV = CBV_CONV the_ptree_compset;
44
45fun add_cast_ptree_compset compset =
46let open listTheory pred_setTheory in
47  add_thms [IMAGE_EMPTY, IMAGE_INSERT, IMAGE_UNION,
48            ADD_INSERT_WORD, ADD_INSERT_STRING,
49            stringTheory.ORD_CHR_COMPUTE, stringTheory.CHAR_EQ_THM, SKIP1_def,
50            string_to_num_def, num_to_string_def, num_to_string_string_to_num,
51            PEEKs_def, PEEKs_def, ADDs_def, ADD_LISTs_def, REMOVEs_def,
52            TRAVERSEs_def, KEYSs_def, IN_PTREEs_def, INSERT_PTREEs_def,
53            STRINGSET_OF_PTREE_def, PTREE_OF_STRINGSET_def,
54            PEEKw_def, FINDw_def, ADDw_def, ADD_LISTw_def, REMOVEw_def,
55            TRAVERSEw_def, KEYSw_def, TRANSFORMw_def, EVERY_LEAFw_def,
56            EXISTS_LEAFw_def, SIZEw_def, DEPTHw_def, IN_PTREEw_def,
57            INSERT_PTREEw_def, WORDSET_OF_PTREE_def, PTREE_OF_WORDSET_def]
58          compset;
59  add_conv (the_ptree_tm, 1, THE_PTREE_CONV) compset
60end;
61
62fun cast_ptree_compset () =
63let val compset = wordsLib.words_compset()
64    val _ = add_ptree_compset compset
65    val _ = add_cast_ptree_compset compset
66in
67  compset
68end;
69
70val CAST_PTREE_CONV = CBV_CONV (cast_ptree_compset());
71
72(* ------------------------------------------------------------------------- *)
73
74fun Define_mk_word_ptree (s1,s2) n t =
75let val _ = mk_word_ptree (n,t)
76    val thm1 = Define_mk_ptree s2 t
77    val tree = mk_some_ptree(fcpLib.index_type n, lhs (concl thm1))
78    val thm2 = Definition.new_definition(s1^"_def", mk_eq(mk_var(s1,Term.type_of tree), tree))
79    val _ = add_thms [thm2] the_compset
80    val _ = add_thms [thm2] the_ptree_compset
81in
82  (thm2, thm1)
83end;
84
85fun iDefine_mk_word_ptree s i t = Define_mk_word_ptree s (Arbnum.fromInt i) t;
86
87(* ------------------------------------------------------------------------- *)
88
89val _ = Feedback.emit_MESG := emit_mesg
90
91end
92