1(* ========================================================================= *)
2(* TEST SUITE FOR HOL BOOLIFICATION.                                         *)
3(* Created by Joe Hurd, July 2002                                            *)
4(* ========================================================================= *)
5
6(*
7val () =
8  loadPath :=
9  ["../../datatype/", "../../list/src", "../../tfl/src", "../src"] @
10  !loadPath;
11*)
12
13val () = app load ["Encode", "EncodeTheory", "DecodeTheory", "CoderTheory"];
14
15open EncodeTheory DecodeTheory CoderTheory;
16
17(* ------------------------------------------------------------------------- *)
18(* Helper functions.                                                         *)
19(* ------------------------------------------------------------------------- *)
20
21fun first_token (QUOTE s :: _) = hd (String.tokens Char.isSpace
22                                            (Lib.deinitcomment s))
23  | first_token _ = "if_you_can_read_this_then_first_token_probably_failed";
24fun mkTy nm =
25    let val kid = {Thy = current_theory(), Tyop = nm}
26        val a = valOf (Type.op_arity kid)
27    in
28      mk_thy_type {
29        Args = List.tabulate(a,
30                             fn i => mk_vartype ("'a" ^ Int.toString i)),
31        Thy = current_theory(),
32        Tyop = nm
33      }
34    end
35val size_of = Lib.total (TypeBase.size_of o mkTy)
36val encode_of = Lib.total (TypeBase.encode_of o mkTy)
37
38val Hol_datatype =
39  fn q =>
40  let
41    val () = Lib.try (Count.apply Datatype.Hol_datatype) q
42    val tyname = first_token q
43  in
44    (tyname, size_of tyname, encode_of tyname)
45  end;
46
47fun encode tm =
48  let
49    val db = TypeBase.theTypeBase()
50    val f = TypeBasePure.type_encode db (type_of tm)
51  in
52    (*CONV_RULE (REDEPTH_CONV pairLib.PAIRED_BETA_CONV)*)
53    (bossLib.EVAL (mk_comb (f, tm)))
54  end;
55
56(* ------------------------------------------------------------------------- *)
57(* Example datatypes to test boolification.                                  *)
58(* ------------------------------------------------------------------------- *)
59
60try Hol_datatype `NumBool0 = Num0 of num | Bool0 of bool`;
61
62try Hol_datatype `NumBoolNums = Num of num | Bool of bool | Nums of num list`;
63
64try Hol_datatype `NTree = Tree of NTree list`;
65
66try Hol_datatype `List = Nil | Cons of 'A => List`;
67
68try Hol_datatype `tri = ONE | TWO | THREE`;
69
70try Hol_datatype
71  `command
72       = Assignment of num list # expression list
73       | Sequence   of command list
74   ;
75   expression
76       = Numeral of num
77       | Plus    of expression # expression
78       | Valof   of command`;
79
80try Hol_datatype
81        `exp = VAR of 'a
82             | IF  of bexp => exp => exp
83             | APP of 'b => exp list
84          ;
85        bexp = EQ  of exp => exp
86             | LEQ of exp => exp
87             | AND of bexp => bexp
88             | OR  of bexp => bexp
89             | NOT of bexp`;
90
91(* ------------------------------------------------------------------------- *)
92(* Encoding of terms.                                                        *)
93(* ------------------------------------------------------------------------- *)
94
95val encode = encode o Term;
96
97try encode `[(1,2,3,4) ; (5,6,7,8)]`;
98try encode `(SOME F, 123, [F;T])`;
99try encode `[]:num list`;
100try encode `[1; 2; 3]`;
101try encode `(Num 1, Nums [2; 3])`;
102try encode `Tree [Tree []; Tree [Tree []; Tree []]; Tree []]`;
103try encode `[INL TWO; INR (Bool0 T)]`;
104try encode `Assignment ([1; 2], [Numeral 1])`;
105
106(* ------------------------------------------------------------------------- *)
107(* Decoding terms.                                                           *)
108(* ------------------------------------------------------------------------- *)
109
110val decode_numlist =
111  MATCH_MP (INST_TYPE [alpha |-> Type`:num`] decode_list)
112  (Q.SPEC `K T` wf_decode_num);
113
114val () = computeLib.add_funs [decode_numlist];
115
116val [encode_num_tm] = decls "encode_num";
117val [decode_num_tm] = decls "decode_num";
118val [decode_list_tm] = decls "decode_list";
119
120(*
121fun Orelsef x [] = false
122  | Orelsef x (h::t) = h(x) orelse Orelsef x t;
123
124val _ = computeLib.monitoring :=
125  SOME (fn x => Orelsef x
126                        (map same_const
127                             [encode_num_tm,decode_num_tm, decode_list_tm]))
128*)
129
130fun ED tm =
131 Count.apply
132    EVAL (Term `decode_list (ALL_EL (K T)) (decode_num (K T))
133                 (encode_list encode_num ^tm)`);
134
135val th1 = ED (Term` [1; 2; 3; 4]`);
136
137val r = rhs (concl th1);
138val M = Term`decode_list (ALL_EL (K T)) (decode_num (K T)) ^r`;
139
140val conv = ONCE_REWRITE_CONV [decode_numlist, combinTheory.K_DEF,
141                         listTheory.list_case_def, bool_case_thm]
142           THENC DEPTH_CONV BETA_CONV;
143
144fun convN 0 = ALL_CONV
145  | convN n = conv THENC convN (n-1);
146
147
148val th2 = bossLib.EVAL (Term`decode_list (ALL_EL (K T)) (decode_num (K T)) ^r`);
149
150val th1 = bossLib.EVAL (Term`encode_list encode_num [1]`);
151
152Count.apply EVAL (Term`decode_num (K T) (encode_num 4)`);
153
154val N = Term`decode_list (ALL_EL (K T)) (decode_num (K T))
155             ^(rhs(concl (EVAL (Term`encode_list encode_num [1; 2]`))))`;
156
157
158EVAL (Term `decode_num (K T) [T; F; T; T; T; F; T; T; F]`);
159
160
161(*---------------------------------------------------------------------------*)
162(* Currently, the decoders installed for basic types are not efficient,      *)
163(* mainly because they use case statements on the rhs, and that is not       *)
164(* efficiently supported. The following two versions of decode_num and       *)
165(* decode_list are far better.                                               *)
166(*---------------------------------------------------------------------------*)
167
168val decode_num_thm =
169 mk_thm ([], Term
170 `(decode_num P [] = NONE) /\
171  (decode_num P [x] = NONE) /\
172  (decode_num P (T::T::t) = SOME (0,t)) /\
173  (decode_num P (T::F::t) =
174     let x = decode_num P t
175     in if IS_SOME x then (let (m,t') = THE(x) in SOME (2*m + 1, t'))
176        else NONE) /\
177  (decode_num P (F::t) =
178     let x = decode_num P t
179     in if IS_SOME x then (let (m,t') = THE(x) in SOME (2*m + 2, t'))
180        else NONE)`);
181
182val decode_list_thm =
183 mk_thm ([],Term
184  `(decode_list (ALL_EL (K T)) (decode_num (K T)) [] = NONE) /\
185   (decode_list (ALL_EL (K T)) (decode_num (K T)) (F::t) = SOME([],t)) /\
186   (decode_list (ALL_EL (K T)) (decode_num (K T)) (T::t) =
187       let x = decode_num (K T) t
188       in if IS_SOME x
189            then let (y,t') = THE(x)
190                 in let z = decode_list (ALL_EL (K T)) (decode_num (K T)) t'
191                    in if IS_SOME z
192                        then (let (u,w) = THE(z) in SOME (y::u,w))
193                        else NONE
194            else NONE)`);
195
196computeLib.add_funs [decode_num_thm,decode_list_thm];
197