--- a/src/HOL/Int.thy Fri Nov 07 08:57:15 2008 +0100
+++ b/src/HOL/Int.thy Mon Nov 10 08:18:56 2008 +0100
@@ -782,11 +782,11 @@
instantiation int :: number_ring
begin
-definition
- int_number_of_def [code del]: "number_of w = (of_int w \<Colon> int)"
+definition int_number_of_def [code del]:
+ "number_of w = (of_int w \<Colon> int)"
-instance
- by intro_classes (simp only: int_number_of_def)
+instance proof
+qed (simp only: int_number_of_def)
end
--- a/src/Tools/code/code_funcgr.ML Fri Nov 07 08:57:15 2008 +0100
+++ b/src/Tools/code/code_funcgr.ML Mon Nov 10 08:18:56 2008 +0100
@@ -14,8 +14,8 @@
val all: T -> string list
val pretty: theory -> T -> Pretty.T
val make: theory -> string list -> T
- val eval_conv: theory -> (term -> term * (T -> term -> thm)) -> cterm -> thm
- val eval_term: theory -> (term -> term * (T -> term -> 'a)) -> term -> 'a
+ val eval_conv: theory -> (term -> term * (T -> thm)) -> cterm -> thm
+ val eval_term: theory -> (term -> term * (T -> 'a)) -> term -> 'a
val timing: bool ref
end
@@ -218,42 +218,42 @@
val ensure_consts = ensure_consts;
-fun proto_eval thy cterm_of evaluator_fr evaluator proto_ct funcgr =
+fun proto_eval thy cterm_of evaluator_lift evaluator proto_ct funcgr =
let
val ct = cterm_of proto_ct;
val _ = Sign.no_vars (Syntax.pp_global thy) (Thm.term_of ct);
val _ = Term.fold_types (Type.no_tvars #> K I) (Thm.term_of ct) ();
- fun consts_of t = fold_aterms (fn Const c_ty => cons c_ty | _ => I)
- t [];
+ fun consts_of t =
+ fold_aterms (fn Const c_ty => cons c_ty | _ => I) t [];
val algebra = Code.coregular_algebra thy;
val thm = Code.preprocess_conv thy ct;
val ct' = Thm.rhs_of thm;
val t' = Thm.term_of ct';
val consts = map fst (consts_of t');
val funcgr' = ensure_consts thy algebra consts funcgr;
- val (t'', evaluator') = apsnd evaluator_fr (evaluator t');
+ val (t'', evaluator_funcgr) = evaluator t';
val consts' = consts_of t'';
val dicts = instances_of_consts thy algebra funcgr' consts';
val funcgr'' = ensure_consts thy algebra dicts funcgr';
- in (evaluator' thm funcgr'' t'', funcgr'') end;
+ in (evaluator_lift evaluator_funcgr thm funcgr'', funcgr'') end;
fun proto_eval_conv thy =
let
- fun evaluator evaluator' thm1 funcgr t =
+ fun evaluator_lift evaluator thm1 funcgr =
let
- val thm2 = evaluator' funcgr t;
+ val thm2 = evaluator funcgr;
val thm3 = Code.postprocess_conv thy (Thm.rhs_of thm2);
in
Thm.transitive thm1 (Thm.transitive thm2 thm3) handle THM _ =>
error ("could not construct evaluation proof:\n"
^ (cat_lines o map Display.string_of_thm) [thm1, thm2, thm3])
end;
- in proto_eval thy I evaluator end;
+ in proto_eval thy I evaluator_lift end;
fun proto_eval_term thy =
let
- fun evaluator evaluator' _ funcgr t = evaluator' funcgr t;
- in proto_eval thy (Thm.cterm_of thy) evaluator end;
+ fun evaluator_lift evaluator _ funcgr = evaluator funcgr;
+ in proto_eval thy (Thm.cterm_of thy) evaluator_lift end;
end; (*local*)
--- a/src/Tools/code/code_ml.ML Fri Nov 07 08:57:15 2008 +0100
+++ b/src/Tools/code/code_ml.ML Mon Nov 10 08:18:56 2008 +0100
@@ -8,9 +8,9 @@
signature CODE_ML =
sig
val eval_conv: string * (unit -> thm) option ref
- -> theory -> cterm -> string list -> thm;
+ -> theory -> cterm -> string list -> thm
val eval_term: string * (unit -> 'a) option ref
- -> theory -> term -> string list -> 'a;
+ -> theory -> term -> string list -> 'a
val setup: theory -> theory
end;
@@ -893,7 +893,7 @@
fun eval' naming program ((vs, ty), t) deps =
let
val _ = if Code_Thingol.contains_dictvar t then
- error "Term to be evaluated constains free dictionaries" else ();
+ error "Term to be evaluated contains free dictionaries" else ();
val value_name = "Value.VALUE.value"
val program' = program
|> Graph.new_node (value_name,
@@ -903,7 +903,7 @@
val sml_code = "let\n" ^ value_code ^ "\nin " ^ value_name'
^ space_implode " " (map (enclose "(" ")") args) ^ " end";
in ML_Context.evaluate ctxt Output.ml_output false reff sml_code end;
- in eval'' thy (fn t => (t, eval')) ct end;
+ in eval'' thy (rpair eval') ct end;
fun eval_conv reff = eval Code_Thingol.eval_conv Thm.term_of reff;
fun eval_term reff = eval Code_Thingol.eval_term I reff;
--- a/src/Tools/code/code_thingol.ML Fri Nov 07 08:57:15 2008 +0100
+++ b/src/Tools/code/code_thingol.ML Mon Nov 10 08:18:56 2008 +0100
@@ -449,6 +449,8 @@
(** translation kernel **)
+(* generic mechanisms *)
+
fun ensure_stmt lookup declare generate thing (dep, (naming, program)) =
let
fun add_dep name = case dep of NONE => I
@@ -482,6 +484,9 @@
^ Syntax.string_of_sort_global thy sort;
in error ("Wellsortedness error" ^ err_thm ^ ":\n" ^ err_typ ^ "\n" ^ err_class) end;
+
+(* translation *)
+
fun ensure_class thy (algbr as (_, algebra)) funcgr class =
let
val superclasses = (Sorts.certify_sort algebra o Sorts.super_classes algebra) class;
@@ -713,8 +718,6 @@
| NONE => translate_app_default thy algbr funcgr thm ((c, ty), ts);
-(** generated programs **)
-
(* store *)
structure Program = CodeDataFun
@@ -733,7 +736,7 @@
val cached_program = Program.get;
-fun generate thy funcgr f name =
+fun invoke_generation thy funcgr f name =
Program.change_yield thy (fn naming_program => (NONE, naming_program)
|> f thy (Code.operational_algebra thy) funcgr name
|-> (fn name => fn (_, naming_program) => (name, naming_program)));
@@ -750,7 +753,7 @@
fun generate_consts thy algebra funcgr =
fold_map (ensure_const thy algebra funcgr);
in
- generate thy (Code_Funcgr.make thy cs) generate_consts cs
+ invoke_generation thy (Code_Funcgr.make thy cs) generate_consts cs
|-> project_consts
end;
@@ -783,20 +786,17 @@
#> term_value
end;
-fun eval eval_kind thy evaluator =
+fun eval thy evaluator t =
let
- fun evaluator'' evaluator''' funcgr t =
+ val (t', evaluator'') = evaluator t;
+ fun evaluator' funcgr =
let
- val (((naming, program), (vs_ty_t, deps)), _) = generate thy funcgr ensure_value t;
- in evaluator''' naming program vs_ty_t deps end;
- fun evaluator' t =
- let
- val (t', evaluator''') = evaluator t;
- in (t', evaluator'' evaluator''') end;
- in eval_kind thy evaluator' end
+ val (((naming, program), (vs_ty_t, deps)), _) = invoke_generation thy funcgr ensure_value t';
+ in evaluator'' naming program vs_ty_t deps end;
+ in (t', evaluator') end
-fun eval_conv thy = eval Code_Funcgr.eval_conv thy;
-fun eval_term thy = eval Code_Funcgr.eval_term thy;
+fun eval_conv thy = Code_Funcgr.eval_conv thy o eval thy;
+fun eval_term thy = Code_Funcgr.eval_term thy o eval thy;
end; (*struct*)