# HG changeset patch # User wenzelm # Date 1006539606 -3600 # Node ID 2b28d7dd91f5bfda119900fe01d1c595facbf03c # Parent 7bafe3d6c248194192cd45dd632e9ddc2c0bd5ea improved ordering of evaluated elements; diff -r 7bafe3d6c248 -r 2b28d7dd91f5 src/Pure/Isar/locale.ML --- a/src/Pure/Isar/locale.ML Fri Nov 23 19:19:35 2001 +0100 +++ b/src/Pure/Isar/locale.ML Fri Nov 23 19:20:06 2001 +0100 @@ -34,7 +34,6 @@ type 'att element type 'att element_i type locale - val the_locale: theory -> string -> locale (* FIXME *) val intern: Sign.sg -> xstring -> string val cond_extern: Sign.sg -> string -> xstring val attribute: ('att -> context attribute) -> ('typ, 'term, 'thm, 'att) elem_expr @@ -49,7 +48,7 @@ val setup: (theory -> theory) list end; -structure Locale: LOCALE = +structure Locale(* FIXME : LOCALE *) = struct @@ -110,6 +109,9 @@ structure LocalesData = TheoryDataFun(LocalesArgs); val print_locales = LocalesData.print; + +(* access locales *) + fun declare_locale name = LocalesData.map (apfst (fn space => (NameSpace.extend (space, [name])))); @@ -121,17 +123,30 @@ Some loc => loc | None => error ("Unknown locale " ^ quote name)); +val intern = NameSpace.intern o #1 o LocalesData.get_sg; -(** internalization **) +(* diagnostics *) -(* names *) - -val intern = NameSpace.intern o #1 o LocalesData.get_sg; val cond_extern = NameSpace.cond_extern o #1 o LocalesData.get_sg; +fun err_in_locale ctxt msg ids = + let + val sg = ProofContext.sign_of ctxt; + fun prt_id (name, parms) = Pretty.block (Pretty.breaks + (Pretty.str (cond_extern sg name) :: map (Pretty.str o fst) parms)); + val prt_ids = flat (separate [Pretty.str " +", Pretty.brk 1] (map (single o prt_id) ids)); + in + if null ids then raise ProofContext.CONTEXT (msg, ctxt) + else raise ProofContext.CONTEXT (msg ^ "\n" ^ Pretty.string_of (Pretty.block + (Pretty.str "The error(s) above occurred in locale:" :: Pretty.brk 1 :: prt_ids)), ctxt) + end; -(* read *) + + +(** operations on locale elements **) + +(* internalization *) fun read_elem ctxt = fn Fixes fixes => @@ -156,23 +171,19 @@ fun read_element ctxt (Elem e) = Elem (read_elem ctxt e) | read_element ctxt (Expr e) = Expr (read_expr ctxt e); - -(* attribute *) - -local fun int_att attrib (x, srcs) = (x, map attrib srcs) in +local fun read_att attrib (x, srcs) = (x, map attrib srcs) in fun attribute _ (Elem (Fixes fixes)) = Elem (Fixes fixes) - | attribute attrib (Elem (Assumes asms)) = Elem (Assumes (map (apfst (int_att attrib)) asms)) - | attribute attrib (Elem (Defines defs)) = Elem (Defines (map (apfst (int_att attrib)) defs)) + | attribute attrib (Elem (Assumes asms)) = Elem (Assumes (map (apfst (read_att attrib)) asms)) + | attribute attrib (Elem (Defines defs)) = Elem (Defines (map (apfst (read_att attrib)) defs)) | attribute attrib (Elem (Notes facts)) = - Elem (Notes (map (apfst (int_att attrib) o apsnd (map (int_att attrib))) facts)) + Elem (Notes (map (apfst (read_att attrib) o apsnd (map (read_att attrib))) facts)) | attribute _ (Expr expr) = Expr expr; end; - -(** renaming **) +(* renaming *) fun rename ren x = if_none (assoc_string (ren, x)) x; @@ -209,52 +220,50 @@ | rename_elem ren (Notes facts) = Notes (map (apsnd (map (apfst (map (rename_thm ren))))) facts); - -(** evaluation **) +(* evaluation *) fun eval_expr ctxt expr = let val thy = ProofContext.theory_of ctxt; - fun renaming (Some x :: xs) (y :: ys) = (y, x) :: renaming xs ys - | renaming (None :: xs) (y :: ys) = renaming xs ys + fun renaming (Some x :: xs) ((y, _) :: ys) = (y, x) :: renaming xs ys + | renaming (None :: xs) ((y, _) :: ys) = renaming xs ys | renaming [] _ = [] | renaming xs [] = raise ProofContext.CONTEXT ("Extraneous arguments in renaming: " ^ commas (map (fn None => "_" | Some x => quote x) xs), ctxt); fun identify ((ids, parms), Locale name) = - let - val {import, params, ...} = the_locale thy name; - val ps = map #1 (#1 params); - in + let val {import, params = (ps, _), ...} = the_locale thy name in if (name, ps) mem ids then (ids, parms) - else identify (((name, ps) :: ids, merge_lists parms ps), import) + else + let val (ids', parms') = identify ((ids, parms), import) (*acyclic dependencies!*) + in ((name, ps) :: ids', merge_lists parms' ps) end end | identify ((ids, parms), Rename (e, xs)) = let val (ids', parms') = identify (([], []), e); - val ren = renaming xs parms'; - val ids'' = map (apsnd (map (rename ren))) ids' \\ ids; - in (ids'' @ ids, merge_lists parms (map (rename ren) parms')) end + val ren = renaming xs parms' + handle ProofContext.CONTEXT (msg, ctxt) => err_in_locale ctxt msg ids'; + val ids'' = map (apsnd (map (apfst (rename ren)))) ids' \\ ids;(* FIXME merge_lists' *) + in (ids'' @ ids, merge_lists parms (map (apfst (rename ren)) parms')) end | identify (arg, Merge es) = foldl identify (arg, es); - val idents = rev (#1 (identify (([], []), expr))); + val (idents, parms) = identify (([], []), expr); + val idents = rev idents; val FIXME = PolyML.print idents; + val FIXME = PolyML.print parms; fun eval (name, ps') = 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), elems) - else ((name, map (apfst (rename ren)) ps), map (rename_elem ren) elems) - end; + val ren = filter_out (op =) (map fst ps ~~ map fst ps'); + in ((name, ps'), if null ren then elems else map (rename_elem ren) elems) end; (* FIXME unify types; specific errors (name) *) - in map eval idents end; + in (map eval idents, parms) end; fun eval_elements ctxt = - flat o map (fn Elem e => [e] | Expr e => flat (map #2 (eval_expr ctxt e))); + flat o map (fn Elem e => [(("", []), [e])] | Expr e => #1 (eval_expr ctxt e)); @@ -273,11 +282,16 @@ fun activate_elems es ctxt = foldl (fn (c, e) => activate_elem e c) (ctxt, es); -fun activate_elements_i elements ctxt = activate_elems (eval_elements ctxt elements) ctxt; +fun activate_locale_elems named_elems context = + foldl (fn (ctxt, ((name, ps), es)) => + activate_elems es ctxt handle ProofContext.CONTEXT (msg, ctxt) => + err_in_locale ctxt msg [(name, ps)]) (context, named_elems); + +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 activate_locale_i name = activate_elements_i [Expr (Locale name)]; -fun activate_locale xname = activate_elements [Expr (Locale xname)]; +val activate_locale_i = activate_elements_i o single o Expr o Locale; +val activate_locale = activate_elements o single o Expr o Locale; @@ -288,7 +302,10 @@ val sg = Theory.sign_of thy; val name = intern sg xname; val {import, elems, params = _, text = _, closed = _} = the_locale thy name; - val locale_ctxt = ProofContext.init thy |> activate_locale_i name; + + val thy_ctxt = ProofContext.init thy; + val locale_elems = #1 (eval_expr thy_ctxt (Locale name)); + val locale_ctxt = activate_locale_elems locale_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; @@ -329,7 +346,10 @@ val prt_header = Pretty.block (Pretty.str ("locale " ^ cond_extern sg name ^ " =") :: (if import = empty then [] else [Pretty.str " ", prt_expr import] @ (if null elems then [] else [Pretty.str " +"]) @ [Pretty.brk 1])); - in Pretty.block (Pretty.fbreaks (prt_header :: map prt_elem elems)) end; + in + Pretty.chunks [Pretty.block (Pretty.fbreaks (prt_header :: map prt_elem elems)), + Pretty.big_list "locale elements:" (map prt_elem (flat (map #2 locale_elems)))] + end; val print_locale = Pretty.writeln oo pretty_locale; @@ -337,7 +357,7 @@ (** define locales **) -(* closeup dangling frees *) +(* closeup -- quantify dangling frees *) fun close_frees_wrt ctxt t = let val frees = rev (filter_out (ProofContext.is_fixed ctxt o #1) (Drule.add_frees ([], t))) @@ -367,23 +387,24 @@ val thy_ctxt = ProofContext.init thy; val import = prep_expr thy_ctxt raw_import; - val (import_ids, import_elemss) = split_list (eval_expr thy_ctxt import); - val import_ctxt = activate_elems (flat import_elemss) thy_ctxt; + val (import_elems, import_params) = eval_expr thy_ctxt import; + val import_ctxt = activate_locale_elems import_elems thy_ctxt; fun prep (ctxt, raw_element) = - let val elems = map (closeup ctxt) (eval_elements ctxt [prep_element ctxt raw_element]); - in (activate_elems elems ctxt, elems) end; + let val elems = map (apsnd (map (closeup ctxt))) + (eval_elements 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); val elems = flat elemss; - val local_ps = (* FIXME proper types *) + val local_params = (* FIXME lookup final types *) flat (map (fn Fixes fixes => map (fn (x, T, _) => (x, T)) fixes | _ => []) elems); - val all_ps = distinct (flat (map #2 import_ids)) @ local_ps; + val all_params = import_params @ local_params; val text = ([], []); (* FIXME *) in thy |> declare_locale name - |> put_locale name (make_locale import elems (all_ps, local_ps) text false) + |> put_locale name (make_locale import elems (all_params, local_params) text false) end; val add_locale = gen_add_locale read_expr read_element;