text:
module Data.Logic.Propositional

%default total

-- Idris uses intuitionistic logic, so it does not validate the
-- principle of excluded middle (PEM) or similar theorems of classical
-- logic. But it does validate certain relations among these
-- propositions, and that's what's in this file.

||| The principle of excluded middle
PEM : Type -> Type
PEM p = Either p (Not p)

||| Double negation elimination
DNE : Type -> Type
DNE p = Not $ Not p -> p

||| The consensus theorem (at least, the interesting part)
Consensus : Type -> Type -> Type -> Type
Consensus p q r = (q, r) -> Either (p, q) (Not p, r)

||| Peirce's law
Peirce : Type -> Type -> Type
Peirce p q = ((p -> q) -> p) -> p

||| Not sure if this one has a name, so call it Frege's law
Frege : Type -> Type -> Type -> Type
Frege p q r = (p -> r) -> (q -> r) -> ((p -> q) -> q) -> r

||| The converse of contraposition: (p -> q) -> Not q -> Not p
Transposition : Type -> Type -> Type
Transposition p q = (Not q -> Not p) -> p -> q

||| This isn't a good name.
Switch : Type -> Type
Switch p = (Not p -> p) -> p

-- PEM and the others can't be proved outright, but it is possible to
-- prove the double negations (DN) of all of them.

||| The double negation of a proposition
DN : Type -> Type
DN p = Not $ Not p

pemDN : DN $ PEM p
pemDN f = f $ Right $ \x => f $ Left x

dneDN : DN $ DNE p
dneDN f = f $ \g => void $ g $ \x => f $ \_ => x

consensusDN : DN $ Consensus p q r
consensusDN f = f $ \(y, z) => Right (\x => f $ \(_, _) => Left (x, y), z)

peirceDN : DN $ Peirce p q
peirceDN f = f $ \g => g $ \x => void $ f $ \_ => x

fregeDN : DN $ Frege p q r
fregeDN f = f $ \g, h, i => h $ i $ \x => void $ f $ \_, _, _ => g x

transpositionDN : DN $ Transposition p q
transpositionDN f = f $ \g, x => void $ g (\y => f $ \_, _ => y) x

switchDN : DN $ Switch p
switchDN f = f $ \g => g $ \x => f $ \_ => x

-- It's easy to prove all these theorems assuming PEM.

dnePEM : PEM p -> DNE p
dnePEM (Left l) _ = l
dnePEM (Right r) f = void $ f r

consensusPEM : PEM p -> Consensus p q r
consensusPEM (Left l) (y, _) = Left (l, y)
consensusPEM (Right r) (_, z) = Right (r, z)

peircePEM : PEM p -> Peirce p q
peircePEM (Left l) _ = l
peircePEM (Right r) f = f $ \x => void $ r x

fregePEM : PEM p -> Frege p q r
fregePEM (Left l) f _ _ = f l
fregePEM (Right r) _ g h = g $ h $ \x => void $ r x

transpositionPEM : PEM p -> Transposition q p
transpositionPEM (Left l) _ _ = l
transpositionPEM (Right r) f x = void $ f r x

switchPEM : PEM p -> Switch p
switchPEM (Left l) _ = l
switchPEM (Right r) f = f r

-- It's trivial to prove these theorems assuming double negation
-- elimination (DNE), since their double negations can all be proved.

||| Eliminate double negations
EDN : DN p -> DNE p -> p
EDN f g = g f

pemDNE : DNE $ PEM p -> PEM p
pemDNE = EDN pemDN

-- It's possible to prove the theorems assuming Peirce's law, but some
-- thought must be given to choosing the right instances. Peirce's law
-- is therefore weaker than PEM on an instance-by-instance basis, but
-- all the instances together are equivalent.

pemPeirce : Peirce (PEM p) Void -> PEM p
pemPeirce f = f $ \g => Right $ \x => g $ Left x

dnePeirce : Peirce p Void -> DNE p
dnePeirce f g = f $ \h => void $ g h

consensusPeirce : Peirce (Consensus p q r) Void -> Consensus p q r
consensusPeirce f (y, z) =
  f (\g, (_, _) => Right (\x => g (\_ => Left (x, y)), z)) (y, z)

fregePeirce : Peirce (Frege p q r) Void -> Frege p q r
fregePeirce f g h i =
  f (\j, _, _, _ => h $ i $ \x => void $ j $ \_, _, _ => g x) g h i

transpositionPeirce : Peirce (Transposition p q) Void -> Transposition p q
transpositionPeirce f g x =
  f (\h, _, _ => void $ g (\y => h $ \_, _ => y) x) (\j, _ => g j x) x

-- There are a variety of single axioms sufficient for deriving all of
-- classical logic. The earliest of these is known as Nicod's axiom,
-- but it is written using only nand operators and doesn't lend itself
-- to Idris's type system. Meredith's axiom, on the other hand, is
-- written using implication and negation.

||| Meredith's axiom, sufficient for deriving all of classical logic
Meredith : (p, q, r, s, t : Type) -> Type
Meredith p q r s t =
  ((((p -> q) -> Not r -> Not s) -> r) -> t) -> (t -> p) -> s -> p

-- The Meredith axiom implies all of classical logic, and so in
-- particular it implies PEM, and therefore cannot be proved in
-- intuitionistic logic. As usual, however, its double negation can be
-- proved.

meredithDN : DN $ Meredith p q r s t
meredithDN f =
  f $ \g, h, x =>
    h $ g $ \i =>
      void $ i
        (\y => void $ f $ \_, _, _ => y)
        (\z => f $ \_, _, _ => h $ g $ \_ => z)
        x

-- Meredith can be proved assuming PEM, since the type system itself
-- takes care of the rest.

meredithPEM : PEM p -> Meredith p q r s t
meredithPEM (Left l) _ _ _ = l
meredithPEM (Right r) f g x =
  g $ f $ \h =>
    void $ h
      (\y => void $ r y)
      (\z => r $ g $ f (\_ => z))
      x


text:
data Foo : Type where [noHints]
  A : Foo
  B : Foo

findA : {auto foo : Foo} -> String
findA {foo = A} = "Found an A"
findA {foo = _} = "Failed to find an A"

Baz : String -> Type
Baz s = s = "Found an A"

baz : (s : String ** Baz s)
baz = let %hint arg : Foo
          arg = A
      in (findA ** Refl)

interface Gnu where
  constructor MkGnu
  hasFoo : Foo

findB : Gnu => String
findB = case hasFoo of
  B => "Found a B"
  _ => "Failed to find a B"

Bar : String -> Type
Bar s = s = "Found a B"

bar : (s : String ** Bar s)
bar = let %hint arg : Gnu
          arg = MkGnu B
      in (findB ** Refl)

interface Gnat a where
  constructor MkGnat
  makeFoo : a -> Foo

record More where
  constructor MkMore
  0 Ty : Type

%unbound_implicits off
bug : forall a . a -> (s : String ** Bar s)
bug {a} x = let M : More
                M = MkMore a
                %hint arg : Gnat (Ty M)
                arg = MkGnat (const B)
            in (findB ** Refl)

ext: idr


text:
import Data.Vect

inputs : Vect 4 Double
inputs = [1.0, 2.0, 3.0, 2.5]

weights : Vect 3 (Vect 4 Double)
weights = [[0.2, 0.8, -0.5, 1.0], [0.5, -0.91, 0.26, -0.5], [-0.26, -0.27, 0.17, 0.87]]

biases : Vect 3 Double
biases = [2.0, 3.0, 0.5]

-- NOTE: match numpy interface in the spirit of the Python lesson
dotProduct : Vect n (Vect m Double) ->
             Vect m Double ->
             Vect n Double
dotProduct xss ys = map (\xs => sum $ zipWith (*) xs ys) xss

-- add the biases to the results of the dot product
output : Vect 3 Double
output = zipWith (+) (dotProduct weights inputs) biases

main : IO ()
main = printLn output


text:
module Screen

import Data.Bits
import Data.Vect
import Effects
import Effect.SDL

import Constants
import Utilities

%default total

-- a bit represents a monochrome pixel
data Pixel = On | Off

Show Pixel where
  show On = "▓"
  show Off = "░"

xorOnePixel : (p1 : Pixel) -> (p2 : Pixel) -> Pixel
xorOnePixel On Off = On
xorOnePixel Off On = On
xorOnePixel _ _ = Off

-- track if any pixel was erased (so we can set VF in the CPU)
pixelWasErased : (p1 : Pixel) -> (p2 : Pixel) -> Bool
pixelWasErased On Off = True
pixelWasErased _ _ = False

-- for convenience
ScreenWidth : Nat
ScreenWidth = 64

ScreenHeight : Nat
ScreenHeight = 32

-- 64x32 monochrome pixel display
export
record Screen where
  constructor MkScreen
  Picture : Vect ScreenHeight (Vect ScreenWidth Pixel)
  WasErased : Bool -- track for VF

data Coord = MkCoord Int Int Pixel

export
wasErased : (screen : Screen) -> Bool
wasErased = WasErased

export
renderScreen : (screen : Screen) -> { [SDL_ON] } Eff ()
renderScreen screen =
  let (coords, _) = foldl pixelCoordsForRow ([], 0) (Picture screen) in
  do
    mapE renderPixel coords
    pure ()
  where
    pixelCoords : (accum : (List Coord, (Int, Int))) -> (pixel : Pixel) -> (List Coord, (Int, Int))
    pixelCoords (rects, (x, y)) pixel =
      MkPair (MkCoord x y pixel :: rects) (x + 1, y)
    pixelCoordsForRow : (accum : (List Coord, Int)) -> Vect ScreenWidth Pixel -> (List Coord, Int)
    pixelCoordsForRow (coords, y) row =
      let (newCoords, _) = foldl pixelCoords ([], (MkPair 0 y)) row in
      MkPair (coords ++ newCoords) (y + 1)
    renderPixel : Coord -> EffM m () [SDL_ON] (\_ => [SDL_ON])
    renderPixel (MkCoord x y pixel) =
      let color = case pixel of On => white; Off => black in
      rectangle color (x * Scale) (y * Scale) Scale Scale

export
Show Screen where
  show s = foldl drawRow "" (Picture s)
  where
    concatenate : (accum : String) -> (p : Pixel) -> String
    concatenate accum val = accum ++ show val
    drawRow : (accum : String) -> (row : Vect ScreenWidth Pixel) -> String
    drawRow accum row = accum ++ (foldl concatenate "" row) ++ "\n"

export
newScreen : Screen
newScreen =
  let picture = Vect.replicate ScreenHeight $ Vect.replicate ScreenWidth Off in
  MkScreen picture False

readPixelFromPicture : (s : Screen) -> (x : Fin ScreenWidth) -> (y : Fin ScreenHeight) -> Pixel
readPixelFromPicture s x y =
  let picture = Picture s in
  let row = Vect.index y picture in
  Vect.index x row

writePixelToPicture : (s : Screen) -> (p : Pixel) -> (x : Fin ScreenWidth) -> (y : Fin ScreenHeight) -> Screen
writePixelToPicture s p x y =
  let picture = Picture s in
  let row = Vect.index y picture in
  let newRow = replaceAt x p row in
  let newPicture = replaceAt y newRow picture in
  record { Picture = newPicture } s

writePixelToScreen : (s : Screen) -> (p : Pixel) -> (x : Int) -> (y : Int) -> Screen
writePixelToScreen s p x y =
  let realX = restrict (pred ScreenWidth) $ cast x in
  let realY = restrict (pred ScreenHeight) $ cast y in
  let pixel = readPixelFromPicture s realX realY in
  let newPixel = xorOnePixel pixel p in
  let newScreen = writePixelToPicture s newPixel realX realY in
  let wasErased = pixelWasErased pixel p || WasErased s in
  record { WasErased = wasErased } newScreen

explodeByte : (val : Bits8) -> Vect 8 Pixel
explodeByte val =
  let bits : Bits 8 = cast val in
  let booleans = map (flip getBit bits) [7, 6, 5, 4, 3, 2, 1, 0] in
  map convertPixel booleans
  where
    convertPixel : Bool -> Pixel
    convertPixel True = On
    convertPixel False = Off

writeSpriteLineToScreen : (screen : Screen) -> (val : Bits8) -> (x : Int) -> (y : Int) -> Screen
writeSpriteLineToScreen screen val x y =
  let pixels = explodeByte val in
  fst $ foldl (drawPixel y) (MkPair screen x) pixels
  where
    drawPixel : (y : Int) -> (accum : (Screen, Int)) -> (pixel : Pixel) -> (Screen, Int)
    drawPixel y (screen, x) p =
      let drawnScreen = writePixelToScreen screen p x y in
      let wasErased = wasErased screen || wasErased drawnScreen in
      let newScreen = record { WasErased = wasErased } drawnScreen in
      MkPair newScreen (x + 1)

export
writeSpriteToScreen : (screen : Screen) -> (sprite : Vect len Bits8) -> (x : Int) -> (y : Int) -> Screen
writeSpriteToScreen screen sprite x y =
  let resetScreen = record { WasErased = False } screen in
    fst $ foldl (drawLine x) (MkPair resetScreen y) sprite
  where
    drawLine : (x : Int) -> (accum : (Screen, Int)) -> (val : Bits8) -> (Screen, Int)
    drawLine x (screen, y) val =
      let drawnScreen = writeSpriteLineToScreen screen val x y in
      let wasErased = wasErased screen || wasErased drawnScreen in
      let newScreen = record { WasErased = wasErased } drawnScreen in
      MkPair newScreen (y + 1)

export
defaultSpriteStartingAddress : Fin 16 -> Bits16
defaultSpriteStartingAddress x =
  let spriteOffset = cast $ finToNat x in
  let offsetAddress = DefaultSpriteDataLength * spriteOffset in
  cast $ DefaultSpriteDataAddress + offsetAddress

-- 16 8x5 sprites for hexadecimal values
export
defaultSpriteData : List Bits8
defaultSpriteData = [
    0xf0, 0x90, 0x90, 0x90, 0xf0,
    0x20, 0x60, 0x20, 0x20, 0x70,
    0xf0, 0x10, 0xf0, 0x80, 0xf0,
    0xf0, 0x10, 0xf0, 0x10, 0xf0,
    0x90, 0x90, 0xf0, 0x10, 0x10,
    0xf0, 0x80, 0xf0, 0x10, 0xf0,
    0xf0, 0x80, 0xf0, 0x90, 0xf0,
    0xf0, 0x10, 0x20, 0x40, 0x40,
    0xf0, 0x90, 0xf0, 0x90, 0xf0,
    0xf0, 0x90, 0xf0, 0x10, 0xf0,
    0xf0, 0x90, 0xf0, 0x90, 0x90,
    0xe0, 0x90, 0xe0, 0x90, 0xe0,
    0xf0, 0x80, 0x80, 0x80, 0xf0,
    0xe0, 0x90, 0x90, 0x90, 0xe0,
    0xf0, 0x80, 0xf0, 0x80, 0xf0,
    0xf0, 0x80, 0xf0, 0x80, 0x80
  ]


text:
||| Adding colours to the adventure game
||| Ported from https://www.linuxjournal.com/content/programming-color-ncurses

module AdventureInColor

import Data.Nat
import NCurses

%default covering

-- Define symbols for the map
grass    = ' '
empty    = '.'
water    = '~'
mountain = '^'
player   = '*'

isMoveOkay : Position -> NCurses i i Bool
isMoveOkay pos = do c <- mvInCh pos
                    pure (c == grass || c == empty)

CFG = MkConfig
  { noDelayEnabled = False
  , keypadEnabled  = True
  , colorEnabled   = True
  }

main : IO ()
main = runNCurses $ NCurses.do
  -- Initialise curses
  cBreak
  noEcho
  clear
  keypad True
  startColor

  -- Grab size
  size <- getSize

  -- Initialise the colors
  grassC    <- initColorPair 1 Yellow Green
  waterC    <- initColorPair 2 Cyan   Blue
  mountainC <- initColorPair 3 Black  White
  playerC   <- initColorPair 4 Red    Magenta

  -- Draw map
  -- background
  nSetAttr (CP grassC)
  for_ @{NCURSES} [0..size.height] $ \ row =>
    mvHLine (MkRow row) grass size.width

  -- mountain
  nSetAttr (CP mountainC)
  for_ @{NCURSES} [half size.width .. threequarter size.width] $ \ col =>
    mvVLine (MkPosition { row = 0, col }) mountain size.height

  -- mountain path
  nSetAttr (CP grassC)
  mvHLine (MkRow $ quarter size.height) grass size.width

  -- lake
  nSetAttr (CP waterC)
  for_ @{NCURSES} [1..half size.height] $ \ row =>
    mvHLine (MkPosition { row, col = 1 }) water (third size.width)

  -- wait for the user quitting
  exploring playerC grassC size (MkRow $ pred size.height)

  where

    quarter : Nat -> Nat
    quarter n = (n `divNatNZ` 4) %search

    third : Nat -> Nat
    third n = (n `divNatNZ` 3) %search

    half : Nat -> Nat
    half n = (n `divNatNZ` 2) %search

    threequarter : Nat -> Nat
    threequarter n = (3 * n `divNatNZ` 4) %search

    step : ColorPair -> (pos, pos' : Position) -> NCurses CFG CFG Position
    step emptyC pos pos'
      = do ok <- isMoveOkay pos'
           ifThenElse (not ok) (pure pos) $ do
             nSetAttr (CP emptyC)
             mvAddCh pos empty
             pure pos'

    exploring : (playerC, emptyC : ColorPair) ->
                Size -> Position -> NCurses CFG CFG ()
    exploring playerC emptyC sz pos@(MkPosition { row, col }) = NCurses.do
      -- display player at position
        nSetAttr (CP playerC)
        mvAddCh pos player
        move pos
        refresh
        -- wait for an input to move
        Left c <- getCh
          | Right 'q' => pure () -- quitting
          | Right _ => exploring playerC emptyC sz pos -- invalid input
        case c of
          Up    => do pos <- step emptyC pos (up pos)
                      exploring playerC emptyC sz pos
          Down  => do let pos' = down pos
                      let True = pos'.row < pred sz.height
                        | _ => exploring playerC emptyC sz pos
                      pos <- step emptyC pos pos'
                      exploring playerC emptyC sz pos
          Left  => do pos <- step emptyC pos (left pos)
                      exploring playerC emptyC sz pos
          Right => do let pos' = right pos
                      let True = pos'.col < pred sz.width
                        | _ => exploring playerC emptyC sz pos
                      pos <- step emptyC pos pos'
                      exploring playerC emptyC sz pos
          _ => exploring playerC emptyC sz pos -- invalid input

max_stars_repo_name: gallais/ncurses-idris

max_issues_repo_name: gallais/ncurses-idris

max_forks_repo_name: gallais/ncurses-idris


text:
module InfoWithImplicit

import public Language.Reflection.Pretty
import public Language.Reflection.Syntax
import public Language.Reflection.Types
import Data.Vect

import Mb

%language ElabReflection

data X : Vect n a -> Type where
  XX : X []

export
inf : TypeInfo
inf = getInfo "X"

export
mbInf : TypeInfo
mbInf = getInfo "T"
-- `T` and its constructors are visible even when they are not exported

max_stars_repo_name: buzden/idris-playground

max_issues_repo_name: buzden/idris-playground

max_forks_repo_name: buzden/idris-playground


text:
module Data.Prim.Char

import public Control.WellFounded
import public Data.DPair
import public Data.Prim.Ord

%default total

unsafeRefl : a === b
unsafeRefl = believe_me (Refl {x = a})

--------------------------------------------------------------------------------
--          (<)
--------------------------------------------------------------------------------

||| Witness that `m < n === True`.
export
data (<) : (m,n : Char) -> Type where
  LT : {0 m,n : Char} -> (0 prf : (m < n) === True) -> m < n

||| Contructor for `(<)`.
|||
||| This can only be used in an erased context.
export %hint
0 mkLT : (0 prf : (m < n) === True) -> m < n
mkLT = LT

||| Extractor for `(<)`.
|||
||| This can only be used in an erased context.
export
0 runLT : m < n -> (m < n) === True
runLT (LT prf) = prf

||| We don't trust values of type `(<)` too much,
||| so we use this when creating magical results.
export
strictLT : (0 p : m < n) -> Lazy c -> c
strictLT (LT prf) x = x

--------------------------------------------------------------------------------
--          Aliases
--------------------------------------------------------------------------------

||| Flipped version of `(<)`.
public export
0 (>) : (m,n : Char) -> Type
m > n = n < m

||| `m <= n` mean that either `m < n` or `m === n` holds.
public export
0 (<=) : (m,n : Char) -> Type
m <= n = Either (m < n) (m === n)

||| Flipped version of `(<=)`.
public export
0 (>=) : (m,n : Char) -> Type
m >= n = n <= m

||| `m /= n` mean that either `m < n` or `m > n` holds.
public export
0 (/=) : (m,n : Char) -> Type
m /= n = Either (m < n) (m > n)

--------------------------------------------------------------------------------
--          Order
--------------------------------------------------------------------------------

0 ltNotEQ : m < n -> Not (m === n)
ltNotEQ x = strictLT x $ assert_total (idris_crash "IMPOSSIBLE: LT and EQ")

0 ltNotGT : m < n -> Not (n < m)
ltNotGT x = strictLT x $ assert_total (idris_crash "IMPOSSIBLE: LT and GT")

0 eqNotLT : m === n -> Not (m < n)
eqNotLT = flip ltNotEQ

export
comp : (m,n : Char) -> Trichotomy (<) m n
comp m n = case prim__lt_Char m n of
  0 => case prim__eq_Char m n of
    0 => GT (ltNotGT $ LT unsafeRefl) (ltNotEQ $ LT unsafeRefl) (LT unsafeRefl)
    x => EQ (eqNotLT unsafeRefl) (unsafeRefl) (eqNotLT unsafeRefl)
  x => LT (LT unsafeRefl) (ltNotEQ $ LT unsafeRefl) (ltNotGT $ LT unsafeRefl)

export
Total Char (<) where
  trichotomy   = comp
  transLT p q  = strictLT p $ strictLT q $ LT unsafeRefl

--------------------------------------------------------------------------------
--          Bounds and Well-Foundedness
--------------------------------------------------------------------------------

||| Lower bound of `Char`
public export
MinChar : Char
MinChar = '\x0000'

||| `m >= MinChar` for all `m` of type `Char`.
export
0 GTE_MinChar : (m : Char) -> m >= MinChar
GTE_MinChar m = case comp MinChar m of
  LT x f g => %search
  EQ f x g => %search
  GT f g x => assert_total $ idris_crash "IMPOSSIBLE: Char smaller than 0"

||| Not value of type `Char` is less than `MinChar`.
export
0 Not_LT_MinChar : m < MinChar -> Void
Not_LT_MinChar = GTE_not_LT (GTE_MinChar m)

||| Every value of type `Char` is accessible with relation
||| to `(<)`.
export
accessLT : (m : Char) -> Accessible (<) m
accessLT m = Access $ \n,lt => accessLT (assert_smaller m n)

||| `(<)` is well founded.
export %inline
WellFounded Char (<) where
  wellFounded = accessLT


text:
-- SPDX-FileCopyrightText: 2021 The toml-idr developers
--
-- SPDX-License-Identifier: MPL-2.0

module Language.TOML.ConcreteSyntax

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

public export
data CKeyAtom = CKBare String
              | CKQuoted String

public export
data CKey = CKAtom CKeyAtom
          | CKDotted (List1 CKeyAtom)

public export
data CValue
    = CVString String
    | CVInteger Integer
    | CVFloat Double
    | CVBoolean Bool
    | CVArray (List CValue)
    | CVInlineTable (List (CKey, CValue))

public export
data Item : Type where
    IKeyValue : (key : CKey) -> (val : CValue) -> Item
    ITableHeader : (header : CKey) -> Item
    ITableArray : (header : CKey) -> Item

public export
Show CKeyAtom where
    show (CKBare x) = x
    show (CKQuoted x) = "\"" ++ x ++ "\""

public export
Show CKey where
    show (CKAtom x) = show x
    show (CKDotted x) = fastConcat . intersperse "." . forget $ show <$> x

public export
Show CValue where
    show (CVString x) = show x
    show (CVInteger x) = show x
    show (CVFloat x) = show x
    show (CVBoolean x) = show x
    show (CVArray xs) = "["
        ++ fastConcat (intersperse ", " $ map (assert_total show) xs)
        ++ "]"
    show (CVInlineTable xs) = "{"
        ++ fastConcat (intersperse ", " $ map (\(k, v) => show k ++ " = " ++ assert_total show v) xs)
        ++ "}"

public export
Show Item where
    show (IKeyValue key val) = "keyval: " ++ show key ++ " = " ++ show val
    show (ITableHeader header) = "table: " ++ show header
    show (ITableArray header) = "tablearr: " ++ show header

max_stars_repo_name: sepiina/toml-idr

max_issues_repo_name: sepiina/toml-idr

max_forks_repo_name: sepiina/toml-idr


text:
||| ASTs representing imperative ES (= ECMAScript)
||| expressions and statements.
||| These are converted to ES code in module `Compiler.ES.ES`.
||| They are generated from `Term []`s in
||| module `Compiler.ES.Imperative`.
module Compiler.ES.ImperativeAst

import Compiler.CompileExpr
import public Core.TT
import public Data.Vect
import public Data.List

%default covering

mutual
  ||| A tree representing an ES expression.
  |||
  ||| This is converted to ES code in function
  ||| `Compiler.ES.ES.impExp2es`.
  public export
  data ImperativeExp : Type where
    ||| A variable of the given name
    IEVar : (name : Name) -> ImperativeExp

    ||| A lambda expression : `(args) => { body }`
    IELambda :  (args : List Name)
             -> (body : ImperativeStatement)
             -> ImperativeExp

    ||| Function application : `lhs(args)`
    IEApp :  (lhs  : ImperativeExp)
          -> (args : List ImperativeExp)
          -> ImperativeExp

    ||| A (primitive) constant
    IEConstant : (value : Constant) -> ImperativeExp

    ||| A primitive function. This will be converted to
    ||| ES code in `Compiler.ES.ES.jsOp`.
    IEPrimFn :  (function : PrimFn arity)
             -> (args : Vect arity ImperativeExp)
             -> ImperativeExp

    ||| A primitive external function. Example `prim__newIORef`
    IEPrimFnExt :  (function : Name)
                -> (args : List ImperativeExp)
                -> ImperativeExp

    ||| Calls `object.h` on the JS object built by `object`
    ||| This is used to extract the constructor, which
    ||| this specific object represents.
    IEConstructorHead : (object : ImperativeExp) -> ImperativeExp

    ||| Tag representing either a data constructor (in that case
    ||| an integer is used as its index) or a type constructor
    ||| (these come up when pattern matching on types).
    IEConstructorTag : (tag : Either Int String) -> ImperativeExp

    ||| Argument of a data constructor applied to the given JS object.
    ||| The arg index starts at 1.
    |||
    ||| Example: `object.a3`
    IEConstructorArg :  (index : Int)
                     -> (object : ImperativeExp)
                     -> ImperativeExp

    ||| Creates a JS object using the given constructor
    ||| tag and arguments. The corresponding values are
    ||| extracted using `IEConstructorTag` and `IEConstructorArg`.
    IEConstructor :  (tag  : Either Int String)
                  -> (args : List ImperativeExp)
                  -> ImperativeExp

    ||| A delayed calculation coming either from a `Lazy`
    ||| or infinite (`Inf`) value.
    |||
    ||| In the JS backends, these are wrapped zero-argument lambdas:
    ||| `(() => expr)`.
    IEDelay : (expr : ImperativeExp) -> ImperativeExp

    ||| Forces the evaluation of a delayed (`Lazy` or `Inf`)
    ||| value.
    |||
    ||| In the JS backends, these just invoke the corresponding
    ||| zero-argument lambdas:
    ||| `expr()`.
    IEForce : (expr : ImperativeExp) -> ImperativeExp

    ||| This is converted to `undefined`.
    |||
    ||| TODO: This should be renamed to `IEUndefined` in
    |||       order not to be confused with the JS constant
    |||       `null`.
    IENull : ImperativeExp

  ||| A tree of ES statements.
  |||
  ||| This is converted to ES code in `Compiler.ES.imperative2es`.
  public export
  data ImperativeStatement : Type where
    ||| This is converted to the empty string.
    DoNothing : ImperativeStatement

    ||| A sequence of statements. These will be processed
    ||| individually and separated by a line break.
    SeqStatement :  (fstStmt : ImperativeStatement)
                 -> (sndStmt : ImperativeStatement)
                 -> ImperativeStatement

    ||| A function declaration. This will be converted
    ||| to a declaration of the following form:
    |||
    ||| ```
    ||| function funName(args){ -- fc
    |||   body
    ||| }
    ||| ```
    FunDecl :  (fc : FC)
            -> (funName : Name)
            -> (args : List Name)
            -> (body : ImperativeStatement)
            -> ImperativeStatement

    ||| An FFI declaration
    |||
    ||| @ ffiImpls : List of implementation strings.
    |||              `Compiler.ES.ES.foreignDecl`
    |||              will try to lookup a valid codegen prefix like "node"
    |||              or "javascript" in each of these and return the
    |||              remainder as the actual ES code in case of a success.
    |||
    ||| The argtypes and returnType will be ignored when generating
    ||| ES code.
    ForeignDecl :  (fc : FC)
                -> (funName : Name)
                -> (ffiImpls : List String)
                -> (argTypes : List CFType)
                -> (returnType : CFType)
                -> ImperativeStatement

    ||| A `return` statement. Example: `return body;`
    ReturnStatement : (body : ImperativeExp) -> ImperativeStatement

    ||| A `switch` statement of the form
    |||
    ||| ```
    ||| switch(expr) {
    |||  case altExp1 : {
    |||    altImpl1
    |||    break;
    |||  }
    |||  case altExp2 : {
    |||    altImpl2
    |||    break;
    |||  }
    |||  default:
    |||    deflt
    ||| }
    ||| ```
    SwitchStatement :  (expr  : ImperativeExp)
                    -> (alts  : List (ImperativeExp, ImperativeStatement))
                    -> (deflt : Maybe ImperativeStatement)
                    -> ImperativeStatement

    ||| A `let` statement with an optional value
    ||| This is converted to `let name;` if `value`
    ||| is `Nothing` and to `let name = expr;` if
    ||| `value` is `Just expr`.
    LetDecl :  (name  : Name)
            -> (value : Maybe ImperativeExp)
            -> ImperativeStatement

    ||| A `const` declaration.
    ||| This is converted to `const name = expr;`.
    ConstDecl :  (name : Name)
              -> (expr :  ImperativeExp)
              -> ImperativeStatement

    ||| Assigns the given expression to the variable
    ||| of the given name: `name = expr;`.
    MutateStatement :  (name : Name)
                    -> (expr : ImperativeExp)
                    -> ImperativeStatement

    ||| Throws an error with the given message:
    ||| `throw new Error(msg);`.
    ErrorStatement : (msg : String) -> ImperativeStatement

    ||| Evaluates the given expression (by ending the corresponding
    ||| ES code with a semicolon):
    ||| `expr;`.
    EvalExpStatement : (expr : ImperativeExp) -> ImperativeStatement

    ||| Adds the given String as a comment
    ||| `/*comment*/`.
    CommentStatement : (comment : String) -> ImperativeStatement

    ||| Runs the given statement 'forever':
    |||
    ||| ```
    ||| while(true){
    |||  body
    ||| }
    ||| ```
    ForEverLoop : (body : ImperativeStatement) -> ImperativeStatement

public export
Semigroup ImperativeStatement where
  DoNothing <+> y = y
  x <+> DoNothing = x
  x <+> y = SeqStatement x y

public export
Monoid ImperativeStatement where
  neutral = DoNothing

mutual
  export
  Show ImperativeExp where
    show (IEVar n) =  "(IEVar " ++ show n ++ ")"
    show (IELambda args b) = "(IELambda " ++ show args ++ " " ++ show b ++ ")"
    show (IEApp f args) = "(IEApp " ++ show f ++ " " ++ show args ++ ")"
    show (IEConstant c) =  "(IEConstant " ++ show c ++ ")"
    show (IEPrimFn f args) = "(IEPrimFn " ++ show f ++ " " ++ show args ++ ")"
    show (IEPrimFnExt f args) = "(IEPrimFnExt " ++ show f ++ " " ++ show args ++ ")"
    show (IEConstructorHead c) =  "(IEConstructorHead " ++ show c ++ ")"
    show (IEConstructorTag t) =  "(IEConstructorTag " ++ show t ++ ")"
    show (IEConstructorArg i c) = "(IEConstructorArg " ++ show i ++ " " ++ show c ++ ")"
    show (IEConstructor i args) = "(IEConstructor " ++ show i ++ " " ++ show args ++ ")"
    show (IEDelay x) =  "(IEDelay " ++ show x ++ ")"
    show (IEForce x) =  "(IEForce " ++ show x ++ ")"
    show IENull = "IENull"

  export
  Show ImperativeStatement where
    show DoNothing = "DoNothing"
    show (SeqStatement x y) = show x ++ ";" ++ show y
    show (FunDecl fc n args b) = "\n\n" ++ "(FunDecl (" ++ show fc ++ ") " ++ show n ++ " " ++ show args ++ " " ++ show b ++ ")"
    show (ForeignDecl fc n path args ret) = "(ForeignDecl " ++ show n ++ " " ++ show path ++")"
    show (ReturnStatement x) = "(ReturnStatement " ++ show x ++ ")"
    show (SwitchStatement e alts d) = "(SwitchStatement " ++ show e ++ " " ++ show alts ++ " " ++ show d ++ ")"
    show (LetDecl n v) = "(LetDecl " ++ show n ++ " " ++ show v ++ ")"
    show (ConstDecl n v) = "(ConstDecl " ++ show n ++ " " ++ show v ++ ")"
    show (MutateStatement n v) = "(MutateStatement " ++ show n ++ " " ++ show v ++ ")"
    show (ErrorStatement s) = "(ErrorStatement " ++ s ++ ")"
    show (EvalExpStatement x) =  "(EvalExpStatement " ++ show x ++ ")"
    show (CommentStatement x) = "(CommentStatement " ++ show x ++ ")"
    show (ForEverLoop x) = "(ForEverLoop " ++ show x ++ ")"

mutual
  ||| Iteratively replaces expressions using
  ||| the given function. This is mainly used for
  ||| replacing variables according to their name as
  ||| in `replaceNamesExp`.
  public export
  replaceExp :  (ImperativeExp -> Maybe ImperativeExp)
             -> ImperativeExp
             -> ImperativeExp
  replaceExp rep x =
    case rep x of
      Just z  => z
      Nothing =>
        case x of
          IEVar _              => x
          IELambda args body   => IELambda args $ replaceExpS rep body
          IEApp f args         => IEApp (replaceExp rep f)
                                        (replaceExp rep <$> args)
          IEConstant _         => x
          IEPrimFn f args      => IEPrimFn f (replaceExp rep <$> args)
          IEPrimFnExt f args   => IEPrimFnExt f (replaceExp rep <$> args)
          IEConstructorHead e  => IEConstructorHead $ replaceExp rep e
          IEConstructorTag _   => x
          IEConstructorArg i e => IEConstructorArg i (replaceExp rep e)
          IEConstructor t args => IEConstructor t (replaceExp rep <$> args)
          IEDelay e            => IEDelay $ replaceExp rep e
          IEForce e            => IEForce $ replaceExp rep e
          IENull               => x

  ||| Iteratively replaces expressions using
  ||| the given function. This is mainly used for
  ||| replacing variables according to their name as
  ||| in `replaceNamesExpS`.
  public export
  replaceExpS :  (ImperativeExp -> Maybe ImperativeExp)
              -> ImperativeStatement
              -> ImperativeStatement
  replaceExpS rep DoNothing =
    DoNothing
  replaceExpS rep (SeqStatement x y) =
    SeqStatement (replaceExpS rep x) (replaceExpS rep y)
  replaceExpS rep (FunDecl fc n args body) =
    FunDecl fc n args $ replaceExpS rep body
  replaceExpS reps decl@(ForeignDecl fc n path args ret) =
    decl
  replaceExpS rep (ReturnStatement e) =
    ReturnStatement $ replaceExp rep e
  replaceExpS rep (SwitchStatement s alts def) =
    let s_    = replaceExp rep s
        alts_ = (\(e,b) => (replaceExp rep e, replaceExpS rep b)) <$> alts
        def_  = replaceExpS rep <$> def
    in SwitchStatement s_ alts_ def_
  replaceExpS rep (LetDecl n v) =
    LetDecl n $ replaceExp rep <$> v
  replaceExpS rep (ConstDecl n v) =
    ConstDecl n $ replaceExp rep v
  replaceExpS rep (MutateStatement n v) =
    MutateStatement n $ replaceExp rep v
  replaceExpS rep (ErrorStatement s) =
    ErrorStatement s
  replaceExpS rep (EvalExpStatement x) =
    EvalExpStatement $ replaceExp rep x
  replaceExpS rep (CommentStatement x) =
    CommentStatement x
  replaceExpS rep (ForEverLoop x) =
    ForEverLoop $ replaceExpS rep x

rep :  List (Name, ImperativeExp)
    -> ImperativeExp
    -> Maybe ImperativeExp
rep reps (IEVar n) = lookup n reps
rep _    _         = Nothing

||| Replaces all occurences of the names in the
||| assoc list with the corresponding expression.
public export
replaceNamesExpS :  List (Name, ImperativeExp)
                 -> ImperativeStatement
                 -> ImperativeStatement
replaceNamesExpS reps x =
  replaceExpS (rep reps) x

||| Replaces all occurences of the names in the
||| assoc list with the corresponding expression.
public export
replaceNamesExp :  List (Name, ImperativeExp)
                -> ImperativeExp
                -> ImperativeExp
replaceNamesExp reps x =
  replaceExp (rep reps) x

max_stars_repo_name: mmhelloworld/idris-jvm

max_issues_repo_name: mmhelloworld/idris-jvm

max_forks_repo_name: mmhelloworld/idris-jvm


text:
module Test.Markdown.Format.HtmlTest

import IdrTest.Test
import IdrTest.Expectation

import Markdown
import Markdown.Data
import Markdown.Format.Html

toHtmlSpecs : List (String, Markdown, String)
toHtmlSpecs =
  [ ( "Render Header", Doc [Header 1 [Text " test"]], "
 test
" )
  , ( "Render Short Paragraph", Doc [Paragraph [Text "test"]], "
test
"  )
  , ( "Render Paragraph", Doc [Paragraph [Text "test"]], "
test
" )
  , ( "Render Two Paragraphs", Doc [Paragraph [Text "test"], Paragraph [Text "test2"]], "
test
\n
test2
" )
  , ( "Render Both", Doc [Header 1 [Text " text"], Paragraph [Text "and more"]], "
 text
\n
and more
" )
  , ( "Render Bold then Italic", Doc [Header 2 [Text " Well ", Bold [Text "hello"], Text " ", Italics [Text "there"]]], "
 Well hello there
" )
  , ( "Render a Link", Doc [Paragraph [Link "here" "http://example.com"]], "
here
" )
  , ( "Render an Image", Doc [Paragraph [Image "desc" "http://example.com/img.svg"]], "

" )
  , ( "Render HTML", Doc [Paragraph [Text "This is ", Html "sup" [Text "Super"], Text "!"]], "
This is Super!
" )
  , ( "Render Preformatted Text", Doc [Paragraph [Pre "t0", CodeBlock "t1 <cool>" Nothing]], "
<tt>t0</tt>
t1 <cool>

" )
  , ( "Render a Link with Space", Doc [Paragraph [Link "here" "http://example.com", Text "."]], "
here.
" )
  ]

export
suite : Test
suite =
  let
    toHtmlTests =
      map (\(name, doc, result) =>
        test name (\_ => assertEq (toHtml doc) result)
      ) toHtmlSpecs
  in
  describe "toHTML Tests" toHtmlTests

max_stars_repo_name: Z-snails/inigo

max_issues_repo_name: Z-snails/inigo

max_forks_repo_name: Z-snails/inigo


text:
module System.File.Support

%default total

||| Shorthand for a function in the C support libary
||| (libidris2_support, idris_file.h)
|||
||| @ fn the function name to refer to in the C support library
public export
support : String -> String
support fn = "C:" ++ fn ++ ", libidris2_support, idris_file.h"

||| Wrap x in the `Right` part of an `io . Either`.
export
ok : HasIO io => (x : a) -> io (Either err a)
ok x = pure (Right x)


text:
---
pandoc-minted:
language: idris
---

= Explosives in Cyberspace

[Link](https://adventofcode.com/2016/day/9)

Wandering around a secure area, you come across a datalink port to a new part of
the network. After briefly scanning it for interesting files, you find one file
in particular that catches your attention. It's compressed with an experimental
format, but fortunately, the documentation for the format is nearby.

The format compresses a sequence of characters. Whitespace is ignored. To
indicate that some sequence should be repeated, a marker is added to the file,
like `(10x2)`. To decompress this marker, take the subsequent `10` characters
and repeat them `2` times. Then, continue reading the file *after* the repeated
data. The marker itself is not included in the decompressed output.

If parentheses or other characters appear within the data referenced by a
marker, that's okay - treat it like normal data, not a marker, and then resume
looking for markers after the decompressed section.

For example:

- `ADVENT` contains no markers and decompresses to itself with no changes,
  resulting in a decompressed length of `6`.
- `A(1x5)BC` repeats only the `B` a total of `5` times, becoming `ABBBBBC` for a
  decompressed length of `7`.
- `(3x3)XYZ1 becomes `XYZXYZXYZ` for a decompressed length of `9`.
- `A(2x2)BCD(2x2)EFG` doubles the `BC` and `EF`, becoming `ABCBCDEFEFG` for a
  decompressed length of `11`.
- `(6x1)(1x3)A` simply becomes `(1x3)A` - the `(1x3)` looks like a marker, but
  because it's within a data section of another marker, it is not treated any
  differently from the A that comes after it. It has a decompressed length of
  `6`.
- `X(8x2)(3x3)ABCY` becomes `X(3x3)ABC(3x3)ABCY` (for a decompressed length of
  `18`), because the decompressed data from the `(8x2)` marker (the `(3x3)ABC`)
  is skipped and not processed further.

== Module Declaration and Imports

> ||| Day 9: Explosives in Cyberspace
> module Data.Advent.Day09

Import the [generic `Day`
structure](https://github.com/yurrriq/advent-of-idris/blob/master/src/Data/Advent/Day.idr),
inspired by [Steve Purcell Haskell
solution](https://github.com/purcell/adventofcode2016).

> import public Data.Advent.Day

== Data Types

Ensure both the type and data constructors are
[exported](http://docs.idris-lang.org/en/latest/tutorial/modules.html#meaning-for-data-types)
for all the following data types.

> %access public export

TODO: describe this

> data Block = Seq Nat String (List Block)
>            | Str String

== Parsers

> %access private
>
> notSpace : Parser Char
> notSpace = satisfy (not . isSpace)

Ensure the type constructors of the following parsers are
[exported](http://docs.idris-lang.org/en/latest/tutorial/modules.html#meaning-for-data-types).

> %access export
>
> partial block : Parser Block
> block = go <|>| Str . pack <$> some letter <?>
>         "a repeated sequence or plain string"
>   where
>     go = do len  <- char '(' *> integer <* char 'x'
>             reps <- fromIntegerNat <$> integer <* char ')'
>             rest <- pack <$> ntimes len notSpace
>             case parse (some block <* eof) rest of
>                  Right subBlocks => pure $ Seq reps rest subBlocks
>                  Left err => fail err

== Part One

\begin{quote}
  What is the \textit{decompressed length} of the file (your puzzle input)?
  Don't count whitespace.
\end{quote}

TODO: describe this

> partOne : Block -> Nat
> partOne (Seq n str _) = n * length str
> partOne (Str str)     = length str
>
> %default partial
>
> namespace PartOne
>
>     ex : String -> Either String Nat
>     ex str = sum . map partOne <$> parse (some block <* newline) str
>
>     ex1 : Either String Nat
>     ex1 = ex "ADVENT"
>
>     ex2 : Either String Nat
>     ex2 = ex "A(1x5)BC"
>
>     ex3 : Either String Nat
>     ex3 = ex "(3x3)XYZ"
>
>     ex4 : Either String Nat
>     ex4 = ex "A(2x2)BCD(2x2)EFG"
>
>     ex5 : Either String Nat
>     ex5 = ex "(6x1)(1x3)A"
>
>     ex6 : Either String Nat
>     ex6 = ex "X(8x2)(3x3)ABCY"

== Part Two

Apparently, the file actually uses *version two* of the format.

In version two, the only difference is that markers within decompressed data
*are* decompressed. This, the documentation explains, provides much more
substantial compression capabilities, allowing many-gigabyte files to be stored
in only a few kilobytes.

For example:

- `(3x3)XYZ` still becomes `XYZXYZXYZ`, as the decompressed section contains no
  markers.
- `X(8x2)(3x3)ABCY` becomes `XABCABCABCABCABCABCY`, because the decompressed
  data from the `(8x2)` marker is then further decompressed, thus triggering the
  `(3x3)` marker twice for a total of six `ABC` sequences.
- `(27x12)(20x12)(13x14)(7x10)(1x12)A` decompresses into a string of `A`
  repeated `241920` times.
- `(25x3)(3x3)ABC(2x3)XY(5x2)PQRSTX(18x9)(3x2)TWO(5x7)SEVEN` becomes `445`
  characters long.

Unfortunately, the computer you brought probably doesn't have enough memory to
actually decompress the file; you'll have to *come up with another way* to get
its decompressed length.

\begin{quote}
  What is the \textit{decompressed length} of the file
  using this improved format?
\end{quote}

TODO: describe this

> partTwo : Block -> Nat
> partTwo (Seq n _ bs) = n * sum (partTwo <$> bs)
> partTwo (Str str)    = length str

== Main

> namespace Main
>
>     main : IO ()
>     main = runDay $ MkDay 9 (some block <* newline)
>            (pure . show . sum . map partOne)
>            (pure . show . sum . map partTwo)

ext: lidr

max_stars_repo_name: yurrriq/advent-of-code


text:
module Language.LSP.Message.Declaration

import Language.JSON
import Language.LSP.Message.Derive
import Language.LSP.Message.Location
import Language.LSP.Message.Progress
import Language.LSP.Message.TextDocument
import Language.LSP.Message.Utils
import Language.Reflection

%language ElabReflection
%default total

||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_declaration
public export
record DeclarationClientCapabilities where
  constructor MkDeclarationClientCapabilities
  dynamicRegistration : Maybe Bool
  linkSupport         : Maybe Bool
%runElab deriveJSON defaultOpts `{{DeclarationClientCapabilities}}

||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_declaration
public export
record DeclarationOptions where
  constructor MkDeclarationOptions
  workDoneProgress : Maybe Bool
%runElab deriveJSON defaultOpts `{{DeclarationOptions}}

||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_declaration
public export
record DeclarationRegistrationOptions where
  constructor MkDeclarationRegistrationOptions
  workDoneProgress : Maybe Bool
  documentSelector : OneOf [DocumentSelector, Null]
  id               : Maybe String
%runElab deriveJSON defaultOpts `{{DeclarationRegistrationOptions}}

||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_declaration
public export
record DeclarationParams where
  constructor MkDeclarationParams
  workDoneToken      : Maybe ProgressToken
  partialResultToken : Maybe ProgressToken
  textDocument       : TextDocumentIdentifier
  position           : Position
%runElab deriveJSON defaultOpts `{{DeclarationParams}}


text:
> module Nat.examples.InductiveProofs

> import Syntax.PreorderReasoning

> succPlusLeftRightEqPlusLeftSuccRight : (m : Nat) -> (n : Nat) -> S (plus m n) = plus m (S n)
> succPlusLeftRightEqPlusLeftSuccRight  Z    n = Refl
> succPlusLeftRightEqPlusLeftSuccRight (S m) n = ( S (plus (S m) n) )
>                                              ={ Refl }=
>                                                ( S (S (plus m n)) )
>                                              ={ cong (succPlusLeftRightEqPlusLeftSuccRight m n) }=
>                                                ( S (plus m (S n)) )
>                                              ={ Refl }=
>                                                ( plus (S m) (S n) )
>                                              QED

max_stars_repo_name: zenntenn/IdrisLibs

max_issues_repo_name: zenntenn/IdrisLibs

max_forks_repo_name: zenntenn/IdrisLibs


text:
module Python.Objects

import Python.Telescope

%default total
%access public export

data Field : Type where
  PAttr : (pt : Type) -> (tf : pt -> Type) -> Field
  Call : (t : Telescope a) -> Field
  NotField : Field

Attr : Type -> Field
Attr t = PAttr Unit $ const t

||| Python object signature is a list of its fields, plus mixins.
Signature : Type
Signature = String -> Field

implementation Semigroup Signature where
  (<+>) s t =
    \field => case s field of
        NotField => t field
        result   => result

implementation Monoid Signature where
  neutral = const NotField

||| Dynamically typed Python reference.
Dyn : Type
Dyn = Ptr

export
toDyn : a -> Dyn
toDyn = believe_me

||| Python object, typed by its signature.
-- TODO: make this abstract
record Obj (sig : Signature) where
  constructor MkObj
  ptr : Ptr

||| Python type of Python types.
PyType : Signature
PyType f = case f of
  "__name__" => Attr String
  _ => NotField

||| Object that all Python objects inherit from.
Object : Signature
Object f = case f of
  "__class__" => Attr $ Obj PyType
  _ => NotField

||| Python modules.
Module : Signature
Module f = case f of
  "__name__" => Attr String
  _ => Object f

max_stars_repo_name: ziman/idris-py

max_issues_repo_name: ziman/idris-py

max_forks_repo_name: ziman/idris-py


text:
module Factorial

facto : Nat -> Nat
facto Z = 1
facto n@(S k) = mult n (fact k)

tf1 : facto 3 = 6
tf1 = Refl

tf2 : facto 5 = mult 10 12
tf2 = Refl


text:
module Registry

-- Import the specifications of existing services
import Int2Str
import Str2Float
import CompoInt2Float

-- Declare the retrieve procedure of the Registry module.  It takes a
-- string representing a type signature and return a pair of strings
-- representing respectively the name of a service and the name of a
-- procedure of that service matching that type signature.  The
-- implementation is only available in Python for now.
export
retrieve : String -> (String, String)

max_stars_repo_name: nunet-io/ai-dsl

max_issues_repo_name: nunet-io/ai-dsl

max_forks_repo_name: nunet-io/ai-dsl


text:
module Typing.Infer

import public Typing.Term
import Syntax.Term as Untyped

import Control.Monad.State.State
import Control.Monad.State.Interface
import Control.Monad.Identity
import Control.Monad.Error.Either
import Control.Monad.Error.Interface
import Control.Monad.Trans

import Data.SortedMap
import Data.List

-- Some helper functions

||| It's like A / B to multiset
complement : Eq a => List a -> List a -> List a
complement = foldl (flip Data.List.delete)

mapMap : Ord k => (v -> n) -> SortedMap k v -> SortedMap k n
mapMap f sMap =
    let vals = toList sMap in
    foldr (\c => insert (Builtin.fst c) (f $ Builtin.snd c)) empty vals

||| Substitutes freeVars for concrete types

Subst : Type
Subst = SortedMap String Ty

emptySubst : Subst
emptySubst = empty

||| Type enviroment that stores all mapping from strings to schemas
data Context = MkCtx (SortedMap (List String) Schema)

remove : Context -> List String -> Context
remove (MkCtx ctx) str = MkCtx (delete str ctx)

findVar : (List String) -> Context -> Maybe Schema
findVar key (MkCtx ctx) = lookup key ctx

insert : Context -> (List String) -> Schema -> Context
insert (MkCtx ctx) key val = MkCtx (insert key val ctx)

-- Apply and freevars implementation
interface Application a where
  freeVars : a -> (List String)
  apply : Subst -> a -> a

Application Ty where
  freeVars (TyVar r n) = [n]
  freeVars (TyPoly r path ty) = freeVars ty
  freeVars (TySimple r s) = []
  freeVars (TyArrow r a b) = (freeVars a) `union` (freeVars b)

  apply subs t@(TyVar r n) =
    case lookup n subs of
      Just val => val
      Nothing  => t

  apply subs (TyArrow r arg ret) = TyArrow r (apply subs arg) (apply subs ret)
  apply subs (TyPoly r name type) = TyPoly r name (apply subs type)
  apply subs (TySimple r t) = TySimple r t

Application Schema where
  freeVars (MkSchema binded ty)   = freeVars ty `complement` binded
  apply subs (MkSchema binded ty) =
    let bindFreeSubs = foldr Data.SortedMap.delete subs binded in
    MkSchema binded (apply bindFreeSubs ty)

Application a => Application (List a) where
  apply      = map . apply
  freeVars   = foldr union [] . map freeVars

Application Context where
  freeVars (MkCtx env) = freeVars (values env)
  apply subs (MkCtx env) = MkCtx (mapMap (apply subs) env)

composeSubst : Subst -> Subst -> Subst
composeSubst s1 s2 = (mapMap (apply s1) s2) `mergeLeft` (s1)

-- Some functions of Hindley milner

TI : Type -> Type
TI = StateT Int (EitherT String Identity)

newTyVar : TI Ty
newTyVar = do
  res <- get
  put (res + 1)
  pure (TyVar emptyRange (cast $ res + 1))

generalize : Context -> Ty -> Schema
generalize ctx ty =
  let vars = freeVars ty `complement` freeVars ctx in
  MkSchema vars ty

instantiate : Schema -> TI Ty
instantiate (MkSchema vars ty) = do
  nvars <- traverse (const newTyVar) vars
  let subst = fromList $ zip vars nvars
  pure (apply subst ty)

-- Unification

isJust : Maybe a -> Bool
isJust a = case a of
  Just a => True
  _ => False

bindVar : String -> Ty -> TI Subst
bindVar name (TyVar r n) = empty
bindVar name other =
  if isJust $ find (== name) (freeVars other)
    then pure $ insert name other empty
    else pure $ insert name other empty

unify : Ty -> Ty -> TI Subst

unify (TyArrow r arg fun) (TyArrow r' arg' fun') = do
  fstSub <- unify arg arg'
  sndSub <- unify fun fun'
  pure (fstSub `composeSubst` sndSub)

unify (TyVar r u) t = bindVar u t
unify t (TyVar r u) = bindVar u t

unify (TySimple r a) (TySimple r' b) =
  if a == b
    then pure empty
    else lift $ throwE ("Cannot unify '" ++ a ++ "' and '" ++ b ++ "'")

unify a b = lift $ throwE ("Cannot unify '" ++ (show a) ++ "' and '" ++ (show b) ++ "'")

-- Inference

pathToList : Path -> List String
pathToList path =
  case path of
    (PDot r (MkName _ str) path) => (pathToList path)
    (PName r str)                => [str]

getVar : Context -> Path -> TI Ty
getVar ctx path =
  let listPath = pathToList path in
  case findVar listPath ctx of
    Just schema => do
      res <- instantiate schema
      pure res
    Nothing     => lift $ throwE ("Cannot find variable: '" ++ (show path) ++ "'")

getTy : Types -> Ty
getTy (TSimple r s)    = TySimple r s
getTy (TArrow r a b)   = TyArrow r (getTy a) (getTy b)
getTy (TPoly r path n) = TyPoly r path (getTy n)
getTy (TVar r a)       = TyVar r a

insertSchema : Context -> (List String) -> Schema -> Context
insertSchema ctx name schema = insert (remove ctx name) name schema

interface Infer e where
  infer : Context -> e -> TI (Subst, Ty)

Infer Literal where
  infer ctx (LStr r _) = pure (empty, TySimple r "Text")
  infer ctx (LInt r _) = pure (empty, TySimple r "Int" )

Infer Expr where
  infer ctx (ELit r lit) = infer ctx lit

  infer ctx (EId path) =
    let listPath = pathToList path in
    case findVar listPath ctx of
      Just schema => do
        res <- instantiate schema
        pure (empty, res)
      Nothing     => lift $ throwE ("Cannot find variable: '" ++ (show path) ++ "'")

  infer ctx (ELambda r (MkName r2 name) expr) = do
    ty <- newTyVar
    let ctxWithArg = insertSchema ctx [name] (MkSchema [] ty)
    (s1, t1) <- infer ctxWithArg expr
    pure (s1, TyArrow r (apply s1 ty) t1)

  infer ctx (ECall r fun expr) = do
    tyRes       <- newTyVar
    (s1, tyFun) <- infer ctx fun
    (s2, tyArg) <- infer (apply s1 ctx) expr
    s3          <- unify (apply s2 tyFun) (TyArrow r tyArg tyRes)
    pure ((s3 `composeSubst` s2) `composeSubst` s1, apply s3 tyRes)

  infer ctx (EDo r (exprs@(h :: tl))) = do
    let lastExpr    = last exprs
    let returnsVoid = init exprs
    (subst, ty) <- infer ctx lastExpr
    subTypeList <- traverse (infer ctx) returnsVoid
    substList   <- traverse (unify (TySimple emptyRange "Unit")) (map snd subTypeList)
    let voidSub   = foldl composeSubst empty substList
    let lastSub   = subTypeList
    pure (subst `composeSubst` voidSub, ty)

  infer ctx (EDo r []) = pure (empty, TySimple r "Unit")

  infer ctx (ELet r (MkName r2 name) val expr) = do
    (s0, tyVal)  <- infer ctx val
    let s0WithArg = insertSchema (apply s0 ctx) [name] (MkSchema [] tyVal)
    (s1, tyExpr) <- infer s0WithArg expr
    pure (s1, tyExpr)

  infer ctx e = lift $ throwE ("Not implemented")

Infer Def where
  infer ctx (Define name Nothing expr) = do
    (s1, ty) <- infer ctx expr
    pure (s1, ty)

  infer ctx (Define name (Just ret) expr) = do
    (s1, ty) <- infer ctx expr
    s2 <- unify (apply s1 (getTy ret)) ty
    pure (s2, ty)

public export
runInference : Def -> Either String (Subst, Ty)
runInference e =
  let ctx = (insert ["unit"] (MkSchema [] (TySimple emptyRange "Unit")) empty) in
  let (Id res) = runEitherT $ evalStateT 0 (infer (MkCtx ctx) e) in
  res

max_stars_repo_name: felipegchi/Yurei

max_issues_repo_name: felipegchi/Yurei

max_forks_repo_name: felipegchi/Yurei


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

module Process

import Tester

import Data.List.Quantifiers
import Language.TOML
import Language.TOML.Processing
import Data.List.Elem

basicUnordered : Test
basicUnordered = test "process unordered table" $ assert $ check result
    where
        Spec : TableTy
        Spec = MkFieldTy "name" False TString `And` MkFieldTy "age" False TInteger `And` Emp

        table : Table
        table = fromList [("age", VInteger 999), ("name", VString "John Doe")]

        result : Either TableError (TableOf Spec)
        result = processTable Spec table

        check : Either TableError (TableOf Spec) -> Bool
        check (Left x) = False
        check (Right [name, age]) = name == "John Doe" && age == 999

basicNested : Test
basicNested = test "process nested table" $ assert $ check result
    where
        Spec : TableTy
        Spec = MkFieldTy "name" False TString `And`
                MkFieldTy "age" False TInteger `And`
                MkFieldTy "skills" False (TTable
                    (MkFieldTy "running" False TInteger `And`
                     MkFieldTy "programming" False TInteger `And`
                     Emp)) `And`
                Emp

        table : Table
        table = fromList [("age", VInteger 999),
                          ("name", VString "John Doe"),
                          ("skills", VTable $ fromList
                              [("running", VInteger 5),
                               ("programming", VInteger 8)])]

        result : Either TableError (TableOf Spec)
        result = processTable Spec table

        check : Either TableError (TableOf Spec) -> Bool
        check (Left x) = False
        check (Right [name, age, [running, programming]]) =
            name == "John Doe" && age == 999 && running == 5 && programming == 8

basicOptional : Test
basicOptional = test "process table with optional field" $ assert $ check result
    where
        Spec : TableTy
        Spec = MkFieldTy "name" True TString `And` MkFieldTy "age" False TInteger `And` Emp

        table : Table
        table = fromList [("age", VInteger 999)]

        result : Either TableError (TableOf Spec)
        result = processTable Spec table

        check : Either TableError (TableOf Spec) -> Bool
        check (Left x) = False
        check (Right [name, age]) = name == Nothing && age == 999

basicDependent : Test
basicDependent = test "process table dependent layout" $ assert $ check result
    where
        Spec : TableTy
        Spec = Ext (MkFieldTy "programmer" False TBoolean) $ \programmer =>
            if programmer
               then MkFieldTy "fave-lang" False TString `And` Emp
               else Emp

        table : Table
        table = fromList [("programmer", VBoolean True), ("fave-lang", VString "idris")]

        result : Either TableError (TableOf Spec)
        result = processTable Spec table

        check : Either TableError (TableOf Spec) -> Bool
        check (Left x) = False
        check (Right (True :: lang :: [])) = lang == "idris"
        check (Right (False :: tbl)) = False

basicEnum : Test
basicEnum = test "process enum" $ assert $ check result
    where
        Spec : ValueTy
        Spec = TEnum ["idris", "haskell", "lisp"]

        table : Value
        table = VString "idris"

        result : Either ValueError (ValueOf Spec)
        result = processValue Spec table

        check : Either ValueError (ValueOf Spec) -> Bool
        check (Left x) = False
        check (Right ("idris" ** _)) = True
        check (Right (_ ** _)) = False

export
tests : List Test
tests = [basicUnordered, basicNested, basicOptional, basicDependent, basicEnum]


text:
import Data.Vect

{-

data Elem : a -> Vect k a -> Type where
   Here : Elem x (x :: xs)
   There : (later : Elem x xs) -> Elem x (y :: xs)

-}

total
removeElem : (value : a) -> (xs : Vect (S n) a) -> (witn : Elem value xs) ->
             Vect n a
removeElem value (value :: ys) Here = ys
{- removeElem value (y :: []) (There later) = absurd  later -}
removeElem {n = (S k)} value (y :: ys) (There later)
     = y :: removeElem value ys later

not_in_nil : Elem value [] -> Void
not_in_nil Here impossible
not_in_nil (There _) impossible

max_stars_repo_name: wdomitrz/Coq-Exercises

max_issues_repo_name: wdomitrz/Coq-Exercises

max_forks_repo_name: wdomitrz/Coq-Exercises


text:
-- ---------------------------------------------------------------- [ Tree.idr ]
-- Module      : Data.Hitchhiker.Tree
-- Description : An Idris implementation of hitchhiker trees.
-- Copyright   : (c) 2016 Eric Bailey
-- License     : BSD-3
-- Link        : https://github.com/elm-community/string-extra
-- --------------------------------------------------------------------- [ EOH ]
||| Hitchhiker trees.
module Data.Hitchhiker.Tree

import public Data.Vect

-- -------------------------------------------------------------- [ Statements ]

%access public export

||| Specify a change in value `a` for a particular key `k`.
data Statement : Type -> Type -> Type where

     ||| Assert the value of `k` is `a`.
     Assert : k -> a -> Statement k a

     ||| Retract the value of `k`.
     Retract : k -> Statement k a

export
keyFor : Statement k a -> k
keyFor (Assert k _) = k
keyFor (Retract k)  = k

export
toStatement : k -> Maybe a -> Statement k a
toStatement k = maybe (Retract k) (Assert k)

export
valueFor : Statement k a -> Maybe a
valueFor (Assert _ a) = Just a
valueFor (Retract _)  = Nothing

Log : Type -> Type -> Type
Log k a = List (Statement k a)

NodeLog : Nat -> Type -> Type -> Type
NodeLog l k a = Vect l (Statement k a)

Leaves : Nat -> Type -> Type -> Type
Leaves c k a = Vect c (k, Log k a)

-- type Hitchhiker l b k = (Ord k, KnownNat l, KnownNat b, 2 ::<= b)
Hitchhiker : Ord k => (l, b, k : Nat) -> Type
Hitchhiker l b k = LTE 2 b

mutual

    Children : (c, d, l, b : Nat) -> Type -> Type -> Type
    Children c d l b k a = Vect c (k, HNode d l b k a)

    data HNode : (d, l, b : Nat) -> Type -> Type -> Type where

         HLeaf : Ord k => Leaves c k a ->
                 {auto lower : LTE b c} ->
                 {auto upper : LTE c (2 * b)} ->
                 HNode 0 l b k a

         HInt  : Ord k => NodeLog e k a ->
                 Children c (pred d) l b k a ->
                 {auto pos   : LTE 1 b} ->
                 {auto lower : LTE b c} ->
                 {auto upper : LTE c (2 * b)} ->
                 {auto log   : LTE e l} ->
                 HNode d l b k a

data HTree : (l, b : Nat) -> (k, a : Type) -> Type where

     ||| Partial root node, acting like a leaf.
     Partial : Leaves c k a ->
               {auto lower : LTE 0 c} -> {auto upper : LTE c (2 * b)} ->
               HTree l b k a

     ||| Full root node, acting like an internal node.
     Full : NodeLog e k a -> Children c d l b k a ->
            -- {auto pos : LTE 1 2} ->
            {auto lower : LTE 2 c} ->
            {auto upper : LTE c (2 * b)} ->
            {auto log   : LTE e l} ->
            HTree l b k a

total
lookupOrdRange : Ord k => k -> Vect n (k, a) -> {auto pos : LTE 1 n} -> a
lookupOrdRange k0 ((_,a0) :: kas) = go a0 kas
  where
    go : a -> Vect m (k,a) -> a
    go a [] = a
    go a ((k, a') :: kas') =
        case compare k0 k of
             LT => a
             EQ => a'
             GT => go a' kas'

lookupLogs : Ord k => k -> HTree l b k a ->
             {auto two : LTE 2 b} ->
             Log k a
lookupLogs x ht =
    case ht of
         Partial lvs  => fromLeaves lvs
         Full lg chld => fromInt lg chld
  where
    fromNode : HNode d l b k a -> Log k a

    fromLeaves : Leaves c k a -> Log k a
    fromLeaves = fromMaybe [] . lookup x

    fromInt : NodeLog e k a ->
              Children c d l b k a ->
              {auto pos   : LTE 1 lb} ->
              {auto lower : LTE lb c} ->
              {auto upper : LTE c (2 * b)} ->
              {auto log   : LTE e l} ->
              Log k a
    fromInt lg chld {pos} {lower} =
        let (_ ** fromLg) = Vect.filter (\z => x == keyFor z) lg
            fromChld = fromNode (lookupOrdRange x chld {pos = lteTransitive pos lower}) in
            toList fromLg ++ fromChld

    fromNode (HLeaf lvs)    = fromLeaves lvs
    fromNode (HInt lg chld) = fromInt lg chld

empty : Ord k => {auto two : LTE 2 b} -> HTree l b k a
empty = Partial Nil

%access export

addLeaves : {res : Nat -> Nat -> Type -> Type -> Type} ->
            Ord k => (lb : Nat) -> (Leaves c' k a -> res l b k a) ->
            NodeLog e k a -> Leaves c k a ->
            {auto pos : LTE 1 b} ->
            {auto lower : LTE lb c} ->
            {auto upper : LTE lb b} ->
            Either (k, res l b k a) (Vect n (k, HNode 0 l b k a))

addInternal : {res : Nat -> Nat -> Type -> Type -> Type} ->
              Ord k => (lb : Nat) ->
              (NodeLog e' k a -> Children c' d l b k a -> res l b k a) ->
              NodeLog lc k a -> NodeLog e k a -> Children c d l b k a ->
              {auto p1 : 1 `LTE` lb} ->
              {auto p2 : lb `LTE` c} ->
              {auto p3 : c `LTE` 2 * b} ->
              {auto p4 : e `LTE` l} ->
              {auto p5 : lb `LTE` c'} ->
              {auto p6 : c' `LTE` 2 * b} ->
              {auto p7 : e' `LTE` l} ->
              Either (k, res l b k a) (Vect m (k, HNode (d + 1) l b k a))
-- addInternal lb mkRes lgAdd lg chld {e'} {l} {res} =
--     case isLTE (S l) e' of
--          Yes prf   => ?addInternal_rhs_rhs_1
--          No contra => let lg' = lgAdd ++ lg in Left (sameLevel lg' chld)
--   where
--     sameLevel : NodeLog e' k a -> Children c' d l b k a -> (k, res l b k a)

addLog : Ord k => NodeLog e k a -> HNode d l b k a ->
         {auto prf : LTE 1 b} ->
         (n ** Vect n (k, HNode d l b k a))
addLog lgAdd (HLeaf lvs)    = ?addLog_rhs_1
addLog lgAdd (HInt lg chld) = ?addLog_rhs_2

addStatements : Ord k => List (Statement k a) -> HTree l b k a ->
                {auto two : LTE 2 b} ->
                HTree l b k a
addStatements [] ht    = ht
addStatements stmts ht =
    let lgAdd = fromList stmts in
        case ht of
             Partial lvs  => ?addStatements_rhs_1
             Full lg chld => ?addStatements_rhs_2
  where
    handleOverflow : Vect n (k, HNode d l b k a) -> HTree l b k a
    checkOverflow : Either (k, HTree l b k a) (Vect n (k, HNode d l b k a)) -> HTree l b k a
    checkOverflow = either snd handleOverflow

fromList : Ord k => List (k,a) -> {auto two : LTE 2 b} -> HTree l b k a
fromList xs = addStatements (map (uncurry Assert) xs) empty

insert : Ord k => k -> a -> HTree l b k a ->
         {auto two : LTE 2 b} ->
         HTree l b k a
insert k a = addStatements [Assert k a]

delete : Ord k => k -> HTree l b k a -> {auto two : LTE 2 b} -> HTree l b k a
delete k = addStatements [Retract k]

addStatement : Ord k => Statement k a -> HTree l b k a ->
               {auto two : LTE 2 b} ->
               HTree l b k a
addStatement = addStatements . pure

lookup : Ord k => k -> HTree l b k a ->
         {auto two : LTE 2 b} ->
         Maybe a
lookup k ht = listToMaybe (lookupLogs k ht) >>= valueFor

adjustWithKey : Ord k => (k -> a -> a) -> k -> HTree l b k a ->
                {auto two : LTE 2 b} ->
                HTree l b k a
adjustWithKey f k ht = maybe ht (\v => insert k (f k v) ht) (lookup k ht)

adjust : Ord k => (a -> a) -> k -> HTree l b k a ->
         {auto two : LTE 2 b} ->
         HTree l b k a
adjust = adjustWithKey . const

updateWithKey : Ord k => (k -> a -> Maybe a) -> k -> HTree l b k a ->
                {auto two : LTE 2 b} ->
                HTree l b k a
updateWithKey f k ht =
    maybe ht (\v => addStatement (toStatement k (f k v)) ht) (lookup k ht)

update : Ord k => (a -> Maybe a) -> k -> HTree l b k a ->
         {auto two : LTE 2 b} ->
         HTree l b k a
update = updateWithKey . const

alter : Ord k => (Maybe a -> Maybe a) -> k -> HTree l b k a ->
        {auto two : LTE 2 b} ->
        HTree l b k a
alter f k ht = addStatement (toStatement k (f (lookup k ht))) ht

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

max_stars_repo_name: yurrriq/idris-hitchhiker-tree

max_issues_repo_name: yurrriq/idris-hitchhiker-tree

max_forks_repo_name: yurrriq/idris-hitchhiker-tree


text:
module Data.List.Views

import Control.Relation
import Control.WellFounded
import Data.List
import Data.Nat
import Data.Nat.Views

%default total

lengthSuc : (xs : List a) -> (y : a) -> (ys : List a) ->
            length (xs ++ (y :: ys)) = S (length (xs ++ ys))
lengthSuc [] _ _ = Refl
lengthSuc (x :: xs) y ys = cong S (lengthSuc xs y ys)

lengthLT : (xs : List a) -> (ys : List a) ->
           LTE (length xs) (length (ys ++ xs))
lengthLT xs [] = reflexive {x = length xs}
lengthLT xs (x :: ys) = lteSuccRight (lengthLT _ _)

smallerLeft : (ys : List a) -> (y : a) -> (zs : List a) ->
              LTE (S (S (length ys))) (S (length (ys ++ (y :: zs))))
smallerLeft [] y zs = LTESucc (LTESucc LTEZero)
smallerLeft (z :: ys) y zs = LTESucc (smallerLeft ys _ _)

smallerRight : (ys : List a) -> (zs : List a) ->
               LTE (S (S (length zs))) (S (length (ys ++ (y :: zs))))
smallerRight ys zs = rewrite lengthSuc ys y zs in
                     (LTESucc (LTESucc (lengthLT _ _)))

||| View for splitting a list in half, non-recursively
public export
data Split : List a -> Type where
     SplitNil : Split []
     SplitOne : (x : a) -> Split [x]
     SplitPair : (x : a) -> (xs : List a) ->
                 (y : a) -> (ys : List a) ->
                 Split (x :: xs ++ y :: ys)

splitHelp : (head : a) ->
            (xs : List a) ->
            (counter : List a) -> Split (head :: xs)
splitHelp head [] counter = SplitOne _
splitHelp head (x :: xs) [] = SplitPair head [] x xs
splitHelp head (x :: xs) [y] = SplitPair head [] x xs
splitHelp head (x :: xs) (_ :: _ :: ys)
    = case splitHelp head xs ys of
           SplitOne x => SplitPair x [] _ []
           SplitPair x' xs y' ys => SplitPair x' (x :: xs) y' ys

||| Covering function for the `Split` view
||| Constructs the view in linear time
export
split : (xs : List a) -> Split xs
split [] = SplitNil
split (x :: xs) = splitHelp x xs xs

public export
data SplitRec : List a -> Type where
     SplitRecNil : SplitRec []
     SplitRecOne : (x : a) -> SplitRec [x]
     SplitRecPair : (lefts, rights : List a) -> -- Explicit, don't erase
                    (lrec : Lazy (SplitRec lefts)) ->
                    (rrec : Lazy (SplitRec rights)) -> SplitRec (lefts ++ rights)

||| Covering function for the `SplitRec` view
||| Constructs the view in O(n lg n)
public export
splitRec : (xs : List a) -> SplitRec xs
splitRec xs with (sizeAccessible xs)
  splitRec xs | acc with (split xs)
    splitRec []  | acc | SplitNil = SplitRecNil
    splitRec [x] | acc | SplitOne x = SplitRecOne x
    splitRec (y :: ys ++ z :: zs) | Access acc | SplitPair y ys z zs
      = SplitRecPair _ _
          (splitRec (y :: ys) | acc _ (smallerLeft ys z zs))
          (splitRec (z :: zs) | acc _ (smallerRight ys zs))

||| View for traversing a list backwards
public export
data SnocList : List a -> Type where
     Empty : SnocList []
     Snoc : (x : a) -> (xs : List a) ->
            (rec : SnocList xs) -> SnocList (xs ++ [x])

snocListHelp : {input : _} ->
               SnocList input -> (rest : List a) -> SnocList (input ++ rest)
snocListHelp snoc [] = rewrite appendNilRightNeutral input in snoc
snocListHelp snoc (x :: xs)
   = rewrite appendAssociative input [x] xs in
             snocListHelp (Snoc x input snoc) xs

||| Covering function for the `SnocList` view
||| Constructs the view in linear time
export
snocList : (xs : List a) -> SnocList xs
snocList xs = snocListHelp Empty xs


text:
f : Num a => a
f = g where
  g : Num a => a
  g = 0


text:
||| A segment is a compositional fragment of a telescope.
||| A key difference is that segments are right-nested, whereas
||| telescopes are left nested.
||| So telescopes are convenient for well-bracketing dependencies,
||| but segments are convenient for processing telescopes from left
||| to right.
|||
||| As with telescopes, indexing segments by their length (hopefully)
||| helps the type-checker infer stuff.
module Data.Telescope.Segment

import Data.Telescope.Telescope

import Syntax.PreorderReasoning
import Data.Fin
import Data.Nat
import Data.DPair

%default total

||| A segment is a compositional fragment of a telescope, indexed by
||| the segment's length.
public export
data Segment : (n : Nat) -> Left.Telescope k -> Type where
  Nil  : Segment 0 gamma
  (::) : (ty : TypeIn gamma) -> (delta : Segment n (gamma -. ty)) -> Segment (S n) gamma

||| A segment of size `n` indexed by `gamma` can be seen as the tabulation of a
||| function that turns environments for `gamma` into telescopes of size `n`.
public export
tabulate : (n : Nat) -> (Left.Environment gamma -> Left.Telescope n) -> Segment n gamma
tabulate Z tel = []
tabulate (S n) tel = (sigma :: tabulate n (uncurry delta)) where

  sigma : TypeIn gamma
  sigma env = fst (uncons (tel env))

  delta : (env : Environment gamma) -> sigma env -> Left.Telescope n
  delta env v with (uncons (tel env))
    delta env v | (sig ** delt ** _) = delt v

||| Any telescope is a segment in the empty telescope. It amounts to looking
||| at it left-to-right instead of right-to-left.
public export
fromTelescope : {k : Nat} -> Left.Telescope k -> Segment k []
fromTelescope gamma = tabulate _ (const gamma)

||| Conversely, a segment of size `n` in telescope `gamma` can be seen as a function
||| from environments for `gamma` to telescopes of size `n`.
public export
untabulate : {n : Nat} -> Segment n gamma -> (Left.Environment gamma -> Left.Telescope n)
untabulate []            _   = []
untabulate (ty :: delta) env = cons (ty env) (untabulate delta . (\ v => (env ** v)))

||| Any segment in the empty telescope correspond to a telescope.
public export
toTelescope : {k : Nat} -> Segment k [] -> Left.Telescope k
toTelescope seg = untabulate seg ()

%name Segment delta,delta',delta1,delta2

infixl 3 |++, :++

||| This lemma comes up all the time when mixing induction on Nat with
||| indexing modulo addition.  An alternative is to use something like
||| frex.
succLemma : (lft, rgt : Nat) -> lft + (S rgt) = S (lft + rgt)
succLemma x y = Calc $
  |~ x + (1 + y)
  ~~ (x + 1)+ y  ...(plusAssociative x 1 y)
  ~~ (1 + x)+ y  ...(cong (+y) $ plusCommutative x 1)
  ~~ 1 + (x + y) ...(sym $ plusAssociative 1 x y)

-- Should go somehwere in stdlib
public export
keep : (0 prf : a ~=~ b) -> a ~=~ b
keep Refl = Refl

-- Keeping the `Nat` argument relevant, should (hopefully) only
-- case-split on it and not the environment unnecessarily, allowing us
-- to calculate, so long as we know the 'shape' of the Segment.
--
-- This should work in theory, I don't think it actually works for
-- Idris at the moment.  Might work in Agda?

||| Segments act on telescope from the right.
public export
(|++) : (gamma : Left.Telescope k) -> {n : Nat} -> (delta : Segment n gamma) -> Left.Telescope (n + k)
(|++)  gamma {n = 0} delta  = gamma
(|++)  gamma {n=S n} (ty :: delta) = rewrite sym $ succLemma n k in
                                       gamma -. ty |++ delta

||| Segments form a kind of an indexed monoid w.r.t. the action `(|++)`
public export
(++) : {gamma : Left.Telescope k}
    -> {n : Nat}
    -> (lft : Segment n  gamma         )
    -> (rgt : Segment m (gamma |++ lft))
    -> Segment (n + m) gamma
(++) {n = 0  } delta       rgt = rgt
(++) {n = S n} (ty :: lft) rgt = ty :: lft ++ rewrite succLemma n k in
                                              rgt
-- This monoid does act on telescopes:
export
actSegmentAssociative : (gamma : Left.Telescope k)
                     -> (lft : Segment n gamma)
                     -> (rgt : Segment m (gamma |++ lft))
                     -> (gamma |++ (lft ++ rgt)) ~=~ ((gamma |++ lft) |++ rgt)
actSegmentAssociative gamma {n = 0}   []          rgt = Refl
actSegmentAssociative gamma {n = S n} (ty :: lft) rgt =
  let rgt' : Segment {k = n + (S k)} m (gamma -. ty |++ lft)
      rgt' = rewrite succLemma n k in
             rgt
      rgt_eq_rgt' : rgt ~=~ rgt'
      rgt_eq_rgt' = rewrite succLemma n k in
                    Refl
  in
  rewrite sym $ succLemma (n + m) k in
  rewrite sym $ succLemma n       k in keep $ Calc $
  |~ ((gamma -. ty) |++ (lft ++ rgt'))
  ~~ ((gamma -. ty |++  lft) |++ rgt')
          ...(actSegmentAssociative (gamma -. ty) lft rgt')

public export
weaken : {0 gamma : Left.Telescope k}
      -> {delta : Segment n gamma} -> (sy : TypeIn gamma)
      -> TypeIn (gamma |++ delta)
weaken           {delta = []         } sy = sy
weaken {n = S n} {delta = ty :: delta} sy = rewrite sym $ succLemma n k in
                                            weaken (weakenTypeIn sy)

public export
projection : {0 gamma : Left.Telescope k}
          -> {n : Nat}
          -> {0 delta : Segment n gamma}
          -> Environment (gamma |++ delta)
          -> Environment gamma
projection {n = 0  } {delta = []         } env = env
projection {n = S n} {delta = ty :: delta} env
  = let (env' ** _) = projection {n} {delta}
                    $ rewrite succLemma n k in env
    in env'

infixl 4 .=

public export
data Environment : (env : Left.Environment gamma)
                -> (delta : Segment n gamma) -> Type where
  Empty : Environment env []
  (.=) : {0 gamma : Left.Telescope k} -> {0 ty : TypeIn gamma}
      -> {0 env   : Left.Environment gamma}
      -> {0 delta : Segment n (gamma -. ty)}

      -> (x : ty env) -> (xs : Segment.Environment (env ** x) delta)
      -> Environment env (ty :: delta)

public export
(:++) : {0 gamma : Left.Telescope k} -> {0 delta : Segment n gamma}
     -> (env : Left.Environment gamma)
     -> (ext : Segment.Environment env delta)
     ->        Left.Environment (gamma |++ delta)
(:++) env Empty = env
(:++) {n = S n} env (x .= xs) = rewrite sym $ succLemma n k in
                                (env ** x) :++ xs

-- This is too nasty for now, leave to later
{-
public export
break : {0 k : Nat} -> (gamma : Telescope k') -> (pos : Position gamma)
     -> {auto 0 ford : k' = cast pos + k } -> Telescope k
break gamma          FZ      {ford = Refl} = gamma
break []            (FS pos) {ford = _   } impossible
break {k' = S k'} (gamma -. ty) (FS pos) {ford} = break gamma pos
  {ford = Calc $
   |~ k'
   ~~ cast pos + k ...(succInjective _ _ ford)}

-- Should go into Data.Fin
export
lastIsLast : {n : Nat} -> cast (last {n}) = n
lastIsLast {n = 0  } = Refl
lastIsLast {n = S n} = rewrite lastIsLast {n} in
                       Refl

public export
finComplement : {n : Nat} -> (i : Fin n) -> Fin n
finComplement FZ = last
finComplement (FS i) = weaken (finComplement i)

export
castNaturality : (i : Fin n) -> finToNat (weaken i) ~=~ finToNat i
castNaturality  FZ    = Refl
castNaturality (FS i) = rewrite castNaturality i in
                        Refl

export
finComplementSpec : (i : Fin (S n)) -> cast i + cast (finComplement i) = n
finComplementSpec FZ = keep lastIsLast
finComplementSpec {n = .(S n)} (FS i@ FZ   ) = rewrite castNaturality (finComplement i) in
                                               rewrite finComplementSpec i in
                                               Refl
finComplementSpec {n = .(S n)} (FS i@(FS _)) = rewrite castNaturality (finComplement i) in
                                               rewrite finComplementSpec i in
                                               Refl

complementLastZero : (n : Nat) -> finComplement (last {n}) = FZ
complementLastZero n = finToNatInjective _ _ $ plusLeftCancel n _ _ $ Calc $
   let n' : Nat
       n' = cast $ finComplement $ last {n} in
   |~ n + n'
   ~~ (finToNat $ last {n})  + n'
                    ...(cong (+n') $ sym $ lastIsLast {n})
   ~~ n             ...(finComplementSpec $ last {n})
   ~~ n         + 0 ...(sym $ plusZeroRightNeutral n)

public export
breakOnto : {0 k,k' : Nat} -> (gamma : Telescope k) -> (pos : Position gamma)
         -> (delta : Segment n gamma)
         -> {auto 0 ford1 : k' === (finToNat $ finComplement pos) }
         -> {default
               -- disgusting, sorry
               (replace {p = \u => k = finToNat pos + u}
                        (sym ford1)
                        (sym $ finComplementSpec pos))
             0 ford2 : (k === ((finToNat pos) + k')) }
         -> Segment (cast pos + n)
                    (break {k = k'}
                           gamma pos
                           {ford = ford2})
breakOnto gamma          FZ      delta {ford1 = Refl} {ford2} =
                         rewrite sym ford2 in
                         delta
breakOnto (gamma -. ty) (FS pos) delta {ford1 = Refl} {ford2} =
                         rewrite sym $ succLemma (cast pos) n in
                         rewrite castNaturality (finComplement pos) in
                         breakOnto gamma pos (ty :: delta)

uip : (prf1, prf2 : x ~=~ y) -> prf1 ~=~ prf2
uip Refl Refl = Refl

export
breakStartEmpty : (gamma : Telescope k')
               -> {auto 0 ford1 : k = 0}
               -> {auto 0 ford2 : k' = finToNat (start gamma) + k}
               -> break {k} {k'} gamma (start gamma) {ford = ford2}
                ~=~ Telescope.Nil
breakStartEmpty [] {ford1 = Refl} {ford2 = Refl}            = Refl
breakStartEmpty {k} {k' = S k'} {ford1} {ford2} (gamma -. ty) =
                -- Yuck!
                let 0 u : (k' = finToNat (start gamma) + k)
                    u = succInjective _ _ ford2
                    v : break {k} {k'} gamma (start gamma) {ford = u}
                        ~=~ Telescope.Nil
                    v = breakStartEmpty {k} {k'} gamma {ford2 = u}
                in replace {p = \z =>
                             Equal {a = Telescope k} {b = Telescope 0}
                                   (break {k'} {k} gamma (start gamma)
                                          {ford = z})
                                          []
                        }
                        (uip u _)
                        (keep v)

public export
projection : {0 gamma : Telescope k} -> (pos : Position gamma) -> (env : Environment gamma)
          -> Environment (break {k = cast (finComplement pos)} gamma pos
                                {ford = sym $ finComplementSpec pos})
projection FZ env = rewrite finComplementSpec $ FZ {k} in
                    env
projection {gamma = []} (FS pos) Empty impossible
projection {k = S k} {gamma = gamma -. ty} (FS pos) (env ** x) =
  rewrite castNaturality (finComplement pos) in
  projection {k} pos env
-}


text:
import System.Signal
import System
import Data.List
import Data.Fuel

main : IO ()
main = do
  Right () <- collectSignal SigABRT
    | Left (Error code) => putStrLn $ "error " ++ (show code)
  Right () <- collectSignal SigILL
    | Left (Error code) => putStrLn $ "error " ++ (show code)
  putStrLn "before"
  [Right (), Right (), Right ()] <- sequence $ replicate 3 (raiseSignal SigABRT)
    | _ => putStrLn $ "got non-zero exit from a system call"
  [Right (), Right (), Right ()] <- sequence $ replicate 3 (raiseSignal SigILL)
    | _ => putStrLn $ "got non-zero exit from a system call"
  sleep 1
  [SigILL, SigABRT] <- handleManyCollectedSignals (limit 4)
    | (_ :: _ :: [])  => putStrLn "received the wrong signals."
    | _ => putStrLn "did not receive expected number of signals."
  putStrLn "after"
  Right () <- defaultSignal SigABRT
    | Left (Error code) => putStrLn $ "error " ++ (show code)
  putStrLn "done."


text:
module IdrTest.Expectation

import Color

public export
Expectation : Type
Expectation = Maybe String

export
assertEq : Show a => Eq a => a -> a -> Expectation
assertEq a b =
  if a == b then
    Nothing
  else
    Just ("Failed expectation, expected " ++ (decorate (Text Green) (show a)) ++ "=" ++ (decorate (Text Red) (show b)))

export
pass : Expectation
pass =
  Nothing

export
fail : String -> Expectation
fail err =
  Just ("Failed expectation: " ++ (decorate (Text Red) err))


text:
||| Implementing `Decidable.Order.Strict` for `Data.Nat.LT`
module Data.Nat.Order.Strict

import Data.Nat
import Decidable.Order.Strict
import Decidable.Equality
import Data.Nat.Order

%default total

public export
Irreflexive Nat LT where
  irreflexive {x = 0} _ impossible
  irreflexive {x = S _} (LTESucc prf) =
    irreflexive {rel = Nat.LT} prf

public export
Transitive Nat LT where
  transitive {x} {y} xy yz =
    transitive {rel = LTE} (lteSuccRight xy) yz

public export
StrictPreorder Nat LT where

public export
decLT : (a, b : Nat) -> DecOrdering {lt = LT} a b
decLT 0       0   = DecEQ Refl
decLT 0     (S b) = DecLT (LTESucc LTEZero)
decLT (S a)  0    = DecGT (LTESucc LTEZero)
decLT (S a) (S b) = case decLT a b of
  DecLT a_lt_b => DecLT (LTESucc a_lt_b)
  DecEQ Refl   => DecEQ Refl
  DecGT b_lt_a => DecGT (LTESucc b_lt_a)

public export
StrictOrdered Nat LT where
  order = decLT


text:
module Derive.ShowTests

import Pruviloj
import Derive.Show

namespace TestDecls
  -- Can't derive Eq for this one!
  data SimpleFun a b = MkSimpleFun (a -> b)

  data MyNat = MyZ | MyS MyNat

  data MyList a = Nil | (::) a (MyList a)

  namespace V
    data MyVect : MyNat -> Type -> Type where
      Nil : MyVect MyZ a
      (::) : a -> MyVect n a -> MyVect (MyS n) a

  -- All elements of this should be Eq, because it's for runtime and the Nat is erased
  data CompileTimeNat : Type where
    MkCTN : .(n : Nat) -> CompileTimeNat

decl syntax derive Show for {n} = %runElab (deriveShow `{n})

derive Show for MyNat
derive Show for MyList
derive Show for MyVect
derive Show for CompileTimeNat

namespace Tests
  test1 : show (with V [1,2,3]) = "(::) 1 ((::) 2 ((::) 3 Nil))"
  test1 = Refl

  test2 : show (MyS (MyS MyZ)) = "MyS (MyS MyZ)"
  test2 = Refl

  test3 : show (the (MyVect _ Integer) [1,2,3]) = show (the (MyList Integer) [1,2,3])
  test3 = Refl

  test4 : show (MkCTN 45) = "MkCTN _"
  test4 = Refl

max_stars_repo_name: Garnasha/derive-all-the-instances

max_issues_repo_name: Garnasha/derive-all-the-instances

max_forks_repo_name: Garnasha/derive-all-the-instances


text:
||| We define some meta types that help with specification of syntax.
|||
||| We need some types to facilitate a nameless representation (De Bruijn indicies) for recursion variables.
|||
||| We need types for local branch and selection
module Sessions.Meta

import Decidable.Equality

%default total

public export
data Ty = R -- recursion variable
        | G -- protocol

public export
data ChoiceTy = BRANCH | SELECT

notBS : BRANCH = SELECT -> Void
notBS Refl impossible

export
DecEq ChoiceTy where
  decEq BRANCH BRANCH = Yes Refl
  decEq BRANCH SELECT = No notBS
  decEq SELECT BRANCH = No (negEqSym notBS)
  decEq SELECT SELECT = Yes Refl

public export
DecEq : (typeR, typeL, typeR : Type)
     -> Type
DecEq a b c = (DecEq a, DecEq b, DecEq c)

-- [ EOF ]

max_stars_repo_name: DSbD-AppControl/sessions-playground

max_issues_repo_name: DSbD-AppControl/sessions-playground

max_forks_repo_name: DSbD-AppControl/sessions-playground


text:
import WebServer

main : JS_IO ()
main = do
  putStrLn' "Server starting..."
  startServer 4000
              (putStrLn' "The server is ready!") $
              \req =>
                MkResponse
                  OK
                  ("Nice " ++ show (method req) ++ " request, bro\n")
                  []

-- Local Variables:
-- idris-load-packages: ("contrib")
-- End:

max_stars_repo_name: camelpunch/idris-web-server

max_issues_repo_name: camelpunch/idris-web-server

max_forks_repo_name: camelpunch/idris-web-server


text:
module Testlib2

import Testlib1

export
val2 : String
val2 = val1 ++ "Have a great day!\n"

max_stars_repo_name: idream-build/idream

max_issues_repo_name: idream-build/idream

max_forks_repo_name: idream-build/idream


text:
import Data.Vect

inputs : Vect 3 Double
inputs = [1.2, 5.1, 2.1]

weights : Vect 3 Double
weights = [3.1, 2.1, 8.7]

bias : Double
bias = 3.0

-- NOTE: this is not the idiomatic way to implement this.  This follows
-- the spirit of the Python lesson, which aims for simplicity and clarity.
output : Double
output = (index 0 inputs)*(index 0 weights) +
         (index 1 inputs)*(index 1 weights) +
         (index 2 inputs)*(index 2 weights) + bias

main : IO ()
main = printLn output


text:
module Web.Internal.GeometryTypes

import JS

--------------------------------------------------------------------------------
--          Interfaces
--------------------------------------------------------------------------------

export data DOMMatrix : Type where [external]

export
ToFFI DOMMatrix DOMMatrix where toFFI = id

export
FromFFI DOMMatrix DOMMatrix where fromFFI = Just

export
SafeCast DOMMatrix where
  safeCast = unsafeCastOnPrototypeName "DOMMatrix"

export data DOMMatrixReadOnly : Type where [external]

export
ToFFI DOMMatrixReadOnly DOMMatrixReadOnly where toFFI = id

export
FromFFI DOMMatrixReadOnly DOMMatrixReadOnly where fromFFI = Just

export
SafeCast DOMMatrixReadOnly where
  safeCast = unsafeCastOnPrototypeName "DOMMatrixReadOnly"

export data DOMPoint : Type where [external]

export
ToFFI DOMPoint DOMPoint where toFFI = id

export
FromFFI DOMPoint DOMPoint where fromFFI = Just

export
SafeCast DOMPoint where
  safeCast = unsafeCastOnPrototypeName "DOMPoint"

export data DOMPointReadOnly : Type where [external]

export
ToFFI DOMPointReadOnly DOMPointReadOnly where toFFI = id

export
FromFFI DOMPointReadOnly DOMPointReadOnly where fromFFI = Just

export
SafeCast DOMPointReadOnly where
  safeCast = unsafeCastOnPrototypeName "DOMPointReadOnly"

export data DOMQuad : Type where [external]

export
ToFFI DOMQuad DOMQuad where toFFI = id

export
FromFFI DOMQuad DOMQuad where fromFFI = Just

export
SafeCast DOMQuad where
  safeCast = unsafeCastOnPrototypeName "DOMQuad"

export data DOMRect : Type where [external]

export
ToFFI DOMRect DOMRect where toFFI = id

export
FromFFI DOMRect DOMRect where fromFFI = Just

export
SafeCast DOMRect where
  safeCast = unsafeCastOnPrototypeName "DOMRect"

export data DOMRectList : Type where [external]

export
ToFFI DOMRectList DOMRectList where toFFI = id

export
FromFFI DOMRectList DOMRectList where fromFFI = Just

export
SafeCast DOMRectList where
  safeCast = unsafeCastOnPrototypeName "DOMRectList"

export data DOMRectReadOnly : Type where [external]

export
ToFFI DOMRectReadOnly DOMRectReadOnly where toFFI = id

export
FromFFI DOMRectReadOnly DOMRectReadOnly where fromFFI = Just

export
SafeCast DOMRectReadOnly where
  safeCast = unsafeCastOnPrototypeName "DOMRectReadOnly"

--------------------------------------------------------------------------------
--          Dictionaries
--------------------------------------------------------------------------------

export data DOMMatrix2DInit : Type where [external]

export
ToFFI DOMMatrix2DInit DOMMatrix2DInit where toFFI = id

export
FromFFI DOMMatrix2DInit DOMMatrix2DInit where fromFFI = Just

export data DOMMatrixInit : Type where [external]

export
ToFFI DOMMatrixInit DOMMatrixInit where toFFI = id

export
FromFFI DOMMatrixInit DOMMatrixInit where fromFFI = Just

export data DOMPointInit : Type where [external]

export
ToFFI DOMPointInit DOMPointInit where toFFI = id

export
FromFFI DOMPointInit DOMPointInit where fromFFI = Just

export data DOMQuadInit : Type where [external]

export
ToFFI DOMQuadInit DOMQuadInit where toFFI = id

export
FromFFI DOMQuadInit DOMQuadInit where fromFFI = Just

export data DOMRectInit : Type where [external]

export
ToFFI DOMRectInit DOMRectInit where toFFI = id

export
FromFFI DOMRectInit DOMRectInit where fromFFI = Just


text:
module Simple

infixr 10 ::

data Nat = Z | S n

data List : Type -> Type where
  Nil : List a
  Cons : a -> List a -> List a

corecord Stream a where
  head : a
  tail : Stream a
  constructor (::)

corecord BisimStream a (s : Stream a) (t : Stream a) where
   phead : head s = head t
   ptail : BisimStream a (tail s) (tail t)

record Foo a where
  xs : List a

max_stars_repo_name: sualitu/thesis

max_issues_repo_name: sualitu/thesis

max_forks_repo_name: sualitu/thesis