1structure ratSyntax :> ratSyntax = 2struct 3 4open HolKernel boolLib Parse; 5 6(* interactive mode 7app load ["ratTheory"]; 8*) 9 10open ratTheory; 11 12 13val ERR = mk_HOL_ERR "ratSyntax"; 14 15(*--------------------------------------------------------------------------* 16 * constants 17 *--------------------------------------------------------------------------*) 18 19(*val int_ty = intSyntax.int_ty;*) 20val rat = mk_thy_type{Tyop = "rat", Thy="rat", Args = []}; 21 22val rat_0_tm = prim_mk_const {Name="rat_0",Thy="rat"}; 23val rat_1_tm = prim_mk_const {Name="rat_1",Thy="rat"}; 24 25val rat_nmr_tm = prim_mk_const {Name="rat_nmr",Thy="rat"}; 26val rat_dnm_tm = prim_mk_const {Name="rat_dnm",Thy="rat"}; 27val rat_sgn_tm = prim_mk_const {Name="rat_sgn",Thy="rat"}; 28 29val rat_ainv_tm = prim_mk_const {Name="rat_ainv",Thy="rat"}; 30val rat_minv_tm = prim_mk_const {Name="rat_minv",Thy="rat"}; 31 32val rat_add_tm = prim_mk_const {Name="rat_add",Thy="rat"}; 33val rat_sub_tm = prim_mk_const {Name="rat_sub",Thy="rat"}; 34val rat_mul_tm = prim_mk_const {Name="rat_mul",Thy="rat"}; 35val rat_div_tm = prim_mk_const {Name="rat_div",Thy="rat"}; 36 37val rat_les_tm = prim_mk_const {Name="rat_les",Thy="rat"}; 38val rat_gre_tm = prim_mk_const {Name="rat_gre",Thy="rat"}; 39val rat_leq_tm = prim_mk_const {Name="rat_leq",Thy="rat"}; 40val rat_geq_tm = prim_mk_const {Name="rat_geq",Thy="rat"}; 41val rat_of_num_tm = prim_mk_const {Name = "rat_of_num", Thy = "rat"} 42 43(*--------------------------------------------------------------------------* 44 * constructors 45 *--------------------------------------------------------------------------*) 46 47fun mk_monop c tm = mk_comb(c,tm); 48fun mk_binop c (tm1,tm2) = mk_comb(mk_comb(c,tm1),tm2); 49 50val mk_rat_nmr = mk_monop rat_nmr_tm; 51val mk_rat_dnm = mk_monop rat_dnm_tm; 52val mk_rat_sgn = mk_monop rat_sgn_tm; 53 54val mk_rat_ainv = mk_monop rat_ainv_tm; 55val mk_rat_minv = mk_monop rat_minv_tm; 56val mk_rat_of_num = mk_monop rat_of_num_tm; 57 58val mk_rat_add = mk_binop rat_add_tm; 59val mk_rat_sub = mk_binop rat_sub_tm; 60val mk_rat_mul = mk_binop rat_mul_tm; 61val mk_rat_div = mk_binop rat_div_tm; 62 63val mk_rat_les = mk_binop rat_les_tm; 64val mk_rat_gre = mk_binop rat_gre_tm; 65val mk_rat_leq = mk_binop rat_leq_tm; 66val mk_rat_geq = mk_binop rat_geq_tm; 67 68(*--------------------------------------------------------------------------* 69 * destructors 70 *--------------------------------------------------------------------------*) 71 72val dest_rat_nmr = dest_monop rat_nmr_tm (ERR "dest_rat_nmr" ""); 73val dest_rat_dnm = dest_monop rat_dnm_tm (ERR "dest_rat_dnm" ""); 74val dest_rat_sgn = dest_monop rat_sgn_tm (ERR "dest_rat_sgn" ""); 75val dest_rat_of_num = dest_monop rat_of_num_tm (ERR "dest_rat_of_num" "") 76 77val dest_rat_ainv = dest_monop rat_ainv_tm (ERR "dest_rat_ainv" ""); 78val dest_rat_minv = dest_monop rat_minv_tm (ERR "dest_rat_minv" ""); 79 80val dest_rat_add = dest_binop rat_add_tm (ERR "dest_rat_add" ""); 81val dest_rat_sub = dest_binop rat_sub_tm (ERR "dest_rat_sub" ""); 82val dest_rat_mul = dest_binop rat_mul_tm (ERR "dest_rat_mul" ""); 83val dest_rat_div = dest_binop rat_div_tm (ERR "dest_rat_div" ""); 84 85val dest_rat_les = dest_binop rat_les_tm (ERR "dest_rat_les" ""); 86val dest_rat_gre = dest_binop rat_gre_tm (ERR "dest_rat_gre" ""); 87val dest_rat_leq = dest_binop rat_leq_tm (ERR "dest_rat_leq" ""); 88val dest_rat_geq = dest_binop rat_geq_tm (ERR "dest_rat_geq" ""); 89 90(*--------------------------------------------------------------------------* 91 * query operations 92 *--------------------------------------------------------------------------*) 93 94val is_rat_nmr = can dest_rat_nmr; 95val is_rat_dnm = can dest_rat_dnm; 96val is_rat_sgn = can dest_rat_sgn; 97val is_rat_of_num = can dest_rat_of_num 98 99val is_rat_ainv = can dest_rat_ainv; 100val is_rat_minv = can dest_rat_minv; 101 102val is_rat_add = can dest_rat_add; 103val is_rat_sub = can dest_rat_sub; 104val is_rat_mul = can dest_rat_mul; 105val is_rat_div = can dest_rat_div; 106 107val is_rat_les = can dest_rat_les; 108val is_rat_gre = can dest_rat_gre; 109val is_rat_leq = can dest_rat_leq; 110val is_rat_geq = can dest_rat_geq; 111 112(* ---------------------------------------------------------------------- 113 literals 114 ---------------------------------------------------------------------- *) 115 116fun is_int_injection t = 117 is_rat_of_num t orelse 118 is_rat_of_num (dest_rat_ainv t) handle HOL_ERR _ => false 119 120fun is_literal t = 121 is_int_injection t orelse 122 (let val (n,d) = dest_rat_div t 123 in 124 is_int_injection n andalso is_rat_of_num d 125 end handle HOL_ERR _ => false) 126 127 128(*--------------------------------------------------------------------------* 129 * list constructors 130 *--------------------------------------------------------------------------*) 131 132fun list_rat_add summands = 133let 134 fun recurse acc [] = acc 135 | recurse acc (x::xs) = recurse (mk_rat_mul(acc, x)) xs 136in 137 recurse (hd summands) (tl summands) 138 handle List.Empty => raise ERR "list_rat_add" "empty summand list" 139end; 140 141 142fun list_rat_mul multiplicands = 143let 144 fun recurse acc [] = acc 145 | recurse acc (x::xs) = recurse (mk_rat_mul(acc, x)) xs 146in 147 recurse (hd multiplicands) (tl multiplicands) 148 handle List.Empty => raise ERR "list_rat_mul" "empty multiplicand list" 149end; 150 151 152(*--------------------------------------------------------------------------* 153 * list destructors 154 *--------------------------------------------------------------------------*) 155 156fun strip_rat_add tm = 157let 158 fun recurse acc tm = 159 let val (l,r) = dest_rat_add tm in 160 recurse (recurse acc r) l 161 end handle HOL_ERR _ => tm::acc 162in 163 recurse [] tm 164end; 165 166 167fun strip_rat_mul tm = 168let 169 fun recurse acc tm = 170 let val (l,r) = dest_rat_mul tm in 171 recurse (recurse acc r) l 172 end handle HOL_ERR _ => tm::acc 173in 174 recurse [] tm 175end; 176 177 178(* into and out of (arbitrary precision) integers *) 179fun int_of_term t = 180 if is_rat_ainv t then Arbint.~ (int_of_term (rand t)) 181 else if is_rat_of_num t then Arbint.fromNat (numSyntax.dest_numeral (rand t)) 182 else raise mk_HOL_ERR "ratSyntax" "int_of_term" "Term not integral" 183 184fun term_of_int i = 185 let 186 val (n, f) = if Arbint.<(i,Arbint.zero) then (Arbint.~ i, mk_rat_ainv) 187 else (i, fn t => t) 188 in 189 f (mk_rat_of_num (numSyntax.mk_numeral (Arbint.toNat n))) 190 end 191 192 193 194(*========================================================================== 195 * end of structure 196 *==========================================================================*) 197end; 198