Stream: Beginner Questions

Topic: Unexpected behaviour of Pattern.matches

Lukas Stevens (Jan 12 2021 at 15:47):

I am using Pattern.matches like so

val binop_pat = Proof_Context.read_term_pattern ctxt "?x ?y ?z"

fun f args =
  ...
  else if Pattern.matches thy (binop_pat, t) then (case t of (t1 $ t2 $ t3) => ...)
  ...

Somehow the match succeeds but the t does not have the form t1 $ t2 $ t3. How can that be?

Mathias Fleury (Jan 12 2021 at 15:50):

Wild guess without running Isabelle: (t1 $ t2 ) $ t3?

Mathias Fleury (Jan 12 2021 at 15:58):

ML ‹
val ctxt = @{context}
val binop_pat = Proof_Context.read_term_pattern ctxt "?x ?y ?z";
val thy = @{theory};
val t = @{term ‹ab›};
val _= if Pattern.matches thy (binop_pat, t) then
   (case t of t1 $ t2 $ t3 =>
      @{print} ("yes", t1)
  | _ => @{print} ("no case", t))
else @{print} ("not matching", t)
›

prints "not matching" as expected. What kind of t do you have?

Lukas Stevens (Jan 12 2021 at 15:59):

I was hoping that there may be a glaring oversight by me which can be easily explained :D. I will investigate what the term is now.

Mathias Fleury (Jan 12 2021 at 16:01):

(@{print} t; raise Fail "")

is very useful for such cases

Simon Roßkopf (Jan 12 2021 at 16:15):

@{term "λx. f y z x"} should match your pattern

Lukas Stevens (Jan 12 2021 at 16:23):

This means that I should eta-contract t before destructuring it, I guess?

Lukas Stevens (Jan 12 2021 at 16:49):

Thanks, that seems to work.

Last updated: Dec 21 2024 at 16:20 UTC