--- 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 []);