idris 糊状战术

Question

所以我正在阅读这篇关于详细反射的论文( https://eb.host.cs.st-andrews.ac.uk/drafts/elab-reflection.pdf )并决定我想尝试这个策略(在第 5.2 节中找到):

mush : Elab ()
mush =
   do attack
      x <- gensym "x"
      intro x
      try intros
      induction (Var x) `andThen` auto
      solve

据说这种策略可以证明加法的结合性:

plusAssoc : (j, k, l : Nat) -> plus (plus j k) l = plus j (plus k l)
plusAssoc = %runElab mush

但是，当尝试键入检查 mush 时，我收到以下错误:

错误:不是终止符，应为:“$”、“&&”、“)”、“”、“>”、“+”、“++”、“-”、“->”、“.”、“/", "/=", "::", ";", "<", "", "<", "<>", "<+>", "<<", "<=", "<|>", "=", "==", ">", ">=", ">>", ">>=", "\\", "`", "in", "|| ", "~=~", 左关联运算符的歧义使用, 非关联运算符的歧义使用, 右关联运算符的歧义使用, 输入结束, 匹配应用程序表达式, 其中块 x <- gensym "x"^

我不明白出了什么问题，是混合策略不正确还是我需要添加到我的文件中？

Answer 1

首先，您需要添加一些导入:

import Language.Reflection
import Pruviloj.Core
import Pruviloj.Induction

auto : Elab ()
auto =
  do compute
     attack
     try intros
     hs <- map fst <$> getEnv
     for_ hs $
       \ih => try (rewriteWith (Var ih))
     hypothesis <|> search
     solve

mush : Elab ()
mush =
   do attack
      x <- gensym "x"
      intro x
      try intros
      induction (Var x) `andThen` auto
      solve

plusAssoc : (j, k, l : Nat) -> plus (plus j k) l = plus j (plus k l)
plusAssoc = %runElab mush

然后你需要告诉 Idris 使用包 Pruviloj :

idris -p pruviloj <fileName.idr>

该类型检查并有效，但我无法重现您的错误消息。