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