1
2(*List.app load ["bossLib","stringTheory","stringLib","HolBddLib","pairTheory","pred_setLib","listLib","CTL","pairSyntax","pairRules","pairTools","muTheory","boolSyntax","Drule","Tactical","Conv","Rewrite","Tactic","boolTheory","stringBinTreeTheory","computeLib"];*)
3
4(* balanced strict bin tree term. At the moment we support one-time construction and find on string keys only *)
5(* further, the string keys can only have dot, underscore, digits and upper/lower-case letters *)
6(* this is useful for efficiently representing maps with string domains as HOL terms *)
7
8structure stringBinTree =
9struct
10
11local
12
13open Globals HolKernel Parse
14
15open bossLib;
16open pairTheory;
17open pred_setTheory;
18open pred_setLib;
19open stringLib;
20open listTheory;
21open simpLib;
22open pairSyntax;
23open pairLib;
24open Binarymap;
25open PairRules;
26open pairTools;
27open boolSyntax;
28open Drule;
29open Tactical;
30open Conv;
31open Rewrite;
32open Tactic;
33open boolTheory;
34open listSyntax;
35open stringTheory;
36open boolSimps;
37open pureSimps;
38open listSimps;
39open numLib;
40open computeLib;
41
42fun term_to_string2 t = with_flag (show_types,false) term_to_string t;
43
44val ONCE_BETA_LET_CONV = (ONCE_DEPTH_CONV BETA_CONV) THENC (ONCE_DEPTH_CONV let_CONV);
45val no_beta_BOOL_ss = rewrites (frag_rewrites BOOL_ss) (* this is BOOL_ss w/o beta-reduction *)
46
47(*apply first arg(conv) to test part of the cond term which is on the rhs of the snd arg (an eq term)*)
48val RHS_COND_TEST_CONV = RHS_CONV o RATOR_CONV o RATOR_CONV o RAND_CONV
49
50fun rmid L = List.nth(L,(List.length L) div 2); (* return middle or right middle element *)
51
52(* take key list sorted in increasing order and return inorder traversal of corresponding balanced BST *)
53fun inorder [] = []
54|   inorder L = rmid(L)::(inorder(List.take(L,(List.length L) div 2)))@(inorder(List.drop(L,((List.length L) div 2)+1)))
55
56(* append a string of the minimum character, of the same length as the longest key (mxl), to all keys *)
57(* this is so that char access for all keys is well-defined, for all indices < mxl *)
58fun stuff_keys keys mxl =
59let  val stuffing = String.implode (List.tabulate(mxl,fn n => chr 33));
60     in  (stuffing,Listsort.sort String.compare (List.map (fn k => k^stuffing) keys)) end
61
62(* rnkv[i] gives the index within keys of the ith most discriminiting characeter *)
63(* clv[i] gives a list of all chars that occur at index i in the keys, with duplicates removed *)
64fun mk_rank keys mxl =
65  let  val cl0 = List.tabulate(mxl,fn n => Binaryset.empty Char.compare)
66       val cl = List.foldl (fn (k,acl) => List.foldr
67                        (fn ((bs,kc),acl2)=> (Binaryset.add(bs,kc))::acl2) [] (ListPair.zip(acl,explode k))) cl0 keys
68       val (_,rnk) = ListPair.unzip(List.rev(Listsort.sort (fn ((r1,i1),(r2,i2)) => Int.compare(r1,r2))
69                        (ListPair.zip(List.map (fn bs => Binaryset.numItems bs) cl,List.tabulate(mxl,fn n => n)))))
70       val rnkv = Vector.fromList rnk
71       val clv = Vector.fromList (List.map Binaryset.listItems cl)
72  in (rnkv,clv) end
73
74(* constructs a term (HD o TL^n) *)
75fun mk_list_nth n = List.foldl (fn (t,at) => ``^at o ^t``) ``HD:char list -> char``
76                                                        (List.tabulate(n,fn n => ``TL:char list -> char list``));
77
78fun string_char_swap s i j =
79        String.implode(List.map (fn (c,k) => if (k=i) then String.sub(s,j)
80                              else if (k=j) then String.sub(s,i) else c)
81          (ListPair.zip(String.explode s,List.tabulate(String.size s,fn n => n))))
82
83fun mk_leaf keymap ranks s mxl dummy =
84    let val idx = (List.tabulate(mxl,fn n => n))
85        val key = implode(List.filter (fn c => not(Char.compare(c,#"!")=EQUAL))
86                        (List.foldl (fn (i,al) => List.map
87                                (fn (j,c) => if (j=(Vector.sub(ranks,i))) then String.sub(s,i) else c)
88                                        (ListPair.zip(idx,al))) (List.tabulate(mxl,fn n => #"+")) idx)
89                  )
90
91        (*val _ = printVal mxl; val _ = print " mxl\n";
92        val _ = printVal ranks; val _ = print (" ranks\n");
93        val _ = printVal s; val _ = print (" s\n");
94        val _ = printVal key; val _ = print (" key\n");*)
95    in Binarymap.find(keymap,key) handle NotFound => dummy end
96
97(* chars at index i are all the same *)
98fun areSame k i = fst(List.foldl (fn (ky,(b,c)) => if (not (Option.isSome c)) then (b,SOME (List.nth(explode ky,i)))
99                                                   else if (Char.compare(Option.valOf c,List.nth(explode ky,i))=EQUAL)
100                                                        then (b,c)
101                                                        else (false,c)) (true,NONE) k)
102
103
104(* builds the BST for index i in the keys *)
105fun mk_subtree keymap ranks cl mxl ccl i s k dummy =
106    if (List.null ccl)
107    then mk_tree_aux keymap ranks cl mxl (i+1)
108                     (s^(if (List.null k) then "+" else Char.toString (String.sub(hd k,Vector.sub(ranks,i))))) k dummy
109    else let val (kl,kr) = List.partition (fn ky => String.sub(ky,Vector.sub(ranks,i))<(hd ccl)) k;
110             val dl = areSame kl (Vector.sub(ranks,i));
111             val dr = areSame kr (Vector.sub(ranks,i))
112             val lt = if dl then mk_tree_aux keymap ranks cl mxl (i+1)
113                                             (s^(if (List.null kl) then "+"
114                                                 else Char.toString(String.sub(hd kl,Vector.sub(ranks,i))))) kl dummy
115                      else mk_subtree keymap ranks cl mxl (List.take((tl ccl),(List.length ccl) div 2)) i s kl dummy
116             val rt = if dr then mk_tree_aux keymap ranks cl mxl (i+1)
117                                             (s^(if (List.null kr) then "+"
118                                                 else Char.toString(String.sub(hd kr,Vector.sub(ranks,i))))) kr dummy
119                      else mk_subtree keymap ranks cl mxl (List.drop((tl ccl),(List.length ccl) div 2)) i s kr dummy
120         in mk_cond(list_mk_comb(numSyntax.less_tm,[mk_comb(``ORD``,mk_comb(mk_list_nth(Vector.sub(ranks,i)),
121                                                              mk_var("x",``:char list``))),
122                                           numSyntax.mk_numeral(Arbnum.fromInt(ord(hd ccl)))]),lt,rt) end
123
124(* glues together the BST's returned from mk_subtree *)
125and mk_tree_aux keymap ranks cl mxl i s keys dummy =
126    if (i=mxl)
127    then mk_leaf keymap ranks s mxl dummy
128    else let val ccl = Vector.sub(cl,Vector.sub(ranks,i))
129         in if (((List.length ccl) = 1)  (* one-way branch, ignore *)
130                orelse (areSame keys (Vector.sub(ranks,i)))) (* redundant branching, ignore *)
131            then mk_tree_aux keymap ranks cl mxl (i+1)
132                             (s^(if (List.null keys) then "+" (* "+" indicates a dummy node *)
133                                 else Char.toString (String.sub(hd keys,Vector.sub(ranks,i))))) keys dummy
134            else mk_subtree keymap ranks cl mxl (inorder ccl) i s keys dummy end
135
136in
137
138(* builds Patricia trie term for the given map *)
139fun mk_tree abs keymap =
140  let val keys = fst(ListPair.unzip keymap)
141      val keymap2 = List.foldl (fn ((k,v),bm) => Binarymap.insert(bm,k,v)) (Binarymap.mkDict String.compare) keymap
142      (*val _ = printVal (Binarymap.listItems keymap2); val _ = print " keymap2\n";*)
143      val mxl =  List.foldl (fn (k,msz) => if (msz<(String.size k)) then (String.size k) else msz) 0 keys;
144      (*val _ = printVal mxl; val _ = print " mxl\n";*)
145      val (stuffing,sk) =  stuff_keys keys mxl
146     (*val _ = printVal sk; val _ = print " sk\n";*)
147      val (ranks,cl) = mk_rank sk mxl
148     (*val _ = printVal ranks; val _ = print " ranks\n";*)
149     (*val _ = printVal cl; val _ = print " cl\n";*)
150      val dummy = if (List.null keys) then ``ARB`` else ``ARB:^(ty_antiq(type_of (snd(hd keymap))))``
151      val tree = mk_let(mk_abs(mk_var("x",``:char list``),
152                               mk_tree_aux keymap2 ranks cl mxl 0 "" sk dummy),
153                                           ``EXPLODE (STRCAT t ^(fromMLstring stuffing))``)
154  in mk_abs(mk_var("t",``:string``),if isSome abs then mk_pabs(valOf abs,tree) else tree) end
155
156val find_CONV =
157    let val rws = new_compset [lazyfy_thm COND_CLAUSES,stringTheory.EXPLODE_EQNS,strictify_thm LET_DEF,strictify_thm literal_case_DEF,combinTheory.o_DEF,
158                               listTheory.HD,listTheory.TL,listTheory.APPEND,stringTheory.IMPLODE_EQNS,
159                               stringTheory.STRCAT]
160        val _ = add_conv (stringSyntax.ord_tm,1,stringLib.ORD_CHR_CONV) rws;
161        val _ = add_conv (numSyntax.less_tm,2,numLib.REDUCE_CONV) rws;
162    in CBV_CONV rws end
163end
164end;
165
166(*
167load "stringBinTree";
168open stringBinTree;
169val k1 = [("m",``0``),("v0_0",``1``),("u0_0",``2``)];
170val k2 = [("ac1",``1``),("ac",``2``),("bc",``3``),("cc",``4``)];
171val ap = ["m","v2_2","v2_1","v2_0","v1_2","v1_1","v1_0","v0_2","v0_1","v0_0","u2_2","u2_1","u2_0","u1_2","u1_1","u1_0","u0_2","u0_1","u0_0"];
172val k3 = List.map (fn s => (s,mk_var(s,``:bool``))) ap;
173*)
174