1structure fracSyntax :> fracSyntax = 2struct 3 4open HolKernel boolLib Parse; 5 6(* interactive mode 7app load ["fracTheory"]; 8*) 9 10open fracTheory; 11 12 13val ERR = mk_HOL_ERR "fracSyntax"; 14 15(*--------------------------------------------------------------------------* 16 * constants 17 *--------------------------------------------------------------------------*) 18 19val int_ty = intSyntax.int_ty; 20val frac = mk_thy_type{Tyop = "frac", Thy="frac", Args = []}; 21 22val frac_0_tm = prim_mk_const {Name="frac_0",Thy="frac"}; 23val frac_1_tm = prim_mk_const {Name="frac_1",Thy="frac"}; 24 25val frac_nmr_tm = prim_mk_const {Name="frac_nmr",Thy="frac"}; 26val frac_dnm_tm = prim_mk_const {Name="frac_dnm",Thy="frac"}; 27val frac_sgn_tm = prim_mk_const {Name="frac_sgn",Thy="frac"}; 28 29val frac_ainv_tm = prim_mk_const {Name="frac_ainv",Thy="frac"}; 30val frac_minv_tm = prim_mk_const {Name="frac_minv",Thy="frac"}; 31 32val frac_add_tm = prim_mk_const {Name="frac_add",Thy="frac"}; 33val frac_sub_tm = prim_mk_const {Name="frac_sub",Thy="frac"}; 34val frac_mul_tm = prim_mk_const {Name="frac_mul",Thy="frac"}; 35val frac_div_tm = prim_mk_const {Name="frac_div",Thy="frac"}; 36 37val frac_save_tm = prim_mk_const {Name="frac_save",Thy="frac"}; 38 39(*--------------------------------------------------------------------------* 40 * constructors 41 *--------------------------------------------------------------------------*) 42 43fun mk_monop c tm = mk_comb(c,tm); 44fun mk_binop c (tm1,tm2) = mk_comb(mk_comb(c,tm1),tm2); 45 46val mk_frac_nmr = mk_monop frac_nmr_tm; 47val mk_frac_dnm = mk_monop frac_dnm_tm; 48val mk_frac_sgn = mk_monop frac_sgn_tm; 49 50val mk_frac_ainv = mk_monop frac_ainv_tm; 51val mk_frac_minv = mk_monop frac_minv_tm; 52 53val mk_frac_add = mk_binop frac_add_tm; 54val mk_frac_sub = mk_binop frac_sub_tm; 55val mk_frac_mul = mk_binop frac_mul_tm; 56val mk_frac_div = mk_binop frac_div_tm; 57 58val mk_frac_save = mk_binop frac_save_tm; 59 60(*--------------------------------------------------------------------------* 61 * destructors 62 *--------------------------------------------------------------------------*) 63 64val dest_frac_nmr = dest_monop frac_nmr_tm (ERR "dest_frac_nmr" ""); 65val dest_frac_dnm = dest_monop frac_dnm_tm (ERR "dest_frac_dnm" ""); 66val dest_frac_sgn = dest_monop frac_sgn_tm (ERR "dest_frac_sgn" ""); 67 68val dest_frac_ainv = dest_monop frac_ainv_tm (ERR "dest_frac_ainv" ""); 69val dest_frac_minv = dest_monop frac_minv_tm (ERR "dest_frac_minv" ""); 70 71val dest_frac_add = dest_binop frac_add_tm (ERR "dest_frac_add" ""); 72val dest_frac_sub = dest_binop frac_sub_tm (ERR "dest_frac_sub" ""); 73val dest_frac_mul = dest_binop frac_mul_tm (ERR "dest_frac_mul" ""); 74val dest_frac_div = dest_binop frac_div_tm (ERR "dest_frac_div" ""); 75 76val dest_frac_save = dest_binop frac_save_tm (ERR "dest_frac_save" ""); 77 78(*--------------------------------------------------------------------------* 79 * query operations 80 *--------------------------------------------------------------------------*) 81 82val is_frac_nmr = can dest_frac_nmr; 83val is_frac_dnm = can dest_frac_dnm; 84val is_frac_sgn = can dest_frac_sgn; 85 86val is_frac_ainv = can dest_frac_ainv; 87val is_frac_minv = can dest_frac_minv; 88 89val is_frac_add = can dest_frac_add; 90val is_frac_sub = can dest_frac_sub; 91val is_frac_mul = can dest_frac_mul; 92val is_frac_div = can dest_frac_div; 93 94val is_frac_save = can dest_frac_save; 95 96(*========================================================================== 97 * end of structure 98 *==========================================================================*) 99end; 100