--- a/NEWS Wed Jul 02 07:11:57 2008 +0200
+++ b/NEWS Wed Jul 02 07:12:17 2008 +0200
@@ -15,8 +15,20 @@
* Keyword 'code_exception' now named 'code_abort'. INCOMPATIBILITY.
+* New ML antiquotation 'code': takes constant as argument, generates
+corresponding code in background and inserts name of the corresponding resulting
+ML value/function/datatype constructor binding in place. All occurences of 'code'
+with a single ML block are generated simultaneously.
+Provides a generic and safe interface for instrumentalizing code generation.
+See HOL/ex/Code_Antiq for a toy example, or HOL/Complex/ex/ReflectedFerrack
+for a more ambitious application. In future you ought refrain from
+ad-hoc compiling generated SML code on the ML toplevel.
+Note that (for technical reasons) 'code' cannot refer to constants for which
+user-defined serializations are set. Refer to the corresponding ML counterpart
+directly in that cases.
+
* Removed exotic 'token_translation' command. INCOMPATIBILITY, use ML
-interface instead.
+interface instead.
*** Document preparation ***
@@ -32,7 +44,10 @@
Complex_Main.thy remain as they are.
* New image HOL-Plain provides a minimal HOL with the most important tools
-available (inductive, datatype, primrec, codegen, ...).
+available (inductive, datatype, primrec, ...). By convention the corresponding
+theory Plain should be ancestor of every further (library) theory. Some library
+theories now have ancestor Plain (instead of Main), thus theory Main
+occasionally has to be imported explicitly.
* Methods "case_tac" and "induct_tac" now refer to the very same rules
as the structured Isar versions "cases" and "induct", cf. the
@@ -66,7 +81,7 @@
*** ML ***
-
+
* Rules and tactics that read instantiations (read_instantiate,
res_inst_tac, thin_tac, subgoal_tac etc.) now demand a proper proof
context, which is required for parsing and type-checking. Moreover,
--- a/src/HOL/Complex/ex/ReflectedFerrack.thy Wed Jul 02 07:11:57 2008 +0200
+++ b/src/HOL/Complex/ex/ReflectedFerrack.thy Wed Jul 02 07:12:17 2008 +0200
@@ -6,7 +6,7 @@
theory ReflectedFerrack
imports Main GCD Real Efficient_Nat
-uses ("linreif.ML") ("linrtac.ML")
+uses ("linrtac.ML")
begin
@@ -1985,30 +1985,97 @@
with lr show ?thesis by blast
qed
-constdefs linrqe:: "fm \<Rightarrow> fm"
- "linrqe \<equiv> (\<lambda> p. qelim (prep p) ferrack)"
+definition linrqe:: "fm \<Rightarrow> fm" where
+ "linrqe p = qelim (prep p) ferrack"
-theorem linrqe: "(Ifm bs (linrqe p) = Ifm bs p) \<and> qfree (linrqe p)"
+theorem linrqe: "Ifm bs (linrqe p) = Ifm bs p \<and> qfree (linrqe p)"
using ferrack qelim_ci prep
unfolding linrqe_def by auto
-definition
- ferrack_test :: "unit \<Rightarrow> fm"
-where
+definition ferrack_test :: "unit \<Rightarrow> fm" where
"ferrack_test u = linrqe (A (A (Imp (Lt (Sub (Bound 1) (Bound 0)))
(E (Eq (Sub (Add (Bound 0) (Bound 2)) (Bound 1)))))))"
-export_code linrqe ferrack_test in SML module_name Ferrack
+ML {* @{code ferrack_test} () *}
+
+oracle linr_oracle ("term") = {*
+
+let
+
+fun num_of_term vs (t as Free (xn, xT)) = (case AList.lookup (op =) vs t
+ of NONE => error "Variable not found in the list!"
+ | SOME n => @{code Bound} n)
+ | num_of_term vs @{term "real (0::int)"} = @{code C} 0
+ | num_of_term vs @{term "real (1::int)"} = @{code C} 1
+ | num_of_term vs @{term "0::real"} = @{code C} 0
+ | num_of_term vs @{term "1::real"} = @{code C} 1
+ | num_of_term vs (Term.Bound i) = @{code Bound} i
+ | num_of_term vs (@{term "uminus :: real \<Rightarrow> real"} $ t') = @{code Neg} (num_of_term vs t')
+ | num_of_term vs (@{term "op + :: real \<Rightarrow> real \<Rightarrow> real"} $ t1 $ t2) = @{code Add} (num_of_term vs t1, num_of_term vs t2)
+ | num_of_term vs (@{term "op - :: real \<Rightarrow> real \<Rightarrow> real"} $ t1 $ t2) = @{code Sub} (num_of_term vs t1, num_of_term vs t2)
+ | num_of_term vs (@{term "op * :: real \<Rightarrow> real \<Rightarrow> real"} $ t1 $ t2) = (case (num_of_term vs t1)
+ of @{code C} i => @{code Mul} (i, num_of_term vs t2)
+ | _ => error "num_of_term: unsupported Multiplication")
+ | num_of_term vs (@{term "real :: int \<Rightarrow> real"} $ (@{term "number_of :: int \<Rightarrow> int"} $ t')) = @{code C} (HOLogic.dest_numeral t')
+ | num_of_term vs (@{term "number_of :: int \<Rightarrow> int"} $ t') = @{code C} (HOLogic.dest_numeral t')
+ | num_of_term vs t = error ("num_of_term: unknown term " ^ Syntax.string_of_term_global @{theory} t);
+
+fun fm_of_term vs @{term True} = @{code T}
+ | fm_of_term vs @{term False} = @{code T}
+ | fm_of_term vs (@{term "op < :: real \<Rightarrow> real \<Rightarrow> bool"} $ t1 $ t2) = @{code Lt} (@{code Sub} (num_of_term vs t1, num_of_term vs t2))
+ | fm_of_term vs (@{term "op \<le> :: real \<Rightarrow> real \<Rightarrow> bool"} $ t1 $ t2) = @{code Le} (@{code Sub} (num_of_term vs t1, num_of_term vs t2))
+ | fm_of_term vs (@{term "op = :: real \<Rightarrow> real \<Rightarrow> bool"} $ t1 $ t2) = @{code Eq} (@{code Sub} (num_of_term vs t1, num_of_term vs t2))
+ | fm_of_term vs (@{term "op = :: bool \<Rightarrow> bool \<Rightarrow> bool"} $ t1 $ t2) = @{code Iff} (fm_of_term vs t1, fm_of_term vs t2)
+ | fm_of_term vs (@{term "op &"} $ t1 $ t2) = @{code And} (fm_of_term vs t1, fm_of_term vs t2)
+ | fm_of_term vs (@{term "op |"} $ t1 $ t2) = @{code Or} (fm_of_term vs t1, fm_of_term vs t2)
+ | fm_of_term vs (@{term "op -->"} $ t1 $ t2) = @{code Imp} (fm_of_term vs t1, fm_of_term vs t2)
+ | fm_of_term vs (@{term "Not"} $ t') = @{code NOT} (fm_of_term vs t')
+ | fm_of_term vs (Const("Ex", _) $ Term.Abs (xn, xT, p)) =
+ @{code E} (fm_of_term (map (fn (v, n) => (v, n + 1)) vs) p)
+ | fm_of_term vs (Const("All", _) $ Term.Abs(xn, xT, p)) =
+ @{code A} (fm_of_term (map (fn (v, n) => (v, n + 1)) vs) p)
+ | fm_of_term vs t = error ("fm_of_term : unknown term " ^ Syntax.string_of_term_global @{theory} t);
-(*code_module Ferrack
- contains
- linrqe = linrqe
- test = ferrack_test*)
+fun term_of_num vs (@{code C} i) = @{term "real :: int \<Rightarrow> real"} $ HOLogic.mk_number HOLogic.intT i
+ | term_of_num vs (@{code Bound} n) = fst (the (find_first (fn (_, m) => n = m) vs))
+ | term_of_num vs (@{code Neg} t') = @{term "uminus :: real \<Rightarrow> real"} $ term_of_num vs t'
+ | term_of_num vs (@{code Add} (t1, t2)) = @{term "op + :: real \<Rightarrow> real \<Rightarrow> real"} $
+ term_of_num vs t1 $ term_of_num vs t2
+ | term_of_num vs (@{code Sub} (t1, t2)) = @{term "op - :: real \<Rightarrow> real \<Rightarrow> real"} $
+ term_of_num vs t1 $ term_of_num vs t2
+ | term_of_num vs (@{code Mul} (i, t2)) = @{term "op * :: real \<Rightarrow> real \<Rightarrow> real"} $
+ term_of_num vs (@{code C} i) $ term_of_num vs t2
+ | term_of_num vs (@{code CN} (n, i, t)) = term_of_num vs (@{code Add} (@{code Mul} (i, @{code Bound} n), t));
-ML {* Ferrack.ferrack_test () *}
+fun term_of_fm vs @{code T} = HOLogic.true_const
+ | term_of_fm vs @{code F} = HOLogic.false_const
+ | term_of_fm vs (@{code Lt} t) = @{term "op < :: real \<Rightarrow> real \<Rightarrow> bool"} $
+ term_of_num vs t $ @{term "0::real"}
+ | term_of_fm vs (@{code Le} t) = @{term "op \<le> :: real \<Rightarrow> real \<Rightarrow> bool"} $
+ term_of_num vs t $ @{term "0::real"}
+ | term_of_fm vs (@{code Gt} t) = @{term "op < :: real \<Rightarrow> real \<Rightarrow> bool"} $
+ @{term "0::real"} $ term_of_num vs t
+ | term_of_fm vs (@{code Ge} t) = @{term "op \<le> :: real \<Rightarrow> real \<Rightarrow> bool"} $
+ @{term "0::real"} $ term_of_num vs t
+ | term_of_fm vs (@{code Eq} t) = @{term "op = :: real \<Rightarrow> real \<Rightarrow> bool"} $
+ term_of_num vs t $ @{term "0::real"}
+ | term_of_fm vs (@{code NEq} t) = term_of_fm vs (@{code NOT} (@{code Eq} t))
+ | term_of_fm vs (@{code NOT} t') = HOLogic.Not $ term_of_fm vs t'
+ | term_of_fm vs (@{code And} (t1, t2)) = HOLogic.conj $ term_of_fm vs t1 $ term_of_fm vs t2
+ | term_of_fm vs (@{code Or} (t1, t2)) = HOLogic.disj $ term_of_fm vs t1 $ term_of_fm vs t2
+ | term_of_fm vs (@{code Imp} (t1, t2)) = HOLogic.imp $ term_of_fm vs t1 $ term_of_fm vs t2
+ | term_of_fm vs (@{code Iff} (t1, t2)) = @{term "op = :: bool \<Rightarrow> bool \<Rightarrow> bool"} $
+ term_of_fm vs t1 $ term_of_fm vs t2
+ | term_of_fm vs _ = error "If this is raised, Isabelle/HOL or generate_code is inconsistent.";
-use "linreif.ML"
-oracle linr_oracle ("term") = ReflectedFerrack.linrqe_oracle
+in fn thy => fn t =>
+ let
+ val fs = term_frees t;
+ val vs = fs ~~ (0 upto (length fs - 1));
+ in HOLogic.mk_Trueprop (HOLogic.mk_eq (t, term_of_fm vs (@{code linrqe} (fm_of_term vs t)))) end
+end;
+*}
+
use "linrtac.ML"
setup LinrTac.setup
--- a/src/HOL/Complex/ex/linreif.ML Wed Jul 02 07:11:57 2008 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,118 +0,0 @@
-(* ID: $Id$
- Author: Amine Chaieb, TU Muenchen
-
-The oracle for Mixed Real-Integer auantifier elimination
-based on the verified Code in ~/work/MIR/MIR.thy.
-*)
-
-structure ReflectedFerrack =
-struct
-
-open Ferrack;
-
-exception LINR;
-
-(* pseudo reification : term -> intterm *)
-val rT = Type ("RealDef.real",[]);
-val bT = HOLogic.boolT;
-val realC = @{term "RealDef.real :: int => real"};
-val rzero = @{term "0 :: real"};
-
-fun num_of_term vs t = case t
- of Free(xn,xT) => (case AList.lookup (op =) vs t of
- NONE => error "Variable not found in the list!"
- | SOME n => Bound n)
- | Const("RealDef.real",_)$ @{term "0::int"} => C 0
- | Const("RealDef.real",_)$ @{term "1::int"} => C 1
- | @{term "0::real"} => C 0
- | @{term "0::real"} => C 1
- | Term.Bound i => Bound i
- | Const (@{const_name "HOL.uminus"},_)$t' => Neg (num_of_term vs t')
- | Const (@{const_name "HOL.plus"},_)$t1$t2 => Add (num_of_term vs t1,num_of_term vs t2)
- | Const (@{const_name "HOL.minus"},_)$t1$t2 => Sub (num_of_term vs t1,num_of_term vs t2)
- | Const (@{const_name "HOL.times"},_)$t1$t2 => (case (num_of_term vs t1) of C i =>
- Mul (i,num_of_term vs t2)
- | _ => error "num_of_term: unsupported Multiplication")
- | Const("RealDef.real",_) $ Const (@{const_name "Int.number_of"},_)$t' => C (HOLogic.dest_numeral t')
- | Const (@{const_name "Int.number_of"},_)$t' => C (HOLogic.dest_numeral t')
- | _ => error ("num_of_term: unknown term " ^ Syntax.string_of_term_global Pure.thy t);
-
-(* pseudo reification : term -> fm *)
-fun fm_of_term vs t =
- case t of
- Const("True",_) => T
- | Const("False",_) => F
- | Const(@{const_name HOL.less},_)$t1$t2 => Lt (Sub (num_of_term vs t1,num_of_term vs t2))
- | Const(@{const_name HOL.less_eq},_)$t1$t2 => Le (Sub (num_of_term vs t1,num_of_term vs t2))
- | Const("op =",eqT)$t1$t2 =>
- if (domain_type eqT = rT)
- then Eq (Sub (num_of_term vs t1,num_of_term vs t2))
- else Iff(fm_of_term vs t1,fm_of_term vs t2)
- | Const("op &",_)$t1$t2 => And(fm_of_term vs t1,fm_of_term vs t2)
- | Const("op |",_)$t1$t2 => Or(fm_of_term vs t1,fm_of_term vs t2)
- | Const("op -->",_)$t1$t2 => Imp(fm_of_term vs t1,fm_of_term vs t2)
- | Const("Not",_)$t' => Not(fm_of_term vs t')
- | Const("Ex",_)$Term.Abs(xn,xT,p) =>
- E(fm_of_term (map (fn(v,n) => (v,1+ n)) vs) p)
- | Const("All",_)$Term.Abs(xn,xT,p) =>
- A(fm_of_term (map (fn(v,n) => (v,1+ n)) vs) p)
- | _ => error ("fm_of_term : unknown term!" ^ Syntax.string_of_term_global Pure.thy t);
-
-
-fun start_vs t =
- let
- val fs = term_frees t
- in fs ~~ (0 upto (length fs - 1)) end;
-
-(* transform num and fm back to terms *)
-
-fun myassoc2 l v =
- case l of
- [] => NONE
- | (x,v')::xs => if v = v' then SOME x
- else myassoc2 xs v;
-
-fun term_of_num vs t =
- case t of
- C i => realC $ (HOLogic.mk_number HOLogic.intT i)
- | Bound n => the (myassoc2 vs n)
- | Neg t' => Const(@{const_name HOL.uminus},rT --> rT)$(term_of_num vs t')
- | Add(t1,t2) => Const(@{const_name HOL.plus},[rT,rT] ---> rT)$
- (term_of_num vs t1)$(term_of_num vs t2)
- | Sub(t1,t2) => Const(@{const_name HOL.minus},[rT,rT] ---> rT)$
- (term_of_num vs t1)$(term_of_num vs t2)
- | Mul(i,t2) => Const(@{const_name HOL.times},[rT,rT] ---> rT)$
- (term_of_num vs (C i))$(term_of_num vs t2)
- | Cn(n,i,t) => term_of_num vs (Add (Mul(i,Bound n),t));
-
-fun term_of_fm vs t =
- case t of
- T => HOLogic.true_const
- | F => HOLogic.false_const
- | Lt t => Const(@{const_name HOL.less},[rT,rT] ---> bT)$
- (term_of_num vs t)$ rzero
- | Le t => Const(@{const_name HOL.less_eq},[rT,rT] ---> bT)$
- (term_of_num vs t)$ rzero
- | Gt t => Const(@{const_name HOL.less},[rT,rT] ---> bT)$
- rzero $(term_of_num vs t)
- | Ge t => Const(@{const_name HOL.less_eq},[rT,rT] ---> bT)$
- rzero $(term_of_num vs t)
- | Eq t => Const("op =",[rT,rT] ---> bT)$
- (term_of_num vs t)$ rzero
- | NEq t => term_of_fm vs (Not (Eq t))
- | Not t' => HOLogic.Not$(term_of_fm vs t')
- | And(t1,t2) => HOLogic.conj$(term_of_fm vs t1)$(term_of_fm vs t2)
- | Or(t1,t2) => HOLogic.disj$(term_of_fm vs t1)$(term_of_fm vs t2)
- | Imp(t1,t2) => HOLogic.imp$(term_of_fm vs t1)$(term_of_fm vs t2)
- | Iff(t1,t2) => (HOLogic.eq_const bT)$(term_of_fm vs t1)$
- (term_of_fm vs t2)
- | _ => error "If this is raised, Isabelle/HOL or generate_code is inconsistent!";
-
-(* The oracle *)
-
-fun linrqe_oracle thy t =
- let
- val vs = start_vs t
- in HOLogic.mk_Trueprop (HOLogic.mk_eq (t, term_of_fm vs (linrqe (fm_of_term vs t)))) end;
-
-end;
--- a/src/HOL/Complex/ex/linrtac.ML Wed Jul 02 07:11:57 2008 +0200
+++ b/src/HOL/Complex/ex/linrtac.ML Wed Jul 02 07:12:17 2008 +0200
@@ -9,13 +9,11 @@
in @{simpset} delsimps ths addsimps (map (fn th => th RS sym) ths)
end;
-val nT = HOLogic.natT;
val binarith =
@{thms normalize_bin_simps} @ @{thms pred_bin_simps} @ @{thms succ_bin_simps} @
@{thms add_bin_simps} @ @{thms minus_bin_simps} @ @{thms mult_bin_simps};
val comp_arith = binarith @ simp_thms
-
val zdvd_int = @{thm zdvd_int};
val zdiff_int_split = @{thm zdiff_int_split};
val all_nat = @{thm all_nat};
@@ -55,7 +53,7 @@
val np = length ps
val (fm',np) = foldr (fn ((x, T), (fm,n)) => mk_all ((x, T), (fm,n)))
(foldr HOLogic.mk_imp c rhs, np) ps
- val (vs, _) = List.partition (fn t => q orelse (type_of t) = nT)
+ val (vs, _) = List.partition (fn t => q orelse (type_of t) = HOLogic.natT)
(term_frees fm' @ term_vars fm');
val fm2 = foldr mk_all2 fm' vs
in (fm2, np + length vs, length rhs) end;
@@ -98,7 +96,7 @@
| _ => (pre_thm, assm_tac i)
in (rtac (((mp_step nh) o (spec_step np)) th) i
THEN tac) st
- end handle Subscript => no_tac st | ReflectedFerrack.LINR => no_tac st);
+ end handle Subscript => no_tac st);
fun linr_meth src =
Method.syntax (Args.mode "no_quantify") src
@@ -108,5 +106,4 @@
Method.add_method ("rferrack", linr_meth,
"decision procedure for linear real arithmetic");
-
end
--- a/src/HOL/Extraction/Higman.thy Wed Jul 02 07:11:57 2008 +0200
+++ b/src/HOL/Extraction/Higman.thy Wed Jul 02 07:12:17 2008 +0200
@@ -426,13 +426,7 @@
code_datatype L0 L1 arbitrary_LT
code_datatype T0 T1 T2 arbitrary_TT
-export_code higman_idx in SML module_name Higman
-
ML {*
-local
- open Higman
-in
-
val a = 16807.0;
val m = 2147483647.0;
@@ -445,36 +439,34 @@
val r = nextRand seed;
val i = Real.round (r / m * 10.0);
in if i > 7 andalso l > 2 then (r, []) else
- apsnd (cons (if i mod 2 = 0 then A else B)) (mk_word r (l+1))
+ apsnd (cons (if i mod 2 = 0 then @{code A} else @{code B})) (mk_word r (l+1))
end;
-fun f s Zero_nat = mk_word s 0
- | f s (Suc n) = f (fst (mk_word s 0)) n;
+fun f s @{code "0::nat"} = mk_word s 0
+ | f s (@{code Suc} n) = f (fst (mk_word s 0)) n;
val g1 = snd o (f 20000.0);
val g2 = snd o (f 50000.0);
-fun f1 Zero_nat = [A,A]
- | f1 (Suc Zero_nat) = [B]
- | f1 (Suc (Suc Zero_nat)) = [A,B]
+fun f1 @{code "0::nat"} = [@{code A}, @{code A}]
+ | f1 (@{code Suc} @{code "0::nat"}) = [@{code B}]
+ | f1 (@{code Suc} (@{code Suc} @{code "0::nat"})) = [@{code A}, @{code B}]
| f1 _ = [];
-fun f2 Zero_nat = [A,A]
- | f2 (Suc Zero_nat) = [B]
- | f2 (Suc (Suc Zero_nat)) = [B,A]
+fun f2 @{code "0::nat"} = [@{code A}, @{code A}]
+ | f2 (@{code Suc} @{code "0::nat"}) = [@{code B}]
+ | f2 (@{code Suc} (@{code Suc} @{code "0::nat"})) = [@{code B}, @{code A}]
| f2 _ = [];
-val (i1, j1) = higman_idx g1;
+val (i1, j1) = @{code higman_idx} g1;
val (v1, w1) = (g1 i1, g1 j1);
-val (i2, j2) = higman_idx g2;
+val (i2, j2) = @{code higman_idx} g2;
val (v2, w2) = (g2 i2, g2 j2);
-val (i3, j3) = higman_idx f1;
+val (i3, j3) = @{code higman_idx} f1;
val (v3, w3) = (f1 i3, f1 j3);
-val (i4, j4) = higman_idx f2;
+val (i4, j4) = @{code higman_idx} f2;
val (v4, w4) = (f2 i4, f2 j4);
-
-end;
*}
end
--- a/src/HOL/Extraction/Pigeonhole.thy Wed Jul 02 07:11:57 2008 +0200
+++ b/src/HOL/Extraction/Pigeonhole.thy Wed Jul 02 07:12:17 2008 +0200
@@ -245,36 +245,34 @@
code_const arbitrary_nat (SML "~1")
-code_module PH1
+code_module PH
contains
test = test
test' = test'
test'' = test''
-export_code test test' test'' in SML module_name PH2
+ML "timeit (PH.test 10)"
+ML "timeit (@{code test} 10)"
-ML "timeit (PH1.test 10)"
-ML "timeit (PH2.test 10)"
+ML "timeit (PH.test' 10)"
+ML "timeit (@{code test'} 10)"
-ML "timeit (PH1.test' 10)"
-ML "timeit (PH2.test' 10)"
+ML "timeit (PH.test 20)"
+ML "timeit (@{code test} 20)"
-ML "timeit (PH1.test 20)"
-ML "timeit (PH2.test 20)"
+ML "timeit (PH.test' 20)"
+ML "timeit (@{code test'} 20)"
-ML "timeit (PH1.test' 20)"
-ML "timeit (PH2.test' 20)"
+ML "timeit (PH.test 25)"
+ML "timeit (@{code test} 25)"
-ML "timeit (PH1.test 25)"
-ML "timeit (PH2.test 25)"
+ML "timeit (PH.test' 25)"
+ML "timeit (@{code test'} 25)"
-ML "timeit (PH1.test' 25)"
-ML "timeit (PH2.test' 25)"
+ML "timeit (PH.test 500)"
+ML "timeit (@{code test} 500)"
-ML "timeit (PH1.test 500)"
-ML "timeit (PH2.test 500)"
-
-ML "timeit PH1.test''"
-ML "timeit PH2.test''"
+ML "timeit PH.test''"
+ML "timeit @{code test''}"
end
--- a/src/HOL/Extraction/QuotRem.thy Wed Jul 02 07:11:57 2008 +0200
+++ b/src/HOL/Extraction/QuotRem.thy Wed Jul 02 07:12:17 2008 +0200
@@ -5,7 +5,10 @@
header {* Quotient and remainder *}
-theory QuotRem imports Util begin
+theory QuotRem
+imports Util
+begin
+
text {* Derivation of quotient and remainder using program extraction. *}
theorem division: "\<exists>r q. a = Suc b * q + r \<and> r \<le> b"
@@ -42,6 +45,6 @@
contains
test = "division 9 2"
-export_code division in SML
+lemma "division 9 2 = (0, 3)" by eval
end
--- a/src/HOL/IsaMakefile Wed Jul 02 07:11:57 2008 +0200
+++ b/src/HOL/IsaMakefile Wed Jul 02 07:12:17 2008 +0200
@@ -791,7 +791,7 @@
Complex/ex/NSPrimes.thy Complex/ex/Sqrt.thy \
Complex/ex/Sqrt_Script.thy Complex/ex/MIR.thy Complex/ex/mirtac.ML \
Complex/ex/mireif.ML Complex/ex/ReflectedFerrack.thy \
- Complex/ex/linreif.ML Complex/ex/linrtac.ML
+ Complex/ex/linrtac.ML
@$(ISATOOL) usedir $(OUT)/HOL ex
--- a/src/HOL/SizeChange/Implementation.thy Wed Jul 02 07:11:57 2008 +0200
+++ b/src/HOL/SizeChange/Implementation.thy Wed Jul 02 07:12:17 2008 +0200
@@ -146,7 +146,6 @@
subsection {* Witness checking *}
-
definition test_SCT_witness :: "nat acg \<Rightarrow> nat acg \<Rightarrow> bool"
where
"test_SCT_witness A T =
@@ -155,7 +154,6 @@
n \<noteq> m \<or> G * G \<noteq> G \<or>
(\<exists>(p::nat,e,q)\<in>dest_graph G. p = q \<and> e = LESS)))"
-
lemma no_bad_graphs_ucl:
assumes "A \<le> B"
assumes "no_bad_graphs B"
@@ -164,8 +162,6 @@
unfolding no_bad_graphs_def has_edge_def graph_leq_def
by blast
-
-
lemma SCT'_witness:
assumes a: "test_SCT_witness A T"
shows "SCT' A"
@@ -184,14 +180,6 @@
by (rule no_bad_graphs_ucl)
qed
-
-code_modulename SML
- Graphs SCT
- Kleene_Algebras SCT
- Implementation SCT
-
-(* FIXME
-export_code test_SCT in SML
-*)
+(* ML {* @{code test_SCT} *} *)
end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/ex/Code_Antiq.thy Wed Jul 02 07:12:17 2008 +0200
@@ -0,0 +1,84 @@
+(* Title: HOL/ex/Code_Antiq.thy
+ ID: $Id$
+ Author: Florian Haftmann
+*)
+
+header {* A simple certificate check as toy example for the code antiquotation *}
+
+theory Code_Antiq
+imports Plain
+begin
+
+lemma div_cert1:
+ fixes n m q r :: nat
+ assumes "r < m"
+ and "0 < m"
+ and "n = m * q + r"
+ shows "n div m = q"
+using assms by (simp add: div_mult_self2 add_commute)
+
+lemma div_cert2:
+ fixes n :: nat
+ shows "n div 0 = 0"
+by simp
+
+ML {*
+local
+
+fun code_of_val k = if k <= 0 then @{code "0::nat"}
+ else @{code Suc} (code_of_val (k - 1));
+
+fun val_of_code @{code "0::nat"} = 0
+ | val_of_code (@{code Suc} n) = val_of_code n + 1;
+
+val term_of_code = HOLogic.mk_nat o val_of_code;
+
+infix 9 &$;
+val op &$ = uncurry Thm.capply;
+
+val simpset = HOL_ss addsimps
+ @{thms plus_nat.simps add_0_right add_Suc_right times_nat.simps mult_0_right mult_Suc_right less_nat_zero_code le_simps(2) less_eq_nat.simps(1) le_simps(3)}
+
+fun prove prop = Goal.prove_internal [] (@{cterm Trueprop} &$ prop)
+ (K (ALLGOALS (Simplifier.simp_tac simpset))); (*FIXME*)
+
+in
+
+fun simp_div ctxt ct_n ct_m =
+ let
+ val m = HOLogic.dest_nat (Thm.term_of ct_m);
+ in if m = 0 then Drule.instantiate'[] [SOME ct_n] @{thm div_cert2} else
+ let
+ val thy = ProofContext.theory_of ctxt;
+ val n = HOLogic.dest_nat (Thm.term_of ct_n);
+ val c_n = code_of_val n;
+ val c_m = code_of_val m;
+ val (c_q, c_r) = @{code divmod} c_n c_m;
+ val t_q = term_of_code c_q;
+ val t_r = term_of_code c_r;
+ val ct_q = Thm.cterm_of thy t_q;
+ val ct_r = Thm.cterm_of thy t_r;
+ val thm_r = prove (@{cterm "op < \<Colon> nat \<Rightarrow> _"} &$ ct_r &$ ct_m);
+ val thm_m = prove (@{cterm "(op < \<Colon> nat \<Rightarrow> _) 0"} &$ ct_m);
+ val thm_n = prove (@{cterm "(op = \<Colon> nat \<Rightarrow> _)"} &$ ct_n
+ &$ (@{cterm "(op + \<Colon> nat \<Rightarrow> _)"}
+ &$ (@{cterm "(op * \<Colon> nat \<Rightarrow> _)"} &$ ct_m &$ ct_q) &$ ct_r));
+ in @{thm div_cert1} OF [thm_r, thm_m, thm_n] end
+ end;
+
+end;
+*}
+
+ML_val {*
+ simp_div @{context}
+ @{cterm "Suc (Suc (Suc (Suc (Suc 0))))"}
+ @{cterm "(Suc (Suc 0))"}
+*}
+
+ML_val {*
+ simp_div @{context}
+ (Thm.cterm_of @{theory} (HOLogic.mk_nat 170))
+ (Thm.cterm_of @{theory} (HOLogic.mk_nat 42))
+*}
+
+end
\ No newline at end of file
--- a/src/HOL/ex/ROOT.ML Wed Jul 02 07:11:57 2008 +0200
+++ b/src/HOL/ex/ROOT.ML Wed Jul 02 07:12:17 2008 +0200
@@ -57,7 +57,8 @@
"Adder",
"Classical",
"set",
- "Meson_Test"
+ "Meson_Test",
+ "Code_Antiq"
];
setmp Proofterm.proofs 2 time_use_thy "Hilbert_Classical";
--- a/src/Tools/code/code_target.ML Wed Jul 02 07:11:57 2008 +0200
+++ b/src/Tools/code/code_target.ML Wed Jul 02 07:12:17 2008 +0200
@@ -71,7 +71,7 @@
| enum_default default sep opn cls xs = Pretty.enum sep opn cls xs;
datatype destination = Compile | Export | File of Path.T | String of string list;
-type serialization = destination -> string option;
+type serialization = destination -> (string * string list) option;
val code_width = ref 80; (*FIXME after Pretty module no longer depends on print mode*)
fun code_setmp f = PrintMode.setmp [] (Pretty.setmp_margin (!code_width) f);
@@ -82,7 +82,7 @@
fun compile f = (code_setmp f Compile; ());
fun export f = (code_setmp f Export; ());
fun file p f = (code_setmp f (File p); ());
-fun string cs f = the (code_setmp f (String cs));
+fun string cs f = fst (the (code_setmp f (String cs)));
fun stmt_names_of_destination (String stmts) = stmts
| stmt_names_of_destination _ = [];
@@ -1194,7 +1194,7 @@
error ("Unknown statement name: " ^ labelled_name name);
in (deresolver, nodes) end;
-fun serialize_ml compile pr_module pr_stmt projection raw_module_name labelled_name reserved_names includes raw_module_alias
+fun serialize_ml compile pr_module pr_stmt raw_module_name labelled_name reserved_names includes raw_module_alias
_ syntax_tyco syntax_const program cs destination =
let
val is_cons = CodeThingol.is_cons program;
@@ -1225,20 +1225,29 @@
fun output Compile = K NONE o compile o code_of_pretty
| output Export = K NONE o code_writeln
| output (File file) = K NONE o File.write file o code_of_pretty
- | output (String _) = SOME o code_of_pretty;
- in projection (output destination p) cs' end;
+ | output (String _) = SOME o rpair cs' o code_of_pretty;
+ in output destination p end;
end; (*local*)
+(* ML (system language) code for evaluation and instrumentalization *)
+
+fun ml_code_of thy program cs = mount_serializer thy
+ (SOME (fn _ => fn [] => serialize_ml (K ()) (K Pretty.chunks) pr_sml_stmt (SOME "")))
+ target_SML NONE [] program cs (String [])
+ |> the;
+
+(* generic entry points for SML/OCaml *)
+
fun isar_seri_sml module_name =
parse_args (Scan.succeed ())
#> (fn () => serialize_ml (use_text (1, "generated code") Output.ml_output false)
- pr_sml_module pr_sml_stmt K module_name);
+ pr_sml_module pr_sml_stmt module_name);
fun isar_seri_ocaml module_name =
parse_args (Scan.succeed ())
#> (fn () => serialize_ml (fn _ => error "OCaml: no internal compilation")
- pr_ocaml_module pr_ocaml_stmt K module_name);
+ pr_ocaml_module pr_ocaml_stmt module_name);
(** Haskell serializer **)
@@ -1640,7 +1649,7 @@
fun output Compile = error ("Haskell: no internal compilation")
| output Export = K NONE o map (code_writeln o snd)
| output (File destination) = K NONE o map (write_module destination)
- | output (String _) = SOME o cat_lines o map (code_of_pretty o snd);
+ | output (String _) = SOME o rpair [] o cat_lines o map (code_of_pretty o snd);
in
output destination (map (uncurry pr_module) includes
@ map serialize_module (Symtab.dest hs_program))
@@ -1813,13 +1822,6 @@
(* evaluation *)
-fun code_antiq_serializer module [] = serialize_ml (K ()) (K Pretty.chunks) pr_sml_stmt
- (fn SOME s => fn cs => SOME ("let\n" ^ s ^ "\nin fn () => " ^ enclose "(" ")" (commas cs) ^ " end"))
- (SOME "Isabelle_Eval");
-
-fun sml_code_of thy program cs = mount_serializer thy (SOME code_antiq_serializer) target_SML NONE [] program cs (String [])
- |> the;
-
fun eval eval'' term_of reff thy ct args =
let
val _ = if null (term_frees (term_of ct)) then () else error ("Term "
@@ -1832,8 +1834,9 @@
val program' = program
|> Graph.new_node (CodeName.value_name, CodeThingol.Fun (([], ty), [(([], t), Drule.dummy_thm)]))
|> fold (curry Graph.add_edge CodeName.value_name) deps;
- val value_code = sml_code_of thy program' [CodeName.value_name] ;
- val sml_code = space_implode " " (value_code :: "()" :: map (enclose "(" ")") args);
+ val (value_code, [value_name']) = ml_code_of thy program' [CodeName.value_name];
+ val sml_code = "let\n" ^ value_code ^ "\nin " ^ value_name'
+ ^ space_implode " " (map (enclose "(" ")") args) ^ " end";
in ML_Context.evaluate Output.ml_output false reff sml_code end;
in eval'' thy (fn t => (t, eval')) ct end;
@@ -1843,11 +1846,50 @@
(* instrumentalization by antiquotation *)
-val ml_code_antiq = Args.theory -- Scan.repeat1 Args.term >> (fn (thy, ts) =>
+local
+
+structure CodeAntiqData = ProofDataFun
+(
+ type T = string list * (bool * string);
+ fun init _ = ([], (true, ""));
+);
+
+val is_first_occ = fst o snd o CodeAntiqData.get;
+
+fun register_const const ctxt =
+ let
+ val (consts, (_, struct_name)) = CodeAntiqData.get ctxt;
+ val (struct_name', ctxt') = if struct_name = ""
+ then ML_Antiquote.variant "Code" ctxt
+ else (struct_name, ctxt);
+ in CodeAntiqData.put (insert (op =) const consts, (false, struct_name')) ctxt' end;
+
+fun print_code thy struct_name is_first const ctxt =
let
- val cs = map (CodeUnit.check_const thy) ts;
- val (cs', program) = CodeThingol.consts_program thy cs;
- in sml_code_of thy program cs' ^ " ()" end);
+ val (consts, (_, struct_code_name)) = CodeAntiqData.get ctxt;
+ val (consts', program) = CodeThingol.consts_program thy consts;
+ val (raw_ml_code, consts'') = ml_code_of thy program consts';
+ val _ = if length consts <> length consts'' then
+ error ("One of the constants " ^ commas (map (quote o CodeUnit.string_of_const thy) consts)
+ ^ "\nhas a user-defined serialization") else ();
+ val const'' = NameSpace.append (NameSpace.append struct_name struct_code_name)
+ ((the o AList.lookup (op =) (consts ~~ consts'')) const);
+ val ml_code = if is_first then "\nstructure " ^ struct_code_name
+ ^ " =\nstruct\n\n" ^ raw_ml_code ^ "\nend;\n\n"
+ else "";
+ in (ml_code, const'') end;
+
+in
+
+fun ml_code_antiq raw_const {struct_name, background} =
+ let
+ val thy = ProofContext.theory_of background;
+ val const = CodeUnit.check_const thy raw_const;
+ val is_first = is_first_occ background;
+ val background' = register_const const background;
+ in (print_code thy struct_name is_first const, background') end;
+
+end; (*local*)
(* code presentation *)
@@ -2291,7 +2333,7 @@
| NONE => error ("Bad directive " ^ quote cmd)))
handle TOPLEVEL_ERROR => OS.Process.exit OS.Process.failure;
-val _ = ML_Antiquote.value "code" ml_code_antiq;
+val _ = ML_Context.add_antiq "code" (Args.term >> ml_code_antiq);
(* serializer setup, including serializer defaults *)