# HG changeset patch # User haftmann # Date 1195848574 -3600 # Node ID 001dfba51869e5e1ec4e19db3a08e4e4370e0ca4 # Parent b80087af22743a4d54fd1ad4da9f3fecd1b45c89 explicit type signature diff -r b80087af2274 -r 001dfba51869 src/Pure/Isar/proof_context.ML --- a/src/Pure/Isar/proof_context.ML Fri Nov 23 21:09:33 2007 +0100 +++ b/src/Pure/Isar/proof_context.ML Fri Nov 23 21:09:34 2007 +0100 @@ -27,6 +27,7 @@ val consts_of: Proof.context -> Consts.T val const_syntax_name: Proof.context -> string -> string val the_const_constraint: Proof.context -> string -> typ + val add_arity: arity -> Proof.context -> Proof.context val set_syntax_mode: Syntax.mode -> Proof.context -> Proof.context val restore_syntax_mode: Proof.context -> Proof.context -> Proof.context val theorems_of: Proof.context -> thm list NameSpace.table @@ -155,7 +156,6 @@ struct val theory_of = Context.theory_of_proof; -val tsig_of = Sign.tsig_of o theory_of; val init = Context.init_proof; @@ -185,14 +185,15 @@ datatype ctxt = Ctxt of {mode: mode, (*inner syntax mode*) + tsig: Type.tsig, (*local type signature*) naming: NameSpace.naming, (*local naming conventions*) syntax: LocalSyntax.T, (*local syntax*) consts: Consts.T * Consts.T, (*local/global consts*) thms: thm list NameSpace.table * FactIndex.T, (*local thms*) cases: (string * (RuleCases.T * bool)) list}; (*local contexts*) -fun make_ctxt (mode, naming, syntax, consts, thms, cases) = - Ctxt {mode = mode, naming = naming, syntax = syntax, +fun make_ctxt (mode, tsig, naming, syntax, consts, thms, cases) = + Ctxt {mode = mode, tsig = tsig, naming = naming, syntax = syntax, consts = consts, thms = thms, cases = cases}; val local_naming = NameSpace.default_naming |> NameSpace.add_path "local"; @@ -201,7 +202,7 @@ ( type T = ctxt; fun init thy = - make_ctxt (mode_default, local_naming, LocalSyntax.init thy, + make_ctxt (mode_default, Sign.tsig_of thy, local_naming, LocalSyntax.init thy, (Sign.consts_of thy, Sign.consts_of thy), (NameSpace.empty_table, FactIndex.empty), []); ); @@ -209,35 +210,39 @@ fun rep_context ctxt = ContextData.get ctxt |> (fn Ctxt args => args); fun map_context f = - ContextData.map (fn Ctxt {mode, naming, syntax, consts, thms, cases} => - make_ctxt (f (mode, naming, syntax, consts, thms, cases))); + ContextData.map (fn Ctxt {mode, tsig, naming, syntax, consts, thms, cases} => + make_ctxt (f (mode, tsig, naming, syntax, consts, thms, cases))); -fun set_mode mode = map_context (fn (_, naming, syntax, consts, thms, cases) => - (mode, naming, syntax, consts, thms, cases)); +fun set_mode mode = map_context (fn (_, tsig, naming, syntax, consts, thms, cases) => + (mode, tsig, naming, syntax, consts, thms, cases)); fun map_mode f = - map_context (fn (Mode {stmt, pattern, schematic, abbrev}, naming, syntax, consts, thms, cases) => - (make_mode (f (stmt, pattern, schematic, abbrev)), naming, syntax, consts, thms, cases)); + map_context (fn (Mode {stmt, pattern, schematic, abbrev}, tsig, naming, syntax, consts, thms, cases) => + (make_mode (f (stmt, pattern, schematic, abbrev)), tsig, naming, syntax, consts, thms, cases)); + +fun map_tsig f = + map_context (fn (mode, tsig, naming, syntax, consts, thms, cases) => + (mode, f tsig, naming, syntax, consts, thms, cases)); fun map_naming f = - map_context (fn (mode, naming, syntax, consts, thms, cases) => - (mode, f naming, syntax, consts, thms, cases)); + map_context (fn (mode, tsig, naming, syntax, consts, thms, cases) => + (mode, tsig, f naming, syntax, consts, thms, cases)); fun map_syntax f = - map_context (fn (mode, naming, syntax, consts, thms, cases) => - (mode, naming, f syntax, consts, thms, cases)); + map_context (fn (mode, tsig, naming, syntax, consts, thms, cases) => + (mode, tsig, naming, f syntax, consts, thms, cases)); fun map_consts f = - map_context (fn (mode, naming, syntax, consts, thms, cases) => - (mode, naming, syntax, f consts, thms, cases)); + map_context (fn (mode, tsig, naming, syntax, consts, thms, cases) => + (mode, tsig, naming, syntax, f consts, thms, cases)); fun map_thms f = - map_context (fn (mode, naming, syntax, consts, thms, cases) => - (mode, naming, syntax, consts, f thms, cases)); + map_context (fn (mode, tsig, naming, syntax, consts, thms, cases) => + (mode, tsig, naming, syntax, consts, f thms, cases)); fun map_cases f = - map_context (fn (mode, naming, syntax, consts, thms, cases) => - (mode, naming, syntax, consts, thms, f cases)); + map_context (fn (mode, tsig, naming, syntax, consts, thms, cases) => + (mode, tsig, naming, syntax, consts, thms, f cases)); val get_mode = #mode o rep_context; fun restore_mode ctxt = set_mode (get_mode ctxt); @@ -248,6 +253,7 @@ val naming_of = #naming o rep_context; val full_name = NameSpace.full o naming_of; +val tsig_of = #tsig o rep_context; val syntax_of = #syntax o rep_context; val syn_of = LocalSyntax.syn_of o syntax_of; val set_syntax_mode = map_syntax o LocalSyntax.set_mode; @@ -395,6 +401,10 @@ fold_map inferred_param (rev (map #2 (Variable.fixes_of ctxt))) ctxt; +(* type signature *) + +fun add_arity arity ctxt = ctxt |> map_tsig (Type.add_arity (Syntax.pp ctxt) arity); + (* type and constant names *) fun read_tyname ctxt c =