text:
module Generics.Derive

import Data.List1
import public Generics.SOP
import public Generics.Meta
import public Decidable.Equality

import public Language.Reflection.Derive

import System.Clock
import System.File

%language ElabReflection

%default total

--------------------------------------------------------------------------------
--          Generic
--------------------------------------------------------------------------------

private
ConNames : Type
ConNames = (Name, List String, List TTImp)

||| Name of record `Generic`'s constructor.
export
mkGeneric : Name
mkGeneric = "MkGeneric"

-- Applies the proper n-ary sum constructor to a list
-- of arguments. `k` is the index of the data type's
-- constructor.
private
mkSOP' : (k : Int) -> (arg : TTImp) -> TTImp
mkSOP' k arg = `(MkSOP) .$ run k
where run : (n : Int) -> TTImp
      run n = if n <= 0 then `(Z) .$ arg
                        else `(S) .$ run (assert_smaller n (n-1))

private
mkSOP : (k : Int) -> (args : List TTImp) -> TTImp
mkSOP k args = mkSOP' k (listOf args)

||| Creates the syntax tree for the code of the given data type.
||| We export this since it might be useful elsewhere.
export
mkCode : ParamTypeInfo -> TTImp
mkCode = listOf . map (listOf . map tpe . explicitArgs) . cons

private
fromClause : (Int,ConNames) -> Clause
fromClause (k,(con,ns,vars)) = bindAll con ns .= mkSOP k vars

private
fromToIdClause : (Int,ConNames) -> Clause
fromToIdClause (k,(con,ns,vars)) = bindAll con ns .= `(Refl)

private
toClause : (Int,ConNames) -> Clause
toClause (k,(con,ns,vars)) = mkSOP k (map bindVar ns) .= appAll con vars

private
impossibleToClause : Int -> Clause
impossibleToClause k = impossibleClause (mkSOP' k implicitTrue)

private
toFromIdClause : (Int,ConNames) -> Clause
toFromIdClause (k,(con,ns,vars)) = mkSOP k (map bindVar ns) .= `(Refl)

private
zipWithIndex : List a -> List (Int,a)
zipWithIndex as = run 0 as
  where run : Int -> List a -> List (Int,a)
        run _ []     = []
        run k (h::t) = (k,h) :: run (k+1) t

private
conNames : ParamCon -> ConNames
conNames (MkParamCon con args) = let ns   = map (nameStr . name) args
                                     vars = map varStr ns
                                  in (con, ns, vars)

||| Derives a `Generic` implementation for the given data type
||| and visibility.
export
GenericVis : Visibility -> DeriveUtil -> InterfaceImpl
GenericVis vis g =
  let names    = zipWithIndex (map conNames g.typeInfo.cons)
      len      = cast {to = Int} $ length names
      genType  = `(Generic) .$ g.appliedType .$ mkCode g.typeInfo
      funType  = piAllImplicit  genType g.paramNames
      x        = lambdaArg "x"
      varX     = var "x"

      from     = x .=> iCase varX implicitFalse (map fromClause names)
      to       = x .=> iCase varX implicitFalse (map toClause names ++ [impossibleToClause len])
      fromToId = x .=> iCase varX implicitFalse (map fromToIdClause names)
      toFromId = x .=> iCase varX implicitFalse (map toFromIdClause names ++ [impossibleToClause len])

      impl     = appAll mkGeneric [from,to,fromToId,toFromId]

   in MkInterfaceImpl "Generic" vis [] impl funType

||| Alias for `GenericVis Public`.
export
Generic : DeriveUtil -> InterfaceImpl
Generic = GenericVis Public

--------------------------------------------------------------------------------
--          Meta
--------------------------------------------------------------------------------

-- a string constant
private
str : String -> TTImp
str = primVal . Str

-- an int constant
private
int : Int -> TTImp
int = primVal . I

-- applies a name's namespace (List String) and name value
-- to a function (`con`) wrapped in a `TTImp`.
private
appNSName : Name -> (con : TTImp) -> TTImp
appNSName (NS (MkNS ss) (UN $ Basic s)) con = let ss' = listOf $ reverse $ map str ss
                                              in con .$ ss' .$ str s
appNSName n con                             = let s = str $ nameStr n
                                               in `(~(con) []) .$ s

-- creates an ArgName's TTImp from an argument's index and name
private
argNameTTImp : (Int,Name) -> TTImp
argNameTTImp (k, UN $ Basic n) = `(NamedArg)   .$ int k .$ str n
argNameTTImp (k, _)            = `(UnnamedArg) .$ int k

-- creates a ConInfo's TTImp from a `ParamCon`.
private
conTTImp : ParamCon -> TTImp
conTTImp (MkParamCon n args) =
  let np = listOf $ map argNameTTImp (zipWithIndex $ map name args)
   in appNSName n `(MkConInfo) .$ np

private
tiTTImp : ParamTypeInfo -> TTImp
tiTTImp (MkParamTypeInfo n _ cons) =
  let nps     = map conTTImp cons
   in appNSName n `(MkTypeInfo) .$ listOf nps

||| Derives a `Meta` implementation for the given data type
||| and visibility.
export
MetaVis : Visibility -> DeriveUtil -> InterfaceImpl
MetaVis vis g =
  let genType  = `(Meta) .$ g.appliedType .$ mkCode g.typeInfo
      funType  = piAllImplicit  genType g.paramNames

      impl     = `(MkMeta) .$ tiTTImp g.typeInfo

   in MkInterfaceImpl "Meta" vis [] impl funType

||| Alias for `EqVis Public`.
export
Meta : DeriveUtil -> InterfaceImpl
Meta = MetaVis Public

--------------------------------------------------------------------------------
--          Eq
--------------------------------------------------------------------------------

||| Derives an `Eq` implementation for the given data type
||| and visibility.
export
EqVis : Visibility -> DeriveUtil -> InterfaceImpl
EqVis vis g = MkInterfaceImpl "Eq" vis []
                `(mkEq genEq)
                (implementationType `(Eq) g)

||| Alias for `EqVis Public`.
export
Eq : DeriveUtil -> InterfaceImpl
Eq = EqVis Public

--------------------------------------------------------------------------------
--          Ord
--------------------------------------------------------------------------------

||| Derives an `Ord` implementation for the given data type
||| and visibility.
export
OrdVis : Visibility -> DeriveUtil -> InterfaceImpl
OrdVis vis g = MkInterfaceImpl "Ord" vis []
                 `(mkOrd genCompare)
                 (implementationType `(Ord) g)

||| Alias for `OrdVis Public`
export
Ord : DeriveUtil -> InterfaceImpl
Ord = OrdVis Public

--------------------------------------------------------------------------------
--          DecEq
--------------------------------------------------------------------------------

||| Derives a `DecEq` implementation for the given data type
||| and visibility.
export
DecEqVis : Visibility -> DeriveUtil -> InterfaceImpl
DecEqVis vis g = MkInterfaceImpl "DecEq" vis []
                   `(mkDecEq genDecEq)
                   (implementationType `(DecEq) g)

||| Alias for `EqVis Public`.
export
DecEq : DeriveUtil -> InterfaceImpl
DecEq = DecEqVis Public

--------------------------------------------------------------------------------
--          Semigroup
--------------------------------------------------------------------------------

||| Derives a `Semigroup` implementation for the given data type
||| and visibility.
export
SemigroupVis : Visibility -> DeriveUtil -> InterfaceImpl
SemigroupVis vis g = MkInterfaceImpl "Semigroup" vis []
                       `(MkSemigroup genAppend)
                       (implementationType `(Semigroup) g)

||| Alias for `SemigroupVis Public`.
export
Semigroup : DeriveUtil -> InterfaceImpl
Semigroup = SemigroupVis Public

--------------------------------------------------------------------------------
--          Monoid
--------------------------------------------------------------------------------

||| Derives a `Monoid` implementation for the given data type
||| and visibility.
export
MonoidVis : Visibility -> DeriveUtil -> InterfaceImpl
MonoidVis vis g = MkInterfaceImpl "Monoid" vis []
                       `(MkMonoid genNeutral)
                       (implementationType `(Monoid) g)

||| Alias for `MonoidVis Public`.
export
Monoid : DeriveUtil -> InterfaceImpl
Monoid = MonoidVis Public

--------------------------------------------------------------------------------
--          Show
--------------------------------------------------------------------------------

||| Derives a `Show` implementation for the given data type
||| and visibility.
export
ShowVis : Visibility -> DeriveUtil -> InterfaceImpl
ShowVis vis g = MkInterfaceImpl "Show" vis []
                  `(mkShowPrec genShowPrec)
                  (implementationType `(Show) g)

||| Alias for `ShowVis Public`.
export
Show : DeriveUtil -> InterfaceImpl
Show = ShowVis Public

--------------------------------------------------------------------------------
--          Prelude and Data Implementations
--------------------------------------------------------------------------------

-- Prelude

%runElab derive "Nat" [Generic,Meta]

%runElab derive "Maybe" [Generic,Meta]

%runElab derive "Either" [Generic,Meta]

%runElab derive "List" [Generic,Meta]

%runElab derive "List1" [Generic,Meta]

%runElab derive "Dec" [Generic,Meta]

%runElab derive "Ordering" [Generic,Meta]

%runElab derive "Bool" [Generic,Meta]

%runElab derive "Prec" [Generic,Meta]

-- System

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

%runElab derive "FileError" [Generic,Meta,Eq,Ord]

%runElab derive "File" [Generic,Meta]

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

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

%runElab derive "ClockType" [Generic,Meta,Eq,Ord]

-- Reflection

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

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

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

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

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

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

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

%runElab derive "Namespace" [Generic,Meta,Eq,Ord]

%runElab derive "UserName" [Generic,Meta,Eq,Ord]

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

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

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

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

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

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

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

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

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

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

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

%default covering

%runElab derive "Name" [Generic,Meta,Eq,Ord]

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

%runElab deriveMutual [ ("TTImp",        [Generic,Meta,Show,Eq])
                      , ("IField",       [Generic,Meta,Show,Eq])
                      , ("IFieldUpdate", [Generic,Meta,Show,Eq])
                      , ("AltType",      [Generic,Meta,Show,Eq])
                      , ("FnOpt",        [Generic,Meta,Show,Eq])
                      , ("ITy",          [Generic,Meta,Show,Eq])
                      , ("Data",         [Generic,Meta,Show,Eq])
                      , ("Record",       [Generic,Meta,Show,Eq])
                      , ("Clause",       [Generic,Meta,Show,Eq])
                      , ("Decl",         [Generic,Meta,Show,Eq])
                      ]


text:
import DataStore

test_store : DataStore (SString .+. SString .+. SInt)
test_store = addToStore ("Mercury", "Mariner 10",   1974)
           $ addToStore ("Venus",   "Venera",       1961)
           $ addToStore ("Uranus",  "Voyager 2",    1986)
           $ addToStore ("Pluto",   "New Horizons", 2015)
           $ empty

ext: idr

max_stars_repo_name: yurrriq/tdd-with-idris

max_issues_repo_name: yurrriq/tdd-with-idris

max_forks_repo_name: yurrriq/tdd-with-idris


text:
module Main

import Control.Arrow
import Control.Category
import Data.Morphisms
import System

%access public export

readNumber : IO (Maybe Nat)
readNumber = do
  input <- getLine
  if   all isDigit (unpack input)
  then pure (Just (cast input))
  else pure Nothing

-- Exercise 5.2.4.{1,3}

partial
guess : (target, guesses : Nat) -> IO ()
guess target guesses = do
  let guesses' = S guesses
  putStr "Guess #"
  print guesses'
  putStr " "
  Just num <- readNumber
    | Nothing => do putStrLn "Invalid input"
                    guess target guesses'
  EQ <- pure $ compare num target
    | LT => do putStrLn "Too low"
               guess target guesses'
    | GT => do putStrLn "Too high"
               guess target guesses'
  putStrLn "Nailed it!"

-- Exercise 5.2.4.2

main : IO ()
main = time >>= pure . flip mod 100 >>= flip guess 0 . cast

-- Exercise 5.2.4.4

{-
syntax "(,)" = MkPair

infixl 8 .:

(.:) : (c -> d) -> (a -> b -> c) -> a -> b -> d
(.:) = (.) . (.)
-}

namespace DIY
  replWith : a -> String -> (a -> String -> Maybe (String, a)) -> IO ()
  replWith state prompt func = do
    putStr prompt
    input <- getLine
    case func state input of
      Just (output, state') => putStr output *> DIY.replWith state' prompt func
      Nothing               => pure ()

  repl : String -> (String -> String) -> IO ()
  repl prompt func = DIY.replWith () prompt (go func)
    where
      go : (a -> b) -> c -> a -> Maybe (b,c)
      go f = curry . applyMor $
        arrow swap >>> first (arrow f) >>> arrow Just


text:
module BoundedGCD

%default total
%access public export

notLTEimpliesLT : (a: Nat) -> (b: Nat) -> (LTE a b -> Void) -> LTE (S b) a
notLTEimpliesLT Z b contra = void (contra (LTEZero))
notLTEimpliesLT (S k) Z f = LTESucc (LTEZero)
notLTEimpliesLT (S k) (S j) contra =
  LTESucc (notLTEimpliesLT k j previousContra) where
    previousContra = \evidence : (LTE k j) => contra (LTESucc evidence)

subWithBound: (n: Nat) -> (m: Nat) -> (LTE m n) -> (k: Nat ** LTE k n)
subWithBound n Z LTEZero = (n ** lteRefl)
subWithBound (S p) (S q) (LTESucc pf) = case subWithBound p q pf of
                                             (x ** pf) =>
                                                (x ** lteSuccRight pf)

boundedGCD : (bnd: Nat) -> (n: Nat) -> (m: Nat) -> (LTE n bnd) -> (LTE (S m) bnd) -> Nat
boundedGCD (S b) Z m x (LTESucc y) = m
boundedGCD (S b) (S k) Z x (LTESucc y) = (S k)
boundedGCD (S b) (S Z) (S j) (LTESucc x) (LTESucc y) = S Z
boundedGCD (S b) (S k) (S Z) (LTESucc x) (LTESucc y) = S Z
boundedGCD (S b) (S (S (k))) (S (S (j))) (LTESucc x) (LTESucc y) =
  case isLTE j k of
        (Yes prf) => case subWithBound k j prf of
                           (diff ** pf) => boundedGCD b (S (S j)) diff y (lteTransitive (LTESucc pf) x)
        (No contra) =>
          let
            ineq = notLTEimpliesLT j k contra
          in
            boundedGCD b (S (S j)) (S (S k)) y (lteTransitive (LTESucc (LTESucc ineq)) y)

gcdAlgo : Nat -> Nat -> Nat
gcdAlgo k j = case isLTE (S j) k of
                   (Yes prf) => boundedGCD k k j lteRefl prf
                   (No contra) =>
                      let
                        ineq = notLTEimpliesLT (S j) k contra
                      in
                        boundedGCD (S j) k j  (lteSuccLeft ineq) lteRefl


text:
module Verified.Functor.Maybe

import Verified.Functor

instance VerifiedFunctor Maybe where
  functorIdentity Nothing = Refl
  functorIdentity (Just x) = Refl
  functorComposition Nothing g1 g2 = Refl
  functorComposition (Just x) g1 g2 = Refl

max_stars_repo_name: yurrriq/idris-verified

max_issues_repo_name: yurrriq/idris-verified

max_forks_repo_name: yurrriq/idris-verified


text:
import System.Directory

main : IO ()
main = do Right () <- createDir "testdir"
               | Left err => printLn err
          Left err <- createDir "testdir"
               | _ => printLn "That wasn't supposed to work"
          printLn err
          ok <- changeDir "nosuchdir"
          printLn ok
          ok <- changeDir "testdir"
          printLn ok
          writeFile "test.txt" "hello\n"
          printLn !currentDir

max_stars_repo_name: boxfire/rapid

max_issues_repo_name: boxfire/rapid

max_forks_repo_name: boxfire/rapid


text:
module TypesAndFunctions

import Data.List
import Data.Strings
import Data.Vect

%default total

-- data types

data MyNat = MZ | MS MyNat

mynat2int : MyNat -> Int
mynat2int MZ = 0
mynat2int (MS n) = 1 + mynat2int n

partial
int2mynat : Int -> MyNat
int2mynat 0 = MZ
int2mynat n = MS (int2mynat (n - 1))

plus : MyNat -> MyNat -> MyNat
plus MZ m = m
plus (MS n) m = MS (plus n m)

mult : MyNat -> MyNat -> MyNat
mult MZ _ = MZ
mult (MS n) m = plus m (mult n m)

infixr 10 ::

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

Show a => Show (MyList a) where
  show Nil = "Nil"
  show (x :: xs) = "(Cons " ++ show x ++ " " ++ show xs ++ ")"

len : MyList a -> Nat
len Nil = Z
len (_ :: xs) = S (len xs)

fromList : List a -> MyList a
fromList [] = Nil
fromList (x :: xs) = (::) x (fromList xs)

-- where clauses

myReverse : List a -> List a
myReverse xs = aux xs [] where
  aux : List a -> List a -> List a
  aux [] acc = acc
  aux (x :: xs) acc = aux xs (x :: acc)

-- till https://github.com/idris-lang/Idris2/issues/588 is fixed, this
-- definition has to be in the top-level
data MyLT = Yes | No

foo : Int -> Int
foo x = case isLT of
            Yes => x * 2
            No => x * 4 where
              isLT : MyLT
              isLT = if x < 10 then Yes else No

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

test : List Nat
test = [c (S 1), c Z, d (S Z)] where
  c : Nat -> Nat
  c x = 42 + x

  d : Nat -> Nat
  d y = c (y + 1 + z y) where
    z : Nat -> Nat
    z w = y + w

-- totality and covering

partial
from : Maybe a -> a
from (Just x) = x

-- dependent types

isSingleton : Bool -> Type
isSingleton False = List Nat
isSingleton True = Nat

mkSingle : (x : Bool) -> isSingleton x
mkSingle False = []
mkSingle True = 0

mysum : (single : Bool) -> isSingleton single -> Nat
mysum False [] = 0
mysum False (n :: ns) = n + mysum False ns
mysum True d = d

-- declaration order and mutual blocks

mutual
  myeven : Nat -> Bool
  myeven Z = True
  myeven (S k) = myodd k

  myodd : Nat -> Bool
  myodd Z = False
  myodd (S k) = myeven k

greet : HasIO io => io ()
greet = do putStr "What is your name? "
           name <- getLine
           putStrLn $ "Nice to meet you, " ++ name

-- laziness
{-
  data Lazy : Type -> Type where
    Delay : (val : a) -> Lazy a

  Force : Lazy a -> a
-}

myIfThenElse : Bool -> Lazy a -> Lazy a -> a
myIfThenElse True t e = t
myIfThenElse False t e = e

-- infinite data types (codata)

{-
  data Stream : Type -> Type where
    (::) : (e : a) -> Inf (Stream a) -> Stream a
-}

ones : Stream Nat
ones = 1 :: ones

-- useful data types

{-
  data List a = Nil | (::) a (List a)

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

{-
  map : (a -> b) -> List a -> List b
  map _ [] = []
  map f (x :: xs) = f x :: map f xs

  map : (a -> b) -> Vect n a -> Vect n b
  map _ [] = []
  map f (x :: xs) = f x :: map f xs
-}

intVec : Vect 5 Int
intVec = [1, 2, 3, 4, 5]

double : Int -> Int
double x = x + x

listLookup : Nat -> List a -> Maybe a
listLookup _ [] = Nothing
listLookup Z (x :: _) = Just x
listLookup (S k) (_ :: xs) = listLookup k xs

-- tuples

{-
  data Pair : Type -> Type -> Type where
    MkPair : a -> b -> Pair a b
-}

fred : (String, Nat)
fred = ("Fred", 42)

jim : (String, Int, String)
jim = ("Jim", 25, "Cambridge")

-- dependent pairs (Signma Types)

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

data DepPair : (a : Type) -> (p : a -> Type) -> Type where
  MkDepPair : { p : a -> Type } -> (x : a) -> p x -> DepPair a p

vec : (n : Nat ** Vect n Int)
vec = (3 ** [1, 2, 3])

vec1 : DPair Nat (\n => Vect n Int)
vec1 = MkDPair 3 [1, 2, 3]

vec2 : DepPair Nat (\n => Vect n Int)
vec2 = MkDepPair 3 [1, 2, 3]

vec3 : (n : Nat ** Vect n String)
vec3 = (_ ** ["Hello", "world"])

vec4 : (n ** Vect n Double)
vec4 = (_ ** [1.0, 2.2, -2.1212])

vFilter : (a -> Bool) -> Vect n a -> (p : Nat ** Vect p a)
vFilter p [] = (0 ** [])
vFilter p (x :: xs) = case p x of
                           False => vFilter p xs
                           True => let (_ ** res) = vFilter p xs in
                                       (_ ** (x :: res))

-- let bindings

mirror : List a -> List a
mirror xs = let xs' = reverse xs in
                 xs ++ xs'

data Person = MkPerson String Int

showPerson : Person -> String
showPerson p = let MkPerson name age = p in
                   name ++ " is " ++ show age ++ " years old"

-- list comprehensions

pythag : Int -> List (Int, Int, Int)
pythag n = [(x, y, z) | z <- [1..n], y <- [1..z], x <- [1..y], x * x + y * y == z * z]

-- case expressions

partial
mySplitAt : Char -> String -> (String, String)
mySplitAt c cs = case break (== c) cs of
                      (h, t) => (h, strTail t)

max_stars_repo_name: timmyjose-study/idris-from-the-docs

max_issues_repo_name: timmyjose-study/idris-from-the-docs

max_forks_repo_name: timmyjose-study/idris-from-the-docs


text:
module Data.List.Properties

import Interfaces.Verified

%hide Prelude.List.reverse
%hide Prelude.Strings.reverse

%default total
%access public export

VerifiedFunctor List where
  functorIdentity [] = Refl
  functorIdentity (x :: xs) = cong (functorIdentity xs)
  functorComposition [] g1 g2 = Refl
  functorComposition (x :: xs) g1 g2 = cong (functorComposition xs g1 g2)

-- | Return the elements of a list in reverse order.
reverse' : List a -> List a -> List a
reverse' acc []      = acc
reverse' acc (x::xs) = reverse' (x::acc) xs

reverse : List a -> List a
reverse xs = reverse' [] xs

reverseNonEmpty : (xs : List a) -> NonEmpty xs -> NonEmpty (reverse xs)
reverseNonEmpty (x :: xs) IsNonEmpty = go [x] IsNonEmpty xs where
  go : (acc : List a) -> NonEmpty acc -> (xs : List a) -> NonEmpty (reverse' acc xs)
  go acc pr []        = pr
  go acc _  (x :: xs) = go (x :: acc) IsNonEmpty xs

reverseAppend : (xs : List a) -> (ys : List a) -> reverse' xs ys = reverse ys <+> xs
reverseAppend xs [] = Refl
reverseAppend xs (y :: ys) =
    rewrite reverseAppend [y] ys in
    rewrite sym $ appendAssociative (reverse' [] ys) [y] xs in
    rewrite reverseAppend (y :: xs) ys in
    Refl

reverseAppend' : (xs : List a) -> (ys : List a) -> (zs : List a) -> reverse' xs ys <+> zs = reverse' (xs <+> zs) ys
reverseAppend' xs ys zs =
    rewrite reverseAppend xs ys in
    rewrite reverseAppend (xs <+> zs) ys in
    rewrite appendAssociative (reverse' [] ys) xs zs in
    Refl

reverse2 : List a -> List a
reverse2 [] = []
reverse2 (x :: xs) = reverse2 xs <+> [x]

reverse2Append : (xs : List a) -> (ys : List a) -> reverse2 (xs <+> ys) = reverse2 ys <+> reverse2 xs
reverse2Append [] ys = rewrite appendNilRightNeutral (reverse2 ys) in Refl
reverse2Append (x :: xs) ys =
    rewrite appendAssociative (reverse2 ys) (reverse2 xs) [x] in
    rewrite reverse2Append xs ys in Refl

reverse2Involution : (xs : List a) -> xs = reverse2 (reverse2 xs)
reverse2Involution [] = Refl
reverse2Involution (x :: xs) =
    rewrite reverse2Append (reverse2 xs) [x] in
    rewrite reverse2Involution xs in
    Refl

reverse2Reverse : (xs : List a) -> reverse2 xs = reverse xs
reverse2Reverse [] = Refl
reverse2Reverse (x :: xs) =
    rewrite reverseAppend [x] xs in
    rewrite reverse2Reverse xs in
    Refl

-- TODO: Write a proof that doesn't need reverse2
reverseInvolution : (xs : List a) -> xs = reverse (reverse xs)
reverseInvolution xs =
    rewrite sym $ reverse2Reverse xs in
    rewrite sym $ reverse2Reverse (reverse2 xs) in
    rewrite reverse2Involution xs in
    Refl

max_stars_repo_name: Risto-Stevcev/idris-catenatable-lists

max_issues_repo_name: Risto-Stevcev/idris-catenable-lists

max_forks_repo_name: Risto-Stevcev/idris-catenatable-lists


text:
module Compiler.LLVM.Rapid.Foreign

import Data.List
import Data.String
import Data.Vect

import Compiler.CompileExpr
import Core.Name

import Compiler.LLVM.IR
import Compiler.LLVM.Instruction
import Compiler.LLVM.Rapid.Object
import Control.Codegen
import Data.Utils
import Rapid.Common

-- we provide our own in Data.Utils
%hide Core.Name.Namespace.showSep

fromCFType : CFType -> IRType
fromCFType CFChar = I32
fromCFType (CFIORes CFChar) = I32
fromCFType CFInt = I64
fromCFType (CFIORes CFInt) = I64
fromCFType CFDouble = F64
fromCFType (CFIORes CFDouble) = F64
fromCFType _ = IRObjPtr

cftypeIsUnit : CFType -> Bool
cftypeIsUnit CFUnit = True
cftypeIsUnit (CFIORes CFUnit) = True
cftypeIsUnit _ = False

wrapForeignResult : (cft : CFType) -> (v: IRValue (fromCFType cft)) -> Codegen (IRValue IRObjPtr)
wrapForeignResult (CFChar) v = cgMkChar v
wrapForeignResult (CFIORes CFChar) v = cgMkChar v
wrapForeignResult (CFInt) v = cgMkInt v
wrapForeignResult (CFIORes CFInt) v = cgMkInt v
wrapForeignResult (CFDouble) v = cgMkDouble v
wrapForeignResult (CFIORes CFDouble) v = cgMkDouble v
wrapForeignResult _ (SSA _ v) = pure (SSA IRObjPtr v)
wrapForeignResult _ _ = do
  addError "can not wrap foreign result"
  pure (SSA IRObjPtr "error")

||| Call a "runtime-aware" foreign function, i.e. one, that can interact with the RTS
export
foreignCall : {t : IRType} -> String -> List String -> Codegen (IRValue t)
foreignCall {t} name args = do
  hp <- load globalHpVar
  hpLim <- load globalHpLimVar
  baseHpPointer <- SSA (Pointer 0 RuntimePtr) <$> assignSSA ("getelementptr inbounds %Idris_TSO.struct, %TSOPtr %BaseArg, i32 0, i32 1")
  store hp baseHpPointer
  result <- SSA t <$> (assignSSA $ "  call ccc " ++ show t ++ " " ++ name ++ "(" ++ (showSep ", " ("%TSOPtr %BaseArg"::args)) ++ ")")
  store !(load baseHpPointer) globalHpVar
  pure result

export
foreignVoidCall : String -> List String -> Codegen ()
foreignVoidCall name args = do
  hp <- load globalHpVar
  hpLim <- load globalHpLimVar
  baseHpPointer <- SSA (Pointer 0 RuntimePtr) <$> assignSSA ("getelementptr inbounds %Idris_TSO.struct, %TSOPtr %BaseArg, i32 0, i32 1")
  store hp baseHpPointer
  appendCode $ "  call ccc void " ++ name ++ "(" ++ (showSep ", " ("%TSOPtr %BaseArg"::args)) ++ ")"
  store !(load baseHpPointer) globalHpVar

export
prepareArgCallConv' : List String -> List String
prepareArgCallConv' rest = ["%RuntimePtr %HpArg", "%TSOPtr %BaseArg", "%RuntimePtr %HpLimArg"] ++ rest

export
prepareArgCallConv : List String -> List String
prepareArgCallConv l = prepareArgCallConv' l

transformArg : (IRValue IRObjPtr, CFType) -> Codegen String
transformArg (arg, CFChar) = do
  i <- unboxChar' arg
  pure (toIR i)
transformArg (arg, CFInt) = do
  i <- unboxInt' arg
  pure (toIR i)
transformArg (arg, CFDouble) = do
  d <- unboxFloat64' arg
  pure (toIR d)
transformArg (arg, _) = pure (toIR arg)

-- TODO: in this file, reg2val is only ever used with RVal, refactor
rvalVar : IRValue (Pointer 0 IRObjPtr)
rvalVar = SSA (Pointer 0 IRObjPtr) ("%rvalVar")

export
genericForeign : String -> Name -> (argTypes : List CFType) -> CFType -> Codegen ()
genericForeign foreignName name argTypes ret = do
  let args = map (\(i, _) => SSA IRObjPtr ("%arg" ++ show i)) (enumerate argTypes)
  appendCode ("define private fastcc %Return1 @" ++ safeName name ++ "(" ++ (showSep ", " $ prepareArgCallConv $ map toIR args) ++ ") gc \"statepoint-example\" {")
  funcEntry
  if cftypeIsUnit ret then do
    foreignVoidCall ("@" ++ foreignName) !(traverse transformArg (zip args argTypes))
    store !(mkUnit) rvalVar
    else do
      fgResult <- foreignCall {t=fromCFType ret} ("@" ++ foreignName) !(traverse transformArg (zip args argTypes))
      store !(wrapForeignResult ret fgResult) rvalVar
  funcReturn
  appendCode "\n}\n"

export
missingForeign : List String -> Name -> (argTypes : List CFType) -> Codegen ()
missingForeign cs name argTypes = do
  let args = map (\(i, _) => SSA IRObjPtr ("%arg" ++ show i)) (enumerate argTypes)
  appendCode ("define private fastcc %Return1 @" ++ safeName name ++ "(" ++ (showSep ", " $ prepareArgCallConv $ map toIR args) ++ ") gc \"statepoint-example\" {")
  funcEntry
  appendCode $ "call ccc void @idris_rts_crash(i64 404) noreturn"
  addError $ "missing foreign: " ++ show name ++ " <- " ++ show cs
  funcReturn
  appendCode "\n}\n"

export
builtinForeign : (n : Nat ** (Vect n (IRValue IRObjPtr) -> Codegen (IRValue IRObjPtr))) -> Name -> (argTypes : List CFType) -> CFType -> Codegen ()
builtinForeign builtin name argTypes ret = do
  let (n ** f) = builtin
  appendCode ("define external fastcc %Return1 @" ++ safeName name ++ "(" ++ (showSep ", " $ prepareArgCallConv $ toList $ map toIR (args n)) ++ ") gc \"statepoint-example\" {")
  funcEntry
  result <- f (args n)
  store result $ SSA (Pointer 0 IRObjPtr) ("%rvalVar")
  funcReturn
  appendCode "\n}\n"
  where
  args : (n : Nat) -> Vect n (IRValue IRObjPtr)
  args n = map (\i => SSA IRObjPtr $ "%arg" ++ show (finToNat i)) range

foreignRedirectMap : List (String, String)
foreignRedirectMap = [
    ("C:idris2_openFile, libidris2_support, idris_file.h", "rapid_system_file_open")
  , ("C:fdopen,libc 6", "rapid_system_fdopen")
  , ("C:idris2_closeFile, libidris2_support, idris_file.h", "rapid_system_file_close")
  , ("C:fflush,libc 6", "rapid_system_file_flush")
  , ("C:idris2_fileSize, libidris2_support, idris_file.h", "rapid_system_file_size")
  , ("C:idris2_fileAccessTime, libidris2_support, idris_file.h", "rapid_system_file_atime")
  , ("C:idris2_fileStatusTime, libidris2_support, idris_file.h", "rapid_system_file_ctime")
  , ("C:idris2_fileModifiedTime, libidris2_support, idris_file.h", "rapid_system_file_mtime")
  , ("C:idris2_readLine, libidris2_support, idris_file.h", "rapid_system_file_read_line")
  , ("C:idris2_readChars, libidris2_support, idris_file.h", "rapid_system_file_read_chars")
  , ("C:idris2_seekLine, libidris2_support, idris_file.h", "rapid_system_file_seek_line")
  , ("C:fgetc,libc 6", "rapid_system_file_read_char")
  , ("C:idris2_chmod, libidris2_support, idris_file.h", "rapid_system_file_chmod")
  , ("C:getchar,libc 6", "rapid_system_getchar")
  , ("C:putchar,libc 6", "rapid_system_putchar")
  , ("C:idris2_getStr, libidris2_support, idris_support.h", "rapid_system_stdin_getline")
  , ("C:idris2_writeLine, libidris2_support, idris_file.h", "rapid_system_file_write_string")
  , ("C:idris2_eof, libidris2_support, idris_file.h", "rapid_system_file_eof")
  , ("C:idris2_removeFile, libidris2_support, idris_file.h", "rapid_system_file_remove")
  , ("C:idris2_fileError, libidris2_support, idris_file.h", "rapid_system_file_error")
  , ("C:idris2_fileErrno, libidris2_support, idris_file.h", "rapid_system_errno")
  , ("C:idris2_getErrno, libidris2_support, idris_support.h", "rapid_system_errno")
  , ("C:idris2_stdin, libidris2_support, idris_file.h", "rapid_system_file_stdin")
  , ("C:idris2_stdout, libidris2_support, idris_file.h", "rapid_system_file_stdout")
  , ("C:idris2_stderr, libidris2_support, idris_file.h", "rapid_system_file_stderr")
  , ("C:idris2_currentDirectory, libidris2_support, idris_directory.h", "rapid_system_current_dir")
  , ("C:idris2_createDir, libidris2_support, idris_directory.h", "rapid_system_dir_create")
  , ("C:idris2_changeDir, libidris2_support, idris_directory.h", "rapid_system_dir_change")
  , ("C:idris2_removeDir, libidris2_support, idris_directory.h", "rapid_system_dir_remove")
  , ("C:idris2_openDir, libidris2_support, idris_directory.h", "rapid_system_dir_open")
  , ("C:idris2_closeDir, libidris2_support, idris_directory.h", "rapid_system_dir_close")
  , ("C:idris2_nextDirEntry, libidris2_support, idris_directory.h", "rapid_system_dir_next_entry")
  , ("C:idris2_popen, libidris2_support, idris_file.h", "rapid_system_popen")
  , ("C:idris2_pclose, libidris2_support, idris_file.h", "rapid_system_pclose")
  , ("C:idris2_free, libidris2_support, idris_memory.h", "rapid_system_free")
  , ("C:idris2_putStr, libidris2_support, idris_support.h", "rapid_putstr")
  , ("C:idris2_readBufferData, libidris2_support, idris_file.h", "idris_rts_read_buffer_data")
  , ("C:idris2_writeBufferData, libidris2_support, idris_file.h", "idris_rts_write_buffer_data")
  , ("C:idris2_isNull, libidris2_support, idris_support.h", "prim/isNull")
  , ("C:idris2_fileErrno, libidris2_suppor, idris_support.h", "rapid_system_file_errno")
  , ("C:idrnet_errno, libidris2_support, idris_net.h", "rapid_system_errno")
  , ("C:idris2_strerror, libidris2_support, idris_support.h", "rapid_system_strerror")
  , ("C:idris2_getString, libidris2_support, idris_support.h", "prim/getString")

  , ("C:idris2_setupTerm, libidris2_support, idris_term.h", "idris2_setupTerm")
  , ("C:idris2_getTermCols, libidris2_support, idris_term.h", "idris2_getTermCols")
  , ("C:idris2_getTermLines, libidris2_support, idris_term.h", "idris2_getTermLines")

  , ("scheme:blodwen-stringbytelen", "rapid_string_bytelength")
  , ("scheme:blodwen-string-iterator-new", "prim/blodwen-string-iterator-new")
  , ("scheme:blodwen-string-iterator-next", "prim/blodwen-string-iterator-next")
  , ("scheme:blodwen-string-iterator-to-string", "prim/blodwen-string-iterator-to-string")
  , ("C:exit, libc 6", "rapid_system_exit")
  , ("C:idris2_system, libidris2_support, idris_system.h", "rapid_system_system")
  , ("C:getenv, libc 6", "rapid_system_get_env")
  , ("scheme:blodwen-arg-count", "rapid_system_get_arg_count")
  , ("scheme:blodwen-arg", "rapid_system_get_arg")

  , ("C:idrnet_af_inet, libidris2_support, idris_net.h", "idrnet_af_inet")
  , ("C:idrnet_af_inet6, libidris2_support, idris_net.h", "idrnet_af_inet6")
  , ("C:idrnet_af_unix, libidris2_support, idris_net.h", "idrnet_af_unix")
  , ("C:idrnet_af_unspec, libidris2_support, idris_net.h", "idrnet_af_unspec")
  , ("C:idrnet_accept, libidris2_support, idris_net.h", "idrnet_accept")
  , ("C:idrnet_bind, libidris2_support, idris_net.h", "idrnet_bind")
  , ("C:idrnet_create_sockaddr, libidris2_support, idris_net.h", "idrnet_create_sockaddr")
  , ("C:idrnet_free, libidris2_support, idris_net.h", "idrnet_free")
  , ("C:idrnet_fdopen, libidris2_support, idris_net.h", "rapid_system_fdopen")
  , ("C:idrnet_sockaddr_family, libidris2_support, idris_net.h", "idrnet_sockaddr_family")
  , ("C:idrnet_sockaddr_ipv4, libidris2_support, idris_net.h", "idrnet_sockaddr_ipv4")
  , ("C:idrnet_sockaddr_unix, libidris2_support, idris_net.h", "idrnet_sockaddr_unix")
  , ("C:idrnet_socket, libidris2_support, idris_net.h", "idrnet_socket")
  , ("C:idrnet_listen, libidris2_support, idris_net.h", "idrnet_listen")

  , ("scheme:blodwen-buffer-size", "prim/blodwen-buffer-size")
  , ("scheme:blodwen-new-buffer", "prim/blodwen-new-buffer")
  , ("scheme:blodwen-buffer-free", "prim/noop2")
  , ("scheme:blodwen-buffer-setbyte", "prim/blodwen-buffer-setbyte")
  , ("scheme:blodwen-buffer-getbyte", "prim/blodwen-buffer-getbyte")
  , ("scheme:blodwen-buffer-setbits16", "prim/blodwen-buffer-setbits16")
  , ("scheme:blodwen-buffer-getbits16", "prim/blodwen-buffer-getbits16")
  , ("scheme:blodwen-buffer-setbits32", "prim/blodwen-buffer-setbits32")
  , ("scheme:blodwen-buffer-getbits32", "prim/blodwen-buffer-getbits32")
  , ("scheme:blodwen-buffer-setbits64", "prim/blodwen-buffer-setbits64")
  , ("scheme:blodwen-buffer-getbits64", "prim/blodwen-buffer-getbits64")
  , ("scheme:blodwen-buffer-setint32", "prim/blodwen-buffer-setint32")
  , ("scheme:blodwen-buffer-getint32", "prim/blodwen-buffer-getint32")
  , ("scheme:blodwen-buffer-setint", "prim/blodwen-buffer-setint")
  , ("scheme:blodwen-buffer-getint", "prim/blodwen-buffer-getint")
  , ("scheme:blodwen-buffer-setdouble", "prim/blodwen-buffer-setdouble")
  , ("scheme:blodwen-buffer-getdouble", "prim/blodwen-buffer-getdouble")
  , ("scheme:blodwen-buffer-setstring", "prim/blodwen-buffer-setstring")
  , ("scheme:blodwen-buffer-getstring", "prim/blodwen-buffer-getstring")
  , ("scheme:blodwen-buffer-copydata", "prim/blodwen-buffer-copydata")

  , ("scheme:blodwen-thread", "rapid_system_fork")

  , ("scheme:blodwen-clock-time-utc", "prim/blodwen-clock-time-utc")
  , ("scheme:blodwen-clock-time-monotonic", "prim/blodwen-clock-time-monotonic")
  , ("scheme:blodwen-clock-time-duration", "prim/blodwen-clock-time-duration")
  , ("scheme:blodwen-clock-time-process", "prim/blodwen-clock-time-process")
  , ("scheme:blodwen-clock-time-thread", "prim/blodwen-clock-time-thread")
  , ("scheme:blodwen-clock-time-gccpu", "prim/blodwen-clock-time-gccpu")
  , ("scheme:blodwen-clock-time-gcreal", "prim/blodwen-clock-time-gcreal")

  , ("scheme:blodwen-is-time?", "prim/blodwen-is-time")
  , ("scheme:blodwen-clock-second", "prim/blodwen-clock-second")
  , ("scheme:blodwen-clock-nanosecond", "prim/blodwen-clock-nanosecond")

  , ("scheme:string-concat", "prim/string-concat")
  , ("scheme:string-pack", "prim/string-pack")
  , ("scheme:string-unpack", "prim/string-unpack")
  ]

export
findForeignName : List String -> Maybe String
findForeignName cs =
  case find (isPrefixOf "rapid:") cs of
       Just found => Just (substr 6 99999 found)
       Nothing => choiceMap (\n => lookup n foreignRedirectMap) cs


text:
module Setoid

%default total
%access public export

Reflx: {A : Type} -> (R: A -> A -> Type) -> Type
Reflx {A} R = (x : A) -> R x x

Symm: {A : Type} -> (R: A -> A -> Type) -> Type
Symm {A} R = (x : A) -> (y : A) -> R x y -> R y x

Trans: {A : Type} -> (R: A -> A -> Type) -> Type
Trans {A} R = (x : A) -> (y : A) -> (z : A) -> R x y -> R y z -> R x z

data IsEquivalence: {A : Type} -> (R: A -> A -> Type) -> Type where
    EqProof: {A: Type} -> (R: A -> A -> Type) -> Reflx {A} R -> Symm {A} R -> Trans {A} R -> IsEquivalence {A} R

record Setoid where
    constructor MkSetoid
    Carrier: Type
    Equivalence: Carrier -> Carrier -> Type
    isEquivalence: IsEquivalence Equivalence


text:
module Package

data Version : Type where
  V : (major : Nat) -> (minor : Nat) -> (patch : Nat) -> Version

Eq Version where
  (V a b c) == (V a' b' c') = (a == a') && (b == b') && (c == c')

Ord Version where
  compare (V a b c) (V a' b' c') = if a > a' then GT else
                                   if a == a' && b > b' then GT else
                                   if a == a' && b == b' && c > c' then GT else
                                   if a == a' && b == b' && c == c' then EQ else LT

Show Version where
  show (V a b c) = "version " ++ show a ++ "." ++ show b ++ "." ++ show c

data PkgConstraint : Type where
  Any     : PkgConstraint
  Up      : Version -> PkgConstraint
  Down    : Version -> PkgConstraint
  Exactly : Version -> PkgConstraint
  Between : Version -> Version -> PkgConstraint

Show PkgConstraint where
  show Any           = ""
  show (Up v)        = "(>= " ++ show v ++ ")"
  show (Down v)      = "(<= " ++ show v ++ ")"
  show (Exactly v)   = "(= " ++ show v ++ ")"
  show (Between v w) = "(>= " ++ show v ++ ", <=" ++ show w ++ ")"

inRange : Version -> PkgConstraint -> Bool
inRange v Any           = True
inRange v (Up w)        = v >= w
inRange v (Down w)      = v <= w
inRange v (Exactly w)   = v == w
inRange v (Between w x) = w <= v && v <= x

data Dep : Type where
  Dependency : String -> PkgConstraint -> List Dep -> Dep

Show Dep where
  show (Dependency s v xs) = "Package " ++ s ++ " " ++ show v

[depverbose] Show Dep where
  show (Dependency s v xs) = "Package " ++ s ++ " " ++ show v ++ " depends on: " ++ show xs

data Hash = None
          | Md5 String
          | Sha1 String
          | Blake2 String

record Pkg where
  constructor Package
  pname : String
  version : Version
  compile, install, uninstall : String
  src : String
  hash : Hash
  deps : List Dep -- Should packages still store their dependencies?

Eq Pkg where
  p == p' = pname p == pname p' && version p == version p'

Ord Pkg where
  compare p p' = if pname p > pname p' then GT else
                 if pname p < pname p' then LT else
                 if version p > version p' then GT else
                 if version p < version p' then LT else EQ

Show Pkg where
  show p = "Package " ++ pname p ++ " " ++ (show $ version p)

[pkgverbose] Show Pkg where
  show p = "Package " ++ pname p ++ " " ++ (show $ version p) ++ " depends on: " ++ show (deps p)

queryPkg : String -> PkgConstraint -> List Pkg -> Maybe Pkg
queryPkg query constraint srcs = head' matches
  where matches = filter (\pkg => pname pkg == query && inRange (version pkg) constraint) $ reverse $ sort srcs -- This is slow, will bottleneck

max_stars_repo_name: nv-vn/Anvil

max_issues_repo_name: nv-vn/Anvil

max_forks_repo_name: nv-vn/Anvil


text:
-- Module      : Main
-- Description :
-- Copyright   : (c) Simon Nielsen Knights 2018
-- License     : MIT
-- Maintainer  : simonank@mail.ru
-- Stability   : unstable
-- Portability : portable

import Itea

hello : Html a
hello = div [] [text "Hello, world!"]

main : JS_IO ()
main = ?runProgram

max_stars_repo_name: simonank/idris-tea

max_issues_repo_name: simonank/idris-tea

max_forks_repo_name: simonank/idris-tea


text:
import Lightyear
import Lightyear.Strings
import Network.Socket
import Prelude.Strings
import System
import System.Concurrency.Process
import Data.Vect

import HydraBot.Types
import HydraBot.NetworkUtils

||| Check news/updates
||| @w A writer process id
||| @c A list of channels
||| @d Delay between checks, in seconds
||| @l A list of news loaders
||| @o A list of previous versions
news' : (w: ProcID Message) -> (c: List String) -> (d: Int) ->
      (l: Vect n (String, IO (Maybe String))) -> (o: Vect n (Maybe String)) ->
      Process Message ()
news' writer channels delay loaders old = do
  Lift $ usleep $ delay * 1000000
  new <- traverse check $ zip loaders old
  news' writer channels delay loaders new
where
  check : ((String, IO (Maybe String)), Maybe String) -> Process Message (Maybe String)
  check ((name, load), o) = do
    n <- Lift load
    case (n, n == o) of
      (Just n', False) => do
        if (o /= Nothing) -- don't write right after [re]start
        then traverse (\x => send writer (cmsg x (name ++ ": " ++ n'))) channels
        else pure []
        pure (Just n')
      (Nothing, False) => do
        Lift . putStrLn $ "Failed to retrieve: " ++ name
        pure o
      (_, _) => pure o

||| Check news/updates
||| @w A writer process id
||| @c A list of channels
||| @d Delay between checks, in seconds
||| @l A list of news loaders
news : (w: ProcID Message) -> (c: List String) -> (d: Int) ->
     (l: Vect n (String, IO (Maybe String))) -> Process Message ()
news w c d l = news' w c d l (map (const Nothing) l)

skipTill : String -> Parser String
skipTill s = string s <|>| ((satisfy $ const True) *> (skipTill s))

tillChar : Char -> Parser String
tillChar c = pack <$> many (satisfy $ (/= c))

||| XKCD scraper
xkcd : IO (Maybe String)
xkcd = scrape "23.235.37.67" 80 req "</feed>" url
where
  req = "GET /atom.xml HTTP/1.0\r\nHost: xkcd.com\r\n"
  url : Parser String
  url = do
    skipTill "<entry><title>"
    title <- tillChar '<'
    skipTill "<link href=\""
    url <- tillChar '"'
    pure $ url ++ " (" ++ title ++ ")"

||| Invisible Bread scraper
IB : IO (Maybe String)
IB = scrape "104.28.24.25" 80 req "<link rel=\"shortcut" url
where
  req = "GET / HTTP/1.0\r\nHost: invisiblebread.com\r\n"
  url : Parser String
  url = do
    skipTill "<meta property=\"og:url\" content=\""
    url <- tillChar '"'
    pure url

comics : Vect 2 (String, IO (Maybe String))
comics = [("XKCD", xkcd), ("Invisible Bread", IB)]

max_stars_repo_name: defanor/hydra-bot

max_issues_repo_name: defanor/hydra-bot

max_forks_repo_name: defanor/hydra-bot


text:
module Control.Lens.Iso

import Control.Lens.Types
import Control.Monad.Identity
import Data.Profunctor

%default total

public export
data Exchange a b s t = MkExchange (s -> a) (b -> t)

public export
Functor (Exchange a b s) where
  map f (MkExchange sa bt) = MkExchange sa (f . bt)

public export
Profunctor (Exchange a b) where
  dimap f g (MkExchange sa bt) = MkExchange (sa . f) (g . bt)

  lmap f (MkExchange sa bt) = MkExchange (sa . f) bt

  rmap g (MkExchange sa bt) = MkExchange sa (g . bt)

public export
AnIso : Type -> Type -> Type -> Type -> Type
AnIso s t a b = Exchange a b a (Identity b) -> Exchange a b s (Identity t)

public export
AnIso' : Type -> Type -> Type
AnIso' = Simple AnIso

public export
iso : (s -> a) -> (b -> t) -> Iso s t a b
iso sa bt = dimap sa (map bt)

public export
withIso : AnIso s t a b -> ((s -> a) -> (b -> t) -> r) -> r
withIso ai k = case ai (MkExchange id Id) of
    MkExchange sa bt => k sa (runIdentity . bt)

public export
from : AnIso s t a b -> Iso b a t s
from l = withIso l $ \sa,bt => iso bt sa


text:
||| https://idris2.readthedocs.io/en/latest/ffi/ffi.html
module Main

import System.FFI

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

||| A pure foreign function.
%foreign (libsmall "add")
add : Int -> Int -> Int

||| An effectful foreign function.
%foreign (libsmall "addWithMessage")
prim__addWithMessage : String -> Int -> Int -> PrimIO Int

addWithMessage : HasIO io => String -> Int -> Int -> io Int
addWithMessage s x y = primIO $ prim__addWithMessage s x y

||| An effectful foreign function that takes a pure callback.
%foreign (libsmall "applyFn")
prim__applyFn : String -> Int -> (String -> Int -> String) -> PrimIO String

applyFn : HasIO io => String -> Int -> (String -> Int -> String) -> io String
applyFn c i f = primIO $ prim__applyFn c i f

||| An effectful foreign function that takes an effectful callback.
%foreign (libsmall "applyFn")
prim__applyFnIO :
  String -> Int -> (String -> Int -> PrimIO String) -> PrimIO String

applyFnIO : HasIO io =>
  String -> Int -> (String -> Int -> IO String) -> io String
applyFnIO c i f = primIO $ prim__applyFnIO c i (\s, i => toPrim $ f s i)

pluralise : String -> Int -> String
pluralise str x =
  show x ++ " " ++
    if x == 1
      then str
      else str ++ "s"

pluraliseIO : String -> Int -> IO String
pluraliseIO str x = pure (pluralise str x)

||| A static member of the dart:core library.
DateTime : Type
DateTime = Struct "DateTime,dart:core" [("hour", Int)]

%foreign "Dart:DateTime.parse,dart:core"
prim__parseDateTime : String -> PrimIO DateTime

namespace DateTime
  export
  parse : HasIO io => String -> io DateTime
  parse s = primIO $ prim__parseDateTime s

  export
  hour : DateTime -> Int
  hour dt = getField dt "hour"

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

%foreign (libsmall "Point")
prim__mkPoint : Int -> Int -> PrimIO Point

mkPoint : Int -> Int -> IO Point
mkPoint x y = primIO $ prim__mkPoint x y

%foreign "Dart:.moveTo"
prim__moveTo : Point -> Int -> Int -> PrimIO ()

%foreign "Dart:.accept"
prim__accept : Point -> (Point -> PrimIO ()) -> PrimIO ()

moveTo : HasIO io => Point -> Int -> Int -> io ()
moveTo p x y = primIO $ prim__moveTo p x y

accept : HasIO io => Point -> (Point -> IO ()) -> io ()
accept p c = primIO $ prim__accept p (\p => toPrim $ c p)

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

PaintingStyle : Type
PaintingStyle = Struct "PaintingStyle,./libsmall.dart" [("index", Int)]

namespace PaintingStyle
  export
  %foreign (libsmall "const PaintingStyle.fill")
  fill : PaintingStyle

  export
  %foreign (libsmall "const PaintingStyle.stroke")
  stroke : PaintingStyle

  export
  index : PaintingStyle -> Int
  index ps = getField ps "index"

main : IO ()
main = do
  printLn (add 70 24)
  addWithMessage "Sum" 70 24 >>= printLn
  applyFn "Biscuit" 10 pluralise >>= putStrLn
  applyFn "Tree" 1 pluralise >>= putStrLn
  applyFnIO "Biscuit" 10 pluraliseIO >>= putStrLn
  applyFnIO "Tree" 1 pluraliseIO >>= putStrLn

  -- Dart classes as records
  moonLanding <- DateTime.parse "1969-07-20 20:18:04Z"
  printLn (hour moonLanding)

  pt <- mkPoint 0 1
  printLn pt
  setField pt "x" (the Int 2)
  setField pt "y" (the Int 3)
  printLn pt
  accept pt (\pt => moveTo pt 4 5)
  printLn pt

  -- Dart enums
  printLn (index PaintingStyle.fill, index PaintingStyle.stroke)


text:
module Lens

import Data.List
import Data.Maybe
import Map

%default total

data PrimitiveValue =
      Boolean Bool
    | Number Nat
    | Text (List Char)

%name PrimitiveValue val, v, v1, v2

Eq PrimitiveValue where
    Boolean b1 == Boolean b2 = b1 == b2
    Number n1 == Number n2 = n1 == n2
    Text t1 == Text t2 = t1 == t2
    _ == _ = False

boolean : (v : PrimitiveValue) -> Maybe Bool
boolean (Boolean b) = Just b
boolean _ = Nothing

number : (v : PrimitiveValue) -> Maybe Nat
number (Number n) = Just n
number _ = Nothing

text : (v : PrimitiveValue) -> Maybe (List Char)
text (Text t) = Just t
text _ = Nothing

data PrimitiveKind =
      KBoolean
    | KNumber
    | KText

%name PrimitiveKind k, k1, k2

Eq PrimitiveKind where
    KBoolean == KBoolean = True
    KNumber == KNumber = True
    KText == KText = True
    _ == _ = False

prim_kind_of : PrimitiveValue -> PrimitiveKind
prim_kind_of (Boolean x) = KBoolean
prim_kind_of (Number x) = KNumber
prim_kind_of (Text x) = KText

data Value =
      Null
    | Primitive PrimitiveValue
    | Array (List Value)
    | Object (Map Value)

%name Value val, v, v1, v2

Eq Value where
    Null == Null = True
    Primitive v1 == Primitive v2 = v1 == v2
    Array vs1 == Array vs2 = assert_total (vs1 == vs2)
    Object ps1 == Object ps2 = assert_total (ps1 == ps2)
    _ == _ = False

prim : Value -> Maybe PrimitiveValue
prim (Primitive v) = Just v
prim _ = Nothing

array : Value -> Maybe (List Value)
array (Array xs) = Just xs
array _ = Nothing

object : Value -> Maybe (Map Value)
object (Object m) = Just m
object _ = Nothing

data Kind =
      KNull
    | KPrimitive PrimitiveKind
    | KArray
    | KObject

%name Kind k, k1, k2

Eq Kind where
    KNull == KNull = True
    KPrimitive k1 == KPrimitive k2 = k1 == k2
    KArray == KArray = True
    KObject == KObject = True
    _ == _ = False

data Schema =
      SNull
    | SBoolean
    | SNumber
    | SText
    | SArray Bool Schema
    | SObject (Map Schema)

%name Schema s, s1, s2

allow_empty : Schema -> Maybe Bool
allow_empty (SArray e _) = Just e
allow_empty _ = Nothing

sarray : Schema -> Maybe Schema
sarray (SArray _ s) = Just s
sarray _ = Nothing

mutual
    validate_properties' : List Key -> Map Value -> Map Schema -> Bool
    validate_properties' [] _ _ = True
    validate_properties' (k :: ks) vm sm with (get k vm, get k sm)
        validate_properties' (k :: ks) vm sm | (Just v, Just s) =
             assert_total (validate s v) && validate_properties' ks vm sm
        validate_properties' (k :: ks) vm sm | (_, _) = False

    validate_properties : Map Value -> Map Schema -> Bool
    validate_properties vm sm = validate_properties' (keys vm) vm sm

    validate : Schema -> Value -> Bool
    validate SNull Null = True
    validate SNull _ = False
    validate SBoolean (Primitive (Boolean _)) = True
    validate SBoolean _ = False
    validate SNumber (Primitive (Number _)) = True
    validate SNumber _ = False
    validate SText (Primitive (Text _)) = True
    validate SText _ = False
    validate (SArray e _) (Array []) = e
    validate (SArray _ s) (Array (x :: xs)) =
        assert_total (validate s) x && assert_total (validate (SArray True s) (Array xs))
    validate (SArray _ _) _ = False
    validate (SObject sm) (Object vm) =
        half_keys_eq sm vm && validate_properties vm sm
    validate (SObject _) _ = False

data Lens =
      Make Kind
    | Destroy Kind
    | AddProperty Key
    | RemoveProperty Key
    | RenameProperty Key Key
    | HoistProperty Key Key
    | PlungeProperty Key Key
    | Wrap
    | Head
    | LensIn Key Lens
    | LensMap Lens
    | Convert PrimitiveKind PrimitiveKind (List (PrimitiveValue, PrimitiveValue))

%name Lens lens, l, l1, l2

Eq Lens where
    Make k1 == Make k2 = k1 == k2
    Destroy k1 == Destroy k2 = k1 == k2
    AddProperty p1 == AddProperty p2 = p1 == p2
    RemoveProperty p1 == RemoveProperty p2 = p1 == p2
    RenameProperty a1 b1 == RenameProperty a2 b2 = a1 == a2 && b1 == b2
    HoistProperty h1 p1 == HoistProperty h2 p2 = h1 == h2 && p1 == p2
    PlungeProperty h1 p1 == PlungeProperty h2 p2 = h1 == h2 && p1 == p2
    Wrap == Wrap = True
    Head == Head = True
    LensIn p1 l1 == LensIn p2 l2 = p1 == p2 && l1 == l2
    LensMap l1 == LensMap l2 = l1 == l2
    Convert k11 k21 f1 == Convert k12 k22 f2 = k11 == k12 && k22 == k22 && f1 == f2
    _ == _ = False

flip_map : List (PrimitiveValue, PrimitiveValue) -> List (PrimitiveValue, PrimitiveValue)
flip_map [] = []
flip_map ((x, y) :: xs) = (y, x) :: (flip_map xs)

validate_map : PrimitiveKind -> PrimitiveKind -> List (PrimitiveValue, PrimitiveValue) -> Bool
validate_map _ _ [] = True
validate_map kx ky ((x, y) :: map) =
    prim_kind_of x == kx && prim_kind_of y == ky && validate_map kx ky map

convert_prim : PrimitiveValue -> List (PrimitiveValue, PrimitiveValue) -> Maybe PrimitiveValue
convert_prim _ [] = Nothing
convert_prim key ((k, v) :: xs) = if key == k then Just v else convert_prim key xs

reverse_lens : Lens -> Lens
reverse_lens (Make k) = Destroy k
reverse_lens (Destroy k) = Make k
reverse_lens (AddProperty x) = RemoveProperty x
reverse_lens (RemoveProperty x) = AddProperty x
reverse_lens (RenameProperty x y) = RenameProperty y x
reverse_lens (HoistProperty x y) = PlungeProperty x y
reverse_lens (PlungeProperty x y) = HoistProperty x y
reverse_lens Wrap = Head
reverse_lens Head = Wrap
reverse_lens (LensIn x y) = LensIn x (reverse_lens y)
reverse_lens (LensMap x) = LensMap (reverse_lens x)
reverse_lens (Convert a b m) = Convert b a (flip_map m)

strip_postfix : Eq a => List a -> List a -> (List a, List a)
strip_postfix (a::as) (b::bs) =
    if a == b
    then strip_postfix as bs
    else (a::as, b::bs)
strip_postfix a b = (a, b)

transform_lenses : List Lens -> List Lens -> List Lens
transform_lenses a b =
    let
        a = reverse a
        b = reverse b
        (a, b) = strip_postfix a b
        a = reverse a
        a = map reverse_lens a
    in a ++ b

transform_schema : Lens -> Schema -> Maybe Schema
transform_schema (Make (KPrimitive KBoolean)) SNull = Just SBoolean
transform_schema (Make (KPrimitive KNumber)) SNull = Just SNumber
transform_schema (Make (KPrimitive KText)) SNull = Just SText
transform_schema (Make KArray) SNull = Just (SArray True SNull)
transform_schema (Make KObject) SNull = Just (SObject Empty)
transform_schema (Make _) _ = Nothing
transform_schema (Destroy (KPrimitive KBoolean)) SBoolean = Just SNull
transform_schema (Destroy (KPrimitive KNumber)) SNumber = Just SNull
transform_schema (Destroy (KPrimitive KText)) SText = Just SNull
transform_schema (Destroy KArray) (SArray True SNull) = Just SNull
transform_schema (Destroy KObject) (SObject Empty) = Just SNull
transform_schema (Destroy KObject) (SObject _) = Nothing
transform_schema (Destroy _) _ = Nothing
transform_schema (AddProperty key) (SObject smap) =
    case get key smap of
        Just _ => Nothing
        Nothing => Just (SObject (insert key SNull smap))
transform_schema (AddProperty _) _ = Nothing
transform_schema (RemoveProperty key) (SObject smap) =
    case get key smap of
        Just SNull => Just (SObject (remove key smap))
        _ => Nothing
transform_schema (RemoveProperty _) _ = Nothing
transform_schema (RenameProperty x y) (SObject smap) =
    case (get x smap, get y smap) of
        (Just p, Nothing) =>
            let
                smap = (remove x smap)
                smap = (insert y p smap)
            in Just (SObject smap)
        _ => Nothing
transform_schema (RenameProperty _ _) _ = Nothing
transform_schema (HoistProperty h t) (SObject m) =
    case (get h m, get t m) of
        (Just (SObject hm), Nothing) =>
            case get t hm of
                Just p =>
                    let
                        hm = remove t hm
                        m = insert t p m
                        m = insert h (SObject hm) m
                     in Just (SObject m)
                Nothing => Nothing
        _ => Nothing
transform_schema (HoistProperty _ _) _ = Nothing
transform_schema (PlungeProperty h t) (SObject m) =
    case (get t m, get h m, t == h) of
        (Just p, Just (SObject hm), False) =>
            case get t hm of
                Nothing =>
                    let
                        hm = insert t p hm
                        m = remove t m
                        m = insert h (SObject hm) m
                    in Just (SObject m)
                _ => Nothing
        _ => Nothing
transform_schema (PlungeProperty _ _) _ = Nothing
transform_schema Wrap schema = Just (SArray False schema)
transform_schema Head (SArray False schema) = Just schema
transform_schema Head _ = Nothing
transform_schema (LensIn key lens) (SObject smap) =
    case get key smap of
        Just schema =>
            case transform_schema lens schema of
                Just schema => Just (SObject (insert key schema smap))
                Nothing => Nothing
        Nothing => Nothing
transform_schema (LensIn _ _) _ = Nothing
transform_schema (LensMap lens) (SArray allowEmpty schema) =
    case transform_schema lens schema of
        Just schema' => Just (SArray allowEmpty schema')
        Nothing => Nothing
transform_schema (LensMap _) _ = Nothing
transform_schema (Convert a b map) s with (validate_map a b map)
    transform_schema (Convert KBoolean KBoolean _) SBoolean | True = Just SBoolean
    transform_schema (Convert KBoolean KNumber _) SBoolean | True = Just SNumber
    transform_schema (Convert KBoolean KText _) SBoolean | True = Just SText
    transform_schema (Convert KNumber KBoolean _) SNumber | True = Just SBoolean
    transform_schema (Convert KNumber KNumber _) SNumber | True = Just SNumber
    transform_schema (Convert KNumber KText _) SNumber | True = Just SText
    transform_schema (Convert KText KBoolean _) SText | True = Just SBoolean
    transform_schema (Convert KText KNumber _) SText | True = Just SNumber
    transform_schema (Convert KText KText _) SText | True = Just SText
    transform_schema (Convert _ _ _) _ | _ = Nothing

lenses_to_schema : List Lens -> Maybe Schema
lenses_to_schema [] = Just SNull
lenses_to_schema (l::ls) =
    case lenses_to_schema ls of
        Just s => transform_schema l s
        Nothing => Nothing

transform_value : Lens -> Value -> Value
transform_value (Make KNull) _ = Null
transform_value (Make (KPrimitive KBoolean)) _ = Primitive (Boolean False)
transform_value (Make (KPrimitive KNumber)) _ = Primitive (Number 0)
transform_value (Make (KPrimitive KText)) _ = Primitive (Text [])
transform_value (Make KArray) _ = Array []
transform_value (Make KObject) _ = Object Empty
transform_value (Destroy _) _ = Null
transform_value (AddProperty k) (Object m) = Object (insert k Null m)
transform_value (AddProperty _) v = v
transform_value (RemoveProperty k) (Object m) = Object (remove k m)
transform_value (RemoveProperty _) v = v
transform_value (RenameProperty k1 k2) (Object m) =
    case get k1 m of
        Just v => Object (insert k2 v (remove k1 m))
        Nothing => Object m
transform_value (RenameProperty _ _) v = v
transform_value (HoistProperty h t) (Object m) =
    case get h m of
        Just (Object hm) =>
            case get t hm of
                Just v => Object (insert h (Object (remove t hm)) $ insert t v m)
                Nothing => Object m
        _ => Object m
transform_value (HoistProperty _ _) v = v
transform_value (PlungeProperty h t) (Object m) =
    case (get h m, get t m) of
        (Just (Object hm), Just v) => Object (insert h (Object (insert t v hm)) $ remove t m)
        _ => Object m
transform_value (PlungeProperty _ _) v = v
transform_value Wrap v = Array [v]
transform_value Head (Array (x :: _)) = x
transform_value Head v = v
transform_value (LensIn k l) (Object vm) =
    case get k vm of
        Just v => Object (insert k (transform_value l v) vm)
        Nothing => Object vm
transform_value (LensIn _ _) v = v
transform_value (LensMap l) (Array xs) = Array (map (transform_value l) xs)
transform_value (LensMap _) v = v
transform_value (Convert _ b m) (Primitive v) =
    case convert_prim v m of
        Just v => (Primitive v)
        Nothing => case b of
            KBoolean => Primitive (Boolean False)
            KNumber => Primitive (Number 0)
            KText => Primitive (Text [])
transform_value (Convert _ _ _) v = v

max_stars_repo_name: Actyx/cambria

max_issues_repo_name: Actyx/cambria

max_forks_repo_name: Actyx/cambria


text:
module BiNat.Properties.Induction

import BiNat
import BiNat.Properties.Plus

%access public export
%default total

composeFunctions : {T : BiNat -> Type} -> ((k : BiNat) -> T k -> T (succ k)) ->
  (m, n : BiNat) -> T m -> T (plus m n)
composeFunctions f m J         pm = replace (sym $ plusJIsSucc m) (f m pm)
composeFunctions f m (ns -: O) pm =
  replace {P = \z => T (plus m z)} (sym $ shiftLeftDoubles ns) $
  replace (sym $ plusAssociative m ns ns) $
  composeFunctions f (plus m ns) ns $
  composeFunctions f m ns pm
composeFunctions f m (ns -: I) pm =
  replace {P = \z => T z} (sym $ plusAssociative m J (ns -: O)) $
  replace {P = \z => T (plus (plus m J) z)} (sym $ shiftLeftDoubles ns) $
  replace {P = \z => T z} (sym $ plusAssociative (plus m J) ns ns) $
  composeFunctions f (plus (plus m J) ns) ns $
  composeFunctions f (plus m J) ns $
  replace (sym $ plusJIsSucc m) (f m pm)

induction : (P : BiNat -> Type) -> ((k : BiNat) -> P k -> P (succ k)) -> P J -> (n : BiNat) -> P n
induction prop step pj J         = pj
induction prop step pj (ns -: n) =
  replace (succOfPred (ns -: n) uninhabited) $
  replace (jPlusIsSucc (pred (ns -: n))) $
  composeFunctions step J (pred (ns -: n)) pj

max_stars_repo_name: SekiT/BiNat

max_issues_repo_name: SekiT/BiNat

max_forks_repo_name: SekiT/BiNat


text:
module Grid

import public Data.AVL.Set
import Data.AVL.Dict

%access public export

Point : Type
Point = (Int, Int)

%name Point point

addPoints : Point -> Point -> Point
addPoints (a, b) (c, d) = (a + c, b + d)

record Grid where
    constructor MkGrid
    leftX, topX, columnN, rowN : Int
    lifes : Set Point

%name Grid grid

inBounds : Point -> Grid -> Bool
inBounds (a, b) (MkGrid x y w h _) =
    x <= a && a < x + w && y <= b && b < y + h

containsLife : Point -> Grid -> Bool
containsLife point grid = contains point (lifes grid)

addLife : Point -> Grid -> Grid
addLife point grid =
    if inBounds point grid
       then record { lifes $= insert point } grid
       else grid

-- TODO figure out how to erase
removeLife : Point -> Grid -> Grid
removeLife point grid = record { lifes = difference (lifes grid) $ fromList [point] } grid

nextGeneration : Grid -> Grid
nextGeneration grid =
    let neighbourCounts = toList $ foldl accountLife empty $ lifes grid
        nextLifes = map fst $ filter checkLife neighbourCounts
    in record { lifes = fromList nextLifes } grid
  where
    neighbourCells : List Point
    neighbourCells = [(-1, -1), (0, -1), (1, -1),
                      (-1,  0),          (1,  0),
                      (-1,  1), (0,  1), (1,  1)]

    lifeNeighbours : Point -> List Point
    lifeNeighbours point = filter (flip inBounds grid) $ map (addPoints point) neighbourCells

    addNeighbour : Dict Point Nat -> Point -> Dict Point Nat
    addNeighbour dict point =
        case lookup point dict of
            Just count => insert point (count + 1) dict
            Nothing    => insert point          1  dict

    accountLife : Dict Point Nat -> Point -> Dict Point Nat
    accountLife dict point = foldl addNeighbour dict $ lifeNeighbours point

    checkLife : (Point, Nat) -> Bool
    checkLife (point, count) = count == 3 || (count == 2 && contains point (lifes grid))

max_stars_repo_name: artemohanjanyan/game-of-life

max_issues_repo_name: artemohanjanyan/game-of-life

max_forks_repo_name: artemohanjanyan/game-of-life


text:
module Ipkg.Lexer

import Data.String.Extra
import Text.Lexer

public export
data PkgToken
  = Comment String
  | Equals
  | Separator
  | Dot
  | Operator String
  | Space
  | StringLit String
  | Identifier String
  | NatLit Nat

public export
Show PkgToken where
  show (Comment x) = "Comment (\{x})"
  show Equals = "EQ"
  show Separator = "SEP"
  show Dot = "DOT"
  show (Operator x) = "Op(\{x})"
  show Space = "<space>"
  show (StringLit x) = "StrLit(\{x})"
  show (Identifier x) = "Id(\{x})"
  show (NatLit k) = "Nat(\{show k})"

operators : List String
operators = [">=", "<=", "==", "&&", ">", "<"]

oneOf' : List String -> Lexer
oneOf' = foldr (\x, y => exact x <|> y) fail

comment : Lexer
comment = lineComment $ exact "--"

ident : Lexer
ident = (alpha <|> is '_') <+> many (alpha <|> is '-' <|> is '_' <|> digit <|> is '.')

export
tokenMap : TokenMap PkgToken
tokenMap =
  [ (oneOf' operators, Operator)
  , (some (space <|> newline), const Space)
  , (comment, Comment)
  , (stringLit, StringLit . shrink 1)
  , (digits, NatLit . cast)
  , (ident, Identifier)
  , (is '.', const Dot)
  , (is ',', const Separator)
  , (is '=', const Equals)
  ]

max_stars_repo_name: claymager/ipkg-to-json

max_issues_repo_name: claymager/ipkg-to-json

max_forks_repo_name: claymager/ipkg-to-json


text:
module Drahko

import public Drahko.Builtins
import public Drahko.FFI

public export
drahko_version : String
drahko_version = "0.0.1"

max_stars_repo_name: NickSeagull/idris-autohotkey

max_issues_repo_name: NickSeagull/drahko

max_forks_repo_name: drahko/drahko


text:
module Data.List.Palindrome

import Data.List
import Data.List.Views
import Data.List.Views.Extra
import Data.List.Reverse
import Data.List.Equalities

%hide Prelude.reverse
%default total

||| Do geese see God?
public export
data Palindrome : (xs : List a) -> Type where
  Empty  : Palindrome []
  Single : Palindrome [_]
  Multi  : Palindrome xs -> Palindrome (x :: (xs `snoc` x))

||| A Palindrome reversed is itself.
export
palindromeReverse : (xs : List a) -> Palindrome xs -> reverse xs = xs
palindromeReverse [] Empty = Refl
palindromeReverse [_] Single = Refl
palindromeReverse ([x] ++ ys ++ [x]) (Multi pf) =
  rewrite reverseAppend ([x] ++ ys) [x] in
    rewrite reverseAppend [x] ys in
      rewrite palindromeReverse ys pf in
        Refl

private
reversePalindromeEqualsLemma
  : (x, x' : a)
  -> (xs : List a)
  -> reverse (x :: (xs ++ [x'])) = (x :: (xs ++ [x']))
  -> (reverse xs = xs, x = x')
reversePalindromeEqualsLemma x x' xs prf = equateInnerAndOuter flipHeadX
  where
    flipHeadX : reverse (xs ++ [x']) ++ [x] = x :: (xs ++ [x'])
    flipHeadX = rewrite (sym (reverseCons x (xs ++ [x']))) in prf
    flipLastX' : reverse (xs ++ [x']) = x :: xs -> (x' :: reverse xs) = (x :: xs)
    flipLastX' prf = rewrite (sym $ reverseAppend xs [x']) in prf
    cancelOuter : (reverse (xs ++ [x'])) = x :: xs -> reverse xs = xs
    cancelOuter prf = snd (consInjective (flipLastX' prf))
    equateInnerAndOuter
      : reverse (xs ++ [x']) ++ [x] = (x :: xs) ++ [x']
      -> (reverse xs = xs, x = x')
    equateInnerAndOuter prf =
      let (prf', xEqualsX') = snocInjective prf
       in (cancelOuter prf', xEqualsX')

||| Only Palindromes are equal to their own reverse.
export
reversePalindrome : (xs : List a) -> reverse xs = xs -> Palindrome xs
reversePalindrome input prf with (vList input)
  reversePalindrome [] _ | VNil = Empty
  reversePalindrome [x] _ | VOne = Single
  reversePalindrome (x :: (inner `snoc` y)) prf | VCons rec with (reversePalindromeEqualsLemma x y inner prf)
    reversePalindrome (x :: (inner `snoc` y)) prf | VCons rec | (revInnerIsIdentical, xIsY) =
      rewrite xIsY in
        Multi $ reversePalindrome inner revInnerIsIdentical | Force rec


text:
-- ----------------------------------------------------------------- [ Set.idr ]
-- Module    : Set.idr
-- Copyright : (c) 2015,2016 See CONTRIBUTORS.md
-- License   : see LICENSE
-- --------------------------------------------------------------------- [ EOH ]
||| Implementation of a Set using an AVL Binary Search Tree.
module Data.AVL.Set

import Data.AVL

%access export

-- ------------------------------------------------------------- [ Definitions ]
||| An ordered set.
data Set : (a : Type) -> Type where
  MkSet : {a : Type} -> AVLTree n a Unit -> Set a

||| Return a empty set.
empty : (Ord a) => Set a
empty = MkSet (Element Empty AVLEmpty)

||| Insert an element into a set.
insert : (Ord a) => a -> Set a -> Set a
insert a (MkSet m) = MkSet (snd $ AVL.API.insert a () m)

||| Does the set contain the given element.
contains : (Ord a) => a -> Set a -> Bool
contains a (MkSet m) = isJust (lookup a m)

||| Construct a set that contains all elements in both of the input sets.
union : (Ord a) => Set a -> Set a -> Set a
union (MkSet m1) (MkSet m2) = MkSet (snd $ AVL.API.foldr insertElement (_ ** m1) m2)
  where
    insertElement : (Ord a) => a
                            -> Unit
                            -> (h : Nat ** AVLTree h a Unit)
                            -> (h' : Nat ** AVLTree h' a Unit)
    insertElement k v m' = AVL.API.insert k v (snd m')

||| Return the size of the Dictionary.
size : Set a -> Nat
size (MkSet m) = AVL.API.size m

||| Construct a set that contains the elements from the first input
||| set but not the second.
|||
||| *Note* Not an efficient operation as we are constructing a new set
||| instead of modifying the right one.
difference : (Ord a) => Set a -> Set a -> Set a
difference (MkSet m1) s2 = AVL.API.foldr (\e,_,t => if (contains e s2) then t else Set.insert e t) empty $ m1

||| Construct a set that contains common elements of the input sets.
intersection : (Ord a) => Set a -> Set a -> Set a
intersection s1 s2 = difference s1 (difference s1 s2)

||| Construct a list using the given set.
toList : Set a -> List a
toList (MkSet m) = map fst $ AVL.API.toList m

||| Construct a set from the given list.
fromList : (Ord a) => List a -> Set a
fromList xs = (foldl (\t,k => Set.insert k t) empty xs)

-- --------------------------------------------------------- [ Implementations ]
Foldable Set where
  foldr f i (MkSet m) = foldr (\x,_,p => f x p) i m

Eq a => Eq (Set a) where
  (==) (MkSet (Element t _)) (MkSet (Element t' _)) = t == t'

Show a => Show (Set a) where
  show s = "{ " ++ (unwords . intersperse "," . map show . Set.toList $ s) ++ " }"

namespace Predicate

  export
  data Elem : (value : type) -> (set : Set type) -> Type where
    IsElem : (prf : HasKey value tree)
          -> Elem value (MkSet tree)

  private
  elemNotInSet : (prfIsNotElem : HasKey value tree -> Void) -> Elem value (MkSet tree) -> Void
  elemNotInSet prfIsNotElem (IsElem prf) = prfIsNotElem prf

  isElem : DecEq type
        => (value : type)
        -> (set   : Set type)
        -> Dec (Elem value set)
  isElem value (MkSet tree) with (isKey value tree)
    isElem value (MkSet tree) | (Yes prf) = Yes (IsElem prf)
    isElem value (MkSet tree) | (No prfIsNotElem) = No (elemNotInSet prfIsNotElem)

namespace Quantifier

  data All : (predicate : type -> Type) -> (set : Set type) -> Type where
    Satisfies : (prf : AllKeys p tree) -> All p (MkSet tree)

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

max_stars_repo_name: elba/idris-containers

max_issues_repo_name: elba/idris-containers

max_forks_repo_name: elba/idris-containers


text:
||| Testing IntMap using silly stupid tests
module Test.Patricia.Spec

import Patricia.IntMap
import Patricia.IntSet
import Specdris.Spec

----------------------------------------------------------------------------
-- Maps to test
----------------------------------------------------------------------------

initMap : Int32Map String
initMap = fromList [(1,"a"), (2,"b"), (3,"c"), (4, "d"), (4, "x")]

biggerMap : Int32Map String
biggerMap = insert 5 "e" initMap

lesserMap : Int32Map String
lesserMap = delete 10 $ delete 5 $ delete 2 biggerMap

----------------------------------------------------------------------------
-- Sets to test
----------------------------------------------------------------------------

initSet : Int32Set
initSet = fromList [1, 2, 3, 4, 4]

biggerSet : Int32Set
biggerSet = insert 5 initSet

lesserSet : Int32Set
lesserSet = delete 10 $ delete 5 $ delete 2 biggerSet

----------------------------------------------------------------------------
-- Test runner
----------------------------------------------------------------------------

export
main : IO ()
main = spec $ do
  describe "Patricia" $ do
    it "size" $ do
      size initMap   `shouldBe` 4
      size biggerMap `shouldBe` 5
      size lesserMap `shouldBe` 3
    it "lookup & insert & delete" $ do
      lookup 2 initMap   `shouldBe` Just "b"
      lookup 4 initMap   `shouldBe` Just "x"
      lookup 0 initMap   `shouldBe` Nothing
      lookup 5 biggerMap `shouldBe` Just "e"
      lookup 5 lesserMap `shouldBe` Nothing
      lookup 2 lesserMap `shouldBe` Nothing
      lookup 3 lesserMap `shouldBe` Just "c"
    it "toList" $ do
      values initMap   `shouldBe` ["a", "b", "c", "x"]
      values biggerMap `shouldBe` ["a", "b", "c", "x", "e"]
      values lesserMap `shouldBe` ["a", "c", "x"]
  describe "IntSet" $ do
    it "size" $ do
      size initSet   `shouldBe` 4
      size biggerSet `shouldBe` 5
      size lesserSet `shouldBe` 3
    it "member & insert & delete" $ do
      member 2 initSet   `shouldBe` True
      member 4 initSet   `shouldBe` True
      member 0 initSet   `shouldBe` False
      member 5 biggerSet `shouldBe` True
      member 5 lesserSet `shouldBe` False
      member 2 lesserSet `shouldBe` False
      member 3 lesserSet `shouldBe` True

max_stars_repo_name: ChShersh/idris-persistent-array

max_issues_repo_name: ChShersh/idris-patricia

max_forks_repo_name: ChShersh/idris-persistent-array


text:
module Idris.Resugar

import Core.Context
import Core.Context.Log
import Core.Env
import Core.Options

import Idris.Syntax

import TTImp.TTImp
import TTImp.TTImp.Functor
import TTImp.Unelab
import TTImp.Utils

import Data.List
import Data.List1
import Data.Maybe
import Data.String
import Libraries.Data.StringMap

%default covering

-- Convert checked terms back to source syntax. Note that this is entirely
-- for readability therefore there is NO GUARANTEE that the result will
-- type check (in fact it probably won't due to tidying up names for
-- readability).

unbracketApp : PTerm' nm -> PTerm' nm
unbracketApp (PBracketed _ tm@(PApp _ _ _)) = tm
unbracketApp tm = tm

-- TODO: Deal with precedences
mkOp : {auto s : Ref Syn SyntaxInfo} ->
       IPTerm -> Core IPTerm
mkOp tm@(PApp fc (PApp _ (PRef opFC kn) x) y)
    = do syn <- get Syn
         let n = rawName kn
         case StringMap.lookup (nameRoot n) (infixes syn) of
              Nothing => pure tm
              Just _ => pure (POp fc opFC kn (unbracketApp x) (unbracketApp y))
mkOp tm = pure tm

export
addBracket : FC -> PTerm' nm -> PTerm' nm
addBracket fc tm = if needed tm then PBracketed fc tm else tm
  where
    needed : PTerm' nm -> Bool
    needed (PBracketed _ _) = False
    needed (PRef _ _) = False
    needed (PPair _ _ _) = False
    needed (PDPair _ _ _ _ _) = False
    needed (PUnit _) = False
    needed (PComprehension _ _ _) = False
    needed (PList _ _ _) = False
    needed (PSnocList _ _ _) = False
    needed (PRange{}) = False
    needed (PRangeStream{}) = False
    needed (PPrimVal _ _) = False
    needed (PIdiom{}) = False
    needed (PBang{}) = False
    needed tm = True

bracket : {auto s : Ref Syn SyntaxInfo} ->
          (outer : Nat) -> (inner : Nat) ->
          IPTerm -> Core IPTerm
bracket outer inner tm
    = do tm' <- mkOp tm
         if outer > inner
            then pure (addBracket emptyFC tm')
            else pure tm'

startPrec : Nat
startPrec = 0

tyPrec : Nat
tyPrec = 1

appPrec : Nat
appPrec = 999

argPrec : Nat
argPrec = 1000

showImplicits : {auto c : Ref Ctxt Defs} ->
                Core Bool
showImplicits
    = do pp <- getPPrint
         pure (showImplicits pp)

showFullEnv : {auto c : Ref Ctxt Defs} ->
              Core Bool
showFullEnv
    = do pp <- getPPrint
         pure (showFullEnv pp)

fullNamespace : {auto c : Ref Ctxt Defs} ->
                Core Bool
fullNamespace
    = do pp <- getPPrint
         pure (fullNamespace pp)

unbracket : PTerm' nm -> PTerm' nm
unbracket (PBracketed _ tm) = tm
unbracket tm = tm

||| Attempt to extract a constant natural number
extractNat : Nat -> IPTerm -> Maybe Nat
extractNat acc tm = case tm of
  PRef _ (MkKindedName _ _ (NS ns (UN (Basic n)))) =>
    do guard (n == "Z")
       guard (ns == typesNS || ns == preludeNS)
       pure acc
  PApp _ (PRef _ (MkKindedName _ _ (NS ns (UN (Basic n))))) k => case n of
    "S" => do guard (ns == typesNS || ns == preludeNS)
              extractNat (1 + acc) k
    "fromInteger" => extractNat acc k
    _ => Nothing
  PPrimVal _ (BI n) => pure (acc + integerToNat n)
  PBracketed _ k    => extractNat acc k
  _                 => Nothing

mutual

  ||| Put the special names (Nil, ::, Pair, Z, S, etc) back as syntax
  ||| Returns `Nothing` in case there was nothing to resugar.
  sugarAppM : IPTerm -> Maybe IPTerm
  sugarAppM (PApp fc (PApp _ (PApp _ (PRef opFC (MkKindedName nt _ (NS ns nm))) l) m) r) =
    case nameRoot nm of
      "rangeFromThenTo" => pure $ PRange fc (unbracket l) (Just $ unbracket m) (unbracket r)
      _ => Nothing
  sugarAppM (PApp fc (PApp _ (PRef opFC (MkKindedName nt _ (NS ns nm))) l) r) =
    if builtinNS == ns
       then case nameRoot nm of
         "Pair"   => pure $ PPair fc (unbracket l) (unbracket r)
         "MkPair" => pure $ PPair fc (unbracket l) (unbracket r)
         "DPair"  => case unbracket r of
            PLam _ _ _ n _ r' => pure $ PDPair fc opFC n (unbracket l) (unbracket r')
            _                 => Nothing
         "Equal"  => pure $ PEq fc (unbracket l) (unbracket r)
         "==="    => pure $ PEq fc (unbracket l) (unbracket r)
         "~=~"    => pure $ PEq fc (unbracket l) (unbracket r)
         _        => Nothing
       else case nameRoot nm of
              "::" => case sugarApp (unbracket r) of
                PList fc nilFC xs => pure $ PList fc nilFC ((opFC, unbracketApp l) :: xs)
                _           => Nothing
              ":<" => case sugarApp (unbracket r) of
                        PSnocList fc nilFC xs => pure $ PSnocList fc nilFC
                                                  -- use a snoc list here in a future version
                                                  (xs ++ [(opFC, unbracketApp l)])
                        _                     => Nothing
              "rangeFromTo" => pure $ PRange fc (unbracket l) Nothing (unbracket r)
              "rangeFromThen" => pure $ PRangeStream fc (unbracket l) (Just $ unbracket r)

              _    => Nothing
  sugarAppM tm =
  -- refolding natural numbers if the expression is a constant
    case extractNat 0 tm of
      Just k  => pure $ PPrimVal (getPTermLoc tm) (BI (cast k))
      Nothing => case tm of
        PRef fc (MkKindedName nt _ (NS ns nm)) =>
          if builtinNS == ns
             then case nameRoot nm of
               "Unit"   => pure $ PUnit fc
               "MkUnit" => pure $ PUnit fc
               _           => Nothing
             else case nameRoot nm of
               "Nil" => pure $ PList fc fc []
               "Lin" => pure $ PSnocList fc fc []
               _     => Nothing
        PApp fc (PRef _ (MkKindedName nt _ (NS ns nm))) arg =>
          case nameRoot nm of
            "rangeFrom" => pure $ PRangeStream fc (unbracket arg) Nothing
            _           => Nothing
        _ => Nothing

  ||| Put the special names (Nil, ::, Pair, Z, S, etc.) back as syntax

  sugarApp : IPTerm -> IPTerm
  sugarApp tm = fromMaybe tm (sugarAppM tm)

export
sugarName : Name -> String
sugarName (MN n _) = "(implicit) " ++ n
sugarName (PV n _) = sugarName n
sugarName (DN n _) = n
sugarName x = show x

toPRef : FC -> KindedName -> Core IPTerm
toPRef fc kn@(MkKindedName nt fn nm) = case nm of
  MN n _     => pure (sugarApp (PRef fc (MkKindedName nt fn $ UN $ Basic n)))
  PV n _     => pure (sugarApp (PRef fc (MkKindedName nt fn $ n)))
  DN n _     => pure (sugarApp (PRef fc (MkKindedName nt fn $ UN $ Basic n)))
  Nested _ n => toPRef fc (MkKindedName nt fn n)
  _          => pure (sugarApp (PRef fc kn))

mutual
  toPTerm : {auto c : Ref Ctxt Defs} ->
            {auto s : Ref Syn SyntaxInfo} ->
            (prec : Nat) -> IRawImp -> Core IPTerm
  toPTerm p (IVar fc nm) = do
    t <- if fullNamespace !(getPPrint)
      then pure $ PRef fc nm
      else toPRef fc nm
    log "resugar.var" 70 $
      unwords [ "Resugaring", show @{Raw} nm.rawName, "to", show t]
    pure t
  toPTerm p (IPi fc rig Implicit n arg ret)
      = do imp <- showImplicits
           if imp
              then do arg' <- toPTerm tyPrec arg
                      ret' <- toPTerm tyPrec ret
                      bracket p tyPrec (PPi fc rig Implicit n arg' ret')
              else if needsBind n
                      then do arg' <- toPTerm tyPrec arg
                              ret' <- toPTerm tyPrec ret
                              bracket p tyPrec (PPi fc rig Implicit n arg' ret')
                      else toPTerm p ret
    where
      needsBind : Maybe Name -> Bool
      needsBind (Just nm@(UN (Basic t)))
          = let ret = map rawName ret
                ns = findBindableNames False [] [] ret
                allNs = findAllNames [] ret in
                (nm `elem` allNs) && not (t `elem` (map Builtin.fst ns))
      needsBind _ = False
  toPTerm p (IPi fc rig pt n arg ret)
      = do arg' <- toPTerm appPrec arg
           ret' <- toPTerm tyPrec ret
           pt' <- traverse (toPTerm argPrec) pt
           bracket p tyPrec (PPi fc rig pt' n arg' ret')
  toPTerm p (ILam fc rig pt mn arg sc)
      = do let n = case mn of
                        Nothing => UN Underscore
                        Just n' => n'
           imp <- showImplicits
           arg' <- if imp then toPTerm tyPrec arg
                          else pure (PImplicit fc)
           sc' <- toPTerm startPrec sc
           pt' <- traverse (toPTerm argPrec) pt
           let var = PRef fc (MkKindedName (Just Bound) n n)
           bracket p startPrec (PLam fc rig pt' var arg' sc')
  toPTerm p (ILet fc lhsFC rig n ty val sc)
      = do imp <- showImplicits
           ty' <- if imp then toPTerm startPrec ty
                         else pure (PImplicit fc)
           val' <- toPTerm startPrec val
           sc' <- toPTerm startPrec sc
           let var = PRef lhsFC (MkKindedName (Just Bound) n n)
           bracket p startPrec (PLet fc rig var ty' val' sc' [])
  toPTerm p (ICase fc sc scty [PatClause _ lhs rhs])
      = do sc' <- toPTerm startPrec sc
           lhs' <- toPTerm startPrec lhs
           rhs' <- toPTerm startPrec rhs
           bracket p startPrec
                   (PLet fc top lhs' (PImplicit fc) sc' rhs' [])
  toPTerm p (ICase fc sc scty alts)
      = do sc' <- toPTerm startPrec sc
           alts' <- traverse toPClause alts
           bracket p startPrec (mkIf (PCase fc sc' alts'))
    where
      mkIf : IPTerm -> IPTerm
      mkIf tm@(PCase loc sc [MkPatClause _ (PRef _ tval) t [],
                             MkPatClause _ (PRef _ fval) f []])
         = if dropNS (rawName tval) == UN (Basic "True")
           && dropNS (rawName fval) == UN (Basic "False")
              then PIfThenElse loc sc t f
              else tm
      mkIf tm = tm
  toPTerm p (ILocal fc ds sc)
      = do ds' <- traverse toPDecl ds
           sc' <- toPTerm startPrec sc
           bracket p startPrec (PLocal fc (mapMaybe id ds') sc')
  toPTerm p (ICaseLocal fc _ _ _ sc) = toPTerm p sc
  toPTerm p (IUpdate fc ds f)
      = do ds' <- traverse toPFieldUpdate ds
           f' <- toPTerm argPrec f
           bracket p startPrec (PApp fc (PUpdate fc ds') f')
  toPTerm p (IApp fc fn arg)
      = do arg' <- toPTerm argPrec arg
           app <- toPTermApp fn [(fc, Nothing, arg')]
           bracket p appPrec app
  toPTerm p (IAutoApp fc fn arg)
      = do arg' <- toPTerm argPrec arg
           app <- toPTermApp fn [(fc, Just Nothing, arg')]
           bracket p appPrec app
  toPTerm p (IWithApp fc fn arg)
      = do arg' <- toPTerm startPrec arg
           fn' <- toPTerm startPrec fn
           bracket p appPrec (PWithApp fc fn' arg')
  toPTerm p (INamedApp fc fn n arg)
      = do arg' <- toPTerm startPrec arg
           app <- toPTermApp fn [(fc, Just (Just n), arg')]
           imp <- showImplicits
           if imp
              then bracket p startPrec app
              else mkOp app
  toPTerm p (ISearch fc d) = pure (PSearch fc d)
  toPTerm p (IAlternative fc _ _) = pure (PImplicit fc)
  toPTerm p (IRewrite fc rule tm)
      = pure (PRewrite fc !(toPTerm startPrec rule)
                               !(toPTerm startPrec tm))
  toPTerm p (ICoerced fc tm) = toPTerm p tm
  toPTerm p (IPrimVal fc c) = pure (PPrimVal fc c)
  toPTerm p (IHole fc str) = pure (PHole fc False str)
  toPTerm p (IType fc) = pure (PType fc)
  toPTerm p (IBindVar fc v)
    = let nm = UN (Basic v) in
      pure (PRef fc (MkKindedName (Just Bound) nm nm))
  toPTerm p (IBindHere fc _ tm) = toPTerm p tm
  toPTerm p (IAs fc nameFC _ n pat) = pure (PAs fc nameFC n !(toPTerm argPrec pat))
  toPTerm p (IMustUnify fc r pat) = pure (PDotted fc !(toPTerm argPrec pat))

  toPTerm p (IDelayed fc r ty) = pure (PDelayed fc r !(toPTerm argPrec ty))
  toPTerm p (IDelay fc tm) = pure (PDelay fc !(toPTerm argPrec tm))
  toPTerm p (IForce fc tm) = pure (PForce fc !(toPTerm argPrec tm))
  toPTerm p (IQuote fc tm) = pure (PQuote fc !(toPTerm argPrec tm))
  toPTerm p (IQuoteName fc n) = pure (PQuoteName fc n)
  toPTerm p (IQuoteDecl fc ds)
      = do ds' <- traverse toPDecl ds
           pure $ PQuoteDecl fc (mapMaybe id ds')
  toPTerm p (IUnquote fc tm) = pure (PUnquote fc !(toPTerm argPrec tm))
  toPTerm p (IRunElab fc tm) = pure (PRunElab fc !(toPTerm argPrec tm))

  toPTerm p (IUnifyLog fc _ tm) = toPTerm p tm
  toPTerm p (Implicit fc True) = pure (PImplicit fc)
  toPTerm p (Implicit fc False) = pure (PInfer fc)

  toPTerm p (IWithUnambigNames fc ns rhs) =
    PWithUnambigNames fc ns <$> toPTerm startPrec rhs

  mkApp : {auto c : Ref Ctxt Defs} ->
          {auto s : Ref Syn SyntaxInfo} ->
          IPTerm ->
          List (FC, Maybe (Maybe Name), IPTerm) ->
          Core IPTerm
  mkApp fn [] = pure fn
  mkApp fn ((fc, Nothing, arg) :: rest)
      = do let ap = sugarApp (PApp fc fn arg)
           mkApp ap rest
  mkApp fn ((fc, Just Nothing, arg) :: rest)
      = do let ap = sugarApp (PAutoApp fc fn arg)
           mkApp ap rest
  mkApp fn ((fc, Just (Just n), arg) :: rest)
      = do imp <- showImplicits
           if imp
              then do let ap = PNamedApp fc fn n arg
                      mkApp ap rest
              else mkApp fn rest

  toPTermApp : {auto c : Ref Ctxt Defs} ->
               {auto s : Ref Syn SyntaxInfo} ->
               IRawImp -> List (FC, Maybe (Maybe Name), IPTerm) ->
               Core IPTerm
  toPTermApp (IApp fc f a) args
      = do a' <- toPTerm argPrec a
           toPTermApp f ((fc, Nothing, a') :: args)
  toPTermApp (INamedApp fc f n a) args
      = do a' <- toPTerm startPrec a
           toPTermApp f ((fc, Just (Just n), a') :: args)
  toPTermApp fn@(IVar fc n) args
      = do defs <- get Ctxt
           case !(lookupCtxtExact (rawName n) (gamma defs)) of
                Nothing => do fn' <- toPTerm appPrec fn
                              mkApp fn' args
                Just def => do fn' <- toPTerm appPrec fn
                               fenv <- showFullEnv
                               let args'
                                     = if fenv
                                          then args
                                          else drop (length (localVars def)) args
                               mkApp fn' args'
  toPTermApp fn args
      = do fn' <- toPTerm appPrec fn
           mkApp fn' args

  toPFieldUpdate : {auto c : Ref Ctxt Defs} ->
                   {auto s : Ref Syn SyntaxInfo} ->
                   IFieldUpdate' KindedName -> Core (PFieldUpdate' KindedName)
  toPFieldUpdate (ISetField p v)
      = do v' <- toPTerm startPrec v
           pure (PSetField p v')
  toPFieldUpdate (ISetFieldApp p v)
      = do v' <- toPTerm startPrec v
           pure (PSetFieldApp p v')

  toPClause : {auto c : Ref Ctxt Defs} ->
              {auto s : Ref Syn SyntaxInfo} ->
              ImpClause' KindedName -> Core (PClause' KindedName)
  toPClause (PatClause fc lhs rhs)
      = pure (MkPatClause fc !(toPTerm startPrec lhs)
                             !(toPTerm startPrec rhs)
                             [])
  toPClause (WithClause fc lhs rhs prf flags cs)
      = pure (MkWithClause fc !(toPTerm startPrec lhs)
                              !(toPTerm startPrec rhs)
                              prf
                              flags
                              !(traverse toPClause cs))
  toPClause (ImpossibleClause fc lhs)
      = pure (MkImpossible fc !(toPTerm startPrec lhs))

  toPTypeDecl : {auto c : Ref Ctxt Defs} ->
                {auto s : Ref Syn SyntaxInfo} ->
                ImpTy' KindedName -> Core (PTypeDecl' KindedName)
  toPTypeDecl (MkImpTy fc nameFC n ty)
      = pure (MkPTy fc nameFC n "" !(toPTerm startPrec ty))

  toPData : {auto c : Ref Ctxt Defs} ->
            {auto s : Ref Syn SyntaxInfo} ->
            ImpData' KindedName -> Core (PDataDecl' KindedName)
  toPData (MkImpData fc n ty opts cs)
      = pure (MkPData fc n !(toPTerm startPrec ty) opts
                   !(traverse toPTypeDecl cs))
  toPData (MkImpLater fc n ty)
      = pure (MkPLater fc n !(toPTerm startPrec ty))

  toPField : {auto c : Ref Ctxt Defs} ->
             {auto s : Ref Syn SyntaxInfo} ->
             IField' KindedName -> Core (PField' KindedName)
  toPField (MkIField fc c p n ty)
      = do ty' <- toPTerm startPrec ty
           p' <- traverse (toPTerm startPrec) p
           pure (MkField fc "" c p' n ty')

  toPRecord : {auto c : Ref Ctxt Defs} ->
              {auto s : Ref Syn SyntaxInfo} ->
              ImpRecord' KindedName ->
              Core ( Name
                   , List (Name, RigCount, PiInfo IPTerm, IPTerm)
                   , Maybe Name
                   , List (PField' KindedName))
  toPRecord (MkImpRecord fc n ps con fs)
      = do ps' <- traverse (\ (n, c, p, ty) =>
                                   do ty' <- toPTerm startPrec ty
                                      p' <- mapPiInfo p
                                      pure (n, c, p', ty')) ps
           fs' <- traverse toPField fs
           pure (n, ps', Just con, fs')
    where
      mapPiInfo : PiInfo IRawImp -> Core (PiInfo IPTerm)
      mapPiInfo Explicit        = pure   Explicit
      mapPiInfo Implicit        = pure   Implicit
      mapPiInfo AutoImplicit    = pure   AutoImplicit
      mapPiInfo (DefImplicit p) = pure $ DefImplicit !(toPTerm startPrec p)

  toPFnOpt : {auto c : Ref Ctxt Defs} ->
             {auto s : Ref Syn SyntaxInfo} ->
             FnOpt' KindedName -> Core (PFnOpt' KindedName)
  toPFnOpt (ForeignFn cs)
      = do cs' <- traverse (toPTerm startPrec) cs
           pure (PForeign cs')
  toPFnOpt o = pure $ IFnOpt o

  toPDecl : {auto c : Ref Ctxt Defs} ->
            {auto s : Ref Syn SyntaxInfo} ->
            ImpDecl' KindedName -> Core (Maybe (PDecl' KindedName))
  toPDecl (IClaim fc rig vis opts ty)
      = do opts' <- traverse toPFnOpt opts
           pure (Just (PClaim fc rig vis opts' !(toPTypeDecl ty)))
  toPDecl (IData fc vis d)
      = pure (Just (PData fc "" vis !(toPData d)))
  toPDecl (IDef fc n cs)
      = pure (Just (PDef fc !(traverse toPClause cs)))
  toPDecl (IParameters fc ps ds)
      = do ds' <- traverse toPDecl ds
           pure (Just (PParameters fc
                        !(traverse (\(n, rig, info, tpe) =>
                            do info' <- traverse (toPTerm startPrec) info
                               tpe' <- toPTerm startPrec tpe
                               pure (n, rig, info', tpe')) ps)
                (mapMaybe id ds')))
  toPDecl (IRecord fc _ vis r)
      = do (n, ps, con, fs) <- toPRecord r
           pure (Just (PRecord fc "" vis n ps con fs))
  toPDecl (INamespace fc ns ds)
      = do ds' <- traverse toPDecl ds
           pure (Just (PNamespace fc ns (mapMaybe id ds')))
  toPDecl (ITransform fc n lhs rhs)
      = pure (Just (PTransform fc (show n)
                                  !(toPTerm startPrec lhs)
                                  !(toPTerm startPrec rhs)))
  toPDecl (IRunElabDecl fc tm)
      = pure (Just (PRunElabDecl fc !(toPTerm startPrec tm)))
  toPDecl (IPragma _ _) = pure Nothing
  toPDecl (ILog _) = pure Nothing
  toPDecl (IBuiltin fc type name) = pure $ Just $ PBuiltin fc type name

export
cleanPTerm : {auto c : Ref Ctxt Defs} ->
             IPTerm -> Core IPTerm
cleanPTerm ptm
   = do ns <- fullNamespace
        if ns then pure ptm else mapPTermM cleanNode ptm

  where

    cleanName : Name -> Core Name
    cleanName nm = case nm of
      MN n _     => pure (UN $ mkUserName n) -- this may be "_"
      PV n _     => pure n
      DN n _     => pure (UN $ mkUserName n) -- this may be "_"
      NS _ n     => cleanName n
      Nested _ n => cleanName n
      UN n       => pure (UN n)
      _          => UN . mkUserName <$> prettyName nm

    cleanKindedName : KindedName -> Core KindedName
    cleanKindedName (MkKindedName nt fn nm) = MkKindedName nt fn <$> cleanName nm

    cleanBinderName : PiInfo IPTerm -> Name -> Core (Maybe Name)
    cleanBinderName AutoImplicit (UN (Basic "__con")) = pure Nothing
    cleanBinderName _ nm = Just <$> cleanName nm

    cleanNode : IPTerm -> Core IPTerm
    cleanNode (PRef fc nm)    =
      PRef fc <$> cleanKindedName nm
    cleanNode (POp fc opFC op x y) =
      (\ op => POp fc opFC op x y) <$> cleanKindedName op
    cleanNode (PPrefixOp fc opFC op x) =
      (\ op => PPrefixOp fc opFC op x) <$> cleanKindedName op
    cleanNode (PSectionL fc opFC op x) =
      (\ op => PSectionL fc opFC op x) <$> cleanKindedName op
    cleanNode (PSectionR fc opFC x op) =
      PSectionR fc opFC x <$> cleanKindedName op
    cleanNode (PPi fc rig vis (Just n) arg ret) =
      (\ n => PPi fc rig vis n arg ret) <$> cleanBinderName vis n
    cleanNode tm = pure tm

toCleanPTerm : {auto c : Ref Ctxt Defs} ->
               {auto s : Ref Syn SyntaxInfo} ->
               (prec : Nat) -> IRawImp -> Core IPTerm
toCleanPTerm prec tti = do
  ptm <- toPTerm prec tti
  cleanPTerm ptm

export
resugar : {vars : _} ->
          {auto c : Ref Ctxt Defs} ->
          {auto s : Ref Syn SyntaxInfo} ->
          Env Term vars -> Term vars -> Core IPTerm
resugar env tm
    = do tti <- unelab env tm
         toCleanPTerm startPrec tti

export
resugarNoPatvars : {vars : _} ->
                   {auto c : Ref Ctxt Defs} ->
                   {auto s : Ref Syn SyntaxInfo} ->
                   Env Term vars -> Term vars -> Core IPTerm
resugarNoPatvars env tm
    = do tti <- unelabNoPatvars env tm
         toCleanPTerm startPrec tti

export
pterm : {auto c : Ref Ctxt Defs} ->
        {auto s : Ref Syn SyntaxInfo} ->
        IRawImp -> Core IPTerm
pterm raw = toCleanPTerm startPrec raw


text:
module Main

import Data.Vect

%default total

data PowerSource = Petrol | Pedal

data Vehicle : PowerSource -> Type where
     Bicycle : Vehicle Pedal
     Car : (fuel : Nat) -> Vehicle Petrol
     Bus : (fuel : Nat) -> Vehicle Petrol

wheels : Vehicle power -> Nat
wheels Bicycle = 2
wheels (Car _) = 4
wheels (Bus _) = 4

refuel : Vehicle Petrol -> Vehicle Petrol
refuel (Car fuel) = Car 100
refuel (Bus _) = Bus 200

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

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

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

vectTake : (m : Fin n) -> Vect n a -> Vect (finToNat m) a
vectTake FZ (x :: xs) = []
vectTake (FS y) (x :: xs) = x :: vectTake y xs

sumEntries : Num a => (m : Fin n) -> Vect n a -> Vect n a -> a
sumEntries FZ (x :: xs) (y :: ys) = (x + y)
sumEntries (FS x) (y :: xs) (z :: ys) = (sumEntries x xs ys)

sumEntries' : Num a => (pos : Integer) -> Vect n a -> Vect n a -> Maybe a
sumEntries' {n} pos l1 l2 = case integerToFin pos n of
                            Nothing => Nothing
                            Just f => Just ((index f l1) + (index f l2))

main : IO ()
main = putStrLn (cast 'x')


text:
module Control.Monad.Ideal

%access public
%default total

data Ideal : (Type -> Type) -> Type -> Type where
  P : {f : Type -> Type} -> a -> Ideal f a
  I : {f : Type -> Type} -> (f a) -> Ideal f a

class Functor f => Mu' (f : Type -> Type) where
  mu' : f (Ideal f a) -> f a

instance Mu' f => Functor (Ideal f) where
  map g (P a) = P $ g a
  map g (I fa) = I $ map g fa

instance Mu' f => Applicative (Ideal f) where
  pure a = P a
  (P g) <$> x = map g x
  (I fg) <$> (P a) = I $ mu' $ map (\k => P $ k a) fg
  (I fg) <$> (I fa) = I $ mu' $ map (\k => I $ map k fa) fg

instance Mu' f => Monad (Ideal f) where
  (P a) >>= k = k a
  (I fa) >>= k = I $ mu' $ map k fa

max_stars_repo_name: seagull-kamome/idris-toy

max_issues_repo_name: seagull-kamome/idris-toy

max_forks_repo_name: seagull-kamome/idris-toy


text:
-- -------------------------------------------------------------- [ Lens.idr ]
-- Description : Idris port of Control.Lens
-- Copyright   : (c) Huw Campbell
-- --------------------------------------------------------------------- [ EOH ]
module Control.Lens.Getter
import Control.Lens.Types
import Control.Lens.Const
import Data.Contravariant
import Control.Lens.First
import Data.Profunctor

%default total

public export
view : Getting a s a -> s -> a
view l = getConst . applyMor (l (Mor MkConst))

public export
views : Getting a s a -> (a -> r) -> s -> r
views l f = f . view l

public export
foldMapOf : Getting r s a -> (a -> r) -> s -> r
foldMapOf l f = getConst . applyMor (l (Mor (MkConst . f)))

-- Creates a lens where the Functor instance must be
-- covariant. Practically this means we can only use
-- Const, so this is a valid getter and nothing else

||| Create a Getter from arbitrary functions `s -> a`.
public export
to : Contravariant f => (s -> a) -> LensLike' f s a
to k = dimap k (contramap k)

infixl 8 ^.
public export
(^.) : s -> Getting a s a -> a
a ^. l = view l a

infixl 8 ^?
public export
(^?) : s -> Getting (First a) s a -> Maybe a
s ^? l = getFirst (foldMapOf l (MkFirst . Just) s)

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