# HG changeset patch # User wenzelm # Date 975611255 -3600 # Node ID 81edb1d201ab78605eb4e808abeb15390c23b098 # Parent 7f239ef89c5031c156d683c56eb964a5f40757e9 schematic props; diff -r 7f239ef89c50 -r 81edb1d201ab src/Pure/Isar/proof_context.ML --- a/src/Pure/Isar/proof_context.ML Thu Nov 30 20:06:52 2000 +0100 +++ b/src/Pure/Isar/proof_context.ML Thu Nov 30 20:07:35 2000 +0100 @@ -38,7 +38,6 @@ val read_term: context -> string -> term val read_prop: context -> string -> term val read_terms: context -> string list -> term list - val read_props: context -> string list -> term list val read_termT_pats: context -> (string * typ) list -> term list val read_term_pats: typ -> context -> string list -> term list val read_prop_pats: context -> string list -> term list @@ -62,10 +61,18 @@ -> context * (term * (term list * term list)) list list val cert_propp: context * (term * (term list * term list)) list list -> context * (term * (term list * term list)) list list + val read_propp_schematic: context * (string * (string list * string list)) list list + -> context * (term * (term list * term list)) list list + val cert_propp_schematic: context * (term * (term list * term list)) list list + -> context * (term * (term list * term list)) list list val bind_propp: context * (string * (string list * string list)) list list -> context * (term list list * (context -> context)) val bind_propp_i: context * (term * (term list * term list)) list list -> context * (term list list * (context -> context)) + val bind_propp_schematic: context * (string * (string list * string list)) list list + -> context * (term list list * (context -> context)) + val bind_propp_schematic_i: context * (term * (term list * term list)) list list + -> context * (term list list * (context -> context)) val get_thm: context -> string -> thm val get_thm_closure: context -> string -> thm val get_thms: context -> string -> thm list @@ -404,8 +411,9 @@ transform_error (read (sign_of ctxt, def_sort ctxt)) s handle ERROR_MESSAGE msg => raise CONTEXT (msg, ctxt); -fun cert_typ_aux cert ctxt raw_T = cert (sign_of ctxt) raw_T - handle TYPE (msg, _, _) => raise CONTEXT (msg, ctxt); +fun cert_typ_aux cert ctxt raw_T = + cert (sign_of ctxt) raw_T + handle TYPE (msg, _, _) => raise CONTEXT (msg, ctxt); in @@ -417,7 +425,6 @@ end; - (* internalize Skolem constants *) fun fixes_of (Context {asms = (_, (fixes, _)), ...}) = fixes; @@ -499,7 +506,7 @@ let val maxidx = Int.max (Term.maxidx_of_typ T, Term.maxidx_of_typ U) in #1 (Type.unify (Sign.tsig_of (sign_of ctxt)) maxidx Vartab.empty (T, U)) end; -fun norm_term (ctxt as Context {binds, ...}) = +fun norm_term (ctxt as Context {binds, ...}) schematic = let (*raised when norm has no effect on a term, to do sharing instead of copying*) exception SAME; @@ -512,7 +519,9 @@ raise TYPE ("norm_term: ill-typed variable assigment", [T, U], [t, u]); val u' = Term.subst_TVars_Vartab env u; in norm u' handle SAME => u' end - | _ => raise CONTEXT ("Unbound schematic variable: " ^ Syntax.string_of_vname xi, ctxt)) + | _ => + if schematic then raise SAME + else raise CONTEXT ("Unbound schematic variable: " ^ Syntax.string_of_vname xi, ctxt)) | norm (Abs (a, T, body)) = Abs (a, T, norm body) | norm (Abs (_, _, body) $ t) = normh (subst_bound (t, body)) | norm (f $ t) = @@ -534,37 +543,50 @@ (* read terms *) -fun gen_read read app is_pat (ctxt as Context {defs = (_, _, (used, _)), ...}) s = +local + +fun gen_read read app is_pat schematic (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) - |> app (if is_pat then I else norm_term ctxt) + |> app (if is_pat then I else norm_term ctxt schematic) |> 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_termT_pats = #1 oo gen_read (read_def_termTs false) (apfst o map) true; +in + +val read_termTs = gen_read (read_def_termTs false) (apfst o map) false false; +val read_termT_pats = #1 oo gen_read (read_def_termTs false) (apfst o map) true false; fun read_term_pats T ctxt pats = read_termT_pats ctxt (map (rpair T) pats); val read_prop_pats = read_term_pats propT; -val read_term = gen_read (read_term_sg true) I false; -val read_prop = gen_read (read_prop_sg true) I false; -val read_terms = gen_read (read_terms_sg true) map false; +val read_term = gen_read (read_term_sg true) I false false; +val read_prop = gen_read (read_prop_sg true) I false false; +val read_terms = gen_read (read_terms_sg true) map false false; val read_props = gen_read (read_props_sg true) map false; +end; + (* certify terms *) -fun gen_cert cert is_pat ctxt t = t - |> (if is_pat then I else norm_term ctxt) +local + +fun gen_cert cert is_pat schematic ctxt t = t + |> (if is_pat then I else norm_term ctxt schematic) |> (fn t' => cert (sign_of ctxt) t' handle TERM (msg, _) => raise CONTEXT (msg, ctxt)); -val cert_term = gen_cert cert_term_sg false; -val cert_prop = gen_cert cert_prop_sg false; +in -fun cert_term_pats _ = map o gen_cert cert_term_sg true; -val cert_prop_pats = map o gen_cert cert_prop_sg true; +val cert_term = gen_cert cert_term_sg false false; +val cert_prop = gen_cert cert_prop_sg false false; +val cert_props = map oo gen_cert cert_prop_sg false; + +fun cert_term_pats _ = map o gen_cert cert_term_sg true false; +val cert_prop_pats = map o gen_cert cert_prop_sg true false; + +end; (* declare terms *) @@ -757,21 +779,35 @@ (* simult_matches *) +local + +val add_vars = Term.foldl_aterms (fn (vs, Var (xi, _)) => xi ins vs | (vs, _) => vs); +fun vars_of ts = foldl add_vars ([], ts); + +in + fun simult_matches ctxt [] = [] | simult_matches ctxt pairs = let + fun fail () = raise CONTEXT ("Pattern match failed!", ctxt); + val maxidx = foldl (fn (i, (t1, t2)) => Int.max (i, Int.max (Term.maxidx_of_term t1, Term.maxidx_of_term t2))) (~1, pairs); - val envs = Unify.smash_unifiers (sign_of ctxt, Envir.empty maxidx, pairs); - val env = (*pick first result*) + val envs = Unify.smash_unifiers (sign_of ctxt, Envir.empty maxidx, + map swap pairs); (*prefer assignment of variables from patterns*) + val env = (case Seq.pull envs of - None => raise CONTEXT ("Pattern match failed!", ctxt) - | Some (env, _) => env); - val add_dom = Term.foldl_aterms (fn (dom, Var (xi, _)) => xi ins dom | (dom, _) => dom); - val domain = foldl add_dom ([], map #1 pairs); + None => fail () + | Some (env, _) => env); (*ignore further results*) + val domain = filter_out Term.is_replaced_dummy_pattern (vars_of (map #1 pairs)); + val _ = (*may not assign variables from text*) + if null (map #1 (Envir.alist_of env) inter vars_of (map #2 pairs)) then () + else fail (); fun norm_bind (xi, t) = if xi mem domain then Some (xi, Envir.norm_term env t) else None; in mapfilter norm_bind (Envir.alist_of env) end; +end; + (* add_binds(_i) *) @@ -782,13 +818,16 @@ fun gen_binds prep binds ctxt = foldl (gen_bind prep) (ctxt, binds); +fun drop_schematic (b as (xi, Some t)) = if null (Term.term_vars t) then b else (xi, None) + | drop_schematic b = b; + in val add_binds = gen_binds read_term; val add_binds_i = gen_binds cert_term; -val auto_bind_goal = add_binds_i o AutoBind.goal; -val auto_bind_facts = add_binds_i oo AutoBind.facts; +val auto_bind_goal = add_binds_i o map drop_schematic o AutoBind.goal; +val auto_bind_facts = (add_binds_i o map drop_schematic) oo AutoBind.facts; end; @@ -831,7 +870,7 @@ local -fun prep_propp prep_props prep_pats (context, args) = +fun prep_propp schematic prep_props prep_pats (context, args) = let fun prep ((ctxt, prop :: props), (_, (raw_pats1, raw_pats2))) = let @@ -841,7 +880,7 @@ in ((ctxt', props), (prop, (take (len1, pats), drop (len1, pats)))) end | prep _ = sys_error "prep_propp"; val ((context', _), propp) = foldl_map (foldl_map prep) - ((context, prep_props context (flat (map (map fst) args))), args); + ((context, prep_props schematic context (flat (map (map fst) args))), args); in (context', propp) end; fun matches ctxt (prop, (pats1, pats2)) = @@ -853,17 +892,22 @@ val binds = flat (flat (map (map (matches ctxt')) args)); val propss = map (map #1) args; - (*generalize result: context evaluated now, binds to be added later*) + (*generalize result: context evaluated now, binds added later*) val gen = generalize ctxt' ctxt; fun gen_binds c = c |> add_binds_i (map (apsnd (Some o gen)) binds); in (ctxt' |> add_binds_i (map (apsnd Some) binds), (propss, gen_binds)) end; in -val read_propp = prep_propp read_props read_prop_pats; -val cert_propp = prep_propp (map o cert_prop) cert_prop_pats; -val bind_propp = gen_bind_propp read_propp; -val bind_propp_i = gen_bind_propp cert_propp; +val read_propp = prep_propp false read_props read_prop_pats; +val cert_propp = prep_propp false cert_props cert_prop_pats; +val read_propp_schematic = prep_propp true read_props read_prop_pats; +val cert_propp_schematic = prep_propp true cert_props cert_prop_pats; + +val bind_propp = gen_bind_propp read_propp; +val bind_propp_i = gen_bind_propp cert_propp; +val bind_propp_schematic = gen_bind_propp read_propp_schematic; +val bind_propp_schematic_i = gen_bind_propp cert_propp_schematic; end;