text:
module Data.Compress.ZLib

import Data.Compress.Utils.Parser
import Data.Compress.Utils.Bytes
import Data.Compress.Utils.Misc
import Data.Compress.Interface
import Data.Vect
import Data.Bits
import Data.List
import Data.SnocList
import Data.Stream
import Data.Compress.CRC
import Control.Monad.Error.Either

import public Data.Compress.Inflate

public export
data ZLibParserState'
  = ZLibHead
  | ZLibFoot
  | ZLibInflate

public export
data ZLibParserState : ZLibParserState' -> Type where
  AtZHeader : ZLibParserState ZLibHead
  AtInflate : (adler32 : Bits32) -> InflateState -> ZLibParserState ZLibInflate
  AtZFooter : (adler32 : Bits32) -> ZLibParserState ZLibFoot

public export
data ZLibState
  = MkState (List Bits8) (DPair ZLibParserState' ZLibParserState)

nul_term_string : Semigroup e => Parser (List Bits8) e String
nul_term_string = map ascii_to_string $ take_until (0 ==) token

record ZLibFooter where
  constructor MkZLibFooter
  adler32 : Bits32

export
parse_zlib_header : Parser (List Bits8) (SimpleError String) ()
parse_zlib_header = do
  cmf <- token
  flg <- token

  let True = 0 == (((shiftL {a=Bits16} (cast cmf) 8) .|. cast flg) `mod` 31)
  | False => fail $ msg "zlib: fcheck checksum failed"

  let False = testBit flg 5
  | True => fail $ msg "zlib: fdict is set"

  pure ()

update_adler32 : Bits32 -> List Bits8 -> Bits32
update_adler32 alder = go (alder .&. 0xffff) (shiftR alder 16) where
  go : Bits32 -> Bits32 -> List Bits8 -> Bits32
  go a b (x :: xs) =
    let base = 65521
        a' = (a + (cast x)) `mod` base
        b' = (a' + b) `mod` base
    in go a' b' xs
  go a b [] = (shiftL b 16) .|. a

export
parse_zlib_footer : Parser (List Bits8) (SimpleError String) ZLibFooter
parse_zlib_footer = do
  adler32 <- cast <$> p_be_nat 4
  pure (MkZLibFooter adler32)

feed_zlib' : SnocList Bits8 -> DPair ZLibParserState' ZLibParserState -> List Bits8 -> Either String (SnocList Bits8, ZLibState)
feed_zlib' acc (_ ** AtZHeader) [] = Right (acc, MkState [] (_ ** AtZHeader))
feed_zlib' acc (_ ** AtZHeader) content =
  case feed content parse_zlib_header of
    Pure leftover header => feed_zlib' acc (_ ** AtInflate 1 init) leftover
    Fail err => Left $ show err
    _ => Right (acc, MkState content (_ ** AtZHeader))
feed_zlib' acc (_ ** AtInflate adler32 inflate_state) content =
  case feed inflate_state content of
    Left err => Left err
    Right (uncompressed, (MkState _ _ (_ ** AtEnd leftover))) =>
      let adler32 = update_adler32 adler32 uncompressed
      in feed_zlib' (acc <>< uncompressed) (_ ** AtZFooter adler32) (toList leftover)
    Right (uncompressed, inflate_state) => -- underfed
      let adler32 = update_adler32 adler32 uncompressed
      in Right (acc <>< uncompressed, MkState [] (_ ** AtInflate adler32 inflate_state))
feed_zlib' acc (_ ** AtZFooter adler32) content =
  case feed content parse_zlib_footer of
    Pure leftover footer =>
      if footer.adler32 /= adler32
         then Left "adler32 mismatch \{show footer.adler32} \{show adler32}"
        else feed_zlib' acc (_ ** AtZHeader) leftover
    Fail err => Left $ show err
    _ => Right (acc, MkState content (_ ** AtZFooter adler32))

export
Decompressor ZLibState where
  feed (MkState leftover state) input = mapFst toList <$> feed_zlib' Lin state (leftover <+> input)
  done (MkState [] (_ ** AtZHeader)) = Right []
  done (MkState _ (_ ** AtZHeader)) = Left "zlib: leftover data after header"
  done _ = Left "zlib: underfed"
  init = MkState [] (_ ** AtZHeader)


text:
-- | Exercises on Ranges
module Koans.Ranges

rangeNums : Bool
rangeNums = ?fillme1 == [1..13]

stepUp : Bool
stepUp = ?fillme2 == [3,6..20]

stepDown : Bool
stepDown = ?fillme3 [20,17..1]

stopMe : List Integer
stopMe = ?fillme4 [1..]

-- --------------------------------------------------------------------- [ EOF ]

ext: idr

max_stars_repo_name: silky/idris-koans

max_issues_repo_name: silky/idris-koans

max_forks_repo_name: silky/idris-koans


text:
module Desc
data Desc : (0 tI : Type) -> (0 tO : tI -> Type) -> Type where
  End : (i : tI) -> tO i -> Desc tI tO
  Rec : (i : tI) -> (b : tO i -> Desc tI tO) -> Desc tI tO
  Ref : (i : tA -> tI)
    -> ((o : (a : tA) -> tO (i a)) -> Desc tI tO)
    -> Desc tI tO
  Arg : (tA : Type) -> (tA -> Desc tI tO) -> Desc tI tO

el : (d : Desc tI tO)
  -> (tX : tI -> Type )
  -> (tY : {i : tI} -> tX i -> tO i)
  -> tI -> Type
el (End j o) tX tY i = i = j
el (Rec j b) tX tY i = (x : (tX j) ** el (b (tY x)) tX tY i )
el (Ref j b) tX tY i = ( f : ((a : _) -> tX (j a)) ** el (b (\a => tY (f a))) tX tY i)
el (Arg tA b) tX tY i = (a : _ ** el (b a) tX tY i)

mutual
  data Fix : (0 d : Desc tI tO) -> (i : tI) -> Type where
    init : el d (Fix d) (foldO {tI = tI} d) i  -> Fix d i

  foldO : {0 tO : tI -> Type} -> (d : Desc tI tO) -> (1 _ : Fix d i) -> tO i
  foldsO : {0 tO : tI -> Type} -> (1 d : Desc tI tO)
    -> (e : Desc tI tO) -> el d (Fix e) (foldO e) i
    -> tO i

  foldO d (init xs) = foldsO d d xs
  foldsO (End j o) e Refl = o
  foldsO (Rec j b) e (x ** xs) = foldsO (b (foldO e x)) e xs
  foldsO (Ref j b) e (f ** xs) = foldsO (b (\a => foldO e (f a))) e xs
  foldsO (Arg tA b) e (a ** xs) = foldsO (b a) e xs

tHyps : (1 d : Desc tI tO) -> (tX : tI -> Type) -> (tY : {i : tI} -> tX i -> tO i)
  -> (p : {0 i : tI} -> tX i -> Type) -> (i : tI) -> (xs : el d tX tY i) -> Type
tHyps (End j o) tX tY p i x = ()
tHyps (Rec j d) tX tY p i (x ** xs) = (p x , tHyps (d (tY x)) tX tY p i xs)
tHyps (Ref j d) tX tY p i (f ** xs) = ((a : _) -> p (f a) , tHyps (d (\a => tY (f a))) tX tY p i xs)
tHyps (Arg tA b) tX tY p i (a ** xs) = tHyps (b a) tX tY p i xs

mutual
  ind : (d : Desc tI tO)
        -> (0 p : {i : _} -> Fix d i -> Type )
        -> (alpha : {i : _}
              -> (xs : el d (Fix d) (foldO d) i)
              -> (ihs : tHyps d (Fix d) (foldO d) p i xs)
              -> (p (init {i = i} xs)))
        -> {i : tI} -> (x : Fix d i) -> (p x)

  hyps : (d : Desc tI tO) -> (e : Desc tI tO)
    -> (0 p : {i : _} -> Fix e i -> Type)
    -> (alpha : {i : _}
      -> (xs : el e (Fix e) (foldO e) i)
      -> (ihs : tHyps e (Fix e) (foldO e) p i xs)
      -> p (init {i = i} xs))
    -> {i : tI} -> (xs : el d (Fix e) (foldO e) i)
    -> tHyps d (Fix e) (foldO e) p i xs

  ind d p alpha (init xs) = alpha xs (hyps d d p alpha xs)

  hyps (End i o) e p alpha x = ()
  hyps (Rec i b) e p alpha (x ** xs) = (ind e p alpha x , hyps (b (foldO e x)) e p alpha xs)
  hyps (Ref i b) e p alpha (f ** xs) = ((\a => ind e p alpha (f a)), hyps (b (\a => foldO e (f a))) e p alpha xs )
  hyps (Arg tA b) e p alpha (a ** xs) = hyps (b a) e p alpha xs


text:
module PQ.SQL

import public PQ.SQL.Query
import public PQ.SQL.Table
import public PQ.SQL.Type


text:
module Main

import Ncurses

main : IO ()
main = ncursesMain $ (do
  window <- initscr
  cbreak
  noecho
  intrflush window False
  ln <- lines
  cl <- cols
  putStrLn window $ (show ln) ++ " x " ++ (show cl)
  getch window
  -- keypad window True
  endwin)

max_stars_repo_name: zenntenn/idris-curses

max_issues_repo_name: zenntenn/idris-curses

max_forks_repo_name: zenntenn/idris-curses


text:
module Rapid

import Data.List
import Data.String
import System
import System.File

import Compiler.VMCode
import Core.CompileExpr
import Core.Name
import Libraries.Data.SortedMap

import Data.Sexp
import Data.Sexp.Lexer
import Data.Sexp.Parser
import Compiler.GenLLVMIR
import Compiler.Optimize
import Compiler.PrepareCode
import Compiler.VMCodeSexp
import Rapid.Driver

record CliOptions where
  constructor MkOptions
  debugEnabled : Bool
  optimizationsEnabled : Bool
  inputFilename : String

emptyOpts : CliOptions
emptyOpts = MkOptions False False ""

parseCliArgs : List String -> Either String CliOptions
parseCliArgs [] = Left "missing argument"
parseCliArgs (_::args) = go args emptyOpts where
  go : List String -> CliOptions -> Either String CliOptions
  go [] opts = if inputFilename opts /= "" then Right opts else Left "missing input filename"
  go ("--debug"::rest) opts = go rest $ record { debugEnabled = True } opts
  go ("--opt"::rest) opts = go rest $ record { optimizationsEnabled = True } opts
  go (fname::rest) opts = go rest $ record { inputFilename = fname } opts

dumpDef : (Name, VMDef) -> String
dumpDef d = (show $ toSexp d) ++ "\n\n"

main : IO ()
main = do
  args <- getArgs
  (Right opts) <- pure $ parseCliArgs args
  | Left e => putStrLn e

  (Right support) <- readFile "support/rapid/support.ll"
  | Left _ => putStrLn "support.ll not found"

  let debug = debugEnabled opts
  let filename = inputFilename opts
  putStrLn $ "reading input from: " ++ filename

  (Right input) <- readFile filename
  | Left _ => putStrLn "read file error"
  (Right parsed) <- pure (lexSexp input >>= parseSexp)
  | Left e => putStrLn $ "error:\n" ++ e
  (Right allFunctions) <- pure $ getVMDefs (filter isVmdef parsed)
  | Left e => putStrLn $ "error parsing VMCode s-exp: " ++ e
  let foreignSexps = (filter isForeignDecl parsed)
  (Right foreigns) <- pure $ getForeignDefs foreignSexps
  | Left e => putStrLn $ "error parsing foreign decls: " ++ e

  optimizedFunctions <- if opts.optimizationsEnabled
    then do
      let optimized = optimize allFunctions
      let optSexp = map dumpDef (optimized)
      ignore $ writeFile (filename ++ ".opt.sexp") (fastAppend optSexp)
      pure optimized
    else do
      pure allFunctions

  writeIR optimizedFunctions foreigns support (filename ++ ".output.ll") debug

max_stars_repo_name: boxfire/rapid

max_issues_repo_name: boxfire/rapid

max_forks_repo_name: boxfire/rapid


text:
module Text.WebIDL.Types.Identifier

import Data.List1
import Generics.Derive
import Language.Reflection.Refined
import Text.PrettyPrint.Prettyprinter

import public Data.So
import public Decidable.Equality

%default total

%language ElabReflection

--------------------------------------------------------------------------------
--          Keyword Predicates
--------------------------------------------------------------------------------

||| Checks, whether a given string corresponds to a WebIDL
||| argument name keyword.
public export
isArgumentNameKeyword : String -> Bool
isArgumentNameKeyword "async"        = True
isArgumentNameKeyword "attribute"    = True
isArgumentNameKeyword "callback"     = True
isArgumentNameKeyword "const"        = True
isArgumentNameKeyword "constructor"  = True
isArgumentNameKeyword "deleter"      = True
isArgumentNameKeyword "dictionary"   = True
isArgumentNameKeyword "enum"         = True
isArgumentNameKeyword "getter"       = True
isArgumentNameKeyword "includes"     = True
isArgumentNameKeyword "inherit"      = True
isArgumentNameKeyword "interface"    = True
isArgumentNameKeyword "iterable"     = True
isArgumentNameKeyword "maplike"      = True
isArgumentNameKeyword "mixin"        = True
isArgumentNameKeyword "namespace"    = True
isArgumentNameKeyword "partial"      = True
isArgumentNameKeyword "readonly"     = True
isArgumentNameKeyword "required"     = True
isArgumentNameKeyword "setlike"      = True
isArgumentNameKeyword "setter"       = True
isArgumentNameKeyword "static"       = True
isArgumentNameKeyword "stringifier"  = True
isArgumentNameKeyword "typedef"      = True
isArgumentNameKeyword "unrestricted" = True
isArgumentNameKeyword _              = False

isAttributeNameKeyword : String -> Bool
isAttributeNameKeyword "async"    = True
isAttributeNameKeyword "required" = True
isAttributeNameKeyword _          = False

||| Checks, whether a given string corresponds to one
||| of the floating point constants "NaN", "Infinity", or
||| "-Infinity".
public export
isFloatKeyword : String -> Bool
isFloatKeyword "NaN"       = True
isFloatKeyword "Infinity"  = True
isFloatKeyword "-Infinity" = True
isFloatKeyword _           = False

||| Checks, whether a given string corresponds to any WebIDL keyword.
public export
isKeyword : String -> Bool
isKeyword "ArrayBuffer"       = True
isKeyword "ByteString"        = True
isKeyword "DOMString"         = True
isKeyword "DataView"          = True
isKeyword "Float32Array"      = True
isKeyword "Float64Array"      = True
isKeyword "FrozenArray"       = True
isKeyword "Int16Array"        = True
isKeyword "Int32Array"        = True
isKeyword "Int8Array"         = True
isKeyword "ObservableArray"   = True
isKeyword "Promise"           = True
isKeyword "USVString"         = True
isKeyword "Uint16Array"       = True
isKeyword "Uint32Array"       = True
isKeyword "Uint8Array"        = True
isKeyword "Uint8ClampedArray" = True
isKeyword "any"               = True
isKeyword "bigint"            = True
isKeyword "boolean"           = True
isKeyword "byte"              = True
isKeyword "double"            = True
isKeyword "false"             = True
isKeyword "float"             = True
isKeyword "long"              = True
isKeyword "null"              = True
isKeyword "object"            = True
isKeyword "octet"             = True
isKeyword "optional"          = True
isKeyword "or"                = True
isKeyword "record"            = True
isKeyword "sequence"          = True
isKeyword "short"             = True
isKeyword "symbol"            = True
isKeyword "true"              = True
isKeyword "undefined"         = True
isKeyword "unsigned"          = True
isKeyword s =  isArgumentNameKeyword s
            || isFloatKeyword s

--------------------------------------------------------------------------------
--          Keyword
--------------------------------------------------------------------------------

public export
record Keyword where
  constructor MkKeyword
  value : String
  0 isValid : So (isKeyword value)

%runElab refinedString "Keyword"

--------------------------------------------------------------------------------
--          ArgumentNameKeyword
--------------------------------------------------------------------------------

public export
record ArgumentNameKeyword where
  constructor MkArgumentNameKeyword
  value : String
  0 isValid : So (isArgumentNameKeyword value)

%runElab refinedString "ArgumentNameKeyword"

--------------------------------------------------------------------------------
--          AttributeNameKeyword
--------------------------------------------------------------------------------

||| Wrapper for one of the attribute name keywords
public export
record AttributeNameKeyword where
  constructor MkAttributeNameKeyword
  value : String
  0 isValid : So (isAttributeNameKeyword value)

%runElab refinedString "AttributeNameKeyword"

--------------------------------------------------------------------------------
--          Identifier
--------------------------------------------------------------------------------

||| Identifier
public export
record Identifier where
  constructor MkIdent
  value : String

%runElab derive "Identifier" [Generic,Meta,Eq,Ord,Show]

||| IdentifierList :: identifier Identifiers
||| Identifiers :: "," identifier Identifiers | ε
public export
IdentifierList : Type
IdentifierList = List1 Identifier

--------------------------------------------------------------------------------
--          Idris Identifier
--------------------------------------------------------------------------------

||| Checks, if a String corresponds to an Idris2 keyword.
public export
isIdrisKeyword : String -> Bool
isIdrisKeyword "covering"       = True
isIdrisKeyword "data"           = True
isIdrisKeyword "do"             = True
isIdrisKeyword "default"        = True
isIdrisKeyword "else"           = True
isIdrisKeyword "export"         = True
isIdrisKeyword "if"             = True
isIdrisKeyword "implementation" = True
isIdrisKeyword "interface"      = True
isIdrisKeyword "module"         = True
isIdrisKeyword "mutual"         = True
isIdrisKeyword "namespace"      = True
isIdrisKeyword "open"           = True
isIdrisKeyword "parameters"     = True
isIdrisKeyword "partial"        = True
isIdrisKeyword "private"        = True
isIdrisKeyword "prefix"         = True
isIdrisKeyword "public"         = True
isIdrisKeyword "record"         = True
isIdrisKeyword "then"           = True
isIdrisKeyword "total"          = True
isIdrisKeyword "using"          = True
isIdrisKeyword "where"          = True
isIdrisKeyword _                = False

||| Wrapper type making sure that no Idris2 keyword
||| is used as a function's name
public export
data IdrisIdent : Type where
  ||| A string that was successfully checked to be not
  ||| an Idris2 keyword. This can be used without further
  ||| adjustments as an Idris2 identifier.
  II         :  (v : String)
             -> (0 _ : isIdrisKeyword v = False)
             -> IdrisIdent

  ||| Primitive function name. This will be prefixed by
  ||| "prim__" during code generation. As such, the resulting
  ||| identifier always valid in idris.
  Prim       : (v : String) -> IdrisIdent

  ||| Fallback constructor for Idris2 keywords. An underscore
  ||| will be appended to the wrapped string during code generation.
  Underscore : (v : String) -> IdrisIdent

export
Show IdrisIdent where
  show (II v _)       = case strM v of
                             StrCons '_' xs => xs
                             _              => v
  show (Prim v)       = "prim__" ++ v
  show (Underscore v) = v ++ "_"

export
FromString IdrisIdent where
  fromString s with (decEq (isIdrisKeyword s) False)
    fromString s | Yes refl = II s refl
    fromString s | No _     = Underscore s

export
Pretty IdrisIdent where
  pretty = pretty . show

export
fromIdent : Identifier -> IdrisIdent
fromIdent = fromString . value


text:
module Libraries.Text.PrettyPrint.Prettyprinter.Render.HTML

import Data.List
import Data.String

%default covering

export
htmlEscape : String -> String
htmlEscape s = fastAppend $ reverse $ go [] s
  where
    isSafe : Char -> Bool
    isSafe '"' = False
    isSafe '<' = False
    isSafe '>' = False
    isSafe '&' = False
    isSafe '\'' = False
    isSafe '\t' = True
    isSafe '\n' = True
    isSafe '\r' = True
    isSafe c = (c >= ' ' && c <= '~')

    htmlQuote : Char -> String
    htmlQuote '"' = """
    htmlQuote '<' = "<"
    htmlQuote '>' = ">"
    htmlQuote '&' = "&"
    htmlQuote '\'' = "'"
    htmlQuote c = "&#" ++ (show $ ord c) ++ ";"

    go : List String -> String -> List String
    go acc "" = acc
    go acc s =
      case span isSafe s of
           (safe, "") => safe::acc
           (safe, rest) => let c = assert_total (strIndex rest 0)
                               escaped = htmlQuote c in
                               go (escaped::safe::acc) (assert_total $ strTail rest)


text:
describe_list_end : List Int -> String
describe_list_end [] = "Empty"
describe_list_end (xs ++ [x]) = "Non-empty, initial portion = " ++ show xs

max_issues_repo_name: gdevanla/TypeDD-Samples

max_forks_repo_name: gdevanla/TypeDD-Samples


text:
|||
|||
||| Module    : NetList/Check.idr
||| Copyright : (c) Jan de Muijnck-Hughes
||| License   : see LICENSE
|||
module Circuits.NetList.Check

import Decidable.Equality

import Data.Nat
import Data.String
import Data.List.Elem
import Data.List.Quantifiers
import Data.Fin
import Data.Singleton

import Toolkit.Decidable.Informative

import Toolkit.Data.Location
import Toolkit.Data.Whole
import Toolkit.Data.DList
import Toolkit.DeBruijn.Context

import Toolkit.Data.List.AtIndex
import Toolkit.DeBruijn.Context.Item
import Toolkit.DeBruijn.Context
import Toolkit.DeBruijn.Renaming

import Circuits.NetList.Core
import Circuits.NetList.Types
import Circuits.NetList.Terms
import Circuits.NetList.AST

%default total

public export
Context : List Ty -> Type
Context = Context Ty

throw : Check.Error -> NetList a
throw = (throw . TyCheck)

throwAt : FileContext
       -> Check.Error
       -> NetList a
throwAt fc = (Check.throw . Err fc)

embedAt : FileContext
       -> Check.Error
       -> Dec     a
       -> NetList a
embedAt _ _ (Yes prf)
  = pure prf
embedAt fc err (No _)
  = throwAt fc err

embedAtInfo : FileContext
           -> Check.Error
           -> DecInfo e a
           -> NetList   a
embedAtInfo _ _ (Yes prfWhy)
  = pure prfWhy
embedAtInfo fc err (No _ _)
  = throwAt fc err

||| Naive program transformations and checks.
namespace Elab

  export
  getDataType : (fc   : FileContext)
             -> (term : (type ** Term ctxt type))
                     -> NetList DType
  getDataType fc (MkDPair (TyPort (d,x)) snd)
    = pure x
  getDataType fc (MkDPair (TyChan x) snd)
    = pure x
  getDataType fc (MkDPair type snd)
    = throwAt fc PortChanExpected

  ||| Need to make sure that the indices are in the correct direction.
  rewriteTerm : Cast flow expected
             -> Index INOUT
             -> Term ctxt (TyPort (flow,type))
             -> Term ctxt (TyPort (flow,type))
  rewriteTerm c d (Var prf) = Var prf

  rewriteTerm BI (UP UB) (Index idir what idx)
    = Index (UP UB) (rewriteTerm BI (UP UB) what) idx

  rewriteTerm BI (DOWN DB) (Index idir what idx)
    = Index (DOWN DB) (rewriteTerm BI (DOWN DB) what) idx

  rewriteTerm BO (UP UB) (Index idir what idx)
    = Index (UP UB) (rewriteTerm BI (UP UB) what) idx

  rewriteTerm BO (DOWN DB) (Index idir what idx)
    = Index (DOWN DB) (rewriteTerm BI (DOWN DB) what) idx

  rewriteTerm BI _ (Project WRITE _) impossible
  rewriteTerm BO _ (Project WRITE _) impossible
  rewriteTerm BI _ (Project READ _) impossible
  rewriteTerm BO _ (Project READ _) impossible

  rewriteTerm BI _ (Cast BI _) impossible
  rewriteTerm BO _ (Cast BI _) impossible
  rewriteTerm BI _ (Cast BO _) impossible
  rewriteTerm BO _ (Cast BO _) impossible

  ||| When casting we finally know which direction indexing should go,
  ||| so lets fix that.
  shouldCast : {type : DType}
            -> (flow,expected : Direction)
            -> (term : Term ctxt (TyPort (flow,type)))
                    -> Dec ( Cast flow expected
                           , Term ctxt (TyPort (expected,type))
                           )
  shouldCast flow expected term with (Cast.cast flow expected)
    shouldCast INOUT INPUT term | (Yes BI) with (dirFromCast BI)
      shouldCast INOUT INPUT term | (Yes BI) | idir
        = Yes $ MkPair BI (Cast BI (rewriteTerm BI idir term))

    shouldCast INOUT OUTPUT term | (Yes BO) with (dirFromCast BO)
      shouldCast INOUT OUTPUT term | (Yes BO) | idir
        = Yes $ MkPair BO (Cast BO (rewriteTerm BO idir term))

    shouldCast flow expected term | (No contra)
      = No (\(prf,t) => contra prf)

  portCast : {type     : DType}
          -> {flow     : Direction}
          -> (fc       : FileContext)
          -> (expected : Direction)
          -> (term     : Term ctxt (TyPort (flow,type)))
                      -> NetList (Term ctxt (TyPort (expected,type)))

  portCast {type} {flow = flow} fc exp term with (shouldCast flow exp term)
    portCast {type} {flow = flow} fc exp term | Yes (p,e)
      = pure e
    portCast {type} {flow = flow} fc exp term | No contra with (decEq flow exp)
      portCast {type} {flow = exp} fc exp term | No contra | (Yes Refl)
        = pure term
      portCast {type} {flow = flow} fc exp term | No contra | (No f)
        = throwAt fc (Mismatch (TyPort (exp,type))
                               (TyPort (flow,type)))

  export
  checkPort : (fc    : FileContext)
           -> (exdir : Direction)
           -> (expty : DType)
           -> (term  : (type ** Term ctxt type))
                    -> NetList (Term ctxt (TyPort (exdir,expty)))

  -- [ NOTE ]
  --
  checkPort fc exdir exty (MkDPair (TyPort (given,x)) term)
    = do Refl <- embedAt fc
                         (MismatchD exty x)
                         (decEq exty x)

         portCast fc exdir term

  -- [ NOTE ]
  --
  -- READ implies INPUT
  checkPort fc INPUT exty (MkDPair (TyChan x) term)
    = do Refl <- embedAt fc (MismatchD exty x)
                            (decEq exty x)

         pure (Project READ term)

  -- [ NOTE ]
  --
  -- WRITE implies OUTPUT
  checkPort fc OUTPUT exty (MkDPair (TyChan x) term)
    = do Refl <- embedAt fc (MismatchD exty x)
                            (decEq exty x)

         pure (Project WRITE term)

  -- [ NOTE ]
  --
  -- INOUT Chan's impossible.
  checkPort fc INOUT exty (MkDPair (TyChan x) term)
     = throwAt fc (ErrI "INOUT CHAN not expected")

  -- [ NOTE ]
  --
  -- Gates/TyUnit not expected
  checkPort fc exdir exty (MkDPair type term)
     = throwAt fc (Mismatch (TyPort (exdir,exty))
                            type)

  export
  indexDir : {flow : Direction}
          -> (fc   : FileContext)
          -> (term : Term ctxt (TyPort (flow,BVECT (W (S n) ItIsSucc) type)))
                  -> NetList (Index flow)
  indexDir {flow} fc term with (flow)
    indexDir {flow = flow} fc term | INPUT
      = pure (DOWN DI)
    indexDir {flow = flow} fc term | OUTPUT
      = pure (UP UO)
    indexDir {flow = flow} fc (Var prf) | INOUT
      = pure (UP UB)
    indexDir {flow = flow} fc (Index idir what idx) | INOUT
      = pure idir
    indexDir {flow = flow} fc (Project how what) | INOUT
      = throwAt fc (ErrI "Shouldn't happen impossible indexing a projection with inout")
    indexDir {flow = flow} fc (Cast x what) | INOUT
      = throwAt fc (ErrI "Shouldn't happen impossible indexing a cast with inout")

construct : {types : List Ty}
         -> (curr : Context types)
         -> (ast  : AST)
                 -> NetList (DPair Ty (Term types))

construct curr (Var x)
  = do prf <- embedAtInfo (span x)
                          (NotBound (get x))
                          (lookup (get x) curr)

       let (ty ** loc ** idx) = deBruijn prf

       pure (ty ** Var (V loc idx))

construct curr (Port fc flow ty n body)
  = do (TyUnit ** term) <- construct (extend curr (get n) (TyPort (flow, ty)))
                                     body
         | (ty ** _) => throwAt fc (Mismatch TyUnit ty)

       pure (_ ** Port flow ty term)

construct curr (Wire fc ty n body)

  = do (TyUnit ** term) <- construct (extend curr (get n) (TyChan ty))
                                     body
         | (ty ** _) => throwAt fc (Mismatch TyUnit ty)

       pure (_ ** Wire ty term)

construct curr (GateDecl fc n g body)
  = do (TyGate ** gate) <- construct curr g
         | (type ** _) => throwAt fc (Mismatch TyGate type)

       (TyUnit ** term) <- construct (extend curr (get n) TyGate)
                                     body
         | (type ** _) => throwAt fc (Mismatch TyUnit type)

       pure (_ ** GateDecl gate term)

construct curr (Shim fc dir thing)
  = do t <- construct curr thing

       dtype <- getDataType fc t

       term <- checkPort fc dir dtype t

       pure (_ ** term)

construct curr (Assign fc o i rest)
  =  do termI <- construct curr i

        ity <- getDataType fc termI

        termO <- construct curr o

        oty <- getDataType fc termO

        Refl <- embedAt fc (MismatchD ity oty)
                           (decEq ity oty)

        o' <- checkPort fc OUTPUT ity termO

        i' <- checkPort fc INPUT  ity termI

        (TyUnit ** r') <- construct curr rest
          | (type ** _) => throwAt fc (Mismatch TyUnit type)

        pure (_ ** Assign o' i' r')

construct curr (Mux fc o c l r)
  = do termO <- construct curr o
       termC <- construct curr c
       termL <- construct curr l
       termR <- construct curr r

       o' <- checkPort fc OUTPUT LOGIC termO
       c' <- checkPort fc INPUT  LOGIC termC
       l' <- checkPort fc INPUT  LOGIC termL
       r' <- checkPort fc INPUT  LOGIC termR

       pure (_ ** Mux o' c' l' r')

construct curr (GateU fc k o i)

  = do termO <- construct curr o
       termI <- construct curr i

       o' <- checkPort fc OUTPUT LOGIC termO
       i' <- checkPort fc INPUT  LOGIC termI

       pure (_ ** GateU k o' i')

construct curr (GateB fc k o l r)

  = do termO <- construct curr o
       termL <- construct curr l
       termR <- construct curr r

       o' <- checkPort fc OUTPUT LOGIC termO
       l' <- checkPort fc INPUT  LOGIC termL
       r' <- checkPort fc INPUT  LOGIC termR

       pure (_ ** GateB k o' l' r')

construct curr (Index fc idx t)

  = do (TyPort (flow,BVECT (W (S n) ItIsSucc) type) ** term) <- construct curr t
         | (type ** term)
             => throwAt fc VectorExpected

       case natToFin idx (S n) of
         Nothing => throw (OOB idx (S n))
         Just idx' => do idir <- indexDir fc term
                         pure (_ ** Index idir term idx')

construct curr (Split fc a b i)

  = do termA <- construct curr a
       termB <- construct curr b
       termI <- construct curr i

       a' <- checkPort fc OUTPUT LOGIC termA
       b' <- checkPort fc OUTPUT LOGIC termB
       i' <- checkPort fc INPUT  LOGIC termI

       pure (_ ** Split a' b' i')

construct curr (Collect fc o l r)

  = do (TyPort (OUTPUT,BVECT (W (S (S Z)) ItIsSucc) type) ** o') <- construct curr o
         | (TyPort (flow,BVECT (W (S (S n)) ItIsSucc) type) ** term)
             => throwAt fc (Mismatch (TyPort (OUTPUT, BVECT (W (S (S Z)) ItIsSucc) type))
                                     (TyPort (flow,   BVECT (W (S (S n)) ItIsSucc) type))
                                       )
         | (type ** term)
             => throwAt fc VectorExpected

       termL <- construct curr l
       termR <- construct curr r

       l' <- checkPort fc INPUT type termL
       r' <- checkPort fc INPUT type termR

       pure (_ ** Collect o' l' r')

construct curr (Stop fc)
  = pure (_ ** Stop)

namespace Design
  export
  check : (ast : AST) -> NetList (Term Nil TyUnit)
  check ast
    = do (TyUnit ** term) <- construct Nil ast
           | (ty ** term) => throw (Mismatch TyUnit ty)
         pure term

-- [ EOF ]

max_stars_repo_name: border-patrol/linear-circuits

max_issues_repo_name: border-patrol/linear-circuits

max_forks_repo_name: border-patrol/linear-circuits


text:
module Test.Suite

import IdrTest.Test

import Test.FmtTest

suite : IO ()
suite = do
  runSuites
    [ Test.FmtTest.suite
    ]

max_stars_repo_name: Z-snails/inigo

max_issues_repo_name: Z-snails/inigo

max_forks_repo_name: Z-snails/inigo


text:
module Specifications.OrderedRing

import public Specifications.Ring
import public Specifications.TranslationInvariance
import public Specifications.DiscreteOrderedGroup

%default total
%access public export

||| composed specification
||| todo: multiplication of positive elements is positive
data PartiallyOrderedRingSpec :
  Binop s -> s -> (s -> s) -> Binop s -> Binrel s -> Type
  where MkPartiallyOrderedRing :
    RingSpec add zero neg mul ->
    PartiallyOrderedMagmaSpec add leq ->
    PartiallyOrderedRingSpec add zero neg mul leq

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

||| forget
partiallyOrderedGroup : PartiallyOrderedRingSpec add zero neg _ leq ->
  PartiallyOrderedGroupSpec add zero neg leq
partiallyOrderedGroup (MkPartiallyOrderedRing r o) =
  MkPartiallyOrderedGroup (group (abelianGroup r)) o

||| composed specification
data OrderedRingSpec :
  Binop s -> s -> (s -> s) -> Binop s -> Binrel s -> Type
  where MkOrderedRing :
    PartiallyOrderedRingSpec add zero neg mul leq ->
    isTotalOrder leq ->
    OrderedRingSpec add zero neg mul leq

namespace ForgetOrder
  ring : OrderedRingSpec add zero neg mul _ -> RingSpec add zero neg mul
  ring (MkOrderedRing r _) = ring r

||| forget
orderedGroup : OrderedRingSpec add zero neg _ leq ->
  OrderedGroupSpec add zero neg leq
orderedGroup (MkOrderedRing r t) = MkOrderedGroup (partiallyOrderedGroup r) t

||| composed specification
data DiscreteOrderedRingSpec :
  Binop s -> s -> (s -> s) -> Binop s -> Binrel s -> s -> Type
  where MkDiscreteOrderedRing :
    OrderedRingSpec add zero neg mul leq ->
    isDiscreteOrder add leq zero one ->
    isNeutralL mul one ->
    isNeutralR mul one ->
    (onePositive : leq zero one) ->
    DiscreteOrderedRingSpec add zero neg mul leq one

||| forget
discreteOrderedGroup : DiscreteOrderedRingSpec add zero neg _ leq one ->
  DiscreteOrderedGroupSpec add zero neg leq one
discreteOrderedGroup (MkDiscreteOrderedRing r d _ _ _) =
  MkDiscreteOrderedGroup (orderedGroup r) (abelian (abelianGroup (ring r))) d

||| forget
unitalRing : DiscreteOrderedRingSpec add zero neg mul _ one ->
  UnitalRingSpec add zero neg mul one
unitalRing (MkDiscreteOrderedRing or _ l r _) = MkUnitalRing (ring or) l r

||| forget
onePositive : DiscreteOrderedRingSpec _ zero _ _ leq one -> leq zero one
onePositive (MkDiscreteOrderedRing _ _ _ _ pos) = pos

max_stars_repo_name: jeroennoels/verified-algebra

max_issues_repo_name: jeroennoels/verified-algebra

max_forks_repo_name: jeroennoels/verified-algebra


text:
module UnbalancedSet

import Set

%default total
%access private

export
data UnbalancedSet a = E | T (UnbalancedSet a) a (UnbalancedSet a)

export
Ord a => Set UnbalancedSet a where
  empty = E

  member x E = False
  member x (T a y b) = case compare x y of
    LT => member x a
    GT => member x b
    EQ => True

  insert x E = T E x E
  insert x s@(T a y b) = case compare x y of
    LT => T (insert x a) y b
    GT => T a y (insert x b)
    EQ => s


text:
module Data.ZZ

import Decidable.Equality

%default total
%access public

||| An integer is either a positive `Nat` or the negated successor of a `Nat`.
|||
||| For example, 3 is `Pos 3` and -2 is `NegS 1`. Zero is arbitrarily chosen
||| to be positive.
|||
data ZZ = Pos Nat | NegS Nat

||| Take the absolute value of a `ZZ`
absZ : ZZ -> Nat
absZ (Pos n) = n
absZ (NegS n) = S n

instance Show ZZ where
  show (Pos n) = show n
  show (NegS n) = "-" ++ show (S n)

negNat : Nat -> ZZ
negNat Z = Pos Z
negNat (S n) = NegS n

||| Construct a `ZZ` as the difference of two `Nat`s
minusNatZ : Nat -> Nat -> ZZ
minusNatZ n Z = Pos n
minusNatZ Z (S m) = NegS m
minusNatZ (S n) (S m) = minusNatZ n m

||| Add two `ZZ`s. Consider using `(+) {a=ZZ}`.
plusZ : ZZ -> ZZ -> ZZ
plusZ (Pos n) (Pos m) = Pos (n + m)
plusZ (NegS n) (NegS m) = NegS (S (n + m))
plusZ (Pos n) (NegS m) = minusNatZ n (S m)
plusZ (NegS n) (Pos m) = minusNatZ m (S n)

instance Eq ZZ where
  (Pos n) == (Pos m) = n == m
  (NegS n) == (NegS m) = n == m
  _ == _ = False

instance Ord ZZ where
  compare (Pos n) (Pos m) = compare n m
  compare (NegS n) (NegS m) = compare m n
  compare (Pos _) (NegS _) = GT
  compare (NegS _) (Pos _) = LT

||| Multiply two `ZZ`s. Consider using `(*) {a=ZZ}`.
multZ : ZZ -> ZZ -> ZZ
multZ (Pos n) (Pos m) = Pos $ n * m
multZ (NegS n) (NegS m) = Pos $ (S n) * (S m)
multZ (NegS n) (Pos m) = negNat $ (S n) * m
multZ (Pos n) (NegS m) = negNat $ n * (S m)

||| Convert an `Integer` to an inductive representation.
fromInt : Integer -> ZZ
fromInt n = if n < 0
            then NegS $ fromInteger {a=Nat} ((-n) - 1)
            else Pos $ fromInteger {a=Nat} n

instance Cast Nat ZZ where
  cast n = Pos n

instance Num ZZ where
  (+) = plusZ
  (*) = multZ
  fromInteger = fromInt

mutual
  instance Neg ZZ where
    negate (Pos Z)     = Pos Z
    negate (Pos (S n)) = NegS n
    negate (NegS n)    = Pos (S n)

    (-) = subZ
    abs = cast . absZ

  ||| Subtract two `ZZ`s. Consider using `(-) {a=ZZ}`.
  subZ : ZZ -> ZZ -> ZZ
  subZ n m = plusZ n (negate m)

instance Cast ZZ Integer where
  cast (Pos n) = cast n
  cast (NegS n) = (-1) * (cast n + 1)

instance Cast Integer ZZ where
  cast = fromInteger

--------------------------------------------------------------------------------
-- Properties
--------------------------------------------------------------------------------

natPlusZPlus : (n : Nat) -> (m : Nat) -> (x : Nat)
             -> n + m = x -> (Pos n) + (Pos m) = Pos x
natPlusZPlus n m x h = cong h

natMultZMult : (n : Nat) -> (m : Nat) -> (x : Nat)
             -> n * m = x -> (Pos n) * (Pos m) = Pos x
natMultZMult n m x h = cong h

doubleNegElim : (z : ZZ) -> negate (negate z) = z
doubleNegElim (Pos Z) = Refl
doubleNegElim (Pos (S n)) = Refl
doubleNegElim (NegS Z) = Refl
doubleNegElim (NegS (S n)) = Refl

-- Injectivity
posInjective : Pos n = Pos m -> n = m
posInjective Refl = Refl

negSInjective : NegS n = NegS m -> n = m
negSInjective Refl = Refl

posNotNeg : Pos n = NegS m -> Void
posNotNeg Refl impossible

-- Decidable equality
instance DecEq ZZ where
  decEq (Pos n) (NegS m) = No posNotNeg
  decEq (NegS n) (Pos m) = No $ negEqSym posNotNeg
  decEq (Pos n) (Pos m) with (decEq n m)
    | Yes p = Yes $ cong p
    | No p = No $ \h => p $ posInjective h
  decEq (NegS n) (NegS m) with (decEq n m)
    | Yes p = Yes $ cong p
    | No p = No $ \h => p $ negSInjective h

-- Plus
plusZeroLeftNeutralZ : (right : ZZ) -> 0 + right = right
plusZeroLeftNeutralZ (Pos n) = Refl
plusZeroLeftNeutralZ (NegS n) = Refl

plusZeroRightNeutralZ : (left : ZZ) -> left + 0 = left
plusZeroRightNeutralZ (Pos n) = cong $ plusZeroRightNeutral n
plusZeroRightNeutralZ (NegS n) = Refl

plusCommutativeZ : (left : ZZ) -> (right : ZZ) -> (left + right = right + left)
plusCommutativeZ (Pos n) (Pos m) = cong $ plusCommutative n m
plusCommutativeZ (Pos n) (NegS m) = Refl
plusCommutativeZ (NegS n) (Pos m) = Refl
plusCommutativeZ (NegS n) (NegS m) = cong {f=NegS} $ cong {f=S} $ plusCommutative n m

max_stars_repo_name: fieldstrength/xquant

max_issues_repo_name: fieldstrength/xquant

max_forks_repo_name: fieldstrength/xquant


text:
import Data.Vect

-- Data type definition

-- Enumeration
data LightSwitch = On | Off

toggle : LightSwitch -> LightSwitch
toggle On = Off
toggle Off = On

-- Union, basically an email where members can have values
data Shape =
  Triangle Double Double |
  Rectangle Double Double |
  Circle Double

-- Recursive
data Nat2 = Z2 | S Nat2

-- List looks like
-- data List elem = Nil | (::) elem (List elem)

data Tree elem =
  Empty |
  Node (Tree elem) elem (Tree elem)
%name Tree tree, tree2

-- inserting into a binary search tree, not caring about balancing
-- Ord elem => means restrict elem to types that there is an Ord for, so
-- we can compare two values.
insert : Ord elem => elem -> Tree elem -> Tree elem
insert x Empty = Node Empty x Empty
insert x original@(Node left y right) = case compare x y of
  LT => Node (insert x left) y right
  EQ => original
  GT => Node left y (insert x right)

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

-- Exercise 2
treeToList : Tree a -> List a
treeToList Empty = []
treeToList (Node left x right) = treeToList left ++ [x] ++ treeToList right

-- *Chapter4> treeToList (listToTree [4,1,8,7,2,3,5,9,6])
-- [1, 2, 3, 4, 5, 6, 7, 8, 9] : List Integer

-- Exercise 3
data Expr =
  EInt Integer |
  EAdd Expr Expr |
  ESub Expr Expr |
  EMul Expr Expr

-- Exercise 4
evaluate : Expr -> Integer
evaluate (EInt x) = x
evaluate (EAdd x y) = evaluate x + evaluate y
evaluate (ESub x y) = evaluate x - evaluate y
evaluate (EMul x y) = evaluate x * evaluate y

-- Exercise 5
maxMaybe : Ord a => Maybe a -> Maybe a -> Maybe a
maxMaybe Nothing y = y
maxMaybe (Just x) Nothing = Just x
maxMaybe (Just x) (Just y) = Just (max x y)

-- Exercise 6
-- Biggest triangle's area.
shapeArea : Shape -> Double
shapeArea (Triangle base height) = 0.5 * base * height
shapeArea (Rectangle x y) = x * y
shapeArea (Circle radius) = pi * radius * radius

data Picture =
  Primitive Shape |
  Combine Picture Picture |
  Rotate Double Picture |
  Translate Double Double Picture

pictureArea : Picture -> Double
pictureArea (Primitive shape) = shapeArea shape
pictureArea (Combine x y) = pictureArea x + pictureArea y
pictureArea (Rotate angle picture) = pictureArea picture
pictureArea (Translate x y picture) = pictureArea picture

biggestTriangle : Picture -> Maybe Double
biggestTriangle (Primitive shape@(Triangle x y)) = Just (shapeArea shape)
biggestTriangle (Primitive (Rectangle x y)) = Nothing
biggestTriangle (Primitive (Circle x)) = Nothing
biggestTriangle (Combine x y) = maxMaybe (biggestTriangle x) (biggestTriangle y)
biggestTriangle (Rotate angle picture) = biggestTriangle picture
biggestTriangle (Translate x y picture) = biggestTriangle picture

-- Dependent Types
-- From Data.Vect
-- data Vect : Nat -> Type -> Type
-- A list whose length is in its type.

data PowerSource = Petrol | Pedal | Electric

data Vehicle : PowerSource -> Type where
  Bicycle : Vehicle Pedal
  Car : (fuel : Nat) -> Vehicle Petrol
  Bus : (fuel : Nat) -> Vehicle Petrol
  Unicycle : Vehicle Pedal
  Motorcycle : (fuel : Nat) -> Vehicle Petrol
  Tram : (wheels : Nat) -> Vehicle Electric

wheels : Vehicle power -> Nat
wheels Bicycle = 2
wheels (Car fuel) = 4
wheels (Bus fuel) = 4
wheels Unicycle = 1
wheels Motorcycle = 2
wheels (Tram wheels) = wheels

refuel : Vehicle Petrol -> Vehicle Petrol
refuel (Car fuel) = Car 100
refuel (Bus fuel) = Bus 200
refuel Bicycle impossible -- compile time check that something wouldn't compile
refuel (Motorcycle fuel) = Motorcycle 50

append : Vect n elem -> Vect m elem -> Vect (n + m) elem
append [] ys = ys
append (x :: xs) ys = x :: append xs ys

zip2 : Vect n a -> Vect n b -> Vect n (a, b)
zip2 [] [] = []
zip2 (x :: xs) (y :: ys) = (x, y) :: zip xs ys

index2 : Fin n -> Vect n elem -> elem
index2 FZ (x :: xs) = x
index2 (FS k) (x :: xs) = index2 k xs

tryIndex : Integer -> Vect n a -> Maybe a
tryIndex {n} index vect = case integerToFin index n of
  Nothing => Nothing
  Just x => Just (index2 x vect)

-- Exercise 3 and 4 (1 and 2 are embedded above)
vectTake : (n : Nat) -> Vect (n + m) elem -> Vect n elem
vectTake Z xs = []
vectTake (S k) (x :: xs) = x :: vectTake k xs

-- Exercise 5
sumEntries : Num a => (pos : Integer) -> Vect n a -> Vect n a -> Maybe a
sumEntries {n} pos xs ys = case integerToFin pos n of
  Nothing => Nothing
  Just index => Just (index2 index xs + index2 index ys)

max_stars_repo_name: rickyclarkson/idris-playground

max_issues_repo_name: rickyclarkson/idris-playground

max_forks_repo_name: rickyclarkson/idris-playground


text:
module RFC.Knock

import Effects
import Effect.StdIO
import Effect.Default
import Effect.State

import System.Protocol
import RFC.Utils

%access public

knockknock : Protocol ['Client, 'Server] ()
knockknock = do
  'Client ==> 'Server | Literal "Knock Knock"
  'Server ==> 'Client | Literal "Who's there?"
  res <- 'Client ==> 'Server | String
  'Server ==> 'Client | Literal (res ++ " who?")
  'Client ==> 'Server | String
  Done

-- --------------------------------------------------------------------- [ EOF ]

max_stars_repo_name: jfdm/idris-protocol-examples

max_issues_repo_name: jfdm/idris-protocol-examples

max_forks_repo_name: jfdm/idris-protocol-examples


text:
module Exercises.Chapter7

import Exercises.Chapter4 -- For Shape

%access public export

-- Exercise 7.1.6.1

Eq Shape where
  (==) (Triangle  b1 h1) (Triangle  b2 h2) = b1 == b2 && h1 == h2
  (==) (Triangle  _  _)   _                = False
  (==) (Rectangle w1 h1) (Rectangle w2 h2) = w1 == w2 && h1 == h2
  (==) (Rectangle _  _)   _                = False
  (==) (Circle    r1)    (Circle r2)       = r1 == r2
  (==) (Circle    _)      _                = False

-- Exercise 7.1.6.2

Ord Shape where
 compare x y = compare (area x) (area y)

data Expr num = Val num
              | Add (Expr num) (Expr num)
              | Sub (Expr num) (Expr num)
              | Mul (Expr num) (Expr num)
              | Div (Expr num) (Expr num)
              | Abs (Expr num)

eval : (Integral num, Neg num) => Expr num -> num
eval (Val x)   = x
eval (Add x y) = eval x + eval y
eval (Sub x y) = eval x - eval y
eval (Mul x y) = eval x * eval y
eval (Div x y) = eval x `div` eval y
eval (Abs x)   = abs (eval x)

Num ty => Num (Expr ty) where
    (+) = Add
    (*) = Mul

    fromInteger = Val . fromInteger

Neg ty => Neg (Expr ty) where
    negate x = 0 - x
    (-) = Sub
    abs = Abs

Cast (Maybe elem) (List elem) where
     cast Nothing  = []
     cast (Just x) = [x]

-- Exercise 7.2.4.1

Show num => Show (Expr num) where
  show (Val x)   = show x
  show (Add x y) = "(" ++ show x ++ " + " ++ show y ++ ")"
  show (Sub x y) = "(" ++ show x ++ " - " ++ show y ++ ")"
  show (Mul x y) = "(" ++ show x ++ " * " ++ show y ++ ")"
  show (Div x y) = "(" ++ show x ++ " / " ++ show y ++ ")"
  show (Abs x)   = "|" ++ show x ++ "|"

-- Exercise 7.2.4.2

(Eq num, Integral num, Neg num) => Eq (Expr num) where
  (==) x y = eval x == eval y

-- textExprEq1 : True  = the (Expr _) (2 + 4) == 3 + 3
-- textExprEq2 : False = the (Expr _) (2 + 4) == 3 + 4

-- Exercise 7.2.4.3

(Integral num, Neg num) => Cast (Expr num) num where
  cast = eval

-- Exercise 7.3.4.1

Functor Expr where
  map f (Val x)   = Val (f x)
  map f (Add x y) = Add (map f x) (map f y)
  map f (Sub x y) = Sub (map f x) (map f y)
  map f (Mul x y) = Mul (map f x) (map f y)
  map f (Div x y) = Div (map f x) (map f y)
  map f (Abs x)   = Abs (map f x)

-- Exercise 7.3.4.2

namespace MyVect
  data Vect : Nat -> Type -> Type where
    Nil  : Vect 0 a
    (::) : (x : a) -> (xs : Vect k a) -> Vect (S k) a

  Eq a => Eq (Vect n a) where
    (==) []      []      = True
    (==) (x::xs) (y::ys) = (x == y) && (xs == ys)

  Foldable (Vect n) where
    foldl _ z []      = z
    foldl f z (x::xs) = foldl f (f z x) xs
    foldr _ z []      = z
    foldr f z (x::xs) = f x $ foldr f z xs

max_stars_repo_name: yurrriq/tdd-with-idris

max_issues_repo_name: yurrriq/tdd-with-idris

max_forks_repo_name: yurrriq/tdd-with-idris


text:
%default total

data Singleton : {a : Type} -> a -> Type where
  Val : (x : a) -> Singleton x

-- data constructors
f : Singleton (MkPair True) -> Bool
f (Val _) = True

-- type constructors
g : Singleton Maybe -> Bool
g (Val _) = True


text:
module Language.LSP.CodeAction.Utils

import Core.Core
import Core.Context.Context
import Language.LSP.CodeAction
import Language.LSP.Message.CodeAction
import Language.LSP.Message.Location
import Server.Configuration
import Server.Log
import Server.Utils

||| Check for code actions that require the request to be on a single line.
||| @topic Logging topic of the code action
||| @params Code action params
||| @onErr Default value returned in case of error
||| @onOk Function that handles the single line
export
withSingleLine : Ref LSPConf LSPConfiguration
              => (topic : Topic)
              -> (params : CodeActionParams)
              -> (onErr : Core r)
              -> (onOk : Int -> Core r)
              -> Core r
withSingleLine topic params onErr onOk =
  let startLine = params.range.start.line
      endLine = params.range.end.line
   in case startLine == endLine of
           True => onOk startLine
           False => do logW topic "The action requires a single line but provided the range \{show startLine} - \{show endLine}"
                       onErr

||| Check for a single cached code action for the given request type.
||| @topic Logging topic of the code action
||| @params Code action params
||| @action Tag of the cached code action
||| @new Handler for cache misses
export
withSingleCache : Ref LSPConf LSPConfiguration
               => (topic : Topic)
               -> (params : CodeActionParams)
               -> (action : IdrisAction)
               -> (new : Core (Maybe (Range, CodeAction)))
               -> Core (Maybe CodeAction)
withSingleCache topic params action new =
  case !(searchCache params.range action) of
       [] => do Just (loc, act) <- new
                  | Nothing => pure Nothing
                update LSPConf ({ cachedActions $= insert (loc, action, [act]) })
                pure $ Just act
       act :: _ => do logD topic "Found cached action"
                      pure $ Just act

||| Check for a multiple cached code actions for the given request type.
||| @topic Logging topic of the code action
||| @params Code action params
||| @action Tag of the cached code action
||| @new Handler for cache misses
export
withMultipleCache : Ref LSPConf LSPConfiguration
                 => (topic : Topic)
                 -> (params : CodeActionParams)
                 -> (action : IdrisAction)
                 -> (new : Core (List (Range, List CodeAction)))
                 -> Core (List CodeAction)
withMultipleCache topic params action new =
  case !(searchCache params.range action) of
       [] => do locs <- new
                for_ locs $ \(loc, acts) =>
                  update LSPConf ({ cachedActions $= insert (loc, action, acts) })
                pure $ concat $ snd <$> locs
       acts => do logD topic "Found cached action"
                  pure acts


text:
module Data.Tree.Perfect

import Control.WellFounded
import Decidable.Order.Strict
import Data.Monoid.Exponentiation
import Data.Num.Implementations
import Data.Nat.Views
import Data.Nat
import Data.Nat.Order
import Data.Nat.Order.Strict
import Data.Nat.Order.Properties
import Data.Nat.Exponentiation
import Data.DPair
import Syntax.WithProof
import Syntax.PreorderReasoning.Generic

%default total

public export
data Tree : Nat -> Type -> Type where
  Leaf : a -> Tree Z a
  Node : Tree n a -> Tree n a -> Tree (S n) a

public export
Functor (Tree n) where
  map f (Leaf a) = Leaf (f a)
  map f (Node l r) = Node (map f l) (map f r)

public export
replicate : (n : Nat) -> a -> Tree n a
replicate Z a = Leaf a
replicate (S n) a = let t = replicate n a in Node t t

public export
{n : _} -> Applicative (Tree n) where
  pure = replicate n

  Leaf f <*> Leaf a = Leaf (f a)
  Node fl fr <*> Node xl xr = Node (fl <*> xl) (fr <*> xr)

public export
data Path : Nat -> Type where
  Here  : Path Z
  Left  : Path n -> Path (S n)
  Right : Path n -> Path (S n)

public export
toNat : {n : _} -> Path n -> Nat
toNat Here = Z
toNat (Left p) = toNat p
toNat {n = S n} (Right p) = toNat p + pow2 n

export
toNatBounded : (n : Nat) -> (p : Path n) -> toNat p `LT` pow2 n
toNatBounded Z Here = reflexive {rel = LTE}
toNatBounded (S n) (Left p) = CalcWith $
  |~ S (toNat p)
  <~ pow2 n          ...( toNatBounded n p )
  <~ pow2 n + pow2 n ...( lteAddRight (pow2 n) )
  ~~ pow2 (S n)      ...( sym unfoldPow2 )
toNatBounded (S n) (Right p) = CalcWith $
  let ih = toNatBounded n p in
  |~ S (toNat p) + pow2 n
  <~ pow2 n + pow2 n      ...( plusLteMonotoneRight _ _ _ ih )
  ~~ pow2 (S n)           ...( sym unfoldPow2 )

namespace FromNat

  ||| This pattern-matching in `fromNat` is annoying:
  ||| The    `Z (S _)` case is impossible
  ||| In the `k (S n)` case we want to branch on whether `k `LT` pow2 n`
  ||| and get our hands on some proofs.
  ||| This view factors out that work.
  public export
  data View : (k, n : Nat) -> Type where
    ZZ   : View Z Z
    SLT  : (0 p : k `LT` pow2 n) -> View k (S n)
    SNLT : (0 p : k `GTE` pow2 n) ->
           (0 rec : minus k (pow2 n) `LT` pow2 n) -> View k (S n)

  public export
  view : (k, n : Nat) -> (0 _ : k `LT` (pow2 n)) -> View k n
  view Z Z p = ZZ
  view (S _) Z p = void $ absurd (fromLteSucc p)
  view k (S n) p with (@@ lt k (pow2 n))
    view k (S n) p | (True ** eq) = SLT (ltIsLT k (pow2 n) eq)
    view k (S n) p | (False ** eq) = SNLT gte prf where

      0 gte : k `GTE` pow2 n
      gte = notLTImpliesGTE (notltIsNotLT k (pow2 n) eq)

      0 prf : minus k (pow2 n) `LT` pow2 n
      prf = CalcWith $
        |~ S (minus k (pow2 n))
        <~ minus (pow2 (S n)) (pow2 n)
           ...( minusLtMonotone p pow2Increasing )
        ~~ minus (pow2 n + pow2 n) (pow2 n)
           ...( cong (\ m => minus m (pow2 n)) unfoldPow2 )
        ~~ pow2 n
           ...( minusPlus (pow2 n) )

||| Convert a natural number to a path in a perfect binary tree
public export
fromNat : (k, n : Nat) -> (0 _ : k `LT` pow2 n) -> Path n
fromNat k n p with (view k n p)
  fromNat Z Z p | ZZ = Here
  fromNat k (S n) p | SLT lt = Left (fromNat k n lt)
  fromNat k (S n) p | SNLT _ lt = Right (fromNat (minus k (pow2 n)) n lt)

||| The `fromNat` conversion is compatible with the semantics `toNat`
export
fromNatCorrect : (k, n : Nat) -> (0 p : k `LT` pow2 n) ->
                 toNat (fromNat k n p) === k
fromNatCorrect k n p with (view k n p)
  fromNatCorrect Z Z p | ZZ = Refl
  fromNatCorrect k (S n) p | SLT lt = fromNatCorrect k n lt
  fromNatCorrect k (S n) p | SNLT gte lt
     = rewrite fromNatCorrect (minus k (pow2 n)) n lt in
       irrelevantEq $ plusMinusLte (pow2 n) k gte

public export
lookup : Tree n a -> Path n -> a
lookup (Leaf a) Here = a
lookup (Node l _) (Left p) = lookup l p
lookup (Node _ r) (Right p) = lookup r p


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

{-
 Str (Lit "=" (Number End))
 represents the format string "%s = %d"
-}

PrintfType : Format -> Type
PrintfType (Number rest) = Int -> PrintfType rest
PrintfType (Str rest) = String -> PrintfType rest
PrintfType (Lit _ rest) = PrintfType rest
PrintfType End = String

printfFmt : (fmt : Format) -> (acc : String) -> PrintfType fmt
printfFmt (Number rest) acc = \i => printfFmt rest (acc ++ show i)
printfFmt (Str rest) acc = \s => printfFmt rest (acc ++ s)
printfFmt (Lit str rest) acc = printfFmt rest (acc ++ str)
printfFmt End acc = acc

toFormat : List Char -> Format
toFormat [] = End
toFormat ('%' :: 'd' :: rest) = Number (toFormat rest)
toFormat ('%' :: 'a' :: rest) = Str (toFormat rest)
toFormat ('%' :: rest) = Lit "%" (toFormat rest)
toFormat (c :: rest) = case toFormat rest of
                            Lit str rest' => Lit (strCons c str) rest'
                            rest' => Lit (strCons c "") rest'

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

max_stars_repo_name: brunoflores/type-driven-with-idris

max_issues_repo_name: brunoflores/type-driven-with-idris

max_forks_repo_name: brunoflores/type-driven-with-idris


text:
import Data.Vect

nums : List (Int, Int)
nums = [(1, 2), (3, 4), (5, 6)]

addToNums : List (Int, Int) -> List (Int, Int)
addToNums = map (\ (x, y) => (x + 1, y + 1))

vects : List (n ** Vect n Int)
vects = [(_ ** [1,2,3]),
         (_ ** [1,2,3,4]),
         (_ ** [1,2,3,4,5])]

lengths : List (n ** Vect n a) -> List Nat
lengths = map (\ (len ** xs) => length xs)


text:
module TyTTP.Core.Step

import Control.Monad.Trans
import TyTTP.Core.Request
import TyTTP.Core.Response

public export
record Step me u h1 s h2 a b where
  constructor MkStep
  request : Request me u h1 a
  response : Response s h2 b

export
Functor (Step me u h1 s h2 a) where
  map f step = { response $= map f } step

export
Bifunctor (Step me u h1 s h2) where
  bimap f g step = { request $= map f, response $= map g } step

infixr 0 :>, :>>

export
(:>) : MonadTrans t
  => Monad m
  => (f : (a -> (t m) b) -> c)
  -> (handler : a -> m b)
  -> c
(:>) f handler = f $ \a => lift $ handler a

export
(:>>) : MonadTrans t1
  => MonadTrans t2
  => Monad m
  => Monad (t1 m)
  => (f : (a -> (t2 (t1 m)) b) -> c)
  -> (handler : a -> m b)
  -> c
(:>>) f handler = f $ \a => lift $ lift $ handler a

max_stars_repo_name: kbertalan/tyttp

max_issues_repo_name: kbertalan/tyttp

max_forks_repo_name: kbertalan/tyttp


text:
module ContriverText.Tests

import Data.SortedSet
import Effects
import Effect.System

import ContriverText
import ContriverText.JsUtil

quoteListOfStrings : List String -> TT
quoteListOfStrings [] = `([] : List String)
quoteListOfStrings (x :: xs) =
  `((~(TConst (Str x)) :: ~(quoteListOfStrings xs)) : List String)

bindingToStrings : (TTName, Binder TT) -> List String
bindingToStrings (UN v, t) = [v]
bindingToStrings _ = []

-- The failure message is based on idris-dev's
-- test/quasiquote004/Quasiquote004.idr

currentLocalVars : List (TTName, Binder TT) -> TT -> Tactic
currentLocalVars ctxt `(List String) =
  Exact (quoteListOfStrings (ctxt >>= bindingToStrings))
currentLocalVars _ _ = Fail [TextPart "Not a List String goal"]

someLocalVars : List String
someLocalVars = proof
  let myVariable : String = "foo"
  let myOtherVariable : String = "bar"
  applyTactic currentLocalVars

runTests : {auto f : FFI} -> IO' f ()
runTests = do
  putStrLn ("Hello tests " ++ show (myInc 4000))
  putStrLn
    ("Number of facts in the initial story state " ++
       show (length (Data.SortedSet.toList initialStoryState)))
  putStrLn (show someLocalVars)
  -- NOTE: This will only work in a non-JS build.
--  putStrLn (show !(run time))

-- NOTE: Some of these tests are very memory-intensive to compile, so
-- we actually can't uncomment the tests all at once (on my machine).
--
-- TODO: See if this will cause problems for actual application
-- development.
--
runJsTests : JS_IO ()
runJsTests = do
  jsf0 """
    console.log( "hello" )
  """
  let foo = jsft (Int -> Int -> JS_IO ()) """
    console.log( "heya " + (%0 + %1) )
  """
  foo 5 6
  foo2 <- jsf0 """function (a, b) {
    console.log( "heya2 " + (a + b) )
  }"""
  jsft (Ptr -> Int -> Int -> JS_IO ()) """
    %0( %1, %2 )
  """ foo2 5 6
  jsc2 foo2 !(jsint 5) !(jsint 10)
{-
  jsm1 !(jsf0 "console") "log"
    !(jsm1 !(jsf0 "JSON") "stringify"
        !(jso2_i
            "foo" !(jsint 1)
            "bar" !(jsint 2)))
-}
{-
  jsft (JsFn (Int -> Int) -> JS_IO ()) """
    console.log(%0(4))
  """ (MkJsFn (\a => unsafePerformIO (do
    jsf0 """
      console.log( "inside 1" )
    """
    return (a + 1))))
-}
{-
  jsm1 !(jsf0 "console") "log"
    !(jsc0 !(jsfn0 (do
      jsf0 """
        console.log( "inside 2" )
      """
      jsptr "outside 2"
    )))
-}
{-
  jsm1 !(jsf0 "console") "log"
    !(jsc1 !(jsfn1 (\s0 => do
      jsf1 """
        console.log( "inside 3 " + %0 )
      """ s0
      jsptr "outside 3"
    )) !(jsptr "world"))
-}
  jsm1 !(jsf0 "console") "log"
    !(jsc2 !(jsfn2_f (\s0, s1 => do
      jsf2 """
        console.log( "inside 4 " + %0 + " " + %1 )
      """ s0 s1
      jsptr "outside 4"
    )) !(jsptr "world") !(jsptr "tour"))
  jsf1 """
    window.onload = function () {
        function arrEach( arr, body ) {
            for ( var i = 0, n = arr.length; i < n; i++ )
                body( arr[ i ], i );
        }
        function arrMappend( arr, check ) {
            var result = [];
            arrEach( arr, function ( item, i ) {
                arrEach( check( item, i ), function ( itemItem ) {
                    result.push( itemItem );
                } );
            } );
            return result;
        }
        var hereEl = document.createElement( "div" );
        var focusEl = document.createElement( "div" );
        document.html.appendChild( hereEl );
        document.html.appendChild( focusEl );
        var currentTime = 0;
        var storyState = %0;
        function setContent( containerEl, content ) {
            while ( containerEl.hasChildNodes() )
                containerEl.removeChild( containerEl.firstChild );
            var innerContainerEl = document.createElement( "div" );
            arrEach( content, function ( para ) {
                var paraEl = document.createElement( "p" );
                arrEach( para, function ( span ) {
                    var spanEl = document.createTextNode( span.text );
                    if ( span.link !== null ) {
                        var newSpanEl = document.createElement( "a" );
                        newSpanEl.setAttribute( "href", "#" );
                        newSpanEl.onclick = function () {
                            setContent( focusEl,
                                getDescription( span.link.val ) );
                        };
                        newSpanEl.appendChild( spanEl );
                        spanEl = newSpanEl;
                    }
                    paraEl.appendChild( spanEl );
                } );
                innerContainerEl.appendChild( paraEl );
            } );
            containerEl.appendChild( innerContainerEl );
        }
        function getDescription( topic ) {
            var descriptions = arrMappend( storyState,
                function ( temporalFact ) {

                if ( currentTime < temporalFact.startTime )
                    return [];

                var end = temporalFact.endTime;
                if ( end.type === "knownEndTime" ) {
                    if ( end.time <= currentTime )
                        return [];
                } else if ( end.type === "assumeAfter" ) {
                    if ( end.time <= currentTime && !end.assumption )
                        return [];
                } else {
                    throw new Error();
                }

                var fact = temporalFact.fact;
                if ( fact.type === "describes"
                    && fact.pov === "you"
                    && fact.topic === "here" )
                    return [ fact.description ];
                else
                    return [];
            } );
            if ( descriptions.length !== 1 )
                throw new Error();
            return descriptions[ 0 ];
        }
        setContent( hereEl, getDescription( topic ) );
    };
  """ !(jsa_i $ for (
    Data.SortedSet.toList initialStoryState
  ) (\(MkTemporalFact (MkStartTime startTime) endTime fact) =>
    jso3_i
      "startTime" !(jsint $ toInt startTime)
      "endTime"
        !(case endTime of
            KnownEndTime time => jso2_i
              "type" !(jsptr "knownEndTime")
              "time" !(jsint $ toInt time)
            AssumeAfter time assumption => jso3_i
              "type" !(jsptr "assumeAfter")
              "time" !(jsint $ toInt time)
              "assumption"
                (ifThenElse assumption !(jsf0 "true") !(jsf0 "false")))
      "fact"
        !(case fact of
            ExistsPov pov => jso2_i
              "type" !(jsptr "existsPov")
              "pov" !(jsptr pov)
            ExistsTopic topic => jso2_i
              "type" !(jsptr "existsTopic")
              "topic" !(jsptr topic)
            Describes pov topic (MkHtextBlocks desc) => jso3_i
              "type" !(jsptr "describes")
              "pov" !(jsptr pov)
              "topic" !(jsptr topic)
              "desc"
                !(jsa_i $ for desc $ \(MkHtextBlock para) =>
                    jsa_i $ for para $ \(MkHtextSpan maybeLink text) =>
                      jso2_i
                        "link"
                          !(case maybeLink of
                              MyNothing => jsf0 "null"
                              MyJust topic =>
                                jso1_i "val" !(jsptr topic))
                        "text" text))
  ))
  return ()

testMain : {auto f : FFI} -> IO' f ()
testMain = do
  putStrLn "Running the tests"
  runTests

appMain : {auto f : FFI} -> IO' f ()
appMain = do
  putStrLn "Running the main app (which runs the tests)"
  runTests

max_stars_repo_name: rocketnia/contrivertext

max_issues_repo_name: rocketnia/contrivertext

max_forks_repo_name: rocketnia/contrivertext


text:
module CantElabType

import Data.Vect

import Language.Reflection

%language ElabReflection

0 T : Nat -> Type
T n = Vect n Nat

desiredType : TTImp
desiredType = IApp EmptyFC (IVar EmptyFC `{CantElabType.T}) `(3)

elabDecl : Name -> Elab Unit
elabDecl n = declare [
    IClaim EmptyFC MW Public [] $ MkTy EmptyFC EmptyFC n desiredType
  ]

%runElab elabDecl `{x1}
x1 = [1, 2, 3]

elabExpr : Elab Type
elabExpr = check desiredType

-- should typecheck because the rig of calling is zero

x2 : %runElab elabExpr
x2 = [1, 2, 3]

-- check that zero does not leak, should not typecheck

T' : Type
T' = %runElab elabExpr

max_stars_repo_name: buzden/idris-playground

max_issues_repo_name: buzden/idris-playground

max_forks_repo_name: buzden/idris-playground


text:
data Cont : (r : Type) -> (a : Type) -> Type where
     MkCont : ((k : a -> r) -> r) -> Cont r a

data ContT : (r : Type) -> (m : Type -> Type) -> (a : Type) -> Type where
     MkContT : ((k : a -> m r) -> m r) -> ContT r m a

cbind : Cont r a -> (a -> Cont r b) -> Cont r b

ctbind : ContT r m a -> (a -> ContT r m b) -> ContT r m b

callCC : ((a -> ContT r m b) -> ContT r m a) -> ContT r m a


text:
module Effect.Exception

import Effects
import System
import Control.IOExcept

data Exception : Type -> Effect where
     Raise : a -> { () } Exception a b

instance Handler (Exception a) Maybe where
     handle _ (Raise e) k = Nothing

instance Show a => Handler (Exception a) IO where
     handle _ (Raise e) k = do print e
                               believe_me (exit 1)

instance Handler (Exception a) (IOExcept a) where
     handle _ (Raise e) k = ioM (return (Left e))

instance Handler (Exception a) (Either a) where
     handle _ (Raise e) k = Left e

EXCEPTION : Type -> EFFECT
EXCEPTION t = MkEff () (Exception t)

raise : a -> { [EXCEPTION a ] } Eff m b
raise err = Raise err

-- TODO: Catching exceptions mid program?
-- probably need to invoke a new interpreter

-- possibly add a 'handle' to the Eff language so that an alternative
-- handler can be introduced mid interpretation?

max_stars_repo_name: edwinb/Eff-new

max_issues_repo_name: edwinb/Eff-new

max_forks_repo_name: edwinb/Eff-new


text:
import Data.Fin

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

%name Vect xs, ys, zs

append : Vect n elem -> Vect m elem -> Vect (n + m) elem
append [] ys = ys
append (x :: xs) ys = x :: append xs ys

zip : Vect n a -> Vect n b -> Vect n (a, b)
zip [] ys = []
zip (x :: xs) (y :: ys) = (x, y) :: zip xs ys

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

tryIndex : Integer -> Vect n a -> Maybe a
tryIndex {n} i xs = flip idx xs <$> integerToFin i n

take : (n : Nat) -> Vect (n + m) a -> Vect n a
take Z xs = []
take (S k) (x :: xs) = x :: take k xs

drop : (n : Nat) -> Vect (n + m) a -> Vect m a
drop Z xs = xs
drop (S k) (x :: xs) = drop k xs

sum : Num a => (pos : Integer) -> Vect n a -> Vect n a -> Maybe a
sum {n} pos xs ys = case integerToFin pos n of
                         Nothing => Nothing
                         (Just i) => Just (idx i xs + idx i ys)

max_stars_repo_name: tekerson/type-driven-development

max_issues_repo_name: tekerson/type-driven-development

max_forks_repo_name: tekerson/type-driven-development


text:
module Example.Pil.GenShow

import Data.List

import Example.Pil.Gen

%default total

%hint
interestingType : Gen Type
interestingType = oneOf $ map pure $ [Int, String, Bool]

DecEq' Type where
  decEq' Int    Int    = Yes Refl
  decEq' String String = Yes Refl
  decEq' Bool   Bool   = Yes Refl
  decEq' _      _      = No

alphaChar : Gen Char
alphaChar = choose ('a', 'z')

%hint
alphaString : Gen String
alphaString = map pack $ sequence $ replicate !(choose (1, 3)) alphaChar

%hint
varName : Gen Name
varName = MkName <$> alphaString

partial
simpleValue : {a : Type} -> Gen a
simpleValue {a=Int}    = chooseAny
simpleValue {a=String} = alphaString
simpleValue {a=Bool}   = chooseAny

partial
uniFunction : {a : Type} -> Gen (a -> a)
uniFunction {a=Int}    = oneOf $ map pure $ [ (+1), (+2), \x => x - 1 ]
uniFunction {a=String} = oneOf $ map pure $ [ ("a"++), (++"z") ]
uniFunction {a=Bool}   = pure not

partial
biFunction : {a : Type} -> Gen (a -> a -> a)
biFunction {a=Int}    = oneOf $ map pure $ [ (+), (*) ]
biFunction {a=String} = pure (++)
biFunction {a=Bool}   = oneOf $ map pure $ [ (\x, y => x && y), (\x, y => x || y) ]

%hint
partial
interestingExpr : {a : Type} -> {ctx : Context} -> Gen (Expression ctx a)
interestingExpr = exprGen 3 simpleValue uniFunction biFunction

partial
someStatementGen : Gen (post ** Statement [] post)
someStatementGen = stmtGen []

partial
someStatement : (post ** Statement [] post)
someStatement = unGen someStatementGen someStdGen

max_stars_repo_name: buzden/code-in-lectures

max_issues_repo_name: buzden/code-in-lectures

max_forks_repo_name: buzden/code-in-lectures


text:
||| Command-line client for Bautzen 1945
module Bautzen.Client

import Bautzen.Options
import Bautzen.Network
import Bautzen.REPL.SExpParser
import Bautzen.SExp

import Data.Strings.Extra

import Builtin
import Prelude
import Data.Nat
import Data.List
import Debug.Trace
import Network.Socket
import Network.Socket.Data
import Network.Socket.Raw
import System
import System.File

sendCommand : Socket -> SExp -> IO (Either String String)
sendCommand socket command = do
  let cmd = toWire command
  putStrLn $ "sending message " ++ cmd
  Right l <- send socket cmd
    | Left err => pure $ Left ("failed to send message " ++ show err)
  putStrLn $ "sent message, waiting answer"
  Right (str, _) <- recv socket 6
    | Left err => pure $ Left ("failed to receive length of message " ++ show err)
  case parseInteger (unpack str) 0 of
    Nothing => pure $ Left ("fail to parse '" ++ str ++ "' to expected number of characters, ignoring")
    Just len => do Right (msg, _) <- recv socket (fromInteger len)
                     | Left err => pure $ Left ("failed to read message " ++ show err)
                   pure (Right msg)

export
openConnection : (host:String) -> (port: Int) -> IO (Either String Socket)
openConnection host port = do
  Right sock <- socket AF_INET Stream 0
        | Left fail => pure (Left $ "Failed to open socket: " ++ show fail)
  res <- connect sock (Hostname host) port
  if res /= 0
    then pure (Left $ "Failed to connect socket with error: " ++ show res)
    else pure (Right sock)

runREPL : Socket -> IO ()
runREPL sock =
  do putStr "> "
     eof <- fEOF stdin
     if eof
       then pure ()
       else do x <- getLine
               case parseSExp x of
                    Right out =>
                        do Right result <- sendCommand sock out
                                 | Left err => do putStrLn ("Error sending command: " ++ err) ; runREPL sock
                           putStrLn result
                           runREPL sock
                    Left err => do putStrLn ("Invalid command: " ++ err) ; runREPL sock

export
client : Options -> IO (Either String ())
client (MkOptions port host _)  = do
  Right cnx <- openConnection host port
        | Left err => pure (Left err)
  runREPL cnx
  pure (Right ())

max_stars_repo_name: steshaw/hsgames

max_issues_repo_name: steshaw/hsgames

max_forks_repo_name: steshaw/hsgames


text:
import Data.List
import Data.List1
import Data.SortedMap as M
import Data.String.Parser

import System.File

Base : Type
Base = Char

Polymer : Type
Polymer = List1 Base

CountMap : Type
CountMap = SortedMap Base Nat

addCounts : CountMap -> CountMap -> CountMap
addCounts = M.mergeWith (+)

addBase : Base -> CountMap -> CountMap
addBase b = addCounts (M.singleton b 1)

decBase : Base -> CountMap -> CountMap
decBase b m = case M.lookup b m of
                   Just n => insert b (minus n 1) m
                   Nothing => m

fromPair : (Base, Base) -> CountMap
fromPair (b1, b2) = addCounts (M.singleton b1 1) (M.singleton b2 1)

Memoize : Type
Memoize = SortedMap ((Base,Base), Nat) CountMap

Rules : Type
Rules = SortedMap (Base, Base) Base

Input : Type
Input = (Polymer, Rules)

ruleParser : Parser ((Base, Base), Base)
ruleParser = do b1 <- letter
                b2 <- letter
                spaces1
                token "->"
                to <- letter
                pure ((b1, b2), to)

parser : Parser Input
parser = do polymer <- some letter
            Just polymer <- pure $ fromList polymer
              | Nothing => fail "no polymer"
            spaces1
            rules <- some (ruleParser <* spaces)
            pure (polymer, M.fromList rules)

countBases : Polymer -> CountMap
countBases p = M.fromList $ (\l => (l.head, length $ forget l)) <$> (group $ sort $ forget p)

insertNPair : Nat -> (Base, Base) -> Rules -> Memoize -> (CountMap, Memoize)
insertNPair Z p _ m = (fromPair p, m)
insertNPair (S n) (b1, b2) r m = case M.lookup ((b1, b2), (S n)) m of
                                      Nothing => case M.lookup (b1, b2) r of
                                                        Nothing => (fromPair (b1, b2), m)
                                                        (Just b) => let (c1, m1) = insertNPair n (b1, b) r m
                                                                        (c2, m2) = insertNPair n (b, b2) r m1
                                                                        c3 = decBase b $ addCounts c1 c2 in
                                                                        (c3, M.insert ((b1, b2), (S n)) c3 m2)
                                      (Just c1) => (c1, m)

insertN : Nat -> Polymer -> Rules -> Memoize -> CountMap
insertN n (b1 ::: []) r m = M.singleton b1 1
insertN n (b1 ::: (b2 :: p)) r m = let (c1, m1) = (insertNPair n (b1, b2) r m)
                                       c2 = insertN n (b2 ::: p) r m1
                                       c3 = addCounts c1 c2 in
                                       decBase b2 c3

subtractQuantity : CountMap -> Maybe Nat
subtractQuantity m = do let l = sort $ values m
                        high <- last' l
                        low <- head' l
                        pure $ minus high low

part1 : Input -> IO String
part1 (p, r) = do let c = insertN 10 p r M.empty
                  pure $ show $ subtractQuantity c

part2 : Input -> IO String
part2 (p, r) = do let c = insertN 40 p r M.empty
                  pure $ show $ subtractQuantity c

main : IO ()
main = do Right input <- readFile "input.txt"
            | Left err => printLn err
          Right (a, _) <- pure $ parse parser input
            | Left err => printLn err
          part1 a >>= putStrLn
          part2 a >>= putStrLn


text:
module Ifui.XDom

import Data.List
import Data.IORef

public export
data Attribute : Type -> Type where
  StringAttribute : String -> String -> Attribute a
  TargetValueEventListener : String -> (String -> a) -> Attribute a

public export
record ADom n where
    constructor MkADom
    create : String -> IO n
    appendChild : n -> n -> IO ()
    replace : n -> n -> IO ()
    setText : n -> String -> IO ()
    setStringAttribute : n -> String -> String -> IO ()
    addTargetValueEventListener : n -> String -> (String -> IO ()) -> IO (IO ())
    addEmptyEventListener : n -> String -> IO () -> IO (IO ())
    remove : n -> IO ()

public export
data Xml : Type -> Type where
  XNode : String -> List (Attribute a) -> Either String (List (Xml a)) -> Xml a

data VirtualAttribute : Type -> Type -> Type where
  VirtualStringAttribute : String -> String -> VirtualAttribute n a
  VirtualTargetValueEventListener : IO ()  ->  String -> (String -> a) -> VirtualAttribute n a

data VirtualDom : Type -> Type -> Type where
  VirtualNode : n -> String -> List (VirtualAttribute n a) -> Either String (List (VirtualDom n a)) -> VirtualDom n a

%foreign "javascript:lambda: (x, y) => x == y"
prim__refEq : AnyPtr -> AnyPtr -> PrimIO Int
export
refEq : HasIO io => a -> b -> io Bool
refEq x y =
  do
    r <- primIO $ prim__refEq (believe_me x) (believe_me y)
    pure $ r>0

initAttribute : (a -> IO()) -> ADom n -> n -> Attribute a -> IO (VirtualAttribute n a)
initAttribute onEvent adom node (StringAttribute k v) =
  do
    adom.setStringAttribute node k v
    pure $ VirtualStringAttribute k v
initAttribute onEvent adom node (TargetValueEventListener k f) =
  do
    rm <- adom.addTargetValueEventListener node k (onEvent . f)
    pure $ VirtualTargetValueEventListener rm k f

removeAttribute : ADom n -> n -> VirtualAttribute n a -> IO ()
removeAttribute adom node (VirtualStringAttribute x y) = adom.setStringAttribute node x ""
removeAttribute adom node (VirtualTargetValueEventListener x y f) = x

updateAttribute : (b -> IO()) -> ADom n -> n -> VirtualAttribute n a -> Attribute b -> IO (VirtualAttribute n b)
updateAttribute onEvent adom node old@(VirtualStringAttribute x y) att@(StringAttribute z w) =
  case x == z of
       True => case y == w of
                    True => pure $ VirtualStringAttribute x y
                    False => adom.setStringAttribute node x w >> pure  (VirtualStringAttribute x w)
       False =>
               do
                 removeAttribute adom node old
                 initAttribute onEvent adom node att
updateAttribute onEvent adom node old@(VirtualStringAttribute x y) att@(TargetValueEventListener z f) =
  do
    removeAttribute adom node old
    initAttribute onEvent adom node att
updateAttribute onEvent adom node old@(VirtualTargetValueEventListener x y f) att@(StringAttribute z w) =
  do
    removeAttribute adom node old
    initAttribute onEvent adom node att
updateAttribute onEvent adom node (VirtualTargetValueEventListener x y f) att@(TargetValueEventListener z g) =
  case y == z of
    True =>
           do
             eq <- refEq f g
             case eq of
                  True => pure $ VirtualTargetValueEventListener x y g
                  False => x >> initAttribute onEvent adom node att
    False =>
            do
              x
              initAttribute onEvent adom node att

getADomNode : VirtualDom n a -> n
getADomNode (VirtualNode node _ _ _) = node

createVNode : (a -> IO()) -> ADom n -> Xml a -> IO (VirtualDom n a)
createVNode onEvent adom (XNode tag attrs w) =
  do
    node <- adom.create tag
    vattrs <- traverse (initAttribute onEvent adom node) attrs
    case w of
         (Left x) =>
                    do
                      adom.setText node x
                      pure $ VirtualNode node tag vattrs (Left x)
         (Right x) =>
                     do
                       dchilds <- traverse (createVNode onEvent adom) x
                       traverse_ (\w => adom.appendChild node $ getADomNode w)  dchilds
                       pure $ VirtualNode node tag vattrs (Right dchilds)

updateVNode : (b -> IO()) -> ADom n -> VirtualDom n a -> Xml b -> IO (VirtualDom n b)
updateVNode onEvent adom ov@(VirtualNode node otag oAttrs z) nn@(XNode ntag attrs w) =
  case otag == ntag of
       True =>
              do
                newW <- case (z, w) of
                            ((Left x), (Left y)) =>
                                                   if x == y then pure $ Left y
                                                             else adom.setText node y >> pure (Left y)
                            ((Left x), (Right y)) =>
                                                    do
                                                       adom.setText node ""
                                                       dchilds <- traverse (createVNode onEvent adom) y
                                                       traverse_ (\w => adom.appendChild node $ getADomNode w)  dchilds
                                                       pure $ Right dchilds
                            ((Right x), (Left y)) =>
                                                    adom.setText node y >> pure (Left y)
                            ((Right x), (Right y)) =>
                                                     do
                                                       updated <- traverse (\(z, y) => updateVNode onEvent adom z y) (zip x y)
                                                       traverse_ (adom.remove . getADomNode) (drop (length y) x)
                                                       new <- traverse (createVNode onEvent adom) (drop (length x) y)
                                                       pure $ Right $ updated ++ new
                updatedAttrs <- traverse (\(z, y) => updateAttribute onEvent adom node z y) (zip oAttrs attrs)
                traverse_ (removeAttribute adom node) (drop (length attrs) oAttrs)
                newAttrs <- traverse (initAttribute onEvent adom node) (drop (length oAttrs) attrs)
                pure $ VirtualNode node ntag (updatedAttrs ++ newAttrs) newW
       False =>
              do
                new_node <- createVNode onEvent adom nn
                adom.replace node (getADomNode new_node)
                pure new_node

createOnEvent : {0 f : s -> Type} -> ADom n -> ((x:s) -> f x -> s) -> ((x : s) -> Xml (f x)) ->
                                     IORef (Maybe (x:s ** VirtualDom n (f x))) -> f x -> IO ()
createOnEvent adom update view viewState y =
  do
    vs <- readIORef viewState
    case vs of
         Just (x ** vdom) =>
                            do
                              let newX = update x (believe_me y)
                              newVdom <- updateVNode (createOnEvent adom update view viewState)  adom vdom (view newX)
                              writeIORef viewState (Just (newX ** newVdom))
         Nothing => pure ()

export
startView : {0 f : s -> Type} -> ADom n -> s -> ((x:s) -> f x -> s) -> ((x : s) -> Xml (f x)) -> IO n
startView adom x update view =
  do
    viewState <- newIORef $ the (Maybe (DPair s (VirtualDom n . f))) Nothing
    vdom <- createVNode (createOnEvent adom update view viewState) adom (view x)
    writeIORef viewState (Just $ (x ** vdom))
    pure $ getADomNode vdom

max_stars_repo_name: rbarreiro/ifui

max_issues_repo_name: rbarreiro/ifui

max_forks_repo_name: rbarreiro/ifui


text:
module Data.Promise

%default total

-- Promise abstraction from NodeJS

-- Heavily inspired by
-- https://raw.githubusercontent.com/andorp/order-taking/main/src/Service/NodeJS/Promise.idr

||| Promise monad
|||
||| Encapsulates the JavaScript abstraction of promise, which consists of a continuation
||| for successful computation and a continuation for errorneous computation. The promise
||| abstraction bounds these two continuations.
export
record Promise a where
  constructor MkPromise
  cmd : (a -> IO ()) -> (String -> IO ()) -> IO ()

%name Promise p, p1, p2

||| Activate the reject branch of the Promise with the given message.
export
reject : String -> Promise a
reject msg = MkPromise (\ok, err => err msg)

-- Promise is a functor, as we can pre-apply the 'f : a -> b' to the 'a' in the first computation.
-- Hint: This is possible as because the 'a' is in a positive position, because it got twice negated.
export
Functor Promise where
  map f (MkPromise cmd) = MkPromise (\succ => \err => cmd (\x => succ (f x)) err)

bind : Promise a -> (a -> Promise b) -> Promise b
bind (MkPromise cmd) f = MkPromise (\succ =>
                                      \err =>
                                              cmd (\x =>
                                                        let (MkPromise cmd_) = (f x)
                                                        in cmd_ succ err
                                                  ) err
                                    )

-- The Applicative instance of the Promise uses the succ
-- continuation with the value injected by the 'pure' function.
-- The '<*>' operator is based on the Monad's bind implementation.
export
Applicative Promise where
  pure x = MkPromise (\succ => \err => succ x)
  x <*> y = x `bind` (\f => f <$> y)

-- Promise is like the continuation monad, we can create a new command
-- function applying the result of the success computation in the
-- 'f' continuation which computes another Promise that can be unwrapped.
export
Monad Promise where
  (>>=) = bind

export
Alternative Promise where
  empty = reject "empty"

  p1 <|> p2 =
    MkPromise (\ok, err => p1.cmd ok (\_ => p2.cmd ok err))

||| The Promise monad under the hood relies on the IO monad, for that
||| reason we can use the IO monad, execute the IO computation and
||| evaluate the success computation with the result.
export
HasIO Promise where
  liftIO x = MkPromise (\ok => \err => x >>= ok)

||| Resolve a promise compuation.
|||
||| When the final computations for successful branch and errorneous
||| branch is given, the promise computation can be resolved, and if the
||| successful branch finished then its result is passed to the success
||| 'a -> IO ()' computation. If the errorneus branch finishes, the
||| given 'String -> IO ()' evalautes with the result error String.
export
resolve : Promise a -> (a -> IO ()) -> (String -> IO ()) -> IO ()
resolve (MkPromise cmd) = cmd

||| Alternative version of the resolve function with different argument order.
export
resolve' : (a -> IO ()) -> (String -> IO ()) -> Promise a -> IO ()
resolve' ok err (MkPromise cmd) = cmd ok err

||| On Left convert it to String and reject the promise, on Right resolve it.
export
either : Show e => Either e a -> Promise a
either (Left x)  = reject $ show x
either (Right x) = pure x

||| Helper function definition which encapsulates the essence of
||| the Promise type, PrimIO is needed for the FFI parts to
||| be easily wired in.
public export
PromiseShape : Type -> Type
PromiseShape a = (a -> IO ()) -> (String -> IO ()) -> PrimIO ()

||| Turn an FFI promise like construction into a Promise.
|||
||| The name of this function comes from its JavaScript
||| counterpart, which is also called promisify and accepts
||| two closures as arguments.
export
promisify : PromiseShape a -> Promise a
promisify prim =
  MkPromise (\ok, err => primIO $ prim ok err)

max_stars_repo_name: mattpolzin/harmony

max_issues_repo_name: mattpolzin/harmony

max_forks_repo_name: mattpolzin/harmony


text:
module Test.Transducers.Utils

import System

%access public export

Test : Type
Test = IO Int

assertThat : Bool -> String -> Test
assertThat test errorMsg =
  if test
    then do putStrLn "Test Passed"; pure 0
    else do putStrLn ("Test Failed: " ++ errorMsg); pure 1

assertEq : (Eq a, Show a) => (expected : a) -> (given : a) -> Test
assertEq e g =
  assertThat (g == e) $
    "Expected == " ++ show e ++ ", Got: " ++ show g

runTests : List Test -> Test
runTests = foldl (\res, t => (+) <$> res <*> t) (pure 0)

runTestSuite : List Test -> IO ()
runTestSuite tests = do
  failedCount <- runTests tests
  if failedCount > 0
    then exitFailure
    else pure ()

odd : Int -> Bool
odd n = mod n 2 == 1

twice : Int -> List Int
twice = replicate 2

vowel : Char -> Bool
vowel c = c `elem` (unpack "aeiou")

max_stars_repo_name: QuentinDuval/IdrisReducers

max_issues_repo_name: QuentinDuval/IdrisReducers

max_forks_repo_name: QuentinDuval/IdrisReducers


text:
StringOrInt : Bool -> Type
StringOrInt False = String
StringOrInt True = Int

getStringOrInt : (isInt : Bool) -> StringOrInt isInt
getStringOrInt False = "Ninety Four"
getStringOrInt True = 94

{-valToString : (isInt : Bool) -> StringOrInt isInt -> String
valToString False y = trim y
valToString True y = cast y-}

valToString : (isInt : Bool) -> (case isInt of
                                      False => String
                                      True => Int) -> String
valToString False y = trim y
valToString True y = cast y


text:
{--
Copyright 2021 Joel Berkeley

Licensed under the Apache License, Version 2.0 (the "License");
you may not use this file except in compliance with the License.
You may obtain a copy of the License at

    http://www.apache.org/licenses/LICENSE-2.0

Unless required by applicable law or agreed to in writing, software
distributed under the License is distributed on an "AS IS" BASIS,
WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
See the License for the specific language governing permissions and
limitations under the License.
--}
||| This module defines supported primitive backend types and their interaction with Idris.
module Primitive

import XLA.Literal

||| A `Primitive` is an Idris type for which there is a corresponding backend primitive type.
export
interface XLAPrimitive dtype => Primitive dtype where

export Primitive Bool where
export Primitive Int where
export Primitive Double where

max_stars_repo_name: joelberkeley/spidr

max_issues_repo_name: joelberkeley/spidr

max_forks_repo_name: joelberkeley/spidr


text:
import Control.App2

namespace Console
  public export
  interface Console e where
    putStr : String -> App e ()
    getStr : App e String

  export
  PrimIO e => Console e where
    putStr str = primIO $ putStr str
    getStr = primIO $ getLine

  export
  putStrLn : Console e => String -> App e ()
  putStrLn str = putStr (str ++ "\n")

namespace StateEx
  public export
  interface Console e => StateEx e where
    inc : App e Int
    testRes : String -> App e Bool

  export
  Has [Console, State Int, Exception String] e => StateEx e where
    inc
        = do count <- get
             put (count + the Int 1)
             pure count

    testRes str
        = do count <- get
             case str of
                  "DONE" => pure True
                  "BAD" => throw "Nope"
                  _ => do putStrLn $ "Hello " ++ str ++ " " ++ show count
                          pure False

test : Has [StateEx] e => App e ()
test
    = do putStr "Name: "
         inc
         x <- getStr
         done <- testRes x
         if done
            then pure ()
            else test

addState : Has [Console, StateEx] e => App e ()
addState
    = do new "foo" $
             do putStrLn "Here we go!"
                str <- get
                putStrLn str

runTest : IO ()
runTest
    = run $ do new (the Int 0) $
               handle (do test; addState) pure
                      (\err : String =>
                              putStrLn $ "Error: " ++ err)


text:
module Data.String.Builder

import Data.Buffer
import Data.List

data BuilderTree : Int -> Type where
    Empty : BuilderTree 0
    Str : (str : String) -> BuilderTree (prim__strLength str)
    Seq : {a : Int} -> (BuilderTree a) -> (BuilderTree b) -> BuilderTree (a + b)

runBuilderTree : Buffer -> (off : Int) -> BuilderTree size -> IO ()
runBuilderTree b off Empty = pure ()
runBuilderTree b off (Str str) = setString b off str
runBuilderTree b off (Seq {a} l r) = runBuilderTree b off l *> runBuilderTree b (off + a) r

mapStringTree : (String -> String) -> BuilderTree _ -> (size ** BuilderTree size)
mapStringTree f Empty = (_ ** Empty)
mapStringTree f (Str str) = (_ ** Str (f str))
mapStringTree f (Seq l r) =
    let (sl ** l') = mapStringTree f l
        (sr ** r') = mapStringTree f r
    in (_ ** Seq l' r')

export
record Builder where
    constructor MkBuilder
    size : Int
    tree : BuilderTree size

export
runBuilder : Builder -> String
runBuilder (MkBuilder size tree) = unsafePerformIO $ do
    Just b <- newBuffer size
        | Nothing => pure ""
    runBuilderTree b 0 tree
    str <- getString b 0 size
    pure str

export
mapString : (String -> String) -> Builder -> Builder
mapString f (MkBuilder _ t) =
    let (size ** tree) = mapStringTree f t
    in MkBuilder size tree

export
Semigroup Builder where
    MkBuilder s1 t1 <+> MkBuilder s2 t2 = MkBuilder (s1 + s2) (Seq t1 t2)

export
Monoid Builder where
    neutral = MkBuilder 0 Empty

export
FromString Builder where
    fromString str = if str == ""
        then neutral
        else MkBuilder (prim__strLength str) (Str str)

public export
interface ShowB a where
    showB : a -> Builder

export
[FromShow] Show a => ShowB a where
    showB = fromString . show

indentSize : Nat
indentSize = 4

export
parens : Builder -> Builder
parens b = "(" <+> b <+> ")"

export
bracket : Builder -> Builder
bracket b = "[" <+> b <+> "]"

export
indent : Nat -> Builder -> Builder
indent n b = fromString (fastConcat $ replicate (n * indentSize) " ") <+> b

export
function : ShowB fun => ShowB arg => Foldable t => fun -> t arg -> Builder
function f args = showB f <+> foldMap (\arg => " " <+> showB arg) args

export
nlSep : ShowB a => Foldable t => t a -> Builder
nlSep xs = foldMap (\x => showB x <+> "\n\n") xs

export
nl1Sep : ShowB a => Foldable t => t a -> Builder
nl1Sep xs = foldMap (\x => "\n" <+> showB x) xs <+> "\n"


text:
module Dart.FFI.Elab.Dsl

import public Dart.FFI.Elab.Types

public export
package : String -> List DartDecl -> DartPackage
package = MkDartPackage

public export
class' : DartName -> List DartDecl -> DartDecl
class' = Class

public export
generic : List DartName -> DartDecl -> DartDecl
generic = Generic

public export
extends : DartType -> DartDecl
extends = Extends

public export
enum : DartName -> List DartName -> DartDecl
enum = Enum

public export
fun : DartType -> DartName -> List DartParameter -> DartDecl
fun = Function

public export
new : DartName -> List DartParameter -> DartDecl
new = Constructor

public export
const : DartDecl -> DartDecl
const = Const

public export
final : DartType -> DartName -> DartDecl
final = Val

public export
getter : DartType -> DartName -> DartDecl
getter type name = Effectful (Val type name)

public export
var : DartType -> DartName -> DartDecl
var = Var

public export
static : DartDecl -> DartDecl
static = Static

public export
io : DartType -> DartName -> List DartParameter -> DartDecl
io ty name ps = Effectful (fun ty name ps)

public export
partial' : DartDecl -> DartDecl
partial' = Partial

public export
primitive : DartDecl -> DartDecl
primitive = Primitive


text:
%default partial

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

append : Vect n a -> Vect m a -> Vect (n + m) a
append [] ys = ys
-- append (x :: xs) ys = x :: append xs ys

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

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

zip : Vect n a -> Vect n b -> Vect n (a, b)
zip [] [] = []
zip (x :: xs) (y :: ys) = (x, y) :: zip xs ys


text:
-- examples in "Type-Driven Development with Idris"
-- chapter 15, section 15.2

import System.Concurrency.Channels

-- check that all functions are total
%default total

data Message = Add Nat Nat

data MessagePID = MkMessage PID

data ProcState = NoRequest | Sent | Complete

data Process : Type ->
               (in_state : ProcState) ->
               (out_state : ProcState) ->
               Type where
  Action : IO a -> Process a st st
  Pure : a -> Process a st st
  (>>=) : Process a st1 st2 -> (a -> Process b st2 st3) ->
          Process b st1 st3
  Spawn : Process () NoRequest Complete ->
          Process (Maybe MessagePID) st st
  Request : MessagePID -> Message -> Process Nat st st
  Respond : ((msg : Message) -> Process Nat NoRequest NoRequest) ->
            Process (Maybe Message) st Sent
  Loop : Inf (Process a NoRequest Complete) ->
         Process a Sent Complete

data Fuel = Dry | More (Lazy Fuel)

run : Fuel -> Process t in_state out_state -> IO (Maybe t)
run Dry _ = pure Nothing
run fuel (Request (MkMessage pid) msg)
  = do Just chan <- connect pid
       | _ => pure Nothing
       ok <- unsafeSend chan msg
       if ok then do Just x <- unsafeRecv Nat chan
                     | Nothing => pure Nothing
                     pure (Just x)
              else pure Nothing
run fuel (Respond calc)
  = do Just sender <- listen 1
       | Nothing => pure (Just Nothing)
       Just msg <- unsafeRecv Message sender
       | Nothing => pure (Just Nothing)
       Just res <- run fuel (calc msg)
       | Nothing => pure Nothing
       unsafeSend sender res
       pure (Just (Just msg))
run fuel (Action act) = do res <- act
                           pure (Just res)
run fuel (Pure val) = pure (Just val)
run fuel (act >>= next) = do Just x <- run fuel act
                             | Nothing => pure Nothing
                             run fuel (next x)
run fuel (Spawn proc) = do Just pid <- spawn (do run fuel proc
                                                 pure ())
                           | Nothing => pure Nothing
                           pure (Just (Just (MkMessage pid)))
run (More fuel) (Loop act) = run fuel act

partial
forever : Fuel
forever = More forever

partial
runProc : Process () in_state out_state -> IO ()
runProc proc = do run forever proc
                  pure ()

Service : Type -> Type
Service a = Process a NoRequest Complete

Client : Type -> Type
Client a = Process a NoRequest NoRequest

procAdder : Service ()
procAdder = do Respond (\msg => case msg of
                                  Add x y => Pure (x + y))
               Loop procAdder

procMain : Client ()
procMain = do Just adder_id <- Spawn procAdder
              | Nothing => Action (putStrLn "Spawn failed")
              answer <- Request adder_id (Add 2 3)
              Action (printLn answer)

-- run with:
-- :exec runProc procMain

max_stars_repo_name: pascalpoizat/idris-book

max_issues_repo_name: pascalpoizat/idris-book

max_forks_repo_name: pascalpoizat/idris-book


text:
-- examples in "Type-Driven Development with Idris"
-- chapter 15, section 15.2

import System.Concurrency.Channels

-- check that all functions are total
%default total

data Message = Add Nat Nat

data MessagePID = MkMessage PID

data Process : Type -> Type where
  Action : IO a -> Process a
  Pure : a -> Process a
  (>>=) : Process a -> (a -> Process b) -> Process b
  Spawn : Process () -> Process (Maybe MessagePID)
  Request : MessagePID -> Message -> Process (Maybe Nat)
  Respond : ((msg : Message) -> Process Nat) -> Process (Maybe Message)
  Loop : Inf (Process a) -> Process a

data Fuel = Dry | More (Lazy Fuel)

run : Fuel -> Process t -> IO (Maybe t)
run Dry _ = pure Nothing
run fuel (Request (MkMessage pid) msg)
  = do Just chan <- connect pid
       | _ => pure (Just Nothing)
       ok <- unsafeSend chan msg
       if ok then do Just x <- unsafeRecv Nat chan
                     | Nothing => pure (Just Nothing)
                     pure (Just (Just x))
              else pure (Just Nothing)
run fuel (Respond calc)
  = do Just sender <- listen 1
       | Nothing => pure (Just Nothing)
       Just msg <- unsafeRecv Message sender
       | Nothing => pure (Just Nothing)
       Just res <- run fuel (calc msg)
       | Nothing => pure Nothing
       unsafeSend sender res
       pure (Just (Just msg))
run fuel (Action act) = do res <- act
                           pure (Just res)
run fuel (Pure val) = pure (Just val)
run fuel (act >>= next) = do Just x <- run fuel act
                             | Nothing => pure Nothing
                             run fuel (next x)
run fuel (Spawn proc) = do Just pid <- spawn (do run fuel proc
                                                 pure ())
                           | Nothing => pure Nothing
                           pure (Just (Just (MkMessage pid)))
run (More fuel) (Loop act) = run fuel act

partial
forever : Fuel
forever = More forever

partial
runProc : Process () -> IO ()
runProc proc = do run forever proc
                  pure ()

procAdder : Process ()
procAdder = do Respond (\msg => case msg of
                                  Add x y => Pure (x + y))
               Loop procAdder

procMain : Process ()
procMain = do Just adder_id <- Spawn procAdder
              | Nothing => Action (putStrLn "Spawn failed")
              Just answer <- Request adder_id (Add 2 3)
              | Nothing => Action (putStrLn "Request failed")
              Action (printLn answer)

-- run with:
-- :exec runProc procMain