# HG changeset patch # User wenzelm # Date 1442925143 -7200 # Node ID 077b88f9ec1653b76624d8f7d0f0cf91128dab61 # Parent 759b5299a9f2c271168cf353b34dd1726bc9525f HOL typedef with explicit dependency checks according to Ondrey Kuncar, 07-Jul-2015, 16-Jul-2015, 30-Jul-2015; defs.ML: track dependencies also for type constructors; typedef.ML: add type defined by typedef to dependencies, Abs and Rep now depend on the type; Pure types and typedecls are final -- no dependencies; diff -r 759b5299a9f2 -r 077b88f9ec16 src/Doc/Implementation/Logic.thy --- a/src/Doc/Implementation/Logic.thy Tue Sep 22 08:38:25 2015 +0200 +++ b/src/Doc/Implementation/Logic.thy Tue Sep 22 14:32:23 2015 +0200 @@ -667,7 +667,7 @@ \end{mldecls} \begin{mldecls} @{index_ML Theory.add_deps: "Proof.context -> string -> - string * typ -> (string * typ) list -> theory -> theory"} \\ + Theory.dep -> Theory.dep list -> theory -> theory"} \\ \end{mldecls} \begin{description} diff -r 759b5299a9f2 -r 077b88f9ec16 src/HOL/Library/bnf_axiomatization.ML --- a/src/HOL/Library/bnf_axiomatization.ML Tue Sep 22 08:38:25 2015 +0200 +++ b/src/HOL/Library/bnf_axiomatization.ML Tue Sep 22 14:32:23 2015 +0200 @@ -35,9 +35,9 @@ fun mk_b name user_b = (if Binding.is_empty user_b then Binding.prefix_name (name ^ "_") b else user_b) |> Binding.qualify false (Binding.name_of b); - val (Tname, lthy) = Typedecl.basic_typedecl (b, length vars, mx) lthy; + val (Tname, lthy) = Typedecl.basic_typedecl true (b, length vars, mx) lthy; val (bd_type_Tname, lthy) = - Typedecl.basic_typedecl (mk_b "bd_type" Binding.empty, length deads, NoSyn) lthy; + Typedecl.basic_typedecl true (mk_b "bd_type" Binding.empty, length deads, NoSyn) lthy; val T = Type (Tname, map TFree vars); val bd_type_T = Type (bd_type_Tname, map TFree deads); val lives = map TFree (filter_out (member (op =) deads) vars); diff -r 759b5299a9f2 -r 077b88f9ec16 src/HOL/SPARK/Tools/spark_vcs.ML --- a/src/HOL/SPARK/Tools/spark_vcs.ML Tue Sep 22 08:38:25 2015 +0200 +++ b/src/HOL/SPARK/Tools/spark_vcs.ML Tue Sep 22 14:32:23 2015 +0200 @@ -389,7 +389,7 @@ case get_type thy prfx s of SOME _ => thy | NONE => Typedecl.typedecl_global - (Binding.name s, [], NoSyn) thy |> snd); + true (Binding.name s, [], NoSyn) thy |> snd); fun term_of_expr thy prfx types pfuns = diff -r 759b5299a9f2 -r 077b88f9ec16 src/HOL/TPTP/TPTP_Parser/tptp_interpret.ML --- a/src/HOL/TPTP/TPTP_Parser/tptp_interpret.ML Tue Sep 22 08:38:25 2015 +0200 +++ b/src/HOL/TPTP/TPTP_Parser/tptp_interpret.ML Tue Sep 22 14:32:23 2015 +0200 @@ -199,7 +199,7 @@ val tyargs = List.tabulate (arity, rpair @{sort type} o prefix "'" o string_of_int) val thy' = - Typedecl.typedecl_global (mk_binding config type_name, tyargs, NoSyn) thy + Typedecl.typedecl_global true (mk_binding config type_name, tyargs, NoSyn) thy |> snd val typ_map_entry = (thf_type, (final_fqn, arity)) val ty_map' = typ_map_entry :: ty_map diff -r 759b5299a9f2 -r 077b88f9ec16 src/HOL/Tools/BNF/bnf_fp_def_sugar.ML --- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Tue Sep 22 08:38:25 2015 +0200 +++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Tue Sep 22 14:32:23 2015 +0200 @@ -1923,7 +1923,7 @@ ||>> variant_tfrees fp_b_names; fun add_fake_type spec = - Typedecl.basic_typedecl (type_binding_of_spec spec, num_As, mixfix_of_spec spec); + Typedecl.basic_typedecl true (type_binding_of_spec spec, num_As, mixfix_of_spec spec); val (fake_T_names, fake_lthy) = fold_map add_fake_type specs no_defs_lthy; diff -r 759b5299a9f2 -r 077b88f9ec16 src/HOL/Tools/typedef.ML --- a/src/HOL/Tools/typedef.ML Tue Sep 22 08:38:25 2015 +0200 +++ b/src/HOL/Tools/typedef.ML Tue Sep 22 14:32:23 2015 +0200 @@ -132,14 +132,22 @@ |> Local_Theory.background_theory_result (Sign.declare_const lthy ((Rep_name, newT --> oldT), NoSyn) ##>> Sign.declare_const lthy ((Abs_name, oldT --> newT), NoSyn)); - - val typedef_deps = Term.add_consts A []; + + fun fold_type_constr f (Type (name, Ts)) = f (name,Ts) #> fold (fold_type_constr f) Ts + | fold_type_constr _ _ = I; + + val A_consts = fold_aterms (fn Const const => insert (op =) (Theory.DConst const) | _ => I) A []; + val A_types = fold_types (fold_type_constr (insert (op =) o Theory.DType)) A [] + val typedef_deps = A_consts @ A_types; + + val newT_dep = Theory.DType (dest_Type newT); val ((axiom_name, axiom), axiom_lthy) = consts_lthy |> Local_Theory.background_theory_result (Thm.add_axiom consts_lthy (type_definition_name, mk_typedef newT oldT RepC AbsC A) ##> - Theory.add_deps consts_lthy "" (dest_Const RepC) typedef_deps ##> - Theory.add_deps consts_lthy "" (dest_Const AbsC) typedef_deps); + Theory.add_deps consts_lthy "" newT_dep typedef_deps ##> + Theory.add_deps consts_lthy "" (Theory.DConst (dest_Const RepC)) [newT_dep] ##> + Theory.add_deps consts_lthy "" (Theory.DConst (dest_Const AbsC)) [newT_dep]); in ((RepC, AbsC, axiom_name, axiom), axiom_lthy) end; @@ -187,7 +195,7 @@ val args = map (Proof_Context.check_tfree tmp_ctxt') raw_args; val (newT, typedecl_lthy) = lthy - |> Typedecl.typedecl (name, args, mx) + |> Typedecl.typedecl false (name, args, mx) ||> Variable.declare_term set; val Type (full_name, _) = newT; diff -r 759b5299a9f2 -r 077b88f9ec16 src/Pure/Isar/isar_syn.ML --- a/src/Pure/Isar/isar_syn.ML Tue Sep 22 08:38:25 2015 +0200 +++ b/src/Pure/Isar/isar_syn.ML Tue Sep 22 14:32:23 2015 +0200 @@ -22,7 +22,7 @@ val _ = Outer_Syntax.local_theory @{command_keyword typedecl} "type declaration" (Parse.type_args -- Parse.binding -- Parse.opt_mixfix - >> (fn ((args, a), mx) => Typedecl.typedecl (a, map (rpair dummyS) args, mx) #> snd)); + >> (fn ((args, a), mx) => Typedecl.typedecl true (a, map (rpair dummyS) args, mx) #> snd)); val _ = Outer_Syntax.local_theory @{command_keyword type_synonym} "declare type abbreviation" diff -r 759b5299a9f2 -r 077b88f9ec16 src/Pure/Isar/object_logic.ML --- a/src/Pure/Isar/object_logic.ML Tue Sep 22 08:38:25 2015 +0200 +++ b/src/Pure/Isar/object_logic.ML Tue Sep 22 14:32:23 2015 +0200 @@ -90,7 +90,7 @@ let val c = Sign.full_name thy b in thy |> add_consts [(b, T, mx)] - |> (fn thy' => Theory.add_deps_global c (c, Sign.the_const_type thy' c) [] thy') + |> (fn thy' => Theory.add_deps_global c (Theory.DConst (c, Sign.the_const_type thy' c)) [] thy') |> (Context.theory_map o map_data) (fn (base_sort, judgment, atomize_rulify) => if is_some judgment then error "Attempt to redeclare object-logic judgment" else (base_sort, SOME c, atomize_rulify)) diff -r 759b5299a9f2 -r 077b88f9ec16 src/Pure/Isar/typedecl.ML --- a/src/Pure/Isar/typedecl.ML Tue Sep 22 08:38:25 2015 +0200 +++ b/src/Pure/Isar/typedecl.ML Tue Sep 22 14:32:23 2015 +0200 @@ -7,9 +7,9 @@ signature TYPEDECL = sig val read_constraint: Proof.context -> string option -> sort - val basic_typedecl: binding * int * mixfix -> local_theory -> string * local_theory - val typedecl: binding * (string * sort) list * mixfix -> local_theory -> typ * local_theory - val typedecl_global: binding * (string * sort) list * mixfix -> theory -> typ * theory + val basic_typedecl: bool -> binding * int * mixfix -> local_theory -> string * local_theory + val typedecl: bool -> binding * (string * sort) list * mixfix -> local_theory -> typ * local_theory + val typedecl_global: bool -> binding * (string * sort) list * mixfix -> theory -> typ * theory val abbrev: binding * string list * mixfix -> typ -> local_theory -> string * local_theory val abbrev_cmd: binding * string list * mixfix -> string -> local_theory -> string * local_theory val abbrev_global: binding * string list * mixfix -> typ -> theory -> string * theory @@ -35,13 +35,6 @@ |> pair name end; -fun basic_typedecl (b, n, mx) lthy = - basic_decl (fn name => - Sign.add_type lthy (b, n, NoSyn) #> - (case Object_Logic.get_base_sort lthy of - SOME S => Axclass.arity_axiomatization (name, replicate n S, S) - | NONE => I)) (b, n, mx) lthy; - (* global type -- without dependencies on type parameters of the context *) @@ -61,21 +54,41 @@ commas_quote (map (Syntax.string_of_typ lthy) bad_args)); in T end; +fun basic_typedecl final (b, n, mx) lthy = + let + fun make_final lthy = + let + val tfree_names = Name.invent (Variable.names_of lthy) Name.aT n + val tfrees = map (fn name => (name, [])) tfree_names + val T = global_type lthy (b, tfrees) + in + Local_Theory.background_theory (Theory.add_deps lthy "" (Theory.DType (dest_Type T)) []) lthy + end + in + lthy + |> basic_decl (fn name => + Sign.add_type lthy (b, n, NoSyn) #> + (case Object_Logic.get_base_sort lthy of + SOME S => Axclass.arity_axiomatization (name, replicate n S, S) + | NONE => I)) (b, n, mx) + ||> (if final then make_final else I) + end + (* type declarations *) -fun typedecl (b, raw_args, mx) lthy = +fun typedecl final (b, raw_args, mx) lthy = let val T = global_type lthy (b, raw_args) in lthy - |> basic_typedecl (b, length raw_args, mx) + |> basic_typedecl final (b, length raw_args, mx) |> snd |> Variable.declare_typ T |> pair T end; -fun typedecl_global decl = +fun typedecl_global final decl = Named_Target.theory_init - #> typedecl decl + #> typedecl final decl #> Local_Theory.exit_result_global Morphism.typ; diff -r 759b5299a9f2 -r 077b88f9ec16 src/Pure/axclass.ML --- a/src/Pure/axclass.ML Tue Sep 22 08:38:25 2015 +0200 +++ b/src/Pure/axclass.ML Tue Sep 22 14:32:23 2015 +0200 @@ -614,7 +614,8 @@ thy |> Sign.primitive_class (bclass, super) |> classrel_axiomatization (map (fn c => (class, c)) super) - |> Theory.add_deps_global "" (class_const class) (map class_const super) + |> Theory.add_deps_global "" (Theory.DConst (class_const class)) + (map (Theory.DConst o class_const) super) end; end; diff -r 759b5299a9f2 -r 077b88f9ec16 src/Pure/defs.ML --- a/src/Pure/defs.ML Tue Sep 22 08:38:25 2015 +0200 +++ b/src/Pure/defs.ML Tue Sep 22 14:32:23 2015 +0200 @@ -7,7 +7,9 @@ signature DEFS = sig - val pretty_const: Proof.context -> string * typ list -> Pretty.T + datatype node = NConst of string | NType of string + val fast_node_ord: node * node -> order + val pretty_node: Proof.context -> node * typ list -> Pretty.T val plain_args: typ list -> bool type T type spec = @@ -15,31 +17,44 @@ description: string, pos: Position.T, lhs: typ list, - rhs: (string * typ list) list} - val all_specifications_of: T -> (string * spec list) list - val specifications_of: T -> string -> spec list + rhs: (node * typ list) list} + val all_specifications_of: T -> (node * spec list) list + val specifications_of: T -> node -> spec list val dest: T -> - {restricts: ((string * typ list) * string) list, - reducts: ((string * typ list) * (string * typ list) list) list} + {restricts: ((node * typ list) * string) list, + reducts: ((node * typ list) * (node * typ list) list) list} val empty: T val merge: Proof.context -> T * T -> T val define: Proof.context -> bool -> string option -> string -> - string * typ list -> (string * typ list) list -> T -> T + node * typ list -> (node * typ list) list -> T -> T end + structure Defs: DEFS = struct +datatype node = NConst of string | NType of string + +fun fast_node_ord (NConst s1, NConst s2) = fast_string_ord (s1, s2) + | fast_node_ord (NType s1, NType s2) = fast_string_ord (s1, s2) + | fast_node_ord (NConst _, NType _) = LESS + | fast_node_ord (NType _, NConst _) = GREATER + +fun string_of_node (NConst s) = "constant " ^ s + | string_of_node (NType s) = "type " ^ s + +structure Deftab = Table(type key = node val ord = fast_node_ord); + (* type arguments *) type args = typ list; -fun pretty_const ctxt (c, args) = +fun pretty_node ctxt (c, args) = let val prt_args = if null args then [] else [Pretty.list "(" ")" (map (Syntax.pretty_typ ctxt o Logic.unvarifyT_global) args)]; - in Pretty.block (Pretty.str c :: prt_args) end; + in Pretty.block (Pretty.str (string_of_node c) :: prt_args) end; fun plain_args args = forall Term.is_TVar args andalso not (has_duplicates (op =) args); @@ -63,31 +78,31 @@ description: string, pos: Position.T, lhs: args, - rhs: (string * args) list}; + rhs: (node * args) list}; type def = {specs: spec Inttab.table, (*source specifications*) restricts: (args * string) list, (*global restrictions imposed by incomplete patterns*) - reducts: (args * (string * args) list) list}; (*specifications as reduction system*) + reducts: (args * (node * args) list) list}; (*specifications as reduction system*) fun make_def (specs, restricts, reducts) = {specs = specs, restricts = restricts, reducts = reducts}: def; fun map_def c f = - Symtab.default (c, make_def (Inttab.empty, [], [])) #> - Symtab.map_entry c (fn {specs, restricts, reducts}: def => + Deftab.default (c, make_def (Inttab.empty, [], [])) #> + Deftab.map_entry c (fn {specs, restricts, reducts}: def => make_def (f (specs, restricts, reducts))); -datatype T = Defs of def Symtab.table; +datatype T = Defs of def Deftab.table; fun lookup_list which defs c = - (case Symtab.lookup defs c of + (case Deftab.lookup defs c of SOME (def: def) => which def | NONE => []); fun all_specifications_of (Defs defs) = - (map o apsnd) (map snd o Inttab.dest o #specs) (Symtab.dest defs); + (map o apsnd) (map snd o Inttab.dest o #specs) (Deftab.dest defs); fun specifications_of (Defs defs) = lookup_list (map snd o Inttab.dest o #specs) defs; @@ -96,13 +111,13 @@ fun dest (Defs defs) = let - val restricts = Symtab.fold (fn (c, {restricts, ...}) => + val restricts = Deftab.fold (fn (c, {restricts, ...}) => fold (fn (args, description) => cons ((c, args), description)) restricts) defs []; - val reducts = Symtab.fold (fn (c, {reducts, ...}) => + val reducts = Deftab.fold (fn (c, {reducts, ...}) => fold (fn (args, deps) => cons ((c, args), deps)) reducts) defs []; in {restricts = restricts, reducts = reducts} end; -val empty = Defs Symtab.empty; +val empty = Defs Deftab.empty; (* specifications *) @@ -110,7 +125,7 @@ fun disjoint_specs c (i, {description = a, pos = pos_a, lhs = Ts, ...}: spec) = Inttab.forall (fn (j, {description = b, pos = pos_b, lhs = Us, ...}: spec) => i = j orelse disjoint_args (Ts, Us) orelse - error ("Clash of specifications for constant " ^ quote c ^ ":\n" ^ + error ("Clash of specifications for " ^ quote (string_of_node c) ^ ":\n" ^ " " ^ quote a ^ Position.here pos_a ^ "\n" ^ " " ^ quote b ^ Position.here pos_b)); @@ -128,9 +143,9 @@ local -val prt = Pretty.string_of oo pretty_const; +val prt = Pretty.string_of oo pretty_node; fun err ctxt (c, args) (d, Us) s1 s2 = - error (s1 ^ " dependency of constant " ^ prt ctxt (c, args) ^ " -> " ^ prt ctxt (d, Us) ^ s2); + error (s1 ^ " dependency of " ^ prt ctxt (c, args) ^ " -> " ^ prt ctxt (d, Us) ^ s2); fun acyclic ctxt (c, args) (d, Us) = c <> d orelse @@ -174,12 +189,12 @@ else (true, defs |> map_def c (fn (specs, restricts, _) => (specs, restricts, reducts'))) end; fun norm_all defs = - (case Symtab.fold norm_update defs (false, defs) of + (case Deftab.fold norm_update defs (false, defs) of (true, defs') => norm_all defs' | (false, _) => defs); fun check defs (c, {reducts, ...}: def) = reducts |> forall (fn (args, deps) => forall (wellformed ctxt defs (c, args)) deps); - in norm_all #> (fn defs => tap (Symtab.forall (check defs)) defs) end; + in norm_all #> (fn defs => tap (Deftab.forall (check defs)) defs) end; fun dependencies ctxt (c, args) restr deps = map_def c (fn (specs, restricts, reducts) => @@ -202,8 +217,8 @@ fun add_def (c, {restricts, reducts, ...}: def) = fold (fn (args, deps) => add_deps (c, args) restricts deps) reducts; in - Defs (Symtab.join join_specs (defs1, defs2) - |> normalize ctxt |> Symtab.fold add_def defs2) + Defs (Deftab.join join_specs (defs1, defs2) + |> normalize ctxt |> Deftab.fold add_def defs2) end; diff -r 759b5299a9f2 -r 077b88f9ec16 src/Pure/display.ML --- a/src/Pure/display.ML Tue Sep 22 08:38:25 2015 +0200 +++ b/src/Pure/display.ML Tue Sep 22 14:32:23 2015 +0200 @@ -104,7 +104,8 @@ fun prt_term t = Pretty.quote (Syntax.pretty_term ctxt t); val prt_term_no_vars = prt_term o Logic.unvarify_global; fun prt_const (c, ty) = [Pretty.mark_str c, Pretty.str " ::", Pretty.brk 1, prt_typ_no_tvars ty]; - val prt_const' = Defs.pretty_const ctxt; + val prt_node = Defs.pretty_node ctxt; + fun sort_node_wrt f = sort (Defs.fast_node_ord o apply2 f) fun pretty_classrel (c, []) = prt_cls c | pretty_classrel (c, cs) = Pretty.block @@ -134,26 +135,29 @@ Pretty.block [Pretty.mark_str a, Pretty.str ":", Pretty.brk 1, prt_term_no_vars t]; fun pretty_finals reds = Pretty.block - (Pretty.str "final:" :: Pretty.brk 1 :: Pretty.commas (map (prt_const' o fst) reds)); + (Pretty.str "final:" :: Pretty.brk 1 :: Pretty.commas (map (prt_node o fst) reds)); fun pretty_reduct (lhs, rhs) = Pretty.block - ([prt_const' lhs, Pretty.str " ->", Pretty.brk 2] @ - Pretty.commas (map prt_const' (sort_by #1 rhs))); + ([prt_node lhs, Pretty.str " ->", Pretty.brk 2] @ + Pretty.commas (map prt_node ((sort_node_wrt #1) rhs))); fun pretty_restrict (const, name) = - Pretty.block ([prt_const' const, Pretty.brk 2, Pretty.str ("(from " ^ quote name ^ ")")]); + Pretty.block ([prt_node const, Pretty.brk 2, Pretty.str ("(from " ^ quote name ^ ")")]); val defs = Theory.defs_of thy; val {restricts, reducts} = Defs.dest defs; val tsig = Sign.tsig_of thy; val consts = Sign.consts_of thy; val {const_space, constants, constraints} = Consts.dest consts; - val extern_const = Name_Space.extern ctxt const_space; val {classes, default, types, ...} = Type.rep_tsig tsig; + val type_space = Type.type_space tsig; val (class_space, class_algebra) = classes; val classes = Sorts.classes_of class_algebra; val arities = Sorts.arities_of class_algebra; + fun extern_node (Defs.NConst c) = Defs.NConst (Name_Space.extern ctxt const_space c) + | extern_node (Defs.NType t) = Defs.NType (Name_Space.extern ctxt type_space t); + val clsses = Name_Space.extern_entries verbose ctxt class_space (map (fn ((c, _), cs) => (c, Sign.minimize_sort thy cs)) (Graph.dest classes)) @@ -163,6 +167,11 @@ Name_Space.extern_entries verbose ctxt (Type.type_space tsig) (Symtab.dest arities) |> map (apfst #1); + fun prune_const c = not verbose andalso Consts.is_concealed consts c; + + fun prune_node (Defs.NConst c) = prune_const c + | prune_node (Defs.NType t) = not verbose andalso Name_Space.is_concealed type_space t; + val cnsts = Name_Space.markup_entries verbose ctxt const_space constants; val log_cnsts = map_filter (fn (c, (ty, NONE)) => SOME (c, ty) | _ => NONE) cnsts; val abbrevs = map_filter (fn (c, (ty, SOME t)) => SOME (c, (ty, t)) | _ => NONE) cnsts; @@ -170,14 +179,13 @@ val axms = Name_Space.markup_table verbose ctxt (Theory.axiom_table thy); - fun prune_const c = not verbose andalso Consts.is_concealed consts c; - val (reds0, (reds1, reds2)) = filter_out (prune_const o fst o fst) reducts + val (reds0, (reds1, reds2)) = filter_out (prune_node o fst o fst) reducts |> map (fn (lhs, rhs) => - (apfst extern_const lhs, map (apfst extern_const) (filter_out (prune_const o fst) rhs))) - |> sort_by (#1 o #1) + (apfst extern_node lhs, map (apfst extern_node) (filter_out (prune_node o fst) rhs))) + |> sort_node_wrt (#1 o #1) |> List.partition (null o #2) ||> List.partition (Defs.plain_args o #2 o #1); - val rests = restricts |> map (apfst (apfst extern_const)) |> sort_by (#1 o #1); + val rests = restricts |> map (apfst (apfst extern_node)) |> sort_node_wrt (#1 o #1); in [Pretty.strs ("names:" :: Context.display_names thy)] @ [Pretty.big_list "classes:" (map pretty_classrel clsses), diff -r 759b5299a9f2 -r 077b88f9ec16 src/Pure/pure_thy.ML --- a/src/Pure/pure_thy.ML Tue Sep 22 08:38:25 2015 +0200 +++ b/src/Pure/pure_thy.ML Tue Sep 22 14:32:23 2015 +0200 @@ -66,6 +66,10 @@ (Binding.make ("prop", @{here}), 0, NoSyn), (Binding.make ("itself", @{here}), 1, NoSyn), (Binding.make ("dummy", @{here}), 0, NoSyn)] + #> Theory.add_deps_global "fun" (Theory.DType ("fun", [typ "'a", typ "'b"])) [] + #> Theory.add_deps_global "prop" (Theory.DType ("prop", [])) [] + #> Theory.add_deps_global "itself" (Theory.DType ("itself", [typ "'a"])) [] + #> Theory.add_deps_global "dummy" (Theory.DType ("dummy", [])) [] #> Sign.add_nonterminals_global (map (fn name => Binding.make (name, @{here})) (Lexicon.terminals @ ["logic", "type", "types", "sort", "classes", @@ -194,11 +198,11 @@ (qualify (Binding.make ("prop", @{here})), typ "prop => prop", NoSyn), (qualify (Binding.make ("type", @{here})), typ "'a itself", NoSyn), (qualify (Binding.make ("dummy_pattern", @{here})), typ "'a", Delimfix "'_")] - #> Theory.add_deps_global "Pure.eq" ("Pure.eq", typ "'a => 'a => prop") [] - #> Theory.add_deps_global "Pure.imp" ("Pure.imp", typ "prop => prop => prop") [] - #> Theory.add_deps_global "Pure.all" ("Pure.all", typ "('a => prop) => prop") [] - #> Theory.add_deps_global "Pure.type" ("Pure.type", typ "'a itself") [] - #> Theory.add_deps_global "Pure.dummy_pattern" ("Pure.dummy_pattern", typ "'a") [] + #> Theory.add_deps_global "Pure.eq" (Theory.DConst ("Pure.eq", typ "'a => 'a => prop")) [] + #> Theory.add_deps_global "Pure.imp" (Theory.DConst ("Pure.imp", typ "prop => prop => prop")) [] + #> Theory.add_deps_global "Pure.all" (Theory.DConst ("Pure.all", typ "('a => prop) => prop")) [] + #> Theory.add_deps_global "Pure.type" (Theory.DConst ("Pure.type", typ "'a itself")) [] + #> Theory.add_deps_global "Pure.dummy_pattern" (Theory.DConst ("Pure.dummy_pattern", typ "'a")) [] #> Sign.parse_ast_translation Syntax_Trans.pure_parse_ast_translation #> Sign.parse_translation Syntax_Trans.pure_parse_translation #> Sign.print_ast_translation Syntax_Trans.pure_print_ast_translation diff -r 759b5299a9f2 -r 077b88f9ec16 src/Pure/theory.ML --- a/src/Pure/theory.ML Tue Sep 22 08:38:25 2015 +0200 +++ b/src/Pure/theory.ML Tue Sep 22 14:32:23 2015 +0200 @@ -23,8 +23,9 @@ val begin_theory: string * Position.T -> theory list -> theory val end_theory: theory -> theory val add_axiom: Proof.context -> binding * term -> theory -> theory - val add_deps: Proof.context -> string -> string * typ -> (string * typ) list -> theory -> theory - val add_deps_global: string -> string * typ -> (string * typ) list -> theory -> theory + datatype dep = DConst of string * typ | DType of string * typ list + val add_deps: Proof.context -> string -> dep -> dep list -> theory -> theory + val add_deps_global: string -> dep -> dep list -> theory -> theory val add_def: Proof.context -> bool -> bool -> binding * term -> theory -> theory val specify_const: (binding * typ) * mixfix -> theory -> term * theory val check_overloading: Proof.context -> bool -> string * typ -> unit @@ -211,17 +212,26 @@ (* dependencies *) +datatype dep = DConst of string * typ | DType of string * typ list + +fun name_of_dep (DConst (s, _)) = s + | name_of_dep (DType (s, _)) = s + fun dependencies ctxt unchecked def description lhs rhs = let val thy = Proof_Context.theory_of ctxt; val consts = Sign.consts_of thy; - fun prep const = + fun prep (DConst const) = let val Const (c, T) = Sign.no_vars ctxt (Const const) - in (c, Consts.typargs consts (c, Logic.varifyT_global T)) end; - - val lhs_vars = Term.add_tfreesT (#2 lhs) []; - val rhs_extras = fold (#2 #> Term.fold_atyps (fn TFree v => - if member (op =) lhs_vars v then I else insert (op =) v | _ => I)) rhs []; + in (Defs.NConst c, Consts.typargs consts (c, Logic.varifyT_global T)) end + | prep (DType typ) = + let val Type (c, T) = Type.no_tvars (Type typ) + in (Defs.NType c, map Logic.varifyT_global T) end; + fun fold_dep_tfree f (DConst (_, T)) = fold_atyps (fn TFree v => f v | _ => I) T + | fold_dep_tfree f (DType (_, Ts)) = fold (fold_atyps (fn TFree v => f v | _ => I)) Ts + val lhs_vars = fold_dep_tfree (insert (op =)) lhs []; + val rhs_extras = fold (fold_dep_tfree + (fn v => if member (op =) lhs_vars v then I else insert (op =) v)) rhs []; val _ = if null rhs_extras then () else error ("Specification depends on extra type variables: " ^ @@ -231,15 +241,17 @@ fun add_deps ctxt a raw_lhs raw_rhs thy = let - val lhs :: rhs = map (dest_Const o Sign.cert_term thy o Const) (raw_lhs :: raw_rhs); - val description = if a = "" then #1 lhs ^ " axiom" else a; + fun cert_dep (DConst const) = const |> Const |> Sign.cert_term thy |> dest_Const |> DConst + | cert_dep (DType typ) = typ |> Type |> Sign.certify_typ thy |> dest_Type |> DType; + val lhs :: rhs = map cert_dep (raw_lhs :: raw_rhs); + val description = if a = "" then name_of_dep lhs ^ " axiom" else a; in thy |> map_defs (dependencies ctxt false NONE description lhs rhs) end; fun add_deps_global a x y thy = add_deps (Syntax.init_pretty_global thy) a x y thy; fun specify_const decl thy = let val (t as Const const, thy') = Sign.declare_const_global decl thy; - in (t, add_deps_global "" const [] thy') end; + in (t, add_deps_global "" (DConst const) [] thy') end; (* overloading *) @@ -271,15 +283,20 @@ local +fun fold_type_constr f (Type (name, Ts)) = f (name,Ts) #> fold (fold_type_constr f) Ts + | fold_type_constr _ _ = I; + fun check_def ctxt thy unchecked overloaded (b, tm) defs = let val name = Sign.full_name thy b; val ((lhs, rhs), _) = Primitive_Defs.dest_def ctxt Term.is_Const (K false) (K false) tm handle TERM (msg, _) => error msg; val lhs_const = Term.dest_Const (Term.head_of lhs); - val rhs_consts = fold_aterms (fn Const const => insert (op =) const | _ => I) rhs []; + val rhs_consts = fold_aterms (fn Const const => insert (op =) (DConst const) | _ => I) rhs []; + val rhs_types = fold_types (fold_type_constr (insert (op =) o DType)) rhs [] + val rhs_deps = rhs_consts @ rhs_types val _ = check_overloading ctxt overloaded lhs_const; - in defs |> dependencies ctxt unchecked (SOME name) name lhs_const rhs_consts end + in defs |> dependencies ctxt unchecked (SOME name) name (DConst lhs_const) rhs_deps end handle ERROR msg => cat_error msg (Pretty.string_of (Pretty.block [Pretty.str ("The error(s) above occurred in definition " ^ Binding.print b ^ ":"), Pretty.fbrk, Pretty.quote (Syntax.pretty_term ctxt tm)]));