1.1 --- a/src/Pure/Isar/proof_context.ML Sat May 01 22:09:45 2004 +0200
1.2 +++ b/src/Pure/Isar/proof_context.ML Sat May 01 22:10:37 2004 +0200
1.3 @@ -157,19 +157,18 @@
1.4 data: Object.T Symtab.table, (*user data*)
1.5 asms:
1.6 ((cterm list * exporter) list * (*assumes: A ==> _*)
1.7 - (string * thm list) list) *
1.8 + (string * thm list) list) * (*prems: A |- A *)
1.9 (string * string) list, (*fixes: !!x. _*)
1.10 - (* CB: asms is of the form ((asms, prems), fixed) *)
1.11 binds: (term * typ) option Vartab.table, (*term bindings*)
1.12 thms: bool * NameSpace.T * thm list option Symtab.table
1.13 * FactIndex.T, (*local thms*)
1.14 - (* CB: thms is of the form (q, n, t, i) where
1.15 + (*thms is of the form (q, n, t, i) where
1.16 q: indicates whether theorems with qualified names may be stored;
1.17 this is initially forbidden (false); flag may be changed with
1.18 qualified and restore_qualified;
1.19 n: theorem namespace;
1.20 t: table of theorems;
1.21 - i: index for theorem lookup (find theorem command) *)
1.22 + i: index for theorem lookup (cf. thms_containing) *)
1.23 cases: (string * RuleCases.T) list, (*local contexts*)
1.24 defs:
1.25 typ Vartab.table * (*type constraints*)
1.26 @@ -304,31 +303,11 @@
1.27 val fixedN = "\\<^fixed>";
1.28 val structN = "\\<^struct>";
1.29
1.30 -fun the_struct structs i =
1.31 - if 1 <= i andalso i <= length structs then Library.nth_elem (i - 1, structs)
1.32 - else raise ERROR_MESSAGE ("Illegal reference to implicit structure #" ^ string_of_int i);
1.33
1.34 -
1.35 -(* parse translations *)
1.36 +(* translation functions *)
1.37
1.38 fun fixed_tr x = (fixedN ^ x, curry Term.list_comb (Syntax.free x));
1.39
1.40 -fun index_tr struct_ (Const ("_noindex", _)) = Syntax.free (struct_ 1)
1.41 - | index_tr struct_ (t as (Const ("_index", _) $ Const (s, _))) =
1.42 - Syntax.free (struct_
1.43 - (case Syntax.read_nat s of Some n => n | None => raise TERM ("index_tr", [t])))
1.44 - | index_tr _ (Const ("_indexlogic", _) $ t) = t
1.45 - | index_tr _ t = raise TERM ("index_tr", [t]);
1.46 -
1.47 -fun struct_tr structs [idx] = index_tr (the_struct structs) idx
1.48 - | struct_tr _ ts = raise TERM ("struct_tr", ts);
1.49 -
1.50 -
1.51 -(* print (ast) translations *)
1.52 -
1.53 -fun index_tr' 1 = Syntax.const "_noindex"
1.54 - | index_tr' i = Syntax.const "_index" $ Syntax.const (Library.string_of_int i);
1.55 -
1.56 fun context_tr' ctxt =
1.57 let
1.58 val (_, structs, mixfixed) = syntax_of ctxt;
1.59 @@ -336,25 +315,14 @@
1.60 fun tr' (t $ u) = tr' t $ tr' u
1.61 | tr' (Abs (x, T, t)) = Abs (x, T, tr' t)
1.62 | tr' (t as Free (x, T)) =
1.63 - let val i = Library.find_index (equal x) structs + 1 in
1.64 - if 1 <= i andalso i <= 9 then Syntax.const "_struct" $ index_tr' i
1.65 - else if x mem_string mixfixed then Const (fixedN ^ x, T)
1.66 + let val i = Library.find_index_eq x structs + 1 in
1.67 + if i = 0 andalso x mem_string mixfixed then Const (fixedN ^ x, T)
1.68 + else if i = 1 then Syntax.const "_struct" $ Syntax.const "_indexdefault"
1.69 else t
1.70 end
1.71 | tr' a = a;
1.72 in tr' end;
1.73
1.74 -fun index_ast_tr' structs s =
1.75 - (case Syntax.read_nat s of
1.76 - Some i => Syntax.Variable (the_struct structs i handle ERROR_MESSAGE _ => raise Match)
1.77 - | None => raise Match);
1.78 -
1.79 -fun struct_ast_tr' structs [Syntax.Constant "_noindex"] =
1.80 - index_ast_tr' structs "1"
1.81 - | struct_ast_tr' structs [Syntax.Appl [Syntax.Constant "_index", Syntax.Constant s]] =
1.82 - index_ast_tr' structs s
1.83 - | struct_ast_tr' _ _ = raise Match;
1.84 -
1.85
1.86 (* add syntax *)
1.87
1.88 @@ -391,8 +359,8 @@
1.89 in (thy, (syn', structs', fixed @ mixfixed), data, asms, binds, thms, cases, defs) end)
1.90
1.91 fun syn_of (Context {syntax = (syn, structs, _), ...}) =
1.92 - syn |> Syntax.extend_trfuns
1.93 - ([], [("_struct", struct_tr structs)], [], [("_struct", struct_ast_tr' structs)]);
1.94 + syn |> Syntax.extend_trfuns (Syntax.struct_trfuns structs);
1.95 +
1.96
1.97 end;
1.98
1.99 @@ -459,8 +427,8 @@
1.100 (case env (x, ~1) of
1.101 Some _ => t
1.102 | None => (case lookup_skolem ctxt (no_skolem false ctxt x) of
1.103 - Some x' => Free (x', T)
1.104 - | None => t))
1.105 + Some x' => Free (x', T)
1.106 + | None => t))
1.107 | intern (t $ u) = intern t $ intern u
1.108 | intern (Abs (x, T, t)) = Abs (x, T, intern t)
1.109 | intern a = a;
1.110 @@ -592,13 +560,13 @@
1.111 | Some (_, _, used'') => used @ used'';
1.112 in
1.113 (transform_error (read (syn_of ctxt)
1.114 - (sign_of ctxt) (types', sorts', used')) s
1.115 + (sign_of ctxt) (types', sorts', used')) s
1.116 handle TERM (msg, _) => raise CONTEXT (msg, ctxt)
1.117 | ERROR_MESSAGE msg => raise CONTEXT (msg, ctxt))
1.118 |> app (intern_skolem ctxt (case env_opt of None => K None | Some (env, _, _) => env))
1.119 |> app (if is_pat then I else norm_term ctxt schematic allow_vars)
1.120 |> app (if is_pat then prepare_dummies
1.121 - else if dummies then I else reject_dummies ctxt)
1.122 + else if dummies then I else reject_dummies ctxt)
1.123 end
1.124 in
1.125
2.1 --- a/src/Pure/Syntax/mixfix.ML Sat May 01 22:09:45 2004 +0200
2.2 +++ b/src/Pure/Syntax/mixfix.ML Sat May 01 22:10:37 2004 +0200
2.3 @@ -239,10 +239,10 @@
2.4 ("", "var => logic", Delimfix "_"),
2.5 ("_DDDOT", "logic", Delimfix "..."),
2.6 ("_constify", "num => num_const", Delimfix "_"),
2.7 - ("_index", "num_const => index", Delimfix "\\<^sub>_"),
2.8 - ("_indexlogic", "logic => index", Delimfix "\\<^bsub>_\\<^esub>"),
2.9 + ("_indexnum", "num_const => index", Delimfix "\\<^sub>_"),
2.10 + ("_index", "logic => index", Delimfix "\\<^bsub>_\\<^esub>"),
2.11 + ("_indexdefault", "index", Delimfix ""),
2.12 ("_indexvar", "index", Delimfix "'\\<index>"),
2.13 - ("_noindex", "index", Delimfix ""),
2.14 ("_struct", "index => logic", Mixfix ("\\<struct>_", [1000], 1000))];
2.15
2.16 val pure_syntax_output =
3.1 --- a/src/Pure/Syntax/syn_ext.ML Sat May 01 22:09:45 2004 +0200
3.2 +++ b/src/Pure/Syntax/syn_ext.ML Sat May 01 22:10:37 2004 +0200
3.3 @@ -267,17 +267,18 @@
3.4 if not (exists is_index args) then (const, typ, [])
3.5 else
3.6 let
3.7 - val c = if const <> "" then "_indexed_" ^ const
3.8 + val indexed_const = if const <> "" then "_indexed_" ^ const
3.9 else err_in_mfix "Missing constant name for indexed syntax" mfix;
3.10 - val T = Term.range_type typ handle Match =>
3.11 + val rangeT = Term.range_type typ handle Match =>
3.12 err_in_mfix "Missing structure argument for indexed syntax" mfix;
3.13
3.14 - val xs = map Ast.Variable (Term.invent_names [] "x" (length args - 1));
3.15 + val xs = map Ast.Variable (Term.invent_names [] "xa" (length args - 1));
3.16 + val (xs1, xs2) = Library.splitAt (Library.find_index is_index args, xs);
3.17 val i = Ast.Variable "i";
3.18 - val n = Library.find_index is_index args;
3.19 - val lhs = Ast.mk_appl (Ast.Constant c) (take (n, xs) @ [i] @ drop (n, xs));
3.20 - val rhs = Ast.mk_appl (Ast.Constant const) (Ast.Appl [Ast.Constant "_struct", i] :: xs);
3.21 - in (c, T, [(lhs, rhs)]) end;
3.22 + val lhs = Ast.mk_appl (Ast.Constant indexed_const)
3.23 + (xs1 @ [Ast.mk_appl (Ast.Constant "_index") [i]] @ xs2);
3.24 + val rhs = Ast.mk_appl (Ast.Constant const) (i :: xs);
3.25 + in (indexed_const, rangeT, [(lhs, rhs)]) end;
3.26
3.27 val (symbs, lhs) = add_args raw_symbs typ' pris;
3.28
4.1 --- a/src/Pure/Syntax/syn_trans.ML Sat May 01 22:09:45 2004 +0200
4.2 +++ b/src/Pure/Syntax/syn_trans.ML Sat May 01 22:10:37 2004 +0200
4.3 @@ -36,6 +36,11 @@
4.4 (string * (term list -> term)) list *
4.5 (string * (Ast.ast list -> Ast.ast)) list
4.6 val pure_trfunsT: (string * (bool -> typ -> term list -> term)) list
4.7 + val struct_trfuns: string list ->
4.8 + (string * (Ast.ast list -> Ast.ast)) list *
4.9 + (string * (term list -> term)) list *
4.10 + (string * (bool -> typ -> term list -> term)) list *
4.11 + (string * (Ast.ast list -> Ast.ast)) list
4.12 end;
4.13
4.14 signature SYN_TRANS =
4.15 @@ -165,10 +170,43 @@
4.16 in (quoteN, tr) end;
4.17
4.18
4.19 -(* index variable *)
4.20 +(* indexed syntax *)
4.21
4.22 -fun indexvar_ast_tr [] = Ast.Variable "some_index"
4.23 - | indexvar_ast_tr asts = raise Ast.AST ("indexvar_ast_tr", asts);
4.24 +fun struct_ast_tr (*"_struct"*) [Ast.Appl [Ast.Constant "_index", ast]] = ast
4.25 + | struct_ast_tr (*"_struct"*) asts = Ast.mk_appl (Ast.Constant "_struct") asts;
4.26 +
4.27 +fun index_ast_tr ast =
4.28 + Ast.mk_appl (Ast.Constant "_index") [Ast.mk_appl (Ast.Constant "_struct") [ast]];
4.29 +
4.30 +fun indexdefault_ast_tr (*"_indexdefault"*) [] =
4.31 + index_ast_tr (Ast.Constant "_indexdefault")
4.32 + | indexdefault_ast_tr (*"_indexdefault"*) asts =
4.33 + raise Ast.AST ("indexdefault_ast_tr", asts);
4.34 +
4.35 +fun indexnum_ast_tr (*"_indexnum"*) [ast] =
4.36 + index_ast_tr (Ast.mk_appl (Ast.Constant "_indexnum") [ast])
4.37 + | indexnum_ast_tr (*"_indexnum"*) asts = raise Ast.AST ("indexnum_ast_tr", asts);
4.38 +
4.39 +fun indexvar_ast_tr (*"_indexvar"*) [] =
4.40 + Ast.mk_appl (Ast.Constant "_index") [Ast.Variable "some_index"]
4.41 + | indexvar_ast_tr (*"_indexvar"*) asts = raise Ast.AST ("indexvar_ast_tr", asts);
4.42 +
4.43 +fun index_tr (*"_index"*) [t] = t
4.44 + | index_tr (*"_index"*) ts = raise TERM ("index_tr", ts);
4.45 +
4.46 +
4.47 +(* implicit structures *)
4.48 +
4.49 +fun the_struct structs i =
4.50 + if 1 <= i andalso i <= length structs then Library.nth_elem (i - 1, structs)
4.51 + else raise ERROR_MESSAGE ("Illegal reference to implicit structure #" ^ string_of_int i);
4.52 +
4.53 +fun struct_tr structs (*"_struct"*) [Const ("_indexdefault", _)] =
4.54 + Lexicon.free (the_struct structs 1)
4.55 + | struct_tr structs (*"_struct"*) [t as (Const ("_indexnum", _) $ Const (s, _))] =
4.56 + Lexicon.free (the_struct structs
4.57 + (case Lexicon.read_nat s of Some n => n | None => raise TERM ("struct_tr", [t])))
4.58 + | struct_tr _ (*"_struct"*) ts = raise TERM ("struct_tr", ts);
4.59
4.60
4.61
4.62 @@ -233,10 +271,9 @@
4.63 foldr (fn (x, t) => Lexicon.const "_abs" $ x $ t)
4.64 (strip_abss strip_abs_vars strip_abs_body (eta_contr tm));
4.65
4.66 -
4.67 -fun atomic_abs_tr' (x,T,t) =
4.68 - let val [xT] = rename_wrt_term t [(x,T)];
4.69 - in (mark_boundT xT, subst_bound (mark_bound(fst xT), t)) end;
4.70 +fun atomic_abs_tr' (x, T, t) =
4.71 + let val [xT] = rename_wrt_term t [(x, T)]
4.72 + in (mark_boundT xT, subst_bound (mark_bound (fst xT), t)) end;
4.73
4.74 fun abs_ast_tr' (*"_abs"*) asts =
4.75 (case Ast.unfold_ast_p "_abs" (Ast.Appl (Ast.Constant "_abs" :: asts)) of
4.76 @@ -370,22 +407,49 @@
4.77 in (name, tr') end;
4.78
4.79
4.80 +(* indexed syntax *)
4.81
4.82 -(** pure_trfuns **)
4.83 +fun index_ast_tr' (*"_index"*) [Ast.Appl [Ast.Constant "_struct", ast]] = ast
4.84 + | index_ast_tr' _ = raise Match;
4.85 +
4.86 +
4.87 +(* implicit structures *)
4.88 +
4.89 +fun the_struct' structs s =
4.90 + [(case Lexicon.read_nat s of
4.91 + Some i => Ast.Variable (the_struct structs i handle ERROR_MESSAGE _ => raise Match)
4.92 + | None => raise Match)] |> Ast.mk_appl (Ast.Constant "_free");
4.93 +;
4.94 +
4.95 +fun struct_ast_tr' structs (*"_struct"*) [Ast.Constant "_indexdefault"] =
4.96 + the_struct' structs "1"
4.97 + | struct_ast_tr' structs (*"_struct"*) [Ast.Appl [Ast.Constant "_indexnum", Ast.Constant s]] =
4.98 + the_struct' structs s
4.99 + | struct_ast_tr' _ _ = raise Match;
4.100 +
4.101 +
4.102 +
4.103 +(** Pure translations **)
4.104
4.105 val pure_trfuns =
4.106 ([("_constify", constify_ast_tr), ("_appl", appl_ast_tr), ("_applC", applC_ast_tr),
4.107 ("_lambda", lambda_ast_tr), ("_idtyp", idtyp_ast_tr), ("_bigimpl", bigimpl_ast_tr),
4.108 - ("_indexvar", indexvar_ast_tr)],
4.109 + ("_indexdefault", indexdefault_ast_tr), ("_indexnum", indexnum_ast_tr),
4.110 + ("_indexvar", indexvar_ast_tr), ("_struct", struct_ast_tr)],
4.111 [("_abs", abs_tr), ("_aprop", aprop_tr), ("_ofclass", ofclass_tr),
4.112 - ("_TYPE", type_tr), ("_DDDOT", dddot_tr), ("_K", k_tr)],
4.113 + ("_TYPE", type_tr), ("_DDDOT", dddot_tr), ("_K", k_tr),
4.114 + ("_index", index_tr)],
4.115 [("all", meta_conjunction_tr')],
4.116 [("_abs", abs_ast_tr'), ("_idts", idtyp_ast_tr' "_idts"),
4.117 - ("_pttrns", idtyp_ast_tr' "_pttrns"), ("==>", impl_ast_tr')]);
4.118 + ("_pttrns", idtyp_ast_tr' "_pttrns"), ("==>", impl_ast_tr'),
4.119 + ("_index", index_ast_tr')]);
4.120
4.121 val pure_trfunsT =
4.122 [("_mk_ofclass", mk_ofclass_tr'), ("TYPE", type_tr')];
4.123
4.124 +fun struct_trfuns structs =
4.125 + ([], [("_struct", struct_tr structs)], [], [("_struct", struct_ast_tr' structs)]);
4.126 +
4.127
4.128
4.129 (** pt_to_ast **)