text:
------------------------------------------------------------------------
-- This module is based on the following papers:

-- Categories of Containers
-- Abbott, Altenkirch, Ghani

-- Derivatives of Containers
-- Abbott, Altenkirch, Ghani, McBride
------------------------------------------------------------------------

module Data.Container

import Data.Either
import Decidable.Equality

%default total

------------------------------------------------------------------------
-- Container and their morphisms
-- * Extension is a functor from Container to Type

-- Objects of the category of containers
namespace Container

  public export
  record Container where
    constructor MkContainer
    Shape : Type
    Position : Shape -> Type

  public export
  record Extension (c : Container) (x : Type) where
    constructor MkExtension
    shape    : Shape c
    payloads : Position c shape -> x

  ||| The image of a container by @Extension@ is a functor
  public export
  Functor (Extension c) where map f (MkExtension s p) = MkExtension s (f . p)

-- Morphisms of the category of containers
namespace Morphism

  public export
  record Morphism (c, d : Container) where
    constructor MkMorphism
    shapeMorphism : Shape c -> Shape d
    positionMorphism : {s : Shape c} -> Position d (shapeMorphism s) -> Position c s

  public export
  Extension : Morphism c d -> Extension c x -> Extension d x
  Extension phi (MkExtension s p)
    = MkExtension (shapeMorphism phi s) (p . positionMorphism phi)

------------------------------------------------------------------------
-- Combinators to build containers

namespace Combinators

  -- Constant
  public export
  Const : Type -> Container
  Const k = MkContainer k (const Void)

  export
  toConst : k -> Extension (Const k) x
  toConst v = MkExtension v absurd

  export
  fromConst : Extension (Const k) x -> k
  fromConst (MkExtension v _) = v

  -- Identity
  public export
  Identity : Container
  Identity = MkContainer () (\ () => ())

  export
  toIdentity : x -> Extension Identity x
  toIdentity v = MkExtension () (const v)

  export
  fromIdentity : Extension Identity x -> x
  fromIdentity (MkExtension () chld) = chld ()

  -- Composition
  public export
  Compose : (d, c : Container) -> Container
  Compose d c = MkContainer
    (Extension d (Shape c))
    (\ (MkExtension shp chld) => (p : Position d shp ** Position c (chld p)))

  export
  toCompose : (Extension d . Extension c) x -> Extension (Compose d c) x
  toCompose (MkExtension shp1 chld)
    = MkExtension (MkExtension shp1 (shape . chld)) (\ (p ** q) => payloads (chld p) q)

  export
  fromCompose : Extension (Compose d c) x -> (Extension d . Extension c) x
  fromCompose (MkExtension (MkExtension shp1 shp2) chld)
    = MkExtension shp1 (\ p => MkExtension (shp2 p) (\ q => chld (p ** q)))

  -- Direct sum
  public export
  Sum : (c, d : Container) -> Container
  Sum c d = MkContainer (Either (Shape c) (Shape d)) (either (Position c) (Position d))

  export
  toSum : Either (Extension c x) (Extension d x) -> Extension (Sum c d) x
  toSum (Left (MkExtension shp chld)) = MkExtension (Left shp) chld
  toSum (Right (MkExtension shp chld)) = MkExtension (Right shp) chld

  export
  fromSum : Extension (Sum c d) x -> Either (Extension c x) (Extension d x)
  fromSum (MkExtension (Left shp) chld) = Left (MkExtension shp chld)
  fromSum (MkExtension (Right shp) chld) = Right (MkExtension shp chld)

  -- Pairing
  public export
  Pair : (c, d : Container) -> Container
  Pair c d = MkContainer (Shape c, Shape d) (\ (p, q) => Either (Position c p) (Position d q))

  export
  toPair : (Extension c x, Extension d x) -> Extension (Pair c d) x
  toPair (MkExtension shp1 chld1, MkExtension shp2 chld2)
    = MkExtension (shp1, shp2) (either chld1 chld2)

  export
  fromPair : Extension (Pair c d) x -> (Extension c x, Extension d x)
  fromPair (MkExtension (shp1, shp2) chld)
    = (MkExtension shp1 (chld . Left), MkExtension shp2 (chld . Right))

  -- Branching over a Type
  public export
  Exponential : Type -> Container -> Container
  Exponential k c = MkContainer (k -> Shape c) (\ p => (v : k ** Position c (p v)))

  export
  toExponential : (k -> Extension c x) -> Extension (Exponential k c) x
  toExponential f = MkExtension (shape . f) (\ (v ** p) => payloads (f v) p)

  export
  fromExponential : Extension (Exponential k c) x -> (k -> Extension c x)
  fromExponential (MkExtension  shp chld) k = MkExtension (shp k) (\ p => chld (k ** p))

------------------------------------------------------------------------
-- Taking various fixpoints of containers

namespace Initial

  public export
  data W : Container -> Type where
    MkW : Extension c (W c) -> W c

  export
  map : Morphism c d -> W c -> W d
  map f (MkW (MkExtension shp chld)) = MkW $ Extension f (MkExtension shp (\ p => map f (chld p)))
  --  Container.map inlined because of -------------------^
  --  termination checking

  export
  foldr : (Extension c x -> x) -> W c -> x
  foldr alg (MkW (MkExtension shp chld)) = alg (MkExtension shp (\ p => foldr alg (chld p)))

  export
  para : (Extension c (x, W c) -> x) -> W c -> x
  para alg (MkW (MkExtension shp chld)) = alg (MkExtension shp (\ p => let w = chld p in (para alg w, w)))

namespace Monad

  ||| @Free@ is a wrapper around @W@ to make it inference friendly.
  ||| Without this wrapper, neither @pure@ nor @bind@ are able to infer their @c@ argument.
  public export
  record Free (c : Container) (x : Type) where
    constructor MkFree
    runFree : W (Sum c (Const x))

  export
  pure : x -> Free c x
  pure x = MkFree $ MkW (toSum (Right (toConst x)))

  export
  (>>=) : Free c x -> (x -> Free c y) -> Free c y
  (>>=) (MkFree mx) k = foldr (alg . fromSum {c} {d = Const x}) mx where

    alg : Either (Extension c (Free c y)) (Extension (Const x) (Free c y)) -> Free c y
    alg  = either (MkFree . MkW . toSum {c} {d = Const y} . Left . map (runFree {c}))
                  (k . fromConst {k = x})

  export
  join : Free c (Free c x) -> Free c x
  join = (>>= id)

namespace Final

  public export
  data M : Container -> Type where
    MkM : Extension c (Inf (M c)) -> M c

  export
  unfoldr : (s -> Extension c s) -> s -> M c
  unfoldr next seed =
    let (MkExtension shp chld) = next seed in
    MkM (MkExtension shp (\ p => unfoldr next (chld p)))

namespace Comonad

  ||| @Cofree@ is a wrapper around @M@ to make it inference friendly.
  ||| Without this wrapper, neither @extract@ nor @extend@ are able to infer their @c@ argument.
  public export
  record Cofree (c : Container) (x : Type) where
    constructor MkCofree
    runCofree : M (Pair (Const x) c)

  export
  extract : Cofree c x -> x
  extract (MkCofree (MkM m)) = fst (shape m)

  export
  extend : (Cofree c a -> b) -> Cofree c a -> Cofree c b
  extend alg = MkCofree . unfoldr next . runCofree where

    next : M (Pair (Const a) c) -> Extension (Pair (Const b) c) (M (Pair (Const a) c))
    next m@(MkM layer) =
      let (_, (MkExtension shp chld)) = fromPair {c = Const a} layer in
      let b = toConst (alg (MkCofree m)) in
      toPair (b, MkExtension shp (\ p => chld p))
-- Eta-expanded to force Inf ------^

  export
  duplicate : Cofree c a -> Cofree c (Cofree c a)
  duplicate = extend id

------------------------------------------------------------------------
-- Derivative

namespace Derivative

  public export
  Derivative : Container -> Container
  Derivative c = MkContainer
    (s : Shape c ** Position c s)
    (\ (s ** p) => (p' : Position c s ** Not (p === p')))

  export
  hole : (v : Extension (Derivative c) x) -> Position c (fst (shape v))
  hole (MkExtension (shp ** p) _) = p

  export
  unplug : (v : Extension c x) -> Position c (shape v) -> (Extension (Derivative c) x, x)
  unplug (MkExtension shp chld) p = (MkExtension (shp ** p) (chld . fst), chld p)

  export
  plug : (v : Extension (Derivative c) x) -> DecEq (Position c (fst (shape v))) => x -> Extension c x
  plug (MkExtension (shp ** p) chld) x = MkExtension shp $ \ p' => case decEq p p' of
    Yes eq => x
    No neq => chld (p' ** neq)

  export
  toConst : Extension (Const Void) x -> Extension (Derivative (Const k)) x
  toConst v = absurd (fromConst v)

  export
  fromConst : Extension (Derivative (Const k)) x -> Extension (Const Void) x
  fromConst v = absurd (hole {c = Const _} v)

  export
  toIdentity : Extension (Derivative Identity) x
  toIdentity = MkExtension (() ** ()) (\ (() ** eq) => absurd (eq Refl))

  export
  toSum : Extension (Sum (Derivative c) (Derivative d)) x ->
          Extension (Derivative (Sum c d)) x
  toSum v = case fromSum {c = Derivative c} {d = Derivative d} v of
    Left (MkExtension (shp ** p) chld) => MkExtension (Left shp ** p) chld
    Right (MkExtension (shp ** p) chld) => MkExtension (Right shp ** p) chld

  export
  fromSum : Extension (Derivative (Sum c d)) x ->
            Extension (Sum (Derivative c) (Derivative d)) x
  fromSum (MkExtension (shp ** p) chld) = toSum {c = Derivative c} {d = Derivative d} $ case shp of
    Left shp => Left (MkExtension (shp ** p) chld)
    Right shp => Right (MkExtension (shp ** p) chld)

  export
  toPair : Extension (Sum (Pair (Derivative c) d) (Pair c (Derivative d))) x ->
           Extension (Derivative (Pair c d)) x
  toPair v = case fromSum {c = Pair (Derivative c) d} {d = Pair c (Derivative d)} v of
    Left p => let (MkExtension (shp1 ** p1) chld1, MkExtension shp2 chld2) = fromPair {c = Derivative c} p in
              MkExtension ((shp1, shp2) ** Left p1) $ \ (p' ** neq) => case p' of
                  Left p1' => chld1 (p1' ** (neq . cong Left))
                  Right p2' => chld2 p2'
    Right p => let (MkExtension shp1 chld1, MkExtension (shp2 ** p2) chld2) = fromPair {c} {d = Derivative d} p in
               MkExtension ((shp1, shp2) ** Right p2) $ \ (p' ** neq) => case p' of
                  Left p1' => chld1 p1'
                  Right p2' => chld2 (p2' ** (neq . cong Right))

  export
  fromPair : Extension (Derivative (Pair c d)) x ->
             Extension (Sum (Pair (Derivative c) d) (Pair c (Derivative d))) x
  fromPair (MkExtension ((shp1, shp2) ** p) chld) = case p of
    Left p1 => toSum {c = Pair (Derivative c) d} {d = Pair c (Derivative d)}
                     (Left (MkExtension ((shp1 ** p1), shp2) $ either
                         (\ p1' => chld (Left (DPair.fst p1') ** DPair.snd p1' . injective))
                         (\ p2 => chld (Right p2 ** absurd))))
    Right p2 => toSum {c = Pair (Derivative c) d} {d = Pair c (Derivative d)}
                     (Right (MkExtension (shp1, (shp2 ** p2)) $ either
                         (\ p1 => chld (Left p1 ** absurd))
                         (\ p2' => chld (Right (DPair.fst p2') ** DPair.snd p2' . injective))))

  export
  fromCompose : Extension (Derivative (Compose c d)) x ->
                Extension (Pair (Derivative d) (Compose (Derivative c) d)) x
  fromCompose (MkExtension (MkExtension shp1 shp2 ** (p1 ** p2)) chld)
    = toPair (left, right) where

      left : Extension (Derivative d) x
      left = MkExtension (shp2 p1 ** p2)
           $ \ (p2' ** neqp2) => chld ((p1 ** p2') ** neqp2 . mkDPairInjectiveSnd)

      right : Extension (Compose (Derivative c) d) x
      right = toCompose
            $ MkExtension (shp1 ** p1)
            $ \ (p1' ** neqp1) => MkExtension (shp2 p1')
                                 $ \ p2' => chld ((p1' ** p2') ** (neqp1 . cong fst))

  export
  toCompose : ((s : _) -> DecEq (Position c s)) -> ((s : _) -> DecEq (Position d s)) ->
              Extension (Pair (Derivative d) (Compose (Derivative c) d)) x ->
              Extension (Derivative (Compose c d)) x
  toCompose dec1 dec2 v with (fromPair {c = Derivative d} {d = Compose (Derivative c) d} v)
    toCompose dec1 dec2 v | (MkExtension (shp2 ** p2) chld2, w) with (fromCompose w)
      toCompose dec1 dec2 v
        | (MkExtension (shp2 ** p2) chld2, w)
        | (MkExtension (shp1 ** p1) chld1)
        = MkExtension (MkExtension shp1 (\ p1' => shp2' p1' (decEq @{dec1 shp1} p1 p1')) **
                      (p1 ** (p2' (decEq @{dec1 shp1} p1 p1))))
        $ \ ((p1' ** p2'') ** neq) => chld2' p1' p2'' neq

         where
          shp2' : (p1' : Position c shp1) -> Dec (p1 === p1') -> Shape d
          shp2' p1' (Yes eq) = shp2
          shp2' p1' (No neq) = shape (chld1 (p1' ** neq))

          p2' : (eq : Dec (p1 === p1)) -> Position d (shp2' p1 eq)
          p2' (Yes Refl) = p2
          p2' (No neq)   = absurd (neq Refl)

          chld2' : (p1' : Position c shp1) ->
                   (p2'' : Position d (shp2' p1' (decEq @{dec1 shp1} p1 p1'))) ->
                   (neq : Not (MkDPair p1 (p2' (decEq @{dec1 shp1} p1 p1)) = MkDPair p1' p2'')) -> x
          chld2' p1' p2'' neq with (decEq @{dec1 shp1} p1 p1')
            chld2' p1' p2'' neq | No neq1 = payloads (chld1 (p1' ** neq1)) p2''
            chld2' _ p2'' neq | Yes Refl with (decEq @{dec1 shp1} p1 p1)
              chld2' _ p2'' neq | Yes Refl | No argh = absurd (argh Refl)
              chld2' _ p2'' neq | Yes Refl | Yes Refl with (decEq @{dec2 shp2} p2 p2'')
                chld2' _ p2'' neq | Yes Refl | Yes Refl | No neq2 = chld2 (p2'' ** neq2)
                chld2' _ _ neq | Yes Refl | Yes Refl | Yes Refl = absurd (neq Refl)


text:
-- %logging 5

interface Interface specifier where
  0 concrete : specifier -> Type

record Value s where
  constructor MkValue
  specifier : s

0 DependentValue : Interface s => Value s -> Type
DependentValue v = concrete (specifier v)

data Record : s -> Type where
  MkRecord : Value s -> DependentValue {s} value -> Record s

ext: idr


text:
module GRIN.PrimOps

import Data.Vect

import Core.CompileExpr
import Core.Core
import Core.Name
import Core.TT

import GRIN.AST
import GRIN.Data

%default total

bindArgs :
    Ref NextVar Var =>
    List (Tag GName) ->
    List Var ->
    (List Var -> Core (Exp GName)) ->
    Core (Exp GName)
bindArgs (tag :: tags) (arg :: args) k = do
    v <- newVar
    rest <- bindArgs tags args (k . (v ::))
    pure $ Bind (ConstTagNode tag [SVar v]) (App (GrinName Eval) [arg]) rest
bindArgs _ _ k = k []

export
primOp :
    Ref NextVar Var =>
    {arity : Nat} ->
    Vect arity (Tag GName) ->
    (primOp : PrimFn arity) ->
    Tag GName ->
    Core (Def GName)
primOp aTags op retTag = do
    args <- replicate arity newVar
    ret <- newVar
    pure $ mkDef (PrimName op) args
         !(bindArgs (toList aTags) args
         $ \as => pure $ Bind (VVar ret) (App (PrimFunc op) as)
         $ SimpleExp $ Pure $ ConstTagNode retTag [SVar ret])

mkConstTag : Constant -> Tag GName
mkConstTag c = MkTag Con (ConstName c)

intTag : Tag GName
intTag = mkConstTag $ I 0
int8Tag : Tag GName
int8Tag = mkConstTag $ I8 0
int16Tag : Tag GName
int16Tag = mkConstTag $ I16 0
int32Tag : Tag GName
int32Tag = mkConstTag $ I32 0
int64Tag : Tag GName
int64Tag = mkConstTag $ I64 0
bits8Tag : Tag GName
bits8Tag = mkConstTag $ B8 0
bits16Tag : Tag GName
bits16Tag = mkConstTag $ B16 0
bits32Tag : Tag GName
bits32Tag = mkConstTag $ B32 0
bits64Tag : Tag GName
bits64Tag = mkConstTag $ B64 0
integerTag : Tag GName
integerTag = mkConstTag $ BI 0

stringTag : Tag GName
stringTag = mkConstTag $ Str ""
charTag : Tag GName
charTag = mkConstTag $ Ch '\0'
doubleTag : Tag GName
doubleTag = mkConstTag $ Db 0.0

ioResTag : Tag GName
ioResTag = MkTag Con $ IdrName $ NS primIONS $ UN "MkIORes"

intTags : List (Constant, Tag GName)
intTags =
    [ (IntType, intTag)
    , (Int8Type, int8Tag), (Int16Type, int16Tag), (Int32Type, int32Tag), (Int64Type, int64Tag)
    , (Bits8Type, bits8Tag), (Bits16Type, bits16Tag), (Bits32Type, bits32Tag), (Bits64Type, bits64Tag)
    , (IntegerType, integerTag)
    ]

cmpTags : List (Constant, Tag GName)
cmpTags = [(StringType, stringTag), (CharType, charTag), (DoubleType, doubleTag)] ++ intTags

concatTraverse : (a -> Core (List b)) -> List a -> Core (List b)
concatTraverse f = map concat . traverse f

concatCore : List (Core (List a)) -> Core (List a)
concatCore [] = pure []
concatCore (xs :: xss) = [| xs ++ concatCore xss |]

export
primOps : Ref NextVar Var => Core (List (Def GName))
primOps = concatCore
    [ concatTraverse mkBinOps intTags
    , concatTraverse mkCmpOps cmpTags
    , stringOps
    , miscOps
    ]
  where
    mkBinOps : (Constant, Tag GName) -> Core (List (Def GName))
    mkBinOps (ty, tag) = traverse (\fn => primOp [tag, tag] fn tag) [Add ty, Sub ty, Mul ty, Div ty]

    mkCmpOps : (Constant, Tag GName) -> Core (List (Def GName))
    mkCmpOps (ty, tag) = traverse (\fn => primOp [tag, tag] fn intTag) [LT ty, LTE ty, EQ ty, GTE ty, GT ty]

    stringOps : Core (List (Def GName))
    stringOps = sequence
        [ primOp [stringTag] StrLength intTag
        , primOp [stringTag] StrHead charTag
        , primOp [stringTag] StrTail stringTag
        , primOp [stringTag, intTag] StrIndex charTag
        , primOp [charTag, stringTag] StrCons stringTag
        , primOp [stringTag, stringTag] StrAppend stringTag
        , primOp [stringTag] StrReverse stringTag
        , primOp [intTag, intTag, stringTag] StrSubstr stringTag
        ]

    miscOps : Core (List (Def GName))
    miscOps = sequence
        [ do
            ty1 <- newVar
            ty2 <- newVar
            arg <- newVar
            pure $ mkDef (PrimName BelieveMe) [ty1, ty2, arg] $ SimpleExp $ App (PrimFunc BelieveMe) [ty1, ty2, arg]
        ]

export
externs : List (Extern GName)
externs = []

export
primCons :
    Ref NextVar Var =>
    (ptr : Var) -> Core (List (Alt GName))
primCons _ = [| miscPrimAlts ++ traverse mkPrimAlt cons |]
  where
    cons : List Constant
    cons =
        [I 0, I8 0, I16 0, I32 0,
         I64 0, BI 0, B8 0, B16 0,
         B32 0, B64 0, Str "", Ch '\0',
         Db 0.0, WorldVal, IntType, Int8Type,
         Int16Type, Int32Type, Int64Type, IntegerType,
         Bits8Type, Bits16Type, Bits32Type, Bits64Type,
         StringType, CharType, DoubleType, WorldType]
    mkPrimAlt : Constant -> Core (Alt GName)
    mkPrimAlt c = do
        v <- newVar
        pure $ MkAlt (getConstantNodePat v c) $ SimpleExp $ Pure $ wrapConstant v c
    miscPrimAlts : Core (List (Alt GName))
    miscPrimAlts = pure
        [ MkAlt (NodePat nullTag []) $ SimpleExp $ Pure $ ConstTagNode nullTag []
        ]

getCFTypeCon : CFType -> Tag GName
getCFTypeCon CFUnit = intTag
getCFTypeCon CFInt = intTag
getCFTypeCon CFInteger = integerTag
getCFTypeCon CFInt8 = int8Tag
getCFTypeCon CFInt16 = int16Tag
getCFTypeCon CFInt32 = int32Tag
getCFTypeCon CFInt64 = int64Tag
getCFTypeCon CFUnsigned8 = bits8Tag
getCFTypeCon CFUnsigned16 = bits16Tag
getCFTypeCon CFUnsigned32 = bits32Tag
getCFTypeCon CFUnsigned64 = bits64Tag
getCFTypeCon CFString = stringTag
getCFTypeCon CFDouble = doubleTag
getCFTypeCon CFChar = charTag
getCFTypeCon CFPtr = MkTag Con $ GrinName PtrVar
getCFTypeCon CFGCPtr = MkTag Con $ GrinName PtrVar
getCFTypeCon CFBuffer = MkTag Con $ GrinName PtrVar
getCFTypeCon CFForeignObj = MkTag Con $ GrinName PtrVar
getCFTypeCon CFWorld = MkTag Con $ GrinName PtrVar
getCFTypeCon (CFFun _ _) = MkTag Con $ GrinName PtrVar
getCFTypeCon (CFIORes ty) = assert_total $ getCFTypeCon ty
getCFTypeCon (CFStruct _ _) = MkTag Con $ GrinName PtrVar
getCFTypeCon (CFUser _ _) = MkTag Con $ GrinName PtrVar

%inline
getCFTypeCons : List CFType -> List (Tag GName)
getCFTypeCons = map getCFTypeCon

bindArgsWithWorld :
    Ref NextVar Var =>
    List CFType ->
    List Var ->
    (List Var -> Var -> Core (Exp GName)) ->
    Core (Exp GName)
bindArgsWithWorld tys args f = doBind tys args Nothing $ handleNoWorld f
  where
    doBind :
        List CFType ->
        List Var ->
        Maybe Var ->
        (List Var -> Maybe Var -> Core (Exp GName)) ->
        Core (Exp GName)
    doBind [] [] world k = k [] world
    doBind (CFWorld :: tys) (arg :: args) _ k = doBind tys args (Just arg) k
    doBind (ty :: tys) (arg :: args) world k = do
        v <- newVar
        rest <- doBind tys args world (k . (v ::))
        pure $ Bind (ConstTagNode (getCFTypeCon ty) [SVar v]) (Pure $ VVar arg)
             rest
    doBind _ _ _ _ = throw $ InternalError "Mismatch between number of arguments and number of types"

    handleNoWorld :
        (List Var ->       Var -> Core (Exp GName)) ->
        (List Var -> Maybe Var -> Core (Exp GName))
    handleNoWorld f vs Nothing = throw $ InternalError "Unable to find World in ffi call"
    handleNoWorld f vs (Just world) = f vs world

export
mkFFIWrapper :
    Ref NextVar Var =>
    GName ->
    List CFType ->
    CFType ->
    GName -> -- primitive function
    Core (Def GName)
mkFFIWrapper fn args ret@(CFIORes innerRet) op = do
    vs <- traverse (\_ => newVar) args
    exp <- bindArgsWithWorld args vs $ \vs', world => do
        res <- newVar
        let res' = if isUnit innerRet then SLit (LInt 0) else SVar res
        pure $ Bind (VVar res) (App op vs')
             $ SimpleExp $ Pure $ ConstTagNode (getCFTypeCon ret) [res']
    pure $ mkDef fn vs exp
  where
    isUnit : CFType -> Bool
    isUnit CFUnit = True
    isUnit _ = False

mkFFIWrapper fn args ret op = do
    vs <- traverse (\_ => newVar) args
    let argCons = getCFTypeCons args
    exp <- bindArgs argCons vs $ \vs' => do
        res <- newVar
        pure $ Bind (VVar res) (App op vs')
             $ SimpleExp $ Pure $ ConstTagNode (getCFTypeCon ret) [SVar res]
    pure $ mkDef fn vs exp


text:
module Fmt

import Data.String

%default total

-- From https://gist.github.com/chrisdone/672efcd784528b7d0b7e17ad9c115292

-- TODO: Add showables

public export
data Format
  = FInt Format
  | FString Format
  | FOther Char Format
  | FEnd

public export
format : List Char -> Format
format ('%' :: 'd' :: cs) = FInt (format cs)
format ('%' :: 's' :: cs) = FString (format cs)
format (c :: cs) = FOther c (format cs)
format [] = FEnd

public export
formatString : String -> Format
formatString = format . unpack

public export
interpFormat : Format -> Type
interpFormat (FInt f) = Int -> interpFormat f
interpFormat (FString f) = String -> interpFormat f
interpFormat (FOther _ f) = interpFormat f
interpFormat FEnd = String

public export
toFunction : (fmt : Format) -> String -> interpFormat fmt
toFunction (FInt f) a = \i => toFunction f (a ++ show i)
toFunction (FString f) a = \s => toFunction f (a ++ s)
toFunction (FOther c f) a = toFunction f (a ++ singleton c)
toFunction FEnd a = a

public export
fmt : (s : String) -> interpFormat (formatString s)
fmt s = toFunction (formatString s) ""

max_stars_repo_name: Z-snails/inigo

max_issues_repo_name: Z-snails/inigo

max_forks_repo_name: Z-snails/inigo


text:
import Arduino.Raw

forever : Monad m => m a -> m b
forever x = do x; forever x

export
main : IO Unit
main = do
  pinMode 13 1
  forever $ do
    digitalWrite 13 1
    sleepFor 1000
    digitalWrite 13 0
    sleepFor 2000

max_stars_repo_name: buzden/idris-arduino-lib

max_issues_repo_name: buzden/idris-arduino-lib

max_forks_repo_name: buzden/idris-arduino-lib


text:
-- PalindromeMain.idr
-- App for checking palindromes

module Main

import Exercises

main : IO ()
main = repl "Enter a string: " (\s => format $ palindrome s)
  where
    format : Bool -> String
    format x = (show x) ++ "\n"

max_stars_repo_name: kkirstein/proglang-playground

max_issues_repo_name: kkirstein/proglang-playground

max_forks_repo_name: kkirstein/proglang-playground


text:
||| Test extended record syntax
data NotZero : Nat -> Type where
  Is : {n : Nat} -> NotZero (S n)

record Positive (n : Nat) {auto 0 pos : NotZero n} where
  constructor Check

a : Positive 1
a = Check

b : Positive 2
b = Check

{- Will not type-check
c : Positive 0
-}

data KindOfString = ASCII | UTF

UTForASCII : KindOfString -> Type
UTForASCII UTF = String
UTForASCII ASCII = List Char   --- Just to demonstrate

record FlexiString { default UTF k : KindOfString} where
  constructor MkFlexiString
  val : UTForASCII k

c : FlexiString
c = MkFlexiString "hello"

d : FlexiString {k = ASCII}
d = MkFlexiString ['h', 'i']


text:
module Main

import Data.String
import Data.Vect
import System

%default total

ints : Vect 4 Int
ints = [1, 2, 3, 4]

main : IO ()
main = do
  [_, arg] <- getArgs
      | _ => do putStrLn "One argument expected."
                exitFailure
  let n = stringToNatOrZ arg
  -- case block in a case block, which is needed to test this properly
  case natToFin n (length ints + 1) of
       Nothing => do putStrLn "Invalid number."
                     exitFailure
       Just (FS i) => putStrLn $ "Value: " ++ show (index i ints)


text:
import System.File
import Data.String

putLines : List String -> IO ()
putLines = putStrLn . fastAppend

total
totalChecks : IO ()
totalChecks =
  do Right (False, l1) <- readFilePage 0 (limit 0) "test.txt"
       | Right (True, _) => putStrLn "Failed EOF check"
       | Left err => putStrLn $ show err
     putStrLn $ "empty: " ++ (show l1)
     Right (False, l2) <- readFilePage 0 (limit 1) "test.txt"
       | Right (True, _) => putStrLn "Failed EOF check"
       | Left err => putStrLn $ show err
     putLines l2
     Right (False, l3) <- readFilePage 1 (limit 2) "test.txt"
       | Right (True, _) => putStrLn "Failed EOF check"
       | Left err => putStrLn $ show err
     putLines l3
     Right (True, l4) <- readFilePage 0 (limit 100) "test.txt"
       | Right (False, _) => putStrLn "Failed EOF check"
       | Left err => putStrLn $ show err
     putLines l4

partial
main : IO ()
main = do totalChecks
          Right (True, l5) <- readFilePage 0 forever "test.txt"
            | Right (False, _) => putStrLn "Failed EOF check"
            | Left err => putStrLn $ show err
          putLines l5
          Right (True, l6) <- readFilePage 2 forever "test.txt"
            | Right (False, _) => putStrLn "Failed EOF check"
            | Left err => putStrLn $ show err
          putLines l6
          Right (True, l7) <- readFilePage 100 forever "test.txt"
            | Right (False, _) => putStrLn "Failed EOF check"
            | Left err => putStrLn $ show err
          putStrLn $ "empty: " ++ (show l7)
          Right l8 <- readFile "test.txt"
            | Left err => putStrLn $ show err
          putStrLn l8


text:
||| Additional views for Vect
module Data.Vect.Views.Extra

import Control.WellFounded
import Data.Vect
import Data.Nat

||| View for splitting a vector in half, non-recursively
public export
data Split : Vect n a -> Type where
    SplitNil : Split []
    SplitOne : Split [x]
    ||| two non-empty parts
    SplitPair : {n : Nat} -> {m : Nat} ->
                (x : a) -> (xs : Vect n a) -> (y : a) -> (ys : Vect m a) ->
                Split (x :: xs ++ y :: ys)

total
splitHelp : {n : Nat} -> (head : a) -> (zs : Vect n a) ->
            Nat -> Split (head :: zs)
splitHelp head [] _ = SplitOne
splitHelp head (z :: zs) 0 = SplitPair head [] z zs
splitHelp head (z :: zs) 1 = SplitPair head [] z zs
splitHelp head (z :: zs) (S (S k))
  = case splitHelp z zs k of
         SplitOne => SplitPair head [] z zs
         SplitPair x xs y ys => SplitPair head (x :: xs) y ys

||| Covering function for the `Split` view
||| Constructs the view in linear time
export total
split : {n : Nat} -> (xs : Vect n a) -> Split xs
split [] = SplitNil
split {n = S k} (x :: xs) = splitHelp x xs k

||| View for splitting a vector in half, recursively
|||
||| This allows us to define recursive functions which repeatedly split vectors
||| in half, with base cases for the empty and singleton lists.
public export
data SplitRec : Vect k a -> Type where
  SplitRecNil : SplitRec []
  SplitRecOne : SplitRec [x]
  SplitRecPair : {n : Nat} -> {m : Nat} -> {xs : Vect (S n) a} -> {ys : Vect (S m) a} ->
    (lrec : Lazy (SplitRec xs)) -> (rrec : Lazy (SplitRec ys)) -> SplitRec (xs ++ ys)

smallerPlusL : (m : Nat) -> (k : Nat) -> LTE (S (S m)) (S (m + S k))
smallerPlusL m k = rewrite sym (plusSuccRightSucc m k) in LTESucc $ LTESucc $ lteAddRight _

smallerPlusR : (m : Nat) -> (k : Nat) -> LTE (S (S k)) (S (m + S k))
smallerPlusR m k = rewrite sym (plusSuccRightSucc m k) in
                    LTESucc $ LTESucc $ rewrite plusCommutative m k in lteAddRight _

||| Covering function for the `SplitRec` view
||| Constructs the view in O(n lg n)
public export total
splitRec : {k : Nat} -> (xs : Vect k a) -> SplitRec xs
splitRec input with (sizeAccessible k)
  splitRec input | acc with (split input)
    splitRec {k = 0} []  | acc | SplitNil = SplitRecNil
    splitRec {k = 1} [x] | acc | SplitOne = SplitRecOne
    splitRec {k = S nl + S nr} (x :: xs ++ y :: ys) | Access rec | SplitPair x xs y ys =
      SplitRecPair
        (splitRec {k = S nl} (x :: xs) | rec _ $ smallerPlusL nl nr)
        (splitRec {k = S nr} (y :: ys) | rec _ $ smallerPlusR nl nr)


text:
module Text.WebIDL.Types.Type

import Data.Bitraversable
import Data.Bifoldable
import Data.Traversable
import Text.WebIDL.Types.Attribute
import Text.WebIDL.Types.Identifier
import Generics.Derive

%language ElabReflection

||| BufferRelatedType ::
|||     ArrayBuffer
|||     DataView
|||     Int8Array
|||     Int16Array
|||     Int32Array
|||     Uint8Array
|||     Uint16Array
|||     Uint32Array
|||     Uint8ClampedArray
|||     Float32Array
|||     Float64Array
public export
data BufferRelatedType = ArrayBuffer
                       | DataView
                       | Int8Array
                       | Int16Array
                       | Int32Array
                       | Uint8Array
                       | Uint16Array
                       | Uint32Array
                       | Uint8ClampedArray
                       | Float32Array
                       | Float64Array

%runElab derive "BufferRelatedType" [Generic,Meta,Eq,Show,HasAttributes]

||| StringType ::
|||     ByteString
|||     DOMString
|||     USVString
public export
data StringType = ByteString
                | DOMString
                | USVString

%runElab derive "Type.StringType" [Generic,Meta,Eq,Show,HasAttributes]

public export
data IntType = Short | Long | LongLong

%runElab derive "Type.IntType" [Generic,Meta,Eq,Show,HasAttributes]

public export
data FloatType = Float | Dbl

%runElab derive "Type.FloatType" [Generic,Meta,Eq,Show,HasAttributes]

||| PrimitiveType ::
|||     UnsignedIntegerType
|||     UnrestrictedFloatType
|||     undefined
|||     boolean
|||     byte
|||     octet
|||     bigint
||| UnrestrictedFloatType ::
|||     unrestricted FloatType
|||     FloatType
|||
||| FloatType ::
|||     float
|||     double
|||
||| UnsignedIntegerType ::
|||     unsigned IntegerType
|||     IntegerType
|||
||| IntegerType ::
|||     short
|||     long OptionalLong
|||
||| OptionalLong ::
|||     long
|||     ε
public export
data PrimitiveType = Unsigned     IntType
                   | Signed       IntType
                   | Unrestricted FloatType
                   | Restricted   FloatType
                   | Undefined
                   | Boolean
                   | Byte
                   | Octet
                   | BigInt

%runElab derive "PrimitiveType" [Generic,Meta,Eq,Show,HasAttributes]

public export
data ConstTypeF a = CP PrimitiveType | CI a

%runElab derive "ConstTypeF" [Generic,Meta,Eq,Show,HasAttributes]

||| Null ::
|||     ?
|||     ε
public export
data Nullable a = MaybeNull a | NotNull a

%runElab derive "Nullable" [Generic,Meta,Eq,Show,HasAttributes]

export
nullVal : Nullable a -> a
nullVal (MaybeNull x) = x
nullVal (NotNull x)   = x

export
nullable : Nullable a -> Nullable a
nullable = MaybeNull . nullVal

export
notNullable : Nullable a -> Nullable a
notNullable = NotNull . nullVal

export
isNullable : Nullable a -> Bool
isNullable (MaybeNull _) = True
isNullable (NotNull _)   = False

mutual
  ||| Type ::
  |||     SingleType
  |||     UnionType Null
  |||
  ||| SingleType ::
  |||     DistinguishableType
  |||     any
  |||     PromiseType
  |||
  ||| PromiseType ::
  |||     Promise < Type >
  public export
  data IdlTypeF : (a : Type) -> (b : Type) -> Type where
    Any     : IdlTypeF a b
    D       : Nullable (DistinguishableF a b) -> IdlTypeF a b
    U       : Nullable (UnionTypeF a b) -> IdlTypeF a b
    Promise : IdlTypeF a b -> IdlTypeF a b

  ||| UnionType ::
  |||     ( UnionMemberType or UnionMemberType UnionMemberTypes )
  |||
  ||| UnionMemberTypes ::
  |||     or UnionMemberType UnionMemberTypes
  |||     ε
  public export
  record UnionTypeF (a : Type) (b : Type) where
    constructor UT
    fst  : UnionMemberTypeF a b
    snd  : UnionMemberTypeF a b
    rest : List (UnionMemberTypeF a b)

  ||| UnionMemberType ::
  |||     ExtendedAttributeList DistinguishableType
  |||     UnionType Null
  public export
  record UnionMemberTypeF (a : Type) (b : Type) where
    constructor MkUnionMember
    attr : a
    type : DistinguishableF a b

  ||| DistinguishableType ::
  |||     PrimitiveType Null
  |||     StringType Null
  |||     identifier Null
  |||     sequence < TypeWithExtendedAttributes > Null
  |||     object Null
  |||     symbol Null
  |||     BufferRelatedType Null
  |||     FrozenArray < TypeWithExtendedAttributes > Null
  |||     ObservableArray < TypeWithExtendedAttributes > Null
  |||     RecordType Null
  |||
  ||| RecordType ::
  |||     record < StringType , TypeWithExtendedAttributes >
  public export
  data DistinguishableF : (a : Type) -> (b : Type) -> Type where
    P : PrimitiveType -> DistinguishableF a b
    S : StringType -> DistinguishableF a b
    I : b -> DistinguishableF a b
    B : BufferRelatedType -> DistinguishableF a b
    Sequence : a -> IdlTypeF a b -> DistinguishableF a b
    FrozenArray : a -> IdlTypeF a b -> DistinguishableF a b
    ObservableArray : a -> IdlTypeF a b -> DistinguishableF a b
    Record : StringType -> a -> IdlTypeF a b -> DistinguishableF a b
    Object : DistinguishableF a b
    Symbol : DistinguishableF a b

%runElab deriveMutual [ ("DistinguishableF", [Generic,Meta,Show,Eq])
                      , ("UnionMemberTypeF", [Generic,Meta,Show,Eq])
                      , ("UnionTypeF",       [Generic,Meta,Show,Eq])
                      , ("IdlTypeF",         [Generic,Meta,Show,Eq])
                      ]

public export
IdlType : Type
IdlType = IdlTypeF ExtAttributeList Identifier

public export
UnionType : Type
UnionType = UnionTypeF ExtAttributeList Identifier

public export
UnionMemberType : Type
UnionMemberType = UnionMemberTypeF ExtAttributeList Identifier

public export
Distinguishable : Type
Distinguishable = DistinguishableF ExtAttributeList Identifier

public export
ConstType : Type
ConstType = ConstTypeF Identifier

||| OptionalType ::
|||     , TypeWithExtendedAttributes
|||     ε
public export
0 OptionalType : Type
OptionalType = Maybe (Attributed IdlType)

||| Wraps and `Indentifier` as a non-nullable type.
export
identToType : b -> IdlTypeF a b
identToType = D . NotNull . I

||| The `Undefined` type
export
undefined : IdlTypeF a b
undefined = D $ NotNull $ P Undefined

export
isUndefined : IdlTypeF a b -> Bool
isUndefined (D $ NotNull $ P Undefined) = True
isUndefined _                           = False

export
domString : IdlTypeF a b
domString = D $ NotNull $ S DOMString

export
ulong : IdlTypeF a b
ulong = D $ NotNull $ P $ Unsigned Long

export
isIndex : IdlTypeF a b -> Bool
isIndex (D $ NotNull $ S DOMString)       = True
isIndex (D $ NotNull $ P $ Unsigned Long) = True
isIndex _                                 = False

--------------------------------------------------------------------------------
--          Implementations
--------------------------------------------------------------------------------

mutual
  export
  Functor Nullable where map = mapDefault

  export
  Foldable Nullable where foldr = foldrDefault

  export
  Traversable Nullable where
    traverse f (MaybeNull x) = MaybeNull <$> f x
    traverse f (NotNull x)   = NotNull <$> f x

mutual
  export
  Functor ConstTypeF where map = mapDefault

  export
  Foldable ConstTypeF where foldr = foldrDefault

  export
  Traversable ConstTypeF where
    traverse _ (CP x) = pure (CP x)
    traverse f (CI x) = CI <$> f x

mutual
  export
  Bifunctor DistinguishableF where bimap = assert_total bimapDefault

  export
  Bifoldable DistinguishableF where bifoldr = bifoldrDefault

  export
  Bitraversable DistinguishableF where
    bitraverse _ _ (P x) = pure (P x)
    bitraverse _ _ (S x) = pure (S x)
    bitraverse _ g (I x) = I <$> g x
    bitraverse _ _ (B x) = pure (B x)
    bitraverse f g (Sequence x y) = [| Sequence (f x) (bitraverse f g y) |]
    bitraverse f g (FrozenArray x y) = [| FrozenArray (f x) (bitraverse f g y) |]
    bitraverse f g (ObservableArray x y) = [| ObservableArray (f x) (bitraverse f g y) |]
    bitraverse f g (Record x y z) = [| Record (pure x) (f y) (bitraverse f g z) |]
    bitraverse _ _ Object = pure Object
    bitraverse _ _ Symbol = pure Symbol

  export
  Functor (DistinguishableF a) where map = bimap id

  export
  Foldable (DistinguishableF a) where foldr = bifoldr (const id)

  export
  Traversable (DistinguishableF a) where traverse = bitraverse pure

  export
  Bifunctor UnionMemberTypeF where bimap = assert_total bimapDefault

  export
  Bifoldable UnionMemberTypeF where bifoldr = bifoldrDefault

  export
  Bitraversable UnionMemberTypeF where
    bitraverse f g (MkUnionMember a t) =
      [| MkUnionMember (f a) (bitraverse f g t) |]

  export
  Functor (UnionMemberTypeF a) where map = bimap id

  export
  Foldable (UnionMemberTypeF a) where foldr = bifoldr (const id)

  export
  Traversable (UnionMemberTypeF a) where traverse = bitraverse pure

  export
  Bifunctor UnionTypeF where bimap = assert_total bimapDefault

  export
  Bifoldable UnionTypeF where bifoldr = bifoldrDefault

  export
  Bitraversable UnionTypeF where
    bitraverse f g (UT a b ts) =
      [| UT (bitraverse f g a) (bitraverse f g b)
            (traverse (bitraverse f g) ts) |]

  export
  Functor (UnionTypeF a) where map = bimap id

  export
  Foldable (UnionTypeF a) where foldr = bifoldr (const id)

  export
  Traversable (UnionTypeF a) where traverse = bitraverse pure

  export
  Bifunctor IdlTypeF where bimap = assert_total bimapDefault

  export
  Bifoldable IdlTypeF where bifoldr = bifoldrDefault

  export
  Bitraversable IdlTypeF where
    bitraverse f g Any = pure Any
    bitraverse f g (D x) = D <$> traverse (bitraverse f g) x
    bitraverse f g (U x) = U <$> traverse (bitraverse f g) x
    bitraverse f g (Promise x) = Promise <$> bitraverse f g x

  export
  Functor (IdlTypeF a) where map = bimap id

  export
  Foldable (IdlTypeF a) where foldr = bifoldr (const id)

  export
  Traversable (IdlTypeF a) where traverse = bitraverse pure

  export
  HasAttributes a => HasAttributes (IdlTypeF a b) where
    attributes = bifoldMap attributes (const Nil)


text:
module Optimisation.StaticProcessing.InstructionDeduplication

import Core.Context
import CairoCode.CairoCode
import CairoCode.CairoCodeUtils
import Data.List
import Data.SortedMap
import CairoCode.Traversal.Base
import CairoCode.Traversal.Composition
import Utils.Lens

-- This helps to deduplicate instructions representing the same operation with the same arguments
--  The second apperance is replaced by assigning the result of the first to the second (instead of recomputing)
--  Note: Together with StaticTransformer this can eliminate CommonSub Expressions unless an if is involved

-- This is part of StaticOptimisation/Constant Folding
--  A seperate module is used to keep the main module small

-- Instruction representation that only captures the inputs not the outputs not implicits
-- However, non relevant instructions like Null, Error or Assign are omitted

export
data InstInput: Type where
     Construct : Maybe Int -> List CairoReg -> InstInput
     Closure : Name -> List CairoReg -> InstInput
     Apply : CairoReg -> CairoReg -> InstInput
     Call : Name -> List CairoReg -> InstInput
     Op : CairoPrimFn -> List CairoReg -> InstInput
     Extprim : Name -> List CairoReg -> InstInput
     Project : Nat -> CairoReg -> InstInput

public export
Eq InstInput where
  (==) (Construct t1 a1) (Construct t2 a2) = t1 == t2 && a1 == a2
  (==) (Closure n1 a1) (Closure n2 a2) = n1 == n2 && a1 == a2
  (==) (Apply c1 a1) (Apply c2 a2) = c1 == c2 && a1 == a2
  (==) (Call n1 a1) (Call n2 a2) = n1 == n2 && a1 == a2
  (==) (Op f1 a1) (Op f2 a2) = f1 == f2 && a1 == a2
  (==) (Extprim n1 a1) (Extprim n2 a2) = n1 == n2 && a1 == a2
  (==) (Project p1 a1) (Project p2 a2) = p1 == p2 && a1 == a2
  (==) _ _  = False

public export
Ord InstInput where
  compare (Construct t1 a1) (Construct t2 a2) = thenCompare (compare t1 t2) (compare a1 a2)
  compare (Closure n1 a1) (Closure n2 a2) = thenCompare (compare n1 n2) (compare a1 a2)
  compare (Apply c1 a1) (Apply c2 a2) = thenCompare (compare c1 c2) (compare a1 a2)
  compare (Call n1 a1) (Call n2 a2) = thenCompare (compare n1 n2) (compare a1 a2)
  compare (Op f1 a1) (Op f2 a2) = thenCompare (compare f1 f2) (compare a1 a2)
  compare (Extprim n1 a1) (Extprim n2 a2) = thenCompare (compare n1 n2) (compare a1 a2)
  compare (Project p1 a1) (Project p2 a2)  = thenCompare (compare p1 p2) (compare a1 a2)
  compare a b = compare (dataOrder a) (dataOrder b)
    where dataOrder : InstInput -> Int
          dataOrder (Construct _ _) = 0
          dataOrder (Closure _ _) = 1
          dataOrder (Apply _ _) = 2
          dataOrder (Call _ _) = 3
          dataOrder (Op _ _) = 4
          dataOrder (Extprim _ _) = 5
          dataOrder (Project _ _) = 6

inputFromVisit : InstVisit CairoReg -> Maybe (List CairoReg, InstInput)
inputFromVisit (VisitMkCon res tag args) = Just ([res], Construct tag args)
inputFromVisit (VisitMkClosure res name _ args) = Just ([res], Closure name args)
inputFromVisit (VisitApply res _ f a) = Just ([res], Apply f a)
inputFromVisit (VisitCall res _ name args) = Just (res, Call name args)
inputFromVisit (VisitOp res _ fn args) =  Just ([res], Op fn args)
inputFromVisit (VisitExtprim res _ name args) = Just (res, Extprim name args)
inputFromVisit (VisitProject res arg pos) = Just ([res], Project pos arg)
inputFromVisit _ = Nothing

public export
ActiveInsts : Type
ActiveInsts = SortedMap InstInput (List CairoReg)

public export
TrackerState : Type
TrackerState = List ActiveInsts

activeInstructionTracker : InstVisit CairoReg -> Traversal TrackerState ()
activeInstructionTracker (VisitConBranch _ ) = readStateL headFailLens >>= (\head => updateState (head::))
activeInstructionTracker (VisitConstBranch _ ) = readStateL headFailLens >>= (\head => updateState (head::))
activeInstructionTracker VisitBranchEnd = readStateL tailFailLens >>= (\tail => writeState tail)
activeInstructionTracker VisitEndFunction = readStateL tailFailLens >>= (\tail => writeState (empty::tail))
activeInstructionTracker inst = process $ inputFromVisit inst
    where process : Maybe (List CairoReg, InstInput) -> Traversal TrackerState ()
          process Nothing = pure ()
          process (Just (regs, inst)) = updateStateL headFailLens (insert inst regs)

activeInstructionDedup : InstVisit CairoReg -> Traversal TrackerState (List (InstVisit CairoReg))
activeInstructionDedup inst = pure $ fromMaybe [inst] (fetchReplacement !(readStateL headFailLens))
    where fetchReplacement : ActiveInsts -> Maybe (List (InstVisit CairoReg))
          fetchReplacement activeInsts = do
              (res, inputInst) <- inputFromVisit inst
              original <- lookup inputInst activeInsts
              pure $ if (length res) == (length original)
                  then zipWith (\r,o => VisitAssign r o) res original
                  else [inst]

export
instructionDeduplication : InstVisit CairoReg -> Traversal TrackerState (List (InstVisit CairoReg))
instructionDeduplication = traverseTransform activeInstructionDedup activeInstructionTracker

export
initialDedupState : TrackerState
initialDedupState = empty::Nil

max_stars_repo_name: skyro-compiler/skyro

max_issues_repo_name: skyro-compiler/skyro

max_forks_repo_name: skyro-compiler/skyro


text:
-- WordLength.idr
--

import Data.Vect

-- allLengths for Vect String
total allLengths : Vect len String -> Vect len Nat
allLengths [] = []
allLengths (word :: words) = length word :: allLengths words


text:
module Main

import System
import Data.Buffer
import Data.Fin
import Effects
import Effect.SDL
import Effect.State
import Effect.StdIO
import Effect.System
import Effect.Random

import Constants
import Opcodes
import Screen
import Keybindings
import Keypad
import Chip8
import Ram
import Cpu
import MemoryIO

%default total

data Counter : Type where -- empty type

-- Effects: support SDL, chip8 state, counter, RAM (buffer I/O),
-- random number generation, console I/O, and system (for `usleep`).
State : Type -> Type -> Type
State i t = { [SDL i, Chip8 ::: STATE Chip8, Counter ::: STATE Integer, RAM, RND, STDIO, SYSTEM] } Effects.DepEff.Eff t

defaultROM : String
defaultROM = "./roms/maze.rom"

readROMFromFile : (filename : String) -> IO Buffer
readROMFromFile filename =
  let maxLength : Int = RamSize - StartingAddress in
  do
    handle <- openFile filename Read
    case handle of
      Right file => do
        buffer <- Buffer.newBuffer maxLength
        case buffer of
          Just mem =>
            Buffer.readBufferFromFile file mem maxLength
          Nothing =>
            do
              putStrLn "Not enough memory"
              System.exitFailure
      Left _ =>
        do
          putStrLn "Could not read ROM"
          System.exitFailure

getROMPath : List String -> String
getROMPath args =
  case index' 1 args of
    Nothing => defaultROM
    Just path => path

partial
runChip8 : { [SDL_ON, Chip8 ::: STATE Chip8, Counter ::: STATE Integer, RAM, RND] } Eff ()
runChip8 =
  do
    chip <- Chip8 :- get
    case State chip of
      Halted _ => pure ()
      WaitingForKey _ => pure ()
      Active =>
        -- The CPU runs at roughly 500Hz, however, we want to tick down the
        -- CPU DT/ST at a rate of 60Hz. As a first approximation, let's say
        -- we tick down DT/ST every 8 CPU cycles.
        let counter = !(Counter :- get) + 1 in
        let newCounter = counter `mod` 8 in
        let tick = newCounter == 7 in
        do
          runOneCycle tick
          Counter :- put newCounter

drawScreen : { [SDL_ON, Chip8 ::: STATE Chip8, STDIO] } Eff ()
drawScreen =
  let c : Chip8 = !(Chip8 :- get) in
  let cpu : Cpu = Computer c in
  let screen : Screen = Display c in
  let keys : Keypad = Keys c in
  do
    -- debugging
    -- putStrLn $ show cpu
    -- putStrLn $ show screen
    -- putStrLn $ show keys
    renderScreen screen
    flip

partial
runChip8Loop : State SDLSurface ()
runChip8Loop =
  do
    runChip8
    drawScreen
    usleep 2083 -- update ~480 times per second
    when !(processKeys !poll) runChip8Loop

partial
kickoff : Buffer -> State () ()
kickoff rom =
  do
    initialise (Width * Scale) (Height * Scale)
    loadDefaultSpriteDataAt DefaultSpriteDataAddress
    runChip8Loop
    quit
    putStrLn "Fin."

partial
main : IO ()
main =
  do
    args <- getArgs
    rom <- readROMFromFile $ getROMPath args
    chip8 <- newChip8
    loadROMAt chip8 rom StartingAddress
    runInit [(), Chip8 := chip8, Counter := 0, (), RandomSeed, (), ()] $ kickoff rom


text:
module RationalSetoid
import Rational
import SignedInt
import Setoid
import SignedSetoid
import NatExtension

%default total
%access public export

rationalReflx : Reflx RationalEq
rationalReflx (MkRat a b) = RationalRefl (signedReflx (a $* (S b)))

rationalSymm : Symm RationalEq
rationalSymm (MkRat a1 b1) (MkRat a2 b2) (RationalRefl rr) = RationalRefl (signedSymm (a1 $* (S b2)) (a2 $* (S b1)) rr)

rationalTrans : Trans RationalEq
rationalTrans (MkRat (SInt p1 n1) b1) (MkRat (SInt p2 n2) b2) (MkRat (SInt p3 n3) b3)
      (RationalRefl (SignedRefl sr12)) (RationalRefl (SignedRefl sr23)) = RationalRefl (SignedRefl sr13)
  where
    _1 : (p1 * S b2) * S b3 + (n2 * S b1) * S b3 = (p2 * S b1) * S b3 + (n1 * S b2) * S b3
    _1 = trans (trans l_tr (cong {f = (* S b3)} sr12)) r_tr
        where
          l_tr : (p1 * S b2) * S b3 + (n2 * S b1) * S b3 = ((p1 * S b2) + (n2 * S b1)) * S b3
          l_tr = sym (multDistributesOverPlusLeft (p1 * S b2) (n2 * S b1) (S b3))

          r_tr : ((p2 * S b1) + (n1 * S b2)) * S b3 = (p2 * S b1) * S b3 + (n1 * S b2) * S b3
          r_tr = multDistributesOverPlusLeft (p2 * S b1) (n1 * S b2) (S b3)

    _2 : (p2 * S b3) * S b1 + (n3 * S b2) * S b1 = (p3 * S b2) * S b1 + (n2 * S b3) * S b1
    _2 = trans (trans l_tr (cong {f = (* S b1)} sr23)) r_tr
      where
        l_tr : (p2 * S b3) * S b1 + (n3 * S b2) * S b1 = ((p2 * S b3) + (n3 * S b2)) * S b1
        l_tr = sym (multDistributesOverPlusLeft (p2 * S b3) (n3 * S b2) (S b1))

        r_tr : ((p3 * S b2) + (n2 * S b3)) * S b1 = (p3 * S b2) * S b1 + (n2 * S b3) * S b1
        r_tr = multDistributesOverPlusLeft (p3 * S b2) (n2 * S b3) (S b1)

    _3 : ((p1 * S b2) * S b3 + (n2 * S b1) * S b3) + ((p2 * S b3) * S b1 + (n3 * S b2) * S b1) =
         ((p2 * S b1) * S b3 + (n1 * S b2) * S b3) + ((p3 * S b2) * S b1 + (n2 * S b3) * S b1)
    _3 = rewrite _1 in rewrite _2 in Refl

    _4 : (p1 * S b2) * S b3 + (n3 * S b2) * S b1 = (n1 * S b2) * S b3 + (p3 * S b2) * S b1
    _4 = rewrite plusCommutative (p1 * S b2 * S b3) (n3 * S b2 * S b1) in _47
      where
        _41 : ((p1 * S b2) * S b3 + (n2 * S b1) * S b3) + ((p2 * S b3) * S b1 + (n3 * S b2) * S b1) =
                   ((p2 * S b3) * S b1 + (n3 * S b2) * S b1) + ((p1 * S b2) * S b3 + (n2 * S b3) * S b1)
        _41 =
            rewrite sym $ multAssociative n2 (S b3) (S b1) in
            rewrite sym $ multAssociative n2 (S b1) (S b3) in
            rewrite sym $ multCommutative (S b3) (S b1) in
            rewrite plusCommutative ((p1 * S b2) * S b3 + n2 * (S (b1 + b3 * S b1))) ((p2 * S b3) * S b1 + (n3 * S b2) * S b1) in
            Refl

        _42 : ((p2 * S b3) * S b1 + (n3 * S b2) * S b1) + (p1 * S b2) * S b3 + (n2 * S b3) * S b1 =
               ((p2 * S b1) * S b3 + (n1 * S b2) * S b3) + (p3 * S b2) * S b1 + (n2 * S b3) * S b1
        _42 =
            rewrite sym $ plusAssociative ((p2 * S b3) * S b1 + (n3 * S b2) * S b1) ((p1 * S b2) * S b3) ((n2 * S b3) * S b1) in
            rewrite sym $ plusAssociative ((p2 * S b1) * S b3 + (n1 * S b2) * S b3) ((p3 * S b2) * S b1) ((n2 * S b3) * S b1) in
            rewrite sym _41 in
            _3

        _43 : (p2 * S b3) * S b1 + (n3 * S b2) * S b1 + (p1 * S b2) * S b3 =
               (p2 * S b1) * S b3 + (n1 * S b2) * S b3 + (p3 * S b2) * S b1
        _43 = plusRightCancel _ _ (n2 * S b3 * S b1) _42

        _44 : (p2 * S b3) * S b1 + ((n3 * S b2) * S b1 + (p1 * S b2) * S b3) =
               (p2 * S b1) * S b3 + ((n1 * S b2) * S b3 + (p3 * S b2) * S b1)
        _44 =
            rewrite plusAssociative ((p2 * S b3) * S b1) ((n3 * S b2) * S b1) ((p1 * S b2) * S b3) in
            rewrite plusAssociative ((p2 * S b1) * S b3) ((n1 * S b2) * S b3) ((p3 * S b2) * S b1) in
            _43

        _45 : (p2 * S b1) * S b3 + ((n3 * S b2) * S b1 + (p1 * S b2) * S b3) =
                   (p2 * S b3) * S b1 + ((n3 * S b2) * S b1 + (p1 * S b2) * S b3)
        _45 =
            rewrite sym $ multAssociative p2 (S b1) (S b3) in
            rewrite multCommutative (S b1) (S b3) in
            rewrite multAssociative p2 (S b3) (S b1) in
            Refl

        _46 : (p2 * S b1) * S b3 + ((n3 * S b2) * S b1 + (p1 * S b2) * S b3) =
               (p2 * S b1) * S b3 + ((n1 * S b2) * S b3 + (p3 * S b2) * S b1)
        _46 = rewrite _45 in _44

        _47 : (n3 * S b2) * S b1 + (p1 * S b2) * S b3 =
               (n1 * S b2) * S b3 + (p3 * S b2) * S b1
        _47 = plusLeftCancel (p2 * S b1 * S b3) _ _ _46

    _5 : S b2 * (p1 * S b3 + n3 * S b1) = S b2 * (n1 * S b3 + p3 * S b1)
    _5 =
        rewrite multDistributesOverPlusRight (S b2) (p1 * S b3) (n3 * S b1) in
        rewrite multDistributesOverPlusRight (S b2) (n1 * S b3) (p3 * S b1) in
        rewrite takeY (S b2) p1 (S b3) in
        rewrite takeY (S b2) n1 (S b3) in
        rewrite takeY (S b2) p3 (S b1) in
        rewrite takeY (S b2) n3 (S b1) in
        _4

    sr13 : p1 * S b3 + n3 * S b1 = p3 * S b1 + n1 * S b3
    sr13 =
        rewrite plusCommutative (p3 * S b1) (n1 * S b3) in
        multLeftCancel _ _ _ _5

RationalSetoid : Setoid
RationalSetoid = MkSetoid Rational RationalEq (EqProof RationalEq rationalReflx rationalSymm rationalTrans)


text:
> data Usage = Once | Many

> data Use : Usage -> (Type -> Type) -> Type -> Type where
>      Pure : (1 x : a) -> Use t m a
>      BindOnce : (1 act : Use Once m a) -> (1 k : (1 x : a) -> Use t m b) -> Use t m b
>      BindMany : (1 act : Use Many m a) -> (1 k : (x : a) -> Use t m b) -> Use t m b

> contType : (Type -> Type) -> Usage -> Usage -> Type -> Type -> Type
> contType m Once q a b = ((1 x : a) -> Use q m b)
> contType m Many q a b = ((x : a) -> Use q m b)

> (>>=) : {p : _} -> (1 f : Use p m a) -> (1 k : contType m p q a b) -> Use q m b
> (>>=) {p = Once} = BindOnce
> (>>=) {p = Many} = BindMany

> pure : (1 x : a) -> Use t m a
> pure = Pure

> One : (Type -> Type) -> Type -> Type
> One = Use Once

> Any : (Type -> Type) -> Type -> Type
> Any = Use Many

> data DoorState = Closed | Open

> data Door : DoorState -> Type where
>      MkDoor : (isOpen : Bool) -> Door (if isOpen then Open else Closed)

> newDoor : One m (Door Closed)
> newDoor = pure (MkDoor False)

> knock : (1 d : Door Closed) -> One m (Door Closed)
> openDoor : (1 d : Door Closed) ->
>            One m (Res Bool (\r => Door (if r then Open else Closed)))

> closeDoor : (1 d : Door Open) -> One m (Door Closed)

> deleteDoor : (1 d : Door Closed) -> Any m ()

> doorProg : Any m ()
> doorProg
>     = do d <- newDoor
>          r <- openDoor d
>          let x = 42
>          case r of
>               what => ?now

> doorProg2 : Any m ()
> doorProg2
>     = do d <- newDoor
>          r <- openDoor d
>          let x = 42
>          case r of
>               (res # d) => ?now_1

> doorProg3 : Any m ()
> doorProg3
>     = do d <- newDoor
>          r <- openDoor d
>          let x = 42
>          case r of
>               (True # d) => ?now_2
>               (False # d) => ?now_3

ext: lidr


text:
module Specifications.Ring

import public Specifications.Group

%default total
%access public export

||| specification
isDistributativeL : Binop s -> Binop s -> Type
isDistributativeL (+) (*) = (a,x,y : _) -> a * (x + y) = a * x + a * y

||| specification
isDistributativeR : Binop s -> Binop s -> Type
isDistributativeR (+) (*) = (x,y,a : _) -> (x + y) * a = x * a + y * a

||| composed specification
data PreRingSpec : Binop s -> Binop s -> Type where
  MkPreRing : isDistributativeL add mul -> isDistributativeR add mul ->
    isAbelian add -> PreRingSpec add mul

||| forget
abelian : PreRingSpec add _ -> isAbelian add
abelian (MkPreRing _ _ a) = a

||| composed specification
data RingSpec : Binop s -> s -> (s -> s) -> Binop s -> Type where
  MkRing : PreRingSpec add mul ->
    GroupSpec add zero neg ->
    isAssociative mul ->
    RingSpec add zero neg mul

||| forget
distributativeL : RingSpec add _ _ mul -> isDistributativeL add mul
distributativeL (MkRing (MkPreRing l _ _) _ _) = l

||| forget
distributativeR : RingSpec add _ _ mul -> isDistributativeR add mul
distributativeR (MkRing (MkPreRing _ r _) _ _) = r

||| forget
group : RingSpec add zero neg _ -> GroupSpec add zero neg
group (MkRing preRing g _) = g

||| forget
abelianGroup : RingSpec add zero neg _ -> AbelianGroupSpec add zero neg
abelianGroup (MkRing preRing g _) = MkAbelianGroup g (abelian preRing)

||| forget
plusAbelian : RingSpec add zero neg _ -> isAbelian add
plusAbelian (MkRing preRing _ _) = abelian preRing

||| composed specification
data UnitalRingSpec : Binop s -> s -> (s -> s) -> Binop s -> s -> Type where
  MkUnitalRing : RingSpec add zero neg mul ->
    isNeutralL mul one ->
    isNeutralR mul one ->
    UnitalRingSpec add zero neg mul one

||| forget
ring : UnitalRingSpec add zero neg mul _ -> RingSpec add zero neg mul
ring (MkUnitalRing r _ _) = r

||| forget
multiplicativeMonoid : UnitalRingSpec _ _ _ mul one -> MonoidSpec mul one
multiplicativeMonoid (MkUnitalRing (MkRing _ _ assoc) l r) = MkMonoid assoc l r

max_stars_repo_name: jeroennoels/verified-algebra

max_issues_repo_name: jeroennoels/verified-algebra

max_forks_repo_name: jeroennoels/verified-algebra


text:
module Core.InitPrimitives

import Compiler.CompileExpr

import Core.Context
import Core.Primitives

%default covering

addPrim : {auto c : Ref Ctxt Defs} ->
          Prim -> Core ()
addPrim p
    = do addBuiltin (opName (fn p)) (type p) (totality p) (fn p)
         compileDef (opName (fn p))

export
addPrimitives : {auto c : Ref Ctxt Defs} -> Core ()
addPrimitives
    = traverse_ addPrim allPrimitives


text:
module Main

import BSTree

listToTree : Ord a => List a -> BSTree a
listToTree [] = Empty
listToTree (x :: xs) = insert x (listToTree xs)

treeToList : BSTree a -> List a
treeToList Empty = []
treeToList (Node left val right) = (treeToList left) ++ val :: (treeToList right)

data Expr = Val Int
          | Add Expr Expr
          | Sub Expr Expr
          | Mult Expr Expr

evaluate : Expr -> Int
evaluate (Val x) = x
evaluate (Add x y) = (evaluate x) + (evaluate y)
evaluate (Sub x y) = (evaluate x) - (evaluate y)
evaluate (Mult x y) = (evaluate x) * (evaluate y)

maxMaybe : Ord a => Maybe a -> Maybe a -> Maybe a
maxMaybe Nothing Nothing = Nothing
maxMaybe Nothing (Just x) = Just x
maxMaybe (Just x) Nothing = Just x
maxMaybe (Just x) (Just y) = case compare x y of
                             LT => Just y
                             EQ => Just x
                             GT => Just x


text:
module Progress

-- Progress theorem for the 'Step' relation.

import Step
import Subst
import Term

%default total
%access export

-------------------------------------
-- Begin: PROGRESS (AND PRESERVATION)

-- Function 'progress' proves the usual progress lemma.
--
-- Progress: a closed, well-typed term is either a value
--           or it can take a step in the reduction relation.
--
-- Preservation: after reducing a term of type 't' by one
--               step, the resulting term is again of type 't'.
--
--   ***  Note that preservation is already built into     ***
--   ***  the relation 'Step' as defined in module "Step". ***
--
progress : (e : Term [] t) -> Either (Value e) (e' : Term [] t ** (Step e e'))
-- Expressions that are variables cannot occur in an empty context:
-- (In other words, variables are not closed expressions.)
progress (TVar _) impossible
-- Abstractions are values already:
progress (TAbs _) = Left VAbs
-- Applications can reduce in three different ways, the most
-- interesting of which occurs when both arguments of 'App'
-- are values already: in this case, the function 'subst'
-- is required:
progress (TApp e1 e2) = case progress e1 of
  Right (e' ** st) => Right (TApp e' e2 ** StApp1 st)
  Left  v1         =>
    case progress e2 of
         Right (e' ** st) => Right (TApp e1 e' ** StApp2 v1 st)
         Left  v2         => case e1 of
                                  TAbs f => let e'' = subst e2 First f
                                            in Right (e'' ** StBeta v2)
-- When the fix-point operator is applied to a value,
-- that value is necessarily an abstraction; hence
-- the function 'subst' is used in reducing 'Fix _':
progress (TFix e) = case progress e of
  Right (e' ** st) => Right (TFix e' ** StFix st)
  Left v           =>
    case e of
         TAbs f => let e'' = subst (TFix (TAbs f)) First f
                   in Right (e'' ** StFixBeta)
-- The constant 'Zero' is a value already:
progress TZero = Left VZero
--
progress (TSucc e) = case progress e of
  Right (e' ** st) => Right (TSucc e' ** StSucc st)
  Left  v          => Left (VSucc v)
progress (TPred e) = case progress e of
  Right (e' ** st) => Right (TPred e' ** StPred st)
  Left v           =>
    case e of
         TZero    => Right (TZero ** StPredZero)
         TSucc e' => case v of
                          VAbs     impossible
                          VZero    impossible
                          VSucc v' => Right (e' ** StPredSucc v')
--
progress (TIfz e1 e2 e3) = case progress e1 of
  Right (e' ** st) => Right $ (TIfz e' e2 e3 ** StIfz st)
  Left v           => case v of
                           VAbs     impossible
                           VZero    => Right (e2 ** StIfzZero)
                           VSucc v' => Right (e3 ** StIfzSucc v')

-- End: PROGRESS (AND PRESERVATION)
-----------------------------------

-------------------------------
-- Begin: VALUE <=> IRREDUCIBLE

-- Establish that values cannot be further reduced under 'Step'.
valueIrreducible : (e : Term [] t) ->
                   Value e ->
                   {e' : Term [] t} -> Step e e' -> Void
valueIrreducible TZero     VZero     _           impossible
valueIrreducible (TSucc n) (VSucc v) (StSucc st) = valueIrreducible n v st
valueIrreducible (TAbs _)  VAbs      _           impossible

-- Establish that irreducible expressions (under 'Step') are values:
irreducibleValue : (e : Term [] t) ->
                   ({e' : Term [] t} -> Step e e' -> Void) ->
                   Value e
irreducibleValue e notStep = case progress e of
  Right (_ ** st) => absurd $ notStep st
  Left v          => v

coTransStepValueIrreducible : CoTransStep e1 e2 -> Value e1 -> e1 = e2
coTransStepValueIrreducible (CoTStRefl e1)       v = Refl
coTransStepValueIrreducible (CoTStTrans st ctst) v = absurd $ valueIrreducible _ v st

-- End: VALUE <=> IRREDUCIBLE
-----------------------------

max_stars_repo_name: normanrink/PCF

max_issues_repo_name: normanrink/PCF

max_forks_repo_name: normanrink/PCF


text:
import Skeletons
import System.Concurrency.BufferedChannel

import Data.List

------------------
-- Farm Example --
------------------

ack : Nat -> Nat -> Nat
ack 0 j = (S j)
ack (S k) 0 = ack k 1
ack (S k) (S j) = ack k $ ack (S k) j

ackList : List (WorkUnit Nat)
ackList = replicate 16 (TASK (ack 4 1))
--ackList = [TASK (ack 2 2), TASK (ack 4 1), TASK (ack 3 12), TASK (ack 4 1)]
--               ^ fast          ^ slow          ^ slow-ish      ^ slow

ackSeq : IO ()
ackSeq = do putStrLn $ show $ ack 4 1
            putStrLn $ show $ ack 4 1
            putStrLn $ show $ ack 4 1
            putStrLn $ show $ ack 4 1
            putStrLn $ show $ ack 4 1
            putStrLn $ show $ ack 4 1
            putStrLn $ show $ ack 4 1
            putStrLn $ show $ ack 4 1
            putStrLn $ show $ ack 4 1
            putStrLn $ show $ ack 4 1
            putStrLn $ show $ ack 4 1
            putStrLn $ show $ ack 4 1
            putStrLn $ show $ ack 4 1
            putStrLn $ show $ ack 4 1
            putStrLn $ show $ ack 4 1
            putStrLn $ show $ ack 4 1

ackFarm : Farm Nat
ackFarm = initFarm 8 ackList

farmMain : IO ()
farmMain =
  do putStrLn "Starting..."
     (bundleThreadID, resRef) <- runFarm ackFarm
     putStrLn "Farm running."
     (MkDPair resChan recv) <- becomeReceiver Blocking resRef
     resList <- collect ackFarm (bundleThreadID, resRef)
     putStrLn $ "Results: " ++ show resList
     putStrLn "DONE"

----------------------
-- Pipeline Example --
----------------------

||| n natural numbers on outChan, in descending order
countdown : (n : Nat)
          -> (outRef : IORef (BufferedChannel (PipelineData Nat)))
          -> IO ()
countdown 0 outRef =
  do (MkDPair outChan send) <- becomeSender outRef
     send Signal outChan DONE

countdown (S k) outRef =
  do (MkDPair outChan send) <- becomeSender outRef
     send Signal outChan $ NEXT (S k)
     countdown k outRef

||| n natural numbers on outChan, in ascending order
nats : (n : Nat)
     -> (outRef : IORef (BufferedChannel (PipelineData Nat)))
     -> IO ()
nats n outRef = nats' n Z outRef
  where
    nats' : Nat -> Nat -> IORef (BufferedChannel (PipelineData Nat)) -> IO ()
    nats' 0 k oRef =
      do (MkDPair outChan send) <- becomeSender oRef
         send Signal outChan $ NEXT k
         send Signal outChan DONE

    nats' (S j) k oRef =
      do (MkDPair outChan send) <- becomeSender oRef
         send Signal outChan $ NEXT k
         nats' j (S k) oRef

||| Squares its input
squareStage : PipelineData Nat -> PipelineData Nat
squareStage DONE = DONE
squareStage (NEXT x) = NEXT (x * x)

||| Converts its input to a String
showStage : Show a => PipelineData a -> PipelineData String
showStage DONE = DONE
showStage (NEXT x) = NEXT (show x)

||| Prints its input
printStage : PipelineData String -> PipelineData (IO ())
printStage DONE = DONE
printStage (NEXT x) = NEXT (putStrLn x)

squarePL : Pipeline Nat String
squarePL = initPipeline squareStage
           |> showStage

partial
pipelineMain : IO ()
pipelineMain =
  do inRef <- makeBufferedChannel
     nats 10 inRef
     (tid, resRef) <- runPipeline squarePL inRef
     (MkDPair resChan recv) <- becomeReceiver Blocking resRef
     firstRes <- recv resChan
     printLoop firstRes (MkDPair resChan recv)
     putStrLn "Main done."
  where
    partial
    printLoop : PipelineData String
              -> (resChan : BufferedChannel (PipelineData String)
                            ** BlockingReceiver (PipelineData String))
              -> IO ()
    printLoop DONE _ = putStrLn "Received DONE"
    printLoop (NEXT s) resDPair@(MkDPair resChan recv) =
      do putStrLn s
         next <- recv resChan
         printLoop next resDPair


text:
module CLaSH.Prelude.Vect

%access public
%default total

infixr 4 +>>
(+>>) : (el : a) -> (vs : Vect (S n) a) -> Vect (S n) a
(+>>) x xs = x :: init xs

vindexM_integer : (vs : Vect n a) -> (ind : Integer) -> Maybe a
vindexM_integer []        _ = Nothing
vindexM_integer (x :: _)  0 = Just x
vindexM_integer (_ :: xs) n = vindexM_integer xs (n-1)

maxIndex : (vs : Vect n a) -> Integer
maxIndex {n} _ = cast n - 1

infix 5 !
partial
(!) : (vs : Vect n a) -> (ind : Integer) -> a
(!) xs i = case (vindexM_integer xs (maxIndex xs - i)) of
             Just a => a

vreplaceM_integer : (vs : Vect n a) -> (ind : Integer) -> (el : a) -> Maybe (Vect n a)
vreplaceM_integer Nil       _ _ = Nothing
vreplaceM_integer (_ :: xs) 0 y = Just (y :: xs)
vreplaceM_integer (x :: xs) n y = case vreplaceM_integer xs (n-1) y of
                                    Just xs' => Just (x :: xs')
                                    Nothing  => Nothing

partial
vreplace : (vs : Vect n a) -> (ind : Integer) -> (el : a) -> Vect n a
vreplace xs i a = case vreplaceM_integer xs (maxIndex xs - i) a of
                    Just xs' => xs'

max_stars_repo_name: christiaanb/clash-prelude-idris

max_issues_repo_name: christiaanb/clash-prelude-idris

max_forks_repo_name: christiaanb/clash-prelude-idris