Idris中的编译时间长且CPU使用率高

Question

我在Idris中玩一些形式化的游戏，并且有一些奇怪的行为：函数的编译时间和CPU使用率很高。

该代码是一个正则表达式模式匹配算法。首先是正则表达式定义：

data RegExp : Type where
  Zero : RegExp
  Eps  : RegExp
  Chr  : Char -> RegExp
  Cat  : RegExp -> RegExp -> RegExp
  Alt  : RegExp -> RegExp -> RegExp
  Star : RegExp -> RegExp
  Comp : RegExp -> RegExp

正则表达式的成员资格和非成员资格定义为以下相互递归的数据类型：

mutual      
  data NotInRegExp : List Char -> RegExp -> Type where
    NotInZero : NotInRegExp xs Zero
    NotInEps  : Not (xs = []) -> NotInRegExp xs Eps
    NotInChr  : Not (xs = [ c ]) -> NotInRegExp xs (Chr c)
    NotInCat  : zs = xs ++ ys -> (Either (NotInRegExp xs l) 
                                         ((InRegExp xs l)
                                         ,(NotInRegExp ys r)))
                              -> NotInRegExp zs (Cat l r)
    NotInAlt  : NotInRegExp xs l -> NotInRegExp xs r -> NotInRegExp xs (Alt l r)   
    NotInStar : NotInRegExp xs Eps ->
                NotInRegExp xs (Cat e (Star e)) ->
                NotInRegExp xs (Star e)
    NotInComp : InRegExp xs e -> NotInRegExp xs (Comp e)                

  data InRegExp : List Char -> RegExp -> Type where
    InEps : InRegExp [] Eps
    InChr : InRegExp [ a ] (Chr a)
    InCat : InRegExp xs l ->
            InRegExp ys r ->
            zs = xs ++ ys ->
            InRegExp zs (Cat l r)
    InAltL : InRegExp xs l ->
             InRegExp xs (Alt l r)
    InAltR : InRegExp xs r ->
             InRegExp xs (Alt l r)
    InStar : InRegExp xs (Alt Eps (Cat e (Star e))) ->
             InRegExp xs (Star e)
    InComp : NotInRegExp xs e -> InRegExp xs (Comp e)

在这些相当长的定义之后，我为替代方法定义了一个智能构造函数：

 infixl 4 .|.

 (.|.) : RegExp -> RegExp -> RegExp
 Zero .|. e = e
 e .|. Zero = e
 e .|. e'   = Alt e e'

现在，我想证明该智能构造函数在正则表达式成员语义方面是健全且完整的。证明几乎是直接的归纳/案例分析。但是，这些证明之一需要大量的时间和CPU才能进行编译（在Mac OS X El Capitan中大约占CPU的90％）。

令人讨厌的功能是：

 altOptNotInComplete : NotInRegExp xs (Alt l r) -> NotInRegExp xs (l .|. r)
 altOptNotInComplete {l = Zero} (NotInAlt x y) = y
 altOptNotInComplete {l = Eps}{r = Zero} (NotInAlt x y) = x
 altOptNotInComplete {l = Eps}{r = Eps} pr = pr
 altOptNotInComplete {l = Eps}{r = (Chr x)} pr = pr
 altOptNotInComplete {l = Eps}{r = (Cat x y)} pr = pr
 altOptNotInComplete {l = Eps}{r = (Alt x y)} pr = pr
 altOptNotInComplete {l = Eps}{r = (Star x)} pr = pr
 altOptNotInComplete {l = Eps}{r = (Comp x)} pr = pr
 altOptNotInComplete {l = (Chr x)}{r = Zero} (NotInAlt y z) = y
 altOptNotInComplete {l = (Chr x)}{r = Eps} pr = pr
 altOptNotInComplete {l = (Chr x)}{r = (Chr y)} pr = pr
 altOptNotInComplete {l = (Chr x)}{r = (Cat y z)} pr = pr
 altOptNotInComplete {l = (Chr x)}{r = (Alt y z)} pr = pr
 altOptNotInComplete {l = (Chr x)}{r = (Star y)} pr = pr
 altOptNotInComplete {l = (Chr x)}{r = (Comp y)} pr = pr
 altOptNotInComplete {l = (Cat x y)}{r = Zero} (NotInAlt z w) = z
 altOptNotInComplete {l = (Cat x y)}{r = Eps} pr = pr
 altOptNotInComplete {l = (Cat x y)}{r = (Chr z)} pr = pr
 altOptNotInComplete {l = (Cat x y)}{r = (Cat z w)} pr = pr
 altOptNotInComplete {l = (Cat x y)}{r = (Alt z w)} pr = pr
 altOptNotInComplete {l = (Cat x y)}{r = (Star z)} pr = pr
 altOptNotInComplete {l = (Cat x y)}{r = (Comp z)} pr = pr
 altOptNotInComplete {l = (Alt x y)}{r = Zero} (NotInAlt z w) = z
 altOptNotInComplete {l = (Alt x y)}{r = Eps} pr = pr
 altOptNotInComplete {l = (Alt x y)}{r = (Chr z)} pr = pr
 altOptNotInComplete {l = (Alt x y)}{r = (Cat z w)} pr = pr
 altOptNotInComplete {l = (Alt x y)}{r = (Alt z w)} pr = pr
 altOptNotInComplete {l = (Alt x y)}{r = (Star z)} pr = pr
 altOptNotInComplete {l = (Alt x y)}{r = (Comp z)} pr = pr
 altOptNotInComplete {l = (Star x)}{r = Zero} (NotInAlt y z) = y
 altOptNotInComplete {l = (Star x)}{r = Eps} pr = pr
 altOptNotInComplete {l = (Star x)}{r = (Chr y)} pr = pr
 altOptNotInComplete {l = (Star x)}{r = (Cat y z)} pr = pr
 altOptNotInComplete {l = (Star x)}{r = (Alt y z)} pr = pr
 altOptNotInComplete {l = (Star x)}{r = (Star y)} pr = pr
 altOptNotInComplete {l = (Star x)}{r = (Comp y)} pr = pr
 altOptNotInComplete {l = (Comp x)}{r = Zero} (NotInAlt y z) = y
 altOptNotInComplete {l = (Comp x)}{r = Eps} pr = pr
 altOptNotInComplete {l = (Comp x)}{r = (Chr y)} pr = pr
 altOptNotInComplete {l = (Comp x)}{r = (Cat y z)} pr = pr
 altOptNotInComplete {l = (Comp x)}{r = (Alt y z)} pr = pr
 altOptNotInComplete {l = (Comp x)}{r = (Star y)} pr = pr
 altOptNotInComplete {l = (Comp x)}{r = (Comp y)} pr = pr

我不明白为什么这个功能需要这么多的CPU。有没有一种方法可以“优化”此代码以使编译正常进行？

前面的代码可在下面的摘要中找到。我在Mac OS X El Capitan上使用Idris 0.10。

任何线索都非常欢迎。