Can't do simple matches

[ghost]

assert foo fails here, and I get a parse error with bar. Is this right?

theory \Bugs extends \root

val foo =
  let 'f:𝒰 → 𝒰'
  let 'x:𝒰'
  match 'f x'
    case '(‹rat› ‹rand›):𝒰' => true
    case _                  => false

val bar =
  let 'x:𝒰'
  match 'x ↦ x'
    case '‹v› ↦ ‹bod›' => true
    case _             => false

assert foo

[phlegmaticprogrammer]

Yes, that is right. In both cases these are not higher order patterns. I'll be in in an hour.

[phlegmaticprogrammer]

So, the first should actually give an exception saying its not a hopattern. The second one will give a parse error. For the second one, if the matching would succeed, what would be the value of v??

[phlegmaticprogrammer]

I was wondering why in the first of the two examples the interpreter does not throw an exception saying that '‹rat› ‹rand›' is not a higher-order pattern. Actually, it is because it IS a higher-order pattern, the one describing set application :-) So, in the following, the assertion actually holds:

    context
      let 'f:𝒰'
      let 'x:𝒰'
      val foo = 
        match 'f x'
          case '‹rat› ‹rand›' => true
          case _ => false
      assert foo

Set application is assumed because '‹rat› ‹rand›' is not a higher-order pattern for higher-order application. Now, if you want to force higher-order application like this:

    context
      let 'f:𝒰 → 𝒰'
      let 'x:𝒰'
      val foo = 
        match 'f x'
          case '(‹rat› : _ → _) ‹rand›' => true
          case _ => false
      assert foo

then you will currently get an exception ill-typed pattern. I actually wasn't sure until this (admittedly obvious :-)) example if that exception can ever be thrown (see the last paragraph of Type Inference for Patterns).

I need to think about this for a little bit, because if we actually want to allow structural patterns, then surely type inference for patterns like '(‹rat› : → ) ‹rand›' should succeed.

[phlegmaticprogrammer]

So it turns out that getting an ill-typed pattern exception when type checking '(‹rat› : → ) ‹rand›' is actually a bug. I have fixed it now. This would open up again the possibility for structural pattern matching, but now I have doubts if that would be a good idea, as pattern matching is complicated enough already it seems.

[phlegmaticprogrammer]

So I just added a destcomb function now, see issue30.thy. Let's see first if that is enough before adding structural pattern matching.