author | bulwahn |
Mon, 11 May 2009 09:39:53 +0200 | |
changeset 31107 | 657386d94f14 |
parent 31106 | 9a1178204dc0 |
child 31108 | 0ce5f53fc65d |
permissions | -rw-r--r-- |
haftmann@30374 | 1 |
theory Predicate_Compile |
haftmann@30810 | 2 |
imports Complex_Main Code_Index Lattice_Syntax |
haftmann@30374 | 3 |
uses "predicate_compile.ML" |
haftmann@30374 | 4 |
begin |
haftmann@30374 | 5 |
|
haftmann@30374 | 6 |
setup {* Predicate_Compile.setup *} |
haftmann@30374 | 7 |
|
bulwahn@31106 | 8 |
ML {* |
bulwahn@31106 | 9 |
OuterSyntax.local_theory_to_proof "code_pred" "sets up goal for cases rule from given introduction rules and compiles predicate" |
bulwahn@31106 | 10 |
OuterKeyword.thy_goal (OuterParse.term_group >> Predicate_Compile.code_pred_cmd) |
bulwahn@31106 | 11 |
*} |
bulwahn@31106 | 12 |
|
haftmann@30374 | 13 |
primrec "next" :: "('a Predicate.pred \<Rightarrow> ('a \<times> 'a Predicate.pred) option) |
haftmann@30374 | 14 |
\<Rightarrow> 'a Predicate.seq \<Rightarrow> ('a \<times> 'a Predicate.pred) option" where |
haftmann@30374 | 15 |
"next yield Predicate.Empty = None" |
haftmann@30374 | 16 |
| "next yield (Predicate.Insert x P) = Some (x, P)" |
haftmann@30374 | 17 |
| "next yield (Predicate.Join P xq) = (case yield P |
haftmann@30374 | 18 |
of None \<Rightarrow> next yield xq | Some (x, Q) \<Rightarrow> Some (x, Predicate.Seq (\<lambda>_. Predicate.Join Q xq)))" |
haftmann@30374 | 19 |
|
haftmann@30810 | 20 |
ML {* |
haftmann@30810 | 21 |
let |
haftmann@30810 | 22 |
fun yield (@{code Predicate.Seq} f) = @{code next} yield (f ()) |
haftmann@30810 | 23 |
in |
haftmann@30810 | 24 |
yield @{code "\<bottom> :: 'a Predicate.pred"} (*replace bottom with sequence to evaluate*) |
haftmann@30810 | 25 |
end |
haftmann@30810 | 26 |
*} |
haftmann@30810 | 27 |
|
haftmann@30812 | 28 |
fun anamorph :: "('b \<Rightarrow> ('a \<times> 'b) option) \<Rightarrow> index \<Rightarrow> 'b \<Rightarrow> 'a list \<times> 'b" where |
haftmann@30812 | 29 |
"anamorph f k x = (if k = 0 then ([], x) |
haftmann@30812 | 30 |
else case f x of None \<Rightarrow> ([], x) | Some (v, y) \<Rightarrow> let (vs, z) = anamorph f (k - 1) y in (v # vs, z))" |
haftmann@30810 | 31 |
|
haftmann@30810 | 32 |
ML {* |
haftmann@30810 | 33 |
let |
haftmann@30810 | 34 |
fun yield (@{code Predicate.Seq} f) = @{code next} yield (f ()) |
haftmann@30812 | 35 |
fun yieldn k = @{code anamorph} yield k |
haftmann@30810 | 36 |
in |
haftmann@30810 | 37 |
yieldn 0 (*replace with number of elements to retrieve*) |
haftmann@30810 | 38 |
@{code "\<bottom> :: 'a Predicate.pred"} (*replace bottom with sequence to evaluate*) |
haftmann@30810 | 39 |
end |
haftmann@30810 | 40 |
*} |
haftmann@30374 | 41 |
|
bulwahn@31106 | 42 |
section {* Example for user interface *} |
bulwahn@31106 | 43 |
|
bulwahn@31106 | 44 |
inductive append :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list \<Rightarrow> bool" |
bulwahn@31106 | 45 |
where |
bulwahn@31106 | 46 |
"append [] ys ys" |
bulwahn@31106 | 47 |
| "append xs' ys zs' \<Longrightarrow> append (x#xs') ys (x#zs')" |
bulwahn@31106 | 48 |
|
bulwahn@31106 | 49 |
code_pred append |
bulwahn@31106 | 50 |
using assms by (rule append.cases) |
bulwahn@31106 | 51 |
|
bulwahn@31107 | 52 |
thm append_codegen |
bulwahn@31106 | 53 |
thm append_cases |
bulwahn@31106 | 54 |
|
bulwahn@31106 | 55 |
|
haftmann@30374 | 56 |
end |