src/HOL/ex/Predicate_Compile.thy
author haftmann
Wed, 20 May 2009 22:24:07 +0200
changeset 31217 c025f32afd4e
parent 31140 e5f8c1c420f3
child 31225 df6945ac4193
permissions -rw-r--r--
experimental values command
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
text {* Experimental code *}
30374
7311a1546d85 added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff changeset
    11
30810
83642621425a ML snippets for experimental evaluation
haftmann
parents: 30374
diff changeset
    12
ML {*
31217
c025f32afd4e experimental values command
haftmann
parents: 31140
diff changeset
    13
structure Predicate_Compile =
30953
d5f5ab29d769 yield is now a static ML function
haftmann
parents: 30812
diff changeset
    14
struct
d5f5ab29d769 yield is now a static ML function
haftmann
parents: 30812
diff changeset
    15
31217
c025f32afd4e experimental values command
haftmann
parents: 31140
diff changeset
    16
open Predicate_Compile;
30972
5b65835ccc92 some experiements towards user interface for predicate compiler
haftmann
parents: 30953
diff changeset
    17
31217
c025f32afd4e experimental values command
haftmann
parents: 31140
diff changeset
    18
fun eval thy t_compr =
c025f32afd4e experimental values command
haftmann
parents: 31140
diff changeset
    19
  let
c025f32afd4e experimental values command
haftmann
parents: 31140
diff changeset
    20
    val t = Predicate_Compile.analyze_compr thy t_compr;
c025f32afd4e experimental values command
haftmann
parents: 31140
diff changeset
    21
    val Type (@{type_name Predicate.pred}, [T]) = fastype_of t;
c025f32afd4e experimental values command
haftmann
parents: 31140
diff changeset
    22
    fun mk_predT T = Type (@{type_name Predicate.pred}, [T]);
c025f32afd4e experimental values command
haftmann
parents: 31140
diff changeset
    23
    val T1 = T --> @{typ term};
c025f32afd4e experimental values command
haftmann
parents: 31140
diff changeset
    24
    val T2 = T1 --> mk_predT T --> mk_predT @{typ term};
c025f32afd4e experimental values command
haftmann
parents: 31140
diff changeset
    25
    val t' = Const (@{const_name Predicate.map}, T2) (*FIXME*)
c025f32afd4e experimental values command
haftmann
parents: 31140
diff changeset
    26
      $ Const (@{const_name Code_Eval.term_of}, T1) $ t;
c025f32afd4e experimental values command
haftmann
parents: 31140
diff changeset
    27
  in (T, Code_ML.eval NONE ("Predicate_Compile.eval_ref", eval_ref) @{code Predicate.map} thy t' []) end;
30972
5b65835ccc92 some experiements towards user interface for predicate compiler
haftmann
parents: 30953
diff changeset
    28
31217
c025f32afd4e experimental values command
haftmann
parents: 31140
diff changeset
    29
fun values ctxt k t_compr =
c025f32afd4e experimental values command
haftmann
parents: 31140
diff changeset
    30
  let
c025f32afd4e experimental values command
haftmann
parents: 31140
diff changeset
    31
    val thy = ProofContext.theory_of ctxt;
c025f32afd4e experimental values command
haftmann
parents: 31140
diff changeset
    32
    val (T, t') = eval thy t_compr;
c025f32afd4e experimental values command
haftmann
parents: 31140
diff changeset
    33
  in t' |> Predicate.yieldn k |> fst |> HOLogic.mk_list T end;
30953
d5f5ab29d769 yield is now a static ML function
haftmann
parents: 30812
diff changeset
    34
31217
c025f32afd4e experimental values command
haftmann
parents: 31140
diff changeset
    35
fun values_cmd modes k raw_t state =
30972
5b65835ccc92 some experiements towards user interface for predicate compiler
haftmann
parents: 30953
diff changeset
    36
  let
31217
c025f32afd4e experimental values command
haftmann
parents: 31140
diff changeset
    37
    val ctxt = Toplevel.context_of state;
c025f32afd4e experimental values command
haftmann
parents: 31140
diff changeset
    38
    val t = Syntax.read_term ctxt raw_t;
c025f32afd4e experimental values command
haftmann
parents: 31140
diff changeset
    39
    val t' = values ctxt k t;
c025f32afd4e experimental values command
haftmann
parents: 31140
diff changeset
    40
    val ty' = Term.type_of t';
c025f32afd4e experimental values command
haftmann
parents: 31140
diff changeset
    41
    val ctxt' = Variable.auto_fixes t' ctxt;
c025f32afd4e experimental values command
haftmann
parents: 31140
diff changeset
    42
    val p = PrintMode.with_modes modes (fn () =>
c025f32afd4e experimental values command
haftmann
parents: 31140
diff changeset
    43
      Pretty.block [Pretty.quote (Syntax.pretty_term ctxt' t'), Pretty.fbrk,
c025f32afd4e experimental values command
haftmann
parents: 31140
diff changeset
    44
        Pretty.str "::", Pretty.brk 1, Pretty.quote (Syntax.pretty_typ ctxt' ty')]) ();
c025f32afd4e experimental values command
haftmann
parents: 31140
diff changeset
    45
  in Pretty.writeln p end;
c025f32afd4e experimental values command
haftmann
parents: 31140
diff changeset
    46
c025f32afd4e experimental values command
haftmann
parents: 31140
diff changeset
    47
end;
c025f32afd4e experimental values command
haftmann
parents: 31140
diff changeset
    48
c025f32afd4e experimental values command
haftmann
parents: 31140
diff changeset
    49
local structure P = OuterParse in
c025f32afd4e experimental values command
haftmann
parents: 31140
diff changeset
    50
c025f32afd4e experimental values command
haftmann
parents: 31140
diff changeset
    51
val opt_modes = Scan.optional (P.$$$ "(" |-- P.!!! (Scan.repeat1 P.xname --| P.$$$ ")")) [];
c025f32afd4e experimental values command
haftmann
parents: 31140
diff changeset
    52
c025f32afd4e experimental values command
haftmann
parents: 31140
diff changeset
    53
val _ = OuterSyntax.improper_command "values" "enumerate and print comprehensions" OuterKeyword.diag
c025f32afd4e experimental values command
haftmann
parents: 31140
diff changeset
    54
  (opt_modes -- Scan.optional P.nat ~1 -- P.term
c025f32afd4e experimental values command
haftmann
parents: 31140
diff changeset
    55
    >> (fn ((modes, k), t) => Toplevel.no_timing o Toplevel.keep
c025f32afd4e experimental values command
haftmann
parents: 31140
diff changeset
    56
        (Predicate_Compile.values_cmd modes k t)));
30953
d5f5ab29d769 yield is now a static ML function
haftmann
parents: 30812
diff changeset
    57
d5f5ab29d769 yield is now a static ML function
haftmann
parents: 30812
diff changeset
    58
end;
30810
83642621425a ML snippets for experimental evaluation
haftmann
parents: 30374
diff changeset
    59
*}
30374
7311a1546d85 added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff changeset
    60
7311a1546d85 added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff changeset
    61
end