src/HOL/ex/Predicate_Compile.thy
author haftmann
Mon, 20 Apr 2009 09:32:09 +0200
changeset 30953 d5f5ab29d769
parent 30812 7d02340f095d
child 30972 5b65835ccc92
permissions -rw-r--r--
yield is now a static ML function
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
30374
7311a1546d85 added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff changeset
     1
theory Predicate_Compile
30810
83642621425a ML snippets for experimental evaluation
haftmann
parents: 30374
diff changeset
     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
30812
7d02340f095d generalized pull to anamorph
haftmann
parents: 30810
diff changeset
    15
fun anamorph :: "('b \<Rightarrow> ('a \<times> 'b) option) \<Rightarrow> index \<Rightarrow> 'b \<Rightarrow> 'a list \<times> 'b" where
7d02340f095d generalized pull to anamorph
haftmann
parents: 30810
diff changeset
    16
  "anamorph f k x = (if k = 0 then ([], x)
7d02340f095d generalized pull to anamorph
haftmann
parents: 30810
diff changeset
    17
    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
83642621425a ML snippets for experimental evaluation
haftmann
parents: 30374
diff changeset
    18
83642621425a ML snippets for experimental evaluation
haftmann
parents: 30374
diff changeset
    19
ML {*
30953
d5f5ab29d769 yield is now a static ML function
haftmann
parents: 30812
diff changeset
    20
structure Predicate =
d5f5ab29d769 yield is now a static ML function
haftmann
parents: 30812
diff changeset
    21
struct
d5f5ab29d769 yield is now a static ML function
haftmann
parents: 30812
diff changeset
    22
d5f5ab29d769 yield is now a static ML function
haftmann
parents: 30812
diff changeset
    23
open Predicate;
d5f5ab29d769 yield is now a static ML function
haftmann
parents: 30812
diff changeset
    24
d5f5ab29d769 yield is now a static ML function
haftmann
parents: 30812
diff changeset
    25
fun yield (Predicate.Seq f) = @{code next} yield (f ());
d5f5ab29d769 yield is now a static ML function
haftmann
parents: 30812
diff changeset
    26
d5f5ab29d769 yield is now a static ML function
haftmann
parents: 30812
diff changeset
    27
fun yieldn k = @{code anamorph} yield k;
d5f5ab29d769 yield is now a static ML function
haftmann
parents: 30812
diff changeset
    28
d5f5ab29d769 yield is now a static ML function
haftmann
parents: 30812
diff changeset
    29
end;
30810
83642621425a ML snippets for experimental evaluation
haftmann
parents: 30374
diff changeset
    30
*}
30374
7311a1546d85 added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff changeset
    31
7311a1546d85 added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff changeset
    32
end