text:
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 : (Neg num, Integral 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

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)

max_stars_repo_name: PiotrJander/TypeDD-Samples

max_issues_repo_name: gdevanla/TypeDD-Samples

max_forks_repo_name: gdevanla/TypeDD-Samples


text:
-- Copyright (c) 2013 Radek Micek

module D3

import Common

-- ---------------------------------------------------------------------------

decodeEntities : String -> IO String
decodeEntities str = mkForeign (FFun "decodeEntities" [FString] FString) str

-- ---------------------------------------------------------------------------
-- Dialogs

prompt : String -> IO (Maybe String)
prompt msg =
  mkForeign
    (FFun
       "promptHelper"
       [FString, FAny (() -> Maybe String), FAny (String -> Maybe String)]
       (FAny $ Maybe String))
    msg
    mkNothing
    mkJust
  where
    mkNothing : () -> Maybe String
    mkNothing () = Nothing
    mkJust : String -> Maybe String
    mkJust s = Just s

-- ---------------------------------------------------------------------------
-- Arrays

data Array a = MkArray Ptr

emptyA : () -> IO (Array a)
emptyA () = mkForeign (FFun "Array" [] (FAny $ Array _))

pushA : Array a -> a -> IO ()
pushA xs x = mkForeign (FFun ".push" [FAny $ Array _, FAny _] FUnit) xs x

lengthA : Array a -> IO Int
lengthA xs = mkForeign (FFun ".length" [FAny $ Array _] FInt) xs

mkArray : List a -> IO (Array a)
mkArray xs = do
  ys <- emptyA ()
  mapM_ (pushA ys) xs
  return ys

getNth : Array a -> Int -> IO a
getNth xs i = mkForeign (FFun "getNth" [FAny $ Array _, FInt] (FAny _)) xs i

setNth : Array a -> Int -> a -> IO ()
setNth xs i x =
  mkForeign (FFun "setNth" [FAny $ Array _, FInt, FAny _] FUnit) xs i x

arrayToList : {a : _} -> Array a -> IO (List a)
arrayToList {a} xs = lengthA xs >>= loop [] . flip (-) 1
  where
    loop : List a -> Int -> IO (List a)
    loop acc i =
      if i >= 0 then do
        x <- getNth xs i
        loop (x :: acc) (i - 1)
      else
        return acc

anyA : {a : _} -> (a -> IO Bool) -> Array a -> IO Bool
anyA {a} f xs =
  pure (/= 0) <$> mkForeign (FFun "anyA" [FAny _, FAny $ Array _] FInt) f2 xs
  where
    f2 : a -> IO Int
    f2 x = [| boolToInt (f x) |]

filterA : {a : _} -> (a -> IO Bool) -> Array a -> IO (Array a)
filterA {a} f xs =
  mkForeign (FFun "filterA" [FAny _, FAny $ Array _] (FAny $ Array _)) f2 xs
  where
    f2 : a -> IO Int
    f2 x = [| boolToInt (f x) |]

findA : {a : _} -> (a -> IO Bool) -> Array a -> IO (Maybe a)
findA {a} f xs = lengthA xs >>= loop 0
  where
    loop : Int -> Int -> IO (Maybe a)
    loop i len =
      if i < len then do
        x <- getNth xs i
        b <- f x
        if b then
          return $ Just x
        else
          loop (i + 1) len
      else
        return Nothing

-- ---------------------------------------------------------------------------
-- Selecting elements

data Sel a b = MkSel Ptr

data NoData = MkNoData Ptr

d3 : Sel NoData NoData
d3 = unsafePerformIO
       $ mkForeign (FFun "d3Root" [] (FAny $ Sel NoData NoData))

select : String -> Sel a b -> IO (Sel a b)
select s sel =
  mkForeign (FFun ".select" [FAny $ Sel _ _, FString] (FAny $ Sel _ _)) sel s

selectAll : String -> Sel a b -> IO (Sel b NoData)
selectAll s sel =
  mkForeign
    (FFun ".selectAll" [FAny $ Sel _ _, FString] (FAny $ Sel _ _))
    sel s

-- ---------------------------------------------------------------------------
-- Operating on selections: Content

attr : String -> String -> Sel a b -> IO (Sel a b)
attr attr val sel =
  mkForeign
    (FFun ".attr" [FAny $ Sel _ _, FString, FString] (FAny $ Sel _ _))
    sel attr val

attr' : String -> (b -> Int -> IO String) -> Sel a b -> IO (Sel a b)
attr' attr f sel =
  mkForeign
    (FFun "attrPrime" [FAny $ Sel _ _, FString, FAny _] (FAny $ Sel _ _))
    sel attr f

classed : String -> Bool -> Sel a b -> IO (Sel a b)
classed cls b sel =
  mkForeign
    (FFun ".classed" [FAny $ Sel _ _, FString, FInt] (FAny $ Sel _ _))
    sel cls (b ? 1 : 0)

classed' :
  {b : _} ->
  String ->
  (b -> Int -> IO Bool) ->
  Sel a b ->
  IO (Sel a b)
classed' {b} cls f sel =
  mkForeign
    (FFun "classedPrime" [FAny $ Sel _ _, FString, FAny _] (FAny $ Sel _ _))
    sel cls f2
  where
    f2 : b -> Int -> IO Int
    f2 d i = do
      result <- f d i
      return (result ? 1 : 0)

style : String -> String -> Sel a b -> IO (Sel a b)
style name val sel =
  mkForeign
    (FFun ".style" [FAny $ Sel _ _, FString, FString] (FAny $ Sel _ _))
    sel name val

style' : String -> (b -> Int -> IO String) -> Sel a b -> IO (Sel a b)
style' name f sel =
  mkForeign
    (FFun "stylePrime" [FAny $ Sel _ _, FString, FAny _] (FAny $ Sel _ _))
    sel name f

getBoolProperty : String -> Sel a b -> IO Bool
getBoolProperty name sel =
  pure (/= 0) <$> mkForeign
                    (FFun "getBoolProperty" [FAny $ Sel _ _, FString] FInt)
                    sel name

boolProperty : String -> Bool -> Sel a b -> IO (Sel a b)
boolProperty name b sel =
  mkForeign
    (FFun "boolProperty" [FAny $ Sel _ _, FString, FInt] (FAny $ Sel _ _))
    sel name (b ? 1 : 0)

property : String -> String -> Sel a b -> IO (Sel a b)
property name val sel =
  mkForeign
    (FFun ".property" [FAny $ Sel _ _, FString, FString] (FAny $ Sel _ _))
    sel name val

property' : String -> (b -> Int -> IO String) -> Sel a b -> IO (Sel a b)
property' name f sel =
  mkForeign
    (FFun "propertyPrime" [FAny $ Sel _ _, FString, FAny _] (FAny $ Sel _ _))
    sel name f

text : String -> Sel a b -> IO (Sel a b)
text val sel =
  mkForeign (FFun ".text" [FAny $ Sel _ _, FString] (FAny $ Sel _ _)) sel val

text' : (b -> Int -> IO String) -> Sel a b -> IO (Sel a b)
text' f sel =
  mkForeign (FFun "textPrime" [FAny $ Sel _ _, FAny _] (FAny $ Sel _ _)) sel f

html : String -> Sel a b -> IO (Sel a b)
html val sel =
  mkForeign (FFun ".html" [FAny $ Sel _ _, FString] (FAny $ Sel _ _)) sel val

html' : (b -> Int -> IO String) -> Sel a b -> IO (Sel a b)
html' f sel =
  mkForeign (FFun "htmlPrime" [FAny $ Sel _ _, FAny _] (FAny $ Sel _ _)) sel f

append : String -> Sel a b -> IO (Sel a b)
append elem sel =
  mkForeign
    (FFun ".append" [FAny $ Sel _ _, FString] (FAny $ Sel _ _))
    sel elem

remove : Sel a b -> IO ()
remove sel = mkForeign (FFun ".remove" [FAny $ Sel _ _, FUnit] FUnit) sel ()

forgetBoundData : Sel a b -> IO (Sel NoData NoData)
forgetBoundData (MkSel s) = return $ MkSel s

castBoundData : Sel a b -> IO (Sel a c)
castBoundData (MkSel s) = return $ MkSel s

-- ---------------------------------------------------------------------------
-- Operating on selections: Data

bind : Array c -> Sel a b -> IO (Sel a c)
bind arr sel =
  mkForeign
    (FFun ".data" [FAny $ Sel _ _, FAny $ Array _] (FAny $ Sel _ _))
    sel arr

bind' : (a -> Int -> IO (Array c)) -> Sel a b -> IO (Sel a c)
bind' f sel =
  mkForeign
    (FFun
       "bindPrime"
       [FAny $ Sel _ _, FAny _]
       (FAny $ Sel _ _))
    sel f

bindK : Array c -> (c -> Int -> IO String) -> Sel a b -> IO (Sel a c)
bindK arr key sel =
  mkForeign
    (FFun "bindK" [FAny $ Sel _ _, FAny $ Array _, FAny _] (FAny $ Sel _ _))
    sel arr key

bindK' :
  (a -> Int -> IO (Array c)) ->
  (c -> Int -> IO String) ->
  Sel a b ->
  IO (Sel a c)
bindK' f key sel =
  mkForeign
    (FFun "bindKPrime" [FAny $ Sel _ _, FAny _, FAny _] (FAny $ Sel _ _))
    sel f key

enter : Sel a b -> IO (Sel a b)
enter sel =
  mkForeign (FFun ".enter" [FAny $ Sel _ _, FUnit] (FAny $ Sel _ _)) sel ()

exit : Sel a b -> IO (Sel a b)
exit sel =
  mkForeign (FFun ".exit" [FAny $ Sel _ _, FUnit] (FAny $ Sel _ _)) sel ()

-- ---------------------------------------------------------------------------
-- Events

onClick : Sel a b -> (() -> IO ()) -> IO ()
onClick sel h =
  mkForeign (FFun "onClick" [FAny $ Sel _ _, FAny (() -> IO ())] FUnit) sel h

-- ---------------------------------------------------------------------------
-- Force layout

data Node a = MkNode Ptr

mkNode : a -> IO (Node a)
mkNode d = mkForeign (FFun "mkNode" [FAny _] (FAny $ Node _)) d

getX : Node a -> IO Float
getX n = mkForeign (FFun ".x" [FAny $ Node _] FFloat) n

getY : Node a -> IO Float
getY n = mkForeign (FFun ".y" [FAny $ Node _] FFloat) n

getNData : Node a -> IO a
getNData n = mkForeign (FFun ".data" [FAny $ Node _] (FAny _)) n

putNData : Node a -> a -> IO ()
putNData n d = mkForeign (FFun ".data=" [FAny $ Node _, FAny _] FUnit) n d

data Link a b = MkLink Ptr

mkLink : Node a -> Node a -> b -> IO (Link a b)
mkLink src tgt d =
  mkForeign
    (FFun "mkLink" [FAny $ Node _, FAny $ Node _, FAny _] (FAny $ Link _ _))
    src tgt d

getSource : Link a b -> IO (Node a)
getSource l = mkForeign (FFun ".source" [FAny $ Link _ _] (FAny $ Node _)) l

getTarget : Link a b -> IO (Node a)
getTarget l = mkForeign (FFun ".target" [FAny $ Link _ _] (FAny $ Node _)) l

getSrcTgt : Link a b -> IO (Node a, Node a)
getSrcTgt l = do
  src <- getSource l
  tgt <- getTarget l
  return (src, tgt)

getLData : Link a b -> IO b
getLData l = mkForeign (FFun ".data" [FAny $ Link _ _] (FAny _)) l

putLData : Link a b -> b -> IO ()
putLData l d = mkForeign (FFun ".data=" [FAny $ Link _ _, FAny _] FUnit) l d

data ForceLayout a b = MkForceLayout Ptr

mkForceLayout : Float -> Float -> IO (ForceLayout a b)
mkForceLayout width height =
  mkForeign
    (FFun "mkForceLayout" [FFloat, FFloat] (FAny $ ForceLayout _ _))
    width height

getNodes : ForceLayout a b -> IO (Array $ Node a)
getNodes fl =
  mkForeign
    (FFun ".nodes" [FAny $ ForceLayout _ _, FUnit] (FAny $ Array $ Node _))
    fl ()

putNodes : ForceLayout a b -> Array (Node a) -> IO ()
putNodes fl ns =
  mkForeign
    (FFun ".nodes" [FAny $ ForceLayout _ _, FAny $ Array $ Node _] FUnit)
    fl ns

getLinks : ForceLayout a b -> IO (Array $ Link a b)
getLinks fl =
  mkForeign
    (FFun ".links" [FAny $ ForceLayout _ _, FUnit] (FAny $ Array $ Link _ _))
    fl ()

putLinks : ForceLayout a b -> Array (Link a b) -> IO ()
putLinks fl ls =
  mkForeign
    (FFun ".links" [FAny $ ForceLayout _ _, FAny $ Array $ Link _ _] FUnit)
    fl ls

getWidthL : ForceLayout a b -> IO Float
getWidthL fl = mkForeign (FFun "getWidthL" [FAny $ ForceLayout _ _] FFloat) fl

getHeightL : ForceLayout a b -> IO Float
getHeightL fl = mkForeign (FFun "getHeightL" [FAny $ ForceLayout _ _] FFloat) fl

chargeL : Float -> ForceLayout a b -> IO (ForceLayout a b)
chargeL val fl =
  mkForeign
    (FFun ".charge" [FAny $ ForceLayout _ _, FFloat] (FAny $ ForceLayout _ _))
    fl val

linkDistanceL : Float -> ForceLayout a b -> IO (ForceLayout a b)
linkDistanceL val fl =
  mkForeign
    (FFun
       ".linkDistance"
       [FAny $ ForceLayout _ _, FFloat]
       (FAny $ ForceLayout _ _))
    fl val

onTickL : ForceLayout a b -> (() -> IO ()) -> IO ()
onTickL fl h =
  mkForeign (FFun "onTickL" [FAny $ ForceLayout _ _, FAny _] FUnit) fl h

startL : ForceLayout a b -> IO ()
startL fl =
  mkForeign (FFun ".start" [FAny $ ForceLayout _ _, FUnit] FUnit) fl ()

stopL : ForceLayout a b -> IO ()
stopL fl =
  mkForeign (FFun ".stop" [FAny $ ForceLayout _ _, FUnit] FUnit) fl ()

makeDraggableL : ForceLayout a b -> Sel c d -> IO (Sel c d)
makeDraggableL fl sel =
  mkForeign
    (FFun "makeDraggableL"
       [FAny $ Sel _ _, FAny $ ForceLayout _ _]
       (FAny $ Sel _ _))
    sel fl

ext: idr

max_stars_repo_name: radekm/satviz

max_issues_repo_name: radekm/satviz

max_forks_repo_name: radekm/satviz


text:
module Ipkg.Parser

import Data.List
import Text.Lexer
import Text.Parser
import Text.Parser.Core

import Ipkg.Types
import Ipkg.Lexer
import Ipkg.Rule

data DescField : Type where
  PVersion : PkgVersion -> DescField
  PStrField : String -> String -> DescField
  PModules : List String -> DescField
  PDepends : List Depends -> DescField

pkgversion : Rule PkgVersion
pkgversion = PV <$> sepBy1 dot nat

packageName : Rule String
packageName = exact "package" *> identifier

version : Rule PkgVersion
version = property "version" >> pkgversion

modules : Rule (List String)
modules = property "modules" >> sep identifier

deps : Rule (List Depends)
deps = property "depends" >> sep depends
  where
    data Bound = LT PkgVersion Bool | GT PkgVersion Bool
    bound : Rule (List Bound)
    bound = do op "<="
               v <- pkgversion
               pure [ LT v True ]
        <|> do op ">="
               v <- pkgversion
               pure [ GT v True ]
        <|> do op "<"
               v <- pkgversion
               pure [ LT v False ]
        <|> do op ">"
               v <- pkgversion
               pure [ GT v False ]
        <|> do op "=="
               v <- pkgversion
               pure [LT v True, GT v True]

    mkBound : List Bound -> PkgVersionBounds -> EmptyRule PkgVersionBounds
    mkBound (LT b i :: bs) pkgbs
      = maybe (mkBound bs . { upperBound := Just b, upperInclusive := i } $ pkgbs)
              (\_ => fail "Dependency already has an upper bound")
              pkgbs.upperBound
    mkBound (GT b i :: bs) pkgbs
      = maybe (mkBound bs . { lowerBound := Just b, lowerInclusive := i } $ pkgbs)
              (\_ => fail "Dependency already has a lower bound")
              pkgbs.lowerBound
    mkBound [] pkgbs = pure pkgbs

    depends : Rule Depends
    depends = do
      name <- identifier
      bs <- sepBy (op "&&") bound
      pure $ D name !(mkBound (concat bs) anyBounds)

strField : Rule (String, String)
strField = do
  name <- identifier
  equals
  value <- stringLit <|> identifier
  pure (name, value)

field : Rule DescField
field = (PVersion <$> version)
    <|> (PDepends <$> deps)
    <|> (PModules <$> modules)
    <|> (uncurry PStrField <$> strField)

addField : DescField -> Package -> Package
addField (PVersion v) = { version := Just v }
addField (PStrField nm val) = { strFields $= ((nm, val) ::) }
addField (PDepends ds) = { depends := ds }
addField (PModules ms) = { modules := ms }

expr : Rule Package
expr = do
  pkg <- def <$> packageName
  fields <- some field
  eof
  pure $ foldr addField pkg fields

processWhitespace : (List (WithBounds PkgToken), a) ->
                    (List (WithBounds PkgToken), a)
processWhitespace = mapFst (filter notComment)
  where
    notComment : WithBounds PkgToken -> Bool
    notComment t with (t.val)
      notComment _ | (Comment x) = False
      notComment _ | Space = False
      notComment _ | _ = True

runParser : String -> Either (List1 (ParsingError PkgToken)) (Package, List (WithBounds PkgToken))
runParser s = parse expr . fst . processWhitespace $ lex tokenMap s

errMsgs : List1 (ParsingError PkgToken) -> String
errMsgs = concatMap decorate . forget
  where decorate : ParsingError PkgToken -> String
        decorate (Error msg bounds) = "ParseError(\{msg}; \{show bounds})"

export
parsePkg : String -> Either String Package
parsePkg = bimap errMsgs fst . runParser

max_stars_repo_name: claymager/ipkg-to-json

max_issues_repo_name: claymager/ipkg-to-json

max_forks_repo_name: claymager/ipkg-to-json


text:
module Main

import SimpleDataRealizedFunction

-- Realized incrementer
incrementer : Int -> Int
incrementer = (+1)
rlz_incrementer : SimpleDataRealizedFunction (Int -> Int) -- 100 1.0
rlz_incrementer = MkSimpleDataRealizedFunction incrementer

-- Realized twicer
twicer : Int -> Int
twicer = (*2)
rlz_twicer : SimpleDataRealizedFunction (Int -> Int) -- 500 0.9
rlz_twicer = MkSimpleDataRealizedFunction twicer

-- Realized (twicer . incrementer).
rlz_composition : SimpleDataRealizedFunction (Int -> Int) -- 600 0.9
-- The following does not work because 601 ≠ 100+500 and 1.0 ≠ (min 1.0 0.9)
-- rlz_composition : SimpleDataRealizedFunction (Int -> Int) 601 1.0
rlz_composition = compose rlz_twicer rlz_incrementer

-- Simple test, result should be (3+1)*2 = 8
rslt : Int
rslt = apply rlz_composition 3


text:
{-
Copyright 2019, Mokshasoft AB (mokshasoft.com)

This software may be distributed and modified according to the terms of
the BSD 2-Clause license. Note that NO WARRANTY is provided.
See "LICENSE_BSD2.txt" for details.
-}

module BareMetal.SocAM335x

%access public export
%default total

-- Cache Line size in ARM Cortex-A8.
socCachelineSizeMax : Bits32
socCachelineSizeMax =
    64

-- Base address of AINTC memory mapped registers
socAintcRegs : Bits32
socAintcRegs =
    0x48200000

-- Base addresses of UART memory mapped registers
socUart0Regs : Bits32
socUart0Regs =
    0x44e09000
socUart1Regs : Bits32
socUart1Regs =
    0x48022000
socUart2Regs : Bits32
socUart2Regs =
    0x48024000
socUart3Regs : Bits32
socUart3Regs =
    0x481a6000
socUart4Regs : Bits32
socUart4Regs =
    0x481a8000
socUart5Regs : Bits32
socUart5Regs =
    0x481aa000

-- Base addresses of USB memory mapped registers
socUsb0Base : Bits32
socUsb0Base =
    0x47401400
socUsb1Base : Bits32
socUsb1Base =
    0x47401c00
-- Base addresses of SPI memory mapped registers
socSpi0Regs : Bits32
socSpi0Regs =
    0x48030000
socSpi1Regs : Bits32
socSpi1Regs =
    0x481a0000

-- Base addresses of GPIO memory mapped registers
socGpio0Regs : Bits32
socGpio0Regs =
    0x44e07000
socGpio1Regs : Bits32
socGpio1Regs =
    0x4804c000
socGpio2Regs : Bits32
socGpio2Regs =
    0x481ac000
socGpio3Regs : Bits32
socGpio3Regs =
    0x481ae000

-- Base addresses of DMTIMER memory mapped registers
socDmtimer0Regs : Bits32
socDmtimer0Regs =
    0x44e05000
socDmtimer1Regs : Bits32
socDmtimer1Regs =
    0x44e31000
socDmtimer2Regs : Bits32
socDmtimer2Regs =
    0x48040000
socDmtimer3Regs : Bits32
socDmtimer3Regs =
    0x48042000
socDmtimer4Regs : Bits32
socDmtimer4Regs =
    0x48044000
socDmtimer5Regs : Bits32
socDmtimer5Regs =
    0x48046000
socDmtimer6Regs : Bits32
socDmtimer6Regs =
    0x48048000
socDmtimer7Regs : Bits32
socDmtimer7Regs =
    0x4804a000

-- Base address of MMC memory mapped registers
socMmchs0Regs : Bits32
socMmchs0Regs =
    0x48060000
socMmchs1Regs : Bits32
socMmchs1Regs =
    0x481d8000
socMmchs2Regs : Bits32
socMmchs2Regs =
    0x47810000

-- Base address of GPMC memory mapped registers
socGpmc0Regs : Bits32
socGpmc0Regs =
    0x50000000

-- Base address of GPMC memory mapped registers
socElm0Regs : Bits32
socElm0Regs =
    0x48080000

-- Base address of I2C memory mapped registers
socI2c0Regs : Bits32
socI2c0Regs =
    0x44e0b000
socI2c1Regs : Bits32
socI2c1Regs =
    0x4802a000
socI2c2Regs : Bits32
socI2c2Regs =
    0x4819c000

-- Base address of WDT memory mapped registers
socWdt0Regs : Bits32
socWdt0Regs =
    0x44e33000
socWdt1Regs : Bits32
socWdt1Regs =
    0x44e35000

-- Base address of WDT memory mapped registers
socCpswSsRegs : Bits32
socCpswSsRegs =
    0x4a100000
socCpswMdioRegs : Bits32
socCpswMdioRegs =
    0x4a101000
socCpswWrRegs : Bits32
socCpswWrRegs =
    0x4a101200
socCpswCpdmaRegs : Bits32
socCpswCpdmaRegs =
    0x4a100800
socCpswAleRegs : Bits32
socCpswAleRegs =
    0x4a100d00
socCpswStatRegs : Bits32
socCpswStatRegs =
    0x4a100900
socCpswPort0Regs : Bits32
socCpswPort0Regs =
    0x4a100100
socCpswPort1Regs : Bits32
socCpswPort1Regs =
    0x4a100200
socCpswSliver1Regs : Bits32
socCpswSliver1Regs =
    0x4a100d80
socCpswPort2Regs : Bits32
socCpswPort2Regs =
    0x4a100300
socCpswSliver2Regs : Bits32
socCpswSliver2Regs =
    0x4a100dc0
socCpswCppiRamRegs : Bits32
socCpswCppiRamRegs =
    0x4a102000

-- Base address of McASP memory mapped registers
socMcasp0CtrlRegs : Bits32
socMcasp0CtrlRegs =
    0x48038000
socMcasp0FifoRegs : Bits32
socMcasp0FifoRegs =
    socMcasp0CtrlRegs + 0x1000
socMcasp0DataRegs : Bits32
socMcasp0DataRegs =
    0x46000000
socMcasp1CtrlRegs : Bits32
socMcasp1CtrlRegs =
    0x4803c000
socMcasp1FifoRegs : Bits32
socMcasp1FifoRegs =
    socMcasp1CtrlRegs + 0x1000
socMcasp1DataRegs : Bits32
socMcasp1DataRegs =
    0x46400000

-- Base address of EMIF memory mapped registers
socEmif0Regs : Bits32
socEmif0Regs =
    0x4c000000

-- Base addresses of RTC memory mapped registers
socRtc0Regs : Bits32
socRtc0Regs =
    0x44e3e000

-- Base addresses of PRCM memory mapped registers
socPrcmRegs : Bits32
socPrcmRegs =
    0x44e00000
socCmPerRegs : Bits32
socCmPerRegs =
    socPrcmRegs + 0
socCmWkupRegs : Bits32
socCmWkupRegs =
    socPrcmRegs + 0x400
socCmDpllRegs : Bits32
socCmDpllRegs =
    socPrcmRegs + 0x500
socCmMpuRegs : Bits32
socCmMpuRegs =
    socPrcmRegs + 0x600
socCmDeviceRegs : Bits32
socCmDeviceRegs =
    socPrcmRegs + 0x700
socCmRtcRegs : Bits32
socCmRtcRegs =
    socPrcmRegs + 0x800
socCmGfxRegs : Bits32
socCmGfxRegs =
    socPrcmRegs + 0x900
socCmCefuseRegs : Bits32
socCmCefuseRegs =
    socPrcmRegs + 0xa00
socOcpSocketRamRegs : Bits32
socOcpSocketRamRegs =
    socPrcmRegs + 0xb00
socPrmPerRegs : Bits32
socPrmPerRegs =
    socPrcmRegs + 0xc00
socPrmWkupRegs : Bits32
socPrmWkupRegs =
    socPrcmRegs + 0xd00
socPrmMpuRegs : Bits32
socPrmMpuRegs =
    socPrcmRegs + 0xe00
socPrmDeviceRegs : Bits32
socPrmDeviceRegs =
    socPrcmRegs + 0xf00
socPrmRtcRegs : Bits32
socPrmRtcRegs =
    socPrcmRegs + 0x1000
socPrmGfxRegs : Bits32
socPrmGfxRegs =
    socPrcmRegs + 0x1100
socPrmCefuseRegs : Bits32
socPrmCefuseRegs =
    socPrcmRegs + 0x1200

-- Base address of control module memory mapped registers
socControlRegs : Bits32
socControlRegs =
    0x44e10000

-- Base address of Channel controller  memory mapped registers
socEdma30cc0Regs : Bits32
socEdma30cc0Regs =
    0x49000000

-- Base address of DCAN module memory mapped registers
socDcan0Regs : Bits32
socDcan0Regs =
    0x481cc000
socDcan1Regs : Bits32
socDcan1Regs =
    0x481d0000

{-
  Parameterizable Configuration: These are fed directly from the RTL
  parameters for the given SOC
-}
tpccMux : Bits32 -> Bits32
tpccMux n =
    0xf90 + (n * 4)

socLcdc0Regs : Bits32
socLcdc0Regs =
    0x4830e000

socAdcTsc0Regs : Bits32
socAdcTsc0Regs =
    0x44e0d000

-- Base addresses of PWMSS memory mapped registers.

socPwmss0Regs : Bits32
socPwmss0Regs =
    0x48300000
socPwmss1Regs : Bits32
socPwmss1Regs =
    0x48302000
socPwmss2Regs : Bits32
socPwmss2Regs =
    0x48304000

socEcapRegs : Bits32
socEcapRegs =
    0x00000100
socEqepRegs : Bits32
socEqepRegs =
    0x00000180
socEpwmRegs : Bits32
socEpwmRegs =
    0x00000200

socEcap0Regs : Bits32
socEcap0Regs =
    socPwmss0Regs + socEcapRegs
socEcap1Regs : Bits32
socEcap1Regs =
    socPwmss1Regs + socEcapRegs
socEcap2Regs : Bits32
socEcap2Regs =
    socPwmss2Regs + socEcapRegs

socEqep0Regs : Bits32
socEqep0Regs =
    socPwmss0Regs + socEqepRegs
socEqep1Regs : Bits32
socEqep1Regs =
    socPwmss1Regs + socEqepRegs
socEqep2Regs : Bits32
socEqep2Regs =
    socPwmss2Regs + socEqepRegs

socEpwm0Regs : Bits32
socEpwm0Regs =
    socPwmss0Regs + socEpwmRegs
socEpwm1Regs : Bits32
socEpwm1Regs =
    socPwmss1Regs + socEpwmRegs
socEpwm2Regs : Bits32
socEpwm2Regs =
    socPwmss2Regs + socEpwmRegs

socEpwmModuleFreq : Bits32
socEpwmModuleFreq =
    100

max_stars_repo_name: mokshasoft/bare-metal-idris-drivers

max_issues_repo_name: mokshasoft/bare-metal-idris-drivers

max_forks_repo_name: mokshasoft/bare-metal-idris-drivers


text:
module Main

import Control.Comonad
import Control.Comonad.Store.Representable
import Conway
import Conway.Parse
import Data.Fuel
import Data.Functor.Representable
import Data.Vect
import System.File.ReadWrite
import System.File.Virtual

%default total

fRead : HasIO io => File -> Fuel -> io String
fRead file fuel = foldMap id <$> go file fuel
  where
    go : File -> Fuel -> io (List String)
    go file Dry = pure []
    go file (More fuel) = do
      False <- fEOF file | _ => pure []
      Right str <- fGetLine file | _ => pure []
      (str ::) <$> go file fuel

covering
main : IO ()
main = do
  text <- fRead stdin forever
  case parseGrid text of
    Nothing => putStrLn "Invalid starting position"
    Just ((n, m) ** grid) => runLife conway grid forever

max_stars_repo_name: pnotequalnp/game-of-life

max_issues_repo_name: pnotequalnp/game-of-life

max_forks_repo_name: pnotequalnp/game-of-life


text:
||| Interface and utilities for encoding Idris2 values to JSON
||| by using the functionality from JS.Object and Javascript's
||| internal JSON stringifier.
|||
||| For regular algebraic data types, implementations can automatically
||| be derived using elaborator reflection.
|||
||| Operators and functionality strongly influenced by Haskell's aeson
||| library
|||
||| Note: This should eventually be generalized for different
||| `Value` types and be moved to its own library.
module JS.JSON.ToJSON

import Data.Vect
import Data.List1
import JS.Array
import JS.Number
import JS.Object
import JS.Undefined

import Generics.Derive

%language ElabReflection

public export
interface ToJSON a where
  toJSON : a -> Value

infixr 8 .=

export
(.=) : ToJSON a => String -> a -> (String,Value)
s .= v = (s, toJSON v)

export
encode : ToJSON a => a -> String
encode v = stringify $ toJSON v

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

export
ToJSON Void where
  toJSON x impossible

export
ToJSON Value where toJSON = id

export
ToJSON String where toJSON = Str

export
ToJSON Char where toJSON = Str . singleton

export
ToJSON Double where toJSON = Num

export
ToJSON Bits8 where toJSON = Num . cast

export
ToJSON Bits16 where toJSON = Num . cast

export
ToJSON Bits32 where toJSON = Num . cast

export
ToJSON Bits64 where toJSON = toJSON . show

export
ToJSON Int where toJSON = toJSON . show

export
ToJSON Integer where toJSON = toJSON . show

export
ToJSON Nat where toJSON = toJSON . show

export
ToJSON Bool where toJSON = Boolean

export
ToJSON Int8 where toJSON = Num . cast

export
ToJSON Int16 where toJSON = Num . cast

export
ToJSON Int32 where toJSON = Num . cast

export
ToJSON Int64 where toJSON = Num . cast

export
ToJSON a => ToJSON (Maybe a) where
  toJSON Nothing  = Null
  toJSON (Just a) = toJSON a

export
ToJSON a => ToJSON (Optional a) where
  toJSON Undef  = Null
  toJSON (Def a) = toJSON a

export
ToJSON a => ToJSON (IArray a) where
  toJSON = Arr . map toJSON

export
ToJSON a => ToJSON (List a) where
  toJSON = toJSON . JS.Array.fromList

export
ToJSON a => ToJSON (List1 a) where
  toJSON = toJSON . forget

export
ToJSON a => ToJSON (Vect n a) where
  toJSON = toJSON . toList

export
ToJSON () where
  toJSON () = Arr neutral

export
(ToJSON a, ToJSON b) => ToJSON (Either a b) where
  toJSON (Left a)  = pairs ["Left"  .= a]
  toJSON (Right b) = pairs ["Right" .= b]

--------------------------------------------------------------------------------
--          SOP Implementations
--------------------------------------------------------------------------------

np : NP (ToJSON . f) ks => NP f ks -> List Value
np = collapseNP . hcmap (ToJSON . f) toJSON

export
NP (ToJSON . f) ks => ToJSON (NP f ks) where
  toJSON = toJSON . np

export
(ToJSON a, ToJSON b) => ToJSON (a,b) where
  toJSON (a,b) = toJSON $ the (NP I _) [a,b]

-- TODO: This should go as a utility or interface to idris2-sop
export
unfoldNP : NP f ks -> (a -> a) -> a -> NP (K a) ks
unfoldNP []     _ _ = []
unfoldNP (_::t) f x = x :: unfoldNP t f (f x)

export
indices : NP f ks ->  NP (K Bits32) ks
indices np = unfoldNP np (+1) (the Bits32 0)

ns : (all : NP (ToJSON . f) ks) => NS f ks -> Value
ns = collapseNS . hcliftA2 (ToJSON . f) enc (indices all)
  where enc : ToJSON (f a) => Bits32 -> f a -> Value
        enc ix v = pairs [show ix .= v]

export
NP (ToJSON . f) ks => ToJSON (NS f ks) where
  toJSON = ns

--------------------------------------------------------------------------------
--          Elab Deriving
--------------------------------------------------------------------------------

-- Converts a single applied constructor, without pairing it
-- with its name.
toJSONC1 : NP (ToJSON . f) ks => ConInfo ks -> NP f ks -> Value
toJSONC1 info args = maybe (toJSON args) encRecord (argNames info)

  where encRecord : NP (K String) ks -> Value
        encRecord ns = pairs (collapseNP $ hcliftA2 (ToJSON . f) (.=) ns args)

toJSONSOP1 : NP (ToJSON . f) ks => TypeInfo [ks] -> SOP f [ks] -> Value
toJSONSOP1 (MkTypeInfo _ _ (v :: [])) (MkSOP (Z x)) = toJSONC1 v x
toJSONSOP1 (MkTypeInfo _ _ (v :: [])) (MkSOP (S x)) impossible

-- Converts a single applied constructor, pairing it with its name
toJSONC : NP (ToJSON . f) ks => ConInfo ks -> NP f ks -> Value
toJSONC i@(MkConInfo _ n _) np = pairs [(n, toJSONC1 i np)]

toJSONSOP :  (all : POP (ToJSON . f) kss)
        => TypeInfo kss -> SOP f kss -> Value
toJSONSOP {all = MkPOP _} (MkTypeInfo _ _ cons) =
  collapseNS . hcliftA2 (NP $ ToJSON . f) toJSONC cons . unSOP

export
genToJSON1 : Meta a [ks] => NP ToJSON ks => a -> Value
genToJSON1 = toJSONSOP1 (metaFor a) . from

export
genToJSON : Meta a code => POP ToJSON code => a -> Value
genToJSON = toJSONSOP (metaFor a) . from

public export
mkToJSON : (toJSON : a -> Value) -> ToJSON a
mkToJSON = %runElab check (var $ singleCon "ToJSON")

namespace Derive

  ||| Derives a `ToJSON` implementation for the given data type
  export
  ToJSON : DeriveUtil -> InterfaceImpl
  ToJSON g = MkInterfaceImpl "ToJSON" Export []
                    `(mkToJSON genToJSON)
                    (implementationType `(ToJSON) g)

  ||| Derives a `ToJSON` implementation for the given single-constructor
  ||| data type
  export
  ToJSON1 : DeriveUtil -> InterfaceImpl
  ToJSON1 g = MkInterfaceImpl "ToJSON" Export []
                    `(mkToJSON genToJSON1)
                    (implementationType `(ToJSON) g)


text:
data Zuple : Type where
    Empty : Zuple
data Monople : Type -> Type where
    Single : a -> Monople a
data Duple : Type -> Type -> Type where
    Dup : a -> b -> Duple a b

append : Duple a b -> c -> Duple (Duple a b) c
append = Dup

--succTup : Duple a b -> Type -> Type
--succTup d t = Duple (Duple a b) t

{-
data NTuple : (n : Nat) -> Type where
    Empty : NTuple 0
    --Singple : (t : Type) -> (x : t) -> NTuple 1
    NTup : NTuple n -> (t : Type) -> (x : t) -> NTuple (S n)

implementation Show (NTuple n) where
    show Empty = "()"
    show (NTup first thist elem) = (Prelude.Strings.++) (show elem) (show first)
-}
{-
implementation Show (NTuple 0) where
    show Empty = "()"

implementation (Show (NTuple n)) => Show (NTuple (S n)) where
    show (NTup first thist elem) = (Prelude.Strings.++) (show elem) (show first)
-}
{-
interface IsTuple (t : Nat -> Type) where
    nextType : t -> (n : Nat) -> t (S n)

implementation IsTuple (
-}

ntypes : (n : Nat) -> Type
ntypes Z = Type
ntypes (S n) = Type -> ntypes n

-- uncurry : (n : Nat) -> ntypes n -> Vector n Type
-- uncurry 2 f

ntuple : (n : Nat) -> ntypes n
ntuple Z = Zuple
ntuple (S Z) = \a => Monople a
ntuple (S (S Z)) = \a => \b => Duple a b
\a => \b => \c => Duple (Duple a b) c
ntuple (S n) = \c => Duple

layerTup : Type -> Type -> Type
layerTup a b = Duple a b

layer2Tup : Type -> Type -> Type -> Type
layer2Tup a b t = Duple (Duple a b) t

layer3Tup : Type -> Type -> Type -> Type -> Type
layer3Tup a b t1 = Duple (layer2Tup a b t1)

layerNTup : (n : Nat) -> ntypes (S n)
layerNTup (S n) = Duple (layerNTup n)


text:
module Main
-- import Effects
-- import Effect.StdIO
-- import Prelude.Monad
-- import Sanity.Hello

-- Convenient for Idris build script
-- forces compiling of all modules
import Part1.Sec1_4_5
import Part1.Sec2_2_2_the
import Util.MiniParser
import Part2.Sec3_2_3_gen
import Part2.Sec4_2_2_gen
import Part2.Sec5_3_3_dpair
import Part2.Sec6_1_1_tyfunc
import Part2.Sec6_2_1_adder
import Part2.Sec6_2_2_printf
import Part2.Sec6_3_datastore
import Part2.Sec6_3b_datastore
import Part2.Sec8_1_eqproof
import Part2.Sec8_2_5_vappd
import Part2.Sec8_2z_reverse
import Part2.Sec8_3_deceq
import Part2.Sec9_1_elem
import Part2.Sec9_2_hangman
import Part2.Sez10_1_views
import Part2.Sez10_2a_snoc
import Part2.Sez10_2b
import Part2.Sez10_2e
import Part2.Sez10_3_hiding
import Part3.Sec14a_DoorJam
import Part3.Sec14b_ATM
import Part3.Sec15a_ProcessLib
import Part3.Sec15b_ProcessList
import Play.FunctorLaws
import Play.RankN

main : IO ()
main = sec6_3b
   --do
   -- run sayHello
   -- putStrLn (valToString True 20)

max_stars_repo_name: rpeszek/IdrisTddNotes

max_issues_repo_name: rpeszek/IdrisTddNotes

max_forks_repo_name: rpeszek/IdrisTddNotes


text:
module Syntax.Reader

import Modified.Parser
import Syntax.Tokens
import Data.List1
import Error.Data
import Loc

public export
data TermExpr
  = TList Range (List TermExpr)
  | TStr  Range String
  | TInt  Range Int
  | TId   Range String

public export
getRange : TermExpr -> Range
getRange (TList r _) = r
getRange (TStr  r _) = r
getRange (TInt  r _) = r
getRange (TId   r _) = r

-- Rule type is the entry point of the reader, It receives Locs and Tkns and
-- Will return in the end a (List (TopLevel Range)).

Rule : Type -> Type
Rule ty = Grammar ErrorType (Range, Tkn) True ty

-- These are the "primitive" functions to make the parsing
expect : Range -> ExpectType -> Tkn -> ParserError ErrorType
expect loc exp actual =
  ErrorCustom $ ReadingError loc $ Expected exp actual

error : Range -> ReaderError -> ParserError ErrorType
error loc err =
  ErrorCustom $ ReadingError loc err

tknRange : Tkn -> Rule Range
tknRange expected = terminal (\(loc, actual) =>
    if actual == expected
      then Right $ loc
      else Left  $ expect loc (ExpectTkn expected) actual)

tkn : Tkn -> Rule ()
tkn res = do
  resP <- tknRange res
  pure ()

identifier : Rule TermExpr
identifier = terminal (\(loc, actual) =>
  case actual of
    TknId x => Right $ TId loc x
    _       => Left  $ expect loc ExpectId actual)

integer : Rule TermExpr
integer = terminal (\(loc, actual) =>
  case actual of
    TknNum x => Right $ TInt loc x
    _        => Left  $ expect loc ExpectInt actual)

string : Rule TermExpr
string = terminal (\(loc, actual) =>
  case actual of
    TknStr x => Right $ TStr loc x
    _        => Left  $ expect loc ExpectStr actual)

-- Actual rules for parsing

failClosedPar : BetweenType -> Range -> Rule Range
failClosedPar between range = do { eof; fail (error range $ NotClosed between)}

mutual
  call : Rule TermExpr
  call = do
    range    <- tknRange TknLPar
    res      <- many expr
    endRange <- mustWork $ tknRange TknRPar <|> failClosedPar Parenthesis range
    pure $ TList (mixRange range endRange) res

  list : Rule TermExpr
  list = do
    range    <- tknRange TknLSquare
    res      <- many expr
    endRange <- mustWork $ tknRange TknRSquare <|> failClosedPar SquareBrackets range
    mixedRange <- pure $ mixRange range endRange
    pure $ TList mixedRange ((TId mixedRange "list") :: res)

  set : Rule TermExpr
  set = do
    range    <- tknRange TknLCurly
    res      <- many expr
    endRange <- mustWork $ tknRange TknRCurly <|> failClosedPar CurlyBrackets range
    mixedRange <- pure $ mixRange range endRange
    pure $ TList mixedRange ((TId mixedRange "set") :: res)

  expr : Rule TermExpr
  expr = string
     <|> identifier
     <|> integer
     <|> list
     <|> call
     <|> set

  program : Rule (List TermExpr)
  program = do
    res <- forget <$> some call
    eof
    pure res

public export
readToTerm : List (Range,Tkn) -> Either ErrorType (List TermExpr)
readToTerm ls =
  case parse program ls of
    Right (res, []) => Right res
    Right (res, (r, hd) :: tl)                 => Left (ReadingError r $ Expected Unknown hd)
    Left  (ExpectedEndOfInput, ((r, hd)::tl))  => Left (ReadingError r $ Expected TknEOF hd)
    Left  (ErrorCustom err, _)                 => Left err
    Left  (EndOfInput, heh)                    => Left EOF
    Left  (err, _)                             => Left UnexpectedInternalError

max_stars_repo_name: felipegchi/Yurei

max_issues_repo_name: felipegchi/Yurei

max_forks_repo_name: felipegchi/Yurei


text:
module Wheres

import Stuff

reverse : List a -> List a
reverse xs = rev' Nil xs
  where
    rev' : List a -> List a -> List a
    rev' acc Nil = acc
    rev' acc (x :: xs) = rev' (x :: acc) xs

foo : Int -> Int
foo x = case isLT of
            Yes => prim__mul_Int x 2
            No => prim__mul_Int x 4
  where
    data MyLT = Yes | No

    isLT : MyLT
    isLT = ifThenElse (intToBool (prim__lt_Int x 20)) Yes No


text:
module Extra.Op

public export
(>>) : (a -> b) -> (b -> c) -> (a -> c)
(>>) f g = g . f
infixr 9 >>

public export
(|>) : a -> (a -> b) -> b
(|>) x f = f x
infixr 5 |>

max_stars_repo_name: Z-snails/inigo

max_issues_repo_name: Z-snails/inigo

max_forks_repo_name: Z-snails/inigo


text:
module Data.TCQueue

%default total

public export
data Tree : (f : Type -> Type) -> (a, b : Type) -> Type where
  Leaf : (a -> f b) -> Tree f a b
  Node : {0 x : _} -> Tree f a x -> Tree f x b -> Tree f a b

public export
data TCQueue : (f : Type -> Type) -> (a, b : Type) -> Type where
  Empty  : TCQueue f a a
  Filled : Tree f a b -> TCQueue f a b

public export %inline
empty : TCQueue f a a
empty = Empty

public export %inline
singleton : (a -> f b) -> TCQueue f a b
singleton = Filled . Leaf

public export
cons : (a -> f x) -> TCQueue f x b -> TCQueue f a b
cons g Empty      = singleton g
cons g (Filled y) = Filled (Node (Leaf g) y)

public export
snoc : TCQueue f a x -> (x -> f b) -> TCQueue f a b
snoc Empty g      = singleton g
snoc (Filled y) g = Filled (Node y (Leaf g))

public export
(++) : TCQueue f a x -> TCQueue f x b -> TCQueue f a b
Empty    ++ w        = w
v        ++ Empty    = v
Filled v ++ Filled w = Filled (Node v w)

infixr 5 :|

||| Left-edge deconstruction
public export
data ViewL : (f : Type -> Type) ->  (a,b : Type) -> Type where
  EmptyV : ViewL f a a
  (:|)   : {0 x : _} -> (a -> f x) -> (TCQueue f x b) -> ViewL f a b

public export
uncons : TCQueue f a b -> ViewL f a b
uncons Empty               = EmptyV
uncons (Filled $ Leaf g)   = g :| Empty
uncons (Filled $ Node v w) = go v w
  where go : Tree f a x -> Tree f x b -> ViewL f a b
        go (Leaf g) w   = g :| Filled w
        go (Node y z) w = go y (Node z w)


text:
module Minecraft.Core.Block

import Minecraft.Core
import public Minecraft.Data.Deserialize
import public Minecraft.Data.Type.Ctx

%default total

public export
interface Eq self => Deserialize self => Block (self : Type) where
  id : String

public export
blockDeserialize : Block b -> Deserialize b
blockDeserialize = %search

public export
blockSerialize : Block b -> Serialize b
blockSerialize = %search

max_stars_repo_name: po-stulate/postulate

max_issues_repo_name: po-stulate/postulate

max_forks_repo_name: po-stulate/postulate


text:
module Linear.V

import Data.Floating
import Data.Void
import Data.Nat
import public Data.Vect

public export
V : Nat -> Type -> Type
V = Vect

public export
T : List Nat -> Type -> Type
T [] a = a
T (n :: ns) a = V n (T ns a)

export
{n : _} -> FromDouble a => FromDouble (V n a) where
  fromDouble = pure . fromDouble

export
{n : _} -> Num a => Num (V n a) where
  (+) = zipWith (+)
  (*) = zipWith (*)
  fromInteger = pure . fromInteger

export
{n : _} -> Neg a => Neg (V n a) where
  (-) = zipWith (-)
  negate = map negate

export
{n : _} -> Fractional a => Fractional (V n a) where
  (/) = zipWith (/)
  recip = map recip

export
{n : _} -> Floating a => Floating (V n a) where
  pi = pure pi
  exp = map exp
  ln = map ln
  sqrt = map sqrt
  pow = zipWith pow
  log = zipWith log
  sin = map sin
  cos = map cos
  tan = map tan
  asin = map asin
  acos = map acos
  atan = map atan
  sinh = map sinh
  cosh = map cosh
  tanh = map tanh

export
dot : (Num a, Foldable f, Zippable f) => f a -> f a -> a
dot x y = sum $ zipWith (*) x y

punch : V i a -> V (S j) a -> V (S j) (V (i + j) a)
punch {j = Z} xs (y :: []) = [rewrite plusZeroRightNeutral i in xs]
punch {j = S j} xs (y :: (y' :: ys)) =
  (xs ++ (y' :: ys)) :: (rewrite sym $ plusSuccRightSucc i j in punch (xs `snoc` y) (y' :: ys))

flipflop : Neg a => Bool -> V n a -> V n a
flipflop _ [] = []
flipflop False (x :: xs) = x :: flipflop True xs
flipflop True (x :: xs) = negate x :: flipflop False xs

export
det : {n : _} -> Neg a => T [S n, S n] a -> a
det {n = Z} [[n]] = n
det {n = S n} xs = sum $ zipWith (*) (flipflop False (map head xs)) (map det $ punch [] (map tail xs))

export
eye : Num a => {n : _} -> V n (V n a)
eye {n = Z} = []
eye {n = S n} = (1 :: pure 0) :: map (0 ::) eye

infix 7 *^, ^*, *!, !*
export
(*^) : (Functor f, Num a) => a -> f a -> f a
(*^) a = map (a *)

export
(^*) : (Functor f, Num a) => f a -> a -> f a
(^*) = flip (*^)

export
(*!) : (Num a, Num (f a), Functor f, Foldable f, Foldable t, Zippable t) => t a -> t (f a) -> f a
f *! g = sum $ zipWith (*^) f g

export
(!*) : Num a => Foldable t => Functor f => Zippable t => f (t a) -> t a -> f a
m !* v = map (\r => sum $ zipWith (*) r v) m

infixl 7 !*!
export
(!*!) : Num a => Num (n a) => Functor m => Foldable t => Zippable t => Zippable n => Functor n => m (t a) -> t (n a) -> m (n a)
xs !*! ys = map (\x => foldl (+) 0 (zipWith (*^) x ys)) xs

export
outer : (Functor f, Functor g, Num a) => f a -> g a -> f (g a)
outer a b = map (\x => map (* x) b) a

public export
prod : List Nat -> Nat
prod [] = 1
prod (x :: xs) = x * prod xs

-- multRightSuccPlus : (left : Nat) -> (right : Nat) -> left * S right = left + (left * right)

export
group : (n : Nat) -> (m : Nat) -> V (n * m) a -> V n (V m a)
group Z     _ _  = []
group (S n) m xs = let (l, r) = splitAt m xs in l :: group n m r

export
ranged : (n : _) -> T [n] Nat
ranged Z = []
ranged (S i) = Z :: map S (ranged i)

export
bump : (size : List Nat) -> {n : _} -> {auto prf : n = prod size} -> V n a -> T size a
bump [] {n} xs with (prf)
  bump [] {n = 1} [x] | Refl = x
bump (m :: ms) {n} xs with (prf)
  bump (m :: ms) {n = m * prod ms} xs | Refl = map (bump ms) $ group m (prod ms) xs

export
dump : {ns : _} -> T ns a -> V (prod ns) a
dump {ns = []} x = [x]
dump {ns = n :: ns} x = concat $ map dump x

export
reshape : (size : _) -> {auto ns : _} -> {auto prf : prod ns = prod size} -> T ns a -> T size a
reshape size = bump size . dump


text:
module Main

import Dart.FFI

libsmall : String -> String
libsmall fn = "Dart:" ++ fn ++ ",./libsmall.dart"

%inline
export
Point : Type
Point = Struct "Point,./libsmall.dart" [("x", Int), ("y", Int)]

Show Point where
  show pt = show (the Int (getField pt "x"), the Int (getField pt "y"))

namespace Point

  namespace New

    data Tag : Type where

    %inline
    public export
    x : Parameter Tag
    x = MkParameter "x" Int Tag

    %inline
    public export
    y : Parameter Tag
    y = MkParameter "y" Int Tag

  %inline
  public export
  new : Parameters [New.x, New.y] -> IO Point
  new ps = primIO $ prim__dart_new Point [] ps

%inline
export
Callbacks : Type
Callbacks = Struct "Callbacks,./libsmall.dart" []

namespace Callbacks

  namespace New

    data Tag : Type where

    %inline
    public export
    x : Parameter Tag
    x = MkParameter "x" (Int -> Int) Tag

    %inline
    public export
    y : Parameter Tag
    y = MkParameter "y" (Int -> IO Int) Tag

  %inline
  public export
  new : Parameters [Callbacks.New.x, Callbacks.New.y] -> IO Callbacks
  new ps = primIO $ prim__dart_new Callbacks [] ps

  export
  %foreign "Dart:.callX"
  callX : Callbacks -> Int -> Int

  export
  %foreign "Dart:.callY"
  callY : Callbacks -> Int -> PrimIO Int

main : IO ()
main = do
  pt <- Point.new [
    x @= 42,
    y @= 37
  ]
  printLn pt

  cb <- Callbacks.new [
    x @= (\i => i * 2),
    y @= (\i => printLn i *> pure (i * 2))
  ]
  printLn (callX cb 21)
  printLn !(primIO (callY cb 21))


text:
module ParseNumber

import DataTypes
import ParserCombinator
import Ratio
import Util
import Data.Complex

%access public export

--------------
-- Integer
--------------
converterHelper : (Char -> Integer) -> Integer -> List Char -> Integer
converterHelper caster base xs = convert 0 xs
    where
        convert : Integer -> List Char -> Integer
        convert acc [] = acc
        convert acc (x::xs) = convert (acc + ((pow base (length xs)) * (caster x))) xs

parseIntegerHelper : (List Char -> Integer) -> Parser Char -> Parser LispVal
parseIntegerHelper converter parser =
  (char '-' *> (parseIntegerHelper' negate)) <|>
  (char '+' *> (parseIntegerHelper' id)) <|>
  (parseIntegerHelper' id)
  where
    parseIntegerHelper' : (Integer -> Integer) -> Parser LispVal
    parseIntegerHelper' op = LispInteger . op . converter <$> many1 parser

decConverter : Char -> Integer
decConverter c = case c of
    '0' => 0
    '1' => 1
    '2' => 2
    '3' => 3
    '4' => 4
    '5' => 5
    '6' => 6
    '7' => 7
    '8' => 8
    '9' => 9

octConverter : Char -> Integer
octConverter c = case c of
    '0' => 0
    '1' => 1
    '2' => 2
    '3' => 3
    '4' => 4
    '5' => 5
    '6' => 6
    '7' => 7

hexConverter : Char -> Integer
hexConverter c = case (toUpper c) of
    '0' => 0
    '1' => 1
    '2' => 2
    '3' => 3
    '4' => 4
    '5' => 5
    '6' => 6
    '7' => 7
    '8' => 8
    '9' => 9
    'A' => 10
    'B' => 11
    'C' => 12
    'D' => 13
    'E' => 14
    'F' => 15

binConverter : Char -> Integer
binConverter c = case c of
    '0' => 0
    '1' => 1

parseIntegerDecimal : Parser LispVal
parseIntegerDecimal = parseIntegerHelper converter digit
    where
        converter :  (List Char -> Integer)
        converter = converterHelper decConverter 10

parseIntegerOctal : Parser LispVal
parseIntegerOctal = parseIntegerHelper converter digit
    where
        converter :  (List Char -> Integer)
        converter = converterHelper octConverter 8

parseIntegerHex : Parser LispVal
parseIntegerHex = parseIntegerHelper converter hexDigit
    where
        converter :  (List Char -> Integer)
        converter = converterHelper hexConverter 16

parseIntegerBinary : Parser LispVal
parseIntegerBinary = parseIntegerHelper converter binDigit
    where
        converter :  (List Char -> Integer)
        converter = converterHelper binConverter 2

parseIntegerBase : Char -> Parser LispVal
parseIntegerBase base =
  case base of
    'd' => parseIntegerDecimal
    'o' => parseIntegerOctal
    'x' => parseIntegerHex
    'b' => parseIntegerBinary
    _ => failure "Bad integer format"

parseInteger : Parser LispVal
parseInteger =
    parseIntegerDecimal <|> parsePrefixedInteger
    where
        parsePrefixedInteger : Parser LispVal
        parsePrefixedInteger = do
            _ <- char '#'
            base <- oneOf "bdox"
            parseIntegerBase base

--------------
-- Float
--------------
parseFloatHelper : (List Char -> Integer) -> Parser Char -> Integer -> Parser LispVal
parseFloatHelper converter parser base =
  (char '-' *> (parseFloat' negate)) <|> (char '+' *> parseFloat' id) <|>
  (parseFloat' id)
  where
    helper : Integer -> Integer -> Double
    helper whole decimal =
      if decimal == 0 then the Double (cast whole)
      else
          let d = the Double (cast decimal)
              w = the Double (cast whole)
              b = the Double (cast base)
              e = logBase b d
              f = fromIntegerNat (the Integer (cast $ floor e))
              g = the Double (d / (pow b (f + 1)))
          in w + g
    parseFloat' : (Double -> Double) -> Parser LispVal
    parseFloat' op = do
      w <- many1 parser
      _ <- char '.'
      d <- many1 parser
      let whole = converter w
      let decimal = converter d
      pure $ LispFloat $ (op (helper whole decimal))

parseFloatDecimal : Parser LispVal
parseFloatDecimal = parseFloatHelper converter digit base
    where
        base : Integer
        base = 10
        converter :  (List Char -> Integer)
        converter = converterHelper decConverter base

parseFloatOctal : Parser LispVal
parseFloatOctal = parseFloatHelper converter octDigit base
    where
        base : Integer
        base = 8
        converter : (List Char -> Integer)
        converter = converterHelper octConverter base

parseFloatHex : Parser LispVal
parseFloatHex = parseFloatHelper converter hexDigit base
    where
        base : Integer
        base = 16
        converter :  (List Char -> Integer)
        converter = converterHelper hexConverter base

parseFloatBinary : Parser LispVal
parseFloatBinary = parseFloatHelper converter binDigit base
    where
        base : Integer
        base = 2
        converter :  (List Char -> Integer)
        converter = converterHelper binConverter base

parseFloatBase : Char -> Parser LispVal
parseFloatBase base =
  case base of
    'd' => parseFloatDecimal
    'o' => parseFloatOctal
    'x' => parseFloatHex
    'b' => parseFloatBinary
    _ => failure "Bad float format"

parseFloat : Parser LispVal
parseFloat =
  parseFloatDecimal <|> do
    _ <- char '#'
    base <- oneOf "bdox"
    parseFloatBase base

--------------
-- Rational
--------------
parseRationalHelper : Parser LispVal -> Parser LispVal
parseRationalHelper p =
    do
        num <- map toInt p
        _ <- char '/'
        denom <- map toInt p
        let ratio = (num :% denom)
        case ratio of
          Just rat => pure $ LispRational rat
          Nothing => failure "Division by zero"
    where
        toInt : LispVal -> Integer
        toInt (LispInteger x) = x

parseRationalDecimal : Parser LispVal
parseRationalDecimal = parseRationalHelper parseIntegerDecimal

parseRationalOctal : Parser LispVal
parseRationalOctal = parseRationalHelper parseIntegerOctal

parseRationalHex : Parser LispVal
parseRationalHex = parseRationalHelper parseIntegerHex

parseRationalBinary : Parser LispVal
parseRationalBinary = parseRationalHelper parseIntegerBinary

parseRationalBase : Char -> Parser LispVal
parseRationalBase base =
  case base of
    'd' => parseRationalDecimal
    'o' => parseRationalOctal
    'x' => parseRationalHex
    'b' => parseRationalBinary
    _ => failure "Bad rational format"

parseRational : Parser LispVal
parseRational =
  parseRationalDecimal <|> do
    _ <- char '#'
    base <- oneOf "bdox"
    parseRationalBase base

--------------
-- Complex
--------------
parseComplexHelper : Parser LispVal -> Parser LispVal -> Parser LispVal -> Parser LispVal
parseComplexHelper pn pf pr =
    do
        real <- map toDouble (pr <|> pf <|> pn)
        imaginary <- map toDouble (pr <|> pf <|> pn)
        _ <- char 'i'
        case (real, imaginary) of
          (Just r, Just i) => pure $ LispComplex (r :+ i)
          (_, _) => failure "Division by zero"
    where
        toDouble : LispVal -> Maybe Double
        toDouble (LispFloat x) = Just x
        toDouble (LispInteger x) = Just $ cast x
        toDouble (LispRational x) = rationalCast x

parseComplexDecimal : Parser LispVal
parseComplexDecimal =
  parseComplexHelper parseIntegerDecimal parseFloatDecimal parseRationalDecimal

parseComplexOctal : Parser LispVal
parseComplexOctal =
  parseComplexHelper parseIntegerOctal parseFloatOctal parseRationalOctal

parseComplexHex : Parser LispVal
parseComplexHex =
  parseComplexHelper parseIntegerHex parseFloatHex parseRationalHex

parseComplexBinary : Parser LispVal
parseComplexBinary =
  parseComplexHelper parseIntegerBinary parseFloatBinary parseRationalBinary

parseComplexBase : Char -> Parser LispVal
parseComplexBase base =
  case base of
    'd' => parseComplexDecimal
    'o' => parseComplexOctal
    'x' => parseComplexHex
    'b' => parseComplexBinary
    _ => failure "Bad complex format"

parseComplex : Parser LispVal
parseComplex =
  parseComplexDecimal <|> do
    _ <- char '#'
    base <- oneOf "bdox"
    parseComplexBase base

parseNumber : Parser LispVal
parseNumber = parseComplex <|> parseRational <|> parseFloat <|> parseInteger

max_stars_repo_name: ebenpack/lidrisp

max_issues_repo_name: ebenpack/lidrisp

max_forks_repo_name: ebenpack/lidrisp


text:
module VecTk

import Data.Vect
import Data.Fin

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

max_stars_repo_name: buzden/idris-playground

max_issues_repo_name: buzden/idris-playground

max_forks_repo_name: buzden/idris-playground


text:
||| The interfaces in this module abstract over how we
||| encode and decode values from and to JSON.
|||
||| This allows us to use different (probably backend dependant)
||| intermediary data representations to be used by the actual
||| marshallers `ToJSON` and `FromJSON`.
module JSON.Value

import Data.List
import Language.JSON

||| In Javascript, numbers are represented as IEEE 64bit
||| floating point numbers. Integers can be represented exactly
||| in the range [-(2^53-1), 2^53-1]. This library's default
||| behavior is, that large integers will be encoded as
||| `string` and smaller values use `number`
public export
maxSafeInteger : Integer
maxSafeInteger = 9007199254740991

--------------------------------------------------------------------------------
--          Encoding
--------------------------------------------------------------------------------

||| Abstraction over JSON value encoding.
public export
interface Encoder v where
  ||| Converts the intermediary data representation
  ||| to a JSON string.
  stringify : v -> String

  ||| Encodes a `String` value.
  string : String -> v

  ||| Encodes a `Double` as a JSON `Number`.
  number : Double -> v

  ||| Encodes a `Bool` as a JSON `Boolean`.
  boolean : Bool -> v

  ||| Encodes a `List` of values as a JSON `Array`.
  array : List v -> v

  ||| Encodes a `List` key-value pairs as a JSON `Object`
  object : List (String,v) -> v

  null : v

||| Encode a small integer (less than or equal to `maxSafeInteger`)
||| as a number.
export %inline
smallInteger : Encoder v => Integer -> v
smallInteger = number . fromInteger

||| Encode an `Integer` (possibly larger than `masSafeInteger`)
||| as a number or a string.
|||
||| The corresponding decoder for potentially large numbers
||| will also try both types: Number and string.
export %inline
largeInteger : Encoder v => Integer -> v
largeInteger n = if abs n <= maxSafeInteger
                    then smallInteger n
                    else string $ show n

--------------------------------------------------------------------------------
--          Decoding
--------------------------------------------------------------------------------

||| Abstraction over JSON Object representation for decoding.
||| It is important that `obj` is the type that guides interface
||| resolution here, otherwise operators like `.:` cannot conveniently
||| be used, since Idris needs additional guidance to resolve interfaces.
public export
interface Object obj v | obj where
  lookup : String -> obj -> Maybe v

||| Abstraction over JSON value representation for decoding.
public export
interface Object obj v => Value v obj | v where
  ||| Returns the actual value. This should be one of
  ||| "String", "Null", "Object", "Number", "Boolean", or "Array".
  ||| However, other types are possible as well, as this is
  ||| only used for error messages when something goes wrong.
  typeOf : v -> String

  ||| Tries to convert a string to an intermediare value.
  parse : String -> Either String v

  ||| Tries to convert a value to an `Object`.
  getObject : v -> Maybe obj

  ||| Tries to convert a value to an `Array` of values.
  getArray : v -> Maybe (List v)

  ||| Tries to convert a value to a `Boolean`.
  getBoolean : v -> Maybe Bool

  ||| Tries to convert a value to a `Number`.
  getNumber : v -> Maybe Double

  ||| Tries to convert a value to a `String`.
  getString : v -> Maybe String

  ||| `True`, if the value in question is `null`.
  isNull : v -> Bool

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

export %inline
Encoder JSON where
  stringify = show
  string    = JString
  number    = JNumber
  boolean   = JBoolean
  null      = JNull
  array     = JArray
  object    = JObject

export %inline
Object (List (String,JSON)) JSON where
  lookup = Data.List.lookup

export %inline
Value JSON (List (String,JSON)) where
  parse     = maybe (Left "Couldn't parse JSON.") Right . parse

  typeOf JNull        = "Null"
  typeOf (JBoolean _) = "Boolean"
  typeOf (JNumber _)  = "Number"
  typeOf (JString _)  = "String"
  typeOf (JArray _)   = "Array"
  typeOf (JObject _)  = "Object"

  getObject (JObject ps) = Just ps
  getObject _            = Nothing

  getNumber (JNumber v) = Just v
  getNumber _           = Nothing

  getBoolean (JBoolean v) = Just v
  getBoolean _            = Nothing

  getArray (JArray v) = Just v
  getArray _          = Nothing

  getString (JString v) = Just v
  getString _           = Nothing

  isNull JNull = True
  isNull _     = False


text:
module Types

mutual

  public export
  data Val = A String -- atom
           | L (List Val) -- list
           | D (List Val) Val -- Dotted List
           | N Integer -- num
           | S String -- string
           | B Bool -- bool
           | PrimitiveFunc (List Val -> ThrowsError Val)
           | Func (List String) (Maybe String) (List Val) Env

  public export
  data Error = ParserE String
             | BadSpecialForm String Val
             | NotFunction String String
             | NumArgs Integer (List Val)
             | TypeMismatch String Val
             | UnboundVar String String

  public export
  ThrowsError : Type -> Type
  ThrowsError = Either Error

  public export
  Env : Type
  Env = List (String, Val)

mutual
  unwordsList : List Val -> String
  unwordsList = unwords . map showVal

  p : Maybe String -> String
  p varargs = case varargs of
                   Nothing => ""
                   Just arg => " . " ++ arg

  export
  showVal : Val -> String
  showVal (A x) = x
  showVal (L xs) = "(" ++ unwordsList xs ++ ")"
  showVal (D xs x) = "(" ++ unwordsList xs ++ " . " ++ showVal x ++ ")"
  showVal (N x) = show x
  showVal (S x) = "\"" ++ x ++ "\""
  showVal (B True) = "#t"
  showVal (B False) = "#f"
  showVal (PrimitiveFunc _) = "<primitive>"
  showVal (Func args varargs body closure) = "(lambda (" ++ (unwords (map show args)) ++ (p varargs) ++ ") ...)"

export
Show Val where
  show = showVal

export
Show Error where
  show (ParserE e)          = "Parse error " ++ e
  show (UnboundVar m v)     = m ++ ": " ++ v
  show (BadSpecialForm s v) = s ++ " : " ++ show v
  show (NotFunction s f)    = s ++ " : " ++ show f
  show (NumArgs e f)        = "Expected " ++ show e ++ " args; found " ++ (show $ length f)
  show (TypeMismatch e f)   = "Invalid type: expected " ++ e ++ ", found " ++ show f
  show _                    = "Error!!!"


text:
module Chapter3

import Data.Vect

-- In this chapter we do interactive development using the
-- "type, define, refine" loop

allLengths : List String -> List Nat  -- <leader>_d
--allLengths xs = ?allLengths_rhs       -- <leader>_c over xs
allLengths [] = []
--allLengths (word :: words) = ?allLengths_rhs_2       -- <leader>_c
--allLengths (word :: words) = length word :: ?rest
-- <l>_e allLengths
-- ["abc", "cde"] will give partial evaluation
allLengths (word :: words) = length word :: allLengths words

xor : Bool -> Bool -> Bool
xor False y = y
xor True y = not y

isEven : Nat -> Bool
isEven Z = True
isEven (S k) = not (isEven k)

mutual
  isEven' : Nat -> Bool
  isEven' Z = True
  isEven' (S k) = isOdd' k

  isOdd' : Nat -> Bool
  isOdd' Z = False
  isOdd' (S k) = isEven' k

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

-- [1,2] is syntactic sugar to ANY datatype with :: and Nil constructors
-- the (Vect _ _) [1,2,3]
-- the (List _) [1,2]
total allLengths2 : Vect n String -> Vect n Nat  -- note we can annotate 'total'
-- (it is still attempted to be inferred by Idris)
allLengths2 [] = []
allLengths2 (x :: xs) = length x :: allLengths2 xs

allLengths3 : Vect n String -> Vect n Nat
allLengths3 [] = []
allLengths3 (word :: words) = length word :: allLengths3 words

-- See VecSort.idr

--createEmpties : Vect n (Vect 0 elem)
--createEmpties = replicate _ []  -- forced by the type to have n elements.
--
--transposeHelper : (x : Vect n elem) -> (xsTrans : Vect n (Vect len elem)) -> Vect n (Vect (S len) elem)
--transposeHelper [] [] = []
--transposeHelper (x :: xs) (y :: ys) = (x :: y) :: transposeHelper xs ys
--
--transposeMat : Vect m (Vect n elem) -> Vect n (Vect m elem)
--transposeMat [] = createEmpties
--transposeMat (x :: xs) = let xsTrans = transposeMat xs in
--                             transposeHelper x xsTrans

--transposeHelper : Vect m elem -> Vect m (Vect len elem) -> Vect m (Vect (S len) elem)
--transposeHelper [] [] = []
--transposeHelper (x :: xs) (y :: ys) = (x :: y) :: transposeHelper xs ys
--
--transposeMat : Vect n (Vect m elem) -> Vect m (Vect n elem)
--transposeMat [] = replicate _ []
--transposeMat (x :: xs) = let xsTrans = transposeMat xs in
--                             transposeHelper x xsTrans

-- Exercises
-- ex1
transposeMat : Vect n (Vect m a) -> Vect m (Vect n a)
transposeMat [] = replicate _ []
transposeMat (x :: xs) = let xsTrans = transposeMat xs in
--                           zipWith ?f x xsTrans  -- Did I say how much I love this language?
                             zipWith (::) x xsTrans

transposeMat2 : Vect n (Vect m a) -> Vect m (Vect n a)
transposeMat2 [] = replicate _ []
transposeMat2 (x :: xs) = zipWith (::) x (transposeMat2 xs)

--ex2
addMatrix : Num a => Vect n (Vect m a) -> Vect n (Vect m a) -> Vect n (Vect m a)
addMatrix [] [] = []
addMatrix (x :: xs) (y :: ys) = zipWith (+) x y :: addMatrix xs ys

addMatrix2 : Num a => Vect n (Vect m a) -> Vect n (Vect m a) -> Vect n (Vect m a)
addMatrix2 = zipWith (zipWith (+))  -- <3

--ex3 (without using transpose)
-- instead we rely on the observation that the result matrix's
-- first row is equal to first row of m1 times m2; hence
-- m1 x m2 = map (rowMult m2) m1
multMatrix : Num a => Vect n (Vect m a) -> Vect m (Vect p a) -> Vect n (Vect p a)
multMatrix m1 m2 = map (flip rowMult m2) m1
  where
    rowMult : Num a => Vect m a -> Vect m (Vect p a) -> Vect p a
    rowMult xs ms = foldr (zipWith (+)) (replicate _ 0) $ zipWith (\x,r => map (*x) r) xs ms

-- Type-level variables
-- Note how we were already were passing elem as an implicit argument.
myAppend : (elem : Type) -> (n : Nat) -> (m : Nat) -> Vect n elem -> Vect m elem -> Vect (n + m) elem
myAppend elem Z m [] ys = ys
myAppend elem (S len) m (x :: xs) ys = x :: myAppend elem len m xs ys

myLength : Vect n a -> Nat
myLength {n} xs = n  -- So much nicer than haskell!

createEmpties2 : Vect n (Vect 0 a)
createEmpties2 {n} = replicate n []

createEmpties3 : Vect n (Vect 0 a)
createEmpties3 {n = Z} = []
createEmpties3 {n = (S k)} = [] :: createEmpties3 {n = k}

createEmpties4 : Vect n (Vect 0 a)
createEmpties4 {n = Z} = []
createEmpties4 {n = (S k)} = [] :: createEmpties4  -- Wooot

max_stars_repo_name: neduard/type-driven-development

max_issues_repo_name: neduard/type-driven-development

max_forks_repo_name: neduard/type-driven-development


text:
-- test that things arrive in the order buffered

import System.Concurrency.BufferedChannel

main : IO ()
main =
  do bcRef <- makeBufferedChannel
     let val1 = 1
     let val2 = 2
     let val3 = 3
     (MkDPair bc buffer) <- becomeBuffer bcRef
     (MkDPair bc' recv) <- becomeReceiver Blocking bcRef
     buffer Signal bc [val1, val2, val3]
     val1' <- recv bc'
     val2' <- recv bc'
     val3' <- recv bc'
     if val1 /= val1'
        then putStrLn "ERROR: First value changed in transit."
        else if val2 /= val2'
                then putStrLn "ERROR: Second value changed in transit."
                else if val3 /= val3'
                        then putStrLn "ERROR: Third value changed in transit."
                        else putStrLn "Success!"


text:
module Data.Morphisms.Algebra

import Control.Algebra
import Data.Morphisms

%default total

public export
SemigroupV (Endomorphism ty) where
  semigroupOpIsAssociative (Endo _) (Endo _) (Endo _) = Refl

public export
MonoidV (Endomorphism ty) where
  monoidNeutralIsNeutralL (Endo _) = Refl
  monoidNeutralIsNeutralR (Endo _) = Refl


text:
module Erlang.Text.PrettyPrint.Prettyprinter.Render.Terminal

import Data.Maybe
import Data.Strings
import public Control.ANSI
import Erlang.Control.Monad.ST
import Text.PrettyPrint.Prettyprinter.Doc

%default covering

public export
AnsiStyle : Type
AnsiStyle = List SGR

export
color : Color -> AnsiStyle
color c = pure $ SetForeground c

export
bgColor : Color -> AnsiStyle
bgColor c = pure $ SetBackground c

export
bold : AnsiStyle
bold = pure $ SetStyle Bold

export
italic : AnsiStyle
italic = pure $ SetStyle Italic

export
underline : AnsiStyle
underline = pure $ SetStyle SingleUnderline

export
strike : AnsiStyle
strike = pure $ SetStyle Striked

export
renderString : SimpleDocStream AnsiStyle -> String
renderString sdoc = fromMaybe "<internal pretty printing error>" $ runST $ do
    styleStackRef <- newSTRef {a = List AnsiStyle} [neutral]
    outputRef <- newSTRef {a = String} neutral
    go styleStackRef outputRef sdoc
    readSTRef styleStackRef >>= \case
      [] => pure Nothing
      [_] => Just <$> readSTRef outputRef
      _ => pure Nothing
  where
    push : STRef s (List AnsiStyle) -> List SGR -> ST s ()
    push stack x = modifySTRef stack (x ::)

    peek : STRef s (List AnsiStyle) -> ST s (Maybe AnsiStyle)
    peek stack = do
      (x :: _) <- readSTRef stack | [] => pure Nothing
      pure (Just x)

    pop : STRef s (List AnsiStyle) -> ST s (Maybe AnsiStyle)
    pop stack = do
      (x :: xs) <- readSTRef stack | [] => pure Nothing
      writeSTRef stack xs
      pure (Just x)

    writeOutput : STRef s String -> String -> ST s ()
    writeOutput out x = modifySTRef out (<+> x)

    go : STRef s (List AnsiStyle) -> STRef s String -> SimpleDocStream AnsiStyle -> ST s ()
    go stack out SEmpty = pure ()
    go stack out (SChar c rest) = do
      writeOutput out (singleton c)
      go stack out rest
    go stack out (SText l t rest) = do
      writeOutput out t
      go stack out rest
    go stack out (SLine l rest) = do
      writeOutput out (singleton '\n' <+> textSpaces l)
      go stack out rest
    go stack out (SAnnPush style rest) = do
      Just currentStyle <- peek stack
        | Nothing => writeSTRef stack []
      let newStyle = style <+> currentStyle
      push stack newStyle
      writeOutput out (escapeSGR newStyle)
      go stack out rest
    go stack out (SAnnPop rest) = do
      _ <- pop stack
      Just newStyle <- peek stack
        | Nothing => writeSTRef stack []
      writeOutput out (escapeSGR (Reset :: newStyle))
      go stack out rest

export
renderIO : SimpleDocStream AnsiStyle -> IO ()
renderIO = putStrLn . renderString

export
putDoc : Doc AnsiStyle -> IO ()
putDoc = renderIO . layoutPretty defaultLayoutOptions


text:
{------------------------------------------------------------------------------
    IdrUtils.idr
------------------------------------------------------------------------------}

||| Miscellaneous Idris utilities.

module IdrUtils

import Debug.Error

%language ElabReflection -- for Debug.Error.error

%default total

-------------------------------------------------------------------------------
--  unwrap                                                                   --
-------------------------------------------------------------------------------

||| Unsafe unwrap of `Maybe` value.
export
unwrap : Maybe a -> a
unwrap = fromMaybe $
  error "unwrap failed: expected Just something, found Nothing"

-------------------------------------------------------------------------------
--  test                                                                     --
-------------------------------------------------------------------------------

export
test : IO ()
test = do
  let foo = [1,2,3]
  let one = unwrap $ index' 0 foo
  putStrLn $ "one: " ++ show one

max_stars_repo_name: spearman/idr-utils

max_issues_repo_name: spearman/idr-utils

max_forks_repo_name: spearman/idr-utils


text:
module Erlang.System.Directory

import Erlang
import public Erlang.System.File

%default total

export
createDir : HasIO io => String -> io (Either FileError ())
createDir dirPath = do
  result <- pure $ erlUnsafeCall ErlTerm "file" "make_dir" [dirPath]
  pure $ erlDecodeDef
    (Left unknownError)
    (exact (MkAtom "ok") *> pure (Right ())
      <|> map Left error)
    result

export
changeDir : HasIO io => String -> io Bool
changeDir dirPath = do
  result <- pure $ erlUnsafeCall ErlTerm "file" "set_cwd" [dirPath]
  pure $ erlDecodeDef False (exact (MkAtom "ok") *> pure True) result

export
currentDir : HasIO io => io (Maybe String)
currentDir = do
  result <- pure $ erlUnsafeCall ErlTerm "file" "get_cwd" []
  pure $ erlDecodeMay (map (\(MkCharlist dirPath) => dirPath) (okTuple charlist)) result

export
removeDir : HasIO io => String -> io ()
removeDir dirPath = do
  pure $ erlUnsafeCall ErlTerm "file" "del_dir_r" [dirPath]
  pure ()

-- TODO: Should this function return `.` and `..`? The Chez codegen does this
export
dirEntries : HasIO io => String -> io (Either FileError (List String))
dirEntries dirPath = do
  result <- pure $ erlUnsafeCall ErlTerm "file" "list_dir" [dirPath]
  pure $ erlDecodeDef
    (Left unknownError)
    (map (\files => Right (map (\(MkCharlist file) => file) files)) (okTuple (list charlist))
      <|> map Left error)
    result

export
dirExists : HasIO io => String -> io Bool
dirExists dirPath = do
  result <- pure $ erlUnsafeCall ErlTerm "filelib" "is_dir" [dirPath]
  pure $ erlDecodeDef False (exact (MkAtom "true") *> pure True) result


text:
module LittleInterpreter

import LittleLang

-- This is not needed, plus does not work. We just use reduce in LittleLang.

-- Many cases commented out to appease typechecker
eqExp : (a: Ty) -> (b: Ty) -> Exp a -> Exp b -> Bool
eqExp NT NT (N k) (N l) = k == l
eqExp BT BT (B x) (B y) = x == y
eqExp NT b (N k) y = False
eqExp BT b (B x) y = False
eqExp BT BT (LTE x z) (LTE p q) = (eqExp NT NT x p) && (eqExp NT NT z q)
eqExp BT BT (EQ x z) (EQ p q)  = (eqExp NT NT x p) && (eqExp NT NT z q)
eqExp BT b (LTE x z) y = False
eqExp BT b (EQ x z) y = False
-- eqExp a b (If x z w) (If p q r) =
--   (eqExp BT BT x p) && (eqExp a b z q) && (eqExp a b w r)
-- eqExp a b (If x z w) y = False
-- eqExp a b (Var name a) (Var other b) = (name == other) && eqTyp a b
-- eqExp a b (Var name a) y = False
-- eqExp (FT domain codomain) (FT dd cc) (Lam var value) (Lam vr vl) =
--   (eqExp domain dd var vr) && (eqExp codomain cc value vl)
-- eqExp (FT domain codomain) b (Lam var value) y = False
-- eqExp a b (App x a f arg) (App y b g ar) =
--   (eqExp (FT x a) (FT y b) f g)
--   && (eqExp x y arg ar)
-- eqExp a b (App x a f arg) y = False
-- eqExp NT NT (Sum x z) (Sum p q) = (eqExp NT NT x p) && (eqExp NT NT z q)
-- eqExp NT NT (Pred x) (Pred y) = eqExp NT NT x y
-- eqExp NT a (Pred x) y = False
-- eqExp NT NT (Prod x z) (Prod p q) = (eqExp NT NT x p) && (eqExp NT NT z q)
-- eqExp NT b (Sum x z) y = False
-- eqExp NT b (Prod x z) y = False

interpret : (ctx: Context) -> (a: Ty) -> (exp : Exp a) -> Exp a
interpret ctx a exp =
  let next = simplify ctx a exp
  in
    if eqExp a a exp next then exp else interpret ctx a next


text:
-- new queue should be empty

import System.Concurrency.Queue

main : IO ()
main = do q <- makeQueue {a=Nat}
          Nothing <- dequeue q
            | (Just x) => putStrLn "ERROR: New queue contained something."
          putStrLn "Success!"


text:
module Flexidisc.OrdList.Disjoint

import Flexidisc.Dec.IsYes
import Flexidisc.OrdList.Fresh
import Flexidisc.OrdList.Label
import Flexidisc.OrdList.Nub
import Flexidisc.OrdList.Type

%default total
%access public export

||| A proof that two `OrdList` don't share a key.
data Disjoint : (left, right : OrdList k v o) -> Type where
  ||| The empty `OrdList` is always `Disjoint` from another `OrdList`
  Nil : Disjoint [] right
  ||| A key in the first `OrdList` is fresh in the second `OrdList`.
  (::) : DecEq l => {k : l} -> IsFresh k right -> Disjoint left right ->
                    Disjoint ((k,v) :: left) right

%name Disjoint djt, dis, prf

freshInMerge : Fresh l left -> Fresh l right -> Fresh l (merge left right)
freshInMerge [] freshR = freshR
freshInMerge (f :: fresh) [] = f :: fresh
freshInMerge (f :: fresh) (g :: prf)
  {left = ((ll, tl) :: xs)} {right = ((lr, tr) :: hs)} with (ll < lr)
  | True  = f :: freshInMerge fresh (g :: prf)
  | False = g :: freshInMerge (f :: fresh) prf

invertFresh : Disjoint left ((lr, ty)::right) -> Fresh lr left
invertFresh [] = []
invertFresh (fresh :: djt) =
  (\(f :: _) => f . sym) (getProof fresh) :: invertFresh djt

disjointSmallerRight : Disjoint left (r::right) -> Disjoint left right
disjointSmallerRight [] = []
disjointSmallerRight (fresh :: djt) =
  tailIsFresh fresh :: disjointSmallerRight djt

disjointNub : Disjoint left right -> Nub left -> Nub right ->
              Nub (merge left right)
disjointNub djt [] z = z
disjointNub djt (yes :: x) [] = yes :: x
disjointNub (fll :: djt) (yes :: x) (prf :: w)
  {left = ((ll, tl) :: xs)} {right = ((lr, tr) :: hs)} with (ll < lr)
  | True  = freshInMerge yes (getProof fll) :: disjointNub djt x (prf :: w)
  | False = freshInMerge (invertFresh (fll :: djt)) prf
              :: disjointNub (disjointSmallerRight (fll :: djt)) (yes :: x) w

max_stars_repo_name: berewt/flexidisc

max_issues_repo_name: LIST-LUXEMBOURG/flexidisc

max_forks_repo_name: LIST-LUXEMBOURG/flexidisc


text:
module Equis.Solver

import Matrix.Numeric
import Data.Matrix.Numeric

%access private

||| Solves a system of linear equations.
|||
||| @coeff the matrix of coefficients
||| @sols the solutions
export
solve : Neg a => Fractional a => (coeff : Matrix (S n) (S n) a) -> (sols : Vect (S n) a) -> Vect (S n) a
solve coeff sols = (inverse coeff) </> sols

max_stars_repo_name: lambdacasserole/equis

max_issues_repo_name: lambdacasserole/equis

max_forks_repo_name: lambdacasserole/equis


text:
module Language.Elab.Deriving.Show

import public Language.Elab.Syntax
import public Language.Reflection

import public Language.Elab.Types

import public Util

import public Data.Strings -- fastAppend

-- NB uses of things like show in the repl can cause ambiguity issues, confirm
-- this is a problem before submitting a complaint. Refer to the note at
-- bottom of this file.

intercalate_str : String -> List String -> String
intercalate_str sep ss = fastAppend (intersperse sep ss)

-- A regular isntance might look like (Show a, Show b, Show c) => ...
-- This pairing isn't actually neccesary, it's just notational convenience and
-- we don't really have a reason to emulate it.
-- Show a => Show b => ...  is just as valid as (Show a, Show b) => ...
-- It also can result in clearer errors.
addShowAutoImps : List String -> TTImp -> TTImp
addShowAutoImps xs retty
  = foldr (\arg,tt => `(Show ~(iBindVar arg) => ~(tt))) retty xs

-- It works! We still need to prune requiring Show on tvars that aren't
-- actually used, since otherwise users have to provide it.
showClaim : (opname : Name) -> TypeInfo -> Visibility -> Elab Decl
showClaim op tyinfo vis = do
  let conargs = pullExplicits tyinfo
      varnames = map (show . name) conargs
      varnames' = map (show . name) (filter (isType . type) conargs)
      tysig = `(~(appTyCon (map (show . name) conargs) tyinfo.name) -> String)
  -- NB: I can't think of a reason not to Inline here
  pure $ iClaim MW vis [Inline] (mkTy op (addShowAutoImps varnames' tysig))

showCon : (opname : Name) -> Constructor -> Elab Clause
showCon op con = do
    let varnames = filter (isExplicitPi . piInfo) con.args
        lhsvars = map (show . name) varnames
        rhsvars = map (\arg => if isUse0 (count arg)
                             then Nothing
                             else Just (show arg.name)) varnames
        lhs = iVar op `iApp`
                foldl (\tt,v => `(~(tt) ~(iBindVar v))) (iVar con.name) lhsvars
        rhs = foldl (\tt,v => `( ~(tt) ++ " " ++ ~(beShown v)))
                (iPrimVal (Str !(showName con.name))) rhsvars
    pure $ patClause lhs rhs
  where
    beShown : Maybe String -> TTImp
    beShown (Just x) = `(show ~(iVar (UN x)))
    beShown Nothing = `("_0") -- param is 0 use

-- TOTO, really we should be defining showPrec and not show at all
-- but let's get everything else sorted out first so we're not fighting
-- type sigs. refer to: Show (Maybe a)
-- TODO if our cons are Nil and :: should we be displaying like [a,b,c] ?
-- I think so, especially since we could write the value that way
-- TODO we should be defining showPrec for things like MyNat to be right
-- currently MS (MS (MS MZ)) = "MS MS MS MZ"
showObject : (decname : Name) -> (funname : Name) -> TypeInfo
          -> Visibility -> Elab (Decl, Decl)
showObject decname showfun tyinfo vis = do
  (qname,_) <- lookupName `{{Show}}
  [NS _ (DN _ showcon)] <- getCons qname
    | _ => fail "showObject: error during Show constructor lookup"
  let conargs = pullExplicits tyinfo
      varnames = map (show . name) conargs
      varnames' = map (show . name) (filter (isType . type) conargs)
      retty = `( Show ~(appTyCon (map (show . name) conargs)  tyinfo.name))
      tysig = addShowAutoImps varnames' retty
      claim = iClaim MW vis [Hint True] (mkTy decname tysig)
       -- TODO prec ignored for the moment, we will want this
      showprecfun = `(\_,x => ~(iVar showfun) x)
      rhs = `( ~(iVar showcon) ~(iVar showfun) ~(showprecfun))
      body = iDef decname [(patClause (iVar decname) rhs)]
  pure $ (claim,body)

-- TODO determine which tyvars are actually used later. We don't need to
-- require Show for phantom parameters.
export
deriveShow : Visibility -> Name -> Elab ()
deriveShow vis sname = do

    (qname,_) <- lookupName sname -- get the qualified name of our type
    -- create human readable names for our instance components
    let decn = mapName (\d => "showImpl" ++ d) sname
        funn = mapName (\d => "showImpl" ++ d ++ "Fun") sname
    -- Build general info about the type we're deriving (e.g. Foo) that we want
    -- to keep around.
    tyinfo <- makeTypeInfo qname

    -- Our components for our showing function
    funclaim <- showClaim funn tyinfo Private -- NB private
    funclauses <- traverse (showCon funn) tyinfo.cons

    -- Our function's complete definition
    let fundecl = iDef funn (funclauses)

    -- TODO check if an instance exists already and abort if so

    -- The actual showFoo : Show Foo instance.
    (objclaim,objclause) <- showObject decn funn tyinfo vis
    -- Place our things into the namespace
    -- Both claims first, otherwise we won't be able to find our own Show
    declare [funclaim, objclaim]
    declare [fundecl, objclause]

-----------------------------
-- Testing
-----------------------------
--
-- %language ElabReflection -- you can remove this once %runElab is no longer used in this module
-- -- That time will be when deriveShow prunes extraneous Show constraints and the
-- -- testing types are moved to their own module
--
-- export
-- data Foo1 : Type -> Type where
--   Bor1 : Foo1 a
--
-- export
-- data Foo2 : Type -> Type where
--   Bor2 : a -> Foo2 a
--
-- data Foo4 : Type -> Type -> Type where
--   Bor4 : b -> Foo4 a b
--
-- data Foo5 : Type -> Type -> Type -> Type where
--   Bor5 : a -> b -> c -> Foo5 a b c
--
-- -- NB c is never used, so Show shouldn't be required for it
-- data Foo7 : Type -> Type -> Type -> Type where
--   Zor7 : a -> Foo7 a b c
--   Gor7 : b -> Foo7 a b c
--   Nor7A : a -> b -> Foo7 a b c
--   Nor7B : a -> b -> c -> Foo7 a b c
--   Bor7 : Foo7 a b c
--
-- -- NB a is never used, so Show shouldn't be required for it
-- data Foo7' : Type -> Type -> Type -> Type where
--   Zor7' : c -> Foo7' a b c
--   Gor7' : b -> Foo7' a b c
--   Nor7' : b -> c -> Foo7' a b c
--   Bor7' : Foo7' a b c
--
-- export
-- data MyNat : Type where
--   MZ : MyNat
--   MS : MyNat -> MyNat
-- -- we'll use our own nat for index experimentation
--
-- %runElab deriveShow Private `{{MyNat}}
--
-- data Foo6 : Type -> Type -> Type -> Nat -> Type where
--   Zor6 : a -> b -> Foo6 a b c Z
--   Gor6 : b -> Foo6 a b c (S k)
--   Nor6A : a -> b -> c -> Foo6 a b c n
--   Nor6B : a -> (0 _ : b) -> c -> Foo6 a b c n -- NB: 0 Use arg
--   Bor6 : Foo6 a b c n
--   Wah6 : a -> (n : Nat) -> Foo6 a b c n
--
-- export
-- data Foo6' : Type -> Type -> Type -> MyNat -> Type where
--   Zor6'  : a -> b -> Foo6' a b c MZ
--   Gor6'  : b -> Foo6' a b c (MS k)
--   Nor6A' : a -> b -> c -> Foo6' a b c n
--   Nor6B' : a -> (0 _ : b) -> c -> Foo6' a b c n
--   Bor6'  : Foo6' a b c n
--   Wah6'  : a -> (n : MyNat) -> Foo6' a b c n
--
-- -- reference impl
-- showFoo6 : (Show a, Show b, Show c) => Foo6 a b c n -> String
-- showFoo6 (Zor6 x y) = "Zor6" ++ " " ++ show x ++ " " ++ show y
-- showFoo6 (Gor6 x) = "Gor6" ++ " " ++ show x
-- showFoo6 (Nor6A x y z)
--   = "Nor6A" ++ " " ++ show x ++ " " ++ show y ++ " " ++ show z
-- showFoo6 (Nor6B x _ z)
--   = "Nor6B" ++ " " ++ show x ++ " " ++ "_0" ++ " " ++ show z
-- showFoo6 (Bor6) = "Bor6"
-- showFoo6 (Wah6 x i) = "Wah6" ++ " " ++ show x ++ " " ++ show i
-- -- showFoo6 {b=Int} {c=String} (Wah6 'c' (S Z))
--
-- data FooN : Nat -> Type -> Type where
--   BorZ : b -> FooN Z b
--   BorS : b -> FooN (S Z) b
--   BorN : b -> FooN n b
-- -- show (BorN 'c')
--
-- %runElab deriveShow Export  `{{Foo1}}
-- %runElab deriveShow Export  `{{Foo2}}
-- %runElab deriveShow Private `{{Foo4}}
-- %runElab deriveShow Private `{{Foo5}}
-- %runElab deriveShow Private `{{Foo6}}
-- %runElab deriveShow Export  `{{Foo6'}}
-- %runElab deriveShow Private `{{Foo7}}
-- %runElab deriveShow Private `{{Foo7'}}
-- %runElab deriveShow Private `{{FooN}}

-- There's an issue in use of `show` from the repl as it's not going to do a
-- bunch of defaulting for you.

-- Demonstrating the problem in interface type inferring:
data Bep : Nat -> Type where
  Ish : Bep n

implementation Show (Bep n) where
  show Ish = "foo"

bif : Bep n -> String
bif = show
-- This is fine in a repl:     bif Ish
-- This is not fine in a repl: show Ish

-- forfo : (Show a, Show b, Show c) => Foo6 a b c n -> String
-- forfo = show
-- This is fine in a repl:     forfo (Nor6A 'c' 'g' 'j')
-- This is not fine in a repl: show (Nor6A 'c' 'g' 'j')

-- I don't know why our type sig should help so much, we never even use the n


text:
module Error.Pretty

import Data.String
import Data.List1
import Error.Data
import Error.Format
import Error.ANSI
import Syntax.Tokens
import Loc

record ErrInfo where
  constructor MKRangedErrInfo
  lines : List String
  mainLine : String
  filename : String
  errorLineNum : (Int, Int)
  defaultRange : Range

-- Helper function

orElse : Maybe a -> a -> a
orElse maybe alternative =
  case maybe of
    Just x => x
    Nothing => alternative

-- Patterns of error messages

commonErrorMessage : ErrInfo -> Maybe Range -> String -> String
commonErrorMessage errInfo maybeRange text =
  let range = orElse maybeRange (ErrInfo.defaultRange errInfo)
      mainLine = Loc.line $ Range.start range
      errRange = (ErrInfo.errorLineNum errInfo)
      markLine = createMarkLine Fg.red (cast $ length (ErrInfo.mainLine errInfo)) range
  in
  unlines [ formatHeader text
          , fileHeader range (ErrInfo.filename errInfo)
          , unlines $
            insertInLines errRange (mainLine + 1) markLine
            (formatLines range errRange mainLine (ErrInfo.lines errInfo))
          , lineJump 1]

-- Lexer error messages

getLexerError : ErrInfo -> Range -> LexerError -> String

getLexerError err range UnterminatedString =
  commonErrorMessage err (Just range) "You forgot to terminate this string with another double quote!"

getLexerError err range UnexpectedChar =
  commonErrorMessage err (Just range) "You cannot use this character here!"

-- Reader error helpers

getBetweenTypeName : BetweenType -> String
getBetweenTypeName kind =
  case kind of
    Parenthesis    => "parenthesis"
    CurlyBrackets  => "curly bracket"
    SquareBrackets => "square bracket"

expectMessage : (List String) -> String -> String
expectMessage fst snd = concat ["Expected ", concat fst, " but instead got \"", snd, "\""]

getExpectTypeMessage : ExpectType -> Tkn -> String
getExpectTypeMessage expect actual =
  case expect of
    ExpectTkn tkn     => expectMessage ["a token like \"", show @{real} tkn, "\""] (show @{real} actual)
    ExpectKeyword str => expectMessage ["the keyword '", str, "'"] (show @{real} actual)
    ExpectId  => expectMessage ["an identifier (name for something)"] (show @{real} actual)
    ExpectStr => expectMessage ["a text (string)"] (show @{real} actual)
    ExpectInt => expectMessage ["a integer number"] (show @{real} actual)
    Unknown   => concat ["Unexpected ", (show @{real} actual)]
    TknEOF    => concat ["Unexpected \"", (show @{real} actual), "\" try to add some top level structure (link here) instead of this."]

-- Reader error messages

getReaderError : ErrInfo -> Range -> ReaderError -> String
getReaderError err range (NotClosed kind) =
  let kindName = getBetweenTypeName kind in
  commonErrorMessage err (Just range) ("You forgot to close the " ++ kindName ++ " that starts in the indicated place")

getReaderError err range (Expected expect tkn) =
  let message = getExpectTypeMessage expect tkn in
  commonErrorMessage err (Just range) message

  -- Reader error messages

getParserError : ErrInfo -> Range -> ParserError -> String
getParserError err range (InvalidTopLevel str) =
  commonErrorMessage err (Just range) ("It's the wrong structure for the " ++ str ++ " structure")

getParserError err range (InvalidIdName str) =
  commonErrorMessage err (Just range) ("The name '" ++ str ++ "' is invalid as a identifier for this structure!")

getParserError err range (InvalidPath str) =
  commonErrorMessage err (Just range) ("Expected a path but instead got '" ++ str ++ "'")

getParserError err range (ExpectedDataField) =
  commonErrorMessage err (Just range) ("Expected a field for the data structure but got something that is not it! (read the link to read more about data structures)")

getParserError err range (ExpectedLiteral) =
  commonErrorMessage err (Just range) ("Expected a literal like 1 or \"some text with commas\"")

getParserError err range (ExpectedIdButGotPath) =
  commonErrorMessage err (Just range) ("Expected a single identifier but instead got a path!")

getParserError err range (ExpectedTypeDef) =
  commonErrorMessage err (Just range) ("Expected a type definition")

getParserError err range (NeedCapitalizedName kind) =
  let structure = case kind of
                    CapitalModule => "module"
                    CapitalType => "type"
                    CapitalADTName => "data name"
                    CapitalDataConstructor => "data constructor"
  in
  commonErrorMessage err (Just range) ("Expected a capitalized name for the " ++ structure ++ " definition")

getParserError err range (NeedMinusculeName) =
  commonErrorMessage err (Just range) ("Expected a minuscule name for this structure")

getParserError err range (ArrowWithOneArg) =
  commonErrorMessage err (Just range) ("The arrow type not supports one type. \nwe cannot transform one type into nothing")

getParserError err range other =
  commonErrorMessage err (Just range) "Sorry i dont have a good parser error message for it"

-- The entry point of the error messages

getMessage : ErrInfo -> ErrorType -> String
getMessage errInfo (LexicalError range err) = getLexerError errInfo range err
getMessage errInfo (ReadingError range err) = getReaderError errInfo range err
getMessage errInfo (ParsingError range err) = getParserError errInfo range err
getMessage errInfo _ = commonErrorMessage errInfo Nothing "We dont have a good error message for it now lol sorry"

public export
Show ErrorData where
  show (MkErrorData file source error) =
    case (getRange error) of
      Just range@(MkRange (MkLoc c mainLine) _) =>
        let lined = lines source
            errRange = getErrorLineRange lined range
            line = (getIndex (cast mainLine) lined "")
            info = MKRangedErrInfo lined line file errRange range
        in
          getMessage info error
      Nothing => "Cannot process now"


text:
-- SPDX-FileCopyrightText: 2021 The toml-idr developers
--
-- SPDX-License-Identifier: CC0-1.0

module Files

import Tester

import Language.TOML

import Data.List
import System.Directory
import System.File

parse : String -> TestFunc Table
parse src = do
    Right table <- pure $ parseTOML src
        | Left err => throw (show err)
    pure table

dirEntries : (path : String) -> TestFunc (List String)
dirEntries path = do

    Right contents <- listDir path
        | Left err =>
            throw $ "\nUnable to open dir \"" ++ path ++ "\": " ++ show err

    pure $ filter (\x => not $ x `elem` [".", ".."]) contents

filesPass : Test
filesPass = test "valid files" $ do
    let basePath = "tests/pass/"
    dirs <- dirEntries basePath
    for_ dirs $ \path => do
        Right src <- readFile (basePath ++ path)
            | Left err => throw $ show err

        Right _ <- pure $ parseTOML src
            | Left err => throw $ show err

        pure ()

export
tests : List Test
tests = [
    filesPass
]

max_stars_repo_name: sepiina/toml-idr

max_issues_repo_name: sepiina/toml-idr

max_forks_repo_name: sepiina/toml-idr


text:
module ListSearch

data NatList : Type where
    Nil : NatList
    Cons : (x : Nat) -> (tail : NatList) -> NatList

data Contains : (k : Nat) -> (xs : NatList) -> Type where
    Here : Contains k (Cons k tail)
    There : (later : Contains k tail) -> Contains k (Cons x tail)

total
emptyNoContains : Not (Contains k Nil)
emptyNoContains Here impossible
emptyNoContains (There _) impossible

total
neitherHeadNorTail : (k : Nat) -> (x : Nat) -> (tail : NatList) -> Not (k = x) -> Not (Contains k tail) -> Not (Contains k (Cons x tail))
neitherHeadNorTail k x tail k_neq_x k_not_in_tail in_cons = case in_cons of
    Here => k_neq_x Refl
    (There later) => k_not_in_tail later

total
testContains : (k : Nat) -> (xs : NatList) -> Dec (Contains k xs)
testContains k [] = No emptyNoContains
testContains k (Cons x tail) = case decEq k x of
    (Yes Refl) => Yes Here
    (No contra) =>
        case testContains k tail of
            (Yes prf) => Yes (There prf)
            (No contra2) => No (neitherHeadNorTail k x tail contra contra2)

total
insert : Nat -> NatList -> NatList
insert k xs = case testContains k xs of
    (Yes prf) => xs
    (No contra) => Cons k xs

total
insertProved : (k : Nat) -> (xs : NatList) -> (xs' : NatList ** Contains k xs')
insertProved k xs = case testContains k xs of
    (Yes prf) => (xs ** prf)
    (No contra) => (Cons k xs ** Here)


text:
module QStateT

import Control.Monad.State
import LinearTypes
import Control.Linear.LIO

%default total

public export
R : Type -> Type
R = L IO {use = Linear}

--Inspired by the indexed state monad in Haskell, and for linear types
public export
data QStateT : (initialType : Type) -> (finalType : Type) -> (returnType : Type) -> Type where
  MkQST : (1 _ : (1 _ : initialType) -> R (LPair finalType returnType)) -> QStateT initialType finalType returnType

||| Unwrap and apply a QStateT monad computation.
public export
runQStateT : (1 _ : initialType) -> (1 _ : QStateT initialType finalType returnType) -> R (LPair finalType returnType)
runQStateT i (MkQST f) = f i

public export
pure : (1 _ : a) -> QStateT t t a
pure x = MkQST (\st => pure1 (st # x))

public export
(>>=) : (1 _ : QStateT i m a) -> (1 _ : ((1 _ : a) -> QStateT m o b)) -> QStateT i o b
v >>= f = MkQST $ \i => do
                         (a # m) <- runQStateT i v
                         runQStateT a (f m)

public export
modify : ((1 _ : i) -> o) -> QStateT i o ()
modify f = MkQST $ \i => pure1 (f i # ())

max_stars_repo_name: zamdzhiev/Qimaera

max_issues_repo_name: zamdzhiev/Qimaera

max_forks_repo_name: zamdzhiev/Qimaera


text:
module Prove

-- One can prove theorems with idris (of course!)

-- propositional equality is defined as below:
--
-- data (=) : a -> b -> Type where
--   Refl : x = x

twoPlusTwo : 2 + 2 = 4
twoPlusTwo = Refl

-- The bottom type (Empty type) has no constructor, we can use it to represent
-- negation of proposition.

disjoint : {n : Nat} -> (Z = S n) -> Void
disjoint p = replace {P = disjointTy} p ()
  where disjointTy : Nat -> Type
        disjointTy Z     = ()
        disjointTy (S _) = Void

-- where the library function `replace' has type of
--
--    replace : (x = y) -> P x -> P y

-- above definition is reduced as:
--
-- replace { P = disjointTy } p ()
-- replace { P = disjointTy } (Z = S n) ()
-- (f : (disjointTy Z -> disjointTy (S n))) ()
-- (f : () -> Void) ()
-- Void

-- now we try prove some simple theorems

plusReduces : {n:Nat} -> (Z + n = n)
plusReduces = Refl
-- since 0 + n is n by the definition of (+).

plusReduces' : (n:Nat) -> (n + Z = n)
plusReduces' Z = Refl
plusReduces' (S k) = cong (plusReduces' k)
-- where `cong' is a library function with type (a = b) -> (f a = f b),
-- representing equality respects function application.

-- To finish the hole we had previously for function `parity', we need to prove
-- that (S (S (j + j))) = (S j) + (S j).

parityHelper1 : (j : Nat) -> (S j + S j) = S (S (j + j))
parityHelper1 Z = Refl
parityHelper1 (S j) = rewrite  in ?b

max_stars_repo_name: shouya/thinking-dumps

max_issues_repo_name: shouya/thinking-dumps

max_forks_repo_name: shouya/thinking-dumps