src/HOL/Library/Eval.thy
author haftmann
Wed, 02 Jan 2008 15:14:15 +0100
changeset 25763 474f8ba9dfa9
parent 25691 8f8d83af100a
child 25864 11f531354852
permissions -rw-r--r--
improved evaluation mechanism
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
22525
d929a900584c cleaned up Library/ and ex/
haftmann
parents:
diff changeset
     1
(*  Title:      HOL/Library/Eval.thy
d929a900584c cleaned up Library/ and ex/
haftmann
parents:
diff changeset
     2
    ID:         $Id$
d929a900584c cleaned up Library/ and ex/
haftmann
parents:
diff changeset
     3
    Author:     Florian Haftmann, TU Muenchen
d929a900584c cleaned up Library/ and ex/
haftmann
parents:
diff changeset
     4
*)
d929a900584c cleaned up Library/ and ex/
haftmann
parents:
diff changeset
     5
d929a900584c cleaned up Library/ and ex/
haftmann
parents:
diff changeset
     6
header {* A simple term evaluation mechanism *}
d929a900584c cleaned up Library/ and ex/
haftmann
parents:
diff changeset
     7
d929a900584c cleaned up Library/ and ex/
haftmann
parents:
diff changeset
     8
theory Eval
25763
474f8ba9dfa9 improved evaluation mechanism
haftmann
parents: 25691
diff changeset
     9
imports ATP_Linkup Code_Message
22525
d929a900584c cleaned up Library/ and ex/
haftmann
parents:
diff changeset
    10
begin
d929a900584c cleaned up Library/ and ex/
haftmann
parents:
diff changeset
    11
25763
474f8ba9dfa9 improved evaluation mechanism
haftmann
parents: 25691
diff changeset
    12
subsection {* Type reflection *}
474f8ba9dfa9 improved evaluation mechanism
haftmann
parents: 25691
diff changeset
    13
474f8ba9dfa9 improved evaluation mechanism
haftmann
parents: 25691
diff changeset
    14
subsubsection {* Definition *}
474f8ba9dfa9 improved evaluation mechanism
haftmann
parents: 25691
diff changeset
    15
474f8ba9dfa9 improved evaluation mechanism
haftmann
parents: 25691
diff changeset
    16
types vname = message_string;
474f8ba9dfa9 improved evaluation mechanism
haftmann
parents: 25691
diff changeset
    17
types "class" = message_string;
474f8ba9dfa9 improved evaluation mechanism
haftmann
parents: 25691
diff changeset
    18
types sort = "class list"
474f8ba9dfa9 improved evaluation mechanism
haftmann
parents: 25691
diff changeset
    19
474f8ba9dfa9 improved evaluation mechanism
haftmann
parents: 25691
diff changeset
    20
datatype "typ" =
474f8ba9dfa9 improved evaluation mechanism
haftmann
parents: 25691
diff changeset
    21
    Type message_string "typ list"
474f8ba9dfa9 improved evaluation mechanism
haftmann
parents: 25691
diff changeset
    22
  | TFree vname sort  
474f8ba9dfa9 improved evaluation mechanism
haftmann
parents: 25691
diff changeset
    23
474f8ba9dfa9 improved evaluation mechanism
haftmann
parents: 25691
diff changeset
    24
abbreviation
474f8ba9dfa9 improved evaluation mechanism
haftmann
parents: 25691
diff changeset
    25
  Fun :: "typ \<Rightarrow> typ \<Rightarrow> typ" where
474f8ba9dfa9 improved evaluation mechanism
haftmann
parents: 25691
diff changeset
    26
  "Fun ty1 ty2 \<equiv> Type (STR ''fun'') [ty1, ty2]"
474f8ba9dfa9 improved evaluation mechanism
haftmann
parents: 25691
diff changeset
    27
474f8ba9dfa9 improved evaluation mechanism
haftmann
parents: 25691
diff changeset
    28
locale (open) pure_term_syntax = -- {* FIXME drop this *}
474f8ba9dfa9 improved evaluation mechanism
haftmann
parents: 25691
diff changeset
    29
  fixes pure_term_Type :: "message_string \<Rightarrow> typ list \<Rightarrow> typ" (infixl "{\<struct>}" 120)
474f8ba9dfa9 improved evaluation mechanism
haftmann
parents: 25691
diff changeset
    30
    and pure_term_TFree :: "vname \<Rightarrow> sort \<Rightarrow> typ" ("\<lbrace>_\<Colon>_\<rbrace>" [118, 118] 117)
474f8ba9dfa9 improved evaluation mechanism
haftmann
parents: 25691
diff changeset
    31
    and pure_term_Fun :: "typ \<Rightarrow> typ \<Rightarrow> typ" (infixr "\<rightarrow>" 114)
474f8ba9dfa9 improved evaluation mechanism
haftmann
parents: 25691
diff changeset
    32
474f8ba9dfa9 improved evaluation mechanism
haftmann
parents: 25691
diff changeset
    33
parse_translation {*
474f8ba9dfa9 improved evaluation mechanism
haftmann
parents: 25691
diff changeset
    34
let
474f8ba9dfa9 improved evaluation mechanism
haftmann
parents: 25691
diff changeset
    35
  fun Type_tr [tyco, tys] = Lexicon.const @{const_syntax Type} $ tyco $ tys
474f8ba9dfa9 improved evaluation mechanism
haftmann
parents: 25691
diff changeset
    36
    | Type_tr ts = raise TERM ("Type_tr", ts);
474f8ba9dfa9 improved evaluation mechanism
haftmann
parents: 25691
diff changeset
    37
  fun TFree_tr [v, sort] = Lexicon.const @{const_syntax TFree} $ v $ sort
474f8ba9dfa9 improved evaluation mechanism
haftmann
parents: 25691
diff changeset
    38
    | TFree_tr ts = raise TERM ("TFree_tr", ts);
474f8ba9dfa9 improved evaluation mechanism
haftmann
parents: 25691
diff changeset
    39
  fun Fun_tr [ty1, ty2] = Lexicon.const @{const_syntax Fun} $ ty1 $ ty2
474f8ba9dfa9 improved evaluation mechanism
haftmann
parents: 25691
diff changeset
    40
    | Fun_tr ts = raise TERM("Fun_tr", ts);
474f8ba9dfa9 improved evaluation mechanism
haftmann
parents: 25691
diff changeset
    41
in [
474f8ba9dfa9 improved evaluation mechanism
haftmann
parents: 25691
diff changeset
    42
  ("\\<^fixed>pure_term_Type", Type_tr),
474f8ba9dfa9 improved evaluation mechanism
haftmann
parents: 25691
diff changeset
    43
  ("\\<^fixed>pure_term_TFree", TFree_tr),
474f8ba9dfa9 improved evaluation mechanism
haftmann
parents: 25691
diff changeset
    44
  ("\\<^fixed>pure_term_Fun", Fun_tr)
474f8ba9dfa9 improved evaluation mechanism
haftmann
parents: 25691
diff changeset
    45
] end
474f8ba9dfa9 improved evaluation mechanism
haftmann
parents: 25691
diff changeset
    46
*}
474f8ba9dfa9 improved evaluation mechanism
haftmann
parents: 25691
diff changeset
    47
474f8ba9dfa9 improved evaluation mechanism
haftmann
parents: 25691
diff changeset
    48
notation (output)
474f8ba9dfa9 improved evaluation mechanism
haftmann
parents: 25691
diff changeset
    49
  Type (infixl "{\<struct>}" 120)
474f8ba9dfa9 improved evaluation mechanism
haftmann
parents: 25691
diff changeset
    50
and
474f8ba9dfa9 improved evaluation mechanism
haftmann
parents: 25691
diff changeset
    51
  TFree ("\<lbrace>_\<Colon>_\<rbrace>" [118, 118] 117)
474f8ba9dfa9 improved evaluation mechanism
haftmann
parents: 25691
diff changeset
    52
and
474f8ba9dfa9 improved evaluation mechanism
haftmann
parents: 25691
diff changeset
    53
  Fun (infixr "\<rightarrow>" 114)
474f8ba9dfa9 improved evaluation mechanism
haftmann
parents: 25691
diff changeset
    54
474f8ba9dfa9 improved evaluation mechanism
haftmann
parents: 25691
diff changeset
    55
ML {*
474f8ba9dfa9 improved evaluation mechanism
haftmann
parents: 25691
diff changeset
    56
structure Eval_Aux =
474f8ba9dfa9 improved evaluation mechanism
haftmann
parents: 25691
diff changeset
    57
struct
474f8ba9dfa9 improved evaluation mechanism
haftmann
parents: 25691
diff changeset
    58
474f8ba9dfa9 improved evaluation mechanism
haftmann
parents: 25691
diff changeset
    59
val mk_sort = HOLogic.mk_list @{typ class} o map Message_String.mk;
474f8ba9dfa9 improved evaluation mechanism
haftmann
parents: 25691
diff changeset
    60
474f8ba9dfa9 improved evaluation mechanism
haftmann
parents: 25691
diff changeset
    61
fun mk_typ f (Type (tyco, tys)) =
474f8ba9dfa9 improved evaluation mechanism
haftmann
parents: 25691
diff changeset
    62
      @{term Type} $ Message_String.mk tyco
474f8ba9dfa9 improved evaluation mechanism
haftmann
parents: 25691
diff changeset
    63
        $ HOLogic.mk_list @{typ typ} (map (mk_typ f) tys)
474f8ba9dfa9 improved evaluation mechanism
haftmann
parents: 25691
diff changeset
    64
  | mk_typ f (TFree v) =
474f8ba9dfa9 improved evaluation mechanism
haftmann
parents: 25691
diff changeset
    65
      f v;
474f8ba9dfa9 improved evaluation mechanism
haftmann
parents: 25691
diff changeset
    66
474f8ba9dfa9 improved evaluation mechanism
haftmann
parents: 25691
diff changeset
    67
end;
474f8ba9dfa9 improved evaluation mechanism
haftmann
parents: 25691
diff changeset
    68
*}
474f8ba9dfa9 improved evaluation mechanism
haftmann
parents: 25691
diff changeset
    69
474f8ba9dfa9 improved evaluation mechanism
haftmann
parents: 25691
diff changeset
    70
474f8ba9dfa9 improved evaluation mechanism
haftmann
parents: 25691
diff changeset
    71
subsubsection {* Class @{text typ_of} *}
22525
d929a900584c cleaned up Library/ and ex/
haftmann
parents:
diff changeset
    72
23062
d88d2087436d evaluation for integers
haftmann
parents: 23020
diff changeset
    73
class typ_of =
d88d2087436d evaluation for integers
haftmann
parents: 23020
diff changeset
    74
  fixes typ_of :: "'a\<Colon>{} itself \<Rightarrow> typ"
22525
d929a900584c cleaned up Library/ and ex/
haftmann
parents:
diff changeset
    75
d929a900584c cleaned up Library/ and ex/
haftmann
parents:
diff changeset
    76
ML {*
25763
474f8ba9dfa9 improved evaluation mechanism
haftmann
parents: 25691
diff changeset
    77
structure Eval_Aux =
22525
d929a900584c cleaned up Library/ and ex/
haftmann
parents:
diff changeset
    78
struct
d929a900584c cleaned up Library/ and ex/
haftmann
parents:
diff changeset
    79
25763
474f8ba9dfa9 improved evaluation mechanism
haftmann
parents: 25691
diff changeset
    80
open Eval_Aux;
474f8ba9dfa9 improved evaluation mechanism
haftmann
parents: 25691
diff changeset
    81
474f8ba9dfa9 improved evaluation mechanism
haftmann
parents: 25691
diff changeset
    82
fun mk_typ_of ty =
22525
d929a900584c cleaned up Library/ and ex/
haftmann
parents:
diff changeset
    83
  Const (@{const_name typ_of}, Term.itselfT ty --> @{typ typ})
d929a900584c cleaned up Library/ and ex/
haftmann
parents:
diff changeset
    84
    $ Logic.mk_type ty;
d929a900584c cleaned up Library/ and ex/
haftmann
parents:
diff changeset
    85
25536
01753a944433 improved
haftmann
parents: 25502
diff changeset
    86
end
22525
d929a900584c cleaned up Library/ and ex/
haftmann
parents:
diff changeset
    87
*}
d929a900584c cleaned up Library/ and ex/
haftmann
parents:
diff changeset
    88
d929a900584c cleaned up Library/ and ex/
haftmann
parents:
diff changeset
    89
setup {*
d929a900584c cleaned up Library/ and ex/
haftmann
parents:
diff changeset
    90
let
25763
474f8ba9dfa9 improved evaluation mechanism
haftmann
parents: 25691
diff changeset
    91
  open Eval_Aux;
25536
01753a944433 improved
haftmann
parents: 25502
diff changeset
    92
  fun define_typ_of ty lthy =
01753a944433 improved
haftmann
parents: 25502
diff changeset
    93
    let
01753a944433 improved
haftmann
parents: 25502
diff changeset
    94
      val lhs = Const (@{const_name typ_of}, Term.itselfT ty --> @{typ typ})
01753a944433 improved
haftmann
parents: 25502
diff changeset
    95
        $ Free ("T", Term.itselfT ty);
25763
474f8ba9dfa9 improved evaluation mechanism
haftmann
parents: 25691
diff changeset
    96
      val rhs = mk_typ (fn v => mk_typ_of (TFree v)) ty;
25603
4b7a58fc168c dropped Class.prep_spec
haftmann
parents: 25594
diff changeset
    97
      val eq = Syntax.check_term lthy (HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs)))
25536
01753a944433 improved
haftmann
parents: 25502
diff changeset
    98
    in lthy |> Specification.definition (NONE, (("", []), eq)) end;
01753a944433 improved
haftmann
parents: 25502
diff changeset
    99
  fun interpretator tyco thy =
01753a944433 improved
haftmann
parents: 25502
diff changeset
   100
    let
01753a944433 improved
haftmann
parents: 25502
diff changeset
   101
      val sorts = replicate (Sign.arity_number thy tyco) @{sort typ_of};
01753a944433 improved
haftmann
parents: 25502
diff changeset
   102
      val ty = Type (tyco, map TFree (Name.names Name.context "'a" sorts));
01753a944433 improved
haftmann
parents: 25502
diff changeset
   103
    in
01753a944433 improved
haftmann
parents: 25502
diff changeset
   104
      thy
25569
c597835d5de4 dropped Instance.instantiate
haftmann
parents: 25559
diff changeset
   105
      |> TheoryTarget.instantiation ([tyco], sorts, @{sort typ_of})
c597835d5de4 dropped Instance.instantiate
haftmann
parents: 25559
diff changeset
   106
      |> define_typ_of ty
c597835d5de4 dropped Instance.instantiate
haftmann
parents: 25559
diff changeset
   107
      |> snd
c597835d5de4 dropped Instance.instantiate
haftmann
parents: 25559
diff changeset
   108
      |> Class.prove_instantiation_instance (K (Class.intro_classes_tac []))
c597835d5de4 dropped Instance.instantiate
haftmann
parents: 25559
diff changeset
   109
      |> LocalTheory.exit
c597835d5de4 dropped Instance.instantiate
haftmann
parents: 25559
diff changeset
   110
      |> ProofContext.theory_of
25536
01753a944433 improved
haftmann
parents: 25502
diff changeset
   111
    end;
01753a944433 improved
haftmann
parents: 25502
diff changeset
   112
in TypedefPackage.interpretation interpretator end
22525
d929a900584c cleaned up Library/ and ex/
haftmann
parents:
diff changeset
   113
*}
d929a900584c cleaned up Library/ and ex/
haftmann
parents:
diff changeset
   114
25536
01753a944433 improved
haftmann
parents: 25502
diff changeset
   115
instantiation "prop" :: typ_of
01753a944433 improved
haftmann
parents: 25502
diff changeset
   116
begin
01753a944433 improved
haftmann
parents: 25502
diff changeset
   117
25666
f46ed5b333fd improved term syntax
haftmann
parents: 25603
diff changeset
   118
definition 
f46ed5b333fd improved term syntax
haftmann
parents: 25603
diff changeset
   119
  "typ_of (T\<Colon>prop itself) = Type (STR ''prop'') []"
25536
01753a944433 improved
haftmann
parents: 25502
diff changeset
   120
01753a944433 improved
haftmann
parents: 25502
diff changeset
   121
instance ..
01753a944433 improved
haftmann
parents: 25502
diff changeset
   122
01753a944433 improved
haftmann
parents: 25502
diff changeset
   123
end
01753a944433 improved
haftmann
parents: 25502
diff changeset
   124
01753a944433 improved
haftmann
parents: 25502
diff changeset
   125
instantiation itself :: (typ_of) typ_of
01753a944433 improved
haftmann
parents: 25502
diff changeset
   126
begin
01753a944433 improved
haftmann
parents: 25502
diff changeset
   127
01753a944433 improved
haftmann
parents: 25502
diff changeset
   128
definition
25666
f46ed5b333fd improved term syntax
haftmann
parents: 25603
diff changeset
   129
  "typ_of (T\<Colon>'a itself itself) = Type (STR ''itself'') [typ_of TYPE('a\<Colon>typ_of)]"
25536
01753a944433 improved
haftmann
parents: 25502
diff changeset
   130
01753a944433 improved
haftmann
parents: 25502
diff changeset
   131
instance ..
01753a944433 improved
haftmann
parents: 25502
diff changeset
   132
01753a944433 improved
haftmann
parents: 25502
diff changeset
   133
end
01753a944433 improved
haftmann
parents: 25502
diff changeset
   134
01753a944433 improved
haftmann
parents: 25502
diff changeset
   135
instantiation set :: (typ_of) typ_of
01753a944433 improved
haftmann
parents: 25502
diff changeset
   136
begin
01753a944433 improved
haftmann
parents: 25502
diff changeset
   137
 
01753a944433 improved
haftmann
parents: 25502
diff changeset
   138
definition
25666
f46ed5b333fd improved term syntax
haftmann
parents: 25603
diff changeset
   139
  "typ_of (T\<Colon>'a set itself) = Type (STR ''set'') [typ_of TYPE('a\<Colon>typ_of)]"
25536
01753a944433 improved
haftmann
parents: 25502
diff changeset
   140
01753a944433 improved
haftmann
parents: 25502
diff changeset
   141
instance ..
01753a944433 improved
haftmann
parents: 25502
diff changeset
   142
01753a944433 improved
haftmann
parents: 25502
diff changeset
   143
end
01753a944433 improved
haftmann
parents: 25502
diff changeset
   144
22525
d929a900584c cleaned up Library/ and ex/
haftmann
parents:
diff changeset
   145
25763
474f8ba9dfa9 improved evaluation mechanism
haftmann
parents: 25691
diff changeset
   146
subsubsection {* Code generator setup *}
474f8ba9dfa9 improved evaluation mechanism
haftmann
parents: 25691
diff changeset
   147
474f8ba9dfa9 improved evaluation mechanism
haftmann
parents: 25691
diff changeset
   148
lemma [code func]:
474f8ba9dfa9 improved evaluation mechanism
haftmann
parents: 25691
diff changeset
   149
  includes pure_term_syntax
474f8ba9dfa9 improved evaluation mechanism
haftmann
parents: 25691
diff changeset
   150
  shows "tyco1 {\<struct>} tys1 = tyco2 {\<struct>} tys2 \<longleftrightarrow> tyco1 = tyco2
474f8ba9dfa9 improved evaluation mechanism
haftmann
parents: 25691
diff changeset
   151
     \<and> list_all2 (op =) tys1 tys2"
474f8ba9dfa9 improved evaluation mechanism
haftmann
parents: 25691
diff changeset
   152
  by (auto simp add: list_all2_eq [symmetric])
474f8ba9dfa9 improved evaluation mechanism
haftmann
parents: 25691
diff changeset
   153
474f8ba9dfa9 improved evaluation mechanism
haftmann
parents: 25691
diff changeset
   154
code_type "typ"
474f8ba9dfa9 improved evaluation mechanism
haftmann
parents: 25691
diff changeset
   155
  (SML "Term.typ")
474f8ba9dfa9 improved evaluation mechanism
haftmann
parents: 25691
diff changeset
   156
474f8ba9dfa9 improved evaluation mechanism
haftmann
parents: 25691
diff changeset
   157
code_const Type and TFree
474f8ba9dfa9 improved evaluation mechanism
haftmann
parents: 25691
diff changeset
   158
  (SML "Term.Type/ (_, _)" and "Term.TFree/ (_, _)")
474f8ba9dfa9 improved evaluation mechanism
haftmann
parents: 25691
diff changeset
   159
474f8ba9dfa9 improved evaluation mechanism
haftmann
parents: 25691
diff changeset
   160
code_reserved SML Term
474f8ba9dfa9 improved evaluation mechanism
haftmann
parents: 25691
diff changeset
   161
474f8ba9dfa9 improved evaluation mechanism
haftmann
parents: 25691
diff changeset
   162
474f8ba9dfa9 improved evaluation mechanism
haftmann
parents: 25691
diff changeset
   163
474f8ba9dfa9 improved evaluation mechanism
haftmann
parents: 25691
diff changeset
   164
subsection {* Term representation *}
474f8ba9dfa9 improved evaluation mechanism
haftmann
parents: 25691
diff changeset
   165
474f8ba9dfa9 improved evaluation mechanism
haftmann
parents: 25691
diff changeset
   166
subsubsection {* Definition *}
474f8ba9dfa9 improved evaluation mechanism
haftmann
parents: 25691
diff changeset
   167
474f8ba9dfa9 improved evaluation mechanism
haftmann
parents: 25691
diff changeset
   168
datatype "term" =
474f8ba9dfa9 improved evaluation mechanism
haftmann
parents: 25691
diff changeset
   169
    Const message_string "typ" (infix "\<Colon>\<subseteq>" 112)
474f8ba9dfa9 improved evaluation mechanism
haftmann
parents: 25691
diff changeset
   170
  | Fix   vname "typ" (infix ":\<epsilon>" 112)
474f8ba9dfa9 improved evaluation mechanism
haftmann
parents: 25691
diff changeset
   171
  | App   "term" "term" (infixl "\<bullet>" 110)
474f8ba9dfa9 improved evaluation mechanism
haftmann
parents: 25691
diff changeset
   172
  | Abs   "vname \<times> typ" "term" (infixr "\<mapsto>" 111)
474f8ba9dfa9 improved evaluation mechanism
haftmann
parents: 25691
diff changeset
   173
  | Bnd   nat
474f8ba9dfa9 improved evaluation mechanism
haftmann
parents: 25691
diff changeset
   174
474f8ba9dfa9 improved evaluation mechanism
haftmann
parents: 25691
diff changeset
   175
code_datatype Const App Fix
474f8ba9dfa9 improved evaluation mechanism
haftmann
parents: 25691
diff changeset
   176
474f8ba9dfa9 improved evaluation mechanism
haftmann
parents: 25691
diff changeset
   177
abbreviation
474f8ba9dfa9 improved evaluation mechanism
haftmann
parents: 25691
diff changeset
   178
  Apps :: "term \<Rightarrow> term list \<Rightarrow> term" (infixl "{\<bullet>}" 110) where
474f8ba9dfa9 improved evaluation mechanism
haftmann
parents: 25691
diff changeset
   179
  "t {\<bullet>} ts \<equiv> foldl (op \<bullet>) t ts"
474f8ba9dfa9 improved evaluation mechanism
haftmann
parents: 25691
diff changeset
   180
abbreviation
474f8ba9dfa9 improved evaluation mechanism
haftmann
parents: 25691
diff changeset
   181
  Abss :: "(vname \<times> typ) list \<Rightarrow> term \<Rightarrow> term" (infixr "{\<mapsto>}" 111) where
474f8ba9dfa9 improved evaluation mechanism
haftmann
parents: 25691
diff changeset
   182
  "vs {\<mapsto>} t \<equiv> foldr (op \<mapsto>) vs t"
474f8ba9dfa9 improved evaluation mechanism
haftmann
parents: 25691
diff changeset
   183
474f8ba9dfa9 improved evaluation mechanism
haftmann
parents: 25691
diff changeset
   184
ML {*
474f8ba9dfa9 improved evaluation mechanism
haftmann
parents: 25691
diff changeset
   185
structure Eval_Aux =
474f8ba9dfa9 improved evaluation mechanism
haftmann
parents: 25691
diff changeset
   186
struct
474f8ba9dfa9 improved evaluation mechanism
haftmann
parents: 25691
diff changeset
   187
474f8ba9dfa9 improved evaluation mechanism
haftmann
parents: 25691
diff changeset
   188
open Eval_Aux;
474f8ba9dfa9 improved evaluation mechanism
haftmann
parents: 25691
diff changeset
   189
474f8ba9dfa9 improved evaluation mechanism
haftmann
parents: 25691
diff changeset
   190
fun mk_term f g (Const (c, ty)) =
474f8ba9dfa9 improved evaluation mechanism
haftmann
parents: 25691
diff changeset
   191
      @{term Const} $ Message_String.mk c $ g ty
474f8ba9dfa9 improved evaluation mechanism
haftmann
parents: 25691
diff changeset
   192
  | mk_term f g (t1 $ t2) =
474f8ba9dfa9 improved evaluation mechanism
haftmann
parents: 25691
diff changeset
   193
      @{term App} $ mk_term f g t1 $ mk_term f g t2
474f8ba9dfa9 improved evaluation mechanism
haftmann
parents: 25691
diff changeset
   194
  | mk_term f g (Free v) = f v;
474f8ba9dfa9 improved evaluation mechanism
haftmann
parents: 25691
diff changeset
   195
474f8ba9dfa9 improved evaluation mechanism
haftmann
parents: 25691
diff changeset
   196
end;
474f8ba9dfa9 improved evaluation mechanism
haftmann
parents: 25691
diff changeset
   197
*}
474f8ba9dfa9 improved evaluation mechanism
haftmann
parents: 25691
diff changeset
   198
474f8ba9dfa9 improved evaluation mechanism
haftmann
parents: 25691
diff changeset
   199
474f8ba9dfa9 improved evaluation mechanism
haftmann
parents: 25691
diff changeset
   200
subsubsection {* Class @{text term_of} *}
22525
d929a900584c cleaned up Library/ and ex/
haftmann
parents:
diff changeset
   201
d929a900584c cleaned up Library/ and ex/
haftmann
parents:
diff changeset
   202
class term_of = typ_of +
23062
d88d2087436d evaluation for integers
haftmann
parents: 23020
diff changeset
   203
  constrains typ_of :: "'a\<Colon>{} itself \<Rightarrow> typ"
22525
d929a900584c cleaned up Library/ and ex/
haftmann
parents:
diff changeset
   204
  fixes term_of :: "'a \<Rightarrow> term"
d929a900584c cleaned up Library/ and ex/
haftmann
parents:
diff changeset
   205
d929a900584c cleaned up Library/ and ex/
haftmann
parents:
diff changeset
   206
ML {*
25763
474f8ba9dfa9 improved evaluation mechanism
haftmann
parents: 25691
diff changeset
   207
structure Eval_Aux =
22525
d929a900584c cleaned up Library/ and ex/
haftmann
parents:
diff changeset
   208
struct
d929a900584c cleaned up Library/ and ex/
haftmann
parents:
diff changeset
   209
25763
474f8ba9dfa9 improved evaluation mechanism
haftmann
parents: 25691
diff changeset
   210
open Eval_Aux;
474f8ba9dfa9 improved evaluation mechanism
haftmann
parents: 25691
diff changeset
   211
22525
d929a900584c cleaned up Library/ and ex/
haftmann
parents:
diff changeset
   212
local
d929a900584c cleaned up Library/ and ex/
haftmann
parents:
diff changeset
   213
  fun term_term_of ty =
d929a900584c cleaned up Library/ and ex/
haftmann
parents:
diff changeset
   214
    Const (@{const_name term_of}, ty --> @{typ term});
d929a900584c cleaned up Library/ and ex/
haftmann
parents:
diff changeset
   215
in
d929a900584c cleaned up Library/ and ex/
haftmann
parents:
diff changeset
   216
  val class_term_of = Sign.intern_class @{theory} "term_of";
d929a900584c cleaned up Library/ and ex/
haftmann
parents:
diff changeset
   217
  fun mk_terms_of_defs vs (tyco, cs) =
d929a900584c cleaned up Library/ and ex/
haftmann
parents:
diff changeset
   218
    let
d929a900584c cleaned up Library/ and ex/
haftmann
parents:
diff changeset
   219
      val dty = Type (tyco, map TFree vs);
d929a900584c cleaned up Library/ and ex/
haftmann
parents:
diff changeset
   220
      fun mk_eq c =
d929a900584c cleaned up Library/ and ex/
haftmann
parents:
diff changeset
   221
        let
d929a900584c cleaned up Library/ and ex/
haftmann
parents:
diff changeset
   222
          val lhs : term = term_term_of dty $ c;
25763
474f8ba9dfa9 improved evaluation mechanism
haftmann
parents: 25691
diff changeset
   223
          val rhs : term = mk_term
22525
d929a900584c cleaned up Library/ and ex/
haftmann
parents:
diff changeset
   224
            (fn (v, ty) => term_term_of ty $ Free (v, ty))
25763
474f8ba9dfa9 improved evaluation mechanism
haftmann
parents: 25691
diff changeset
   225
            (mk_typ (fn (v, sort) => mk_typ_of (TFree (v, sort)))) c
22525
d929a900584c cleaned up Library/ and ex/
haftmann
parents:
diff changeset
   226
        in
25559
f14305fb698c authentic primrec
haftmann
parents: 25557
diff changeset
   227
          HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs))
22525
d929a900584c cleaned up Library/ and ex/
haftmann
parents:
diff changeset
   228
        end;
d929a900584c cleaned up Library/ and ex/
haftmann
parents:
diff changeset
   229
    in map mk_eq cs end;
d929a900584c cleaned up Library/ and ex/
haftmann
parents:
diff changeset
   230
  fun mk_term_of t =
d929a900584c cleaned up Library/ and ex/
haftmann
parents:
diff changeset
   231
    term_term_of (Term.fastype_of t) $ t;
d929a900584c cleaned up Library/ and ex/
haftmann
parents:
diff changeset
   232
end;
d929a900584c cleaned up Library/ and ex/
haftmann
parents:
diff changeset
   233
d929a900584c cleaned up Library/ and ex/
haftmann
parents:
diff changeset
   234
end;
d929a900584c cleaned up Library/ and ex/
haftmann
parents:
diff changeset
   235
*}
d929a900584c cleaned up Library/ and ex/
haftmann
parents:
diff changeset
   236
d929a900584c cleaned up Library/ and ex/
haftmann
parents:
diff changeset
   237
setup {*
d929a900584c cleaned up Library/ and ex/
haftmann
parents:
diff changeset
   238
let
25763
474f8ba9dfa9 improved evaluation mechanism
haftmann
parents: 25691
diff changeset
   239
  open Eval_Aux;
22525
d929a900584c cleaned up Library/ and ex/
haftmann
parents:
diff changeset
   240
  fun thy_note ((name, atts), thms) =
d929a900584c cleaned up Library/ and ex/
haftmann
parents:
diff changeset
   241
    PureThy.add_thmss [((name, thms), atts)] #-> (fn [thms] => pair (name, thms));
d929a900584c cleaned up Library/ and ex/
haftmann
parents:
diff changeset
   242
  fun thy_def ((name, atts), t) =
d929a900584c cleaned up Library/ and ex/
haftmann
parents:
diff changeset
   243
    PureThy.add_defs_i false [((name, t), atts)] #-> (fn [thm] => pair (name, thm));
25536
01753a944433 improved
haftmann
parents: 25502
diff changeset
   244
  fun prep_dtyp thy vs tyco =
01753a944433 improved
haftmann
parents: 25502
diff changeset
   245
    let
01753a944433 improved
haftmann
parents: 25502
diff changeset
   246
      val (_, cs) = DatatypePackage.the_datatype_spec thy tyco;
01753a944433 improved
haftmann
parents: 25502
diff changeset
   247
      val prep_typ = map_atyps (fn TFree (v, sort) =>
01753a944433 improved
haftmann
parents: 25502
diff changeset
   248
        TFree (v, (the o AList.lookup (op =) vs) v));
01753a944433 improved
haftmann
parents: 25502
diff changeset
   249
      fun prep_c (c, tys) = list_comb (Const (c, tys ---> Type (tyco, map TFree vs)),
01753a944433 improved
haftmann
parents: 25502
diff changeset
   250
        map Free (Name.names Name.context "a" tys));
01753a944433 improved
haftmann
parents: 25502
diff changeset
   251
    in (tyco, map (prep_c o (apsnd o map) prep_typ) cs) end;
01753a944433 improved
haftmann
parents: 25502
diff changeset
   252
  fun prep thy tycos =
22525
d929a900584c cleaned up Library/ and ex/
haftmann
parents:
diff changeset
   253
    let
25536
01753a944433 improved
haftmann
parents: 25502
diff changeset
   254
      val inter_sort = curry (Sorts.inter_sort (Sign.classes_of thy)) @{sort term_of};
01753a944433 improved
haftmann
parents: 25502
diff changeset
   255
      val tyco = hd tycos;
01753a944433 improved
haftmann
parents: 25502
diff changeset
   256
      val (vs_proto, _) = DatatypePackage.the_datatype_spec thy tyco;
01753a944433 improved
haftmann
parents: 25502
diff changeset
   257
      val all_typs = maps (maps snd o snd o DatatypePackage.the_datatype_spec thy) tycos;
01753a944433 improved
haftmann
parents: 25502
diff changeset
   258
      fun add_tycos (Type (tyco, tys)) = insert (op =) tyco #>
01753a944433 improved
haftmann
parents: 25502
diff changeset
   259
            fold add_tycos tys
01753a944433 improved
haftmann
parents: 25502
diff changeset
   260
        | add_tycos _ = I;
01753a944433 improved
haftmann
parents: 25502
diff changeset
   261
      val dep_tycos = [] |> fold add_tycos all_typs |> subtract (op =) tycos;
01753a944433 improved
haftmann
parents: 25502
diff changeset
   262
      val sorts = map (inter_sort o snd) vs_proto;
01753a944433 improved
haftmann
parents: 25502
diff changeset
   263
      val vs = map fst vs_proto ~~ sorts;
01753a944433 improved
haftmann
parents: 25502
diff changeset
   264
      val css = map (prep_dtyp thy vs) tycos;
25763
474f8ba9dfa9 improved evaluation mechanism
haftmann
parents: 25691
diff changeset
   265
      val defs = map (mk_terms_of_defs vs) css;
25536
01753a944433 improved
haftmann
parents: 25502
diff changeset
   266
    in if forall (fn tyco => can (Sign.arity_sorts thy tyco) @{sort term_of}) dep_tycos
01753a944433 improved
haftmann
parents: 25502
diff changeset
   267
        andalso not (tycos = [@{type_name typ}])
25559
f14305fb698c authentic primrec
haftmann
parents: 25557
diff changeset
   268
      then SOME (sorts, defs)
25536
01753a944433 improved
haftmann
parents: 25502
diff changeset
   269
      else NONE
22525
d929a900584c cleaned up Library/ and ex/
haftmann
parents:
diff changeset
   270
    end;
25559
f14305fb698c authentic primrec
haftmann
parents: 25557
diff changeset
   271
  fun prep' ctxt proto_eqs =
f14305fb698c authentic primrec
haftmann
parents: 25557
diff changeset
   272
    let
25603
4b7a58fc168c dropped Class.prep_spec
haftmann
parents: 25594
diff changeset
   273
      val eqs as eq :: _ = map (Syntax.check_term ctxt) proto_eqs;
25559
f14305fb698c authentic primrec
haftmann
parents: 25557
diff changeset
   274
      val (Free (v, ty), _) =
f14305fb698c authentic primrec
haftmann
parents: 25557
diff changeset
   275
        (strip_comb o fst o HOLogic.dest_eq o HOLogic.dest_Trueprop) eq;
f14305fb698c authentic primrec
haftmann
parents: 25557
diff changeset
   276
    in ((v, SOME ty, NoSyn), map (pair ("", [])) eqs) end;
f14305fb698c authentic primrec
haftmann
parents: 25557
diff changeset
   277
  fun primrec primrecs ctxt =
f14305fb698c authentic primrec
haftmann
parents: 25557
diff changeset
   278
    let
f14305fb698c authentic primrec
haftmann
parents: 25557
diff changeset
   279
      val (fixes, eqnss) = split_list (map (prep' ctxt) primrecs);
f14305fb698c authentic primrec
haftmann
parents: 25557
diff changeset
   280
    in PrimrecPackage.add_primrec fixes (flat eqnss) ctxt end;
25536
01753a944433 improved
haftmann
parents: 25502
diff changeset
   281
  fun interpretator tycos thy = case prep thy tycos
01753a944433 improved
haftmann
parents: 25502
diff changeset
   282
   of SOME (sorts, defs) =>
01753a944433 improved
haftmann
parents: 25502
diff changeset
   283
      thy
25569
c597835d5de4 dropped Instance.instantiate
haftmann
parents: 25559
diff changeset
   284
      |> TheoryTarget.instantiation (tycos, sorts, @{sort term_of})
c597835d5de4 dropped Instance.instantiate
haftmann
parents: 25559
diff changeset
   285
      |> primrec defs
c597835d5de4 dropped Instance.instantiate
haftmann
parents: 25559
diff changeset
   286
      |> snd
c597835d5de4 dropped Instance.instantiate
haftmann
parents: 25559
diff changeset
   287
      |> Class.prove_instantiation_instance (K (Class.intro_classes_tac []))
c597835d5de4 dropped Instance.instantiate
haftmann
parents: 25559
diff changeset
   288
      |> LocalTheory.exit
c597835d5de4 dropped Instance.instantiate
haftmann
parents: 25559
diff changeset
   289
      |> ProofContext.theory_of
25536
01753a944433 improved
haftmann
parents: 25502
diff changeset
   290
    | NONE => thy;
01753a944433 improved
haftmann
parents: 25502
diff changeset
   291
  in DatatypePackage.interpretation interpretator end
22525
d929a900584c cleaned up Library/ and ex/
haftmann
parents:
diff changeset
   292
*}
d929a900584c cleaned up Library/ and ex/
haftmann
parents:
diff changeset
   293
25666
f46ed5b333fd improved term syntax
haftmann
parents: 25603
diff changeset
   294
abbreviation (in pure_term_syntax) (input)
23062
d88d2087436d evaluation for integers
haftmann
parents: 23020
diff changeset
   295
  intT :: "typ"
d88d2087436d evaluation for integers
haftmann
parents: 23020
diff changeset
   296
where
25666
f46ed5b333fd improved term syntax
haftmann
parents: 25603
diff changeset
   297
  "intT \<equiv> Type (STR ''IntDef.int'') []"
23062
d88d2087436d evaluation for integers
haftmann
parents: 23020
diff changeset
   298
25666
f46ed5b333fd improved term syntax
haftmann
parents: 25603
diff changeset
   299
abbreviation (in pure_term_syntax) (input)
23133
5a6935d598c3 fixed typo
haftmann
parents: 23062
diff changeset
   300
  bitT :: "typ"
5a6935d598c3 fixed typo
haftmann
parents: 23062
diff changeset
   301
where
25666
f46ed5b333fd improved term syntax
haftmann
parents: 25603
diff changeset
   302
  "bitT \<equiv> Type (STR ''Numeral.bit'') []"
23133
5a6935d598c3 fixed typo
haftmann
parents: 23062
diff changeset
   303
25666
f46ed5b333fd improved term syntax
haftmann
parents: 25603
diff changeset
   304
function (in pure_term_syntax)
23062
d88d2087436d evaluation for integers
haftmann
parents: 23020
diff changeset
   305
  mk_int :: "int \<Rightarrow> term"
d88d2087436d evaluation for integers
haftmann
parents: 23020
diff changeset
   306
where
d88d2087436d evaluation for integers
haftmann
parents: 23020
diff changeset
   307
  "mk_int k = (if k = 0 then STR ''Numeral.Pls'' \<Colon>\<subseteq> intT
d88d2087436d evaluation for integers
haftmann
parents: 23020
diff changeset
   308
    else if k = -1 then STR ''Numeral.Min'' \<Colon>\<subseteq> intT
d88d2087436d evaluation for integers
haftmann
parents: 23020
diff changeset
   309
    else let (l, m) = divAlg (k, 2)
23133
5a6935d598c3 fixed typo
haftmann
parents: 23062
diff changeset
   310
  in STR ''Numeral.Bit'' \<Colon>\<subseteq> intT \<rightarrow> bitT \<rightarrow> intT \<bullet> mk_int l \<bullet>
5a6935d598c3 fixed typo
haftmann
parents: 23062
diff changeset
   311
    (if m = 0 then STR ''Numeral.bit.B0'' \<Colon>\<subseteq> bitT else STR ''Numeral.bit.B1'' \<Colon>\<subseteq> bitT))"
23062
d88d2087436d evaluation for integers
haftmann
parents: 23020
diff changeset
   312
by pat_completeness auto
25666
f46ed5b333fd improved term syntax
haftmann
parents: 25603
diff changeset
   313
termination (in pure_term_syntax)
f46ed5b333fd improved term syntax
haftmann
parents: 25603
diff changeset
   314
by (relation "measure (nat o abs)") (auto simp add: divAlg_mod_div)
f46ed5b333fd improved term syntax
haftmann
parents: 25603
diff changeset
   315
f46ed5b333fd improved term syntax
haftmann
parents: 25603
diff changeset
   316
declare pure_term_syntax.mk_int.simps [code func]
f46ed5b333fd improved term syntax
haftmann
parents: 25603
diff changeset
   317
f46ed5b333fd improved term syntax
haftmann
parents: 25603
diff changeset
   318
definition (in pure_term_syntax)
f46ed5b333fd improved term syntax
haftmann
parents: 25603
diff changeset
   319
  "term_of_int_aux k = STR ''Numeral.number_class.number_of'' \<Colon>\<subseteq> intT \<rightarrow> intT \<bullet> mk_int k"
f46ed5b333fd improved term syntax
haftmann
parents: 25603
diff changeset
   320
f46ed5b333fd improved term syntax
haftmann
parents: 25603
diff changeset
   321
declare pure_term_syntax.term_of_int_aux_def [code func]
23062
d88d2087436d evaluation for integers
haftmann
parents: 23020
diff changeset
   322
25569
c597835d5de4 dropped Instance.instantiate
haftmann
parents: 25559
diff changeset
   323
instantiation int :: term_of
c597835d5de4 dropped Instance.instantiate
haftmann
parents: 25559
diff changeset
   324
begin
c597835d5de4 dropped Instance.instantiate
haftmann
parents: 25559
diff changeset
   325
c597835d5de4 dropped Instance.instantiate
haftmann
parents: 25559
diff changeset
   326
definition
25666
f46ed5b333fd improved term syntax
haftmann
parents: 25603
diff changeset
   327
  "term_of = pure_term_syntax.term_of_int_aux"
25569
c597835d5de4 dropped Instance.instantiate
haftmann
parents: 25559
diff changeset
   328
c597835d5de4 dropped Instance.instantiate
haftmann
parents: 25559
diff changeset
   329
instance ..
c597835d5de4 dropped Instance.instantiate
haftmann
parents: 25559
diff changeset
   330
c597835d5de4 dropped Instance.instantiate
haftmann
parents: 25559
diff changeset
   331
end
23062
d88d2087436d evaluation for integers
haftmann
parents: 23020
diff changeset
   332
d88d2087436d evaluation for integers
haftmann
parents: 23020
diff changeset
   333
25763
474f8ba9dfa9 improved evaluation mechanism
haftmann
parents: 25691
diff changeset
   334
subsubsection {* Code generator setup *}
474f8ba9dfa9 improved evaluation mechanism
haftmann
parents: 25691
diff changeset
   335
474f8ba9dfa9 improved evaluation mechanism
haftmann
parents: 25691
diff changeset
   336
lemmas [code func del] = term.recs term.cases term.size
474f8ba9dfa9 improved evaluation mechanism
haftmann
parents: 25691
diff changeset
   337
lemmas [code func del] = term_of_message_string.simps
474f8ba9dfa9 improved evaluation mechanism
haftmann
parents: 25691
diff changeset
   338
lemma [code func, code func del]: "(t1\<Colon>term) = t2 \<longleftrightarrow> t1 = t2" ..
22525
d929a900584c cleaned up Library/ and ex/
haftmann
parents:
diff changeset
   339
25763
474f8ba9dfa9 improved evaluation mechanism
haftmann
parents: 25691
diff changeset
   340
code_type "term"
474f8ba9dfa9 improved evaluation mechanism
haftmann
parents: 25691
diff changeset
   341
  (SML "Term.term")
474f8ba9dfa9 improved evaluation mechanism
haftmann
parents: 25691
diff changeset
   342
474f8ba9dfa9 improved evaluation mechanism
haftmann
parents: 25691
diff changeset
   343
code_const Const and App and Fix
474f8ba9dfa9 improved evaluation mechanism
haftmann
parents: 25691
diff changeset
   344
  (SML "Term.Const/ (_, _)" and "Term.$/ (_, _)" and "Term.Free/ (_, _)")
22525
d929a900584c cleaned up Library/ and ex/
haftmann
parents:
diff changeset
   345
d929a900584c cleaned up Library/ and ex/
haftmann
parents:
diff changeset
   346
25763
474f8ba9dfa9 improved evaluation mechanism
haftmann
parents: 25691
diff changeset
   347
subsection {* Evaluation setup *}
22525
d929a900584c cleaned up Library/ and ex/
haftmann
parents:
diff changeset
   348
d929a900584c cleaned up Library/ and ex/
haftmann
parents:
diff changeset
   349
ML {*
d929a900584c cleaned up Library/ and ex/
haftmann
parents:
diff changeset
   350
signature EVAL =
d929a900584c cleaned up Library/ and ex/
haftmann
parents:
diff changeset
   351
sig
24587
4f2cbf6e563f multi-functional value keyword
haftmann
parents: 24508
diff changeset
   352
  val eval_ref: (unit -> term) option ref
24835
8c26128f8997 clarified relationship of code generator conversions and evaluations
haftmann
parents: 24659
diff changeset
   353
  val eval_term: theory -> term -> term
8c26128f8997 clarified relationship of code generator conversions and evaluations
haftmann
parents: 24659
diff changeset
   354
  val evaluate: Proof.context -> term -> unit
8c26128f8997 clarified relationship of code generator conversions and evaluations
haftmann
parents: 24659
diff changeset
   355
  val evaluate': string -> Proof.context -> term -> unit
8c26128f8997 clarified relationship of code generator conversions and evaluations
haftmann
parents: 24659
diff changeset
   356
  val evaluate_cmd: string option -> Toplevel.state -> unit
22525
d929a900584c cleaned up Library/ and ex/
haftmann
parents:
diff changeset
   357
end;
d929a900584c cleaned up Library/ and ex/
haftmann
parents:
diff changeset
   358
24280
c9867bdf2424 updated code generator setup
haftmann
parents: 24219
diff changeset
   359
structure Eval =
22525
d929a900584c cleaned up Library/ and ex/
haftmann
parents:
diff changeset
   360
struct
d929a900584c cleaned up Library/ and ex/
haftmann
parents:
diff changeset
   361
24587
4f2cbf6e563f multi-functional value keyword
haftmann
parents: 24508
diff changeset
   362
val eval_ref = ref (NONE : (unit -> term) option);
22525
d929a900584c cleaned up Library/ and ex/
haftmann
parents:
diff changeset
   363
24835
8c26128f8997 clarified relationship of code generator conversions and evaluations
haftmann
parents: 24659
diff changeset
   364
fun eval_invoke thy code ((_, ty), t) deps _ =
24916
dc56dd1b3cda simplified evaluation
haftmann
parents: 24867
diff changeset
   365
  CodeTarget.eval_invoke thy ("Eval.eval_ref", eval_ref) code (t, ty) [];
24280
c9867bdf2424 updated code generator setup
haftmann
parents: 24219
diff changeset
   366
24835
8c26128f8997 clarified relationship of code generator conversions and evaluations
haftmann
parents: 24659
diff changeset
   367
fun eval_term thy =
25763
474f8ba9dfa9 improved evaluation mechanism
haftmann
parents: 25691
diff changeset
   368
  Eval_Aux.mk_term_of
24835
8c26128f8997 clarified relationship of code generator conversions and evaluations
haftmann
parents: 24659
diff changeset
   369
  #> CodePackage.eval_term thy (eval_invoke thy)
8c26128f8997 clarified relationship of code generator conversions and evaluations
haftmann
parents: 24659
diff changeset
   370
  #> Code.postprocess_term thy;
24280
c9867bdf2424 updated code generator setup
haftmann
parents: 24219
diff changeset
   371
24835
8c26128f8997 clarified relationship of code generator conversions and evaluations
haftmann
parents: 24659
diff changeset
   372
val evaluators = [
8c26128f8997 clarified relationship of code generator conversions and evaluations
haftmann
parents: 24659
diff changeset
   373
  ("code", eval_term),
8c26128f8997 clarified relationship of code generator conversions and evaluations
haftmann
parents: 24659
diff changeset
   374
  ("SML", Codegen.eval_term),
8c26128f8997 clarified relationship of code generator conversions and evaluations
haftmann
parents: 24659
diff changeset
   375
  ("normal_form", Nbe.norm_term)
8c26128f8997 clarified relationship of code generator conversions and evaluations
haftmann
parents: 24659
diff changeset
   376
];
22525
d929a900584c cleaned up Library/ and ex/
haftmann
parents:
diff changeset
   377
24835
8c26128f8997 clarified relationship of code generator conversions and evaluations
haftmann
parents: 24659
diff changeset
   378
fun gen_evaluate evaluators ctxt t =
24280
c9867bdf2424 updated code generator setup
haftmann
parents: 24219
diff changeset
   379
  let
c9867bdf2424 updated code generator setup
haftmann
parents: 24219
diff changeset
   380
    val thy = ProofContext.theory_of ctxt;
24835
8c26128f8997 clarified relationship of code generator conversions and evaluations
haftmann
parents: 24659
diff changeset
   381
    val (evls, evl) = split_last evaluators;
8c26128f8997 clarified relationship of code generator conversions and evaluations
haftmann
parents: 24659
diff changeset
   382
    val t' = case get_first (fn f => try (f thy) t) evls
8c26128f8997 clarified relationship of code generator conversions and evaluations
haftmann
parents: 24659
diff changeset
   383
     of SOME t' => t'
8c26128f8997 clarified relationship of code generator conversions and evaluations
haftmann
parents: 24659
diff changeset
   384
      | NONE => evl thy t;
8c26128f8997 clarified relationship of code generator conversions and evaluations
haftmann
parents: 24659
diff changeset
   385
    val ty' = Term.type_of t';
24920
2a45e400fdad generic Syntax.pretty/string_of operations;
wenzelm
parents: 24916
diff changeset
   386
    val p = Pretty.block [Pretty.quote (Syntax.pretty_term ctxt t'),
24835
8c26128f8997 clarified relationship of code generator conversions and evaluations
haftmann
parents: 24659
diff changeset
   387
      Pretty.fbrk, Pretty.str "::", Pretty.brk 1,
24920
2a45e400fdad generic Syntax.pretty/string_of operations;
wenzelm
parents: 24916
diff changeset
   388
      Pretty.quote (Syntax.pretty_typ ctxt ty')];
24280
c9867bdf2424 updated code generator setup
haftmann
parents: 24219
diff changeset
   389
  in Pretty.writeln p end;
c9867bdf2424 updated code generator setup
haftmann
parents: 24219
diff changeset
   390
24835
8c26128f8997 clarified relationship of code generator conversions and evaluations
haftmann
parents: 24659
diff changeset
   391
val evaluate = gen_evaluate (map snd evaluators);
8c26128f8997 clarified relationship of code generator conversions and evaluations
haftmann
parents: 24659
diff changeset
   392
8c26128f8997 clarified relationship of code generator conversions and evaluations
haftmann
parents: 24659
diff changeset
   393
fun evaluate' name = gen_evaluate
8c26128f8997 clarified relationship of code generator conversions and evaluations
haftmann
parents: 24659
diff changeset
   394
  [(the o AList.lookup (op =) evaluators) name];
8c26128f8997 clarified relationship of code generator conversions and evaluations
haftmann
parents: 24659
diff changeset
   395
8c26128f8997 clarified relationship of code generator conversions and evaluations
haftmann
parents: 24659
diff changeset
   396
fun evaluate_cmd some_name raw_t state =
22525
d929a900584c cleaned up Library/ and ex/
haftmann
parents:
diff changeset
   397
  let
22804
haftmann
parents: 22665
diff changeset
   398
    val ctxt = Toplevel.context_of state;
24508
c8b82fec6447 replaced ProofContext.read_term/prop by general Syntax.read_term/prop;
wenzelm
parents: 24423
diff changeset
   399
    val t = Syntax.read_term ctxt raw_t;
24835
8c26128f8997 clarified relationship of code generator conversions and evaluations
haftmann
parents: 24659
diff changeset
   400
  in case some_name
8c26128f8997 clarified relationship of code generator conversions and evaluations
haftmann
parents: 24659
diff changeset
   401
   of NONE => evaluate ctxt t
8c26128f8997 clarified relationship of code generator conversions and evaluations
haftmann
parents: 24659
diff changeset
   402
    | SOME name => evaluate' name ctxt t
8c26128f8997 clarified relationship of code generator conversions and evaluations
haftmann
parents: 24659
diff changeset
   403
  end;
22525
d929a900584c cleaned up Library/ and ex/
haftmann
parents:
diff changeset
   404
d929a900584c cleaned up Library/ and ex/
haftmann
parents:
diff changeset
   405
end;
d929a900584c cleaned up Library/ and ex/
haftmann
parents:
diff changeset
   406
*}
d929a900584c cleaned up Library/ and ex/
haftmann
parents:
diff changeset
   407
22804
haftmann
parents: 22665
diff changeset
   408
ML {*
haftmann
parents: 22665
diff changeset
   409
  OuterSyntax.improper_command "value" "read, evaluate and print term" OuterKeyword.diag
24835
8c26128f8997 clarified relationship of code generator conversions and evaluations
haftmann
parents: 24659
diff changeset
   410
    (Scan.option (OuterParse.$$$ "(" |-- OuterParse.name --| OuterParse.$$$ ")")
8c26128f8997 clarified relationship of code generator conversions and evaluations
haftmann
parents: 24659
diff changeset
   411
    -- OuterParse.term
8c26128f8997 clarified relationship of code generator conversions and evaluations
haftmann
parents: 24659
diff changeset
   412
      >> (fn (some_name, t) => Toplevel.no_timing o Toplevel.keep
8c26128f8997 clarified relationship of code generator conversions and evaluations
haftmann
parents: 24659
diff changeset
   413
           (Eval.evaluate_cmd some_name t)));
22804
haftmann
parents: 22665
diff changeset
   414
*}
haftmann
parents: 22665
diff changeset
   415
22665
cf152ff55d16 tuned document (headers, sections, spacing);
wenzelm
parents: 22527
diff changeset
   416
end