# HG changeset patch # User noschinl # Date 1429192555 -7200 # Node ID 0a064330a885b8681884b14460fa2e1a3749da1f # Parent bc57cb0c5001513be743cf6ca8a7a0b5bca9da60 rewrite: use distinct names for unnamed abstractions diff -r bc57cb0c5001 -r 0a064330a885 src/HOL/Library/rewrite.ML --- a/src/HOL/Library/rewrite.ML Wed Apr 15 22:27:31 2015 +0200 +++ b/src/HOL/Library/rewrite.ML Thu Apr 16 15:55:55 2015 +0200 @@ -69,7 +69,7 @@ (* A focusterm represents a subterm. It is a tuple (t, p), consisting of the subterm t itself and its subterm position p. *) -type focusterm = Type.tyenv * term * subterm_position +type focusterm = (Type.tyenv * Proof.context) * term * subterm_position val dummyN = Name.internal "__dummy" val holeN = Name.internal "_hole" @@ -96,7 +96,7 @@ (* focus terms *) -fun ft_abs ctxt (s,T) (tyenv, u, pos) = +fun ft_abs ctxt (s,T) ((tyenv, u_ctxt), u, pos) = case try (fastype_of #> dest_funT) u of NONE => raise TERM ("ft_abs: no function type", [u]) | SOME (U, _) => @@ -104,14 +104,18 @@ val tyenv' = if T = dummyT then tyenv else Sign.typ_match (Proof_Context.theory_of ctxt) (T, U) tyenv - val x = Free (the_default (Name.internal dummyN) s, Envir.norm_type tyenv' T) + val (s', u_ctxt') = + case s of + NONE => yield_singleton Variable.variant_fixes (Name.internal dummyN) u_ctxt + | SOME s => (s, u_ctxt) + val x = Free (s', Envir.norm_type tyenv' T) val eta_expand_cconv = CConv.rewr_cconv @{thm eta_expand} fun eta_expand rewr ctxt bounds = eta_expand_cconv then_conv rewr ctxt bounds val (u', pos') = case u of Abs (_,_,t') => (subst_bound (x, t'), pos o abs_rewr_cconv s) | _ => (u $ x, pos o eta_expand o abs_rewr_cconv s) - in (tyenv', u', pos') end + in ((tyenv', u_ctxt'), u', pos') end handle Pattern.MATCH => raise TYPE ("ft_abs: types don't match", [T,U], [u]) fun ft_fun _ (tyenv, l $ _, pos) = (tyenv, l, pos o fun_rewr_cconv) @@ -235,10 +239,10 @@ let val (_, ts) = strip_comb t in map fastype_of (snd (take_suffix is_Var ts)) end - fun do_match (tyenv, u, pos) = - case try (Pattern.match thy (t,u)) (tyenv, Vartab.empty) of + fun do_match ((tyenv, u_ctxt), u, pos) = + case try (Pattern.match thy (apply2 Logic.mk_term (t,u))) (tyenv, Vartab.empty) of NONE => NONE - | SOME (tyenv', _) => SOME (off (tyenv', u, pos)) + | SOME (tyenv', _) => SOME (off ((tyenv', u_ctxt), u, pos)) fun match_argT T u = let val (U, _) = dest_funT (fastype_of u) @@ -246,12 +250,12 @@ handle TYPE _ => K NONE fun desc [] ft = do_match ft - | desc (T :: Ts) (ft as (tyenv , u, pos)) = + | desc (T :: Ts) (ft as ((tyenv, u_ctxt) , u, pos)) = case do_match ft of NONE => (case match_argT T u tyenv of NONE => NONE - | SOME tyenv' => desc Ts (ft_abs ctxt (NONE, T) (tyenv', u, pos))) + | SOME tyenv' => desc Ts (ft_abs ctxt (NONE, T) ((tyenv', u_ctxt), u, pos))) | SOME ft => SOME ft in desc eta_expands ft end @@ -349,7 +353,7 @@ in map (map_term_pattern f) end val pattern' = interpret_term_patterns ctxt pattern - val matches = find_matches ctxt pattern' (Vartab.empty, Thm.term_of ct, I) + val matches = find_matches ctxt pattern' ((Vartab.empty, ctxt), Thm.term_of ct, I) val thms' = maps (prep_meta_eq ctxt) thms @@ -361,7 +365,7 @@ NONE => th | SOME (th', _) => th' - fun conv ((tyenv, _, position) : focusterm) = + fun conv (((tyenv, _), _, position) : focusterm) = distinct_prems o position (rewrite_conv (to, tyenv)) ctxt [] in Seq.map (fn ft => conv ft) matches end diff -r bc57cb0c5001 -r 0a064330a885 src/HOL/ex/Rewrite_Examples.thy --- a/src/HOL/ex/Rewrite_Examples.thy Wed Apr 15 22:27:31 2015 +0200 +++ b/src/HOL/ex/Rewrite_Examples.thy Thu Apr 16 15:55:55 2015 +0200 @@ -254,5 +254,22 @@ |> Seq.list_of \ +section \Regression tests\ + +ML \ + val ct = @{cterm "(\b :: int. (\a. b + a))"} + val (x, ctxt) = yield_singleton Variable.add_fixes "x" @{context} + val pat = [ + Rewrite.In, + Rewrite.Term (@{const plus(int)} $ Var (("c", 0), @{typ int}) $ Var (("c", 0), @{typ int}), []) + ] + val to = NONE + val ct_ths = Rewrite.rewrite ctxt (pat, to) @{thms add.commute} ct + val _ = case Seq.pull ct_ths of NONE => () + | _ => error "should not have matched anything" +\ + + + end