1structure ratUtils :> ratUtils = 2struct 3 4open HolKernel boolLib Parse bossLib; 5 6(* interactive mode 7app load ["pairTheory", "pairLib", 8 "integerTheory", "intLib", 9 "jbUtils"]; 10*) 11 12open 13 pairTheory pairLib 14 integerTheory intLib 15 jbUtils; 16 17structure Parse = 18struct 19 open Parse 20 val (Type,Term) = parse_from_grammars fracTheory.frac_grammars 21end; 22 23 24(*-------------------------------------------------------------------------- 25 * dest_rat : term -> term * term list 26 *--------------------------------------------------------------------------*) 27 28fun dest_rat (t1:term) = 29 if is_comb t1 then 30 let 31 val (top_rator, top_rand) = dest_comb t1 32 in 33 if top_rator ~~ ``abs_rat`` then (``abs_rat``,[top_rand]) 34 else 35 (* Hier gibt es noch Probleme: X (v1:vec) ist auch vom Typ rat *) 36 if top_rator ~~ ``rat_ainv`` orelse top_rator ~~ ``rat_minv`` orelse 37 top_rator ~~ ``X`` orelse top_rator ~~ ``Y`` 38 then 39 (top_rator, [top_rand]) 40 else 41 let 42 val (this_op, this_first, this_second) = dest_binop_triple t1 43 in 44 (this_op, [this_first, this_second]) 45 end 46 end 47 else (* t1 must be a variable *) 48 (t1,[]) 49 50(* ---------- test cases ---------- * 51 dest_rat ``r1:rat``; 52 dest_rat ``abs_rat( abs_frac(3i,4i) )``; 53 dest_rat ``rat_add r1 r2``; 54 dest_rat ``rat_add (rat_sub r1 r2) r3``; 55 dest_rat ``rat_add (abs_rat(abs_frac(3i,4i))) (abs_rat(abs_frac(4i,5i)))``; 56 * ---------- test cases ---------- *) 57 58 59(*-------------------------------------------------------------------------- 60 * extract_rat : term -> term list 61 *--------------------------------------------------------------------------*) 62 63fun extract_rat (t1:term) = 64 extract_terms_of_type ``:rat`` t1; 65 66 67(* ---------- test cases ---------- * 68 extract_rat ``4i + (rat_nmr(abs_rat(abs_frac(3i,4i)))) = 3``; 69 extract_rat ``rat_add r1 r2 = rat_sub r1 r2``; 70 extract_rat ``!r1 r2. rat_nmr (rat_add r1 r2) = rat_dnm (rat_sub r1 r2)``; 71 extract_rat ``rat_nmr (rat_add r1 r2) = rat_dnm (rat_sub r1 r2)``; 72 * ---------- test cases ---------- *) 73 74(*-------------------------------------------------------------------------- 75 * rat_vars_of_term : term -> term list 76 *--------------------------------------------------------------------------*) 77 78fun extract_rat_vars t1 = 79 filter (fn t => type_of t=``:rat``) (free_vars t1); 80 81(*-------------------------------------------------------------------------- 82 * extract_rat_equations : term -> term list 83 *--------------------------------------------------------------------------*) 84 85fun extract_rat_equations (t1:term) = 86 if (is_comb t1) then 87 if (is_eq t1) andalso (type_of (fst (dest_eq t1)) = ``:rat``) then 88 [t1] 89 else 90 let val (ta,tb) = dest_comb t1 in 91 (extract_rat_equations ta) @ (extract_rat_equations tb) 92 end 93 else 94 []; 95 96 97(*-------------------------------------------------------------------------- 98 * extract_rat_minv : term -> term list 99 *--------------------------------------------------------------------------*) 100 101fun extract_rat_minv (t1:term) = 102 if (is_comb t1) then 103 if rator t1 ~~ ``rat_minv`` then [t1] 104 else 105 let 106 val (ta,tb) = dest_comb t1 107 in 108 tunion (extract_rat_minv ta) (extract_rat_minv tb) 109 end 110 else 111 []; 112 113(*========================================================================== 114 * end of structure 115 *==========================================================================*) 116end; 117