1(*---------------------------------------------------------------------------* 2 * Setting information for types. * 3 * * 4 * Here we fill in the "size" entries in theTypeBase for some types that * 5 * are non-recursive and built before numbers. Also add some lifters. * 6 *---------------------------------------------------------------------------*) 7 8structure basicSize = 9struct 10 11local 12 open HolKernel boolLib Parse basicSizeTheory basicSizeSyntax 13 14 (*----------------------------------------------------------------------*) 15 (* Booleans *) 16 (*----------------------------------------------------------------------*) 17 18 val bool_info = Option.valOf (TypeBase.read {Thy="min", Tyop = "bool"}); 19 val bool_size_info = (bool_size_tm,TypeBasePure.ORIG bool_size_def) 20 val ty = mk_vartype "'type" 21 val tm = mk_vartype "'term" 22 val lift_bool_var = mk_var("boolSyntax.lift_bool",ty --> bool --> tm) 23 val bool_info' = TypeBasePure.put_lift lift_bool_var 24 (TypeBasePure.put_size bool_size_info bool_info); 25 26 (*----------------------------------------------------------------------*) 27 (* Products *) 28 (*----------------------------------------------------------------------*) 29 30 val prod_size_info = (pair_size_tm,TypeBasePure.ORIG pair_size_def) 31 val prod_info' = TypeBasePure.put_size prod_size_info 32 (Option.valOf (TypeBase.read {Tyop="prod", Thy="pair"})) 33 34 (*----------------------------------------------------------------------*) 35 (* Sums *) 36 (*----------------------------------------------------------------------*) 37 38 val sum_size_info = (sum_size_tm,TypeBasePure.ORIG sum_size_def) 39 val sum_info' = TypeBasePure.put_size sum_size_info 40 (Option.valOf(TypeBase.read {Tyop="sum", Thy="sum"})); 41 42 (*----------------------------------------------------------------------*) 43 (* Unit type *) 44 (*----------------------------------------------------------------------*) 45 46 val one_info = Option.valOf (TypeBase.read {Tyop="one",Thy="one"}) 47 val one_size_info = (one_size_tm,TypeBasePure.ORIG one_size_def) 48 val ty = mk_vartype "'type" 49 val tm = mk_vartype "'term" 50 val lift_one_var = mk_var("oneSyntax.lift_one", ty --> oneSyntax.one_ty --> tm) 51 val one_info' = TypeBasePure.put_lift lift_one_var 52 (TypeBasePure.put_size one_size_info one_info) 53 54 (*----------------------------------------------------------------------*) 55 (* Options *) 56 (*----------------------------------------------------------------------*) 57 58 val option_info = Option.valOf (TypeBase.read {Tyop="option", Thy="option"}) 59 val option_size_info = (option_size_tm,TypeBasePure.ORIG option_size_def) 60 val option_info' = TypeBasePure.put_size option_size_info option_info 61 62in 63 val _ = TypeBase.write [bool_info'] 64 val _ = TypeBase.write [prod_info'] 65 val _ = TypeBase.write [sum_info'] 66 val _ = TypeBase.write [one_info'] 67 val _ = TypeBase.write [option_info'] 68end 69 70end 71