Stream: Equations devs & users

Topic: Can where definitions make recursive calls in a with node?


view this post on Zulip Kevin Orr (Sep 29 2020 at 21:00):

Hello, I'm trying to write a where clause that makes a recursive call to itself in a with node. Here's a simplified version:

Require Import List.
Import ListNotations.
Require Import Equations.Equations.

Fail Equations ok_clause (e : nat -> option bool) (xs : list nat) : bool by struct xs :=
  ok_clause => ok_clause'
    where
      ok_clause' (e : nat -> option bool) (xs : list nat) : bool by struct xs :=
      ok_clause' _ [] => true;
      ok_clause' e (x::xs) with e x =>
      { | Some _ => ok_clause' e xs;
        | _ => false }.

This fails with the message

Error:
Recursive definition of ok_clause' is ill-formed.
In environment
ok_clause : let H := fixproto in (nat -> option bool) -> list nat -> bool
ok_clause' : (nat -> option bool) -> list nat -> bool
e : nat -> option bool
xs : list nat
n : nat
l : list nat
Recursive call to ok_clause' has not enough arguments.
Recursive definition is:
"fun (e : nat -> option bool) (xs : list nat) =>
 match xs with
 | [] => true
 | n :: l =>
     (fun (_ : let H := fixproto in (nat -> option bool) -> list nat -> bool) (e0 : nat -> option bool)
        (_ : nat) (refine : option bool) (ok_clause' : (nat -> option bool) -> list nat -> bool)
        (l0 : list nat) =>
      match refine with
      | Some _ => fun (ok_clause'0 : (nat -> option bool) -> list nat -> bool) (l1 : list nat) => ok_clause'0 e0 l1
      | None => fun (_ : (nat -> option bool) -> list nat -> bool) (_ : list nat) => false
      end ok_clause' l0) ok_clause e n (e n) ok_clause' l
 end".

As the error indicates, ok_clause' is being passed as an argument to the lambda, and then this argument is being called as the recursive call. I suppose the fixpoint checker doesn't allow (fun f0 => match ... => f0 x end) f (typo: (match ... => fun f0 => (f0 x) end) f), where f is the fixpoint.

Interestingly enough, ok_clause' works as a top-level definition:

Require Import List.
Import ListNotations.
Require Import Equations.Equations.

Equations ok_clause' (e : nat -> option bool) (xs : list nat) : bool by struct xs :=
  ok_clause' _ [] => true;
  ok_clause' e (x::xs) with e x =>
  { | Some _ => ok_clause' e xs;
    | _ => false }.

So is there some weird interaction happening between where, with, and a recursive call? Or is this just something that's not supported?

Thanks.

P.S. this is easy to work around by just using an explicit match instead of a with clause, or by extracting out the subprogram into its own definition.

view this post on Zulip Matthieu Sozeau (Sep 30 2020 at 08:06):

Sadly yes, this is not supported by the core calculus: it requires all recursive calls be full applications, and cannot handle this commutation of match and lambda. We might be able to do better here though: there is no reason to abstract on the recursive function ok_clause' in the match branches, as its type is independent of the the scrutinee of the pattern-matching. So could you please report this as an issue of Equations github page?

view this post on Zulip Kevin Orr (Oct 01 2020 at 22:12):

Sure thing


Last updated: Jan 29 2023 at 15:02 UTC