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