src/HOL/ex/Predicate_Compile.thy
author haftmann
Fri, 24 Apr 2009 17:45:16 +0200
changeset 30972 5b65835ccc92
parent 30953 d5f5ab29d769
child 31108 0ce5f53fc65d
permissions -rw-r--r--
some experiements towards user interface for predicate compiler
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
30972
5b65835ccc92 some experiements towards user interface for predicate compiler
haftmann
parents: 30953
diff changeset
     2
imports Complex_Main Lattice_Syntax Code_Eval
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
30972
5b65835ccc92 some experiements towards user interface for predicate compiler
haftmann
parents: 30953
diff changeset
     6
text {* Package setup *}
5b65835ccc92 some experiements towards user interface for predicate compiler
haftmann
parents: 30953
diff changeset
     7
30374
7311a1546d85 added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff changeset
     8
setup {* Predicate_Compile.setup *}
7311a1546d85 added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff changeset
     9
30972
5b65835ccc92 some experiements towards user interface for predicate compiler
haftmann
parents: 30953
diff changeset
    10
5b65835ccc92 some experiements towards user interface for predicate compiler
haftmann
parents: 30953
diff changeset
    11
text {* Experimental code *}
30374
7311a1546d85 added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff changeset
    12
30972
5b65835ccc92 some experiements towards user interface for predicate compiler
haftmann
parents: 30953
diff changeset
    13
definition pred_map :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a Predicate.pred \<Rightarrow> 'b Predicate.pred" where
5b65835ccc92 some experiements towards user interface for predicate compiler
haftmann
parents: 30953
diff changeset
    14
  "pred_map f P = Predicate.bind P (Predicate.single o f)"
30810
83642621425a ML snippets for experimental evaluation
haftmann
parents: 30374
diff changeset
    15
83642621425a ML snippets for experimental evaluation
haftmann
parents: 30374
diff changeset
    16
ML {*
30953
d5f5ab29d769 yield is now a static ML function
haftmann
parents: 30812
diff changeset
    17
structure Predicate =
d5f5ab29d769 yield is now a static ML function
haftmann
parents: 30812
diff changeset
    18
struct
d5f5ab29d769 yield is now a static ML function
haftmann
parents: 30812
diff changeset
    19
d5f5ab29d769 yield is now a static ML function
haftmann
parents: 30812
diff changeset
    20
open Predicate;
d5f5ab29d769 yield is now a static ML function
haftmann
parents: 30812
diff changeset
    21
30972
5b65835ccc92 some experiements towards user interface for predicate compiler
haftmann
parents: 30953
diff changeset
    22
val pred_ref = ref (NONE : (unit -> term Predicate.pred) option);
5b65835ccc92 some experiements towards user interface for predicate compiler
haftmann
parents: 30953
diff changeset
    23
5b65835ccc92 some experiements towards user interface for predicate compiler
haftmann
parents: 30953
diff changeset
    24
fun eval_pred thy t =
5b65835ccc92 some experiements towards user interface for predicate compiler
haftmann
parents: 30953
diff changeset
    25
  t 
5b65835ccc92 some experiements towards user interface for predicate compiler
haftmann
parents: 30953
diff changeset
    26
  |> Eval.mk_term_of (fastype_of t)
5b65835ccc92 some experiements towards user interface for predicate compiler
haftmann
parents: 30953
diff changeset
    27
  |> (fn t => Code_ML.eval NONE ("Predicate.pred_ref", pred_ref) @{code pred_map} thy t []);
5b65835ccc92 some experiements towards user interface for predicate compiler
haftmann
parents: 30953
diff changeset
    28
5b65835ccc92 some experiements towards user interface for predicate compiler
haftmann
parents: 30953
diff changeset
    29
fun eval_pred_elems thy t T length =
5b65835ccc92 some experiements towards user interface for predicate compiler
haftmann
parents: 30953
diff changeset
    30
  t |> eval_pred thy |> yieldn length |> fst |> HOLogic.mk_list T;
30953
d5f5ab29d769 yield is now a static ML function
haftmann
parents: 30812
diff changeset
    31
30972
5b65835ccc92 some experiements towards user interface for predicate compiler
haftmann
parents: 30953
diff changeset
    32
fun analyze_compr thy t =
5b65835ccc92 some experiements towards user interface for predicate compiler
haftmann
parents: 30953
diff changeset
    33
  let
5b65835ccc92 some experiements towards user interface for predicate compiler
haftmann
parents: 30953
diff changeset
    34
    val split = case t of (Const (@{const_name Collect}, _) $ t') => t'
5b65835ccc92 some experiements towards user interface for predicate compiler
haftmann
parents: 30953
diff changeset
    35
      | _ => error ("Not a set comprehension: " ^ Syntax.string_of_term_global thy t);
5b65835ccc92 some experiements towards user interface for predicate compiler
haftmann
parents: 30953
diff changeset
    36
    val (body, Ts, fp) = HOLogic.strip_split split;
5b65835ccc92 some experiements towards user interface for predicate compiler
haftmann
parents: 30953
diff changeset
    37
    val (t_pred, args) = strip_comb body;
5b65835ccc92 some experiements towards user interface for predicate compiler
haftmann
parents: 30953
diff changeset
    38
    val pred = case t_pred of Const (pred, _) => pred
5b65835ccc92 some experiements towards user interface for predicate compiler
haftmann
parents: 30953
diff changeset
    39
      | _ => error ("Not a constant: " ^ Syntax.string_of_term_global thy t_pred);
5b65835ccc92 some experiements towards user interface for predicate compiler
haftmann
parents: 30953
diff changeset
    40
    val mode = map is_Bound args; (*FIXME what about higher-order modes?*)
5b65835ccc92 some experiements towards user interface for predicate compiler
haftmann
parents: 30953
diff changeset
    41
    val args' = filter_out is_Bound args;
5b65835ccc92 some experiements towards user interface for predicate compiler
haftmann
parents: 30953
diff changeset
    42
    val T = HOLogic.mk_tupleT fp Ts;
5b65835ccc92 some experiements towards user interface for predicate compiler
haftmann
parents: 30953
diff changeset
    43
    val mk = HOLogic.mk_tuple' fp T;
5b65835ccc92 some experiements towards user interface for predicate compiler
haftmann
parents: 30953
diff changeset
    44
  in (((pred, mode), args), (mk, T)) end;
30953
d5f5ab29d769 yield is now a static ML function
haftmann
parents: 30812
diff changeset
    45
d5f5ab29d769 yield is now a static ML function
haftmann
parents: 30812
diff changeset
    46
end;
30810
83642621425a ML snippets for experimental evaluation
haftmann
parents: 30374
diff changeset
    47
*}
30374
7311a1546d85 added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff changeset
    48
30972
5b65835ccc92 some experiements towards user interface for predicate compiler
haftmann
parents: 30953
diff changeset
    49
5b65835ccc92 some experiements towards user interface for predicate compiler
haftmann
parents: 30953
diff changeset
    50
text {* Example(s) *}
5b65835ccc92 some experiements towards user interface for predicate compiler
haftmann
parents: 30953
diff changeset
    51
5b65835ccc92 some experiements towards user interface for predicate compiler
haftmann
parents: 30953
diff changeset
    52
inductive even :: "nat \<Rightarrow> bool" and odd :: "nat \<Rightarrow> bool" where
5b65835ccc92 some experiements towards user interface for predicate compiler
haftmann
parents: 30953
diff changeset
    53
    "even 0"
5b65835ccc92 some experiements towards user interface for predicate compiler
haftmann
parents: 30953
diff changeset
    54
  | "even n \<Longrightarrow> odd (Suc n)"
5b65835ccc92 some experiements towards user interface for predicate compiler
haftmann
parents: 30953
diff changeset
    55
  | "odd n \<Longrightarrow> even (Suc n)"
5b65835ccc92 some experiements towards user interface for predicate compiler
haftmann
parents: 30953
diff changeset
    56
5b65835ccc92 some experiements towards user interface for predicate compiler
haftmann
parents: 30953
diff changeset
    57
setup {* pred_compile "even" *}
5b65835ccc92 some experiements towards user interface for predicate compiler
haftmann
parents: 30953
diff changeset
    58
thm even_codegen
5b65835ccc92 some experiements towards user interface for predicate compiler
haftmann
parents: 30953
diff changeset
    59
5b65835ccc92 some experiements towards user interface for predicate compiler
haftmann
parents: 30953
diff changeset
    60
5b65835ccc92 some experiements towards user interface for predicate compiler
haftmann
parents: 30953
diff changeset
    61
inductive append :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list \<Rightarrow> bool" where
5b65835ccc92 some experiements towards user interface for predicate compiler
haftmann
parents: 30953
diff changeset
    62
    append_Nil: "append [] xs xs"
5b65835ccc92 some experiements towards user interface for predicate compiler
haftmann
parents: 30953
diff changeset
    63
  | append_Cons: "append xs ys zs \<Longrightarrow> append (x # xs) ys (x # zs)"
5b65835ccc92 some experiements towards user interface for predicate compiler
haftmann
parents: 30953
diff changeset
    64
5b65835ccc92 some experiements towards user interface for predicate compiler
haftmann
parents: 30953
diff changeset
    65
setup {* pred_compile "append" *}
5b65835ccc92 some experiements towards user interface for predicate compiler
haftmann
parents: 30953
diff changeset
    66
thm append_codegen
5b65835ccc92 some experiements towards user interface for predicate compiler
haftmann
parents: 30953
diff changeset
    67
5b65835ccc92 some experiements towards user interface for predicate compiler
haftmann
parents: 30953
diff changeset
    68
5b65835ccc92 some experiements towards user interface for predicate compiler
haftmann
parents: 30953
diff changeset
    69
inductive partition :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> 'a list \<Rightarrow> 'a list \<Rightarrow> bool"
5b65835ccc92 some experiements towards user interface for predicate compiler
haftmann
parents: 30953
diff changeset
    70
  for f where
5b65835ccc92 some experiements towards user interface for predicate compiler
haftmann
parents: 30953
diff changeset
    71
    "partition f [] [] []"
5b65835ccc92 some experiements towards user interface for predicate compiler
haftmann
parents: 30953
diff changeset
    72
  | "f x \<Longrightarrow> partition f xs ys zs \<Longrightarrow> partition f (x # xs) (x # ys) zs"
5b65835ccc92 some experiements towards user interface for predicate compiler
haftmann
parents: 30953
diff changeset
    73
  | "\<not> f x \<Longrightarrow> partition f xs ys zs \<Longrightarrow> partition f (x # xs) ys (x # zs)"
5b65835ccc92 some experiements towards user interface for predicate compiler
haftmann
parents: 30953
diff changeset
    74
5b65835ccc92 some experiements towards user interface for predicate compiler
haftmann
parents: 30953
diff changeset
    75
setup {* pred_compile "partition" *}
5b65835ccc92 some experiements towards user interface for predicate compiler
haftmann
parents: 30953
diff changeset
    76
thm partition_codegen
5b65835ccc92 some experiements towards user interface for predicate compiler
haftmann
parents: 30953
diff changeset
    77
5b65835ccc92 some experiements towards user interface for predicate compiler
haftmann
parents: 30953
diff changeset
    78
setup {* pred_compile "tranclp" *}
5b65835ccc92 some experiements towards user interface for predicate compiler
haftmann
parents: 30953
diff changeset
    79
thm tranclp_codegen
5b65835ccc92 some experiements towards user interface for predicate compiler
haftmann
parents: 30953
diff changeset
    80
5b65835ccc92 some experiements towards user interface for predicate compiler
haftmann
parents: 30953
diff changeset
    81
ML_val {* Predicate_Compile.modes_of @{theory} @{const_name partition} *}
5b65835ccc92 some experiements towards user interface for predicate compiler
haftmann
parents: 30953
diff changeset
    82
ML_val {* Predicate_Compile.modes_of @{theory} @{const_name tranclp} *}
5b65835ccc92 some experiements towards user interface for predicate compiler
haftmann
parents: 30953
diff changeset
    83
5b65835ccc92 some experiements towards user interface for predicate compiler
haftmann
parents: 30953
diff changeset
    84
ML_val {* Predicate.analyze_compr @{theory} @{term "{n. odd n}"} *}
5b65835ccc92 some experiements towards user interface for predicate compiler
haftmann
parents: 30953
diff changeset
    85
30374
7311a1546d85 added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff changeset
    86
end