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