text:
module Backprop.Math

import Backprop.CanBack
import Backprop.Node
import Control.Optics
import public Data.Floating
import public Data.Num

export
view : {a, b : _} -> CanBack a => Simple Lens a b -> Node i a -> Node i b
view l = op1 $ \[x] => (x ^. l, \d => [set l d zero])

infixl 0 ^.
export
(^.) : {a, b : _} -> CanBack a => Node i a -> Simple Lens a b -> Node i b
x ^. l = view l x

export
sum : {a : _} -> (CanBack a, NodeFunctor f, Num a, Foldable f) => Node i (f a) -> Node i a
sum x = Prelude.sum $ Node.sequence x

export
max, min : {a : _} -> (CanBack a, Num a, Ord a) => Node i a -> Node i a -> Node i a
max = op2 $ \[x, y] => (max x y, \d => [d * if x > y then 1 else 0, d * if y > x then 1 else 0])
min = op2 $ \[x, y] => (min x y, \d => [d * if x < y then 1 else 0, d * if y < x then 1 else 0])

-- machine learning specific

export
relu : {a : _} -> (CanBack a, Num a, Ord a) => Node i a -> Node i a
relu x = max 0 x


text:
module Gen
import Data.Fin
import Data.ZZ

%hide Prelude.Classes.(+)
%hide Prelude.Classes.(*)
%hide Prelude.Classes.(-)
%hide Prelude.Classes.(/)

%default total

-- Fin -> Nat

implicit finNat : Fin n -> Nat
finNat = finToNat

-- Fin, Nat, Integer -> ZZ

implicit finZZ : Fin n -> ZZ
finZZ = Pos . finToNat

implicit natZZ : Nat -> ZZ
natZZ = Pos

implicit integerZZ : Integer -> ZZ
integerZZ = cast

-- Fin, Nat, ZZ -> Integer

implicit zzInteger : ZZ -> Integer
zzInteger = cast

implicit natInteger : Nat -> Integer
natInteger = zzInteger . natZZ

implicit finInteger : Fin n -> Integer
finInteger = zzInteger . finZZ

-- operations

namespace NatOp
  (+) : Nat -> Nat -> Nat
  (+) = plus

  (*) : Nat -> Nat -> Nat
  (*) = mult

namespace ZZOp
  (+) : ZZ -> ZZ -> ZZ
  (+) = plusZ

  (*) : ZZ -> ZZ -> ZZ
  (*) = multZ

  (-) : ZZ -> ZZ -> ZZ
  (-) = subZ

namespace IntegerOp
  (+) : Integer -> Integer -> Integer
  (+) = prim__addBigInt

  (*) : Integer -> Integer -> Integer
  (*) = prim__mulBigInt

  (-) : Integer -> Integer -> Integer
  (-) = prim__subBigInt

-- Rationals

data Rat : Type where
  (#) : ZZ -> (y:Nat) -> {default Refl nz: isZero y = False} -> Rat

infixl 9 #

nonZeroMult : (x,y: Nat) -> isZero x = False -> isZero y = False -> isZero (mult x y) = False
nonZeroMult Z y p1 p2 = void $ trueNotFalse p1
nonZeroMult (S k) Z p1 p2 = void $ trueNotFalse p2
nonZeroMult (S k) (S j) p1 p2 = Refl

isRZero : Rat -> Bool
isRZero ((#) (Pos Z) y) = True
isRZero _ = False

rPlus : Rat -> Rat -> Rat
rPlus ((#) x y {nz=p1}) ((#) x' y' {nz=p2}) =
  (#) (x * y' + x' * y) (y * y') {nz=nonZeroMult y y' p1 p2}

rSub : Rat -> Rat -> Rat
rSub ((#) x y {nz=p1}) ((#) x' y' {nz=p2}) =
  (#) (x * y' - x' * y) (y * y') {nz=nonZeroMult y y' p1 p2}

rMult : Rat -> Rat -> Rat
rMult ((#) k j {nz=p1}) ((#) i y {nz=p2}) =
  (#) (k * i) (j * y) {nz=nonZeroMult j y p1 p2}

rDiv : Rat -> (y: Rat) -> isRZero y = False -> Rat
rDiv ((#) k j {nz=p1}) ((#) (Pos Z) y {nz=p2}) rnz = void $ trueNotFalse rnz
rDiv ((#) k j {nz=p1}) ((#) (Pos (S i)) y {nz=p2}) rnz =
  (#) (k * y) (j * (S i)) {nz=nonZeroMult j (S i) p1 Refl}
rDiv ((#) (Pos Z) j {nz=p1}) ((#) (NegS i) y {nz=p2}) rnz = 0#1
rDiv ((#) (Pos (S k)) j {nz=p1}) ((#) (NegS i) y {nz=p2}) rnz =
  (#) ((NegS k) * y) (j * (S i)) {nz=nonZeroMult j (S i) p1 Refl}
rDiv ((#) (NegS k) j {nz=p1}) ((#) (NegS i) y {nz=p2}) rnz =
  (#) ((S k) * y) (j * (S i)) {nz=nonZeroMult j (S i) p1 Refl}

-- Fin, Nat, ZZ, Integer -> Rat

implicit zzRat : ZZ -> Rat
zzRat = (# 1)

implicit integerRat : Integer -> Rat
integerRat = zzRat . integerZZ

implicit natRat : Nat -> Rat
natRat = zzRat . natZZ

implicit finRat : Fin n -> Rat
finRat = zzRat . finZZ

namespace RatOp
  (+) : Rat -> Rat -> Rat
  (+) = rPlus

  (*) : Rat -> Rat -> Rat
  (*) = rMult

  (-) : Rat -> Rat -> Rat
  (-) = rSub

  (/) : Rat -> (y: Rat) -> {default Refl nz: isRZero y = False} -> Rat
  (/) x y {nz} = rDiv x y nz

ext: idr

max_stars_repo_name: defanor/numtower

max_issues_repo_name: defanor/numtower

max_forks_repo_name: defanor/numtower


text:
module Common.Lte

import Data.Fin

%access export

%default total

fromEqLte : (l = r) -> LTE l r
fromEqLte prf = rewrite prf in lteRefl

lteAddBoth : LTE n m -> LTE (c + n) (c + m)
lteAddBoth {c = Z} lte = lte
lteAddBoth {c = (S k)} lte =
  let ind = lteAddBoth lte
  in (LTESucc ind)

lteSum : LTE l1 r1 -> LTE l2 r2 -> LTE (l1 + l2) (r1 + r2)
lteSum LTEZero lte2 {r1} {r2} =
  rewrite plusCommutative r1 r2 in
  lte2 `lteTransitive` lteAddRight r2
lteSum (LTESucc lte1') lte2 = LTESucc (lteSum lte1' lte2)

lteMultConst : LTE n m -> LTE (c * n) (c * m)
lteMultConst {c = Z} lte = LTEZero
lteMultConst {c = (S k)} {m} {n} lte =
  let ind = lteMultConst {c=k} lte
  in lteSum lte ind

elemStrictlySmallerThanBound : (n : Fin m) -> LT (finToNat n) m
elemStrictlySmallerThanBound FZ = LTESucc LTEZero
elemStrictlySmallerThanBound (FS x) =
  let ind = elemStrictlySmallerThanBound x
  in LTESucc ind

lteZeqZ : LTE a Z -> a = Z
lteZeqZ LTEZero = Refl

tightBound : LTE a b -> LTE b a -> a = b
tightBound LTEZero LTEZero = Refl
tightBound (LTESucc x) (LTESucc y) = eqSucc _ _ (tightBound x y)

splitLte : LTE a b -> Either (a = b) (LT a b)
splitLte {a = Z} {b = Z} LTEZero = Left Refl
splitLte {a = Z} {b = (S k)} LTEZero = Right (LTESucc LTEZero)
splitLte {a = (S _)} {b = Z} LTEZero impossible
splitLte {a = (S _)} {b = Z} (LTESucc _) impossible
splitLte {a = (S k)} {b = (S j)} (LTESucc lte') =
  case splitLte lte' of
    (Left eq) => Left (eqSucc _ _ eq)
    (Right lt) => Right (LTESucc lt)

max_stars_repo_name: farrellm/dailyprover

max_issues_repo_name: farrellm/dailyprover

max_forks_repo_name: farrellm/dailyprover


text:
module Evens

-- The type `IsEven(n)`  has terms (objects) that are proofs that `n` is even.
data IsEven : Nat -> Type where
  ZeroEven : IsEven 0
  SSEven : (n: Nat) -> (pf: IsEven n) -> IsEven (S (S n))

twoEven : IsEven 2
twoEven = SSEven Z ZeroEven

fourEven : IsEven 4
fourEven = SSEven _ twoEven

half : (n: Nat) -> IsEven n -> Nat
half Z ZeroEven = 0
half (S (S k)) (SSEven k pf) =
  S (half k pf)

double: Nat -> Nat
double Z = Z
double (S k) = S (S (double k))

doubleEven: (n: Nat) -> IsEven (double n)
doubleEven Z = ZeroEven
doubleEven (S k) =
  SSEven (double k) (doubleEven k)

halfDouble : Nat -> Nat
halfDouble n = half (double n) (doubleEven n)

nOrSnEven : (n : Nat) -> Either (IsEven n) (IsEven (S n))
nOrSnEven Z = Left ZeroEven
nOrSnEven (S k) = case nOrSnEven k of
                       (Left l) => Right (SSEven k l)
                       (Right r) => Left r

oneOdd : IsEven 1 -> Void
oneOdd ZeroEven impossible
oneOdd (SSEven _ _) impossible

threeOdd : IsEven 3 -> Void
threeOdd (SSEven (S Z) ZeroEven) impossible
threeOdd (SSEven (S Z) (SSEven _ _)) impossible

nAndSnNotBothEven : (n: Nat) -> IsEven n -> IsEven (S n) -> Void
nAndSnNotBothEven Z ZeroEven ZeroEven impossible
nAndSnNotBothEven Z ZeroEven (SSEven _ _) impossible
nAndSnNotBothEven (S (S k)) (SSEven k pf) (SSEven (S k) x) =
  nAndSnNotBothEven k pf x

nOddThenSnEven : (n: Nat) -> (IsEven n -> Void) -> IsEven (S n)
nOddThenSnEven n contra =
  (case (nOrSnEven n) of
        (Left l) => void (contra l)
        (Right r) => r
        )

halfSucc : (n : Nat) -> ((IsEven n) -> Void) -> Nat
halfSucc n contra = half (S n) (nOddThenSnEven n contra)

apNat : (f: Nat -> Nat) -> (n: Nat) -> (m: Nat) -> n = m -> f n = f m
apNat f m m Refl = Refl

byTwo : (n: Nat) -> IsEven n -> (k: Nat ** double k = n)
byTwo Z ZeroEven = (Z ** Refl)
byTwo (S (S k)) (SSEven k pf) =
  (case byTwo k pf of
        (x ** pf) => (S x ** (apNat (\m => (S (S m))) (double x) k pf)))

isDouble: Nat -> Type
isDouble n = (m : Nat ** (double m) = n)

evenIsDouble: (n: Nat) -> IsEven n -> (isDouble n)
evenIsDouble = byTwo

transport : (a : Type) -> (P : a -> Type) ->  (x : a) -> (y : a) -> (x = y) -> P(x) -> P(y)
transport a P y y Refl z = z

doubleIsEven: (n: Nat) -> isDouble n -> IsEven n
doubleIsEven n pair =
  case pair of
        (k ** pf) =>
          transport Nat IsEven (double k) n pf (doubleEven k)

-- The Peano axioms

sInj : (x: Nat) -> (y: Nat) -> (S x = S y) -> (x = y)
sInj Z Z Refl = Refl
sInj (S k) (S k) Refl = Refl

sNotZ : (x: Nat) -> (S x = Z) -> Void
sNotZ _ Refl impossible

symmEq : (x: Nat) -> (y: Nat) -> (x = y) -> (y = x)
symmEq y y Refl = Refl

transEq: (x: Nat) -> (y: Nat) -> (z: Nat) -> (x = y) -> (y = z) -> (x = z)
transEq y y y Refl Refl = Refl

--- Less than or equal and subtraction

sub : (n: Nat) -> (m : Nat) -> (LTE m n) -> Nat
sub n Z LTEZero = n
sub (S right) (S left) (LTESucc x) = sub right left x

superSub : (n: Nat) -> (m : Nat) -> (LTE m n) -> (diff: Nat ** LTE diff n)
superSub n Z LTEZero = (n ** lteRefl)
superSub (S n) (S m) (LTESucc x) = case (superSub n m x) of
                                               (diff ** pf) => (diff ** lteSuccRight pf)

oneLTEFour : LTE 1 4
oneLTEFour = LTESucc LTEZero

fourMinusOne : Nat
fourMinusOne = sub 4 1 oneLTEFour

-- Range type

data InRange : Nat -> Nat -> Type where
  MkInRange : (l : Nat) -> (u : Nat) -> (n : Nat) -> LTE l n -> LTE n u -> InRange l u

oneBetween0And4 : InRange 0 4
oneBetween0And4 = MkInRange 0 4 1 LTEZero oneLTEFour

Cast (InRange n m) Nat where -- cast is an interface (typeclass in scala)
  cast (MkInRange n m k x y) = k

one: Nat
one = cast oneBetween0And4

--- space

max_stars_repo_name: siddhartha-gadgil/TrainLogic

max_issues_repo_name: siddhartha-gadgil/TrainLogic

max_forks_repo_name: siddhartha-gadgil/TrainLogic


text:
module Loops

import Data.Strings
import System

%default total

countdown : HasIO io => (secs : Nat) -> io ()
countdown Z = putStrLn "Lift-off!"
countdown (S k) = do putStrLn (show (S k))
                     usleep 1000000
                     countdown k

readNumber : HasIO io => io (Maybe Nat)
readNumber = do ns <- getLine
                if all isDigit (unpack ns)
                   then pure $ Just (stringToNatOrZ ns)
                   else pure Nothing

partial
countdowns : HasIO io => io ()
countdowns = do putStr "Enter starting number: "
                Just num <- readNumber
                  | Nothing => putStrLn "We accept only numbers, sorry!"
                countdown num
                putStr "Try again? [y/n]: "
                choice <- getLine
                if choice == "y" || choice == "yes"
                   then countdowns
                   else pure ()

max_stars_repo_name: timmyjose-study/tdd-with-idris

max_issues_repo_name: timmyjose-study/tdd-with-idris

max_forks_repo_name: timmyjose-study/tdd-with-idris


text:
module IdrisScript.Date

import IdrisScript
import public IdrisScript.Date.Months
import public IdrisScript.Date.Days
import public IdrisScript.Date.Types

%access public export

Date : JS_IO (JSValue JSFunction)
Date = do
  date <- jscall  "Date" (JS_IO Ptr)
  pure $ MkJSFunction date

JSDate : JSType
JSDate = JSObject "Date"

||| Creates a new `Date` object with the current time.
now : JS_IO (JSValue JSDate)
now = do
  res <- jscall "new Date()" (JS_IO Ptr)
  pure $ MkJSObject res

||| Creates a new `Date` object from milliseconds.
newDateFromMilliseconds : Milliseconds -> JS_IO (JSValue JSDate)
newDateFromMilliseconds (MkMilliseconds millis) = do
  res <- jscall "new Date(%0)" (Int -> JS_IO Ptr) millis
  pure $ MkJSObject res

||| Creates a new `Date` object from a string.
newDateFromString : String -> JS_IO (JSValue JSDate)
newDateFromString str = do
  res <- jscall "new Date(%0)" (String -> JS_IO Ptr) str
  pure $ MkJSObject res

||| Copies a `Date` object.
copyDate : (JSValue JSDate) -> JS_IO (JSValue JSDate)
copyDate date = do
  res <- jscall "new Date(%0)" (Ptr -> JS_IO Ptr) (unpack date)
  pure $ MkJSObject res

||| Gets the day of `Date` object.
getDay : JSValue JSDate -> JS_IO Day
getDay date = do
  day <- jscall "%0.getDay()" (Ptr -> JS_IO Int) (unpack date)
  pure $ toDay day
where
  toDay : Int -> Day
  toDay 1 = Monday
  toDay 2 = Tuesday
  toDay 3 = Wednesday
  toDay 4 = Thursday
  toDay 5 = Friday
  toDay 6 = Saturday
  toDay _ = Sunday

||| Gets the milliseconds from a `Date` object.
getMilliseconds : JSValue JSDate -> JS_IO Milliseconds
getMilliseconds date = do
  millis <- jscall "%0.getMilliseconds()" (Ptr -> JS_IO Int) (unpack date)
  pure $ MkMilliseconds millis

||| Sets the milliseconds from a `Date` object. Modifies the original date.
setMilliseconds : JSValue JSDate -> Milliseconds -> JS_IO (JSValue JSDate)
setMilliseconds date millis = do
  jscall "%0.getMilliseconds(%1)" (Ptr -> Int -> JS_IO Int)
             (unpack date) (unMilliseconds millis)
  pure date

||| Gets the month from a `Date` object.
getMonth : JSValue JSDate -> JS_IO Month
getMonth date  = do
  month <- jscall "%0.getMonth()" (Ptr -> JS_IO Int) (unpack date)
  pure $ toMonth month
where
  toMonth : Int -> Month
  toMonth 0  = January
  toMonth 1  = February
  toMonth 2  = March
  toMonth 3  = April
  toMonth 4  = May
  toMonth 5  = June
  toMonth 6  = July
  toMonth 7  = August
  toMonth 8  = September
  toMonth 9  = October
  toMonth 10 = November
  toMonth _  = December

||| Sets the month from a `Date` object. Modifies the original date.
setMonth : JSValue JSDate -> Month -> JS_IO (JSValue JSDate)
setMonth date month = do
  jscall "%0.setMonth(%1)" (Ptr -> Int -> JS_IO Int)
           (unpack date) (fromMonth month)
  pure date
where
  fromMonth : Month -> Int
  fromMonth January   = 0
  fromMonth February  = 1
  fromMonth March     = 2
  fromMonth April     = 3
  fromMonth May       = 4
  fromMonth June      = 5
  fromMonth July      = 6
  fromMonth August    = 7
  fromMonth September = 8
  fromMonth October   = 9
  fromMonth November  = 10
  fromMonth December  = 11

||| Gets the year from a `Date` object.
getYear : JSValue JSDate -> JS_IO Int
getYear date = jscall "%0.getYear()" (Ptr -> JS_IO Int) (unpack date)

||| Sets the year from a `Date` object. Modifies the original date.
setYear : JSValue JSDate -> Year -> JS_IO (JSValue JSDate)
setYear date year = do
  jscall "%0.setYear(%1)" (Ptr -> Int -> JS_IO Int)
         (unpack date) (unYear year)
  pure date

||| Gets the date from a `Date` object.
getDate : JSValue JSDate -> JS_IO Date
getDate date = do
  date' <- jscall "%0.getDate()" (Ptr -> JS_IO Int) (unpack date)
  pure $ MkDate date'

||| Sets the date from a `Date` object. Modifies the original date.
setDate : JSValue JSDate -> Date -> JS_IO (JSValue JSDate)
setDate date date' = do
  jscall "%0.setDate(%1)" (Ptr -> Int -> JS_IO Int)
          (unpack date) (unDate date')
  pure date

||| Gets the hours from a `Date` object.
getHours : JSValue JSDate -> JS_IO Hours
getHours date = do
  hours <- jscall "%0.getHours()" (Ptr -> JS_IO Int) (unpack date)
  pure $ MkHours hours

||| Sets the hours from a `Date` object. Modifies the original date.
setHours : JSValue JSDate -> Hours -> JS_IO (JSValue JSDate)
setHours date hours = do
  jscall "%0.setHours(%1)" (Ptr -> Int -> JS_IO Int)
         (unpack date) (unHours hours)
  pure date

||| Gets the minutes from a `Date` object.
getMinutes : JSValue JSDate -> JS_IO Minutes
getMinutes date = do
  minutes <- jscall "%0.getMinutes()" (Ptr -> JS_IO Int) (unpack date)
  pure $ MkMinutes minutes

||| Sets the minutes from a `Date` object. Modifies the original date.
setMinutes : JSValue JSDate -> Minutes -> JS_IO (JSValue JSDate)
setMinutes date mins = do
  jscall "%0.setMinutes(%1)" (Ptr -> Int -> JS_IO Int)
         (unpack date) (unMinutes mins)
  pure date

||| Gets the seconds from a `Date` object.
getSeconds : JSValue JSDate -> JS_IO Seconds
getSeconds date = do
  seconds <- jscall "%0.getSeconds()" (Ptr -> JS_IO Int) (unpack date)
  pure $ MkSeconds seconds

||| Sets the seconds from a `Date` object. Modifies the original date.
setSeconds : JSValue JSDate -> Seconds -> JS_IO (JSValue JSDate)
setSeconds date secs = do
  jscall "%0.setSeconds(%1)" (Ptr -> Int -> JS_IO Int)
         (unpack date) (unSeconds secs)
  pure date

||| Gets the full year of a `Date` object.
getFullYear : JSValue JSDate -> JS_IO Year
getFullYear date = do
  year <- jscall "%0.getFullYear()" (Ptr -> JS_IO Int) (unpack date)
  pure $ MkYear year

||| Sets the full year of a `Date` object. Modifies the original date.
setFullYear : JSValue JSDate -> Year -> JS_IO (JSValue JSDate)
setFullYear date year = do
  jscall "%0.setFullYear(%1)" (Ptr -> Int -> JS_IO Int)
         (unpack date) (unYear year)
  pure date

max_stars_repo_name: jimmyhmiller/IdrisScript

max_issues_repo_name: jimmyhmiller/IdrisScript

max_forks_repo_name: jimmyhmiller/IdrisScript


text:
module CFT.DependentLens

public export
record DepLens (s, a : Type) (t : s -> Type) (b : a -> Type) where
  constructor MkDepLens
  get : s -> a
  set : (es : s) -> b (get es) -> t es

max_stars_repo_name: andrevidela/dev-notes

max_issues_repo_name: andrevidela/dev-notes

max_forks_repo_name: andrevidela/dev-notes


text:
module Core.Context.Context

import        Core.CaseTree
import        Core.CompileExpr
import        Core.Env
import        Core.Hash
import public Core.Name
import public Core.Options.Log
import public Core.TT

import Data.Fin
import Data.IORef
import Data.List
import Data.List1
import Data.Maybe
import Data.Nat

import Libraries.Data.IntMap
import Libraries.Data.IOArray
import Libraries.Data.NameMap
import Libraries.Data.UserNameMap
import Libraries.Utils.Binary

public export
data Ref : (l : label) -> Type -> Type where
     [search l]
     MkRef : IORef a -> Ref x a

public export
data HoleInfo
        = NotHole
        | SolvedHole Nat

public export
record PMDefInfo where
  constructor MkPMDefInfo
  holeInfo : HoleInfo -- data if it comes from a solved hole
  alwaysReduce : Bool -- always reduce, even when quoting etc
                 -- typically for inlinable metavariable solutions
  externalDecl : Bool -- declared in another module, which may affect how it
                      -- is compiled

export
defaultPI : PMDefInfo
defaultPI = MkPMDefInfo NotHole False False

public export
record TypeFlags where
  constructor MkTypeFlags
  uniqueAuto : Bool  -- should 'auto' implicits check for uniqueness
  external : Bool -- defined externally (e.g. in a C or Scheme library)

export
defaultFlags : TypeFlags
defaultFlags = MkTypeFlags False False

public export
record HoleFlags where
  constructor MkHoleFlags
  implbind : Bool -- stands for an implicitly bound name
  precisetype : Bool -- don't generalise multiplicities when instantiating

export
holeInit : Bool -> HoleFlags
holeInit b = MkHoleFlags b False

public export
data Def : Type where
    None : Def -- Not yet defined
    PMDef : (pminfo : PMDefInfo) ->
            (args : List Name) ->
            (treeCT : CaseTree args) ->
            (treeRT : CaseTree args) ->
            (pats : List (vs ** (Env Term vs, Term vs, Term vs))) ->
                -- original checked patterns (LHS/RHS) with the names in
                -- the environment. Used for display purposes, for helping
                -- find size changes in termination checking, and for
                -- generating specialised definitions (so needs to be the
                -- full, non-erased, term)
            Def -- Ordinary function definition
    ExternDef : (arity : Nat) -> Def
    ForeignDef : (arity : Nat) ->
                 List String -> -- supported calling conventions,
                                -- e.g "C:printf,libc,stdlib.h", "scheme:display", ...
                 Def
    Builtin : {arity : Nat} -> PrimFn arity -> Def
    DCon : (tag : Int) -> (arity : Nat) ->
           (newtypeArg : Maybe (Bool, Nat)) ->
               -- if only constructor, and only one argument is non-Rig0,
               -- flag it here. The Nat is the unerased argument position.
               -- The Bool is 'True' if there is no %World token in the
               -- structure, which means it is safe to completely erase
               -- when pattern matching (otherwise we still have to ensure
               -- that the value is inspected, to make sure external effects
               -- happen)
           Def -- data constructor
    TCon : (tag : Int) -> (arity : Nat) ->
           (parampos : List Nat) -> -- parameters
           (detpos : List Nat) -> -- determining arguments
           (flags : TypeFlags) -> -- should 'auto' implicits check
           (mutwith : List Name) ->
           (datacons : List Name) ->
           (detagabbleBy : Maybe (List Nat)) ->
                    -- argument positions which can be used for
                    -- detagging, if it's possible (to check if it's
                    -- safe to erase)
           Def
    Hole : (numlocs : Nat) -> -- Number of locals in scope at binding point
                              -- (mostly to help display)
           HoleFlags ->
           Def
    BySearch : RigCount -> (maxdepth : Nat) -> (defining : Name) -> Def
    -- Constraints are integer references into the current map of
    -- constraints in the UnifyState (see Core.UnifyState)
    Guess : (guess : ClosedTerm) ->
            (envbind : Nat) -> -- Number of things in the environment when
                               -- we guessed the term
            (constraints : List Int) -> Def
    ImpBind : Def -- global name temporarily standing for an implicitly bound name
    -- A delayed elaboration. The elaborators themselves are stored in the
    -- unification state
    Delayed : Def

export
defNameType : Def -> Maybe NameType
defNameType None = Nothing
defNameType (PMDef {}) = Just Func
defNameType (ExternDef {}) = Just Func
defNameType (ForeignDef {}) = Just Func
defNameType (Builtin {}) = Just Func
defNameType (DCon tag ar _) = Just (DataCon tag ar)
defNameType (TCon tag ar _ _ _ _ _ _) = Just (TyCon tag ar)
defNameType (Hole {}) = Just Func
defNameType (BySearch {}) = Nothing
defNameType (Guess {}) = Nothing
defNameType ImpBind = Just Bound
defNameType Delayed = Nothing

export
Show Def where
  show None = "undefined"
  show (PMDef _ args ct rt pats)
      = show args ++ ";\nCompile time tree: " ++ show ct ++
        "\nRun time tree: " ++ show rt
  show (DCon t a nt)
      = "DataCon " ++ show t ++ " " ++ show a
           ++ maybe "" (\n => " (newtype by " ++ show n ++ ")") nt
  show (TCon t a ps ds u ms cons det)
      = "TyCon " ++ show t ++ " " ++ show a ++ " params: " ++ show ps ++
        " constructors: " ++ show cons ++
        " mutual with: " ++ show ms ++
        " detaggable by: " ++ show det
  show (ExternDef arity) = "<external def with arity " ++ show arity ++ ">"
  show (ForeignDef a cs) = "<foreign def with arity " ++ show a ++
                           " " ++ show cs ++">"
  show (Builtin {arity} _) = "<builtin with arith " ++ show arity ++ ">"
  show (Hole _ p) = "Hole" ++ if implbind p then " [impl]" else ""
  show (BySearch c depth def) = "Search in " ++ show def
  show (Guess tm _ cs) = "Guess " ++ show tm ++ " when " ++ show cs
  show ImpBind = "Bound name"
  show Delayed = "Delayed"

public export
record Constructor where
  constructor MkCon
  loc : FC
  name : Name
  arity : Nat
  type : ClosedTerm

public export
data DataDef : Type where
     MkData : (tycon : Constructor) -> (datacons : List Constructor) ->
              DataDef

public export
data Clause : Type where
     MkClause : {vars : _} ->
                (env : Env Term vars) ->
                (lhs : Term vars) -> (rhs : Term vars) -> Clause

export
Show Clause where
  show (MkClause {vars} env lhs rhs)
      = show vars ++ ": " ++ show lhs ++ " = " ++ show rhs

public export
data DefFlag
    = Inline
    | Invertible -- assume safe to cancel arguments in unification
    | Overloadable -- allow ad-hoc overloads
    | TCInline -- always inline before totality checking
         -- (in practice, this means it's reduced in 'normaliseHoles')
         -- This means the function gets inlined when calculating the size
         -- change graph, but otherwise not. It's only safe if the function
         -- being inlined is terminating no matter what, and is really a bit
         -- of a hack to make sure interface dictionaries are properly inlined
         -- (otherwise they look potentially non terminating) so use with
         -- care!
    | SetTotal TotalReq
    | BlockedHint -- a hint, but blocked for the moment (so don't use)
    | Macro
    | PartialEval (List (Name, Nat)) -- Partially evaluate on completing defintion.
         -- This means the definition is standing for a specialisation so we
         -- should evaluate the RHS, with reduction limits on the given names,
         -- and ensure the name has made progress in doing so (i.e. has reduced
         -- at least once)
    | AllGuarded -- safe to treat as a constructor for the purposes of
         -- productivity checking. All clauses are guarded by constructors,
         -- and there are no other function applications
    | ConType ConInfo
         -- Is it a special type of constructor, e.g. a nil or cons shaped
         -- thing, that can be compiled specially?
    | Identity Nat
         -- Is it the identity function at runtime?
         -- The nat represents which argument the function evaluates to

export
Eq DefFlag where
    (==) Inline Inline = True
    (==) Invertible Invertible = True
    (==) Overloadable Overloadable = True
    (==) TCInline TCInline = True
    (==) (SetTotal x) (SetTotal y) = x == y
    (==) BlockedHint BlockedHint = True
    (==) Macro Macro = True
    (==) (PartialEval x) (PartialEval y) = x == y
    (==) AllGuarded AllGuarded = True
    (==) (ConType x) (ConType y) = x == y
    (==) (Identity x) (Identity y) = x == y
    (==) _ _ = False

export
Show DefFlag where
  show Inline = "inline"
  show Invertible = "invertible"
  show Overloadable = "overloadable"
  show TCInline = "tcinline"
  show (SetTotal x) = show x
  show BlockedHint = "blockedhint"
  show Macro = "macro"
  show (PartialEval _) = "partialeval"
  show AllGuarded = "allguarded"
  show (ConType ci) = "contype " ++ show ci
  show (Identity x) = "identity " ++ show x

public export
data SizeChange = Smaller | Same | Unknown

export
Show SizeChange where
  show Smaller = "Smaller"
  show Same = "Same"
  show Unknown = "Unknown"

export
Eq SizeChange where
  Smaller == Smaller = True
  Same == Same = True
  Unknown == Unknown = True
  _ == _ = False

public export
record SCCall where
     constructor MkSCCall
     fnCall : Name -- Function called
     fnArgs : List (Maybe (Nat, SizeChange))
        -- relationship to arguments of calling function; argument position
        -- (in the calling function), and how its size changed in the call.
        -- 'Nothing' if it's not related to any of the calling function's
        -- arguments

export
Show SCCall where
  show c = show (fnCall c) ++ ": " ++ show (fnArgs c)

export
Eq SCCall where
  x == y = fnCall x == fnCall y && fnArgs x == fnArgs y

public export
record GlobalDef where
  constructor MkGlobalDef
  location : FC
  fullname : Name -- original unresolved name
  type : ClosedTerm
  eraseArgs : List Nat -- which argument positions to erase at runtime
  safeErase : List Nat -- which argument positions are safe to assume
                       -- erasable without 'dotting', because their types
                       -- are collapsible relative to non-erased arguments
  specArgs : List Nat -- arguments to specialise by
  inferrable : List Nat -- arguments which can be inferred from elsewhere in the type
  multiplicity : RigCount
  localVars : List Name -- environment name is defined in
  visibility : Visibility
  totality : Totality
  flags : List DefFlag
  refersToM : Maybe (NameMap Bool)
  refersToRuntimeM : Maybe (NameMap Bool)
  invertible : Bool -- for an ordinary definition, is it invertible in unification
  noCycles : Bool -- for metavariables, whether they can be cyclic (this
                  -- would only be allowed when using a metavariable as a
                  -- placeholder for a yet to be elaborated arguments, but
                  -- not for implicits because that'd indicate failing the
                  -- occurs check)
  linearChecked : Bool -- Flag whether we've already checked its linearity
  definition : Def
  compexpr : Maybe CDef
  sizeChange : List SCCall

export
gDefKindedName : GlobalDef -> KindedName
gDefKindedName def
  = let nm = fullname def in
    MkKindedName (defNameType $ definition def) nm nm

export
refersTo : GlobalDef -> NameMap Bool
refersTo def = maybe empty id (refersToM def)

export
refersToRuntime : GlobalDef -> NameMap Bool
refersToRuntime def = maybe empty id (refersToRuntimeM def)

export
findSetTotal : List DefFlag -> Maybe TotalReq
findSetTotal [] = Nothing
findSetTotal (SetTotal t :: _) = Just t
findSetTotal (_ :: xs) = findSetTotal xs

-- Label for array references
export
data Arr : Type where

-- A context entry. If it's never been looked up, we haven't decoded the
-- binary blob yet, so decode it first time
public export
data ContextEntry : Type where
     Coded : Namespace -> -- namespace for decoding into, with restoreNS
             Binary -> ContextEntry
     Decoded : GlobalDef -> ContextEntry

public export
data PossibleName : Type where
     Direct : Name -> Int -> PossibleName -- full name and resolved name id
     Alias : Name -> -- aliased name (from "import as")
             Name -> Int -> -- real full name and resolved name, as above
             PossibleName

-- All the GlobalDefs. We can only have one context, because name references
-- point at locations in here, and if we have more than one the indices won't
-- match up. So, this isn't polymorphic.
public export
record Context where
    constructor MkContext
    firstEntry : Int -- First entry in the current source file
    nextEntry : Int
    -- Map from full name to its position in the context
    resolvedAs : NameMap Int
    -- Map from usernames to all the possible names in all namespaces
    possibles : UserNameMap (List PossibleName)
    -- Reference to the actual content, indexed by Int
    content : Ref Arr (IOArray ContextEntry)
    -- Branching depth, in a backtracking elaborator. 0 is top level; at lower
    -- levels we need to stage updates rather than add directly to the
    -- 'content' store
    branchDepth : Nat
    -- Things which we're going to add, if this branch succeeds
    staging : IntMap ContextEntry

    -- Namespaces which are visible (i.e. have been imported)
    -- This only matters during evaluation and type checking, to control
    -- access in a program - in all other cases, we'll assume everything is
    -- visible
    visibleNS : List Namespace
    allPublic : Bool -- treat everything as public. This is intended
                     -- for checking partially evaluated definitions
                     -- or for use outside of the main compilation
                     -- process (e.g. when implementing interactive
                     -- features such as case splitting).
    inlineOnly : Bool -- only return things with the 'alwaysReduce' flag
    hidden : NameMap () -- Never return these


text:
module LoooongRecur

%default total

data TTy : Nat -> Nat -> Nat -> Nat -> Bool -> Type where

  TA : TTy p1 r1 i1 i2 False ->
       TTy i1 i2 i1 u2 False ->
       TTy i1 i2 p2 b1 b2    ->
       TTy p1 r1 p1 i2 False

  TB : TTy v1 r1 v2 r2 bt ->
       TTy v1 r1 v1 r2 (be && bt)

  TC : TTy p1 r1 v2 r2 False ->
       TTy v2 r2 v3 r3 b2    ->
       TTy p1 r1 v3 r3 b2

n : Nat -> Nat
n = (+ 2)

showInd : (indent : Nat) -> TTy p1 r1 v3 r3 br -> String
showInd i (TA x1 x2 x3) = if False
                            then (if False then show' i else show' i)
                            else showInd (n i) x1 ++ show' (n i)
                            where
                              show' : Nat -> String
                              show' i = showInd (n i) x3 ++ if False then "" else showInd (n i) x2
showInd i (TB x) = showInd (n i) x ++ if False then "" else showInd (n i) x
showInd i (TC x y) = if False then showInd i y else showInd i x ++ showInd i y

max_stars_repo_name: buzden/idris-playground

max_issues_repo_name: buzden/idris-playground

max_forks_repo_name: buzden/idris-playground


text:
-- Based on https://www.iana.org/assignments/http-status-codes/http-status-codes.txt

module Network.HTTP.Status

import Data.Nat
import Generics.Derive

%language ElabReflection

public export
record StatusCodeNumber (n : Nat) where
  constructor Abv100Und600
  lte599 : LTE n 599
  gte100 : GTE n 100

export
is_status_code_number : (n : Nat) -> Dec (StatusCodeNumber n)
is_status_code_number n =
  case isLTE n 599 of
    Yes ok1 =>
      case isGTE n 100 of
        Yes ok2 => Yes (Abv100Und600 ok1 ok2)
        No nope => No (nope . gte100)
    No nope => No (nope . lte599)

public export
data StatusCodeClass : Type where
  Information : StatusCodeClass
  Successful : StatusCodeClass
  Redirection : StatusCodeClass
  ClientError : StatusCodeClass
  ServerError : StatusCodeClass

%runElab derive "StatusCodeClass" [Generic, Meta, Eq, Show]

public export
data StatusCode : Nat -> Type where
  Continue : StatusCode 100
  SwitchingProtocols : StatusCode 101
  Processing : StatusCode 102
  EarlyHints : StatusCode 103
  OK : StatusCode 200
  Created : StatusCode 201
  Accepted : StatusCode 202
  NonAuthoritativeInformation : StatusCode 203
  NoContent : StatusCode 204
  ResetContent : StatusCode 205
  PartialContent : StatusCode 206
  MultiStatus : StatusCode 207
  AlreadyReported : StatusCode 208
  IMUsed : StatusCode 226
  MultipleChoices : StatusCode 300
  MovedPermanently : StatusCode 301
  Found : StatusCode 302
  SeeOther : StatusCode 303
  NotModified : StatusCode 304
  UseProxy : StatusCode 305
  TemporaryRedirect : StatusCode 307
  PermanentRedirect : StatusCode 308
  Unauthorized : StatusCode 401
  PaymentRequired : StatusCode 402
  Forbidden : StatusCode 403
  NotFound : StatusCode 404
  MethodNotAllowed : StatusCode 405
  NotAcceptable : StatusCode 406
  ProxyAuthenticationRequired : StatusCode 407
  RequestTimeout : StatusCode 408
  Conflict : StatusCode 409
  Gone : StatusCode 410
  LengthRequired : StatusCode 411
  PreconditionFailed : StatusCode 412
  ContentTooLarge : StatusCode 413
  URITooLong : StatusCode 414
  UnsupportedMediaType : StatusCode 415
  RangeNotSatisfiable : StatusCode 416
  ExpectationFailed : StatusCode 417
  MisdirectedRequest : StatusCode 421
  UnprocessableContent : StatusCode 422
  Locked : StatusCode 423
  FailedDependency : StatusCode 424
  TooEarly : StatusCode 425
  UpgradeRequired : StatusCode 426
  PreconditionRequired : StatusCode 428
  TooManyRequests : StatusCode 429
  RequestHeaderFieldsTooLarge : StatusCode 431
  UnavailableForLegalReasons : StatusCode 451
  InternalServerError : StatusCode 500
  NotImplemented : StatusCode 501
  BadGateway : StatusCode 502
  ServiceUnavailable : StatusCode 503
  GatewayTimeout : StatusCode 504
  HTTPVersionNotSupported : StatusCode 505
  VariantAlsoNegotiates : StatusCode 506
  InsufficientStorage : StatusCode 507
  LoopDetected : StatusCode 508
  NetworkAuthenticationRequired : StatusCode 511
  UnknownStatusCode : (n : Nat) -> StatusCodeNumber n -> StatusCode n

export
Show (StatusCode n) where
  show Continue = "Continue"
  show SwitchingProtocols = "SwitchingProtocols"
  show Processing = "Processing"
  show EarlyHints = "EarlyHints"
  show OK = "OK"
  show Created = "Created"
  show Accepted = "Accepted"
  show NonAuthoritativeInformation = "NonAuthoritativeInformation"
  show NoContent = "NoContent"
  show ResetContent = "ResetContent"
  show PartialContent = "PartialContent"
  show MultiStatus = "MultiStatus"
  show AlreadyReported = "AlreadyReported"
  show IMUsed = "IMUsed"
  show MultipleChoices = "MultipleChoices"
  show MovedPermanently = "MovedPermanently"
  show Found = "Found"
  show SeeOther = "SeeOther"
  show NotModified = "NotModified"
  show UseProxy = "UseProxy"
  show TemporaryRedirect = "TemporaryRedirect"
  show PermanentRedirect = "PermanentRedirect"
  show Unauthorized = "Unauthorized"
  show PaymentRequired = "PaymentRequired"
  show Forbidden = "Forbidden"
  show NotFound = "NotFound"
  show MethodNotAllowed = "MethodNotAllowed"
  show NotAcceptable = "NotAcceptable"
  show ProxyAuthenticationRequired = "ProxyAuthenticationRequired"
  show RequestTimeout = "RequestTimeout"
  show Conflict = "Conflict"
  show Gone = "Gone"
  show LengthRequired = "LengthRequired"
  show PreconditionFailed = "PreconditionFailed"
  show ContentTooLarge = "ContentTooLarge"
  show URITooLong = "URITooLong"
  show UnsupportedMediaType = "UnsupportedMediaType"
  show RangeNotSatisfiable = "RangeNotSatisfiable"
  show ExpectationFailed = "ExpectationFailed"
  show MisdirectedRequest = "MisdirectedRequest"
  show UnprocessableContent = "UnprocessableContent"
  show Locked = "Locked"
  show FailedDependency = "FailedDependency"
  show TooEarly = "TooEarly"
  show UpgradeRequired = "UpgradeRequired"
  show PreconditionRequired = "PreconditionRequired"
  show TooManyRequests = "TooManyRequests"
  show RequestHeaderFieldsTooLarge = "RequestHeaderFieldsTooLarge"
  show UnavailableForLegalReasons = "UnavailableForLegalReasons"
  show InternalServerError = "InternalServerError"
  show NotImplemented = "NotImplemented"
  show BadGateway = "BadGateway"
  show ServiceUnavailable = "ServiceUnavailable"
  show GatewayTimeout = "GatewayTimeout"
  show HTTPVersionNotSupported = "HTTPVersionNotSupported"
  show VariantAlsoNegotiates = "VariantAlsoNegotiates"
  show InsufficientStorage = "InsufficientStorage"
  show LoopDetected = "LoopDetected"
  show NetworkAuthenticationRequired = "NetworkAuthenticationRequired"
  show (UnknownStatusCode n _) = "Unknown (" <+> show n <+> ")"

export
status_code_to_nat : {n : Nat} -> StatusCode n -> Nat
status_code_to_nat _ = n

export
nat_to_status_code : (n : Nat) -> (prf : StatusCodeNumber n) -> StatusCode n
nat_to_status_code 100 _ = Continue
nat_to_status_code 101 _ = SwitchingProtocols
nat_to_status_code 102 _ = Processing
nat_to_status_code 103 _ = EarlyHints
nat_to_status_code 200 _ = OK
nat_to_status_code 201 _ = Created
nat_to_status_code 202 _ = Accepted
nat_to_status_code 203 _ = NonAuthoritativeInformation
nat_to_status_code 204 _ = NoContent
nat_to_status_code 205 _ = ResetContent
nat_to_status_code 206 _ = PartialContent
nat_to_status_code 207 _ = MultiStatus
nat_to_status_code 208 _ = AlreadyReported
nat_to_status_code 226 _ = IMUsed
nat_to_status_code 300 _ = MultipleChoices
nat_to_status_code 301 _ = MovedPermanently
nat_to_status_code 302 _ = Found
nat_to_status_code 303 _ = SeeOther
nat_to_status_code 304 _ = NotModified
nat_to_status_code 305 _ = UseProxy
nat_to_status_code 307 _ = TemporaryRedirect
nat_to_status_code 308 _ = PermanentRedirect
nat_to_status_code 401 _ = Unauthorized
nat_to_status_code 402 _ = PaymentRequired
nat_to_status_code 403 _ = Forbidden
nat_to_status_code 404 _ = NotFound
nat_to_status_code 405 _ = MethodNotAllowed
nat_to_status_code 406 _ = NotAcceptable
nat_to_status_code 407 _ = ProxyAuthenticationRequired
nat_to_status_code 408 _ = RequestTimeout
nat_to_status_code 409 _ = Conflict
nat_to_status_code 410 _ = Gone
nat_to_status_code 411 _ = LengthRequired
nat_to_status_code 412 _ = PreconditionFailed
nat_to_status_code 413 _ = ContentTooLarge
nat_to_status_code 414 _ = URITooLong
nat_to_status_code 415 _ = UnsupportedMediaType
nat_to_status_code 416 _ = RangeNotSatisfiable
nat_to_status_code 417 _ = ExpectationFailed
nat_to_status_code 421 _ = MisdirectedRequest
nat_to_status_code 422 _ = UnprocessableContent
nat_to_status_code 423 _ = Locked
nat_to_status_code 424 _ = FailedDependency
nat_to_status_code 425 _ = TooEarly
nat_to_status_code 426 _ = UpgradeRequired
nat_to_status_code 428 _ = PreconditionRequired
nat_to_status_code 429 _ = TooManyRequests
nat_to_status_code 431 _ = RequestHeaderFieldsTooLarge
nat_to_status_code 451 _ = UnavailableForLegalReasons
nat_to_status_code 500 _ = InternalServerError
nat_to_status_code 501 _ = NotImplemented
nat_to_status_code 502 _ = BadGateway
nat_to_status_code 503 _ = ServiceUnavailable
nat_to_status_code 504 _ = GatewayTimeout
nat_to_status_code 505 _ = HTTPVersionNotSupported
nat_to_status_code 506 _ = VariantAlsoNegotiates
nat_to_status_code 507 _ = InsufficientStorage
nat_to_status_code 508 _ = LoopDetected
nat_to_status_code 511 _ = NetworkAuthenticationRequired
nat_to_status_code n prf = UnknownStatusCode n prf

export
status_code_class : {n : Nat} -> StatusCode n -> StatusCodeClass
status_code_class code =
  case (status_code_to_nat code) `div` 100 of
    1 => Information
    2 => Successful
    3 => Redirection
    4 => ClientError
    _ => ServerError


text:
module Data.Time.Clock.Internal.POSIXTime

import Data.Time.Clock.Internal.NominalDiffTime

||| 86400 nominal seconds in every day
posixDayLength: NominalDiffTime
posixDayLength = nominalDay

||| POSIX time = Nominal time since 1970-01-01 00:00 UTC

POSIXTime : Type
POSIXTime = NominalDiffTime

max_stars_repo_name: gdevanla/idris-time

max_issues_repo_name: gdevanla/idris-time

max_forks_repo_name: gdevanla/idris-time


text:
module Utils.Either

%default total

export
mapError : (a -> c) -> Either a b -> Either c b
mapError f e = either (Left . f) (Right . id) e

export
partitionEithers : List (Either a b) -> (List a, List b)
partitionEithers [] = ([], [])
partitionEithers (Left x :: es)
        = let (ls, rs) = partitionEithers es in
              (x :: ls, rs)
partitionEithers (Right y :: es)
        = let (ls, rs) = partitionEithers es in
              (ls, y :: rs)


text:
import Common

eitherBool : Iso (Either a a) (a, Bool)
eitherBool = MkIso to from tf ft
  where
    to : (Either a a) -> (a, Bool)
    to (Left x) = (x, False)
    to (Right x) = (x, True)
    from : (a, Bool) -> (Either a a)
    from (x, False) = Left x
    from (x, True) = Right x
    tf (a, False) = Refl
    tf (a, True) = Refl
    ft (Left x) = Refl
    ft (Right x) = Refl

dec : (pc: a -> Type) -> (f : (x: a) -> Dec (pc x)) -> Iso (Sigma a (\x => Dec (pc x))) a
dec pc f = MkIso to from tf ft
  where
    to : (Sigma a (\x => Dec (pc x))) -> a
    to (MkSigma x p) = x
    from : a -> (Sigma a (\x => Dec (pc x)))
    from x = MkSigma x (f x)
    tf x = Refl
    ft (MkSigma x (Yes prf)) with (f x)
      | Yes prf = cong {f=\r => MkSigma x (Yes r)} $ believe_me ()
      | No contra = void $ contra prf
    ft (MkSigma x (No contra)) with (f x)
      | Yes prf = void $ contra prf
      | No contra = cong {f=\r => MkSigma x (No r)} $ believe_me ()

eitherDec : (pc: a -> Type) -> Iso (Sigma a (\x => Dec (pc x))) (Sigma a (\x => (Either (pc x -> Void) (pc x))))
eitherDec pc = MkIso to from tf ft
  where
    to : (Sigma a (\x => Dec (pc x))) -> (Sigma a (\x => (Either (pc x -> Void) (pc x))))
    to (MkSigma x (No contra)) = (x ** Left contra)
    to (MkSigma x (Yes prf)) = (x ** Right prf)
    from : (Sigma a (\x => (Either (pc x -> Void) (pc x)))) -> (Sigma a (\x => Dec (pc x)))
    from (MkSigma x (Left contra)) = (x ** No contra)
    from (MkSigma x (Right prf)) = (x ** Yes prf)
    tf (MkSigma x (Left contra)) = Refl
    tf (MkSigma x (Right prf)) = Refl
    ft (MkSigma x (No contra)) = Refl
    ft (MkSigma x (Yes prf)) = Refl

eitherSigmaDistribLeft : Iso (Sigma a (\x => (Either pa pb)))
                             (Either (Sigma a (\x => pa)) (Sigma a (\x => pb)))
eitherSigmaDistribLeft = MkIso to from tf ft
  where
    to : (Sigma a (\x => (Either pa pb))) -> (Either (Sigma a (\x => pa)) (Sigma a (\x => pb)))
    to (MkSigma x (Left pa)) = Left (MkSigma x pa)
    to (MkSigma x (Right pb)) = Right (MkSigma x pb)
    from : (Either (Sigma a (\x => pa)) (Sigma a (\x => pb))) -> (Sigma a (\x => (Either pa pb)))
    from (Left (MkSigma x pa)) = MkSigma x (Left pa)
    from (Right (MkSigma x pb)) = MkSigma x (Right pb)
    tf (Left (MkSigma x p)) = Refl
    tf (Right (MkSigma x p)) = Refl
    ft (MkSigma x (Left pa)) = Refl
    ft (MkSigma x (Right pb)) = Refl

-- use a to find whether it's b or c next to it
branch : (pc: a -> Type) ->
       ((x: a) -> Dec (pc x)) ->
       Iso b d ->
       Iso c d ->
       Iso (Sigma a (\x => (Either (pc x -> Void, b) (pc x, c)))) (a, d)
branch pc
       f
       (MkIso bdto bdfrom bdtf bdft)
       (MkIso cdto cdfrom cdtf cdft)
       = MkIso to from tf ft
  where
    to : (Sigma a (\x => (Either (pc x -> Void, b) (pc x, c)))) -> (a, d)
    to (MkSigma x (Left (p, y))) = (x, bdto y)
    to (MkSigma x (Right (p, y))) = (x, cdto y)
    from : (a, d) -> (Sigma a (\x => (Either (pc x -> Void, b) (pc x, c))))
    from (x, y) = case (appIso (eitherDec pc) (unappIso (dec pc f) x)) of
      (MkSigma z (Left p)) => MkSigma z $ Left (p, bdfrom y)
      (MkSigma z (Right p)) => MkSigma z $ Right (p, cdfrom y)
    tf (x, y) with (f x)
      | Yes prf = rewrite (cdtf y) in Refl
      | No contra = rewrite (bdtf y) in Refl
    ft (MkSigma x (Left (p, y))) with (f x)
      | Yes prf = void $ p prf
      | No contra = rewrite (bdft y) in cong {f=\r => MkSigma x (Left (r, y))} $ believe_me ()
    ft (MkSigma x (Right (p, y))) with (f x)
      | Yes prf = rewrite (cdft y) in cong {f=\r => MkSigma x (Right (r, y))} $ believe_me ()
      | No contra = void $ contra p

max_stars_repo_name: defanor/morphisms

max_issues_repo_name: defanor/morphisms

max_forks_repo_name: defanor/morphisms


text:
import Js
import Js.Object
import Js.DOM.Document
import Js.DOM.Element
import Js.React.DOM
import Js.React.Element

%default total

hello : String -> JS_IO Js.React.Element.Element
hello = simple (\who => div !(wrap "color" "blue" >>= wrap "style")
                            [Text $ "Hello, " ++ who ++ "!"])

main : JS_IO ()
main = render !(getElement "root")
              !(div !empty
                    [ ChildElement !(hello "Idris")
                    , ChildElement !(hello "Electron")
                    , ChildElement !(hello "React")
                    , Text "... it's working :)"
                    ])

max_stars_repo_name: jheiling/idris-electron-react-scaffold

max_issues_repo_name: jheiling/idris-electron-react-scaffold

max_forks_repo_name: jheiling/idris-electron-react-scaffold


text:
module Data.List.Extra

%default total

||| Fetches the element at a given position.
||| Returns `Nothing` if the position beyond the list's end.
public export
elemAt : List a -> Nat -> Maybe a
elemAt []        _     = Nothing
elemAt (l :: _)  Z     = Just l
elemAt (_ :: ls) (S n) = elemAt ls n


text:
%default total

data Format = Number Format
            | Str Format
            | FChar Format
            | FDouble Format
            | Lit String Format
            | End

%name Format f

PrintfType : Format -> Type
PrintfType (Number f)  = Int    -> PrintfType f
PrintfType (Str f)     = String -> PrintfType f
PrintfType (FChar f)   = Char   -> PrintfType f
PrintfType (FDouble f) = Double -> PrintfType f
PrintfType (Lit str f) =           PrintfType f
PrintfType End         =           String

parseFormatString : List Char -> Format
parseFormatString [] = End
parseFormatString ('%' :: 'd' :: xs) = Number $ parseFormatString xs
parseFormatString ('%' :: 's' :: xs) = Str $ parseFormatString xs
parseFormatString ('%' :: 'c' :: xs) = FChar $ parseFormatString xs
parseFormatString ('%' :: 'f' :: xs) = FDouble $ parseFormatString xs
parseFormatString (x :: xs) = case parseFormatString xs of
                                   (Lit str f) => Lit (strCons x str) f
                                   format => Lit (cast x) format

printFormat : (f : Format) -> (acc : String) -> PrintfType f
printFormat (Number  f) acc = \i      => printFormat f (acc ++ show i     )
printFormat (Str     f) acc = \str    => printFormat f (acc ++ str        )
printFormat (FDouble f) acc = \double => printFormat f (acc ++ show double)
printFormat (FChar   f) acc = \c      => printFormat f (acc ++ cast c     )
printFormat (Lit str f) acc =            printFormat f (acc ++ str        )
printFormat  End        acc =                           acc

printf : (s : String) -> PrintfType (parseFormatString $ unpack s)
printf s with (parseFormatString $ unpack s)
  printf s | format = printFormat format ""

TupleVect : Nat -> Type -> Type
TupleVect Z x = ()
TupleVect (S k) x = (x, TupleVect k x)

test : TupleVect 4 Nat
test = (1,2,3,4,())


text:
module Main

%include C "idrisfs.h"
%link C "idrisfs.o"

getSizeIsize : IO Int
getSizeIsize = foreign FFI_C "sizeof_isize" (IO Int)

main : IO ()
main = do
    x <- getSizeIsize
    putStrLn (show x)

max_stars_repo_name: bvssvni/rust-idris-fs

max_issues_repo_name: bvssvni/rust-idris-fs

max_forks_repo_name: bvssvni/rust-idris-fs


text:
||| Experimenting with shell auto-completion for Idris2
module Main

import IdrisPaths

import Core.Context
import Core.Directory
import Core.Metadata
import Core.Options
import Core.Unify

import Idris.Env
import Idris.Version
import Idris.Package.Types

import Core.Name.Namespace
import Core.Options

import Libraries.Utils.Path
import Libraries.Data.List1 as Lib
import Libraries.System.Directory.Tree
import Data.List1
import Data.Strings
import Data.Maybe
import Data.String
import System
import System.Directory

--------------------------------------------------------------------------------
--          Options
--------------------------------------------------------------------------------

-- These are copied right now, since lots of this stuff is private in
-- Idris.CommandLine
public export
data PkgCommand
      = Build
      | Install
      | MkDoc
      | Typecheck
      | Clean
      | REPL
      | Init

export
Show PkgCommand where
  show Build = "--build"
  show Install = "--install"
  show MkDoc = "--mkdoc"
  show Typecheck = "--typecheck"
  show Clean = "--clean"
  show REPL = "--repl"
  show Init = "--init"

public export
data DirCommand
      = LibDir -- show top level package directory

export
Show DirCommand where
  show LibDir = "--libdir"

||| CLOpt - possible command line options
public export
data CLOpt
  =
   ||| Only typecheck the given file
  CheckOnly |
   ||| The output file from the code generator
  OutputFile String |
   ||| Execute a given function after checking the source file
  ExecFn String |
   ||| Use a specific code generator
  SetCG String |
   ||| Pass a directive to the code generator
  Directive String |
   ||| Don't implicitly import Prelude
  NoPrelude |
   ||| Set source directory
  SourceDir String |
   ||| Set build directory
  BuildDir String |
   ||| Set output directory
  OutputDir String |
   ||| Generate profile data when compiling (backend dependent)
  Profile |
   ||| Show the installation prefix
  ShowPrefix |
   ||| Display Idris version
  Version |
   ||| Display help text
  Help |
   ||| Suppress the banner
  NoBanner |
   ||| Run Idris 2 in quiet mode
  Quiet |
   ||| Run Idris 2 in verbose mode (cancels quiet if it's the default)
  Verbose |
   ||| Set the console width for REPL output
  ConsoleWidth (Maybe Nat) |
   ||| Whether to use color in the console output
  Color Bool |
   ||| Set the log level globally
  Logging LogLevel |
   ||| Add a package as a dependency
  PkgPath String |
   ||| Build or install a given package, depending on PkgCommand
  Package PkgCommand String |
   ||| Show locations of data/library directories
  Directory DirCommand |
   ||| The input Idris file
  InputFile String |
   ||| Whether or not to run in IdeMode (easily parsable for other tools)
  IdeMode |
   ||| Whether or not to run IdeMode (using a socket instead of stdin/stdout)
  IdeModeSocket String |
   ||| Run as a checker for the core language TTImp
  Yaffle String |
   ||| Dump metadata from a .ttm file
  Metadata String |
   ||| Dump cases before compiling
  DumpCases String |
   ||| Dump lambda lifted defs before compiling
  DumpLifted String |
   ||| Dump ANF defs before compiling
  DumpANF String |
   ||| Dump VM code defs before compiling
  DumpVMCode String |
   ||| Run a REPL command then exit immediately
  RunREPL String |
  IgnoreMissingIPKG |
  FindIPKG |
  Timing |
  DebugElabCheck |
  BlodwenPaths

data OptType
  = Required String
   | Optional String
   | RequiredNat String
   | AutoNat String
   | RequiredLogLevel String

Show OptType where
  show (Required a) = "<" ++ a ++ ">"
  show (RequiredNat a) = "<" ++ a ++ ">"
  show (RequiredLogLevel a) = "<" ++ a ++ ">"
  show (Optional a) = "[" ++ a ++ "]"
  show (AutoNat a) = "<" ++ a ++ ">"

ActType : List OptType -> Type
ActType [] = List CLOpt
ActType (Required a :: as) = String -> ActType as
ActType (RequiredNat a :: as) = Nat -> ActType as
ActType (RequiredLogLevel a :: as) = LogLevel -> ActType as
ActType (Optional a :: as) = Maybe String -> ActType as
ActType (AutoNat a :: as) = Maybe Nat -> ActType as

||| Extract the host and port to bind the IDE socket to
export
ideSocketModeAddress : List CLOpt -> (String, Int)
ideSocketModeAddress []  = ("localhost", 38398)
ideSocketModeAddress (IdeModeSocket hp :: _) =
  let (h, p) = Strings.break (== ':') hp
      port = fromMaybe 38398 (portPart p >>= parsePositive)
      host = if h == "" then "localhost" else h
  in (host, port)
  where
    portPart : String -> Maybe String
    portPart p = if p == ""
                    then Nothing
                    else Just $ assert_total $ prim__strTail p
ideSocketModeAddress (_ :: rest) = ideSocketModeAddress rest

formatSocketAddress : (String, Int) -> String
formatSocketAddress (host, port) = host ++ ":" ++ show port

record OptDesc where
  constructor MkOpt
  flags : List String
  argdescs : List OptType
  action : ActType argdescs
  help : Maybe String

optSeparator : OptDesc
optSeparator = MkOpt [] [] [] Nothing

showDefault : Show a => a -> String
showDefault x = "(default " ++ show x ++ ")"

options : List OptDesc
options = [MkOpt ["--check", "-c"] [] [CheckOnly]
              (Just "Exit after checking source file"),
           MkOpt ["--output", "-o"] [Required "file"] (\f => [OutputFile f, Quiet])
              (Just "Specify output file"),
           MkOpt ["--exec", "-x"] [Required "name"] (\f => [ExecFn f, Quiet])
              (Just "Execute function after checking source file"),
           MkOpt ["--no-prelude"] [] [NoPrelude]
              (Just "Don't implicitly import Prelude"),
           MkOpt ["--codegen", "--cg"] [Required "backend"] (\f => [SetCG f])
              (Just $ "Set code generator " ++ showDefault (codegen defaultSession)),
           MkOpt ["--directive"] [Required "directive"] (\d => [Directive d])
              (Just $ "Pass a directive to the current code generator"),
           MkOpt ["--package", "-p"] [Required "package"] (\f => [PkgPath f])
              (Just "Add a package as a dependency"),
           MkOpt ["--source-dir"] [Required "dir"] (\d => [SourceDir d])
              (Just $ "Set source directory"),
           MkOpt ["--build-dir"] [Required "dir"] (\d => [BuildDir d])
              (Just $ "Set build directory"),
           MkOpt ["--output-dir"] [Required "dir"] (\d => [OutputDir d])
              (Just $ "Set output directory"),
           MkOpt ["--profile"] [] [Profile]
              (Just "Generate profile data when compiling, if supported"),

           optSeparator,
           MkOpt ["--prefix"] [] [ShowPrefix]
              (Just "Show installation prefix"),
           MkOpt ["--paths"] [] [BlodwenPaths]
              (Just "Show paths"),
           MkOpt ["--libdir"] [] [Directory LibDir]
              (Just "Show library directory"),

           optSeparator,
           MkOpt ["--init"] [Optional "package file"]
              (\ f => [Package Init (fromMaybe "" f)])
              (Just "Interactively initialise a new project"),

           MkOpt ["--build"] [Required "package file"] (\f => [Package Build f])
              (Just "Build modules/executable for the given package"),
           MkOpt ["--install"] [Required "package file"] (\f => [Package Install f])
              (Just "Install the given package"),
           MkOpt ["--mkdoc"] [Required "package file"] (\f => [Package MkDoc f])
              (Just "Build documentation for the given package"),
           MkOpt ["--typecheck"] [Required "package file"] (\f => [Package Typecheck f])
              (Just "Typechecks the given package without code generation"),
           MkOpt ["--clean"] [Required "package file"] (\f => [Package Clean f])
              (Just "Clean intermediate files/executables for the given package"),
           MkOpt ["--repl"] [Required "package file"] (\f => [Package REPL f])
              (Just "Build the given package and launch a REPL instance."),
           MkOpt ["--find-ipkg"] [] [FindIPKG]
              (Just "Find and use an .ipkg file in a parent directory."),
           MkOpt ["--ignore-missing-ipkg"] [] [IgnoreMissingIPKG]
              (Just "Fail silently if a dependency is missing."),

           optSeparator,
           MkOpt ["--ide-mode"] [] [IdeMode]
              (Just "Run the REPL with machine-readable syntax"),
           MkOpt ["--ide-mode-socket"] [Optional "host:port"]
                 (\hp => [IdeModeSocket $ fromMaybe (formatSocketAddress (ideSocketModeAddress [])) hp])
              (Just $ "Run the ide socket mode on given host and port " ++
                      showDefault (formatSocketAddress (ideSocketModeAddress []))),

           optSeparator,
           MkOpt ["--client"] [Required "REPL command"] (\f => [RunREPL f])
              (Just "Run a REPL command then quit immediately"),
           MkOpt ["--timing"] [] [Timing]
              (Just "Display timing logs"),

           optSeparator,
           MkOpt ["--no-banner"] [] [NoBanner]
              (Just "Suppress the banner"),
           MkOpt ["--quiet", "-q"] [] [Quiet]
              (Just "Quiet mode; display fewer messages"),
           MkOpt ["--console-width"] [AutoNat "console width"] (\l => [ConsoleWidth l])
              (Just "Width for console output (0 for unbounded) (auto by default)"),
           MkOpt ["--color", "--colour"] [] ([Color True])
              (Just "Forces colored console output (enabled by default)"),
           MkOpt ["--no-color", "--no-colour"] [] ([Color False])
              (Just "Disables colored console output"),
           MkOpt ["--verbose"] [] [Verbose]
              (Just "Verbose mode (default)"),
           MkOpt ["--log"] [RequiredLogLevel "log level"] (\l => [Logging l])
              (Just "Global log level (0 by default)"),

           optSeparator,
           MkOpt ["--version", "-v"] [] [Version]
              (Just "Display version string"),
           MkOpt ["--help", "-h", "-?"] [] [Help]
              (Just "Display help text"),

           -- Internal debugging options
           MkOpt ["--yaffle", "--ttimp"] [Required "ttimp file"] (\f => [Yaffle f])
              Nothing, -- run ttimp REPL rather than full Idris
           MkOpt ["--ttm" ] [Required "ttimp file"] (\f => [Metadata f])
              Nothing, -- dump metadata information from the given ttm file
           MkOpt ["--dumpcases"] [Required "output file"] (\f => [DumpCases f])
              Nothing, -- dump case trees to the given file
           MkOpt ["--dumplifted"] [Required "output file"] (\f => [DumpLifted f])
              Nothing, -- dump lambda lifted trees to the given file
           MkOpt ["--dumpanf"] [Required "output file"] (\f => [DumpANF f])
              Nothing, -- dump ANF to the given file
           MkOpt ["--dumpvmcode"] [Required "output file"] (\f => [DumpVMCode f])
              Nothing, -- dump VM Code to the given file
           MkOpt ["--debug-elab-check"] [] [DebugElabCheck]
              Nothing -- do more elaborator checks (currently conversion in LinearCheck)
           ]

--------------------------------------------------------------------------------
--          Context
--------------------------------------------------------------------------------

-- More copy paste
-- Add extra data from the "IDRIS2_x" environment variables
updateEnv : {auto c : Ref Ctxt Defs} ->
            Core ()
updateEnv
    = do defs <- get Ctxt
         bprefix <- coreLift $ idrisGetEnv "IDRIS2_PREFIX"
         the (Core ()) $ case bprefix of
              Just p => setPrefix p
              Nothing => setPrefix yprefix
         bpath <- coreLift $ idrisGetEnv "IDRIS2_PATH"
         the (Core ()) $ case bpath of
              Just path => do traverseList1_ addExtraDir (map trim (split (==pathSeparator) path))
              Nothing => pure ()
         bdata <- coreLift $ idrisGetEnv "IDRIS2_DATA"
         the (Core ()) $ case bdata of
              Just path => do traverseList1_ addDataDir (map trim (split (==pathSeparator) path))
              Nothing => pure ()
         blibs <- coreLift $ idrisGetEnv "IDRIS2_LIBS"
         the (Core ()) $ case blibs of
              Just path => do traverseList1_ addLibDir (map trim (split (==pathSeparator) path))
              Nothing => pure ()
         pdirs <- coreLift $ idrisGetEnv "IDRIS2_PACKAGE_PATH"
         the (Core ()) $ case pdirs of
              Just path => do traverseList1_ addPackageDir (map trim (split (==pathSeparator) path))
              Nothing => pure ()
         cg <- coreLift $ idrisGetEnv "IDRIS2_CG"
         the (Core ()) $ case cg of
              Just e => case getCG (options defs) e of
                             Just cg => setCG cg
                             Nothing => throw (InternalError ("Unknown code generator " ++ show e))
              Nothing => pure ()

         -- IDRIS2_PATH goes first so that it overrides this if there's
         -- any conflicts. In particular, that means that setting IDRIS2_PATH
         -- for the tests means they test the local version not the installed
         -- version
         defs <- get Ctxt
         -- These might fail while bootstrapping
         addDataDir (prefix_dir (dirs (options defs)) </>
                        ("idris2-" ++ showVersion False version) </> "support")
         addLibDir (prefix_dir (dirs (options defs)) </>
                        ("idris2-" ++ showVersion False version) </> "lib")
         Just cwd <- coreLift $ currentDir
              | Nothing => throw (InternalError "Can't get current directory")
         addLibDir cwd

--------------------------------------------------------------------------------
--          Package Names
--------------------------------------------------------------------------------

exploreNonHidden : (root : Path) -> IO (Tree root)
exploreNonHidden r = map (filter notHidden notHidden) $ explore r
  where notHidden : {root : _} -> FileName root -> Bool
        notHidden = not . isPrefixOf "." . fileName

-- List of directory entries at the given path
dirsAt : String -> IO (List String)
dirsAt pth = do MkTree _ ds <- exploreNonHidden (parse pth)
                pure (map (fileName . fst) ds)

-- List of directory entries at the given path
dirsPathsAt : String -> IO (List String)
dirsPathsAt pth = do MkTree _ ds <- exploreNonHidden (parse pth)
                     pure (map (\p => (toFilePath $ fst p) ++ "/") ds)

-- List of file entries at the given path
filesAt : String -> IO (List String)
filesAt pth = do MkTree fs _ <- exploreNonHidden (parse pth)
                 pure (map fileName fs)

-- lots of duplications with functionality in `Idris.SetOptions`. Will have
-- to extract the common parts once this goes to Idris2 itself
export
packageNames : String -> IO (List String)
packageNames dname = map (map (fst . getVersion)) $ dirsAt dname
  where
    toVersion : String -> Maybe PkgVersion
    toVersion = map MkPkgVersion
              . traverse parsePositive
              . split (== '.')

    getVersion : String -> (String, Maybe PkgVersion)
    getVersion str =
      -- Split the dir name into parts concatenated by "-"
      -- treating the last part as the version number
      -- and the initial parts as the package name.
      -- For reasons of backwards compatibility, we also
      -- accept hyphenated directory names without a part
      -- corresponding to a version number.
      case Lib.unsnoc $ split (== '-') str of
        (Nil, last) => (last, Nothing)
        (init,last) =>
          case toVersion last of
            Just v  => (concat $ intersperse "-" init, Just v)
            Nothing => (str, Nothing)

findIpkg : {auto c : Ref Ctxt Defs} -> Core (List String)
findIpkg =
  do Just srcdir <- coreLift currentDir
       | Nothing => throw (InternalError "Can't get current directory")
     fs <- coreLift $ filesAt srcdir
     pure $ filter (".ipkg" `isSuffixOf`) fs

findPackages : {auto c : Ref Ctxt Defs} -> Core (List String)
findPackages =
  do defs <- get Ctxt
     let globaldir = prefix_dir (dirs (options defs)) </>
                           "idris2-" ++ showVersion False version
     let depends = depends_dir (dirs (options defs))
     Just srcdir <- coreLift currentDir
         | Nothing => throw (InternalError "Can't get current directory")
     let localdir = srcdir </> depends

     -- Get candidate directories from the global install location,
     -- and the local package directory
     locFiles <- coreLift $ packageNames localdir
     globFiles <- coreLift $ packageNames globaldir
     pure $ locFiles ++ globFiles

--------------------------------------------------------------------------------
--          Options
--------------------------------------------------------------------------------

sortedNub : Ord a => List a -> List a
sortedNub = nub . sort
  where nub : List a -> List a
        nub (a :: t@(b :: _)) = if a == b then nub t else a :: nub t
        nub xs                = xs

prefixOnly : String -> List String -> List String
prefixOnly x = sortedNub . filter (\s => x /= s && isPrefixOf x s)

prefixOnlyIfNonEmpty : String -> List String -> List String
prefixOnlyIfNonEmpty "--" = id
prefixOnlyIfNonEmpty s    = prefixOnly s

optStrings : List String
optStrings = options >>= flags

codegens : {auto c : Ref Ctxt Defs} -> Core (List String)
codegens = map fst . availableCGs . options <$> get Ctxt

logLevels : List String
logLevels = map show $ [0 .. 10]

opts : {auto c : Ref Ctxt Defs} -> (String,String) -> Core (List String)
opts ("--","idris2") = pure optStrings

-- codegens
opts (x, "--cg")      = prefixOnlyIfNonEmpty x <$> codegens
opts (x, "--codegen") = prefixOnlyIfNonEmpty x <$> codegens

-- packages
opts (x, "-p")        = prefixOnlyIfNonEmpty x  <$> findPackages
opts (x, "--package") = prefixOnlyIfNonEmpty x  <$> findPackages

-- logging
opts (x, "--log")     = pure $ prefixOnlyIfNonEmpty x logLevels

-- with directories
opts ("--", "-o")           = pure []
opts ("--", "--output")     = pure []
opts ("--", "--source-dir") = pure []
opts ("--", "--build-dir")  = pure []
opts ("--", "--output-dir") = pure []

-- with package files
opts (x, "--build")     = prefixOnlyIfNonEmpty x <$> findIpkg
opts (x, "--install")   = prefixOnlyIfNonEmpty x <$> findIpkg
opts (x, "--mkdoc")     = prefixOnlyIfNonEmpty x <$> findIpkg
opts (x, "--typecheck") = prefixOnlyIfNonEmpty x <$> findIpkg
opts (x, "--clean")     = prefixOnlyIfNonEmpty x <$> findIpkg
opts (x, "--repl")      = prefixOnlyIfNonEmpty x <$> findIpkg

-- options
opts (x,_) = pure $ if (x `elem` optStrings)
                       then Nil
                       else prefixOnly x  optStrings

--------------------------------------------------------------------------------
--          Main
--------------------------------------------------------------------------------

-- Parts of stMain from Idris.Driver
stMain : (String,String) -> Core (List String)
stMain ss = do defs <- initDefs
               c <- newRef Ctxt defs
               setWorkingDir "."
               updateEnv
               opts ss

main : IO ()
main = do [_,a,b] <- getArgs
            | _ => pure ()
          opts <- coreRun (stMain (a,b)) (\_ => pure []) pure
          putStr $ unlines opts


text:
main : IO ()
main = do
    x <- getLine
    putStrLn x


text:
module Primitives

import Data.Vect
import ProcessLib
import Proto

%default total

||| Takes a pure function and returns a process that depends on a slot
||| This process will wait for another process to register to its output
||| Then it will tranform messages according to the pure function.
mkPure': (Show a, Show b) => (name: String) -> (f: a -> b) -> Slot b -> Hom [Down a] [Down b]
mkPure' name f EmptySlot = do Just msg <- Respond (\msg => Pure (fst (handleInitMsg msg))) | _ => Loop (mkPure' name f EmptySlot)
                              Loop $ mkPure' name f (snd (handleInitMsg msg))
  where
    handleInitMsg: (msg : Req (MkNiche [Down a] [Down b])) ->
                   ( ProcIF (MkNiche [Down a] [Down b]) msg
                   , Slot b )
    handleInitMsg (Conn (BotOutWire Here) pid targetInWire) = ( ConnAccepted, FullSlot pid targetInWire )
    handleInitMsg (Val _ _)                                 = ( Error       , EmptySlot                 )
    handleInitMsg (Conn (BotOutWire (There _)) _ _)         impossible
    handleInitMsg (Conn (TopOutWire (There _)) _ _)         impossible
mkPure' name f {a} {b} fs@(FullSlot pid tar) = do --Action $ putStrLn $ name ++ "normal loop"
                                                  Just msg <- Respond (\msg => Pure (normal msg)) | _ => Loop (mkPure' name f fs)
                                                  forward msg
                                                  Loop (mkPure' name f fs)
  where
    forward: Req (MkNiche [Down a] [Down b]) -> Process (ProcIF (MkNiche [Down a] [Down b])) () Sent Sent
    forward (Conn _ _ _) = Pure ()
    forward (Val (TopInWire Here) x) = do Request pid (Val tar (f x))
                                          Action $ putStrLn $ name ++ show x ++ " -->-- " ++ show (f x)
    forward (Val (TopInWire (There l)) _) = absurd l
    forward (Val (BotInWire (There l)) _) = absurd l

    normal: (msg : Req (MkNiche [Down a] [Down b])) -> ProcIF (MkNiche [Down a] [Down b]) msg
    normal (Conn _ _ _)                  = Taken
    normal (Val (TopInWire Here) _)      = Accepted
    normal (Val (TopInWire (There l)) _) = absurd l
    normal (Val (BotInWire (There l)) _) = absurd l

export mkPure: (Show a, Show b) => (name: String) -> (f: a -> b) -> Hom [Down a] [Down b]
mkPure name f = mkPure' name f EmptySlot

||| A service wich prints integers to the console
export downPrinter: Hom [Down Int] []
downPrinter = do Respond resp
                 Loop downPrinter
  where resp: (msg : Req (MkNiche [Down Int] [])) -> Process (ProcIF (MkNiche [Down Int] [])) (ProcIF (MkNiche [Down Int] []) msg) Ready Ready
        resp (Conn _ _ _) = do Action $ putStrLn "ERROR: printer got connection request"
                               Pure Taken
        resp (Val (TopInWire Here) i) = do Action $ putStrLn $ "Hello this is IntPrinter, here is your Int: " ++ show i
                                           Pure Accepted
        resp (Val (TopInWire (There _)) _) impossible
        resp (Val (BotInWire Here) _)      impossible
        resp (Val (BotInWire (There _)) _) impossible

export upPrinter: Hom [] [Up Int]
upPrinter = do Respond resp
               Loop upPrinter
  where
    resp: (msg : Req (MkNiche [] [Up Int])) -> SubProc (MkNiche [] [Up Int]) (ProcIF (MkNiche [] [Up Int]) msg)
    resp (Conn _ _ _) = do Action $ putStrLn "ERROR: printer got conn req"
                           Pure Taken
    resp (Val (BotInWire Here) i) = do Action $ putStrLn $ "upPrinter: " ++ show i
                                       Pure Accepted
    resp (Val (BotInWire (There later)) x) impossible
    resp (Val (TopInWire Here) _) impossible
    resp (Val (TopInWire (There _)) _) impossible

-- downTick': Slot () -> Hom [] [Down ()]
-- downTick' EmptySlot = ?oo_1
-- downTick' s@(FullSlot pid tar) = do Respond (\msg => Pure Error)
--                                     Loop (downTick' s)

max_stars_repo_name: jameshaydon/smproc

max_issues_repo_name: jameshaydon/smproc

max_forks_repo_name: jameshaydon/smproc


text:
module Service
%default total

||| Placeholder description of a smart contract
public export
data Contract : IO t -> Type -> Type where
     MkContract : (a : IO b) -> Contract a b

public export
trustContract : Contract a b -> b
-- This definition left blank for now, but in the future
-- it should provide proof of the existence of a smart contract

||| Abstract Syntax Tree for the Service DSL
public export
data Service : Type -> Type where
     ||| A Service that is definitely of type `a`
     Val     : a -> Service a
     ||| A contract has promised a reward if `a` is not a Service b
     Promise : Contract a b ->  Service b
     ||| Application of a Service to another Service
     App     : Service (a -> b) -> Service a -> Service b
     ||| Explicitly construct a Service using monadic binding
     Bind    : Service a -> (a -> Service b) -> Service b

public export
Functor Service where
        map f (Val a) = Val $ f a
        map f (Promise c) = Val $ f $ trustContract c  --TODO It might be better to never allow Vals to be made from Promises
        map f s = App (Val f) s

public export
Applicative Service where
            pure = Val
            (<*>) = App

public export
Monad Service where
      (>>=) = Bind
      join m = !m

||| Execute an entire service in an IO context
public export
execute : Service a -> IO a
execute (Val x) = pure x
execute (Promise (MkContract c)) = c
execute (App sf sx) = do
                        f <- execute sf
                        x <- execute sx
                        pure $ f x
execute (Bind sx f) = do
                        x <- execute sx
                        execute $ f x

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 Syntax

-- Gettin used to idris's syntax and type system
--
-- Those that are same as haskell are omitted, complicated syntax (like with)
-- are played in other files

-- all top-level functions/variables' types must be explicitly declared
foo : String
foo = "hello"

-- String in idris are not List Char, but rather packed Text as in haskell
bar : List Char
bar = unpack foo

-- Nat is unbound integer within [0,inf), inductively defined
data Nat' : Type where
  Z' : Nat'
  S' : Nat' -> Nat'

-- One can either use the GADT style to define a data, or simply:
data Nat'' = Z'' | S'' Nat''

replicate1 : Nat -> List Nat
replicate1 Z = []
-- replicate1 0 = Nil       -- the same
replicate1 (S k) = 1 :: replicate1 k
-- here the value 1's type is automatically set to Nat because it knows it's
-- constructing a list of Nat

-- [] is the syntatic sugar for Nil. [1,2,3] is for 1::2::3::Nil

-- idris allows overloading functions over argument types, as long as there is
-- they are defined in different namespaces,
--
-- the compiler will figure out which definition to use automatically when
-- calling with arguments with different types

-- finite set captures the idea of matching Nat that are less than or equal to a
-- given Nat.
data Fin' : Nat -> Type where
  FZ' : Fin' (S k)
  FS' : Fin' k -> Fin' (S k)

-- typeclass in haskell ~= interfaces in idris, the instance implementation
-- syntax is slightly different:

Show Nat' where
  show Z' = "Z"
  show (S' n) = "S (" ++ show n ++ ")"

-- idris doesn't have things like Constraint at the kind level. Interfaces (or
-- typeclass in haskell) are implemented as partial functions. i.e. unsatisfied
-- types are not implemented.
--
-- example with Show : Type -> Type, where Show Nat : Type is implemented and
-- Show (Nat -> Nat) : Type is not implemented (doesn't have a proof).

-- more sensible Functor/Applicative/Monad interfaces
--
-- Functor has `map' instead of `fmap' as its implementation
--
-- Applicative has `pure' and `<*>', same as Haskell
--
-- Monad has `>>=', `return' is not needed, since we already got `pure'

-- do notation works as in haskell. Monad comprehension as well. Monad
-- comprehension requires (Monad m, Alternative m) (for use of guard).
-- Alternative is the same as in haskell.

-- Multiple implementations for the same type with a interface is allowed.
--
-- e.g. Nat can be a Semigroup in two ways: additive and multiplicative
--
-- This is achieved by named impl, where a name is used when defining

[SemiNatMult] Semigroup Nat where
  (<+>) m n = m * n

[SemiNatAdd] Semigroup Nat where
  (<+>) m n = m + n

-- dependent implementation can be achieved with the 'using' syntax
[MonoidNatMult] Monoid Nat using SemiNatMult where
  neutral = 1
[MonoidNatAdd]  Monoid Nat using SemiNatAdd  where
  neutral = 0

-- !-notation makes writing monadic code easier:
--
--

m_add : Maybe Int -> Maybe Int -> Maybe Int
-- without !-notation
-- m_add x y = do x' <- x
--                y' <- y
--                pure (x + y)
-- with !-notation
m_add x y = pure (!x + !y)

-- ! can be thought of like a prefix function with this type:
--
-- (!) : m a -> a

-- Another convenient syntax is the idiom bracket. idiom bracket makes writing
-- Applicative code cleaner:

m_add' : Maybe Int -> Maybe Int -> Maybe Int
-- without idiom bracket:
-- m_add' x y = pure (+) <*> x <*> y
-- with idiom bracket:
m_add' x y = [| x + y |]

-- idris values are by default strict, Lazy values must be declared explicitly.
--
-- Lazy : Type -> Type

my_if : Bool -> Lazy a -> Lazy a -> a
my_if b x y = if b then x else y

-- when we acquire a value of 'a' where we have a 'Lazy a', it will
-- automatically be evaluated.
--
-- similarly, when we acquire a 'Lazy a' where we have an 'a'-typed expr, the
-- expr will be converted into a unresolved lazy value of type 'Lazy a'

-- function definitions are evaluated in the order they are defined therefore
-- you cannot write plain functions depending on each other directly (you can
-- define recursive function with no problem, though). 'mutual' syntax can be
-- used in this situation, in a 'mutual' block, first the type declarations are
-- added, then the function definitions.

fact' : Nat -> Nat
fact' Z = 1
fact' (S n) = (S n) * fact' n

mutual
  even : Nat -> Bool
  even Z = True
  even (S k) = odd k

  odd : Nat -> Bool
  odd Z = False
  odd (S k) = even k

-- infinte data structure are called co-data types.
--
-- codata-types will gets translated into same as a kind of 'Lazy' data types
namespace StreamCodata
  codata Stream' : Type -> Type where
    (::) : (e : a) -> Stream' a -> Stream' a

-- is the same as

namespace StreamInfData
  data Stream'' : Type -> Type where
    (::) : (e : a) -> Inf (Stream'' a) -> Stream'' a

-- since (::) cannot be defined twice under the same namespace, so here we
-- define them under two namespaces. They can be used without distinguishing
-- explicitly since they differ by the type of the second argument.

-- Inf is mostly the same as Lazy except some nauce differences on their effects
-- on totality.

-- just as a canonical example of typical dependent-type language, there's a
-- built-in Vect data structure is the list parametrized with its length.
-- Defined as below:

data Vect' : (n : Nat) -> a -> Type where
  Nil  : Vect' 0 a
  (::) : a -> Vect' n a -> Vect' (S n) a

-- Tuple syntax (a,b), as both type and value, is a syntatic sugar again.
-- (a, b) as a type is Pair a b; (a, b) as a value is MkPair a b

-- There's another interesting data structure called DPair (Dependent Pair). Defined as:

data DPair' : (a : Type) -> (P : a -> Type) -> Type where
  MkDPair' : {P : a -> Type} -> (x : a) -> P x -> DPair' a P

-- where the second element is a value whose type depends on the value of the
-- first argument. In type theory this type is referred to as `Sigma types'.
--
-- There's, again, a syntatic sugar for DPair: (a:A ** p) stands for MkDPair a p

vec : (n : Nat ** Vect' n Int)
vec = (_ ** [1,2])
-- we can write `_' in place of values which the typechecker can infer
-- automatically.

vec' : DPair Nat (\n => Vect' n Int)
vec' = MkDPair _ [3,4]
-- the same, desugared version.

max_stars_repo_name: shouya/thinking-dumps

max_issues_repo_name: shouya/thinking-dumps

max_forks_repo_name: shouya/thinking-dumps


text:
module Triple

%default total
%access public export
%language LinearTypes

data Triple : (A : Type) -> (B : Type) -> (C : Type) -> Type where
  MkTriple : {A, B, C : Type} ->
             (1 a : A) -> (1 b : B) -> (1 c : C) ->
             Triple A B C

fst3 : (a,b,c) -> a
fst3 (x, y, z) = x

snd3 : (a,b,c) -> b
snd3 (x, y, z) = y

trd3 : (a,b,c) -> c
trd3 (x, y, z) = z

||| Dependent Triple 1
||| Type of A -> (B -> C)
||| Dual to DTriple 2
data DTriple1 : (a : Type) -> (b : a -> Type) ->
                (c : a -> (Type -> Type)) -> Type where
  MkDPair1 : {c : a -> (Type -> Type)} -> {b : a -> Type} ->
             (1 af : a) -> (1 bf : b af) -> (1 cf: (c af) (b af)) ->
             DTriple1 a b c

||| Dependent Triple 2
||| Type of (A -> B) -> C
||| Dual to DTriple 1
data DTriple2 : (a : Type) -> (b : a -> Type) ->
                (c : (a -> Type) -> Type) -> Type where
  MkDPair2 : {c : (a -> Type) -> Type} -> {b : a -> Type} ->
             (1 af : a) -> (1 bf : b af) -> (1 cf: c b) ->
             DTriple2 a b c

max_stars_repo_name: lemastero/Idris-Trifunctors

max_issues_repo_name: lemastero/Idris-Trifunctors

max_forks_repo_name: lemastero/Idris-Trifunctors


text:
module Data.SOP

import public Data.SOP.Interfaces
import public Data.SOP.NP
import public Data.SOP.NS
import public Data.SOP.POP
import public Data.SOP.SOP
import public Data.SOP.Utils

%default total


text:
module IR.Event

import IR.Lens

KeyCode : Type
KeyCode = Int

record Key : Type where
  MkKey : (keyCode : KeyCode) ->
          (keyHasAlt : Bool) ->
          (keyHasCmd : Bool) ->
          (keyHasCtrl : Bool) ->
          (keyHasShift : Bool) ->
          Key

instance Eq Key where
  (==) (MkKey a b c d e) (MkKey a' b' c' d' e') = a == a' && b == b' && c == c' && d == d' && e == e'

-- Should be the Monoid instance:
infixl 3 <!>
(<!>) : Ordering -> Ordering -> Ordering
(<!>) EQ r = r
(<!>) l  r = l

-- Should be the Ord instance:
compareBool : Bool -> Bool -> Ordering
compareBool False False = EQ
compareBool False True = LT
compareBool True False = GT
compareBool True True = EQ

instance Ord Key where
  compare (MkKey a b c d e) (MkKey a' b' c' d' e') = compare a a'
                                                 <!> compareBool b b'
                                                 <!> compareBool c c'
                                                 <!> compareBool d d'
                                                 <!> compareBool e e'

keyCode' : Lens Key KeyCode
keyCode' = lens (\(MkKey x _ _ _ _) => x) (\x, (MkKey _ a b c d) => MkKey x a b c d)

keyHasAlt' : Lens Key Bool
keyHasAlt' = lens (\(MkKey _ x _ _ _) => x) (\x, (MkKey a _ b c d) => MkKey a x b c d)

keyHasCmd' : Lens Key Bool
keyHasCmd' = lens (\(MkKey _ _ x _ _) => x) (\x, (MkKey a b _ c d) => MkKey a b x c d)

keyHasCtrl' : Lens Key Bool
keyHasCtrl' = lens (\(MkKey _ _ _ x _) => x) (\x, (MkKey a b c _ d) => MkKey a b c x d)

keyHasShift' : Lens Key Bool
keyHasShift' = lens (\(MkKey _ _ _ _ x) => x) (\x, (MkKey a b c d _) => MkKey a b c d x)

data Event = KeyEvent Key
           | RefreshEvent
           | IgnoredEvent

eventFromPtr : Ptr -> IO Event
eventFromPtr p = do
  t <- mkForeign (FFun "irEventType" [FPtr] FInt) p
  c <- mkForeign (FFun "irEventKeyCode" [FPtr] FInt) p
  alt <- map (/= 0) (mkForeign (FFun "irEventKeyAlternate" [FPtr] FInt) p)
  cmd <- map (/= 0) (mkForeign (FFun "irEventKeyCommand" [FPtr] FInt) p)
  ctrl <- map (/= 0) (mkForeign (FFun "irEventKeyControl" [FPtr] FInt) p)
  shift <- map (/= 0) (mkForeign (FFun "irEventKeyShift" [FPtr] FInt) p)
  mkForeign (FFun "irEventFree" [FPtr] FUnit) p
  return (case t of
    0 => KeyEvent (MkKey c alt cmd ctrl shift)
    1 => RefreshEvent
    _ => IgnoredEvent)

max_stars_repo_name: puffnfresh/iridium

max_issues_repo_name: victoredwardocallaghan/iridium

max_forks_repo_name: victoredwardocallaghan/iridium


text:
data Id : Type where
    MkId : Nat -> Id

beq_id : (x1, x2 : Id) -> Bool
beq_id (MkId n1) (MkId n2) = n1 == n2

beq_id_refl : (x : Id) -> True = beq_id x x
beq_id_refl (MkId Z) = Refl
beq_id_refl (MkId (S k)) = rewrite beq_id_refl (MkId k) in Refl

data PartialMap : Type where
    Empty : PartialMap
    Record : Id -> Nat -> PartialMap -> PartialMap

update : (d : PartialMap) -> (x : Id) -> (value : Nat) -> PartialMap
update d x value = Record x value d

find : (x : Id) -> (d : PartialMap) -> Maybe Nat
find x Empty = Nothing
find x (Record y v d') =
    if beq_id x y
        then Just v
        else find x d'

update_eq : (d : PartialMap) -> (x : Id) -> (v : Nat) -> find x (update d x v) = Just v
update_eq d x v = rewrite sym $ beq_id_refl x in Refl

update_neq : (d : PartialMap) -> (x, y : Id) -> (o : Nat) -> beq_id x y = False -> find x (update d y o) = find x d
update_neq d x y o prf = rewrite prf in Refl

data Baz : Type where
    Baz1 : Baz -> Baz
    Baz2 : Baz -> Bool -> Baz


text:
import Control.Monad.Identity

%default total

-- Validated - an Either with a monoidal error --

public export
data Validated e a = Valid a | Invalid e

public export
(Eq e, Eq a) => Eq (Validated e a) where
  Valid x   == Valid y   = x == y
  Invalid e == Invalid f = e == f
  _ == _ = False

export
(Show e, Show a) => Show (Validated e a) where
  showPrec d $ Valid   x = showCon d "Valid" $ showArg x
  showPrec d $ Invalid e = showCon d "Invalid" $ showArg e

public export
Functor (Validated e) where
  map f $ Valid x   = Valid $ f x
  map _ $ Invalid e = Invalid e

public export
Bifunctor Validated where
  bimap _ s $ Valid x   = Valid   $ s x
  bimap f _ $ Invalid e = Invalid $ f e

-- Composition preserves invalidity
public export
Semigroup e => Applicative (Validated e) where
  pure = Valid

  Valid f    <*> Valid x    = Valid $ f x
  Invalid e1 <*> Invalid e2 = Invalid $ e1 <+> e2
  Invalid e  <*> Valid _    = Invalid e
  Valid _    <*> Invalid e  = Invalid e

-- Composition preserves validity
public export
Semigroup e => Semigroup (Validated e a) where
  l@(Valid _) <+> _           = l
  _           <+> r@(Valid _) = r
  Invalid e1  <+> Invalid e2  = Invalid $ e1 <+> e2

public export
Monoid e => Monoid (Validated e a) where
  neutral = Invalid neutral

-- Composition preserves validity
public export
Monoid e => Alternative (Validated e) where
  empty = neutral
  (<|>) = (<+>)

public export
Foldable (Validated e) where
  foldr op init $ Valid x   = x `op` init
  foldr _  init $ Invalid _ = init

  foldl op init $ Valid x   = init `op` x
  foldl _  init $ Invalid _ = init

  null $ Valid _   = False
  null $ Invalid _ = True

public export
Traversable (Validated e) where
  traverse f $ Valid x   = Valid <$> f x
  traverse _ $ Invalid e = pure $ Invalid e

public export %inline
ValidatedL : Type -> Type -> Type
ValidatedL e a = Validated (List e) a

public export %inline
oneInvalid : e -> Applicative f => Validated (f e) a
oneInvalid x = Invalid $ pure x

public export %inline
fromEither : Either e a -> Validated e a
fromEither $ Right x = Valid x
fromEither $ Left  e = Invalid e

public export %inline
fromEitherL : Either e a -> ValidatedL e a
fromEitherL $ Right x = Valid x
fromEitherL $ Left  e = oneInvalid e

public export %inline
toEither : Validated e a -> Either e a
toEither $ Valid   x = Right x
toEither $ Invalid e = Left e

-- Errorful monadic functions --

f1 : Monad m => Int -> m $ ValidatedL String Int
f1 5 = pure $ pure 0
f1 _ = pure $ oneInvalid "fail 1"

f2 : Monad m => Int -> m $ ValidatedL String Int
f2 6 = pure $ pure 0
f2 _ = pure $ oneInvalid "fail 2"

-- Compositions --

c1 : Monad m => m (ValidatedL String Int)
c1 = f1 1 *> f2 1

c2 : Monad m => m (ValidatedL String Int)
c2 = (f1 1 *> f2 1) @{Applicative.Compose}

-- These checks are meant to be true --

r1 : Bool
r1 = runIdentity c1 == Invalid ["fail 2"]

r2 : Bool
r2 = runIdentity c2 == Invalid ["fail 1", "fail 2"]


text:
module Hedgehog.Internal.Range

import Data.Bounded
import Data.Maybe
import Data.Fin
import Decidable.Equality

import Hedgehog.Internal.Util

%hide Prelude.Range

public export
MaxSizeNat : Nat
MaxSizeNat = 100

||| A wrapper of a natural number plus an erased proof that
||| the value is within its bounds.
|||
||| Unlike the original Hedgehog, we allow values in the range [0,100]
||| treating size as a proper percentage.
public export
record Size where
  constructor MkSize
  size     : Nat
  0 sizeOk : size <= MaxSizeNat = True

public export
mkSize : (n : Nat) -> {auto 0 ok : n <= MaxSizeNat = True} -> Size
mkSize n = MkSize n ok

public export
minSize : Size
minSize = mkSize 0

public export
maxSize : Size
maxSize = mkSize MaxSizeNat

export
mkSizeMay : Nat -> Maybe Size
mkSizeMay n with (decEq (n <= MaxSizeNat) True)
  mkSizeMay n | Yes _ = Just $ mkSize n
  mkSizeMay n | No  c = Nothing

export
mkSizeOrZero : Nat -> Size
mkSizeOrZero = fromMaybe minSize . mkSizeMay

export
mkSizeOrMax : Nat -> Size
mkSizeOrMax = fromMaybe maxSize . mkSizeMay

public export
resize : (Nat -> Nat) -> Size -> Size
resize f s = mkSizeOrMax (f s.size)

--------------------------------------------------------------------------------
--          Interface Implementations
--------------------------------------------------------------------------------

export
Show Size where
  showPrec p (MkSize n _) = showPrec p n

export
Eq Size where
  (==) = (==) `on` size

export
Ord Size where
  compare = compare `on` size

export
MinBound Size where
  minBound = minSize

export
MaxBound Size where
  maxBound = maxSize

export
Num Size where
  a + b = mkSizeOrMax $ size a + size b
  a * b = mkSizeOrMax $ size a * size b
  fromInteger = mkSizeOrMax . fromInteger

public export
ToInteger Size where toInteger = toInteger . size

--------------------------------------------------------------------------------
--          Range
--------------------------------------------------------------------------------

public export
record Range a where
  constructor MkRange
  origin  : a
  bounds' : Size -> (a,a)

export
bounds : Size -> Range a -> (a,a)
bounds s r = r.bounds' s

||| Get the lower bound of a range for the given size.
export
lowerBound : Ord a => Size -> Range a -> a
lowerBound sz = uncurry min . bounds sz

||| Get the lower bound of a range for the given size.
export
upperBound : Ord a => Size -> Range a -> a
upperBound sz = uncurry max . bounds sz

export
Functor Range where
  map f (MkRange origin bounds') =
    MkRange (f origin) $
            \si => let (x,y) = bounds' si
                    in (f x, f y)

--------------------------------------------------------------------------------
--          Constant Ranges
--------------------------------------------------------------------------------

||| Construct a range which represents a constant single value.
|||
||| >>> bounds x $ singleton 5
||| (5,5)
|||
||| >>> origin $ singleton 5
||| 5
export
singleton : a -> Range a
singleton x = MkRange x $ \_ => (x, x)

||| Construct a range which is unaffected by the size parameter with a origin
||| point which may differ from the bounds.
|||
||| A range from @-10@ to @10@, with the origin at @0@:
|||
||| >>> bounds x $ constantFrom 0 (-10) 10
||| (-10,10)
|||
||| >>> origin $ constantFrom 0 (-10) 10
||| 0
|||
||| A range from @1970@ to @2100@, with the origin at @2000@:
|||
||| >>> bounds x $ constantFrom 2000 1970 2100
||| (1970,2100)
|||
||| >>> origin $ constantFrom 2000 1970 2100
||| 2000
export
constantFrom : (origin,lower,upper : a) -> Range a
constantFrom o l u = MkRange o $ \_ => (l, u)

||| Construct a range which is unaffected by the size parameter.
|||
||| A range from @0@ to @10@, with the origin at @0@:
|||
||| >>> bounds x $ constant 0 10
||| (0,10)
|||
||| >>> origin $ constant 0 10
||| 0
|||
export
constant : a -> a -> Range a
constant x y = constantFrom x x y

||| Construct a range which is unaffected by the size parameter using the full
||| range of a data type.
|||
||| A range from @-128@ to @127@, with the origin at @0@:
|||
||| >>> bounds x (constantBounded :: Range Int8)
||| (-128,127)
|||
||| >>> origin (constantBounded :: Range Int8)
||| 0
export
constantBounded : (MinBound a, MaxBound a, Num a) => Range a
constantBounded = constantFrom 0 minBound maxBound

--------------------------------------------------------------------------------
--          Linear Ranges
--------------------------------------------------------------------------------

||| Truncate a value so it stays within some range.
|||
||| >>> clamp 5 10 15
||| 10
|||
||| >>> clamp 5 10 0
||| 5
export
clamp : Ord a => (lower,upper,val : a) -> a
clamp l u v = if l > u then min l (max u v)
                       else min u (max l v)

||| Scales an integral value linearly with the size parameter.
export
scaleLinear : ToInteger a => Size -> (origin,bound : a) -> a
scaleLinear sz o0 b0 =
  let o    = toInteger o0
      b    = toInteger b0
      rng  = b - o
      diff = (rng * toInteger sz) `safeDiv` 100
   in fromInteger $ o + diff

||| Scales a fractional value linearly with the size parameter.
export
scaleLinearFrac :  (Neg a, Fractional a) => Size -> (origin,bound : a) -> a
scaleLinearFrac sz o b =
  let diff = (b - o) * (fromIntegral sz / 100)
   in o + diff

export %inline
scaled :  Ord a
       => (scale : Size -> (origin,bound : a) -> a)
       -> (origin,lower,upper : a)
       -> Range a
scaled f o l u = MkRange o $ \sz => let x_sized = clamp l u $ f sz o l
                                        y_sized = clamp l u $ f sz o u
                                     in (x_sized, y_sized)

||| Construct a range which scales the bounds relative to the size parameter.
|||
||| >>> bounds 0 $ linearFrom 0 (-10) 10
||| (0,0)
|||
||| >>> bounds 50 $ linearFrom 0 (-10) 20
||| (-5,10)
|||
||| >>> bounds 100 $ linearFrom 0 (-10) 20
||| (-10,20)
export
linearFrom : Ord a => ToInteger a => (origin,lower,upper : a) -> Range a
linearFrom = scaled scaleLinear

export
linear : Ord a => ToInteger a => (origin,upper : a) -> Range a
linear origin upper = linearFrom origin origin upper

export
linearFin : (n : Nat) -> Range (Fin $ S n)
linearFin n = map toFin $ linearFrom 0 0 (natToInteger n)
  where toFin : Integer -> Fin (S n)
        toFin k = fromMaybe FZ (integerToFin k (S n))

||| Construct a range which scales the bounds relative to the size parameter.
|||
||| This works the same as 'linearFrom', but for fractional values.
export
linearFracFrom :  (Neg a, Ord a, Fractional a)
               => (origin,lower,uppder : a) -> Range a
linearFracFrom = scaled scaleLinearFrac

||| Construct a range which is scaled relative to the size parameter and uses
||| the full range of a data type.
|||
||| >>> bounds 0 (linearBounded :: Range Int8)
||| (0,0)
|||
||| >>> bounds 50 (linearBounded :: Range Int8)
||| (-64,64)
|||
||| >>> bounds 99 (linearBounded :: Range Int8)
|||   (-128,127)
export
linearBounded :  (MinBound a, MaxBound a, Ord a, ToInteger a) => Range a
linearBounded = linearFrom minBound minBound maxBound

--------------------------------------------------------------------------------
--          Exponential Ranges
--------------------------------------------------------------------------------

EulerMinus1 : Double
EulerMinus1 = euler - 1

||| Scale a floating-point number exponentially with the size parameter.
|||
||| Note : This scales the difference between the two values exponentially.
export
scaleExponentialDouble : Size -> (origin,bound : Double) -> Double
scaleExponentialDouble sz o b =
  let e     = fromIntegral sz / 100.0
      delta = b - o
      diff  = pow (abs delta + 1) e - 1
   in o + diff * signum delta

||| Scale an integral exponentially with the size parameter.
export
scaleExponential : ToInteger a => Size -> (origin,bound : a) -> a
scaleExponential sz o b =
  round (scaleExponentialDouble sz (fromIntegral o) (fromIntegral b))

export
exponentialDoubleFrom : (origin,lower,upper : Double) -> Range Double
exponentialDoubleFrom = scaled scaleExponentialDouble

export
exponentialDouble : (lower,upper : Double) -> Range Double
exponentialDouble l u = exponentialDoubleFrom l l u

export
exponentialFrom : Ord a => ToInteger a => (origin,lower,upper : a) -> Range a
exponentialFrom = scaled scaleExponential

export
exponential : Ord a => ToInteger a => (lower,upper : a) -> Range a
exponential l u = exponentialFrom l l u

export
exponentialFin : (n : Nat) -> Range (Fin $ S n)
exponentialFin n = map toFin $ exponentialFrom 0 0 (natToInteger n)
  where toFin : Integer -> Fin (S n)
        toFin k = fromMaybe FZ (integerToFin k (S n))

--------------------------------------------------------------------------------
--          Tests and Proofs
--------------------------------------------------------------------------------

singletonOriginId : origin (singleton x) = x
singletonOriginId = Refl

singletonBoundsId : bounds s (singleton x) = (x,x)
singletonBoundsId = Refl

constantFromOrigin : origin (constantFrom o l u) = o
constantFromOrigin = Refl

constantFromBounds : bounds s (constantFrom o l u) = (l,u)
constantFromBounds = Refl

constantOrigin : origin (constant o u) = o
constantOrigin = Refl

constantBounds : bounds s (constant o u) = (o,u)
constantBounds = Refl

One : Int
One = 1

Zero : Int
Zero = 0

clamp1_100_0 : clamp One 100 0 = One
clamp1_100_0 = Refl

clamp100_1_0 : clamp 100 One 0 = One
clamp100_1_0 = Refl

clamp1_100_150 : clamp One 100 150 = 100
clamp1_100_150 = Refl

clamp100_1_150 : clamp 100 One 150 = 100
clamp100_1_150 = Refl

clamp1_100_50 : clamp One 100 50 = 50
clamp1_100_50 = Refl

clamp100_1_50 : clamp 100 One 50 = 50
clamp100_1_50 = Refl