multi-functional value keyword
authorhaftmann
Sat Sep 15 19:27:42 2007 +0200 (2007-09-15)
changeset 245874f2cbf6e563f
parent 24586 c87238132dc3
child 24588 ed9a1254d674
multi-functional value keyword
src/HOL/Library/Eval.thy
src/HOL/ex/Eval_Examples.thy
     1.1 --- a/src/HOL/Library/Eval.thy	Sat Sep 15 19:27:41 2007 +0200
     1.2 +++ b/src/HOL/Library/Eval.thy	Sat Sep 15 19:27:42 2007 +0200
     1.3 @@ -34,11 +34,14 @@
     1.4  end;
     1.5  *}
     1.6  
     1.7 +instance "prop" :: typ_of
     1.8 +  "typ_of T \<equiv> STR ''prop'' {\<struct>} []" ..
     1.9 +
    1.10  instance itself :: (typ_of) typ_of
    1.11    "typ_of T \<equiv> STR ''itself'' {\<struct>} [typ_of TYPE('a\<Colon>typ_of)]" ..
    1.12  
    1.13 -instance "prop" :: typ_of
    1.14 -  "typ_of T \<equiv> STR ''prop'' {\<struct>} []" ..
    1.15 +instance set :: (typ_of) typ_of
    1.16 +  "typ_of T \<equiv> STR ''set'' {\<struct>} [typ_of TYPE('a\<Colon>typ_of)]" ..
    1.17  
    1.18  instance int :: typ_of
    1.19    "typ_of T \<equiv> STR ''IntDef.int'' {\<struct>} []" ..
    1.20 @@ -153,7 +156,7 @@
    1.21  ML {*
    1.22  signature EVAL =
    1.23  sig
    1.24 -  val eval_ref: term option ref
    1.25 +  val eval_ref: (unit -> term) option ref
    1.26    val eval_conv: cterm -> thm
    1.27    val eval_print: (cterm -> thm) -> Proof.context -> term -> unit
    1.28    val eval_print_cmd: (cterm -> thm) -> string -> Toplevel.state -> unit
    1.29 @@ -162,7 +165,7 @@
    1.30  structure Eval =
    1.31  struct
    1.32  
    1.33 -val eval_ref = ref (NONE : term option);
    1.34 +val eval_ref = ref (NONE : (unit -> term) option);
    1.35  
    1.36  end;
    1.37  *}
    1.38 @@ -223,9 +226,11 @@
    1.39  ML {*
    1.40  val valueP =
    1.41    OuterSyntax.improper_command "value" "read, evaluate and print term" OuterKeyword.diag
    1.42 -    ((OuterParse.opt_keyword "overloaded" -- OuterParse.term)
    1.43 -      >> (fn (b, t) => Toplevel.no_timing o Toplevel.keep
    1.44 -           (Eval.eval_print_cmd (if b then Eval.eval_conv else Codegen.evaluation_conv) t)));
    1.45 +    (OuterParse.term
    1.46 +      >> (fn t => Toplevel.no_timing o Toplevel.keep
    1.47 +           (Eval.eval_print_cmd (fn ct => case try Eval.eval_conv ct
    1.48 +     of SOME thm => thm
    1.49 +      | NONE => Codegen.evaluation_conv ct) t)));
    1.50  
    1.51  val _ = OuterSyntax.add_parsers [valueP];
    1.52  *}
     2.1 --- a/src/HOL/ex/Eval_Examples.thy	Sat Sep 15 19:27:41 2007 +0200
     2.2 +++ b/src/HOL/ex/Eval_Examples.thy	Sat Sep 15 19:27:42 2007 +0200
     2.3 @@ -26,13 +26,14 @@
     2.4  
     2.5  text {* term evaluation *}
     2.6  
     2.7 -value (overloaded) "(Suc 2 + 1) * 4"
     2.8 -value (overloaded) "(Suc 2 + 1) * 4"
     2.9 -value (overloaded) "(Suc 2 + Suc 0) * Suc 3"
    2.10 -value (overloaded) "nat 100"
    2.11 -value (overloaded) "(10\<Colon>int) \<le> 12"
    2.12 -value (overloaded) "[]::nat list"
    2.13 -value (overloaded) "[(nat 100, ())]"
    2.14 +value "(Suc 2 + 1) * 4"
    2.15 +value "(Suc 2 + 1) * 4"
    2.16 +value "(Suc 2 + Suc 0) * Suc 3"
    2.17 +value "nat 100"
    2.18 +value "(10\<Colon>int) \<le> 12"
    2.19 +value "[]::nat list"
    2.20 +value "[(nat 100, ())]"
    2.21 +value "max (2::int) 4"
    2.22  
    2.23  text {* a fancy datatype *}
    2.24  
    2.25 @@ -43,6 +44,6 @@
    2.26  and ('a, 'b) cair =
    2.27      Cair 'a 'b
    2.28  
    2.29 -value (overloaded) "Shift (Cair (4::nat) [Suc 0])"
    2.30 +value "Shift (Cair (4::nat) [Suc 0])"
    2.31  
    2.32  end