--- a/src/Pure/Isar/proof_context.ML Sat May 01 22:09:45 2004 +0200
+++ b/src/Pure/Isar/proof_context.ML Sat May 01 22:10:37 2004 +0200
@@ -157,19 +157,18 @@
data: Object.T Symtab.table, (*user data*)
asms:
((cterm list * exporter) list * (*assumes: A ==> _*)
- (string * thm list) list) *
+ (string * thm list) list) * (*prems: A |- A *)
(string * string) list, (*fixes: !!x. _*)
- (* CB: asms is of the form ((asms, prems), fixed) *)
binds: (term * typ) option Vartab.table, (*term bindings*)
thms: bool * NameSpace.T * thm list option Symtab.table
* FactIndex.T, (*local thms*)
- (* CB: thms is of the form (q, n, t, i) where
+ (*thms is of the form (q, n, t, i) where
q: indicates whether theorems with qualified names may be stored;
this is initially forbidden (false); flag may be changed with
qualified and restore_qualified;
n: theorem namespace;
t: table of theorems;
- i: index for theorem lookup (find theorem command) *)
+ i: index for theorem lookup (cf. thms_containing) *)
cases: (string * RuleCases.T) list, (*local contexts*)
defs:
typ Vartab.table * (*type constraints*)
@@ -304,31 +303,11 @@
val fixedN = "\\<^fixed>";
val structN = "\\<^struct>";
-fun the_struct structs i =
- if 1 <= i andalso i <= length structs then Library.nth_elem (i - 1, structs)
- else raise ERROR_MESSAGE ("Illegal reference to implicit structure #" ^ string_of_int i);
-
-(* parse translations *)
+(* translation functions *)
fun fixed_tr x = (fixedN ^ x, curry Term.list_comb (Syntax.free x));
-fun index_tr struct_ (Const ("_noindex", _)) = Syntax.free (struct_ 1)
- | index_tr struct_ (t as (Const ("_index", _) $ Const (s, _))) =
- Syntax.free (struct_
- (case Syntax.read_nat s of Some n => n | None => raise TERM ("index_tr", [t])))
- | index_tr _ (Const ("_indexlogic", _) $ t) = t
- | index_tr _ t = raise TERM ("index_tr", [t]);
-
-fun struct_tr structs [idx] = index_tr (the_struct structs) idx
- | struct_tr _ ts = raise TERM ("struct_tr", ts);
-
-
-(* print (ast) translations *)
-
-fun index_tr' 1 = Syntax.const "_noindex"
- | index_tr' i = Syntax.const "_index" $ Syntax.const (Library.string_of_int i);
-
fun context_tr' ctxt =
let
val (_, structs, mixfixed) = syntax_of ctxt;
@@ -336,25 +315,14 @@
fun tr' (t $ u) = tr' t $ tr' u
| tr' (Abs (x, T, t)) = Abs (x, T, tr' t)
| tr' (t as Free (x, T)) =
- let val i = Library.find_index (equal x) structs + 1 in
- if 1 <= i andalso i <= 9 then Syntax.const "_struct" $ index_tr' i
- else if x mem_string mixfixed then Const (fixedN ^ x, T)
+ let val i = Library.find_index_eq x structs + 1 in
+ if i = 0 andalso x mem_string mixfixed then Const (fixedN ^ x, T)
+ else if i = 1 then Syntax.const "_struct" $ Syntax.const "_indexdefault"
else t
end
| tr' a = a;
in tr' end;
-fun index_ast_tr' structs s =
- (case Syntax.read_nat s of
- Some i => Syntax.Variable (the_struct structs i handle ERROR_MESSAGE _ => raise Match)
- | None => raise Match);
-
-fun struct_ast_tr' structs [Syntax.Constant "_noindex"] =
- index_ast_tr' structs "1"
- | struct_ast_tr' structs [Syntax.Appl [Syntax.Constant "_index", Syntax.Constant s]] =
- index_ast_tr' structs s
- | struct_ast_tr' _ _ = raise Match;
-
(* add syntax *)
@@ -391,8 +359,8 @@
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", struct_tr structs)], [], [("_struct", struct_ast_tr' structs)]);
+ syn |> Syntax.extend_trfuns (Syntax.struct_trfuns structs);
+
end;
@@ -459,8 +427,8 @@
(case env (x, ~1) of
Some _ => t
| None => (case lookup_skolem ctxt (no_skolem false ctxt x) of
- Some x' => Free (x', T)
- | None => t))
+ Some x' => Free (x', T)
+ | None => t))
| intern (t $ u) = intern t $ intern u
| intern (Abs (x, T, t)) = Abs (x, T, intern t)
| intern a = a;
@@ -592,13 +560,13 @@
| Some (_, _, used'') => used @ used'';
in
(transform_error (read (syn_of ctxt)
- (sign_of ctxt) (types', sorts', used')) s
+ (sign_of ctxt) (types', sorts', used')) s
handle TERM (msg, _) => raise CONTEXT (msg, ctxt)
| ERROR_MESSAGE msg => raise CONTEXT (msg, ctxt))
|> app (intern_skolem ctxt (case env_opt of None => K None | Some (env, _, _) => env))
|> app (if is_pat then I else norm_term ctxt schematic allow_vars)
|> app (if is_pat then prepare_dummies
- else if dummies then I else reject_dummies ctxt)
+ else if dummies then I else reject_dummies ctxt)
end
in