# HG changeset patch # User wenzelm # Date 1442933396 -7200 # Node ID 8611f408ec13f7ad3a222678472b83502365b0a7 # Parent 066792098895000c334f33a891de777b4e7c51c5 renamed Defs.node to Defs.item; clarified type Defs.item; clarified item_ord for printing; diff -r 066792098895 -r 8611f408ec13 src/Pure/defs.ML --- a/src/Pure/defs.ML Tue Sep 22 16:17:49 2015 +0200 +++ b/src/Pure/defs.ML Tue Sep 22 16:49:56 2015 +0200 @@ -7,9 +7,10 @@ signature DEFS = sig - 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 + datatype item_kind = Constant | Type + type item = item_kind * string + val item_ord: item * item -> order + val pretty_item: Proof.context -> item * typ list -> Pretty.T val plain_args: typ list -> bool type T type spec = @@ -17,44 +18,49 @@ description: string, pos: Position.T, lhs: typ list, - rhs: (node * typ list) list} - val all_specifications_of: T -> (node * spec list) list - val specifications_of: T -> node -> spec list + rhs: (item * typ list) list} + val all_specifications_of: T -> (item * spec list) list + val specifications_of: T -> item -> spec list val dest: T -> - {restricts: ((node * typ list) * string) list, - reducts: ((node * typ list) * (node * typ list) list) list} + {restricts: ((item * typ list) * string) list, + reducts: ((item * typ list) * (item * typ list) list) list} val empty: T val merge: Proof.context -> T * T -> T val define: Proof.context -> bool -> string option -> string -> - node * typ list -> (node * typ list) list -> T -> T -end - + item * typ list -> (item * typ list) list -> T -> T +end; structure Defs: DEFS = struct -datatype node = NConst of string | NType of string +(* specification items *) + +datatype item_kind = Constant | Type; +type item = item_kind * string; + +fun item_kind_ord (Constant, Type) = LESS + | item_kind_ord (Type, Constant) = GREATER + | item_kind_ord _ = EQUAL; -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 +val item_ord = prod_ord item_kind_ord string_ord; +val fast_item_ord = prod_ord item_kind_ord fast_string_ord; -fun string_of_node (NConst s) = "constant " ^ s - | string_of_node (NType s) = "type " ^ s +val print_item_kind = fn Constant => "constant" | Type => "type"; +fun print_item (k, s) = print_item_kind k ^ " " ^ quote s; -structure Deftab = Table(type key = node val ord = fast_node_ord); +structure Itemtab = Table(type key = item val ord = fast_item_ord); + (* type arguments *) type args = typ list; -fun pretty_node ctxt (c, args) = +fun pretty_item 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 (string_of_node c) :: prt_args) end; + in Pretty.block (Pretty.str (print_item c) :: prt_args) end; fun plain_args args = forall Term.is_TVar args andalso not (has_duplicates (op =) args); @@ -78,31 +84,31 @@ description: string, pos: Position.T, lhs: args, - rhs: (node * args) list}; + rhs: (item * args) list}; type def = {specs: spec Inttab.table, (*source specifications*) restricts: (args * string) list, (*global restrictions imposed by incomplete patterns*) - reducts: (args * (node * args) list) list}; (*specifications as reduction system*) + reducts: (args * (item * 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 = - Deftab.default (c, make_def (Inttab.empty, [], [])) #> - Deftab.map_entry c (fn {specs, restricts, reducts}: def => + Itemtab.default (c, make_def (Inttab.empty, [], [])) #> + Itemtab.map_entry c (fn {specs, restricts, reducts}: def => make_def (f (specs, restricts, reducts))); -datatype T = Defs of def Deftab.table; +datatype T = Defs of def Itemtab.table; fun lookup_list which defs c = - (case Deftab.lookup defs c of + (case Itemtab.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) (Deftab.dest defs); + (map o apsnd) (map snd o Inttab.dest o #specs) (Itemtab.dest defs); fun specifications_of (Defs defs) = lookup_list (map snd o Inttab.dest o #specs) defs; @@ -111,13 +117,13 @@ fun dest (Defs defs) = let - val restricts = Deftab.fold (fn (c, {restricts, ...}) => + val restricts = Itemtab.fold (fn (c, {restricts, ...}) => fold (fn (args, description) => cons ((c, args), description)) restricts) defs []; - val reducts = Deftab.fold (fn (c, {reducts, ...}) => + val reducts = Itemtab.fold (fn (c, {reducts, ...}) => fold (fn (args, deps) => cons ((c, args), deps)) reducts) defs []; in {restricts = restricts, reducts = reducts} end; -val empty = Defs Deftab.empty; +val empty = Defs Itemtab.empty; (* specifications *) @@ -125,7 +131,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 " ^ quote (string_of_node c) ^ ":\n" ^ + error ("Clash of specifications for " ^ print_item c ^ ":\n" ^ " " ^ quote a ^ Position.here pos_a ^ "\n" ^ " " ^ quote b ^ Position.here pos_b)); @@ -143,7 +149,7 @@ local -val prt = Pretty.string_of oo pretty_node; +val prt = Pretty.string_of oo pretty_item; fun err ctxt (c, args) (d, Us) s1 s2 = error (s1 ^ " dependency of " ^ prt ctxt (c, args) ^ " -> " ^ prt ctxt (d, Us) ^ s2); @@ -189,12 +195,12 @@ else (true, defs |> map_def c (fn (specs, restricts, _) => (specs, restricts, reducts'))) end; fun norm_all defs = - (case Deftab.fold norm_update defs (false, defs) of + (case Itemtab.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 (Deftab.forall (check defs)) defs) end; + in norm_all #> (fn defs => tap (Itemtab.forall (check defs)) defs) end; fun dependencies ctxt (c, args) restr deps = map_def c (fn (specs, restricts, reducts) => @@ -217,8 +223,8 @@ fun add_def (c, {restricts, reducts, ...}: def) = fold (fn (args, deps) => add_deps (c, args) restricts deps) reducts; in - Defs (Deftab.join join_specs (defs1, defs2) - |> normalize ctxt |> Deftab.fold add_def defs2) + Defs (Itemtab.join join_specs (defs1, defs2) + |> normalize ctxt |> Itemtab.fold add_def defs2) end; @@ -229,7 +235,7 @@ val pos = Position.thread_data (); val restr = if plain_args args orelse - (case args of [Type (_, rec_args)] => plain_args rec_args | _ => false) + (case args of [Term.Type (_, rec_args)] => plain_args rec_args | _ => false) then [] else [(args, description)]; val spec = (serial (), {def = def, description = description, pos = pos, lhs = args, rhs = deps}); diff -r 066792098895 -r 8611f408ec13 src/Pure/display.ML --- a/src/Pure/display.ML Tue Sep 22 16:17:49 2015 +0200 +++ b/src/Pure/display.ML Tue Sep 22 16:49:56 2015 +0200 @@ -104,8 +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_node = Defs.pretty_node ctxt; - fun sort_node_wrt f = sort (Defs.fast_node_ord o apply2 f) + val prt_item = Defs.pretty_item ctxt; + fun sort_item_by f = sort (Defs.item_ord o apply2 f); fun pretty_classrel (c, []) = prt_cls c | pretty_classrel (c, cs) = Pretty.block @@ -135,14 +135,14 @@ 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_node o fst) reds)); + (Pretty.str "final:" :: Pretty.brk 1 :: Pretty.commas (map (prt_item o fst) reds)); fun pretty_reduct (lhs, rhs) = Pretty.block - ([prt_node lhs, Pretty.str " ->", Pretty.brk 2] @ - Pretty.commas (map prt_node ((sort_node_wrt #1) rhs))); + ([prt_item lhs, Pretty.str " ->", Pretty.brk 2] @ + Pretty.commas (map prt_item (sort_item_by #1 rhs))); fun pretty_restrict (const, name) = - Pretty.block ([prt_node const, Pretty.brk 2, Pretty.str ("(from " ^ quote name ^ ")")]); + Pretty.block ([prt_item const, Pretty.brk 2, Pretty.str ("(from " ^ quote name ^ ")")]); val defs = Theory.defs_of thy; val {restricts, reducts} = Defs.dest defs; @@ -155,8 +155,11 @@ 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); + fun extern_item (Defs.Constant, c) = (Defs.Constant, Name_Space.extern ctxt const_space c) + | extern_item (Defs.Type, c) = (Defs.Type, Name_Space.extern ctxt type_space c); + + fun prune_item (Defs.Constant, c) = not verbose andalso Consts.is_concealed consts c + | prune_item (Defs.Type, c) = not verbose andalso Name_Space.is_concealed type_space c; val clsses = Name_Space.extern_entries verbose ctxt class_space @@ -167,11 +170,6 @@ 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; @@ -179,13 +177,13 @@ val axms = Name_Space.markup_table verbose ctxt (Theory.axiom_table thy); - val (reds0, (reds1, reds2)) = filter_out (prune_node o fst o fst) reducts + val (reds0, (reds1, reds2)) = filter_out (prune_item o fst o fst) reducts |> map (fn (lhs, rhs) => - (apfst extern_node lhs, map (apfst extern_node) (filter_out (prune_node o fst) rhs))) - |> sort_node_wrt (#1 o #1) + (apfst extern_item lhs, map (apfst extern_item) (filter_out (prune_item o fst) rhs))) + |> sort_item_by (#1 o #1) |> List.partition (null o #2) ||> List.partition (Defs.plain_args o #2 o #1); - val rests = restricts |> map (apfst (apfst extern_node)) |> sort_node_wrt (#1 o #1); + val rests = restricts |> map (apfst (apfst extern_item)) |> sort_item_by (#1 o #1); in [Pretty.strs ("names:" :: Context.display_names thy)] @ [Pretty.big_list "classes:" (map pretty_classrel clsses), diff -r 066792098895 -r 8611f408ec13 src/Pure/theory.ML --- a/src/Pure/theory.ML Tue Sep 22 16:17:49 2015 +0200 +++ b/src/Pure/theory.ML Tue Sep 22 16:49:56 2015 +0200 @@ -221,14 +221,17 @@ let val thy = Proof_Context.theory_of ctxt; val consts = Sign.consts_of thy; + fun prep (DConst const) = - let val Const (c, T) = Sign.no_vars ctxt (Const const) - in (Defs.NConst c, Consts.typargs consts (c, Logic.varifyT_global T)) end + let val Const (c, T) = Sign.no_vars ctxt (Const const) + in ((Defs.Constant, 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; + let val Type (c, Ts) = Type.no_tvars (Type typ) + in ((Defs.Type, c), map Logic.varifyT_global Ts) 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 + | 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 [];