author | haftmann |
Tue, 31 Mar 2009 11:11:36 +0200 | |
changeset 30812 | 7d02340f095d |
parent 30810 | 83642621425a |
child 30953 | d5f5ab29d769 |
child 31106 | 9a1178204dc0 |
permissions | -rw-r--r-- |
30374
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
1 |
theory Predicate_Compile |
30810 | 2 |
imports Complex_Main Code_Index Lattice_Syntax |
30374
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
3 |
uses "predicate_compile.ML" |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
4 |
begin |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
5 |
|
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
6 |
setup {* Predicate_Compile.setup *} |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
7 |
|
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
8 |
primrec "next" :: "('a Predicate.pred \<Rightarrow> ('a \<times> 'a Predicate.pred) option) |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
9 |
\<Rightarrow> 'a Predicate.seq \<Rightarrow> ('a \<times> 'a Predicate.pred) option" where |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
10 |
"next yield Predicate.Empty = None" |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
11 |
| "next yield (Predicate.Insert x P) = Some (x, P)" |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
12 |
| "next yield (Predicate.Join P xq) = (case yield P |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
13 |
of None \<Rightarrow> next yield xq | Some (x, Q) \<Rightarrow> Some (x, Predicate.Seq (\<lambda>_. Predicate.Join Q xq)))" |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
14 |
|
30810 | 15 |
ML {* |
16 |
let |
|
17 |
fun yield (@{code Predicate.Seq} f) = @{code next} yield (f ()) |
|
18 |
in |
|
19 |
yield @{code "\<bottom> :: 'a Predicate.pred"} (*replace bottom with sequence to evaluate*) |
|
20 |
end |
|
21 |
*} |
|
22 |
||
30812 | 23 |
fun anamorph :: "('b \<Rightarrow> ('a \<times> 'b) option) \<Rightarrow> index \<Rightarrow> 'b \<Rightarrow> 'a list \<times> 'b" where |
24 |
"anamorph f k x = (if k = 0 then ([], x) |
|
25 |
else case f x of None \<Rightarrow> ([], x) | Some (v, y) \<Rightarrow> let (vs, z) = anamorph f (k - 1) y in (v # vs, z))" |
|
30810 | 26 |
|
27 |
ML {* |
|
28 |
let |
|
29 |
fun yield (@{code Predicate.Seq} f) = @{code next} yield (f ()) |
|
30812 | 30 |
fun yieldn k = @{code anamorph} yield k |
30810 | 31 |
in |
32 |
yieldn 0 (*replace with number of elements to retrieve*) |
|
33 |
@{code "\<bottom> :: 'a Predicate.pred"} (*replace bottom with sequence to evaluate*) |
|
34 |
end |
|
35 |
*} |
|
30374
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
36 |
|
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
37 |
end |