text:
module Compiler.Erlang.Codegen.NamedCExpToErlExpr.RtsSupport

import Data.List
import Data.NameMap
import Data.Stream
import Data.Vect
import Core.Core
import Core.TT
import Compiler.Erlang.Name
import Compiler.Erlang.IR.ErlExpr

%default total

-- LOCAL VARIABLES

export
data LV : Type where

export
newLocalVar : {auto lv : Ref LV LocalVars} -> Core LocalVar
newLocalVar = do
  MkLocalVars varPrefix nextIndex <- get LV
  put LV $ MkLocalVars varPrefix (nextIndex + 1)
  pure $ MkLocalVar varPrefix nextIndex

export
newLocalVars : {auto lv : Ref LV LocalVars} -> (count : Nat) -> Core (List LocalVar)
newLocalVars Z = pure []
newLocalVars (S k) = do
  newVar <- newLocalVar
  vars <- newLocalVars k
  pure (newVar :: vars)

export
addLocalVar : {auto lv : Ref LV LocalVars} -> (varName : Name) -> NameMap LocalVar -> Core (NameMap LocalVar, LocalVar)
addLocalVar varName vs = do
  newVar <- newLocalVar
  pure (insert varName newVar vs, newVar)

export
addLocalVars : {auto lv : Ref LV LocalVars} -> (args : List Name) -> NameMap LocalVar -> Core (NameMap LocalVar, List LocalVar)
addLocalVars [] vs = pure (vs, [])
addLocalVars (n :: ns) vs = do
  (vs', newVar) <- addLocalVar n vs
  (vs'', vars) <- addLocalVars ns vs'
  pure (vs'', newVar :: vars)

-- MISC

export
genFC : FC -> Line
genFC (MkFC fileName (startLine, startCol) (endLine, endCol)) = startLine
genFC EmptyFC = 1 -- TODO: What value should I put here?

export
genErased : Line -> ErlExpr
genErased l =
  EAtom l "erased"

-- DATA CONSTRUCTORS

export
genMkUnit : Line -> ErlExpr
genMkUnit l =
  ECon l (constructorName (NS builtinNS (UN "MkUnit"))) []

export
genJust : Line -> ErlExpr -> ErlExpr
genJust l expr =
  ECon l (constructorName (NS typesNS (UN "Just"))) [expr]

export
genNothing : Line -> ErlExpr
genNothing l =
  ECon l (constructorName (NS typesNS (UN "Nothing"))) []

export
genRight : Line -> ErlExpr -> ErlExpr
genRight l expr =
  ECon l (constructorName (NS typesNS (UN "Right"))) [expr]

export
genLeft : Line -> ErlExpr -> ErlExpr
genLeft l expr =
  ECon l (constructorName (NS typesNS (UN "Left"))) [expr]

-- PrimIO.MkIORes : {0 a : Type} -> (result : a) -> (1 x : %World) -> IORes a
export
genMkIORes : Line -> ErlExpr -> ErlExpr
genMkIORes l expr =
  -- Newtype optimization removes the data constructor:
  -- ECon l (constructorName (NS ["PrimIO"] (UN "MkIORes"))) [expr, EIdrisConstant l IWorldVal]
  expr

-- PrimIO.MkIO : {0 a : Type} -> (1 fn : (1 x : %World) -> IORes a) -> IO a
export
genMkIO : Line -> (worldVar : LocalVar) -> ErlExpr -> ErlExpr
genMkIO l worldVar expr =
  let fn = ELam l [worldVar] (genMkIORes l expr)
  in -- Newtype optimization removes the data constructor:
     -- ECon l (constructorName (NS ["PrimIO"] (UN "MkIO"))) [fn]
     fn

-- HELPER FUNCTIONS

export
genRef : NamespaceInfo -> Line -> Name -> ErlExpr
genRef namespaceInfo l name =
  let (modName, fnName) = moduleNameFunctionName namespaceInfo name
  in if isNameInCurrentModule namespaceInfo name
    then EAtom l fnName
    else ERef l (EAtom l modName) (EAtom l fnName)

export
genUnsafePerformIO : NamespaceInfo -> Line -> ErlExpr -> ErlExpr
genUnsafePerformIO namespaceInfo l action =
  EApp l (genRef namespaceInfo l (NS primIONS (UN "unsafePerformIO"))) [genErased l, action]

export
genFunCall : Line -> String -> String -> List ErlExpr -> ErlExpr
genFunCall l modName fnName args =
  EApp l (ERef l (EAtom l modName) (EAtom l fnName)) args

export
genList : Line -> List ErlExpr -> ErlExpr
genList l xs = foldr (\x, acc => ECons l x acc) (ENil l) xs

export
genThrow : Line -> String -> ErlExpr
genThrow l msg =
  genFunCall l "erlang" "throw" [ECharlist l msg]

export
genUnsafeStringToAtom : Line -> ErlExpr -> ErlExpr
genUnsafeStringToAtom l (EIdrisConstant _ (IString x)) = EAtom l x
genUnsafeStringToAtom l binary =
  genFunCall l "erlang" "binary_to_atom" [binary, EAtom l "utf8"]

export
genAtomToString : Line -> ErlExpr -> ErlExpr
genAtomToString l expr =
  genFunCall l "erlang" "atom_to_binary" [expr, EAtom l "utf8"]

-- TODO: Replace with `map (ELocal l)`
export
genArgsToLocals : Line -> (args : List LocalVar) -> List ErlExpr
genArgsToLocals l [] = []
genArgsToLocals l (n :: ns) = ELocal l n :: genArgsToLocals l ns

export
genAppCurriedFun : Line -> (curriedFun : ErlExpr) -> List ErlExpr -> ErlExpr
genAppCurriedFun l body [] = body
genAppCurriedFun l body (x :: xs) = genAppCurriedFun l (EApp l body [x]) xs

-- Create a curried function from an uncurried function of a given arity.
-- The transform function is applied to the inner result.
--
-- In Erlang it is similar to:
-- ```
-- fun(V0) -> fun(V1) -> Transform(UncurriedFun(V0, V1)) end end
-- ```
export
genCurry : {auto lv : Ref LV LocalVars} -> Line -> (arity : Nat) -> (transform : ErlExpr -> ErlExpr) -> (uncurriedFun : ErlExpr) -> Core ErlExpr
genCurry l arity transform uncurriedFun = curry l arity transform uncurriedFun []
  where
    curry : Line -> (arity : Nat) -> (transform : ErlExpr -> ErlExpr) -> ErlExpr -> List ErlExpr -> Core ErlExpr
    curry l Z transform body args = pure $ transform (EApp l body (reverse args))
    curry l (S k) transform body args = do
      newVar <- newLocalVar
      pure $ ELam l [newVar] !(curry l k transform body (ELocal l newVar :: args))

-- Create an uncurried function from a curried function of a given arity.
-- The transform function is applied to the inner result.
--
-- In Erlang it is similar to:
-- ```
-- fun(V0, V1) -> Transform((CurriedFun(V0))(V1)) end
-- ```
export
genUncurry : {auto lv : Ref LV LocalVars} -> Line -> (arity : Nat) -> (transform : ErlExpr -> ErlExpr) -> (curriedFun : ErlExpr) -> Core ErlExpr
genUncurry l arity transform curriedFun = do
  vars <- newLocalVars arity
  pure $ ELam l vars (transform (genAppCurriedFun l curriedFun (genArgsToLocals l vars)))

export
genEscriptMain : Line -> (body : ErlExpr) -> ErlExpr
genEscriptMain l body =
  let setEncodingCall = genFunCall l "io" "setopts" [genList l [ETuple l [EAtom l "encoding", EAtom l "unicode"]]]
  in ESequence l
      [ setEncodingCall
      , body
      ]

export
genErlMain : {auto lv : Ref LV LocalVars} -> Line -> (body : ErlExpr) -> Core ErlExpr
genErlMain l body = do
  let processFlagCall = genFunCall l "erlang" "process_flag" [EAtom l "trap_exit", EAtom l "false"]
  okVar <- newLocalVar
  errorVar <- newLocalVar
  let mainProgram = ESequence l
        [ processFlagCall
        , genEscriptMain l body
        , genHalt l 0
        ]
  pure $ ETryCatch l mainProgram okVar (ELocal l okVar) errorVar (ESequence l [genFunCall l "erlang" "display" [ELocal l errorVar], genHalt l 127])
  where
    genHalt : Line -> (errorCode : Integer) -> ErlExpr
    genHalt l errorCode = genFunCall l "erlang" "halt" [EInteger l errorCode]

-- OS

export
genOsType : {auto lv : Ref LV LocalVars} -> Line -> Core ErlExpr
genOsType l = do
  unixOsFamilyVar <- newLocalVar
  unixOsNameVar <- newLocalVar
  winOsFamilyVar <- newLocalVar
  winOsNameVar <- newLocalVar
  let osTypeCall = genFunCall l "os" "type" []
  let unixOsName = EMatcherCase l
        (ELocal l unixOsNameVar)
        [ MConst (MExact (EAtom l "darwin")) (EBinary l "darwin")
        ]
        (EBinary l "unix")
  pure $ EMatcherCase l
    osTypeCall
    [ MTuple [(unixOsFamilyVar, MExact (EAtom l "unix")), (unixOsNameVar, MAny)] unixOsName
    , MTuple [(winOsFamilyVar, MExact (EAtom l "win32")), (winOsNameVar, MAny)] (EBinary l "windows")
    ]
    (EBinary l "unknown")

-- BOOLEANS

export
genBoolToInt : Line -> ErlExpr -> ErlExpr
genBoolToInt l expr =
  EMatcherCase l
    expr
    [ MConst (MExact (EAtom l "false")) (EInteger l 0)
    ]
    (EInteger l 1)

-- ARITHMETIC

integerPower : Integer -> Nat -> Integer
integerPower base exp = product (take exp (repeat base))

genIntOp : (op : String) -> Line -> (bits : Nat) -> ErlExpr -> ErlExpr -> ErlExpr
genIntOp op l bits x y = EOp l "rem" (EOp l op x y) (EInteger l (integerPower 2 bits))

export
genIntAdd : Line -> (bits : Nat) -> ErlExpr -> ErlExpr -> ErlExpr
genIntAdd = genIntOp "+"

export
genIntSub : Line -> (bits : Nat) -> ErlExpr -> ErlExpr -> ErlExpr
genIntSub = genIntOp "-"

export
genIntMult : Line -> (bits : Nat) -> ErlExpr -> ErlExpr -> ErlExpr
genIntMult = genIntOp "*"

export
genIntDiv : Line -> (bits : Nat) -> ErlExpr -> ErlExpr -> ErlExpr
genIntDiv = genIntOp "div"

export
genIntShiftL : Line -> (bits : Nat) -> ErlExpr -> ErlExpr -> ErlExpr
genIntShiftL = genIntOp "bsl"

genMod : Line -> ErlExpr -> ErlExpr -> ErlExpr
genMod l x y =
  EMatcherCase l
    (EOp l ">=" x (EInteger l 0))
    [ MConst (MExact (EAtom l "true")) (EOp l "rem" x y)
    ]
    (EOp l "rem" (EOp l "+" x y) y)

-- STRINGS

genUnicodeStringOp : (op : String) -> Line -> ErlExpr -> ErlExpr -> ErlExpr
genUnicodeStringOp op l x y =
  genBoolToInt l (EOp l op x y)

export
genUnicodeStringLT : Line -> ErlExpr -> ErlExpr -> ErlExpr
genUnicodeStringLT = genUnicodeStringOp "<"

export
genUnicodeStringLTE : Line -> ErlExpr -> ErlExpr -> ErlExpr
genUnicodeStringLTE = genUnicodeStringOp "=<"

export
genUnicodeStringEQ : Line -> ErlExpr -> ErlExpr -> ErlExpr
genUnicodeStringEQ = genUnicodeStringOp "=:="

export
genUnicodeStringGTE : Line -> ErlExpr -> ErlExpr -> ErlExpr
genUnicodeStringGTE = genUnicodeStringOp ">="

export
genUnicodeStringGT : Line -> ErlExpr -> ErlExpr -> ErlExpr
genUnicodeStringGT = genUnicodeStringOp ">"

-- NOTE: Must be total
export
genUnicodeStringLength : Line -> (str : ErlExpr) -> ErlExpr
genUnicodeStringLength l str =
  genFunCall l "string" "length" [str]

-- NOTE: Is allowed to be partial
export
genUnicodeStringHead : Line -> (str : ErlExpr) -> ErlExpr
genUnicodeStringHead l str =
  let nextGraphemeCall = genFunCall l "string" "next_grapheme" [str]
  in genFunCall l "erlang" "hd" [nextGraphemeCall]

-- NOTE: Is allowed to be partial
--
-- Erlang docs for `string_grapheme/1`:
-- (https://erlang.org/doc/man/string.html#next_grapheme-1)
--
-- Returns the first codepoint in String and the rest of String in the tail.
-- Returns an empty list if String is empty or an {error, String} tuple if
-- the next byte is invalid.
export
genUnicodeStringTail : {auto lv : Ref LV LocalVars} -> Line -> (str : ErlExpr) -> Core ErlExpr
genUnicodeStringTail l str = do
  headVar <- newLocalVar
  tailVar <- newLocalVar
  let nextGraphemeCall = genFunCall l "string" "next_grapheme" [str]
  pure $ EMatcherCase l
      nextGraphemeCall
      [ MCons MAny MBinary headVar tailVar (ELocal l tailVar)
      ]
      (EBinary l "")

-- NOTE: Is allowed to be partial
export
genUnicodeStringIndex : Line -> (str : ErlExpr) -> (index : ErlExpr) -> ErlExpr
genUnicodeStringIndex l str index =
  let charStringCall = genFunCall l "string" "slice" [str, index, EInteger l 1]
      nextGraphemeCall = genFunCall l "string" "next_grapheme" [charStringCall]
  in genFunCall l "erlang" "hd" [nextGraphemeCall]

-- NOTE: Must be total
export
genUnicodeStringCons : Line -> (char : ErlExpr) -> (str : ErlExpr) -> ErlExpr
genUnicodeStringCons l char str =
  let charBinary = genFunCall l "unicode" "characters_to_binary" [genList l [char]]
  in EBinaryConcat l charBinary str

-- NOTE: Must be total
export
genUnicodeStringAppend : Line -> (str1 : ErlExpr) -> (str2 : ErlExpr) -> ErlExpr
genUnicodeStringAppend l str1 str2 =
  EBinaryConcat l str1 str2

-- NOTE: Must be total
export
genUnicodeStringReverse : Line -> (str : ErlExpr) -> ErlExpr
genUnicodeStringReverse l str =
  let reversedString = genFunCall l "string" "reverse" [str]
  in genFunCall l "unicode" "characters_to_binary" [reversedString]

-- NOTE: Must be total
export
genUnicodeStringSubstr : Line -> (start : ErlExpr) -> (len : ErlExpr) -> (str : ErlExpr) -> ErlExpr
genUnicodeStringSubstr l start len str =
  genFunCall l "string" "slice" [str, start, len]

-- CHARACTERS

-- A codepoint is represented by an integer between 0x0 and 0x10FFFF.
-- Return "replacement character" (0xFFFD) if character is not recognized.
-- https://en.wikipedia.org/wiki/Specials_(Unicode_block)
genValidChar : Line -> ErlExpr -> ErlExpr
genValidChar l x =
  EMatcherCase l x [MCodepoint] (EInteger l 65533)

-- CAST: Integer -> *

export
genIntegerToInt : Line -> ErlExpr -> ErlExpr
genIntegerToInt l integer =
  integer

export
genIntegerToDouble : Line -> ErlExpr -> ErlExpr
genIntegerToDouble l integer =
  genFunCall l "erlang" "float" [integer]

export
genIntegerToString : Line -> ErlExpr -> ErlExpr
genIntegerToString l integer =
  genFunCall l "erlang" "integer_to_binary" [integer]

export
genIntegerToBits : Line -> (bits : Nat) -> ErlExpr -> ErlExpr
genIntegerToBits l bits integer =
  genMod l integer (EInteger l (integerPower 2 bits))

-- CAST: Int -> *

export
genIntToInteger : Line -> ErlExpr -> ErlExpr
genIntToInteger l int =
  int

export
genIntToDouble : Line -> ErlExpr -> ErlExpr
genIntToDouble l int =
  genFunCall l "erlang" "float" [int]

-- Char is an integer
export
genIntToChar : Line -> ErlExpr -> ErlExpr
genIntToChar l int =
  genValidChar l int

export
genIntToString : Line -> ErlExpr -> ErlExpr
genIntToString l int =
  genFunCall l "erlang" "integer_to_binary" [int]

-- CAST: Double -> *

export
genDoubleToInteger : Line -> ErlExpr -> ErlExpr
genDoubleToInteger l double =
  genFunCall l "erlang" "trunc" [double]

export
genDoubleToInt : Line -> ErlExpr -> ErlExpr
genDoubleToInt l double =
  genFunCall l "erlang" "trunc" [double]

export
genDoubleToString : Line -> ErlExpr -> ErlExpr
genDoubleToString l double =
  let opts = genList l [ETuple l [EAtom l "decimals", EInteger l 10], EAtom l "compact"]
  in genFunCall l "erlang" "float_to_binary" [double, opts]

-- CAST: Char -> *

export
genCharToInteger : Line -> ErlExpr -> ErlExpr
genCharToInteger l char =
  genValidChar l char

export
genCharToInt : Line -> ErlExpr -> ErlExpr
genCharToInt l char =
  genValidChar l char

export
genCharToString : Line -> ErlExpr -> ErlExpr
genCharToString l char =
  genFunCall l "unicode" "characters_to_binary" [genList l [char]]

-- CAST: String -> *

export
genStringToInteger : {auto lv : Ref LV LocalVars} -> Line -> ErlExpr -> Core ErlExpr
genStringToInteger l str = do
  integerVar <- newLocalVar
  restVar <- newLocalVar
  let toIntegerCall = genFunCall l "string" "to_integer" [str]
  pure $ EMatcherCase l
      toIntegerCall
      [ MTuple [(integerVar, MInteger), (restVar, MAny)]
          (EMatcherCase l
            (genFunCall l "string" "is_empty" [ELocal l restVar])
            [ MConst (MExact (EAtom l "true")) (ELocal l integerVar)
            ]
            (EInteger l 0))
      ]
      (EInteger l 0)

export
genStringToInt : {auto lv : Ref LV LocalVars} -> Line -> ErlExpr -> Core ErlExpr
genStringToInt l str =
  genStringToInteger l str

-- Try to convert String to Double
-- If it fails; try to convert String to Integer to Double
export
genStringToDouble : {auto lv : Ref LV LocalVars} -> Line -> ErlExpr -> Core ErlExpr
genStringToDouble l str = do
  errorAtomVar <- newLocalVar
  noFloatAtomVar <- newLocalVar
  floatVar <- newLocalVar
  restVar <- newLocalVar
  let toFloatCall = genFunCall l "string" "to_float" [str]
  pure $ EMatcherCase l
      toFloatCall
      [ MTuple [(errorAtomVar, MExact (EAtom l "error")), (noFloatAtomVar, MExact (EAtom l "no_float"))]
          (genFunCall l "erlang" "float" [!(genStringToInteger l str)])
      , MTuple [(floatVar, MFloat), (restVar, MAny)]
          (EMatcherCase l
            (genFunCall l "string" "is_empty" [ELocal l restVar])
            [ MConst (MExact (EAtom l "true")) (ELocal l floatVar)
            ]
            (EFloat l 0))
      ]
      (EFloat l 0)

-- IO

export
genUnicodePutStr : Line -> ErlExpr -> ErlExpr
genUnicodePutStr l str =
  genFunCall l "io" "format" [ECharlist l "~ts", genList l [str]]

export
genUnicodeGetStr : Line -> ErlExpr -> ErlExpr
genUnicodeGetStr l prompt =
  let getLineCall = genFunCall l "io" "get_line" [prompt]
      trimmedLine = genFunCall l "string" "trim" [getLineCall, EAtom l "trailing", ECharlist l "\n"]
  in genFunCall l "unicode" "characters_to_binary" [trimmedLine]


text:
import OCaml.IO

orderedType : Type -> Type
orderedType t = Module [ val "compare" (t -> t -> Int) ]

setSig : Type -> Type -> Type
setSig elt t = Module [ val "empty" t
                      , val "is_empty" (t -> Bool)
                      , val "mem" (elt -> t -> Bool)
                      , val "add" (elt -> t -> t)
                      ]

makeset : {auto p : OCaml_Types elt} ->
          orderedType elt ->
          (t : Type ** p : OCaml_Types t ** setSig elt t)
makeset {elt} ordered =
  MkDPair Ptr
  (MkDPair OCaml_Ptr
    (unsafePerformIO $
     ocamlCall "Stdlib.Set.Make" (orderedType elt -> OCaml_IO (setSig elt Ptr)) ordered))

IntOrdered : orderedType Int
IntOrdered = struct [ Let "compare" (\x => \y => x - y) ]

main : IO ()
main = do
  let MkDPair s (MkDPair _ ops) = makeset IntOrdered
  let set = ops#"empty"
  let set1 = (ops#"add") 45 set
  if (ops#"is_empty") set then putStrLn "'set' is empty"
                          else putStrLn "'set' is not empty"
  if (ops#"is_empty") set1 then putStrLn "'set1' is empty"
                           else putStrLn "'set1' is not empty"

ext: idr

max_stars_repo_name: ioanluca/real-world-idris

max_issues_repo_name: ioanluca/real-world-idris

max_forks_repo_name: ioanluca/real-world-idris


text:
module Streaming.Core

import Control.Monad.Error.Interface
import Control.Monad.RWS.Interface
import Control.Monad.Reader.Interface
import Control.Monad.State.Interface
import Control.Monad.Trans
import Control.Monad.Writer.Interface
import Control.Monad.Morph
import Data.Functor.Of
import Data.List
import Data.Nat

%default total

||| based on: https://github.com/MarcelineVQ/idris2-streaming/blob/master/src/Streaming/Internal.idr
public export
data Stream : (f : Type -> Type) -> (m : Type -> Type) -> (r : Type) -> Type where
  Step : Inf (f (Stream f m r)) -> Stream f m r
  Effect : Inf (m (Stream f m r)) -> Stream f m r
  Return : r -> Stream f m r
  Build : (forall b. (r -> b) -> (m b -> b) -> (f b -> b) -> b) -> Stream f m r

||| Wrap a new layer of a `Stream`
public export
wrap : f (Stream f m r) -> Stream f m r
wrap x = Step x

||| Wrap a new effect layer of a `Stream`
public export
effect : m (Stream f m r) -> Stream f m r
effect x = Effect x

export
build : (forall b. (r -> b) -> (m b -> b) -> (f b -> b) -> b) -> Stream f m r
build = \phi => phi Return (\x => Effect x) (\x => Step x)

||| collapse a `Stream` into another thing
export
fold : (Functor f, Monad m) => (r -> b) -> (m b -> b) -> (f b -> b) -> Stream f m r -> b
fold return effect step (Return x) = return x
fold return effect step (Effect x) = effect (assert_total fold return effect step <$> x)
fold return effect step (Step x) = step (assert_total fold return effect step <$> x)
fold return effect step (Build g) = g return effect step

||| `fold` but the argument positions are different
export
destroy : (Functor f, Monad m) => (f a -> a) -> (m a -> a) -> (r -> a) -> Stream f m r -> a
destroy step effect return = fold return effect step

||| unfold a `Stream`
export
unfold : (Functor f, Monad m) => (a -> m (Either r (f a))) -> a -> Stream f m r
unfold f a = Effect $ do
  Right a' <- f a
  | Left r => pure (Return r)
  pure (Step (assert_total unfold f <$> a'))

export
inspect : (Functor f, Monad m) => Stream f m r -> m (Either r (f (Stream f m r)))
inspect = destroy (pure . (Right . map (effect {f} {m} . map (either Return wrap)))) join (pure . Left)

export
Functor f => MFunctor (Stream f) where
  hoist f = fold Return (\x => Effect $ f x) (\x => Step x)

export
(Functor f, Monad m) => Functor (Stream f m) where
  map f x = Build (\return, effect, step => fold (return . f) effect step x)

mutual
  export
  (Functor f, Monad m) => Applicative (Stream f m) where
    pure = Return
    x <*> y = do
      assert_total (>>=) x $ \x => y >>= \y => pure (x y)

  export
    (Functor f, Monad m) => Monad (Stream f m) where
      x >>= k = Build (\return, effect, step => fold (fold return effect step . k) effect step x)

export
MonadTrans (Stream f) where
  lift x = Effect (map Return x)

export
(HasIO m, Monad (Stream f m)) => HasIO (Stream f m) where
  liftIO x = lift (liftIO x)

export
(Functor f, MonadState s m) => MonadState s (Stream f m) where
  get = lift get
  put = lift . put
  state f = lift (state f)

export
(Functor f, MonadReader s m) => MonadReader s (Stream f m) where
  ask = lift ask
  local f = hoist (local f)

export
(Functor f, MonadError e m) => MonadError e (Stream f m) where
  throwError = lift . throwError
  stream `catchError` f = fold pure (\x => assert_total catchError (Effect x) f) wrap stream

||| analogous to `Prelude.unfoldr` but for `Stream (Of a)`
export
unfoldr : Monad m => (s -> m (Either r (a, s))) -> s -> Stream (Of a) m r
unfoldr f = unfold $ \x => map from_pair <$> f x

||| analogous to `Data.Stream.iterate` but for `Stream (Of a)`
export
iterate : Monad m => (a -> a) -> a -> Stream (Of a) m r
iterate f = unfoldr $ \x => pure $ Right $ dup (f x)

||| analogous to `Data.Stream.repeat` but for `Stream (Of a)`
export
repeat : Monad m => a -> Stream (Of a) m r
repeat = iterate id

||| yield an element / analogous to `Prelude.singleton` but for `Stream (Of a)`
export
yield : Monad m => a -> Stream (Of a) m ()
yield x = Step (x :> Return ())

||| `Stream m m r` basically means that `Step`s and `Effect`s of the stream are the same thing, we still use `join` to collapse the entire `Stream`
export
run : Monad m => Stream m m r -> m r
run (Return x) = pure x
run (Effect x) = x >>= assert_total run
run (Step x) = x >>= assert_total run
run (Build g) = assert_total run (build g)

||| turns a `Stream` into a list
export
toList : Monad m => Stream (Of a) m r -> m (List a, r)
toList = destroy (\(a :> b) => map (mapFst (a ::)) b) join (\x => pure (Nil, x))

||| `toList` but discards the result
export
toList_ : Monad m => Stream (Of a) m r -> m (List a)
toList_ = destroy (\(a :> b) => map (a ::) b) join (const (pure Nil))

||| construct a `Stream` from a `List` with a result type
export
fromList : r -> List a -> Stream (Of a) m r
fromList r Nil = Return r
fromList r (a :: as) = Step (a :> fromList r as)

||| `fromList` but discards the result
export
fromList_ : List a -> Stream (Of a) m ()
fromList_ = fromList ()

||| cons an element into a `Stream (Of a)`
export
cons : a -> Stream (Of a) m r -> Stream (Of a) m r
cons x stream = Step (x :> stream)

||| essentially the "un" version fo `cons`
export
next : Monad m => Stream (Of a) m r -> m (Either r (a, Stream (Of a) m r))
next stream = case !(inspect stream) of
  Left r => pure (Left r)
  Right (x :> xs) => pure (Right (x, xs))

||| map `Step`s
export
mapf : (Functor f, Monad m) => (forall x. f x -> g x) -> Stream f m r -> Stream g m r
mapf f s = Build (\return, effect, step => fold return effect (step . f) s)

||| monadic version of `mapf`
export
mapfM : (Monad m, Functor f) => (forall x. f x -> m (g x)) -> Stream f m r -> Stream g m r
mapfM f stream = Build (\return, effect, step => fold return effect (effect . map step . f) stream)

||| map values in a `Stream (Of a)`
export
maps : Monad m => (a -> b) -> Stream (Of a) m r -> Stream (Of b) m r
maps f s = mapf (mapFst f) s

||| monadic version of `mapsM`
export
mapsM : Monad m => (a -> m b) -> Stream (Of a) m r -> Stream (Of b) m r
mapsM f s = mapfM (\(c :> g) => (:> g) <$> f c) s

||| replace each element of a stream with an associated `Stream`
export
traverse : (Monad m, Functor f) => (a -> Stream f m x) -> Stream (Of a) m r -> Stream f m r
traverse f = fold pure effect (\(x :> xs) => ignore (f x) >> xs)

||| `for = flip traverse`
export
for : (Monad m, Functor f) => Stream (Of a) m r -> (a -> Stream f m x) -> Stream f m r
for = flip traverse

export
mapM_ : Monad m => (a -> m b) -> Stream (Of a) m r -> m r
mapM_ f = fold pure join (\(x :> xs) => ignore (f x) >> xs)

export
scan : Functor m => (acc -> a -> acc) -> (acc -> b) -> acc -> Stream (Of a) m r -> Stream (Of b) m r
scan step done begin stream = Step (done begin :> loop begin stream)
  where
  loop : acc -> Stream (Of a) m r -> Stream (Of b) m r
  loop acc (Step (x :> xs)) = let acc = step acc x in Step (done acc :> loop acc xs)
  loop acc (Return r) = Return r
  loop acc (Effect m) = Effect (map (assert_total loop acc) m)
  loop acc (Build g) = loop acc (g Return effect wrap)

export
scanM : Monad m => (acc -> a -> m acc) -> (acc -> m b) -> m acc -> Stream (Of a) m r -> Stream (Of b) m r
scanM step done begin stream = Effect $ do
  begin <- begin
  x0 <- done begin
  pure $ Step (x0 :> loop begin stream)
  where
  loop : acc -> Stream (Of a) m r -> Stream (Of b) m r
  loop acc (Step (x :> xs)) = Effect $ do
    acc <- step acc x
    xn <- done acc
    pure $ Step (xn :> assert_total loop acc xs)
  loop acc (Return r) = Return r
  loop acc (Effect m) = Effect $ m >>= pure . assert_total loop acc
  loop acc (Build g) = loop acc (g pure effect wrap)


text:
module Common

import Data.String
import Data.List
import Data.List1

public export
Solution : Type
Solution = (input : String) -> Either String (String, String)

-- This maps over a list strings and performs some non-total conversion on them
-- if all lines are successful it returns the list of converted lines, if not
-- it retuns the index of the first error
export
processLines : (func : String -> Maybe a) -> String -> Either String (List a)
processLines func input = go (lines $ input) func (1, [])
  where
    go : List String -> (String -> Maybe a) -> (Nat, List a) -> Either String (List a)
    go [] func (count, acc) = Right (reverse acc)
    go [""] func (count, acc) = Right (reverse acc)  -- this might not be needed with the new 'lines' behaviour
    go (x :: xs) func (count, acc) =
      case (func x) of
         Just next => go xs func (S count, next :: acc)
         Nothing => Left $ "Error on Line: \{show count}\n"

export
linesToInts : String -> Either String (List Integer)
linesToInts = processLines parseInteger

export
decEither : String -> Dec a -> Either String a
decEither err (Yes a) = Right a
decEither err (No a) = Left err

infixl 4 !!
export
(!!) : List a -> Nat -> Maybe a
(!!) [] k = Nothing
(!!) (x :: xs) 0 = Just x
(!!) (x :: xs) (S k) = xs !! k

infixl 4 >|
export
(>|) : List a -> Integer -> Maybe a
(>|) [] x = Nothing
(>|) (y :: xs) x =
  case compare x 0 of
    EQ => Just y
    GT => xs >| (x - 1)
    LT => Nothing

-- Repeatedly applys a function until it converges
export
fixedPoint : Eq a => (a -> a) -> a -> a
fixedPoint f x =
  let y = f x in
  if y == x
     then x
     else fixedPoint f y

foldl' : (a -> a -> a) -> List a -> Maybe a
foldl' f [] = Nothing
foldl' f (x :: xs) = Just $ foldl f x xs

export
min : Ord a => List a -> Maybe a
min = foldl' Prelude.min

export
max : Ord a => List a -> Maybe a
max = foldl' Prelude.max


text:
import Data.Vect

readStringVector : IO (n ** Vect n String)
readStringVector = do
  elem <- getLine
  if elem == ""
     then pure (0 ** [])
     else do
       (restSize ** rest) <- readStringVector
       pure (S restSize ** elem :: rest)

zipInputs : IO (n ** Vect n (String, String))
zipInputs = do
  (len1 ** v1) <- readStringVector
  (len2 ** v2) <- readStringVector
  case exactLength len1 v2 of
       Nothing => putStrLn "Oh no! Bad lengths..." >>= const zipInputs
       (Just rightLenV2) => pure $ (len1 ** zip v1 rightLenV2)

readUntilBlank : IO (List String)
readUntilBlank = do
  elem <- getLine
  if elem == ""
     then pure []
     else do
       rest <- readUntilBlank
       pure (elem :: rest)

joinWithNewlines : List String -> String
joinWithNewlines [] = ""
joinWithNewlines (x :: xs) = x ++ "\n" ++ joinWithNewlines xs

readAndSave : IO ()
readAndSave = do
  content <- readUntilBlank
  name <- getLine
  Right () <- writeFile name (joinWithNewlines content)
    | Left fileError => printLn fileError
  pure ()

readVectFileHelper : File -> IO (n ** Vect n String)
readVectFileHelper file = do
  False <- fEOF file
    | True => pure (_ ** [])
  Right line <- fGetLine file
    | Left fileError => pure (_ ** [])
  (len ** rest) <- readVectFileHelper file
  pure (S len ** line :: rest)

readVectFile : IO (n ** Vect n String)
readVectFile = do
  -- Let's open the file
  Right file <- openFile "written.txt" Read
    | Left fileError => pure (_ ** [])
  readVectFileHelper file


text:
data MyNat = Zero | Succ MyNat

total mynat_plus : MyNat -> MyNat -> MyNat
mynat_plus Zero m = m
mynat_plus (Succ k) m = Succ (mynat_plus k m)

-- proving that 0 + a = a
total first_proof : (a: MyNat) -> mynat_plus Zero a = a
first_proof a = Refl

-- proving that there exists an x such that Succ x exists
-- we are basically constructing a dependent pair of (x, Succ x)
-- that is accomplished with the DPair type
total second_proof : MyNat -> DPair MyNat (\_ => MyNat)
second_proof x = MkDPair x (Succ x)

data MyLTE : MyNat -> MyNat -> Type where
  MyLTEZero : MyLTE Zero right
  MyLTESucc : MyLTE left right -> MyLTE (Succ left) (Succ right)

-- proving that a + 0 = a
-- using induction here
-- what we do it rewrite the induction hypothesis
total third_proof : (a: MyNat) -> mynat_plus a Zero = a
third_proof Zero = Refl
third_proof (Succ x) = rewrite (third_proof x) in Refl


text:
module Submodule.DepD

empty : ()
empty = ()

max_stars_repo_name: chrrasmussen/Idris-Deps

max_issues_repo_name: chrrasmussen/Idris-Deps

max_forks_repo_name: chrrasmussen/Idris-Deps


text:
module FreeQ2

%default total
%access public export

||| Type representing a query type which encodes a query _request_ (presumably a
||| GADT), paired with a handler for it. The handler's output type is
||| parameterized over a size to help smooth out totality proofs when used with
||| the free query. This makes us loose our functor instance, but we can still
||| define a concept of map.
record HandledQry (q : Type -> Type) (n : Nat) (o : Nat -> Type) where
  constructor HandleQry
  qry : q i
  handle : i -> o n

mapHQ : {n, m : Nat} -> (a n -> b m) -> HandledQry q n a -> HandledQry q m b
mapHQ f (HandleQry qry handle) = HandleQry qry (f . handle)

||| Since the standard Haskell-style Free monad is not strictly positive, and I
||| do not understand yet how to constrain a functor to be strictly positive;
||| nor do I understand Conor McBride's `General` free monad in
||| [Turing-Completeness Totally
||| Free](https://pdfs.semanticscholar.org/e291/5b546b9039a8cf8f28e0b814f6502630239f.pdf)
||| I define a FreeQ: a version of free that is monomorphic to the concept of a
||| handled query---that is, of a query GADT paired with a handler
||| function---but not monorphic to the specific query GADT. This definition is
||| then strictly positive. With the addition of a size to the type, the
||| consuming code is able to be total. Thus I am able to get one definition of
||| free for all my query DSLs, which is everywhere to date that I have
||| personally had a need for free monads, and yet maintain my dogmatism about
||| total programming. I don't doubt that sometime in the future I will have a
||| need for free monads with something that is not a query. But let the future
||| be the future. For now, it would be a tremendous step forward in my F# code
||| if I could use this approach!
data FreeQ : Nat -> (Type -> Type) -> Type -> Type where
  PureQ : a -> FreeQ Z q a
  BindHQ : HandledQry q n (\m => FreeQ m q a)
         -> FreeQ (S n) q a

||| Thankfully due to the nature of functor, we are ablel to implement the
||| interface, since it does not change the size of our FreeQ.
Functor (FreeQ n q) where
  map f (PureQ x) = PureQ (f x)
  map f (BindHQ slave) = BindHQ (mapHQ (map f) slave)

||| Recover applicative and monad instances by lifting... I mean half the point
||| of a free monad is to actually be able to use do notation etc. right?
record FreeQry (q : Type -> Type) a where
  constructor WrapFHQ
  unwrapFHQ : FreeQ qsize q a

Functor (FreeQry q) where
  map f (WrapFHQ x) = WrapFHQ $ map f x

||| Applicative apply, except we can't implement the type class because the size
||| of our type changes between inputs and output.
apfq : FreeQ n f (a -> b) -> FreeQ m f a -> FreeQ (n + m) f b
apfq {n=Z} (PureQ y) x = map y x
apfq (BindHQ y) x = BindHQ (mapHQ (flip apfq x) y)

Applicative (FreeQry q) where
  pure x = WrapFHQ (PureQ x)
  (WrapFHQ f) <*> (WrapFHQ x) = WrapFHQ $ apfq f x

||| Monad bind, except we can't implement the type class because the size of our
||| type changes between inputs and output.
bindfq : Functor f => (a -> FreeQ n f b) -> FreeQ m f a -> FreeQ (m + n) f b
bindfq {n} {m=Z} f (PureQ x) = f x
bindfq f (BindHQ x) = BindHQ (mapHQ (bindfq f) x)

||| Monad join, except we can't implement the type class because the size of our
||| type changes between inputs and output.
joinfq : Functor f => FreeQ n f (FreeQ m f a) -> FreeQ (n + m) f a
joinfq (PureQ x) = x
joinfq (BindHQ x) = BindHQ (mapHQ joinfq x)

join' : (n : Nat) -> FreeQ n q (FreeQry q a) -> FreeQry q a
join' Z (PureQ x) = x
join' (S m) (BindHQ x) =
  ?asdf $ map (join' m) x
  --WrapFHQ (S m) $ BindHQ $ map (unwrapFHQ . join' m) x

Monad (FreeQry q) where
  join (WrapFHQ n x) = join' n x


text:
module Data.Nat

import public Control.Relation
import public Control.Order

%default total

export
Uninhabited (Z = S n) where
  uninhabited Refl impossible

export
Uninhabited (S n = Z) where
  uninhabited Refl impossible

export
Uninhabited (a = b) => Uninhabited (S a = S b) where
  uninhabited Refl @{ab} = uninhabited @{ab} Refl

public export
isZero : Nat -> Bool
isZero Z     = True
isZero (S n) = False

public export
isSucc : Nat -> Bool
isSucc Z     = False
isSucc (S n) = True

public export
data IsSucc : (n : Nat) -> Type where
  ItIsSucc : IsSucc (S n)

export
Uninhabited (IsSucc Z) where
  uninhabited ItIsSucc impossible

public export
isItSucc : (n : Nat) -> Dec (IsSucc n)
isItSucc Z = No absurd
isItSucc (S n) = Yes ItIsSucc

public export
power : Nat -> Nat -> Nat
power base Z       = S Z
power base (S exp) = base * (power base exp)

public export
hyper : Nat -> Nat -> Nat -> Nat
hyper Z        a b      = S b
hyper (S Z)    a Z      = a
hyper (S(S Z)) a Z      = Z
hyper n        a Z      = S Z
hyper (S pn)   a (S pb) = hyper pn a (hyper (S pn) a pb)

public export
pred : Nat -> Nat
pred Z     = Z
pred (S n) = n

-- Comparisons

public export
data NotBothZero : (n, m : Nat) -> Type where
  LeftIsNotZero  : NotBothZero (S n) m
  RightIsNotZero : NotBothZero n     (S m)

export
Uninhabited (NotBothZero 0 0) where
  uninhabited LeftIsNotZero impossible
  uninhabited RightIsNotZero impossible

public export
data LTE  : (n, m : Nat) -> Type where
  LTEZero : LTE Z    right
  LTESucc : LTE left right -> LTE (S left) (S right)

export
Uninhabited (LTE (S n) Z) where
  uninhabited LTEZero impossible

export
Uninhabited (LTE m n) => Uninhabited (LTE (S m) (S n)) where
  uninhabited (LTESucc lte) = uninhabited lte

public export
Reflexive Nat LTE where
  reflexive {x = Z} = LTEZero
  reflexive {x = S k} = LTESucc $ reflexive {x = k}

public export
Transitive Nat LTE where
  transitive LTEZero _ = LTEZero
  transitive (LTESucc xy) (LTESucc yz) =
    LTESucc $ transitive {rel = LTE} xy yz

public export
Antisymmetric Nat LTE where
  antisymmetric LTEZero LTEZero = Refl
  antisymmetric (LTESucc xy) (LTESucc yx) =
    cong S $ antisymmetric xy yx

public export
Connex Nat LTE where
  connex {x = Z} _ = Left LTEZero
  connex {y = Z} _ = Right LTEZero
  connex {x = S _} {y = S _} prf =
    case connex {rel = LTE} $ prf . (cong S) of
      Left jk => Left $ LTESucc jk
      Right kj => Right $ LTESucc kj

public export
Preorder Nat LTE where

public export
PartialOrder Nat LTE where

public export
LinearOrder Nat LTE where

public export
GTE : Nat -> Nat -> Type
GTE left right = LTE right left

public export
LT : Nat -> Nat -> Type
LT left right = LTE (S left) right

namespace LT

  ||| LT is defined in terms of LTE which makes it annoying to use.
  ||| This convenient view of allows us to avoid having to constantly
  ||| perform nested matches to obtain another LT subproof instead of
  ||| an LTE one.
  public export
  data View : LT m n -> Type where
    LTZero : View (LTESucc LTEZero)
    LTSucc : (lt : m `LT` n) -> View (LTESucc lt)

  ||| Deconstruct an LT proof into either a base case or a further *LT*
  export
  view : (lt : LT m n) -> View lt
  view (LTESucc LTEZero) = LTZero
  view (LTESucc lt@(LTESucc _)) = LTSucc lt

  ||| A convenient alias for trivial LT proofs
  export
  ltZero : Z `LT` S m
  ltZero = LTESucc LTEZero

public export
GT : Nat -> Nat -> Type
GT left right = LT right left

export
succNotLTEzero : Not (LTE (S m) Z)
succNotLTEzero LTEZero impossible

export
fromLteSucc : LTE (S m) (S n) -> LTE m n
fromLteSucc (LTESucc x) = x

export
succNotLTEpred : {x : Nat} -> Not $ LTE (S x) x
succNotLTEpred {x =   0} prf = succNotLTEzero prf
succNotLTEpred {x = S _} prf = succNotLTEpred $ fromLteSucc prf

public export
isLTE : (m, n : Nat) -> Dec (LTE m n)
isLTE Z n = Yes LTEZero
isLTE (S k) Z = No succNotLTEzero
isLTE (S k) (S j)
    = case isLTE k j of
           No contra => No (contra . fromLteSucc)
           Yes prf => Yes (LTESucc prf)

public export
isGTE : (m, n : Nat) -> Dec (GTE m n)
isGTE m n = isLTE n m

public export
isLT : (m, n : Nat) -> Dec (LT m n)
isLT m n = isLTE (S m) n

public export
isGT : (m, n : Nat) -> Dec (GT m n)
isGT m n = isLT n m

export
lteSuccRight : LTE n m -> LTE n (S m)
lteSuccRight LTEZero     = LTEZero
lteSuccRight (LTESucc x) = LTESucc (lteSuccRight x)

export
lteSuccLeft : LTE (S n) m -> LTE n m
lteSuccLeft (LTESucc x) = lteSuccRight x

export
lteAddRight : (n : Nat) -> LTE n (n + m)
lteAddRight Z = LTEZero
lteAddRight (S k) {m} = LTESucc (lteAddRight {m} k)

export
notLTEImpliesGT : {a, b : Nat} -> Not (a `LTE` b) -> a `GT` b
notLTEImpliesGT {a = 0  }           not_z_lte_b    = absurd $ not_z_lte_b LTEZero
notLTEImpliesGT {a = S a} {b = 0  } notLTE = LTESucc LTEZero
notLTEImpliesGT {a = S a} {b = S k} notLTE = LTESucc (notLTEImpliesGT (notLTE . LTESucc))

export
LTEImpliesNotGT : a `LTE` b -> Not (a `GT` b)
LTEImpliesNotGT LTEZero q = absurd q
LTEImpliesNotGT (LTESucc p) (LTESucc q) = LTEImpliesNotGT p q

export
notLTImpliesGTE : {a, b : _} -> Not (LT a b) -> GTE a b
notLTImpliesGTE notLT = fromLteSucc $ notLTEImpliesGT notLT

export
LTImpliesNotGTE : a `LT` b -> Not (a `GTE` b)
LTImpliesNotGTE p q = LTEImpliesNotGT q p

public export
lte : Nat -> Nat -> Bool
lte Z        right     = True
lte left     Z         = False
lte (S left) (S right) = lte left right

public export
gte : Nat -> Nat -> Bool
gte left right = lte right left

public export
lt : Nat -> Nat -> Bool
lt left right = lte (S left) right

public export
gt : Nat -> Nat -> Bool
gt left right = lt right left

export
lteReflectsLTE : (k : Nat) -> (n : Nat) -> lte k n === True -> k `LTE` n
lteReflectsLTE (S k)  0    _ impossible
lteReflectsLTE 0      0    _   = LTEZero
lteReflectsLTE 0     (S k) _   = LTEZero
lteReflectsLTE (S k) (S j) prf = LTESucc (lteReflectsLTE k j prf)

export
gteReflectsGTE : (k : Nat) -> (n : Nat) -> gte k n === True -> k `GTE` n
gteReflectsGTE k n prf = lteReflectsLTE n k prf

export
ltReflectsLT : (k : Nat) -> (n : Nat) -> lt k n === True -> k `LT` n
ltReflectsLT k n prf = lteReflectsLTE (S k) n prf

export
gtReflectsGT : (k : Nat) -> (n : Nat) -> gt k n === True -> k `GT` n
gtReflectsGT k n prf = ltReflectsLT n k prf

public export
minimum : Nat -> Nat -> Nat
minimum Z m = Z
minimum (S n) Z = Z
minimum (S n) (S m) = S (minimum n m)

public export
maximum : Nat -> Nat -> Nat
maximum Z m = m
maximum (S n) Z = S n
maximum (S n) (S m) = S (maximum n m)

-- Proofs on S

export
eqSucc : (0 left, right : Nat) -> left = right -> S left = S right
eqSucc _ _ Refl = Refl

export
succInjective : (0 left, right : Nat) -> S left = S right -> left = right
succInjective _ _ Refl = Refl

||| A definition of non-zero with a better behaviour than `Not (x = Z)`
||| This is amenable to proof search and `NonZero Z` is more readily
||| detected as impossible by Idris
public export
data NonZero : Nat -> Type where
  SIsNonZero : NonZero (S x)

export Uninhabited (NonZero Z) where uninhabited SIsNonZero impossible

export
SIsNotZ : Not (S x = Z)
SIsNotZ = absurd

||| Auxiliary function:
||| mod' fuel a b = a `mod` (S b)
||| assuming we have enough fuel
public export
mod' : Nat -> Nat -> Nat -> Nat
mod' Z        centre right = centre
mod' (S fuel) centre right =
      if lte centre right then
        centre
      else
        mod' fuel (minus centre (S right)) right

public export
modNatNZ : Nat -> (y: Nat) -> (0 _ : NonZero y) -> Nat
modNatNZ left Z         p = void (absurd p)
modNatNZ left (S right) _ = mod' left left right

export partial
modNat : Nat -> Nat -> Nat
modNat left (S right) = modNatNZ left (S right) SIsNonZero

||| Auxiliary function:
||| div' fuel a b = a `div` (S b)
||| assuming we have enough fuel
public export
div' : Nat -> Nat -> Nat -> Nat
div' Z        centre right = Z
div' (S fuel) centre right =
  if lte centre right then
    Z
  else
    S (div' fuel (minus centre (S right)) right)

-- 'public' to allow type-level division
public export
divNatNZ : Nat -> (y: Nat) -> (0 _ : NonZero y) -> Nat
divNatNZ left (S right) _ = div' left left right

export partial
divNat : Nat -> Nat -> Nat
divNat left (S right) = divNatNZ left (S right) SIsNonZero

export partial
divCeilNZ : Nat -> (y: Nat) -> (0 _ : NonZero y) -> Nat
divCeilNZ x y p = case (modNatNZ x y p) of
  Z   => divNatNZ x y p
  S _ => S (divNatNZ x y p)

export partial
divCeil : Nat -> Nat -> Nat
divCeil x (S y) = divCeilNZ x (S y) SIsNonZero

public export
divmod' : Nat -> Nat -> Nat -> (Nat, Nat)
divmod' Z        centre right = (Z, centre)
divmod' (S fuel) centre right =
  if lte centre right then
    (Z, centre)
  else
    let qr = divmod' fuel (minus centre (S right)) right
    in (S (fst qr), snd qr)

public export
divmodNatNZ : Nat -> (y: Nat) -> (0 _ : NonZero y) -> (Nat, Nat)
divmodNatNZ left (S right) _ = divmod' left left right

public export
Integral Nat where
  div = divNat
  mod = modNat

export partial
gcd : (a: Nat) -> (b: Nat) -> {auto ok: NotBothZero a b} -> Nat
gcd a Z     = a
gcd Z b     = b
gcd a (S b) = gcd (S b) (modNatNZ a (S b) SIsNonZero)

export partial
lcm : Nat -> Nat -> Nat
lcm _ Z     = Z
lcm Z _     = Z
lcm a (S b) = divNat (a * (S b)) (gcd a (S b))

--------------------------------------------------------------------------------
-- An informative comparison view
--------------------------------------------------------------------------------
public export
data CmpNat : Nat -> Nat -> Type where
     CmpLT : (y : _) -> CmpNat x (x + S y)
     CmpEQ : CmpNat x x
     CmpGT : (x : _) -> CmpNat (y + S x) y

export
cmp : (x, y : Nat) -> CmpNat x y
cmp Z Z     = CmpEQ
cmp Z (S k) = CmpLT _
cmp (S k) Z = CmpGT _
cmp (S x) (S y) with (cmp x y)
  cmp (S x) (S (x + (S k))) | CmpLT k = CmpLT k
  cmp (S x) (S x)           | CmpEQ   = CmpEQ
  cmp (S (y + (S k))) (S y) | CmpGT k = CmpGT k

-- Proofs on +

export
plusZeroLeftNeutral : (right : Nat) -> 0 + right = right
plusZeroLeftNeutral _ = Refl

export
plusZeroRightNeutral : (left : Nat) -> left + 0 = left
plusZeroRightNeutral Z     = Refl
plusZeroRightNeutral (S n) = rewrite plusZeroRightNeutral n in Refl

export
plusSuccRightSucc : (left, right : Nat) -> S (left + right) = left + (S right)
plusSuccRightSucc Z _ = Refl
plusSuccRightSucc (S left) right = rewrite plusSuccRightSucc left right in Refl

export
plusCommutative : (left, right : Nat) -> left + right = right + left
plusCommutative Z right = rewrite plusZeroRightNeutral right in Refl
plusCommutative (S left) right =
  rewrite plusCommutative left right in
    rewrite plusSuccRightSucc right left in
      Refl

export
plusAssociative : (left, centre, right : Nat) ->
  left + (centre + right) = (left + centre) + right
plusAssociative Z _ _ = Refl
plusAssociative (S left) centre right =
    rewrite plusAssociative left centre right in Refl

export
plusConstantRight : (left, right, c : Nat) -> left = right ->
  left + c = right + c
plusConstantRight _ _ _ Refl = Refl

export
plusConstantLeft : (left, right, c : Nat) -> left = right ->
  c + left = c + right
plusConstantLeft _ _ _ Refl = Refl

export
plusOneSucc : (right : Nat) -> 1 + right = S right
plusOneSucc _ = Refl

export
plusLeftCancel : (left, right, right' : Nat) ->
  left + right = left + right' -> right = right'
plusLeftCancel Z _ _ p = p
plusLeftCancel (S left) right right' p =
    plusLeftCancel left right right' (succInjective _ _ p)

export
plusRightCancel : (left, left', right : Nat) ->
  left + right = left' + right -> left = left'
plusRightCancel left left' right p =
  plusLeftCancel right left left' $
    rewrite plusCommutative right left in
      rewrite plusCommutative right left' in
        p

export
plusLeftLeftRightZero : (left, right : Nat) ->
  left + right = left -> right = Z
plusLeftLeftRightZero left right p =
  plusLeftCancel left right Z $
    rewrite plusZeroRightNeutral left in
      p

export
plusLteMonotoneRight : (p, q, r : Nat) -> q `LTE` r -> (q+p) `LTE` (r+p)
plusLteMonotoneRight p  Z     r     LTEZero    = rewrite plusCommutative r p in
                                                 lteAddRight p
plusLteMonotoneRight p (S q) (S r) (LTESucc l) = LTESucc $ plusLteMonotoneRight p q r l

export
plusLteMonotoneLeft : (p, q, r : Nat) -> q `LTE` r -> (p + q) `LTE` (p + r)
plusLteMonotoneLeft p q r p_lt_q
   = rewrite plusCommutative p q in
     rewrite plusCommutative p r in
     plusLteMonotoneRight p q r p_lt_q

export
plusLteMonotone : {m, n, p, q : Nat} -> m `LTE` n -> p `LTE` q ->
                  (m + p) `LTE` (n + q)
plusLteMonotone left right =
  transitive {rel=LTE}
    (plusLteMonotoneLeft m p q right)
    (plusLteMonotoneRight q m n left)

zeroPlusLeftZero : (a,b : Nat) -> (0 = a + b) -> a = 0
zeroPlusLeftZero 0 0 Refl = Refl
zeroPlusLeftZero (S k) b _ impossible

zeroPlusRightZero : (a,b : Nat) -> (0 = a + b) -> b = 0
zeroPlusRightZero 0 0 Refl = Refl
zeroPlusRightZero (S k) b _ impossible

-- Proofs on *

export
multZeroLeftZero : (right : Nat) -> Z * right = Z
multZeroLeftZero _ = Refl

export
multZeroRightZero : (left : Nat) -> left * Z = Z
multZeroRightZero Z        = Refl
multZeroRightZero (S left) = multZeroRightZero left

export
multRightSuccPlus : (left, right : Nat) ->
  left * (S right) = left + (left * right)
multRightSuccPlus Z _ = Refl
multRightSuccPlus (S left) right =
  rewrite multRightSuccPlus left right in
  rewrite plusAssociative left right (left * right) in
  rewrite plusAssociative right left (left * right) in
  rewrite plusCommutative right left in
          Refl

export
multLeftSuccPlus : (left, right : Nat) ->
  (S left) * right = right + (left * right)
multLeftSuccPlus _ _ = Refl

export
multCommutative : (left, right : Nat) -> left * right = right * left
multCommutative Z right = rewrite multZeroRightZero right in Refl
multCommutative (S left) right =
  rewrite multCommutative left right in
  rewrite multRightSuccPlus right left in
          Refl

export
multDistributesOverPlusLeft : (left, centre, right : Nat) ->
  (left + centre) * right = (left * right) + (centre * right)
multDistributesOverPlusLeft Z _ _ = Refl
multDistributesOverPlusLeft (S k) centre right =
  rewrite multDistributesOverPlusLeft k centre right in
    rewrite plusAssociative right (k * right) (centre * right) in
      Refl

export
multDistributesOverPlusRight : (left, centre, right : Nat) ->
  left * (centre + right) = (left * centre) + (left * right)
multDistributesOverPlusRight left centre right =
  rewrite multCommutative left (centre + right) in
    rewrite multCommutative left centre in
      rewrite multCommutative left right in
  multDistributesOverPlusLeft centre right left

export
multAssociative : (left, centre, right : Nat) ->
  left * (centre * right) = (left * centre) * right
multAssociative Z _ _ = Refl
multAssociative (S left) centre right =
  rewrite multAssociative left centre right in
    rewrite multDistributesOverPlusLeft centre (mult left centre) right in
      Refl

export
multOneLeftNeutral : (right : Nat) -> 1 * right = right
multOneLeftNeutral right = plusZeroRightNeutral right

export
multOneRightNeutral : (left : Nat) -> left * 1 = left
multOneRightNeutral left =
  rewrite multCommutative left 1 in
  multOneLeftNeutral left

-- Proofs on minus

export
minusSuccSucc : (left, right : Nat) ->
  minus (S left) (S right) = minus left right
minusSuccSucc _ _ = Refl

export
minusZeroLeft : (right : Nat) -> minus 0 right = Z
minusZeroLeft _ = Refl

export
minusZeroRight : (left : Nat) -> minus left 0 = left
minusZeroRight Z     = Refl
minusZeroRight (S _) = Refl

export
minusZeroN : (n : Nat) -> Z = minus n n
minusZeroN Z     = Refl
minusZeroN (S n) = minusZeroN n

export
minusOneSuccN : (n : Nat) -> S Z = minus (S n) n
minusOneSuccN Z     = Refl
minusOneSuccN (S n) = minusOneSuccN n

export
minusSuccOne : (n : Nat) -> minus (S n) 1 = n
minusSuccOne Z     = Refl
minusSuccOne (S _) = Refl

export
minusPlusZero : (n, m : Nat) -> minus n (n + m) = Z
minusPlusZero Z     _ = Refl
minusPlusZero (S n) m = minusPlusZero n m

export
minusPos : m `LT` n -> Z `LT` minus n m
minusPos lt = case view lt of
  LTZero    => ltZero
  LTSucc lt => minusPos lt

export
minusLteMonotone : {p : Nat} -> m `LTE` n -> minus m p `LTE` minus n p
minusLteMonotone LTEZero = LTEZero
minusLteMonotone {p = Z} prf@(LTESucc _) = prf
minusLteMonotone {p = S p} (LTESucc lte) = minusLteMonotone lte

export
minusLtMonotone : m `LT` n -> p `LT` n -> minus m p `LT` minus n p
minusLtMonotone mltn pltn = case view pltn of
  LTZero => rewrite minusZeroRight m in mltn
  LTSucc pltn => case view mltn of
    LTZero => minusPos pltn
    LTSucc mltn => minusLtMonotone mltn pltn

public export
minusPlus : (m : Nat) -> minus (plus m n) m === n
minusPlus Z = irrelevantEq (minusZeroRight n)
minusPlus (S m) = minusPlus m

export
plusMinusLte : (n, m : Nat) -> LTE n m -> (minus m n) + n = m
plusMinusLte  Z     m    _   = rewrite minusZeroRight m in
                               plusZeroRightNeutral m
plusMinusLte (S _)  Z    lte = absurd lte
plusMinusLte (S n) (S m) lte = rewrite sym $ plusSuccRightSucc (minus m n) n in
                               cong S $ plusMinusLte n m (fromLteSucc lte)

export
minusMinusMinusPlus : (left, centre, right : Nat) ->
  minus (minus left centre) right = minus left (centre + right)
minusMinusMinusPlus Z Z _ = Refl
minusMinusMinusPlus (S _) Z _ = Refl
minusMinusMinusPlus Z (S _) _ = Refl
minusMinusMinusPlus (S left) (S centre) right =
  rewrite minusMinusMinusPlus left centre right in Refl

export
plusMinusLeftCancel : (left, right : Nat) -> (right' : Nat) ->
  minus (left + right) (left + right') = minus right right'
plusMinusLeftCancel Z _ _ = Refl
plusMinusLeftCancel (S left) right right' =
  rewrite plusMinusLeftCancel left right right' in Refl

export
multDistributesOverMinusLeft : (left, centre, right : Nat) ->
  (minus left centre) * right = minus (left * right) (centre * right)
multDistributesOverMinusLeft Z Z _ = Refl
multDistributesOverMinusLeft (S left) Z right =
  rewrite minusZeroRight (right + (left * right)) in Refl
multDistributesOverMinusLeft Z (S _) _ = Refl
multDistributesOverMinusLeft (S left) (S centre) right =
  rewrite multDistributesOverMinusLeft left centre right in
  rewrite plusMinusLeftCancel right (left * right) (centre * right) in
          Refl

export
multDistributesOverMinusRight : (left, centre, right : Nat) ->
  left * (minus centre right) = minus (left * centre) (left * right)
multDistributesOverMinusRight left centre right =
    rewrite multCommutative left (minus centre right) in
    rewrite multDistributesOverMinusLeft centre right left in
    rewrite multCommutative centre left in
    rewrite multCommutative right left in
            Refl

export
zeroMultEitherZero : (a,b : Nat) -> a*b = 0 -> Either (a = 0) (b = 0)
zeroMultEitherZero 0 b prf = Left Refl
zeroMultEitherZero (S a) b prf = Right $ zeroPlusLeftZero b (a * b) (sym prf)

-- power proofs

-- multPowerPowerPlus : (base, exp, exp' : Nat) ->
--   power base (exp + exp') = (power base exp) * (power base exp')
-- multPowerPowerPlus base Z       exp' =
--     rewrite sym $ plusZeroRightNeutral (power base exp') in Refl
-- multPowerPowerPlus base (S exp) exp' =
--   rewrite multPowerPowerPlus base exp exp' in
--     rewrite sym $ multAssociative base (power base exp) (power base exp') in
--       Refl

--powerOneNeutral : (base : Nat) -> power base 1 = base
--powerOneNeutral base = rewrite multCommutative base 1 in multOneLeftNeutral base
--
--powerOneSuccOne : (exp : Nat) -> power 1 exp = 1
--powerOneSuccOne Z       = Refl
--powerOneSuccOne (S exp) = rewrite powerOneSuccOne exp in Refl
--
--powerPowerMultPower : (base, exp, exp' : Nat) ->
--  power (power base exp) exp' = power base (exp * exp')
--powerPowerMultPower _ exp Z = rewrite multZeroRightZero exp in Refl
--powerPowerMultPower base exp (S exp') =
--  rewrite powerPowerMultPower base exp exp' in
--  rewrite multRightSuccPlus exp exp' in
--  rewrite sym $ multPowerPowerPlus base exp (exp * exp') in
--          Refl

-- minimum / maximum proofs

export
maximumAssociative : (l, c, r : Nat) ->
  maximum l (maximum c r) = maximum (maximum l c) r
maximumAssociative Z _ _ = Refl
maximumAssociative (S _) Z _ = Refl
maximumAssociative (S _) (S _) Z = Refl
maximumAssociative (S k) (S j) (S i) = rewrite maximumAssociative k j i in Refl

export
maximumCommutative : (l, r : Nat) -> maximum l r = maximum r l
maximumCommutative Z Z = Refl
maximumCommutative Z (S _) = Refl
maximumCommutative (S _) Z = Refl
maximumCommutative (S k) (S j) = rewrite maximumCommutative k j in Refl

export
maximumIdempotent : (n : Nat) -> maximum n n = n
maximumIdempotent Z = Refl
maximumIdempotent (S k) = cong S $ maximumIdempotent k

export
minimumAssociative : (l, c, r : Nat) ->
  minimum l (minimum c r) = minimum (minimum l c) r
minimumAssociative Z _ _ = Refl
minimumAssociative (S _) Z _ = Refl
minimumAssociative (S _) (S _) Z = Refl
minimumAssociative (S k) (S j) (S i) = rewrite minimumAssociative k j i in Refl

export
minimumCommutative : (l, r : Nat) -> minimum l r = minimum r l
minimumCommutative Z Z = Refl
minimumCommutative Z (S _) = Refl
minimumCommutative (S _) Z = Refl
minimumCommutative (S k) (S j) = rewrite minimumCommutative k j in Refl

export
minimumIdempotent : (n : Nat) -> minimum n n = n
minimumIdempotent Z = Refl
minimumIdempotent (S k) = cong S $ minimumIdempotent k

export
minimumZeroZeroLeft : (left : Nat) -> minimum left 0 = Z
minimumZeroZeroLeft left = rewrite minimumCommutative left 0 in Refl

export
minimumSuccSucc : (left, right : Nat) ->
  minimum (S left) (S right) = S (minimum left right)
minimumSuccSucc _ _ = Refl

export
maximumZeroNLeft : (left : Nat) -> maximum left Z = left
maximumZeroNLeft left = rewrite maximumCommutative left Z in Refl

export
maximumSuccSucc : (left, right : Nat) ->
  S (maximum left right) = maximum (S left) (S right)
maximumSuccSucc _ _ = Refl

export
sucMaxL : (l : Nat) -> maximum (S l) l = (S l)
sucMaxL Z = Refl
sucMaxL (S l) = cong S $ sucMaxL l

export
sucMaxR : (l : Nat) -> maximum l (S l) = (S l)
sucMaxR Z = Refl
sucMaxR (S l) = cong S $ sucMaxR l

export
sucMinL : (l : Nat) -> minimum (S l) l = l
sucMinL Z = Refl
sucMinL (S l) = cong S $ sucMinL l

export
sucMinR : (l : Nat) -> minimum l (S l) = l
sucMinR Z = Refl
sucMinR (S l) = cong S $ sucMinR l

-- Algebra -----------------------------

namespace Semigroup

  public export
  [Maximum] Semigroup Nat where
    (<+>) = max

  public export
  [Minimum] Semigroup Nat where
    (<+>) = min

namespace Monoid

  public export
  [Maximum] Monoid Nat using Semigroup.Maximum where
    neutral = 0


text:
data Vect : Nat -> Type -> Type where
    Nil : Vect Z a
    (::) : a-> Vect k a-> Vect (S k) a

(++) : Vect n a -> Vect m a -> Vect (n+m) a
(++) Nil ys =ys
(++) (x::xs) ys = x :: xs ++ ys

data Fin : Nat -> Type where
    FZ : Fin (S k)
    FS : Fin k  -> Fin (S k)

index : Fin n -> Vect n a -> a
index FZ (x::xs) = x
index (FS k) (x::xs) = index k xs

isEmpty : Vect n a -> Bool
isEmpty {n=Z} _ = True
isEmpty {n=S k} _ = False

1::(2::(3::Nil)) : Vect 3 Integer

max_stars_repo_name: shij-hsu/idr

max_issues_repo_name: shij-hsu/idr

max_forks_repo_name: shij-hsu/idr


text:
module Transducers.Algorithms

import Control.Monad.State
import Transducers.Core

--------------------------------------------------------------------------------
-- Basic Transducers (stateless)
--------------------------------------------------------------------------------

export
mapping : (a -> b) -> Transducer acc s s a b
mapping fn = statelessTransducer $ \next, acc, outer => next acc (fn outer)

export
filtering : (a -> Bool) -> Transducer acc s s a a
filtering pf = statelessTransducer $
  \next, acc, a =>
    if pf a
      then next acc a
      else pure (Continue acc)

export
catMapping : (Foldable t) => (a -> t b) -> Transducer acc s s a b
catMapping fn = statelessTransducer $
  \next, acc, a => runSteps next acc (fn a)

export
takingWhile : (a -> Bool) -> Transducer acc s s a a
takingWhile p = statelessTransducer $
  \next, acc, a => do
    if p a
      then next acc a
      else pure (Done acc)

--------------------------------------------------------------------------------
-- Basic Transducers (stateful)
--------------------------------------------------------------------------------

export
dropping : Nat -> Transducer acc s (Nat, s) a a
dropping n = statefulTransducer n dropImpl
  where
    dropImpl next (S n, acc) _ = pure $ Continue (n, acc)
    dropImpl next (Z, acc) a = withState Z <$> next acc a

export
taking : Nat -> Transducer acc s (Nat, s) a a
taking n = statefulTransducer n takeImpl
  where
    takeImpl next (Z, acc) a = pure (Done (Z, acc))
    takeImpl next (n, acc) a = withState (pred n) <$> next acc a

export
interspersing : a -> Transducer acc s (Bool, s) a a
interspersing separator = statefulTransducer False stepImpl
  where
    stepImpl next (False, acc) a = withState True <$> next acc a
    stepImpl next (True, acc) a =
      withState True <$> runSteps next acc [separator, a]

export
indexingFrom : Int -> Transducer acc s (Int, s) a (Int, a)
indexingFrom startIndex = statefulTransducer startIndex stepImpl
  where
    stepImpl next (n, acc) a = withState (succ n) <$> next acc (n, a)

export
indexing : Transducer acc s (Int, s) a (Int, a)
indexing = indexingFrom 0

export
chunksOf : Nat -> Transducer acc s (List a, s) a (List a)
chunksOf chunkSize = makeTransducer [] nextChunk dumpRemaining
  where
    nextChunk next (remaining, acc) a =
      let remaining' = a :: remaining in
      if length remaining' == chunkSize
        then withState [] <$> next acc (reverse remaining')
        else pure $ Continue (remaining', acc)
    dumpRemaining next remaining acc =
      if isNil remaining
        then pure acc
        else unStatus <$> next acc (reverse remaining)

export
deduplicate : (Eq a) => Transducer acc s (Maybe a, s) a a
deduplicate = statefulTransducer Nothing stepImpl
  where
    stepImpl next (oldVal, acc) a =
      if oldVal == Just a
        then pure $ Continue (oldVal, acc)
        else withState (Just a) <$> next acc a

export
groupingBy : (a -> a -> Bool) -> Transducer acc s (List a, s) a (List a)
groupingBy sameGroup = makeTransducer [] stepImpl dumpRemaining
  where
    stepImpl next (previousVals, acc) a =
      case nonEmpty previousVals of
        No _ => pure $ Continue ([a], acc)
        Yes _ => if sameGroup (head previousVals) a -- Maintain stable order
          then pure $ Continue (a :: previousVals, acc)
          else withState [a] <$> next acc (reverse previousVals)
    dumpRemaining next remaining acc =
      if isNil remaining
        then pure acc
        else unStatus <$> next acc (reverse remaining)

--------------------------------------------------------------------------------
-- Higher order transducers
--------------------------------------------------------------------------------

public export
record Iso a b where
  constructor MkIso
  toIso : a -> b
  fromIso : b -> a

export
under : Iso a b -> Transducer acc s1 s2 b b -> Transducer acc s1 s2 a a
under iso xf = mapping (toIso iso) . xf . mapping (fromIso iso)

max_stars_repo_name: QuentinDuval/IdrisReducers

max_issues_repo_name: QuentinDuval/IdrisReducers

max_forks_repo_name: QuentinDuval/IdrisReducers


text:
{- Ctrl-Alt-A: Add definition
   Ctrl-Alt-C: Case split
   Ctrl-Alt-D: Documentation
   Ctrl-Alt-L: Lift hole: Lifts a hole to the top level as a new function definition
   Ctrl-Alt-M: Match: Replaces a hole with a case expression that matches on an intermediate result
   Ctrl-Alt-R: Reloads and typechecks the current buffer
   Ctrl-Alt-S: Search
   Ctrl-Alt-T: Type-check: Displays the type under cursor -}
module Main

import Data.Vect

infixr 5 .+.

data Schema
  = SString
  | SInt
  | (.+.) Schema Schema

SchemaType : Schema -> Type
SchemaType SString = String
SchemaType SInt = Int
SchemaType (x .+. y) = (SchemaType x, SchemaType y)

record DataStore where
  constructor MkData
  schema : Schema
  size : Nat
  items : Vect size (SchemaType schema)

addToStore : (store : DataStore) -> SchemaType (schema store) -> DataStore
addToStore (MkData sch s i) n = MkData sch _ (addToData i)
  where
    addToData : Vect old (SchemaType sch) -> Vect (S old) (SchemaType sch)
    addToData [] = [n]
    addToData (i :: is) = i :: addToData is

data Command : Schema -> Type where
  SetSchema : (newschema : Schema) -> Command schema
  Add : SchemaType schema -> Command schema
  Get : Integer -> Command schema
  Quit : Command schema

parsePrefix : (sch : Schema) -> String -> Maybe (SchemaType sch, String)
parsePrefix SString x = getQuoted (unpack x)
  where
    getQuoted : List Char -> Maybe (String, String)
    getQuoted ('"' :: xs) = case span (/= '"') xs of
      (qouted, '"' :: rest) => Just (pack qouted, ltrim (pack rest))
      _                     => Nothing
    getQuoted _ = Nothing
parsePrefix SInt x = case span isDigit x of
  ("", rest) => Nothing
  (num, rest) => Just (cast num, ltrim rest)
parsePrefix (y .+. z) x = case parsePrefix y x of
  Nothing => Nothing
  Just (lval, x') => case parsePrefix z x' of
    Nothing => Nothing
    Just (rval, x'') => Just ((lval, rval), x'')

parseBySchema : (sch : Schema) -> (str : String) -> Maybe (SchemaType sch)
parseBySchema sch inp = case parsePrefix sch inp of
  Just (res, "") => Just res
  Just _ => Nothing
  Nothing => Nothing

parseSchema : List String -> Maybe Schema
parseSchema ("String" :: xs) = case xs of
  [] => Just SString
  _ => case parseSchema xs of
    Nothing  => Nothing
    Just xsh => Just (SString .+. xsh)
parseSchema ("Int" :: xs) = case xs of
  [] => Just SInt
  _ => case parseSchema xs of
    Nothing  => Nothing
    Just xsh => Just (SInt .+. xsh)
parseSchema _ = Nothing

parseCommand : (schema : Schema) -> (cmd : String) -> (args : String) -> Maybe (Command schema)
parseCommand sch "add" str    = case parseBySchema sch str of
                                  Nothing => Nothing
                                  Just ok => Just (Add ok)
parseCommand sch "get" val    = case all isDigit (unpack val) of
                                  False => Nothing
                                  True  => Just (Get (cast val))
parseCommand sch "quit" ""    = Just Quit
parseCommand sch "schema" rest = case parseSchema (words rest) of
  Nothing => Nothing
  Just sok => Just (SetSchema sok)
parseCommand _   _      _     = Nothing

setSchema : (store : DataStore) -> Schema -> Maybe DataStore
setSchema s sc = case size s of
  Z => Just (MkData sc _ [])
  S _ => Nothing

parse : (schema : Schema) -> (input : String) -> Maybe (Command schema)
parse sch input = case span (/= ' ') input of
  (cmd, args) => parseCommand sch cmd (ltrim args)

display : SchemaType schema -> String
display {schema = SString} item = item
display {schema = SInt} item = cast item
display {schema = (x .+. y)} (a, b) = display a ++ ", " ++ display b

getEntry : (pos : Integer) -> (store : DataStore) -> Maybe (String, DataStore)
getEntry pos store =
  let store_items = items store
  in case integerToFin pos (size store) of
    Nothing => Just ("Out of range\n", store)
    Just ix => Just (display (index ix store_items) ++ "\n", store)

getSize : (store : DataStore) -> Maybe (String, DataStore)
getSize store = Just ("Size of store: " ++ cast (size store), store)

processInput : DataStore -> String -> Maybe (String, DataStore)
processInput store inp = case parse (schema store) inp of
  Nothing           => Just ("Invalid command\n", store)
  Just (SetSchema sc) => case setSchema store sc of
                          Nothing => Just ("Can't update schema\n", store)
                          Just st => Just ("OK\n", st)
  Just (Add item)   => Just ("ID " ++ show (size store) ++ "\n", addToStore store item)
  Just (Get pos)    => getEntry pos store
  Just Quit         => Nothing

main : IO ()
main = replWith (MkData SString _ []) "Command: " processInput

max_stars_repo_name: pdani/idris-grin

max_issues_repo_name: pdani/idris-grin

max_forks_repo_name: pdani/idris-grin


text:
||| Position and geometry of Hexagonal grid system
||| https://www.redblobgames.com/grids/hexagons/
module Bautzen.Pos

import Data.Nat
import Data.Nat.DivMod
import Data.Nat.Parity
import Data.ZZ

import public Data.ZZ.Extra
import Data.Maybe.Extra

-- Positions & Map

||| A position/hex of the game board encoded as a pair of `Nat`
||| with bounds
public export
data Pos : Type where
  Hex : (col : Nat) -> (row : Nat)
      -> { auto cbound : LTE col 22 }
      -> { auto rbound : LTE row 12 }
      -> Pos

public export
Eq Pos where
  (==) (Hex col row) (Hex col' row') = col == col' && row == row'

public export
Show Pos where
  show (Hex c r) = show2Digits c ++ show2Digits r
    where
      show2Digits : Nat -> String
      show2Digits n =
        if n < 9
        then "0" ++ show (n + 1)
        else show (n + 1)

public export
Ord Pos where
  compare (Hex col row) (Hex col' row') =
    case compare col col' of
      LT => LT
      EQ => compare row row'
      GT => GT

||| Cube coordinates.
||| Cube coordinates stem from the observation a 2-D hexagonal grid is equivalent
||| to a diagonal "slice" of a 3-D cubic grid. Using cubic coordinates makes it
||| much easier to compute geometric values.
||| We only store the `x` (column) and `z` (depth) coordinates instead
||| of a triple as the `y` dimension can be simply recovered as `-x -z`.
public export
data Cube : Type where
  MkCube : (x : ZZ) -> (z : ZZ) -> Cube

||| Compute the L1 distance between 2 `Cube`s
||| see [Red Blob Games](https://www.redblobgames.com/grids/hexagons/#distances-cube) page
||| for details on the (pretty cool) algorithm.
public export
cubeDistance : Cube -> Cube -> Nat
cubeDistance (MkCube x z) (MkCube x' z') =
  let y  = negate x - z
      y' = negate x' - z'
  in max (max (absZ (x - x')) (absZ (y - y'))) (absZ (z - z'))

public export
posToCube : Pos -> Cube
posToCube (Hex col row) =
  let x = cast col
      sign = if odd col then 1 else 0
      z = cast row - divZZNZ (x - sign) 2 {z = PosSIsNotZ }
  in MkCube x z

public export
distance : Pos -> Pos -> Nat
distance x y =
  let c1 = posToCube x
      c2 = posToCube y
  in cubeDistance c1 c2

public export
data Mvmt : Type where
  Dec : Mvmt
  Neut : Mvmt
  Inc : Mvmt

public export
succNotLTEZ : Not (LTE (S m) Z)
succNotLTEZ LTEZero impossible

public export
fromLTESucc : LTE (S m) (S n) -> LTE m n
fromLTESucc (LTESucc x) = x

public export
lteSuccR : LTE n m -> LTE n (S m)
lteSuccR LTEZero     = LTEZero
lteSuccR (LTESucc x) = LTESucc (lteSuccR x)

public export
lteSuccL : LTE (S n) m -> LTE n m
lteSuccL (LTESucc x) = lteSuccR x

public export
isLte : (m, n : Nat) -> Dec (LTE m n)
isLte Z n = Yes LTEZero
isLte (S k) Z = No succNotLTEZ
isLte (S k) (S j)
    = case isLte k j of
           No contra => No (contra . fromLTESucc)
           Yes prf => Yes (LTESucc prf)

public export
shiftPos : (x : Nat) -> {bound : Nat} -> (prf : LTE x bound) -> Mvmt -> Maybe (n : Nat ** LTE n bound)
shiftPos Z prf Dec = Nothing
shiftPos (S k) prf Dec = Just (k ** lteSuccL prf)
shiftPos x prf Neut = Just (x ** prf)
shiftPos x prf Inc {bound} with (isLte (S x) bound)
  shiftPos x prf Inc | (Yes y) = Just (S x ** y)
  shiftPos x prf Inc | (No contra) = Nothing

public export
makePos : (pos : Pos) -> (Mvmt, Mvmt) -> Maybe Pos
makePos (Hex col row {cbound} {rbound} ) (a, b) = do
  (c' ** p1) <- shiftPos col cbound a
  (r' ** p2) <- shiftPos row rbound b
  pure $ Hex c' r' {cbound = p1} {rbound = p2}

public export
oddShifts : List (Mvmt, Mvmt)
oddShifts = [ (Dec, Neut)
            , (Neut, Dec)
            , (Inc, Neut)
            , (Inc, Inc)
            , (Neut, Inc)
            , (Dec, Inc)
            ]

public export
evenShifts : List (Mvmt, Mvmt)
evenShifts = [ (Dec, Dec)
            , (Neut, Dec)
            , (Inc, Dec)
            , (Inc, Neut)
            , (Neut, Inc)
            , (Dec, Neut)
            ]

||| Compute the neighbours of a given position
||| There are at most 6 neighbours, with side and corner hexes having of
||| course less.
public export
neighbours : (pos : Pos) -> List Pos
neighbours (Hex col row) with (col `divMod` (S Z))
  neighbours (Hex col@(Z + (q * (S(S Z)))) row)     | (MkDivMod q Z remainderSmall) = catMaybes $ map (makePos (Hex col row)) evenShifts
  neighbours (Hex col@((S Z) + (q * (S(S Z)))) row) | (MkDivMod q (S Z) remainderSmall) = catMaybes $ map (makePos (Hex col row)) oddShifts
  neighbours (Hex ((S (S r)) + (q * (S(S Z)))) _)   | (MkDivMod q (S (S r)) LTEZero) impossible
  neighbours (Hex ((S (S r)) + (q * (S(S Z)))) _)   | (MkDivMod q (S (S r)) (LTESucc lte)) = absurd $ succNotLTEZ (fromLTESucc lte)

namespace PosTest

  neighbours1_test : (neighbours (Hex 3 3) = [ Hex 2 3, Hex 3 2, Hex 4 3, Hex 4 4, Hex 3 4, Hex 2 4] )
  neighbours1_test = Refl

  neighbours_test : (neighbours (Hex 2 2) = [ Hex 1 1, Hex 2 1, Hex 3 1, Hex 3 2, Hex 2 3, Hex 1 2] )
  neighbours_test = Refl

  -- distance_to_odd_neighbours_is_1 : map (distance (Hex 3 2)) (neighbours (Hex 3 2)) = [ 1, 1, 1, 1, 1, 1 ]
  -- distance_to_odd_neighbours_is_1 = Refl

  -- distance_to_even_neighbours_is_1 : map (distance (Hex 2 2)) (neighbours (Hex 2 2)) = [ 1, 1, 1, 1, 1, 1 ]
  -- distance_to_even_neighbours_is_1 = Refl

  -- distance_test : distance (Hex 3 2) (Hex 4 4) = 2
  -- distance_test = Refl

max_stars_repo_name: steshaw/hsgames

max_issues_repo_name: steshaw/hsgames

max_forks_repo_name: steshaw/hsgames


text:
{-| A custom prelude -}
module Eth.Prelude

import Prelude
import Prelude.Bool -- using (bool)
import Data.List -- using (intercalate)
import Prelude.Monad -- using ((>=>))
import public Control.Monad.Identity -- using
import Control.Monad.Writer -- using
--  (MonadWriter, WriterT, Writer, execWriterT, execWriter, tell)
import Control.Monad.Reader -- using
--  (MonadReader, ReaderT, Reader, runReaderT, runReader, ask, local)

infixl 6 <>

export
isNullStr : String -> Bool
isNullStr = (== neutral)

export
(<>) : Monoid m => m -> m -> m
(<>) = (<+>)

export
bool : a -> a -> Bool -> a
bool x y b = case b of
  True => x
  False => y

export
execWriterT : Functor m => WriterT w m a -> m w
execWriterT = map snd . runWriterT

-- works : WriterT w (ReaderT r Identity) _ -> ReaderT r Identity w
-- works = execWriterT @{ }

doesnt : WriterT w (Reader r) _ -> Reader r w
doesnt = execWriterT
  -- using ReaderTFunctor

export
execWriter : Writer w a -> w
execWriter = runIdentity . execWriterT

export
runReader : Reader r a -> r -> a
runReader m = runIdentity . runReaderT m

-- M : Type -> Type -> Type -> Type
-- M w r a = WriterT w (Reader r) a

-- unM : M w r a -> w -> r -> a
-- unM = ?foo

max_stars_repo_name: fredefox/ethambda-idr

max_issues_repo_name: fredefox/ethambda-idr

max_forks_repo_name: fredefox/ethambda-idr


text:
import System.FFI

pfn : String -> String
pfn fn = "C:" ++ fn ++ ",libstruct"

Point : Type
Point = Struct "point" [("x", Int), ("y", Int)]

NamedPoint : Type
NamedPoint = Struct "namedpoint" [("name", Ptr String), ("pt", Point)]

%foreign (pfn "getString")
getStr : Ptr String -> String

%foreign (pfn "mkPoint")
mkPoint : Int -> Int -> Point

%foreign (pfn "freePoint")
freePoint : Point -> PrimIO ()

%foreign (pfn "mkNamedPoint")
mkNamedPoint : String -> Point -> PrimIO NamedPoint

%foreign (pfn "freeNamedPoint")
freeNamedPoint : NamedPoint -> PrimIO ()

showPoint : Point -> String
showPoint pt
    = let x : Int = getField pt "x"
          y : Int = getField pt "y" in
          show (x, y)

showNamedPoint : NamedPoint -> String
showNamedPoint pt
    = let x : String = getStr (getField pt "name")
          p : Point = getField pt "pt" in
          show x ++ ": " ++ showPoint p

main : IO ()
main = do let pt = mkPoint 20 30
          np <- primIO $ mkNamedPoint "Here" pt
          setField pt "x" (the Int 40)
          putStrLn $ showPoint pt
          putStrLn $ showNamedPoint np

          primIO $ freeNamedPoint np
          primIO $ freePoint pt

max_stars_repo_name: boxfire/rapid

max_issues_repo_name: boxfire/rapid

max_forks_repo_name: boxfire/rapid


text:
module PQ.FFI

import Control.Monad.Either
import Data.SOP
import PQ.Types

--------------------------------------------------------------------------------
--          Foreign Types
--------------------------------------------------------------------------------

public export
data PGConnection : Type where

public export
data PGResult : Type where

public export
Connection : Type
Connection = Ptr PGConnection

public export
Result : Type
Result = Ptr PGResult

--------------------------------------------------------------------------------
--          FFI
--------------------------------------------------------------------------------

pq : String -> String
pq s = #"C:\#{s},libpq"#

%foreign pq "PQconnectdb"
prim__connect : String -> PrimIO Connection

%foreign pq "PQstatus"
prim__status : Connection -> PrimIO Bits8

%foreign pq "PQerrorMessage"
prim__errorMessage : Connection -> PrimIO String

%foreign pq "PQfinish"
prim__finish : Connection -> PrimIO ()

%foreign pq "PQexec"
prim__exec : Connection -> String -> PrimIO Result

%foreign pq "PQntuples"
prim__ntuples : Result -> PrimIO Bits32

%foreign pq "PQnfields"
prim__nfields : Result -> PrimIO Bits32

%foreign pq "PQresultStatus"
prim__resultStatus : Result -> PrimIO Bits8

%foreign pq "PQresultErrorMessage"
prim__resultErrorMsg : Result -> PrimIO String

%foreign pq "PQclear"
prim__clear : Result -> PrimIO ()

%foreign pq "PQgetvalue"
prim__getValue : Result -> Bits32 -> Bits32 -> PrimIO String

--------------------------------------------------------------------------------
--          Low level API
--------------------------------------------------------------------------------

export
status : HasIO io => Connection -> io ConnStatusType
status c = fromBits8 <$> primIO (prim__status c)

export
finish : HasIO io => Connection -> io ()
finish c = primIO $ prim__finish c

export
connect : HasIO io => MonadError SQLError io => String -> io Connection
connect s = do
  c <- primIO (prim__connect s)
  BAD <- status c
    | _ => pure c
  msg <- primIO (prim__errorMessage c)
  finish c
  throwError $ ConnectionError BAD msg

export
resultStatus : HasIO io => Result -> io ExecStatusType
resultStatus r = fromBits8 <$> primIO (prim__resultStatus r)

export
resultErrorMsg : HasIO io => Result -> io String
resultErrorMsg r = primIO (prim__resultErrorMsg r)

export
clear : HasIO io => Result -> io ()
clear r = primIO $ prim__clear r

export
exec :  HasIO io
     => MonadError SQLError io
     => Connection
     -> String
     -> ExecStatusType
     -> io Result
exec c s est = do
  res <- primIO (prim__exec c s)
  st  <- resultStatus res
  if st == est
     then pure res
     else do
       msg <- resultErrorMsg res
       clear res
       throwError $ ExecError st msg

export
exec_ :  HasIO io
      => MonadError SQLError io
      => Connection
      -> String
      -> ExecStatusType
      -> io ()
exec_ c s est = exec c s est >>= clear

export
ntuples : HasIO io => Result -> io Bits32
ntuples r = primIO $ prim__ntuples r

export
nfields : HasIO io => Result -> io Bits32
nfields r = primIO $ prim__nfields r

ptrToString : Ptr String -> Maybe String
ptrToString ptr =
  if prim__nullPtr ptr == 1
     then Nothing
     else Just (believe_me ptr)

export
getValue : HasIO io => Result -> Bits32 -> Bits32 -> io String
getValue r row col = primIO $ prim__getValue r row col

--------------------------------------------------------------------------------
--          SOP
--------------------------------------------------------------------------------

getVal :  HasIO io
       => MonadError SQLError io
       => Result
       -> (row  : Bits32)
       -> (name : String)
       -> (col  : Bits32)
       -> (read : String -> Maybe t)
       -> io t
getVal res row name col read = do
  s <- getValue res row col
  case read s of
    Just t => pure t
    Nothing => throwError $ ReadError name row col s

getRow :  {0 ts : List Type}
       -> HasIO io
       => MonadError SQLError io
       => NP (K String) ts
       -> NP (K Bits32) ts
       -> NP (\t => String -> Maybe t) ts
       -> Result
       -> (row : Bits32)
       -> io (NP I ts)
getRow names columns readers res row =
  sequenceNP $ hliftA3 (getVal res row) names columns readers

export
getRows :  {0 ts : List Type}
        -> HasIO io
        => MonadError SQLError io
        => NP (K String) ts
        -> NP (\t => String -> Maybe t) ts
        -> Result
        -> io (List $ NP I ts)
getRows names readers res =
  let fieldCount = cast {to = Bits32} . length $ collapseNP names
      indices    = the (NP (K Bits32) ts) $ iterateNP names (+1) 0
   in do
      nt <- ntuples res
      if nt == 0
         then pure []
         else do
           nf <- nfields res
           if nf == fieldCount
              then traverse (getRow names indices readers res) [0 .. nt - 1]
              else throwError $ QueryError fieldCount nf


text:
module Parser.Support

import public Text.Lexer
import public Text.Parser
import Text.PrettyPrint.Prettyprinter
import Text.PrettyPrint.Prettyprinter.Util

import Core.TT
import Data.List
import Data.List.Views
import Data.Strings
import Parser.Unlit
import System.File

%default total

public export
data ParseError tok
  = ParseFail String (Maybe (Int, Int)) (List tok)
  | LexFail   (Int, Int, String)
  | FileFail  FileError
  | LitFail   LiterateError

export
Show tok => Show (ParseError tok) where
  show (ParseFail err loc toks)
      = "Parse error: " ++ err ++ " (next tokens: "
            ++ show (take 10 toks) ++ ")"
  show (LexFail (c, l, str))
      = "Lex error at " ++ show (c, l) ++ " input: " ++ str
  show (FileFail err)
      = "File error: " ++ show err
  show (LitFail (MkLitErr l c str))
      = "Lit error(s) at " ++ show (c, l) ++ " input: " ++ str

export
Pretty tok => Pretty (ParseError tok) where
  pretty (ParseFail err loc toks)
      = reflow "Parse error" <+> prettyLine loc <+> ":" <+> line <+> pretty err <++> parens (reflow "next tokens:"
            <++> brackets (align $ concatWith (surround (comma <+> space)) (pretty <$> take 10 toks)))
    where
      prettyLine : Maybe (Int, Int) -> Doc ann
      prettyLine Nothing = emptyDoc
      prettyLine (Just (r, c)) = space <+> "at" <++> "line" <++> pretty (r + 1) <+> ":" <+> pretty (c + 1)
  pretty (LexFail (c, l, str))
      = reflow "Lex error at" <++> pretty (c, l) <++> pretty "input:" <++> pretty str
  pretty (FileFail err)
      = reflow "File error:" <++> pretty (show err)
  pretty (LitFail (MkLitErr l c str))
      = reflow "Lit error(s) at" <++> pretty (c, l) <++> pretty "input:" <++> pretty str

export
toGenericParsingError : ParsingError token -> ParseError token
toGenericParsingError (Error err [])      = ParseFail err Nothing []
toGenericParsingError (Error err (t::ts)) = ParseFail err (Just (t.startLine, t.startCol)) (map val (t :: ts))

export
hex : Char -> Maybe Int
hex '0' = Just 0
hex '1' = Just 1
hex '2' = Just 2
hex '3' = Just 3
hex '4' = Just 4
hex '5' = Just 5
hex '6' = Just 6
hex '7' = Just 7
hex '8' = Just 8
hex '9' = Just 9
hex 'a' = Just 10
hex 'b' = Just 11
hex 'c' = Just 12
hex 'd' = Just 13
hex 'e' = Just 14
hex 'f' = Just 15
hex _ = Nothing

export
dec : Char -> Maybe Int
dec '0' = Just 0
dec '1' = Just 1
dec '2' = Just 2
dec '3' = Just 3
dec '4' = Just 4
dec '5' = Just 5
dec '6' = Just 6
dec '7' = Just 7
dec '8' = Just 8
dec '9' = Just 9
dec _ = Nothing

export
oct : Char -> Maybe Int
oct '0' = Just 0
oct '1' = Just 1
oct '2' = Just 2
oct '3' = Just 3
oct '4' = Just 4
oct '5' = Just 5
oct '6' = Just 6
oct '7' = Just 7
oct _ = Nothing

export
getEsc : String -> Maybe Char
getEsc "NUL" = Just '\NUL'
getEsc "SOH" = Just '\SOH'
getEsc "STX" = Just '\STX'
getEsc "ETX" = Just '\ETX'
getEsc "EOT" = Just '\EOT'
getEsc "ENQ" = Just '\ENQ'
getEsc "ACK" = Just '\ACK'
getEsc "BEL" = Just '\BEL'
getEsc "BS" = Just '\BS'
getEsc "HT" = Just '\HT'
getEsc "LF" = Just '\LF'
getEsc "VT" = Just '\VT'
getEsc "FF" = Just '\FF'
getEsc "CR" = Just '\CR'
getEsc "SO" = Just '\SO'
getEsc "SI" = Just '\SI'
getEsc "DLE" = Just '\DLE'
getEsc "DC1" = Just '\DC1'
getEsc "DC2" = Just '\DC2'
getEsc "DC3" = Just '\DC3'
getEsc "DC4" = Just '\DC4'
getEsc "NAK" = Just '\NAK'
getEsc "SYN" = Just '\SYN'
getEsc "ETB" = Just '\ETB'
getEsc "CAN" = Just '\CAN'
getEsc "EM" = Just '\EM'
getEsc "SUB" = Just '\SUB'
getEsc "ESC" = Just '\ESC'
getEsc "FS" = Just '\FS'
getEsc "GS" = Just '\GS'
getEsc "RS" = Just '\RS'
getEsc "US" = Just '\US'
getEsc "SP" = Just '\SP'
getEsc "DEL" = Just '\DEL'
getEsc str = Nothing

escape' : List Char -> Maybe (List Char)
escape' [] = pure []
escape' ('\\' :: '\\' :: xs) = pure $ '\\' :: !(escape' xs)
escape' ('\\' :: '&' :: xs) = pure !(escape' xs)
escape' ('\\' :: 'a' :: xs) = pure $ '\a' :: !(escape' xs)
escape' ('\\' :: 'b' :: xs) = pure $ '\b' :: !(escape' xs)
escape' ('\\' :: 'f' :: xs) = pure $ '\f' :: !(escape' xs)
escape' ('\\' :: 'n' :: xs) = pure $ '\n' :: !(escape' xs)
escape' ('\\' :: 'r' :: xs) = pure $ '\r' :: !(escape' xs)
escape' ('\\' :: 't' :: xs) = pure $ '\t' :: !(escape' xs)
escape' ('\\' :: 'v' :: xs) = pure $ '\v' :: !(escape' xs)
escape' ('\\' :: '\'' :: xs) = pure $ '\'' :: !(escape' xs)
escape' ('\\' :: '\"' :: xs) = pure $ '\"' :: !(escape' xs)
escape' ('\\' :: 'x' :: xs)
    = case span isHexDigit xs of
           ([], rest) => assert_total (escape' rest)
           (ds, rest) => pure $ cast !(toHex 1 (reverse ds)) ::
                                 !(assert_total (escape' rest))
  where
    toHex : Int -> List Char -> Maybe Int
    toHex _ [] = Just 0
    toHex m (d :: ds)
        = pure $ !(hex (toLower d)) * m + !(toHex (m*16) ds)
escape' ('\\' :: 'o' :: xs)
    = case span isOctDigit xs of
           ([], rest) => assert_total (escape' rest)
           (ds, rest) => pure $ cast !(toOct 1 (reverse ds)) ::
                                 !(assert_total (escape' rest))
  where
    toOct : Int -> List Char -> Maybe Int
    toOct _ [] = Just 0
    toOct m (d :: ds)
        = pure $ !(oct (toLower d)) * m + !(toOct (m*8) ds)
escape' ('\\' :: xs)
    = case span isDigit xs of
           ([], (a :: b :: c :: rest)) =>
               case getEsc (fastPack (the (List _) [a, b, c])) of
                   Just v => Just (v :: !(assert_total (escape' rest)))
                   Nothing => case getEsc (fastPack (the (List _) [a, b])) of
                                   Just v => Just (v :: !(assert_total (escape' (c :: rest))))
                                   Nothing => escape' xs
           ([], (a :: b :: [])) =>
               case getEsc (fastPack (the (List _) [a, b])) of
                   Just v => Just (v :: [])
                   Nothing => escape' xs
           ([], rest) => assert_total (escape' rest)
           (ds, rest) => Just $ cast (cast {to=Int} (fastPack ds)) ::
                                 !(assert_total (escape' rest))
escape' (x :: xs) = Just $ x :: !(escape' xs)

export
escape : String -> Maybe String
escape x = pure $ fastPack !(escape' (unpack x))

export
getCharLit : String -> Maybe Char
getCharLit str
   = do e <- escape str
        if length e == 1
           then Just (assert_total (prim__strHead e))
           else if length e == 0 -- parsed the NULL character that terminated the string!
                   then Just '\0000'
                   else Nothing


text:
module Python.Exceptions

import Python.Objects
import Python.Fields
import Python.IO

%default total
%access public export

Exception : Signature
Exception f = case f of
  "message" => Attr String
  _ => Object f

||| Standard Python exceptions.
data ExceptionType : Type where
  StopIteration : ExceptionType
  StandardError : ExceptionType
  BufferError : ExceptionType
  ArithmeticError : ExceptionType
  FloatingPointError : ExceptionType
  OverflowError : ExceptionType
  ZeroDivisionError : ExceptionType
  AssertionError : ExceptionType
  AttributeError : ExceptionType
  EnvironmentError : ExceptionType
  IOError : ExceptionType
  OSError : ExceptionType
  WindowsError : ExceptionType
  VMSError : ExceptionType
  EOFError : ExceptionType
  ImportError : ExceptionType
  LookupError : ExceptionType
  IndexError : ExceptionType
  KeyError : ExceptionType
  MemoryError : ExceptionType
  NameError : ExceptionType
  UnboundLocalError : ExceptionType
  ReferenceError : ExceptionType
  RuntimeError : ExceptionType
  NotImplementedError : ExceptionType
  SyntaxError : ExceptionType
  IndentationError : ExceptionType
  TabError : ExceptionType
  SystemError : ExceptionType
  TypeError : ExceptionType
  ValueError : ExceptionType
  UnicodeError : ExceptionType
  UnicodeDecodeError : ExceptionType
  UnicodeEncodeError : ExceptionType
  UnicodeTranslateError : ExceptionType
  Other : String -> ExceptionType

private
fromString : String -> ExceptionType
fromString s = case s of
  "StopIteration" => StopIteration
  "StandardError" => StandardError
  "BufferError" => BufferError
  "ArithmeticError" => ArithmeticError
  "FloatingPointError" => FloatingPointError
  "OverflowError" => OverflowError
  "ZeroDivisionError" => ZeroDivisionError
  "AssertionError" => AssertionError
  "AttributeError" => AttributeError
  "EnvironmentError" => EnvironmentError
  "IOError" => IOError
  "OSError" => OSError
  "WindowsError" => WindowsError
  "VMSError" => VMSError
  "EOFError" => EOFError
  "ImportError" => ImportError
  "LookupError" => LookupError
  "IndexError" => IndexError
  "KeyError" => KeyError
  "MemoryError" => MemoryError
  "NameError" => NameError
  "UnboundLocalError" => UnboundLocalError
  "ReferenceError" => ReferenceError
  "RuntimeError" => RuntimeError
  "NotImplementedError" => NotImplementedError
  "SyntaxError" => SyntaxError
  "IndentationError" => IndentationError
  "TabError" => TabError
  "SystemError" => SystemError
  "TypeError" => TypeError
  "ValueError" => ValueError
  "UnicodeError" => UnicodeError
  "UnicodeDecodeError" => UnicodeDecodeError
  "UnicodeEncodeError" => UnicodeEncodeError
  "UnicodeTranslateError" => UnicodeTranslateError
  other => Other other

||| Result of try-catch.
data Result : Type -> Type where
  ||| No exception was raised, `PIO` action was performed normally.
  OK : (x : a) -> Result a

  ||| An exception was raised.
  Except : (etype : ExceptionType) -> (e : Obj Exception) -> Result a

||| Catch exceptions in the given PIO action.
export
try : PIO a -> PIO (Result a)
try {a = a} x = do
    MkRaw r <- foreign
      FFI_Py
      "_idris_try"
      (Raw (PIO a)
        -> (Obj Exception -> Raw (Either (Obj Exception) a))
        -> (Raw a -> Raw (Either (Obj Exception) a))
        -> PIO (Raw $ Either (Obj Exception) a)
      )
      (MkRaw x)
      (MkRaw . Left)
      (MkRaw . Right . unRaw)

    case r of
      Right x => pure $ OK x
      Left e => do
        let et = e /. "__class__" /. "__name__"
        pure $ Except (fromString et) e

export
raise : Obj Exception -> PIO a
raise {a = a} e = unRaw <$> foreign FFI_Py "_idris_raise" (Obj Exception -> PIO (Raw a)) e

catch : PIO (Result a) -> (ExceptionType -> Obj Exception -> PIO a) -> PIO a
catch action handler = do
  OK result <- action
    | Except etype e => handler etype e
  pure result

||| Get basic information about the exception as `String`.
export
showException : Obj Exception -> String
showException e =
  unsafePerformIO
    $ foreign FFI_Py "str" (Obj Exception -> PIO String) e

{-
instance Show (Obj Exception) where
  show = showException
-}

max_stars_repo_name: ziman/idris-py

max_issues_repo_name: ziman/idris-py

max_forks_repo_name: ziman/idris-py


text:
module Types

--data Example: Type where
--  Points: Double -> Double -> Example
public export
data Examples = Points Double Double
--data Dataset = TrainingSet [Example] | TestSet [Example]
public export
data Dataset : Type where
  TrainingSet: List Examples -> Dataset
  TestSet: List Examples -> Dataset

public export
data Coefficients = Val Double Double

example1 : Examples
example1 = Points 10.2 10.9

example2 : Examples
example2 = Points 0.0 0.0

example3 : Examples
example3 = Points 2.8 4.9

mytrainset: Dataset
mytrainset = TrainingSet [example1,example2, example3]

max_stars_repo_name: nunet-io/ai-dsl

max_issues_repo_name: nunet-io/ai-dsl

max_forks_repo_name: nunet-io/ai-dsl


text:
module Language.Reflection

import public Language.Reflection.TT
import public Language.Reflection.TTImp

%default total

||| Elaboration scripts
||| Where types/terms are returned, binders will have unique, if not
||| necessarily human readabe, names
export
data Elab : Type -> Type where
     Pure : a -> Elab a
     Bind : Elab a -> (a -> Elab b) -> Elab b
     Fail : FC -> String -> Elab a

     LogMsg : String -> Nat -> String -> Elab ()
     LogTerm : String -> Nat -> String -> TTImp -> Elab ()

     -- Elaborate a TTImp term to a concrete value
     Check : TTImp -> Elab expected
     -- Quote a concrete expression back to a TTImp
     Quote : (0 _ : val) -> Elab TTImp

     -- Elaborate under a lambda
     Lambda : (0 x : Type) ->
              {0 ty : x -> Type} ->
              ((val : x) -> Elab (ty val)) -> Elab ((val : x) -> (ty val))

     -- Get the current goal type, if known
     -- (it might need to be inferred from the solution)
     Goal : Elab (Maybe TTImp)
     -- Get the names of local variables in scope
     LocalVars : Elab (List Name)
     -- Generate a new unique name, based on the given string
     GenSym : String -> Elab Name
     -- Put a name in the current namespace
     InCurrentNS : Name -> Elab Name
     -- Get the types of every name which matches.
     -- There may be ambiguities - returns a list of fully explicit names
     -- and their types. If there's no results, the name is undefined.
     GetType : Name -> Elab (List (Name, TTImp))
     -- Get the type of a local variable
     GetLocalType : Name -> Elab TTImp
     -- Get the constructors of a data type. The name must be fully resolved.
     GetCons : Name -> Elab (List Name)
     -- Check a group of top level declarations
     Declare : List Decl -> Elab ()

export
Functor Elab where
  map f e = Bind e $ Pure . f

export
Applicative Elab where
  pure = Pure
  f <*> a = Bind f (<$> a)

export
Monad Elab where
  (>>=) = Bind

||| Report an error in elaboration
export
fail : String -> Elab a
fail = Fail EmptyFC

export
failAt : FC -> String -> Elab a
failAt = Fail

||| Write a log message, if the log level is >= the given level
export
logMsg : String -> Nat -> String -> Elab ()
logMsg = LogMsg

||| Write a log message and a rendered term, if the log level is >= the given level
export
logTerm : String -> Nat -> String -> TTImp -> Elab ()
logTerm = LogTerm

||| Log the current goal type, if the log level is >= the given level
export
logGoal : String -> Nat -> String -> Elab ()
logGoal str n msg
    = do g <- Goal
         case g of
              Nothing => pure ()
              Just t => logTerm str n msg t

||| Check that some TTImp syntax has the expected type
||| Returns the type checked value
export
check : TTImp -> Elab expected
check = Check

||| Return TTImp syntax of a given value
export
quote : (0 _ : val) -> Elab TTImp
quote = Quote

||| Build a lambda expression
export
lambda : (0 x : Type) ->
         {0 ty : x -> Type} ->
         ((val : x) -> Elab (ty val)) -> Elab ((val : x) -> (ty val))
lambda = Lambda

||| Get the goal type of the current elaboration
export
goal : Elab (Maybe TTImp)
goal = Goal

||| Get the names of the local variables in scope
export
localVars : Elab (List Name)
localVars = LocalVars

||| Generate a new unique name
export
genSym : String -> Elab Name
genSym = GenSym

||| Given a name, return the name decorated with the current namespace
export
inCurrentNS : Name -> Elab Name
inCurrentNS = InCurrentNS

||| Given a possibly ambiguous name, get all the matching names and their types
export
getType : Name -> Elab (List (Name, TTImp))
getType = GetType

||| Get the type of a local variable
export
getLocalType : Name -> Elab TTImp
getLocalType = GetLocalType

||| Get the constructors of a fully qualified data type name
export
getCons : Name -> Elab (List Name)
getCons = GetCons

||| Make some top level declarations
export
declare : List Decl -> Elab ()
declare = Declare


text:
-- ------------------------------------------------------------- [ Forward.idr ]
-- Module    : Forward.idr
-- Copyright : (c) Jan de Muijnck-Hughes
-- License   : see LICENSE
-- --------------------------------------------------------------------- [ EOH ]

module GRL.Eval.Forward

import Data.AVL.Dict
import Data.AVL.Graph
import Data.Stack
import Data.Queue
import Data.Vect

import GRL.Common
import GRL.Model

import GRL.Eval.Qualitative
import GRL.Eval.Strategy
import GRL.Eval.Common

%default partial
%access private

-- ----------------------------------------------------- [ Forward Propagation ]

private
getSat' : NodeID -> GModel -> Maybe SValue
getSat' id g =
  case getValueByID id g of
    Nothing => Nothing
    Just v  => getSValue v

calcDecomp : NodeID -> GModel -> Maybe SValue
calcDecomp id g =
    case getValueByID id g of
      Nothing  => Nothing
      Just val =>
        case getStructTy val of
          Nothing   => Nothing
          Just dval =>
            case dval of
              ANDty => Just $ getDecompAnd csat
              XORty => Just $ getDecompXOR csat
              IORty => Just $ getDecompIOR csat
  where
    children : List NodeID
    children = map fst $ getDeCompEdges id g

    csat : List SValue
    csat = catMaybes $ map (\x => getSat' x g) children

getWeightedContrib : NodeID -> CValue -> GModel -> Maybe SValue
getWeightedContrib id y g = case getSat' id g of
  Nothing => Nothing
  Just x  => Just $ weightedContrib x y

calcWeightedContrib : DemiEdge GoalEdge -> GModel -> Maybe SValue
calcWeightedContrib (id, Just (Contribution x))  g = getWeightedContrib id x g
calcWeightedContrib (id, Just (Correlation  x))  g = getWeightedContrib id x g
calcWeightedContrib _                            _ = Nothing

calcContrib : Maybe SValue -> NodeID -> GModel -> SValue
calcContrib dval id g =
    if (noUndec count > 0)
      then UNDECIDED
      else combineContribs count
  where
    children : List (DemiEdge GoalEdge)
    children = getIntentEdges id g

    wsat : List SValue
    wsat = catMaybes $ map (\e => calcWeightedContrib e g) children

    vals : List SValue
    vals = case dval of {Nothing => wsat; Just x  => x :: wsat}

    count : ContribCount
    count = adjustCounts vals

evalElem : NodeID -> GModel -> SValue
evalElem e g = calcContrib dVal e g
  where
    dVal : Maybe SValue
    dVal = (calcDecomp e g)

-- -------------------------------------------------------------- [ Init Check ]

validityCheck : GModel -> Bool
validityCheck g = allLeafsValid && not gTy
  where
    allLeafsValid : Bool
    allLeafsValid = and $ map (\x => isJust (getSValue x)) (getValuesByID (leafNodes g) g)

    gTy : Bool
    gTy = isDisconnected g

initGraph : GModel -> GModel
initGraph g = foldl (doUp) g (leaves)
  where
    leaves : List GoalNode
    leaves = map (\x => if isJust (getSValue x) then x else record {getSValue = Just NONE} x) (getValuesByID (leafNodes g) g)

    doUp : GModel -> GoalNode -> GModel
    doUp m n = updateGoalNode (\x => getNodeTitle n == getNodeTitle x)
                              (\x => n)
                              m

-- ------------------------------------------------------- [ Forward Algorithm ]

partial
export
doEval : GModel -> (Queue NodeID) -> GModel
doEval g q =
    case popQ' q of
      Nothing        => g
      Just (c, newQ) => --  TODO
        case getValueByID c g of --- if node doesn't exist
          Nothing => g
          Just c' =>
            if isJust $ getSValue c' --- if satisfied then move on
              then doEval g newQ
              else let cs = children c in
                if isNil cs --- if leaf node
                  then g
                  else do
                    if and $ map (\x => isJust $ getSValue x) cs
                      then doEval (newG c) newQ
                      else doEval g        (pushQ c newQ)
  where
    childrenIDs : NodeID -> List (DemiEdge GoalEdge)
    childrenIDs n = (getEdgesByID n g)

    children : NodeID -> List GoalNode
    children n = getValuesByID (map fst $ childrenIDs n) g

    newG : NodeID -> GModel
    newG n = updateNodeValueByIDUsing
                   n
                   (\x => record {getSValue = Just (evalElem n g)} x)
                   g

private
partial
runEval : GModel -> EvalResult
runEval g =
    if validityCheck g
        then Result (vertices (doEval g (defQueue g)))
        else let newG = getNewG g in
             let theQ = defQueue newG in
          if validityCheck newG
            then Result (vertices (doEval newG theQ))
            else BadModel
  where
    getNewG : GModel -> GModel
    getNewG m = initGraph m

    defQueue : GModel -> Queue NodeID
    defQueue m = (pushQThings (verticesID m) mkQueue)

||| Evaluate a model with or without a given strategy.
|||
||| This function will deploy the strategy if it is given. Using this
||| code with a predeployed strategy may give unexpected results.
partial
export
forwardEval : Maybe Strategy -> GModel -> EvalResult
forwardEval Nothing  g = runEval g
forwardEval (Just s) g = runEval $ fst (deployStrategy g s)
-- --------------------------------------------------------------------- [ EOF ]

max_stars_repo_name: jfdm/idris-grl

max_issues_repo_name: jfdm/idris-grl

max_forks_repo_name: jfdm/idris-grl