1open HolKernel Parse boolLib bossLib sptreeSyntax testutils 2open totoTheory totoTacs tcTacs enumTacs fmapalTacs; 3open alist_treeLib 4 5fun optionToString f NONE = "NONE" 6 | optionToString f (SOME x) = "SOME("^f x^")" 7fun pairToString f g (x,y) = "(" ^ f x ^ ", " ^ g y ^ ")" 8 9val _ = tprint "Check that finite maps have plausible size in TypeBase" 10val _ = require_msg 11 (check_result (fn (t,th) => null (free_vars t))) 12 (pairToString term_to_string thm_to_string) TypeBase.size_of 13 ���:'a |-> 'b��� 14 15fun testeval (s, t, expected) = 16 let 17 val _ = tprint s 18 in 19 require_msg (check_result (aconv expected)) term_to_string 20 (rhs o concl o EVAL) t 21 end 22 23val _ = tprint "sptreeSyntax.fromList" 24val tm1 = 25 fromList (List.tabulate (100, fn i => numSyntax.term_of_int (2 * i))) 26 handle HOL_ERR _ => (die "FAILED"; boolSyntax.T) 27val _ = OK() 28val _ = tprint "sptreeSytax.fromAList" 29val tm2 = 30 fromAList 31 (List.tabulate 32 (100, fn i => (Arbnum.fromInt (2 * i), numSyntax.term_of_int i))) 33 handle HOL_ERR _ => (die "FAILED"; boolSyntax.T) 34val _ = OK() 35 36 37val _ = app testeval [ 38 ("EVAL fromAList", 39 ``fromAList [(23746, a:num); (73246, b); (912, c); (0, d)] = 40 fromAList [(0, d); (73246, b); (23746, a:num); (912, c)]``, 41 boolSyntax.T), 42 ("EVAL fromList", 43 ``fromList [a;b;c;d:num]``, 44 ``BS (LS c) (a:num) (BS LN b (LS d))``), 45 ("EVAL wf o fromList", ``wf ^tm1``, boolSyntax.T), 46 ("EVAL wf o fromAList", ``wf ^tm2``, boolSyntax.T)] 47 48val _ = temp_add_sptree_printer () 49val _ = remove_sptree_printer () 50val _ = temp_add_sptree_printer () 51 52fun tpp' (i,out) = 53 tpp_expected {testf = standard_tpp_message, input = i, output = out} 54val _ = app tpp' [ 55 ("BS (LS c) (a:num) (BS LN b (LS d))", "sptree$fromList [a; b; c; d]"), 56 ("BS LN (a:num) (BS LN b (LS d))", "sptree$fromAList [(0,a); (1,b); (3,d)]") 57] 58 59(* File: enumfDemo Author: F. Lockwood Morris created: 17 Dec. 2013 *) 60 61(* A small example exercising much of the finite-sets-and-maps package 62 via computation of a transitive closure of a relation whose element 63 type is string # num. *) 64 65(* Start with the Hasse diagram of the relation of lineal descent 66 on nine of the Romanov emperors. *) 67 68val RomHasse = 69``fmap [(("PETER", 1), {("PETER", 3)}); 70 (("PETER", 3), {("PAUL", 1)}); 71 (("CATHERINE", 2), {("PAUL", 1)}); 72 (("PAUL", 1), {("ALEXANDER", 1); ("NICHOLAS", 1)}); 73 (("NICHOLAS", 1), {("ALEXANDER", 2)}); 74 (("ALEXANDER", 2), {("ALEXANDER", 3)}); 75 (("ALEXANDER", 3), {("NICHOLAS", 2)})]``; 76 77val tsarto_CONV = lextoto_CONV stringto_CONV numto_CONV; 78 79val RomH = ENUF_CONV tsarto_CONV ``stringto lextoto numto`` RomHasse; 80 81val tsar_tc = ``(FMAP_TO_RELN ^(rand (concl RomH)))^+``; 82 83val tsar_anc_thm = Count.apply (TC_CONV tsarto_CONV) tsar_tc; 84(* 21401 primitive inferences *) 85 86val tsar_enum_fmap = Count.apply (FMAPAL_TO_fmap_CONV tsarto_CONV) 87 (rand (rand (concl tsar_anc_thm))); 88(* 912 primitive inferences *) 89 90val alist = 91rand (concl 92 (Count.apply (MAP_ELEM_CONV (RAND_CONV (ENUMERAL_TO_DISPLAY_CONV tsarto_CONV))) 93 (rand (rand (concl tsar_enum_fmap))))); 94(* 3665 primitive inferences *) 95 96(* Find that the transitive closure holds of a particular pair *) 97 98val tcpair = let 99 val tc_fmapal = rand (rand (concl tsar_anc_thm)) 100 val testNic2 = ``("NICHOLAS", 2) IN (^tc_fmapal ' ("PETER", 1))`` 101in 102 (Count.apply (RAND_CONV (FAPPLY_CONV tsarto_CONV)) (* 178 prim infs *) THENC 103 Count.apply (IN_CONV tsarto_CONV) (* 221 prim infs *)) testNic2 104end; 105 106(* Same example the asymptotically slow way, with no trees. *) 107 108val TSAR_EQ_CONV = 109 REWR_CONV pairTheory.PAIR_EQ THENC 110 RATOR_CONV (RAND_CONV stringLib.string_EQ_CONV) THENC 111 numLib.REDUCE_CONV 112 113val tsar_anc_no_trees = 114 Count.apply (TC_CONV TSAR_EQ_CONV) ``(FMAP_TO_RELN ^RomHasse)^+``; 115(* 15254 primitive inferences *) 116 117(* Find that the transitive closure holds of a particular pair *) 118 119val tcpair' = let 120 val tc_fmap = rand (rand (concl tsar_anc_no_trees)) 121 val testNic2 = ``("NICHOLAS", 2) IN (^tc_fmap ' ("PETER", 1))`` 122in 123 (Count.apply (RAND_CONV (FAPPLY_CONV TSAR_EQ_CONV)) (* 66 prim infs *) THENC 124 Count.apply (IN_CONV TSAR_EQ_CONV) (* 473 prim infs *)) testNic2 125end; 126