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