| author | wenzelm |
| Wed, 31 Aug 2005 15:46:40 +0200 | |
| changeset 17203 | 29b2563f5c11 |
| parent 17202 | d364e0fd9c2f |
| child 17204 | 6f0f8b6cd3f3 |
--- a/TFL/rules.ML Wed Aug 31 15:46:39 2005 +0200 +++ b/TFL/rules.ML Wed Aug 31 15:46:40 2005 +0200 @@ -308,8 +308,7 @@ let val gth = forall_intr v th val {prop=Const("all",_)$Abs(x,ty,rst),sign,...} = rep_thm gth val P' = Abs(x,ty, HOLogic.dest_Trueprop rst) (* get rid of trueprop *) - val tsig = Sign.tsig_of sign - val theta = Pattern.match tsig (P,P') + val theta = Pattern.match sign (P,P') val allI2 = instantiate (certify sign theta) allI val thm = Thm.implies_elim allI2 gth val {prop = tp $ (A $ Abs(_,_,M)),sign,...} = rep_thm thm
--- a/TFL/thry.ML Wed Aug 31 15:46:39 2005 +0200 +++ b/TFL/thry.ML Wed Aug 31 15:46:40 2005 +0200 @@ -34,8 +34,7 @@ fun match_term thry pat ob = let - val tsig = Sign.tsig_of (Theory.sign_of thry) - val (ty_theta, tm_theta) = Pattern.match tsig (pat,ob) + val (ty_theta, tm_theta) = Pattern.match thry (pat,ob) fun tmbind (ixn, (T, t)) = (Var (ixn, Envir.typ_subst_TVars ty_theta T), t) in (map tmbind (Vartab.dest tm_theta), map tybind (Vartab.dest ty_theta)) end; @@ -51,7 +50,7 @@ *---------------------------------------------------------------------------*) fun typecheck thry t = - Thm.cterm_of (Theory.sign_of thry) t + Thm.cterm_of thry t handle TYPE (msg, _, _) => raise THRY_ERR "typecheck" msg | TERM (msg, _) => raise THRY_ERR "typecheck" msg;
--- a/src/HOL/Extraction.thy Wed Aug 31 15:46:39 2005 +0200 +++ b/src/HOL/Extraction.thy Wed Aug 31 15:46:40 2005 +0200 @@ -38,11 +38,11 @@ [Extraction.add_types [("bool", ([], NONE)), ("set", ([realizes_set_proc], SOME mk_realizes_set))], - Extraction.set_preprocessor (fn sg => + Extraction.set_preprocessor (fn thy => Proofterm.rewrite_proof_notypes ([], ("HOL/elim_cong", RewriteHOLProof.elim_cong) :: ProofRewriteRules.rprocs true) o - Proofterm.rewrite_proof (Sign.tsig_of sg) + Proofterm.rewrite_proof thy (RewriteHOLProof.rews, ProofRewriteRules.rprocs true) o ProofRewriteRules.elim_vars (curry Const "arbitrary"))] end
--- a/src/HOL/Tools/recfun_codegen.ML Wed Aug 31 15:46:39 2005 +0200 +++ b/src/HOL/Tools/recfun_codegen.ML Wed Aug 31 15:46:40 2005 +0200 @@ -60,9 +60,8 @@ fun del_redundant thy eqs [] = eqs | del_redundant thy eqs (eq :: eqs') = let - val tsig = Sign.tsig_of (sign_of thy); val matches = curry - (Pattern.matches tsig o pairself (lhs_of o fst)) + (Pattern.matches thy o pairself (lhs_of o fst)) in del_redundant thy (eq :: eqs) (filter_out (matches eq) eqs') end; fun get_equations thy defs (s, T) =
--- a/src/Pure/IsaPlanner/isa_fterm.ML Wed Aug 31 15:46:39 2005 +0200 +++ b/src/Pure/IsaPlanner/isa_fterm.ML Wed Aug 31 15:46:40 2005 +0200 @@ -31,7 +31,7 @@ val add_upterm : UpTerm -> FcTerm -> FcTerm val clean_match_ft : - Type.tsig -> + theory -> Term.term -> FcTerm -> ( @@ -457,9 +457,9 @@ bound variables. New names have been introduced to make sure they are unique w.r.t all names in the term and each other. usednames' is oldnames + new names. *) -fun clean_match_ft tsig pat ft = +fun clean_match_ft thy pat ft = let val (t, (FakeTs,Ts,absterm)) = prepmatch ft in - case TermLib.clean_match tsig (pat, t) of + case TermLib.clean_match thy (pat, t) of NONE => NONE | SOME insts => SOME (insts, FakeTs, Ts, absterm) end; (* ix = max var index *)
--- a/src/Pure/IsaPlanner/term_lib.ML Wed Aug 31 15:46:39 2005 +0200 +++ b/src/Pure/IsaPlanner/term_lib.ML Wed Aug 31 15:46:40 2005 +0200 @@ -20,7 +20,7 @@ val current_sign : unit -> Sign.sg (* Matching/unification with exceptions handled *) - val clean_match : Type.tsig -> Term.term * Term.term + val clean_match : theory -> Term.term * Term.term -> ((Term.indexname * (Term.sort * Term.typ)) list * (Term.indexname * (Term.typ * Term.term)) list) option val clean_unify : Sign.sg -> int -> Term.term * Term.term @@ -83,7 +83,7 @@ val has_new_vars : Term.term * Term.term -> bool val has_new_typ_vars : Term.term * Term.term -> bool (* checks to see if the lhs -> rhs is a invalid rewrite rule *) - val is_not_valid_rwrule : Type.tsig -> (Term.term * Term.term) -> bool + val is_not_valid_rwrule : theory -> (Term.term * Term.term) -> bool (* get the frees in a term that are of atomic type, ie non-functions *) val atomic_frees_of_term : Term.term -> (string * Term.typ) list @@ -143,8 +143,8 @@ (* Higher order matching with exception handled *) (* returns optional instantiation *) -fun clean_match tsig (a as (pat, t)) = - let val (tyenv, tenv) = Pattern.match tsig a +fun clean_match thy (a as (pat, t)) = + let val (tyenv, tenv) = Pattern.match thy a in SOME (Vartab.dest tyenv, Vartab.dest tenv) end handle Pattern.MATCH => NONE; (* Higher order unification with exception handled, return the instantiations *) @@ -408,11 +408,11 @@ which embeds into the rhs, this would be much closer to the normal notion of valid wave rule - ie there exists at least one case where it is a valid wave rule... *) - fun is_not_valid_rwrule tysig (lhs, rhs) = + fun is_not_valid_rwrule thy (lhs, rhs) = Term.is_Var (Term.head_of lhs) (* if lhs is essentially just a var *) orelse has_new_vars (lhs,rhs) orelse has_new_typ_vars (lhs,rhs) - orelse Pattern.matches_subterm tysig (lhs, rhs); + orelse Pattern.matches_subterm thy (lhs, rhs); (* first term contains the second in some name convertable way... *)
--- a/src/Pure/Isar/locale.ML Wed Aug 31 15:46:39 2005 +0200 +++ b/src/Pure/Isar/locale.ML Wed Aug 31 15:46:40 2005 +0200 @@ -287,19 +287,18 @@ fun dest regs = map (apfst untermify) (Termtab.dest regs); (* registrations that subsume t *) - fun subsumers tsig t regs = - List.filter (fn (t', _) => Pattern.matches tsig (t', t)) (Termtab.dest regs); + fun subsumers thy t regs = + List.filter (fn (t', _) => Pattern.matches thy (t', t)) (Termtab.dest regs); (* look up registration, pick one that subsumes the query *) fun lookup sign (regs, ts) = let - val tsig = Sign.tsig_of sign; val t = termify ts; - val subs = subsumers tsig t regs; + val subs = subsumers sign t regs; in (case subs of [] => NONE | ((t', (attn, thms)) :: _) => let - val (tinst, inst) = Pattern.match tsig (t', t); + val (tinst, inst) = Pattern.match sign (t', t); (* thms contain Frees, not Vars *) val tinst' = tinst |> Vartab.dest |> map (fn ((x, 0), (_, T)) => (x, Type.unvarifyT T)) @@ -316,13 +315,12 @@ additionally returns registrations that are strictly subsumed *) fun insert sign (ts, attn) regs = let - val tsig = Sign.tsig_of sign; val t = termify ts; - val subs = subsumers tsig t regs ; + val subs = subsumers sign t regs ; in (case subs of [] => let val sups = - List.filter (fn (t', _) => Pattern.matches tsig (t, t')) (Termtab.dest regs); + List.filter (fn (t', _) => Pattern.matches sign (t, t')) (Termtab.dest regs); val sups' = map (apfst untermify) sups in (Termtab.update ((t, (attn, [])), regs), sups') end | _ => (regs, []))
--- a/src/Pure/Isar/proof.ML Wed Aug 31 15:46:39 2005 +0200 +++ b/src/Pure/Isar/proof.ML Wed Aug 31 15:46:40 2005 +0200 @@ -490,7 +490,6 @@ [Pretty.str (string_of_int ngoals ^ " unsolved goal(s)!")])))); val {hyps, thy, ...} = Thm.rep_thm raw_th; - val tsig = Sign.tsig_of thy; val casms = List.concat (map #1 (ProofContext.assumptions_of (context_of state))); val bad_hyps = Library.gen_rems Term.aconv (hyps, map Thm.term_of casms); @@ -500,7 +499,7 @@ in conditional (not (null bad_hyps)) (fn () => err ("Additional hypotheses:\n" ^ cat_lines (map (ProofContext.string_of_term ctxt) bad_hyps))); - conditional (exists (not o Pattern.matches tsig) (ts ~~ map Thm.prop_of ths)) (fn () => + conditional (exists (not o Pattern.matches thy) (ts ~~ map Thm.prop_of ths)) (fn () => err ("Proved a different theorem: " ^ Pretty.string_of (ProofContext.pretty_thm ctxt th))); ths end;
--- a/src/Pure/Proof/extraction.ML Wed Aug 31 15:46:39 2005 +0200 +++ b/src/Pure/Proof/extraction.ML Wed Aug 31 15:46:40 2005 +0200 @@ -88,10 +88,8 @@ fun condrew thy rules procs = let - val tsig = Sign.tsig_of thy; - fun rew tm = - Pattern.rewrite_term tsig [] (condrew' :: procs) tm + Pattern.rewrite_term thy [] (condrew' :: procs) tm and condrew' tm = let val cache = ref ([] : (term * term) list); @@ -105,7 +103,7 @@ let fun ren t = getOpt (Term.rename_abs tm1 tm t, t); val inc = Logic.incr_indexes ([], maxidx_of_term tm + 1); - val env as (Tenv, tenv) = Pattern.match tsig (inc tm1, tm); + val env as (Tenv, tenv) = Pattern.match thy (inc tm1, tm); val prems' = map (pairself (Envir.subst_vars env o inc o ren)) prems; val env' = Envir.Envir {maxidx = Library.foldl Int.max @@ -321,7 +319,7 @@ let val name = Thm.name_of_thm thm; val _ = assert (name <> "") "add_realizers: unnamed theorem"; - val prop = Pattern.rewrite_term (Sign.tsig_of thy') + val prop = Pattern.rewrite_term thy' (map (Logic.dest_equals o prop_of) defs) [] (prop_of thm); val vars = vars_of prop; val vars' = filter_out (fn v => @@ -350,7 +348,7 @@ ExtractionData.get thy'; val procs = List.concat (map (fst o snd) types); val eqns = Net.merge (K false) (#net realizes_eqns, #net typeof_eqns); - val prop' = Pattern.rewrite_term (Sign.tsig_of thy') + val prop' = Pattern.rewrite_term thy' (map (Logic.dest_equals o prop_of) defs) [] prop; in freeze_thaw (condrew thy' eqns (procs @ [typeof_proc (Sign.defaultS thy') vs, rlz_proc]))
--- a/src/Pure/Proof/proof_rewrite_rules.ML Wed Aug 31 15:46:39 2005 +0200 +++ b/src/Pure/Proof/proof_rewrite_rules.ML Wed Aug 31 15:46:40 2005 +0200 @@ -10,7 +10,7 @@ val rew : bool -> typ list -> Proofterm.proof -> Proofterm.proof option val rprocs : bool -> (string * (typ list -> Proofterm.proof -> Proofterm.proof option)) list val rewrite_terms : (term -> term) -> Proofterm.proof -> Proofterm.proof - val elim_defs : Sign.sg -> bool -> thm list -> Proofterm.proof -> Proofterm.proof + val elim_defs : theory -> bool -> thm list -> Proofterm.proof -> Proofterm.proof val elim_vars : (typ -> term) -> Proofterm.proof -> Proofterm.proof end; @@ -235,9 +235,8 @@ | (_, []) => prf | (prf', ts) => proof_combt' (insert_refl defs Ts prf', ts)); -fun elim_defs sign r defs prf = +fun elim_defs thy r defs prf = let - val tsig = Sign.tsig_of sign; val defs' = map (Logic.dest_equals o prop_of o Drule.abs_def) defs val defnames = map Thm.name_of_thm defs; val f = if not r then I else @@ -248,9 +247,9 @@ else map (pair s o SOME o fst) (filter_out (fn (p, _) => null (term_consts p inter cnames)) ps)) (Symtab.dest (thms_of_proof prf Symtab.empty))) - in Reconstruct.expand_proof sign thms end + in Reconstruct.expand_proof thy thms end in - rewrite_terms (Pattern.rewrite_term tsig defs' []) + rewrite_terms (Pattern.rewrite_term thy defs' []) (insert_refl defnames [] (f prf)) end;
--- a/src/Pure/drule.ML Wed Aug 31 15:46:39 2005 +0200 +++ b/src/Pure/drule.ML Wed Aug 31 15:46:40 2005 +0200 @@ -852,7 +852,7 @@ fun norm_hhf thy t = if is_norm_hhf t then t - else Pattern.rewrite_term (Sign.tsig_of thy) [Logic.dest_equals (prop_of norm_hhf_eq)] [] t; + else Pattern.rewrite_term thy [Logic.dest_equals (prop_of norm_hhf_eq)] [] t; (*** Instantiate theorem th, reading instantiations in theory thy ****)
--- a/src/Pure/goals.ML Wed Aug 31 15:46:39 2005 +0200 +++ b/src/Pure/goals.ML Wed Aug 31 15:46:40 2005 +0200 @@ -752,7 +752,7 @@ (map (Sign.string_of_term thy) (List.filter (fn x => (not (in_locale [x] thy))) hyps))) - else if Pattern.matches (Sign.tsig_of thy) + else if Pattern.matches thy (Envir.beta_norm (term_of chorn), Envir.beta_norm prop) then final_th else !result_error_fn state "proved a different theorem"
--- a/src/Pure/meta_simplifier.ML Wed Aug 31 15:46:39 2005 +0200 +++ b/src/Pure/meta_simplifier.ML Wed Aug 31 15:46:40 2005 +0200 @@ -437,7 +437,7 @@ *) exists (fn t => Logic.occs (lhs, t)) (rhs :: prems) orelse - null prems andalso Pattern.matches (Sign.tsig_of thy) (lhs, rhs) + null prems andalso Pattern.matches thy (lhs, rhs) (*the condition "null prems" is necessary because conditional rewrites with extra variables in the conditions may terminate although the rhs is an instance of the lhs; example: ?m < ?n ==> f(?n) == f(?m)*) @@ -796,7 +796,6 @@ val eta_thm = Thm.eta_conversion t; val eta_t' = rhs_of eta_thm; val eta_t = term_of eta_t'; - val tsigt = Sign.tsig_of thyt; fun rew {thm, name, lhs, elhs, fo, perm} = let val {thy, prop, maxidx, ...} = rep_thm thm; @@ -853,7 +852,7 @@ fun proc_rews [] = NONE | proc_rews (Proc {name, proc, lhs, ...} :: ps) = - if Pattern.matches tsigt (Thm.term_of lhs, Thm.term_of t) then + if Pattern.matches thyt (Thm.term_of lhs, Thm.term_of t) then (debug_term false ("Trying procedure " ^ quote name ^ " on:") ss thyt eta_t; case transform_failure (curry SIMPROC_FAIL name) (fn () => proc thyt ss eta_t) () of @@ -1136,7 +1135,7 @@ (*simple term rewriting -- no proof*) fun rewrite_term thy rules procs = - Pattern.rewrite_term (Sign.tsig_of thy) (map decomp_simp' rules) procs; + Pattern.rewrite_term thy (map decomp_simp' rules) procs; fun rewrite_thm mode prover ss = Drule.fconv_rule (rewrite_cterm mode prover ss);
--- a/src/Pure/pattern.ML Wed Aug 31 15:46:39 2005 +0200 +++ b/src/Pure/pattern.ML Wed Aug 31 15:46:40 2005 +0200 @@ -15,29 +15,26 @@ signature PATTERN = sig - val trace_unify_fail : bool ref - val aeconv : term * term -> bool - val eta_contract : term -> term - val eta_long : typ list -> term -> term - val beta_eta_contract : term -> term - val eta_contract_atom : term -> term - val match : Type.tsig -> term * term - -> Type.tyenv * Envir.tenv - val first_order_match : Type.tsig -> term * term - -> Type.tyenv * Envir.tenv - val matches : Type.tsig -> term * term -> bool - val matches_subterm : Type.tsig -> term * term -> bool - val unify : Sign.sg * Envir.env * (term * term)list -> Envir.env - val first_order : term -> bool - val pattern : term -> bool - val rewrite_term : Type.tsig -> (term * term) list -> (term -> term option) list - -> term -> term + val trace_unify_fail: bool ref + val aeconv: term * term -> bool + val eta_contract: term -> term + val eta_long: typ list -> term -> term + val beta_eta_contract: term -> term + val eta_contract_atom: term -> term + val match: theory -> term * term -> Type.tyenv * Envir.tenv + val first_order_match: theory -> term * term -> Type.tyenv * Envir.tenv + val matches: theory -> term * term -> bool + val matches_subterm: theory -> term * term -> bool + val unify: theory * Envir.env * (term * term)list -> Envir.env + val first_order: term -> bool + val pattern: term -> bool + val rewrite_term: theory -> (term * term) list -> (term -> term option) list -> term -> term exception Unif exception MATCH exception Pattern end; -structure Pattern : PATTERN = +structure Pattern: PATTERN = struct exception Unif; @@ -45,16 +42,16 @@ val trace_unify_fail = ref false; -fun string_of_term sg env binders t = Sign.string_of_term sg +fun string_of_term thy env binders t = Sign.string_of_term thy (Envir.norm_term env (subst_bounds(map Free binders,t))); fun bname binders i = fst(List.nth(binders,i)); fun bnames binders is = space_implode " " (map (bname binders) is); -fun typ_clash sg (tye,T,U) = +fun typ_clash thy (tye,T,U) = if !trace_unify_fail - then let val t = Sign.string_of_typ sg (Envir.norm_type tye T) - and u = Sign.string_of_typ sg (Envir.norm_type tye U) + then let val t = Sign.string_of_typ thy (Envir.norm_type tye T) + and u = Sign.string_of_typ thy (Envir.norm_type tye U) in tracing("The following types do not unify:\n" ^ t ^ "\n" ^ u) end else () @@ -72,11 +69,11 @@ if !trace_unify_fail then clash (boundVar binders i) s else () -fun proj_fail sg (env,binders,F,_,is,t) = +fun proj_fail thy (env,binders,F,_,is,t) = if !trace_unify_fail then let val f = Syntax.string_of_vname F val xs = bnames binders is - val u = string_of_term sg env binders t + val u = string_of_term thy env binders t val ys = bnames binders (loose_bnos t \\ is) in tracing("Cannot unify variable " ^ f ^ " (depending on bound variables " ^ xs ^ ")\nwith term " ^ u ^ @@ -84,10 +81,10 @@ end else () -fun ocheck_fail sg (F,t,binders,env) = +fun ocheck_fail thy (F,t,binders,env) = if !trace_unify_fail then let val f = Syntax.string_of_vname F - val u = string_of_term sg env binders t + val u = string_of_term thy env binders t in tracing("Variable " ^ f ^ " occurs in term\n" ^ u ^ "\nCannot unify!\n") end @@ -225,29 +222,29 @@ end; in if xless(G,F) then ff(F,Fty,is,G,Gty,js) else ff(G,Gty,js,F,Fty,is) end -fun unify_types sg (T,U, env as Envir.Envir{asol,iTs,maxidx}) = +fun unify_types thy (T,U, env as Envir.Envir{asol,iTs,maxidx}) = if T=U then env - else let val (iTs',maxidx') = Sign.typ_unify sg (U, T) (iTs, maxidx) + else let val (iTs',maxidx') = Sign.typ_unify thy (U, T) (iTs, maxidx) in Envir.Envir{asol=asol,maxidx=maxidx',iTs=iTs'} end - handle Type.TUNIFY => (typ_clash sg (iTs,T,U); raise Unif); + handle Type.TUNIFY => (typ_clash thy (iTs,T,U); raise Unif); -fun unif sg binders (env,(s,t)) = case (Envir.head_norm env s, Envir.head_norm env t) of +fun unif thy binders (env,(s,t)) = case (Envir.head_norm env s, Envir.head_norm env t) of (Abs(ns,Ts,ts),Abs(nt,Tt,tt)) => let val name = if ns = "" then nt else ns - in unif sg ((name,Ts)::binders) (env,(ts,tt)) end - | (Abs(ns,Ts,ts),t) => unif sg ((ns,Ts)::binders) (env,(ts,(incr t)$Bound(0))) - | (t,Abs(nt,Tt,tt)) => unif sg ((nt,Tt)::binders) (env,((incr t)$Bound(0),tt)) - | p => cases sg (binders,env,p) + in unif thy ((name,Ts)::binders) (env,(ts,tt)) end + | (Abs(ns,Ts,ts),t) => unif thy ((ns,Ts)::binders) (env,(ts,(incr t)$Bound(0))) + | (t,Abs(nt,Tt,tt)) => unif thy ((nt,Tt)::binders) (env,((incr t)$Bound(0),tt)) + | p => cases thy (binders,env,p) -and cases sg (binders,env,(s,t)) = case (strip_comb s,strip_comb t) of +and cases thy (binders,env,(s,t)) = case (strip_comb s,strip_comb t) of ((Var(F,Fty),ss),(Var(G,Gty),ts)) => if F = G then flexflex1(env,binders,F,Fty,ints_of' env ss,ints_of' env ts) else flexflex2(env,binders,F,Fty,ints_of' env ss,G,Gty,ints_of' env ts) - | ((Var(F,Fty),ss),_) => flexrigid sg (env,binders,F,Fty,ints_of' env ss,t) - | (_,(Var(F,Fty),ts)) => flexrigid sg (env,binders,F,Fty,ints_of' env ts,s) - | ((Const c,ss),(Const d,ts)) => rigidrigid sg (env,binders,c,d,ss,ts) - | ((Free(f),ss),(Free(g),ts)) => rigidrigid sg (env,binders,f,g,ss,ts) - | ((Bound(i),ss),(Bound(j),ts)) => rigidrigidB sg (env,binders,i,j,ss,ts) + | ((Var(F,Fty),ss),_) => flexrigid thy (env,binders,F,Fty,ints_of' env ss,t) + | (_,(Var(F,Fty),ts)) => flexrigid thy (env,binders,F,Fty,ints_of' env ts,s) + | ((Const c,ss),(Const d,ts)) => rigidrigid thy (env,binders,c,d,ss,ts) + | ((Free(f),ss),(Free(g),ts)) => rigidrigid thy (env,binders,f,g,ss,ts) + | ((Bound(i),ss),(Bound(j),ts)) => rigidrigidB thy (env,binders,i,j,ss,ts) | ((Abs(_),_),_) => raise Pattern | (_,(Abs(_),_)) => raise Pattern | ((Const(c,_),_),(Free(f,_),_)) => (clash c f; raise Unif) @@ -258,21 +255,21 @@ | ((Bound i,_),(Free(f,_),_)) => (clashB binders i f; raise Unif) -and rigidrigid sg (env,binders,(a,Ta),(b,Tb),ss,ts) = +and rigidrigid thy (env,binders,(a,Ta),(b,Tb),ss,ts) = if a<>b then (clash a b; raise Unif) - else Library.foldl (unif sg binders) (unify_types sg (Ta,Tb,env), ss~~ts) + else Library.foldl (unif thy binders) (unify_types thy (Ta,Tb,env), ss~~ts) -and rigidrigidB sg (env,binders,i,j,ss,ts) = +and rigidrigidB thy (env,binders,i,j,ss,ts) = if i <> j then (clashBB binders i j; raise Unif) - else Library.foldl (unif sg binders) (env ,ss~~ts) + else Library.foldl (unif thy binders) (env ,ss~~ts) -and flexrigid sg (params as (env,binders,F,Fty,is,t)) = - if occurs(F,t,env) then (ocheck_fail sg (F,t,binders,env); raise Unif) +and flexrigid thy (params as (env,binders,F,Fty,is,t)) = + if occurs(F,t,env) then (ocheck_fail thy (F,t,binders,env); raise Unif) else (let val (u,env') = proj(t,env,binders,is) in Envir.update (((F, Fty), mkabs (binders, is, u)), env') end - handle Unif => (proj_fail sg params; raise Unif)); + handle Unif => (proj_fail thy params; raise Unif)); -fun unify(sg,env,tus) = Library.foldl (unif sg []) (env,tus); +fun unify(thy,env,tus) = Library.foldl (unif thy []) (env,tus); (*Eta-contract a term (fully)*) @@ -343,38 +340,38 @@ exception MATCH; -fun typ_match tsig (tyenv, TU) = Type.typ_match tsig TU tyenv +fun typ_match thy (tyenv, TU) = Sign.typ_match thy TU tyenv handle Type.TYPE_MATCH => raise MATCH; (*First-order matching; - fomatch tsig (pattern, object) returns a (tyvar,typ)list and (var,term)list. + fomatch thy (pattern, object) returns a (tyvar,typ)list and (var,term)list. The pattern and object may have variables in common. Instantiation does not affect the object, so matching ?a with ?a+1 works. Object is eta-contracted on the fly (by eta-expanding the pattern). Precondition: the pattern is already eta-contracted! Note: types are matched on the fly *) -fun fomatch tsig = +fun fomatch thy = let fun mtch (instsp as (tyinsts,insts)) = fn (Var(ixn,T), t) => if loose_bvar(t,0) then raise MATCH else (case Envir.lookup' (insts, (ixn, T)) of - NONE => (typ_match tsig (tyinsts, (T, fastype_of t)), + NONE => (typ_match thy (tyinsts, (T, fastype_of t)), Vartab.update_new ((ixn, (T, t)), insts)) | SOME u => if t aeconv u then instsp else raise MATCH) | (Free (a,T), Free (b,U)) => - if a=b then (typ_match tsig (tyinsts,(T,U)), insts) else raise MATCH + if a=b then (typ_match thy (tyinsts,(T,U)), insts) else raise MATCH | (Const (a,T), Const (b,U)) => - if a=b then (typ_match tsig (tyinsts,(T,U)), insts) else raise MATCH + if a=b then (typ_match thy (tyinsts,(T,U)), insts) else raise MATCH | (Bound i, Bound j) => if i=j then instsp else raise MATCH | (Abs(_,T,t), Abs(_,U,u)) => - mtch (typ_match tsig (tyinsts,(T,U)),insts) (t,u) + mtch (typ_match thy (tyinsts,(T,U)),insts) (t,u) | (f$t, g$u) => mtch (mtch instsp (f,g)) (t, u) | (t, Abs(_,U,u)) => mtch instsp ((incr t)$(Bound 0), u) | _ => raise MATCH in mtch end; -fun first_order_match tsig = fomatch tsig (Vartab.empty, Vartab.empty); +fun first_order_match thy = fomatch thy (Vartab.empty, Vartab.empty); (* Matching of higher-order patterns *) @@ -389,7 +386,7 @@ else raise MATCH end; -fun match tsg (po as (pat,obj)) = +fun match thy (po as (pat,obj)) = let (* Pre: pat and obj have same type *) fun mtch binders (env as (iTs,itms),(pat,obj)) = @@ -410,7 +407,7 @@ Library.foldl (mtch binders) ((iTs,itms), pargs~~oargs) fun rigrig2((a:string,Ta),(b,Tb),oargs) = if a <> b then raise MATCH - else rigrig1(typ_match tsg (iTs,(Ta,Tb)), oargs) + else rigrig1(typ_match thy (iTs,(Ta,Tb)), oargs) in case ph of Var(ixn,T) => let val is = ints_of pargs @@ -434,19 +431,19 @@ val pT = fastype_of pat and oT = fastype_of obj - val iTs = typ_match tsg (Vartab.empty, (pT,oT)) + val iTs = typ_match thy (Vartab.empty, (pT,oT)) val insts2 = (iTs, Vartab.empty) in mtch [] (insts2, po) - handle Pattern => fomatch tsg insts2 po + handle Pattern => fomatch thy insts2 po end; (*Predicate: does the pattern match the object?*) -fun matches tsig po = (match tsig po; true) handle MATCH => false; +fun matches thy po = (match thy po; true) handle MATCH => false; (* Does pat match a subterm of obj? *) -fun matches_subterm tsig (pat,obj) = - let fun msub(bounds,obj) = matches tsig (pat,obj) orelse +fun matches_subterm thy (pat,obj) = + let fun msub(bounds,obj) = matches thy (pat,obj) orelse case obj of Abs(x,T,t) => let val y = variant bounds x val f = Free(":" ^ y,T) @@ -471,7 +468,7 @@ (* rewriting -- simple but fast *) -fun rewrite_term tsig rules procs tm = +fun rewrite_term thy rules procs tm = let val skel0 = Bound 0; @@ -483,7 +480,7 @@ fun match_rew tm (tm1, tm2) = let val rtm = if_none (Term.rename_abs tm1 tm tm2) tm2 in - SOME (Envir.subst_vars (match tsig (tm1, tm)) rtm, rtm) + SOME (Envir.subst_vars (match thy (tm1, tm)) rtm, rtm) handle MATCH => NONE end;
--- a/src/Pure/proofterm.ML Wed Aug 31 15:46:39 2005 +0200 +++ b/src/Pure/proofterm.ML Wed Aug 31 15:46:40 2005 +0200 @@ -106,7 +106,7 @@ val add_prf_rrules : (proof * proof) list -> theory -> theory val add_prf_rprocs : (string * (Term.typ list -> proof -> proof option)) list -> theory -> theory - val rewrite_proof : Type.tsig -> (proof * proof) list * + val rewrite_proof : theory -> (proof * proof) list * (string * (typ list -> proof -> proof option)) list -> proof -> proof val rewrite_proof_notypes : (proof * proof) list * (string * (typ list -> proof -> proof option)) list -> proof -> proof @@ -1107,8 +1107,8 @@ in getOpt (rew1 [] skel0 prf, prf) end; -fun rewrite_proof tsig = rewrite_prf (fn (tyenv, f) => - Type.typ_match tsig (f ()) tyenv handle Type.TYPE_MATCH => raise PMatch); +fun rewrite_proof thy = rewrite_prf (fn (tyenv, f) => + Sign.typ_match thy (f ()) tyenv handle Type.TYPE_MATCH => raise PMatch); fun rewrite_proof_notypes rews = rewrite_prf fst rews;
--- a/src/Pure/tactic.ML Wed Aug 31 15:46:39 2005 +0200 +++ b/src/Pure/tactic.ML Wed Aug 31 15:46:40 2005 +0200 @@ -693,7 +693,7 @@ val raw_result = goal' RS Drule.rev_triv_goal; val prop' = prop_of raw_result; - val _ = conditional (not (Pattern.matches (Sign.tsig_of thy) (prop, prop'))) (fn () => + val _ = conditional (not (Pattern.matches thy (prop, prop'))) (fn () => err ("Proved a different theorem: " ^ Sign.string_of_term thy prop')); in Drule.conj_elim_precise (length props) raw_result
--- a/src/Pure/thm.ML Wed Aug 31 15:46:39 2005 +0200 +++ b/src/Pure/thm.ML Wed Aug 31 15:46:40 2005 +0200 @@ -290,7 +290,7 @@ ct2 as Cterm {t = t2, maxidx = maxidx2, sorts = sorts2, ...}) = let val thy_ref = merge_thys0 ct1 ct2; - val (Tinsts, tinsts) = match (Sign.tsig_of (Theory.deref thy_ref)) (t1, t2); + val (Tinsts, tinsts) = match (Theory.deref thy_ref) (t1, t2); val maxidx = Int.max (maxidx1, maxidx2); val sorts = Sorts.union sorts1 sorts2; fun mk_cTinst (ixn, (S, T)) = @@ -988,7 +988,7 @@ val sorts' = Sorts.union sorts_U sorts; in (case T of TVar (v as (_, S)) => - if Type.of_sort (Sign.tsig_of thy') (U, S) then ((v, U), (thy_ref', sorts')) + if Sign.of_sort thy' (U, S) then ((v, U), (thy_ref', sorts')) else raise TYPE ("Type not of sort " ^ Sign.string_of_sort thy' S, [U], []) | _ => raise TYPE (Pretty.string_of (Pretty.block [Pretty.str "instantiate: not a type variable",