# HG changeset patch # User wenzelm # Date 1005071346 -3600 # Node ID 4281198fb8cd461e8f7134292b839839ed106097 # Parent 3ef642b449da9017df3abdb6b41504167bdcaf15 local syntax: add_syntax, proper read/pretty functions; diff -r 3ef642b449da -r 4281198fb8cd src/Pure/Isar/proof_context.ML --- a/src/Pure/Isar/proof_context.ML Tue Nov 06 19:28:11 2001 +0100 +++ b/src/Pure/Isar/proof_context.ML Tue Nov 06 19:29:06 2001 +0100 @@ -13,6 +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 fixed_names_of: context -> string list val assumptions_of: context -> (cterm list * exporter) list val prems_of: context -> thm list @@ -100,6 +101,7 @@ val add_cases: (string * RuleCases.T) list -> context -> context val apply_case: RuleCases.T -> context -> context * ((indexname * term option) list * term list) val show_hyps: bool ref + val add_syntax: (string * typ option * mixfix option) list -> context -> context val pretty_term: context -> term -> Pretty.T val pretty_typ: context -> typ -> Pretty.T val pretty_sort: context -> sort -> Pretty.T @@ -108,6 +110,7 @@ val string_of_term: context -> term -> string val verbose: bool ref val setmp_verbose: ('a -> 'b) -> 'a -> 'b + val print_syntax: context -> unit val print_binds: context -> unit val print_lthms: context -> unit val print_cases: context -> unit @@ -137,32 +140,34 @@ datatype context = Context of - {thy: theory, (*current theory*) - data: Object.T Symtab.table, (*user data*) + {thy: theory, (*current theory*) + syntax: Syntax.syntax * string list * string list, (*syntax with structs and mixfixed*) + data: Object.T Symtab.table, (*user data*) asms: - ((cterm list * exporter) list * (*assumes: A ==> _*) + ((cterm list * exporter) list * (*assumes: A ==> _*) (string * thm list) list) * - ((string * string) list * string list), (*fixes: !!x. _*) - binds: (term * typ) option Vartab.table, (*term bindings*) - thms: thm list option Symtab.table, (*local thms*) - cases: (string * RuleCases.T) list, (*local contexts*) + ((string * string) list * string list), (*fixes: !!x. _*) + binds: (term * typ) option Vartab.table, (*term bindings*) + thms: thm list option Symtab.table, (*local thms*) + cases: (string * RuleCases.T) list, (*local contexts*) defs: - typ Vartab.table * (*type constraints*) - sort Vartab.table * (*default sorts*) - (string list * term list Symtab.table)}; (*used type variables*) + typ Vartab.table * (*type constraints*) + sort Vartab.table * (*default sorts*) + (string list * term list Symtab.table)}; (*used type variables*) exception CONTEXT of string * context; -fun make_context (thy, data, asms, binds, thms, cases, defs) = - Context {thy = thy, data = data, asms = asms, binds = binds, thms = thms, - cases = cases, defs = defs}; +fun make_context (thy, syntax, data, asms, binds, thms, cases, defs) = + Context {thy = thy, syntax = syntax, data = data, asms = asms, binds = binds, + thms = thms, cases = cases, defs = defs}; -fun map_context f (Context {thy, data, asms, binds, thms, cases, defs}) = - make_context (f (thy, data, asms, binds, thms, cases, defs)); +fun map_context f (Context {thy, syntax, data, asms, binds, thms, cases, defs}) = + make_context (f (thy, syntax, data, asms, binds, thms, cases, defs)); fun theory_of (Context {thy, ...}) = thy; val sign_of = Theory.sign_of o theory_of; +fun syntax_of (Context {syntax, ...}) = syntax; fun fixes_of (Context {asms = (_, (fixes, _)), ...}) = fixes; val fixed_names_of = map #2 o fixes_of; @@ -254,16 +259,17 @@ fun put_data kind f x ctxt = (lookup_data ctxt kind; - ctxt |> map_context (fn (thy, data, asms, binds, thms, cases, defs) => - (thy, Symtab.update ((Object.name_of_kind kind, f x), data), asms, binds, thms, cases, defs))); + map_context (fn (thy, syntax, data, asms, binds, thms, cases, defs) => + (thy, syntax, Symtab.update ((Object.name_of_kind kind, f x), data), + asms, binds, thms, cases, defs)) ctxt); (* init context *) fun init thy = let val data = Symtab.map (fn (_, (f, _)) => f thy) (ProofDataData.get thy) in - make_context (thy, data, (([], []), ([], [])), Vartab.empty, Symtab.empty, [], - (Vartab.empty, Vartab.empty, ([], Symtab.empty))) + make_context (thy, (Theory.syn_of thy, [], []), data, (([], []), ([], [])), Vartab.empty, + Symtab.empty, [], (Vartab.empty, Vartab.empty, ([], Symtab.empty))) end; @@ -288,7 +294,7 @@ local fun read_typ_aux read ctxt s = - transform_error (read (sign_of ctxt, def_sort ctxt)) s + transform_error (read (#1 (syntax_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 = @@ -297,8 +303,8 @@ in -val read_typ = read_typ_aux Sign.read_typ; -val read_typ_no_norm = read_typ_aux Sign.read_typ_no_norm; +val read_typ = read_typ_aux Sign.read_typ'; +val read_typ_no_norm = read_typ_aux Sign.read_typ_no_norm'; val cert_typ = cert_typ_aux Sign.certify_typ; val cert_typ_no_norm = cert_typ_aux Sign.certify_typ_no_norm; @@ -356,16 +362,20 @@ (* read / certify wrt. signature *) (*exception ERROR*) (*exception TERM*) -fun read_def_termTs freeze sg (types, sorts, used) sTs = - Sign.read_def_terms (sg, types, sorts) used freeze sTs; +fun read_def_termTs freeze syn sg (types, sorts, used) sTs = + Sign.read_def_terms' syn (sg, types, sorts) used freeze sTs; -fun read_def_termT freeze sg defs sT = apfst hd (read_def_termTs freeze sg defs [sT]); +fun read_def_termT freeze syn sg defs sT = apfst hd (read_def_termTs freeze syn sg defs [sT]); -fun read_term_sg freeze sg defs s = #1 (read_def_termT freeze sg defs (s, TypeInfer.logicT)); -fun read_prop_sg freeze sg defs s = #1 (read_def_termT freeze sg defs (s, propT)); -fun read_terms_sg freeze sg defs = - #1 o read_def_termTs freeze sg defs o map (rpair TypeInfer.logicT); -fun read_props_sg freeze sg defs = #1 o read_def_termTs freeze sg defs o map (rpair propT); +fun read_term_sg freeze syn sg defs s = + #1 (read_def_termT freeze syn sg defs (s, TypeInfer.logicT)); + +fun read_prop_sg freeze syn sg defs s = #1 (read_def_termT freeze syn sg defs (s, propT)); + +fun read_terms_sg freeze syn sg defs = + #1 o read_def_termTs freeze syn sg defs o map (rpair TypeInfer.logicT); + +fun read_props_sg freeze syn sg defs = #1 o read_def_termTs freeze syn sg defs o map (rpair propT); fun cert_term_sg sg t = Thm.term_of (Thm.cterm_of sg t); @@ -426,7 +436,8 @@ local fun gen_read read app is_pat schematic (ctxt as Context {defs = (_, _, (used, _)), ...}) s = - (transform_error (read (sign_of ctxt) (def_type ctxt is_pat, def_sort ctxt, used)) s + (transform_error (read (#1 (syntax_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)) |> app (intern_skolem ctxt) @@ -494,8 +505,8 @@ Some T => Vartab.update (((x, ~1), T), types) | None => types)); -fun map_defaults f = map_context (fn (thy, data, asms, binds, thms, cases, defs) => - (thy, data, asms, binds, thms, cases, f defs)); +fun map_defaults f = map_context (fn (thy, syntax, data, asms, binds, thms, cases, defs) => + (thy, syntax, data, asms, binds, thms, cases, f defs)); fun declare_syn (ctxt, t) = ctxt @@ -518,9 +529,69 @@ -(** pretty printing **) (* FIXME observe local syntax *) +(** 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 -val pretty_term = Sign.pretty_term o sign_of; +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; + val pretty_typ = Sign.pretty_typ o sign_of; val pretty_sort = Sign.pretty_sort o sign_of; @@ -529,7 +600,8 @@ val show_hyps = ref false; fun pretty_thm ctxt thm = - if ! show_hyps then setmp Display.show_hyps true Display.pretty_thm_no_quote thm + if ! show_hyps then setmp Display.show_hyps true (fn () => + Display.pretty_thm_aux (pretty_sort ctxt) (pretty_term ctxt) false thm) () else pretty_term ctxt (#prop (Thm.rep_thm thm)); fun pretty_thms ctxt [th] = pretty_thm ctxt th @@ -630,8 +702,8 @@ fun del_bind (ctxt, xi) = ctxt - |> map_context (fn (thy, data, asms, binds, thms, cases, defs) => - (thy, data, asms, Vartab.update ((xi, None), binds), thms, cases, defs)); + |> map_context (fn (thy, syntax, data, asms, binds, thms, cases, defs) => + (thy, syntax, data, asms, Vartab.update ((xi, None), binds), thms, cases, defs)); fun upd_bind (ctxt, ((x, i), t)) = let @@ -642,8 +714,8 @@ in ctxt |> declare_term t' - |> map_context (fn (thy, data, asms, binds, thms, cases, defs) => - (thy, data, asms, Vartab.update (((x, i), Some (t', T)), binds), thms, cases, defs)) + |> map_context (fn (thy, syntax, data, asms, binds, thms, cases, defs) => + (thy, syntax, data, asms, Vartab.update (((x, i), Some (t', T)), binds), thms, cases, defs)) end; fun del_upd_bind (ctxt, (xi, None)) = del_bind (ctxt, xi) @@ -819,8 +891,8 @@ fun put_thms ("", _) = I | put_thms (name, ths) = map_context - (fn (thy, data, asms, binds, thms, cases, defs) => - (thy, data, asms, binds, Symtab.update ((name, Some ths), thms), cases, defs)); + (fn (thy, syntax, data, asms, binds, thms, cases, defs) => + (thy, syntax, data, asms, binds, Symtab.update ((name, Some ths), thms), cases, defs)); fun put_thm (name, th) = put_thms (name, [th]); @@ -830,8 +902,8 @@ (* reset_thms *) -fun reset_thms name = map_context (fn (thy, data, asms, binds, thms, cases, defs) => - (thy, data, asms, binds, Symtab.update ((name, None), thms), cases, defs)); +fun reset_thms name = map_context (fn (thy, syntax, data, asms, binds, thms, cases, defs) => + (thy, syntax, data, asms, binds, Symtab.update ((name, None), thms), cases, defs)); (* have_thmss *) @@ -920,10 +992,9 @@ val cprops = flat (map #1 results); val asmss = map #2 results; val thmss = map #3 results; - val ctxt3 = - ctxt2 - |> map_context (fn (thy, data, ((asms_ct, asms_th), fixes), binds, thms, cases, defs) => - (thy, data, ((asms_ct @ [(cprops, exp)], asms_th @ asmss), fixes), binds, thms, + val ctxt3 = ctxt2 |> map_context + (fn (thy, syntax, data, ((asms_ct, asms_th), fixes), binds, thms, cases, defs) => + (thy, syntax, data, ((asms_ct @ [(cprops, exp)], asms_th @ asmss), fixes), binds, thms, cases, defs)); val ctxt4 = ctxt3 |> put_thms ("prems", prems_of ctxt3); in (warn_extra_tfrees ctxt ctxt4, thmss) end; @@ -962,8 +1033,8 @@ local -fun map_vars f = map_context (fn (thy, data, (assumes, vars), binds, thms, cases, defs) => - (thy, data, (assumes, f vars), binds, thms, cases, defs)); +fun map_vars f = map_context (fn (thy, syntax, data, (assumes, vars), binds, thms, cases, defs) => + (thy, syntax, data, (assumes, f vars), binds, thms, cases, defs)); fun err_dups ctxt xs = raise CONTEXT ("Duplicate variable(s): " ^ commas_quote xs, ctxt); @@ -1038,8 +1109,8 @@ | Some c => prep_case ctxt name xs c); -fun add_cases xs = map_context (fn (thy, data, asms, binds, thms, cases, defs) => - (thy, data, asms, binds, thms, rev (filter_out (equal "" o #1) xs) @ cases, defs)); +fun add_cases xs = map_context (fn (thy, syntax, data, asms, binds, thms, cases, defs) => + (thy, syntax, data, asms, binds, thms, rev (filter_out (equal "" o #1) xs) @ cases, defs)); @@ -1061,6 +1132,11 @@ end; +(* local syntax *) + +val print_syntax = Syntax.print_syntax o #1 o syntax_of; + + (* term bindings *) val smash_option = fn (_, None) => None | (xi, Some b) => Some (xi, b);