author | haftmann |
Sun, 08 Mar 2009 15:25:28 +0100 | |
changeset 30374 | 7311a1546d85 |
child 30810 | 83642621425a |
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 |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
2 |
imports Complex_Main Lattice_Syntax |
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 |
|
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
15 |
primrec pull :: "('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
|
16 |
\<Rightarrow> nat \<Rightarrow> 'a Predicate.pred \<Rightarrow> 'a list \<times> 'a Predicate.pred" where |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
17 |
"pull yield 0 P = ([], \<bottom>)" |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
18 |
| "pull yield (Suc n) P = (case yield P |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
19 |
of None \<Rightarrow> ([], \<bottom>) | Some (x, Q) \<Rightarrow> let (xs, R) = pull yield n Q in (x # xs, R))" |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
20 |
|
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
21 |
end |