1structure realSyntax :> realSyntax =
2struct
3
4  local open realTheory in end;
5  open HolKernel Abbrev
6
7  val ERR = mk_HOL_ERR "realSyntax"
8
9
10  (* Fundamental terms, mainly constants *)
11
12  fun mk_raconst (n, ty) = mk_thy_const {Thy = "realax", Name = n, Ty = ty}
13  fun mk_rconst (n, ty) = mk_thy_const {Thy = "real", Name = n, Ty = ty}
14
15  val real_ty = mk_thy_type {Thy = "realax", Tyop = "real", Args = []}
16  val bop_ty = real_ty --> real_ty --> real_ty
17  val rel_ty = real_ty --> real_ty --> bool
18
19  val real_injection = mk_rconst("real_of_num", numSyntax.num --> real_ty)
20
21  val zero_tm = mk_comb(real_injection, numSyntax.zero_tm)
22  val one_tm = mk_comb(real_injection, numSyntax.mk_numeral (Arbnum.fromInt 1))
23  val negate_tm = mk_raconst("real_neg", real_ty --> real_ty)
24  val absval_tm = mk_rconst("abs", real_ty --> real_ty)
25  val plus_tm = mk_raconst("real_add", bop_ty)
26  val minus_tm = mk_rconst("real_sub", bop_ty)
27  val mult_tm = mk_raconst("real_mul", bop_ty)
28  val div_tm = mk_rconst("/", bop_ty)
29  val exp_tm = mk_rconst("pow", real_ty --> numSyntax.num --> real_ty)
30
31  val real_eq_tm = mk_thy_const { Thy = "min", Name = "=", Ty = rel_ty}
32  val less_tm = mk_raconst("real_lt", rel_ty)
33  val leq_tm = mk_rconst("real_lte", rel_ty)
34  val great_tm = mk_rconst("real_gt", rel_ty)
35  val geq_tm = mk_rconst("real_ge", rel_ty)
36
37  val min_tm = mk_rconst("min", bop_ty)
38  val max_tm = mk_rconst("max", bop_ty)
39
40  (* Functions *)
41
42  fun dest1 c fnm nm t = let
43    val (f, x) = dest_comb t
44    val _ = assert (same_const f) c
45  in
46    x
47  end handle HOL_ERR _ => raise ERR fnm ("Term is not a "^nm)
48
49  fun dest2 c fnm nm t = let
50    val (fx, y) = dest_comb t
51    val (f, x) = dest_comb fx
52    val _ = assert (same_const f) c
53in
54    (x, y)
55  end handle HOL_ERR _ => raise ERR fnm ("Term is not a "^nm)
56
57  val dest_negated = dest1 negate_tm "dest_negated" "negation"
58  val is_negated = can dest_negated
59  fun mk_negated t = mk_comb(negate_tm, t)
60
61  val dest_injected = dest1 real_injection "dest_injected" "injection"
62  val is_injected = can dest_injected
63  fun mk_injected t = mk_comb(real_injection, t)
64
65
66
67  fun is_real_literal t = let
68    (* returns true if a term is in the range of the implicit injection from
69       the integers *)
70    fun remove_negs t = remove_negs (dest_negated t) handle HOL_ERR _ => t
71    val number_part = dest_injected (remove_negs t)
72  in
73    numSyntax.is_numeral number_part
74  end handle HOL_ERR _ => false
75
76  fun term_of_int i = let
77    fun posint i =
78        mk_comb(real_injection, numSyntax.mk_numeral(Arbint.toNat i))
79  in
80    if Arbint.<(i,Arbint.zero) then mk_negated(posint(Arbint.~ i))
81    else posint i
82  end
83
84
85  fun flip f (x,y) = f (y, x)
86  val dest_plus = dest2 plus_tm "dest_plus" "plus"
87  val is_plus = can dest_plus
88  fun mk_plus(t1, t2) = list_mk_comb(plus_tm, [t1, t2])
89  fun list_mk_plus tlist =
90      case tlist of
91        [] => raise ERR "list_mk_plus" "Empty list"
92      | [t] => t
93      | t::ts => List.foldl (flip mk_plus) t ts
94  fun strip_plus t = let
95    fun recurse a k =
96        case k of
97          [] => a
98        | (t::ts) => let
99            val (t1, t2) = dest_plus t
100          in
101            recurse a (t2::t1::ts)
102          end handle HOL_ERR _ => recurse (t::a) ts
103  in
104    recurse [] [t]
105  end
106
107  val dest_minus = dest2 minus_tm "dest_minus" "subtraction"
108  val is_minus = can dest_minus
109  fun mk_minus(t1,t2) = list_mk_comb(minus_tm, [t1, t2])
110
111  val dest_mult = dest2 mult_tm "dest_mult" "multiplication"
112  val is_mult = can dest_mult
113  fun mk_mult(t1, t2) = list_mk_comb(mult_tm, [t1, t2])
114  fun list_mk_mult tlist =
115      case tlist of
116        [] => raise ERR "list_mk_mult" "Empty list"
117      | [t] => t
118      | t::ts => List.foldl (flip mk_mult) t ts
119  fun strip_mult t = let
120    fun recurse a k =
121        case k of
122          [] => a
123        | t::ts => let
124            val (t1, t2) = dest_mult t
125          in
126            recurse a (t2::t1::ts)
127          end handle HOL_ERR _ => recurse (t::a) ts
128  in
129    recurse [] [t]
130  end
131
132
133  val dest_div = dest2 div_tm "dest_div" "division"
134  val is_div = can dest_div
135  fun mk_div(t1, t2) = list_mk_comb(div_tm, [t1, t2])
136
137  val dest_absval = dest1 absval_tm "dest_absval" "absolute value"
138  val is_absval = can dest_absval
139  fun mk_absval t = mk_comb(absval_tm, t)
140
141  val dest_less = dest2 less_tm "dest_less" "less-than term"
142  val is_less = can dest_less
143  fun mk_less(t1, t2) = list_mk_comb(less_tm, [t1, t2])
144
145  val dest_leq = dest2 leq_tm "dest_leq" "less-than-or-equal term"
146  val is_leq = can dest_leq
147  fun mk_leq(t1, t2) = list_mk_comb(leq_tm, [t1, t2])
148
149  val dest_great = dest2 great_tm "dest_great" "greater-than term"
150  val is_great = can dest_great
151  fun mk_great(t1, t2) = list_mk_comb(great_tm, [t1, t2])
152
153  val dest_geq = dest2 geq_tm "dest_geq" "greater-than-or-equal term"
154  val is_geq = can dest_geq
155  fun mk_geq(t1, t2) = list_mk_comb(geq_tm, [t1, t2])
156
157  val dest_min = dest2 min_tm "dest_min" "min term"
158  val is_min = can dest_min
159  fun mk_min(t1, t2) = list_mk_comb(min_tm, [t1, t2])
160
161  val dest_max = dest2 max_tm "dest_max" "max term"
162  val is_max = can dest_max
163  fun mk_max(t1, t2) = list_mk_comb(max_tm, [t1, t2])
164
165
166  fun int_of_term t = let
167    val (is_pos, n) =
168        case Lib.total dest_negated t of
169          NONE => (true, numSyntax.dest_numeral (dest_injected t))
170        | SOME neg_i => (false, numSyntax.dest_numeral (dest_injected neg_i))
171  in
172    if is_pos then Arbint.fromNat n
173    else Arbint.~(Arbint.fromNat n)
174  end
175
176end ;
177