# HG changeset patch # User haftmann # Date 1187957660 -7200 # Node ID ae9cd0e9242351579dce4d6690f012e8c2acf5f7 # Parent c0b5ff9e9e4dea813ed1319424cab92ef76f91cc overloaded definitions accompanied by explicit constants diff -r c0b5ff9e9e4d -r ae9cd0e92423 src/HOL/Complex/ex/ReflectedFerrack.thy --- 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 diff -r c0b5ff9e9e4d -r ae9cd0e92423 src/HOL/Complex/ex/linreif.ML --- 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!"; diff -r c0b5ff9e9e4d -r ae9cd0e92423 src/HOL/Complex/ex/mireif.ML --- 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 *) diff -r c0b5ff9e9e4d -r ae9cd0e92423 src/HOL/Lambda/WeakNorm.thy --- 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 diff -r c0b5ff9e9e4d -r ae9cd0e92423 src/HOL/Library/Efficient_Nat.thy --- 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 \ 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") diff -r c0b5ff9e9e4d -r ae9cd0e92423 src/HOL/Library/Eval.thy --- 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; diff -r c0b5ff9e9e4d -r ae9cd0e92423 src/HOL/Library/Executable_Set.thy --- 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 \ A \ B \ B \ A" by blast -lemma [code func]: - "(A\'a\eq set) = B \ A \ B \ B \ A" - by blast - -lemma [code func]: - "(A\'a\eq set) \ B \ (\x\A. x \ B)" - unfolding subset_def .. - -lemma [code func]: - "(A\'a\eq set) \ B \ A \ B \ A \ B" - by blast - lemma [code]: "a \ A \ (\x\A. x = a)" unfolding bex_triv_one_point1 .. @@ -37,8 +23,6 @@ filter_set :: "('a \ bool) \ 'a set \ 'a set" where "filter_set P xs = {x\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 \ 'a\eq) = insert x" .. - -lemma [code func]: - "(xs \ 'a\eq set) \ ys = xs \ ys" .. - -lemma [code func]: - "(xs \ 'a\eq set) \ ys = xs \ ys" .. - -lemma [code func]: - "(op -) (xs \ 'a\eq set) = (op -) (xs \ 'a\eq set)" .. - -lemma [code func]: - "image (f \ 'a \ 'b\eq) = image f" .. - -lemma [code func]: - "Union (xss \ 'a\eq set set) = Union xss" .. - -lemma [code func]: - "Inter (xss \ 'a\eq set set) = Inter xss" .. - -lemma [code func]: - "UNION xs (f \ 'a \ 'b\eq set) = UNION xs f" .. - -lemma [code func]: - "INTER xs (f \ 'a \ 'b\eq set) = INTER xs f" .. - -lemma [code func]: - "Ball (xs \ 'a\type set) = Ball xs" .. - -lemma [code func]: - "Bex (xs \ 'a\type set) = Bex xs" .. - -lemma [code func]: - "filter_set P (xs \ 'a\type set) = filter_set P xs" .. - - -code_abstype "'a set" "'a list" where - "{}" \ empty_list - insert \ insertl - "op \" \ unionl - "op \" \ intersect - "op - \ 'a set \ 'a set \ 'a set" \ subtract' - image \ map_distinct - Union \ unions - Inter \ intersects - UNION \ map_union - INTER \ map_inter - Ball \ Blall - Bex \ Blex - filter_set \ filter - - subsubsection {* type serializations *} types_code diff -r c0b5ff9e9e4d -r ae9cd0e92423 src/HOL/Library/Graphs.thy --- 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 *} diff -r c0b5ff9e9e4d -r ae9cd0e92423 src/HOL/Library/ML_Int.thy --- 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 \ 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} diff -r c0b5ff9e9e4d -r ae9cd0e92423 src/HOL/Library/Pretty_Int.thy --- 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 \ 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} diff -r c0b5ff9e9e4d -r ae9cd0e92423 src/HOL/Library/SCT_Implementation.thy --- 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 \ 'e \ 'n) \ ('n \ 'e \ 'n) \ bool" diff -r c0b5ff9e9e4d -r ae9cd0e92423 src/HOL/Tools/datatype_abs_proofs.ML --- 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') = diff -r c0b5ff9e9e4d -r ae9cd0e92423 src/HOL/Tools/datatype_codegen.ML --- 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; diff -r c0b5ff9e9e4d -r ae9cd0e92423 src/HOL/Tools/datatype_package.ML --- 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 diff -r c0b5ff9e9e4d -r ae9cd0e92423 src/HOL/ex/Classpackage.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 - diff -r c0b5ff9e9e4d -r ae9cd0e92423 src/HOL/ex/Codegenerator.thy --- 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 - diff -r c0b5ff9e9e4d -r ae9cd0e92423 src/HOL/ex/Eval_Examples.thy --- 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\int) \ 12" +value (overloaded) "[]::nat list" value (overloaded) "[(nat 100, ())]" -value (overloaded) "[]::nat list" text {* a fancy datatype *} diff -r c0b5ff9e9e4d -r ae9cd0e92423 src/HOL/ex/ExecutableContent.thy --- 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 diff -r c0b5ff9e9e4d -r ae9cd0e92423 src/HOL/ex/coopereif.ML --- 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 *) diff -r c0b5ff9e9e4d -r ae9cd0e92423 src/Pure/Isar/ROOT.ML --- 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"; diff -r c0b5ff9e9e4d -r ae9cd0e92423 src/Pure/Isar/class.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*) diff -r c0b5ff9e9e4d -r ae9cd0e92423 src/Pure/Isar/code.ML --- 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*) diff -r c0b5ff9e9e4d -r ae9cd0e92423 src/Pure/Isar/code_unit.ML --- 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 *) diff -r c0b5ff9e9e4d -r ae9cd0e92423 src/Pure/Isar/isar_syn.ML --- 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.$$$ "\\" || 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)); diff -r c0b5ff9e9e4d -r ae9cd0e92423 src/Tools/code/code_funcgr.ML --- 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*) diff -r c0b5ff9e9e4d -r ae9cd0e92423 src/Tools/code/code_name.ML --- 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 diff -r c0b5ff9e9e4d -r ae9cd0e92423 src/Tools/code/code_package.ML --- 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.$$$ "\\" || 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.$$$ "\\" || 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 *) diff -r c0b5ff9e9e4d -r ae9cd0e92423 src/Tools/code/code_target.ML --- 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; diff -r c0b5ff9e9e4d -r ae9cd0e92423 src/Tools/nbe.ML --- 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