# HG changeset patch # User haftmann # Date 1177060895 -7200 # Node ID d87ccbcc270249c20182845434c9f548ca33983a # Parent 4948e2bd67e5a5326cd88d7c102909d966dd7c36 tuned diff -r 4948e2bd67e5 -r d87ccbcc2702 src/HOL/Extraction/Pigeonhole.thy --- a/src/HOL/Extraction/Pigeonhole.thy Fri Apr 20 11:21:34 2007 +0200 +++ b/src/HOL/Extraction/Pigeonhole.thy Fri Apr 20 11:21:35 2007 +0200 @@ -5,7 +5,9 @@ header {* The pigeonhole principle *} -theory Pigeonhole imports EfficientNat begin +theory Pigeonhole +imports EfficientNat +begin text {* We formalize two proofs of the pigeonhole principle, which lead diff -r 4948e2bd67e5 -r d87ccbcc2702 src/HOL/Lattices.thy --- a/src/HOL/Lattices.thy Fri Apr 20 11:21:34 2007 +0200 +++ b/src/HOL/Lattices.thy Fri Apr 20 11:21:35 2007 +0200 @@ -13,18 +13,20 @@ text{* This theory of lattices only defines binary sup and inf - operations. The extension to (finite) sets is done in theories @{text FixedPoint} - and @{text Finite_Set}. + operations. The extension to (finite) sets is done in theories + @{text FixedPoint} and @{text Finite_Set}. *} class lower_semilattice = order + fixes inf :: "'a \ 'a \ 'a" (infixl "\" 70) - assumes inf_le1 [simp]: "x \ y \ x" and inf_le2 [simp]: "x \ y \ y" + assumes inf_le1 [simp]: "x \ y \ x" + and inf_le2 [simp]: "x \ y \ y" and inf_greatest: "x \ y \ x \ z \ x \ y \ z" class upper_semilattice = order + fixes sup :: "'a \ 'a \ 'a" (infixl "\" 65) - assumes sup_ge1 [simp]: "x \ x \ y" and sup_ge2 [simp]: "y \ x \ y" + assumes sup_ge1 [simp]: "x \ x \ y" + and sup_ge2 [simp]: "y \ x \ y" and sup_least: "y \ x \ z \ x \ y \ z \ x" class lattice = lower_semilattice + upper_semilattice @@ -251,28 +253,28 @@ subsection {* Uniqueness of inf and sup *} -lemma inf_unique: +lemma (in lower_semilattice) inf_unique: fixes f (infixl "\" 70) - assumes le1: "\x y. x \ y \ x" and le2: "\x y. x \ y \ y" - and greatest: "\x y z. x \ y \ x \ z \ x \ y \ z" - shows "inf x y = f x y" + assumes le1: "\x y. x \ y \<^loc>\ x" and le2: "\x y. x \ y \<^loc>\ y" + and greatest: "\x y z. x \<^loc>\ y \ x \<^loc>\ z \ x \<^loc>\ y \ z" + shows "x \ y = x \ y" proof (rule antisym) - show "x \ y \ inf x y" by (rule le_infI) (rule le1 le2) + show "x \ y \<^loc>\ x \ y" by (rule le_infI) (rule le1 le2) next - have leI: "\x y z. x \ y \ x \ z \ x \ y \ z" by (blast intro: greatest) - show "inf x y \ x \ y" by (rule leI) simp_all + have leI: "\x y z. x \<^loc>\ y \ x \<^loc>\ z \ x \<^loc>\ y \ z" by (blast intro: greatest) + show "x \ y \<^loc>\ x \ y" by (rule leI) simp_all qed -lemma sup_unique: +lemma (in upper_semilattice) sup_unique: fixes f (infixl "\" 70) - assumes ge1 [simp]: "\x y. x \ x \ y" and ge2: "\x y. y \ x \ y" - and least: "\x y z. y \ x \ z \ x \ y \ z \ x" - shows "sup x y = f x y" + assumes ge1 [simp]: "\x y. x \<^loc>\ x \ y" and ge2: "\x y. y \<^loc>\ x \ y" + and least: "\x y z. y \<^loc>\ x \ z \<^loc>\ x \ y \ z \<^loc>\ x" + shows "x \ y = x \ y" proof (rule antisym) - show "sup x y \ x \ y" by (rule le_supI) (rule ge1 ge2) + show "x \ y \<^loc>\ x \ y" by (rule le_supI) (rule ge1 ge2) next - have leI: "\x y z. x \ z \ y \ z \ x \ y \ z" by (blast intro: least) - show "x \ y \ sup x y" by (rule leI) simp_all + have leI: "\x y z. x \<^loc>\ z \ y \<^loc>\ z \ x \ y \<^loc>\ z" by (blast intro: least) + show "x \ y \<^loc>\ x \ y" by (rule leI) simp_all qed diff -r 4948e2bd67e5 -r d87ccbcc2702 src/HOL/Relation_Power.thy --- a/src/HOL/Relation_Power.thy Fri Apr 20 11:21:34 2007 +0200 +++ b/src/HOL/Relation_Power.thy Fri Apr 20 11:21:35 2007 +0200 @@ -40,7 +40,8 @@ *} definition - funpow :: "nat \ ('a \ 'a) \ 'a \ 'a" where + funpow :: "nat \ ('a \ 'a) \ 'a \ 'a" +where funpow_def: "funpow n f = f ^ n" lemmas [code inline] = funpow_def [symmetric] diff -r 4948e2bd67e5 -r d87ccbcc2702 src/HOL/ex/Records.thy --- a/src/HOL/ex/Records.thy Fri Apr 20 11:21:34 2007 +0200 +++ b/src/HOL/ex/Records.thy Fri Apr 20 11:21:35 2007 +0200 @@ -35,17 +35,21 @@ 'a point_scheme = \xpos :: nat, ypos :: nat, ... :: 'a\ = 'a point_ext_type"} *} -consts foo1 :: point consts foo2 :: "(| xpos :: nat, ypos :: nat |)" -consts foo3 :: "'a => 'a point_scheme" consts foo4 :: "'a => (| xpos :: nat, ypos :: nat, ... :: 'a |)" subsubsection {* Introducing concrete records and record schemes *} -defs - foo1_def: "foo1 == (| xpos = 1, ypos = 0 |)" - foo3_def: "foo3 ext == (| xpos = 1, ypos = 0, ... = ext |)" +definition + foo1 :: point +where + foo1_def: "foo1 = (| xpos = 1, ypos = 0 |)" + +definition + foo3 :: "'a => 'a point_scheme" +where + foo3_def: "foo3 ext = (| xpos = 1, ypos = 0, ... = ext |)" subsubsection {* Record selection and record update *} diff -r 4948e2bd67e5 -r d87ccbcc2702 src/Pure/Tools/class_package.ML --- a/src/Pure/Tools/class_package.ML Fri Apr 20 11:21:34 2007 +0200 +++ b/src/Pure/Tools/class_package.ML Fri Apr 20 11:21:35 2007 +0200 @@ -9,6 +9,8 @@ sig val fork_mixfix: bool -> string option -> mixfix -> mixfix * mixfix + val axclass_cmd: bstring * xstring list + -> ((bstring * Attrib.src list) * string list) list -> theory -> class * theory val class: bstring -> class list -> Element.context_i Locale.element list -> string list -> theory -> string * Proof.context val class_cmd: bstring -> string list -> Element.context Locale.element list @@ -45,10 +47,21 @@ fun fork_mixfix is_loc some_class mx = let val mx' = Syntax.unlocalize_mixfix mx; - val mx_global = if is_some some_class orelse (is_loc andalso mx = mx') then NoSyn else mx'; + val mx_global = if is_some some_class orelse (is_loc andalso mx = mx') + then NoSyn else mx'; val mx_local = if is_loc then mx else NoSyn; in (mx_global, mx_local) end; +fun axclass_cmd (class, raw_superclasses) raw_specs thy = + let + val ctxt = ProofContext.init thy; + val superclasses = map (Sign.read_class thy) raw_superclasses; + val name_atts = map ((apsnd o map) (Attrib.attribute thy) o fst) raw_specs; + val axiomss = ProofContext.read_propp (ctxt, map (map (rpair []) o snd) raw_specs) + |> snd + |> (map o map) fst; + in AxClass.define_class (class, superclasses) [] (name_atts ~~ axiomss) thy end; + (** AxClasses with implicit parameter handling **) @@ -95,7 +108,7 @@ thy |> fold_map add_const consts |-> (fn cs => mk_axioms cs - #-> (fn axioms_prop => AxClass.define_class_i (name, superclasses) (map fst cs @ other_consts) axioms_prop + #-> (fn axioms_prop => AxClass.define_class (name, superclasses) (map fst cs @ other_consts) axioms_prop #-> (fn class => `(fn thy => AxClass.get_definition thy class) #-> (fn {intro, axioms, ...} => fold (add_constraint class) cs #> pair (class, ((intro, (map Thm.prop_of axioms, axioms)), cs)))))) @@ -177,14 +190,15 @@ thy |> PureThy.add_defs_i true (map ((apsnd o map) (Attrib.attribute thy) o snd) defs) |-> (fn thms => pair (map fst defs ~~ thms)); - fun after_qed cs thy = + fun after_qed cs defs thy = thy - |> fold Sign.add_const_constraint_i (map (apsnd SOME) cs); + |> fold Sign.add_const_constraint_i (map (apsnd SOME) cs) + |> fold (CodegenData.add_func false o snd) defs; in theory |> fold_map get_remove_contraint (map fst cs |> distinct (op =)) ||>> add_defs defs - |-> (fn (cs, _) => do_proof (after_qed cs) arities) + |-> (fn (cs, defs) => do_proof (after_qed cs defs) arities) end; fun instance_arity_e' do_proof = gen_instance_arity Sign.read_arity read_def_cmd do_proof; @@ -343,20 +357,6 @@ (* tactics and methods *) -(*FIXME adjust these when minimal intro rules are at hand*) -fun intro_classes_tac' facts st = - let - val thy = Thm.theory_of_thm st; - val ctxt = ProofContext.init thy; - val intro_classes_tac = ALLGOALS - (Method.insert_tac facts THEN' REPEAT_ALL_NEW (resolve_tac (AxClass.class_intros thy))) - THEN Tactic.distinct_subgoals_tac; - val intro_locales_tac = SOMEGOAL (SELECT_GOAL (Locale.intro_locales_tac true ctxt facts)) - THEN Tactic.distinct_subgoals_tac; - in - (intro_classes_tac THEN REPEAT (intro_locales_tac ORELSE intro_locales_tac)) st - end; - fun intro_classes_tac facts st = let val thy = Thm.theory_of_thm st; @@ -381,9 +381,7 @@ default_intro_classes_tac facts; val _ = Context.add_setup (Method.add_methods - [("intro_classes2", Method.no_args (Method.METHOD intro_classes_tac'), - "back-chain introduction rules of classes"), - ("intro_classes", Method.no_args (Method.METHOD intro_classes_tac), + [("intro_classes", Method.no_args (Method.METHOD intro_classes_tac), "back-chain introduction rules of classes"), ("default", Method.thms_ctxt_args (Method.METHOD oo default_tac), "apply some intro/elim rule")]); @@ -481,6 +479,14 @@ local +fun read_param thy raw_t = + let + val t = Sign.read_term thy raw_t + in case try dest_Const t + of SOME (c, _) => c + | NONE => error ("Not a constant: " ^ Sign.string_of_term thy t) + end; + fun gen_class add_locale prep_class prep_param bname raw_supclasses raw_elems raw_other_consts thy = let @@ -573,7 +579,7 @@ in -val class_cmd = gen_class Locale.add_locale Sign.intern_class AxClass.read_param; +val class_cmd = gen_class Locale.add_locale Sign.intern_class read_param; val class = gen_class Locale.add_locale_i Sign.certify_class (K I); end; (*local*) @@ -643,7 +649,7 @@ thy |> PureThy.add_defs_i false [((name, prop), map (Attrib.attribute thy) atts)] |>> the_single; - val _ = warning "------ DEF ------"; + (*val _ = warning "------ DEF ------"; val _ = warning c; val _ = warning name; val _ = (warning o Sign.string_of_term thy) rhs'; @@ -658,14 +664,14 @@ val _ = map print_witness witness; val _ = (warning o string_of_thm) eq'; val eq'' = Element.satisfy_thm witness eq'; - val _ = (warning o string_of_thm) eq''; + val _ = (warning o string_of_thm) eq'';*) in thy - |> Sign.add_path prfx + (* |> Sign.add_path prfx |> add_const (c, ty, syn') |-> (fn c => add_def ((name, atts), Logic.mk_equals (Const c, rhs'))) |-> (fn global_def_thm => tap (fn _ => (warning o string_of_thm) global_def_thm)) - |> Sign.restore_naming thy + |> Sign.restore_naming thy *) end; end; diff -r 4948e2bd67e5 -r d87ccbcc2702 src/Pure/Tools/codegen_consts.ML --- a/src/Pure/Tools/codegen_consts.ML Fri Apr 20 11:21:34 2007 +0200 +++ b/src/Pure/Tools/codegen_consts.ML Fri Apr 20 11:21:35 2007 +0200 @@ -16,6 +16,8 @@ val string_of_typ: theory -> typ -> string val string_of_const: theory -> const -> string val read_const: theory -> string -> const + val read_const_exprs: theory -> (const list -> const list) + -> string list -> const list val co_of_const: theory -> const -> string * ((string * sort) list * (string * typ list)) @@ -68,7 +70,7 @@ ^ " " ^ enclose "[" "]" (Sign.extern_type thy tyco); -(* reading constants as terms *) +(* reading constants as terms and wildcards pattern *) fun read_const thy raw_t = let @@ -78,6 +80,47 @@ | NONE => error ("Not a constant: " ^ Sign.string_of_term thy t) end; +local + +fun consts_of thy some_thyname = + let + 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) = + 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 + end; + +fun read_const_expr thy "*" = ([], consts_of thy NONE) + | read_const_expr thy s = if String.isSuffix ".*" s + then ([], consts_of thy (SOME (unsuffix ".*" s))) + else ([read_const thy s], []); + +in + +fun read_const_exprs thy select = + (op @) o apsnd select o pairself flat o split_list o map (read_const_expr thy); + +end; (*local*) (* conversion between constants, constant expressions and datatype constructors *) diff -r 4948e2bd67e5 -r d87ccbcc2702 src/Pure/Tools/codegen_func.ML --- a/src/Pure/Tools/codegen_func.ML Fri Apr 20 11:21:34 2007 +0200 +++ b/src/Pure/Tools/codegen_func.ML Fri Apr 20 11:21:35 2007 +0200 @@ -8,12 +8,12 @@ signature CODEGEN_FUNC = sig val assert_rew: thm -> thm - val mk_rew: thm -> thm list - val assert_func: bool -> thm -> thm option - val mk_func: bool -> thm -> (CodegenConsts.const * thm) list - val mk_head: thm -> CodegenConsts.const * thm - val dest_func: thm -> (string * typ) * term list - val typ_func: thm -> typ + val mk_rew: thm -> thm + val mk_func: thm -> thm + val head_func: thm -> CodegenConsts.const * typ + val bad_thm: string -> 'a + val error_thm: (thm -> thm) -> thm -> thm + val warning_thm: (thm -> thm) -> thm -> thm option val inst_thm: sort Vartab.table -> thm -> thm val expand_eta: int -> thm -> thm @@ -25,10 +25,14 @@ structure CodegenFunc : CODEGEN_FUNC = struct -fun lift_thm_thy f thm = f (Thm.theory_of_thm thm) thm; + +(* auxiliary *) -fun bad_thm msg thm = - error (msg ^ ": " ^ string_of_thm thm); +exception BAD_THM of string; +fun bad_thm msg = raise BAD_THM msg; +fun error_thm f thm = f thm handle BAD_THM msg => error msg; +fun warning_thm f thm = SOME (f thm) handle BAD_THM msg + => (warning msg; NONE); (* making rewrite theorems *) @@ -36,85 +40,82 @@ fun assert_rew thm = let val thy = Thm.theory_of_thm thm; - val (lhs, rhs) = (Logic.dest_equals o Thm.prop_of) thm; + val (lhs, rhs) = (Logic.dest_equals o Thm.prop_of) thm + handle TERM _ => bad_thm ("Not an equation: " ^ Display.string_of_thm thm); fun vars_of t = fold_aterms (fn Var (v, _) => insert (op =) v - | Free _ => bad_thm "Illegal free variable in rewrite theorem" thm + | Free _ => bad_thm ("Illegal free variable in rewrite theorem\n" + ^ Display.string_of_thm thm) | _ => I) t []; fun tvars_of t = fold_term_types (fn _ => fold_atyps (fn TVar (v, _) => insert (op =) v - | TFree _ => bad_thm "Illegal free type variable in rewrite theorem" thm)) t []; + | TFree _ => bad_thm + ("Illegal free type variable in rewrite theorem\n" ^ Display.string_of_thm thm))) t []; val lhs_vs = vars_of lhs; val rhs_vs = vars_of rhs; val lhs_tvs = tvars_of lhs; val rhs_tvs = tvars_of lhs; val _ = if null (subtract (op =) lhs_vs rhs_vs) then () - else bad_thm "Free variables on right hand side of rewrite theorems" thm + else bad_thm ("Free variables on right hand side of rewrite theorem\n" + ^ Display.string_of_thm thm); val _ = if null (subtract (op =) lhs_tvs rhs_tvs) then () - else bad_thm "Free type variables on right hand side of rewrite theorems" thm + else bad_thm ("Free type variables on right hand side of rewrite theorem\n" + ^ Display.string_of_thm thm) in thm end; fun mk_rew thm = let val thy = Thm.theory_of_thm thm; - val thms = (#mk o #mk_rews o snd o MetaSimplifier.rep_ss o Simplifier.simpset_of) thy thm; + val ctxt = ProofContext.init thy; in - map assert_rew thms + thm + |> LocalDefs.meta_rewrite_rule ctxt + |> assert_rew end; (* making defining equations *) -val typ_func = lift_thm_thy (fn thy => snd o dest_Const o fst o strip_comb - o fst o Logic.dest_equals o ObjectLogic.drop_judgment thy o Thm.plain_prop_of); - -val dest_func = lift_thm_thy (fn thy => apfst dest_Const o strip_comb - o fst o Logic.dest_equals o ObjectLogic.drop_judgment thy o Thm.plain_prop_of - o Drule.fconv_rule Drule.beta_eta_conversion); - -val mk_head = lift_thm_thy (fn thy => fn thm => - ((CodegenConsts.const_of_cexpr thy o fst o dest_func) thm, thm)); - -local - -exception BAD of string; - -fun handle_bad strict thm msg = - if strict then error (msg ^ ": " ^ string_of_thm thm) - else (warning (msg ^ ": " ^ string_of_thm thm); NONE); - -in +fun assert_func thm = + let + val thy = Thm.theory_of_thm thm; + val args = (snd o strip_comb o fst o Logic.dest_equals + o ObjectLogic.drop_judgment thy o Thm.plain_prop_of) thm; + val _ = + if has_duplicates (op =) + ((fold o fold_aterms) (fn Var (v, _) => cons v + | _ => I + ) args []) + then bad_thm ("Duplicated variables on left hand side of equation\n" + ^ Display.string_of_thm thm) + else () + fun check _ (Abs _) = bad_thm + ("Abstraction on left hand side of equation\n" + ^ Display.string_of_thm thm) + | check 0 (Var _) = () + | check _ (Var _) = bad_thm + ("Variable with application on left hand side of defining equation\n" + ^ Display.string_of_thm thm) + | check n (t1 $ t2) = (check (n+1) t1; check 0 t2) + | check n (Const (_, ty)) = if n <> (length o fst o strip_type) ty + then bad_thm + ("Partially applied constant on left hand side of equation" + ^ Display.string_of_thm thm) + else (); + val _ = map (check 0) args; + in thm end; -fun assert_func strict thm = case try dest_func thm - of SOME (c_ty as (c, ty), args) => ( - let - val thy = Thm.theory_of_thm thm; - val _ = - if has_duplicates (op =) - ((fold o fold_aterms) (fn Var (v, _) => cons v - | _ => I - ) args []) - then raise BAD "Repeated variables on left hand side of defining equation" - else () - fun check _ (Abs _) = raise BAD - "Abstraction on left hand side of defining equation" - | check 0 (Var _) = () - | check _ (Var _) = raise BAD - "Variable with application on left hand side of defining equation" - | check n (t1 $ t2) = (check (n+1) t1; check 0 t2) - | check n (Const (_, ty)) = if n <> (length o fst o strip_type) ty - then raise BAD - ("Partially applied constant on left hand side of defining equation") - else (); - val _ = map (check 0) args; - in SOME thm end handle BAD msg => handle_bad strict thm msg) - | NONE => handle_bad strict thm "Not a defining equation"; +val mk_func = assert_func o Drule.fconv_rule Drule.beta_eta_conversion o mk_rew; -end; - -fun mk_func strict = map_filter (Option.map mk_head o assert_func strict) o mk_rew; +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 + o ObjectLogic.drop_judgment thy o Thm.plain_prop_of) thm; + val const = CodegenConsts.const_of_cexpr thy c_ty; + in (const, ty) end; (* utilities *) diff -r 4948e2bd67e5 -r d87ccbcc2702 src/Pure/Tools/codegen_funcgr.ML --- a/src/Pure/Tools/codegen_funcgr.ML Fri Apr 20 11:21:34 2007 +0200 +++ b/src/Pure/Tools/codegen_funcgr.ML Fri Apr 20 11:21:35 2007 +0200 @@ -157,9 +157,9 @@ fun resort_rec tap_typ (const, []) = (true, (const, [])) | resort_rec tap_typ (const, thms as thm :: _) = let - val ty = CodegenFunc.typ_func thm; + val (_, ty) = CodegenFunc.head_func thm; val thms' as thm' :: _ = resort_thms algebra tap_typ thms - val ty' = CodegenFunc.typ_func thm'; + val (_, ty') = CodegenFunc.head_func thm'; in (Sign.typ_equiv thy (ty, ty'), (const, thms')) end; fun resort_recs funcss = let @@ -167,7 +167,7 @@ of SOME const => AList.lookup (CodegenConsts.eq_const) funcss const |> these |> try hd - |> Option.map CodegenFunc.typ_func + |> Option.map (snd o CodegenFunc.head_func) | NONE => NONE; val (unchangeds, funcss') = split_list (map (resort_rec tap_typ) funcss); val unchanged = fold (fn x => fn y => x andalso y) unchangeds true; @@ -241,10 +241,10 @@ |> resort_funcss thy algebra funcgr |> filter_out (can (Constgraph.get_node funcgr) o fst); fun typ_func const [] = CodegenData.default_typ thy const - | typ_func (_, NONE) (thm :: _) = CodegenFunc.typ_func thm + | typ_func (_, NONE) (thm :: _) = (snd o CodegenFunc.head_func) thm | typ_func (const as (c, SOME tyco)) (thms as (thm :: _)) = let - val ty = CodegenFunc.typ_func thm; + val (_, ty) = CodegenFunc.head_func thm; val SOME class = AxClass.class_of_param thy c; val sorts_decl = Sorts.mg_domain algebra tyco [class]; val tys = CodegenConsts.typargs thy (c, ty); diff -r 4948e2bd67e5 -r d87ccbcc2702 src/Pure/Tools/codegen_package.ML --- a/src/Pure/Tools/codegen_package.ML Fri Apr 20 11:21:34 2007 +0200 +++ b/src/Pure/Tools/codegen_package.ML Fri Apr 20 11:21:35 2007 +0200 @@ -71,12 +71,22 @@ fun rewrites thy = []; ); -fun print_codethms thy = - Pretty.writeln o CodegenFuncgr.pretty thy o Funcgr.make thy; +fun code_depgr thy [] = Funcgr.make thy [] + | code_depgr thy consts = + let + val gr = Funcgr.make thy consts; + val select = CodegenFuncgr.Constgraph.all_succs gr consts; + in + CodegenFuncgr.Constgraph.subgraph + (member CodegenConsts.eq_const select) gr + end; + +fun code_thms thy = + Pretty.writeln o CodegenFuncgr.pretty thy o code_depgr thy; fun code_deps thy consts = let - val gr = Funcgr.make thy consts; + val gr = code_depgr thy consts; fun mk_entry (const, (_, (_, parents))) = let val name = CodegenConsts.string_of_const thy const; @@ -113,7 +123,7 @@ fun prep_eqs thy (thms as thm :: _) = let - val ty = (Logic.unvarifyT o CodegenFunc.typ_func) thm; + val ty = (Logic.unvarifyT o snd o CodegenFunc.head_func) thm; val thms' = if (null o Term.typ_tfrees) ty orelse (null o fst o strip_type) ty then thms else map (CodegenFunc.expand_eta 1) thms; @@ -600,34 +610,6 @@ fun satisfies thy t witnesses = raw_eval_term thy (("CodegenPackage.satisfies_ref", satisfies_ref), t) witnesses; - -(* constant specifications with wildcards *) - -fun consts_of thy thyname = - let - val this_thy = Option.map theory 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) = - not (exists (fn thy => Sign.declared_const thy c) (Theory.parents_of this_thy)) - | belongs_here thyname (c, SOME tyco) = - not (exists (fn thy => test_instance thy ((the o AxClass.class_of_param thy) c, tyco)) - (Theory.parents_of this_thy)) - in case thyname - of NONE => consts - | SOME thyname => filter (belongs_here thyname) consts - end; - fun filter_generatable thy targets consts = let val (consts', funcgr) = Funcgr.make_consts thy consts; @@ -636,11 +618,6 @@ (consts' ~~ consts''); in consts''' end; -fun read_constspec thy targets "*" = filter_generatable thy targets (consts_of thy NONE) - | read_constspec thy targets s = if String.isSuffix ".*" s - then filter_generatable thy targets (consts_of thy (SOME (unsuffix ".*" s))) - else [CodegenConsts.read_const thy s]; - (** toplevel interface and setup **) @@ -655,7 +632,8 @@ (target, SOME (CodegenSerializer.get_serializer thy target args CodegenNames.labelled_name)) | (target, []) => (CodegenSerializer.assert_serializer thy target, NONE)) seris; val targets = case map fst seris' of [] => NONE | xs => SOME xs; - val cs = maps (read_constspec thy targets) raw_cs; + val cs = CodegenConsts.read_const_exprs thy + (filter_generatable thy targets) raw_cs; fun generate' thy = case cs of [] => [] | _ => @@ -671,11 +649,11 @@ (map (serialize' cs code) (map_filter snd seris'); ()) end; -fun print_codethms_cmd thy = - print_codethms thy o map (CodegenConsts.read_const thy); +fun code_thms_cmd thy = + code_thms thy o CodegenConsts.read_const_exprs thy (fst o Funcgr.make_consts thy); fun code_deps_cmd thy = - code_deps thy o map (CodegenConsts.read_const thy); + code_deps thy o CodegenConsts.read_const_exprs thy (fst o Funcgr.make_consts thy); val code_exprP = ( (Scan.repeat P.term @@ -713,13 +691,13 @@ ); val code_thmsP = - OuterSyntax.improper_command code_thmsK "print cached defining equations" OuterKeyword.diag + OuterSyntax.improper_command code_thmsK "print system of defining equations for code" OuterKeyword.diag (Scan.repeat P.term >> (fn cs => Toplevel.no_timing o Toplevel.unknown_theory - o Toplevel.keep ((fn thy => print_codethms_cmd thy cs) o Toplevel.theory_of))); + o Toplevel.keep ((fn thy => code_thms_cmd thy cs) o Toplevel.theory_of))); val code_depsP = - OuterSyntax.improper_command code_depsK "visualize dependencies of defining equations" OuterKeyword.diag + OuterSyntax.improper_command code_depsK "visualize dependencies of defining equations for code" OuterKeyword.diag (Scan.repeat P.term >> (fn cs => Toplevel.no_timing o Toplevel.unknown_theory o Toplevel.keep ((fn thy => code_deps_cmd thy cs) o Toplevel.theory_of)));