# HG changeset patch # User haftmann # Date 1226301536 -3600 # Node ID 4656aacba2bc44b86972f9e995eda50c27bccc71 # Parent c4fcffe0fe489e3f780ff2ff874777049fc0a9ee tuned diff -r c4fcffe0fe48 -r 4656aacba2bc src/HOL/Int.thy --- 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 \ int)" +definition int_number_of_def [code del]: + "number_of w = (of_int w \ int)" -instance - by intro_classes (simp only: int_number_of_def) +instance proof +qed (simp only: int_number_of_def) end diff -r c4fcffe0fe48 -r 4656aacba2bc src/Tools/code/code_funcgr.ML --- 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*) diff -r c4fcffe0fe48 -r 4656aacba2bc src/Tools/code/code_ml.ML --- 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; diff -r c4fcffe0fe48 -r 4656aacba2bc src/Tools/code/code_thingol.ML --- 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*)