text:
module Erlang.Decode

import Erlang.Conversion
import Erlang.IO
import Erlang.Types

%default total

-- This module contains functions to turn an untyped Erlang value into a
-- typed Idris value.
-- The decoding functions are commonly used together with `erlCall` and
-- `erlUnsafeCall`.

||| The possible errors that can happen when decoding an Erlang value.
public export
data ErlDecoderError
  = Error String
  | OneOf ErlDecoderError ErlDecoderError
  | Empty

||| The decoder type.
export
data ErlDecoder a =
  MkDecoder (ErlTerm -> Either ErlDecoderError a)

namespace ErlDecoders
  ||| A list of decoders.
  public export
  data ErlDecoders : List Type -> Type where
    Nil : ErlDecoders []
    (::) : ErlDecoder a -> ErlDecoders as -> ErlDecoders (a :: as)

||| A type describing how to decode an entry in an Erlang map.
public export
data ErlMapEntryDecoder : key -> Type -> Type where
  MkDecoderMapEntry : (key : a) -> ErlDecoder value -> ErlMapEntryDecoder key value

||| Convenience operator for creating an `MkDecoderMapEntry`.
|||
||| `"name" := string` is equivalent to `MkDecoderMapEntry "name" string`
public export
(:=) : (key : a) -> ErlDecoder value -> ErlMapEntryDecoder key value
(:=) = MkDecoderMapEntry

namespace ErlMapDecoders
  ||| A list describing how to decode entries in an Erlang map.
  public export
  data ErlMapDecoders : List ErlMapEntry -> Type where
    Nil : ErlMapDecoders []
    (::) : ErlMapEntryDecoder key valueTy -> ErlMapDecoders xs -> ErlMapDecoders (MkMapEntry key valueTy :: xs)

-- IMPLEMENTATIONS FOR `ErlDecoder`

export
Functor ErlDecoder where
  map f (MkDecoder valueDecoder) =
    MkDecoder (\term => either Left (Right . f) (valueDecoder term))

export
Applicative ErlDecoder where
  pure value =
    MkDecoder (\_ => Right value)
  (MkDecoder fDecoder) <*> (MkDecoder valueDecoder) =
    MkDecoder (\term => do
      f <- fDecoder term
      value <- valueDecoder term
      pure (f value))

export
Monad ErlDecoder where
  (MkDecoder valueDecoder) >>= f =
    MkDecoder (\term => do
      value <- valueDecoder term
      let (MkDecoder nextDecoder) = f value
      nextDecoder term)

export
Alternative ErlDecoder where
  empty =
    MkDecoder (\_ => Left Empty)
  (MkDecoder decoder1) <|> (MkDecoder decoder2) =
    MkDecoder (\term => case decoder1 term of
      Right res => Right res
      Left firstErr => case decoder2 term of
        Right res => Right res
        Left secondErr => Left (OneOf firstErr secondErr))

-- DECODE ERLANG TERM

||| Try to decode the given value using the given decoder.
||| Returns an `ErlDecoderError` in the case of failure.
export
erlDecode : ErlType from => ErlDecoder a -> from -> Either ErlDecoderError a
erlDecode (MkDecoder decoder) term =
  decoder (cast term)

||| Try to decode the given value using the given decoder.
||| Returns `Nothing` in the case of failure.
export
erlDecodeMay : ErlType from => ErlDecoder a -> from -> Maybe a
erlDecodeMay decoder term =
  case erlDecode decoder term of
    Right res => Just res
    Left _ => Nothing

||| Try to decode the given value using the given decoder.
||| Returns a default value in the case of failure.
export
erlDecodeDef : ErlType from => Lazy a -> ErlDecoder a -> from -> a
erlDecodeDef def decoder term =
  case erlDecode decoder term of
    Right res => res
    Left _ => def

-- PRIMITIVES

%extern prim__erlMatchExact       : ErlTerm -> ErlTerm -> Int
%extern prim__erlDecodeCodepoint  : ErlTerm -> Maybe Char
%extern prim__erlDecodeInteger    : ErlTerm -> Maybe Integer
%extern prim__erlDecodeDouble     : ErlTerm -> Maybe Double
%extern prim__erlDecodeAtom       : ErlTerm -> Maybe ErlAtom
%extern prim__erlDecodeBinary     : ErlTerm -> Maybe String
%extern prim__erlDecodePid        : ErlTerm -> Maybe ErlPid
%extern prim__erldecodeReference  : ErlTerm -> Maybe ErlReference
%extern prim__erlDecodePort       : ErlTerm -> Maybe ErlPort
%extern prim__erlDecodeAnyMap     : ErlTerm -> Maybe ErlAnyMap
%extern prim__erlDecodeAnyList    : ErlTerm -> Maybe ErlTerm
%extern prim__erlDecodeNil        : ErlTerm -> Maybe ErlNil
%extern prim__erlDecodeCons       : ErlTerm -> Maybe (ErlCons ErlTerm ErlTerm)
%extern prim__erlDecodeTuple0     : ErlTerm -> Maybe ErlTuple0
%extern prim__erlDecodeTuple1     : ErlTerm -> Maybe (ErlTuple1 ErlTerm)
%extern prim__erlDecodeTuple2     : ErlTerm -> Maybe (ErlTuple2 ErlTerm ErlTerm)
%extern prim__erlDecodeTuple3     : ErlTerm -> Maybe (ErlTuple3 ErlTerm ErlTerm ErlTerm)
%extern prim__erlDecodeTuple4     : ErlTerm -> Maybe (ErlTuple4 ErlTerm ErlTerm ErlTerm ErlTerm)
%extern prim__erlDecodeTuple5     : ErlTerm -> Maybe (ErlTuple5 ErlTerm ErlTerm ErlTerm ErlTerm ErlTerm)
%extern prim__erlDecodeTuple6     : ErlTerm -> Maybe (ErlTuple6 ErlTerm ErlTerm ErlTerm ErlTerm ErlTerm ErlTerm)
%extern prim__erlDecodeTuple7     : ErlTerm -> Maybe (ErlTuple7 ErlTerm ErlTerm ErlTerm ErlTerm ErlTerm ErlTerm ErlTerm)
%extern prim__erlDecodeTuple8     : ErlTerm -> Maybe (ErlTuple8 ErlTerm ErlTerm ErlTerm ErlTerm ErlTerm ErlTerm ErlTerm ErlTerm)
%extern prim__erlDecodeFun0       : ErlTerm -> Maybe (ErlIOFun0 ErlTerm)
%extern prim__erlDecodeFun1       : ErlTerm -> Maybe (ErlIOFun1 a ErlTerm)
%extern prim__erlDecodeFun2       : ErlTerm -> Maybe (ErlIOFun2 a b ErlTerm)
%extern prim__erlDecodeFun3       : ErlTerm -> Maybe (ErlIOFun3 a b c ErlTerm)
%extern prim__erlDecodeFun4       : ErlTerm -> Maybe (ErlIOFun4 a b c d ErlTerm)
%extern prim__erlDecodeFun5       : ErlTerm -> Maybe (ErlIOFun5 a b c d e ErlTerm)
%extern prim__erlDecodeFun6       : ErlTerm -> Maybe (ErlIOFun6 a b c d e f ErlTerm)
%extern prim__erlDecodeFun7       : ErlTerm -> Maybe (ErlIOFun7 a b c d e f g ErlTerm)
%extern prim__erlDecodeFun8       : ErlTerm -> Maybe (ErlIOFun8 a b c d e f g h ErlTerm)

-- DECODERS

||| Decoder that always fails, with the given error message.
export
fail : String -> ErlDecoder a
fail msg =
  MkDecoder (\term => Left (Error msg))

||| Decoder that always succeeds.
export
any : ErlDecoder ErlTerm
any =
  MkDecoder (\term => Right term)

||| Decoder that always succeeds, where the success value is turned into
||| `Just value` and failure is turned into `Nothing`.
export
optional : ErlDecoder a -> ErlDecoder (Maybe a)
optional decoder =
  map Just decoder <|>
    pure Nothing

infixr 2 `lazyAlt`

||| A lazy version of `<|>`
lazyAlt : ErlDecoder a -> Lazy (ErlDecoder a) -> ErlDecoder a
lazyAlt decoder1 decoder2 = do
  result <- optional decoder1
  case result of
    Just value => pure value
    Nothing => decoder2

||| Decoder that expects an exact value.
export
exact : ErlType a => a -> ErlDecoder a
exact matchValue =
  MkDecoder (\term =>
    if prim__erlMatchExact term (cast matchValue) == 1
      then Right matchValue
      else Left (Error "Expected the value to match exactly"))

||| Decoder that expects a codepoint value.
export
codepoint : ErlDecoder Char
codepoint =
  MkDecoder (maybe (Left (Error "Expected a char")) Right . prim__erlDecodeCodepoint)

||| Decoder that expects an Erlang integer value.
export
integer : ErlDecoder Integer
integer =
  MkDecoder (maybe (Left (Error "Expected an integer")) Right . prim__erlDecodeInteger)

||| Decoder that expects a Erlang float value.
export
double : ErlDecoder Double
double =
  MkDecoder (maybe (Left (Error "Expected a double")) Right . prim__erlDecodeDouble)

||| Decoder that expects an Erlang atom value.
export
atom : ErlDecoder ErlAtom
atom =
  MkDecoder (maybe (Left (Error "Expected an atom")) Right . prim__erlDecodeAtom)

||| Decoder that expects an Erlang binary value.
export
string : ErlDecoder String
string =
  MkDecoder (maybe (Left (Error "Expected a binary")) Right . prim__erlDecodeBinary)

||| Decoder that expects a Erlang PID value.
export
pid : ErlDecoder ErlPid
pid =
  MkDecoder (maybe (Left (Error "Expected a pid")) Right . prim__erlDecodePid)

||| Decoder that expects an Erlang reference value.
export
reference : ErlDecoder ErlReference
reference =
  MkDecoder (maybe (Left (Error "Expected a reference")) Right . prim__erldecodeReference)

||| Decoder that expects an Erlang port value.
export
port : ErlDecoder ErlPort
port =
  MkDecoder (maybe (Left (Error "Expected a port")) Right . prim__erlDecodePort)

||| Decoder that expects any Erlang map.
export
anyMap : ErlDecoder ErlAnyMap
anyMap =
  MkDecoder (maybe (Left (Error "Expected a map")) Right . prim__erlDecodeAnyMap)

||| Decoder that expects any Erlang list.
|||
||| The list may either be the empty list or a list with a head and a tail.
export
anyList : ErlDecoder ErlTerm
anyList =
  MkDecoder (maybe (Left (Error "Expected a list")) Right . prim__erlDecodeAnyList)

||| Decoder that expects an Erlang empty list.
export
nil : ErlDecoder ErlNil
nil =
  MkDecoder (maybe (Left (Error "Expected a nil value")) Right . prim__erlDecodeNil)

||| Decoder that expects an Erlang list with a head and a tail.
export
cons : ErlDecoder a -> ErlDecoder b -> ErlDecoder (ErlCons a b)
cons (MkDecoder xDecoder) (MkDecoder yDecoder) =
  MkDecoder (\term => do
    let Just (x :: y) = prim__erlDecodeCons term
      | Nothing => Left (Error "Expected a cons value")
    xRes <- xDecoder x
    yRes <- yDecoder y
    pure (xRes :: yRes))

||| Decoder that expects a tuple of size 0.
export
tuple0 : ErlDecoder ErlTuple0
tuple0 =
  MkDecoder (maybe (Left (Error "Expected a tuple with 0 elements")) Right . prim__erlDecodeTuple0)

||| Decoder that expects a tuple of size 1, where each element in the tuple must
||| match the given decoder.
export
tuple1 : ErlDecoder a -> ErlDecoder (ErlTuple1 a)
tuple1 (MkDecoder aDecoder) =
  MkDecoder (\term => do
    let Just (MkTuple1 a) = prim__erlDecodeTuple1 term
      | Nothing => Left (Error "Expected a tuple with 1 element")
    pure (MkTuple1 !(aDecoder a)))

||| Decoder that expects a tuple of size 2, where each element in the tuple must
||| match the given decoder.
export
tuple2 : ErlDecoder a -> ErlDecoder b -> ErlDecoder (ErlTuple2 a b)
tuple2 (MkDecoder aDecoder) (MkDecoder bDecoder) =
  MkDecoder (\term => do
    let Just (MkTuple2 a b) = prim__erlDecodeTuple2 term
      | Nothing => Left (Error "Expected a tuple with 2 elements")
    pure (MkTuple2 !(aDecoder a) !(bDecoder b)))

||| Decoder that expects a tuple of size 3, where each element in the tuple must
||| match the given decoder.
export
tuple3 : ErlDecoder a -> ErlDecoder b -> ErlDecoder c -> ErlDecoder (ErlTuple3 a b c)
tuple3 (MkDecoder aDecoder) (MkDecoder bDecoder) (MkDecoder cDecoder) =
  MkDecoder (\term => do
    let Just (MkTuple3 a b c) = prim__erlDecodeTuple3 term
      | Nothing => Left (Error "Expected a tuple with 3 elements")
    pure (MkTuple3 !(aDecoder a) !(bDecoder b) !(cDecoder c)))

||| Decoder that expects a tuple of size 4, where each element in the tuple must
||| match the given decoder.
export
tuple4 : ErlDecoder a -> ErlDecoder b -> ErlDecoder c -> ErlDecoder d -> ErlDecoder (ErlTuple4 a b c d)
tuple4 (MkDecoder aDecoder) (MkDecoder bDecoder) (MkDecoder cDecoder) (MkDecoder dDecoder) =
  MkDecoder (\term => do
    let Just (MkTuple4 a b c d) = prim__erlDecodeTuple4 term
      | Nothing => Left (Error "Expected a tuple with 4 elements")
    pure (MkTuple4 !(aDecoder a) !(bDecoder b) !(cDecoder c) !(dDecoder d)))

||| Decoder that expects a tuple of size 5, where each element in the tuple must
||| match the given decoder.
export
tuple5 : ErlDecoder a -> ErlDecoder b -> ErlDecoder c -> ErlDecoder d -> ErlDecoder e -> ErlDecoder (ErlTuple5 a b c d e)
tuple5 (MkDecoder aDecoder) (MkDecoder bDecoder) (MkDecoder cDecoder) (MkDecoder dDecoder) (MkDecoder eDecoder) =
  MkDecoder (\term => do
    let Just (MkTuple5 a b c d e) = prim__erlDecodeTuple5 term
      | Nothing => Left (Error "Expected a tuple with 5 elements")
    pure (MkTuple5 !(aDecoder a) !(bDecoder b) !(cDecoder c) !(dDecoder d) !(eDecoder e)))

||| Decoder that expects a tuple of size 6, where each element in the tuple must
||| match the given decoder.
export
tuple6 : ErlDecoder a -> ErlDecoder b -> ErlDecoder c -> ErlDecoder d -> ErlDecoder e -> ErlDecoder f -> ErlDecoder (ErlTuple6 a b c d e f)
tuple6 (MkDecoder aDecoder) (MkDecoder bDecoder) (MkDecoder cDecoder) (MkDecoder dDecoder) (MkDecoder eDecoder) (MkDecoder fDecoder) =
  MkDecoder (\term => do
    let Just (MkTuple6 a b c d e f) = prim__erlDecodeTuple6 term
      | Nothing => Left (Error "Expected a tuple with 6 elements")
    pure (MkTuple6 !(aDecoder a) !(bDecoder b) !(cDecoder c) !(dDecoder d) !(eDecoder e) !(fDecoder f)))

||| Decoder that expects a tuple of size 6, where each element in the tuple must
||| match the given decoder.
export
tuple7 : ErlDecoder a -> ErlDecoder b -> ErlDecoder c -> ErlDecoder d -> ErlDecoder e -> ErlDecoder f -> ErlDecoder g -> ErlDecoder (ErlTuple7 a b c d e f g)
tuple7 (MkDecoder aDecoder) (MkDecoder bDecoder) (MkDecoder cDecoder) (MkDecoder dDecoder) (MkDecoder eDecoder) (MkDecoder fDecoder) (MkDecoder gDecoder) =
  MkDecoder (\term => do
    let Just (MkTuple7 a b c d e f g) = prim__erlDecodeTuple7 term
      | Nothing => Left (Error "Expected a tuple with 7 elements")
    pure (MkTuple7 !(aDecoder a) !(bDecoder b) !(cDecoder c) !(dDecoder d) !(eDecoder e) !(fDecoder f) !(gDecoder g)))

||| Decoder that expects a tuple of size 7, where each element in the tuple must
||| match the given decoder.
export
tuple8 : ErlDecoder a -> ErlDecoder b -> ErlDecoder c -> ErlDecoder d -> ErlDecoder e -> ErlDecoder f -> ErlDecoder g -> ErlDecoder h -> ErlDecoder (ErlTuple8 a b c d e f g h)
tuple8 (MkDecoder aDecoder) (MkDecoder bDecoder) (MkDecoder cDecoder) (MkDecoder dDecoder) (MkDecoder eDecoder) (MkDecoder fDecoder) (MkDecoder gDecoder) (MkDecoder hDecoder) =
  MkDecoder (\term => do
    let Just (MkTuple8 a b c d e f g h) = prim__erlDecodeTuple8 term
      | Nothing => Left (Error "Expected a tuple with 8 elements")
    pure (MkTuple8 !(aDecoder a) !(bDecoder b) !(cDecoder c) !(dDecoder d) !(eDecoder e) !(fDecoder f) !(gDecoder g) !(hDecoder h)))

||| Decoder that expects a tuple of size 8.
export
list : ErlDecoder a -> ErlDecoder (List a)
list decoder =
  nil *> pure [] `lazyAlt`
    map (\(x :: xs) => x :: xs) (cons decoder (assert_total (list decoder)))

||| Decoder that expects an Erlang list, where each element in the list must
||| match the given decoder.
export
hList : ErlDecoders xs -> ErlDecoder (ErlList xs)
hList [] = nil *> pure []
hList (x :: xs) = map (\(y :: ys) => y :: ys) (cons x (hList xs))

||| Decoder that expects an Erlang charlist.
-- http://erlang.org/doc/man/unicode.html
-- charlist() = [char()]
export
charlist : ErlDecoder ErlCharlist
charlist = do
  xs <- list codepoint
  pure (erlUnsafeCast ErlCharlist xs)

||| Decoder that expects an Erlang IO data
-- http://erlang.org/doc/man/unicode.html#type-chardata
-- chardata() = charlist() | unicode_binary()
-- charlist() = maybe_improper_list(char() | unicode_binary() | charlist(), unicode_binary() | [])
-- maybe_improper_list(X, Y) = [X | maybe_improper_list(X, Y)]
export
ioData : ErlDecoder ErlTerm
ioData =
  map believe_me string `lazyAlt`
    map believe_me nil `lazyAlt`
    map believe_me (cons (assert_total listHead) (assert_total ioData))
  where
    listHead : ErlDecoder String
    listHead =
      map believe_me codepoint `lazyAlt` -- NOTE: Codepoints are only valid in head position in an IO list
        map believe_me string `lazyAlt`
        map believe_me nil `lazyAlt`
        map believe_me (cons (assert_total listHead) ioData)

||| Decoder for an Erlang map entry.
export
mapEntry : ErlType key => key -> ErlDecoder value -> ErlDecoder value
mapEntry key (MkDecoder valueDecoder) =
  MkDecoder (\term => do
    let Just m = prim__erlDecodeAnyMap term
      | Nothing => Left (Error "Expected a map")
    let lookupResult = erlUnsafeCall ErlTerm "maps" "find" [key, m]
    let Just (MkTuple2 ok value) = prim__erlDecodeTuple2 lookupResult
      | Nothing => Left (Error "Could not find key in map")
    valueDecoder value)

||| Decoder for an Erlang map containing at least the specified entries.
|||
||| This function does not put any restrictions on the keys and values because
||| getting them wrong just means you won't get the expected result. It will
||| not result in any run-time errors.
export
mapSubset : ErlMapDecoders xs -> ErlDecoder (ErlMapSubset xs)
mapSubset [] = believe_me anyMap
mapSubset (MkDecoderMapEntry key valueDecoder :: xs) = believe_me (mapEntry (MkRaw key) valueDecoder *> mapSubset xs)

||| Decoder that expects a function of arity 0.
|||
||| The returned function from the `fun/N` decoders is wrapped in the `IO`
||| type in case the function performs any side-effects. The returned function
||| is also wrapped in a try/catch in case in crashes at run-time.
|||
||| The try/catch is especially important for the `fun/N` decoders where the
||| arity is 1 or higher because, in these cases, the caller is allowed to choose
||| any type for the input parameters of the returned function. If the values
||| passed to the Erlang function are not what the Erlang function expects, it
||| could cause an run-time error.
export
fun0 : ErlDecoder (IO (Either ErlException ErlTerm))
fun0 =
  MkDecoder (\term => do
    let Just (MkIOFun0 fun) = prim__erlDecodeFun0 term
      | Nothing => Left (Error "Expected a function of arity 0")
    pure $ erlTryCatch fun)

||| Decoder that expects a function of arity 1.
|||
||| See the documentation of `fun0` for more details.
export
fun1 : (a : Type) -> ErlDecoder (a -> IO (Either ErlException ErlTerm))
fun1 aType =
  MkDecoder (\term => do
    let Just (MkIOFun1 fun) = prim__erlDecodeFun1 term
      | Nothing => Left (Error "Expected a function of arity 1")
    pure $ (\a => erlTryCatch (fun a)))

||| Decoder that expects a function of arity 2.
|||
||| See the documentation of `fun0` for more details.
export
fun2 : (a : Type) -> (b : Type) -> ErlDecoder (a -> b -> IO (Either ErlException ErlTerm))
fun2 aType bType =
  MkDecoder (\term => do
    let Just (MkIOFun2 fun) = prim__erlDecodeFun2 term
      | Nothing => Left (Error "Expected a function of arity 2")
    pure $ (\a, b => erlTryCatch (fun a b)))

||| Decoder that expects a function of arity 3.
|||
||| See the documentation of `fun0` for more details.
export
fun3 : (a : Type) -> (b : Type) -> (c : Type) -> ErlDecoder (a -> b -> c -> IO (Either ErlException ErlTerm))
fun3 aType bType cType =
  MkDecoder (\term => do
    let Just (MkIOFun3 fun) = prim__erlDecodeFun3 term
      | Nothing => Left (Error "Expected a function of arity 3")
    pure $ (\a, b, c => erlTryCatch (fun a b c)))

||| Decoder that expects a function of arity 4.
|||
||| See the documentation of `fun0` for more details.
export
fun4 : (a : Type) -> (b : Type) -> (c : Type) -> (d : Type) -> ErlDecoder (a -> b -> c -> d -> IO (Either ErlException ErlTerm))
fun4 aType bType cType dType =
  MkDecoder (\term => do
    let Just (MkIOFun4 fun) = prim__erlDecodeFun4 term
      | Nothing => Left (Error "Expected a function of arity 4")
    pure $ (\a, b, c, d => erlTryCatch (fun a b c d)))

||| Decoder that expects a function of arity 5.
|||
||| See the documentation of `fun0` for more details.
export
fun5 : (a : Type) -> (b : Type) -> (c : Type) -> (d : Type) -> (e : Type) -> ErlDecoder (a -> b -> c -> d -> e -> IO (Either ErlException ErlTerm))
fun5 aType bType cType dType eType =
  MkDecoder (\term => do
    let Just (MkIOFun5 fun) = prim__erlDecodeFun5 term
      | Nothing => Left (Error "Expected a function of arity 5")
    pure $ (\a, b, c, d, e => erlTryCatch (fun a b c d e)))

||| Decoder that expects a function of arity 6.
|||
||| See the documentation of `fun0` for more details.
export
fun6 : (a : Type) -> (b : Type) -> (c : Type) -> (d : Type) -> (e : Type) -> (f : Type) -> ErlDecoder (a -> b -> c -> d -> e -> f -> IO (Either ErlException ErlTerm))
fun6 aType bType cType dType eType fType =
  MkDecoder (\term => do
    let Just (MkIOFun6 fun) = prim__erlDecodeFun6 term
      | Nothing => Left (Error "Expected a function of arity 6")
    pure $ (\a, b, c, d, e, f => erlTryCatch (fun a b c d e f)))

||| Decoder that expects a function of arity 7.
|||
||| See the documentation of `fun0` for more details.
export
fun7 : (a : Type) -> (b : Type) -> (c : Type) -> (d : Type) -> (e : Type) -> (f : Type) -> (g : Type) -> ErlDecoder (a -> b -> c -> d -> e -> f -> g -> IO (Either ErlException ErlTerm))
fun7 aType bType cType dType eType fType gType =
  MkDecoder (\term => do
    let Just (MkIOFun7 fun) = prim__erlDecodeFun7 term
      | Nothing => Left (Error "Expected a function of arity 7")
    pure $ (\a, b, c, d, e, f, g => erlTryCatch (fun a b c d e f g)))

||| Decoder that expects a function of arity 8.
|||
||| See the documentation of `fun0` for more details.
export
fun8 : (a : Type) -> (b : Type) -> (c : Type) -> (d : Type) -> (e : Type) -> (f : Type) -> (g : Type) -> (h : Type) -> ErlDecoder (a -> b -> c -> d -> e -> f -> g -> h -> IO (Either ErlException ErlTerm))
fun8 aType bType cType dType eType fType gType hType =
  MkDecoder (\term => do
    let Just (MkIOFun8 fun) = prim__erlDecodeFun8 term
      | Nothing => Left (Error "Expected a function of arity 8")
    pure $ (\a, b, c, d, e, f, g, h => erlTryCatch (fun a b c d e f g h)))

||| Decoder that expects an Erlang boolean value.
|||
||| Note that the Idris `Bool` type is not represented as the Erlang atoms
||| `true` and `false`. It is still useful to be able to decode those atoms
||| into the type `Bool`.
export
bool : ErlDecoder Bool
bool =
  (exact (MkAtom "true") *> pure True)
    <|> (exact (MkAtom "false") *> pure False)

||| Decoder that expects an Erlang value in the format `{ok, Value}`.
export
okTuple : ErlDecoder a -> ErlDecoder a
okTuple decoder =
  map (\(MkTuple2 _ result) => result) (tuple2 (exact (MkAtom "ok")) decoder)

||| Decoder that expects an Erlang value in the format `{error, Value}`.
export
errorTuple : ErlDecoder a -> ErlDecoder a
errorTuple decoder =
  map (\(MkTuple2 _ result) => result) (tuple2 (exact (MkAtom "error")) decoder)


text:
||| An App that can generate fresh integer.
|||
||| Copyright 2021, HATTORI, Hiroki
||| This file is released under the MIT license, see LICENSE for more detail.
|||
module Control.App.Fresh

import Control.App

export Fresh : Type -> List Type -> Type
Fresh tag = State tag Int

export fresh : (0 tag:_) -> (Fresh tag e => App e Int)
fresh tag = modify tag (\x => x + 1) >> get tag

export runFresh : tag -> (Fresh tag e => App e a) -> App e a
runFresh tag = new 0

-- vim: tw=80 sw=2 expandtab :

ext: idr


text:
data Format = Number Format
            | Str Format
            | Character Format
            | Decimal Format
            | Lit String Format
            | End

PrintfType : Format -> Type
PrintfType (Number fmt) = (i:Int) -> PrintfType fmt
PrintfType (Str fmt) = (s:String) -> PrintfType fmt
PrintfType (Character fmt) = (c:Char) -> PrintfType fmt
PrintfType (Decimal fmt) = (d:Double) -> PrintfType fmt
PrintfType (Lit str fmt) = PrintfType fmt
PrintfType End = String

printfFmt : (fmt : Format) -> (acc : String) -> PrintfType fmt
printfFmt (Number fmt) acc = \i => printfFmt fmt (acc ++ show i)
printfFmt (Str fmt) acc = \s => printfFmt fmt (acc ++ s)
printfFmt (Character fmt) acc = \c => printfFmt fmt (acc ++ show c)
printfFmt (Decimal fmt) acc = \d => printfFmt fmt (acc ++ show d)
printfFmt (Lit lit fmt) acc = printfFmt fmt (acc ++ lit)
printfFmt End acc = acc

toFormat : (xs : List Char) -> Format
toFormat [] = End
toFormat ('%' :: 'd' :: chars) = Number (toFormat chars)
toFormat ('%' :: 's' :: chars) = Str (toFormat chars)
toFormat ('%' :: 'c' :: chars) = Character (toFormat chars)
toFormat ('%' :: 'f' :: chars) = Decimal (toFormat chars)
toFormat (c :: chars) = case toFormat chars of
                             Lit lit chars' => Lit (strCons c lit) chars'
                             fmt => Lit (strCons c "") fmt

printf : (fmt : String) -> PrintfType (toFormat (unpack fmt))
printf fmt = printfFmt _ ""

max_stars_repo_name: janschultecom/idris-examples

max_issues_repo_name: janschultecom/idris-examples

max_forks_repo_name: janschultecom/idris-examples


text:
import Data.Nat.Views

toBinary : Nat -> String
toBinary k with (halfRec k)
  toBinary Z | HalfRecZ = ""
  toBinary (n + n) | (HalfRecEven rec) = (toBinary n | rec) ++ "0"
  toBinary (S (n + n)) | (HalfRecOdd rec) = (toBinary n | rec) ++ "1"

max_stars_repo_name: tekerson/type-driven-development

max_issues_repo_name: tekerson/type-driven-development

max_forks_repo_name: tekerson/type-driven-development


text:
= Induction : Proof by Induction

> module Induction

First, we import all of our definitions from the previous chapter.

> import Basics

Next, we import the following \idr{Prelude} modules, since we'll be dealing with
natural numbers.

> import Prelude.Interfaces
> import Prelude.Nat

For \idr{import Basics} to work, you first need to use `idris` to compile
`Basics.lidr` into `Basics.ibc`. This is like making a .class file from a .java
file, or a .o file from a .c file. There are at least two ways to do it:

  - In your editor with an Idris plugin, e.g. [Emacs][idris-mode]:

    Open `Basics.lidr`. Evaluate \idr{idris-load-file}.

    There exists similar support for [Vim][idris-vim], [Sublime
    Text][idris-sublime] and [Visual Studio Code][idris-vscode] as well.

    [idris-mode]: https://github.com/idris-hackers/idris-mode
    [idris-vim]: https://github.com/idris-hackers/idris-vim
    [idris-sublime]: https://github.com/idris-hackers/idris-sublime
    [idris-vscode]: https://github.com/zjhmale/vscode-idris

  - From the command line:

    Run \mintinline[]{sh}{idris --check --total --noprelude src/Basics.lidr}.

    Refer to the Idris man page (or \mintinline[]{sh}{idris --help} for
    descriptions of the flags.

> %access public export

> %default total

== Proof by Induction

We proved in the last chapter that \idr{0} is a neutral element for \idr{+} on
the left using an easy argument based on simplification. The fact that it is
also a neutral element on the _right_...

```coq
Theorem plus_n_O_firsttry : forall n:nat,
  n = n + 0.
```

... cannot be proved in the same simple way in Coq, but as we saw in `Basics`,
Idris's \idr{Refl} just works.

To prove interesting facts about numbers, lists, and other inductively defined
sets, we usually need a more powerful reasoning principle: _induction_.

Recall (from high school, a discrete math course, etc.) the principle of
induction over natural numbers: If \idr{p n} is some proposition involving a
natural number \idr{n} and we want to show that \idr{p} holds for _all_ numbers
\idr{n}, we can reason like this:

  - show that \idr{p Z} holds;
  - show that, for any \idr{k}, if \idr{p k} holds, then so does \idr{p (S k)};
  - conclude that \idr{p n} holds for all \idr{n}.

In Idris, the steps are the same and can often be written as function clauses by
case splitting. Here's how this works for the theorem at hand.

> plus_n_Z : (n : Nat) -> n = n + 0
> plus_n_Z  Z    = Refl
> plus_n_Z (S k) =
>   let inductiveHypothesis = plus_n_Z k in
>     rewrite inductiveHypothesis in Refl

In the first clause, \idr{n} is replaced by \idr{Z} and the goal becomes \idr{0
= 0}, which follows by \idr{Refl}exivity. In the second, \idr{n} is replaced by
\idr{S k} and the goal becomes \idr{S k = S (plus k 0)}. Then we define the
inductive hypothesis, \idr{k = k + 0}, which can be written as \idr{plus_n_Z k},
and the goal follows from it.

> minus_diag : (n : Nat) -> minus n n = 0
> minus_diag  Z    = Refl
> minus_diag (S k) = minus_diag k

==== Exercise: 2 stars, recommended (basic_induction)

Prove the following using induction. You might need previously proven results.

> mult_0_r : (n : Nat) -> n * 0 = 0
> mult_0_r n = ?mult_0_r_rhs

> plus_n_Sm : (n, m : Nat) -> S (n + m) = n + (S m)
> plus_n_Sm n m = ?plus_n_Sm_rhs

> plus_comm : (n, m : Nat) -> n + m = m + n
> plus_comm n m = ?plus_comm_rhs

> plus_assoc : (n, m, p : Nat) -> n + (m + p) = (n + m) + p
> plus_assoc n m p = ?plus_assoc_rhs

$\square$

==== Exercise: 2 stars (double_plus)

Consider the following function, which doubles its argument:

> double : (n : Nat) -> Nat
> double  Z    = Z
> double (S k) = S (S (double k))

Use induction to prove this simple fact about \idr{double}:

> double_plus : (n : Nat) -> double n = n + n
> double_plus n = ?double_plus_rhs

$\square$

==== Exercise: 2 stars, optional (evenb_S)

One inconvenient aspect of our definition of \idr{evenb n} is that it may need
to perform a recursive call on \idr{n - 2}. This makes proofs about \idr{evenb
n} harder when done by induction on \idr{n}, since we may need an induction
hypothesis about \idr{n - 2}. The following lemma gives a better
characterization of \idr{evenb (S n)}:

> evenb_S : (n : Nat) -> evenb (S n) = not (evenb n)
> evenb_S n = ?evenb_S_rhs

$\square$

== Proofs Within Proofs

\ \todo[inline]{Edit the section}

In Coq, as in informal mathematics, large proofs are often broken into a
sequence of theorems, with later proofs referring to earlier theorems. But
sometimes a proof will require some miscellaneous fact that is too trivial and
of too little general interest to bother giving it its own top-level name. In
such cases, it is convenient to be able to simply state and prove the needed
"sub-theorem" right at the point where it is used. The `assert` tactic allows us
to do this. For example, our earlier proof of the \idr{mult_0_plus} theorem
referred to a previous theorem named \idr{plus_Z_n}. We could instead use
`assert` to state and prove \idr{plus_Z_n} in-line:

> mult_0_plus' : (n, m : Nat) -> (0 + n) * m = n * m
> mult_0_plus' n m = Refl

The `assert` tactic introduces two sub-goals. The first is the assertion itself;
by prefixing it with `H:` we name the assertion `H`. (We can also name the
assertion with `as` just as we did above with `destruct` and `induction`, i.e.,
`assert (0 + n = n) as H`.) Note that we surround the proof of this assertion
with curly braces `{ ... }`, both for readability and so that, when using Coq
interactively, we can see more easily when we have finished this sub-proof. The
second goal is the same as the one at the point where we invoke `assert` except
that, in the context, we now have the assumption `H` that `0 + n = n`. That is,
`assert` generates one subgoal where we must prove the asserted fact and a
second subgoal where we can use the asserted fact to make progress on whatever
we were trying to prove in the first place.

The `assert` tactic is handy in many sorts of situations. For example, suppose
we want to prove that `(n + m) + (p + q) = (m + n) + (p + q)`. The only
difference between the two sides of the `=` is that the arguments `m` and `n` to
the first inner `+` are swapped, so it seems we should be able to use the
commutativity of addition (`plus_comm`) to rewrite one into the other. However,
the `rewrite` tactic is a little stupid about _where_ it applies the rewrite.
There are three uses of `+` here, and it turns out that doing `rewrite ->
plus_comm` will affect only the _outer_ one...

```idris
plus_rearrange_firsttry : (n, m, p, q : Nat) ->
                          (n + m) + (p + q) = (m + n) + (p + q)
plus_rearrange_firsttry n m p q = rewrite plus_comm in Refl
```
```
When checking right hand side of plus_rearrange_firsttry with expected type
        n + m + (p + q) = m + n + (p + q)

_ does not have an equality type ((n1 : Nat) ->
(n1 : Nat) -> plus n1 m1 = plus m1 n1)
```

To get \idr{plus_comm} to apply at the point where we want it to, we can
introduce a local lemma using the \idr{where} keyword stating that \idr{n + m =
m + n} (for the particular \idr{m} and \idr{n} that we are talking about here),
prove this lemma using \idr{plus_comm}, and then use it to do the desired
rewrite.

> plus_rearrange : (n, m, p, q : Nat) ->
>                  (n + m) + (p + q) = (m + n) + (p + q)
> plus_rearrange n m p q = rewrite plus_rearrange_lemma n m in Refl
>   where
>   plus_rearrange_lemma : (n, m : Nat) -> n + m = m + n
>   plus_rearrange_lemma = plus_comm

== More Exercises

==== Exercise: 3 stars, recommended (mult_comm)

Use \idr{rewrite} to help prove this theorem. You shouldn't need to use
induction on \idr{plus_swap}.

> plus_swap : (n, m, p : Nat) -> n + (m + p) = m + (n + p)
> plus_swap n m p = ?plus_swap_rhs

Now prove commutativity of multiplication. (You will probably need to define and
prove a separate subsidiary theorem to be used in the proof of this one. You may
find that \idr{plus_swap} comes in handy.)

> mult_comm : (m, n : Nat) -> m * n = n * m
> mult_comm m n = ?mult_comm_rhs

$\square$

==== Exercise: 3 stars, optional (more_exercises)

\ \todo[inline]{Edit}

Take a piece of paper. For each of the following theorems, first _think_ about
whether (a) it can be proved using only simplification and rewriting, (b) it
also requires case analysis (`destruct`), or (c) it also requires induction.
Write down your prediction. Then fill in the proof. (There is no need to turn in
your piece of paper; this is just to encourage you to reflect before you hack!)

> lte_refl : (n : Nat) -> True = lte n n
> lte_refl n = ?lte_refl_rhs

> zero_nbeq_S : (n : Nat) -> 0 == (S n) = False
> zero_nbeq_S n = ?zero_nbeq_S_rhs

> andb_false_r : (b : Bool) -> b && False = False
> andb_false_r b = ?andb_false_r_rhs

> plus_ble_compat_l : (n, m, p : Nat) ->
>                     lte n m = True -> lte (p + n) (p + m) = True
> plus_ble_compat_l n m p prf = ?plus_ble_compat_l_rhs

> S_nbeq_0 : (n : Nat) -> (S n) == 0 = False
> S_nbeq_0 n = ?S_nbeq_0_rhs

> mult_1_l : (n : Nat) -> 1 * n = n
> mult_1_l n = ?mult_1_l_rhs

> all3_spec : (b, c : Bool) ->
>             (b && c) || ((not b) || (not c)) = True
> all3_spec b c = ?all3_spec_rhs

> mult_plus_distr_r : (n, m, p : Nat) -> (n + m) * p = (n * p) + (m * p)
> mult_plus_distr_r n m p = ?mult_plus_distr_r_rhs

> mult_assoc : (n, m, p : Nat) -> n * (m * p) = (n * m) * p
> mult_assoc n m p = ?mult_assoc_rhs

$\square$

==== Exercise: 2 stars, optional (beq_nat_refl)

\ \todo[inline]{Edit}

Prove the following theorem. (Putting the \idr{True} on the left-hand side of
the equality may look odd, but this is how the theorem is stated in the Coq
standard library, so we follow suit. Rewriting works equally well in either
direction, so we will have no problem using the theorem no matter which way we
state it.)

> beq_nat_refl : (n : Nat) -> True = n == n
> beq_nat_refl n = ?beq_nat_refl_rhs

$\square$

==== Exercise: 2 stars, optional (plus_swap')

\ \todo[inline]{Edit}

The `replace` tactic allows you to specify a particular subterm to rewrite and
what you want it rewritten to: `replace (t) with (u)` replaces (all copies of)
expression `t` in the goal by expression `u`, and generates `t = u` as an
additional subgoal. This is often useful when a plain \idr{rewrite} acts on the
wrong part of the goal.

Use the `replace` tactic to do a proof of \idr{plus_swap'}, just like
\idr{plus_swap} but without needing `assert (n + m = m + n)`.

> plus_swap' : (n, m, p : Nat) -> n + (m + p) = m + (n + p)
> plus_swap' n m p = ?plus_swap__rhs

$\square$

==== Exercise: 3 stars, recommended (binary_commute)

Recall the \idr{incr} and \idr{bin_to_nat} functions that you wrote for the
\idr{binary} exercise in the `Basics` chapter. Prove that the following diagram
commutes:

           bin --------- incr -------> bin
            |                           |
        bin_to_nat                  bin_to_nat
            |                           |
            v                           v
           nat ---------- S ---------> nat

That is, incrementing a binary number and then converting it to a (unary)
natural number yields the same result as first converting it to a natural number
and then incrementing. Name your theorem \idr{bin_to_nat_pres_incr} ("pres" for
"preserves").

Before you start working on this exercise, please copy the definitions from your
solution to the \idr{binary} exercise here so that this file can be graded on
its own. If you find yourself wanting to change your original definitions to
make the property easier to prove, feel free to do so!

$\square$

==== Exercise: 5 stars, advanced (binary_inverse)

This exercise is a continuation of the previous exercise about binary numbers.
You will need your definitions and theorems from there to complete this one.

(a) First, write a function to convert natural numbers to binary numbers. Then
    prove that starting with any natural number, converting to binary, then
    converting back yields the same natural number you started with.

(b) You might naturally think that we should also prove the opposite direction:
    that starting with a binary number, converting to a natural, and then back
    to binary yields the same number we started with. However, this is not true!
    Explain what the problem is.

(c) Define a "direct" normalization function -- i.e., a function \idr{normalize}
    from binary numbers to binary numbers such that, for any binary number b,
    converting to a natural and then back to binary yields \idr{(normalize b)}.
    Prove it. (Warning: This part is tricky!)

Again, feel free to change your earlier definitions if this helps here.

$\square$

ext: lidr

max_stars_repo_name: diseraluca/software-foundations

max_issues_repo_name: diseraluca/software-foundations

max_forks_repo_name: diseraluca/software-foundations


text:
module TypesAndFunctions

%default total

public export
appEq : {a, b : Type} -> {f, g : a -> b} -> {x : a} -> f = g -> f x = g x
appEq Refl = Refl

public export
FunctionalExtensionality : (a, b : Type) -> Type
FunctionalExtensionality a b =
  {f, g : a -> b} -> ((x : a) -> f x = g x) -> f = g

public export
IsLeftInverse : {a, b : Type} -> (a -> b) -> (b -> a) -> Type
IsLeftInverse f g = (x : a) -> g (f x) = x

public export
HasLeftInverseImpliesInjective :
  {a, b : Type} -> {f : a -> b} -> {g : b -> a} ->
  IsLeftInverse f g ->
  {x, x' : a} -> f x = f x' -> x = x'
HasLeftInverseImpliesInjective isLeftInv {x} {x'} fxeq =
  trans (sym (isLeftInv x)) (trans (cong g fxeq) (isLeftInv x'))

public export
IsRightInverse : {a, b : Type} -> (a -> b) -> (b -> a) -> Type
IsRightInverse {a} {b} f g = IsLeftInverse {b=a} {a=b} g f

public export
IsInverse : {a, b : Type} -> (a -> b) -> (b -> a) -> Type
IsInverse f g = (IsLeftInverse f g, IsRightInverse f g)

public export
isInverseSym : {a, b : Type} -> {f : a -> b} -> {g : b -> a} ->
               IsInverse f g -> IsInverse g f
isInverseSym (isLeftInv, isRightInv) = (isRightInv, isLeftInv)

public export
IsBijection : {a, b : Type} -> (a -> b) -> Type
IsBijection {a} {b} f = DPair (b -> a) (IsInverse f)

public export
Bijection : (a, b : Type) -> Type
Bijection a b = DPair (a -> b) IsBijection

public export
IsBijectionForEach : {a : Type} -> {b, c : a -> Type} ->
  ((x : a) -> b x -> c x) -> Type
IsBijectionForEach f = (x : a) -> IsBijection (f x)

public export
ForEachInverse : {a : Type} -> {b, c : a -> Type} ->
  {f : (x : a) -> b x -> c x} -> IsBijectionForEach f ->
  ((x : a) -> c x -> b x)
ForEachInverse isBijection x cx = fst (isBijection x) cx

public export
ForEachInverseIsInverse : {a : Type} -> {b, c : a -> Type} ->
  {f : (x : a) -> b x -> c x} -> (isBijection : IsBijectionForEach f) ->
  ((x : a) -> IsInverse (f x) (ForEachInverse {f} isBijection x))
ForEachInverseIsInverse isBijection x =
  let isBijectionX = snd (isBijection x) in
  (\bx => fst isBijectionX bx, \cx => snd isBijectionX cx)

public export
forEachInverseSym : {a : Type} -> {b, c : a -> Type} ->
  {f : (x : a) -> b x -> c x} -> (isBijection : IsBijectionForEach f) ->
  IsBijectionForEach {a} {b=c} {c=b} (ForEachInverse {f} isBijection)
forEachInverseSym isBijection x =
  (f x ** (snd (snd (isBijection x)), fst (snd (isBijection x))))

max_stars_repo_name: rokopt/dao-fp-exercises

max_issues_repo_name: rokopt/dao-fp-exercises

max_forks_repo_name: rokopt/dao-fp-exercises


text:
import Data.Vect

allLengths : Vect l String -> Vect l Nat
allLengths [] = []
allLengths (x :: xs) = length x :: allLengths xs

insert : Ord elem => (x : elem) -> (xsSorted : Vect len elem) -> Vect (S len) elem
insert x [] = [x]
insert x (y :: xs) = case x < y of
                          False => y :: insert x xs
                          True => x :: y :: xs

insSort : Ord elem => Vect n elem -> Vect n elem
insSort [] = []
insSort (x :: xs) = let xsSorted = insSort xs in
                        insert x xsSorted

myLength : List a -> Nat
myLength [] = 0
myLength (x :: xs) = 1 + myLength xs

myRev : List a -> List a
myRev [] = []
myRev (x :: xs) = myRev xs ++ [x]

myMap : (a -> b) -> List a -> List b
myMap f [] = []
myMap f (x :: xs) = f x :: map f xs

vecMap : (a -> b) -> Vect n a -> Vect n b
vecMap f [] = []
vecMap f (x :: xs) = f x :: vecMap f xs


text:
> module Main

Import the literate module

> import Lit

> main : IO ()
> main = Lit.main

max_stars_repo_name: grin-compiler/idris-grin

max_issues_repo_name: grin-compiler/idris-grin

max_forks_repo_name: grin-compiler/idris-grin