# HG changeset patch # User wenzelm # Date 1537813443 -7200 # Node ID da448868a18a2f51d966c661170b4b2c7486fe7b # Parent df6c946cb296ab6771036ddce3b5cff2defd0eb0 tuned signature: more explicit types; diff -r df6c946cb296 -r da448868a18a src/Pure/Isar/locale.ML --- a/src/Pure/Isar/locale.ML Mon Sep 24 20:05:41 2018 +0200 +++ b/src/Pure/Isar/locale.ML Mon Sep 24 20:24:03 2018 +0200 @@ -101,6 +101,11 @@ (*** Locales ***) +type dep = {name: string, morphisms: morphism * morphism, serial: serial}; + +fun make_dep (name, morphisms) : dep = + {name = name, morphisms = morphisms, serial = serial ()}; + (*table of mixin lists, per list mixins in reverse order of declaration; lists indexed by registration/dependency serial, entries for empty lists may be omitted*) @@ -140,7 +145,7 @@ (*theorem declarations*) notes: ((string * Attrib.fact list) * serial) list, (*locale dependencies (sublocale relation) in reverse order*) - dependencies: ((string * (morphism * morphism)) * serial) list, + dependencies: dep list, (*mixin part of dependencies*) mixins: mixins }; @@ -163,7 +168,7 @@ ((parameters, spec, intros, axioms, hyp_spec), ((merge (eq_snd op =) (syntax_decls, syntax_decls'), merge (eq_snd op =) (notes, notes')), - (merge (eq_snd op =) (dependencies, dependencies'), + (merge (op = o apply2 #serial) (dependencies, dependencies'), (merge_mixins (mixins, mixins'))))); structure Locales = Theory_Data @@ -194,13 +199,14 @@ SOME (Loc loc) => loc | NONE => error ("Unknown locale " ^ quote name)); -fun register_locale binding parameters spec intros axioms hyp_spec syntax_decls notes dependencies thy = +fun register_locale + binding parameters spec intros axioms hyp_spec syntax_decls notes dependencies thy = thy |> Locales.map (Name_Space.define (Context.Theory thy) true (binding, mk_locale ((parameters, spec, (apply2 o Option.map) Thm.trim_context intros, map Thm.trim_context axioms, hyp_spec), ((map (fn decl => (decl, serial ())) syntax_decls, map (fn n => (n, serial ())) notes), - (map (fn d => (d |> apsnd (rpair Morphism.identity), serial ())) dependencies, + (map (fn (name, morph) => make_dep (name, (morph, Morphism.identity))) dependencies, Inttab.empty)))) #> snd); (* FIXME Morphism.identity *) @@ -294,17 +300,15 @@ if redundant_ident thy marked (name, instance) then (deps, marked) else let - (* no inheritance of mixins, regardless of requests by clients *) - val dependencies = dependencies_of thy name |> - map (fn ((name', (morph', export')), serial') => - (name', morph' $> export' $> compose_mixins (mixins_of thy name serial'))); + (*no inheritance of mixins, regardless of requests by clients*) + val dependencies = + dependencies_of thy name |> map (fn dep as {morphisms = (morph', export'), ...} => + (#name dep, morph' $> export' $> compose_mixins (mixins_of thy name (#serial dep)))); val marked' = insert_idents (name, instance) marked; val (deps', marked'') = fold_rev (add thy (depth + 1) (morph $> stem) export) dependencies ([], marked'); - in - ((name, morph $> stem) :: deps' @ deps, marked'') - end + in ((name, morph $> stem) :: deps' @ deps, marked'') end end; in @@ -606,10 +610,10 @@ fun add_dependency loc {inst = (name, morph), mixin, export} thy = let - val serial' = serial (); + val dep = make_dep (name, (morph, export)); val add_dep = - apfst (cons ((name, (morph, export)), serial')) #> - apsnd (case mixin of NONE => I | SOME mixin => insert_mixin serial' mixin); + apfst (cons dep) #> + apsnd (case mixin of NONE => I | SOME mixin => insert_mixin (#serial dep) mixin); val thy' = change_locale loc (apsnd add_dep) thy; val context' = Context.Theory thy'; val (_, regs) = @@ -744,7 +748,7 @@ let fun make_node name = {name = name, - parents = map (fst o fst) (dependencies_of thy name), + parents = map #name (dependencies_of thy name), body = pretty_locale thy false name}; val names = sort_strings (Name_Space.fold_table (cons o #1) (Locales.get thy) []); in map make_node names end;