diff -r 39442248a027 -r db0b87085c16 src/Pure/variable.ML --- a/src/Pure/variable.ML Tue Mar 24 18:10:56 2015 +0100 +++ b/src/Pure/variable.ML Tue Mar 24 23:39:42 2015 +0100 @@ -6,9 +6,6 @@ signature VARIABLE = sig - val is_body: Proof.context -> bool - val set_body: bool -> Proof.context -> Proof.context - val restore_body: Proof.context -> Proof.context -> Proof.context val names_of: Proof.context -> Name.context val binds_of: Proof.context -> (typ * term) Vartab.table val maxidx_of: Proof.context -> int @@ -34,6 +31,9 @@ val declare_const: string * string -> Proof.context -> Proof.context val next_bound: string * typ -> Proof.context -> term * Proof.context val revert_bounds: Proof.context -> term -> term + val is_body: Proof.context -> bool + val set_body: bool -> Proof.context -> Proof.context + val restore_body: Proof.context -> Proof.context -> Proof.context val improper_fixes: Proof.context -> Proof.context val restore_proper_fixes: Proof.context -> Proof.context -> Proof.context val is_improper: Proof.context -> string -> bool @@ -52,15 +52,16 @@ val add_fixes: string list -> Proof.context -> string list * Proof.context val add_fixes_direct: string list -> Proof.context -> Proof.context val auto_fixes: term -> Proof.context -> Proof.context + val fix_dummy_patterns: term -> Proof.context -> term * Proof.context val variant_fixes: string list -> Proof.context -> string list * Proof.context val dest_fixes: Proof.context -> (string * string) list - val invent_types: sort list -> Proof.context -> (string * sort) list * Proof.context val export_terms: Proof.context -> Proof.context -> term list -> term list val exportT_terms: Proof.context -> Proof.context -> term list -> term list val exportT: Proof.context -> Proof.context -> thm list -> thm list val export_prf: Proof.context -> Proof.context -> Proofterm.proof -> Proofterm.proof val export: Proof.context -> Proof.context -> thm list -> thm list val export_morphism: Proof.context -> Proof.context -> morphism + val invent_types: sort list -> Proof.context -> (string * sort) list * Proof.context val importT_inst: term list -> Proof.context -> ((indexname * sort) * typ) list * Proof.context val import_inst: bool -> term list -> Proof.context -> (((indexname * sort) * typ) list * ((indexname * typ) * term) list) * Proof.context @@ -89,8 +90,7 @@ val empty_fixes: fixes = Name_Space.empty_table Markup.fixedN; datatype data = Data of - {is_body: bool, (*inner body mode*) - names: Name.context, (*type/term variable names*) + {names: Name.context, (*type/term variable names*) consts: string Symtab.table, (*consts within the local scope*) bounds: int * ((string * typ) * string) list, (*next index, internal name, type, external name*) fixes: fixes, (*term fixes -- global name space, intern ~> extern*) @@ -102,13 +102,12 @@ typ Vartab.table * (*type constraints*) sort Vartab.table}; (*default sorts*) -fun make_data - (is_body, names, consts, bounds, fixes, binds, type_occs, maxidx, sorts, constraints) = - Data {is_body = is_body, names = names, consts = consts, bounds = bounds, fixes = fixes, - binds = binds, type_occs = type_occs, maxidx = maxidx, sorts = sorts, constraints = constraints}; +fun make_data (names, consts, bounds, fixes, binds, type_occs, maxidx, sorts, constraints) = + Data {names = names, consts = consts, bounds = bounds, fixes = fixes, binds = binds, + type_occs = type_occs, maxidx = maxidx, sorts = sorts, constraints = constraints}; val empty_data = - make_data (false, Name.context, Symtab.empty, (0, []), empty_fixes, Vartab.empty, + make_data (Name.context, Symtab.empty, (0, []), empty_fixes, Vartab.empty, Symtab.empty, ~1, [], (Vartab.empty, Vartab.empty)); structure Data = Proof_Data @@ -118,66 +117,47 @@ ); fun map_data f = - Data.map (fn - Data {is_body, names, consts, bounds, fixes, binds, type_occs, maxidx, sorts, constraints} => - make_data - (f (is_body, names, consts, bounds, fixes, binds, type_occs, maxidx, sorts, constraints))); + Data.map (fn Data {names, consts, bounds, fixes, binds, type_occs, maxidx, sorts, constraints} => + make_data (f (names, consts, bounds, fixes, binds, type_occs, maxidx, sorts, constraints))); fun map_names f = - map_data (fn - (is_body, names, consts, bounds, fixes, binds, type_occs, maxidx, sorts, constraints) => - (is_body, f names, consts, bounds, fixes, binds, type_occs, maxidx, sorts, constraints)); + map_data (fn (names, consts, bounds, fixes, binds, type_occs, maxidx, sorts, constraints) => + (f names, consts, bounds, fixes, binds, type_occs, maxidx, sorts, constraints)); fun map_consts f = - map_data (fn - (is_body, names, consts, bounds, fixes, binds, type_occs, maxidx, sorts, constraints) => - (is_body, names, f consts, bounds, fixes, binds, type_occs, maxidx, sorts, constraints)); + map_data (fn (names, consts, bounds, fixes, binds, type_occs, maxidx, sorts, constraints) => + (names, f consts, bounds, fixes, binds, type_occs, maxidx, sorts, constraints)); fun map_bounds f = - map_data (fn - (is_body, names, consts, bounds, fixes, binds, type_occs, maxidx, sorts, constraints) => - (is_body, names, consts, f bounds, fixes, binds, type_occs, maxidx, sorts, constraints)); + map_data (fn (names, consts, bounds, fixes, binds, type_occs, maxidx, sorts, constraints) => + (names, consts, f bounds, fixes, binds, type_occs, maxidx, sorts, constraints)); fun map_fixes f = - map_data (fn - (is_body, names, consts, bounds, fixes, binds, type_occs, maxidx, sorts, constraints) => - (is_body, names, consts, bounds, f fixes, binds, type_occs, maxidx, sorts, constraints)); + map_data (fn (names, consts, bounds, fixes, binds, type_occs, maxidx, sorts, constraints) => + (names, consts, bounds, f fixes, binds, type_occs, maxidx, sorts, constraints)); fun map_binds f = - map_data (fn - (is_body, names, consts, bounds, fixes, binds, type_occs, maxidx, sorts, constraints) => - (is_body, names, consts, bounds, fixes, f binds, type_occs, maxidx, sorts, constraints)); + map_data (fn (names, consts, bounds, fixes, binds, type_occs, maxidx, sorts, constraints) => + (names, consts, bounds, fixes, f binds, type_occs, maxidx, sorts, constraints)); fun map_type_occs f = - map_data (fn - (is_body, names, consts, bounds, fixes, binds, type_occs, maxidx, sorts, constraints) => - (is_body, names, consts, bounds, fixes, binds, f type_occs, maxidx, sorts, constraints)); + map_data (fn (names, consts, bounds, fixes, binds, type_occs, maxidx, sorts, constraints) => + (names, consts, bounds, fixes, binds, f type_occs, maxidx, sorts, constraints)); fun map_maxidx f = - map_data (fn - (is_body, names, consts, bounds, fixes, binds, type_occs, maxidx, sorts, constraints) => - (is_body, names, consts, bounds, fixes, binds, type_occs, f maxidx, sorts, constraints)); + map_data (fn (names, consts, bounds, fixes, binds, type_occs, maxidx, sorts, constraints) => + (names, consts, bounds, fixes, binds, type_occs, f maxidx, sorts, constraints)); fun map_sorts f = - map_data (fn - (is_body, names, consts, bounds, fixes, binds, type_occs, maxidx, sorts, constraints) => - (is_body, names, consts, bounds, fixes, binds, type_occs, maxidx, f sorts, constraints)); + map_data (fn (names, consts, bounds, fixes, binds, type_occs, maxidx, sorts, constraints) => + (names, consts, bounds, fixes, binds, type_occs, maxidx, f sorts, constraints)); fun map_constraints f = - map_data (fn - (is_body, names, consts, bounds, fixes, binds, type_occs, maxidx, sorts, constraints) => - (is_body, names, consts, bounds, fixes, binds, type_occs, maxidx, sorts, f constraints)); + map_data (fn (names, consts, bounds, fixes, binds, type_occs, maxidx, sorts, constraints) => + (names, consts, bounds, fixes, binds, type_occs, maxidx, sorts, f constraints)); fun rep_data ctxt = Data.get ctxt |> (fn Data rep => rep); -val is_body = #is_body o rep_data; - -fun set_body b = - map_data (fn (_, names, consts, bounds, fixes, binds, type_occs, maxidx, sorts, constraints) => - (b, names, consts, bounds, fixes, binds, type_occs, maxidx, sorts, constraints)); - -fun restore_body ctxt = set_body (is_body ctxt); - val names_of = #names o rep_data; val fixes_of = #fixes o rep_data; val fixes_space = Name_Space.space_of_table o fixes_of; @@ -338,6 +318,16 @@ (** fixes **) +(* inner body mode *) + +val inner_body = + Config.bool (Config.declare ("inner_body", @{here}) (K (Config.Bool false))); + +fun is_body ctxt = Config.get ctxt inner_body; +val set_body = Config.put inner_body; +fun restore_body ctxt = set_body (is_body ctxt); + + (* proper mode *) val proper_fixes = @@ -460,11 +450,21 @@ |> not (is_body ctxt) ? add_fixes_direct (rev (add_free_names ctxt t [])) |> declare_term t; -fun invent_types Ss ctxt = - let - val tfrees = Name.invent (names_of ctxt) Name.aT (length Ss) ~~ Ss; - val ctxt' = fold (declare_constraints o Logic.mk_type o TFree) tfrees ctxt; - in (tfrees, ctxt') end; + +(* dummy patterns *) + +fun fix_dummy_patterns (Const ("Pure.dummy_pattern", T)) ctxt = + let val ([x], ctxt') = add_fixes [Name.uu_] ctxt + in (Free (x, T), ctxt') end + | fix_dummy_patterns (Abs (x, T, b)) ctxt = + let val (b', ctxt') = fix_dummy_patterns b ctxt + in (Abs (x, T, b'), ctxt') end + | fix_dummy_patterns (t $ u) ctxt = + let + val (t', ctxt') = fix_dummy_patterns t ctxt; + val (u', ctxt'') = fix_dummy_patterns u ctxt'; + in (t' $ u', ctxt'') end + | fix_dummy_patterns a ctxt = (a, ctxt); @@ -541,6 +541,12 @@ (** import -- fix schematic type/term variables **) +fun invent_types Ss ctxt = + let + val tfrees = Name.invent (names_of ctxt) Name.aT (length Ss) ~~ Ss; + val ctxt' = fold (declare_constraints o Logic.mk_type o TFree) tfrees ctxt; + in (tfrees, ctxt') end; + fun importT_inst ts ctxt = let val tvars = rev (fold Term.add_tvars ts []);