Idris2:嵌套WITH子句

Question

我的密码

我的代码，即：

equal_suffix: Eq a => List a -> List a -> List a
equal_suffix u v with (snocList u)
    equal_suffix _ _ | Empty = []
    equal_suffix _ v | (Snoc x xs snx) with (snocList v)
        equal_suffix _ _ | (Snoc x xs snx) | Empty = []
        equal_suffix _ _ | (Snoc x xs snx) | (Snoc y ys sny) = case x == y of
            False => []
            True => (equal_suffix xs ys | snx | sny) ++ [x]

不键入check，并在编译时大喊大叫：

Error: With clause does not match parent

Hello:857:25--857:38
 853 | 
 854 | equal_suffix: Eq a => List a -> List a -> List a
 855 | equal_suffix u v with (snocList u)
 856 |     equal_suffix _ _ | Empty = []
 857 |     equal_suffix _ v | (Snoc x xs snx) with (snocList v)
                               ^^^^^^^^^^^^^

我的问题

我的第一个问题是：

with parent 对于Idris上下文中的子句意味着什么？ (Edit1:感谢@joel，我现在明白了)

如果第一个问题不能帮助我理解这一点：

我的代码有什么问题？ (Edit1:原始的最终问题)

在Idris(2)中使用嵌套的with 子句的正确语法是什么？ (Edit1:由于注释@Vega的提醒，这是一个更集中的问题)

(请原谅我用蛇来命名变量:D)

Edit1 (2022-05-09)：问题结束了，因为最初的最后一个问题不够集中.我希望通过调整我的问题来重新讨论这个问题，因为我仍然面临着with条款的麻烦。

我试过的

为了添加更多细节，我独立尝试了@joel版本，也就是说，在指定了所有with语句之后，只进行了大小写拆分：

func: input_type -> output_type
func input with (view1 input)
    func input | input_in_view1 with (view2 input)
        func input | input_in_view1 | input_in_view2 = ...

我还试着把这两种观点结合起来，即，

func: input_type -> output_type
func input with (view1 input, view2 input)
    func input | (input_in_view1, input_in_view2) = ...

但是，这两种方法似乎不起作用(第一种导致unsolved hole错误，而第二种非覆盖错误或非终止类型检查取决于我如何拆分)。

Edwin的TDD示例

这个equal_suffix练习来自Edwin的TDD。我还是被困住了，就在这个练习中停下来了。

以下是我所复制的书中的一个例子：

isSuffix : Eq a => List a -> List a -> Bool
isSuffix input1 input2 with (snocList input1)
    isSuffix [] input2 | Empty = True
    isSuffix (xs ++ [x]) input2 | (Snoc rec) with (snocList input2)
        isSuffix (xs ++ [x]) [] | (Snoc rec) | Empty = False
        isSuffix (xs ++ [x]) (ys ++ [y]) | (Snoc rec) | (Snoc z) 
            = if x == y then isSuffix xs ys | xsrec | ysrec
                else False

在这本书中，为了教育目的重新定义了snocList，而rec可能只是xsrec和ysrec的一个错误。

直接对with子句进行整体递归。

在将递归调用equal_suffix xs ys | snx | sny更改为equal_suffix xs ys时，我确实设法使其工作。

但是，根据“P275”一书，要创建一个完全定义的函数，我们需要直接对with子句进行递归，以告诉编译器递归调用之间的关系，因此我希望通过递归直接调用with子句来定义函数。

Answer 1

最简单的修正:删除最后一行中的| sny。显然不需要。

“父”大概是指递归循环中的父函数调用。

至于为什么它不使用| sny编译..。我猜想，您的第二个视图只存在于模式匹配的一个分支中，而如果要在sny中递归地传递equal_suffix xs ys | snx | sny，则需要在这两个分支中都存在该视图。

你也许能让这样的东西起作用

equal_suffix: Eq a => List a -> List a -> List a
equal_suffix u v with (snocList u)
  equal_suffix u v | su with (snocList v)
    equal_suffix [] _ | Empty | _ = []
    equal_suffix _ [] | _ | Empty = []
    equal_suffix (xs ++ [x]) (ys ++ [y]) | (Snoc x xs snx) | (Snoc y ys sny) =
      case x == y of
        False => []
        True => (equal_suffix xs ys | snx | sny) ++ [x]

但是这个特殊的例子无法用未解决的漏洞进行编译。