# HG changeset patch # User wenzelm # Date 938719236 -7200 # Node ID 460fedf14b09006f3a2df0d8cd03af47c19382c8 # Parent 062a782d7402c52c91c7ce29601f2210d284bc60 export def_sort, def_type; fix_i: typ option; init: maxidx = 0 is workaround for obscure bug in Unify.smash_unifiers; diff -r 062a782d7402 -r 460fedf14b09 src/Pure/Isar/proof_context.ML --- a/src/Pure/Isar/proof_context.ML Thu Sep 30 20:49:06 1999 +0200 +++ b/src/Pure/Isar/proof_context.ML Thu Sep 30 21:20:36 1999 +0200 @@ -21,6 +21,8 @@ val strings_of_context: context -> string list val print_proof_data: theory -> unit val init: theory -> context + val def_sort: context -> indexname -> sort option + val def_type: context -> bool -> indexname -> typ option val read_typ: context -> string -> typ val cert_typ: context -> typ -> typ val read_termTs: context -> (string * typ) list -> term list * (indexname * typ) list @@ -59,7 +61,7 @@ -> (string * context attribute list * (term * (term list * term list)) list) list -> context -> context * ((string * thm list) list * thm list) val fix: (string list * string option) list -> context -> context - val fix_i: (string list * typ) list -> context -> context + val fix_i: (string list * typ option) list -> context -> context val setup: (theory -> theory) list end; @@ -84,7 +86,7 @@ {thy: theory, (*current theory*) data: Object.T Symtab.table, (*user data*) asms: - ((cterm * ((int -> tactic) * (int -> tactic))) list * (*assumes: A ==> _*) + ((cterm * ((int -> tactic) * (int -> tactic))) list * (*assumes: A ==> _*) (string * thm list) list) * ((string * string) list * string list), (*fixes: !!x. _*) binds: (term * typ) option Vartab.table, (*term bindings*) @@ -301,18 +303,29 @@ fun init thy = let val data = Symtab.map (fn (_, (f, _)) => f thy) (ProofDataData.get thy) in make_context (thy, data, (([], []), ([], [])), Vartab.empty, Symtab.empty, - (Vartab.empty, Vartab.empty, ~1, [])) + (Vartab.empty, Vartab.empty, 0, [])) + (*Note: maxidx = 0 is workaround for obscure bug in Unify.smash_unifiers*) end; +(** default sorts and types **) + +fun def_sort (Context {defs = (_, sorts, _, _), ...}) xi = Vartab.lookup (sorts, xi); + +fun def_type (Context {binds, defs = (types, _, _, _), ...}) is_pat xi = + (case Vartab.lookup (types, xi) of + None => + if is_pat then None + else (case Vartab.lookup (binds, xi) of Some (Some (_, T)) => Some T | _ => None) + | some => some); + + (** prepare types **) -fun read_typ (ctxt as Context {defs = (_, sorts, _, _), ...}) s = - let fun def_sort xi = Vartab.lookup (sorts, xi) in - transform_error (Sign.read_typ (sign_of ctxt, def_sort)) s - handle ERROR_MESSAGE msg => raise CONTEXT (msg, ctxt) - end; +fun read_typ ctxt s = + transform_error (Sign.read_typ (sign_of ctxt, def_sort ctxt)) s + handle ERROR_MESSAGE msg => raise CONTEXT (msg, ctxt); fun cert_typ ctxt raw_T = Sign.certify_typ (sign_of ctxt) raw_T @@ -431,24 +444,13 @@ (* read terms *) -fun gen_read read app is_pat (ctxt as Context {binds, defs = (types, sorts, _, used), ...}) s = - let - fun def_type xi = - (case Vartab.lookup (types, xi) of - None => - if is_pat then None - else (case Vartab.lookup (binds, xi) of Some (Some (_, T)) => Some T | _ => None) - | some => some); - - fun def_sort xi = Vartab.lookup (sorts, xi); - in - (transform_error (read (sign_of ctxt) (def_type, def_sort, used)) s - handle TERM (msg, _) => raise CONTEXT (msg, ctxt) - | ERROR_MESSAGE msg => raise CONTEXT (msg, ctxt)) - |> app (intern_skolem ctxt true) - |> app (if is_pat then I else norm_term ctxt) - |> app (if is_pat then prepare_dummies else (reject_dummies ctxt)) - end; +fun gen_read read app is_pat (ctxt as Context {defs = (_, _, _, used), ...}) s = + (transform_error (read (sign_of ctxt) (def_type ctxt is_pat, def_sort ctxt, used)) s + handle TERM (msg, _) => raise CONTEXT (msg, ctxt) + | ERROR_MESSAGE msg => raise CONTEXT (msg, ctxt)) + |> app (intern_skolem ctxt true) + |> app (if is_pat then I else norm_term ctxt) + |> app (if is_pat then prepare_dummies else (reject_dummies ctxt)); val read_termTs = gen_read (read_def_termTs false) (apfst o map) false; val read_term = gen_read (read_term_sg true) I false; @@ -487,9 +489,9 @@ | (used, TVar ((x, _), _)) => x ins used | (used, _) => used)); -fun ins_skolem def_type = foldr +fun ins_skolem def_ty = foldr (fn ((x, x'), types) => - (case def_type x' of + (case def_ty x' of Some T => Vartab.update (((x, ~1), T), types) | None => types)); @@ -537,7 +539,7 @@ | del_upd_bind (ctxt, (xi, Some t)) = upd_bind (ctxt, (xi, t)); fun update_binds bs ctxt = foldl upd_bind (ctxt, bs); -fun update_binds_env env = (*Envir.norm_term ensures proper type instantiation*) +fun update_binds_env env = (*Note: Envir.norm_term ensures proper type instantiation*) update_binds (map (apsnd (Envir.norm_term env)) (Envir.alist_of env)); fun delete_update_binds bs ctxt = foldl del_upd_bind (ctxt, bs); @@ -700,7 +702,7 @@ fun gen_fix prep check (ctxt, (x, raw_T)) = (check_skolem ctxt check x; ctxt - |> (case prep ctxt raw_T of None => I | Some T => declare_term (Free (x, T))) + |> (case (apsome o prep) ctxt raw_T of None => I | Some T => declare_term (Free (x, T))) |> map_context (fn (thy, data, (assumes, (fixes, names)), binds, thms, defs) => let val x' = variant names x in (thy, data, (assumes, ((x, Syntax.skolem x') :: fixes, x' :: names)), binds, thms, defs) @@ -709,8 +711,8 @@ fun gen_fixs prep check vars ctxt = foldl (gen_fix prep check) (ctxt, flat (map (fn (xs, T) => map (rpair T) xs) vars)); -val fix = gen_fixs (apsome o read_typ) true; -val fix_i = gen_fixs (Some oo cert_typ) false; +val fix = gen_fixs read_typ true; +val fix_i = gen_fixs cert_typ false;