code antiquotation roaring ahead
authorhaftmann
Wed Jul 02 07:12:17 2008 +0200 (2008-07-02)
changeset 274369581777503e9
parent 27435 b3f8e9bdf9a7
child 27437 727297fcf7c8
code antiquotation roaring ahead
NEWS
src/HOL/Complex/ex/ReflectedFerrack.thy
src/HOL/Complex/ex/linreif.ML
src/HOL/Complex/ex/linrtac.ML
src/HOL/Extraction/Higman.thy
src/HOL/Extraction/Pigeonhole.thy
src/HOL/Extraction/QuotRem.thy
src/HOL/IsaMakefile
src/HOL/SizeChange/Implementation.thy
src/HOL/ex/Code_Antiq.thy
src/HOL/ex/ROOT.ML
src/Tools/code/code_target.ML
     1.1 --- a/NEWS	Wed Jul 02 07:11:57 2008 +0200
     1.2 +++ b/NEWS	Wed Jul 02 07:12:17 2008 +0200
     1.3 @@ -15,8 +15,20 @@
     1.4  
     1.5  * Keyword 'code_exception' now named 'code_abort'.  INCOMPATIBILITY.
     1.6  
     1.7 +* New ML antiquotation 'code': takes constant as argument, generates
     1.8 +corresponding code in background and inserts name of the corresponding resulting
     1.9 +ML value/function/datatype constructor binding in place.  All occurences of 'code'
    1.10 +with a single ML block are generated simultaneously.
    1.11 +Provides a generic and safe interface for instrumentalizing code generation.
    1.12 +See HOL/ex/Code_Antiq for a toy example, or HOL/Complex/ex/ReflectedFerrack
    1.13 +for a more ambitious application.  In future you ought refrain from
    1.14 +ad-hoc compiling generated SML code on the ML toplevel.
    1.15 +Note that (for technical reasons) 'code' cannot refer to constants for which
    1.16 +user-defined serializations are set.  Refer to the corresponding ML counterpart
    1.17 +directly in that cases.
    1.18 +
    1.19  * Removed exotic 'token_translation' command.  INCOMPATIBILITY, use ML
    1.20 -interface instead.
    1.21 +interface instead. 
    1.22  
    1.23  
    1.24  *** Document preparation ***
    1.25 @@ -32,7 +44,10 @@
    1.26  Complex_Main.thy remain as they are.
    1.27  
    1.28  * New image HOL-Plain provides a minimal HOL with the most important tools
    1.29 -available (inductive, datatype, primrec, codegen, ...).
    1.30 +available (inductive, datatype, primrec, ...).  By convention the corresponding
    1.31 +theory Plain should be ancestor of every further (library) theory.  Some library
    1.32 +theories now have ancestor Plain (instead of Main), thus theory Main
    1.33 +occasionally has to be imported explicitly.
    1.34  
    1.35  * Methods "case_tac" and "induct_tac" now refer to the very same rules
    1.36  as the structured Isar versions "cases" and "induct", cf. the
    1.37 @@ -66,7 +81,7 @@
    1.38  
    1.39  
    1.40  *** ML ***
    1.41 -
    1.42 + 
    1.43  * Rules and tactics that read instantiations (read_instantiate,
    1.44  res_inst_tac, thin_tac, subgoal_tac etc.) now demand a proper proof
    1.45  context, which is required for parsing and type-checking.  Moreover,
     2.1 --- a/src/HOL/Complex/ex/ReflectedFerrack.thy	Wed Jul 02 07:11:57 2008 +0200
     2.2 +++ b/src/HOL/Complex/ex/ReflectedFerrack.thy	Wed Jul 02 07:12:17 2008 +0200
     2.3 @@ -6,7 +6,7 @@
     2.4  
     2.5  theory ReflectedFerrack
     2.6  imports Main GCD Real Efficient_Nat
     2.7 -uses ("linreif.ML") ("linrtac.ML")
     2.8 +uses ("linrtac.ML")
     2.9  begin
    2.10  
    2.11  
    2.12 @@ -1985,30 +1985,97 @@
    2.13    with lr show ?thesis by blast
    2.14  qed
    2.15  
    2.16 -constdefs linrqe:: "fm \<Rightarrow> fm"
    2.17 -  "linrqe \<equiv> (\<lambda> p. qelim (prep p) ferrack)"
    2.18 +definition linrqe:: "fm \<Rightarrow> fm" where
    2.19 +  "linrqe p = qelim (prep p) ferrack"
    2.20  
    2.21 -theorem linrqe: "(Ifm bs (linrqe p) = Ifm bs p) \<and> qfree (linrqe p)"
    2.22 +theorem linrqe: "Ifm bs (linrqe p) = Ifm bs p \<and> qfree (linrqe p)"
    2.23  using ferrack qelim_ci prep
    2.24  unfolding linrqe_def by auto
    2.25  
    2.26 -definition
    2.27 -  ferrack_test :: "unit \<Rightarrow> fm"
    2.28 -where
    2.29 +definition ferrack_test :: "unit \<Rightarrow> fm" where
    2.30    "ferrack_test u = linrqe (A (A (Imp (Lt (Sub (Bound 1) (Bound 0)))
    2.31      (E (Eq (Sub (Add (Bound 0) (Bound 2)) (Bound 1)))))))"
    2.32  
    2.33 -export_code linrqe ferrack_test in SML module_name Ferrack
    2.34 +ML {* @{code ferrack_test} () *}
    2.35 +
    2.36 +oracle linr_oracle ("term") = {*
    2.37 +
    2.38 +let
    2.39 +
    2.40 +fun num_of_term vs (t as Free (xn, xT)) = (case AList.lookup (op =) vs t
    2.41 +     of NONE => error "Variable not found in the list!"
    2.42 +      | SOME n => @{code Bound} n)
    2.43 +  | num_of_term vs @{term "real (0::int)"} = @{code C} 0
    2.44 +  | num_of_term vs @{term "real (1::int)"} = @{code C} 1
    2.45 +  | num_of_term vs @{term "0::real"} = @{code C} 0
    2.46 +  | num_of_term vs @{term "1::real"} = @{code C} 1
    2.47 +  | num_of_term vs (Term.Bound i) = @{code Bound} i
    2.48 +  | num_of_term vs (@{term "uminus :: real \<Rightarrow> real"} $ t') = @{code Neg} (num_of_term vs t')
    2.49 +  | 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)
    2.50 +  | 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)
    2.51 +  | num_of_term vs (@{term "op * :: real \<Rightarrow> real \<Rightarrow> real"} $ t1 $ t2) = (case (num_of_term vs t1)
    2.52 +     of @{code C} i => @{code Mul} (i, num_of_term vs t2)
    2.53 +      | _ => error "num_of_term: unsupported Multiplication")
    2.54 +  | num_of_term vs (@{term "real :: int \<Rightarrow> real"} $ (@{term "number_of :: int \<Rightarrow> int"} $ t')) = @{code C} (HOLogic.dest_numeral t')
    2.55 +  | num_of_term vs (@{term "number_of :: int \<Rightarrow> int"} $ t') = @{code C} (HOLogic.dest_numeral t')
    2.56 +  | num_of_term vs t = error ("num_of_term: unknown term " ^ Syntax.string_of_term_global @{theory} t);
    2.57 +
    2.58 +fun fm_of_term vs @{term True} = @{code T}
    2.59 +  | fm_of_term vs @{term False} = @{code T}
    2.60 +  | 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))
    2.61 +  | 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))
    2.62 +  | 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)) 
    2.63 +  | 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)
    2.64 +  | fm_of_term vs (@{term "op &"} $ t1 $ t2) = @{code And} (fm_of_term vs t1, fm_of_term vs t2)
    2.65 +  | fm_of_term vs (@{term "op |"} $ t1 $ t2) = @{code Or} (fm_of_term vs t1, fm_of_term vs t2)
    2.66 +  | fm_of_term vs (@{term "op -->"} $ t1 $ t2) = @{code Imp} (fm_of_term vs t1, fm_of_term vs t2)
    2.67 +  | fm_of_term vs (@{term "Not"} $ t') = @{code NOT} (fm_of_term vs t')
    2.68 +  | fm_of_term vs (Const("Ex", _) $ Term.Abs (xn, xT, p)) =
    2.69 +      @{code E} (fm_of_term (map (fn (v, n) => (v, n + 1)) vs) p)
    2.70 +  | fm_of_term vs (Const("All", _) $ Term.Abs(xn, xT, p)) =
    2.71 +      @{code A} (fm_of_term (map (fn (v, n) => (v, n + 1)) vs) p)
    2.72 +  | fm_of_term vs t = error ("fm_of_term : unknown term " ^ Syntax.string_of_term_global @{theory} t);
    2.73  
    2.74 -(*code_module Ferrack
    2.75 -  contains
    2.76 -    linrqe = linrqe
    2.77 -    test = ferrack_test*)
    2.78 +fun term_of_num vs (@{code C} i) = @{term "real :: int \<Rightarrow> real"} $ HOLogic.mk_number HOLogic.intT i
    2.79 +  | term_of_num vs (@{code Bound} n) = fst (the (find_first (fn (_, m) => n = m) vs))
    2.80 +  | term_of_num vs (@{code Neg} t') = @{term "uminus :: real \<Rightarrow> real"} $ term_of_num vs t'
    2.81 +  | term_of_num vs (@{code Add} (t1, t2)) = @{term "op + :: real \<Rightarrow> real \<Rightarrow> real"} $
    2.82 +      term_of_num vs t1 $ term_of_num vs t2
    2.83 +  | term_of_num vs (@{code Sub} (t1, t2)) = @{term "op - :: real \<Rightarrow> real \<Rightarrow> real"} $
    2.84 +      term_of_num vs t1 $ term_of_num vs t2
    2.85 +  | term_of_num vs (@{code Mul} (i, t2)) = @{term "op * :: real \<Rightarrow> real \<Rightarrow> real"} $
    2.86 +      term_of_num vs (@{code C} i) $ term_of_num vs t2
    2.87 +  | term_of_num vs (@{code CN} (n, i, t)) = term_of_num vs (@{code Add} (@{code Mul} (i, @{code Bound} n), t));
    2.88  
    2.89 -ML {* Ferrack.ferrack_test () *}
    2.90 +fun term_of_fm vs @{code T} = HOLogic.true_const 
    2.91 +  | term_of_fm vs @{code F} = HOLogic.false_const
    2.92 +  | term_of_fm vs (@{code Lt} t) = @{term "op < :: real \<Rightarrow> real \<Rightarrow> bool"} $
    2.93 +      term_of_num vs t $ @{term "0::real"}
    2.94 +  | term_of_fm vs (@{code Le} t) = @{term "op \<le> :: real \<Rightarrow> real \<Rightarrow> bool"} $
    2.95 +      term_of_num vs t $ @{term "0::real"}
    2.96 +  | term_of_fm vs (@{code Gt} t) = @{term "op < :: real \<Rightarrow> real \<Rightarrow> bool"} $
    2.97 +      @{term "0::real"} $ term_of_num vs t
    2.98 +  | term_of_fm vs (@{code Ge} t) = @{term "op \<le> :: real \<Rightarrow> real \<Rightarrow> bool"} $
    2.99 +      @{term "0::real"} $ term_of_num vs t
   2.100 +  | term_of_fm vs (@{code Eq} t) = @{term "op = :: real \<Rightarrow> real \<Rightarrow> bool"} $
   2.101 +      term_of_num vs t $ @{term "0::real"}
   2.102 +  | term_of_fm vs (@{code NEq} t) = term_of_fm vs (@{code NOT} (@{code Eq} t))
   2.103 +  | term_of_fm vs (@{code NOT} t') = HOLogic.Not $ term_of_fm vs t'
   2.104 +  | term_of_fm vs (@{code And} (t1, t2)) = HOLogic.conj $ term_of_fm vs t1 $ term_of_fm vs t2
   2.105 +  | term_of_fm vs (@{code Or} (t1, t2)) = HOLogic.disj $ term_of_fm vs t1 $ term_of_fm vs t2
   2.106 +  | term_of_fm vs (@{code Imp}  (t1, t2)) = HOLogic.imp $ term_of_fm vs t1 $ term_of_fm vs t2
   2.107 +  | term_of_fm vs (@{code Iff} (t1, t2)) = @{term "op = :: bool \<Rightarrow> bool \<Rightarrow> bool"} $
   2.108 +      term_of_fm vs t1 $ term_of_fm vs t2
   2.109 +  | term_of_fm vs _ = error "If this is raised, Isabelle/HOL or generate_code is inconsistent.";
   2.110  
   2.111 -use "linreif.ML"
   2.112 -oracle linr_oracle ("term") = ReflectedFerrack.linrqe_oracle
   2.113 +in fn thy => fn t =>
   2.114 +  let 
   2.115 +    val fs = term_frees t;
   2.116 +    val vs = fs ~~ (0 upto (length fs - 1));
   2.117 +  in HOLogic.mk_Trueprop (HOLogic.mk_eq (t, term_of_fm vs (@{code linrqe} (fm_of_term vs t)))) end
   2.118 +end;
   2.119 +*}
   2.120 +
   2.121  use "linrtac.ML"
   2.122  setup LinrTac.setup
   2.123  
     3.1 --- a/src/HOL/Complex/ex/linreif.ML	Wed Jul 02 07:11:57 2008 +0200
     3.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.3 @@ -1,118 +0,0 @@
     3.4 -(*  ID:         $Id$
     3.5 -    Author:     Amine Chaieb, TU Muenchen
     3.6 -
     3.7 -The oracle for Mixed Real-Integer auantifier elimination
     3.8 -based on the verified Code in ~/work/MIR/MIR.thy.
     3.9 -*)
    3.10 -
    3.11 -structure ReflectedFerrack =
    3.12 -struct
    3.13 -
    3.14 -open Ferrack;
    3.15 -
    3.16 -exception LINR;
    3.17 -
    3.18 -(* pseudo reification : term -> intterm *)
    3.19 -val rT = Type ("RealDef.real",[]);
    3.20 -val bT = HOLogic.boolT;
    3.21 -val realC = @{term "RealDef.real :: int => real"};
    3.22 -val rzero = @{term "0 :: real"};
    3.23 -
    3.24 -fun num_of_term vs t = case t
    3.25 -   of Free(xn,xT) => (case AList.lookup (op =) vs t of 
    3.26 -           NONE   => error "Variable not found in the list!"
    3.27 -         | SOME n => Bound n)
    3.28 -      | Const("RealDef.real",_)$ @{term "0::int"} => C 0
    3.29 -      | Const("RealDef.real",_)$ @{term "1::int"} => C 1
    3.30 -      | @{term "0::real"} => C 0
    3.31 -      | @{term "0::real"} => C 1
    3.32 -      | Term.Bound i => Bound i
    3.33 -      | Const (@{const_name "HOL.uminus"},_)$t' => Neg (num_of_term vs t')
    3.34 -      | Const (@{const_name "HOL.plus"},_)$t1$t2 => Add (num_of_term vs t1,num_of_term vs t2)
    3.35 -      | Const (@{const_name "HOL.minus"},_)$t1$t2 => Sub (num_of_term vs t1,num_of_term vs t2)
    3.36 -      | Const (@{const_name "HOL.times"},_)$t1$t2 => (case (num_of_term vs t1) of C i => 
    3.37 -          Mul (i,num_of_term vs t2)
    3.38 -        | _ => error "num_of_term: unsupported Multiplication")
    3.39 -      | Const("RealDef.real",_) $ Const (@{const_name "Int.number_of"},_)$t' => C (HOLogic.dest_numeral t')
    3.40 -      | Const (@{const_name "Int.number_of"},_)$t' => C (HOLogic.dest_numeral t')
    3.41 -      | _ => error ("num_of_term: unknown term " ^ Syntax.string_of_term_global Pure.thy t);
    3.42 -
    3.43 -(* pseudo reification : term -> fm *)
    3.44 -fun fm_of_term vs t = 
    3.45 -    case t of 
    3.46 -	Const("True",_) => T
    3.47 -      | Const("False",_) => F
    3.48 -      | Const(@{const_name HOL.less},_)$t1$t2 => Lt (Sub (num_of_term vs t1,num_of_term vs t2))
    3.49 -      | Const(@{const_name HOL.less_eq},_)$t1$t2 => Le (Sub (num_of_term vs t1,num_of_term vs t2))
    3.50 -      | Const("op =",eqT)$t1$t2 => 
    3.51 -	if (domain_type eqT = rT)
    3.52 -	then Eq (Sub (num_of_term vs t1,num_of_term vs t2)) 
    3.53 -	else Iff(fm_of_term vs t1,fm_of_term vs t2)
    3.54 -      | Const("op &",_)$t1$t2 => And(fm_of_term vs t1,fm_of_term vs t2)
    3.55 -      | Const("op |",_)$t1$t2 => Or(fm_of_term vs t1,fm_of_term vs t2)
    3.56 -      | Const("op -->",_)$t1$t2 => Imp(fm_of_term vs t1,fm_of_term vs t2)
    3.57 -      | Const("Not",_)$t' => Not(fm_of_term vs t')
    3.58 -      | Const("Ex",_)$Term.Abs(xn,xT,p) => 
    3.59 -	E(fm_of_term (map (fn(v,n) => (v,1+ n)) vs) p)
    3.60 -      | Const("All",_)$Term.Abs(xn,xT,p) => 
    3.61 -	A(fm_of_term (map (fn(v,n) => (v,1+ n)) vs) p)
    3.62 -      | _ => error ("fm_of_term : unknown term!" ^ Syntax.string_of_term_global Pure.thy t);
    3.63 -
    3.64 -
    3.65 -fun start_vs t =
    3.66 -  let
    3.67 -    val fs = term_frees t
    3.68 -  in fs ~~ (0 upto (length fs - 1)) end;
    3.69 -
    3.70 -(* transform num and fm back to terms *)
    3.71 -
    3.72 -fun myassoc2 l v =
    3.73 -    case l of
    3.74 -	[] => NONE
    3.75 -      | (x,v')::xs => if v = v' then SOME x
    3.76 -		      else myassoc2 xs v;
    3.77 -
    3.78 -fun term_of_num vs t =
    3.79 -    case t of 
    3.80 -	C i => realC $ (HOLogic.mk_number HOLogic.intT i)
    3.81 -      | Bound n => the (myassoc2 vs n)
    3.82 -      | Neg t' => Const(@{const_name HOL.uminus},rT --> rT)$(term_of_num vs t')
    3.83 -      | Add(t1,t2) => Const(@{const_name HOL.plus},[rT,rT] ---> rT)$
    3.84 -			   (term_of_num vs t1)$(term_of_num vs t2)
    3.85 -      | Sub(t1,t2) => Const(@{const_name HOL.minus},[rT,rT] ---> rT)$
    3.86 -			   (term_of_num vs t1)$(term_of_num vs t2)
    3.87 -      | Mul(i,t2) => Const(@{const_name HOL.times},[rT,rT] ---> rT)$
    3.88 -			   (term_of_num vs (C i))$(term_of_num vs t2)
    3.89 -      | Cn(n,i,t) => term_of_num vs (Add (Mul(i,Bound n),t));
    3.90 -
    3.91 -fun term_of_fm vs t = 
    3.92 -    case t of 
    3.93 -	T => HOLogic.true_const 
    3.94 -      | F => HOLogic.false_const
    3.95 -      | Lt t => Const(@{const_name HOL.less},[rT,rT] ---> bT)$
    3.96 -			   (term_of_num vs t)$ rzero
    3.97 -      | Le t => Const(@{const_name HOL.less_eq},[rT,rT] ---> bT)$
    3.98 -			  (term_of_num vs t)$ rzero
    3.99 -      | Gt t => Const(@{const_name HOL.less},[rT,rT] ---> bT)$
   3.100 -			   rzero $(term_of_num vs t)
   3.101 -      | Ge t => Const(@{const_name HOL.less_eq},[rT,rT] ---> bT)$
   3.102 -			  rzero $(term_of_num vs t)
   3.103 -      | Eq t => Const("op =",[rT,rT] ---> bT)$
   3.104 -			   (term_of_num vs t)$ rzero
   3.105 -      | NEq t => term_of_fm vs (Not (Eq t))
   3.106 -      | Not t' => HOLogic.Not$(term_of_fm vs t')
   3.107 -      | And(t1,t2) => HOLogic.conj$(term_of_fm vs t1)$(term_of_fm vs t2)
   3.108 -      | Or(t1,t2) => HOLogic.disj$(term_of_fm vs t1)$(term_of_fm vs t2)
   3.109 -      | Imp(t1,t2) => HOLogic.imp$(term_of_fm vs t1)$(term_of_fm vs t2)
   3.110 -      | Iff(t1,t2) => (HOLogic.eq_const bT)$(term_of_fm vs t1)$
   3.111 -					   (term_of_fm vs t2)
   3.112 -      | _ => error "If this is raised, Isabelle/HOL or generate_code is inconsistent!";
   3.113 -
   3.114 -(* The oracle *)
   3.115 -
   3.116 -fun linrqe_oracle thy t = 
   3.117 -  let 
   3.118 -    val vs = start_vs t
   3.119 -  in HOLogic.mk_Trueprop (HOLogic.mk_eq (t, term_of_fm vs (linrqe (fm_of_term vs t)))) end;
   3.120 -
   3.121 -end;
     4.1 --- a/src/HOL/Complex/ex/linrtac.ML	Wed Jul 02 07:11:57 2008 +0200
     4.2 +++ b/src/HOL/Complex/ex/linrtac.ML	Wed Jul 02 07:12:17 2008 +0200
     4.3 @@ -9,13 +9,11 @@
     4.4  	     in @{simpset} delsimps ths addsimps (map (fn th => th RS sym) ths)
     4.5  	     end;
     4.6  
     4.7 -val nT = HOLogic.natT;
     4.8  val binarith =
     4.9    @{thms normalize_bin_simps} @ @{thms pred_bin_simps} @ @{thms succ_bin_simps} @
    4.10    @{thms add_bin_simps} @ @{thms minus_bin_simps} @  @{thms mult_bin_simps};
    4.11  val comp_arith = binarith @ simp_thms
    4.12  
    4.13 -
    4.14  val zdvd_int = @{thm zdvd_int};
    4.15  val zdiff_int_split = @{thm zdiff_int_split};
    4.16  val all_nat = @{thm all_nat};
    4.17 @@ -55,7 +53,7 @@
    4.18      val np = length ps
    4.19      val (fm',np) =  foldr (fn ((x, T), (fm,n)) => mk_all ((x, T), (fm,n)))
    4.20        (foldr HOLogic.mk_imp c rhs, np) ps
    4.21 -    val (vs, _) = List.partition (fn t => q orelse (type_of t) = nT)
    4.22 +    val (vs, _) = List.partition (fn t => q orelse (type_of t) = HOLogic.natT)
    4.23        (term_frees fm' @ term_vars fm');
    4.24      val fm2 = foldr mk_all2 fm' vs
    4.25    in (fm2, np + length vs, length rhs) end;
    4.26 @@ -98,7 +96,7 @@
    4.27        | _ => (pre_thm, assm_tac i)
    4.28    in (rtac (((mp_step nh) o (spec_step np)) th) i 
    4.29        THEN tac) st
    4.30 -  end handle Subscript => no_tac st | ReflectedFerrack.LINR => no_tac st);
    4.31 +  end handle Subscript => no_tac st);
    4.32  
    4.33  fun linr_meth src =
    4.34    Method.syntax (Args.mode "no_quantify") src
    4.35 @@ -108,5 +106,4 @@
    4.36    Method.add_method ("rferrack", linr_meth,
    4.37       "decision procedure for linear real arithmetic");
    4.38  
    4.39 -
    4.40  end
     5.1 --- a/src/HOL/Extraction/Higman.thy	Wed Jul 02 07:11:57 2008 +0200
     5.2 +++ b/src/HOL/Extraction/Higman.thy	Wed Jul 02 07:12:17 2008 +0200
     5.3 @@ -426,13 +426,7 @@
     5.4  code_datatype L0 L1 arbitrary_LT
     5.5  code_datatype T0 T1 T2 arbitrary_TT
     5.6  
     5.7 -export_code higman_idx in SML module_name Higman
     5.8 -
     5.9  ML {*
    5.10 -local
    5.11 -  open Higman
    5.12 -in
    5.13 -
    5.14  val a = 16807.0;
    5.15  val m = 2147483647.0;
    5.16  
    5.17 @@ -445,36 +439,34 @@
    5.18      val r = nextRand seed;
    5.19      val i = Real.round (r / m * 10.0);
    5.20    in if i > 7 andalso l > 2 then (r, []) else
    5.21 -    apsnd (cons (if i mod 2 = 0 then A else B)) (mk_word r (l+1))
    5.22 +    apsnd (cons (if i mod 2 = 0 then @{code A} else @{code B})) (mk_word r (l+1))
    5.23    end;
    5.24  
    5.25 -fun f s Zero_nat = mk_word s 0
    5.26 -  | f s (Suc n) = f (fst (mk_word s 0)) n;
    5.27 +fun f s @{code "0::nat"} = mk_word s 0
    5.28 +  | f s (@{code Suc} n) = f (fst (mk_word s 0)) n;
    5.29  
    5.30  val g1 = snd o (f 20000.0);
    5.31  
    5.32  val g2 = snd o (f 50000.0);
    5.33  
    5.34 -fun f1 Zero_nat = [A,A]
    5.35 -  | f1 (Suc Zero_nat) = [B]
    5.36 -  | f1 (Suc (Suc Zero_nat)) = [A,B]
    5.37 +fun f1 @{code "0::nat"} = [@{code A}, @{code A}]
    5.38 +  | f1 (@{code Suc} @{code "0::nat"}) = [@{code B}]
    5.39 +  | f1 (@{code Suc} (@{code Suc} @{code "0::nat"})) = [@{code A}, @{code B}]
    5.40    | f1 _ = [];
    5.41  
    5.42 -fun f2 Zero_nat = [A,A]
    5.43 -  | f2 (Suc Zero_nat) = [B]
    5.44 -  | f2 (Suc (Suc Zero_nat)) = [B,A]
    5.45 +fun f2 @{code "0::nat"} = [@{code A}, @{code A}]
    5.46 +  | f2 (@{code Suc} @{code "0::nat"}) = [@{code B}]
    5.47 +  | f2 (@{code Suc} (@{code Suc} @{code "0::nat"})) = [@{code B}, @{code A}]
    5.48    | f2 _ = [];
    5.49  
    5.50 -val (i1, j1) = higman_idx g1;
    5.51 +val (i1, j1) = @{code higman_idx} g1;
    5.52  val (v1, w1) = (g1 i1, g1 j1);
    5.53 -val (i2, j2) = higman_idx g2;
    5.54 +val (i2, j2) = @{code higman_idx} g2;
    5.55  val (v2, w2) = (g2 i2, g2 j2);
    5.56 -val (i3, j3) = higman_idx f1;
    5.57 +val (i3, j3) = @{code higman_idx} f1;
    5.58  val (v3, w3) = (f1 i3, f1 j3);
    5.59 -val (i4, j4) = higman_idx f2;
    5.60 +val (i4, j4) = @{code higman_idx} f2;
    5.61  val (v4, w4) = (f2 i4, f2 j4);
    5.62 -
    5.63 -end;
    5.64  *}
    5.65  
    5.66  end
     6.1 --- a/src/HOL/Extraction/Pigeonhole.thy	Wed Jul 02 07:11:57 2008 +0200
     6.2 +++ b/src/HOL/Extraction/Pigeonhole.thy	Wed Jul 02 07:12:17 2008 +0200
     6.3 @@ -245,36 +245,34 @@
     6.4  
     6.5  code_const  arbitrary_nat (SML "~1")
     6.6  
     6.7 -code_module PH1
     6.8 +code_module PH
     6.9  contains
    6.10    test = test
    6.11    test' = test'
    6.12    test'' = test''
    6.13  
    6.14 -export_code test test' test'' in SML module_name PH2
    6.15 +ML "timeit (PH.test 10)"
    6.16 +ML "timeit (@{code test} 10)" 
    6.17  
    6.18 -ML "timeit (PH1.test 10)"
    6.19 -ML "timeit (PH2.test 10)"
    6.20 +ML "timeit (PH.test' 10)"
    6.21 +ML "timeit (@{code test'} 10)"
    6.22  
    6.23 -ML "timeit (PH1.test' 10)"
    6.24 -ML "timeit (PH2.test' 10)"
    6.25 +ML "timeit (PH.test 20)"
    6.26 +ML "timeit (@{code test} 20)"
    6.27  
    6.28 -ML "timeit (PH1.test 20)"
    6.29 -ML "timeit (PH2.test 20)"
    6.30 +ML "timeit (PH.test' 20)"
    6.31 +ML "timeit (@{code test'} 20)"
    6.32  
    6.33 -ML "timeit (PH1.test' 20)"
    6.34 -ML "timeit (PH2.test' 20)"
    6.35 +ML "timeit (PH.test 25)"
    6.36 +ML "timeit (@{code test} 25)"
    6.37  
    6.38 -ML "timeit (PH1.test 25)"
    6.39 -ML "timeit (PH2.test 25)"
    6.40 +ML "timeit (PH.test' 25)"
    6.41 +ML "timeit (@{code test'} 25)"
    6.42  
    6.43 -ML "timeit (PH1.test' 25)"
    6.44 -ML "timeit (PH2.test' 25)"
    6.45 +ML "timeit (PH.test 500)"
    6.46 +ML "timeit (@{code test} 500)"
    6.47  
    6.48 -ML "timeit (PH1.test 500)"
    6.49 -ML "timeit (PH2.test 500)"
    6.50 -
    6.51 -ML "timeit PH1.test''"
    6.52 -ML "timeit PH2.test''"
    6.53 +ML "timeit PH.test''"
    6.54 +ML "timeit @{code test''}"
    6.55  
    6.56  end
     7.1 --- a/src/HOL/Extraction/QuotRem.thy	Wed Jul 02 07:11:57 2008 +0200
     7.2 +++ b/src/HOL/Extraction/QuotRem.thy	Wed Jul 02 07:12:17 2008 +0200
     7.3 @@ -5,7 +5,10 @@
     7.4  
     7.5  header {* Quotient and remainder *}
     7.6  
     7.7 -theory QuotRem imports Util begin
     7.8 +theory QuotRem
     7.9 +imports Util
    7.10 +begin
    7.11 +
    7.12  text {* Derivation of quotient and remainder using program extraction. *}
    7.13  
    7.14  theorem division: "\<exists>r q. a = Suc b * q + r \<and> r \<le> b"
    7.15 @@ -42,6 +45,6 @@
    7.16  contains
    7.17    test = "division 9 2"
    7.18  
    7.19 -export_code division in SML
    7.20 +lemma "division 9 2 = (0, 3)" by eval
    7.21  
    7.22  end
     8.1 --- a/src/HOL/IsaMakefile	Wed Jul 02 07:11:57 2008 +0200
     8.2 +++ b/src/HOL/IsaMakefile	Wed Jul 02 07:12:17 2008 +0200
     8.3 @@ -791,7 +791,7 @@
     8.4    Complex/ex/NSPrimes.thy Complex/ex/Sqrt.thy				\
     8.5    Complex/ex/Sqrt_Script.thy Complex/ex/MIR.thy Complex/ex/mirtac.ML	\
     8.6    Complex/ex/mireif.ML Complex/ex/ReflectedFerrack.thy			\
     8.7 -  Complex/ex/linreif.ML Complex/ex/linrtac.ML
     8.8 +  Complex/ex/linrtac.ML
     8.9  	@$(ISATOOL) usedir $(OUT)/HOL ex
    8.10  
    8.11  
     9.1 --- a/src/HOL/SizeChange/Implementation.thy	Wed Jul 02 07:11:57 2008 +0200
     9.2 +++ b/src/HOL/SizeChange/Implementation.thy	Wed Jul 02 07:12:17 2008 +0200
     9.3 @@ -146,7 +146,6 @@
     9.4  
     9.5  subsection {* Witness checking *}
     9.6  
     9.7 -
     9.8  definition test_SCT_witness :: "nat acg \<Rightarrow> nat acg \<Rightarrow> bool"
     9.9  where
    9.10    "test_SCT_witness A T = 
    9.11 @@ -155,7 +154,6 @@
    9.12            n \<noteq> m \<or> G * G \<noteq> G \<or> 
    9.13           (\<exists>(p::nat,e,q)\<in>dest_graph G. p = q \<and> e = LESS)))"
    9.14  
    9.15 -
    9.16  lemma no_bad_graphs_ucl:
    9.17    assumes "A \<le> B"
    9.18    assumes "no_bad_graphs B"
    9.19 @@ -164,8 +162,6 @@
    9.20    unfolding no_bad_graphs_def has_edge_def graph_leq_def 
    9.21    by blast
    9.22  
    9.23 -
    9.24 -
    9.25  lemma SCT'_witness:
    9.26    assumes a: "test_SCT_witness A T"
    9.27    shows "SCT' A"
    9.28 @@ -184,14 +180,6 @@
    9.29      by (rule no_bad_graphs_ucl)
    9.30  qed
    9.31  
    9.32 -
    9.33 -code_modulename SML
    9.34 -  Graphs SCT
    9.35 -  Kleene_Algebras SCT
    9.36 -  Implementation SCT
    9.37 -
    9.38 -(* FIXME
    9.39 -export_code test_SCT in SML
    9.40 -*)
    9.41 +(* ML {* @{code test_SCT} *} *)
    9.42  
    9.43  end
    10.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    10.2 +++ b/src/HOL/ex/Code_Antiq.thy	Wed Jul 02 07:12:17 2008 +0200
    10.3 @@ -0,0 +1,84 @@
    10.4 +(*  Title:      HOL/ex/Code_Antiq.thy
    10.5 +    ID:         $Id$
    10.6 +    Author:     Florian Haftmann
    10.7 +*)
    10.8 +
    10.9 +header {* A simple certificate check as toy example for the code antiquotation *}
   10.10 +
   10.11 +theory Code_Antiq
   10.12 +imports Plain
   10.13 +begin
   10.14 +
   10.15 +lemma div_cert1:
   10.16 +  fixes n m q r :: nat
   10.17 +  assumes "r < m"
   10.18 +    and "0 < m"
   10.19 +    and "n = m * q + r"
   10.20 +  shows "n div m = q"
   10.21 +using assms by (simp add: div_mult_self2 add_commute)
   10.22 +
   10.23 +lemma div_cert2:
   10.24 +  fixes n :: nat
   10.25 +  shows "n div 0 = 0"
   10.26 +by simp
   10.27 +
   10.28 +ML {*
   10.29 +local
   10.30 +
   10.31 +fun code_of_val k = if k <= 0 then @{code "0::nat"}
   10.32 +  else @{code Suc} (code_of_val (k - 1));
   10.33 +
   10.34 +fun val_of_code @{code "0::nat"} = 0
   10.35 +  | val_of_code (@{code Suc} n) = val_of_code n + 1;
   10.36 +
   10.37 +val term_of_code = HOLogic.mk_nat o val_of_code;
   10.38 +
   10.39 +infix 9 &$;
   10.40 +val op &$ = uncurry Thm.capply;
   10.41 +
   10.42 +val simpset = HOL_ss addsimps
   10.43 +  @{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)}
   10.44 +
   10.45 +fun prove prop = Goal.prove_internal [] (@{cterm Trueprop} &$ prop)
   10.46 +  (K (ALLGOALS (Simplifier.simp_tac simpset))); (*FIXME*)
   10.47 +
   10.48 +in
   10.49 +
   10.50 +fun simp_div ctxt ct_n ct_m =
   10.51 +  let
   10.52 +    val m = HOLogic.dest_nat (Thm.term_of ct_m);
   10.53 +  in if m = 0 then Drule.instantiate'[] [SOME ct_n] @{thm div_cert2} else
   10.54 +    let
   10.55 +      val thy = ProofContext.theory_of ctxt;
   10.56 +      val n = HOLogic.dest_nat (Thm.term_of ct_n);
   10.57 +      val c_n = code_of_val n;
   10.58 +      val c_m = code_of_val m;
   10.59 +      val (c_q, c_r) = @{code divmod} c_n c_m;
   10.60 +      val t_q = term_of_code c_q;
   10.61 +      val t_r = term_of_code c_r;
   10.62 +      val ct_q = Thm.cterm_of thy t_q;
   10.63 +      val ct_r = Thm.cterm_of thy t_r;
   10.64 +      val thm_r = prove (@{cterm "op < \<Colon> nat \<Rightarrow> _"} &$ ct_r &$ ct_m);
   10.65 +      val thm_m = prove (@{cterm "(op < \<Colon> nat \<Rightarrow> _) 0"} &$ ct_m);
   10.66 +      val thm_n = prove (@{cterm "(op = \<Colon> nat \<Rightarrow> _)"} &$ ct_n
   10.67 +        &$ (@{cterm "(op + \<Colon> nat \<Rightarrow> _)"}
   10.68 +          &$ (@{cterm "(op * \<Colon> nat \<Rightarrow> _)"} &$ ct_m &$ ct_q) &$ ct_r));
   10.69 +    in @{thm div_cert1} OF [thm_r, thm_m, thm_n] end
   10.70 +  end;
   10.71 +
   10.72 +end;
   10.73 +*}
   10.74 +
   10.75 +ML_val {*
   10.76 +  simp_div @{context}
   10.77 +    @{cterm "Suc (Suc (Suc (Suc (Suc 0))))"}
   10.78 +    @{cterm "(Suc (Suc 0))"}
   10.79 +*}
   10.80 +
   10.81 +ML_val {*
   10.82 +  simp_div @{context}
   10.83 +    (Thm.cterm_of @{theory} (HOLogic.mk_nat 170))
   10.84 +    (Thm.cterm_of @{theory} (HOLogic.mk_nat 42))
   10.85 +*}
   10.86 +
   10.87 +end
   10.88 \ No newline at end of file
    11.1 --- a/src/HOL/ex/ROOT.ML	Wed Jul 02 07:11:57 2008 +0200
    11.2 +++ b/src/HOL/ex/ROOT.ML	Wed Jul 02 07:12:17 2008 +0200
    11.3 @@ -57,7 +57,8 @@
    11.4    "Adder",
    11.5    "Classical",
    11.6    "set",
    11.7 -  "Meson_Test"
    11.8 +  "Meson_Test",
    11.9 +  "Code_Antiq"
   11.10  ];
   11.11  
   11.12  setmp Proofterm.proofs 2 time_use_thy "Hilbert_Classical";
    12.1 --- a/src/Tools/code/code_target.ML	Wed Jul 02 07:11:57 2008 +0200
    12.2 +++ b/src/Tools/code/code_target.ML	Wed Jul 02 07:12:17 2008 +0200
    12.3 @@ -71,7 +71,7 @@
    12.4    | enum_default default sep opn cls xs = Pretty.enum sep opn cls xs;
    12.5  
    12.6  datatype destination = Compile | Export | File of Path.T | String of string list;
    12.7 -type serialization = destination -> string option;
    12.8 +type serialization = destination -> (string * string list) option;
    12.9  
   12.10  val code_width = ref 80; (*FIXME after Pretty module no longer depends on print mode*)
   12.11  fun code_setmp f = PrintMode.setmp [] (Pretty.setmp_margin (!code_width) f);
   12.12 @@ -82,7 +82,7 @@
   12.13  fun compile f = (code_setmp f Compile; ());
   12.14  fun export f = (code_setmp f Export; ());
   12.15  fun file p f = (code_setmp f (File p); ());
   12.16 -fun string cs f = the (code_setmp f (String cs));
   12.17 +fun string cs f = fst (the (code_setmp f (String cs)));
   12.18  
   12.19  fun stmt_names_of_destination (String stmts) = stmts
   12.20    | stmt_names_of_destination _ = [];
   12.21 @@ -1194,7 +1194,7 @@
   12.22          error ("Unknown statement name: " ^ labelled_name name);
   12.23    in (deresolver, nodes) end;
   12.24  
   12.25 -fun serialize_ml compile pr_module pr_stmt projection raw_module_name labelled_name reserved_names includes raw_module_alias
   12.26 +fun serialize_ml compile pr_module pr_stmt raw_module_name labelled_name reserved_names includes raw_module_alias
   12.27    _ syntax_tyco syntax_const program cs destination =
   12.28    let
   12.29      val is_cons = CodeThingol.is_cons program;
   12.30 @@ -1225,20 +1225,29 @@
   12.31      fun output Compile = K NONE o compile o code_of_pretty
   12.32        | output Export = K NONE o code_writeln
   12.33        | output (File file) = K NONE o File.write file o code_of_pretty
   12.34 -      | output (String _) = SOME o code_of_pretty;
   12.35 -  in projection (output destination p) cs' end;
   12.36 +      | output (String _) = SOME o rpair cs' o code_of_pretty;
   12.37 +  in output destination p end;
   12.38  
   12.39  end; (*local*)
   12.40  
   12.41 +(* ML (system language) code for evaluation and instrumentalization *)
   12.42 +
   12.43 +fun ml_code_of thy program cs = mount_serializer thy
   12.44 +  (SOME (fn _ => fn [] => serialize_ml (K ()) (K Pretty.chunks) pr_sml_stmt (SOME "")))
   12.45 +    target_SML NONE [] program cs (String [])
   12.46 +  |> the;
   12.47 +
   12.48 +(* generic entry points for SML/OCaml *)
   12.49 +
   12.50  fun isar_seri_sml module_name =
   12.51    parse_args (Scan.succeed ())
   12.52    #> (fn () => serialize_ml (use_text (1, "generated code") Output.ml_output false)
   12.53 -      pr_sml_module pr_sml_stmt K module_name);
   12.54 +      pr_sml_module pr_sml_stmt module_name);
   12.55  
   12.56  fun isar_seri_ocaml module_name =
   12.57    parse_args (Scan.succeed ())
   12.58    #> (fn () => serialize_ml (fn _ => error "OCaml: no internal compilation")
   12.59 -      pr_ocaml_module pr_ocaml_stmt K module_name);
   12.60 +      pr_ocaml_module pr_ocaml_stmt module_name);
   12.61  
   12.62  
   12.63  (** Haskell serializer **)
   12.64 @@ -1640,7 +1649,7 @@
   12.65      fun output Compile = error ("Haskell: no internal compilation")
   12.66        | output Export = K NONE o map (code_writeln o snd)
   12.67        | output (File destination) = K NONE o map (write_module destination)
   12.68 -      | output (String _) = SOME o cat_lines o map (code_of_pretty o snd);
   12.69 +      | output (String _) = SOME o rpair [] o cat_lines o map (code_of_pretty o snd);
   12.70    in
   12.71      output destination (map (uncurry pr_module) includes
   12.72        @ map serialize_module (Symtab.dest hs_program))
   12.73 @@ -1813,13 +1822,6 @@
   12.74  
   12.75  (* evaluation *)
   12.76  
   12.77 -fun code_antiq_serializer module [] = serialize_ml (K ()) (K Pretty.chunks) pr_sml_stmt
   12.78 -  (fn SOME s => fn cs => SOME ("let\n" ^ s ^ "\nin fn () => " ^ enclose "(" ")" (commas cs) ^ " end"))
   12.79 -  (SOME "Isabelle_Eval");
   12.80 -
   12.81 -fun sml_code_of thy program cs = mount_serializer thy (SOME code_antiq_serializer) target_SML NONE [] program cs (String [])
   12.82 -  |> the;
   12.83 -
   12.84  fun eval eval'' term_of reff thy ct args =
   12.85    let
   12.86      val _ = if null (term_frees (term_of ct)) then () else error ("Term "
   12.87 @@ -1832,8 +1834,9 @@
   12.88          val program' = program
   12.89            |> Graph.new_node (CodeName.value_name, CodeThingol.Fun (([], ty), [(([], t), Drule.dummy_thm)]))
   12.90            |> fold (curry Graph.add_edge CodeName.value_name) deps;
   12.91 -        val value_code = sml_code_of thy program' [CodeName.value_name] ;
   12.92 -        val sml_code = space_implode " " (value_code :: "()" :: map (enclose "(" ")") args);
   12.93 +        val (value_code, [value_name']) = ml_code_of thy program' [CodeName.value_name];
   12.94 +        val sml_code = "let\n" ^ value_code ^ "\nin " ^ value_name'
   12.95 +          ^ space_implode " " (map (enclose "(" ")") args) ^ " end";
   12.96        in ML_Context.evaluate Output.ml_output false reff sml_code end;
   12.97    in eval'' thy (fn t => (t, eval')) ct end;
   12.98  
   12.99 @@ -1843,11 +1846,50 @@
  12.100  
  12.101  (* instrumentalization by antiquotation *)
  12.102  
  12.103 -val ml_code_antiq = Args.theory -- Scan.repeat1 Args.term >> (fn (thy, ts) =>
  12.104 +local
  12.105 +
  12.106 +structure CodeAntiqData = ProofDataFun
  12.107 +(
  12.108 +  type T = string list * (bool * string);
  12.109 +  fun init _ = ([], (true, ""));
  12.110 +);
  12.111 +
  12.112 +val is_first_occ = fst o snd o CodeAntiqData.get;
  12.113 +
  12.114 +fun register_const const ctxt =
  12.115 +  let
  12.116 +    val (consts, (_, struct_name)) = CodeAntiqData.get ctxt;
  12.117 +    val (struct_name', ctxt') = if struct_name = ""
  12.118 +      then ML_Antiquote.variant "Code" ctxt
  12.119 +      else (struct_name, ctxt);
  12.120 +  in CodeAntiqData.put (insert (op =) const consts, (false, struct_name')) ctxt' end;
  12.121 +
  12.122 +fun print_code thy struct_name is_first const ctxt =
  12.123    let
  12.124 -    val cs = map (CodeUnit.check_const thy) ts;
  12.125 -    val (cs', program) = CodeThingol.consts_program thy cs;
  12.126 -  in sml_code_of thy program cs' ^ " ()" end);
  12.127 +    val (consts, (_, struct_code_name)) = CodeAntiqData.get ctxt;
  12.128 +    val (consts', program) = CodeThingol.consts_program thy consts;
  12.129 +    val (raw_ml_code, consts'') = ml_code_of thy program consts';
  12.130 +    val _ = if length consts <> length consts'' then
  12.131 +      error ("One of the constants " ^ commas (map (quote o CodeUnit.string_of_const thy) consts)
  12.132 +        ^ "\nhas a user-defined serialization") else ();
  12.133 +    val const'' = NameSpace.append (NameSpace.append struct_name struct_code_name)
  12.134 +      ((the o AList.lookup (op =) (consts ~~ consts'')) const);
  12.135 +    val ml_code = if is_first then "\nstructure " ^ struct_code_name
  12.136 +        ^ " =\nstruct\n\n" ^ raw_ml_code ^ "\nend;\n\n"
  12.137 +      else "";
  12.138 +  in (ml_code, const'') end;
  12.139 +
  12.140 +in
  12.141 +
  12.142 +fun ml_code_antiq raw_const {struct_name, background} =
  12.143 +  let
  12.144 +    val thy = ProofContext.theory_of background;
  12.145 +    val const = CodeUnit.check_const thy raw_const;
  12.146 +    val is_first = is_first_occ background;
  12.147 +    val background' = register_const const background;
  12.148 +  in (print_code thy struct_name is_first const, background') end;
  12.149 +
  12.150 +end; (*local*)
  12.151  
  12.152  
  12.153  (* code presentation *)
  12.154 @@ -2291,7 +2333,7 @@
  12.155      | NONE => error ("Bad directive " ^ quote cmd)))
  12.156    handle TOPLEVEL_ERROR => OS.Process.exit OS.Process.failure;
  12.157  
  12.158 -val _ = ML_Antiquote.value "code" ml_code_antiq;
  12.159 +val _ = ML_Context.add_antiq "code" (Args.term >> ml_code_antiq);
  12.160  
  12.161  
  12.162  (* serializer setup, including serializer defaults *)