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