# HG changeset patch # User wenzelm # Date 1005153499 -3600 # Node ID 1b890f1e0b4d2f8f929d9cc3af0ff2b32b3ad080 # Parent d1896409ff1311e93ad56227b9b201158c3b659d syntax for structures; diff -r d1896409ff13 -r 1b890f1e0b4d src/Pure/Isar/proof_context.ML --- a/src/Pure/Isar/proof_context.ML Wed Nov 07 18:17:45 2001 +0100 +++ b/src/Pure/Isar/proof_context.ML Wed Nov 07 18:18:19 2001 +0100 @@ -13,7 +13,7 @@ exception CONTEXT of string * context val theory_of: context -> theory val sign_of: context -> Sign.sg - val syntax_of: context -> Syntax.syntax * string list * string list (* FIXME *) + val syntax_of: context -> Syntax.syntax * string list * string list val fixed_names_of: context -> string list val assumptions_of: context -> (cterm list * exporter) list val prems_of: context -> thm list @@ -274,6 +274,87 @@ + +(** local syntax **) + +val fixedN = "\\<^fixed>"; +val structN = "\\<^struct>"; + + +(* add_syntax and syn_of *) + +local + +val aT = TFree ("'a", logicS); + +fun mixfix x None mx = (fixedN ^ x, replicate (Syntax.mixfix_args mx) aT ---> aT, mx) + | mixfix x (Some T) mx = (fixedN ^ x, T, mx); + +fun prep_mixfix (_, _, None) = None + | prep_mixfix (x, opt_T, Some mx) = Some (mixfix x opt_T mx); + +fun prep_mixfix' (_, _, None) = None + | prep_mixfix' (x, _, Some Syntax.NoSyn) = None + | prep_mixfix' (x, opt_T, _) = Some (x, mixfix x opt_T (Syntax.Delimfix x)); + +fun fixed_tr x = (fixedN ^ x, curry Term.list_comb (Syntax.free x)); + +fun index_tr (Const ("_structs", _) $ Const ("_struct", _) $ idx) = index_tr idx + 1 + | index_tr (Const ("_struct", _)) = 0 + | index_tr t = raise TERM ("index_tr", [t]); + +fun struct_app_tr structs [idx, f] = + let val i = index_tr idx in + if i < length structs then f $ Syntax.free (Library.nth_elem (i, structs)) + else error ("Illegal reference to structure #" ^ string_of_int (i + 1)) + end + | struct_app_tr _ ts = raise TERM ("struct_app_tr", ts); + +fun prep_struct (x, _, None) = Some x + | prep_struct _ = None; + +in + +fun add_syntax decls = + map_context (fn (thy, (syn, structs, mixfixed), data, asms, binds, thms, cases, defs) => + let + val structs' = structs @ mapfilter prep_struct decls; + val mxs = mapfilter prep_mixfix decls; + val (fixed, mxs_output) = Library.split_list (mapfilter prep_mixfix' decls); + val trs = map fixed_tr fixed; + val syn' = syn + |> Syntax.extend_const_gram ("", false) mxs_output + |> Syntax.extend_const_gram ("", true) mxs + |> Syntax.extend_trfuns ([], trs, [], []); + in (thy, (syn', structs', fixed @ mixfixed), data, asms, binds, thms, cases, defs) end) + +fun syn_of (Context {syntax = (syn, structs, _), ...}) = + syn |> Syntax.extend_trfuns ([], [("_struct_app", struct_app_tr structs)], [], []); + + +end; + + +(* context_tr' *) + +fun context_tr' (Context {syntax = (_, structs, mixfixed), ...}) = + let + fun structs_tr' 0 t = t + | structs_tr' i t = Syntax.const "_structs" $ Syntax.const "_struct" $ structs_tr' (i - 1) t; + + fun tr' (f $ (t as Free (x, T))) = + let val i = Library.find_index (equal x) structs in + if i < 0 then tr' f $ tr' t + else Syntax.const "_struct_app" $ structs_tr' i (Syntax.const "_struct") $ f + end + | tr' (t as Free (x, T)) = if x mem_string mixfixed then Const (fixedN ^ x, T) else t + | tr' (t $ u) = tr' t $ tr' u + | tr' (Abs (x, T, t)) = Abs (x, T, tr' t) + | tr' a = a; + in tr' end; + + + (** default sorts and types **) fun def_sort (Context {defs = (_, sorts, _), ...}) xi = Vartab.lookup (sorts, xi); @@ -294,7 +375,7 @@ local fun read_typ_aux read ctxt s = - transform_error (read (#1 (syntax_of ctxt)) (sign_of ctxt, def_sort ctxt)) s + transform_error (read (syn_of ctxt) (sign_of ctxt, def_sort ctxt)) s handle ERROR_MESSAGE msg => raise CONTEXT (msg, ctxt); fun cert_typ_aux cert ctxt raw_T = @@ -436,7 +517,7 @@ local fun gen_read read app is_pat schematic (ctxt as Context {defs = (_, _, (used, _)), ...}) s = - (transform_error (read (#1 (syntax_of ctxt)) + (transform_error (read (syn_of ctxt) (sign_of ctxt) (def_type ctxt is_pat, def_sort ctxt, used)) s handle TERM (msg, _) => raise CONTEXT (msg, ctxt) | ERROR_MESSAGE msg => raise CONTEXT (msg, ctxt)) @@ -529,69 +610,9 @@ -(** local syntax **) - -val fixedN = "\\<^fixed>"; -val structN = "\\<^struct>"; - - -(* add_syntax *) - -local - -val aT = TFree ("'a", logicS); - -fun mixfix x None mx = (fixedN ^ x, replicate (Syntax.mixfix_args mx) aT ---> aT, mx) - | mixfix x (Some T) mx = (fixedN ^ x, T, mx); - -fun prep_mixfix (_, _, None) = None - | prep_mixfix (x, opt_T, Some mx) = Some (mixfix x opt_T mx); - -fun prep_mixfix' (_, _, None) = None - | prep_mixfix' (x, _, Some Syntax.NoSyn) = None - | prep_mixfix' (x, opt_T, _) = Some (x, mixfix x opt_T (Syntax.Delimfix x)); - -fun fixed_tr x = (fixedN ^ x, curry Term.list_comb (Syntax.free x)); - -fun prep_struct (x, _, None) = Some x - | prep_struct _ = None; - -in - -fun add_syntax decls = - map_context (fn (thy, (syn, structs, mixfixed), data, asms, binds, thms, cases, defs) => - let - val structs' = mapfilter prep_struct decls @ structs; - val mxs = mapfilter prep_mixfix decls; - val (fixed, mxs_output) = Library.split_list (mapfilter prep_mixfix' decls); - val trs = map fixed_tr fixed; - val syn' = syn - |> Syntax.extend_const_gram ("", false) mxs_output - |> Syntax.extend_const_gram ("", true) mxs - |> Syntax.extend_trfuns ([], trs, [], []); - in (thy, (syn', structs', fixed @ mixfixed), data, asms, binds, thms, cases, defs) end) - -end; - - -(* annotate_term *) (* FIXME structs *) - -fun annotate_term ctxt = - let - val (_, structs, mixfixed) = syntax_of ctxt; - fun annotate (t as Free (x, T)) = if x mem_string mixfixed then Const (fixedN ^ x, T) else t - | annotate (t $ u) = annotate t $ annotate u - | annotate (Abs (x, T, t)) = Abs (x, T, annotate t) - | annotate a = a; - in annotate end; - - - (** pretty printing **) -fun pretty_term ctxt = - Sign.pretty_term' (#1 (syntax_of ctxt)) (sign_of ctxt) o annotate_term ctxt; - +fun pretty_term ctxt = Sign.pretty_term' (syn_of ctxt) (sign_of ctxt) o context_tr' ctxt; val pretty_typ = Sign.pretty_typ o sign_of; val pretty_sort = Sign.pretty_sort o sign_of; @@ -953,7 +974,6 @@ err "Element to be defined occurs on rhs"); conditional (not (null extra_frees)) (fn () => err ("Extra free variables on rhs: " ^ commas_quote (map (#1 o dest_Free) extra_frees))); - (* FIXME check for extra type variables on rhs *) (c, Term.list_all_free (mapfilter (try Term.dest_Free) xs, eq)) end; @@ -1135,7 +1155,7 @@ (* local syntax *) -val print_syntax = Syntax.print_syntax o #1 o syntax_of; +val print_syntax = Syntax.print_syntax o syn_of; (* term bindings *) @@ -1208,25 +1228,31 @@ let val prt_term = pretty_term ctxt; + (*structures*) + val (_, structs, _) = syntax_of ctxt; + val prt_structs = if null structs then [] + else [Pretty.block (Pretty.str "structures:" :: Pretty.brk 1 :: + Pretty.commas (map Pretty.str structs))]; + (*fixes*) fun prt_fix (x, x') = if x = x' then Pretty.str x else Pretty.block [Pretty.str x, Pretty.str " =", Pretty.brk 1, prt_term (Syntax.free x')]; - fun prt_fixes [] = [] - | prt_fixes xs = [Pretty.block (Pretty.str "fixed variables:" :: Pretty.brk 1 :: - Pretty.commas (map prt_fix xs))]; + val fixes = rev (filter_out + ((can Syntax.dest_internal o #1) orf (fn (_, x') => x' mem_string structs)) (fixes_of ctxt)); + val prt_fixes = if null fixes then [] + else [Pretty.block (Pretty.str "fixed variables:" :: Pretty.brk 1 :: + Pretty.commas (map prt_fix fixes))]; (*prems*) val limit = ! prems_limit; val prems = prems_of ctxt; val len = length prems; - val prt_prems = - (if len <= limit then [] else [Pretty.str "..."]) @ - map (pretty_thm ctxt) (Library.drop (len - limit, prems)); - in - prt_fixes (rev (filter_out (can Syntax.dest_internal o #1) (fixes_of ctxt))) @ - (if null prems then [] else [Pretty.big_list "prems:" prt_prems]) - end; + val prt_prems = if null prems then [] + else [Pretty.big_list "prems:" ((if len <= limit then [] else [Pretty.str "..."]) @ + map (pretty_thm ctxt) (Library.drop (len - limit, prems)))]; + + in prt_structs @ prt_fixes @ prt_prems end; (* main context *)