sellout

-- error: expected: "{",
--    function declaration
--  | M = MD5 (zipWith (+) [A, B, C, D] (loop 64 [A, B, C, D])) 


updateMD5Context : MessageDigest5 -> Bits 512 -> MessageDigest5
updateMD5Context (MD5 [A, B, C, D]) chunk with (the (Vect 16 (Bits 32)) (partition chunk))
  | M = MD5 (zipWith (+) [A, B, C, D] (loop 64 [A, B, C, D]))
  where loop : Fin 65 -> Vect 4 (Bits 32) -> Vect 4 (Bits 32)
        loop fZ     context      = context

sellout

-- Prelude.Fin (S n) instance of Prelude.Enum, method enumFromThen is possibly not total due to recursive path Prelude.Fin (S n) instance of Prelude.Enum, method enumFromThen --> Prelude.Fin (S n) instance of Prelude.Enum, method enumFromThen
-- Prelude.idr:370:3:Prelude.Fin (S n) instance of Prelude.Enum, method enumFromTo is possibly not total due to: Prelude.Fin (S n) instance of Prelude.Enum, method enumFromThen
-- Prelude.idr:372:3:Prelude.Fin (S n) instance of Prelude.Enum, method enumFromThenTo is possibly not total due to: Prelude.Fin (S n) instance of Prelude.Enum, method enumFromThen

-- predifine Nat versions of Enum, so we can use them in the default impls
total natEnumFromThen : Nat -> Nat -> Stream Nat
natEnumFromThen n inc = n :: natEnumFromThen (plus inc n) inc
total natEnumFromThenTo : Nat -> Nat -> Nat -> List Nat
natEnumFromThenTo _ Z   _ = []
natEnumFromThenTo n inc m = map (plus n . (* inc)) (natRange (S ((m - n) `div` inc)))

sellout

-- Data.Bifunctor.Either instance of Data.Bifunctor.Bifunctor, method first is possibly not total due to recursive path Data.Bifunctor.Either instance of Data.Bifunctor.Bifunctor, method first
-- Data.Bifunctor.Either instance of Data.Bifunctor.Bifunctor, method second is possibly not total due to: Data.Bifunctor.Either instance of Data.Bifunctor.Bifunctor, method first

class Bifunctor (p : Type -> Type -> Type) where
  bimap : (a -> b) -> (c -> d) -> p a c -> p b d
  -- bimap f g = first f . second g
  first : (a -> b) -> p a c -> p b c
  -- first f = bimap f id
  second : (c -> d) -> p a c -> p a d
  -- second g = bimap id g

sellout

--     When elaborating constructor constructor of Main.Foo:
--     When elaborating an application of type constructor Prelude.Vect.Vect:
--             Can't convert
--                     a b6
--             with
--                     Type
--             
--             
--             In context:
--                     a : (__pi_arg : Type) -> Type

sellout

syntax "bitOp" {name} [prim8] [prim16] [prim32] [prim64] =
name {n=Z}           = prim8
name {n=S Z}         = prim16
name {n=S (S Z)}     = prim32
name {n=S (S (S _))} = prim64
;

gte : machineTy n -> machineTy n -> Int
bitOp gte prim__gteB8 prim__gteB16 prim__gteB32 prim__gteB64

sellout

     Can't unify
             Buffer (bytesUsed (S n) + (fromInteger 1 * fromInteger 8))
     with
             Buffer (plus (plus (plus (plus (power 2 n) (plus (power 2 n) 0)) (plus (plus (power 2 n) (plus (power 2 n) 0)) 0)) (plus (plus (plus (power 2 n) (plus (power 2 n) 0)) (plus (plus (power 2 n) (plus (power 2 n) 0)) 0)) 0)) (plus (plus (plus (plus (power 2 n) (plus (power 2 n) 0)) (plus (plus (power 2 n) (plus (power 2 n) 0)) 0)) (plus (plus (plus (power 2 n) (plus (power 2 n) 0)) (plus (plus (power 2 n) (plus (power 2 n) 0)) 0)) 0)) 0))

sellout

-- using a local function with an additional decrementing parameter because Idris can’t tell that `x - (S n) < x`
tightmod : Nat -> (m : Nat) -> {default () ok : notZero m} -> Fin m
tightmod _ Z {ok=prf} = FalseElim prf
tightmod left (S modulus) = tightmod' left left modulus
  where
    tightmod' : Nat -> Nat -> (n : Nat) -> Fin (S n)
    tightmod' Z center right = fromMaybe fZ (natToFin center (S right))
    tightmod' (S left) center right =
      if lte center right
      then fromMaybe fZ (natToFin center (S right))

sellout

foldIntoBuff : (Buffer k -> elt -> Buffer (m+k)) -> Buffer k -> Vect n elt -> Buffer (n*m+k)
foldIntoBuff _ buff [] = buff
foldIntoBuff fn buff (i::is) = foldIntoBuff fn (fn buff i) is

--   When elaborating right hand side of foldIntoBuff:
--   When elaborating an application of Data.Bits.foldIntoBuff:
--           Can't unify
--                   Buffer (m + k)
--           with
--                   Buffer k

sellout

instance Integral (Fin (S n)) where
  div _ fZ = last
  div left (fS right) = div' left left (fS right)
    where
      div' : Fin (S n) -> Fin (S n) -> Fin (S n) -> Fin (S n)
      div' fZ       center right = fZ
      div' (fS left) center right =
        if center <= right
        then fZ
        else case strengthen (fS (div' (weaken left) (center - right) right)) of

sellout

Debugger entered--Lisp error: (wrong-type-argument stringp nil)
  directory-files(nil t "ipkg$")
  #[257 "\302
!\303
\304\300\305P#\211\203\211\202(
\203
\306!\232\203\"\307\202(\301\242\306!!\207" ["ipkg" (#0) file-name-directory directory-files t "$" directory-file-name nil] 7 "\n\n(fn PATH)"]("~")
  #[257 "\302
!\303
\304\300\305P#\211\203\211\202(
\203
\306!\232\203\"\307\202(\301\242\306!!\207" ["ipkg" (#0) file-name-directory directory-files t "$" directory-file-name nil] 7 "\n\n(fn PATH)"]("~/Documents")
  #[257 "\302
!\303
\304\300\305P#\211\203\211\202(
\203
\306!\232\203\"\307\202(\301\242\306!!\207" ["ipkg" (#0) file-name-directory directory-files t "$" directory-file-name nil] 7 "\n\n(fn PATH)"]("~/Documents/Clozure")
  #[257 "\302
!\303
\304\300\305P#\211\203\211\202(
\203
\306!\232\203\"\307\202(\301\242\306!!\207" ["ipkg" (#0) file-name-directory directory-files t "$" directory-file-name nil] 7 "\n\n(fn PATH)"]("~/Documents/Clozure/ccl-clean")
  #[257 "\302
!