Проверка типа процедуры принятия решения Idris чрезвычайно медленная, это проблема производительности? - PullRequest
Новая
       61

Проверка типа процедуры принятия решения Idris чрезвычайно медленная, это проблема производительности?

0 голосов
/ 05 марта 2019 
decLte : (n : Nat) -> (m : Nat) -> Dec (LTE n m)
decLte Z _ = Yes LTEZero
decLte (S _) Z = No (\x => case x of LTEZero impossible ; LTESucc _ impossible)
decLte (S n) (S m) with (decLte n m)
  | Yes ltePrf = Yes (LTESucc ltePrf)
  | No lteContra = No (\(LTESucc p) => lteContra p)

data NatRange : Type where
   In : (l: Nat) -> (u: Nat) -> {auto yep : decLte l u = Yes _} -> NatRange

natRangeEx1 : NatRange
natRangeEx1 = In 500 2100

Этот код занимает около 5 минут для проверки типа и использует> 2 ГБ памяти.Я ошеломлен крайне плохой работой.Может ли кто-нибудь дать мне вескую причину, например, в проблеме моего кода или в собственной проблеме Idris?

...