# HG changeset patch # User wenzelm # Date 1083442237 -7200 # Node ID 5ad13d05049bb38d745f265b47b1064d5576400c # Parent e862cc138e9cc2a1a33ddcb8a6e1b280b2e17730 improved indexed syntax / implicit structures; diff -r e862cc138e9c -r 5ad13d05049b src/Pure/Isar/proof_context.ML --- 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 diff -r e862cc138e9c -r 5ad13d05049b src/Pure/Syntax/mixfix.ML --- a/src/Pure/Syntax/mixfix.ML Sat May 01 22:09:45 2004 +0200 +++ b/src/Pure/Syntax/mixfix.ML Sat May 01 22:10:37 2004 +0200 @@ -239,10 +239,10 @@ ("", "var => logic", Delimfix "_"), ("_DDDOT", "logic", Delimfix "..."), ("_constify", "num => num_const", Delimfix "_"), - ("_index", "num_const => index", Delimfix "\\<^sub>_"), - ("_indexlogic", "logic => index", Delimfix "\\<^bsub>_\\<^esub>"), + ("_indexnum", "num_const => index", Delimfix "\\<^sub>_"), + ("_index", "logic => index", Delimfix "\\<^bsub>_\\<^esub>"), + ("_indexdefault", "index", Delimfix ""), ("_indexvar", "index", Delimfix "'\\"), - ("_noindex", "index", Delimfix ""), ("_struct", "index => logic", Mixfix ("\\_", [1000], 1000))]; val pure_syntax_output = diff -r e862cc138e9c -r 5ad13d05049b src/Pure/Syntax/syn_ext.ML --- a/src/Pure/Syntax/syn_ext.ML Sat May 01 22:09:45 2004 +0200 +++ b/src/Pure/Syntax/syn_ext.ML Sat May 01 22:10:37 2004 +0200 @@ -267,17 +267,18 @@ if not (exists is_index args) then (const, typ, []) else let - val c = if const <> "" then "_indexed_" ^ const + val indexed_const = if const <> "" then "_indexed_" ^ const else err_in_mfix "Missing constant name for indexed syntax" mfix; - val T = Term.range_type typ handle Match => + val rangeT = Term.range_type typ handle Match => err_in_mfix "Missing structure argument for indexed syntax" mfix; - val xs = map Ast.Variable (Term.invent_names [] "x" (length args - 1)); + val xs = map Ast.Variable (Term.invent_names [] "xa" (length args - 1)); + val (xs1, xs2) = Library.splitAt (Library.find_index is_index args, xs); val i = Ast.Variable "i"; - val n = Library.find_index is_index args; - val lhs = Ast.mk_appl (Ast.Constant c) (take (n, xs) @ [i] @ drop (n, xs)); - val rhs = Ast.mk_appl (Ast.Constant const) (Ast.Appl [Ast.Constant "_struct", i] :: xs); - in (c, T, [(lhs, rhs)]) end; + val lhs = Ast.mk_appl (Ast.Constant indexed_const) + (xs1 @ [Ast.mk_appl (Ast.Constant "_index") [i]] @ xs2); + val rhs = Ast.mk_appl (Ast.Constant const) (i :: xs); + in (indexed_const, rangeT, [(lhs, rhs)]) end; val (symbs, lhs) = add_args raw_symbs typ' pris; diff -r e862cc138e9c -r 5ad13d05049b src/Pure/Syntax/syn_trans.ML --- a/src/Pure/Syntax/syn_trans.ML Sat May 01 22:09:45 2004 +0200 +++ b/src/Pure/Syntax/syn_trans.ML Sat May 01 22:10:37 2004 +0200 @@ -36,6 +36,11 @@ (string * (term list -> term)) list * (string * (Ast.ast list -> Ast.ast)) list val pure_trfunsT: (string * (bool -> typ -> term list -> term)) list + val struct_trfuns: string list -> + (string * (Ast.ast list -> Ast.ast)) list * + (string * (term list -> term)) list * + (string * (bool -> typ -> term list -> term)) list * + (string * (Ast.ast list -> Ast.ast)) list end; signature SYN_TRANS = @@ -165,10 +170,43 @@ in (quoteN, tr) end; -(* index variable *) +(* indexed syntax *) + +fun struct_ast_tr (*"_struct"*) [Ast.Appl [Ast.Constant "_index", ast]] = ast + | struct_ast_tr (*"_struct"*) asts = Ast.mk_appl (Ast.Constant "_struct") asts; + +fun index_ast_tr ast = + Ast.mk_appl (Ast.Constant "_index") [Ast.mk_appl (Ast.Constant "_struct") [ast]]; + +fun indexdefault_ast_tr (*"_indexdefault"*) [] = + index_ast_tr (Ast.Constant "_indexdefault") + | indexdefault_ast_tr (*"_indexdefault"*) asts = + raise Ast.AST ("indexdefault_ast_tr", asts); + +fun indexnum_ast_tr (*"_indexnum"*) [ast] = + index_ast_tr (Ast.mk_appl (Ast.Constant "_indexnum") [ast]) + | indexnum_ast_tr (*"_indexnum"*) asts = raise Ast.AST ("indexnum_ast_tr", asts); -fun indexvar_ast_tr [] = Ast.Variable "some_index" - | indexvar_ast_tr asts = raise Ast.AST ("indexvar_ast_tr", asts); +fun indexvar_ast_tr (*"_indexvar"*) [] = + Ast.mk_appl (Ast.Constant "_index") [Ast.Variable "some_index"] + | indexvar_ast_tr (*"_indexvar"*) asts = raise Ast.AST ("indexvar_ast_tr", asts); + +fun index_tr (*"_index"*) [t] = t + | index_tr (*"_index"*) ts = raise TERM ("index_tr", ts); + + +(* implicit structures *) + +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); + +fun struct_tr structs (*"_struct"*) [Const ("_indexdefault", _)] = + Lexicon.free (the_struct structs 1) + | struct_tr structs (*"_struct"*) [t as (Const ("_indexnum", _) $ Const (s, _))] = + Lexicon.free (the_struct structs + (case Lexicon.read_nat s of Some n => n | None => raise TERM ("struct_tr", [t]))) + | struct_tr _ (*"_struct"*) ts = raise TERM ("struct_tr", ts); @@ -233,10 +271,9 @@ foldr (fn (x, t) => Lexicon.const "_abs" $ x $ t) (strip_abss strip_abs_vars strip_abs_body (eta_contr tm)); - -fun atomic_abs_tr' (x,T,t) = - let val [xT] = rename_wrt_term t [(x,T)]; - in (mark_boundT xT, subst_bound (mark_bound(fst xT), t)) end; +fun atomic_abs_tr' (x, T, t) = + let val [xT] = rename_wrt_term t [(x, T)] + in (mark_boundT xT, subst_bound (mark_bound (fst xT), t)) end; fun abs_ast_tr' (*"_abs"*) asts = (case Ast.unfold_ast_p "_abs" (Ast.Appl (Ast.Constant "_abs" :: asts)) of @@ -370,22 +407,49 @@ in (name, tr') end; +(* indexed syntax *) -(** pure_trfuns **) +fun index_ast_tr' (*"_index"*) [Ast.Appl [Ast.Constant "_struct", ast]] = ast + | index_ast_tr' _ = raise Match; + + +(* implicit structures *) + +fun the_struct' structs s = + [(case Lexicon.read_nat s of + Some i => Ast.Variable (the_struct structs i handle ERROR_MESSAGE _ => raise Match) + | None => raise Match)] |> Ast.mk_appl (Ast.Constant "_free"); +; + +fun struct_ast_tr' structs (*"_struct"*) [Ast.Constant "_indexdefault"] = + the_struct' structs "1" + | struct_ast_tr' structs (*"_struct"*) [Ast.Appl [Ast.Constant "_indexnum", Ast.Constant s]] = + the_struct' structs s + | struct_ast_tr' _ _ = raise Match; + + + +(** Pure translations **) val pure_trfuns = ([("_constify", constify_ast_tr), ("_appl", appl_ast_tr), ("_applC", applC_ast_tr), ("_lambda", lambda_ast_tr), ("_idtyp", idtyp_ast_tr), ("_bigimpl", bigimpl_ast_tr), - ("_indexvar", indexvar_ast_tr)], + ("_indexdefault", indexdefault_ast_tr), ("_indexnum", indexnum_ast_tr), + ("_indexvar", indexvar_ast_tr), ("_struct", struct_ast_tr)], [("_abs", abs_tr), ("_aprop", aprop_tr), ("_ofclass", ofclass_tr), - ("_TYPE", type_tr), ("_DDDOT", dddot_tr), ("_K", k_tr)], + ("_TYPE", type_tr), ("_DDDOT", dddot_tr), ("_K", k_tr), + ("_index", index_tr)], [("all", meta_conjunction_tr')], [("_abs", abs_ast_tr'), ("_idts", idtyp_ast_tr' "_idts"), - ("_pttrns", idtyp_ast_tr' "_pttrns"), ("==>", impl_ast_tr')]); + ("_pttrns", idtyp_ast_tr' "_pttrns"), ("==>", impl_ast_tr'), + ("_index", index_ast_tr')]); val pure_trfunsT = [("_mk_ofclass", mk_ofclass_tr'), ("TYPE", type_tr')]; +fun struct_trfuns structs = + ([], [("_struct", struct_tr structs)], [], [("_struct", struct_ast_tr' structs)]); + (** pt_to_ast **)