--- a/src/HOL/Complex/ex/ReflectedFerrack.thy Fri Aug 24 14:14:18 2007 +0200
+++ b/src/HOL/Complex/ex/ReflectedFerrack.thy Fri Aug 24 14:14:20 2007 +0200
@@ -1954,7 +1954,6 @@
let ?res = "disj ?mp (disj ?pp ?ep)"
from rminusinf_bound0[OF lq] rplusinf_bound0[OF lq] ep_nb
have nbth: "bound0 ?res" by auto
- thm rlfm_I[OF simpfm_qf[OF qf]]
from conjunct1[OF rlfm_I[OF simpfm_qf[OF qf]]] simpfm
@@ -1997,7 +1996,7 @@
use "linreif.ML"
oracle linr_oracle ("term") = ReflectedFerrack.linrqe_oracle
-use"linrtac.ML"
-setup "LinrTac.setup"
+use "linrtac.ML"
+setup LinrTac.setup
end
--- a/src/HOL/Complex/ex/linreif.ML Fri Aug 24 14:14:18 2007 +0200
+++ b/src/HOL/Complex/ex/linreif.ML Fri Aug 24 14:14:20 2007 +0200
@@ -44,16 +44,16 @@
case t of
Const("True",_) => T
| Const("False",_) => F
- | Const(@{const_name HOL.less},_)$t1$t2 => Lta (Sub (num_of_term vs t1,num_of_term vs t2))
- | Const(@{const_name HOL.less_eq},_)$t1$t2 => Lea (Sub (num_of_term vs t1,num_of_term vs t2))
+ | Const(@{const_name HOL.less},_)$t1$t2 => Lt (Sub (num_of_term vs t1,num_of_term vs t2))
+ | Const(@{const_name HOL.less_eq},_)$t1$t2 => Le (Sub (num_of_term vs t1,num_of_term vs t2))
| Const("op =",eqT)$t1$t2 =>
if (domain_type eqT = rT)
- then Eqa (Sub (num_of_term vs t1,num_of_term vs t2))
- else Iffa(fm_of_term vs t1,fm_of_term vs t2)
+ then Eq (Sub (num_of_term vs t1,num_of_term vs t2))
+ else Iff(fm_of_term vs t1,fm_of_term vs t2)
| Const("op &",_)$t1$t2 => And(fm_of_term vs t1,fm_of_term vs t2)
| Const("op |",_)$t1$t2 => Or(fm_of_term vs t1,fm_of_term vs t2)
- | Const("op -->",_)$t1$t2 => Impa(fm_of_term vs t1,fm_of_term vs t2)
- | Const("Not",_)$t' => Nota(fm_of_term vs t')
+ | Const("op -->",_)$t1$t2 => Imp(fm_of_term vs t1,fm_of_term vs t2)
+ | Const("Not",_)$t' => Not(fm_of_term vs t')
| Const("Ex",_)$Term.Abs(xn,xT,p) =>
E(fm_of_term (map (fn(v,n) => (v,1+ n)) vs) p)
| Const("All",_)$Term.Abs(xn,xT,p) =>
@@ -91,22 +91,22 @@
case t of
T => HOLogic.true_const
| F => HOLogic.false_const
- | Lta t => Const(@{const_name HOL.less},[rT,rT] ---> bT)$
+ | Lt t => Const(@{const_name HOL.less},[rT,rT] ---> bT)$
(term_of_num vs t)$ rzero
- | Lea t => Const(@{const_name HOL.less_eq},[rT,rT] ---> bT)$
+ | Le t => Const(@{const_name HOL.less_eq},[rT,rT] ---> bT)$
(term_of_num vs t)$ rzero
- | Gta t => Const(@{const_name HOL.less},[rT,rT] ---> bT)$
+ | Gt t => Const(@{const_name HOL.less},[rT,rT] ---> bT)$
rzero $(term_of_num vs t)
- | Gea t => Const(@{const_name HOL.less_eq},[rT,rT] ---> bT)$
+ | Ge t => Const(@{const_name HOL.less_eq},[rT,rT] ---> bT)$
rzero $(term_of_num vs t)
- | Eqa t => Const("op =",[rT,rT] ---> bT)$
+ | Eq t => Const("op =",[rT,rT] ---> bT)$
(term_of_num vs t)$ rzero
- | NEq t => term_of_fm vs (Nota (Eqa t))
- | Nota t' => HOLogic.Not$(term_of_fm vs t')
+ | NEq t => term_of_fm vs (Not (Eq t))
+ | Not t' => HOLogic.Not$(term_of_fm vs t')
| And(t1,t2) => HOLogic.conj$(term_of_fm vs t1)$(term_of_fm vs t2)
| Or(t1,t2) => HOLogic.disj$(term_of_fm vs t1)$(term_of_fm vs t2)
- | Impa(t1,t2) => HOLogic.imp$(term_of_fm vs t1)$(term_of_fm vs t2)
- | Iffa(t1,t2) => (HOLogic.eq_const bT)$(term_of_fm vs t1)$
+ | Imp(t1,t2) => HOLogic.imp$(term_of_fm vs t1)$(term_of_fm vs t2)
+ | Iff(t1,t2) => (HOLogic.eq_const bT)$(term_of_fm vs t1)$
(term_of_fm vs t2)
| _ => error "If this is raised, Isabelle/HOL or generate_code is inconsistent!";
--- a/src/HOL/Complex/ex/mireif.ML Fri Aug 24 14:14:18 2007 +0200
+++ b/src/HOL/Complex/ex/mireif.ML Fri Aug 24 14:14:20 2007 +0200
@@ -42,18 +42,18 @@
case t of
Const("True",_) => T
| Const("False",_) => F
- | Const(@{const_name HOL.less},_)$t1$t2 => Lta (Sub (num_of_term vs t1,num_of_term vs t2))
- | Const(@{const_name HOL.less_eq},_)$t1$t2 => Lea (Sub (num_of_term vs t1,num_of_term vs t2))
+ | Const(@{const_name HOL.less},_)$t1$t2 => Lt (Sub (num_of_term vs t1,num_of_term vs t2))
+ | Const(@{const_name HOL.less_eq},_)$t1$t2 => Le (Sub (num_of_term vs t1,num_of_term vs t2))
| Const (@{const_name "MIR.rdvd"},_ )$ (Const("RealDef.real",_) $ (Const(@{const_name "Numeral.number_of"},_)$t1))$t2 =>
- Dvda (HOLogic.dest_numeral t1, num_of_term vs t2)
+ Dvd (HOLogic.dest_numeral t1, num_of_term vs t2)
| Const("op =",eqT)$t1$t2 =>
if (domain_type eqT = @{typ real})
- then Eqa (Sub (num_of_term vs t1, num_of_term vs t2))
- else Iffa (fm_of_term vs t1, fm_of_term vs t2)
+ then Eq (Sub (num_of_term vs t1, num_of_term vs t2))
+ else Iff (fm_of_term vs t1, fm_of_term vs t2)
| Const("op &",_)$t1$t2 => And (fm_of_term vs t1, fm_of_term vs t2)
| Const("op |",_)$t1$t2 => Or (fm_of_term vs t1, fm_of_term vs t2)
- | Const("op -->",_)$t1$t2 => Impa (fm_of_term vs t1, fm_of_term vs t2)
- | Const("Not",_)$t' => Nota (fm_of_term vs t')
+ | Const("op -->",_)$t1$t2 => Imp (fm_of_term vs t1, fm_of_term vs t2)
+ | Const("Not",_)$t' => Not (fm_of_term vs t')
| Const("Ex",_)$Abs(xn,xT,p) =>
E (fm_of_term (map (fn (v, n) => (v, Suc n)) vs) p)
| Const("All",_)$Abs(xn,xT,p) =>
@@ -93,19 +93,19 @@
case t of
T => HOLogic.true_const
| F => HOLogic.false_const
- | Lta t => @{term "op <:: real => _"} $ term_of_num vs t $ rzero
- | Lea t => @{term "op <=:: real => _"} $ term_of_num vs t $ rzero
- | Gta t => @{term "op <:: real => _"}$ rzero $ term_of_num vs t
- | Gea t => @{term "op <=:: real => _"} $ rzero $ term_of_num vs t
- | Eqa t => @{term "op = :: real => _"}$ term_of_num vs t $ rzero
- | NEq t => term_of_fm vs (Nota (Eqa t))
- | NDvd (i,t) => term_of_fm vs (Nota (Dvda (i,t)))
- | Dvda (i,t) => @{term "op rdvd"} $ term_of_num vs (C i) $ term_of_num vs t
- | Nota t' => HOLogic.Not$(term_of_fm vs t')
+ | Lt t => @{term "op <:: real => _"} $ term_of_num vs t $ rzero
+ | Le t => @{term "op <=:: real => _"} $ term_of_num vs t $ rzero
+ | Gt t => @{term "op <:: real => _"}$ rzero $ term_of_num vs t
+ | Ge t => @{term "op <=:: real => _"} $ rzero $ term_of_num vs t
+ | Eq t => @{term "op = :: real => _"}$ term_of_num vs t $ rzero
+ | NEq t => term_of_fm vs (Not (Eq t))
+ | NDvd (i,t) => term_of_fm vs (Not (Dvd (i,t)))
+ | Dvd (i,t) => @{term "op rdvd"} $ term_of_num vs (C i) $ term_of_num vs t
+ | Not t' => HOLogic.Not$(term_of_fm vs t')
| And(t1,t2) => HOLogic.conj $ term_of_fm vs t1 $ term_of_fm vs t2
| Or(t1,t2) => HOLogic.disj $ term_of_fm vs t1 $ term_of_fm vs t2
- | Impa(t1,t2) => HOLogic.imp $ term_of_fm vs t1 $ term_of_fm vs t2
- | Iffa(t1,t2) => HOLogic.mk_eq (term_of_fm vs t1, term_of_fm vs t2)
+ | Imp(t1,t2) => HOLogic.imp $ term_of_fm vs t1 $ term_of_fm vs t2
+ | Iff(t1,t2) => HOLogic.mk_eq (term_of_fm vs t1, term_of_fm vs t2)
| _ => error "If this is raised, Isabelle/HOL or generate_code is inconsistent!";
(* The oracle *)
--- a/src/HOL/Lambda/WeakNorm.thy Fri Aug 24 14:14:18 2007 +0200
+++ b/src/HOL/Lambda/WeakNorm.thy Fri Aug 24 14:14:20 2007 +0200
@@ -614,13 +614,13 @@
fun typing_of_term Ts e (Bound i) =
Norm.Vara (e, nat_of_int i, dBtype_of_typ (nth Ts i))
| typing_of_term Ts e (t $ u) = (case fastype_of1 (Ts, t) of
- Type ("fun", [T, U]) => Norm.Appaa (e, dB_of_term t,
+ Type ("fun", [T, U]) => Norm.Appb (e, dB_of_term t,
dBtype_of_typ T, dBtype_of_typ U, dB_of_term u,
typing_of_term Ts e t, typing_of_term Ts e u)
| _ => error "typing_of_term: function type expected")
| typing_of_term Ts e (Abs (s, T, t)) =
let val dBT = dBtype_of_typ T
- in Norm.Absaa (e, dBT, dB_of_term t,
+ in Norm.Absb (e, dBT, dB_of_term t,
dBtype_of_typ (fastype_of1 (T :: Ts, t)),
typing_of_term (T :: Ts) (Norm.shift e Norm.Zero_nat dBT) t)
end
--- a/src/HOL/Library/Efficient_Nat.thy Fri Aug 24 14:14:18 2007 +0200
+++ b/src/HOL/Library/Efficient_Nat.thy Fri Aug 24 14:14:20 2007 +0200
@@ -63,6 +63,8 @@
lemma eq_nat_of_int: "int' n = x \<Longrightarrow> n = nat_of_int x"
by (erule subst, simp only: nat_of_int_int)
+code_datatype nat_of_int
+
text {*
Case analysis on natural numbers is rephrased using a conditional
expression:
@@ -161,8 +163,6 @@
@{typ nat} is no longer a datatype but embedded into the integers.
*}
-code_datatype nat_of_int
-
code_type nat
(SML "IntInf.int")
(OCaml "Big'_int.big'_int")
--- a/src/HOL/Library/Eval.thy Fri Aug 24 14:14:18 2007 +0200
+++ b/src/HOL/Library/Eval.thy Fri Aug 24 14:14:20 2007 +0200
@@ -52,7 +52,7 @@
fun hook specs =
DatatypeCodegen.prove_codetypes_arities (Class.intro_classes_tac [])
(map (fn (tyco, (is_dt, _)) => (tyco, is_dt)) specs)
- [TypOf.class_typ_of] mk ((K o K) I)
+ [TypOf.class_typ_of] mk ((K o K) (fold (Code.add_func true)))
in DatatypeCodegen.add_codetypes_hook_bootstrap hook end
*}
@@ -98,7 +98,7 @@
PureThy.add_thmss [((name, thms), atts)] #-> (fn [thms] => pair (name, thms));
fun thy_def ((name, atts), t) =
PureThy.add_defs_i false [((name, t), atts)] #-> (fn [thm] => pair (name, thm));
- fun mk arities css thy =
+ fun mk arities css _ thy =
let
val (_, asorts, _) :: _ = arities;
val vs = Name.names Name.context "'a" asorts;
--- a/src/HOL/Library/Executable_Set.thy Fri Aug 24 14:14:18 2007 +0200
+++ b/src/HOL/Library/Executable_Set.thy Fri Aug 24 14:14:20 2007 +0200
@@ -11,24 +11,10 @@
subsection {* Definitional rewrites *}
-instance set :: (eq) eq ..
-
lemma [code target: Set]:
"A = B \<longleftrightarrow> A \<subseteq> B \<and> B \<subseteq> A"
by blast
-lemma [code func]:
- "(A\<Colon>'a\<Colon>eq set) = B \<longleftrightarrow> A \<subseteq> B \<and> B \<subseteq> A"
- by blast
-
-lemma [code func]:
- "(A\<Colon>'a\<Colon>eq set) \<subseteq> B \<longleftrightarrow> (\<forall>x\<in>A. x \<in> B)"
- unfolding subset_def ..
-
-lemma [code func]:
- "(A\<Colon>'a\<Colon>eq set) \<subset> B \<longleftrightarrow> A \<subseteq> B \<and> A \<noteq> B"
- by blast
-
lemma [code]:
"a \<in> A \<longleftrightarrow> (\<exists>x\<in>A. x = a)"
unfolding bex_triv_one_point1 ..
@@ -37,8 +23,6 @@
filter_set :: "('a \<Rightarrow> bool) \<Rightarrow> 'a set \<Rightarrow> 'a set" where
"filter_set P xs = {x\<in>xs. P x}"
-lemmas [symmetric, code inline] = filter_set_def
-
subsection {* Operations on lists *}
@@ -256,74 +240,6 @@
nonfix subset;
*}
-code_modulename SML
- Executable_Set List
- Set List
-
-code_modulename OCaml
- Executable_Set List
- Set List
-
-code_modulename Haskell
- Executable_Set List
- Set List
-
-definition [code inline]:
- "empty_list = []"
-
-lemma [code func]:
- "insert (x \<Colon> 'a\<Colon>eq) = insert x" ..
-
-lemma [code func]:
- "(xs \<Colon> 'a\<Colon>eq set) \<union> ys = xs \<union> ys" ..
-
-lemma [code func]:
- "(xs \<Colon> 'a\<Colon>eq set) \<inter> ys = xs \<inter> ys" ..
-
-lemma [code func]:
- "(op -) (xs \<Colon> 'a\<Colon>eq set) = (op -) (xs \<Colon> 'a\<Colon>eq set)" ..
-
-lemma [code func]:
- "image (f \<Colon> 'a \<Rightarrow> 'b\<Colon>eq) = image f" ..
-
-lemma [code func]:
- "Union (xss \<Colon> 'a\<Colon>eq set set) = Union xss" ..
-
-lemma [code func]:
- "Inter (xss \<Colon> 'a\<Colon>eq set set) = Inter xss" ..
-
-lemma [code func]:
- "UNION xs (f \<Colon> 'a \<Rightarrow> 'b\<Colon>eq set) = UNION xs f" ..
-
-lemma [code func]:
- "INTER xs (f \<Colon> 'a \<Rightarrow> 'b\<Colon>eq set) = INTER xs f" ..
-
-lemma [code func]:
- "Ball (xs \<Colon> 'a\<Colon>type set) = Ball xs" ..
-
-lemma [code func]:
- "Bex (xs \<Colon> 'a\<Colon>type set) = Bex xs" ..
-
-lemma [code func]:
- "filter_set P (xs \<Colon> 'a\<Colon>type set) = filter_set P xs" ..
-
-
-code_abstype "'a set" "'a list" where
- "{}" \<equiv> empty_list
- insert \<equiv> insertl
- "op \<union>" \<equiv> unionl
- "op \<inter>" \<equiv> intersect
- "op - \<Colon> 'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" \<equiv> subtract'
- image \<equiv> map_distinct
- Union \<equiv> unions
- Inter \<equiv> intersects
- UNION \<equiv> map_union
- INTER \<equiv> map_inter
- Ball \<equiv> Blall
- Bex \<equiv> Blex
- filter_set \<equiv> filter
-
-
subsubsection {* type serializations *}
types_code
--- a/src/HOL/Library/Graphs.thy Fri Aug 24 14:14:18 2007 +0200
+++ b/src/HOL/Library/Graphs.thy Fri Aug 24 14:14:20 2007 +0200
@@ -6,7 +6,7 @@
header {* General Graphs as Sets *}
theory Graphs
-imports Main SCT_Misc Kleene_Algebras Executable_Set
+imports Main SCT_Misc Kleene_Algebras
begin
subsection {* Basic types, Size Change Graphs *}
--- a/src/HOL/Library/ML_Int.thy Fri Aug 24 14:14:18 2007 +0200
+++ b/src/HOL/Library/ML_Int.thy Fri Aug 24 14:14:20 2007 +0200
@@ -170,7 +170,7 @@
setup {*
CodeTarget.add_pretty_numeral "SML" false
- (@{const_name number_of}, @{typ "int \<Rightarrow> ml_int"})
+ @{const_name ml_int_of_int}
@{const_name Numeral.B0} @{const_name Numeral.B1}
@{const_name Numeral.Pls} @{const_name Numeral.Min}
@{const_name Numeral.Bit}
--- a/src/HOL/Library/Pretty_Int.thy Fri Aug 24 14:14:18 2007 +0200
+++ b/src/HOL/Library/Pretty_Int.thy Fri Aug 24 14:14:20 2007 +0200
@@ -25,7 +25,7 @@
setup {*
fold (fn target => CodeTarget.add_pretty_numeral target true
- (@{const_name number_of}, @{typ "int \<Rightarrow> int"})
+ @{const_name number_int_inst.number_of_int}
@{const_name Numeral.B0} @{const_name Numeral.B1}
@{const_name Numeral.Pls} @{const_name Numeral.Min}
@{const_name Numeral.Bit}
--- a/src/HOL/Library/SCT_Implementation.thy Fri Aug 24 14:14:18 2007 +0200
+++ b/src/HOL/Library/SCT_Implementation.thy Fri Aug 24 14:14:20 2007 +0200
@@ -6,7 +6,7 @@
header {* Implemtation of the SCT criterion *}
theory SCT_Implementation
-imports Executable_Set SCT_Definition SCT_Theorem
+imports SCT_Definition SCT_Theorem
begin
fun edges_match :: "('n \<times> 'e \<times> 'n) \<times> ('n \<times> 'e \<times> 'n) \<Rightarrow> bool"
--- a/src/HOL/Tools/datatype_abs_proofs.ML Fri Aug 24 14:14:18 2007 +0200
+++ b/src/HOL/Tools/datatype_abs_proofs.ML Fri Aug 24 14:14:20 2007 +0200
@@ -429,6 +429,7 @@
thy
|> Class.prove_instance_arity (Class.intro_classes_tac [])
[(tyco, replicate n HOLogic.typeS, [HOLogic.class_size])] []
+ |> snd
end
val (size_def_thms, thy') =
--- a/src/HOL/Tools/datatype_codegen.ML Fri Aug 24 14:14:18 2007 +0200
+++ b/src/HOL/Tools/datatype_codegen.ML Fri Aug 24 14:14:20 2007 +0200
@@ -26,7 +26,7 @@
val prove_codetypes_arities: tactic -> (string * bool) list -> sort
-> (arity list -> (string * term list) list -> theory
-> ((bstring * Attrib.src list) * term) list * theory)
- -> (arity list -> (string * term list) list -> theory -> theory)
+ -> (arity list -> (string * term list) list -> thm list -> theory -> theory)
-> theory -> theory
val setup: theory -> theory
@@ -537,8 +537,13 @@
(* registering code types in code generator *)
-fun codetype_hook dtspecs =
- fold (fn (dtco, (_, spec)) => Code.add_datatype (dtco, spec)) dtspecs;
+fun add_datatype_spec (tyco, (vs, cos)) thy =
+ let
+ val cs = map (fn (c, tys) => (c, tys ---> Type (tyco, map TFree vs))) cos;
+ in try (Code.add_datatype cs) thy |> the_default thy end;
+
+val codetype_hook =
+ fold (fn (dtco, (_, spec)) => add_datatype_spec (dtco, spec));
(* instrumentalizing the sort algebra *)
@@ -586,7 +591,8 @@
f arities css
#-> (fn defs =>
Class.prove_instance_arity tac arities defs
- #> after_qed arities css))
+ #-> (fn defs =>
+ after_qed arities css defs)))
end;
@@ -597,7 +603,7 @@
fun add_eq_thms (dtco, (_, (vs, cs))) thy =
let
val thy_ref = Theory.check_thy thy;
- val const = ("op =", SOME dtco);
+ val const = Class.inst_const thy ("op =", dtco);
val get_thms = (fn () => get_eq (Theory.deref thy_ref) dtco |> rev);
in
Code.add_funcl (const, Susp.delay get_thms) thy
@@ -605,7 +611,7 @@
in
prove_codetypes_arities (Class.intro_classes_tac [])
(map (fn (tyco, (is_dt, _)) => (tyco, is_dt)) specs)
- [HOLogic.class_eq] ((K o K o pair) []) ((K o K) (fold add_eq_thms specs))
+ [HOLogic.class_eq] ((K o K o pair) []) ((K o K o K) (fold add_eq_thms specs))
end;
--- a/src/HOL/Tools/datatype_package.ML Fri Aug 24 14:14:18 2007 +0200
+++ b/src/HOL/Tools/datatype_package.ML Fri Aug 24 14:14:20 2007 +0200
@@ -567,6 +567,7 @@
thy
|> Class.prove_instance_arity (Class.intro_classes_tac [])
[(tyco, replicate n HOLogic.typeS, [HOLogic.class_size])] []
+ |> snd
end
val thy2' = thy
--- a/src/HOL/ex/Classpackage.thy Fri Aug 24 14:14:18 2007 +0200
+++ b/src/HOL/ex/Classpackage.thy Fri Aug 24 14:14:20 2007 +0200
@@ -342,7 +342,7 @@
definition "x2 = X (1::int) 2 3"
definition "y2 = Y (1::int) 2 3"
-export_code x1 x2 y2 in SML module_name Classpackage
+export_code mult x1 x2 y2 in SML module_name Classpackage
in OCaml file -
in Haskell file -
--- a/src/HOL/ex/Codegenerator.thy Fri Aug 24 14:14:18 2007 +0200
+++ b/src/HOL/ex/Codegenerator.thy Fri Aug 24 14:14:20 2007 +0200
@@ -8,7 +8,7 @@
imports ExecutableContent
begin
-export_code "*" in SML module_name CodegenTest
+export_code * in SML module_name CodegenTest
in OCaml file -
in Haskell file -
--- a/src/HOL/ex/Eval_Examples.thy Fri Aug 24 14:14:18 2007 +0200
+++ b/src/HOL/ex/Eval_Examples.thy Fri Aug 24 14:14:20 2007 +0200
@@ -31,8 +31,8 @@
value (overloaded) "(Suc 2 + Suc 0) * Suc 3"
value (overloaded) "nat 100"
value (overloaded) "(10\<Colon>int) \<le> 12"
+value (overloaded) "[]::nat list"
value (overloaded) "[(nat 100, ())]"
-value (overloaded) "[]::nat list"
text {* a fancy datatype *}
--- a/src/HOL/ex/ExecutableContent.thy Fri Aug 24 14:14:18 2007 +0200
+++ b/src/HOL/ex/ExecutableContent.thy Fri Aug 24 14:14:20 2007 +0200
@@ -19,7 +19,7 @@
List_Prefix
Nat_Infinity
NatPair
- Nested_Environment
+ (*Nested_Environment*)
Permutation
Primes
Product_ord
--- a/src/HOL/ex/coopereif.ML Fri Aug 24 14:14:18 2007 +0200
+++ b/src/HOL/ex/coopereif.ML Fri Aug 24 14:14:20 2007 +0200
@@ -37,11 +37,11 @@
| Const(@{const_name "Divides.dvd"},_)$t1$t2 =>
(Dvd(HOLogic.dest_number t1 |> snd, i_of_term vs t2) handle _ => error "qf_of_term: unsupported dvd")
| @{term "op = :: int => _"}$t1$t2 => Eq (Sub (i_of_term vs t1,i_of_term vs t2))
- | @{term "op = :: bool => _ "}$t1$t2 => Iffa(qf_of_term ps vs t1,qf_of_term ps vs t2)
+ | @{term "op = :: bool => _ "}$t1$t2 => Iff(qf_of_term ps vs t1,qf_of_term ps vs t2)
| Const("op &",_)$t1$t2 => And(qf_of_term ps vs t1,qf_of_term ps vs t2)
| Const("op |",_)$t1$t2 => Or(qf_of_term ps vs t1,qf_of_term ps vs t2)
- | Const("op -->",_)$t1$t2 => Impa(qf_of_term ps vs t1,qf_of_term ps vs t2)
- | Const("Not",_)$t' => Nota(qf_of_term ps vs t')
+ | Const("op -->",_)$t1$t2 => Imp(qf_of_term ps vs t1,qf_of_term ps vs t2)
+ | Const("Not",_)$t' => Not(qf_of_term ps vs t')
| Const("Ex",_)$Abs(xn,xT,p) =>
let val (xn',p') = variant_abs (xn,xT,p)
val vs' = (Free (xn',xT), nat 0) :: (map (fn(v,n) => (v,1 + n)) vs)
@@ -102,17 +102,17 @@
| Gt t' => @{term "op < :: int => _ "}$ @{term "0::int"}$ term_of_i vs t'
| Ge t' => @{term "op <= :: int => _ "}$ @{term "0::int"}$ term_of_i vs t'
| Eq t' => @{term "op = :: int => _ "}$ term_of_i vs t'$ @{term "0::int"}
- | NEq t' => term_of_qf ps vs (Nota(Eq t'))
+ | NEq t' => term_of_qf ps vs (Not(Eq t'))
| Dvd(i,t') => @{term "op dvd :: int => _ "}$
(HOLogic.mk_number HOLogic.intT i)$(term_of_i vs t')
- | NDvd(i,t')=> term_of_qf ps vs (Nota(Dvd(i,t')))
- | Nota t' => HOLogic.Not$(term_of_qf ps vs t')
+ | NDvd(i,t')=> term_of_qf ps vs (Not(Dvd(i,t')))
+ | Not t' => HOLogic.Not$(term_of_qf ps vs t')
| And(t1,t2) => HOLogic.conj$(term_of_qf ps vs t1)$(term_of_qf ps vs t2)
| Or(t1,t2) => HOLogic.disj$(term_of_qf ps vs t1)$(term_of_qf ps vs t2)
- | Impa(t1,t2) => HOLogic.imp$(term_of_qf ps vs t1)$(term_of_qf ps vs t2)
- | Iffa(t1,t2) => HOLogic.eq_const HOLogic.boolT $ term_of_qf ps vs t1 $ term_of_qf ps vs t2
+ | Imp(t1,t2) => HOLogic.imp$(term_of_qf ps vs t1)$(term_of_qf ps vs t2)
+ | Iff(t1,t2) => HOLogic.eq_const HOLogic.boolT $ term_of_qf ps vs t1 $ term_of_qf ps vs t2
| Closed n => (fst o the) (find_first (fn (_, m) => m = n) ps)
- | NClosed n => term_of_qf ps vs (Nota (Closed n))
+ | NClosed n => term_of_qf ps vs (Not (Closed n))
| _ => error "If this is raised, Isabelle/HOL or generate_code is inconsistent!";
(* The oracle *)
--- a/src/Pure/Isar/ROOT.ML Fri Aug 24 14:14:18 2007 +0200
+++ b/src/Pure/Isar/ROOT.ML Fri Aug 24 14:14:20 2007 +0200
@@ -43,15 +43,17 @@
use "net_rules.ML";
use "induct_attrib.ML";
-(*executable theory content*)
-use "code_unit.ML";
-use "code.ML";
-
(*derived theory and proof elements*)
use "calculation.ML";
use "obtain.ML";
use "locale.ML";
use "class.ML";
+
+(*executable theory content*)
+use "code_unit.ML";
+use "code.ML";
+
+(*local theories and specifications*)
use "local_theory.ML";
use "theory_target.ML";
use "spec_parse.ML";
--- a/src/Pure/Isar/class.ML Fri Aug 24 14:14:18 2007 +0200
+++ b/src/Pure/Isar/class.ML Fri Aug 24 14:14:20 2007 +0200
@@ -15,31 +15,35 @@
-> string list -> theory -> string * Proof.context
val class_cmd: bstring -> string list -> Element.context Locale.element list
-> string list -> theory -> string * Proof.context
+ val class_of_locale: theory -> string -> class option
+ val add_const_in_class: string -> (string * term) * Syntax.mixfix
+ -> theory -> theory
+
val instance_arity: arity list -> ((bstring * Attrib.src list) * term) list
+ -> (thm list -> theory -> theory)
-> theory -> Proof.state
val instance_arity_cmd: (bstring * string list * string) list
-> ((bstring * Attrib.src list) * string) list
+ -> (thm list -> theory -> theory)
-> theory -> Proof.state
val prove_instance_arity: tactic -> arity list
-> ((bstring * Attrib.src list) * term) list
- -> theory -> theory
+ -> theory -> thm list * theory
+ val unoverload: theory -> conv
+ val overload: theory -> conv
+ val unoverload_const: theory -> string * typ -> string
+ val inst_const: theory -> string * string -> string
+ val param_const: theory -> string -> (string * string) option
+ val intro_classes_tac: thm list -> tactic
+ val default_intro_classes_tac: thm list -> tactic
+
val instance_class: class * class -> theory -> Proof.state
val instance_class_cmd: string * string -> theory -> Proof.state
val instance_sort: class * sort -> theory -> Proof.state
val instance_sort_cmd: string * string -> theory -> Proof.state
val prove_instance_sort: tactic -> class * sort -> theory -> theory
- val class_of_locale: theory -> string -> class option
- val add_const_in_class: string -> (string * term) * Syntax.mixfix
- -> theory -> theory
-
- val unoverload: theory -> thm -> thm
- val overload: theory -> thm -> thm
- val inst_const: theory -> string * string -> string
-
val print_classes: theory -> unit
- val intro_classes_tac: thm list -> tactic
- val default_intro_classes_tac: thm list -> tactic
end;
structure Class : CLASS =
@@ -130,24 +134,39 @@
structure InstData = TheoryDataFun
(
- type T = (string * thm) Symtab.table Symtab.table;
- (*constant name ~> type constructor ~> (constant name, equation)*)
- val empty = Symtab.empty;
+ type T = (string * thm) Symtab.table Symtab.table * (string * string) Symtab.table;
+ (*constant name ~> type constructor ~> (constant name, equation),
+ constant name ~> (constant name, type constructor)*)
+ val empty = (Symtab.empty, Symtab.empty);
val copy = I;
val extend = I;
- fun merge _ = Symtab.join (K (Symtab.merge (K true)));
+ fun merge _ ((taba1, tabb1), (taba2, tabb2)) =
+ (Symtab.join (K (Symtab.merge (K true))) (taba1, taba2),
+ Symtab.merge (K true) (tabb1, tabb2));
);
fun inst_thms f thy =
- Symtab.fold (Symtab.fold (cons o f o snd o snd) o snd) (InstData.get thy) [];
-fun add_inst (c, tyco) inst = (InstData.map o Symtab.map_default (c, Symtab.empty))
- (Symtab.update_new (tyco, inst));
+ (Symtab.fold (Symtab.fold (cons o f o snd o snd) o snd) o fst) (InstData.get thy) [];
+fun add_inst (c, tyco) inst = (InstData.map o apfst o Symtab.map_default (c, Symtab.empty))
+ (Symtab.update_new (tyco, inst))
+ #> (InstData.map o apsnd) (Symtab.update_new (fst inst, (c, tyco)));
-fun unoverload thy thm = MetaSimplifier.rewrite_rule (inst_thms I thy) thm;
-fun overload thy thm = MetaSimplifier.rewrite_rule (inst_thms symmetric thy) thm;
+fun unoverload thy thm = MetaSimplifier.rewrite false (inst_thms I thy) thm;
+fun overload thy thm = MetaSimplifier.rewrite false (inst_thms symmetric thy) thm;
fun inst_const thy (c, tyco) =
- (fst o the o Symtab.lookup ((the o Symtab.lookup (InstData.get thy)) c)) tyco;
+ (fst o the o Symtab.lookup ((the o Symtab.lookup (fst (InstData.get thy))) c)) tyco;
+fun unoverload_const thy (c_ty as (c, _)) =
+ case AxClass.class_of_param thy c
+ of SOME class => (case Sign.const_typargs thy c_ty
+ of [Type (tyco, _)] =>
+ (case Symtab.lookup ((the o Symtab.lookup (fst (InstData.get thy))) c) tyco
+ of SOME (c, _) => c
+ | NONE => c)
+ | [_] => c)
+ | NONE => c;
+
+val param_const = Symtab.lookup o snd o InstData.get;
fun add_inst_def (class, tyco) (c, ty) thy =
let
@@ -166,7 +185,7 @@
end;
fun add_inst_def' (class, tyco) (c, ty) thy =
- if case Symtab.lookup (InstData.get thy) c
+ if case Symtab.lookup (fst (InstData.get thy)) c
of NONE => true
| SOME tab => is_none (Symtab.lookup tab tyco)
then add_inst_def (class, tyco) (c, Logic.unvarifyT ty) thy
@@ -176,7 +195,7 @@
let
val ((lhs as Const (c, ty), args), rhs) = (apfst Term.strip_comb o Logic.dest_equals) prop;
fun add_inst' def ([], (Const (c_inst, ty))) =
- if forall (fn TFree_ => true | _ => false) (Sign.const_typargs thy (c_inst, ty))
+ if forall (fn TFree _ => true | _ => false) (Sign.const_typargs thy (c_inst, ty))
then add_inst (c, tyco) (c_inst, def)
else add_inst_def (class, tyco) (c, ty)
| add_inst' _ t = add_inst_def (class, tyco) (c, ty);
@@ -205,7 +224,7 @@
fun read_def_cmd thy = gen_read_def thy Attrib.intern_src Theory.read_axm;
fun read_def thy = gen_read_def thy (K I) (K I);
-fun gen_instance_arity prep_arity read_def do_proof raw_arities raw_defs theory =
+fun gen_instance_arity prep_arity read_def do_proof raw_arities raw_defs after_qed theory =
let
val arities = map (prep_arity theory) raw_arities;
val _ = if null arities then error "at least one arity must be given" else ();
@@ -259,28 +278,32 @@
|> Sign.add_const_constraint_i (c, NONE)
|> pair (c, Logic.unvarifyT ty)
end;
- fun after_qed cs defs =
+ fun after_qed' cs defs =
fold Sign.add_const_constraint_i (map (apsnd SOME) cs)
- #> fold (Code.add_func false) defs;
+ #> after_qed defs;
in
theory
|> fold_map get_remove_contraint (map fst cs |> distinct (op =))
||>> fold_map add_def defs
||> fold (fn (c, ((class, tyco), ty)) => add_inst_def' (class, tyco) (c, ty)) other_cs
- |-> (fn (cs, defs) => do_proof (after_qed cs defs) arities)
+ |-> (fn (cs, defs) => do_proof (after_qed' cs defs) arities defs)
end;
fun instance_arity_cmd' do_proof = gen_instance_arity Sign.read_arity read_def_cmd do_proof;
fun instance_arity' do_proof = gen_instance_arity Sign.cert_arity read_def do_proof;
-fun tactic_proof tac after_qed arities =
+fun tactic_proof tac f arities defs =
fold (fn arity => AxClass.prove_arity arity tac) arities
- #> after_qed;
+ #> f
+ #> pair defs;
in
-val instance_arity_cmd = instance_arity_cmd' axclass_instance_arity;
-val instance_arity = instance_arity' axclass_instance_arity;
-val prove_instance_arity = instance_arity' o tactic_proof;
+val instance_arity_cmd = instance_arity_cmd'
+ (fn f => fn arities => fn defs => axclass_instance_arity f arities);
+val instance_arity = instance_arity'
+ (fn f => fn arities => fn defs => axclass_instance_arity f arities);
+fun prove_instance_arity tac arities defs =
+ instance_arity' (tactic_proof tac) arities defs (K I);
end; (*local*)
--- a/src/Pure/Isar/code.ML Fri Aug 24 14:14:18 2007 +0200
+++ b/src/Pure/Isar/code.ML Fri Aug 24 14:14:20 2007 +0200
@@ -10,7 +10,7 @@
sig
val add_func: bool -> thm -> theory -> theory
val del_func: thm -> theory -> theory
- val add_funcl: CodeUnit.const * thm list Susp.T -> theory -> theory
+ val add_funcl: string * thm list Susp.T -> theory -> theory
val add_func_attr: bool -> Attrib.src
val add_inline: thm -> theory -> theory
val del_inline: thm -> theory -> theory
@@ -20,17 +20,15 @@
val del_preproc: string -> theory -> theory
val add_post: thm -> theory -> theory
val del_post: thm -> theory -> theory
- val add_datatype: string * ((string * sort) list * (string * typ list) list)
- -> theory -> theory
- val add_datatype_consts: CodeUnit.const list -> theory -> theory
- val add_datatype_consts_cmd: string list -> theory -> theory
+ val add_datatype: (string * typ) list -> theory -> theory
+ val add_datatype_cmd: string list -> theory -> theory
val coregular_algebra: theory -> Sorts.algebra
val operational_algebra: theory -> (sort -> sort) * Sorts.algebra
- val these_funcs: theory -> CodeUnit.const -> thm list
+ val these_funcs: theory -> string -> thm list
val get_datatype: theory -> string -> ((string * sort) list * (string * typ list) list)
- val get_datatype_of_constr: theory -> CodeUnit.const -> string option
- val default_typ: theory -> CodeUnit.const -> typ
+ val get_datatype_of_constr: theory -> string -> string option
+ val default_typ: theory -> string -> typ
val preprocess_conv: cterm -> thm
val postprocess_conv: cterm -> thm
@@ -45,7 +43,7 @@
type T
val empty: T
val merge: Pretty.pp -> T * T -> T
- val purge: theory option -> CodeUnit.const list option -> T -> T
+ val purge: theory option -> string list option -> T -> T
end;
signature CODE_DATA =
@@ -60,7 +58,7 @@
sig
include CODE
val declare_data: Object.T -> (Pretty.pp -> Object.T * Object.T -> Object.T)
- -> (theory option -> CodeUnit.const list option -> Object.T -> Object.T) -> serial
+ -> (theory option -> string list option -> Object.T -> Object.T) -> serial
val get_data: serial * ('a -> Object.T) * (Object.T -> 'a)
-> theory -> 'a
val change_data: serial * ('a -> Object.T) * (Object.T -> 'a)
@@ -74,9 +72,6 @@
(** preliminaries **)
-structure Consttab = CodeUnit.Consttab;
-
-
(* certificate theorems *)
fun string_of_lthms r = case Susp.peek r
@@ -224,24 +219,23 @@
fun join_func_thms (tabs as (tab1, tab2)) =
let
- val cs1 = Consttab.keys tab1;
- val cs2 = Consttab.keys tab2;
- val cs' = filter (member CodeUnit.eq_const cs2) cs1;
+ val cs1 = Symtab.keys tab1;
+ val cs2 = Symtab.keys tab2;
+ val cs' = filter (member (op =) cs2) cs1;
val cs'' = subtract (op =) cs' cs1 @ subtract (op =) cs' cs2;
- val cs''' = ref [] : CodeUnit.const list ref;
+ val cs''' = ref [] : string list ref;
fun merge c x = let val (touched, thms') = merge_sdthms x in
(if touched then cs''' := cons c (!cs''') else (); thms') end;
- in (cs'' @ !cs''', Consttab.join merge tabs) end;
+ in (cs'' @ !cs''', Symtab.join merge tabs) end;
fun merge_funcs (thms1, thms2) =
let
val (consts, thms) = join_func_thms (thms1, thms2);
in (SOME consts, thms) end;
val eq_string = op = : string * string -> bool;
-val eq_co = op = : (string * typ list) * (string * typ list) -> bool;
fun eq_dtyp ((vs1, cs1), (vs2, cs2)) =
gen_eq_set (eq_pair eq_string (gen_eq_set eq_string)) (vs1, vs2)
- andalso gen_eq_set eq_co (cs1, cs2);
+ andalso gen_eq_set (eq_fst eq_string) (cs1, cs2);
fun merge_dtyps (tabs as (tab1, tab2)) =
let
val tycos1 = Symtab.keys tab1;
@@ -256,7 +250,7 @@
in ((new_types, diff_types), Symtab.join join tabs) end;
datatype spec = Spec of {
- funcs: sdthms Consttab.table,
+ funcs: sdthms Symtab.table,
dtyps: ((string * sort) list * (string * typ list) list) Symtab.table
};
@@ -289,7 +283,7 @@
val touched = if touched' then NONE else touched_cs;
in (touched, mk_exec (thmproc, spec)) end;
val empty_exec = mk_exec (mk_thmproc ((([], []), []), []),
- mk_spec (Consttab.empty, Symtab.empty));
+ mk_spec (Symtab.empty, Symtab.empty));
fun the_thmproc (Exec { thmproc = Preproc x, ...}) = x;
fun the_spec (Exec { spec = Spec x, ...}) = x;
@@ -310,7 +304,7 @@
type kind = {
empty: Object.T,
merge: Pretty.pp -> Object.T * Object.T -> Object.T,
- purge: theory option -> CodeUnit.const list option -> Object.T -> Object.T
+ purge: theory option -> string list option -> Object.T -> Object.T
};
val kinds = ref (Datatab.empty: kind Datatab.table);
@@ -429,13 +423,14 @@
:: separate (Pretty.str "|") (map (fn (c, []) => Pretty.str c
| (c, tys) =>
(Pretty.block o Pretty.breaks)
- (Pretty.str c :: Pretty.str "of" :: map (Pretty.quote o Sign.pretty_typ thy) tys)) cos)
+ (Pretty.str (CodeUnit.string_of_const thy c)
+ :: Pretty.str "of" :: map (Pretty.quote o Sign.pretty_typ thy) tys)) cos)
);
val inlines = (#inlines o the_thmproc) exec;
val inline_procs = (map fst o #inline_procs o the_thmproc) exec;
val preprocs = (map fst o #preprocs o the_thmproc) exec;
val funs = the_funcs exec
- |> Consttab.dest
+ |> Symtab.dest
|> (map o apfst) (CodeUnit.string_of_const thy)
|> sort (string_ord o pairself fst);
val dtyps = the_dtyps exec
@@ -499,9 +494,11 @@
cons (Thm.ctyp_of thy (TVar (x_i, sort)), Thm.ctyp_of thy ty)) env [];
in map (Thm.instantiate (instT, [])) thms' end;
+fun const_of_func thy = Class.unoverload_const thy o CodeUnit.head_func;
+
fun certify_const thy const thms =
let
- fun cert thm = if CodeUnit.eq_const (const, fst (CodeUnit.head_func thm))
+ fun cert thm = if const = const_of_func thy thm
then thm else error ("Wrong head of defining equation,\nexpected constant "
^ CodeUnit.string_of_const thy const ^ "\n" ^ string_of_thm thm)
in map cert thms end;
@@ -527,15 +524,17 @@
fun specific_constraints thy (class, tyco) =
let
val vs = Name.invents Name.context "" (Sign.arity_number thy tyco);
- val clsops = (these o Option.map snd o try (AxClass.params_of_class thy)) class;
+ val clsops = (map fst o these o Option.map snd
+ o try (AxClass.params_of_class thy)) class;
val funcs = clsops
- |> map (fn (clsop, _) => (clsop, SOME tyco))
- |> map (Consttab.lookup ((the_funcs o get_exec) thy))
+ |> map (fn c => Class.inst_const thy (c, tyco))
+ |> map (Symtab.lookup ((the_funcs o get_exec) thy))
|> (map o Option.map) (Susp.force o fst)
|> maps these
- |> map (Thm.transfer thy);
- val sorts = map (map (snd o dest_TVar) o snd o dest_Type o the_single
- o Sign.const_typargs thy o (fn ((c, _), ty) => (c, ty)) o CodeUnit.head_func) funcs;
+ |> map (Thm.transfer thy)
+ fun sorts_of [Type (_, tys)] = map (snd o dest_TVar) tys
+ | sorts_of tys = map (snd o dest_TVar) tys;
+ val sorts = map (sorts_of o Sign.const_typargs thy o CodeUnit.head_func) funcs;
in sorts end;
fun weakest_constraints thy (class, tyco) =
@@ -587,8 +586,9 @@
fun assert_func_typ thm =
let
val thy = Thm.theory_of_thm thm;
- fun check_typ_classop class (const as (c, SOME tyco), thm) =
+ fun check_typ_classop tyco (c, thm) =
let
+ val SOME class = AxClass.class_of_param thy c;
val (_, ty) = CodeUnit.head_func thm;
val ty_decl = classop_weakest_typ thy class (c, tyco);
val ty_strongest = classop_strongest_typ thy class (c, tyco);
@@ -615,12 +615,8 @@
^ string_of_thm thm
^ "\nis incompatible with permitted least general type\n"
^ CodeUnit.string_of_typ thy ty_strongest)
- end
- | check_typ_classop class ((c, NONE), thm) =
- CodeUnit.bad_thm ("Illegal type for class operation " ^ quote c
- ^ "\nin defining equation\n"
- ^ string_of_thm thm);
- fun check_typ_fun (const as (c, _), thm) =
+ end;
+ fun check_typ_fun (c, thm) =
let
val (_, ty) = CodeUnit.head_func thm;
val ty_decl = Sign.the_const_type thy c;
@@ -632,11 +628,11 @@
^ "\nis incompatible with declared function type\n"
^ CodeUnit.string_of_typ thy ty_decl)
end;
- fun check_typ (const as (c, _), thm) =
- case AxClass.class_of_param thy c
- of SOME class => check_typ_classop class (const, thm)
- | NONE => check_typ_fun (const, thm);
- in check_typ (fst (CodeUnit.head_func thm), thm) end;
+ fun check_typ (c, thm) =
+ case Class.param_const thy c
+ of SOME (c, tyco) => check_typ_classop tyco (c, thm)
+ | NONE => check_typ_fun (c, thm);
+ in check_typ (const_of_func thy thm, thm) end;
val mk_func = CodeUnit.error_thm (assert_func_typ o CodeUnit.mk_func);
val mk_func_liberal = CodeUnit.warning_thm (assert_func_typ o CodeUnit.mk_func);
@@ -647,21 +643,56 @@
(** interfaces and attributes **)
+fun get_datatype thy tyco =
+ case Symtab.lookup ((the_dtyps o get_exec) thy) tyco
+ of SOME spec => spec
+ | NONE => Sign.arity_number thy tyco
+ |> Name.invents Name.context "'a"
+ |> map (rpair [])
+ |> rpair [];
+
+fun get_datatype_of_constr thy c =
+ case (snd o strip_type o Sign.the_const_type thy) c
+ of Type (tyco, _) => if member (op =)
+ ((the_default [] o Option.map (map fst o snd) o Symtab.lookup ((the_dtyps o get_exec) thy)) tyco) c
+ then SOME tyco else NONE
+ | _ => NONE;
+
+fun get_constr_typ thy c =
+ case get_datatype_of_constr thy c
+ of SOME tyco => let
+ val (vs, cos) = get_datatype thy tyco;
+ val SOME tys = AList.lookup (op =) cos c;
+ val ty = tys ---> Type (tyco, map TFree vs);
+ in SOME (Logic.varifyT ty) end
+ | NONE => NONE;
+
fun add_func true thm thy =
let
val func = mk_func thm;
- val (const, _) = CodeUnit.head_func func;
- in map_exec_purge (SOME [const]) (map_funcs
- (Consttab.map_default
- (const, (Susp.value [], [])) (add_thm func))) thy
+ val c = const_of_func thy func;
+ val _ = if (is_some o AxClass.class_of_param thy) c
+ then error ("Rejected polymorphic equation for overloaded constant:\n"
+ ^ string_of_thm thm)
+ else ();
+ val _ = if (is_some o get_datatype_of_constr thy) c
+ then error ("Rejected equation for datatype constructor:\n"
+ ^ string_of_thm func)
+ else ();
+ in map_exec_purge (SOME [c]) (map_funcs
+ (Symtab.map_default
+ (c, (Susp.value [], [])) (add_thm func))) thy
end
| add_func false thm thy =
case mk_func_liberal thm
of SOME func => let
- val (const, _) = CodeUnit.head_func func
- in map_exec_purge (SOME [const]) (map_funcs
- (Consttab.map_default
- (const, (Susp.value [], [])) (add_thm func))) thy
+ val c = const_of_func thy func
+ in if (is_some o AxClass.class_of_param thy) c
+ orelse (is_some o get_datatype_of_constr thy) c
+ then thy
+ else map_exec_purge (SOME [c]) (map_funcs
+ (Symtab.map_default
+ (c, (Susp.value [], [])) (add_thm func))) thy
end
| NONE => thy;
@@ -672,9 +703,9 @@
fun del_func thm thy =
let
val func = mk_func thm;
- val (const, _) = CodeUnit.head_func func;
+ val const = const_of_func thy func;
in map_exec_purge (SOME [const]) (map_funcs
- (Consttab.map_entry
+ (Symtab.map_entry
const (del_thm func))) thy
end;
@@ -684,41 +715,31 @@
(*FIXME must check compatibility with sort algebra;
alas, naive checking results in non-termination!*)
in
- map_exec_purge (SOME [const]) (map_funcs (Consttab.map_default (const, (Susp.value [], []))
+ map_exec_purge (SOME [const]) (map_funcs (Symtab.map_default (const, (Susp.value [], []))
(add_lthms lthms'))) thy
end;
fun add_func_attr strict = Attrib.internal (fn _ => Thm.declaration_attribute
(fn thm => Context.mapping (add_func strict thm) I));
-local
-
-fun del_datatype tyco thy =
- case Symtab.lookup ((the_dtyps o get_exec) thy) tyco
- of SOME (vs, cos) => let
- val consts = CodeUnit.consts_of_cos thy tyco vs cos;
- in map_exec_purge (if null consts then NONE else SOME consts)
- (map_dtyps (Symtab.delete tyco)) thy end
- | NONE => thy;
-
-in
-
-fun add_datatype (tyco, (vs_cos as (vs, cos))) thy =
+fun add_datatype raw_cs thy =
let
- val consts = CodeUnit.consts_of_cos thy tyco vs cos;
+ val cs = map (fn c_ty as (_, ty) => (Class.unoverload_const thy c_ty, ty)) raw_cs;
+ val (tyco, vs_cos) = CodeUnit.constrset_of_consts thy cs;
+ val purge_cs = map fst (snd vs_cos);
+ val purge_cs' = case Symtab.lookup ((the_dtyps o get_exec) thy) tyco
+ of SOME (vs, cos) => if null cos then NONE else SOME (purge_cs @ map fst cos)
+ | NONE => NONE;
in
thy
- |> del_datatype tyco
- |> map_exec_purge (SOME consts) (map_dtyps (Symtab.update_new (tyco, vs_cos)))
+ |> map_exec_purge purge_cs' (map_dtyps (Symtab.update (tyco, vs_cos))
+ #> map_funcs (fold (Symtab.delete_safe o fst) cs))
end;
-fun add_datatype_consts consts thy =
- add_datatype (CodeUnit.cos_of_consts thy consts) thy;
-
-fun add_datatype_consts_cmd raw_cs thy =
- add_datatype_consts (map (CodeUnit.read_const thy) raw_cs) thy
-
-end; (*local*)
+fun add_datatype_cmd raw_cs thy =
+ let
+ val cs = map (CodeUnit.read_bare_const thy) raw_cs;
+ in add_datatype cs thy end;
fun add_inline thm thy =
(map_exec_purge NONE o map_thmproc o apfst o apfst o apfst)
@@ -790,7 +811,7 @@
fun apply_preproc thy f [] = []
| apply_preproc thy f (thms as (thm :: _)) =
let
- val (const, _) = CodeUnit.head_func thm;
+ val const = const_of_func thy thm;
val thms' = f thy thms;
in certify_const thy const thms' end;
@@ -807,7 +828,8 @@
|> map (CodeUnit.rewrite_func ((#inlines o the_thmproc o get_exec) thy))
|> fold (fn (_, (_, f)) => apply_inline_proc thy f) ((#inline_procs o the_thmproc o get_exec) thy)
(*FIXME - must check: rewrite rule, defining equation, proper constant |> map (snd o check_func false thy) *)
- |> common_typ_funcs;
+ |> common_typ_funcs
+ |> map (Conv.fconv_rule (Class.unoverload thy));
fun preprocess_conv ct =
let
@@ -817,6 +839,7 @@
|> MetaSimplifier.rewrite false ((#inlines o the_thmproc o get_exec) thy)
|> fold (fn (_, (_, f)) => rhs_conv (apply_inline_proc_cterm thy f))
((#inline_procs o the_thmproc o get_exec) thy)
+ |> rhs_conv (Class.unoverload thy)
end;
fun postprocess_conv ct =
@@ -824,49 +847,24 @@
val thy = Thm.theory_of_cterm ct;
in
ct
- |> MetaSimplifier.rewrite false ((#posts o the_thmproc o get_exec) thy)
+ |> Class.overload thy
+ |> rhs_conv (MetaSimplifier.rewrite false ((#posts o the_thmproc o get_exec) thy))
end;
end; (*local*)
-fun get_datatype thy tyco =
- case Symtab.lookup ((the_dtyps o get_exec) thy) tyco
- of SOME spec => spec
- | NONE => Sign.arity_number thy tyco
- |> Name.invents Name.context "'a"
- |> map (rpair [])
- |> rpair [];
-
-fun get_datatype_of_constr thy const =
- case CodeUnit.co_of_const' thy const
- of SOME (tyco, (_, co)) => if member eq_co
- (Symtab.lookup (((the_dtyps o get_exec) thy)) tyco
- |> Option.map snd
- |> the_default []) co then SOME tyco else NONE
- | NONE => NONE;
-
-fun get_constr_typ thy const =
- case get_datatype_of_constr thy const
- of SOME tyco => let
- val (vs, cos) = get_datatype thy tyco;
- val (_, (_, (co, tys))) = CodeUnit.co_of_const thy const
- in (tys ---> Type (tyco, map TFree vs))
- |> map_atyps (fn TFree (v, _) => TFree (v, AList.lookup (op =) vs v |> the))
- |> Logic.varifyT
- |> SOME end
- | NONE => NONE;
-
-fun default_typ_proto thy (const as (c, SOME tyco)) = classop_weakest_typ thy
- ((the o AxClass.class_of_param thy) c) (c, tyco) |> SOME
- | default_typ_proto thy (const as (c, NONE)) = case AxClass.class_of_param thy c
- of SOME class => SOME (Term.map_type_tvar
- (K (TVar (("'a", 0), [class]))) (Sign.the_const_type thy c))
- | NONE => get_constr_typ thy const;
+fun default_typ_proto thy c = case Class.param_const thy c
+ of SOME (c, tyco) => classop_weakest_typ thy ((the o AxClass.class_of_param thy) c)
+ (c, tyco) |> SOME
+ | NONE => (case AxClass.class_of_param thy c
+ of SOME class => SOME (Term.map_type_tvar
+ (K (TVar (("'a", 0), [class]))) (Sign.the_const_type thy c))
+ | NONE => get_constr_typ thy c);
local
fun get_funcs thy const =
- Consttab.lookup ((the_funcs o get_exec) thy) const
+ Symtab.lookup ((the_funcs o get_exec) thy) const
|> Option.map (Susp.force o fst)
|> these
|> map (Thm.transfer thy);
@@ -883,10 +881,10 @@
|> drop_refl thy
end;
-fun default_typ thy (const as (c, _)) = case default_typ_proto thy const
+fun default_typ thy c = case default_typ_proto thy c
of SOME ty => ty
- | NONE => (case get_funcs thy const
- of thm :: _ => snd (CodeUnit.head_func thm)
+ | NONE => (case get_funcs thy c
+ of thm :: _ => snd (CodeUnit.head_func (Conv.fconv_rule (Class.unoverload thy) thm))
| [] => Sign.the_const_type thy c);
end; (*local*)
--- a/src/Pure/Isar/code_unit.ML Fri Aug 24 14:14:18 2007 +0200
+++ b/src/Pure/Isar/code_unit.ML Fri Aug 24 14:14:20 2007 +0200
@@ -2,45 +2,28 @@
ID: $Id$
Author: Florian Haftmann, TU Muenchen
-Basic units of code generation: Identifying (possibly overloaded) constants
-by name plus optional type constructor. Convenient data structures for constants.
-Defining equations ("func"s). Auxiliary.
+Basic units of code generation. Auxiliary.
*)
signature CODE_UNIT =
sig
- type const = string * string option (*constant name, possibly instance*)
- val const_ord: const * const -> order
- val eq_const: const * const -> bool
- structure Consttab: TABLE
- val const_of_cexpr: theory -> string * typ -> const
val string_of_typ: theory -> typ -> string
- val string_of_const: theory -> const -> string
+ val string_of_const: theory -> string -> string
+ val no_args: theory -> string -> int
val read_bare_const: theory -> string -> string * typ
- val read_const: theory -> string -> const
- val read_const_exprs: theory -> (const list -> const list)
- -> string list -> bool * const list
+ val read_const: theory -> string -> string
+ val read_const_exprs: theory -> (string list -> string list)
+ -> string list -> bool * string list
- val co_of_const: theory -> const
- -> string * ((string * sort) list * (string * typ list))
- val co_of_const': theory -> const
- -> (string * ((string * sort) list * (string * typ list))) option
- val cos_of_consts: theory -> const list
+ val constrset_of_consts: theory -> (string * typ) list
-> string * ((string * sort) list * (string * typ list) list)
- val const_of_co: theory -> string -> (string * sort) list
- -> string * typ list -> const
- val consts_of_cos: theory -> string -> (string * sort) list
- -> (string * typ list) list -> const list
- val no_args: theory -> const -> int
-
- val typargs: theory -> string * typ -> typ list
val typ_sort_inst: Sorts.algebra -> typ * sort
-> sort Vartab.table -> sort Vartab.table
val assert_rew: thm -> thm
val mk_rew: thm -> thm
val mk_func: thm -> thm
- val head_func: thm -> const * typ
+ val head_func: thm -> string * typ
val bad_thm: string -> 'a
val error_thm: (thm -> thm) -> thm -> thm
val warning_thm: (thm -> thm) -> thm -> thm option
@@ -64,37 +47,12 @@
fun warning_thm f thm = SOME (f thm) handle BAD_THM msg
=> (warning ("code generator: " ^ msg); NONE);
-
-(* basic data structures *)
-
-type const = string * string option;
-val const_ord = prod_ord fast_string_ord (option_ord string_ord);
-val eq_const = is_equal o const_ord;
-
-structure Consttab =
- TableFun(
- type key = const;
- val ord = const_ord;
- );
-
fun string_of_typ thy = setmp show_sorts true (Sign.string_of_typ thy);
-
+fun string_of_const thy c = case Class.param_const thy c
+ of SOME (c, tyco) => Sign.extern_const thy c ^ " " ^ enclose "[" "]" (Sign.extern_type thy tyco)
+ | NONE => Sign.extern_const thy c;
-(* conversion between constant expressions and constants *)
-
-fun const_of_cexpr thy (c_ty as (c, _)) =
- case AxClass.class_of_param thy c
- of SOME class => (case Sign.const_typargs thy c_ty
- of [Type (tyco, _)] => if can (Sorts.mg_domain (Sign.classes_of thy) tyco) [class]
- then (c, SOME tyco)
- else (c, NONE)
- | [_] => (c, NONE))
- | NONE => (c, NONE);
-
-fun string_of_const thy (c, NONE) = Sign.extern_const thy c
- | string_of_const thy (c, SOME tyco) = Sign.extern_const thy c
- ^ " " ^ enclose "[" "]" (Sign.extern_type thy tyco);
-
+fun no_args thy = length o fst o strip_type o Sign.the_const_type thy;
(* reading constants as terms and wildcards pattern *)
@@ -106,7 +64,7 @@
| NONE => error ("Not a constant: " ^ Sign.string_of_term thy t)
end;
-fun read_const thy = const_of_cexpr thy o read_bare_const thy;
+fun read_const thy = Class.unoverload_const thy o read_bare_const thy;
local
@@ -115,27 +73,11 @@
val this_thy = Option.map theory some_thyname |> the_default thy;
val cs = Symtab.fold (fn (c, (_, NONE)) => cons c | _ => I)
((snd o #constants o Consts.dest o #consts o Sign.rep_sg) this_thy) [];
- fun classop c = case AxClass.class_of_param thy c
- of NONE => [(c, NONE)]
- | SOME class => Symtab.fold
- (fn (tyco, classes) => if AList.defined (op =) classes class
- then cons (c, SOME tyco) else I)
- ((#arities o Sorts.rep_algebra o Sign.classes_of) this_thy)
- [(c, NONE)];
- val consts = maps classop cs;
- fun test_instance thy (class, tyco) =
- can (Sorts.mg_domain (Sign.classes_of thy) tyco) [class]
- fun belongs_here thyname (c, NONE) =
+ fun belongs_here thyname c =
not (exists (fn thy' => Sign.declared_const thy' c) (Theory.parents_of this_thy))
- | belongs_here thyname (c, SOME tyco) =
- let
- val SOME class = AxClass.class_of_param thy c
- in not (exists (fn thy' => test_instance thy' (class, tyco))
- (Theory.parents_of this_thy))
- end;
in case some_thyname
- of NONE => consts
- | SOME thyname => filter (belongs_here thyname) consts
+ of NONE => cs
+ | SOME thyname => filter (belongs_here thyname) cs
end;
fun read_const_expr thy "*" = ([], consts_of thy NONE)
@@ -152,89 +94,48 @@
end; (*local*)
-(* conversion between constants, constant expressions and datatype constructors *)
-
-fun const_of_co thy tyco vs (co, tys) =
- const_of_cexpr thy (co, tys ---> Type (tyco, map TFree vs));
-
-fun consts_of_cos thy tyco vs cos =
- let
- val dty = Type (tyco, map TFree vs);
- fun mk_co (co, tys) = const_of_cexpr thy (co, tys ---> dty);
- in map mk_co cos end;
-
-local
-exception BAD of string;
+(* constructor sets *)
-fun mg_typ_of_const thy (c, NONE) = Sign.the_const_type thy c
- | mg_typ_of_const thy (c, SOME tyco) =
- let
- val SOME class = AxClass.class_of_param thy c;
- val ty = Sign.the_const_type thy c;
- (*an approximation*)
- val sorts = Sorts.mg_domain (Sign.classes_of thy) tyco [class]
- handle CLASS_ERROR => raise BAD ("No such instance: " ^ tyco ^ " :: " ^ class
- ^ ",\nrequired for overloaded constant " ^ c);
- val vs = Name.invents Name.context "'a" (length sorts);
- in map_atyps (K (Type (tyco, map (fn v => TVar ((v, 0), [])) vs))) ty end;
-
-fun gen_co_of_const thy const =
+fun constrset_of_consts thy cs =
let
- val (c, _) = const;
- val ty = (Logic.unvarifyT o mg_typ_of_const thy) const;
- fun err () = raise BAD
- ("Illegal type for datatype constructor: " ^ string_of_typ thy ty);
- val (tys, ty') = strip_type ty;
- val (tyco, vs) = ((apsnd o map) dest_TFree o dest_Type) ty'
- handle TYPE _ => err ();
- val sorts = if has_duplicates (eq_fst op =) vs then err ()
- else map snd vs;
- val vs_names = Name.invent_list [] "'a" (length vs);
- val vs_map = map fst vs ~~ vs_names;
- val vs' = vs_names ~~ sorts;
- val tys' = (map o map_type_tfree) (fn (v, sort) =>
- (TFree ((the o AList.lookup (op =) vs_map) v, sort))) tys
- handle Option => err ();
- in (tyco, (vs', (c, tys'))) end;
-
-in
-
-fun co_of_const thy const = gen_co_of_const thy const handle BAD msg => error msg;
-fun co_of_const' thy const = SOME (gen_co_of_const thy const) handle BAD msg => NONE;
-
-fun no_args thy = length o fst o strip_type o mg_typ_of_const thy;
-
-end;
-
-fun cos_of_consts thy consts =
- let
- val raw_cos = map (co_of_const thy) consts;
- val (tyco, (vs_names, sorts_cos)) = if (length o distinct (eq_fst op =)) raw_cos = 1
- then ((fst o hd) raw_cos, ((map fst o fst o snd o hd) raw_cos,
- map ((apfst o map) snd o snd) raw_cos))
- else error ("Term constructors not referring to the same type: "
- ^ commas (map (string_of_const thy) consts));
- val sorts = foldr1 ((uncurry o map2 o curry o Sorts.inter_sort) (Sign.classes_of thy))
- (map fst sorts_cos);
- val cos = map snd sorts_cos;
- val vs = vs_names ~~ sorts;
- in (tyco, (vs, cos)) end;
+ fun no_constr (c, ty) = error ("Not a datatype constructor: " ^ string_of_const thy c
+ ^ " :: " ^ string_of_typ thy ty);
+ fun last_typ c_ty ty =
+ let
+ val frees = typ_tfrees ty;
+ val (tyco, vs) = ((apsnd o map) (dest_TFree) o dest_Type o snd o strip_type) ty
+ handle TYPE _ => no_constr c_ty
+ val _ = if has_duplicates (eq_fst (op =)) vs then no_constr c_ty else ();
+ val _ = if length frees <> length vs then no_constr c_ty else ();
+ in (tyco, vs) end;
+ fun ty_sorts (c, ty) =
+ let
+ val ty_decl = (Logic.unvarifyT o Sign.the_const_type thy) c;
+ val (tyco, vs_decl) = last_typ (c, ty) ty_decl;
+ val (_, vs) = last_typ (c, ty) ty;
+ in ((tyco, map snd vs), (c, (map fst vs, ty_decl))) end;
+ fun add ((tyco', sorts'), c) ((tyco, sorts), cs) =
+ let
+ val _ = if tyco' <> tyco
+ then error "Different type constructors in constructor set"
+ else ();
+ val sorts'' = map2 (curry (Sorts.inter_sort (Sign.classes_of thy))) sorts' sorts
+ in ((tyco, sorts), c :: cs) end;
+ fun inst vs' (c, (vs, ty)) =
+ let
+ val the_v = the o AList.lookup (op =) (vs ~~ vs');
+ val ty' = map_atyps (fn TFree (v, _) => TFree (the_v v)) ty;
+ in (c, (fst o strip_type) ty') end;
+ val c' :: cs' = map ty_sorts cs;
+ val ((tyco, sorts), cs'') = fold add cs' (apsnd single c');
+ val vs = Name.names Name.context "'a" sorts;
+ val cs''' = map (inst vs) cs'';
+ in (tyco, (vs, cs''')) end;
(* dictionary values *)
-fun typargs thy (c_ty as (c, ty)) =
- let
- val opt_class = AxClass.class_of_param thy c;
- val tys = Sign.const_typargs thy (c, ty);
- in case (opt_class, tys)
- of (SOME class, ty as [Type (tyco, tys')]) =>
- if can (Sorts.mg_domain (Sign.classes_of thy) tyco) [class]
- then tys' else ty
- | _ => tys
- end;
-
fun typ_sort_inst algebra =
let
val inters = Sorts.inter_sort algebra;
@@ -324,10 +225,9 @@
fun head_func thm =
let
val thy = Thm.theory_of_thm thm;
- val (Const (c_ty as (_, ty))) = (fst o strip_comb o fst o Logic.dest_equals
+ val Const (c, ty) = (fst o strip_comb o fst o Logic.dest_equals
o ObjectLogic.drop_judgment thy o Thm.plain_prop_of) thm;
- val const = const_of_cexpr thy c_ty;
- in (const, ty) end;
+ in (c, ty) end;
(* utilities *)
--- a/src/Pure/Isar/isar_syn.ML Fri Aug 24 14:14:18 2007 +0200
+++ b/src/Pure/Isar/isar_syn.ML Fri Aug 24 14:14:20 2007 +0200
@@ -431,7 +431,7 @@
|| P.$$$ "advanced" |-- P.xname -- ((P.$$$ "\\<subseteq>" || P.$$$ "<") |-- P.!!! P.xname)
>> Class.instance_sort_cmd
|| P.and_list1 P.arity -- Scan.repeat (SpecParse.opt_thm_name ":" -- P.prop)
- >> (fn (arities, defs) => Class.instance_arity_cmd arities defs)
+ >> (fn (arities, defs) => Class.instance_arity_cmd arities defs (fold (Code.add_func false)))
) >> (Toplevel.print oo Toplevel.theory_to_proof));
end;
@@ -441,7 +441,7 @@
val code_datatypeP =
OuterSyntax.command "code_datatype" "define set of code datatype constructors" K.thy_decl
- (Scan.repeat1 P.term >> (Toplevel.theory o Code.add_datatype_consts_cmd));
+ (Scan.repeat1 P.term >> (Toplevel.theory o Code.add_datatype_cmd));
--- a/src/Tools/code/code_funcgr.ML Fri Aug 24 14:14:18 2007 +0200
+++ b/src/Tools/code/code_funcgr.ML Fri Aug 24 14:14:20 2007 +0200
@@ -10,17 +10,14 @@
sig
type T
val timing: bool ref
- val funcs: T -> CodeUnit.const -> thm list
- val typ: T -> CodeUnit.const -> typ
- val all: T -> CodeUnit.const list
+ val funcs: T -> string -> thm list
+ val typ: T -> string -> typ
+ val all: T -> string list
val pretty: theory -> T -> Pretty.T
- val make: theory -> CodeUnit.const list -> T
- val make_consts: theory -> CodeUnit.const list -> CodeUnit.const list * T
+ val make: theory -> string list -> T
+ val make_consts: theory -> string list -> string list * T
val eval_conv: theory -> (T -> cterm -> thm) -> cterm -> thm
val eval_term: theory -> (T -> cterm -> 'a) -> cterm -> 'a
- val intervene: theory -> T -> T
- (*FIXME drop intervene as soon as possible*)
- structure Constgraph : GRAPH
end
structure CodeFuncgr : CODE_FUNCGR =
@@ -28,23 +25,18 @@
(** the graph type **)
-structure Constgraph = GraphFun (
- type key = CodeUnit.const;
- val ord = CodeUnit.const_ord;
-);
-
-type T = (typ * thm list) Constgraph.T;
+type T = (typ * thm list) Graph.T;
fun funcs funcgr =
- these o Option.map snd o try (Constgraph.get_node funcgr);
+ these o Option.map snd o try (Graph.get_node funcgr);
fun typ funcgr =
- fst o Constgraph.get_node funcgr;
+ fst o Graph.get_node funcgr;
-fun all funcgr = Constgraph.keys funcgr;
+fun all funcgr = Graph.keys funcgr;
fun pretty thy funcgr =
- AList.make (snd o Constgraph.get_node funcgr) (Constgraph.keys funcgr)
+ AList.make (snd o Graph.get_node funcgr) (Graph.keys funcgr)
|> (map o apfst) (CodeUnit.string_of_const thy)
|> sort (string_ord o pairself fst)
|> map (fn (s, thms) =>
@@ -63,13 +55,9 @@
|> (fold o fold_aterms) (fn Const c => f c | _ => I);
fun consts_of (const, []) = []
- | consts_of (const, thms as thm :: _) =
+ | consts_of (const, thms as _ :: _) =
let
- val thy = Thm.theory_of_thm thm;
- val is_refl = curry CodeUnit.eq_const const;
- fun the_const c = case try (CodeUnit.const_of_cexpr thy) c
- of SOME const => if is_refl const then I else insert CodeUnit.eq_const const
- | NONE => I
+ fun the_const (c, _) = if c = const then I else insert (op =) c
in fold_consts the_const thms [] end;
fun insts_of thy algebra c ty_decl ty =
@@ -114,7 +102,7 @@
local
-exception INVALID of CodeUnit.const list * string;
+exception INVALID of string list * string;
fun resort_thms algebra tap_typ [] = []
| resort_thms algebra tap_typ (thms as thm :: _) =
@@ -123,11 +111,11 @@
val cs = fold_consts (insert (op =)) thms [];
fun match_const c (ty, ty_decl) =
let
- val tys = CodeUnit.typargs thy (c, ty);
- val sorts = map (snd o dest_TVar) (CodeUnit.typargs thy (c, ty_decl));
+ val tys = Sign.const_typargs thy (c, ty);
+ val sorts = map (snd o dest_TVar) (Sign.const_typargs thy (c, ty_decl));
in fold2 (curry (CodeUnit.typ_sort_inst algebra)) tys sorts end;
- fun match (c_ty as (c, ty)) =
- case tap_typ c_ty
+ fun match (c, ty) =
+ case tap_typ c
of SOME ty_decl => match_const c (ty, ty_decl)
| NONE => I;
val tvars = fold match cs Vartab.empty;
@@ -135,7 +123,7 @@
fun resort_funcss thy algebra funcgr =
let
- val typ_funcgr = try (fst o Constgraph.get_node funcgr o CodeUnit.const_of_cexpr thy);
+ val typ_funcgr = try (fst o Graph.get_node funcgr);
fun resort_dep (const, thms) = (const, resort_thms algebra typ_funcgr thms)
handle Sorts.CLASS_ERROR e => raise INVALID ([const], Sorts.msg_class_error (Sign.pp thy) e
^ ",\nfor constant " ^ CodeUnit.string_of_const thy const
@@ -150,12 +138,11 @@
in (Sign.typ_equiv thy (ty, ty'), (const, thms')) end;
fun resort_recs funcss =
let
- fun tap_typ c_ty = case try (CodeUnit.const_of_cexpr thy) c_ty
- of SOME const => AList.lookup (CodeUnit.eq_const) funcss const
- |> these
- |> try hd
- |> Option.map (snd o CodeUnit.head_func)
- | NONE => NONE;
+ fun tap_typ c =
+ AList.lookup (op =) funcss c
+ |> these
+ |> try hd
+ |> Option.map (snd o CodeUnit.head_func);
val (unchangeds, funcss') = split_list (map (resort_rec tap_typ) funcss);
val unchanged = fold (fn x => fn y => x andalso y) unchangeds true;
in (unchanged, funcss') end;
@@ -172,7 +159,7 @@
try (AxClass.params_of_class thy) class
|> Option.map snd
|> these
- |> map (fn (c, _) => (c, SOME tyco))
+ |> map (fn (c, _) => Class.inst_const thy (c, tyco))
in
Symtab.empty
|> fold (fn (tyco, class) =>
@@ -184,8 +171,7 @@
fun instances_of_consts thy algebra funcgr consts =
let
fun inst (cexpr as (c, ty)) = insts_of thy algebra c
- ((fst o Constgraph.get_node funcgr o CodeUnit.const_of_cexpr thy) cexpr)
- ty handle CLASS_ERROR => [];
+ ((fst o Graph.get_node funcgr) c) ty handle CLASS_ERROR => [];
in
[]
|> fold (fold (insert (op =)) o inst) consts
@@ -193,13 +179,13 @@
end;
fun ensure_const' thy algebra funcgr const auxgr =
- if can (Constgraph.get_node funcgr) const
+ if can (Graph.get_node funcgr) const
then (NONE, auxgr)
- else if can (Constgraph.get_node auxgr) const
+ else if can (Graph.get_node auxgr) const
then (SOME const, auxgr)
else if is_some (Code.get_datatype_of_constr thy const) then
auxgr
- |> Constgraph.new_node (const, [])
+ |> Graph.new_node (const, [])
|> pair (SOME const)
else let
val thms = Code.these_funcs thy const
@@ -208,9 +194,9 @@
val rhs = consts_of (const, thms);
in
auxgr
- |> Constgraph.new_node (const, thms)
+ |> Graph.new_node (const, thms)
|> fold_map (ensure_const thy algebra funcgr) rhs
- |-> (fn rhs' => fold (fn SOME const' => Constgraph.add_edge (const, const')
+ |-> (fn rhs' => fold (fn SOME const' => Graph.add_edge (const, const')
| NONE => I) rhs')
|> pair (SOME const)
end
@@ -225,24 +211,25 @@
let
val funcss = raw_funcss
|> resort_funcss thy algebra funcgr
- |> filter_out (can (Constgraph.get_node funcgr) o fst);
- fun typ_func const [] = Code.default_typ thy const
- | typ_func (_, NONE) (thm :: _) = (snd o CodeUnit.head_func) thm
- | typ_func (const as (c, SOME tyco)) (thms as (thm :: _)) =
- let
- val (_, ty) = CodeUnit.head_func thm;
- val SOME class = AxClass.class_of_param thy c;
- val sorts_decl = Sorts.mg_domain algebra tyco [class];
- val tys = CodeUnit.typargs thy (c, ty);
- val sorts = map (snd o dest_TVar) tys;
- in if sorts = sorts_decl then ty
- else raise INVALID ([const], "Illegal instantation for class operation "
- ^ CodeUnit.string_of_const thy const
- ^ "\nin defining equations\n"
- ^ (cat_lines o map string_of_thm) thms)
- end;
+ |> filter_out (can (Graph.get_node funcgr) o fst);
+ fun typ_func c [] = Code.default_typ thy c
+ | typ_func c (thms as thm :: _) = case Class.param_const thy c
+ of SOME (c', tyco) =>
+ let
+ val (_, ty) = CodeUnit.head_func thm;
+ val SOME class = AxClass.class_of_param thy c';
+ val sorts_decl = Sorts.mg_domain algebra tyco [class];
+ val tys = Sign.const_typargs thy (c, ty);
+ val sorts = map (snd o dest_TVar) tys;
+ in if sorts = sorts_decl then ty
+ else raise INVALID ([c], "Illegal instantation for class operation "
+ ^ CodeUnit.string_of_const thy c
+ ^ "\nin defining equations\n"
+ ^ (cat_lines o map string_of_thm) thms)
+ end
+ | NONE => (snd o CodeUnit.head_func) thm;
fun add_funcs (const, thms) =
- Constgraph.new_node (const, (typ_func const thms, thms));
+ Graph.new_node (const, (typ_func const thms, thms));
fun add_deps (funcs as (const, thms)) funcgr =
let
val deps = consts_of funcs;
@@ -251,8 +238,8 @@
in
funcgr
|> ensure_consts' thy algebra insts
- |> fold (curry Constgraph.add_edge const) deps
- |> fold (curry Constgraph.add_edge const) insts
+ |> fold (curry Graph.add_edge const) deps
+ |> fold (curry Graph.add_edge const) insts
end;
in
funcgr
@@ -261,29 +248,24 @@
end
and ensure_consts' thy algebra cs funcgr =
let
- val auxgr = Constgraph.empty
+ val auxgr = Graph.empty
|> fold (snd oo ensure_const thy algebra funcgr) cs;
in
funcgr
|> fold (merge_funcss thy algebra)
- (map (AList.make (Constgraph.get_node auxgr))
- (rev (Constgraph.strong_conn auxgr)))
+ (map (AList.make (Graph.get_node auxgr))
+ (rev (Graph.strong_conn auxgr)))
end handle INVALID (cs', msg)
- => raise INVALID (fold (insert CodeUnit.eq_const) cs' cs, msg);
-
-fun ensure_consts thy consts funcgr =
- let
- val algebra = Code.coregular_algebra thy
- in ensure_consts' thy algebra consts funcgr
- handle INVALID (cs', msg) => error (msg ^ ",\nwhile preprocessing equations for constant(s) "
- ^ commas (map (CodeUnit.string_of_const thy) cs'))
- end;
+ => raise INVALID (fold (insert (op =)) cs' cs, msg);
in
(** retrieval interfaces **)
-val ensure_consts = ensure_consts;
+fun ensure_consts thy algebra consts funcgr =
+ ensure_consts' thy algebra consts funcgr
+ handle INVALID (cs', msg) => error (msg ^ ",\nwhile preprocessing equations for constant(s) "
+ ^ commas (map (CodeUnit.string_of_const thy) cs'));
fun check_consts thy consts funcgr =
let
@@ -294,25 +276,20 @@
val (consts', funcgr') = fold_map try_const consts funcgr;
in (map_filter I consts', funcgr') end;
-fun ensure_consts_term_proto thy f ct funcgr =
+fun raw_eval thy f ct funcgr =
let
- fun consts_of thy t =
- fold_aterms (fn Const c => cons (CodeUnit.const_of_cexpr thy c) | _ => I) t []
- fun rhs_conv conv thm =
- let
- val thm' = (conv o Thm.rhs_of) thm;
- in Thm.transitive thm thm' end
+ val algebra = Code.coregular_algebra thy;
+ fun consts_of ct = fold_aterms (fn Const c_ty => cons c_ty | _ => I)
+ (Thm.term_of ct) [];
val _ = Sign.no_vars (Sign.pp thy) (Thm.term_of ct);
val _ = Term.fold_types (Type.no_tvars #> K I) (Thm.term_of ct) ();
val thm1 = Code.preprocess_conv ct;
val ct' = Thm.rhs_of thm1;
- val consts = consts_of thy (Thm.term_of ct');
- val funcgr' = ensure_consts thy consts funcgr;
- val algebra = Code.coregular_algebra thy;
+ val cs = map fst (consts_of ct');
+ val funcgr' = ensure_consts thy algebra cs funcgr;
val (_, thm2) = Thm.varifyT' [] thm1;
val thm3 = Thm.reflexive (Thm.rhs_of thm2);
- val typ_funcgr = try (fst o Constgraph.get_node funcgr' o CodeUnit.const_of_cexpr thy);
- val [thm4] = resort_thms algebra typ_funcgr [thm3];
+ val [thm4] = resort_thms algebra (try (fst o Graph.get_node funcgr')) [thm3];
val tfrees = Term.add_tfrees (Thm.prop_of thm1) [];
fun inst thm =
let
@@ -323,56 +300,54 @@
val thm5 = inst thm2;
val thm6 = inst thm4;
val ct'' = Thm.rhs_of thm6;
- val cs = fold_aterms (fn Const c => cons c | _ => I) (Thm.term_of ct'') [];
+ val c_exprs = consts_of ct'';
val drop = drop_classes thy tfrees;
- val instdefs = instances_of_consts thy algebra funcgr' cs;
- val funcgr'' = ensure_consts thy instdefs funcgr';
- in (f funcgr'' drop ct'' thm5, funcgr'') end;
+ val instdefs = instances_of_consts thy algebra funcgr' c_exprs;
+ val funcgr'' = ensure_consts thy algebra instdefs funcgr';
+ in (f drop thm5 funcgr'' ct'' , funcgr'') end;
-fun ensure_consts_eval thy conv =
+fun raw_eval_conv thy conv =
let
- fun conv' funcgr drop_classes ct thm1 =
+ fun conv' drop_classes thm1 funcgr ct =
let
val thm2 = conv funcgr ct;
val thm3 = Code.postprocess_conv (Thm.rhs_of thm2);
val thm23 = drop_classes (Thm.transitive thm2 thm3);
in
Thm.transitive thm1 thm23 handle THM _ =>
- error ("eval_conv - could not construct proof:\n"
+ error ("could not construct proof:\n"
^ (cat_lines o map string_of_thm) [thm1, thm2, thm3])
end;
- in ensure_consts_term_proto thy conv' end;
+ in raw_eval thy conv' end;
-fun ensure_consts_term thy f =
+fun raw_eval_term thy f =
let
- fun f' funcgr drop_classes ct thm1 = f funcgr ct;
- in ensure_consts_term_proto thy f' end;
+ fun f' _ _ funcgr ct = f funcgr ct;
+ in raw_eval thy f' end;
end; (*local*)
structure Funcgr = CodeDataFun
(struct
type T = T;
- val empty = Constgraph.empty;
- fun merge _ _ = Constgraph.empty;
- fun purge _ NONE _ = Constgraph.empty
+ val empty = Graph.empty;
+ fun merge _ _ = Graph.empty;
+ fun purge _ NONE _ = Graph.empty
| purge _ (SOME cs) funcgr =
- Constgraph.del_nodes ((Constgraph.all_preds funcgr
- o filter (can (Constgraph.get_node funcgr))) cs) funcgr;
+ Graph.del_nodes ((Graph.all_preds funcgr
+ o filter (can (Graph.get_node funcgr))) cs) funcgr;
end);
fun make thy =
- Funcgr.change thy o ensure_consts thy;
+ Funcgr.change thy o ensure_consts thy (Code.coregular_algebra thy);
fun make_consts thy =
Funcgr.change_yield thy o check_consts thy;
fun eval_conv thy f =
- fst o Funcgr.change_yield thy o ensure_consts_eval thy f;
+ fst o Funcgr.change_yield thy o raw_eval_conv thy f;
fun eval_term thy f =
- fst o Funcgr.change_yield thy o ensure_consts_term thy f;
-
-fun intervene thy funcgr = Funcgr.change thy (K funcgr);
+ fst o Funcgr.change_yield thy o raw_eval_term thy f;
end; (*struct*)
--- a/src/Tools/code/code_name.ML Fri Aug 24 14:14:18 2007 +0200
+++ b/src/Tools/code/code_name.ML Fri Aug 24 14:14:20 2007 +0200
@@ -17,18 +17,16 @@
val intro_vars: string list -> var_ctxt -> var_ctxt;
val lookup_var: var_ctxt -> string -> string;
- type tyco = string
- type const = string
val class: theory -> class -> class
val class_rev: theory -> class -> class option
val classrel: theory -> class * class -> string
val classrel_rev: theory -> string -> (class * class) option
- val tyco: theory -> tyco -> tyco
- val tyco_rev: theory -> tyco -> tyco option
- val instance: theory -> class * tyco -> string
- val instance_rev: theory -> string -> (class * tyco) option
- val const: theory -> CodeUnit.const -> const
- val const_rev: theory -> const -> CodeUnit.const option
+ val tyco: theory -> string -> string
+ val tyco_rev: theory -> string -> string option
+ val instance: theory -> class * string -> string
+ val instance_rev: theory -> string -> (class * string) option
+ val const: theory -> string -> string
+ val const_rev: theory -> string -> string option
val labelled_name: theory -> string -> string
val setup: theory -> theory
@@ -186,8 +184,7 @@
#> NameSpace.explode
#> map (purify_name true);
-fun purify_base "op =" = "eq"
- | purify_base "op &" = "and"
+fun purify_base "op &" = "and"
| purify_base "op |" = "or"
| purify_base "op -->" = "implies"
| purify_base "{}" = "empty"
@@ -196,7 +193,9 @@
| purify_base "op Un" = "union"
| purify_base "*" = "product"
| purify_base "+" = "sum"
- | purify_base s = purify_name false s;
+ | purify_base s = if String.isPrefix "op =" s
+ then "eq" ^ purify_name false s
+ else purify_name false s;
fun default_policy thy get_basename get_thyname name =
let
@@ -212,30 +211,28 @@
fun instance_policy thy = default_policy thy (fn (class, tyco) =>
NameSpace.base class ^ "_" ^ NameSpace.base tyco) thyname_of_instance;
-fun force_thyname thy (const as (c, opt_tyco)) =
- case Code.get_datatype_of_constr thy const
- of SOME dtco => SOME (thyname_of_tyco thy dtco)
- | NONE => (case AxClass.class_of_param thy c
- of SOME class => (case opt_tyco
- of SOME tyco => SOME (thyname_of_instance thy (class, tyco))
- | NONE => SOME (thyname_of_class thy class))
- | NONE => NONE);
+fun force_thyname thy c = case Code.get_datatype_of_constr thy c
+ of SOME dtco => SOME (thyname_of_tyco thy dtco)
+ | NONE => (case AxClass.class_of_param thy c
+ of SOME class => SOME (thyname_of_class thy class)
+ | NONE => (case Class.param_const thy c
+ of SOME (c, tyco) => SOME (thyname_of_instance thy
+ ((the o AxClass.class_of_param thy) c, tyco))
+ | NONE => NONE));
-fun const_policy thy (const as (c, opt_tyco)) =
- case force_thyname thy const
+fun const_policy thy c =
+ case force_thyname thy c
of NONE => default_policy thy NameSpace.base thyname_of_const c
| SOME thyname => let
val prefix = purify_prefix thyname;
- val tycos = the_list opt_tyco;
- val base = map (purify_base o NameSpace.base) (c :: tycos);
- in NameSpace.implode (prefix @ [space_implode "_" base]) end;
+ val base = (purify_base o NameSpace.base) c;
+ in NameSpace.implode (prefix @ [base]) end;
(* theory and code data *)
type tyco = string;
type const = string;
-structure Consttab = CodeUnit.Consttab;
structure StringPairTab =
TableFun(
@@ -294,14 +291,14 @@
structure ConstName = CodeDataFun
(
- type T = const Consttab.table * (string * string option) Symtab.table;
- val empty = (Consttab.empty, Symtab.empty);
+ type T = const Symtab.table * string Symtab.table;
+ val empty = (Symtab.empty, Symtab.empty);
fun merge _ ((const1, constrev1), (const2, constrev2)) : T =
- (Consttab.merge (op =) (const1, const2),
- Symtab.merge CodeUnit.eq_const (constrev1, constrev2));
+ (Symtab.merge (op =) (const1, const2),
+ Symtab.merge (op =) (constrev1, constrev2));
fun purge _ NONE _ = empty
- | purge _ (SOME cs) (const, constrev) = (fold Consttab.delete_safe cs const,
- fold Symtab.delete (map_filter (Consttab.lookup const) cs) constrev);
+ | purge _ (SOME cs) (const, constrev) = (fold Symtab.delete_safe cs const,
+ fold Symtab.delete_safe (map_filter (Symtab.lookup const) cs) constrev);
);
val setup = CodeName.init;
@@ -333,10 +330,10 @@
val tabs = ConstName.get thy;
fun declare name =
let
- val names' = (Consttab.update (const, name) (fst tabs),
+ val names' = (Symtab.update (const, name) (fst tabs),
Symtab.update_new (name, const) (snd tabs))
in (ConstName.change thy (K names'); name) end;
- in case Consttab.lookup (fst tabs) const
+ in case Symtab.lookup (fst tabs) const
of SOME name => name
| NONE =>
const
--- a/src/Tools/code/code_package.ML Fri Aug 24 14:14:18 2007 +0200
+++ b/src/Tools/code/code_package.ML Fri Aug 24 14:14:20 2007 +0200
@@ -45,35 +45,25 @@
-> CodeFuncgr.T
-> (string * typ) * term list -> CodeThingol.transact -> iterm * CodeThingol.transact;
-type appgens = (int * (appgen * stamp)) Symtab.table;
-val merge_appgens : appgens * appgens -> appgens =
- Symtab.merge (fn ((bounds1, (_, stamp1)), (bounds2, (_, stamp2))) =>
- bounds1 = bounds2 andalso stamp1 = stamp2);
-
-structure Consttab = CodeUnit.Consttab;
-type abstypes = typ Symtab.table * CodeUnit.const Consttab.table;
-fun merge_abstypes ((typs1, consts1) : abstypes, (typs2, consts2) : abstypes) =
- (Symtab.merge (Type.eq_type Vartab.empty) (typs1, typs2),
- Consttab.merge CodeUnit.eq_const (consts1, consts2));
-
-structure Translation = TheoryDataFun
+structure Appgens = TheoryDataFun
(
- type T = appgens * abstypes;
- val empty = (Symtab.empty, (Symtab.empty, Consttab.empty));
+ type T = (int * (appgen * stamp)) Symtab.table;
+ val empty = Symtab.empty;
val copy = I;
val extend = I;
- fun merge _ ((appgens1, abstypes1), (appgens2, abstypes2)) =
- (merge_appgens (appgens1, appgens2), merge_abstypes (abstypes1, abstypes2));
+ fun merge _ = Symtab.merge (fn ((bounds1, (_, stamp1)), (bounds2, (_, stamp2))) =>
+ bounds1 = bounds2 andalso stamp1 = stamp2);
);
fun code_depgr thy [] = CodeFuncgr.make thy []
| code_depgr thy consts =
let
val gr = CodeFuncgr.make thy consts;
- val select = CodeFuncgr.Constgraph.all_succs gr consts;
+ val select = Graph.all_succs gr consts;
in
- CodeFuncgr.Constgraph.subgraph
- (member CodeUnit.eq_const select) gr
+ gr
+ |> Graph.subgraph (member (op =) select)
+ |> Graph.map_nodes ((apsnd o map) (Conv.fconv_rule (Class.overload thy)))
end;
fun code_thms thy =
@@ -89,7 +79,7 @@
in { name = name, ID = name, dir = "", unfold = true,
path = "", parents = nameparents }
end;
- val prgr = CodeFuncgr.Constgraph.fold ((fn x => fn xs => xs @ [x]) o mk_entry) gr [];
+ val prgr = Graph.fold ((fn x => fn xs => xs @ [x]) o mk_entry) gr [];
in Present.display_graph prgr end;
structure Program = CodeDataFun
@@ -105,7 +95,7 @@
map_filter (CodeName.const_rev thy) (Graph.keys code);
val dels = (Graph.all_preds code
o map (CodeName.const thy)
- o filter (member CodeUnit.eq_const cs_exisiting)
+ o filter (member (op =) cs_exisiting)
) cs;
in Graph.del_nodes dels code end;
);
@@ -113,10 +103,6 @@
(* translation kernel *)
-fun get_abstype thy (tyco, tys) = case Symtab.lookup ((fst o snd o Translation.get) thy) tyco
- of SOME ty => SOME ((map_atyps (fn TFree (n, _) => nth tys (the (Int.fromString n)))) ty)
- | NONE => NONE;
-
val value_name = "Isabelle_Eval.EVAL.EVAL";
fun ensure_def thy = CodeThingol.ensure_def
@@ -128,7 +114,7 @@
val (v, cs) = AxClass.params_of_class thy class;
val class' = CodeName.class thy class;
val classrels' = map (curry (CodeName.classrel thy) class) superclasses;
- val classops' = map (CodeName.const thy o CodeUnit.const_of_cexpr thy) cs;
+ val classops' = map (CodeName.const thy o fst) cs;
val defgen_class =
fold_map (ensure_def_class thy algbr funcgr) superclasses
##>> (fold_map (exprgen_typ thy algbr funcgr) o map snd) cs
@@ -152,9 +138,7 @@
fold_map (exprgen_tyvar_sort thy algbr funcgr) vs
##>> fold_map (fn (c, tys) =>
fold_map (exprgen_typ thy algbr funcgr) tys
- #>> (fn tys' =>
- ((CodeName.const thy o CodeUnit.const_of_cexpr thy)
- (c, tys ---> Type (tyco, map TFree vs)), tys'))) cos
+ #>> (fn tys' => (CodeName.const thy c, tys'))) cos
#>> (fn (vs, cos) => CodeThingol.Datatype (vs, cos))
end;
val tyco' = CodeName.tyco thy tyco;
@@ -171,15 +155,10 @@
|> exprgen_tyvar_sort thy algbr funcgr vs
|>> (fn (v, sort) => ITyVar v)
| exprgen_typ thy algbr funcgr (Type (tyco, tys)) trns =
- case get_abstype thy (tyco, tys)
- of SOME ty =>
- trns
- |> exprgen_typ thy algbr funcgr ty
- | NONE =>
- trns
- |> ensure_def_tyco thy algbr funcgr tyco
- ||>> fold_map (exprgen_typ thy algbr funcgr) tys
- |>> (fn (tyco, tys) => tyco `%% tys);
+ trns
+ |> ensure_def_tyco thy algbr funcgr tyco
+ ||>> fold_map (exprgen_typ thy algbr funcgr) tys
+ |>> (fn (tyco, tys) => tyco `%% tys);
exception CONSTRAIN of (string * typ) * typ;
val timing = ref false;
@@ -216,10 +195,8 @@
end
and exprgen_dict_parms thy (algbr as (_, consts)) funcgr (c, ty_ctxt) =
let
- val c' = CodeUnit.const_of_cexpr thy (c, ty_ctxt)
- val idf = CodeName.const thy c';
- val ty_decl = Consts.the_declaration consts idf;
- val (tys, tys_decl) = pairself (curry (Consts.typargs consts) idf) (ty_ctxt, ty_decl);
+ val ty_decl = Consts.the_declaration consts c;
+ val (tys, tys_decl) = pairself (curry (Consts.typargs consts) c) (ty_ctxt, ty_decl);
val sorts = map (snd o dest_TVar) tys_decl;
in
fold_map (exprgen_dicts thy algbr funcgr) (tys ~~ sorts)
@@ -237,10 +214,11 @@
||>> exprgen_dicts thy algbr funcgr (arity_typ, [superclass])
|>> (fn ((superclass, classrel), [DictConst (inst, dss)]) =>
(superclass, (classrel, (inst, dss))));
- fun gen_classop_def (classop as (c, ty)) trns =
+ fun gen_classop_def (c, ty) trns =
trns
- |> ensure_def_const thy algbr funcgr (CodeUnit.const_of_cexpr thy classop)
- ||>> exprgen_term thy algbr funcgr (Const (c, map_type_tfree (K arity_typ) ty));
+ |> ensure_def_const thy algbr funcgr c
+ ||>> exprgen_term thy algbr funcgr
+ (Const (Class.inst_const thy (c, tyco), map_type_tfree (K arity_typ) ty));
fun defgen_inst trns =
trns
|> ensure_def_class thy algbr funcgr class
@@ -256,13 +234,13 @@
|> ensure_def thy defgen_inst ("generating instance " ^ quote class ^ " / " ^ quote tyco) inst
|> pair inst
end
-and ensure_def_const thy (algbr as (_, consts)) funcgr (const as (c, opt_tyco)) =
+and ensure_def_const thy (algbr as (_, consts)) funcgr c =
let
- val c' = CodeName.const thy const;
+ val c' = CodeName.const thy c;
fun defgen_datatypecons trns =
trns
|> ensure_def_tyco thy algbr funcgr
- ((the o Code.get_datatype_of_constr thy) const)
+ ((the o Code.get_datatype_of_constr thy) c)
|>> (fn _ => CodeThingol.Bot);
fun defgen_classop trns =
trns
@@ -271,15 +249,14 @@
|>> (fn _ => CodeThingol.Bot);
fun defgen_fun trns =
let
- val const' = perhaps (Consttab.lookup ((snd o snd o Translation.get) thy)) const;
- val raw_thms = CodeFuncgr.funcs funcgr const';
- val ty = (Logic.unvarifyT o CodeFuncgr.typ funcgr) const';
+ val raw_thms = CodeFuncgr.funcs funcgr c;
+ val ty = (Logic.unvarifyT o CodeFuncgr.typ funcgr) c;
val thms = if (null o Term.typ_tfrees) ty orelse (null o fst o strip_type) ty
then raw_thms
else map (CodeUnit.expand_eta 1) raw_thms;
- val timeap = if !timing then Output.timeap_msg ("time for " ^ c')
+ val timeap = if !timing then Output.timeap_msg ("time for " ^ c)
else I;
- val vs = (map dest_TFree o Consts.typargs consts) (c', ty);
+ val vs = (map dest_TFree o Consts.typargs consts) (c, ty);
val dest_eqthm =
apfst (snd o strip_comb) o Logic.dest_equals o Logic.unvarify o prop_of;
fun exprgen_eq (args, rhs) =
@@ -292,14 +269,13 @@
||>> timeap (fold_map (exprgen_eq o dest_eqthm) thms)
|>> (fn ((vs, ty), eqs) => CodeThingol.Fun ((vs, ty), eqs))
end;
- val defgen = if (is_some o Code.get_datatype_of_constr thy) const
+ val defgen = if (is_some o Code.get_datatype_of_constr thy) c
then defgen_datatypecons
- else if is_some opt_tyco
- orelse (not o is_some o AxClass.class_of_param thy) c
- then defgen_fun
- else defgen_classop
+ else if (is_some o AxClass.class_of_param thy) c
+ then defgen_classop
+ else defgen_fun
in
- ensure_def thy defgen ("generating constant " ^ CodeUnit.string_of_const thy const) c'
+ ensure_def thy defgen ("generating constant " ^ CodeUnit.string_of_const thy c) c'
#> pair c'
end
and exprgen_term thy algbr funcgr (Const (c, ty)) trns =
@@ -330,14 +306,14 @@
|>> (fn (t, ts) => t `$$ ts)
and appgen_default thy algbr funcgr ((c, ty), ts) trns =
trns
- |> ensure_def_const thy algbr funcgr (CodeUnit.const_of_cexpr thy (c, ty))
+ |> ensure_def_const thy algbr funcgr c
||>> fold_map (exprgen_typ thy algbr funcgr) ((fst o Term.strip_type) ty)
||>> exprgen_typ thy algbr funcgr ((snd o Term.strip_type) ty)
||>> exprgen_dict_parms thy algbr funcgr (c, ty)
||>> fold_map (exprgen_term thy algbr funcgr) ts
|>> (fn ((((c, tys), ty), iss), ts) => IConst (c, (iss, tys)) `$$ ts)
and select_appgen thy algbr funcgr ((c, ty), ts) trns =
- case Symtab.lookup (fst (Translation.get thy)) c
+ case Symtab.lookup (Appgens.get thy) c
of SOME (i, (appgen, _)) =>
if length ts < i then
let
@@ -396,7 +372,9 @@
let
val SOME ([], ((st, sty), ds)) = dest_case_expr thy (list_comb (Const c_ty, ts));
fun clause_gen (dt, bt) =
- exprgen_term thy algbr funcgr dt
+ exprgen_term thy algbr funcgr
+ (map_aterms (fn Const (c_ty as (c, ty)) => Const
+ (Class.unoverload_const thy c_ty, ty) | t => t) dt)
##>> exprgen_term thy algbr funcgr bt;
in
exprgen_term thy algbr funcgr st
@@ -429,107 +407,25 @@
val i = (length o fst o strip_type o Sign.the_const_type thy) c;
val _ = Program.change thy (K CodeThingol.empty_code);
in
- (Translation.map o apfst)
- (Symtab.update (c, (i, (appgen, stamp ())))) thy
+ Appgens.map (Symtab.update (c, (i, (appgen, stamp ())))) thy
end;
-
-(** abstype and constsubst interface **)
-
-local
-
-fun add_consts thy f (c1, c2 as (c, opt_tyco)) =
- let
- val _ = if
- is_some (AxClass.class_of_param thy c) andalso is_none opt_tyco
- orelse is_some (Code.get_datatype_of_constr thy c2)
- then error ("Not a function: " ^ CodeUnit.string_of_const thy c2)
- else ();
- val funcgr = CodeFuncgr.make thy [c1, c2];
- val ty1 = (f o CodeFuncgr.typ funcgr) c1;
- val ty2 = CodeFuncgr.typ funcgr c2;
- val _ = if Sign.typ_equiv thy (ty1, ty2) then () else
- error ("Incompatiable type signatures of " ^ CodeUnit.string_of_const thy c1
- ^ " and " ^ CodeUnit.string_of_const thy c2 ^ ":\n"
- ^ CodeUnit.string_of_typ thy ty1 ^ "\n" ^ CodeUnit.string_of_typ thy ty2);
- in Consttab.update (c1, c2) end;
-
-fun gen_abstyp prep_const prep_typ (raw_abstyp, raw_substtyp) raw_absconsts thy =
- let
- val abstyp = Type.no_tvars (prep_typ thy raw_abstyp);
- val substtyp = Type.no_tvars (prep_typ thy raw_substtyp);
- val absconsts = (map o pairself) (prep_const thy) raw_absconsts;
- val Type (abstyco, tys) = abstyp handle BIND => error ("Bad type: " ^ Sign.string_of_typ thy abstyp);
- val typarms = map (fst o dest_TFree) tys handle MATCH => error ("Bad type: " ^ Sign.string_of_typ thy abstyp);
- fun mk_index v =
- let
- val k = find_index (fn w => v = w) typarms;
- in if k = ~1
- then error ("Free type variable: " ^ quote v)
- else TFree (string_of_int k, [])
- end;
- val typpat = map_atyps (fn TFree (v, _) => mk_index v) substtyp;
- fun apply_typpat (Type (tyco, tys)) =
- let
- val tys' = map apply_typpat tys;
- in if tyco = abstyco then
- (map_atyps (fn TFree (n, _) => nth tys' (the (Int.fromString n)))) typpat
- else
- Type (tyco, tys')
- end
- | apply_typpat ty = ty;
- val _ = Program.change thy (K CodeThingol.empty_code);
- in
- thy
- |> (Translation.map o apsnd) (fn (abstypes, abscs) =>
- (abstypes
- |> Symtab.update (abstyco, typpat),
- abscs
- |> fold (add_consts thy apply_typpat) absconsts)
- )
- end;
-
-fun gen_constsubst prep_const raw_constsubsts thy =
- let
- val constsubsts = (map o pairself) (prep_const thy) raw_constsubsts;
- val _ = Program.change thy (K CodeThingol.empty_code);
- in
- thy
- |> (Translation.map o apsnd o apsnd) (fold (add_consts thy I) constsubsts)
- end;
-
-in
-
-val abstyp = gen_abstyp (K I) Sign.certify_typ;
-val abstyp_e = gen_abstyp CodeUnit.read_const Sign.read_typ;
-
-val constsubst = gen_constsubst (K I);
-val constsubst_e = gen_constsubst CodeUnit.read_const;
-
-end; (*local*)
-
-
(** code generation interfaces **)
(* generic generation combinators *)
fun generate thy funcgr gen it =
let
- (*FIXME*)
- val _ = CodeFuncgr.intervene thy funcgr;
- val cs = map_filter (Consttab.lookup ((snd o snd o Translation.get) thy))
- (CodeFuncgr.all funcgr);
- val CodeFuncgr' = CodeFuncgr.make thy cs;
val naming = NameSpace.qualified_names NameSpace.default_naming;
val consttab = Consts.empty
|> fold (fn c => Consts.declare naming
- ((CodeName.const thy c, CodeFuncgr.typ CodeFuncgr' c), true))
- (CodeFuncgr.all CodeFuncgr');
+ ((c, CodeFuncgr.typ funcgr c), true))
+ (CodeFuncgr.all funcgr);
val algbr = (Code.operational_algebra thy, consttab);
in
Program.change_yield thy
- (CodeThingol.start_transact (gen thy algbr CodeFuncgr' it))
+ (CodeThingol.start_transact (gen thy algbr funcgr it))
|> fst
end;
@@ -630,8 +526,7 @@
val _ = OuterSyntax.add_keywords [inK, module_nameK, fileK];
-val (codeK, code_abstypeK, code_axiomsK, code_thmsK, code_depsK) =
- ("export_code", "code_abstype", "code_axioms", "code_thms", "code_deps");
+val (codeK, code_thmsK, code_depsK) = ("export_code", "code_thms", "code_deps");
in
@@ -644,19 +539,6 @@
of SOME f => (writeln "Now generating code..."; f thy)
| NONE => error ("Bad directive " ^ quote cmd);
-val code_abstypeP =
- OuterSyntax.command code_abstypeK "axiomatic abstypes for code generation" K.thy_decl (
- (P.typ -- P.typ -- Scan.optional (P.$$$ "where" |-- Scan.repeat1
- (P.term --| (P.$$$ "\\<equiv>" || P.$$$ "==") -- P.term)) [])
- >> (Toplevel.theory o uncurry abstyp_e)
- );
-
-val code_axiomsP =
- OuterSyntax.command code_axiomsK "axiomatic constant equalities for code generation" K.thy_decl (
- Scan.repeat1 (P.term --| (P.$$$ "\\<equiv>" || P.$$$ "==") -- P.term)
- >> (Toplevel.theory o constsubst_e)
- );
-
val code_thmsP =
OuterSyntax.improper_command code_thmsK "print system of defining equations for code" OuterKeyword.diag
(Scan.repeat P.term
@@ -669,7 +551,7 @@
>> (fn cs => Toplevel.no_timing o Toplevel.unknown_theory
o Toplevel.keep ((fn thy => code_deps_cmd thy cs) o Toplevel.theory_of)));
-val _ = OuterSyntax.add_parsers [codeP, code_abstypeP, code_axiomsP, code_thmsP, code_depsP];
+val _ = OuterSyntax.add_parsers [codeP, code_thmsP, code_depsP];
end; (* local *)
--- a/src/Tools/code/code_target.ML Fri Aug 24 14:14:18 2007 +0200
+++ b/src/Tools/code/code_target.ML Fri Aug 24 14:14:20 2007 +0200
@@ -11,7 +11,7 @@
include BASIC_CODE_THINGOL;
val add_syntax_class: string -> class
- -> (string * (CodeUnit.const * string) list) option -> theory -> theory;
+ -> (string * (string * string) list) option -> theory -> theory;
val add_syntax_inst: string -> string * class -> bool -> theory -> theory;
val add_syntax_tycoP: string -> string -> OuterParse.token list
-> (theory -> theory) * OuterParse.token list;
@@ -23,7 +23,7 @@
val add_pretty_list_string: string -> string -> string
-> string -> string list -> theory -> theory;
val add_pretty_char: string -> string -> string list -> theory -> theory
- val add_pretty_numeral: string -> bool -> string * typ -> string -> string -> string
+ val add_pretty_numeral: string -> bool -> string -> string -> string -> string
-> string -> string -> theory -> theory;
val add_pretty_ml_string: string -> string -> string list -> string
-> string -> string -> theory -> theory;
@@ -1410,7 +1410,7 @@
|> distinct (op =)
|> remove (op =) modlname';
val qualified =
- imports
+ imports @ map fst defs
|> map_filter (try deresolv)
|> map NameSpace.base
|> has_duplicates (op =);
@@ -1793,8 +1793,8 @@
let
val cls = prep_class thy raw_class;
val class = CodeName.class thy cls;
- fun mk_classop (const as (c, _)) = case AxClass.class_of_param thy c
- of SOME class' => if cls = class' then CodeName.const thy const
+ fun mk_classop c = case AxClass.class_of_param thy c
+ of SOME class' => if cls = class' then CodeName.const thy c
else error ("Not a class operation for class " ^ quote class ^ ": " ^ quote c)
| NONE => error ("Not a class operation: " ^ quote c);
fun mk_syntax_ops raw_ops = AList.lookup (op =)
@@ -1845,8 +1845,8 @@
let
val c = prep_const thy raw_c;
val c' = CodeName.const thy c;
- fun check_args (syntax as (n, _)) = if n > (length o fst o strip_type o Sign.the_const_type thy o fst) c
- then error ("Too many arguments in syntax for constant " ^ (quote o fst) c)
+ fun check_args (syntax as (n, _)) = if n > CodeUnit.no_args thy c
+ then error ("Too many arguments in syntax for constant " ^ quote c)
else syntax;
in case raw_syn
of SOME syntax =>
@@ -1883,12 +1883,6 @@
else error ("No such type constructor: " ^ quote raw_tyco);
in tyco end;
-fun idfs_of_const thy c =
- let
- val c' = (c, Sign.the_const_type thy c);
- val c'' = CodeUnit.const_of_cexpr thy c';
- in (c'', CodeName.const thy c'') end;
-
fun no_bindings x = (Option.map o apsnd)
(fn pretty => fn pr => fn vars => pretty (pr vars)) x;
@@ -1974,79 +1968,75 @@
fun add_undefined target undef target_undefined thy =
let
- val (undef', _) = idfs_of_const thy undef;
fun pr _ _ _ _ = str target_undefined;
in
thy
- |> add_syntax_const target undef' (SOME (~1, pr))
+ |> add_syntax_const target undef (SOME (~1, pr))
end;
fun add_pretty_list target nill cons thy =
let
- val (_, nil'') = idfs_of_const thy nill;
- val (cons', cons'') = idfs_of_const thy cons;
- val pr = pretty_list nil'' cons'' target;
+ val nil' = CodeName.const thy nill;
+ val cons' = CodeName.const thy cons;
+ val pr = pretty_list nil' cons' target;
in
thy
- |> add_syntax_const target cons' (SOME pr)
+ |> add_syntax_const target cons (SOME pr)
end;
fun add_pretty_list_string target nill cons charr nibbles thy =
let
- val (_, nil'') = idfs_of_const thy nill;
- val (cons', cons'') = idfs_of_const thy cons;
- val (_, charr'') = idfs_of_const thy charr;
- val (_, nibbles'') = split_list (map (idfs_of_const thy) nibbles);
- val pr = pretty_list_string nil'' cons'' charr'' nibbles'' target;
+ val nil' = CodeName.const thy nill;
+ val cons' = CodeName.const thy cons;
+ val charr' = CodeName.const thy charr;
+ val nibbles' = map (CodeName.const thy) nibbles;
+ val pr = pretty_list_string nil' cons' charr' nibbles' target;
in
thy
- |> add_syntax_const target cons' (SOME pr)
+ |> add_syntax_const target cons (SOME pr)
end;
fun add_pretty_char target charr nibbles thy =
let
- val (charr', charr'') = idfs_of_const thy charr;
- val (_, nibbles'') = split_list (map (idfs_of_const thy) nibbles);
- val pr = pretty_char charr'' nibbles'' target;
+ val charr' = CodeName.const thy charr;
+ val nibbles' = map (CodeName.const thy) nibbles;
+ val pr = pretty_char charr' nibbles' target;
in
thy
- |> add_syntax_const target charr' (SOME pr)
+ |> add_syntax_const target charr (SOME pr)
end;
fun add_pretty_numeral target unbounded number_of b0 b1 pls min bit thy =
let
- val number_of' = CodeUnit.const_of_cexpr thy number_of;
- val (_, b0'') = idfs_of_const thy b0;
- val (_, b1'') = idfs_of_const thy b1;
- val (_, pls'') = idfs_of_const thy pls;
- val (_, min'') = idfs_of_const thy min;
- val (_, bit'') = idfs_of_const thy bit;
- val pr = pretty_numeral unbounded b0'' b1'' pls'' min'' bit'' target;
+ val b0' = CodeName.const thy b0;
+ val b1' = CodeName.const thy b1;
+ val pls' = CodeName.const thy pls;
+ val min' = CodeName.const thy min;
+ val bit' = CodeName.const thy bit;
+ val pr = pretty_numeral unbounded b0' b1' pls' min' bit' target;
in
thy
- |> add_syntax_const target number_of' (SOME pr)
+ |> add_syntax_const target number_of (SOME pr)
end;
fun add_pretty_ml_string target charr nibbles nill cons str thy =
let
- val (_, charr'') = idfs_of_const thy charr;
- val (_, nibbles'') = split_list (map (idfs_of_const thy) nibbles);
- val (_, nil'') = idfs_of_const thy nill;
- val (_, cons'') = idfs_of_const thy cons;
- val (str', _) = idfs_of_const thy str;
- val pr = pretty_ml_string charr'' nibbles'' nil'' cons'' target;
+ val charr' = CodeName.const thy charr;
+ val nibbles' = map (CodeName.const thy) nibbles;
+ val nil' = CodeName.const thy nill;
+ val cons' = CodeName.const thy cons;
+ val pr = pretty_ml_string charr' nibbles' nil' cons' target;
in
thy
- |> add_syntax_const target str' (SOME pr)
+ |> add_syntax_const target str (SOME pr)
end;
fun add_pretty_imperative_monad_bind target bind thy =
let
- val (bind', _) = idfs_of_const thy bind;
val pr = pretty_imperative_monad_bind
in
thy
- |> add_syntax_const target bind' (SOME pr)
+ |> add_syntax_const target bind (SOME pr)
end;
val add_haskell_monad = gen_add_haskell_monad CodeUnit.read_const;
--- a/src/Tools/nbe.ML Fri Aug 24 14:14:18 2007 +0200
+++ b/src/Tools/nbe.ML Fri Aug 24 14:14:20 2007 +0200
@@ -25,7 +25,7 @@
val app: Univ -> Univ -> Univ (*explicit application*)
val univs_ref: Univ list ref
- val lookup_fun: CodeName.const -> Univ
+ val lookup_fun: string -> Univ
val normalization_conv: cterm -> thm
@@ -295,8 +295,8 @@
#>> (fn ts' => list_comb (t, rev ts'))
and of_univ bounds (Const (name, ts)) typidx =
let
- val SOME (const as (c, _)) = CodeName.const_rev thy name;
- val T = Code.default_typ thy const;
+ val SOME c = CodeName.const_rev thy name;
+ val T = Code.default_typ thy c;
val T' = map_type_tvar (fn ((v, i), S) => TypeInfer.param (typidx + i) (v, S)) T;
val typidx' = typidx + maxidx_of_typ T' + 1;
in of_apps bounds (Term.Const (c, T'), ts) typidx' end