1(* File: totoTacs.sml. Author: F. Lockwood Morris. Begun 25 Oct. 2012. *) 2(* Revised 23 Sept 2013 to include treatment of type int. *) 3(* Revised 12 Dec. 2013 to suit HOL-Kananaskis 9. *) 4 5(* Conversions for evaluating expressions of type cpn, that is three-way 6 comparisons, typically of the form f x y, where f:t->t->cpn satisfies 7 TotOrd, more particularly of the form apto g x y, with g:t toto for 8 some type t. *) 9 10structure totoTacs :> totoTacs = 11struct 12(* 13app load ["totoTheory", "pred_setLib", "bossLib", 14 "reduceLib", "relationTheory", "stringLib"]; 15*) 16open Parse HolKernel boolLib bossLib; 17 18structure Parse = struct 19 open Parse 20 val (Type,Term) = parse_from_grammars totoTheory.toto_grammars 21end 22open Parse 23 24val _ = set_trace "Unicode" 0; 25open totoTheory reduceLib relationTheory 26 listTheory pairTheory optionTheory pred_setLib stringLib; 27 28val AR = ASM_REWRITE_TAC []; 29fun ulist x = [x]; 30 31val ERR = mk_HOL_ERR "totoTacs"; 32 33(* At least for composing conversions, Hol's MATCH_MP is prone to yield 34 generality that we don't want, by introducing variants of variables 35 when it is sound to do so. Relying again on PART_MATCH, we devise a 36 plain version to suit our needs. *) 37 38fun PURE_MATCH_MP f x = MP (PART_MATCH (rand o rator) f (concl x)) x; 39 40(* As I understand it, results from PART_MATCH never have quantifiers, 41 and we need only preserve the same for all products of conversions. *) 42 43(* seem to need a tripartite equivalent of illegitimate REWR cpn_case_def 44 (to avoid searching the whole term with REWRITE_CONV) *) 45 46val cpn_case_def = TypeBase.case_def_of ``:ordering``; 47 48val [LESS_REWR, EQUAL_REWR, GREATER_REWR] = CONJUNCTS cpn_case_def; 49 50(* LESS_REWR = |- !v0 v1 v2. 51 (case LESS of LESS -> v0 || EQUAL -> v1 || GREATER -> v2) = v0 52 EQUAL_REWR = |- !v0 v1 v2. 53 (case EQUAL of LESS -> v0 || EQUAL -> v1 || GREATER -> v2) = v1 54 GREATER_REWR = |- !v0 v1 v2. 55 (case GREATER of LESS -> v0 || EQUAL -> v1 || GREATER -> v2) = v2 *) 56 57val cpn_REWR_CONV = REWR_CONV LESS_REWR ORELSEC REWR_CONV EQUAL_REWR ORELSEC 58 REWR_CONV GREATER_REWR ORELSEC 59(fn _ => Raise (mk_HOL_ERR "rbtTacs" "cpn_REWR_CONV" "not a case cpn of ...")); 60 61(* *********************************************************************** *) 62(* **** Getting to toto-deciding conversions. **** *) 63(* *********************************************************************** *) 64 65(* Given 66 lin_ord_thm: |- LinearOrder phi; 67 toto_of_thm: |- cmp = toto_of_LinearOrder phi; 68 eq_conv: reduces equations of ground terms (of phi's arg. type) to T/F; 69 lo_conv: reduces terms c phi c' to T/F; 70 71 we expect 72 toto_CONV lin_ord_thm toto_of_thm eq_conv lo_conv 73 74 to be a conversion that will reduce terms apto cmp c c' 75 to LESS/EQUAL/GREATER. *) 76 77val var1 = mk_var ("_z", Type`:bool`); (* supposedly not an identifier *) 78 79fun toto_CONV lin_ord_thm toto_of_thm eq_conv lo_conv = 80let val phi = snd (dest_comb (concl lin_ord_thm)); 81 (* val cmp = fst (dest_eq (concl toto_of_thm)); *) 82 val cj = CONJ lin_ord_thm toto_of_thm; 83 val eq_thm = PURE_MATCH_MP toto_equal_imp cj 84 and uneq_thm = PURE_MATCH_MP toto_unequal_imp cj 85in fn (t:term) => (* supposed to have the form apto cmp t1 t2 *) 86 let val (t1, t2) = (rand (rator t), rand t); 87 val eq_verdict = eq_conv (mk_eq (t1, t2)) 88 in PURE_MATCH_MP eq_thm eq_verdict 89 handle _ => 90 let val cond = PURE_MATCH_MP uneq_thm eq_verdict; 91 (* cond = `if phi x y then ... = LESS else ... = GREATER` *) 92 val (phi12, arm1, arm2) = dest_cond (concl cond); 93 val subst_res = SUBST [var1 |-> lo_conv phi12] 94 (mk_cond (var1, arm1, arm2)) 95 cond 96 in CONV_RULE COND_CONV subst_res end end end; 97 98(* ** However, we don't obtain numto, or any specific order, by toto_CONV: ** *) 99 100(* ***************************************************************** *) 101(* numto_CONV *) 102(* ***************************************************************** *) 103 104(* imitate equality checks for nums, chars, strings from stringLib *) 105 106val refl_clause_num = MATCH_MP TO_refl TO_numOrd; 107 108(* refl_clause_num = |- !x. numOrd x x = EQUAL *) 109 110val TLA_ZERO = GSYM arithmeticTheory.ALT_ZERO; 111 112val num_pre_CONV = REWR_CONV arithmeticTheory.NUMERAL_DEF ORELSEC 113 REWR_CONV TLA_ZERO ORELSEC 114 ALL_CONV; 115 116val numeral_lt_CONV = BINOP_CONV num_pre_CONV THENC 117 REWRITE_CONV [numeralTheory.numeral_lt]; 118 119val numeralOrd_CONV = BINOP_CONV num_pre_CONV THENC 120 PURE_REWRITE_CONV [numeralOrd, cpn_case_def]; 121 122fun numOrd_CONV t = 123 let val (Na, Nb) = dest_binop (Term`numOrd`) 124 (ERR "numOrd_CONV" "not a numOrd N N' comparison") t 125 in 126 if Na ~~ Nb then SPEC Na refl_clause_num 127 else 128 let val eqn = numeralOrd_CONV t; 129 val ans = rand (concl eqn) 130 in if is_const ans andalso type_of ans = Type`:cpn` then eqn 131 else 132 Raise (ERR "numOrd_CONV" "not a numOrd test") 133 end 134 end; 135 136val numto_CONV = 137RATOR_CONV (RATOR_CONV (REWR_CONV apnumto_thm)) THENC 138 numOrd_CONV; 139 140fun charOrd_CONV t = 141 let val (Ca, Cb) = dest_binop (Term`charOrd`) 142 (ERR "charOrd_CONV" "not a charOrd C C' comparison") t; 143 val (a, b) = (rand Ca, rand Cb); 144 val dictum = numOrd_CONV (mk_comb (mk_comb (Term`numOrd`, a), b)); 145 val outcome = rand (concl dictum) 146 in if outcome ~~ Term`EQUAL` then PURE_MATCH_MP charOrd_eq_lem dictum 147 else if outcome ~~ Term`LESS` then 148 let val bless = numeral_lt_CONV (mk_comb (mk_comb (Term`($<):num reln`, b), 149 Term`256`)) 150 in PURE_MATCH_MP (PURE_MATCH_MP charOrd_lt_lem dictum) bless end 151 else if outcome ~~ Term`GREATER` then 152 let val aless = numeral_lt_CONV (mk_comb (mk_comb (Term`($<):num reln`, a), 153 Term`256`)) 154 in PURE_MATCH_MP (PURE_MATCH_MP charOrd_gt_lem dictum) aless end 155 else Raise (ERR "charOrd_CONV" "not a good character comparison") 156 end; 157 158val charto_CONV = RATOR_CONV (RATOR_CONV (REWR_CONV apcharto_thm)) THENC 159 charOrd_CONV; 160 161(* ********* qk_numto_CONV similar to numto_CONV: *********** *) 162 163val refl_clause_qk_num = MATCH_MP TO_refl TO_qk_numOrd; 164 165val qk_numeralOrd_CONV = BINOP_CONV num_pre_CONV THENC 166 PURE_REWRITE_CONV [qk_numeralOrd, cpn_case_def]; 167 168fun qk_numOrd_CONV t = 169 let val (Na, Nb) = dest_binop (Term`qk_numOrd`) 170 (ERR "qk_numOrd_CONV" "not a qk_numOrd N N' comparison") t 171 in if Na ~~ Nb then SPEC Na refl_clause_qk_num else 172 let val eqn = qk_numeralOrd_CONV t; 173 val ans = rand (concl eqn) 174 in if is_const ans andalso type_of ans = Type`:cpn` then eqn else 175 Raise (ERR "qk_numOrd_CONV" "not a qk_numOrd test") 176 end end; 177 178val qk_numto_CONV = 179RATOR_CONV (RATOR_CONV (REWR_CONV ap_qk_numto_thm)) THENC 180 qk_numOrd_CONV; 181 182(* ******************************************************************** *) 183(* ********** lextoto_CONV ********* *) 184(* ******************************************************************** *) 185 186(* lextoto_CONV expects two conversions, say Ato_CONV, Bto_CONV for computing 187 orders Ato, Bto, and a term (apto (lextoto Ato Bto) (a1, b1) (a2, b2)). 188 Tests follow declaration of stringto_CONV below. *) 189 190fun lextoto_CONV Aconv Bconv = 191REWR_CONV aplextoto THENC 192RATOR_CONV (RATOR_CONV (RATOR_CONV (RAND_CONV Aconv))) THENC 193 ((REWR_CONV EQUAL_REWR THENC Bconv) ORELSEC 194 REWR_CONV LESS_REWR ORELSEC REWR_CONV GREATER_REWR); 195 196(* ***** listoto_CONV should also be easily developed from aplistoto; ***** *) 197(* ***** it expects one conversion (for elements) as first argument, ***** *) 198(* *** and a term argument of the form (apto (listtoto elem_CONV) l1 l2) ** *) 199 200val [lsnn, lsnc, lscn, lscc] = map GEN_ALL (CONJUNCTS (SPEC_ALL aplistoto)); 201 202(* lsnn = |- !c. apto (listoto c) [] [] = EQUAL 203 lsnc = |- !c b y. apto (listoto c) [] (b::y) = LESS 204 lscn = |- !c a x. apto (listoto c) (a::x) [] = GREATER 205 lscc = |- !c a x b y. apto (listoto c) (a::x) (b::y) = 206 case apto c a b of 207 LESS -> LESS 208 || EQUAL -> apto (listoto c) x y 209 || GREATER -> GREATER *) 210 211fun listoto_CONV elem_conv = 212 let fun lis_c t = 213 ((REWR_CONV lscc THENC 214 RATOR_CONV (RATOR_CONV (RATOR_CONV (RAND_CONV elem_conv))) THENC 215 ((REWR_CONV EQUAL_REWR THENC lis_c) ORELSEC 216 REWR_CONV LESS_REWR ORELSEC REWR_CONV GREATER_REWR)) ORELSEC 217 REWR_CONV lsnn ORELSEC REWR_CONV lsnc ORELSEC REWR_CONV lscn) t 218 in lis_c ORELSEC (fn _ => Raise (ERR "listoto_CONV" "unsuitable args")) end; 219 220(* ******* Type string treated as synonymous with char list ******* *) 221 222val refl_clause_string = MATCH_MP TO_refl 223 (ISPEC (Term`stringto`) TotOrd_apto); 224 225fun stringto_CONV t = 226if rand (rator t) ~~ rand t then SPEC (rand t) refl_clause_string else 227 (RATOR_CONV (RATOR_CONV (RAND_CONV (REWR_CONV stringto))) THENC 228 listoto_CONV charto_CONV) t; 229 230(* ************ test cases, just to put everyone throught the motions: 231 232numOrd_CONV (Term`numOrd 57 54`); 233 234numto_CONV (Term`apto numto 6 6`); 235numto_CONV (Term`apto numto 6 7`); 236numto_CONV (Term`apto numto 8 7`); 237 238charOrd_CONV (Term`charOrd (#"A") (#"B")`); 239charOrd_CONV (Term`charOrd (#"A") (#"A")`); 240charOrd_CONV (Term`charOrd (#"Z") (#"B")`); 241charOrd_CONV (Term`charOrd (CHR 0) (CHR 0)`); 242 243charto_CONV (Term`apto charto #"8" #"7"`); 244 245val testn = Count.apply (numto_CONV o Term); 246 247testn`apto numto 5 7`; 248testn`apto numto 0 0`; 249 250val testc = Count.apply (charOrd_CONV o Term); 251 252testc`charOrd #"A" #"B"`; 253testc`charOrd #"<" #"<"`; 254testc`charOrd #"a" #">"`; 255 256qk_numOrd_CONV (Term`qk_numOrd 57 54`); (* LESS *) 257 258qk_numto_CONV (Term`apto qk_numto 6 6`); (* EQUAL *) 259qk_numto_CONV (Term`apto qk_numto 6 7`); (* GREATER *) 260qk_numto_CONV (Term`apto qk_numto 8 7`); (* GREATER *) 261 262val lnC = listoto_CONV numto_CONV; 263lnC (Term`apto (listoto numto) [5; 3; 7] [5; 3]`); 264lnC (Term`apto (listoto numto) [5; 3; 7] [5; 3; 7]`); 265lnC (Term`apto (listoto numto) [5; 3] [5; 3; 7]`); 266 267stringto_CONV (Term`apto stringto "abcdefghijklmnopq" "abcdefghijklmnopr"`); 268 stringto_CONV (Term`apto stringto "abc" "ab"`); 269Count.apply string_EQ_CONV 270 (Term`"abcdefghijklmnopqrstuvwxyz" = "abcdefghijklmnopqrstuvwxyzA"`); 271(* last used 270 inference steps *) 272Count.apply stringto_CONV (Term 273 `apto stringto "abcdefghijklmnopqrstuvwxyz" "abcdefghijklmnopqrstuvwxyzA"`); 274(* 1067 inference steps, not quite as good as the 772 steps from specially 275 written stringOrd/stringto (under HOL-Kananaskis-8), but close enough. *) 276 277val p1 = Term`(6, "ab")`; 278val p2 = Term`(7, "ab")`; 279val p3 = Term`(6, "ac")`; 280 281val lexns = lextoto_CONV numto_CONV stringto_CONV; 282 283lexns (Term`apto (numto lextoto stringto) ^p1 ^p2`); 284lexns (Term`apto (numto lextoto stringto) ^p2 ^p1`); 285lexns (Term`apto (numto lextoto stringto) ^p1 ^p3`); 286lexns (Term`apto (numto lextoto stringto) ^p3 ^p1`); 287lexns (Term`apto (numto lextoto stringto) ^p2 ^p3`); 288lexns (Term`apto (numto lextoto stringto) ^p3 ^p2`); 289lexns (Term`apto (numto lextoto stringto) ^p3 ^p3`); 290*************** *) 291end; 292