--- a/Admin/isatest/settings/cygwin-poly-e Wed Sep 15 16:23:11 2010 +0200
+++ b/Admin/isatest/settings/cygwin-poly-e Wed Sep 15 17:05:18 2010 +0200
@@ -24,5 +24,4 @@
ISABELLE_USEDIR_OPTIONS="-M 1 -i false -d false"
-unset KODKODI
-#init_component "$HOME/contrib_devel/kodkodi"
+init_component "$HOME/contrib/kodkodi"
--- a/src/HOL/Code_Evaluation.thy Wed Sep 15 16:23:11 2010 +0200
+++ b/src/HOL/Code_Evaluation.thy Wed Sep 15 17:05:18 2010 +0200
@@ -278,6 +278,7 @@
"term_of (k::code_numeral) = termify (number_of :: int \<Rightarrow> code_numeral) <\<cdot>> term_of_num (2::code_numeral) k"
by (simp only: term_of_anything)
+
subsection {* Obfuscate *}
print_translation {*
@@ -292,52 +293,47 @@
end
*}
-hide_const dummy_term App valapp
-hide_const (open) Const termify valtermify term_of term_of_num
-subsection {* Tracing of generated and evaluated code *}
-
-definition tracing :: "String.literal => 'a => 'a"
-where
- [code del]: "tracing s x = x"
+subsection {* Evaluation setup *}
ML {*
-structure Code_Evaluation =
+signature CODE_EVALUATION =
+sig
+ val eval_term: theory -> term -> term
+ val put_term: (unit -> term) -> Proof.context -> Proof.context
+ val tracing: string -> 'a -> 'a
+end;
+
+structure Code_Evaluation : CODE_EVALUATION =
struct
-fun tracing s x = (Output.tracing s; x)
+structure Evaluation = Proof_Data (
+ type T = unit -> term
+ fun init _ () = error "Evaluation"
+);
+val put_term = Evaluation.put;
+
+fun tracing s x = (Output.tracing s; x);
+
+fun eval_term thy t = Code_Runtime.value NONE (Evaluation.get, put_term, "Code_Evaluation.put_term")
+ I thy (HOLogic.mk_term_of (fastype_of t) t) [];
end
*}
+setup {*
+ Value.add_evaluator ("code", Code_Evaluation.eval_term o ProofContext.theory_of)
+*}
+
+definition tracing :: "String.literal \<Rightarrow> 'a \<Rightarrow> 'a" where
+ [code del]: "tracing s x = x"
+
code_const "tracing :: String.literal => 'a => 'a"
(Eval "Code'_Evaluation.tracing")
-hide_const (open) tracing
code_reserved Eval Code_Evaluation
-subsection {* Evaluation setup *}
-
-ML {*
-signature EVAL =
-sig
- val eval_ref: (unit -> term) option Unsynchronized.ref
- val eval_term: theory -> term -> term
-end;
-
-structure Eval : EVAL =
-struct
-
-val eval_ref = Unsynchronized.ref (NONE : (unit -> term) option);
-
-fun eval_term thy t =
- Code_Eval.eval NONE ("Eval.eval_ref", eval_ref) I thy (HOLogic.mk_term_of (fastype_of t) t) [];
-
-end;
-*}
-
-setup {*
- Value.add_evaluator ("code", Eval.eval_term o ProofContext.theory_of)
-*}
+hide_const dummy_term App valapp
+hide_const (open) Const termify valtermify term_of term_of_num tracing
end
--- a/src/HOL/HOL.thy Wed Sep 15 16:23:11 2010 +0200
+++ b/src/HOL/HOL.thy Wed Sep 15 17:05:18 2010 +0200
@@ -1966,12 +1966,10 @@
*}
ML {*
-structure Eval_Method =
-struct
-
-val eval_ref : (unit -> bool) option Unsynchronized.ref = Unsynchronized.ref NONE;
-
-end;
+structure Eval_Method = Proof_Data(
+ type T = unit -> bool
+ fun init thy () = error "Eval_Method"
+)
*}
oracle eval_oracle = {* fn ct =>
@@ -1980,8 +1978,8 @@
val t = Thm.term_of ct;
val dummy = @{cprop True};
in case try HOLogic.dest_Trueprop t
- of SOME t' => if Code_Eval.eval NONE
- ("Eval_Method.eval_ref", Eval_Method.eval_ref) (K I) thy t' []
+ of SOME t' => if Code_Runtime.value NONE
+ (Eval_Method.get, Eval_Method.put, "Eval_Method.put") (K I) thy t' []
then Thm.capply (Thm.capply @{cterm "op \<equiv> \<Colon> prop \<Rightarrow> prop \<Rightarrow> prop"} ct) dummy
else dummy
| NONE => dummy
--- a/src/HOL/IsaMakefile Wed Sep 15 16:23:11 2010 +0200
+++ b/src/HOL/IsaMakefile Wed Sep 15 17:05:18 2010 +0200
@@ -106,12 +106,12 @@
$(SRC)/Provers/quantifier1.ML \
$(SRC)/Provers/splitter.ML \
$(SRC)/Tools/cache_io.ML \
- $(SRC)/Tools/Code/code_eval.ML \
$(SRC)/Tools/Code/code_haskell.ML \
$(SRC)/Tools/Code/code_ml.ML \
$(SRC)/Tools/Code/code_namespace.ML \
$(SRC)/Tools/Code/code_preproc.ML \
$(SRC)/Tools/Code/code_printer.ML \
+ $(SRC)/Tools/Code/code_runtime.ML \
$(SRC)/Tools/Code/code_scala.ML \
$(SRC)/Tools/Code/code_simp.ML \
$(SRC)/Tools/Code/code_target.ML \
@@ -1011,6 +1011,7 @@
ex/InductiveInvariant_examples.thy ex/Intuitionistic.thy \
ex/Lagrange.thy ex/LocaleTest2.thy ex/MT.thy ex/MergeSort.thy \
ex/Meson_Test.thy ex/MonoidGroup.thy ex/Multiquote.thy ex/NatSum.thy \
+ ex/Normalization_by_Evaluation.thy \
ex/Numeral.thy ex/PER.thy ex/PresburgerEx.thy ex/Primrec.thy \
ex/Quickcheck_Examples.thy ex/Quickcheck_Lattice_Examples.thy \
ex/ROOT.ML ex/Recdefs.thy ex/Records.thy ex/ReflectionEx.thy \
--- a/src/HOL/Library/Eval_Witness.thy Wed Sep 15 16:23:11 2010 +0200
+++ b/src/HOL/Library/Eval_Witness.thy Wed Sep 15 17:05:18 2010 +0200
@@ -44,15 +44,6 @@
instance bool :: ml_equiv ..
instance list :: (ml_equiv) ml_equiv ..
-ML {*
-structure Eval_Witness_Method =
-struct
-
-val eval_ref : (unit -> bool) option Unsynchronized.ref = Unsynchronized.ref NONE;
-
-end;
-*}
-
oracle eval_witness_oracle = {* fn (cgoal, ws) =>
let
val thy = Thm.theory_of_cterm cgoal;
@@ -68,7 +59,7 @@
| dest_exs _ _ = sys_error "dest_exs";
val t = dest_exs (length ws) (HOLogic.dest_Trueprop goal);
in
- if Code_Eval.eval NONE ("Eval_Witness_Method.eval_ref", Eval_Witness_Method.eval_ref) (K I) thy t ws
+ if Code_Runtime.value NONE (Eval_Method.get, Eval_Method.put, "Eval_Method.put") (K I) thy t ws
then Thm.cterm_of thy goal
else @{cprop True} (*dummy*)
end
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Wed Sep 15 16:23:11 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Wed Sep 15 17:05:18 2010 +0200
@@ -43,18 +43,20 @@
val print_stored_rules : Proof.context -> unit
val print_all_modes : compilation -> Proof.context -> unit
val mk_casesrule : Proof.context -> term -> thm list -> term
- val eval_ref : (unit -> term Predicate.pred) option Unsynchronized.ref
- val random_eval_ref : (unit -> int * int -> term Predicate.pred * (int * int))
- option Unsynchronized.ref
- val dseq_eval_ref : (unit -> term DSequence.dseq) option Unsynchronized.ref
- val random_dseq_eval_ref : (unit -> int -> int -> int * int -> term DSequence.dseq * (int * int))
- option Unsynchronized.ref
- val new_random_dseq_eval_ref :
- (unit -> int -> int -> int * int -> int -> term Lazy_Sequence.lazy_sequence)
- option Unsynchronized.ref
- val new_random_dseq_stats_eval_ref :
- (unit -> int -> int -> int * int -> int -> (term * int) Lazy_Sequence.lazy_sequence)
- option Unsynchronized.ref
+
+ val put_pred_result : (unit -> term Predicate.pred) -> Proof.context -> Proof.context
+ val put_pred_random_result : (unit -> int * int -> term Predicate.pred * (int * int)) ->
+ Proof.context -> Proof.context
+ val put_dseq_result : (unit -> term DSequence.dseq) -> Proof.context -> Proof.context
+ val put_dseq_random_result : (unit -> int -> int -> int * int -> term DSequence.dseq * (int * int)) ->
+ Proof.context -> Proof.context
+ val put_lseq_random_result :
+ (unit -> int -> int -> int * int -> int -> term Lazy_Sequence.lazy_sequence) ->
+ Proof.context -> Proof.context
+ val put_lseq_random_stats_result :
+ (unit -> int -> int -> int * int -> int -> (term * int) Lazy_Sequence.lazy_sequence) ->
+ Proof.context -> Proof.context
+
val code_pred_intro_attrib : attribute
(* used by Quickcheck_Generator *)
(* temporary for testing of the compilation *)
@@ -3105,17 +3107,41 @@
(* transformation for code generation *)
-val eval_ref = Unsynchronized.ref (NONE : (unit -> term Predicate.pred) option);
-val random_eval_ref =
- Unsynchronized.ref (NONE : (unit -> int * int -> term Predicate.pred * (int * int)) option);
-val dseq_eval_ref = Unsynchronized.ref (NONE : (unit -> term DSequence.dseq) option);
-val random_dseq_eval_ref =
- Unsynchronized.ref (NONE : (unit -> int -> int -> int * int -> term DSequence.dseq * (int * int)) option);
-val new_random_dseq_eval_ref =
- Unsynchronized.ref (NONE : (unit -> int -> int -> int * int -> int -> term Lazy_Sequence.lazy_sequence) option)
-val new_random_dseq_stats_eval_ref =
- Unsynchronized.ref (NONE :
- (unit -> int -> int -> int * int -> int -> (term * int) Lazy_Sequence.lazy_sequence) option)
+structure Pred_Result = Proof_Data (
+ type T = unit -> term Predicate.pred
+ fun init _ () = error "Pred_Result"
+);
+val put_pred_result = Pred_Result.put;
+
+structure Pred_Random_Result = Proof_Data (
+ type T = unit -> int * int -> term Predicate.pred * (int * int)
+ fun init _ () = error "Pred_Random_Result"
+);
+val put_pred_random_result = Pred_Random_Result.put;
+
+structure Dseq_Result = Proof_Data (
+ type T = unit -> term DSequence.dseq
+ fun init _ () = error "Dseq_Result"
+);
+val put_dseq_result = Dseq_Result.put;
+
+structure Dseq_Random_Result = Proof_Data (
+ type T = unit -> int -> int -> int * int -> term DSequence.dseq * (int * int)
+ fun init _ () = error "Dseq_Random_Result"
+);
+val put_dseq_random_result = Dseq_Random_Result.put;
+
+structure Lseq_Random_Result = Proof_Data (
+ type T = unit -> int -> int -> int * int -> int -> term Lazy_Sequence.lazy_sequence
+ fun init _ () = error "Lseq_Random_Result"
+);
+val put_lseq_random_result = Lseq_Random_Result.put;
+
+structure Lseq_Random_Stats_Result = Proof_Data (
+ type T = unit -> int -> int -> int * int -> int -> (term * int) Lazy_Sequence.lazy_sequence
+ fun init _ () = error "Lseq_Random_Stats_Result"
+);
+val put_lseq_random_stats_result = Lseq_Random_Stats_Result.put;
(*FIXME turn this into an LCF-guarded preprocessor for comprehensions*)
fun analyze_compr ctxt compfuns param_user_modes (compilation, arguments) t_compr =
@@ -3251,7 +3277,7 @@
val [nrandom, size, depth] = arguments
in
rpair NONE (fst (DSequence.yieldn k
- (Code_Eval.eval NONE ("Predicate_Compile_Core.random_dseq_eval_ref", random_dseq_eval_ref)
+ (Code_Runtime.value NONE (Dseq_Random_Result.get, put_dseq_random_result, "Predicate_Compile_Core.put_dseq_random_result")
(fn proc => fn g => fn nrandom => fn size => fn s => g nrandom size s |>> DSequence.map proc)
thy t' [] nrandom size
|> Random_Engine.run)
@@ -3259,7 +3285,7 @@
end
| DSeq =>
rpair NONE (fst (DSequence.yieldn k
- (Code_Eval.eval NONE ("Predicate_Compile_Core.dseq_eval_ref", dseq_eval_ref)
+ (Code_Runtime.value NONE (Dseq_Result.get, put_dseq_result, "Predicate_Compile_Core.put_dseq_result")
DSequence.map thy t' []) (the_single arguments) true))
| New_Pos_Random_DSeq =>
let
@@ -3269,22 +3295,22 @@
if stats then
apsnd (SOME o accumulate) (split_list
(fst (Lazy_Sequence.yieldn k
- (Code_Eval.eval NONE
- ("Predicate_Compile_Core.new_random_dseq_stats_eval_ref", new_random_dseq_stats_eval_ref)
+ (Code_Runtime.value NONE
+ (Lseq_Random_Stats_Result.get, put_lseq_random_stats_result, "Predicate_Compile_Core.put_lseq_random_stats_result")
(fn proc => fn g => fn nrandom => fn size => fn s => fn depth => g nrandom size s depth
|> Lazy_Sequence.mapa (apfst proc))
thy t' [] nrandom size seed depth))))
else rpair NONE
(fst (Lazy_Sequence.yieldn k
- (Code_Eval.eval NONE
- ("Predicate_Compile_Core.new_random_dseq_eval_ref", new_random_dseq_eval_ref)
+ (Code_Runtime.value NONE
+ (Lseq_Random_Result.get, put_lseq_random_result, "Predicate_Compile_Core.put_lseq_random_result")
(fn proc => fn g => fn nrandom => fn size => fn s => fn depth => g nrandom size s depth
|> Lazy_Sequence.mapa proc)
thy t' [] nrandom size seed depth)))
end
| _ =>
rpair NONE (fst (Predicate.yieldn k
- (Code_Eval.eval NONE ("Predicate_Compile_Core.eval_ref", eval_ref)
+ (Code_Runtime.value NONE (Pred_Result.get, put_pred_result, "Predicate_Compile_Core.put_pred_result")
Predicate.map thy t' [])))
in ((T, ts), statistics) end;
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML Wed Sep 15 16:23:11 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML Wed Sep 15 17:05:18 2010 +0200
@@ -7,12 +7,15 @@
signature PREDICATE_COMPILE_QUICKCHECK =
sig
(*val quickcheck : Proof.context -> term -> int -> term list option*)
- val test_ref :
- ((unit -> int -> int -> int * int -> term list DSequence.dseq * (int * int)) option) Unsynchronized.ref
- val new_test_ref :
- ((unit -> int -> int -> int * int -> int -> term list Lazy_Sequence.lazy_sequence) option) Unsynchronized.ref;
- val eval_random_ref :
- ((unit -> int -> int -> int -> int * int -> term list Predicate.pred) option) Unsynchronized.ref;
+ val put_pred_result :
+ (unit -> int -> int -> int -> int * int -> term list Predicate.pred) ->
+ Proof.context -> Proof.context;
+ val put_dseq_result :
+ (unit -> int -> int -> int * int -> term list DSequence.dseq * (int * int)) ->
+ Proof.context -> Proof.context;
+ val put_lseq_result :
+ (unit -> int -> int -> int * int -> int -> term list Lazy_Sequence.lazy_sequence) ->
+ Proof.context -> Proof.context;
val tracing : bool Unsynchronized.ref;
val quiet : bool Unsynchronized.ref;
@@ -30,15 +33,23 @@
open Predicate_Compile_Aux;
-val test_ref =
- Unsynchronized.ref (NONE : (unit -> int -> int -> int * int -> term list DSequence.dseq * (int * int)) option);
+structure Pred_Result = Proof_Data (
+ type T = unit -> int -> int -> int -> int * int -> term list Predicate.pred
+ fun init _ () = error "Pred_Result"
+);
+val put_pred_result = Pred_Result.put;
-val new_test_ref =
- Unsynchronized.ref (NONE : (unit -> int -> int -> int * int -> int -> term list Lazy_Sequence.lazy_sequence) option)
+structure Dseq_Result = Proof_Data (
+ type T = unit -> int -> int -> int * int -> term list DSequence.dseq * (int * int)
+ fun init _ () = error "Dseq_Result"
+);
+val put_dseq_result = Dseq_Result.put;
-val eval_random_ref =
- Unsynchronized.ref (NONE : (unit -> int -> int -> int -> int * int -> term list Predicate.pred) option);
-
+structure Lseq_Result = Proof_Data (
+ type T = unit -> int -> int -> int * int -> int -> term list Lazy_Sequence.lazy_sequence
+ fun init _ () = error "Lseq_Result"
+);
+val put_lseq_result = Lseq_Result.put;
val tracing = Unsynchronized.ref false;
@@ -261,7 +272,7 @@
Pos_Random_DSeq =>
let
val compiled_term =
- Code_Eval.eval (SOME target) ("Predicate_Compile_Quickcheck.test_ref", test_ref)
+ Code_Runtime.value (SOME target) (Dseq_Result.get, put_dseq_result, "Predicate_Compile_Quickcheck.put_dseq_result")
(fn proc => fn g => fn n => fn size => fn s => g n size s |>> (DSequence.map o map) proc)
thy4 qc_term []
in
@@ -272,8 +283,8 @@
| New_Pos_Random_DSeq =>
let
val compiled_term =
- Code_Eval.eval (SOME target)
- ("Predicate_Compile_Quickcheck.new_test_ref", new_test_ref)
+ Code_Runtime.value (SOME target)
+ (Lseq_Result.get, put_lseq_result, "Predicate_Compile_Quickcheck.put_lseq_result")
(fn proc => fn g => fn nrandom => fn size => fn s => fn depth =>
g nrandom size s depth |> (Lazy_Sequence.mapa o map) proc)
thy4 qc_term []
@@ -286,8 +297,8 @@
end
| Depth_Limited_Random =>
let
- val compiled_term = Code_Eval.eval (SOME target)
- ("Predicate_Compile_Quickcheck.eval_random_ref", eval_random_ref)
+ val compiled_term = Code_Runtime.value (SOME target)
+ (Pred_Result.get, put_pred_result, "Predicate_Compile_Quickcheck.put_pred_result")
(fn proc => fn g => fn depth => fn nrandom => fn size => fn seed =>
g depth nrandom size seed |> (Predicate.map o map) proc)
thy4 qc_term []
--- a/src/HOL/Tools/quickcheck_generators.ML Wed Sep 15 16:23:11 2010 +0200
+++ b/src/HOL/Tools/quickcheck_generators.ML Wed Sep 15 17:05:18 2010 +0200
@@ -15,9 +15,10 @@
val ensure_random_datatype: Datatype.config -> string list -> theory -> theory
val compile_generator_expr:
Proof.context -> term -> int -> term list option * (bool list * bool)
- val eval_ref: (unit -> int -> seed -> term list option * seed) option Unsynchronized.ref
- val eval_report_ref:
- (unit -> int -> seed -> (term list option * (bool list * bool)) * seed) option Unsynchronized.ref
+ val put_counterexample: (unit -> int -> seed -> term list option * seed)
+ -> Proof.context -> Proof.context
+ val put_counterexample_report: (unit -> int -> seed -> (term list option * (bool list * bool)) * seed)
+ -> Proof.context -> Proof.context
val setup: theory -> theory
end;
@@ -304,13 +305,17 @@
(** building and compiling generator expressions **)
-val eval_ref :
- (unit -> int -> int * int -> term list option * (int * int)) option Unsynchronized.ref =
- Unsynchronized.ref NONE;
+structure Counterexample = Proof_Data (
+ type T = unit -> int -> int * int -> term list option * (int * int)
+ fun init _ () = error "Counterexample"
+);
+val put_counterexample = Counterexample.put;
-val eval_report_ref :
- (unit -> int -> seed -> (term list option * (bool list * bool)) * seed) option Unsynchronized.ref =
- Unsynchronized.ref NONE;
+structure Counterexample_Report = Proof_Data (
+ type T = unit -> int -> seed -> (term list option * (bool list * bool)) * seed
+ fun init _ () = error "Counterexample_Report"
+);
+val put_counterexample_report = Counterexample_Report.put;
val target = "Quickcheck";
@@ -387,13 +392,15 @@
in if Quickcheck.report ctxt then
let
val t' = mk_reporting_generator_expr thy t Ts;
- val compile = Code_Eval.eval (SOME target) ("Quickcheck_Generators.eval_report_ref", eval_report_ref)
+ val compile = Code_Runtime.value (SOME target)
+ (Counterexample_Report.get, put_counterexample_report, "Quickcheck_Generators.put_counterexample_report")
(fn proc => fn g => fn s => g s #>> (apfst o Option.map o map) proc) thy t' [];
in compile #> Random_Engine.run end
else
let
val t' = mk_generator_expr thy t Ts;
- val compile = Code_Eval.eval (SOME target) ("Quickcheck_Generators.eval_ref", eval_ref)
+ val compile = Code_Runtime.value (SOME target)
+ (Counterexample.get, put_counterexample, "Quickcheck_Generators.put_counterexample")
(fn proc => fn g => fn s => g s #>> (Option.map o map) proc) thy t' [];
val dummy_report = ([], false)
in compile #> Random_Engine.run #> rpair dummy_report end
@@ -404,7 +411,7 @@
val setup =
Datatype.interpretation ensure_random_datatype
- #> Code_Target.extend_target (target, (Code_Eval.target, K I))
+ #> Code_Target.extend_target (target, (Code_Runtime.target, K I))
#> Context.theory_map
(Quickcheck.add_generator ("code", compile_generator_expr));
--- a/src/HOL/ex/NormalForm.thy Wed Sep 15 16:23:11 2010 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,131 +0,0 @@
-(* Authors: Klaus Aehlig, Tobias Nipkow *)
-
-header {* Testing implementation of normalization by evaluation *}
-
-theory NormalForm
-imports Complex_Main
-begin
-
-lemma "True" by normalization
-lemma "p \<longrightarrow> True" by normalization
-declare disj_assoc [code nbe]
-lemma "((P | Q) | R) = (P | (Q | R))" by normalization
-lemma "0 + (n::nat) = n" by normalization
-lemma "0 + Suc n = Suc n" by normalization
-lemma "Suc n + Suc m = n + Suc (Suc m)" by normalization
-lemma "~((0::nat) < (0::nat))" by normalization
-
-datatype n = Z | S n
-
-primrec add :: "n \<Rightarrow> n \<Rightarrow> n" where
- "add Z = id"
- | "add (S m) = S o add m"
-
-primrec add2 :: "n \<Rightarrow> n \<Rightarrow> n" where
- "add2 Z n = n"
- | "add2 (S m) n = S(add2 m n)"
-
-declare add2.simps [code]
-lemma [code nbe]: "add2 (add2 n m) k = add2 n (add2 m k)"
- by (induct n) auto
-lemma [code]: "add2 n (S m) = S (add2 n m)"
- by(induct n) auto
-lemma [code]: "add2 n Z = n"
- by(induct n) auto
-
-lemma "add2 (add2 n m) k = add2 n (add2 m k)" by normalization
-lemma "add2 (add2 (S n) (S m)) (S k) = S(S(S(add2 n (add2 m k))))" by normalization
-lemma "add2 (add2 (S n) (add2 (S m) Z)) (S k) = S(S(S(add2 n (add2 m k))))" by normalization
-
-primrec mul :: "n \<Rightarrow> n \<Rightarrow> n" where
- "mul Z = (%n. Z)"
- | "mul (S m) = (%n. add (mul m n) n)"
-
-primrec mul2 :: "n \<Rightarrow> n \<Rightarrow> n" where
- "mul2 Z n = Z"
- | "mul2 (S m) n = add2 n (mul2 m n)"
-
-primrec exp :: "n \<Rightarrow> n \<Rightarrow> n" where
- "exp m Z = S Z"
- | "exp m (S n) = mul (exp m n) m"
-
-lemma "mul2 (S(S(S(S(S Z))))) (S(S(S Z))) = S(S(S(S(S(S(S(S(S(S(S(S(S(S(S Z))))))))))))))" by normalization
-lemma "mul (S(S(S(S(S Z))))) (S(S(S Z))) = S(S(S(S(S(S(S(S(S(S(S(S(S(S(S Z))))))))))))))" by normalization
-lemma "exp (S(S Z)) (S(S(S(S Z)))) = exp (S(S(S(S Z)))) (S(S Z))" by normalization
-
-lemma "(let ((x,y),(u,v)) = ((Z,Z),(Z,Z)) in add (add x y) (add u v)) = Z" by normalization
-lemma "split (%x y. x) (a, b) = a" by normalization
-lemma "(%((x,y),(u,v)). add (add x y) (add u v)) ((Z,Z),(Z,Z)) = Z" by normalization
-
-lemma "case Z of Z \<Rightarrow> True | S x \<Rightarrow> False" by normalization
-
-lemma "[] @ [] = []" by normalization
-lemma "map f [x,y,z::'x] = [f x, f y, f z]" by normalization
-lemma "[a, b, c] @ xs = a # b # c # xs" by normalization
-lemma "[] @ xs = xs" by normalization
-lemma "map (%f. f True) [id, g, Not] = [True, g True, False]" by normalization
-
-lemma "map (%f. f True) ([id, g, Not] @ fs) = [True, g True, False] @ map (%f. f True) fs"
- by normalization rule+
-lemma "rev [a, b, c] = [c, b, a]" by normalization
-normal_form "rev (a#b#cs) = rev cs @ [b, a]"
-normal_form "map (%F. F [a,b,c::'x]) (map map [f,g,h])"
-normal_form "map (%F. F ([a,b,c] @ ds)) (map map ([f,g,h]@fs))"
-normal_form "map (%F. F [Z,S Z,S(S Z)]) (map map [S,add (S Z),mul (S(S Z)),id])"
-lemma "map (%x. case x of None \<Rightarrow> False | Some y \<Rightarrow> True) [None, Some ()] = [False, True]"
- by normalization
-normal_form "case xs of [] \<Rightarrow> True | x#xs \<Rightarrow> False"
-normal_form "map (%x. case x of None \<Rightarrow> False | Some y \<Rightarrow> True) xs = P"
-lemma "let x = y in [x, x] = [y, y]" by normalization
-lemma "Let y (%x. [x,x]) = [y, y]" by normalization
-normal_form "case n of Z \<Rightarrow> True | S x \<Rightarrow> False"
-lemma "(%(x,y). add x y) (S z,S z) = S (add z (S z))" by normalization
-normal_form "filter (%x. x) ([True,False,x]@xs)"
-normal_form "filter Not ([True,False,x]@xs)"
-
-lemma "[x,y,z] @ [a,b,c] = [x, y, z, a, b, c]" by normalization
-lemma "(%(xs, ys). xs @ ys) ([a, b, c], [d, e, f]) = [a, b, c, d, e, f]" by normalization
-lemma "map (%x. case x of None \<Rightarrow> False | Some y \<Rightarrow> True) [None, Some ()] = [False, True]" by normalization
-
-lemma "last [a, b, c] = c" by normalization
-lemma "last ([a, b, c] @ xs) = last (c # xs)" by normalization
-
-lemma "(2::int) + 3 - 1 + (- k) * 2 = 4 + - k * 2" by normalization
-lemma "(-4::int) * 2 = -8" by normalization
-lemma "abs ((-4::int) + 2 * 1) = 2" by normalization
-lemma "(2::int) + 3 = 5" by normalization
-lemma "(2::int) + 3 * (- 4) * (- 1) = 14" by normalization
-lemma "(2::int) + 3 * (- 4) * 1 + 0 = -10" by normalization
-lemma "(2::int) < 3" by normalization
-lemma "(2::int) <= 3" by normalization
-lemma "abs ((-4::int) + 2 * 1) = 2" by normalization
-lemma "4 - 42 * abs (3 + (-7\<Colon>int)) = -164" by normalization
-lemma "(if (0\<Colon>nat) \<le> (x\<Colon>nat) then 0\<Colon>nat else x) = 0" by normalization
-lemma "4 = Suc (Suc (Suc (Suc 0)))" by normalization
-lemma "nat 4 = Suc (Suc (Suc (Suc 0)))" by normalization
-lemma "[Suc 0, 0] = [Suc 0, 0]" by normalization
-lemma "max (Suc 0) 0 = Suc 0" by normalization
-lemma "(42::rat) / 1704 = 1 / 284 + 3 / 142" by normalization
-normal_form "Suc 0 \<in> set ms"
-
-lemma "f = f" by normalization
-lemma "f x = f x" by normalization
-lemma "(f o g) x = f (g x)" by normalization
-lemma "(f o id) x = f x" by normalization
-normal_form "(\<lambda>x. x)"
-
-(* Church numerals: *)
-
-normal_form "(%m n f x. m f (n f x)) (%f x. f(f(f(x)))) (%f x. f(f(f(x))))"
-normal_form "(%m n f x. m (n f) x) (%f x. f(f(f(x)))) (%f x. f(f(f(x))))"
-normal_form "(%m n. n m) (%f x. f(f(f(x)))) (%f x. f(f(f(x))))"
-
-(* handling of type classes in connection with equality *)
-
-lemma "map f [x, y] = [f x, f y]" by normalization
-lemma "(map f [x, y], w) = ([f x, f y], w)" by normalization
-lemma "map f [x, y] = [f x \<Colon> 'a\<Colon>semigroup_add, f y]" by normalization
-lemma "map f [x \<Colon> 'a\<Colon>semigroup_add, y] = [f x, f y]" by normalization
-lemma "(map f [x \<Colon> 'a\<Colon>semigroup_add, y], w \<Colon> 'b\<Colon>finite) = ([f x, f y], w)" by normalization
-
-end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/ex/Normalization_by_Evaluation.thy Wed Sep 15 17:05:18 2010 +0200
@@ -0,0 +1,131 @@
+(* Authors: Klaus Aehlig, Tobias Nipkow *)
+
+header {* Testing implementation of normalization by evaluation *}
+
+theory Normalization_by_Evaluation
+imports Complex_Main
+begin
+
+lemma "True" by normalization
+lemma "p \<longrightarrow> True" by normalization
+declare disj_assoc [code nbe]
+lemma "((P | Q) | R) = (P | (Q | R))" by normalization
+lemma "0 + (n::nat) = n" by normalization
+lemma "0 + Suc n = Suc n" by normalization
+lemma "Suc n + Suc m = n + Suc (Suc m)" by normalization
+lemma "~((0::nat) < (0::nat))" by normalization
+
+datatype n = Z | S n
+
+primrec add :: "n \<Rightarrow> n \<Rightarrow> n" where
+ "add Z = id"
+ | "add (S m) = S o add m"
+
+primrec add2 :: "n \<Rightarrow> n \<Rightarrow> n" where
+ "add2 Z n = n"
+ | "add2 (S m) n = S(add2 m n)"
+
+declare add2.simps [code]
+lemma [code nbe]: "add2 (add2 n m) k = add2 n (add2 m k)"
+ by (induct n) auto
+lemma [code]: "add2 n (S m) = S (add2 n m)"
+ by(induct n) auto
+lemma [code]: "add2 n Z = n"
+ by(induct n) auto
+
+lemma "add2 (add2 n m) k = add2 n (add2 m k)" by normalization
+lemma "add2 (add2 (S n) (S m)) (S k) = S(S(S(add2 n (add2 m k))))" by normalization
+lemma "add2 (add2 (S n) (add2 (S m) Z)) (S k) = S(S(S(add2 n (add2 m k))))" by normalization
+
+primrec mul :: "n \<Rightarrow> n \<Rightarrow> n" where
+ "mul Z = (%n. Z)"
+ | "mul (S m) = (%n. add (mul m n) n)"
+
+primrec mul2 :: "n \<Rightarrow> n \<Rightarrow> n" where
+ "mul2 Z n = Z"
+ | "mul2 (S m) n = add2 n (mul2 m n)"
+
+primrec exp :: "n \<Rightarrow> n \<Rightarrow> n" where
+ "exp m Z = S Z"
+ | "exp m (S n) = mul (exp m n) m"
+
+lemma "mul2 (S(S(S(S(S Z))))) (S(S(S Z))) = S(S(S(S(S(S(S(S(S(S(S(S(S(S(S Z))))))))))))))" by normalization
+lemma "mul (S(S(S(S(S Z))))) (S(S(S Z))) = S(S(S(S(S(S(S(S(S(S(S(S(S(S(S Z))))))))))))))" by normalization
+lemma "exp (S(S Z)) (S(S(S(S Z)))) = exp (S(S(S(S Z)))) (S(S Z))" by normalization
+
+lemma "(let ((x,y),(u,v)) = ((Z,Z),(Z,Z)) in add (add x y) (add u v)) = Z" by normalization
+lemma "split (%x y. x) (a, b) = a" by normalization
+lemma "(%((x,y),(u,v)). add (add x y) (add u v)) ((Z,Z),(Z,Z)) = Z" by normalization
+
+lemma "case Z of Z \<Rightarrow> True | S x \<Rightarrow> False" by normalization
+
+lemma "[] @ [] = []" by normalization
+lemma "map f [x,y,z::'x] = [f x, f y, f z]" by normalization
+lemma "[a, b, c] @ xs = a # b # c # xs" by normalization
+lemma "[] @ xs = xs" by normalization
+lemma "map (%f. f True) [id, g, Not] = [True, g True, False]" by normalization
+
+lemma "map (%f. f True) ([id, g, Not] @ fs) = [True, g True, False] @ map (%f. f True) fs"
+ by normalization rule+
+lemma "rev [a, b, c] = [c, b, a]" by normalization
+value [nbe] "rev (a#b#cs) = rev cs @ [b, a]"
+value [nbe] "map (%F. F [a,b,c::'x]) (map map [f,g,h])"
+value [nbe] "map (%F. F ([a,b,c] @ ds)) (map map ([f,g,h]@fs))"
+value [nbe] "map (%F. F [Z,S Z,S(S Z)]) (map map [S,add (S Z),mul (S(S Z)),id])"
+lemma "map (%x. case x of None \<Rightarrow> False | Some y \<Rightarrow> True) [None, Some ()] = [False, True]"
+ by normalization
+value [nbe] "case xs of [] \<Rightarrow> True | x#xs \<Rightarrow> False"
+value [nbe] "map (%x. case x of None \<Rightarrow> False | Some y \<Rightarrow> True) xs = P"
+lemma "let x = y in [x, x] = [y, y]" by normalization
+lemma "Let y (%x. [x,x]) = [y, y]" by normalization
+value [nbe] "case n of Z \<Rightarrow> True | S x \<Rightarrow> False"
+lemma "(%(x,y). add x y) (S z,S z) = S (add z (S z))" by normalization
+value [nbe] "filter (%x. x) ([True,False,x]@xs)"
+value [nbe] "filter Not ([True,False,x]@xs)"
+
+lemma "[x,y,z] @ [a,b,c] = [x, y, z, a, b, c]" by normalization
+lemma "(%(xs, ys). xs @ ys) ([a, b, c], [d, e, f]) = [a, b, c, d, e, f]" by normalization
+lemma "map (%x. case x of None \<Rightarrow> False | Some y \<Rightarrow> True) [None, Some ()] = [False, True]" by normalization
+
+lemma "last [a, b, c] = c" by normalization
+lemma "last ([a, b, c] @ xs) = last (c # xs)" by normalization
+
+lemma "(2::int) + 3 - 1 + (- k) * 2 = 4 + - k * 2" by normalization
+lemma "(-4::int) * 2 = -8" by normalization
+lemma "abs ((-4::int) + 2 * 1) = 2" by normalization
+lemma "(2::int) + 3 = 5" by normalization
+lemma "(2::int) + 3 * (- 4) * (- 1) = 14" by normalization
+lemma "(2::int) + 3 * (- 4) * 1 + 0 = -10" by normalization
+lemma "(2::int) < 3" by normalization
+lemma "(2::int) <= 3" by normalization
+lemma "abs ((-4::int) + 2 * 1) = 2" by normalization
+lemma "4 - 42 * abs (3 + (-7\<Colon>int)) = -164" by normalization
+lemma "(if (0\<Colon>nat) \<le> (x\<Colon>nat) then 0\<Colon>nat else x) = 0" by normalization
+lemma "4 = Suc (Suc (Suc (Suc 0)))" by normalization
+lemma "nat 4 = Suc (Suc (Suc (Suc 0)))" by normalization
+lemma "[Suc 0, 0] = [Suc 0, 0]" by normalization
+lemma "max (Suc 0) 0 = Suc 0" by normalization
+lemma "(42::rat) / 1704 = 1 / 284 + 3 / 142" by normalization
+value [nbe] "Suc 0 \<in> set ms"
+
+lemma "f = f" by normalization
+lemma "f x = f x" by normalization
+lemma "(f o g) x = f (g x)" by normalization
+lemma "(f o id) x = f x" by normalization
+value [nbe] "(\<lambda>x. x)"
+
+(* Church numerals: *)
+
+value [nbe] "(%m n f x. m f (n f x)) (%f x. f(f(f(x)))) (%f x. f(f(f(x))))"
+value [nbe] "(%m n f x. m (n f) x) (%f x. f(f(f(x)))) (%f x. f(f(f(x))))"
+value [nbe] "(%m n. n m) (%f x. f(f(f(x)))) (%f x. f(f(f(x))))"
+
+(* handling of type classes in connection with equality *)
+
+lemma "map f [x, y] = [f x, f y]" by normalization
+lemma "(map f [x, y], w) = ([f x, f y], w)" by normalization
+lemma "map f [x, y] = [f x \<Colon> 'a\<Colon>semigroup_add, f y]" by normalization
+lemma "map f [x \<Colon> 'a\<Colon>semigroup_add, y] = [f x, f y]" by normalization
+lemma "(map f [x \<Colon> 'a\<Colon>semigroup_add, y], w \<Colon> 'b\<Colon>finite) = ([f x, f y], w)" by normalization
+
+end
--- a/src/HOL/ex/ROOT.ML Wed Sep 15 16:23:11 2010 +0200
+++ b/src/HOL/ex/ROOT.ML Wed Sep 15 17:05:18 2010 +0200
@@ -8,7 +8,7 @@
"Efficient_Nat_examples",
"FuncSet",
"Eval_Examples",
- "NormalForm"
+ "Normalization_by_Evaluation"
];
use_thys [
--- a/src/Pure/Isar/code.ML Wed Sep 15 16:23:11 2010 +0200
+++ b/src/Pure/Isar/code.ML Wed Sep 15 17:05:18 2010 +0200
@@ -89,16 +89,14 @@
signature CODE_DATA =
sig
type T
- val change: theory -> (T -> T) -> T
- val change_yield: theory -> (T -> 'a * T) -> 'a * T
+ val change: theory option -> (T -> T) -> T
+ val change_yield: theory option -> (T -> 'a * T) -> 'a * T
end;
signature PRIVATE_CODE =
sig
include CODE
val declare_data: Object.T -> serial
- val change_data: serial * ('a -> Object.T) * (Object.T -> 'a)
- -> theory -> ('a -> 'a) -> 'a
val change_yield_data: serial * ('a -> Object.T) * (Object.T -> 'a)
-> theory -> ('a -> 'b * 'a) -> 'b * 'a
end;
@@ -310,8 +308,6 @@
((K o SOME) (Datatab.update (kind, mk data') datatab, thy_ref));
in result end;
-fun change_data ops theory f = change_yield_data ops theory (f #> pair ()) |> snd;
-
end; (*local*)
@@ -1277,8 +1273,10 @@
val data_op = (kind, Data, dest);
-val change = Code.change_data data_op;
-fun change_yield thy = Code.change_yield_data data_op thy;
+fun change_yield (SOME thy) f = Code.change_yield_data data_op thy f
+ | change_yield NONE f = f Data.empty
+
+fun change some_thy f = snd (change_yield some_thy (pair () o f));
end;
--- a/src/Pure/ML/ml_context.ML Wed Sep 15 16:23:11 2010 +0200
+++ b/src/Pure/ML/ml_context.ML Wed Sep 15 17:05:18 2010 +0200
@@ -36,8 +36,9 @@
val eval_text_in: Proof.context option -> bool -> Position.T -> Symbol_Pos.text -> unit
val expression: Position.T -> string -> string -> ML_Lex.token Antiquote.antiquote list ->
Context.generic -> Context.generic
- val evaluate: Proof.context -> bool ->
- string * (unit -> 'a) option Unsynchronized.ref -> string * string -> 'a
+ val value: Proof.context ->
+ (Proof.context -> unit -> 'a) * ((unit -> 'a) -> Proof.context -> Proof.context) * string ->
+ string * string -> 'a
end
structure ML_Context: ML_CONTEXT =
@@ -213,17 +214,15 @@
(ML_Lex.read Position.none ("Context.set_thread_data (SOME (let " ^ bind ^ " = ") @ ants @
ML_Lex.read Position.none (" in " ^ body ^ " end (ML_Context.the_generic_context ())));")));
-
-(* FIXME not thread-safe -- reference can be accessed directly *)
-fun evaluate ctxt verbose (ref_name, r) (prelude, txt) = NAMED_CRITICAL "ML" (fn () =>
+fun value ctxt (get, put, put_ml) (prelude, value) =
let
- val s = prelude ^ "val _ = (" ^ ref_name ^ " := SOME (fn () => " ^ txt ^ "))"
- val ants = ML_Lex.read Position.none s;
- val _ = r := NONE;
- val _ =
- Context.setmp_thread_data (SOME (Context.Proof ctxt))
- (fn () => eval verbose Position.none ants) ();
- in (case ! r of NONE => error ("Bad evaluation for " ^ ref_name) | SOME e => e) end) ();
+ val read = ML_Lex.read Position.none;
+ val ants = read prelude @ read ("val _ = Context.set_thread_data (SOME (Context.map_proof (" ^ put_ml
+ ^ " (fn () => " ^ value ^ ")) (ML_Context.the_generic_context ())))");
+ val ctxt' = ctxt
+ |> put (fn () => error ("Bad evaluation for " ^ quote put_ml))
+ |> Context.proof_map (exec (fn () => eval false Position.none ants));
+ in get ctxt' () end;
end;
--- a/src/Pure/PIDE/document.ML Wed Sep 15 16:23:11 2010 +0200
+++ b/src/Pure/PIDE/document.ML Wed Sep 15 17:05:18 2010 +0200
@@ -204,10 +204,10 @@
fun async_state tr st =
if Toplevel.print_of tr then
ignore
- (Future.fork
+ (Future.fork_group (Task_Queue.new_group NONE)
(fn () =>
Toplevel.setmp_thread_position tr
- (fn () => Future.status (fn () => Toplevel.print_state false st)) ()))
+ (fn () => Toplevel.print_state false st) ()))
else ();
in
--- a/src/Tools/Code/code_eval.ML Wed Sep 15 16:23:11 2010 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,221 +0,0 @@
-(* Title: Tools/Code/code_eval.ML
- Author: Florian Haftmann, TU Muenchen
-
-Runtime services building on code generation into implementation language SML.
-*)
-
-signature CODE_EVAL =
-sig
- val target: string
- val eval: string option -> string * (unit -> 'a) option Unsynchronized.ref
- -> ((term -> term) -> 'a -> 'a) -> theory -> term -> string list -> 'a
- val setup: theory -> theory
-end;
-
-structure Code_Eval : CODE_EVAL =
-struct
-
-(** generic **)
-
-val target = "Eval";
-
-fun evaluation_code thy module_name tycos consts =
- let
- val (consts', (naming, program)) = Code_Thingol.consts_program thy false consts;
- val tycos' = map (the o Code_Thingol.lookup_tyco naming) tycos;
- val (ml_code, target_names) = Code_Target.produce_code_for thy
- target NONE module_name [] naming program (consts' @ tycos');
- val (consts'', tycos'') = chop (length consts') target_names;
- val consts_map = map2 (fn const => fn NONE =>
- error ("Constant " ^ (quote o Code.string_of_const thy) const
- ^ "\nhas a user-defined serialization")
- | SOME const'' => (const, const'')) consts consts''
- val tycos_map = map2 (fn tyco => fn NONE =>
- error ("Type " ^ (quote o Sign.extern_type thy) tyco
- ^ "\nhas a user-defined serialization")
- | SOME tyco'' => (tyco, tyco'')) tycos tycos'';
- in (ml_code, (tycos_map, consts_map)) end;
-
-
-(** evaluation **)
-
-fun eval some_target reff postproc thy t args =
- let
- val ctxt = ProofContext.init_global thy;
- fun evaluator naming program ((_, (_, ty)), t) deps =
- let
- val _ = if Code_Thingol.contains_dictvar t then
- error "Term to be evaluated contains free dictionaries" else ();
- val value_name = "Value.VALUE.value"
- val program' = program
- |> Graph.new_node (value_name,
- Code_Thingol.Fun (Term.dummy_patternN, ((([], ty), [(([], t), (NONE, true))]), NONE)))
- |> fold (curry Graph.add_edge value_name) deps;
- val (program_code, [SOME value_name']) = Code_Target.produce_code_for thy
- (the_default target some_target) NONE "Code" [] naming program' [value_name];
- val value_code = space_implode " "
- (value_name' :: map (enclose "(" ")") args);
- in ML_Context.evaluate ctxt false reff (program_code, value_code) end;
- in Code_Thingol.dynamic_eval_value thy postproc evaluator t end;
-
-
-(** instrumentalization by antiquotation **)
-
-local
-
-structure Code_Antiq_Data = Proof_Data
-(
- type T = (string list * string list) * (bool
- * (string * ((string * string) list * (string * string) list)) lazy);
- fun init _ = (([], []), (true, (Lazy.value ("", ([], [])))));
-);
-
-val is_first_occ = fst o snd o Code_Antiq_Data.get;
-
-fun register_code new_tycos new_consts ctxt =
- let
- val ((tycos, consts), _) = Code_Antiq_Data.get ctxt;
- val tycos' = fold (insert (op =)) new_tycos tycos;
- val consts' = fold (insert (op =)) new_consts consts;
- val acc_code = Lazy.lazy (fn () =>
- evaluation_code (ProofContext.theory_of ctxt) "Code" tycos' consts');
- in Code_Antiq_Data.put ((tycos', consts'), (false, acc_code)) ctxt end;
-
-fun register_const const = register_code [] [const];
-
-fun register_datatype tyco constrs = register_code [tyco] constrs;
-
-fun print_const const all_struct_name tycos_map consts_map =
- (Long_Name.append all_struct_name o the o AList.lookup (op =) consts_map) const;
-
-fun print_code is_first print_it ctxt =
- let
- val (_, (_, acc_code)) = Code_Antiq_Data.get ctxt;
- val (ml_code, (tycos_map, consts_map)) = Lazy.force acc_code;
- val ml_code = if is_first then ml_code
- else "";
- val all_struct_name = "Isabelle";
- in (ml_code, print_it all_struct_name tycos_map consts_map) end;
-
-in
-
-fun ml_code_antiq raw_const background =
- let
- val const = Code.check_const (ProofContext.theory_of background) raw_const;
- val is_first = is_first_occ background;
- val background' = register_const const background;
- in (print_code is_first (print_const const), background') end;
-
-end; (*local*)
-
-
-(** reflection support **)
-
-fun check_datatype thy tyco consts =
- let
- val constrs = (map (fst o fst) o snd o Code.get_type thy) tyco;
- val missing_constrs = subtract (op =) consts constrs;
- val _ = if null missing_constrs then []
- else error ("Missing constructor(s) " ^ commas (map quote missing_constrs)
- ^ " for datatype " ^ quote tyco);
- val false_constrs = subtract (op =) constrs consts;
- val _ = if null false_constrs then []
- else error ("Non-constructor(s) " ^ commas (map quote false_constrs)
- ^ " for datatype " ^ quote tyco);
- in () end;
-
-fun add_eval_tyco (tyco, tyco') thy =
- let
- val k = Sign.arity_number thy tyco;
- fun pr pr' fxy [] = tyco'
- | pr pr' fxy [ty] =
- Code_Printer.concat [pr' Code_Printer.BR ty, tyco']
- | pr pr' fxy tys =
- Code_Printer.concat [Code_Printer.enum "," "(" ")" (map (pr' Code_Printer.BR) tys), tyco']
- in
- thy
- |> Code_Target.add_tyco_syntax target tyco (SOME (k, pr))
- end;
-
-fun add_eval_constr (const, const') thy =
- let
- val k = Code.args_number thy const;
- fun pr pr' fxy ts = Code_Printer.brackify fxy
- (const' :: the_list (Code_Printer.tuplify pr' Code_Printer.BR (map fst ts)));
- in
- thy
- |> Code_Target.add_const_syntax target const (SOME (Code_Printer.simple_const_syntax (k, pr)))
- end;
-
-fun add_eval_const (const, const') = Code_Target.add_const_syntax target
- const (SOME (Code_Printer.simple_const_syntax (0, (K o K o K) const')));
-
-fun process (code_body, (tyco_map, (constr_map, const_map))) module_name NONE thy =
- thy
- |> Code_Target.add_reserved target module_name
- |> Context.theory_map
- (ML_Context.exec (fn () => ML_Context.eval_text true Position.none code_body))
- |> fold (add_eval_tyco o apsnd Code_Printer.str) tyco_map
- |> fold (add_eval_constr o apsnd Code_Printer.str) constr_map
- |> fold (add_eval_const o apsnd Code_Printer.str) const_map
- | process (code_body, _) _ (SOME file_name) thy =
- let
- val preamble =
- "(* Generated from " ^ Path.implode (Thy_Header.thy_path (Context.theory_name thy))
- ^ "; DO NOT EDIT! *)";
- val _ = File.write (Path.explode file_name) (preamble ^ "\n\n" ^ code_body);
- in
- thy
- end;
-
-fun gen_code_reflect prep_type prep_const raw_datatypes raw_functions module_name some_file thy =
- let
- val datatypes = map (fn (raw_tyco, raw_cos) =>
- (prep_type thy raw_tyco, map (prep_const thy) raw_cos)) raw_datatypes;
- val _ = map (uncurry (check_datatype thy)) datatypes;
- val tycos = map fst datatypes;
- val constrs = maps snd datatypes;
- val functions = map (prep_const thy) raw_functions;
- val result = evaluation_code thy module_name tycos (constrs @ functions)
- |> (apsnd o apsnd) (chop (length constrs));
- in
- thy
- |> process result module_name some_file
- end;
-
-val code_reflect = gen_code_reflect Code_Target.cert_tyco Code.check_const;
-val code_reflect_cmd = gen_code_reflect Code_Target.read_tyco Code.read_const;
-
-
-(** Isar setup **)
-
-val _ = ML_Context.add_antiq "code" (fn _ => Args.term >> ml_code_antiq);
-
-local
-
-val datatypesK = "datatypes";
-val functionsK = "functions";
-val fileK = "file";
-val andK = "and"
-
-val _ = List.app Keyword.keyword [datatypesK, functionsK];
-
-val parse_datatype =
- Parse.name --| Parse.$$$ "=" -- (Parse.term ::: (Scan.repeat (Parse.$$$ "|" |-- Parse.term)));
-
-in
-
-val _ =
- Outer_Syntax.command "code_reflect" "enrich runtime environment with generated code"
- Keyword.thy_decl (Parse.name -- Scan.optional (Parse.$$$ datatypesK |-- (parse_datatype
- ::: Scan.repeat (Parse.$$$ andK |-- parse_datatype))) []
- -- Scan.optional (Parse.$$$ functionsK |-- Scan.repeat1 Parse.name) []
- -- Scan.option (Parse.$$$ fileK |-- Parse.name)
- >> (fn (((module_name, raw_datatypes), raw_functions), some_file) => Toplevel.theory
- (code_reflect_cmd raw_datatypes raw_functions module_name some_file)));
-
-end; (*local*)
-
-val setup = Code_Target.extend_target (target, (Code_ML.target_SML, K I));
-
-end; (*struct*)
--- a/src/Tools/Code/code_preproc.ML Wed Sep 15 16:23:11 2010 +0200
+++ b/src/Tools/Code/code_preproc.ML Wed Sep 15 17:05:18 2010 +0200
@@ -23,7 +23,7 @@
val sortargs: code_graph -> string -> sort list
val all: code_graph -> string list
val pretty: theory -> code_graph -> Pretty.T
- val obtain: theory -> string list -> term list -> code_algebra * code_graph
+ val obtain: bool -> theory -> string list -> term list -> code_algebra * code_graph
val dynamic_eval_conv: theory
-> (code_algebra -> code_graph -> (string * sort) list -> term -> conv) -> conv
val dynamic_eval_value: theory -> ((term -> term) -> 'a -> 'a)
@@ -422,8 +422,8 @@
(** retrieval and evaluation interfaces **)
-fun obtain thy consts ts = apsnd snd
- (Wellsorted.change_yield thy (extend_arities_eqngr thy consts ts));
+fun obtain ignore_cache thy consts ts = apsnd snd
+ (Wellsorted.change_yield (if ignore_cache then NONE else SOME thy) (extend_arities_eqngr thy consts ts));
fun dest_cterm ct = let val t = Thm.term_of ct in (Term.add_tfrees t [], t) end;
@@ -437,7 +437,7 @@
val (vs', t') = dest_cterm ct';
val consts = fold_aterms
(fn Const (c, _) => insert (op =) c | _ => I) t' [];
- val (algebra', eqngr') = obtain thy consts [t'];
+ val (algebra', eqngr') = obtain false thy consts [t'];
in conclude_evaluation (evaluator algebra' eqngr' vs' t' ct') thm end;
fun dynamic_eval_conv thy =
@@ -457,15 +457,12 @@
fun static_eval_conv thy consts conv =
let
- val (algebra, eqngr) = obtain thy consts [];
- fun conv' ct =
- let
- val (vs, t) = dest_cterm ct;
- in
- Conv.tap_thy (fn thy => (preprocess_conv thy)
- then_conv (conv algebra eqngr vs t) then_conv (postprocess_conv thy)) ct
- end;
- in conv' end;
+ val (algebra, eqngr) = obtain true thy consts [];
+ in
+ Conv.tap_thy (fn thy => (preprocess_conv thy)
+ then_conv (fn ct => uncurry (conv algebra eqngr) (dest_cterm ct) ct)
+ then_conv (postprocess_conv thy))
+ end;
(** setup **)
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/Code/code_runtime.ML Wed Sep 15 17:05:18 2010 +0200
@@ -0,0 +1,222 @@
+(* Title: Tools/Code/code_runtime.ML
+ Author: Florian Haftmann, TU Muenchen
+
+Runtime services building on code generation into implementation language SML.
+*)
+
+signature CODE_RUNTIME =
+sig
+ val target: string
+ val value: string option
+ -> (Proof.context -> unit -> 'a) * ((unit -> 'a) -> Proof.context -> Proof.context) * string
+ -> ((term -> term) -> 'a -> 'a) -> theory -> term -> string list -> 'a
+ val setup: theory -> theory
+end;
+
+structure Code_Runtime : CODE_RUNTIME =
+struct
+
+(** evaluation **)
+
+val target = "Eval";
+
+fun value some_target cookie postproc thy t args =
+ let
+ val ctxt = ProofContext.init_global thy;
+ fun evaluator naming program ((_, (_, ty)), t) deps =
+ let
+ val _ = if Code_Thingol.contains_dictvar t then
+ error "Term to be evaluated contains free dictionaries" else ();
+ val value_name = "Value.VALUE.value"
+ val program' = program
+ |> Graph.new_node (value_name,
+ Code_Thingol.Fun (Term.dummy_patternN, ((([], ty), [(([], t), (NONE, true))]), NONE)))
+ |> fold (curry Graph.add_edge value_name) deps;
+ val (program_code, [SOME value_name']) = Code_Target.produce_code_for thy
+ (the_default target some_target) NONE "Code" [] naming program' [value_name];
+ val value_code = space_implode " "
+ (value_name' :: map (enclose "(" ")") args);
+ in ML_Context.value ctxt cookie (program_code, value_code) end;
+ in Code_Thingol.dynamic_eval_value thy postproc evaluator t end;
+
+
+(** instrumentalization **)
+
+fun evaluation_code thy module_name tycos consts =
+ let
+ val (consts', (naming, program)) = Code_Thingol.consts_program thy false consts;
+ val tycos' = map (the o Code_Thingol.lookup_tyco naming) tycos;
+ val (ml_code, target_names) = Code_Target.produce_code_for thy
+ target NONE module_name [] naming program (consts' @ tycos');
+ val (consts'', tycos'') = chop (length consts') target_names;
+ val consts_map = map2 (fn const => fn NONE =>
+ error ("Constant " ^ (quote o Code.string_of_const thy) const
+ ^ "\nhas a user-defined serialization")
+ | SOME const'' => (const, const'')) consts consts''
+ val tycos_map = map2 (fn tyco => fn NONE =>
+ error ("Type " ^ (quote o Sign.extern_type thy) tyco
+ ^ "\nhas a user-defined serialization")
+ | SOME tyco'' => (tyco, tyco'')) tycos tycos'';
+ in (ml_code, (tycos_map, consts_map)) end;
+
+
+(* by antiquotation *)
+
+local
+
+structure Code_Antiq_Data = Proof_Data
+(
+ type T = (string list * string list) * (bool
+ * (string * ((string * string) list * (string * string) list)) lazy);
+ fun init _ = (([], []), (true, (Lazy.value ("", ([], [])))));
+);
+
+val is_first_occ = fst o snd o Code_Antiq_Data.get;
+
+fun register_code new_tycos new_consts ctxt =
+ let
+ val ((tycos, consts), _) = Code_Antiq_Data.get ctxt;
+ val tycos' = fold (insert (op =)) new_tycos tycos;
+ val consts' = fold (insert (op =)) new_consts consts;
+ val acc_code = Lazy.lazy (fn () =>
+ evaluation_code (ProofContext.theory_of ctxt) "Code" tycos' consts');
+ in Code_Antiq_Data.put ((tycos', consts'), (false, acc_code)) ctxt end;
+
+fun register_const const = register_code [] [const];
+
+fun register_datatype tyco constrs = register_code [tyco] constrs;
+
+fun print_const const all_struct_name tycos_map consts_map =
+ (Long_Name.append all_struct_name o the o AList.lookup (op =) consts_map) const;
+
+fun print_code is_first print_it ctxt =
+ let
+ val (_, (_, acc_code)) = Code_Antiq_Data.get ctxt;
+ val (ml_code, (tycos_map, consts_map)) = Lazy.force acc_code;
+ val ml_code = if is_first then ml_code
+ else "";
+ val all_struct_name = "Isabelle";
+ in (ml_code, print_it all_struct_name tycos_map consts_map) end;
+
+in
+
+fun ml_code_antiq raw_const background =
+ let
+ val const = Code.check_const (ProofContext.theory_of background) raw_const;
+ val is_first = is_first_occ background;
+ val background' = register_const const background;
+ in (print_code is_first (print_const const), background') end;
+
+end; (*local*)
+
+
+(* reflection support *)
+
+fun check_datatype thy tyco consts =
+ let
+ val constrs = (map (fst o fst) o snd o Code.get_type thy) tyco;
+ val missing_constrs = subtract (op =) consts constrs;
+ val _ = if null missing_constrs then []
+ else error ("Missing constructor(s) " ^ commas (map quote missing_constrs)
+ ^ " for datatype " ^ quote tyco);
+ val false_constrs = subtract (op =) constrs consts;
+ val _ = if null false_constrs then []
+ else error ("Non-constructor(s) " ^ commas (map quote false_constrs)
+ ^ " for datatype " ^ quote tyco);
+ in () end;
+
+fun add_eval_tyco (tyco, tyco') thy =
+ let
+ val k = Sign.arity_number thy tyco;
+ fun pr pr' fxy [] = tyco'
+ | pr pr' fxy [ty] =
+ Code_Printer.concat [pr' Code_Printer.BR ty, tyco']
+ | pr pr' fxy tys =
+ Code_Printer.concat [Code_Printer.enum "," "(" ")" (map (pr' Code_Printer.BR) tys), tyco']
+ in
+ thy
+ |> Code_Target.add_tyco_syntax target tyco (SOME (k, pr))
+ end;
+
+fun add_eval_constr (const, const') thy =
+ let
+ val k = Code.args_number thy const;
+ fun pr pr' fxy ts = Code_Printer.brackify fxy
+ (const' :: the_list (Code_Printer.tuplify pr' Code_Printer.BR (map fst ts)));
+ in
+ thy
+ |> Code_Target.add_const_syntax target const (SOME (Code_Printer.simple_const_syntax (k, pr)))
+ end;
+
+fun add_eval_const (const, const') = Code_Target.add_const_syntax target
+ const (SOME (Code_Printer.simple_const_syntax (0, (K o K o K) const')));
+
+fun process (code_body, (tyco_map, (constr_map, const_map))) module_name NONE thy =
+ thy
+ |> Code_Target.add_reserved target module_name
+ |> Context.theory_map
+ (ML_Context.exec (fn () => ML_Context.eval_text true Position.none code_body))
+ |> fold (add_eval_tyco o apsnd Code_Printer.str) tyco_map
+ |> fold (add_eval_constr o apsnd Code_Printer.str) constr_map
+ |> fold (add_eval_const o apsnd Code_Printer.str) const_map
+ | process (code_body, _) _ (SOME file_name) thy =
+ let
+ val preamble =
+ "(* Generated from " ^ Path.implode (Thy_Header.thy_path (Context.theory_name thy))
+ ^ "; DO NOT EDIT! *)";
+ val _ = File.write (Path.explode file_name) (preamble ^ "\n\n" ^ code_body);
+ in
+ thy
+ end;
+
+fun gen_code_reflect prep_type prep_const raw_datatypes raw_functions module_name some_file thy =
+ let
+ val datatypes = map (fn (raw_tyco, raw_cos) =>
+ (prep_type thy raw_tyco, map (prep_const thy) raw_cos)) raw_datatypes;
+ val _ = map (uncurry (check_datatype thy)) datatypes;
+ val tycos = map fst datatypes;
+ val constrs = maps snd datatypes;
+ val functions = map (prep_const thy) raw_functions;
+ val result = evaluation_code thy module_name tycos (constrs @ functions)
+ |> (apsnd o apsnd) (chop (length constrs));
+ in
+ thy
+ |> process result module_name some_file
+ end;
+
+val code_reflect = gen_code_reflect Code_Target.cert_tyco Code.check_const;
+val code_reflect_cmd = gen_code_reflect Code_Target.read_tyco Code.read_const;
+
+
+(** Isar setup **)
+
+val _ = ML_Context.add_antiq "code" (fn _ => Args.term >> ml_code_antiq);
+
+local
+
+val datatypesK = "datatypes";
+val functionsK = "functions";
+val fileK = "file";
+val andK = "and"
+
+val _ = List.app Keyword.keyword [datatypesK, functionsK];
+
+val parse_datatype =
+ Parse.name --| Parse.$$$ "=" -- (Parse.term ::: (Scan.repeat (Parse.$$$ "|" |-- Parse.term)));
+
+in
+
+val _ =
+ Outer_Syntax.command "code_reflect" "enrich runtime environment with generated code"
+ Keyword.thy_decl (Parse.name -- Scan.optional (Parse.$$$ datatypesK |-- (parse_datatype
+ ::: Scan.repeat (Parse.$$$ andK |-- parse_datatype))) []
+ -- Scan.optional (Parse.$$$ functionsK |-- Scan.repeat1 Parse.name) []
+ -- Scan.option (Parse.$$$ fileK |-- Parse.name)
+ >> (fn (((module_name, raw_datatypes), raw_functions), some_file) => Toplevel.theory
+ (code_reflect_cmd raw_datatypes raw_functions module_name some_file)));
+
+end; (*local*)
+
+val setup = Code_Target.extend_target (target, (Code_ML.target_SML, K I));
+
+end; (*struct*)
--- a/src/Tools/Code/code_thingol.ML Wed Sep 15 16:23:11 2010 +0200
+++ b/src/Tools/Code/code_thingol.ML Wed Sep 15 17:05:18 2010 +0200
@@ -832,15 +832,11 @@
val empty = (empty_naming, Graph.empty);
);
-fun cache_generation thy (algebra, eqngr) f name =
- Program.change_yield thy (fn naming_program => (NONE, naming_program)
- |> f thy algebra eqngr name
- |-> (fn name => fn (_, naming_program) => (name, naming_program)));
-
-fun transient_generation thy (algebra, eqngr) f name =
- (NONE, (empty_naming, Graph.empty))
- |> f thy algebra eqngr name
- |-> (fn name => fn (_, naming_program) => (name, naming_program));
+fun invoke_generation ignore_cache thy (algebra, eqngr) f name =
+ Program.change_yield (if ignore_cache then NONE else SOME thy)
+ (fn naming_program => (NONE, naming_program)
+ |> f thy algebra eqngr name
+ |-> (fn name => fn (_, naming_program) => (name, naming_program)));
(* program generation *)
@@ -853,10 +849,9 @@
in (cs, (naming, Graph.subgraph (member (op =) cs_all) program)) end;
fun generate_consts thy algebra eqngr =
fold_map (ensure_const thy algebra eqngr permissive);
- val invoke_generation = if permissive
- then transient_generation else cache_generation
in
- invoke_generation thy (Code_Preproc.obtain thy cs []) generate_consts cs
+ invoke_generation (not permissive) thy (Code_Preproc.obtain false thy cs [])
+ generate_consts cs
|-> project_consts
end;
@@ -892,7 +887,7 @@
fun base_evaluator thy evaluator algebra eqngr vs t =
let
val (((naming, program), (((vs', ty'), t'), deps)), _) =
- cache_generation thy (algebra, eqngr) ensure_value t;
+ invoke_generation false thy (algebra, eqngr) ensure_value t;
val vs'' = map (fn (v, _) => (v, (the o AList.lookup (op =) vs o prefix "'") v)) vs';
in evaluator naming program ((vs'', (vs', ty')), t') deps end;
@@ -926,7 +921,7 @@
fun code_depgr thy consts =
let
- val (_, eqngr) = Code_Preproc.obtain thy consts [];
+ val (_, eqngr) = Code_Preproc.obtain true thy consts [];
val all_consts = Graph.all_succs eqngr consts;
in Graph.subgraph (member (op =) all_consts) eqngr end;
--- a/src/Tools/Code_Generator.thy Wed Sep 15 16:23:11 2010 +0200
+++ b/src/Tools/Code_Generator.thy Wed Sep 15 17:05:18 2010 +0200
@@ -21,7 +21,7 @@
"~~/src/Tools/Code/code_ml.ML"
"~~/src/Tools/Code/code_haskell.ML"
"~~/src/Tools/Code/code_scala.ML"
- "~~/src/Tools/Code/code_eval.ML"
+ "~~/src/Tools/Code/code_runtime.ML"
"~~/src/Tools/nbe.ML"
begin
@@ -32,7 +32,7 @@
#> Code_ML.setup
#> Code_Haskell.setup
#> Code_Scala.setup
- #> Code_Eval.setup
+ #> Code_Runtime.setup
#> Nbe.setup
#> Quickcheck.setup
*}
--- a/src/Tools/nbe.ML Wed Sep 15 16:23:11 2010 +0200
+++ b/src/Tools/nbe.ML Wed Sep 15 17:05:18 2010 +0200
@@ -8,6 +8,7 @@
sig
val dynamic_eval_conv: conv
val dynamic_eval_value: theory -> term -> term
+ val static_eval_conv: theory -> string list -> conv
datatype Univ =
Const of int * Univ list (*named (uninterpreted) constants*)
@@ -19,7 +20,7 @@
(*abstractions as closures*)
val same: Univ -> Univ -> bool
- val univs_ref: (unit -> Univ list -> Univ list) option Unsynchronized.ref
+ val put_result: (unit -> Univ list -> Univ list) -> Proof.context -> Proof.context
val trace: bool Unsynchronized.ref
val setup: theory -> theory
@@ -228,10 +229,15 @@
(* nbe specific syntax and sandbox communication *)
-val univs_ref = Unsynchronized.ref (NONE : (unit -> Univ list -> Univ list) option);
+structure Univs = Proof_Data (
+ type T = unit -> Univ list -> Univ list
+ fun init _ () = error "Univs"
+);
+val put_result = Univs.put;
local
val prefix = "Nbe.";
+ val name_put = prefix ^ "put_result";
val name_ref = prefix ^ "univs_ref";
val name_const = prefix ^ "Const";
val name_abss = prefix ^ "abss";
@@ -239,7 +245,7 @@
val name_same = prefix ^ "same";
in
-val univs_cookie = (name_ref, univs_ref);
+val univs_cookie = (Univs.get, put_result, name_put);
fun nbe_fun 0 "" = "nbe_value"
| nbe_fun i c = "c_" ^ translate_string (fn "." => "_" | c => c) c ^ "_" ^ string_of_int i;
@@ -372,15 +378,16 @@
in ml_abs deps_vars (ml_Let (ml_fundefs (flat fun_vars)) (ml_list fun_vals)) end;
-(* code compilation *)
+(* compile equations *)
-fun compile_eqnss ctxt gr raw_deps [] = []
- | compile_eqnss ctxt gr raw_deps eqnss =
+fun compile_eqnss thy nbe_program raw_deps [] = []
+ | compile_eqnss thy nbe_program raw_deps eqnss =
let
+ val ctxt = ProofContext.init_global thy;
val (deps, deps_vals) = split_list (map_filter
- (fn dep => Option.map (fn univ => (dep, univ)) (fst ((Graph.get_node gr dep)))) raw_deps);
+ (fn dep => Option.map (fn univ => (dep, univ)) (fst ((Graph.get_node nbe_program dep)))) raw_deps);
val idx_of = raw_deps
- |> map (fn dep => (dep, snd (Graph.get_node gr dep)))
+ |> map (fn dep => (dep, snd (Graph.get_node nbe_program dep)))
|> AList.lookup (op =)
|> (fn f => the o f);
val s = assemble_eqnss idx_of deps eqnss;
@@ -389,13 +396,13 @@
s
|> traced (fn s => "\n--- code to be evaluated:\n" ^ s)
|> pair ""
- |> ML_Context.evaluate ctxt (!trace) univs_cookie
+ |> ML_Context.value ctxt univs_cookie
|> (fn f => f deps_vals)
|> (fn univs => cs ~~ univs)
end;
-(* preparing function equations *)
+(* extract equations from statements *)
fun eqns_of_stmt (_, Code_Thingol.Fun (_, ((_, []), _))) =
[]
@@ -423,7 +430,16 @@
map (fn (_, (_, (inst, dss))) => IConst (inst, (([], dss), []))) super_instances
@ map (IConst o snd o fst) classparam_instances)]))];
-fun compile_stmts ctxt stmts_deps =
+
+(* compile whole programs *)
+
+fun ensure_const_idx name (nbe_program, (maxidx, idx_tab)) =
+ if can (Graph.get_node nbe_program) name
+ then (nbe_program, (maxidx, idx_tab))
+ else (Graph.new_node (name, (NONE, maxidx)) nbe_program,
+ (maxidx + 1, Inttab.update_new (maxidx, name) idx_tab));
+
+fun compile_stmts thy stmts_deps =
let
val names = map (fst o fst) stmts_deps;
val names_deps = map (fn ((name, _), deps) => (name, deps)) stmts_deps;
@@ -432,26 +448,22 @@
|> maps snd
|> distinct (op =)
|> fold (insert (op =)) names;
- fun new_node name (gr, (maxidx, idx_tab)) = if can (Graph.get_node gr) name
- then (gr, (maxidx, idx_tab))
- else (Graph.new_node (name, (NONE, maxidx)) gr,
- (maxidx + 1, Inttab.update_new (maxidx, name) idx_tab));
- fun compile gr = eqnss
- |> compile_eqnss ctxt gr refl_deps
- |> rpair gr;
+ fun compile nbe_program = eqnss
+ |> compile_eqnss thy nbe_program refl_deps
+ |> rpair nbe_program;
in
- fold new_node refl_deps
+ fold ensure_const_idx refl_deps
#> apfst (fold (fn (name, deps) => fold (curry Graph.add_edge name) deps) names_deps
#> compile
#-> fold (fn (name, univ) => (Graph.map_node name o apfst) (K (SOME univ))))
end;
-fun ensure_stmts ctxt program =
+fun compile_program thy program =
let
- fun add_stmts names (gr, (maxidx, idx_tab)) = if exists ((can o Graph.get_node) gr) names
- then (gr, (maxidx, idx_tab))
- else (gr, (maxidx, idx_tab))
- |> compile_stmts ctxt (map (fn name => ((name, Graph.get_node program name),
+ fun add_stmts names (nbe_program, (maxidx, idx_tab)) = if exists ((can o Graph.get_node) nbe_program) names
+ then (nbe_program, (maxidx, idx_tab))
+ else (nbe_program, (maxidx, idx_tab))
+ |> compile_stmts thy (map (fn name => ((name, Graph.get_node program name),
Graph.imm_succs program name)) names);
in
fold_rev add_stmts (Graph.strong_conn program)
@@ -460,20 +472,20 @@
(** evaluation **)
-(* term evaluation *)
+(* term evaluation by compilation *)
-fun eval_term ctxt gr deps (vs : (string * sort) list, t) =
+fun compile_term thy nbe_program deps (vs : (string * sort) list, t) =
let
val dict_frees = maps (fn (v, sort) => map_index (curry DFree v o fst) sort) vs;
in
("", (vs, [([], t)]))
- |> singleton (compile_eqnss ctxt gr deps)
+ |> singleton (compile_eqnss thy nbe_program deps)
|> snd
|> (fn t => apps t (rev dict_frees))
end;
-(* reification *)
+(* reconstruction *)
fun typ_of_itype program vs (ityco `%% itys) =
let
@@ -520,6 +532,29 @@
in of_univ 0 t 0 |> fst end;
+(* evaluation with type reconstruction *)
+
+fun eval_term thy program (nbe_program, idx_tab) ((vs0, (vs, ty)), t) deps =
+ let
+ val ctxt = Syntax.init_pretty_global thy;
+ val string_of_term = Syntax.string_of_term (Config.put show_types true ctxt);
+ val ty' = typ_of_itype program vs0 ty;
+ fun type_infer t = singleton
+ (Type_Infer.infer_types ctxt (try (Type.strip_sorts o Sign.the_const_type thy)) (K NONE))
+ (Type.constraint ty' t);
+ fun check_tvars t =
+ if null (Term.add_tvars t []) then t
+ else error ("Illegal schematic type variables in normalized term: " ^ string_of_term t);
+ in
+ compile_term thy nbe_program deps (vs, t)
+ |> term_of_univ thy program idx_tab
+ |> traced (fn t => "Normalized:\n" ^ string_of_term t)
+ |> type_infer
+ |> traced (fn t => "Types inferred:\n" ^ string_of_term t)
+ |> check_tvars
+ |> traced (fn _ => "---\n")
+ end;
+
(* function store *)
structure Nbe_Functions = Code_Data
@@ -528,46 +563,15 @@
val empty = (Graph.empty, (0, Inttab.empty));
);
-
-(* compilation, evaluation and reification *)
-
-fun compile_eval thy program =
+fun compile ignore_cache thy program =
let
- val ctxt = ProofContext.init_global thy;
- val (gr, (_, idx_tab)) =
- Nbe_Functions.change thy (ensure_stmts ctxt program);
- in fn vs_t => fn deps =>
- vs_t
- |> eval_term ctxt gr deps
- |> term_of_univ thy program idx_tab
- end;
+ val (nbe_program, (_, idx_tab)) =
+ Nbe_Functions.change (if ignore_cache then NONE else SOME thy)
+ (compile_program thy program);
+ in (nbe_program, idx_tab) end;
-(* evaluation with type reconstruction *)
-
-fun normalize thy program ((vs0, (vs, ty)), t) deps =
- let
- val ctxt = Syntax.init_pretty_global thy;
- val ty' = typ_of_itype program vs0 ty;
- fun type_infer t =
- singleton
- (Type_Infer.infer_types ctxt (try (Type.strip_sorts o Sign.the_const_type thy)) (K NONE))
- (Type.constraint ty' t);
- val string_of_term = Syntax.string_of_term (Config.put show_types true ctxt);
- fun check_tvars t =
- if null (Term.add_tvars t []) then t
- else error ("Illegal schematic type variables in normalized term: " ^ string_of_term t);
- in
- compile_eval thy program (vs, t) deps
- |> traced (fn t => "Normalized:\n" ^ string_of_term t)
- |> type_infer
- |> traced (fn t => "Types inferred:\n" ^ string_of_term t)
- |> check_tvars
- |> traced (fn _ => "---\n")
- end;
-
-
-(* evaluation oracle *)
+(* dynamic evaluation oracle *)
fun mk_equals thy lhs raw_rhs =
let
@@ -577,10 +581,12 @@
in Thm.mk_binop eq lhs rhs end;
val (_, raw_oracle) = Context.>>> (Context.map_theory_result
- (Thm.add_oracle (Binding.name "norm", fn (thy, program, vsp_ty_t, deps, ct) =>
- mk_equals thy ct (normalize thy program vsp_ty_t deps))));
+ (Thm.add_oracle (Binding.name "normalization_by_evaluation",
+ fn (thy, program, nbe_program_idx_tab, vsp_ty_t, deps, ct) =>
+ mk_equals thy ct (eval_term thy program nbe_program_idx_tab vsp_ty_t deps))));
-fun oracle thy program vsp_ty_t deps ct = raw_oracle (thy, program, vsp_ty_t, deps, ct);
+fun oracle thy program nbe_program_idx_tab vsp_ty_t deps ct =
+ raw_oracle (thy, program, nbe_program_idx_tab, vsp_ty_t, deps, ct);
fun no_frees_rew rew t =
let
@@ -592,41 +598,22 @@
|> curry (Term.betapplys o swap) frees
end;
-val dynamic_eval_conv = Code_Simp.no_frees_conv (Conv.tap_thy
- (fn thy => lift_triv_classes_conv thy (Code_Thingol.dynamic_eval_conv thy (K (oracle thy)))));
+val dynamic_eval_conv = Conv.tap_thy (fn thy => Code_Simp.no_frees_conv
+ (lift_triv_classes_conv thy (Code_Thingol.dynamic_eval_conv thy
+ (K (fn program => oracle thy program (compile false thy program))))));
fun dynamic_eval_value thy = lift_triv_classes_rew thy
- (no_frees_rew (Code_Thingol.dynamic_eval_value thy I (K (normalize thy))));
+ (no_frees_rew (Code_Thingol.dynamic_eval_value thy I
+ (K (fn program => eval_term thy program (compile false thy program)))));
+
+fun static_eval_conv thy consts = Code_Simp.no_frees_conv
+ (lift_triv_classes_conv thy (Code_Thingol.static_eval_conv thy consts
+ (K (fn program => oracle thy program (compile true thy program)))));
-(* evaluation command *)
-
-fun norm_print_term ctxt modes t =
- let
- val thy = ProofContext.theory_of ctxt;
- val t' = dynamic_eval_value thy t;
- val ty' = Term.type_of t';
- val ctxt' = Variable.auto_fixes t ctxt;
- val p = Print_Mode.with_modes modes (fn () =>
- Pretty.block [Pretty.quote (Syntax.pretty_term ctxt' t'), Pretty.fbrk,
- Pretty.str "::", Pretty.brk 1, Pretty.quote (Syntax.pretty_typ ctxt' ty')]) ();
- in Pretty.writeln p end;
-
-
-(** Isar setup **)
-
-fun norm_print_term_cmd (modes, s) state =
- let val ctxt = Toplevel.context_of state
- in norm_print_term ctxt modes (Syntax.read_term ctxt s) end;
+(** setup **)
val setup = Value.add_evaluator ("nbe", dynamic_eval_value o ProofContext.theory_of);
-val opt_modes =
- Scan.optional (Parse.$$$ "(" |-- Parse.!!! (Scan.repeat1 Parse.xname --| Parse.$$$ ")")) [];
-
-val _ =
- Outer_Syntax.improper_command "normal_form" "normalize term by evaluation" Keyword.diag
- (opt_modes -- Parse.term >> (Toplevel.keep o norm_print_term_cmd));
-
end;
\ No newline at end of file