overloaded definitions accompanied by explicit constants
authorhaftmann
Fri Aug 24 14:14:20 2007 +0200 (2007-08-24)
changeset 24423ae9cd0e92423
parent 24422 c0b5ff9e9e4d
child 24424 90500d3b5b5d
overloaded definitions accompanied by explicit constants
src/HOL/Complex/ex/ReflectedFerrack.thy
src/HOL/Complex/ex/linreif.ML
src/HOL/Complex/ex/mireif.ML
src/HOL/Lambda/WeakNorm.thy
src/HOL/Library/Efficient_Nat.thy
src/HOL/Library/Eval.thy
src/HOL/Library/Executable_Set.thy
src/HOL/Library/Graphs.thy
src/HOL/Library/ML_Int.thy
src/HOL/Library/Pretty_Int.thy
src/HOL/Library/SCT_Implementation.thy
src/HOL/Tools/datatype_abs_proofs.ML
src/HOL/Tools/datatype_codegen.ML
src/HOL/Tools/datatype_package.ML
src/HOL/ex/Classpackage.thy
src/HOL/ex/Codegenerator.thy
src/HOL/ex/Eval_Examples.thy
src/HOL/ex/ExecutableContent.thy
src/HOL/ex/coopereif.ML
src/Pure/Isar/ROOT.ML
src/Pure/Isar/class.ML
src/Pure/Isar/code.ML
src/Pure/Isar/code_unit.ML
src/Pure/Isar/isar_syn.ML
src/Tools/code/code_funcgr.ML
src/Tools/code/code_name.ML
src/Tools/code/code_package.ML
src/Tools/code/code_target.ML
src/Tools/nbe.ML
     1.1 --- a/src/HOL/Complex/ex/ReflectedFerrack.thy	Fri Aug 24 14:14:18 2007 +0200
     1.2 +++ b/src/HOL/Complex/ex/ReflectedFerrack.thy	Fri Aug 24 14:14:20 2007 +0200
     1.3 @@ -1954,7 +1954,6 @@
     1.4    let ?res = "disj ?mp (disj ?pp ?ep)"
     1.5    from rminusinf_bound0[OF lq] rplusinf_bound0[OF lq] ep_nb
     1.6    have nbth: "bound0 ?res" by auto
     1.7 -  thm rlfm_I[OF simpfm_qf[OF qf]]
     1.8  
     1.9    from conjunct1[OF rlfm_I[OF simpfm_qf[OF qf]]] simpfm  
    1.10  
    1.11 @@ -1997,7 +1996,7 @@
    1.12  
    1.13  use "linreif.ML"
    1.14  oracle linr_oracle ("term") = ReflectedFerrack.linrqe_oracle
    1.15 -use"linrtac.ML"
    1.16 -setup "LinrTac.setup"
    1.17 +use "linrtac.ML"
    1.18 +setup LinrTac.setup
    1.19  
    1.20  end
     2.1 --- a/src/HOL/Complex/ex/linreif.ML	Fri Aug 24 14:14:18 2007 +0200
     2.2 +++ b/src/HOL/Complex/ex/linreif.ML	Fri Aug 24 14:14:20 2007 +0200
     2.3 @@ -44,16 +44,16 @@
     2.4      case t of 
     2.5  	Const("True",_) => T
     2.6        | Const("False",_) => F
     2.7 -      | Const(@{const_name HOL.less},_)$t1$t2 => Lta (Sub (num_of_term vs t1,num_of_term vs t2))
     2.8 -      | Const(@{const_name HOL.less_eq},_)$t1$t2 => Lea (Sub (num_of_term vs t1,num_of_term vs t2))
     2.9 +      | Const(@{const_name HOL.less},_)$t1$t2 => Lt (Sub (num_of_term vs t1,num_of_term vs t2))
    2.10 +      | Const(@{const_name HOL.less_eq},_)$t1$t2 => Le (Sub (num_of_term vs t1,num_of_term vs t2))
    2.11        | Const("op =",eqT)$t1$t2 => 
    2.12  	if (domain_type eqT = rT)
    2.13 -	then Eqa (Sub (num_of_term vs t1,num_of_term vs t2)) 
    2.14 -	else Iffa(fm_of_term vs t1,fm_of_term vs t2)
    2.15 +	then Eq (Sub (num_of_term vs t1,num_of_term vs t2)) 
    2.16 +	else Iff(fm_of_term vs t1,fm_of_term vs t2)
    2.17        | Const("op &",_)$t1$t2 => And(fm_of_term vs t1,fm_of_term vs t2)
    2.18        | Const("op |",_)$t1$t2 => Or(fm_of_term vs t1,fm_of_term vs t2)
    2.19 -      | Const("op -->",_)$t1$t2 => Impa(fm_of_term vs t1,fm_of_term vs t2)
    2.20 -      | Const("Not",_)$t' => Nota(fm_of_term vs t')
    2.21 +      | Const("op -->",_)$t1$t2 => Imp(fm_of_term vs t1,fm_of_term vs t2)
    2.22 +      | Const("Not",_)$t' => Not(fm_of_term vs t')
    2.23        | Const("Ex",_)$Term.Abs(xn,xT,p) => 
    2.24  	E(fm_of_term (map (fn(v,n) => (v,1+ n)) vs) p)
    2.25        | Const("All",_)$Term.Abs(xn,xT,p) => 
    2.26 @@ -91,22 +91,22 @@
    2.27      case t of 
    2.28  	T => HOLogic.true_const 
    2.29        | F => HOLogic.false_const
    2.30 -      | Lta t => Const(@{const_name HOL.less},[rT,rT] ---> bT)$
    2.31 +      | Lt t => Const(@{const_name HOL.less},[rT,rT] ---> bT)$
    2.32  			   (term_of_num vs t)$ rzero
    2.33 -      | Lea t => Const(@{const_name HOL.less_eq},[rT,rT] ---> bT)$
    2.34 +      | Le t => Const(@{const_name HOL.less_eq},[rT,rT] ---> bT)$
    2.35  			  (term_of_num vs t)$ rzero
    2.36 -      | Gta t => Const(@{const_name HOL.less},[rT,rT] ---> bT)$
    2.37 +      | Gt t => Const(@{const_name HOL.less},[rT,rT] ---> bT)$
    2.38  			   rzero $(term_of_num vs t)
    2.39 -      | Gea t => Const(@{const_name HOL.less_eq},[rT,rT] ---> bT)$
    2.40 +      | Ge t => Const(@{const_name HOL.less_eq},[rT,rT] ---> bT)$
    2.41  			  rzero $(term_of_num vs t)
    2.42 -      | Eqa t => Const("op =",[rT,rT] ---> bT)$
    2.43 +      | Eq t => Const("op =",[rT,rT] ---> bT)$
    2.44  			   (term_of_num vs t)$ rzero
    2.45 -      | NEq t => term_of_fm vs (Nota (Eqa t))
    2.46 -      | Nota t' => HOLogic.Not$(term_of_fm vs t')
    2.47 +      | NEq t => term_of_fm vs (Not (Eq t))
    2.48 +      | Not t' => HOLogic.Not$(term_of_fm vs t')
    2.49        | And(t1,t2) => HOLogic.conj$(term_of_fm vs t1)$(term_of_fm vs t2)
    2.50        | Or(t1,t2) => HOLogic.disj$(term_of_fm vs t1)$(term_of_fm vs t2)
    2.51 -      | Impa(t1,t2) => HOLogic.imp$(term_of_fm vs t1)$(term_of_fm vs t2)
    2.52 -      | Iffa(t1,t2) => (HOLogic.eq_const bT)$(term_of_fm vs t1)$
    2.53 +      | Imp(t1,t2) => HOLogic.imp$(term_of_fm vs t1)$(term_of_fm vs t2)
    2.54 +      | Iff(t1,t2) => (HOLogic.eq_const bT)$(term_of_fm vs t1)$
    2.55  					   (term_of_fm vs t2)
    2.56        | _ => error "If this is raised, Isabelle/HOL or generate_code is inconsistent!";
    2.57  
     3.1 --- a/src/HOL/Complex/ex/mireif.ML	Fri Aug 24 14:14:18 2007 +0200
     3.2 +++ b/src/HOL/Complex/ex/mireif.ML	Fri Aug 24 14:14:20 2007 +0200
     3.3 @@ -42,18 +42,18 @@
     3.4      case t of 
     3.5          Const("True",_) => T
     3.6        | Const("False",_) => F
     3.7 -      | Const(@{const_name HOL.less},_)$t1$t2 => Lta (Sub (num_of_term vs t1,num_of_term vs t2))
     3.8 -      | Const(@{const_name HOL.less_eq},_)$t1$t2 => Lea (Sub (num_of_term vs t1,num_of_term vs t2))
     3.9 +      | Const(@{const_name HOL.less},_)$t1$t2 => Lt (Sub (num_of_term vs t1,num_of_term vs t2))
    3.10 +      | Const(@{const_name HOL.less_eq},_)$t1$t2 => Le (Sub (num_of_term vs t1,num_of_term vs t2))
    3.11        | Const (@{const_name "MIR.rdvd"},_ )$ (Const("RealDef.real",_) $ (Const(@{const_name "Numeral.number_of"},_)$t1))$t2 => 
    3.12 -        Dvda (HOLogic.dest_numeral t1, num_of_term vs t2)
    3.13 +        Dvd (HOLogic.dest_numeral t1, num_of_term vs t2)
    3.14        | Const("op =",eqT)$t1$t2 => 
    3.15          if (domain_type eqT = @{typ real})
    3.16 -        then Eqa (Sub (num_of_term vs t1, num_of_term vs t2)) 
    3.17 -        else Iffa (fm_of_term vs t1, fm_of_term vs t2)
    3.18 +        then Eq (Sub (num_of_term vs t1, num_of_term vs t2)) 
    3.19 +        else Iff (fm_of_term vs t1, fm_of_term vs t2)
    3.20        | Const("op &",_)$t1$t2 => And (fm_of_term vs t1, fm_of_term vs t2)
    3.21        | Const("op |",_)$t1$t2 => Or (fm_of_term vs t1, fm_of_term vs t2)
    3.22 -      | Const("op -->",_)$t1$t2 => Impa (fm_of_term vs t1, fm_of_term vs t2)
    3.23 -      | Const("Not",_)$t' => Nota (fm_of_term vs t')
    3.24 +      | Const("op -->",_)$t1$t2 => Imp (fm_of_term vs t1, fm_of_term vs t2)
    3.25 +      | Const("Not",_)$t' => Not (fm_of_term vs t')
    3.26        | Const("Ex",_)$Abs(xn,xT,p) => 
    3.27          E (fm_of_term (map (fn (v, n) => (v, Suc n)) vs) p)
    3.28        | Const("All",_)$Abs(xn,xT,p) => 
    3.29 @@ -93,19 +93,19 @@
    3.30      case t of 
    3.31          T => HOLogic.true_const 
    3.32        | F => HOLogic.false_const
    3.33 -      | Lta t => @{term "op <:: real => _"} $ term_of_num vs t $ rzero
    3.34 -      | Lea t => @{term "op <=:: real => _"} $ term_of_num vs t $ rzero
    3.35 -      | Gta t => @{term "op <:: real => _"}$ rzero $ term_of_num vs t
    3.36 -      | Gea t => @{term "op <=:: real => _"} $ rzero $ term_of_num vs t
    3.37 -      | Eqa t => @{term "op = :: real => _"}$ term_of_num vs t $ rzero
    3.38 -      | NEq t => term_of_fm vs (Nota (Eqa t))
    3.39 -      | NDvd (i,t) => term_of_fm vs (Nota (Dvda (i,t)))
    3.40 -      | Dvda (i,t) => @{term "op rdvd"} $ term_of_num vs (C i) $ term_of_num vs t
    3.41 -      | Nota t' => HOLogic.Not$(term_of_fm vs t')
    3.42 +      | Lt t => @{term "op <:: real => _"} $ term_of_num vs t $ rzero
    3.43 +      | Le t => @{term "op <=:: real => _"} $ term_of_num vs t $ rzero
    3.44 +      | Gt t => @{term "op <:: real => _"}$ rzero $ term_of_num vs t
    3.45 +      | Ge t => @{term "op <=:: real => _"} $ rzero $ term_of_num vs t
    3.46 +      | Eq t => @{term "op = :: real => _"}$ term_of_num vs t $ rzero
    3.47 +      | NEq t => term_of_fm vs (Not (Eq t))
    3.48 +      | NDvd (i,t) => term_of_fm vs (Not (Dvd (i,t)))
    3.49 +      | Dvd (i,t) => @{term "op rdvd"} $ term_of_num vs (C i) $ term_of_num vs t
    3.50 +      | Not t' => HOLogic.Not$(term_of_fm vs t')
    3.51        | And(t1,t2) => HOLogic.conj $ term_of_fm vs t1 $ term_of_fm vs t2
    3.52        | Or(t1,t2) => HOLogic.disj $ term_of_fm vs t1 $ term_of_fm vs t2
    3.53 -      | Impa(t1,t2) => HOLogic.imp $ term_of_fm vs t1 $ term_of_fm vs t2
    3.54 -      | Iffa(t1,t2) => HOLogic.mk_eq (term_of_fm vs t1, term_of_fm vs t2)
    3.55 +      | Imp(t1,t2) => HOLogic.imp $ term_of_fm vs t1 $ term_of_fm vs t2
    3.56 +      | Iff(t1,t2) => HOLogic.mk_eq (term_of_fm vs t1, term_of_fm vs t2)
    3.57        | _ => error "If this is raised, Isabelle/HOL or generate_code is inconsistent!";
    3.58  
    3.59  (* The oracle *)
     4.1 --- a/src/HOL/Lambda/WeakNorm.thy	Fri Aug 24 14:14:18 2007 +0200
     4.2 +++ b/src/HOL/Lambda/WeakNorm.thy	Fri Aug 24 14:14:20 2007 +0200
     4.3 @@ -614,13 +614,13 @@
     4.4  fun typing_of_term Ts e (Bound i) =
     4.5        Norm.Vara (e, nat_of_int i, dBtype_of_typ (nth Ts i))
     4.6    | typing_of_term Ts e (t $ u) = (case fastype_of1 (Ts, t) of
     4.7 -        Type ("fun", [T, U]) => Norm.Appaa (e, dB_of_term t,
     4.8 +        Type ("fun", [T, U]) => Norm.Appb (e, dB_of_term t,
     4.9            dBtype_of_typ T, dBtype_of_typ U, dB_of_term u,
    4.10            typing_of_term Ts e t, typing_of_term Ts e u)
    4.11        | _ => error "typing_of_term: function type expected")
    4.12    | typing_of_term Ts e (Abs (s, T, t)) =
    4.13        let val dBT = dBtype_of_typ T
    4.14 -      in Norm.Absaa (e, dBT, dB_of_term t,
    4.15 +      in Norm.Absb (e, dBT, dB_of_term t,
    4.16          dBtype_of_typ (fastype_of1 (T :: Ts, t)),
    4.17          typing_of_term (T :: Ts) (Norm.shift e Norm.Zero_nat dBT) t)
    4.18        end
     5.1 --- a/src/HOL/Library/Efficient_Nat.thy	Fri Aug 24 14:14:18 2007 +0200
     5.2 +++ b/src/HOL/Library/Efficient_Nat.thy	Fri Aug 24 14:14:20 2007 +0200
     5.3 @@ -63,6 +63,8 @@
     5.4  lemma eq_nat_of_int: "int' n = x \<Longrightarrow> n = nat_of_int x"
     5.5  by (erule subst, simp only: nat_of_int_int)
     5.6  
     5.7 +code_datatype nat_of_int
     5.8 +
     5.9  text {*
    5.10    Case analysis on natural numbers is rephrased using a conditional
    5.11    expression:
    5.12 @@ -161,8 +163,6 @@
    5.13    @{typ nat} is no longer a datatype but embedded into the integers.
    5.14  *}
    5.15  
    5.16 -code_datatype nat_of_int
    5.17 -
    5.18  code_type nat
    5.19    (SML "IntInf.int")
    5.20    (OCaml "Big'_int.big'_int")
     6.1 --- a/src/HOL/Library/Eval.thy	Fri Aug 24 14:14:18 2007 +0200
     6.2 +++ b/src/HOL/Library/Eval.thy	Fri Aug 24 14:14:20 2007 +0200
     6.3 @@ -52,7 +52,7 @@
     6.4    fun hook specs =
     6.5      DatatypeCodegen.prove_codetypes_arities (Class.intro_classes_tac [])
     6.6        (map (fn (tyco, (is_dt, _)) => (tyco, is_dt)) specs)
     6.7 -      [TypOf.class_typ_of] mk ((K o K) I)
     6.8 +      [TypOf.class_typ_of] mk ((K o K) (fold (Code.add_func true)))
     6.9  in DatatypeCodegen.add_codetypes_hook_bootstrap hook end
    6.10  *}
    6.11  
    6.12 @@ -98,7 +98,7 @@
    6.13      PureThy.add_thmss [((name, thms), atts)] #-> (fn [thms] => pair (name, thms));
    6.14    fun thy_def ((name, atts), t) =
    6.15      PureThy.add_defs_i false [((name, t), atts)] #-> (fn [thm] => pair (name, thm));
    6.16 -  fun mk arities css thy =
    6.17 +  fun mk arities css _ thy =
    6.18      let
    6.19        val (_, asorts, _) :: _ = arities;
    6.20        val vs = Name.names Name.context "'a" asorts;
     7.1 --- a/src/HOL/Library/Executable_Set.thy	Fri Aug 24 14:14:18 2007 +0200
     7.2 +++ b/src/HOL/Library/Executable_Set.thy	Fri Aug 24 14:14:20 2007 +0200
     7.3 @@ -11,24 +11,10 @@
     7.4  
     7.5  subsection {* Definitional rewrites *}
     7.6  
     7.7 -instance set :: (eq) eq ..
     7.8 -
     7.9  lemma [code target: Set]:
    7.10    "A = B \<longleftrightarrow> A \<subseteq> B \<and> B \<subseteq> A"
    7.11    by blast
    7.12  
    7.13 -lemma [code func]:
    7.14 -  "(A\<Colon>'a\<Colon>eq set) = B \<longleftrightarrow> A \<subseteq> B \<and> B \<subseteq> A"
    7.15 -  by blast
    7.16 -
    7.17 -lemma [code func]:
    7.18 -  "(A\<Colon>'a\<Colon>eq set) \<subseteq> B \<longleftrightarrow> (\<forall>x\<in>A. x \<in> B)"
    7.19 -  unfolding subset_def ..
    7.20 -
    7.21 -lemma [code func]:
    7.22 -  "(A\<Colon>'a\<Colon>eq set) \<subset> B \<longleftrightarrow> A \<subseteq> B \<and> A \<noteq> B"
    7.23 -  by blast
    7.24 -
    7.25  lemma [code]:
    7.26    "a \<in> A \<longleftrightarrow> (\<exists>x\<in>A. x = a)"
    7.27    unfolding bex_triv_one_point1 ..
    7.28 @@ -37,8 +23,6 @@
    7.29    filter_set :: "('a \<Rightarrow> bool) \<Rightarrow> 'a set \<Rightarrow> 'a set" where
    7.30    "filter_set P xs = {x\<in>xs. P x}"
    7.31  
    7.32 -lemmas [symmetric, code inline] = filter_set_def
    7.33 -
    7.34  
    7.35  subsection {* Operations on lists *}
    7.36  
    7.37 @@ -256,74 +240,6 @@
    7.38  nonfix subset;
    7.39  *}
    7.40  
    7.41 -code_modulename SML
    7.42 -  Executable_Set List
    7.43 -  Set List
    7.44 -
    7.45 -code_modulename OCaml
    7.46 -  Executable_Set List
    7.47 -  Set List
    7.48 -
    7.49 -code_modulename Haskell
    7.50 -  Executable_Set List
    7.51 -  Set List
    7.52 -
    7.53 -definition [code inline]:
    7.54 -  "empty_list = []"
    7.55 -
    7.56 -lemma [code func]:
    7.57 -  "insert (x \<Colon> 'a\<Colon>eq) = insert x" ..
    7.58 -
    7.59 -lemma [code func]:
    7.60 -  "(xs \<Colon> 'a\<Colon>eq set) \<union> ys = xs \<union> ys" ..
    7.61 -
    7.62 -lemma [code func]:
    7.63 -  "(xs \<Colon> 'a\<Colon>eq set) \<inter> ys = xs \<inter> ys" ..
    7.64 -
    7.65 -lemma [code func]:
    7.66 -  "(op -) (xs \<Colon> 'a\<Colon>eq set) = (op -) (xs \<Colon> 'a\<Colon>eq set)" ..
    7.67 -
    7.68 -lemma [code func]:
    7.69 -  "image (f \<Colon> 'a \<Rightarrow> 'b\<Colon>eq) = image f" ..
    7.70 -
    7.71 -lemma [code func]:
    7.72 -  "Union (xss \<Colon> 'a\<Colon>eq set set) = Union xss" ..
    7.73 -
    7.74 -lemma [code func]:
    7.75 -  "Inter (xss \<Colon> 'a\<Colon>eq set set) = Inter xss" ..
    7.76 -
    7.77 -lemma [code func]:
    7.78 -  "UNION xs (f \<Colon> 'a \<Rightarrow> 'b\<Colon>eq set) = UNION xs f" ..
    7.79 -
    7.80 -lemma [code func]:
    7.81 -  "INTER xs (f \<Colon> 'a \<Rightarrow> 'b\<Colon>eq set) = INTER xs f" ..
    7.82 -
    7.83 -lemma [code func]:
    7.84 -  "Ball (xs \<Colon> 'a\<Colon>type set) = Ball xs" ..
    7.85 -
    7.86 -lemma [code func]:
    7.87 -  "Bex (xs \<Colon> 'a\<Colon>type set) = Bex xs" ..
    7.88 -
    7.89 -lemma [code func]:
    7.90 -  "filter_set P (xs \<Colon> 'a\<Colon>type set) = filter_set P xs" ..
    7.91 -
    7.92 -
    7.93 -code_abstype "'a set" "'a list" where
    7.94 -  "{}" \<equiv> empty_list
    7.95 -  insert \<equiv> insertl
    7.96 -  "op \<union>" \<equiv> unionl
    7.97 -  "op \<inter>" \<equiv> intersect
    7.98 -  "op - \<Colon> 'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" \<equiv> subtract'
    7.99 -  image \<equiv> map_distinct
   7.100 -  Union \<equiv> unions
   7.101 -  Inter \<equiv> intersects
   7.102 -  UNION \<equiv> map_union
   7.103 -  INTER \<equiv> map_inter
   7.104 -  Ball \<equiv> Blall
   7.105 -  Bex \<equiv> Blex
   7.106 -  filter_set \<equiv> filter
   7.107 -
   7.108 -
   7.109  subsubsection {* type serializations *}
   7.110  
   7.111  types_code
     8.1 --- a/src/HOL/Library/Graphs.thy	Fri Aug 24 14:14:18 2007 +0200
     8.2 +++ b/src/HOL/Library/Graphs.thy	Fri Aug 24 14:14:20 2007 +0200
     8.3 @@ -6,7 +6,7 @@
     8.4  header {* General Graphs as Sets *}
     8.5  
     8.6  theory Graphs
     8.7 -imports Main SCT_Misc Kleene_Algebras Executable_Set
     8.8 +imports Main SCT_Misc Kleene_Algebras
     8.9  begin
    8.10  
    8.11  subsection {* Basic types, Size Change Graphs *}
     9.1 --- a/src/HOL/Library/ML_Int.thy	Fri Aug 24 14:14:18 2007 +0200
     9.2 +++ b/src/HOL/Library/ML_Int.thy	Fri Aug 24 14:14:20 2007 +0200
     9.3 @@ -170,7 +170,7 @@
     9.4  
     9.5  setup {*
     9.6    CodeTarget.add_pretty_numeral "SML" false
     9.7 -    (@{const_name number_of}, @{typ "int \<Rightarrow> ml_int"})
     9.8 +    @{const_name ml_int_of_int}
     9.9      @{const_name Numeral.B0} @{const_name Numeral.B1}
    9.10      @{const_name Numeral.Pls} @{const_name Numeral.Min}
    9.11      @{const_name Numeral.Bit}
    10.1 --- a/src/HOL/Library/Pretty_Int.thy	Fri Aug 24 14:14:18 2007 +0200
    10.2 +++ b/src/HOL/Library/Pretty_Int.thy	Fri Aug 24 14:14:20 2007 +0200
    10.3 @@ -25,7 +25,7 @@
    10.4  
    10.5  setup {*
    10.6    fold (fn target => CodeTarget.add_pretty_numeral target true
    10.7 -    (@{const_name number_of}, @{typ "int \<Rightarrow> int"})
    10.8 +    @{const_name number_int_inst.number_of_int}
    10.9      @{const_name Numeral.B0} @{const_name Numeral.B1}
   10.10      @{const_name Numeral.Pls} @{const_name Numeral.Min}
   10.11      @{const_name Numeral.Bit}
    11.1 --- a/src/HOL/Library/SCT_Implementation.thy	Fri Aug 24 14:14:18 2007 +0200
    11.2 +++ b/src/HOL/Library/SCT_Implementation.thy	Fri Aug 24 14:14:20 2007 +0200
    11.3 @@ -6,7 +6,7 @@
    11.4  header {* Implemtation of the SCT criterion *}
    11.5  
    11.6  theory SCT_Implementation
    11.7 -imports Executable_Set SCT_Definition SCT_Theorem
    11.8 +imports SCT_Definition SCT_Theorem
    11.9  begin
   11.10  
   11.11  fun edges_match :: "('n \<times> 'e \<times> 'n) \<times> ('n \<times> 'e \<times> 'n) \<Rightarrow> bool"
    12.1 --- a/src/HOL/Tools/datatype_abs_proofs.ML	Fri Aug 24 14:14:18 2007 +0200
    12.2 +++ b/src/HOL/Tools/datatype_abs_proofs.ML	Fri Aug 24 14:14:20 2007 +0200
    12.3 @@ -429,6 +429,7 @@
    12.4          thy
    12.5          |> Class.prove_instance_arity (Class.intro_classes_tac [])
    12.6              [(tyco, replicate n HOLogic.typeS, [HOLogic.class_size])] []
    12.7 +        |> snd
    12.8        end
    12.9  
   12.10      val (size_def_thms, thy') =
    13.1 --- a/src/HOL/Tools/datatype_codegen.ML	Fri Aug 24 14:14:18 2007 +0200
    13.2 +++ b/src/HOL/Tools/datatype_codegen.ML	Fri Aug 24 14:14:20 2007 +0200
    13.3 @@ -26,7 +26,7 @@
    13.4    val prove_codetypes_arities: tactic -> (string * bool) list -> sort
    13.5      -> (arity list -> (string * term list) list -> theory
    13.6        -> ((bstring * Attrib.src list) * term) list * theory)
    13.7 -    -> (arity list -> (string * term list) list -> theory -> theory)
    13.8 +    -> (arity list -> (string * term list) list -> thm list -> theory -> theory)
    13.9      -> theory -> theory
   13.10  
   13.11    val setup: theory -> theory
   13.12 @@ -537,8 +537,13 @@
   13.13  
   13.14  (* registering code types in code generator *)
   13.15  
   13.16 -fun codetype_hook dtspecs =
   13.17 -  fold (fn (dtco, (_, spec)) => Code.add_datatype (dtco, spec)) dtspecs;
   13.18 +fun add_datatype_spec (tyco, (vs, cos)) thy =
   13.19 +  let
   13.20 +    val cs = map (fn (c, tys) => (c, tys ---> Type (tyco, map TFree vs))) cos;
   13.21 +  in try (Code.add_datatype cs) thy |> the_default thy end;
   13.22 +
   13.23 +val codetype_hook =
   13.24 +  fold (fn (dtco, (_, spec)) => add_datatype_spec (dtco, spec));
   13.25  
   13.26  
   13.27  (* instrumentalizing the sort algebra *)
   13.28 @@ -586,7 +591,8 @@
   13.29              f arities css
   13.30              #-> (fn defs =>
   13.31                Class.prove_instance_arity tac arities defs
   13.32 -            #> after_qed arities css))
   13.33 +            #-> (fn defs =>
   13.34 +              after_qed arities css defs)))
   13.35        end;
   13.36  
   13.37  
   13.38 @@ -597,7 +603,7 @@
   13.39      fun add_eq_thms (dtco, (_, (vs, cs))) thy =
   13.40        let
   13.41          val thy_ref = Theory.check_thy thy;
   13.42 -        val const = ("op =", SOME dtco);
   13.43 +        val const = Class.inst_const thy ("op =", dtco);
   13.44          val get_thms = (fn () => get_eq (Theory.deref thy_ref) dtco |> rev);
   13.45        in
   13.46          Code.add_funcl (const, Susp.delay get_thms) thy
   13.47 @@ -605,7 +611,7 @@
   13.48    in
   13.49      prove_codetypes_arities (Class.intro_classes_tac [])
   13.50        (map (fn (tyco, (is_dt, _)) => (tyco, is_dt)) specs)
   13.51 -      [HOLogic.class_eq] ((K o K o pair) []) ((K o K) (fold add_eq_thms specs))
   13.52 +      [HOLogic.class_eq] ((K o K o pair) []) ((K o K o K) (fold add_eq_thms specs))
   13.53    end;
   13.54  
   13.55  
    14.1 --- a/src/HOL/Tools/datatype_package.ML	Fri Aug 24 14:14:18 2007 +0200
    14.2 +++ b/src/HOL/Tools/datatype_package.ML	Fri Aug 24 14:14:20 2007 +0200
    14.3 @@ -567,6 +567,7 @@
    14.4          thy
    14.5          |> Class.prove_instance_arity (Class.intro_classes_tac [])
    14.6              [(tyco, replicate n HOLogic.typeS, [HOLogic.class_size])] []
    14.7 +        |> snd
    14.8        end
    14.9  
   14.10      val thy2' = thy
    15.1 --- a/src/HOL/ex/Classpackage.thy	Fri Aug 24 14:14:18 2007 +0200
    15.2 +++ b/src/HOL/ex/Classpackage.thy	Fri Aug 24 14:14:20 2007 +0200
    15.3 @@ -342,7 +342,7 @@
    15.4  definition "x2 = X (1::int) 2 3"
    15.5  definition "y2 = Y (1::int) 2 3"
    15.6  
    15.7 -export_code x1 x2 y2 in SML module_name Classpackage
    15.8 +export_code mult x1 x2 y2 in SML module_name Classpackage
    15.9    in OCaml file -
   15.10    in Haskell file -
   15.11  
    16.1 --- a/src/HOL/ex/Codegenerator.thy	Fri Aug 24 14:14:18 2007 +0200
    16.2 +++ b/src/HOL/ex/Codegenerator.thy	Fri Aug 24 14:14:20 2007 +0200
    16.3 @@ -8,7 +8,7 @@
    16.4  imports ExecutableContent
    16.5  begin
    16.6  
    16.7 -export_code "*" in SML module_name CodegenTest
    16.8 +export_code * in SML module_name CodegenTest
    16.9    in OCaml file -
   16.10    in Haskell file -
   16.11  
    17.1 --- a/src/HOL/ex/Eval_Examples.thy	Fri Aug 24 14:14:18 2007 +0200
    17.2 +++ b/src/HOL/ex/Eval_Examples.thy	Fri Aug 24 14:14:20 2007 +0200
    17.3 @@ -31,8 +31,8 @@
    17.4  value (overloaded) "(Suc 2 + Suc 0) * Suc 3"
    17.5  value (overloaded) "nat 100"
    17.6  value (overloaded) "(10\<Colon>int) \<le> 12"
    17.7 +value (overloaded) "[]::nat list"
    17.8  value (overloaded) "[(nat 100, ())]"
    17.9 -value (overloaded) "[]::nat list"
   17.10  
   17.11  text {* a fancy datatype *}
   17.12  
    18.1 --- a/src/HOL/ex/ExecutableContent.thy	Fri Aug 24 14:14:18 2007 +0200
    18.2 +++ b/src/HOL/ex/ExecutableContent.thy	Fri Aug 24 14:14:20 2007 +0200
    18.3 @@ -19,7 +19,7 @@
    18.4    List_Prefix
    18.5    Nat_Infinity
    18.6    NatPair
    18.7 -  Nested_Environment
    18.8 +  (*Nested_Environment*)
    18.9    Permutation
   18.10    Primes
   18.11    Product_ord
    19.1 --- a/src/HOL/ex/coopereif.ML	Fri Aug 24 14:14:18 2007 +0200
    19.2 +++ b/src/HOL/ex/coopereif.ML	Fri Aug 24 14:14:20 2007 +0200
    19.3 @@ -37,11 +37,11 @@
    19.4        | Const(@{const_name "Divides.dvd"},_)$t1$t2 => 
    19.5            (Dvd(HOLogic.dest_number t1 |> snd, i_of_term vs t2) handle _ => error "qf_of_term: unsupported dvd")
    19.6        | @{term "op = :: int => _"}$t1$t2 => Eq (Sub (i_of_term vs t1,i_of_term vs t2))
    19.7 -      | @{term "op = :: bool => _ "}$t1$t2 => Iffa(qf_of_term ps vs t1,qf_of_term ps vs t2)
    19.8 +      | @{term "op = :: bool => _ "}$t1$t2 => Iff(qf_of_term ps vs t1,qf_of_term ps vs t2)
    19.9        | Const("op &",_)$t1$t2 => And(qf_of_term ps vs t1,qf_of_term ps vs t2)
   19.10        | Const("op |",_)$t1$t2 => Or(qf_of_term ps vs t1,qf_of_term ps vs t2)
   19.11 -      | Const("op -->",_)$t1$t2 => Impa(qf_of_term ps vs t1,qf_of_term ps vs t2)
   19.12 -      | Const("Not",_)$t' => Nota(qf_of_term ps vs t')
   19.13 +      | Const("op -->",_)$t1$t2 => Imp(qf_of_term ps vs t1,qf_of_term ps vs t2)
   19.14 +      | Const("Not",_)$t' => Not(qf_of_term ps vs t')
   19.15        | Const("Ex",_)$Abs(xn,xT,p) => 
   19.16           let val (xn',p') = variant_abs (xn,xT,p)
   19.17               val vs' = (Free (xn',xT), nat 0) :: (map (fn(v,n) => (v,1 + n)) vs)
   19.18 @@ -102,17 +102,17 @@
   19.19    | Gt t' => @{term "op < :: int => _ "}$ @{term "0::int"}$ term_of_i vs t'
   19.20    | Ge t' => @{term "op <= :: int => _ "}$ @{term "0::int"}$ term_of_i vs t'
   19.21    | Eq t' => @{term "op = :: int => _ "}$ term_of_i vs t'$ @{term "0::int"}
   19.22 -  | NEq t' => term_of_qf ps vs (Nota(Eq t'))
   19.23 +  | NEq t' => term_of_qf ps vs (Not(Eq t'))
   19.24    | Dvd(i,t') => @{term "op dvd :: int => _ "}$ 
   19.25        (HOLogic.mk_number HOLogic.intT i)$(term_of_i vs t')
   19.26 -  | NDvd(i,t')=> term_of_qf ps vs (Nota(Dvd(i,t')))
   19.27 -  | Nota t' => HOLogic.Not$(term_of_qf ps vs t')
   19.28 +  | NDvd(i,t')=> term_of_qf ps vs (Not(Dvd(i,t')))
   19.29 +  | Not t' => HOLogic.Not$(term_of_qf ps vs t')
   19.30    | And(t1,t2) => HOLogic.conj$(term_of_qf ps vs t1)$(term_of_qf ps vs t2)
   19.31    | Or(t1,t2) => HOLogic.disj$(term_of_qf ps vs t1)$(term_of_qf ps vs t2)
   19.32 -  | Impa(t1,t2) => HOLogic.imp$(term_of_qf ps vs t1)$(term_of_qf ps vs t2)
   19.33 -  | Iffa(t1,t2) => HOLogic.eq_const HOLogic.boolT $ term_of_qf ps vs t1 $ term_of_qf ps vs t2
   19.34 +  | Imp(t1,t2) => HOLogic.imp$(term_of_qf ps vs t1)$(term_of_qf ps vs t2)
   19.35 +  | Iff(t1,t2) => HOLogic.eq_const HOLogic.boolT $ term_of_qf ps vs t1 $ term_of_qf ps vs t2
   19.36    | Closed n => (fst o the) (find_first (fn (_, m) => m = n) ps)
   19.37 -  | NClosed n => term_of_qf ps vs (Nota (Closed n))
   19.38 +  | NClosed n => term_of_qf ps vs (Not (Closed n))
   19.39    | _ => error "If this is raised, Isabelle/HOL or generate_code is inconsistent!";
   19.40  
   19.41  (* The oracle *)
    20.1 --- a/src/Pure/Isar/ROOT.ML	Fri Aug 24 14:14:18 2007 +0200
    20.2 +++ b/src/Pure/Isar/ROOT.ML	Fri Aug 24 14:14:20 2007 +0200
    20.3 @@ -43,15 +43,17 @@
    20.4  use "net_rules.ML";
    20.5  use "induct_attrib.ML";
    20.6  
    20.7 -(*executable theory content*)
    20.8 -use "code_unit.ML";
    20.9 -use "code.ML";
   20.10 -
   20.11  (*derived theory and proof elements*)
   20.12  use "calculation.ML";
   20.13  use "obtain.ML";
   20.14  use "locale.ML";
   20.15  use "class.ML";
   20.16 +
   20.17 +(*executable theory content*)
   20.18 +use "code_unit.ML";
   20.19 +use "code.ML";
   20.20 +
   20.21 +(*local theories and specifications*)
   20.22  use "local_theory.ML";
   20.23  use "theory_target.ML";
   20.24  use "spec_parse.ML";
    21.1 --- a/src/Pure/Isar/class.ML	Fri Aug 24 14:14:18 2007 +0200
    21.2 +++ b/src/Pure/Isar/class.ML	Fri Aug 24 14:14:20 2007 +0200
    21.3 @@ -15,31 +15,35 @@
    21.4      -> string list -> theory -> string * Proof.context
    21.5    val class_cmd: bstring -> string list -> Element.context Locale.element list
    21.6      -> string list -> theory -> string * Proof.context
    21.7 +  val class_of_locale: theory -> string -> class option
    21.8 +  val add_const_in_class: string -> (string * term) * Syntax.mixfix
    21.9 +    -> theory -> theory
   21.10 +
   21.11    val instance_arity: arity list -> ((bstring * Attrib.src list) * term) list
   21.12 +    -> (thm list -> theory -> theory)
   21.13      -> theory -> Proof.state
   21.14    val instance_arity_cmd: (bstring * string list * string) list
   21.15      -> ((bstring * Attrib.src list) * string) list
   21.16 +    -> (thm list -> theory -> theory)
   21.17      -> theory -> Proof.state
   21.18    val prove_instance_arity: tactic -> arity list
   21.19      -> ((bstring * Attrib.src list) * term) list
   21.20 -    -> theory -> theory
   21.21 +    -> theory -> thm list * theory
   21.22 +  val unoverload: theory -> conv
   21.23 +  val overload: theory -> conv
   21.24 +  val unoverload_const: theory -> string * typ -> string
   21.25 +  val inst_const: theory -> string * string -> string
   21.26 +  val param_const: theory -> string -> (string * string) option
   21.27 +  val intro_classes_tac: thm list -> tactic
   21.28 +  val default_intro_classes_tac: thm list -> tactic
   21.29 +
   21.30    val instance_class: class * class -> theory -> Proof.state
   21.31    val instance_class_cmd: string * string -> theory -> Proof.state
   21.32    val instance_sort: class * sort -> theory -> Proof.state
   21.33    val instance_sort_cmd: string * string -> theory -> Proof.state
   21.34    val prove_instance_sort: tactic -> class * sort -> theory -> theory
   21.35  
   21.36 -  val class_of_locale: theory -> string -> class option
   21.37 -  val add_const_in_class: string -> (string * term) * Syntax.mixfix
   21.38 -    -> theory -> theory
   21.39 -
   21.40 -  val unoverload: theory -> thm -> thm
   21.41 -  val overload: theory -> thm -> thm
   21.42 -  val inst_const: theory -> string * string -> string
   21.43 -
   21.44    val print_classes: theory -> unit
   21.45 -  val intro_classes_tac: thm list -> tactic
   21.46 -  val default_intro_classes_tac: thm list -> tactic
   21.47  end;
   21.48  
   21.49  structure Class : CLASS =
   21.50 @@ -130,24 +134,39 @@
   21.51  
   21.52  structure InstData = TheoryDataFun
   21.53  (
   21.54 -  type T = (string * thm) Symtab.table Symtab.table;
   21.55 -    (*constant name ~> type constructor ~> (constant name, equation)*)
   21.56 -  val empty = Symtab.empty;
   21.57 +  type T = (string * thm) Symtab.table Symtab.table * (string * string) Symtab.table;
   21.58 +    (*constant name ~> type constructor ~> (constant name, equation),
   21.59 +        constant name ~> (constant name, type constructor)*)
   21.60 +  val empty = (Symtab.empty, Symtab.empty);
   21.61    val copy = I;
   21.62    val extend = I;
   21.63 -  fun merge _ = Symtab.join (K (Symtab.merge (K true)));
   21.64 +  fun merge _ ((taba1, tabb1), (taba2, tabb2)) =
   21.65 +    (Symtab.join (K (Symtab.merge (K true))) (taba1, taba2),
   21.66 +      Symtab.merge (K true) (tabb1, tabb2));
   21.67  );
   21.68  
   21.69  fun inst_thms f thy =
   21.70 -  Symtab.fold (Symtab.fold (cons o f o snd o snd) o snd) (InstData.get thy) [];
   21.71 -fun add_inst (c, tyco) inst = (InstData.map o Symtab.map_default (c, Symtab.empty))
   21.72 -  (Symtab.update_new (tyco, inst));
   21.73 +  (Symtab.fold (Symtab.fold (cons o f o snd o snd) o snd) o fst) (InstData.get thy) [];
   21.74 +fun add_inst (c, tyco) inst = (InstData.map o apfst o Symtab.map_default (c, Symtab.empty))
   21.75 +  (Symtab.update_new (tyco, inst))
   21.76 +  #> (InstData.map o apsnd) (Symtab.update_new (fst inst, (c, tyco)));
   21.77  
   21.78 -fun unoverload thy thm = MetaSimplifier.rewrite_rule (inst_thms I thy) thm;
   21.79 -fun overload thy thm = MetaSimplifier.rewrite_rule (inst_thms symmetric thy) thm;
   21.80 +fun unoverload thy thm = MetaSimplifier.rewrite false (inst_thms I thy) thm;
   21.81 +fun overload thy thm = MetaSimplifier.rewrite false (inst_thms symmetric thy) thm;
   21.82  
   21.83  fun inst_const thy (c, tyco) =
   21.84 -  (fst o the o Symtab.lookup ((the o Symtab.lookup (InstData.get thy)) c)) tyco;
   21.85 +  (fst o the o Symtab.lookup ((the o Symtab.lookup (fst (InstData.get thy))) c)) tyco;
   21.86 +fun unoverload_const thy (c_ty as (c, _)) =
   21.87 +  case AxClass.class_of_param thy c
   21.88 +   of SOME class => (case Sign.const_typargs thy c_ty
   21.89 +       of [Type (tyco, _)] =>
   21.90 +            (case Symtab.lookup ((the o Symtab.lookup (fst (InstData.get thy))) c) tyco
   21.91 +             of SOME (c, _) => c
   21.92 +              | NONE => c)
   21.93 +        | [_] => c)
   21.94 +    | NONE => c;
   21.95 +
   21.96 +val param_const = Symtab.lookup o snd o InstData.get;
   21.97  
   21.98  fun add_inst_def (class, tyco) (c, ty) thy =
   21.99    let
  21.100 @@ -166,7 +185,7 @@
  21.101    end;
  21.102  
  21.103  fun add_inst_def' (class, tyco) (c, ty) thy =
  21.104 -  if case Symtab.lookup (InstData.get thy) c
  21.105 +  if case Symtab.lookup (fst (InstData.get thy)) c
  21.106     of NONE => true
  21.107      | SOME tab => is_none (Symtab.lookup tab tyco)
  21.108    then add_inst_def (class, tyco) (c, Logic.unvarifyT ty) thy
  21.109 @@ -176,7 +195,7 @@
  21.110    let
  21.111      val ((lhs as Const (c, ty), args), rhs) = (apfst Term.strip_comb o Logic.dest_equals) prop;
  21.112      fun add_inst' def ([], (Const (c_inst, ty))) =
  21.113 -          if forall (fn TFree_ => true | _ => false) (Sign.const_typargs thy (c_inst, ty))
  21.114 +          if forall (fn TFree _ => true | _ => false) (Sign.const_typargs thy (c_inst, ty))
  21.115            then add_inst (c, tyco) (c_inst, def)
  21.116            else add_inst_def (class, tyco) (c, ty)
  21.117        | add_inst' _ t = add_inst_def (class, tyco) (c, ty);
  21.118 @@ -205,7 +224,7 @@
  21.119  fun read_def_cmd thy = gen_read_def thy Attrib.intern_src Theory.read_axm;
  21.120  fun read_def thy = gen_read_def thy (K I) (K I);
  21.121  
  21.122 -fun gen_instance_arity prep_arity read_def do_proof raw_arities raw_defs theory =
  21.123 +fun gen_instance_arity prep_arity read_def do_proof raw_arities raw_defs after_qed theory =
  21.124    let
  21.125      val arities = map (prep_arity theory) raw_arities;
  21.126      val _ = if null arities then error "at least one arity must be given" else ();
  21.127 @@ -259,28 +278,32 @@
  21.128          |> Sign.add_const_constraint_i (c, NONE)
  21.129          |> pair (c, Logic.unvarifyT ty)
  21.130        end;
  21.131 -    fun after_qed cs defs =
  21.132 +    fun after_qed' cs defs =
  21.133        fold Sign.add_const_constraint_i (map (apsnd SOME) cs)
  21.134 -      #> fold (Code.add_func false) defs;
  21.135 +      #> after_qed defs;
  21.136    in
  21.137      theory
  21.138      |> fold_map get_remove_contraint (map fst cs |> distinct (op =))
  21.139      ||>> fold_map add_def defs
  21.140      ||> fold (fn (c, ((class, tyco), ty)) => add_inst_def' (class, tyco) (c, ty)) other_cs
  21.141 -    |-> (fn (cs, defs) => do_proof (after_qed cs defs) arities)
  21.142 +    |-> (fn (cs, defs) => do_proof (after_qed' cs defs) arities defs)
  21.143    end;
  21.144  
  21.145  fun instance_arity_cmd' do_proof = gen_instance_arity Sign.read_arity read_def_cmd do_proof;
  21.146  fun instance_arity' do_proof = gen_instance_arity Sign.cert_arity read_def do_proof;
  21.147 -fun tactic_proof tac after_qed arities =
  21.148 +fun tactic_proof tac f arities defs =
  21.149    fold (fn arity => AxClass.prove_arity arity tac) arities
  21.150 -  #> after_qed;
  21.151 +  #> f
  21.152 +  #> pair defs;
  21.153  
  21.154  in
  21.155  
  21.156 -val instance_arity_cmd = instance_arity_cmd' axclass_instance_arity;
  21.157 -val instance_arity = instance_arity' axclass_instance_arity;
  21.158 -val prove_instance_arity = instance_arity' o tactic_proof;
  21.159 +val instance_arity_cmd = instance_arity_cmd'
  21.160 +  (fn f => fn arities => fn defs => axclass_instance_arity f arities);
  21.161 +val instance_arity = instance_arity'
  21.162 +  (fn f => fn arities => fn defs => axclass_instance_arity f arities);
  21.163 +fun prove_instance_arity tac arities defs =
  21.164 +  instance_arity' (tactic_proof tac) arities defs (K I);
  21.165  
  21.166  end; (*local*)
  21.167  
    22.1 --- a/src/Pure/Isar/code.ML	Fri Aug 24 14:14:18 2007 +0200
    22.2 +++ b/src/Pure/Isar/code.ML	Fri Aug 24 14:14:20 2007 +0200
    22.3 @@ -10,7 +10,7 @@
    22.4  sig
    22.5    val add_func: bool -> thm -> theory -> theory
    22.6    val del_func: thm -> theory -> theory
    22.7 -  val add_funcl: CodeUnit.const * thm list Susp.T -> theory -> theory
    22.8 +  val add_funcl: string * thm list Susp.T -> theory -> theory
    22.9    val add_func_attr: bool -> Attrib.src
   22.10    val add_inline: thm -> theory -> theory
   22.11    val del_inline: thm -> theory -> theory
   22.12 @@ -20,17 +20,15 @@
   22.13    val del_preproc: string -> theory -> theory
   22.14    val add_post: thm -> theory -> theory
   22.15    val del_post: thm -> theory -> theory
   22.16 -  val add_datatype: string * ((string * sort) list * (string * typ list) list)
   22.17 -    -> theory -> theory
   22.18 -  val add_datatype_consts: CodeUnit.const list -> theory -> theory
   22.19 -  val add_datatype_consts_cmd: string list -> theory -> theory
   22.20 +  val add_datatype: (string * typ) list -> theory -> theory
   22.21 +  val add_datatype_cmd: string list -> theory -> theory
   22.22  
   22.23    val coregular_algebra: theory -> Sorts.algebra
   22.24    val operational_algebra: theory -> (sort -> sort) * Sorts.algebra
   22.25 -  val these_funcs: theory -> CodeUnit.const -> thm list
   22.26 +  val these_funcs: theory -> string -> thm list
   22.27    val get_datatype: theory -> string -> ((string * sort) list * (string * typ list) list)
   22.28 -  val get_datatype_of_constr: theory -> CodeUnit.const -> string option
   22.29 -  val default_typ: theory -> CodeUnit.const -> typ
   22.30 +  val get_datatype_of_constr: theory -> string -> string option
   22.31 +  val default_typ: theory -> string -> typ
   22.32  
   22.33    val preprocess_conv: cterm -> thm
   22.34    val postprocess_conv: cterm -> thm
   22.35 @@ -45,7 +43,7 @@
   22.36    type T
   22.37    val empty: T
   22.38    val merge: Pretty.pp -> T * T -> T
   22.39 -  val purge: theory option -> CodeUnit.const list option -> T -> T
   22.40 +  val purge: theory option -> string list option -> T -> T
   22.41  end;
   22.42  
   22.43  signature CODE_DATA =
   22.44 @@ -60,7 +58,7 @@
   22.45  sig
   22.46    include CODE
   22.47    val declare_data: Object.T -> (Pretty.pp -> Object.T * Object.T -> Object.T)
   22.48 -    -> (theory option -> CodeUnit.const list option -> Object.T -> Object.T) -> serial
   22.49 +    -> (theory option -> string list option -> Object.T -> Object.T) -> serial
   22.50    val get_data: serial * ('a -> Object.T) * (Object.T -> 'a)
   22.51      -> theory -> 'a
   22.52    val change_data: serial * ('a -> Object.T) * (Object.T -> 'a)
   22.53 @@ -74,9 +72,6 @@
   22.54  
   22.55  (** preliminaries **)
   22.56  
   22.57 -structure Consttab = CodeUnit.Consttab;
   22.58 -
   22.59 -
   22.60  (* certificate theorems *)
   22.61  
   22.62  fun string_of_lthms r = case Susp.peek r
   22.63 @@ -224,24 +219,23 @@
   22.64  
   22.65  fun join_func_thms (tabs as (tab1, tab2)) =
   22.66    let
   22.67 -    val cs1 = Consttab.keys tab1;
   22.68 -    val cs2 = Consttab.keys tab2;
   22.69 -    val cs' = filter (member CodeUnit.eq_const cs2) cs1;
   22.70 +    val cs1 = Symtab.keys tab1;
   22.71 +    val cs2 = Symtab.keys tab2;
   22.72 +    val cs' = filter (member (op =) cs2) cs1;
   22.73      val cs'' = subtract (op =) cs' cs1 @ subtract (op =) cs' cs2;
   22.74 -    val cs''' = ref [] : CodeUnit.const list ref;
   22.75 +    val cs''' = ref [] : string list ref;
   22.76      fun merge c x = let val (touched, thms') = merge_sdthms x in
   22.77        (if touched then cs''' := cons c (!cs''') else (); thms') end;
   22.78 -  in (cs'' @ !cs''', Consttab.join merge tabs) end;
   22.79 +  in (cs'' @ !cs''', Symtab.join merge tabs) end;
   22.80  fun merge_funcs (thms1, thms2) =
   22.81    let
   22.82      val (consts, thms) = join_func_thms (thms1, thms2);
   22.83    in (SOME consts, thms) end;
   22.84  
   22.85  val eq_string = op = : string * string -> bool;
   22.86 -val eq_co = op = : (string * typ list) * (string * typ list) -> bool;
   22.87  fun eq_dtyp ((vs1, cs1), (vs2, cs2)) = 
   22.88    gen_eq_set (eq_pair eq_string (gen_eq_set eq_string)) (vs1, vs2)
   22.89 -    andalso gen_eq_set eq_co (cs1, cs2);
   22.90 +    andalso gen_eq_set (eq_fst eq_string) (cs1, cs2);
   22.91  fun merge_dtyps (tabs as (tab1, tab2)) =
   22.92    let
   22.93      val tycos1 = Symtab.keys tab1;
   22.94 @@ -256,7 +250,7 @@
   22.95    in ((new_types, diff_types), Symtab.join join tabs) end;
   22.96  
   22.97  datatype spec = Spec of {
   22.98 -  funcs: sdthms Consttab.table,
   22.99 +  funcs: sdthms Symtab.table,
  22.100    dtyps: ((string * sort) list * (string * typ list) list) Symtab.table
  22.101  };
  22.102  
  22.103 @@ -289,7 +283,7 @@
  22.104      val touched = if touched' then NONE else touched_cs;
  22.105    in (touched, mk_exec (thmproc, spec)) end;
  22.106  val empty_exec = mk_exec (mk_thmproc ((([], []), []), []),
  22.107 -  mk_spec (Consttab.empty, Symtab.empty));
  22.108 +  mk_spec (Symtab.empty, Symtab.empty));
  22.109  
  22.110  fun the_thmproc (Exec { thmproc = Preproc x, ...}) = x;
  22.111  fun the_spec (Exec { spec = Spec x, ...}) = x;
  22.112 @@ -310,7 +304,7 @@
  22.113  type kind = {
  22.114    empty: Object.T,
  22.115    merge: Pretty.pp -> Object.T * Object.T -> Object.T,
  22.116 -  purge: theory option -> CodeUnit.const list option -> Object.T -> Object.T
  22.117 +  purge: theory option -> string list option -> Object.T -> Object.T
  22.118  };
  22.119  
  22.120  val kinds = ref (Datatab.empty: kind Datatab.table);
  22.121 @@ -429,13 +423,14 @@
  22.122              :: separate (Pretty.str "|") (map (fn (c, []) => Pretty.str c
  22.123                   | (c, tys) =>
  22.124                       (Pretty.block o Pretty.breaks)
  22.125 -                        (Pretty.str c :: Pretty.str "of" :: map (Pretty.quote o Sign.pretty_typ thy) tys)) cos)
  22.126 +                        (Pretty.str (CodeUnit.string_of_const thy c)
  22.127 +                          :: Pretty.str "of" :: map (Pretty.quote o Sign.pretty_typ thy) tys)) cos)
  22.128            );
  22.129      val inlines = (#inlines o the_thmproc) exec;
  22.130      val inline_procs = (map fst o #inline_procs o the_thmproc) exec;
  22.131      val preprocs = (map fst o #preprocs o the_thmproc) exec;
  22.132      val funs = the_funcs exec
  22.133 -      |> Consttab.dest
  22.134 +      |> Symtab.dest
  22.135        |> (map o apfst) (CodeUnit.string_of_const thy)
  22.136        |> sort (string_ord o pairself fst);
  22.137      val dtyps = the_dtyps exec
  22.138 @@ -499,9 +494,11 @@
  22.139            cons (Thm.ctyp_of thy (TVar (x_i, sort)), Thm.ctyp_of thy ty)) env [];
  22.140        in map (Thm.instantiate (instT, [])) thms' end;
  22.141  
  22.142 +fun const_of_func thy = Class.unoverload_const thy o CodeUnit.head_func;
  22.143 +
  22.144  fun certify_const thy const thms =
  22.145    let
  22.146 -    fun cert thm = if CodeUnit.eq_const (const, fst (CodeUnit.head_func thm))
  22.147 +    fun cert thm = if const = const_of_func thy thm
  22.148        then thm else error ("Wrong head of defining equation,\nexpected constant "
  22.149          ^ CodeUnit.string_of_const thy const ^ "\n" ^ string_of_thm thm)
  22.150    in map cert thms end;
  22.151 @@ -527,15 +524,17 @@
  22.152  fun specific_constraints thy (class, tyco) =
  22.153    let
  22.154      val vs = Name.invents Name.context "" (Sign.arity_number thy tyco);
  22.155 -    val clsops = (these o Option.map snd o try (AxClass.params_of_class thy)) class;
  22.156 +    val clsops = (map fst o these o Option.map snd
  22.157 +      o try (AxClass.params_of_class thy)) class;
  22.158      val funcs = clsops
  22.159 -      |> map (fn (clsop, _) => (clsop, SOME tyco))
  22.160 -      |> map (Consttab.lookup ((the_funcs o get_exec) thy))
  22.161 +      |> map (fn c => Class.inst_const thy (c, tyco))
  22.162 +      |> map (Symtab.lookup ((the_funcs o get_exec) thy))
  22.163        |> (map o Option.map) (Susp.force o fst)
  22.164        |> maps these
  22.165 -      |> map (Thm.transfer thy);
  22.166 -    val sorts = map (map (snd o dest_TVar) o snd o dest_Type o the_single
  22.167 -      o Sign.const_typargs thy o (fn ((c, _), ty) => (c, ty)) o CodeUnit.head_func) funcs;
  22.168 +      |> map (Thm.transfer thy)
  22.169 +    fun sorts_of [Type (_, tys)] = map (snd o dest_TVar) tys
  22.170 +      | sorts_of tys = map (snd o dest_TVar) tys;
  22.171 +    val sorts = map (sorts_of o Sign.const_typargs thy o CodeUnit.head_func) funcs;
  22.172    in sorts end;
  22.173  
  22.174  fun weakest_constraints thy (class, tyco) =
  22.175 @@ -587,8 +586,9 @@
  22.176  fun assert_func_typ thm =
  22.177    let
  22.178      val thy = Thm.theory_of_thm thm;
  22.179 -    fun check_typ_classop class (const as (c, SOME tyco), thm) =
  22.180 +    fun check_typ_classop tyco (c, thm) =
  22.181            let
  22.182 +            val SOME class = AxClass.class_of_param thy c;
  22.183              val (_, ty) = CodeUnit.head_func thm;
  22.184              val ty_decl = classop_weakest_typ thy class (c, tyco);
  22.185              val ty_strongest = classop_strongest_typ thy class (c, tyco);
  22.186 @@ -615,12 +615,8 @@
  22.187                ^ string_of_thm thm
  22.188                ^ "\nis incompatible with permitted least general type\n"
  22.189                ^ CodeUnit.string_of_typ thy ty_strongest)
  22.190 -          end
  22.191 -      | check_typ_classop class ((c, NONE), thm) =
  22.192 -          CodeUnit.bad_thm ("Illegal type for class operation " ^ quote c
  22.193 -           ^ "\nin defining equation\n"
  22.194 -           ^ string_of_thm thm);
  22.195 -    fun check_typ_fun (const as (c, _), thm) =
  22.196 +          end;
  22.197 +    fun check_typ_fun (c, thm) =
  22.198        let
  22.199          val (_, ty) = CodeUnit.head_func thm;
  22.200          val ty_decl = Sign.the_const_type thy c;
  22.201 @@ -632,11 +628,11 @@
  22.202             ^ "\nis incompatible with declared function type\n"
  22.203             ^ CodeUnit.string_of_typ thy ty_decl)
  22.204        end;
  22.205 -    fun check_typ (const as (c, _), thm) =
  22.206 -      case AxClass.class_of_param thy c
  22.207 -       of SOME class => check_typ_classop class (const, thm)
  22.208 -        | NONE => check_typ_fun (const, thm);
  22.209 -  in check_typ (fst (CodeUnit.head_func thm), thm) end;
  22.210 +    fun check_typ (c, thm) =
  22.211 +      case Class.param_const thy c
  22.212 +       of SOME (c, tyco) => check_typ_classop tyco (c, thm)
  22.213 +        | NONE => check_typ_fun (c, thm);
  22.214 +  in check_typ (const_of_func thy thm, thm) end;
  22.215  
  22.216  val mk_func = CodeUnit.error_thm (assert_func_typ o CodeUnit.mk_func);
  22.217  val mk_func_liberal = CodeUnit.warning_thm (assert_func_typ o CodeUnit.mk_func);
  22.218 @@ -647,21 +643,56 @@
  22.219  
  22.220  (** interfaces and attributes **)
  22.221  
  22.222 +fun get_datatype thy tyco =
  22.223 +  case Symtab.lookup ((the_dtyps o get_exec) thy) tyco
  22.224 +   of SOME spec => spec
  22.225 +    | NONE => Sign.arity_number thy tyco
  22.226 +        |> Name.invents Name.context "'a"
  22.227 +        |> map (rpair [])
  22.228 +        |> rpair [];
  22.229 +
  22.230 +fun get_datatype_of_constr thy c =
  22.231 +  case (snd o strip_type o Sign.the_const_type thy) c
  22.232 +   of Type (tyco, _) => if member (op =)
  22.233 +       ((the_default [] o Option.map (map fst o snd) o Symtab.lookup ((the_dtyps o get_exec) thy)) tyco) c
  22.234 +       then SOME tyco else NONE
  22.235 +    | _ => NONE;
  22.236 +
  22.237 +fun get_constr_typ thy c =
  22.238 +  case get_datatype_of_constr thy c
  22.239 +   of SOME tyco => let
  22.240 +          val (vs, cos) = get_datatype thy tyco;
  22.241 +          val SOME tys = AList.lookup (op =) cos c;
  22.242 +          val ty = tys ---> Type (tyco, map TFree vs);
  22.243 +        in SOME (Logic.varifyT ty) end
  22.244 +    | NONE => NONE;
  22.245 +
  22.246  fun add_func true thm thy =
  22.247        let
  22.248          val func = mk_func thm;
  22.249 -        val (const, _) = CodeUnit.head_func func;
  22.250 -      in map_exec_purge (SOME [const]) (map_funcs
  22.251 -        (Consttab.map_default
  22.252 -          (const, (Susp.value [], [])) (add_thm func))) thy
  22.253 +        val c = const_of_func thy func;
  22.254 +        val _ = if (is_some o AxClass.class_of_param thy) c
  22.255 +          then error ("Rejected polymorphic equation for overloaded constant:\n"
  22.256 +            ^ string_of_thm thm)
  22.257 +          else ();
  22.258 +        val _ = if (is_some o get_datatype_of_constr thy) c
  22.259 +          then error ("Rejected equation for datatype constructor:\n"
  22.260 +            ^ string_of_thm func)
  22.261 +          else ();
  22.262 +      in map_exec_purge (SOME [c]) (map_funcs
  22.263 +        (Symtab.map_default
  22.264 +          (c, (Susp.value [], [])) (add_thm func))) thy
  22.265        end
  22.266    | add_func false thm thy =
  22.267        case mk_func_liberal thm
  22.268         of SOME func => let
  22.269 -              val (const, _) = CodeUnit.head_func func
  22.270 -            in map_exec_purge (SOME [const]) (map_funcs
  22.271 -              (Consttab.map_default
  22.272 -                (const, (Susp.value [], [])) (add_thm func))) thy
  22.273 +              val c = const_of_func thy func
  22.274 +            in if (is_some o AxClass.class_of_param thy) c
  22.275 +              orelse (is_some o get_datatype_of_constr thy) c
  22.276 +              then thy
  22.277 +              else map_exec_purge (SOME [c]) (map_funcs
  22.278 +              (Symtab.map_default
  22.279 +                (c, (Susp.value [], [])) (add_thm func))) thy
  22.280              end
  22.281          | NONE => thy;
  22.282  
  22.283 @@ -672,9 +703,9 @@
  22.284  fun del_func thm thy =
  22.285    let
  22.286      val func = mk_func thm;
  22.287 -    val (const, _) = CodeUnit.head_func func;
  22.288 +    val const = const_of_func thy func;
  22.289    in map_exec_purge (SOME [const]) (map_funcs
  22.290 -    (Consttab.map_entry
  22.291 +    (Symtab.map_entry
  22.292        const (del_thm func))) thy
  22.293    end;
  22.294  
  22.295 @@ -684,41 +715,31 @@
  22.296        (*FIXME must check compatibility with sort algebra;
  22.297          alas, naive checking results in non-termination!*)
  22.298    in
  22.299 -    map_exec_purge (SOME [const]) (map_funcs (Consttab.map_default (const, (Susp.value [], []))
  22.300 +    map_exec_purge (SOME [const]) (map_funcs (Symtab.map_default (const, (Susp.value [], []))
  22.301        (add_lthms lthms'))) thy
  22.302    end;
  22.303  
  22.304  fun add_func_attr strict = Attrib.internal (fn _ => Thm.declaration_attribute
  22.305    (fn thm => Context.mapping (add_func strict thm) I));
  22.306  
  22.307 -local
  22.308 -
  22.309 -fun del_datatype tyco thy =
  22.310 -  case Symtab.lookup ((the_dtyps o get_exec) thy) tyco
  22.311 -   of SOME (vs, cos) => let
  22.312 -        val consts = CodeUnit.consts_of_cos thy tyco vs cos;
  22.313 -      in map_exec_purge (if null consts then NONE else SOME consts)
  22.314 -        (map_dtyps (Symtab.delete tyco)) thy end
  22.315 -    | NONE => thy;
  22.316 -
  22.317 -in
  22.318 -
  22.319 -fun add_datatype (tyco, (vs_cos as (vs, cos))) thy =
  22.320 +fun add_datatype raw_cs thy =
  22.321    let
  22.322 -    val consts = CodeUnit.consts_of_cos thy tyco vs cos;
  22.323 +    val cs = map (fn c_ty as (_, ty) => (Class.unoverload_const thy c_ty, ty)) raw_cs;
  22.324 +    val (tyco, vs_cos) = CodeUnit.constrset_of_consts thy cs;
  22.325 +    val purge_cs = map fst (snd vs_cos);
  22.326 +    val purge_cs' = case Symtab.lookup ((the_dtyps o get_exec) thy) tyco
  22.327 +     of SOME (vs, cos) => if null cos then NONE else SOME (purge_cs @ map fst cos)
  22.328 +      | NONE => NONE;
  22.329    in
  22.330      thy
  22.331 -    |> del_datatype tyco
  22.332 -    |> map_exec_purge (SOME consts) (map_dtyps (Symtab.update_new (tyco, vs_cos)))
  22.333 +    |> map_exec_purge purge_cs' (map_dtyps (Symtab.update (tyco, vs_cos))
  22.334 +        #> map_funcs (fold (Symtab.delete_safe o fst) cs))
  22.335    end;
  22.336  
  22.337 -fun add_datatype_consts consts thy =
  22.338 -  add_datatype (CodeUnit.cos_of_consts thy consts) thy;
  22.339 -
  22.340 -fun add_datatype_consts_cmd raw_cs thy =
  22.341 -  add_datatype_consts (map (CodeUnit.read_const thy) raw_cs) thy
  22.342 -
  22.343 -end; (*local*)
  22.344 +fun add_datatype_cmd raw_cs thy =
  22.345 +  let
  22.346 +    val cs = map (CodeUnit.read_bare_const thy) raw_cs;
  22.347 +  in add_datatype cs thy end;
  22.348  
  22.349  fun add_inline thm thy =
  22.350    (map_exec_purge NONE o map_thmproc o apfst o apfst o apfst)
  22.351 @@ -790,7 +811,7 @@
  22.352  fun apply_preproc thy f [] = []
  22.353    | apply_preproc thy f (thms as (thm :: _)) =
  22.354        let
  22.355 -        val (const, _) = CodeUnit.head_func thm;
  22.356 +        val const = const_of_func thy thm;
  22.357          val thms' = f thy thms;
  22.358        in certify_const thy const thms' end;
  22.359  
  22.360 @@ -807,7 +828,8 @@
  22.361    |> map (CodeUnit.rewrite_func ((#inlines o the_thmproc o get_exec) thy))
  22.362    |> fold (fn (_, (_, f)) => apply_inline_proc thy f) ((#inline_procs o the_thmproc o get_exec) thy)
  22.363  (*FIXME - must check: rewrite rule, defining equation, proper constant |> map (snd o check_func false thy) *)
  22.364 -  |> common_typ_funcs;
  22.365 +  |> common_typ_funcs
  22.366 +  |> map (Conv.fconv_rule (Class.unoverload thy));
  22.367  
  22.368  fun preprocess_conv ct =
  22.369    let
  22.370 @@ -817,6 +839,7 @@
  22.371      |> MetaSimplifier.rewrite false ((#inlines o the_thmproc o get_exec) thy)
  22.372      |> fold (fn (_, (_, f)) => rhs_conv (apply_inline_proc_cterm thy f))
  22.373          ((#inline_procs o the_thmproc o get_exec) thy)
  22.374 +    |> rhs_conv (Class.unoverload thy)
  22.375    end;
  22.376  
  22.377  fun postprocess_conv ct =
  22.378 @@ -824,49 +847,24 @@
  22.379      val thy = Thm.theory_of_cterm ct;
  22.380    in
  22.381      ct
  22.382 -    |> MetaSimplifier.rewrite false ((#posts o the_thmproc o get_exec) thy)
  22.383 +    |> Class.overload thy
  22.384 +    |> rhs_conv (MetaSimplifier.rewrite false ((#posts o the_thmproc o get_exec) thy))
  22.385    end;
  22.386  
  22.387  end; (*local*)
  22.388  
  22.389 -fun get_datatype thy tyco =
  22.390 -  case Symtab.lookup ((the_dtyps o get_exec) thy) tyco
  22.391 -   of SOME spec => spec
  22.392 -    | NONE => Sign.arity_number thy tyco
  22.393 -        |> Name.invents Name.context "'a"
  22.394 -        |> map (rpair [])
  22.395 -        |> rpair [];
  22.396 -
  22.397 -fun get_datatype_of_constr thy const =
  22.398 -  case CodeUnit.co_of_const' thy const
  22.399 -   of SOME (tyco, (_, co)) => if member eq_co
  22.400 -        (Symtab.lookup (((the_dtyps o get_exec) thy)) tyco
  22.401 -          |> Option.map snd
  22.402 -          |> the_default []) co then SOME tyco else NONE
  22.403 -    | NONE => NONE;
  22.404 -
  22.405 -fun get_constr_typ thy const =
  22.406 -  case get_datatype_of_constr thy const
  22.407 -   of SOME tyco => let
  22.408 -        val (vs, cos) = get_datatype thy tyco;
  22.409 -        val (_, (_, (co, tys))) = CodeUnit.co_of_const thy const
  22.410 -      in (tys ---> Type (tyco, map TFree vs))
  22.411 -        |> map_atyps (fn TFree (v, _) => TFree (v, AList.lookup (op =) vs v |> the))
  22.412 -        |> Logic.varifyT
  22.413 -        |> SOME end
  22.414 -    | NONE => NONE;
  22.415 -
  22.416 -fun default_typ_proto thy (const as (c, SOME tyco)) = classop_weakest_typ thy
  22.417 -      ((the o AxClass.class_of_param thy) c) (c, tyco) |> SOME
  22.418 -  | default_typ_proto thy (const as (c, NONE)) = case AxClass.class_of_param thy c
  22.419 -       of SOME class => SOME (Term.map_type_tvar
  22.420 -            (K (TVar (("'a", 0), [class]))) (Sign.the_const_type thy c))
  22.421 -        | NONE => get_constr_typ thy const;
  22.422 +fun default_typ_proto thy c = case Class.param_const thy c
  22.423 + of SOME (c, tyco) => classop_weakest_typ thy ((the o AxClass.class_of_param thy) c)
  22.424 +      (c, tyco) |> SOME
  22.425 +  | NONE => (case AxClass.class_of_param thy c
  22.426 +     of SOME class => SOME (Term.map_type_tvar
  22.427 +          (K (TVar (("'a", 0), [class]))) (Sign.the_const_type thy c))
  22.428 +      | NONE => get_constr_typ thy c);
  22.429  
  22.430  local
  22.431  
  22.432  fun get_funcs thy const =
  22.433 -  Consttab.lookup ((the_funcs o get_exec) thy) const
  22.434 +  Symtab.lookup ((the_funcs o get_exec) thy) const
  22.435    |> Option.map (Susp.force o fst)
  22.436    |> these
  22.437    |> map (Thm.transfer thy);
  22.438 @@ -883,10 +881,10 @@
  22.439      |> drop_refl thy
  22.440    end;
  22.441  
  22.442 -fun default_typ thy (const as (c, _)) = case default_typ_proto thy const
  22.443 +fun default_typ thy c = case default_typ_proto thy c
  22.444   of SOME ty => ty
  22.445 -  | NONE => (case get_funcs thy const
  22.446 -     of thm :: _ => snd (CodeUnit.head_func thm)
  22.447 +  | NONE => (case get_funcs thy c
  22.448 +     of thm :: _ => snd (CodeUnit.head_func (Conv.fconv_rule (Class.unoverload thy) thm))
  22.449        | [] => Sign.the_const_type thy c);
  22.450  
  22.451  end; (*local*)
    23.1 --- a/src/Pure/Isar/code_unit.ML	Fri Aug 24 14:14:18 2007 +0200
    23.2 +++ b/src/Pure/Isar/code_unit.ML	Fri Aug 24 14:14:20 2007 +0200
    23.3 @@ -2,45 +2,28 @@
    23.4      ID:         $Id$
    23.5      Author:     Florian Haftmann, TU Muenchen
    23.6  
    23.7 -Basic units of code generation:  Identifying (possibly overloaded) constants
    23.8 -by name plus optional type constructor.  Convenient data structures for constants.
    23.9 -Defining equations ("func"s).  Auxiliary.
   23.10 +Basic units of code generation.  Auxiliary.
   23.11  *)
   23.12  
   23.13  signature CODE_UNIT =
   23.14  sig
   23.15 -  type const = string * string option (*constant name, possibly instance*)
   23.16 -  val const_ord: const * const -> order
   23.17 -  val eq_const: const * const -> bool
   23.18 -  structure Consttab: TABLE
   23.19 -  val const_of_cexpr: theory -> string * typ -> const
   23.20    val string_of_typ: theory -> typ -> string
   23.21 -  val string_of_const: theory -> const -> string
   23.22 +  val string_of_const: theory -> string -> string
   23.23 +  val no_args: theory -> string -> int
   23.24    val read_bare_const: theory -> string -> string * typ
   23.25 -  val read_const: theory -> string -> const
   23.26 -  val read_const_exprs: theory -> (const list -> const list)
   23.27 -    -> string list -> bool * const list
   23.28 +  val read_const: theory -> string -> string
   23.29 +  val read_const_exprs: theory -> (string list -> string list)
   23.30 +    -> string list -> bool * string list
   23.31  
   23.32 -  val co_of_const: theory -> const
   23.33 -    -> string * ((string * sort) list * (string * typ list))
   23.34 -  val co_of_const': theory -> const
   23.35 -    -> (string * ((string * sort) list * (string * typ list))) option
   23.36 -  val cos_of_consts: theory -> const list
   23.37 +  val constrset_of_consts: theory -> (string * typ) list
   23.38      -> string * ((string * sort) list * (string * typ list) list)
   23.39 -  val const_of_co: theory -> string -> (string * sort) list
   23.40 -    -> string * typ list -> const
   23.41 -  val consts_of_cos: theory -> string -> (string * sort) list
   23.42 -    -> (string * typ list) list -> const list
   23.43 -  val no_args: theory -> const -> int
   23.44 -
   23.45 -  val typargs: theory -> string * typ -> typ list
   23.46    val typ_sort_inst: Sorts.algebra -> typ * sort
   23.47      -> sort Vartab.table -> sort Vartab.table
   23.48  
   23.49    val assert_rew: thm -> thm
   23.50    val mk_rew: thm -> thm
   23.51    val mk_func: thm -> thm
   23.52 -  val head_func: thm -> const * typ
   23.53 +  val head_func: thm -> string * typ
   23.54    val bad_thm: string -> 'a
   23.55    val error_thm: (thm -> thm) -> thm -> thm
   23.56    val warning_thm: (thm -> thm) -> thm -> thm option
   23.57 @@ -64,37 +47,12 @@
   23.58  fun warning_thm f thm = SOME (f thm) handle BAD_THM msg
   23.59    => (warning ("code generator: " ^ msg); NONE);
   23.60  
   23.61 -
   23.62 -(* basic data structures *)
   23.63 -
   23.64 -type const = string * string option;
   23.65 -val const_ord = prod_ord fast_string_ord (option_ord string_ord);
   23.66 -val eq_const = is_equal o const_ord;
   23.67 -
   23.68 -structure Consttab =
   23.69 -  TableFun(
   23.70 -    type key = const;
   23.71 -    val ord = const_ord;
   23.72 -  );
   23.73 -
   23.74  fun string_of_typ thy = setmp show_sorts true (Sign.string_of_typ thy);
   23.75 -
   23.76 +fun string_of_const thy c = case Class.param_const thy c
   23.77 + of SOME (c, tyco) => Sign.extern_const thy c ^ " " ^ enclose "[" "]" (Sign.extern_type thy tyco)
   23.78 +  | NONE => Sign.extern_const thy c;
   23.79  
   23.80 -(* conversion between constant expressions and constants *)
   23.81 -
   23.82 -fun const_of_cexpr thy (c_ty as (c, _)) =
   23.83 -  case AxClass.class_of_param thy c
   23.84 -   of SOME class => (case Sign.const_typargs thy c_ty
   23.85 -       of [Type (tyco, _)] => if can (Sorts.mg_domain (Sign.classes_of thy) tyco) [class]
   23.86 -              then (c, SOME tyco)
   23.87 -              else (c, NONE)
   23.88 -        | [_] => (c, NONE))
   23.89 -    | NONE => (c, NONE);
   23.90 -
   23.91 -fun string_of_const thy (c, NONE) = Sign.extern_const thy c
   23.92 -  | string_of_const thy (c, SOME tyco) = Sign.extern_const thy c
   23.93 -      ^ " " ^ enclose "[" "]" (Sign.extern_type thy tyco);
   23.94 -
   23.95 +fun no_args thy = length o fst o strip_type o Sign.the_const_type thy;
   23.96  
   23.97  (* reading constants as terms and wildcards pattern *)
   23.98  
   23.99 @@ -106,7 +64,7 @@
  23.100      | NONE => error ("Not a constant: " ^ Sign.string_of_term thy t)
  23.101    end;
  23.102  
  23.103 -fun read_const thy = const_of_cexpr thy o read_bare_const thy;
  23.104 +fun read_const thy = Class.unoverload_const thy o read_bare_const thy;
  23.105  
  23.106  local
  23.107  
  23.108 @@ -115,27 +73,11 @@
  23.109      val this_thy = Option.map theory some_thyname |> the_default thy;
  23.110      val cs = Symtab.fold (fn (c, (_, NONE)) => cons c | _ => I)
  23.111        ((snd o #constants o Consts.dest o #consts o Sign.rep_sg) this_thy) [];
  23.112 -    fun classop c = case AxClass.class_of_param thy c
  23.113 -     of NONE => [(c, NONE)]
  23.114 -      | SOME class => Symtab.fold
  23.115 -          (fn (tyco, classes) => if AList.defined (op =) classes class
  23.116 -            then cons (c, SOME tyco) else I)
  23.117 -          ((#arities o Sorts.rep_algebra o Sign.classes_of) this_thy)
  23.118 -          [(c, NONE)];
  23.119 -    val consts = maps classop cs;
  23.120 -    fun test_instance thy (class, tyco) =
  23.121 -      can (Sorts.mg_domain (Sign.classes_of thy) tyco) [class]
  23.122 -    fun belongs_here thyname (c, NONE) =
  23.123 +    fun belongs_here thyname c =
  23.124            not (exists (fn thy' => Sign.declared_const thy' c) (Theory.parents_of this_thy))
  23.125 -      | belongs_here thyname (c, SOME tyco) =
  23.126 -          let
  23.127 -            val SOME class = AxClass.class_of_param thy c
  23.128 -          in not (exists (fn thy' => test_instance thy' (class, tyco))
  23.129 -            (Theory.parents_of this_thy))
  23.130 -          end;
  23.131    in case some_thyname
  23.132 -   of NONE => consts
  23.133 -    | SOME thyname => filter (belongs_here thyname) consts
  23.134 +   of NONE => cs
  23.135 +    | SOME thyname => filter (belongs_here thyname) cs
  23.136    end;
  23.137  
  23.138  fun read_const_expr thy "*" = ([], consts_of thy NONE)
  23.139 @@ -152,89 +94,48 @@
  23.140  
  23.141  end; (*local*)
  23.142  
  23.143 -(* conversion between constants, constant expressions and datatype constructors *)
  23.144 -
  23.145 -fun const_of_co thy tyco vs (co, tys) =
  23.146 -  const_of_cexpr thy (co, tys ---> Type (tyco, map TFree vs));
  23.147 -
  23.148 -fun consts_of_cos thy tyco vs cos =
  23.149 -  let
  23.150 -    val dty = Type (tyco, map TFree vs);
  23.151 -    fun mk_co (co, tys) = const_of_cexpr thy (co, tys ---> dty);
  23.152 -  in map mk_co cos end;
  23.153 -
  23.154 -local
  23.155  
  23.156 -exception BAD of string;
  23.157 +(* constructor sets *)
  23.158  
  23.159 -fun mg_typ_of_const thy (c, NONE) = Sign.the_const_type thy c
  23.160 -  | mg_typ_of_const thy (c, SOME tyco) =
  23.161 -      let
  23.162 -        val SOME class = AxClass.class_of_param thy c;
  23.163 -        val ty = Sign.the_const_type thy c;
  23.164 -          (*an approximation*)
  23.165 -        val sorts = Sorts.mg_domain (Sign.classes_of thy) tyco [class]
  23.166 -          handle CLASS_ERROR => raise BAD ("No such instance: " ^ tyco ^ " :: " ^ class
  23.167 -            ^ ",\nrequired for overloaded constant " ^ c);
  23.168 -        val vs = Name.invents Name.context "'a" (length sorts);
  23.169 -      in map_atyps (K (Type (tyco, map (fn v => TVar ((v, 0), [])) vs))) ty end;
  23.170 -
  23.171 -fun gen_co_of_const thy const =
  23.172 +fun constrset_of_consts thy cs =
  23.173    let
  23.174 -    val (c, _) = const;
  23.175 -    val ty = (Logic.unvarifyT o mg_typ_of_const thy) const;
  23.176 -    fun err () = raise BAD
  23.177 -      ("Illegal type for datatype constructor: " ^ string_of_typ thy ty);
  23.178 -    val (tys, ty') = strip_type ty;
  23.179 -    val (tyco, vs) = ((apsnd o map) dest_TFree o dest_Type) ty'
  23.180 -      handle TYPE _ => err ();
  23.181 -    val sorts = if has_duplicates (eq_fst op =) vs then err ()
  23.182 -      else map snd vs;
  23.183 -    val vs_names = Name.invent_list [] "'a" (length vs);
  23.184 -    val vs_map = map fst vs ~~ vs_names;
  23.185 -    val vs' = vs_names ~~ sorts;
  23.186 -    val tys' = (map o map_type_tfree) (fn (v, sort) =>
  23.187 -      (TFree ((the o AList.lookup (op =) vs_map) v, sort))) tys
  23.188 -      handle Option => err ();
  23.189 -  in (tyco, (vs', (c, tys'))) end;
  23.190 -
  23.191 -in
  23.192 -
  23.193 -fun co_of_const thy const = gen_co_of_const thy const handle BAD msg => error msg;
  23.194 -fun co_of_const' thy const = SOME (gen_co_of_const thy const) handle BAD msg => NONE;
  23.195 -
  23.196 -fun no_args thy = length o fst o strip_type o mg_typ_of_const thy;
  23.197 -
  23.198 -end;
  23.199 -
  23.200 -fun cos_of_consts thy consts =
  23.201 -  let
  23.202 -    val raw_cos  = map (co_of_const thy) consts;
  23.203 -    val (tyco, (vs_names, sorts_cos)) = if (length o distinct (eq_fst op =)) raw_cos = 1
  23.204 -      then ((fst o hd) raw_cos, ((map fst o fst o snd o hd) raw_cos,
  23.205 -        map ((apfst o map) snd o snd) raw_cos))
  23.206 -      else error ("Term constructors not referring to the same type: "
  23.207 -        ^ commas (map (string_of_const thy) consts));
  23.208 -    val sorts = foldr1 ((uncurry o map2 o curry o Sorts.inter_sort) (Sign.classes_of thy))
  23.209 -      (map fst sorts_cos);
  23.210 -    val cos = map snd sorts_cos;
  23.211 -    val vs = vs_names ~~ sorts;
  23.212 -  in (tyco, (vs, cos)) end;
  23.213 +    fun no_constr (c, ty) = error ("Not a datatype constructor: " ^ string_of_const thy c
  23.214 +      ^ " :: " ^ string_of_typ thy ty);
  23.215 +    fun last_typ c_ty ty =
  23.216 +      let
  23.217 +        val frees = typ_tfrees ty;
  23.218 +        val (tyco, vs) = ((apsnd o map) (dest_TFree) o dest_Type o snd o strip_type) ty
  23.219 +          handle TYPE _ => no_constr c_ty
  23.220 +        val _ = if has_duplicates (eq_fst (op =)) vs then no_constr c_ty else ();
  23.221 +        val _ = if length frees <> length vs then no_constr c_ty else ();
  23.222 +      in (tyco, vs) end;
  23.223 +    fun ty_sorts (c, ty) =
  23.224 +      let
  23.225 +        val ty_decl = (Logic.unvarifyT o Sign.the_const_type thy) c;
  23.226 +        val (tyco, vs_decl) = last_typ (c, ty) ty_decl;
  23.227 +        val (_, vs) = last_typ (c, ty) ty;
  23.228 +      in ((tyco, map snd vs), (c, (map fst vs, ty_decl))) end;
  23.229 +    fun add ((tyco', sorts'), c) ((tyco, sorts), cs) =
  23.230 +      let
  23.231 +        val _ = if tyco' <> tyco
  23.232 +          then error "Different type constructors in constructor set"
  23.233 +          else ();
  23.234 +        val sorts'' = map2 (curry (Sorts.inter_sort (Sign.classes_of thy))) sorts' sorts
  23.235 +      in ((tyco, sorts), c :: cs) end;
  23.236 +    fun inst vs' (c, (vs, ty)) =
  23.237 +      let
  23.238 +        val the_v = the o AList.lookup (op =) (vs ~~ vs');
  23.239 +        val ty' = map_atyps (fn TFree (v, _) => TFree (the_v v)) ty;
  23.240 +      in (c, (fst o strip_type) ty') end;
  23.241 +    val c' :: cs' = map ty_sorts cs;
  23.242 +    val ((tyco, sorts), cs'') = fold add cs' (apsnd single c');
  23.243 +    val vs = Name.names Name.context "'a" sorts;
  23.244 +    val cs''' = map (inst vs) cs'';
  23.245 +  in (tyco, (vs, cs''')) end;
  23.246  
  23.247  
  23.248  (* dictionary values *)
  23.249  
  23.250 -fun typargs thy (c_ty as (c, ty)) =
  23.251 -  let
  23.252 -    val opt_class = AxClass.class_of_param thy c;
  23.253 -    val tys = Sign.const_typargs thy (c, ty);
  23.254 -  in case (opt_class, tys)
  23.255 -   of (SOME class, ty as [Type (tyco, tys')]) =>
  23.256 -        if can (Sorts.mg_domain (Sign.classes_of thy) tyco) [class]
  23.257 -        then tys' else ty
  23.258 -    | _ => tys
  23.259 -  end;
  23.260 -
  23.261  fun typ_sort_inst algebra =
  23.262    let
  23.263      val inters = Sorts.inter_sort algebra;
  23.264 @@ -324,10 +225,9 @@
  23.265  fun head_func thm =
  23.266    let
  23.267      val thy = Thm.theory_of_thm thm;
  23.268 -    val (Const (c_ty as (_, ty))) = (fst o strip_comb o fst o Logic.dest_equals
  23.269 +    val Const (c, ty) = (fst o strip_comb o fst o Logic.dest_equals
  23.270        o ObjectLogic.drop_judgment thy o Thm.plain_prop_of) thm;
  23.271 -    val const = const_of_cexpr thy c_ty;
  23.272 -  in (const, ty) end;
  23.273 +  in (c, ty) end;
  23.274  
  23.275  
  23.276  (* utilities *)
    24.1 --- a/src/Pure/Isar/isar_syn.ML	Fri Aug 24 14:14:18 2007 +0200
    24.2 +++ b/src/Pure/Isar/isar_syn.ML	Fri Aug 24 14:14:20 2007 +0200
    24.3 @@ -431,7 +431,7 @@
    24.4        || P.$$$ "advanced" |-- P.xname -- ((P.$$$ "\\<subseteq>" || P.$$$ "<") |-- P.!!! P.xname)
    24.5             >> Class.instance_sort_cmd
    24.6        || P.and_list1 P.arity -- Scan.repeat (SpecParse.opt_thm_name ":" -- P.prop)
    24.7 -           >> (fn (arities, defs) => Class.instance_arity_cmd arities defs)
    24.8 +           >> (fn (arities, defs) => Class.instance_arity_cmd arities defs (fold (Code.add_func false)))
    24.9      ) >> (Toplevel.print oo Toplevel.theory_to_proof));
   24.10  
   24.11  end;
   24.12 @@ -441,7 +441,7 @@
   24.13  
   24.14  val code_datatypeP =
   24.15    OuterSyntax.command "code_datatype" "define set of code datatype constructors" K.thy_decl
   24.16 -    (Scan.repeat1 P.term >> (Toplevel.theory o Code.add_datatype_consts_cmd));
   24.17 +    (Scan.repeat1 P.term >> (Toplevel.theory o Code.add_datatype_cmd));
   24.18  
   24.19  
   24.20  
    25.1 --- a/src/Tools/code/code_funcgr.ML	Fri Aug 24 14:14:18 2007 +0200
    25.2 +++ b/src/Tools/code/code_funcgr.ML	Fri Aug 24 14:14:20 2007 +0200
    25.3 @@ -10,17 +10,14 @@
    25.4  sig
    25.5    type T
    25.6    val timing: bool ref
    25.7 -  val funcs: T -> CodeUnit.const -> thm list
    25.8 -  val typ: T -> CodeUnit.const -> typ
    25.9 -  val all: T -> CodeUnit.const list
   25.10 +  val funcs: T -> string -> thm list
   25.11 +  val typ: T -> string -> typ
   25.12 +  val all: T -> string list
   25.13    val pretty: theory -> T -> Pretty.T
   25.14 -  val make: theory -> CodeUnit.const list -> T
   25.15 -  val make_consts: theory -> CodeUnit.const list -> CodeUnit.const list * T
   25.16 +  val make: theory -> string list -> T
   25.17 +  val make_consts: theory -> string list -> string list * T
   25.18    val eval_conv: theory -> (T -> cterm -> thm) -> cterm -> thm
   25.19    val eval_term: theory -> (T -> cterm -> 'a) -> cterm -> 'a
   25.20 -  val intervene: theory -> T -> T
   25.21 -    (*FIXME drop intervene as soon as possible*)
   25.22 -  structure Constgraph : GRAPH
   25.23  end
   25.24  
   25.25  structure CodeFuncgr : CODE_FUNCGR =
   25.26 @@ -28,23 +25,18 @@
   25.27  
   25.28  (** the graph type **)
   25.29  
   25.30 -structure Constgraph = GraphFun (
   25.31 -  type key = CodeUnit.const;
   25.32 -  val ord = CodeUnit.const_ord;
   25.33 -);
   25.34 -
   25.35 -type T = (typ * thm list) Constgraph.T;
   25.36 +type T = (typ * thm list) Graph.T;
   25.37  
   25.38  fun funcs funcgr =
   25.39 -  these o Option.map snd o try (Constgraph.get_node funcgr);
   25.40 +  these o Option.map snd o try (Graph.get_node funcgr);
   25.41  
   25.42  fun typ funcgr =
   25.43 -  fst o Constgraph.get_node funcgr;
   25.44 +  fst o Graph.get_node funcgr;
   25.45  
   25.46 -fun all funcgr = Constgraph.keys funcgr;
   25.47 +fun all funcgr = Graph.keys funcgr;
   25.48  
   25.49  fun pretty thy funcgr =
   25.50 -  AList.make (snd o Constgraph.get_node funcgr) (Constgraph.keys funcgr)
   25.51 +  AList.make (snd o Graph.get_node funcgr) (Graph.keys funcgr)
   25.52    |> (map o apfst) (CodeUnit.string_of_const thy)
   25.53    |> sort (string_ord o pairself fst)
   25.54    |> map (fn (s, thms) =>
   25.55 @@ -63,13 +55,9 @@
   25.56    |> (fold o fold_aterms) (fn Const c => f c | _ => I);
   25.57  
   25.58  fun consts_of (const, []) = []
   25.59 -  | consts_of (const, thms as thm :: _) = 
   25.60 +  | consts_of (const, thms as _ :: _) = 
   25.61        let
   25.62 -        val thy = Thm.theory_of_thm thm;
   25.63 -        val is_refl = curry CodeUnit.eq_const const;
   25.64 -        fun the_const c = case try (CodeUnit.const_of_cexpr thy) c
   25.65 -         of SOME const => if is_refl const then I else insert CodeUnit.eq_const const
   25.66 -          | NONE => I
   25.67 +        fun the_const (c, _) = if c = const then I else insert (op =) c
   25.68        in fold_consts the_const thms [] end;
   25.69  
   25.70  fun insts_of thy algebra c ty_decl ty =
   25.71 @@ -114,7 +102,7 @@
   25.72  
   25.73  local
   25.74  
   25.75 -exception INVALID of CodeUnit.const list * string;
   25.76 +exception INVALID of string list * string;
   25.77  
   25.78  fun resort_thms algebra tap_typ [] = []
   25.79    | resort_thms algebra tap_typ (thms as thm :: _) =
   25.80 @@ -123,11 +111,11 @@
   25.81          val cs = fold_consts (insert (op =)) thms [];
   25.82          fun match_const c (ty, ty_decl) =
   25.83            let
   25.84 -            val tys = CodeUnit.typargs thy (c, ty);
   25.85 -            val sorts = map (snd o dest_TVar) (CodeUnit.typargs thy (c, ty_decl));
   25.86 +            val tys = Sign.const_typargs thy (c, ty);
   25.87 +            val sorts = map (snd o dest_TVar) (Sign.const_typargs thy (c, ty_decl));
   25.88            in fold2 (curry (CodeUnit.typ_sort_inst algebra)) tys sorts end;
   25.89 -        fun match (c_ty as (c, ty)) =
   25.90 -          case tap_typ c_ty
   25.91 +        fun match (c, ty) =
   25.92 +          case tap_typ c
   25.93             of SOME ty_decl => match_const c (ty, ty_decl)
   25.94              | NONE => I;
   25.95          val tvars = fold match cs Vartab.empty;
   25.96 @@ -135,7 +123,7 @@
   25.97  
   25.98  fun resort_funcss thy algebra funcgr =
   25.99    let
  25.100 -    val typ_funcgr = try (fst o Constgraph.get_node funcgr o CodeUnit.const_of_cexpr thy);
  25.101 +    val typ_funcgr = try (fst o Graph.get_node funcgr);
  25.102      fun resort_dep (const, thms) = (const, resort_thms algebra typ_funcgr thms)
  25.103        handle Sorts.CLASS_ERROR e => raise INVALID ([const], Sorts.msg_class_error (Sign.pp thy) e
  25.104                      ^ ",\nfor constant " ^ CodeUnit.string_of_const thy const
  25.105 @@ -150,12 +138,11 @@
  25.106            in (Sign.typ_equiv thy (ty, ty'), (const, thms')) end;
  25.107      fun resort_recs funcss =
  25.108        let
  25.109 -        fun tap_typ c_ty = case try (CodeUnit.const_of_cexpr thy) c_ty
  25.110 -         of SOME const => AList.lookup (CodeUnit.eq_const) funcss const
  25.111 -              |> these
  25.112 -              |> try hd
  25.113 -              |> Option.map (snd o CodeUnit.head_func)
  25.114 -          | NONE => NONE;
  25.115 +        fun tap_typ c =
  25.116 +          AList.lookup (op =) funcss c
  25.117 +          |> these
  25.118 +          |> try hd
  25.119 +          |> Option.map (snd o CodeUnit.head_func);
  25.120          val (unchangeds, funcss') = split_list (map (resort_rec tap_typ) funcss);
  25.121          val unchanged = fold (fn x => fn y => x andalso y) unchangeds true;
  25.122        in (unchanged, funcss') end;
  25.123 @@ -172,7 +159,7 @@
  25.124        try (AxClass.params_of_class thy) class
  25.125        |> Option.map snd
  25.126        |> these
  25.127 -      |> map (fn (c, _) => (c, SOME tyco))
  25.128 +      |> map (fn (c, _) => Class.inst_const thy (c, tyco))
  25.129    in
  25.130      Symtab.empty
  25.131      |> fold (fn (tyco, class) =>
  25.132 @@ -184,8 +171,7 @@
  25.133  fun instances_of_consts thy algebra funcgr consts =
  25.134    let
  25.135      fun inst (cexpr as (c, ty)) = insts_of thy algebra c
  25.136 -      ((fst o Constgraph.get_node funcgr o CodeUnit.const_of_cexpr thy) cexpr)
  25.137 -      ty handle CLASS_ERROR => [];
  25.138 +      ((fst o Graph.get_node funcgr) c) ty handle CLASS_ERROR => [];
  25.139    in
  25.140      []
  25.141      |> fold (fold (insert (op =)) o inst) consts
  25.142 @@ -193,13 +179,13 @@
  25.143    end;
  25.144  
  25.145  fun ensure_const' thy algebra funcgr const auxgr =
  25.146 -  if can (Constgraph.get_node funcgr) const
  25.147 +  if can (Graph.get_node funcgr) const
  25.148      then (NONE, auxgr)
  25.149 -  else if can (Constgraph.get_node auxgr) const
  25.150 +  else if can (Graph.get_node auxgr) const
  25.151      then (SOME const, auxgr)
  25.152    else if is_some (Code.get_datatype_of_constr thy const) then
  25.153      auxgr
  25.154 -    |> Constgraph.new_node (const, [])
  25.155 +    |> Graph.new_node (const, [])
  25.156      |> pair (SOME const)
  25.157    else let
  25.158      val thms = Code.these_funcs thy const
  25.159 @@ -208,9 +194,9 @@
  25.160      val rhs = consts_of (const, thms);
  25.161    in
  25.162      auxgr
  25.163 -    |> Constgraph.new_node (const, thms)
  25.164 +    |> Graph.new_node (const, thms)
  25.165      |> fold_map (ensure_const thy algebra funcgr) rhs
  25.166 -    |-> (fn rhs' => fold (fn SOME const' => Constgraph.add_edge (const, const')
  25.167 +    |-> (fn rhs' => fold (fn SOME const' => Graph.add_edge (const, const')
  25.168                             | NONE => I) rhs')
  25.169      |> pair (SOME const)
  25.170    end
  25.171 @@ -225,24 +211,25 @@
  25.172    let
  25.173      val funcss = raw_funcss
  25.174        |> resort_funcss thy algebra funcgr
  25.175 -      |> filter_out (can (Constgraph.get_node funcgr) o fst);
  25.176 -    fun typ_func const [] = Code.default_typ thy const
  25.177 -      | typ_func (_, NONE) (thm :: _) = (snd o CodeUnit.head_func) thm
  25.178 -      | typ_func (const as (c, SOME tyco)) (thms as (thm :: _)) =
  25.179 -          let
  25.180 -            val (_, ty) = CodeUnit.head_func thm;
  25.181 -            val SOME class = AxClass.class_of_param thy c;
  25.182 -            val sorts_decl = Sorts.mg_domain algebra tyco [class];
  25.183 -            val tys = CodeUnit.typargs thy (c, ty);
  25.184 -            val sorts = map (snd o dest_TVar) tys;
  25.185 -          in if sorts = sorts_decl then ty
  25.186 -            else raise INVALID ([const], "Illegal instantation for class operation "
  25.187 -              ^ CodeUnit.string_of_const thy const
  25.188 -              ^ "\nin defining equations\n"
  25.189 -              ^ (cat_lines o map string_of_thm) thms)
  25.190 -          end;
  25.191 +      |> filter_out (can (Graph.get_node funcgr) o fst);
  25.192 +    fun typ_func c [] = Code.default_typ thy c
  25.193 +      | typ_func c (thms as thm :: _) = case Class.param_const thy c
  25.194 +         of SOME (c', tyco) => 
  25.195 +              let
  25.196 +                val (_, ty) = CodeUnit.head_func thm;
  25.197 +                val SOME class = AxClass.class_of_param thy c';
  25.198 +                val sorts_decl = Sorts.mg_domain algebra tyco [class];
  25.199 +                val tys = Sign.const_typargs thy (c, ty);
  25.200 +                val sorts = map (snd o dest_TVar) tys;
  25.201 +              in if sorts = sorts_decl then ty
  25.202 +                else raise INVALID ([c], "Illegal instantation for class operation "
  25.203 +                  ^ CodeUnit.string_of_const thy c
  25.204 +                  ^ "\nin defining equations\n"
  25.205 +                  ^ (cat_lines o map string_of_thm) thms)
  25.206 +              end
  25.207 +          | NONE => (snd o CodeUnit.head_func) thm;
  25.208      fun add_funcs (const, thms) =
  25.209 -      Constgraph.new_node (const, (typ_func const thms, thms));
  25.210 +      Graph.new_node (const, (typ_func const thms, thms));
  25.211      fun add_deps (funcs as (const, thms)) funcgr =
  25.212        let
  25.213          val deps = consts_of funcs;
  25.214 @@ -251,8 +238,8 @@
  25.215        in
  25.216          funcgr
  25.217          |> ensure_consts' thy algebra insts
  25.218 -        |> fold (curry Constgraph.add_edge const) deps
  25.219 -        |> fold (curry Constgraph.add_edge const) insts
  25.220 +        |> fold (curry Graph.add_edge const) deps
  25.221 +        |> fold (curry Graph.add_edge const) insts
  25.222         end;
  25.223    in
  25.224      funcgr
  25.225 @@ -261,29 +248,24 @@
  25.226    end
  25.227  and ensure_consts' thy algebra cs funcgr =
  25.228    let
  25.229 -    val auxgr = Constgraph.empty
  25.230 +    val auxgr = Graph.empty
  25.231        |> fold (snd oo ensure_const thy algebra funcgr) cs;
  25.232    in
  25.233      funcgr
  25.234      |> fold (merge_funcss thy algebra)
  25.235 -         (map (AList.make (Constgraph.get_node auxgr))
  25.236 -         (rev (Constgraph.strong_conn auxgr)))
  25.237 +         (map (AList.make (Graph.get_node auxgr))
  25.238 +         (rev (Graph.strong_conn auxgr)))
  25.239    end handle INVALID (cs', msg)
  25.240 -    => raise INVALID (fold (insert CodeUnit.eq_const) cs' cs, msg);
  25.241 -
  25.242 -fun ensure_consts thy consts funcgr =
  25.243 -  let
  25.244 -    val algebra = Code.coregular_algebra thy
  25.245 -  in ensure_consts' thy algebra consts funcgr
  25.246 -    handle INVALID (cs', msg) => error (msg ^ ",\nwhile preprocessing equations for constant(s) "
  25.247 -    ^ commas (map (CodeUnit.string_of_const thy) cs'))
  25.248 -  end;
  25.249 +    => raise INVALID (fold (insert (op =)) cs' cs, msg);
  25.250  
  25.251  in
  25.252  
  25.253  (** retrieval interfaces **)
  25.254  
  25.255 -val ensure_consts = ensure_consts;
  25.256 +fun ensure_consts thy algebra consts funcgr =
  25.257 +  ensure_consts' thy algebra consts funcgr
  25.258 +    handle INVALID (cs', msg) => error (msg ^ ",\nwhile preprocessing equations for constant(s) "
  25.259 +    ^ commas (map (CodeUnit.string_of_const thy) cs'));
  25.260  
  25.261  fun check_consts thy consts funcgr =
  25.262    let
  25.263 @@ -294,25 +276,20 @@
  25.264      val (consts', funcgr') = fold_map try_const consts funcgr;
  25.265    in (map_filter I consts', funcgr') end;
  25.266  
  25.267 -fun ensure_consts_term_proto thy f ct funcgr =
  25.268 +fun raw_eval thy f ct funcgr =
  25.269    let
  25.270 -    fun consts_of thy t =
  25.271 -      fold_aterms (fn Const c => cons (CodeUnit.const_of_cexpr thy c) | _ => I) t []
  25.272 -    fun rhs_conv conv thm =
  25.273 -      let
  25.274 -        val thm' = (conv o Thm.rhs_of) thm;
  25.275 -      in Thm.transitive thm thm' end
  25.276 +    val algebra = Code.coregular_algebra thy;
  25.277 +    fun consts_of ct = fold_aterms (fn Const c_ty => cons c_ty | _ => I)
  25.278 +      (Thm.term_of ct) [];
  25.279      val _ = Sign.no_vars (Sign.pp thy) (Thm.term_of ct);
  25.280      val _ = Term.fold_types (Type.no_tvars #> K I) (Thm.term_of ct) ();
  25.281      val thm1 = Code.preprocess_conv ct;
  25.282      val ct' = Thm.rhs_of thm1;
  25.283 -    val consts = consts_of thy (Thm.term_of ct');
  25.284 -    val funcgr' = ensure_consts thy consts funcgr;
  25.285 -    val algebra = Code.coregular_algebra thy;
  25.286 +    val cs = map fst (consts_of ct');
  25.287 +    val funcgr' = ensure_consts thy algebra cs funcgr;
  25.288      val (_, thm2) = Thm.varifyT' [] thm1;
  25.289      val thm3 = Thm.reflexive (Thm.rhs_of thm2);
  25.290 -    val typ_funcgr = try (fst o Constgraph.get_node funcgr' o CodeUnit.const_of_cexpr thy);
  25.291 -    val [thm4] = resort_thms algebra typ_funcgr [thm3];
  25.292 +    val [thm4] = resort_thms algebra (try (fst o Graph.get_node funcgr')) [thm3];
  25.293      val tfrees = Term.add_tfrees (Thm.prop_of thm1) [];
  25.294      fun inst thm =
  25.295        let
  25.296 @@ -323,56 +300,54 @@
  25.297      val thm5 = inst thm2;
  25.298      val thm6 = inst thm4;
  25.299      val ct'' = Thm.rhs_of thm6;
  25.300 -    val cs = fold_aterms (fn Const c => cons c | _ => I) (Thm.term_of ct'') [];
  25.301 +    val c_exprs = consts_of ct'';
  25.302      val drop = drop_classes thy tfrees;
  25.303 -    val instdefs = instances_of_consts thy algebra funcgr' cs;
  25.304 -    val funcgr'' = ensure_consts thy instdefs funcgr';
  25.305 -  in (f funcgr'' drop ct'' thm5, funcgr'') end;
  25.306 +    val instdefs = instances_of_consts thy algebra funcgr' c_exprs;
  25.307 +    val funcgr'' = ensure_consts thy algebra instdefs funcgr';
  25.308 +  in (f drop thm5 funcgr'' ct'' , funcgr'') end;
  25.309  
  25.310 -fun ensure_consts_eval thy conv =
  25.311 +fun raw_eval_conv thy conv =
  25.312    let
  25.313 -    fun conv' funcgr drop_classes ct thm1 =
  25.314 +    fun conv' drop_classes thm1 funcgr ct =
  25.315        let
  25.316          val thm2 = conv funcgr ct;
  25.317          val thm3 = Code.postprocess_conv (Thm.rhs_of thm2);
  25.318          val thm23 = drop_classes (Thm.transitive thm2 thm3);
  25.319        in
  25.320          Thm.transitive thm1 thm23 handle THM _ =>
  25.321 -          error ("eval_conv - could not construct proof:\n"
  25.322 +          error ("could not construct proof:\n"
  25.323            ^ (cat_lines o map string_of_thm) [thm1, thm2, thm3])
  25.324        end;
  25.325 -  in ensure_consts_term_proto thy conv' end;
  25.326 +  in raw_eval thy conv' end;
  25.327  
  25.328 -fun ensure_consts_term thy f =
  25.329 +fun raw_eval_term thy f =
  25.330    let
  25.331 -    fun f' funcgr drop_classes ct thm1 = f funcgr ct;
  25.332 -  in ensure_consts_term_proto thy f' end;
  25.333 +    fun f' _ _ funcgr ct = f funcgr ct;
  25.334 +  in raw_eval thy f' end;
  25.335  
  25.336  end; (*local*)
  25.337  
  25.338  structure Funcgr = CodeDataFun
  25.339  (struct
  25.340    type T = T;
  25.341 -  val empty = Constgraph.empty;
  25.342 -  fun merge _ _ = Constgraph.empty;
  25.343 -  fun purge _ NONE _ = Constgraph.empty
  25.344 +  val empty = Graph.empty;
  25.345 +  fun merge _ _ = Graph.empty;
  25.346 +  fun purge _ NONE _ = Graph.empty
  25.347      | purge _ (SOME cs) funcgr =
  25.348 -        Constgraph.del_nodes ((Constgraph.all_preds funcgr 
  25.349 -          o filter (can (Constgraph.get_node funcgr))) cs) funcgr;
  25.350 +        Graph.del_nodes ((Graph.all_preds funcgr 
  25.351 +          o filter (can (Graph.get_node funcgr))) cs) funcgr;
  25.352  end);
  25.353  
  25.354  fun make thy =
  25.355 -  Funcgr.change thy o ensure_consts thy;
  25.356 +  Funcgr.change thy o ensure_consts thy (Code.coregular_algebra thy);
  25.357  
  25.358  fun make_consts thy =
  25.359    Funcgr.change_yield thy o check_consts thy;
  25.360  
  25.361  fun eval_conv thy f =
  25.362 -  fst o Funcgr.change_yield thy o ensure_consts_eval thy f;
  25.363 +  fst o Funcgr.change_yield thy o raw_eval_conv thy f;
  25.364  
  25.365  fun eval_term thy f =
  25.366 -  fst o Funcgr.change_yield thy o ensure_consts_term thy f;
  25.367 -
  25.368 -fun intervene thy funcgr = Funcgr.change thy (K funcgr);
  25.369 +  fst o Funcgr.change_yield thy o raw_eval_term thy f;
  25.370  
  25.371  end; (*struct*)
    26.1 --- a/src/Tools/code/code_name.ML	Fri Aug 24 14:14:18 2007 +0200
    26.2 +++ b/src/Tools/code/code_name.ML	Fri Aug 24 14:14:20 2007 +0200
    26.3 @@ -17,18 +17,16 @@
    26.4    val intro_vars: string list -> var_ctxt -> var_ctxt;
    26.5    val lookup_var: var_ctxt -> string -> string;
    26.6  
    26.7 -  type tyco = string
    26.8 -  type const = string
    26.9    val class: theory -> class -> class
   26.10    val class_rev: theory -> class -> class option
   26.11    val classrel: theory -> class * class -> string
   26.12    val classrel_rev: theory -> string -> (class * class) option
   26.13 -  val tyco: theory -> tyco -> tyco
   26.14 -  val tyco_rev: theory -> tyco -> tyco option
   26.15 -  val instance: theory -> class * tyco -> string
   26.16 -  val instance_rev: theory -> string -> (class * tyco) option
   26.17 -  val const: theory -> CodeUnit.const -> const
   26.18 -  val const_rev: theory -> const -> CodeUnit.const option
   26.19 +  val tyco: theory -> string -> string
   26.20 +  val tyco_rev: theory -> string -> string option
   26.21 +  val instance: theory -> class * string -> string
   26.22 +  val instance_rev: theory -> string -> (class * string) option
   26.23 +  val const: theory -> string -> string
   26.24 +  val const_rev: theory -> string -> string option
   26.25    val labelled_name: theory -> string -> string
   26.26  
   26.27    val setup: theory -> theory
   26.28 @@ -186,8 +184,7 @@
   26.29    #> NameSpace.explode
   26.30    #> map (purify_name true);
   26.31  
   26.32 -fun purify_base "op =" = "eq"
   26.33 -  | purify_base "op &" = "and"
   26.34 +fun purify_base "op &" = "and"
   26.35    | purify_base "op |" = "or"
   26.36    | purify_base "op -->" = "implies"
   26.37    | purify_base "{}" = "empty"
   26.38 @@ -196,7 +193,9 @@
   26.39    | purify_base "op Un" = "union"
   26.40    | purify_base "*" = "product"
   26.41    | purify_base "+" = "sum"
   26.42 -  | purify_base s = purify_name false s;
   26.43 +  | purify_base s = if String.isPrefix "op =" s
   26.44 +      then "eq" ^ purify_name false s
   26.45 +      else purify_name false s;
   26.46  
   26.47  fun default_policy thy get_basename get_thyname name =
   26.48    let
   26.49 @@ -212,30 +211,28 @@
   26.50  fun instance_policy thy = default_policy thy (fn (class, tyco) => 
   26.51    NameSpace.base class ^ "_" ^ NameSpace.base tyco) thyname_of_instance;
   26.52  
   26.53 -fun force_thyname thy (const as (c, opt_tyco)) =
   26.54 -  case Code.get_datatype_of_constr thy const
   26.55 -   of SOME dtco => SOME (thyname_of_tyco thy dtco)
   26.56 -    | NONE => (case AxClass.class_of_param thy c
   26.57 -       of SOME class => (case opt_tyco
   26.58 -           of SOME tyco => SOME (thyname_of_instance thy (class, tyco))
   26.59 -            | NONE => SOME (thyname_of_class thy class))
   26.60 -        | NONE => NONE);
   26.61 +fun force_thyname thy c = case Code.get_datatype_of_constr thy c
   26.62 + of SOME dtco => SOME (thyname_of_tyco thy dtco)
   26.63 +  | NONE => (case AxClass.class_of_param thy c
   26.64 +     of SOME class => SOME (thyname_of_class thy class)
   26.65 +      | NONE => (case Class.param_const thy c
   26.66 +         of SOME (c, tyco) => SOME (thyname_of_instance thy
   26.67 +              ((the o AxClass.class_of_param thy) c, tyco))
   26.68 +          | NONE => NONE));
   26.69  
   26.70 -fun const_policy thy (const as (c, opt_tyco)) =
   26.71 -  case force_thyname thy const
   26.72 +fun const_policy thy c =
   26.73 +  case force_thyname thy c
   26.74     of NONE => default_policy thy NameSpace.base thyname_of_const c
   26.75      | SOME thyname => let
   26.76          val prefix = purify_prefix thyname;
   26.77 -        val tycos = the_list opt_tyco;
   26.78 -        val base = map (purify_base o NameSpace.base) (c :: tycos);
   26.79 -      in NameSpace.implode (prefix @ [space_implode "_" base]) end;
   26.80 +        val base = (purify_base o NameSpace.base) c;
   26.81 +      in NameSpace.implode (prefix @ [base]) end;
   26.82  
   26.83  
   26.84  (* theory and code data *)
   26.85  
   26.86  type tyco = string;
   26.87  type const = string;
   26.88 -structure Consttab = CodeUnit.Consttab;
   26.89  
   26.90  structure StringPairTab =
   26.91    TableFun(
   26.92 @@ -294,14 +291,14 @@
   26.93  
   26.94  structure ConstName = CodeDataFun
   26.95  (
   26.96 -  type T = const Consttab.table * (string * string option) Symtab.table;
   26.97 -  val empty = (Consttab.empty, Symtab.empty);
   26.98 +  type T = const Symtab.table * string Symtab.table;
   26.99 +  val empty = (Symtab.empty, Symtab.empty);
  26.100    fun merge _ ((const1, constrev1), (const2, constrev2)) : T =
  26.101 -    (Consttab.merge (op =) (const1, const2),
  26.102 -      Symtab.merge CodeUnit.eq_const (constrev1, constrev2));
  26.103 +    (Symtab.merge (op =) (const1, const2),
  26.104 +      Symtab.merge (op =) (constrev1, constrev2));
  26.105    fun purge _ NONE _ = empty
  26.106 -    | purge _ (SOME cs) (const, constrev) = (fold Consttab.delete_safe cs const,
  26.107 -        fold Symtab.delete (map_filter (Consttab.lookup const) cs) constrev);
  26.108 +    | purge _ (SOME cs) (const, constrev) = (fold Symtab.delete_safe cs const,
  26.109 +        fold Symtab.delete_safe (map_filter (Symtab.lookup const) cs) constrev);
  26.110  );
  26.111  
  26.112  val setup = CodeName.init;
  26.113 @@ -333,10 +330,10 @@
  26.114      val tabs = ConstName.get thy;
  26.115      fun declare name =
  26.116        let
  26.117 -        val names' = (Consttab.update (const, name) (fst tabs),
  26.118 +        val names' = (Symtab.update (const, name) (fst tabs),
  26.119            Symtab.update_new (name, const) (snd tabs))
  26.120        in (ConstName.change thy (K names'); name) end;
  26.121 -  in case Consttab.lookup (fst tabs) const
  26.122 +  in case Symtab.lookup (fst tabs) const
  26.123     of SOME name => name
  26.124      | NONE => 
  26.125          const
    27.1 --- a/src/Tools/code/code_package.ML	Fri Aug 24 14:14:18 2007 +0200
    27.2 +++ b/src/Tools/code/code_package.ML	Fri Aug 24 14:14:20 2007 +0200
    27.3 @@ -45,35 +45,25 @@
    27.4    -> CodeFuncgr.T
    27.5    -> (string * typ) * term list -> CodeThingol.transact -> iterm * CodeThingol.transact;
    27.6  
    27.7 -type appgens = (int * (appgen * stamp)) Symtab.table;
    27.8 -val merge_appgens : appgens * appgens -> appgens =
    27.9 -  Symtab.merge (fn ((bounds1, (_, stamp1)), (bounds2, (_, stamp2))) =>
   27.10 -    bounds1 = bounds2 andalso stamp1 = stamp2);
   27.11 -
   27.12 -structure Consttab = CodeUnit.Consttab;
   27.13 -type abstypes = typ Symtab.table * CodeUnit.const Consttab.table;
   27.14 -fun merge_abstypes ((typs1, consts1) : abstypes, (typs2, consts2) : abstypes) =
   27.15 -  (Symtab.merge (Type.eq_type Vartab.empty) (typs1, typs2),
   27.16 -    Consttab.merge CodeUnit.eq_const (consts1, consts2));
   27.17 -
   27.18 -structure Translation = TheoryDataFun
   27.19 +structure Appgens = TheoryDataFun
   27.20  (
   27.21 -  type T = appgens * abstypes;
   27.22 -  val empty = (Symtab.empty, (Symtab.empty, Consttab.empty));
   27.23 +  type T = (int * (appgen * stamp)) Symtab.table;
   27.24 +  val empty = Symtab.empty;
   27.25    val copy = I;
   27.26    val extend = I;
   27.27 -  fun merge _ ((appgens1, abstypes1), (appgens2, abstypes2)) =
   27.28 -    (merge_appgens (appgens1, appgens2), merge_abstypes (abstypes1, abstypes2));
   27.29 +  fun merge _ = Symtab.merge (fn ((bounds1, (_, stamp1)), (bounds2, (_, stamp2))) =>
   27.30 +    bounds1 = bounds2 andalso stamp1 = stamp2);
   27.31  );
   27.32  
   27.33  fun code_depgr thy [] = CodeFuncgr.make thy []
   27.34    | code_depgr thy consts =
   27.35        let
   27.36          val gr = CodeFuncgr.make thy consts;
   27.37 -        val select = CodeFuncgr.Constgraph.all_succs gr consts;
   27.38 +        val select = Graph.all_succs gr consts;
   27.39        in
   27.40 -        CodeFuncgr.Constgraph.subgraph
   27.41 -          (member CodeUnit.eq_const select) gr
   27.42 +        gr
   27.43 +        |> Graph.subgraph (member (op =) select) 
   27.44 +        |> Graph.map_nodes ((apsnd o map) (Conv.fconv_rule (Class.overload thy)))
   27.45        end;
   27.46  
   27.47  fun code_thms thy =
   27.48 @@ -89,7 +79,7 @@
   27.49        in { name = name, ID = name, dir = "", unfold = true,
   27.50          path = "", parents = nameparents }
   27.51        end;
   27.52 -    val prgr = CodeFuncgr.Constgraph.fold ((fn x => fn xs => xs @ [x]) o mk_entry) gr [];
   27.53 +    val prgr = Graph.fold ((fn x => fn xs => xs @ [x]) o mk_entry) gr [];
   27.54    in Present.display_graph prgr end;
   27.55  
   27.56  structure Program = CodeDataFun
   27.57 @@ -105,7 +95,7 @@
   27.58              map_filter (CodeName.const_rev thy) (Graph.keys code);
   27.59            val dels = (Graph.all_preds code
   27.60                o map (CodeName.const thy)
   27.61 -              o filter (member CodeUnit.eq_const cs_exisiting)
   27.62 +              o filter (member (op =) cs_exisiting)
   27.63              ) cs;
   27.64          in Graph.del_nodes dels code end;
   27.65  );
   27.66 @@ -113,10 +103,6 @@
   27.67  
   27.68  (* translation kernel *)
   27.69  
   27.70 -fun get_abstype thy (tyco, tys) = case Symtab.lookup ((fst o snd o Translation.get) thy) tyco
   27.71 - of SOME ty => SOME ((map_atyps (fn TFree (n, _) => nth tys (the (Int.fromString n)))) ty)
   27.72 -  | NONE => NONE;
   27.73 -
   27.74  val value_name = "Isabelle_Eval.EVAL.EVAL";
   27.75  
   27.76  fun ensure_def thy = CodeThingol.ensure_def
   27.77 @@ -128,7 +114,7 @@
   27.78      val (v, cs) = AxClass.params_of_class thy class;
   27.79      val class' = CodeName.class thy class;
   27.80      val classrels' = map (curry (CodeName.classrel thy) class) superclasses;
   27.81 -    val classops' = map (CodeName.const thy o CodeUnit.const_of_cexpr thy) cs;
   27.82 +    val classops' = map (CodeName.const thy o fst) cs;
   27.83      val defgen_class =
   27.84        fold_map (ensure_def_class thy algbr funcgr) superclasses
   27.85        ##>> (fold_map (exprgen_typ thy algbr funcgr) o map snd) cs
   27.86 @@ -152,9 +138,7 @@
   27.87              fold_map (exprgen_tyvar_sort thy algbr funcgr) vs
   27.88              ##>> fold_map (fn (c, tys) =>
   27.89                fold_map (exprgen_typ thy algbr funcgr) tys
   27.90 -              #>> (fn tys' =>
   27.91 -                ((CodeName.const thy o CodeUnit.const_of_cexpr thy)
   27.92 -                  (c, tys ---> Type (tyco, map TFree vs)), tys'))) cos
   27.93 +              #>> (fn tys' => (CodeName.const thy c, tys'))) cos
   27.94              #>> (fn (vs, cos) => CodeThingol.Datatype (vs, cos))
   27.95            end;
   27.96          val tyco' = CodeName.tyco thy tyco;
   27.97 @@ -171,15 +155,10 @@
   27.98        |> exprgen_tyvar_sort thy algbr funcgr vs
   27.99        |>> (fn (v, sort) => ITyVar v)
  27.100    | exprgen_typ thy algbr funcgr (Type (tyco, tys)) trns =
  27.101 -      case get_abstype thy (tyco, tys)
  27.102 -       of SOME ty =>
  27.103 -            trns
  27.104 -            |> exprgen_typ thy algbr funcgr ty
  27.105 -        | NONE =>
  27.106 -            trns
  27.107 -            |> ensure_def_tyco thy algbr funcgr tyco
  27.108 -            ||>> fold_map (exprgen_typ thy algbr funcgr) tys
  27.109 -            |>> (fn (tyco, tys) => tyco `%% tys);
  27.110 +      trns
  27.111 +      |> ensure_def_tyco thy algbr funcgr tyco
  27.112 +      ||>> fold_map (exprgen_typ thy algbr funcgr) tys
  27.113 +      |>> (fn (tyco, tys) => tyco `%% tys);
  27.114  
  27.115  exception CONSTRAIN of (string * typ) * typ;
  27.116  val timing = ref false;
  27.117 @@ -216,10 +195,8 @@
  27.118    end
  27.119  and exprgen_dict_parms thy (algbr as (_, consts)) funcgr (c, ty_ctxt) =
  27.120    let
  27.121 -    val c' = CodeUnit.const_of_cexpr thy (c, ty_ctxt)
  27.122 -    val idf = CodeName.const thy c';
  27.123 -    val ty_decl = Consts.the_declaration consts idf;
  27.124 -    val (tys, tys_decl) = pairself (curry (Consts.typargs consts) idf) (ty_ctxt, ty_decl);
  27.125 +    val ty_decl = Consts.the_declaration consts c;
  27.126 +    val (tys, tys_decl) = pairself (curry (Consts.typargs consts) c) (ty_ctxt, ty_decl);
  27.127      val sorts = map (snd o dest_TVar) tys_decl;
  27.128    in
  27.129      fold_map (exprgen_dicts thy algbr funcgr) (tys ~~ sorts)
  27.130 @@ -237,10 +214,11 @@
  27.131        ||>> exprgen_dicts thy algbr funcgr (arity_typ, [superclass])
  27.132        |>> (fn ((superclass, classrel), [DictConst (inst, dss)]) =>
  27.133              (superclass, (classrel, (inst, dss))));
  27.134 -    fun gen_classop_def (classop as (c, ty)) trns =
  27.135 +    fun gen_classop_def (c, ty) trns =
  27.136        trns
  27.137 -      |> ensure_def_const thy algbr funcgr (CodeUnit.const_of_cexpr thy classop)
  27.138 -      ||>> exprgen_term thy algbr funcgr (Const (c, map_type_tfree (K arity_typ) ty));
  27.139 +      |> ensure_def_const thy algbr funcgr c
  27.140 +      ||>> exprgen_term thy algbr funcgr
  27.141 +            (Const (Class.inst_const thy (c, tyco), map_type_tfree (K arity_typ) ty));
  27.142      fun defgen_inst trns =
  27.143        trns
  27.144        |> ensure_def_class thy algbr funcgr class
  27.145 @@ -256,13 +234,13 @@
  27.146      |> ensure_def thy defgen_inst ("generating instance " ^ quote class ^ " / " ^ quote tyco) inst
  27.147      |> pair inst
  27.148    end
  27.149 -and ensure_def_const thy (algbr as (_, consts)) funcgr (const as (c, opt_tyco)) =
  27.150 +and ensure_def_const thy (algbr as (_, consts)) funcgr c =
  27.151    let
  27.152 -    val c' = CodeName.const thy const;
  27.153 +    val c' = CodeName.const thy c;
  27.154      fun defgen_datatypecons trns =
  27.155        trns 
  27.156        |> ensure_def_tyco thy algbr funcgr
  27.157 -          ((the o Code.get_datatype_of_constr thy) const)
  27.158 +          ((the o Code.get_datatype_of_constr thy) c)
  27.159        |>> (fn _ => CodeThingol.Bot);
  27.160      fun defgen_classop trns =
  27.161        trns 
  27.162 @@ -271,15 +249,14 @@
  27.163        |>> (fn _ => CodeThingol.Bot);
  27.164      fun defgen_fun trns =
  27.165        let
  27.166 -        val const' = perhaps (Consttab.lookup ((snd o snd o Translation.get) thy)) const;
  27.167 -        val raw_thms = CodeFuncgr.funcs funcgr const';
  27.168 -        val ty = (Logic.unvarifyT o CodeFuncgr.typ funcgr) const';
  27.169 +        val raw_thms = CodeFuncgr.funcs funcgr c;
  27.170 +        val ty = (Logic.unvarifyT o CodeFuncgr.typ funcgr) c;
  27.171          val thms = if (null o Term.typ_tfrees) ty orelse (null o fst o strip_type) ty
  27.172            then raw_thms
  27.173            else map (CodeUnit.expand_eta 1) raw_thms;
  27.174 -        val timeap = if !timing then Output.timeap_msg ("time for " ^ c')
  27.175 +        val timeap = if !timing then Output.timeap_msg ("time for " ^ c)
  27.176            else I;
  27.177 -        val vs = (map dest_TFree o Consts.typargs consts) (c', ty);
  27.178 +        val vs = (map dest_TFree o Consts.typargs consts) (c, ty);
  27.179          val dest_eqthm =
  27.180            apfst (snd o strip_comb) o Logic.dest_equals o Logic.unvarify o prop_of;
  27.181          fun exprgen_eq (args, rhs) =
  27.182 @@ -292,14 +269,13 @@
  27.183          ||>> timeap (fold_map (exprgen_eq o dest_eqthm) thms)
  27.184          |>> (fn ((vs, ty), eqs) => CodeThingol.Fun ((vs, ty), eqs))
  27.185        end;
  27.186 -    val defgen = if (is_some o Code.get_datatype_of_constr thy) const
  27.187 +    val defgen = if (is_some o Code.get_datatype_of_constr thy) c
  27.188        then defgen_datatypecons
  27.189 -      else if is_some opt_tyco
  27.190 -        orelse (not o is_some o AxClass.class_of_param thy) c
  27.191 -      then defgen_fun
  27.192 -      else defgen_classop
  27.193 +      else if (is_some o AxClass.class_of_param thy) c
  27.194 +      then defgen_classop
  27.195 +      else defgen_fun
  27.196    in
  27.197 -    ensure_def thy defgen ("generating constant " ^ CodeUnit.string_of_const thy const) c'
  27.198 +    ensure_def thy defgen ("generating constant " ^ CodeUnit.string_of_const thy c) c'
  27.199      #> pair c'
  27.200    end
  27.201  and exprgen_term thy algbr funcgr (Const (c, ty)) trns =
  27.202 @@ -330,14 +306,14 @@
  27.203              |>> (fn (t, ts) => t `$$ ts)
  27.204  and appgen_default thy algbr funcgr ((c, ty), ts) trns =
  27.205    trns
  27.206 -  |> ensure_def_const thy algbr funcgr (CodeUnit.const_of_cexpr thy (c, ty))
  27.207 +  |> ensure_def_const thy algbr funcgr c
  27.208    ||>> fold_map (exprgen_typ thy algbr funcgr) ((fst o Term.strip_type) ty)
  27.209    ||>> exprgen_typ thy algbr funcgr ((snd o Term.strip_type) ty)
  27.210    ||>> exprgen_dict_parms thy algbr funcgr (c, ty)
  27.211    ||>> fold_map (exprgen_term thy algbr funcgr) ts
  27.212    |>> (fn ((((c, tys), ty), iss), ts) => IConst (c, (iss, tys)) `$$ ts)
  27.213  and select_appgen thy algbr funcgr ((c, ty), ts) trns =
  27.214 -  case Symtab.lookup (fst (Translation.get thy)) c
  27.215 +  case Symtab.lookup (Appgens.get thy) c
  27.216     of SOME (i, (appgen, _)) =>
  27.217          if length ts < i then
  27.218            let
  27.219 @@ -396,7 +372,9 @@
  27.220    let
  27.221      val SOME ([], ((st, sty), ds)) = dest_case_expr thy (list_comb (Const c_ty, ts));
  27.222      fun clause_gen (dt, bt) =
  27.223 -      exprgen_term thy algbr funcgr dt
  27.224 +      exprgen_term thy algbr funcgr
  27.225 +        (map_aterms (fn Const (c_ty as (c, ty)) => Const
  27.226 +          (Class.unoverload_const thy c_ty, ty) | t => t) dt)
  27.227        ##>> exprgen_term thy algbr funcgr bt;
  27.228    in
  27.229      exprgen_term thy algbr funcgr st
  27.230 @@ -429,107 +407,25 @@
  27.231      val i = (length o fst o strip_type o Sign.the_const_type thy) c;
  27.232      val _ = Program.change thy (K CodeThingol.empty_code);
  27.233    in
  27.234 -    (Translation.map o apfst)
  27.235 -      (Symtab.update (c, (i, (appgen, stamp ())))) thy
  27.236 +    Appgens.map (Symtab.update (c, (i, (appgen, stamp ())))) thy
  27.237    end;
  27.238  
  27.239  
  27.240 -
  27.241 -(** abstype and constsubst interface **)
  27.242 -
  27.243 -local
  27.244 -
  27.245 -fun add_consts thy f (c1, c2 as (c, opt_tyco)) =
  27.246 -  let
  27.247 -    val _ = if
  27.248 -        is_some (AxClass.class_of_param thy c) andalso is_none opt_tyco
  27.249 -        orelse is_some (Code.get_datatype_of_constr thy c2)
  27.250 -      then error ("Not a function: " ^ CodeUnit.string_of_const thy c2)
  27.251 -      else ();
  27.252 -    val funcgr = CodeFuncgr.make thy [c1, c2];
  27.253 -    val ty1 = (f o CodeFuncgr.typ funcgr) c1;
  27.254 -    val ty2 = CodeFuncgr.typ funcgr c2;
  27.255 -    val _ = if Sign.typ_equiv thy (ty1, ty2) then () else
  27.256 -      error ("Incompatiable type signatures of " ^ CodeUnit.string_of_const thy c1
  27.257 -        ^ " and " ^ CodeUnit.string_of_const thy c2 ^ ":\n"
  27.258 -        ^ CodeUnit.string_of_typ thy ty1 ^ "\n" ^ CodeUnit.string_of_typ thy ty2);
  27.259 -  in Consttab.update (c1, c2) end;
  27.260 -
  27.261 -fun gen_abstyp prep_const prep_typ (raw_abstyp, raw_substtyp) raw_absconsts thy =
  27.262 -  let
  27.263 -    val abstyp = Type.no_tvars (prep_typ thy raw_abstyp);
  27.264 -    val substtyp = Type.no_tvars (prep_typ thy raw_substtyp);
  27.265 -    val absconsts = (map o pairself) (prep_const thy) raw_absconsts;
  27.266 -    val Type (abstyco, tys) = abstyp handle BIND => error ("Bad type: " ^ Sign.string_of_typ thy abstyp);
  27.267 -    val typarms = map (fst o dest_TFree) tys handle MATCH => error ("Bad type: " ^ Sign.string_of_typ thy abstyp);
  27.268 -    fun mk_index v = 
  27.269 -      let
  27.270 -        val k = find_index (fn w => v = w) typarms;
  27.271 -      in if k = ~1
  27.272 -        then error ("Free type variable: " ^ quote v)
  27.273 -        else TFree (string_of_int k, [])
  27.274 -      end;
  27.275 -    val typpat = map_atyps (fn TFree (v, _) => mk_index v) substtyp;
  27.276 -    fun apply_typpat (Type (tyco, tys)) =
  27.277 -          let
  27.278 -            val tys' = map apply_typpat tys;
  27.279 -          in if tyco = abstyco then
  27.280 -            (map_atyps (fn TFree (n, _) => nth tys' (the (Int.fromString n)))) typpat
  27.281 -          else
  27.282 -            Type (tyco, tys')
  27.283 -          end
  27.284 -      | apply_typpat ty = ty;
  27.285 -    val _ = Program.change thy (K CodeThingol.empty_code);
  27.286 -  in
  27.287 -    thy
  27.288 -    |> (Translation.map o apsnd) (fn (abstypes, abscs) =>
  27.289 -          (abstypes
  27.290 -          |> Symtab.update (abstyco, typpat),
  27.291 -          abscs
  27.292 -          |> fold (add_consts thy apply_typpat) absconsts)
  27.293 -       )
  27.294 -  end;
  27.295 -
  27.296 -fun gen_constsubst prep_const raw_constsubsts thy =
  27.297 -  let
  27.298 -    val constsubsts = (map o pairself) (prep_const thy) raw_constsubsts;
  27.299 -    val _ = Program.change thy (K CodeThingol.empty_code);
  27.300 -  in
  27.301 -    thy
  27.302 -    |> (Translation.map o apsnd o apsnd) (fold (add_consts thy I) constsubsts)
  27.303 -  end;
  27.304 -
  27.305 -in
  27.306 -
  27.307 -val abstyp = gen_abstyp (K I) Sign.certify_typ;
  27.308 -val abstyp_e = gen_abstyp CodeUnit.read_const Sign.read_typ;
  27.309 -
  27.310 -val constsubst = gen_constsubst (K I);
  27.311 -val constsubst_e = gen_constsubst CodeUnit.read_const;
  27.312 -
  27.313 -end; (*local*)
  27.314 -
  27.315 -
  27.316  (** code generation interfaces **)
  27.317  
  27.318  (* generic generation combinators *)
  27.319  
  27.320  fun generate thy funcgr gen it =
  27.321    let
  27.322 -    (*FIXME*)
  27.323 -    val _ = CodeFuncgr.intervene thy funcgr;
  27.324 -    val cs = map_filter (Consttab.lookup ((snd o snd o Translation.get) thy))
  27.325 -      (CodeFuncgr.all funcgr);
  27.326 -    val CodeFuncgr' = CodeFuncgr.make thy cs;
  27.327      val naming = NameSpace.qualified_names NameSpace.default_naming;
  27.328      val consttab = Consts.empty
  27.329        |> fold (fn c => Consts.declare naming
  27.330 -           ((CodeName.const thy c, CodeFuncgr.typ CodeFuncgr' c), true))
  27.331 -           (CodeFuncgr.all CodeFuncgr');
  27.332 +           ((c, CodeFuncgr.typ funcgr c), true))
  27.333 +           (CodeFuncgr.all funcgr);
  27.334      val algbr = (Code.operational_algebra thy, consttab);
  27.335    in   
  27.336      Program.change_yield thy
  27.337 -      (CodeThingol.start_transact (gen thy algbr CodeFuncgr' it))
  27.338 +      (CodeThingol.start_transact (gen thy algbr funcgr it))
  27.339      |> fst
  27.340    end;
  27.341  
  27.342 @@ -630,8 +526,7 @@
  27.343  
  27.344  val _ = OuterSyntax.add_keywords [inK, module_nameK, fileK];
  27.345  
  27.346 -val (codeK, code_abstypeK, code_axiomsK, code_thmsK, code_depsK) =
  27.347 -  ("export_code", "code_abstype", "code_axioms", "code_thms", "code_deps");
  27.348 +val (codeK, code_thmsK, code_depsK) = ("export_code", "code_thms", "code_deps");
  27.349  
  27.350  in
  27.351  
  27.352 @@ -644,19 +539,6 @@
  27.353     of SOME f => (writeln "Now generating code..."; f thy)
  27.354      | NONE => error ("Bad directive " ^ quote cmd);
  27.355  
  27.356 -val code_abstypeP =
  27.357 -  OuterSyntax.command code_abstypeK "axiomatic abstypes for code generation" K.thy_decl (
  27.358 -    (P.typ -- P.typ -- Scan.optional (P.$$$ "where" |-- Scan.repeat1
  27.359 -        (P.term --| (P.$$$ "\\<equiv>" || P.$$$ "==") -- P.term)) [])
  27.360 -    >> (Toplevel.theory o uncurry abstyp_e)
  27.361 -  );
  27.362 -
  27.363 -val code_axiomsP =
  27.364 -  OuterSyntax.command code_axiomsK "axiomatic constant equalities for code generation" K.thy_decl (
  27.365 -    Scan.repeat1 (P.term --| (P.$$$ "\\<equiv>" || P.$$$ "==") -- P.term)
  27.366 -    >> (Toplevel.theory o constsubst_e)
  27.367 -  );
  27.368 -
  27.369  val code_thmsP =
  27.370    OuterSyntax.improper_command code_thmsK "print system of defining equations for code" OuterKeyword.diag
  27.371      (Scan.repeat P.term
  27.372 @@ -669,7 +551,7 @@
  27.373        >> (fn cs => Toplevel.no_timing o Toplevel.unknown_theory
  27.374          o Toplevel.keep ((fn thy => code_deps_cmd thy cs) o Toplevel.theory_of)));
  27.375  
  27.376 -val _ = OuterSyntax.add_parsers [codeP, code_abstypeP, code_axiomsP, code_thmsP, code_depsP];
  27.377 +val _ = OuterSyntax.add_parsers [codeP, code_thmsP, code_depsP];
  27.378  
  27.379  end; (* local *)
  27.380  
    28.1 --- a/src/Tools/code/code_target.ML	Fri Aug 24 14:14:18 2007 +0200
    28.2 +++ b/src/Tools/code/code_target.ML	Fri Aug 24 14:14:20 2007 +0200
    28.3 @@ -11,7 +11,7 @@
    28.4    include BASIC_CODE_THINGOL;
    28.5  
    28.6    val add_syntax_class: string -> class
    28.7 -    -> (string * (CodeUnit.const * string) list) option -> theory -> theory;
    28.8 +    -> (string * (string * string) list) option -> theory -> theory;
    28.9    val add_syntax_inst: string -> string * class -> bool -> theory -> theory;
   28.10    val add_syntax_tycoP: string -> string -> OuterParse.token list
   28.11      -> (theory -> theory) * OuterParse.token list;
   28.12 @@ -23,7 +23,7 @@
   28.13    val add_pretty_list_string: string -> string -> string
   28.14      -> string -> string list -> theory -> theory;
   28.15    val add_pretty_char: string -> string -> string list -> theory -> theory
   28.16 -  val add_pretty_numeral: string -> bool -> string * typ -> string -> string -> string
   28.17 +  val add_pretty_numeral: string -> bool -> string -> string -> string -> string
   28.18      -> string -> string -> theory -> theory;
   28.19    val add_pretty_ml_string: string -> string -> string list -> string
   28.20      -> string -> string -> theory -> theory;
   28.21 @@ -1410,7 +1410,7 @@
   28.22            |> distinct (op =)
   28.23            |> remove (op =) modlname';
   28.24          val qualified =
   28.25 -          imports
   28.26 +          imports @ map fst defs
   28.27            |> map_filter (try deresolv)
   28.28            |> map NameSpace.base
   28.29            |> has_duplicates (op =);
   28.30 @@ -1793,8 +1793,8 @@
   28.31    let
   28.32      val cls = prep_class thy raw_class;
   28.33      val class = CodeName.class thy cls;
   28.34 -    fun mk_classop (const as (c, _)) = case AxClass.class_of_param thy c
   28.35 -     of SOME class' => if cls = class' then CodeName.const thy const
   28.36 +    fun mk_classop c = case AxClass.class_of_param thy c
   28.37 +     of SOME class' => if cls = class' then CodeName.const thy c
   28.38            else error ("Not a class operation for class " ^ quote class ^ ": " ^ quote c)
   28.39        | NONE => error ("Not a class operation: " ^ quote c);
   28.40      fun mk_syntax_ops raw_ops = AList.lookup (op =)
   28.41 @@ -1845,8 +1845,8 @@
   28.42    let
   28.43      val c = prep_const thy raw_c;
   28.44      val c' = CodeName.const thy c;
   28.45 -    fun check_args (syntax as (n, _)) = if n > (length o fst o strip_type o Sign.the_const_type thy o fst) c
   28.46 -      then error ("Too many arguments in syntax for constant " ^ (quote o fst) c)
   28.47 +    fun check_args (syntax as (n, _)) = if n > CodeUnit.no_args thy c
   28.48 +      then error ("Too many arguments in syntax for constant " ^ quote c)
   28.49        else syntax;
   28.50    in case raw_syn
   28.51     of SOME syntax =>
   28.52 @@ -1883,12 +1883,6 @@
   28.53        else error ("No such type constructor: " ^ quote raw_tyco);
   28.54    in tyco end;
   28.55  
   28.56 -fun idfs_of_const thy c =
   28.57 -  let
   28.58 -    val c' = (c, Sign.the_const_type thy c);
   28.59 -    val c'' = CodeUnit.const_of_cexpr thy c';
   28.60 -  in (c'', CodeName.const thy c'') end;
   28.61 -
   28.62  fun no_bindings x = (Option.map o apsnd)
   28.63    (fn pretty => fn pr => fn vars => pretty (pr vars)) x;
   28.64  
   28.65 @@ -1974,79 +1968,75 @@
   28.66  
   28.67  fun add_undefined target undef target_undefined thy =
   28.68    let
   28.69 -    val (undef', _) = idfs_of_const thy undef;
   28.70      fun pr _ _ _ _ = str target_undefined;
   28.71    in
   28.72      thy
   28.73 -    |> add_syntax_const target undef' (SOME (~1, pr))
   28.74 +    |> add_syntax_const target undef (SOME (~1, pr))
   28.75    end;
   28.76  
   28.77  fun add_pretty_list target nill cons thy =
   28.78    let
   28.79 -    val (_, nil'') = idfs_of_const thy nill;
   28.80 -    val (cons', cons'') = idfs_of_const thy cons;
   28.81 -    val pr = pretty_list nil'' cons'' target;
   28.82 +    val nil' = CodeName.const thy nill;
   28.83 +    val cons' = CodeName.const thy cons;
   28.84 +    val pr = pretty_list nil' cons' target;
   28.85    in
   28.86      thy
   28.87 -    |> add_syntax_const target cons' (SOME pr)
   28.88 +    |> add_syntax_const target cons (SOME pr)
   28.89    end;
   28.90  
   28.91  fun add_pretty_list_string target nill cons charr nibbles thy =
   28.92    let
   28.93 -    val (_, nil'') = idfs_of_const thy nill;
   28.94 -    val (cons', cons'') = idfs_of_const thy cons;
   28.95 -    val (_, charr'') = idfs_of_const thy charr;
   28.96 -    val (_, nibbles'') = split_list (map (idfs_of_const thy) nibbles);
   28.97 -    val pr = pretty_list_string nil'' cons'' charr'' nibbles'' target;
   28.98 +    val nil' = CodeName.const thy nill;
   28.99 +    val cons' = CodeName.const thy cons;
  28.100 +    val charr' = CodeName.const thy charr;
  28.101 +    val nibbles' = map (CodeName.const thy) nibbles;
  28.102 +    val pr = pretty_list_string nil' cons' charr' nibbles' target;
  28.103    in
  28.104      thy
  28.105 -    |> add_syntax_const target cons' (SOME pr)
  28.106 +    |> add_syntax_const target cons (SOME pr)
  28.107    end;
  28.108  
  28.109  fun add_pretty_char target charr nibbles thy =
  28.110    let
  28.111 -    val (charr', charr'') = idfs_of_const thy charr;
  28.112 -    val (_, nibbles'') = split_list (map (idfs_of_const thy) nibbles);
  28.113 -    val pr = pretty_char charr'' nibbles'' target;
  28.114 +    val charr' = CodeName.const thy charr;
  28.115 +    val nibbles' = map (CodeName.const thy) nibbles;
  28.116 +    val pr = pretty_char charr' nibbles' target;
  28.117    in
  28.118      thy
  28.119 -    |> add_syntax_const target charr' (SOME pr)
  28.120 +    |> add_syntax_const target charr (SOME pr)
  28.121    end;
  28.122  
  28.123  fun add_pretty_numeral target unbounded number_of b0 b1 pls min bit thy =
  28.124    let
  28.125 -    val number_of' = CodeUnit.const_of_cexpr thy number_of;
  28.126 -    val (_, b0'') = idfs_of_const thy b0;
  28.127 -    val (_, b1'') = idfs_of_const thy b1;
  28.128 -    val (_, pls'') = idfs_of_const thy pls;
  28.129 -    val (_, min'') = idfs_of_const thy min;
  28.130 -    val (_, bit'') = idfs_of_const thy bit;
  28.131 -    val pr = pretty_numeral unbounded b0'' b1'' pls'' min'' bit'' target;
  28.132 +    val b0' = CodeName.const thy b0;
  28.133 +    val b1' = CodeName.const thy b1;
  28.134 +    val pls' = CodeName.const thy pls;
  28.135 +    val min' = CodeName.const thy min;
  28.136 +    val bit' = CodeName.const thy bit;
  28.137 +    val pr = pretty_numeral unbounded b0' b1' pls' min' bit' target;
  28.138    in
  28.139      thy
  28.140 -    |> add_syntax_const target number_of' (SOME pr)
  28.141 +    |> add_syntax_const target number_of (SOME pr)
  28.142    end;
  28.143  
  28.144  fun add_pretty_ml_string target charr nibbles nill cons str thy =
  28.145    let
  28.146 -    val (_, charr'') = idfs_of_const thy charr;
  28.147 -    val (_, nibbles'') = split_list (map (idfs_of_const thy) nibbles);
  28.148 -    val (_, nil'') = idfs_of_const thy nill;
  28.149 -    val (_, cons'') = idfs_of_const thy cons;
  28.150 -    val (str', _) = idfs_of_const thy str;
  28.151 -    val pr = pretty_ml_string charr'' nibbles'' nil'' cons'' target;
  28.152 +    val charr' = CodeName.const thy charr;
  28.153 +    val nibbles' = map (CodeName.const thy) nibbles;
  28.154 +    val nil' = CodeName.const thy nill;
  28.155 +    val cons' = CodeName.const thy cons;
  28.156 +    val pr = pretty_ml_string charr' nibbles' nil' cons' target;
  28.157    in
  28.158      thy
  28.159 -    |> add_syntax_const target str' (SOME pr)
  28.160 +    |> add_syntax_const target str (SOME pr)
  28.161    end;
  28.162  
  28.163  fun add_pretty_imperative_monad_bind target bind thy =
  28.164    let
  28.165 -    val (bind', _) = idfs_of_const thy bind;
  28.166      val pr = pretty_imperative_monad_bind
  28.167    in
  28.168      thy
  28.169 -    |> add_syntax_const target bind' (SOME pr)
  28.170 +    |> add_syntax_const target bind (SOME pr)
  28.171    end;
  28.172  
  28.173  val add_haskell_monad = gen_add_haskell_monad CodeUnit.read_const;
    29.1 --- a/src/Tools/nbe.ML	Fri Aug 24 14:14:18 2007 +0200
    29.2 +++ b/src/Tools/nbe.ML	Fri Aug 24 14:14:20 2007 +0200
    29.3 @@ -25,7 +25,7 @@
    29.4    val app: Univ -> Univ -> Univ              (*explicit application*)
    29.5  
    29.6    val univs_ref: Univ list ref 
    29.7 -  val lookup_fun: CodeName.const -> Univ
    29.8 +  val lookup_fun: string -> Univ
    29.9  
   29.10    val normalization_conv: cterm -> thm
   29.11  
   29.12 @@ -295,8 +295,8 @@
   29.13        #>> (fn ts' => list_comb (t, rev ts'))
   29.14      and of_univ bounds (Const (name, ts)) typidx =
   29.15            let
   29.16 -            val SOME (const as (c, _)) = CodeName.const_rev thy name;
   29.17 -            val T = Code.default_typ thy const;
   29.18 +            val SOME c = CodeName.const_rev thy name;
   29.19 +            val T = Code.default_typ thy c;
   29.20              val T' = map_type_tvar (fn ((v, i), S) => TypeInfer.param (typidx + i) (v, S)) T;
   29.21              val typidx' = typidx + maxidx_of_typ T' + 1;
   29.22            in of_apps bounds (Term.Const (c, T'), ts) typidx' end