1(* ========================================================================= *)
2(* FILE          : fcpLib.sml                                                *)
3(* DESCRIPTION   : Tools for fcpTheory.                                      *)
4(*                                                                           *)
5(* AUTHOR        : (c) Anthony Fox, University of Cambridge                  *)
6(* DATE          : 2005                                                      *)
7(* ========================================================================= *)
8
9structure fcpLib :> fcpLib =
10struct
11
12open HolKernel Parse boolLib bossLib
13open fcpTheory fcpSyntax
14
15(* ------------------------------------------------------------------------- *)
16
17val ERR = mk_HOL_ERR "fcpLib"
18
19val index_type   = fcpSyntax.mk_numeric_type
20val index_to_num = fcpSyntax.dest_numeric_type
21
22fun index_compset () =
23   let
24      open numeral_bitTheory
25      val compset = reduceLib.num_compset()
26      val rule = REWRITE_RULE [arithmeticTheory.TIMES2, GSYM numeralTheory.iDUB]
27      val () = computeLib.add_thms
28                 [index_sum, index_one, rule index_bit0, rule index_bit1,
29                  finite_sum, finite_one, finite_bit0, finite_bit1,
30                  numeral_bitTheory.iDUB_NUMERAL] compset
31   in
32      compset
33   end
34
35val INDEX_CONV = Conv.CHANGED_CONV (computeLib.CBV_CONV (index_compset()))
36
37local
38   fun conv n = INDEX_CONV o Term.inst [Type.alpha |-> index_type n]
39in
40   fun DIMINDEX n = conv n (fcpSyntax.mk_dimindex Type.alpha)
41   fun FINITE n =
42      Type.alpha
43      |> pred_setSyntax.mk_univ
44      |> pred_setSyntax.mk_finite
45      |> conv n
46      |> Drule.EQT_ELIM
47end
48
49fun SIZE n =
50   PURE_REWRITE_RULE [DIMINDEX n]
51      (Thm.MP (Thm.INST_TYPE [Type.alpha |-> index_type n]
52                  fcpTheory.card_dimindex)
53              (FINITE n))
54
55val FCP_ss =
56  simpLib.rewrites [fcpTheory.FCP_BETA, fcpTheory.FCP_ETA, fcpTheory.CART_EQ]
57
58val notify_on_length_guess = ref true
59
60val () = Feedback.register_btrace
61            ("notify FCP length guesses", notify_on_length_guess)
62
63local
64   fun t2s t = String.extract (Hol_pp.type_to_string t, 1, NONE)
65   fun infer_fcp_type tm =
66      case Lib.total (fst o listSyntax.dest_list o fcpSyntax.dest_l2v) tm of
67         SOME l =>
68            let
69               val ty = snd (fcpSyntax.dest_cart_type (Term.type_of tm))
70               val _ = Type.polymorphic ty orelse raise ERR "infer_fcp_type" ""
71            in
72               ty |-> index_type (Arbnum.fromInt (List.length l))
73            end
74       | NONE => raise ERR "infer_fcp_type" ""
75in
76   fun inst_fcp_lengths tm =
77      case total (HolKernel.find_term (Lib.can infer_fcp_type)) tm of
78         NONE => tm
79       | SOME subtm =>
80          let
81             val theinst as {redex, residue} = infer_fcp_type subtm
82             val _ = if !Globals.interactive andalso !notify_on_length_guess
83                        then Feedback.HOL_MESG
84                                (String.concat ["assigning FCP length: ",
85                                                t2s redex, " <- ", t2s residue])
86                     else ()
87          in
88             inst_fcp_lengths (Term.inst [theinst] tm)
89          end
90end
91
92end
93