--- a/src/HOL/Code_Setup.thy Thu Oct 04 16:59:30 2007 +0200
+++ b/src/HOL/Code_Setup.thy Thu Oct 04 19:41:49 2007 +0200
@@ -136,7 +136,7 @@
subsection {* Evaluation oracle *}
oracle eval_oracle ("term") = {* fn thy => fn t =>
- if CodePackage.satisfies thy (Thm.cterm_of thy (HOLogic.dest_Trueprop t)) []
+ if CodePackage.satisfies thy (HOLogic.dest_Trueprop t) []
then t
else HOLogic.Trueprop $ HOLogic.true_const (*dummy*)
*}
@@ -156,7 +156,7 @@
method_setup normalization = {*
Method.no_args (Method.SIMPLE_METHOD'
- (CONVERSION (ObjectLogic.judgment_conv Nbe.normalization_conv)
+ (CONVERSION (ObjectLogic.judgment_conv Nbe.norm_conv)
THEN' resolve_tac [TrueI, refl]))
*} "solve goal by normalization"
--- a/src/HOL/Library/Eval.thy Thu Oct 04 16:59:30 2007 +0200
+++ b/src/HOL/Library/Eval.thy Thu Oct 04 19:41:49 2007 +0200
@@ -157,9 +157,10 @@
signature EVAL =
sig
val eval_ref: (unit -> term) option ref
- val eval_conv: cterm -> thm
- val eval_print: (cterm -> thm) -> Proof.context -> term -> unit
- val eval_print_cmd: (cterm -> thm) -> string -> Toplevel.state -> unit
+ val eval_term: theory -> term -> term
+ val evaluate: Proof.context -> term -> unit
+ val evaluate': string -> Proof.context -> term -> unit
+ val evaluate_cmd: string option -> Toplevel.state -> unit
end;
structure Eval =
@@ -167,61 +168,46 @@
val eval_ref = ref (NONE : (unit -> term) option);
-end;
-*}
+fun eval_invoke thy code ((_, ty), t) deps _ =
+ CodePackage.eval_invoke thy ("Eval.eval_ref", eval_ref) code (t, ty) [];
-oracle eval_oracle ("term * CodeThingol.code * (CodeThingol.typscheme * CodeThingol.iterm) * cterm") =
-{* fn thy => fn (t0, code, ((vs, ty), t), ct) =>
-let
- val _ = (Term.map_types o Term.map_atyps) (fn _ =>
- error ("Term " ^ Sign.string_of_term thy t0 ^ " contains polymorphic type"))
- t0;
-in
- Logic.mk_equals (t0,
- CodePackage.eval_invoke thy ("Eval.eval_ref", Eval.eval_ref) code (t, ty) [])
-end;
-*}
+fun eval_term thy =
+ TermOf.mk_term_of
+ #> CodePackage.eval_term thy (eval_invoke thy)
+ #> Code.postprocess_term thy;
-ML {*
-structure Eval : EVAL =
-struct
-
-open Eval;
-
-fun eval_invoke thy t0 code vs_ty_t _ ct = eval_oracle thy (t0, code, vs_ty_t, ct);
+val evaluators = [
+ ("code", eval_term),
+ ("SML", Codegen.eval_term),
+ ("normal_form", Nbe.norm_term)
+];
-fun eval_conv ct =
- let
- val thy = Thm.theory_of_cterm ct;
- val ct' = (Thm.cterm_of thy o TermOf.mk_term_of o Thm.term_of) ct;
- in
- CodePackage.eval_term thy
- (eval_invoke thy (Thm.term_of ct)) ct'
- end;
-
-fun eval_print conv ctxt t =
+fun gen_evaluate evaluators ctxt t =
let
val thy = ProofContext.theory_of ctxt;
- val ct = Thm.cterm_of thy t;
- val (_, t') = (Logic.dest_equals o Thm.prop_of o conv) ct;
- val ty = Term.type_of t';
- val p =
- Pretty.block [Pretty.quote (ProofContext.pretty_term ctxt t'), Pretty.fbrk,
- Pretty.str "::", Pretty.brk 1, Pretty.quote (ProofContext.pretty_typ ctxt ty)];
+ val (evls, evl) = split_last evaluators;
+ val t' = case get_first (fn f => try (f thy) t) evls
+ of SOME t' => t'
+ | NONE => evl thy t;
+ val ty' = Term.type_of t';
+ val p = Pretty.block [Pretty.quote (ProofContext.pretty_term ctxt t'),
+ Pretty.fbrk, Pretty.str "::", Pretty.brk 1,
+ Pretty.quote (ProofContext.pretty_typ ctxt ty')];
in Pretty.writeln p end;
-fun eval_print_cmd conv raw_t state =
+val evaluate = gen_evaluate (map snd evaluators);
+
+fun evaluate' name = gen_evaluate
+ [(the o AList.lookup (op =) evaluators) name];
+
+fun evaluate_cmd some_name raw_t state =
let
val ctxt = Toplevel.context_of state;
val t = Syntax.read_term ctxt raw_t;
- val thy = ProofContext.theory_of ctxt;
- val ct = Thm.cterm_of thy t;
- val (_, t') = (Logic.dest_equals o Thm.prop_of o conv) ct;
- val ty = Term.type_of t';
- val p =
- Pretty.block [Pretty.quote (ProofContext.pretty_term ctxt t'), Pretty.fbrk,
- Pretty.str "::", Pretty.brk 1, Pretty.quote (ProofContext.pretty_typ ctxt ty)];
- in Pretty.writeln p end;
+ in case some_name
+ of NONE => evaluate ctxt t
+ | SOME name => evaluate' name ctxt t
+ end;
end;
*}
@@ -229,11 +215,10 @@
ML {*
val valueP =
OuterSyntax.improper_command "value" "read, evaluate and print term" OuterKeyword.diag
- (OuterParse.term
- >> (fn t => Toplevel.no_timing o Toplevel.keep
- (Eval.eval_print_cmd (fn ct => case try Eval.eval_conv ct
- of SOME thm => thm
- | NONE => Codegen.evaluation_conv ct) t)));
+ (Scan.option (OuterParse.$$$ "(" |-- OuterParse.name --| OuterParse.$$$ ")")
+ -- OuterParse.term
+ >> (fn (some_name, t) => Toplevel.no_timing o Toplevel.keep
+ (Eval.evaluate_cmd some_name t)));
val _ = OuterSyntax.add_parsers [valueP];
*}
--- a/src/HOL/Library/Eval_Witness.thy Thu Oct 04 16:59:30 2007 +0200
+++ b/src/HOL/Library/Eval_Witness.thy Thu Oct 04 19:41:49 2007 +0200
@@ -57,12 +57,11 @@
| dest_exs n (Const ("Ex", _) $ Abs (v,T,b)) =
Abs (v, check_type T, dest_exs (n - 1) b)
| dest_exs _ _ = sys_error "dest_exs";
-
- val ct = Thm.cterm_of thy (dest_exs (length ws) (HOLogic.dest_Trueprop goal))
+ val t = dest_exs (length ws) (HOLogic.dest_Trueprop goal);
in
- if CodePackage.satisfies thy ct ws
+ if CodePackage.satisfies thy t ws
then goal
- else HOLogic.Trueprop $ (HOLogic.true_const) (*dummy*)
+ else HOLogic.Trueprop $ HOLogic.true_const (*dummy*)
end
*}
--- a/src/HOL/ex/Eval_Examples.thy Thu Oct 04 16:59:30 2007 +0200
+++ b/src/HOL/ex/Eval_Examples.thy Thu Oct 04 19:41:49 2007 +0200
@@ -27,14 +27,44 @@
text {* term evaluation *}
value "(Suc 2 + 1) * 4"
-value "(Suc 2 + 1) * 4"
+value (code) "(Suc 2 + 1) * 4"
+value (SML) "(Suc 2 + 1) * 4"
+value ("normal_form") "(Suc 2 + 1) * 4"
+
value "(Suc 2 + Suc 0) * Suc 3"
+value (code) "(Suc 2 + Suc 0) * Suc 3"
+value (SML) "(Suc 2 + Suc 0) * Suc 3"
+value ("normal_form") "(Suc 2 + Suc 0) * Suc 3"
+
value "nat 100"
+value (code) "nat 100"
+value (SML) "nat 100"
+value ("normal_form") "nat 100"
+
value "(10\<Colon>int) \<le> 12"
+value (code) "(10\<Colon>int) \<le> 12"
+value (SML) "(10\<Colon>int) \<le> 12"
+value ("normal_form") "(10\<Colon>int) \<le> 12"
+
+value "max (2::int) 4"
+value (code) "max (2::int) 4"
+value (SML) "max (2::int) 4"
+value ("normal_form") "max (2::int) 4"
+
+value "of_int 2 / of_int 4 * (1::rat)"
+(*value (code) "of_int 2 / of_int 4 * (1::rat)" FIXME*)
+value (SML) "of_int 2 / of_int 4 * (1::rat)"
+value ("normal_form") "of_int 2 / of_int 4 * (1::rat)"
+
value "[]::nat list"
+value (code) "[]::nat list"
+(*value (SML) "[]::nat list" FIXME*)
+value ("normal_form") "[]::nat list"
+
value "[(nat 100, ())]"
-value "max (2::int) 4"
-value "of_int 2 / of_int 4 * (1::rat)"
+value (code) "[(nat 100, ())]"
+(*value (SML) "[(nat 100, ())]" FIXME*)
+value ("normal_form") "[(nat 100, ())]"
text {* a fancy datatype *}
@@ -47,5 +77,8 @@
Cair 'a 'b
value "Shift (Cair (4::nat) [Suc 0])"
+value (code) "Shift (Cair (4::nat) [Suc 0])"
+value (SML) "Shift (Cair (4::nat) [Suc 0])"
+value ("normal_form") "Shift (Cair (4::nat) [Suc 0])"
end
--- a/src/Tools/code/code_funcgr.ML Thu Oct 04 16:59:30 2007 +0200
+++ b/src/Tools/code/code_funcgr.ML Thu Oct 04 19:41:49 2007 +0200
@@ -17,7 +17,7 @@
val make: theory -> string list -> T
val make_consts: theory -> string list -> string list * T
val eval_conv: theory -> (T -> cterm -> thm) -> cterm -> thm
- val eval_term: theory -> (T -> cterm -> 'a) -> cterm -> 'a
+ val eval_term: theory -> (T -> term -> 'a) -> term -> 'a
end
structure CodeFuncgr : CODE_FUNCGR =
@@ -155,7 +155,7 @@
fun instances_of thy algebra insts =
let
val thy_classes = (#classes o Sorts.rep_algebra o Sign.classes_of) thy;
- fun all_classops tyco class =
+ fun all_classparams tyco class =
try (AxClass.params_of_class thy) class
|> Option.map snd
|> these
@@ -164,7 +164,7 @@
Symtab.empty
|> fold (fn (tyco, class) =>
Symtab.map_default (tyco, []) (insert (op =) class)) insts
- |> (fn tab => Symtab.fold (fn (tyco, classes) => append (maps (all_classops tyco)
+ |> (fn tab => Symtab.fold (fn (tyco, classes) => append (maps (all_classparams tyco)
(Graph.all_succs thy_classes classes))) tab [])
end;
@@ -320,10 +320,10 @@
end;
in raw_eval thy conv' end;
-fun raw_eval_term thy f =
+fun raw_eval_term thy f t =
let
- fun f' _ _ funcgr ct = f funcgr ct;
- in raw_eval thy f' end;
+ fun f' _ _ funcgr ct = f funcgr (Thm.term_of ct);
+ in raw_eval thy f' (Thm.cterm_of thy t) end;
end; (*local*)
--- a/src/Tools/code/code_package.ML Thu Oct 04 16:59:30 2007 +0200
+++ b/src/Tools/code/code_package.ML Thu Oct 04 19:41:49 2007 +0200
@@ -13,10 +13,10 @@
-> cterm -> thm;
val eval_term: theory
-> (CodeThingol.code -> CodeThingol.typscheme * CodeThingol.iterm
- -> string list -> cterm -> 'a)
- -> cterm -> 'a;
+ -> string list -> term -> 'a)
+ -> term -> 'a;
val satisfies_ref: (unit -> bool) option ref;
- val satisfies: theory -> cterm -> string list -> bool;
+ val satisfies: theory -> term -> string list -> bool;
val eval_invoke: theory -> (string * (unit -> 'a) option ref) -> CodeThingol.code
-> CodeThingol.iterm * CodeThingol.itype -> string list -> 'a;
val codegen_command: theory -> string -> unit;
@@ -213,20 +213,20 @@
and ensure_def_inst thy (algbr as ((_, algebra), _)) funcgr (class, tyco) =
let
val superclasses = (Sorts.certify_sort algebra o Sorts.super_classes algebra) class;
- val (var, classops) = try (AxClass.params_of_class thy) class |> the_default ("'a", [])
+ val (var, classparams) = try (AxClass.params_of_class thy) class |> the_default ("'a", [])
val vs = Name.names Name.context "'a" (Sorts.mg_domain algebra tyco [class]);
val sorts' = Sorts.mg_domain (Sign.classes_of thy) tyco [class];
val vs' = map2 (fn (v, sort1) => fn sort2 => (v,
Sorts.inter_sort (Sign.classes_of thy) (sort1, sort2))) vs sorts';
val arity_typ = Type (tyco, map TFree vs);
val arity_typ' = Type (tyco, map (fn (v, sort) => TVar ((v, 0), sort)) vs');
- fun gen_superarity superclass =
+ fun exprgen_superarity superclass =
ensure_def_class thy algbr funcgr superclass
##>> ensure_def_classrel thy algbr funcgr (class, superclass)
##>> exprgen_dicts thy algbr funcgr (arity_typ, [superclass])
#>> (fn ((superclass, classrel), [DictConst (inst, dss)]) =>
(superclass, (classrel, (inst, dss))));
- fun gen_classop_def (c, ty) =
+ fun exprgen_classparam_inst (c, ty) =
let
val c_inst = Const (c, map_type_tfree (K arity_typ') ty);
val thm = Class.unoverload thy (Thm.cterm_of thy c_inst);
@@ -241,10 +241,10 @@
ensure_def_class thy algbr funcgr class
##>> ensure_def_tyco thy algbr funcgr tyco
##>> fold_map (exprgen_tyvar_sort thy algbr funcgr) vs
- ##>> fold_map gen_superarity superclasses
- ##>> fold_map gen_classop_def classops
- #>> (fn ((((class, tyco), arity), superarities), classops) =>
- CodeThingol.Classinst ((class, (tyco, arity)), (superarities, classops)));
+ ##>> fold_map exprgen_superarity superclasses
+ ##>> fold_map exprgen_classparam_inst classparams
+ #>> (fn ((((class, tyco), arity), superarities), classparams) =>
+ CodeThingol.Classinst ((class, (tyco, arity)), (superarities, classparams)));
val inst = CodeName.instance thy (class, tyco);
in
ensure_def thy defgen_inst inst
@@ -256,9 +256,9 @@
fun defgen_datatypecons tyco =
ensure_def_tyco thy algbr funcgr tyco
#>> K (CodeThingol.Datatypecons c');
- fun defgen_classop class =
+ fun defgen_classparam class =
ensure_def_class thy algbr funcgr class
- #>> K (CodeThingol.Classop c');
+ #>> K (CodeThingol.Classparam c');
fun defgen_fun trns =
let
val raw_thms = CodeFuncgr.funcs funcgr c;
@@ -277,14 +277,14 @@
val defgen = case Code.get_datatype_of_constr thy c
of SOME tyco => defgen_datatypecons tyco
| NONE => (case AxClass.class_of_param thy c
- of SOME class => defgen_classop class
+ of SOME class => defgen_classparam class
| NONE => defgen_fun)
in
ensure_def thy defgen c'
#> pair c'
end
and exprgen_term thy algbr funcgr (Const (c, ty)) =
- select_appgen thy algbr funcgr ((c, ty), [])
+ exprgen_app thy algbr funcgr ((c, ty), [])
| exprgen_term thy algbr funcgr (Free (v, _)) =
pair (IVar v)
| exprgen_term thy algbr funcgr (Abs (abs as (_, ty, _))) =
@@ -298,7 +298,7 @@
| exprgen_term thy algbr funcgr (t as _ $ _) =
case strip_comb t
of (Const (c, ty), ts) =>
- select_appgen thy algbr funcgr ((c, ty), ts)
+ exprgen_app thy algbr funcgr ((c, ty), ts)
| (t', ts) =>
exprgen_term thy algbr funcgr t'
##>> fold_map (exprgen_term thy algbr funcgr) ts
@@ -313,7 +313,7 @@
exprgen_const thy algbr funcgr c_ty
##>> fold_map (exprgen_term thy algbr funcgr) ts
#>> (fn (t, ts) => t `$$ ts)
-and select_appgen thy algbr funcgr ((c, ty), ts) =
+and exprgen_app thy algbr funcgr ((c, ty), ts) =
case Symtab.lookup (Appgens.get thy) c
of SOME (i, (appgen, _)) =>
if length ts < i then
@@ -430,10 +430,10 @@
val code = Program.get thy;
val seris' = map (fn (((target, module), file), args) =>
CodeTarget.get_serializer thy target permissive module file args
- CodeName.labelled_name (K false) cs) seris;
+ CodeName.labelled_name cs) seris;
in (map (fn f => f code) seris' : unit list; ()) end;
-fun raw_eval f thy g =
+fun raw_eval evaluate term_of thy g =
let
val value_name = "Isabelle_Eval.EVAL.EVAL";
fun ensure_eval thy algbr funcgr t =
@@ -459,23 +459,23 @@
end;
fun h funcgr ct =
let
- val (code, vs_ty_t, deps) = generate thy funcgr ensure_eval (Thm.term_of ct);
+ val (code, vs_ty_t, deps) = generate thy funcgr ensure_eval (term_of ct);
in g code vs_ty_t deps ct end;
- in f thy h end;
+ in evaluate thy h end;
-fun eval_conv thy = raw_eval CodeFuncgr.eval_conv thy;
-fun eval_term thy = raw_eval CodeFuncgr.eval_term thy;
+fun eval_conv thy = raw_eval CodeFuncgr.eval_conv Thm.term_of thy;
+fun eval_term thy = raw_eval CodeFuncgr.eval_term I thy;
-fun eval_invoke thy = CodeTarget.eval_invoke thy CodeName.labelled_name (K false);
+fun eval_invoke thy = CodeTarget.eval_invoke thy CodeName.labelled_name;
val satisfies_ref : (unit -> bool) option ref = ref NONE;
-fun satisfies thy ct witnesses =
+fun satisfies thy t witnesses =
let
fun evl code ((vs, ty), t) deps ct =
eval_invoke thy ("CodePackage.satisfies_ref", satisfies_ref)
code (t, ty) witnesses;
- in eval_term thy evl ct end;
+ in eval_term thy evl t end;
fun filter_generatable thy consts =
let