haftmann@30374: theory Predicate_Compile
haftmann@30810: imports Complex_Main Code_Index Lattice_Syntax
haftmann@30374: uses "predicate_compile.ML"
haftmann@30374: begin
haftmann@30374: 
haftmann@30374: setup {* Predicate_Compile.setup *}
haftmann@30374: 
bulwahn@31106: ML {*
bulwahn@31106:   OuterSyntax.local_theory_to_proof "code_pred" "sets up goal for cases rule from given introduction rules and compiles predicate"
bulwahn@31106:   OuterKeyword.thy_goal (OuterParse.term_group >> Predicate_Compile.code_pred_cmd)
bulwahn@31106: *}
bulwahn@31106: 
haftmann@30374: primrec "next" :: "('a Predicate.pred \<Rightarrow> ('a \<times> 'a Predicate.pred) option)
haftmann@30374:   \<Rightarrow> 'a Predicate.seq \<Rightarrow> ('a \<times> 'a Predicate.pred) option" where
haftmann@30374:     "next yield Predicate.Empty = None"
haftmann@30374:   | "next yield (Predicate.Insert x P) = Some (x, P)"
haftmann@30374:   | "next yield (Predicate.Join P xq) = (case yield P
haftmann@30374:    of None \<Rightarrow> next yield xq | Some (x, Q) \<Rightarrow> Some (x, Predicate.Seq (\<lambda>_. Predicate.Join Q xq)))"
haftmann@30374: 
haftmann@30810: ML {*
haftmann@30810: let
haftmann@30810:   fun yield (@{code Predicate.Seq} f) = @{code next} yield (f ())
haftmann@30810: in
haftmann@30810:   yield @{code "\<bottom> :: 'a Predicate.pred"} (*replace bottom with sequence to evaluate*)
haftmann@30810: end
haftmann@30810: *}
haftmann@30810: 
haftmann@30812: fun anamorph :: "('b \<Rightarrow> ('a \<times> 'b) option) \<Rightarrow> index \<Rightarrow> 'b \<Rightarrow> 'a list \<times> 'b" where
haftmann@30812:   "anamorph f k x = (if k = 0 then ([], x)
haftmann@30812:     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: 
haftmann@30810: ML {*
haftmann@30810: let
haftmann@30810:   fun yield (@{code Predicate.Seq} f) = @{code next} yield (f ())
haftmann@30812:   fun yieldn k = @{code anamorph} yield k
haftmann@30810: in
haftmann@30810:   yieldn 0 (*replace with number of elements to retrieve*)
haftmann@30810:     @{code "\<bottom> :: 'a Predicate.pred"} (*replace bottom with sequence to evaluate*)
haftmann@30810: end
haftmann@30810: *}
haftmann@30374: 
bulwahn@31106: section {* Example for user interface *}
bulwahn@31106: 
bulwahn@31106: inductive append ::  "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list \<Rightarrow> bool"
bulwahn@31106: where
bulwahn@31106:   "append [] ys ys"
bulwahn@31106: | "append xs' ys zs' \<Longrightarrow> append (x#xs') ys (x#zs')"
bulwahn@31106: 
bulwahn@31106: code_pred append
bulwahn@31106:   using assms by (rule append.cases)
bulwahn@31106: 
bulwahn@31107: thm append_codegen
bulwahn@31106: thm append_cases
bulwahn@31106: 
bulwahn@31106: 
haftmann@30374: end