# HG changeset patch # User wenzelm # Date 1006904524 -3600 # Node ID 459aa05af6bea40b5d4f9febf96d25da684b55d1 # Parent 749a04f0cfb0efe5e60cda6e67c476fd6838615d qualify imported facts; clarified read/cert_element; theory data: removed obsolete finish; tuned; diff -r 749a04f0cfb0 -r 459aa05af6be src/Pure/Isar/locale.ML --- a/src/Pure/Isar/locale.ML Wed Nov 28 00:39:33 2001 +0100 +++ b/src/Pure/Isar/locale.ML Wed Nov 28 00:42:04 2001 +0100 @@ -91,7 +91,6 @@ val empty = (NameSpace.empty, Symtab.empty); val copy = I; val prep_ext = I; - val finish = I; (*joining of locale elements: only facts may be added later!*) fun join ({import, elems, params, text}: locale, {elems = elems', ...}: locale) = @@ -143,19 +142,32 @@ (* prepare elements *) -fun read_elem ctxt = +local + +fun prep_name ctxt (name, atts) = + if NameSpace.is_qualified name then + raise ProofContext.CONTEXT ("Illegal qualified name: " ^ quote name, ctxt) + else (name, atts); + +fun prep_elem prep_vars prep_propp prep_thms ctxt = fn Fixes fixes => - let val vars = - #2 (foldl_map ProofContext.read_vars (ctxt, map (fn (x, T, _) => ([x], T)) fixes)) - in Fixes (map2 (fn (([x'], T'), (_, _, mx)) => (x', T', mx)) (vars, fixes)) end + let val vars = snd (foldl_map prep_vars (ctxt, map (fn (x, T, _) => ([x], T)) fixes)) + in Fixes (map (fn (([x'], T'), (_, _, mx)) => (x', T', mx)) (vars ~~ fixes)) end | Assumes asms => - Assumes (map #1 asms ~~ #2 (ProofContext.read_propp (ctxt, map #2 asms))) + Assumes (map (prep_name ctxt o #1) asms ~~ snd (prep_propp (ctxt, map #2 asms))) | Defines defs => - let val propps = - #2 (ProofContext.read_propp (ctxt, map (fn (_, (t, ps)) => [(t, (ps, []))]) defs)) - in Defines (map #1 defs ~~ map (fn [(t', (ps', []))] => (t', ps')) propps) end + let val propps = snd (prep_propp (ctxt, map (fn (_, (t, ps)) => [(t, (ps, []))]) defs)) in + Defines (map (prep_name ctxt o #1) defs ~~ map (fn [(t', (ps', []))] => (t', ps')) propps) + end | Notes facts => - Notes (map (apsnd (map (apfst (ProofContext.get_thms ctxt)))) facts); + Notes (map (fn (a, bs) => (prep_name ctxt a, map (apfst (prep_thms ctxt)) bs)) facts); + +fun read_elem x = prep_elem ProofContext.read_vars ProofContext.read_propp ProofContext.get_thms x; +fun cert_elem x = prep_elem ProofContext.cert_vars ProofContext.cert_propp (K I) x; + +fun read_att attrib (x, srcs) = (x, map attrib srcs); + +in fun read_expr ctxt (Locale xname) = Locale (intern (ProofContext.sign_of ctxt) xname) | read_expr ctxt (Merge exprs) = Merge (map (read_expr ctxt) exprs) @@ -164,7 +176,8 @@ fun read_element ctxt (Elem e) = Elem (read_elem ctxt e) | read_element ctxt (Expr e) = Expr (read_expr ctxt e); -local fun read_att attrib (x, srcs) = (x, map attrib srcs) in +fun cert_element ctxt (Elem e) = Elem (cert_elem ctxt e) + | cert_element ctxt (Expr e) = Expr e; fun attribute _ (Elem (Fixes fixes)) = Elem (Fixes fixes) | attribute attrib (Elem (Assumes asms)) = Elem (Assumes (map (apfst (read_att attrib)) asms)) @@ -212,6 +225,18 @@ (rename_term ren t, map (rename_term ren) ps))) defs) | rename_elem ren (Notes facts) = Notes (map (apsnd (map (apfst (map (rename_thm ren))))) facts); +fun qualify_elem prfx elem = + let + fun qualify ((name, atts), x) = + ((NameSpace.pack (filter_out (equal "") (prfx @ [name])), atts), x); + in + (case elem of + Fixes fixes => Fixes fixes + | Assumes asms => Assumes (map qualify asms) + | Defines defs => Defines (map qualify defs) + | Notes facts => Notes (map qualify facts)) + end; + (* evaluation *) @@ -250,25 +275,29 @@ in (merge_lists ids ids'', merge_lists parms parms'') end | identify (arg, Merge es) = foldl identify (arg, es); - fun eval (name, ps') = + fun eval (name, xs) = let val {params = (ps, _), elems, ...} = the_locale thy name; - val ren = filter_out (op =) (map #1 ps ~~ ps'); - in - if null ren then ((name, ps), map #1 elems) - else ((name, map (apfst (rename ren)) ps), map (rename_elem ren o #1) elems) end; - (* FIXME unify types; specific errors (name) *) + val ren = filter_out (op =) (map #1 ps ~~ xs); + val (ps', elems') = + if null ren then (ps, map #1 elems) + else (map (apfst (rename ren)) ps, map (rename_elem ren o #1) elems); + in ((name, ps'), map (qualify_elem [NameSpace.base name, space_implode "_" xs]) elems') end; + + (* FIXME unify types *) val (idents, parms) = identify (([], []), expr); in (map eval idents, parms) end; -fun eval_elements ctxt = - flat o map (fn Elem e => [(("", []), [e])] | Expr e => #1 (eval_expr ctxt e)); +fun eval_element _ (Elem e) = [(("", []), [e])] + | eval_element ctxt (Expr e) = #1 (eval_expr ctxt e); (** activation **) +(* internal elems *) + fun activate_elem (Fixes fixes) = ProofContext.add_syntax fixes o ProofContext.fix_direct (map (fn (x, T, mx) => ([x], T)) fixes) | activate_elem (Assumes asms) = @@ -282,14 +311,20 @@ fun activate_elems es ctxt = foldl (fn (c, e) => activate_elem e c) (ctxt, es); -fun activate_locale_elems named_elems context = +fun activate_locale_elems named_elems = ProofContext.qualified (fn context => foldl (fn (ctxt, ((name, ps), es)) => (* FIXME type inst *) activate_elems es ctxt handle ProofContext.CONTEXT (msg, ctxt) => - err_in_locale ctxt msg [(name, map fst ps)]) (context, named_elems); + err_in_locale ctxt msg [(name, map fst ps)]) (context, named_elems)); + + +(* external elements and locales *) -fun activate_elements_i elements ctxt = activate_locale_elems (eval_elements ctxt elements) ctxt; -fun activate_elements elements ctxt = activate_elements_i (map (read_element ctxt) elements) ctxt; +fun gen_activate_elements prep_element raw_elements context = + foldl (fn (ctxt, e) => activate_locale_elems (eval_element ctxt (prep_element ctxt e)) ctxt) + (context, raw_elements); +val activate_elements = gen_activate_elements read_element; +val activate_elements_i = gen_activate_elements cert_element; val activate_locale_i = activate_elements_i o single o Expr o Locale; val activate_locale = activate_elements o single o Expr o Locale; @@ -297,37 +332,32 @@ (** print locale **) -fun pretty_locale thy raw_expr = +fun print_locale thy raw_expr = let val sg = Theory.sign_of thy; val thy_ctxt = ProofContext.init thy; val expr = read_expr thy_ctxt raw_expr; - val locale_elems = #1 (eval_expr thy_ctxt expr); - val locale_ctxt = activate_locale_elems locale_elems thy_ctxt; + val elems = #1 (eval_expr thy_ctxt expr); + val ctxt = activate_locale_elems elems thy_ctxt; - val prt_typ = Pretty.quote o ProofContext.pretty_typ locale_ctxt; - val prt_term = Pretty.quote o ProofContext.pretty_term locale_ctxt; - val prt_thm = Pretty.quote o ProofContext.pretty_thm locale_ctxt; + val prt_typ = Pretty.quote o ProofContext.pretty_typ ctxt; + val prt_term = Pretty.quote o ProofContext.pretty_term ctxt; + val prt_thm = Pretty.quote o ProofContext.pretty_thm ctxt; fun prt_syn syn = let val s = (case syn of None => "(structure)" | Some mx => Syntax.string_of_mixfix mx) in if s = "" then [] else [Pretty.brk 4, Pretty.str s] end; - fun prt_fix (x, Some T, syn) = Pretty.block (Pretty.str (x ^ " ::") :: Pretty.brk 1 :: prt_typ T :: Pretty.brk 1 :: prt_syn syn) | prt_fix (x, None, syn) = Pretty.block (Pretty.str x :: Pretty.brk 1 :: prt_syn syn); - fun prt_asm (("", _), ts) = Pretty.block (Pretty.breaks (map (prt_term o fst) ts)) - | prt_asm ((a, _), ts) = Pretty.block - (Pretty.breaks (Pretty.str (a ^ ":") :: map (prt_term o fst) ts)); - - fun prt_def (("", _), (t, _)) = Pretty.block [Pretty.brk 1, prt_term t] - | prt_def ((a, _), (t, _)) = Pretty.block [Pretty.str (a ^ ":"), Pretty.brk 1, prt_term t]; - - fun prt_fact (("", _), ths) = Pretty.block (Pretty.breaks (map prt_thm (flat (map fst ths)))) - | prt_fact ((a, _), ths) = Pretty.block - (Pretty.breaks (Pretty.str (a ^ ":") :: map prt_thm (flat (map fst ths)))); + fun prt_name "" = [Pretty.brk 1] + | prt_name name = [Pretty.str (ProofContext.cond_extern ctxt name ^ ":"), Pretty.brk 1]; + fun prt_asm ((a, _), ts) = Pretty.block (prt_name a @ Pretty.breaks (map (prt_term o fst) ts)); + fun prt_def ((a, _), (t, _)) = Pretty.block (prt_name a @ [prt_term t]); + fun prt_fact ((a, _), ths) = Pretty.block + (prt_name a @ Pretty.breaks (map prt_thm (flat (map fst ths)))); fun items _ [] = [] | items prfx (x :: xs) = Pretty.block [Pretty.str prfx, Pretty.brk 1, x] :: items " and" xs; @@ -336,12 +366,10 @@ | prt_elem (Defines defs) = items "defines" (map prt_def defs) | prt_elem (Notes facts) = items "notes" (map prt_fact facts); in - Pretty.big_list "locale elements:" - (map (Pretty.chunks o prt_elem) (flat (map #2 locale_elems))) + Pretty.big_list "locale elements:" (map (Pretty.chunks o prt_elem) (flat (map #2 elems))) + |> Pretty.writeln end; -val print_locale = Pretty.writeln oo pretty_locale; - (** define locales **) @@ -381,7 +409,7 @@ fun prep (ctxt, raw_element) = let val elems = map (apsnd (map (closeup ctxt))) - (eval_elements ctxt [prep_element ctxt raw_element]) + (eval_element ctxt (prep_element ctxt raw_element)) in (activate_locale_elems elems ctxt, flat (map #2 elems)) end; val (locale_ctxt, elemss) = foldl_map prep (import_ctxt, raw_elements);