Kevin Orr (Sep 29 2020 at 21:00): 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(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.
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?
Kevin Orr (Oct 01 2020 at 22:12):Sure thing
Last updated: May 28 2023 at 18:29 UTC