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