# HG changeset patch # User wenzelm # Date 1139255993 -3600 # Node ID 93903be7ff66e78e201402a3e7fe3b999b81f59e # Parent 0388d0b0f3d521547ff7357698311002a06d5517 norm_term: Sign.const_expansion, Envir.expand_atom; diff -r 0388d0b0f3d5 -r 93903be7ff66 src/Pure/Isar/proof_context.ML --- a/src/Pure/Isar/proof_context.ML Mon Feb 06 20:59:52 2006 +0100 +++ b/src/Pure/Isar/proof_context.ML Mon Feb 06 20:59:53 2006 +0100 @@ -180,7 +180,7 @@ assms: ((cterm list * export) list * (*assumes and views: A ==> _*) (string * thm list) list), (*prems: A |- A*) - binds: (term * typ) Vartab.table, (*term bindings*) + binds: (typ * term) Vartab.table, (*term bindings*) thms: NameSpace.naming * (*local thms*) thm list NameSpace.table * FactIndex.T, cases: (string * (RuleCases.T * bool)) list, (*local contexts*) @@ -400,7 +400,7 @@ (case Vartab.lookup types xi of NONE => if pattern then NONE - else Vartab.lookup binds xi |> Option.map (TypeInfer.polymorphicT o #2) + else Vartab.lookup binds xi |> Option.map (TypeInfer.polymorphicT o #1) | some => some) end; @@ -516,30 +516,32 @@ (* norm_term *) -(*beta normal form for terms (not eta normal form), chase variables in - bindings environment (code taken from Pure/envir.ML)*) - -fun unifyT ctxt (T, U) = - let val maxidx = Int.max (Term.maxidx_of_typ T, Term.maxidx_of_typ U) - in #1 (Sign.typ_unify (theory_of ctxt) (T, U) (Vartab.empty, maxidx)) end; +(* + - expand abbreviations (polymorphic Consts) + - expand term bindings (polymorphic Vars) + - beta contraction +*) fun norm_term ctxt schematic = let - (*raised when norm has no effect on a term, to do sharing instead of copying*) - exception SAME; + val thy = theory_of ctxt; + val tsig = Sign.tsig_of thy; + val expansion = Sign.const_expansion thy; + val binding = Vartab.lookup (binds_of ctxt); - val binds = binds_of ctxt; - fun norm (t as Var (xi, T)) = - (case Vartab.lookup binds xi of - SOME (u, U) => - let - val env = unifyT ctxt (T, U) handle Type.TUNIFY => - raise TYPE ("norm_term: ill-typed variable assignment", [T, U], [t, u]); - val u' = Envir.subst_TVars env u; - in norm u' handle SAME => u' end + exception SAME; + fun norm (Const c) = + (case expansion c of + SOME u => (norm u handle SAME => u) + | NONE => raise SAME) + | norm (Var (xi, T)) = + (case binding xi of + SOME b => + let val u = Envir.expand_atom tsig T b + in norm u handle SAME => u end | NONE => - if schematic then raise SAME - else error ("Unbound schematic variable: " ^ Syntax.string_of_vname xi)) + if schematic then raise SAME + else error ("Unbound schematic variable: " ^ Syntax.string_of_vname xi)) | norm (Abs (a, T, body)) = Abs (a, T, norm body) | norm (Abs (_, _, body) $ t) = normh (subst_bound (t, body)) | norm (f $ t) = @@ -651,7 +653,7 @@ fold_atyps (fn TFree (x, _) => insert (op =) x | _ => I)); val ins_occs = fold_term_types (fn t => - fold_atyps (fn TFree (x, _) => Symtab.update_multi (x, t) | _ => I)); + fold_atyps (fn TFree (x, _) => Symtab.update_list (x, t) | _ => I)); fun ins_skolem def_ty = fold_rev (fn (x, x') => (case def_ty x' of @@ -748,7 +750,7 @@ val occs_outer = type_occs_of outer; fun add a gen = if Symtab.defined occs_outer a orelse - exists still_fixed (Symtab.lookup_multi occs_inner a) + exists still_fixed (Symtab.lookup_list occs_inner a) then gen else a :: gen; in fn tfrees => fold add tfrees [] end; @@ -812,7 +814,7 @@ val t' = if null (Term.term_tvars t \\ Term.typ_tvars T) then t else Var ((x ^ "_has_extra_type_vars_on_rhs", i), T); - in declare_term t' #> map_binds (Vartab.update ((x, i), (t', T))) end; + in declare_term t' #> map_binds (Vartab.update ((x, i), (T, t'))) end; fun del_upd_bind (xi, NONE) = del_bind xi | del_upd_bind (xi, SOME t) = upd_bind (xi, t); @@ -1337,7 +1339,7 @@ fun pretty_binds ctxt = let val binds = binds_of ctxt; - fun prt_bind (xi, (t, T)) = pretty_term ctxt (Logic.mk_equals (Var (xi, T), t)); + fun prt_bind (xi, (T, t)) = pretty_term ctxt (Logic.mk_equals (Var (xi, T), t)); in if Vartab.is_empty binds andalso not (! verbose) then [] else [Pretty.big_list "term bindings:" (map prt_bind (Vartab.dest binds))]