Pattern matching help

Stream: new members

[Dominic Steinitz]

This may be the equivalent of real programmers can write fortran in any language but I get

invalid pattern, constructor or constant marked with '[match_pattern]' expected

def HHaskell {α : Type} [LinearOrderedField α] (n : ℕ) (k : ℕ) (_ : 2 * k - 1 ≤ 2^n - 1) (s : α) : ℤ :=
  let k' := 2 * k + 1
  match true with
  | (k' - 1) * 2^(-n : ℤ) < s ∧ s <= k'       * 2^(-n : ℤ) =>  2^((n - 1) / 2)
  | k'       * 2^(-n : ℤ) < s ∧ s <= (k' + 1) * 2^(-n : ℤ) => -2^((n - 1) / 2)
  | _                                                      => 0

[Henrik Böving]

That's just not a pattern you can match on

[Dominic Steinitz]

I can write this but pattern matching would be clearer

def HHaskell {α : Type} [LinearOrderedField α] (n : ℕ) (k : ℕ) (_ : 2 * k - 1 ≤ 2^n -1) (s : α) : ℤ :=
  let k':= 2 * k + 1
  if (k' - 1) * 2^(-n : ℤ) < s ∧ s <= k' * 2^(-n : ℤ)
  then 2^((n - 1) / 2)
  else if k' * 2^(-n : ℤ) < s && s <= (k' + 1) * 2^(-n : ℤ)
       then -2^((n - 1) / 2)
       else 0

Here's the Haskell for reference

> haar :: forall n k .
>         (KnownNat n, KnownNat k, (2 * k - 1 <=? 2^n - 1) ~ 'True) =>
>         Haar n (2 * k - 1)
> haar = Haar g where
>   g t | (k' - 1) * 2 ** (-n') < t && t <= k'       * 2 ** (-n') =  2 ** ((n' - 1) / 2)
>       | k'       * 2 ** (-n') < t && t <= (k' + 1) * 2 ** (-n') = -2 ** ((n' - 1) / 2)
>       | otherwise                                               =  0
>     where
>         n' = fromIntegral (natVal (Proxy :: Proxy n))
>         k' = 2 * (fromIntegral (natVal (Proxy :: Proxy k))) - 1

[Henrik Böving]

Yes, Lean doesn't do pattern guards

[Paige Thomas]

Henrik Böving said:

Yes, Lean doesn't do pattern guards

Is there a canonical way to emulate pattern guards, where if a guard evaluates to false, then the next pattern is tried?

[Kyle Miller]

No, no pattern guards unfortunately. The next best thing is to add extra discriminants that evaluate to true or false with your conditions, but that's usually pretty awkward.

[Paige Thomas]

By extra discriminants, do you mean extra patterns, or something else?

[Paige Thomas]

I can add an if, then, else after the pattern, but I'm not sure how to make it go to the next pattern based on the if, then, else.

[Kyle Miller]

I mean match val, cond1, cond2, cond3 where, where cond1, cond2, and cond3 are somehow able to be evaluated from val before pattern matching, and then you use true/false in the patterns for these three discriminants.

[Kyle Miller]

It's awkward and not always applicable.

[Kyle Miller]

Issue lean4#1894 tracks having more complicated if conditions that can bind patterns and have guards.

[Paige Thomas]

I see. Yeah, I was thinking of the case where the conditional in the guard uses part of the matched pattern, like isval here: https://www.cis.upenn.edu/~bcpierce/tapl/checkers/untyped/core.ml

[Paige Thomas]

I can get around it in my simpler translation for now though.

[Kyle Miller]

An annoying way to address it is to make a separate function that does the match and evaluates the guard, and then you put that in as an extra discriminant...

[Kyle Miller]

Imagine having Tm.appV1? and Tm.AppV2? functions, and then you use Option.map to apply the guard's function

[Paige Thomas]

Does the RFC you linked cover this case? I don't entirely follow the discussion there.

[Kyle Miller]

No, the RFC would let you write that ML like (modulo some notation questions)

def eval1 ctx t :=
  if (let TmApp fi (TmAbs _ x t12) v2 := t) && isval ctx v2 then
      termSubstTop v2 t12
  else if (let TmApp fi v1 t2 := t) && isval ctx v1 then
      let t2' := eval1 ctx t2 in
      TmApp fi v1 t2'
  else let TmApp fi t1 t2 := t then
      let t1' = eval1 ctx t1 in
      TmApp fi t1' t2
  else
      throw NoRuleApplies

[Paige Thomas]

I see.

[Paige Thomas]

Is it a feasible feature request to add pattern guards?