# HG changeset patch # User ballarin # Date 1142585845 -3600 # Node ID 4d762b77d319d5684982e0dd455e6f6bf964419c # Parent f7602e74d9489d6d57dab4d2a3832e1ade2fe0d4 Internal restructuring: local parameters. diff -r f7602e74d948 -r 4d762b77d319 src/Pure/Isar/locale.ML --- a/src/Pure/Isar/locale.ML Fri Mar 17 09:34:23 2006 +0100 +++ b/src/Pure/Isar/locale.ML Fri Mar 17 09:57:25 2006 +0100 @@ -148,7 +148,8 @@ *) import: expr, (*dynamic import*) elems: (Element.context_i * stamp) list, (*static content*) - params: ((string * typ) * mixfix) list * string list, (*all/local params*) + params: ((string * typ) * mixfix) list, (*all params*) + lparams: string list, (*local parmas*) abbrevs: ((bool * (bstring * term * mixfix) list) * stamp) list, (*abbreviations*) regs: ((string * string list) * (term * thm) list) list} (* Registrations: indentifiers and witness theorems of locales interpreted @@ -266,12 +267,13 @@ val copy = I; val extend = I; - fun join_locs _ ({predicate, import, elems, params, abbrevs, regs}: locale, + fun join_locs _ ({predicate, import, elems, params, lparams, abbrevs, regs}: locale, {elems = elems', abbrevs = abbrevs', regs = regs', ...}: locale) = {predicate = predicate, import = import, elems = gen_merge_lists (eq_snd (op =)) elems elems', params = params, + lparams = lparams, abbrevs = Library.merge (eq_snd (op =)) (abbrevs, abbrevs'), regs = merge_alists regs regs'}; fun merge _ ((space1, locs1, regs1), (space2, locs2, regs2)) = @@ -325,12 +327,12 @@ fun change_locale name f thy = let - val {predicate, import, elems , params, abbrevs, regs} = the_locale thy name; - val (predicate', import', elems', params', abbrevs', regs') = - f (predicate, import, elems, params, abbrevs, regs); + val {predicate, import, elems, params, lparams, abbrevs, regs} = the_locale thy name; + val (predicate', import', elems', params', lparams', abbrevs', regs') = + f (predicate, import, elems, params, lparams, abbrevs, regs); in put_locale name {predicate = predicate', import = import', elems = elems', - params = params', abbrevs = abbrevs', regs = regs'} thy + params = params', lparams = lparams', abbrevs = abbrevs', regs = regs'} thy end; @@ -395,8 +397,8 @@ gen_put_registration LocalLocalesData.map ProofContext.theory_of; fun put_registration_in_locale name id = - change_locale name (fn (predicate, import, elems, params, abbrevs, regs) => - (predicate, import, elems, params, abbrevs, regs @ [(id, [])])); + change_locale name (fn (predicate, import, elems, params, lparams, abbrevs, regs) => + (predicate, import, elems, params, lparams, abbrevs, regs @ [(id, [])])); (* add witness theorem to registration in theory or context, @@ -411,11 +413,11 @@ val add_local_witness = LocalLocalesData.map oo add_witness; fun add_witness_in_locale name id thm = - change_locale name (fn (predicate, import, elems, params, abbrevs, regs) => + change_locale name (fn (predicate, import, elems, params, lparams, abbrevs, regs) => let fun add (id', thms) = if id = id' then (id', thm :: thms) else (id', thms); - in (predicate, import, elems, params, abbrevs, map add regs) end); + in (predicate, import, elems, params, lparams, abbrevs, map add regs) end); (* printing of registrations *) @@ -696,7 +698,7 @@ fun add_regs (name, ps) (ths, ids) = let val {params, regs, ...} = the_locale thy name; - val ps' = map #1 (#1 params); + val ps' = map #1 params; val ren = map #1 ps' ~~ map (fn (x, _) => (x, NONE)) ps; (* dummy syntax, since required by rename *) val ps'' = map (fn ((p, _), (_, T)) => (p, T)) (ps ~~ ps'); @@ -742,16 +744,16 @@ let val {predicate = (_, axioms), import, params, ...} = the_locale thy name; - val ps = map (#1 o #1) (#1 params); + val ps = map (#1 o #1) params; val (ids', parms', _) = identify false import; (* acyclic import dependencies *) val ids'' = ids' @ [((name, ps), ([], Assumed []))]; - val (_, ids''') = add_regs (name, map #1 (#1 params)) ([], ids''); + val (_, ids''') = add_regs (name, map #1 params) ([], ids''); val ids_ax = if top then fst (fold_map (axiomify ps) ids''' axioms) else ids'''; - val syn = Symtab.make (map (apfst fst) (#1 params)); + val syn = Symtab.make (map (apfst fst) params); in (ids_ax, merge_lists parms' ps, syn) end | identify top (Rename (e, xs)) = let @@ -782,7 +784,7 @@ fun eval syn ((name, xs), axs) = let - val {params = (ps, qs), elems, ...} = the_locale thy name; + val {params = ps, lparams = qs, elems, ...} = the_locale thy name; val ps' = map (apsnd SOME o #1) ps; fun lookup_syn x = (case Symtab.lookup syn x of SOME Structure => NONE | opt => opt); val ren = map #1 ps' ~~ map (fn x => (x, lookup_syn x)) xs; @@ -1275,7 +1277,7 @@ in fun parameters_of thy name = - the_locale thy name |> #params |> fst; + the_locale thy name |> #params; fun parameters_of_expr thy expr = let @@ -1343,7 +1345,7 @@ (case locale of NONE => ([], [], empty) | SOME name => - let val {predicate = (stmt, _), params = (ps, _), ...} = the_locale thy name + let val {predicate = (stmt, _), params = ps, ...} = the_locale thy name in (stmt, map fst ps, Locale name) end); val ((((locale_ctxt, _), (elems_ctxt, _, _)), _), (elems_stmt, concl')) = prep_ctxt false fixed_params import elems concl ctxt; @@ -1424,7 +1426,7 @@ fun note_thmss_registrations kind target args thy = let - val parms = the_locale thy target |> #params |> fst |> map fst; + val parms = the_locale thy target |> #params |> map fst; val ids = flatten (ProofContext.init thy, intern_expr thy) (([], Symtab.empty), Expr (Locale target)) |> fst |> fst |> List.mapPartial (fn (id, (_, Assumed _)) => SOME id | _ => NONE) @@ -1452,8 +1454,8 @@ fun add_abbrevs loc revert decls = snd #> ProofContext.add_abbrevs_i revert decls #> ProofContext.map_theory (change_locale loc - (fn (predicate, import, elems, params, abbrevs, regs) => - (predicate, import, elems, params, ((revert, decls), stamp ()) :: abbrevs, regs))); + (fn (predicate, import, elems, params, lparams, abbrevs, regs) => + (predicate, import, elems, params, lparams, ((revert, decls), stamp ()) :: abbrevs, regs))); fun init_abbrevs loc ctxt = fold_rev (uncurry ProofContext.add_abbrevs_i o fst) @@ -1482,8 +1484,8 @@ activate_facts prep_facts (ctxt, [((("", []), Assumed []), [Ext (Notes args)])]); val (facts', thy') = thy - |> change_locale loc (fn (predicate, import, elems, params, abbrevs, regs) => - (predicate, import, elems @ [(Notes args', stamp ())], params, abbrevs, regs)) + |> change_locale loc (fn (predicate, import, elems, params, lparams, abbrevs, regs) => + (predicate, import, elems @ [(Notes args', stamp ())], params, lparams, abbrevs, regs)) |> note_thmss_registrations kind loc args' |> global_results (map (#1 o #1) args' ~~ map #2 facts) (view, ctxt); in ((facts, facts'), (ProofContext.transfer thy' ctxt', thy')) end; @@ -1702,8 +1704,8 @@ {predicate = predicate, import = import, elems = map (fn e => (e, stamp ())) elems', - params = (params_of elemss' |> map (fn (x, SOME T) => ((x, T), the (Symtab.lookup syn x))), - map #1 (params_of body_elemss)), + params = params_of elemss' |> map (fn (x, SOME T) => ((x, T), the (Symtab.lookup syn x))), + lparams = map #1 (params_of body_elemss), abbrevs = [], regs = []}; in (ProofContext.transfer thy' body_ctxt, thy') end; @@ -2008,7 +2010,7 @@ val ctxt = ProofContext.init thy; val ((raw_target_ids, target_syn), _) = flatten (ctxt, I) (([], Symtab.empty), Expr (Locale target)); - val fixed = the_locale thy target |> #params |> #1 |> map #1; + val fixed = the_locale thy target |> #params |> map #1; val ((all_ids, syn), raw_elemss) = flatten (ctxt, intern_expr thy) ((raw_target_ids, target_syn), Expr expr); val (target_ids, ids) = chop (length raw_target_ids) all_ids;