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