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