19039
|
1 |
ML {*
|
|
2 |
|
|
3 |
fun strip_abs_split 0 t = ([], t)
|
|
4 |
| strip_abs_split i (Abs (s, T, t)) =
|
|
5 |
let
|
|
6 |
val s' = Codegen.new_name t s;
|
|
7 |
val v = Free (s', T)
|
|
8 |
in apfst (cons v) (strip_abs_split (i-1) (subst_bound (v, t))) end
|
|
9 |
| strip_abs_split i (u as Const ("split", _) $ t) = (case strip_abs_split (i+1) t of
|
|
10 |
(v :: v' :: vs, u) => (HOLogic.mk_prod (v, v') :: vs, u)
|
|
11 |
| _ => ([], u))
|
|
12 |
| strip_abs_split i t = ([], t);
|
|
13 |
|
|
14 |
fun let_codegen thy defs gr dep thyname brack t = (case strip_comb t of
|
|
15 |
(t1 as Const ("Let", _), t2 :: t3 :: ts) =>
|
|
16 |
let
|
|
17 |
fun dest_let (l as Const ("Let", _) $ t $ u) =
|
|
18 |
(case strip_abs_split 1 u of
|
|
19 |
([p], u') => apfst (cons (p, t)) (dest_let u')
|
|
20 |
| _ => ([], l))
|
|
21 |
| dest_let t = ([], t);
|
|
22 |
fun mk_code (gr, (l, r)) =
|
|
23 |
let
|
|
24 |
val (gr1, pl) = Codegen.invoke_codegen thy defs dep thyname false (gr, l);
|
|
25 |
val (gr2, pr) = Codegen.invoke_codegen thy defs dep thyname false (gr1, r);
|
|
26 |
in (gr2, (pl, pr)) end
|
|
27 |
in case dest_let (t1 $ t2 $ t3) of
|
|
28 |
([], _) => NONE
|
|
29 |
| (ps, u) =>
|
|
30 |
let
|
|
31 |
val (gr1, qs) = foldl_map mk_code (gr, ps);
|
|
32 |
val (gr2, pu) = Codegen.invoke_codegen thy defs dep thyname false (gr1, u);
|
|
33 |
val (gr3, pargs) = foldl_map
|
|
34 |
(Codegen.invoke_codegen thy defs dep thyname true) (gr2, ts)
|
|
35 |
in
|
|
36 |
SOME (gr3, Codegen.mk_app brack
|
|
37 |
(Pretty.blk (0, [Pretty.str "let ", Pretty.blk (0, List.concat
|
|
38 |
(separate [Pretty.str ";", Pretty.brk 1] (map (fn (pl, pr) =>
|
|
39 |
[Pretty.block [Pretty.str "val ", pl, Pretty.str " =",
|
|
40 |
Pretty.brk 1, pr]]) qs))),
|
|
41 |
Pretty.brk 1, Pretty.str "in ", pu,
|
|
42 |
Pretty.brk 1, Pretty.str "end"])) pargs)
|
|
43 |
end
|
|
44 |
end
|
|
45 |
| _ => NONE);
|
|
46 |
|
|
47 |
fun split_codegen thy defs gr dep thyname brack t = (case strip_comb t of
|
|
48 |
(t1 as Const ("split", _), t2 :: ts) =>
|
|
49 |
(case strip_abs_split 1 (t1 $ t2) of
|
|
50 |
([p], u) =>
|
|
51 |
let
|
|
52 |
val (gr1, q) = Codegen.invoke_codegen thy defs dep thyname false (gr, p);
|
|
53 |
val (gr2, pu) = Codegen.invoke_codegen thy defs dep thyname false (gr1, u);
|
|
54 |
val (gr3, pargs) = foldl_map
|
|
55 |
(Codegen.invoke_codegen thy defs dep thyname true) (gr2, ts)
|
|
56 |
in
|
|
57 |
SOME (gr2, Codegen.mk_app brack
|
|
58 |
(Pretty.block [Pretty.str "(fn ", q, Pretty.str " =>",
|
|
59 |
Pretty.brk 1, pu, Pretty.str ")"]) pargs)
|
|
60 |
end
|
|
61 |
| _ => NONE)
|
|
62 |
| _ => NONE);
|
|
63 |
|
|
64 |
val prod_codegen_setup =
|
|
65 |
Codegen.add_codegen "let_codegen" let_codegen #>
|
|
66 |
Codegen.add_codegen "split_codegen" split_codegen #>
|
|
67 |
CodegenPackage.add_appconst
|
|
68 |
("Let", ((2, 2), CodegenPackage.appgen_let strip_abs_split)) #>
|
|
69 |
CodegenPackage.add_appconst
|
|
70 |
("split", ((1, 1), CodegenPackage.appgen_split strip_abs_split));
|
|
71 |
|
|
72 |
*}
|
|
73 |
|
|
74 |
(* Title: HOL/Library/ExecutableRat.thy
|
|
75 |
ID: $Id$
|
|
76 |
Author: Florian Haftmann, TU Muenchen
|
|
77 |
*)
|
|
78 |
|
|
79 |
header {* Executable implementation of rational numbers in HOL *}
|
|
80 |
|
|
81 |
theory ExecutableRat
|
|
82 |
imports "~~/src/HOL/Real/Rational" "~~/src/HOL/NumberTheory/IntPrimes"
|
|
83 |
begin
|
|
84 |
|
|
85 |
text {*
|
|
86 |
Actually nothing is proved about the implementation.
|
|
87 |
*}
|
|
88 |
|
|
89 |
datatype erat = Rat bool int int
|
|
90 |
|
|
91 |
instance erat :: zero by intro_classes
|
|
92 |
instance erat :: one by intro_classes
|
|
93 |
instance erat :: plus by intro_classes
|
|
94 |
instance erat :: minus by intro_classes
|
|
95 |
instance erat :: times by intro_classes
|
|
96 |
instance erat :: inverse by intro_classes
|
|
97 |
instance erat :: ord by intro_classes
|
|
98 |
|
|
99 |
consts
|
|
100 |
norm :: "erat \<Rightarrow> erat"
|
|
101 |
common :: "(int * int) * (int * int) \<Rightarrow> (int * int) * int"
|
|
102 |
of_quotient :: "int * int \<Rightarrow> erat"
|
|
103 |
of_rat :: "rat \<Rightarrow> erat"
|
|
104 |
to_rat :: "erat \<Rightarrow> rat"
|
|
105 |
|
|
106 |
defs
|
|
107 |
norm_def [simp]: "norm r == case r of (Rat a p q) \<Rightarrow>
|
|
108 |
if p = 0 then Rat True 0 1
|
|
109 |
else
|
|
110 |
let
|
|
111 |
absp = abs p
|
|
112 |
in let
|
|
113 |
m = zgcd (absp, q)
|
|
114 |
in Rat (a = (0 <= p)) (absp div m) (q div m)"
|
|
115 |
common_def [simp]: "common r == case r of ((p1, q1), (p2, q2)) \<Rightarrow>
|
|
116 |
let q' = q1 * q2 div int (gcd (nat q1, nat q2))
|
|
117 |
in ((p1 * (q' div q1), p2 * (q' div q2)), q')"
|
|
118 |
of_quotient_def [simp]: "of_quotient r == case r of (a, b) \<Rightarrow>
|
|
119 |
norm (Rat True a b)"
|
|
120 |
of_rat_def [simp]: "of_rat r == of_quotient (THE s. s : Rep_Rat r)"
|
|
121 |
to_rat_def [simp]: "to_rat r == case r of (Rat a p q) \<Rightarrow>
|
|
122 |
if a then Fract p q else Fract (uminus p) q"
|
|
123 |
|
|
124 |
consts
|
|
125 |
zero :: erat
|
|
126 |
one :: erat
|
|
127 |
add :: "erat \<Rightarrow> erat \<Rightarrow> erat"
|
|
128 |
neg :: "erat \<Rightarrow> erat"
|
|
129 |
mult :: "erat \<Rightarrow> erat \<Rightarrow> erat"
|
|
130 |
inv :: "erat \<Rightarrow> erat"
|
|
131 |
le :: "erat \<Rightarrow> erat \<Rightarrow> bool"
|
|
132 |
|
|
133 |
defs (overloaded)
|
|
134 |
zero_rat_def [simp]: "0 == Rat False 0 1"
|
|
135 |
one_rat_def [simp]: "1 == Rat False 1 1"
|
|
136 |
add_rat_def [simp]: "r + s == case r of Rat a1 p1 q1 \<Rightarrow> case s of Rat a2 p2 q2 \<Rightarrow>
|
|
137 |
let
|
|
138 |
((r1, r2), den) = common ((p1, q1), (p2, q2))
|
|
139 |
in let
|
|
140 |
num = (if a1 then r1 else -r1) + (if a2 then r2 else -r2)
|
|
141 |
in norm (Rat True num den)"
|
|
142 |
uminus_rat_def [simp]: "- r == case r of Rat a p q \<Rightarrow>
|
|
143 |
if p = 0 then Rat a p q
|
|
144 |
else Rat (\<not> a) p q"
|
|
145 |
times_rat_def [simp]: "r * s == case r of Rat a1 p1 q1 \<Rightarrow> case s of Rat a2 p2 q2 \<Rightarrow>
|
|
146 |
norm (Rat (a1 = a2) (p1 * p2) (q1 * q2))"
|
|
147 |
inverse_rat_def [simp]: "inverse r == case r of Rat a p q \<Rightarrow>
|
|
148 |
if p = 0 then arbitrary
|
|
149 |
else Rat a q p"
|
|
150 |
le_rat_def [simp]: "r <= s == case r of Rat a1 p1 q1 \<Rightarrow> case s of Rat a2 p2 q2 \<Rightarrow>
|
|
151 |
(\<not> a1 \<and> a2) \<or>
|
|
152 |
(\<not> (a1 \<and> \<not> a2) \<and>
|
|
153 |
(let
|
|
154 |
((r1, r2), dummy) = common ((p1, q1), (p2, q2))
|
|
155 |
in if a1 then r1 <= r2 else r2 <= r1))"
|
|
156 |
|
|
157 |
code_syntax_tyco rat
|
|
158 |
ml (target_atom "{*erat*}")
|
|
159 |
haskell (target_atom "{*erat*}")
|
|
160 |
|
|
161 |
code_alias
|
|
162 |
(* an intermediate solution until name resolving of ad-hoc overloaded
|
|
163 |
constants is refined *)
|
|
164 |
"HOL.inverse" "Rational.inverse"
|
|
165 |
"HOL.divide" "Rational.divide"
|
|
166 |
|
|
167 |
code_syntax_const
|
|
168 |
Fract
|
|
169 |
ml ("{*of_quotient*}")
|
|
170 |
haskell ("{*of_quotient*}")
|
|
171 |
0 :: "rat"
|
|
172 |
ml ("{*0::erat*}")
|
|
173 |
haskell ("{*1::erat*}")
|
|
174 |
1 :: "rat"
|
|
175 |
ml ("{*1::erat*}")
|
|
176 |
haskell ("{*1::erat*}")
|
|
177 |
"op +" :: "rat \<Rightarrow> rat \<Rightarrow> rat"
|
|
178 |
ml ("{*op + :: erat \<Rightarrow> erat \<Rightarrow> erat*}")
|
|
179 |
haskell ("{*op + :: erat \<Rightarrow> erat \<Rightarrow> erat*}")
|
|
180 |
uminus :: "rat \<Rightarrow> rat"
|
|
181 |
ml ("{*uminus :: erat \<Rightarrow> erat*}")
|
|
182 |
haskell ("{*uminus :: erat \<Rightarrow> erat*}")
|
|
183 |
"op *" :: "rat \<Rightarrow> rat \<Rightarrow> rat"
|
|
184 |
ml ("{*op * :: erat \<Rightarrow> erat \<Rightarrow> erat*}")
|
|
185 |
haskell ("{*op * :: erat \<Rightarrow> erat \<Rightarrow> erat*}")
|
|
186 |
inverse :: "rat \<Rightarrow> rat"
|
|
187 |
ml ("{*inverse :: erat \<Rightarrow> erat*}")
|
|
188 |
haskell ("{*inverse :: erat \<Rightarrow> erat*}")
|
|
189 |
divide :: "rat \<Rightarrow> rat \<Rightarrow> rat"
|
|
190 |
ml ("{*op * :: erat \<Rightarrow> erat \<Rightarrow> erat*}/ _/ ({*inverse :: erat \<Rightarrow> erat*}/ _)")
|
|
191 |
haskell ("{*op * :: erat \<Rightarrow> erat \<Rightarrow> erat*}/ _/ ({*inverse :: erat \<Rightarrow> erat*}/ _)")
|
|
192 |
"op <=" :: "rat \<Rightarrow> rat \<Rightarrow> bool"
|
|
193 |
ml ("{*op <= :: erat \<Rightarrow> erat \<Rightarrow> bool*}")
|
|
194 |
haskell ("{*op <= :: erat \<Rightarrow> erat \<Rightarrow> bool*}")
|
|
195 |
|
|
196 |
end
|
|
197 |
|