text:
module Commons.ST

import Control.ST

import Commons.Data.Action

%default total
%access public export

addIfResult : Type -> Action (Action RESULT ety Var)
addIfResult ty = Add (result Nil (\var => [var ::: ty]))

onAction : a -> a -> Action aty ety rty -> a
onAction x y Success    = x
onAction x y (Result _) = x
onAction x y (Error _)  = y

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

max_stars_repo_name: jfdm/idris-common

max_issues_repo_name: jfdm/idris-common

max_forks_repo_name: jfdm/idris-common


text:
-- Like SimpleRealizedFunction but uses data instead of record

module SimpleDataRealizedFunction

public export
data SimpleDataRealizedFunction : (a -> b) -> (cost : Integer) -> (quality : Double)
                                  -> Type where
  MkSimpleDataRealizedFunction : (f : a -> b) -> (cost : Integer) -> (quality : Double)
                                 -> SimpleDataRealizedFunction f cost quality

-- Perform the composition between 2 simple realized functions.  The
-- resulting realized function is formed as follows:
--
-- 1. Composed lifted functions
-- 2. Costs are added
-- public export
-- compose : (SimpleDataRealizedFunction (b -> c) g_cost g_q) ->
--           (SimpleDataRealizedFunction (a -> b) f_cost f_q) ->
--           (SimpleDataRealizedFunction (a -> c) (f_cost + g_cost) (min f_q g_q))
public export
compose : (SimpleDataRealizedFunction (b -> c) g_cost g_q) ->
          (SimpleDataRealizedFunction (a -> b) f_cost f_q) ->
          (SimpleDataRealizedFunction (a -> c) (f_cost + g_cost) (min f_q g_q))
compose (MkSimpleDataRealizedFunction f) (MkSimpleDataRealizedFunction g) =
  MkSimpleDataRealizedFunction (f . g)

-- Perform function application over realized functions.  Maybe we'd
-- want to used some funded data, as defined in FndType.
public export
apply : (SimpleDataRealizedFunction (a -> b) cost quality) -> a -> b
apply (MkSimpleDataRealizedFunction f) = f

ext: idr


text:
module Main

import Data.Vect

-- check that all functions are total
  %default total

zeroNotSuc : (0 = S k) -> Void
zeroNotSuc Refl impossible

sucNotZero : (S k = 0) -> Void
sucNotZero Refl impossible

noRec : (contra : (k=j)-> Void) -> (S k = S j) -> Void
noRec contra Refl = contra Refl

checkEqNat : (num1: Nat) -> (num2: Nat) -> Dec (num1 = num2)
checkEqNat Z Z = Yes Refl
checkEqNat Z (S k) = No zeroNotSuc
checkEqNat (S k) Z = No sucNotZero
checkEqNat (S k) (S j) = case checkEqNat k j of
  Yes prf => Yes (cong prf)
  No contra => No (noRec contra)

--noWhere : (contra: Elem value xs -> Void) -> Elem value (x::xs) -> Void

noWhere : (notThere: Elem value xs -> Void) -> (notHere: value = x -> Void) -> Elem value (x::xs) -> Void
noWhere notThere notHere Here = notHere Refl
noWhere notThere notHere (There later) = notThere later

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

isElem1 : DecEq a => (value: a) -> (xs: Vect n a) -> Dec (Elem value xs)
isElem1 value [] = No notInNil1
isElem1 value (x :: xs) = case decEq value x of
  Yes Refl => Yes Here
  No contra => case isElem1 value xs of
    Yes prof => Yes (There prof)
    No contra1 => No (noWhere contra1 contra)

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

data Elem1 : a -> List a -> Type where
  Here : Elem1 x (x::xs)
  There: (later: Elem1 x xs) -> Elem1 x (y :: ys)

data Last : List a -> a -> Type where
  LastOne : Last [value] value
  LastCons : (prf : Last xs value) -> Last (x :: xs) value

notInEmptyList : Last [] value -> Void
notInEmptyList LastOne impossible
notInEmptyList (LastCons _) impossible

notInLast : (contra: value = x -> Void) -> (Last [x] value) -> Void
notInLast contra LastOne = contra Refl
notInLast contra (LastCons prf) impossible

anotherContra : (contra : Last [] value) -> Void
anotherContra LastOne impossible
anotherContra (LastCons _) impossible

Uninhabited (Last [] a) where
  uninhabited LastOne impossible

notAnywhere : (contra: Last (x::xs) value -> Void) -> (Last (y::x::xs) value) -> Void
notAnywhere contra (LastCons prf) = contra prf

--notAnywhere contra LastOne = contra ?hole
--notAnywhere contra (LastCons prf) = contra prf

--notAnywhere contra LastOne = contra ?hole_2
--notAnywhere contra (LastCons prf) = contra prf

isLast : DecEq a => (xs : List a) -> (value : a) -> Dec (Last xs value)
isLast [] value = No notInEmptyList
isLast [x] value = case decEq value x of
       Yes Refl => Yes LastOne
       No contra => No (notInLast contra)
isLast (x :: y :: xs) value = case isLast (y :: xs) value of
  Yes prf => Yes (LastCons prf)
  No contra => No (notAnywhere contra)

-- game functions
removeElem_auto : (value: a) -> (xs: Vect (S n) a) -> {auto prf: Elem value xs} -> Vect n a
removeElem_auto value (value :: ys) {prf=Here} = ys
removeElem_auto {n = Z} value (y :: []) {prf=There later} =  absurd later
removeElem_auto {n = (S k)} value (y :: ys) {prf=There later} = y :: removeElem_auto value ys

data WordState : (guesses_remaing: Nat) -> (letters: Nat) -> Type where
  MkWordState: (word: String) -> (missing: Vect letters Char) -> WordState guessess_remaining letters

data Finished: Type where
  Lost: (game: WordState 0 (S letters)) -> Finished
  Won: (game: WordState (S guesses) 0) -> Finished

data ValidInput : List Char -> Type where
  Letter: (c: Char) -> ValidInput [c]

isValidNil : ValidInput [] -> Void
isValidNil (Letter _) impossible

isMoreChar : (ValidInput (c1::c2::cs)) -> Void
isMoreChar (Letter _) impossible

isValidInput : (cs: List Char) -> Dec (ValidInput cs)
isValidInput [] = No isValidNil
isValidInput (c::[]) = Yes (Letter c)
isValidInput (c1::c2::cs) = No isMoreChar

isValidString : (s: String) -> Dec (ValidInput (unpack s))
isValidString s = isValidInput (unpack s)

readGuess: IO (x**ValidInput x)
readGuess = do putStr "Guess"
               x <- getLine
               case isValidString (toUpper x) of
                 Yes prf => pure (_ ** prf)
                 No contra => do putStrLn "Invalid guess"
                                 readGuess
processGuess : (letter: Char) ->
  WordState (S guesses) (S letters) ->
  Either (WordState guesses (S letters)) (WordState (S guesses) letters)
processGuess letter (MkWordState word missing) = case isElem letter missing of
  Yes prf => Right (MkWordState word (removeElem_auto letter missing))
  No contra => Left (MkWordState word missing)

game : WordState (S guesses) (S letters) -> IO Finished
game {guesses} {letters} st = do
  (_ ** Letter letter) <- readGuess
  case processGuess letter st of
    Left l => do putStrLn "Wrong"
                 case guesses of
                   Z => pure (Lost l)
                   S k => game l
    Right r => do putStrLn "Right!"
                  case letters of
                    Z => pure (Won r)
                    S k => game r

max_stars_repo_name: gdevanla/idris-learn

max_issues_repo_name: gdevanla/idris-learn

max_forks_repo_name: gdevanla/idris-learn


text:
module Bimonad

import Bifunctor
import Biapplicative

infixl 4 >>==

||| Bimonads
||| @p the action of the first Bifunctor component on pairs of objects
||| @q the action of the second Bifunctor component on pairs of objects
interface (Biapplicative p, Biapplicative q) =>
      Bimonad (p : Type -> Type -> Type) (q : Type -> Type -> Type) where

  bijoin : (p (p a b) (q a b), q (p a b) (q a b)) -> (p a b, q a b)
  bijoin p = p >>== (id, id)

  (>>==) : (p a b, q a b) -> ((a -> p c d), (b -> q c d)) -> (p c d, q c d)
  (pab, qab) >>== (f, g) = bijoin $ (bimap f g, bimap f g) <<*>> (pab, qab)

biunit : (Bimonad p q) => a -> b -> (p a b, q a b)
biunit a b = (bipure a b, bipure a b)

implementation Bimonad Pair Pair where
  bijoin = bimap fst snd


text:
import Data.Vect
import Python
import Python.Lib.Numpy.Matrix

%default total

f : Nat -> Maybe (List Bool)
f Z = Just [True, False]
f (S n) = f n

xs : Matrix 3 4 DDouble
xs = array _
  [[1.0,-2.1, 3.3, -0.1]
  ,[3.5, 7.0, 0.0, -5.2]
  ,[0.5, 7.2,-1.1,  0.0]
  ]

ys : Matrix 6 2 DDouble
ys = reshape xs

zs : Matrix 4 3 DDouble
zs = reshape ys

main : PIO ()
main = do
  printLn' $ f 4
  printLn' xs
  printLn' ys
  printLn' zs
  -- printLn (ys `dot` zs)  -- won't work!
  printLn' (xs `dot` zs)
  printLn' (xs `dot` transpose xs)
  printLn' (transpose xs `dot` xs)
  printLn' $ 2 * transpose (zs `dot` xs) + fromDouble 0.2

max_stars_repo_name: ziman/idris-py

max_issues_repo_name: ziman/idris-py

max_forks_repo_name: ziman/idris-py


text:
module Issue1200

%default total

main : IO ()
main = traverse_ printLn $ do
  f <- [(1/), log, sin, cos, tan, asin, acos, atan, sqrt, floor, ceiling]
  x <- [-2,-1,-0.5,0,0.5,1,2]
  pure (f x)


text:
module Main

-- base
import Control.Monad.State
import Data.List
import Data.Nat
import Data.Vect
import System.File

-- contrib
import Data.SortedMap
import Text.Lexer
import Text.Lexer.Core
import Text.Parser
import Text.Parser.Core
import Text.Token

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

Resolution1D : Nat
Resolution1D = 10

Tiling : Type
Tiling = Vect Resolution1D $ Vect Resolution1D Bool

tilingOrientations : Tiling -> Vect 16 Tiling
tilingOrientations tiling = concat $ tilingRotations <$> tilingFlippings tiling where
  tilingFlippings : Tiling -> Vect 4 Tiling
  tilingFlippings tiling =
    [ tiling
    , reverse tiling
    , reverse <$> tiling
    , reverse <$> reverse tiling
    ]
  tilingRotations : Tiling -> Vect 4 Tiling
  tilingRotations tiling =
    [ tiling
    , rotate90 tiling
    , rotate90 $ rotate90 tiling
    , rotate90 $ rotate90 $ rotate90 tiling
    ] where
      rotate90 : Tiling -> Tiling
      rotate90 = reverse . transpose

record Tile where
  constructor MkTile
  id : Nat
  tiling : Tiling

Show Tile where
  show (MkTile id tiling) = "Tile " ++ show id ++ " " ++ show tiling

TilingMap : Type
TilingMap = SortedMap Nat Tiling

createTilingMap : List Tile -> TilingMap
createTilingMap = fromList . map f where
  f : Tile -> (Nat, Tiling)
  f (MkTile id tiling) = (id, tiling)

-- from square root of `length tiles`
Resolution1DImage : Nat
Resolution1DImage = 12

Arrangement : Type
Arrangement = Vect Resolution1DImage $ Vect Resolution1DImage $ Maybe Nat

nextCoordinate : {n : Nat} -> (x : Fin $ S n) -> Fin $ S n
nextCoordinate x with (strengthen x)
  nextCoordinate x | (Left y) = FZ
  nextCoordinate x | (Right y) = FS y

nextCoordinates : {n : Nat} ->
                  (x : Fin n) ->
                  (y : Fin n) ->
                  Maybe (Fin n, Fin n)
nextCoordinates x y with (n)
  nextCoordinates x y | Z = Nothing
  nextCoordinates x y | (S k) =
    if x == last
       then if y == last
               then Nothing
               else Just (FZ, nextCoordinate y)
       else Just (nextCoordinate x, nextCoordinate y)

data Direction = DirectionLeft
               | DirectionUp

neighborsToCheck : {n : Nat} ->
                   (x : Fin n) ->
                   (y : Fin n) ->
                   List ((Fin n, Fin n), Direction)
neighborsToCheck x y = [ ((pred x, y), DirectionUp), ((x, pred y), DirectionLeft) ] where
  pred : {n : Nat} -> (x : Fin n) -> Fin n
  pred FZ = last -- this is additional and not necessary, but allows returning Vect
  pred (FS k) = weaken k

neighborsToCheck' : (arrangement : Arrangement) ->
                    (x : Fin Resolution1DImage) ->
                    (y : Fin Resolution1DImage) ->
                    List (Nat, Direction)
neighborsToCheck' arrangement x y = do
  ((x', y'), d') <- neighborsToCheck x y
  let n = index x' $ index y' arrangement
  case n of
       Nothing => []
       Just n' => pure (n', d')

checkTiling : Direction -> (new : Tiling) -> (old : Tiling) -> Bool
checkTiling DirectionLeft new old = (index last <$> old) == (index FZ <$> new)
checkTiling DirectionUp new old = index last old == index FZ new

checkNeighbors : (tilingMap : TilingMap) ->
                 (new : Tiling) ->
                 List (Nat, Direction) ->
                 Bool
checkNeighbors tilingMap new [] = True
checkNeighbors tilingMap new ((n, d) :: xs) =
  case lookup n tilingMap of
       Nothing => ?keysShouldMatch
       Just old => if checkTiling d new old
                      then checkNeighbors tilingMap new xs
                      else False

checkNeighbors' : (tilingMap : TilingMap) ->
                  (arrangement : Arrangement) ->
                  (new : Tiling) ->
                  (x : Fin Resolution1DImage) ->
                  (y : Fin Resolution1DImage) ->
                  Bool
checkNeighbors' tilingMap arrangement new x y =
  checkNeighbors tilingMap new $ neighborsToCheck' arrangement x y

filterTilings : (tilingMap : TilingMap) ->
                (arrangement : Arrangement) ->
                (tilings : List (Nat, Tiling)) ->
                (x : Fin Resolution1DImage) ->
                (y : Fin Resolution1DImage) ->
                List (Nat, Tiling)
filterTilings tilingMap arrangement tilings x y =
  filter (\(_,t) => checkNeighbors' tilingMap arrangement t x y) tilings

tryTilings : (tilingMap : TilingMap) ->
             (arrangement : Arrangement) ->
             (x : Fin Resolution1DImage) ->
             (y : Fin Resolution1DImage) ->
             List Arrangement
tryTilings tilingMap arrangement x y = ?tryTilings_rhs where
  tilingsToTry : List (Nat, Tiling)
  tilingsToTry = do
    (n, t) <- Data.SortedMap.toList tilingMap
    t' <- toList $ tilingOrientations t
    pure (n, t')
  possibleTilings : List (Nat, Tiling)
  possibleTilings = filterTilings tilingMap arrangement tilingsToTry x y
  nextTry : (Nat, Tiling) -> List Arrangement
  nextTry (n, t) = case nextCoordinates x y of
                        Nothing => pure newArrangement
                        Just (x',y') => tryTilings newTilingMap newArrangement x' y'
                        where
                          newTilingMap : TilingMap
                          newTilingMap = insert n t tilingMap
                          newArrangement : Arrangement
                          newArrangement = replaceAt y (replaceAt x (Just n) $ index y arrangement) arrangement

findTilings : (tilingMap : TilingMap) ->
              List Arrangement
findTilings tilingMap = tryTilings tilingMap (pure $ pure Nothing) FZ FZ

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

namespace Parsing

  data DataKind = DKTile
                | DKSpace
                | DKNum
                | DKColon
                | DKNewline
                | DKDot
                | DKHash

  Eq DataKind where
    DKTile == DKTile = True
    DKSpace == DKSpace = True
    DKNum == DKNum = True
    DKColon == DKColon = True
    DKNewline == DKNewline = True
    DKDot == DKDot = True
    DKHash == DKHash = True
    _ == _ = False

  TokenKind DataKind where
    TokType DKNum = Nat
    TokType _ = ()
    tokValue DKNum x = integerToNat $ cast x
    tokValue DKTile _ = ()
    tokValue DKSpace _ = ()
    tokValue DKColon _ = ()
    tokValue DKNewline _ = ()
    tokValue DKDot _ = ()
    tokValue DKHash _ = ()

  tokenMap : TokenMap $ Token DataKind
  tokenMap = toTokenMap
    [ (digits, DKNum)
    , (is '.', DKDot)
    , (is '#', DKHash)
    , (exact "Tile", DKTile)
    , (newline, DKNewline)
    , (space, DKSpace)
    , (is ':', DKColon)
    ]

  countExactly : (n : Nat) -> (p : Grammar tok True a) -> Grammar tok (isSucc n) (Vect n a)
  countExactly Z p = Empty []
  countExactly (S k) p = [| p :: countExactly k p |]

  grammarTiles : Grammar (Token DataKind) True (List Tile)
  grammarTiles = sepBy1 (match DKNewline) grammarTile where
    grammarPixel : Grammar (Token DataKind) True Bool
    grammarPixel = match DKDot $> False <|> match DKHash $> True
    grammarTiling : Grammar (Token DataKind) True Tiling
    grammarTiling =
      countExactly Resolution1D $ countExactly Resolution1D grammarPixel <* match DKNewline
    grammarTile : Grammar (Token DataKind) True Tile
    grammarTile = do
      match DKTile
      match DKSpace
      id <- match DKNum
      match DKColon
      match DKNewline
      tiling <- grammarTiling
      pure $ MkTile id tiling

  export
  readData : String -> Maybe $ List Tile
  readData str = do
    let (tokens, debugLexed) = lex tokenMap str
        parsed = parse grammarTiles $ tok <$> tokens
    case parsed of
         Left _ => Nothing
         Right (rule, _) => Just rule

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

main : IO ()
main = do
  inputData <- readFile "./data"
  case inputData of
       Left err => print err
       Right dat => do
         case readData dat of
              Nothing => pure ()
              Just tiles => do
                let tilingMap = createTilingMap tiles
                print $ findTilings tilingMap
  pure ()


text:
module Compiler.Jvm.InferredType

import Data.String

public export
data InferredType = IBool | IByte | IChar | IShort | IInt | ILong | IFloat | IDouble | IRef String
                  | IArray InferredType | IVoid | IUnknown

export
Eq InferredType where
  IBool == IBool = True
  IByte == IByte = True
  IChar == IChar = True
  IShort == IShort = True
  IInt == IInt = True
  ILong == ILong = True
  IFloat == IFloat = True
  IDouble == IDouble = True
  (IRef ty1) == (IRef ty2) = ty1 == ty2
  (IArray elemTy1) == (IArray elemTy2) = elemTy1 == elemTy2
  IUnknown == IUnknown = True
  IVoid == IVoid = True
  _ == _ = False

export
Show InferredType where
    show IBool = "boolean"
    show IByte = "byte"
    show IChar = "char"
    show IShort = "short"
    show IInt = "int"
    show ILong = "long"
    show IFloat = "float"
    show IDouble = "double"
    show (IRef clsName) = clsName
    show (IArray elemTy) = "Array " ++ show elemTy
    show IUnknown = "unknown"
    show IVoid = "void"

export
inferredObjectType : InferredType
inferredObjectType = IRef "java/lang/Object"

%inline
public export
bigIntegerClass : String
bigIntegerClass = "java/math/BigInteger"

export
inferredBigIntegerType : InferredType
inferredBigIntegerType = IRef bigIntegerClass

%inline
public export
stringClass : String
stringClass = "java/lang/String"

export
inferredStringType : InferredType
inferredStringType = IRef stringClass

export
inferredLambdaType : InferredType
inferredLambdaType = IRef "java/util/function/Function"

export
function2Type : InferredType
function2Type = IRef "java/util/function/BiFunction"

export
getFunctionInterface : (arity: Nat) -> InferredType
getFunctionInterface 1 = inferredLambdaType
getFunctionInterface 2 = function2Type
getFunctionInterface arity = IRef ("io/github/mmhelloworld/idrisjvm/runtime/Function" ++ show arity)

%inline
public export
inferredForkJoinTaskType : InferredType
inferredForkJoinTaskType = IRef "java/util/concurrent/ForkJoinTask"

%inline
public export
arrayListClass : String
arrayListClass = "java/util/ArrayList"

%inline
public export
arrayListType : InferredType
arrayListType = IRef arrayListClass

%inline
public export
idrisSystemClass : String
idrisSystemClass = "io/github/mmhelloworld/idrisjvm/runtime/IdrisSystem"

%inline
public export
idrisListClass : String
idrisListClass = "io/github/mmhelloworld/idrisjvm/runtime/IdrisList"

export
idrisListType : InferredType
idrisListType = IRef idrisListClass

%inline
public export
idrisNilClass : String
idrisNilClass = "io/github/mmhelloworld/idrisjvm/runtime/IdrisList$Nil"

export
idrisNilType : InferredType
idrisNilType = IRef idrisNilClass

%inline
public export
idrisConsClass : String
idrisConsClass = "io/github/mmhelloworld/idrisjvm/runtime/IdrisList$Cons"

export
idrisConsType : InferredType
idrisConsType = IRef idrisConsClass

%inline
public export
idrisNothingClass : String
idrisNothingClass = "io/github/mmhelloworld/idrisjvm/runtime/Maybe$Nothing"

export
idrisNothingType : InferredType
idrisNothingType = IRef idrisNothingClass

%inline
public export
idrisJustClass : String
idrisJustClass = "io/github/mmhelloworld/idrisjvm/runtime/Maybe$Just"

export
idrisJustType : InferredType
idrisJustType = IRef idrisJustClass

%inline
public export
functionsClass : String
functionsClass = "io/github/mmhelloworld/idrisjvm/runtime/Functions"

export
isPrimitive : InferredType -> Bool
isPrimitive IBool = True
isPrimitive IByte = True
isPrimitive IChar = True
isPrimitive IShort = True
isPrimitive IInt = True
isPrimitive ILong = True
isPrimitive IFloat = True
isPrimitive IDouble = True
isPrimitive _ = False

%inline
public export
getRuntimeClass : String -> String
getRuntimeClass name = "io/github/mmhelloworld/idrisjvm/runtime/" ++ name

%inline
public export
intThunkClass : String
intThunkClass = getRuntimeClass "IntThunk"

%inline
public export
doubleThunkClass : String
doubleThunkClass = getRuntimeClass "DoubleThunk"

%inline
public export
longThunkClass : String
longThunkClass = getRuntimeClass "LongThunk"

%inline
public export
thunkClass : String
thunkClass = getRuntimeClass "Thunk"

export
intThunkType : InferredType
intThunkType = IRef intThunkClass

export
longThunkType : InferredType
longThunkType = IRef longThunkClass

export
doubleThunkType : InferredType
doubleThunkType = IRef doubleThunkClass

export
thunkType : InferredType
thunkType = IRef thunkClass

%inline
public export
delayedClass : String
delayedClass = getRuntimeClass "Delayed"

export
delayedType : InferredType
delayedType = IRef delayedClass

%inline
public export
idrisObjectClass : String
idrisObjectClass = getRuntimeClass "IdrisObject"

%inline
public export
arraysClass : String
arraysClass = getRuntimeClass "Arrays"

%inline
public export
refClass : String
refClass = getRuntimeClass "Ref"

export
refType : InferredType
refType = IRef refClass

export
idrisObjectType : InferredType
idrisObjectType = IRef idrisObjectClass

public export
isRefType : InferredType -> Bool
isRefType (IRef _) = True
isRefType _ = False

public export
Semigroup InferredType where
  IUnknown <+> ty2 = ty2
  ty1 <+> IUnknown = ty1
  ty1 <+> ty2 = if ty1 == ty2 then ty1 else inferredObjectType

%inline
public export
Monoid InferredType where
  neutral = IUnknown

export
stripInterfacePrefix : InferredType -> InferredType
stripInterfacePrefix (IRef className) =
    IRef $ if "i:" `isPrefixOf` className then substr 2 (length className) className else className
stripInterfacePrefix ty = ty

export
parse : String -> InferredType
parse "boolean" = IBool
parse "byte" = IByte
parse "char" = IChar
parse "short" = IShort
parse "int" = IInt
parse "long" = ILong
parse "float" = IFloat
parse "double" = IDouble
parse "String" = inferredStringType
parse "BigInteger" = inferredBigIntegerType
parse "void" = IVoid
parse className = IRef className

export
createExtPrimTypeSpec : InferredType -> String
createExtPrimTypeSpec IBool = "Bool"
createExtPrimTypeSpec IByte = "Byte"
createExtPrimTypeSpec IShort = "Short"
createExtPrimTypeSpec IInt = "Int"
createExtPrimTypeSpec IChar = "Char"
createExtPrimTypeSpec ILong = "long"
createExtPrimTypeSpec IFloat = "float"
createExtPrimTypeSpec IDouble = "Double"
createExtPrimTypeSpec (IArray ty) = "[" ++ createExtPrimTypeSpec ty
createExtPrimTypeSpec IVoid = "void"
createExtPrimTypeSpec IUnknown = createExtPrimTypeSpec inferredObjectType
createExtPrimTypeSpec (IRef ty) = ty

export
isObjectType : InferredType -> Bool
isObjectType IUnknown = True
isObjectType (IRef "java/lang/Object") = True
isObjectType _ = False


text:
module Data.These

%default total

public export
data These a b = This a | That b | Both a b

public export
fromEither : Either a b -> These a b
fromEither = either This That

public export
fromThis : These a b -> Maybe a
fromThis (This a) = Just a
fromThis (That _) = Nothing
fromThis (Both a _) = Just a

public export
fromThat : These a b -> Maybe b
fromThat (This _) = Nothing
fromThat (That b) = Just b
fromThat (Both _ b) = Just b

public export
these : (a -> c) -> (b -> c) -> (a -> b -> c) -> These a b -> c
these l r lr (This a)   = l a
these l r lr (That b)   = r b
these l r lr (Both a b) = lr a b

public export
swap : These a b -> These b a
swap (This a)   = That a
swap (That b)   = This b
swap (Both a b) = Both b a

public export
(Show a, Show b) => Show (These a b) where
  showPrec d (This x)   = showCon d "This" $ showArg x
  showPrec d (That x)   = showCon d "That" $ showArg x
  showPrec d (Both x y) = showCon d "Both" $ showArg x ++ showArg y

%inline
public export
Bifunctor These where
  bimap f g (This a)   = This (f a)
  bimap f g (That b)   = That (g b)
  bimap f g (Both a b) = Both (f a) (g b)

%inline
public export
Bifoldable These where
  bifoldr f _ acc (This a)   = f a acc
  bifoldr _ g acc (That b)   = g b acc
  bifoldr f g acc (Both a b) = f a (g b acc)

  bifoldl f _ acc (This a)   = f acc a
  bifoldl _ g acc (That b)   = g acc b
  bifoldl f g acc (Both a b) = g (f acc a) b

  binull _ = False

%inline
public export
Bitraversable These where
  bitraverse f _ (This a)   = This <$> f a
  bitraverse _ g (That b)   = That <$> g b
  bitraverse f g (Both a b) = [| Both (f a) (g b) |]

%inline
public export
Functor (These a) where
  map = mapSnd

public export
bifold : Monoid m => These m m -> m
bifold (This a)   = a
bifold (That b)   = b
bifold (Both a b) = a <+> b


text:
module lib.test.LibTest

import lib.Library
import System
import idristest.Suite

testDouble : (Bool, String)
testDouble = assertEq "Test double" (2 * 2) 4

testTriple : (Bool, String)
testTriple = assertNotEq "Test triple" (2 * 2 * 2) 5

testLibrary1 : (Bool, String)
testLibrary1 = assertEq "Test salute" salute "Hello, library example of idris"

testLibrary2 : (Bool, String)
testLibrary2 = assertNotEq "Test salute diff" salute "Ups"

export
test : IO Bool
test = runTests [testDouble, testTriple, testLibrary1, testLibrary2]


text:
module SearchOrder

%default total

interface De where
  f : Nat -> Nat

De where
  f = (+1)

g : De => Nat -> Nat
g x = f (x + 1)

[R] De where
  f = (+2)

ch1 : g 4 = 6
ch1 = Refl

-- Check that local is preferred to the global
ch2 : g @{R} 4 = 7
ch2 = Refl

max_stars_repo_name: buzden/idris-playground

max_issues_repo_name: buzden/idris-playground

max_forks_repo_name: buzden/idris-playground


text:
module Data.Time.LocalTime

import Data.So
import Data.Rational

import public Data.Time.LocalTime.TimeZone
import public Data.Time.LocalTime.TimeOfDay
import public Data.Time.LocalTime.CalendarDiffTime
import public Data.Time.LocalTime.Internal.LocalTime

import Data.Time.Calendar.Days
import Data.Time.Calendar.Gregorian
import Data.Time.Clock.DiffTime
import Data.Time.Clock.UTCTime
import Data.Time.Clock

%default total

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

||| addLocalTime a b = a + b
export addLocalTime : NominalDiffTime -> LocalTime -> LocalTime
addLocalTime x = utcToLocalTime utc . addUTCTime x . localTimeToUTC utc

||| diffLocalTime a b = a - b
export diffLocalTime : LocalTime -> LocalTime -> NominalDiffTime
diffLocalTime a b = diffUTCTime (localTimeToUTC utc a) (localTimeToUTC utc b)

||| Get the local time of a UT1 time on a particular meridian (in degrees, positive is East).
export ut1ToLocalTime : Rational -> UniversalTime -> Maybe LocalTime
ut1ToLocalTime long date = let
  localTime = date.modJulianDate + long / 360
  in do
    localMJD  <- floor localTime
    dt <- dayFractionToTimeOfDay (localTime - cast localMJD)
    pure $ MkLocalTime (ModifiedJulianDay localMJD) dt

||| Get the UT1 time of a local time on a particular meridian (in degrees, positive is East).
export localTimeToUT1 : Rational -> LocalTime -> UniversalTime
localTimeToUT1 long lt =
    ModJulianDate (fromInteger lt.localDay.modifiedJulianDay
                  + (timeOfDayToDayFraction lt.localTimeOfDay) - (long / 360))

public export
Show UniversalTime where
    show t = show (ut1ToLocalTime 0 t)

-- --------------------------------------------------------------------------
-- vim: tw=80 sw=2 expandtab :


text:
module MergeSort
import Data.List.Views as V

%hide merge
%hide sort
%default total

lteOrGte : (x, y : Nat) -> Either (LTE x y) (GTE x y)
lteOrGte Z _ = Left LTEZero
lteOrGte _ Z = Right LTEZero
lteOrGte (S k) (S j) with (lteOrGte k j)
    | (Left ltekj) = Left (LTESucc ltekj)
    | (Right gtekj) = Right (LTESucc gtekj)

notLTE : Not (LTE x y) -> LTE y x
notLTE {x = x} {y = y} contra with (lteOrGte x y)
    | (Left ltexy) = absurd (contra ltexy)
    | (Right gtexy) = gtexy

data Permutation : List a -> List a -> Type where
    PermNil : Permutation [] []
    PermCons : Permutation xs xs' -> Permutation (x::xs) (x::xs')
    PermSwap : Permutation (y::x::xs) (x::y::xs)
    PermTrans : Permutation xs ys -> Permutation ys zs -> Permutation xs zs

permRefl : Permutation xs xs
permRefl {xs = []} = PermNil
permRefl {xs = x :: xs} =
    PermCons (permRefl {xs = xs})

permSym : Permutation xs ys -> Permutation ys xs
permSym PermNil = PermNil
permSym (PermCons p) = PermCons (permSym p)
permSym PermSwap = PermSwap
permSym (PermTrans p1 p2) = PermTrans (permSym p2) (permSym p1)

permAppFront : Permutation xs xs' -> Permutation (ys ++ xs) (ys ++ xs')
permAppFront {ys = []} p = p
permAppFront {ys = (y :: ys)} p =
    PermCons (permAppFront p)

permAppBack : Permutation xs xs' -> Permutation (xs ++ ys) (xs' ++ ys)
permAppBack PermNil = permRefl
permAppBack (PermCons p) = PermCons (permAppBack p)
permAppBack PermSwap = PermSwap
permAppBack (PermTrans p1 p2) =
    let ih1 = permAppBack p1 in
    let ih2 = permAppBack p2 in
    PermTrans ih1 ih2

permAppComm : Permutation (xs ++ ys) (ys ++ xs)
permAppComm {xs = []} {ys = ys} =
    rewrite appendNilRightNeutral ys in
    permRefl
permAppComm {xs = (x :: xs)} {ys = []} =
    rewrite appendNilRightNeutral (x :: xs) in
    permRefl
permAppComm {xs = (x :: xs)} {ys = (y :: ys)} =
    let ih1 = permAppComm {xs = xs} {ys = ys} in
    let ih2 = permAppComm {xs = (x::xs)} {ys = ys} in
    let ih3 = permAppComm {xs = xs} {ys = (y::ys)} in
    PermTrans
        (PermCons (PermTrans ih3 (PermCons (permSym ih1))))
        (PermTrans PermSwap (PermCons ih2))

data All : (a -> Type) -> List a -> Type where
    AllNil : All p []
    AllCons : p x -> All p xs -> All p (x::xs)

allLTEtrans : LTE x y -> All (LTE y) ys -> All (LTE x) ys
allLTEtrans _ AllNil = AllNil
allLTEtrans ltexy (AllCons py allys) =
    AllCons (lteTransitive ltexy py) (allLTEtrans ltexy allys)

allAppend : All p xs -> All p ys -> All p (xs ++ ys)
allAppend AllNil pa = pa
allAppend (AllCons px allx) ally =
    AllCons px (allAppend allx ally)

allPerm : All p xs -> Permutation xs ys -> All p ys
allPerm _ PermNil = AllNil
allPerm (AllCons p1 all) (PermCons p2) = AllCons p1 (allPerm all p2)
allPerm (AllCons p1 (AllCons p2 all)) PermSwap = (AllCons p2 (AllCons p1 all))
allPerm allxs (PermTrans p1 p2) = allPerm (allPerm allxs p1) p2

data Ordered : List Nat -> Type where
    OrdNil : Ordered []
    OrdCons : Ordered xs -> All (\x => y `LTE` x) xs -> Ordered (y::xs)

orderedSingle : Ordered [x]
orderedSingle = OrdCons OrdNil AllNil

mergeLemma : All (LTE x) xs -> All (LTE y) ys -> LTE x y -> Permutation (xs ++ y::ys) zs ->
     All (LTE x) zs
mergeLemma xsltex ysltey ltexy p =
    let ysltex = allLTEtrans ltexy ysltey in
    let yssltex = AllCons ltexy ysltex in
    allPerm (allAppend xsltex yssltex) p

merge : (xs : List Nat) -> Ordered xs -> (ys : List Nat) -> Ordered ys ->
    (zs : List Nat ** (Ordered zs, Permutation (xs ++ ys) zs))
merge [] _ ys ordys =
    (ys ** (ordys, permRefl))
merge xs ordxs [] _ =
    rewrite appendNilRightNeutral xs in
    (xs ** (ordxs, permRefl))
merge (x::xs) (OrdCons ordxs p1) (y::ys) (OrdCons ordys p2) with (isLTE x y)
    | Yes ltexy =
        let (zs ** (ordzs, permzs)) = (merge xs ordxs (y::ys) (OrdCons ordys p2)) in
        let ordxzs = OrdCons ordzs (mergeLemma p1 p2 ltexy permzs) in
        (x::zs ** (ordxzs, PermCons permzs))
    | No contra =
        let (zs ** (ordzs, permzs)) = merge (x::xs) (OrdCons ordxs p1) ys ordys in
        let ordyzs = OrdCons ordzs (mergeLemma p2 p1 (notLTE contra) (PermTrans permAppComm permzs)) in
        let tmp = PermCons (PermTrans permAppComm permzs) in
        let permyzs = PermTrans (permAppComm {xs = (x::xs)}) tmp in
        (y::zs ** (ordyzs, permyzs))

mergeSortLemma : Permutation xs1 xs -> Permutation ys1 ys ->
    Permutation (xs ++ ys) zs -> Permutation (xs1 ++ ys1) zs
mergeSortLemma p1 p2 p =
    PermTrans (permAppFront p2) (PermTrans (permAppBack p1) p)

mergeSort : (xs : List Nat) -> (ys : List Nat ** (Ordered ys, Permutation xs ys))
mergeSort xs with (V.splitRec xs)
    mergeSort [] | SplitRecNil = ([] ** (OrdNil, permRefl))
    mergeSort [x] | SplitRecOne = ([x] ** (orderedSingle, permRefl))
    mergeSort (ys ++ zs) | SplitRecPair ysrec zsrec =
        let (rs1 ** (ordrs1, permrs1)) = (mergeSort ys | ysrec) in
        let (rs2 ** (ordrs2, permrs2)) = (mergeSort zs | zsrec) in
        let (rs ** (ordrs, permrs)) = merge rs1 ordrs1 rs2 ordrs2 in
        (rs ** (ordrs, mergeSortLemma permrs1 permrs2 permrs))


text:
module Algebra

import public Algebra.ZeroOneOmega
import public Algebra.Semiring
import public Algebra.Preorder

%default total

public export
RigCount : Type
RigCount = ZeroOneOmega

export
showCount : RigCount -> String
showCount = elimSemi "0 " "1 " (const "")


text:
{-
Idris
-}
module Main

record Language where
  constructor MkLanguage
  name: String

-- intentionally convoluted to avoid inlining
Idris : IO Language
Idris = pure $ MkLanguage "Idris"

main : IO ()
main = putStrLn $ name !Idris

max_stars_repo_name: timjs/iris-clean

max_issues_repo_name: timjs/iris-clean

max_forks_repo_name: timjs/iris-clean


text:
module DataType
import Data.Vect
%default total

data Expr : Type where
  Bind : String ->Expr
  Plus : Expr->Expr->Expr
  Cst : Double->Expr -- constant

expr1 : Expr
expr1 = Plus (Cst 3) $ Bind "x"

expr2 : Expr
expr2 = Plus (Cst 2) $ Plus (Cst 3) $ Bind "x"

expr3 : Expr
expr3 = Plus (Bind "x") $ Plus (Cst 3) $ Bind "x"

expr4 : Expr
expr4 = Plus (Bind "y") $ Plus (Cst 3) $ Bind "x"

numericDf : (Double->Double) -> Double ->Double
numericDf f x = ((f $ x+0.1) - f x )/0.1

--expression,varname
exp2f : Expr->String -> (Double->Double)
exp2f (Bind x) y = if (x==y) then (\x=>x) else (\_=>1.0)--err
exp2f (Plus x z) y = (\arg=>((exp2f x y) arg)*((exp2f z y) arg))
exp2f (Cst x) y = \_=>x

exp2vf : Expr->Vect n String -> (Vect n Double->Double)
exp2vf x [] _ =  1
exp2vf a (y :: xs) (z :: ys)= exp2f a y $ exp2vf a xs ys

-- f , x , x value
numericDiffExpr : Expr -> String -> Double -> Double
numericDiffExpr x y z = numericDf (exp2f x y) z

data Exp : Type->Type where
  Vf : Int->Exp a
  Adf : a -> a -> Exp a

Functor Exp where
  map func (Vf x) = Vf x
  map f (Adf x y) = Adf (f x) $ f y

e1 : Exp Int
e1 = Vf 1 -- Adf (Vf 1) (Vf 2)

isNil11 : List a -> Bool
isNil11 [] = True
isNil11 (x :: xs) = False

l1isNil11 : (\x=>True) Prelude.List.Nil = True
l1isNil11 = Refl

max_stars_repo_name: idris-industry/paradise

max_issues_repo_name: idris-industry/paradise

max_forks_repo_name: idris-industry/paradise


text:
module Quicksort

import Data.Vect

partitionVect :  Ord elem => {n : Nat} -> (elem) -> (Vect n elem) -> (l1 : Nat ** (l2 : Nat ** (n = (l1 + l2), (Vect l1 elem, Vect l2 elem))))
partitionVect pivot [] = (0 ** 0 ** (Refl, [], []))
partitionVect pivot (x :: xs) with (partitionVect pivot xs)
 partitionVect pivot (x :: xs) | (l1 ** l2 ** ( equality, v1, v2)) = if (x <= pivot) then (S (l1) ** l2 ** (cong {f = S} equality, (x :: v1), v2)) else
   (l1 ** S (l2) ** (trans (cong {f = S} equality) (plusSuccRightSucc l1 l2), v1, x :: v2))

nLTESn : (n : Nat) -> LTE n (S n)
nLTESn Z = LTEZero
nLTESn (S k) = LTESucc (nLTESn k)

-- type for a Preorder
data PreOrder : (a : Type) -> (a -> a -> Type)-> Type where
  PreOrd : {rel : a -> a -> Type} -> ((x : a) -> rel x x) -> ((x : a) -> (y : a) -> (z : a) -> rel x y -> rel y z -> rel x z) -> PreOrder a rel

-- type for a total order
data TotalOrder : (a : Type) -> (a -> a -> Type) -> Type where
  TotOrd : {rel : a -> a -> Type} -> PreOrder a rel -> ((x : a) -> (y : a) -> Either (rel y x) (rel x y)) -> TotalOrder a rel

-- type that states the proposition that a property is satisified by all elements of a list
data ForAll : (elem -> Type) -> List elem -> Type where
  None: ForAll p []
  Append: p x -> ForAll p xs -> ForAll p (x :: xs)

-- concatenation of lists obeys the propery forall
forAllConcat : (xs : List elem) -> (ForAll p xs) -> (ys : List elem) -> (ForAll p ys) -> (ForAll p (xs ++ ys))
forAllConcat [] None ys pfys = pfys
forAllConcat (x :: xs) (Append px pfxs) ys pfys = Append px (forAllConcat xs pfxs ys pfys)

-- splitting a list obeys the property forall
forAllBreak : (xs : List elem) -> (ys : List elem) -> (ForAll p (xs ++ ys)) -> (ForAll p xs, ForAll p ys)
forAllBreak [] ys pf = (None, pf)
forAllBreak (x :: xs) ys (Append px pfxs) = let (faxs, fays) = forAllBreak xs ys pfxs in (Append px faxs, fays)

-- mapping lists by a function obeys the forall property
forAllMap : (f : (x : elem) -> p x -> q x) -> (xs : List elem) -> ForAll p xs -> ForAll q xs
forAllMap f [] None = None
forAllMap f (x :: xs) (Append px pfxs) = Append (f x px) (forAllMap f xs pfxs)

-- transitive mapping obeys the forall property
forAllDobMap : (f : (x : elem) -> p x -> q x -> r x) -> (xs : List elem) -> ForAll p xs -> ForAll q xs -> ForAll r xs
forAllDobMap f [] None None = None
forAllDobMap f (x :: xs) (Append px pxs) (Append qx qxs) = Append (f x px qx) (forAllDobMap f xs pxs qxs)

-- type that proves that length of one list is LTE length of the other
data LTEforList : List elem -> List elem -> Type where
  LTEEmpty : LTEforList [] xs
  LTEAppend : LTEforList xs ys -> LTEforList (x :: xs) (y :: ys)

-- LTE for lists holds when an element is added to larger list
lemma1 : LTEforList xs ys -> LTEforList xs (y :: ys)
lemma1 LTEEmpty = LTEEmpty
lemma1 (LTEAppend pf) = LTEAppend (lemma1 pf)

-- LTE for lists holds reflexively
lemma2 : (xs : List elem) -> LTEforList xs xs
lemma2 [] = LTEEmpty
lemma2 (x :: xs) = LTEAppend (lemma2 xs)

-- LTE for lists is transitive
lemma3 : LTEforList xs ys -> LTEforList ys zs -> LTEforList xs zs
lemma3 LTEEmpty _ = LTEEmpty
lemma3 (LTEAppend pf1) (LTEAppend pf2) = LTEAppend (lemma3 pf1 pf2)

-- type for Sorted Lists
data IsSortedAlternate : (elem -> elem -> Type) -> List elem -> Type where
  EmptySorted : IsSortedAlternate rel []
  AppendSorted : {rel : elem -> elem -> Type} -> ForAll (rel x) xs -> IsSortedAlternate rel xs -> IsSortedAlternate rel (x :: xs)

-- type for Permutations
data Permutation : List elem -> List elem -> Type where
  Empty : Permutation [] []
  Split : (xs : List elem) -> (ys : List elem) -> (zs : List elem) -> Permutation xs (ys ++ zs) -> Permutation (x :: xs) (ys ++ (x :: zs))
  Compos : Permutation xs ys -> Permutation ys zs -> Permutation xs zs
  Cat : Permutation ws ys -> Permutation xs zs -> Permutation (ws ++ xs) (ys ++ zs)

-- Permutations follow the for all property
forAllPerm : (xs : List elem) -> ForAll p xs -> (ys : List elem) -> Permutation xs ys -> ForAll p ys
forAllPerm [] None [] Empty = None
forAllPerm (x :: xs) (Append px faxs) (ws ++ (x :: ys)) (Split xs ws ys pfperm) =
  let (faws,fays) = forAllBreak ws ys (forAllPerm xs faxs (ws ++ ys) pfperm) in forAllConcat ws faws (x :: ys) (Append px fays)
forAllPerm xs {p} pfxs zs (Compos {ys} permxsys permyszs) = forAllPerm ys (forAllPerm xs pfxs ys permxsys) zs permyszs
forAllPerm (ws ++ xs) pfwscatxs (ys ++ zs) (Cat pfwsys pfxszs) =
  let (pfws,pfxs) = (forAllBreak ws xs pfwscatxs) in forAllConcat ys (forAllPerm ws pfws ys pfwsys) zs (forAllPerm xs pfxs zs pfxszs)

-- function that partitions a list according to some function on the elements of the list
partitionFunc : {p : elem -> Type} -> {q : elem -> Type} -> (f : (x : elem) -> Either (p x) (q x)) ->
                (xs : List elem) -> (ys : List elem ** (zs : List elem ** (LTEforList ys xs,LTEforList zs xs , ForAll p ys, ForAll q zs, Permutation xs (ys ++ zs))))
partitionFunc f [] = ([] ** ([] ** (LTEEmpty, LTEEmpty, None, None, Empty)))
partitionFunc f (x :: xs) =
  let (ys ** (zs ** (ysltexs, zsltexs, pfys, pfzs, pfperm))) = partitionFunc f xs in
  case (f x) of
    (Left px) => ((x :: ys) ** (zs ** (LTEAppend ysltexs, lemma1 zsltexs, Append px pfys, pfzs, Split xs [] (ys ++ zs) pfperm)))
    (Right qx) => (ys ** ((x :: zs) ** (lemma1 ysltexs, LTEAppend zsltexs, pfys, Append qx pfzs, Split xs ys zs pfperm)))

-- function that partitions according to a total order, and gives a proof that
-- all elements of the first list are smaller than the pivot, pivot is smaller
-- than all elements of the second list, all elements of first list are smaller
-- than second list and the concatenation of the two lists is a permutation of the original list
ordPartition : TotalOrder elem rel -> (pivot : elem) ->
              (xs : List elem) -> (ys : List elem ** (zs : List elem ** (LTEforList ys xs, LTEforList zs xs, ForAll (flip rel pivot) ys, ForAll (rel pivot) zs,
              ForAll (\y => ForAll (rel y) zs) ys, Permutation xs (ys ++ zs))))
ordPartition {rel} (TotOrd (PreOrd refl transt) eith) pivot xs =
  let (ys ** (zs ** (ysltexs, zsltexs, pfys, pfzs, perm))) =
    partitionFunc {p = flip rel pivot} {q = rel pivot} (eith pivot) xs in
    (ys ** (zs ** (ysltexs, zsltexs, pfys, pfzs, lem2 zs pfzs ys pfys, perm)))
    where
      lem2 : (zs : List elem) -> ForAll (rel pivot) zs -> (ys : List elem) -> ForAll (flip rel pivot) ys -> ForAll (\y => ForAll (rel y) zs) ys
      lem2 zs xltzs = forAllMap (\y, yltx => lem y yltx zs xltzs)
        where
          lem : (y : elem) -> rel y pivot -> (zs : List elem) -> ForAll (rel pivot) zs -> ForAll (rel y) zs
          lem y yltx = forAllMap (\z ,xltz => transt y pivot z yltx xltz)

-- proof that the concatenation of the two elements obtained after partitioning
-- using the above function is a sorted list
partSorted : (xs : List elem) -> IsSortedAlternate rel xs -> (ys : List elem) -> IsSortedAlternate rel ys ->
              ForAll (\x => ForAll (rel x) ys) xs -> IsSortedAlternate rel (xs ++ ys)
partSorted [] _ ys sortys _ = sortys
partSorted (x :: xs) {rel} (AppendSorted xltxs sortxs) ys sortys (Append xltys xsltys) =
  AppendSorted xltxsys sortxsys
  where
    sortxsys : IsSortedAlternate rel (xs ++ ys)
    sortxsys = partSorted xs sortxs ys sortys xsltys
    xltxsys :  ForAll (rel x) (xs ++ ys)
    xltxsys = forAllConcat xs xltxs ys xltys

-- auxiliary function used to define quicksort
quicksortAux : TotalOrder elem rel -> (xs : List elem) -> (listBound : List elem) -> (xsbdd : LTEforList xs listBound) ->
                (ys : List elem ** (IsSortedAlternate rel ys, Permutation xs ys))
quicksortAux totorder [] _ _ = ([] ** (EmptySorted, Empty))
quicksortAux {rel} totorder (x :: xs) (xB :: xsB) (LTEAppend xsbdd) =
  --partition
  let (ys ** (zs ** (ysSmall, zsSmall, ysltx, xltzs, ysltzs, perm))) = ordPartition totorder x xs in
  --recursive calls
  let (ys' ** (sortedys', permysys')) = quicksortAux totorder ys xsB (lemma3 ysSmall xsbdd) in
  let (zs' ** (sortedzs', permzszs')) = quicksortAux totorder zs xsB (lemma3 zsSmall xsbdd) in
  --proof that result list is sorted
  let ysltzs' : ForAll (\y => ForAll (rel y) zs') ys
              = forAllMap (\y, yltzs => forAllPerm zs yltzs zs' permzszs') ys ysltzs in
  let ys'ltzs' : ForAll (\y => ForAll (rel y) zs') ys'
                = forAllPerm ys ysltzs' ys' permysys' in
  let ys'ltx : ForAll (flip rel x) ys'
              = forAllPerm ys ysltx ys' permysys' in
  let ys'ltxzs' : ForAll (\y => ForAll (rel y) (x :: zs')) ys'
                  = forAllDobMap (\y => Append) ys' ys'ltx ys'ltzs' in
  let sortedxzs' : IsSortedAlternate rel (x :: zs')
                    = AppendSorted (forAllPerm zs xltzs zs' permzszs') sortedzs' in
  let sortedys'xzs' : IsSortedAlternate rel (ys' ++ x :: zs')
                      = partSorted ys' sortedys' (x :: zs') sortedxzs' ys'ltxzs' in
  -- proof that result is a Permutation
  let perm' : Permutation (ys ++ zs) (ys' ++ zs')
              = Cat permysys' permzszs' in
  let perm'' : Permutation xs (ys' ++ zs')
              = Compos perm perm' in
  let permAll : Permutation (x :: xs) (ys' ++ x :: zs')
              = Split xs ys' zs' perm'' in
  --merging everything together
  ((ys' ++ (x :: zs')) ** (sortedys'xzs', permAll))

-- the quicksort funtion
quickSort : TotalOrder elem rel -> (xs : List elem) -> (ys : List elem ** (IsSortedAlternate rel ys, Permutation xs ys))
quickSort totorder xs = quicksortAux totorder xs xs (lemma2 xs)

--Applying to Nat
reflLTE : (n: Nat) -> LTE n n
reflLTE Z = LTEZero
reflLTE (S k) = LTESucc (reflLTE k)

natLTETrans : (a,b,c : Nat) -> LTE a b -> LTE b c -> LTE a c
natLTETrans Z _ _ _ _ = LTEZero
natLTETrans (S a) (S b) (S c) (LTESucc p) (LTESucc q) = LTESucc (natLTETrans a b c p q)

natLTEEith : (a, b : Nat) -> Either (LTE b a) (LTE a b)
natLTEEith Z _ = Right LTEZero
natLTEEith _ Z = Left LTEZero
natLTEEith (S n) (S m) with (natLTEEith n m)
  | Right x = Right (LTESucc x)
  | Left y = Left (LTESucc y)

totOrdNat : TotalOrder Nat LTE
totOrdNat = TotOrd (PreOrd reflLTE natLTETrans) natLTEEith

quickSortNat : (xs : List Nat) -> (ys : List Nat ** (IsSortedAlternate LTE ys, Permutation xs ys))
quickSortNat xs = quickSort totOrdNat xs


text:
module Core.Termination

import Core.CaseTree
import Core.Context
import Core.Context.Log
import Core.Env
import Core.Normalise
import Core.TT
import Core.Value

import Control.Monad.State

import Libraries.Data.NameMap
import Libraries.Data.SortedMap
import Data.List
import Data.String

%default covering

-- Check that the names a function refers to are terminating
totRefs : {auto c : Ref Ctxt Defs} ->
          Defs -> List Name -> Core Terminating
totRefs defs [] = pure IsTerminating
totRefs defs (n :: ns)
    = do rest <- totRefs defs ns
         Just d <- lookupCtxtExact n (gamma defs)
              | Nothing => pure rest
         case isTerminating (totality d) of
              IsTerminating => pure rest
              Unchecked => do
                log "totality" 20 $ "Totality unchecked for " ++ show !(toFullNames n)
                pure rest
              _ => case rest of
                          NotTerminating (BadCall ns)
                             => toFullNames $ NotTerminating (BadCall (n :: ns))
                          _ => toFullNames $ NotTerminating (BadCall [n])

totRefsIn : {auto c : Ref Ctxt Defs} ->
            Defs -> Term vars -> Core Terminating
totRefsIn defs ty = totRefs defs (keys (getRefs (Resolved (-1)) ty))

-- Check if all branches end up as constructor arguments, with no other
-- function application, and set 'AllGuarded' if so.
-- This is to check whether a function can be considered a constructor form
-- for the sake of termination checking (and might have other uses...)
export
checkIfGuarded : {auto c : Ref Ctxt Defs} ->
                 FC -> Name -> Core ()
checkIfGuarded fc n
    = do log "totality.termination.guarded" 6 $ "Check if Guarded: " ++ show !(toFullNames n)
         defs <- get Ctxt
         Just (PMDef _ _ _ _ pats) <- lookupDefExact n (gamma defs)
              | _ => pure ()
         t <- allGuarded pats
         when t $ setFlag fc n AllGuarded
  where
    guardedNF : {vars : _} -> Defs -> Env Term vars -> NF vars -> Core Bool
    guardedNF defs env (NDCon _ _ _ _ args) = pure True
    guardedNF defs env (NApp _ (NRef _ n) args)
        = do Just gdef <- lookupCtxtExact n (gamma defs)
                  | Nothing => pure False
             pure (AllGuarded `elem` flags gdef)
    guardedNF defs env _ = pure False

    checkNotFn : Defs -> Name -> Core Bool
    checkNotFn defs n
        = do Just gdef <- lookupCtxtExact n (gamma defs)
                  | Nothing => pure False
             case definition gdef of
                  DCon _ _ _ => pure True
                  _ => pure (multiplicity gdef == erased
                              || (AllGuarded `elem` flags gdef))

    guarded : {vars : _} -> Env Term vars -> Term vars -> Core Bool
    guarded env tm
        = do defs <- get Ctxt
             empty <- clearDefs defs
             tmnf <- nf empty env tm
             if !(guardedNF defs env tmnf)
                then do Just gdef <- lookupCtxtExact n (gamma defs)
                             | Nothing => pure False
                        allM (checkNotFn defs) (keys (refersTo gdef))
                else pure False

    allGuarded : List (vs ** (Env Term vs, Term vs, Term vs)) -> Core Bool
    allGuarded [] = pure True
    allGuarded ((_ ** (env, lhs, rhs)) :: ps)
        = if !(guarded env rhs)
             then allGuarded ps
             else pure False

-- Equal for the purposes of size change means, ignoring as patterns, all
-- non-metavariable positions are equal
scEq : Term vars -> Term vars -> Bool
scEq (Local _ _ idx _) (Local _ _ idx' _) = idx == idx'
scEq (Ref _ _ n) (Ref _ _ n') = n == n'
scEq (Meta _ _ i args) _ = True
scEq _ (Meta _ _ i args) = True
scEq (Bind _ _ b sc) (Bind _ _ b' sc') = False -- not checkable
scEq (App _ f a) (App _ f' a') = scEq f f' && scEq a a'
scEq (As _ _ a p) p' = scEq p p'
scEq p (As _ _ a p') = scEq p p'
scEq (TDelayed _ _ t) (TDelayed _ _ t') = scEq t t'
scEq (TDelay _ _ t x) (TDelay _ _ t' x') = scEq t t' && scEq x x'
scEq (TForce _ _ t) (TForce _ _ t') = scEq t t'
scEq (PrimVal _ c) (PrimVal _ c') = c == c'
scEq (Erased _ _) (Erased _ _) = True
scEq (TType _) (TType _) = True
scEq _ _ = False

data Guardedness = Toplevel | Unguarded | Guarded | InDelay

Show Guardedness where
  show Toplevel = "Toplevel"
  show Unguarded = "Unguarded"
  show Guarded = "Guarded"
  show InDelay = "InDelay"

-- Remove all force and delay annotations which are nothing to do with
-- coinduction meaning that all Delays left guard coinductive calls.
delazy : Defs -> Term vars -> Term vars
delazy defs (TDelayed fc r tm)
    = let tm' = delazy defs tm in
          case r of
               LInf => TDelayed fc r tm'
               _ => tm'
delazy defs (TDelay fc r ty tm)
    = let ty' = delazy defs ty
          tm' = delazy defs tm in
          case r of
               LInf => TDelay fc r ty' tm'
               _ => tm'
delazy defs (TForce fc r t)
    = case r of
           LInf => TForce fc r (delazy defs t)
           _ => delazy defs t
delazy defs (Meta fc n i args) = Meta fc n i (map (delazy defs) args)
delazy defs (Bind fc x b sc)
    = Bind fc x (map (delazy defs) b) (delazy defs sc)
delazy defs (App fc f a) = App fc (delazy defs f) (delazy defs a)
delazy defs (As fc s a p) = As fc s (delazy defs a) (delazy defs p)
delazy defs tm = tm

mutual
  findSC : {vars : _} ->
           {auto c : Ref Ctxt Defs} ->
           Defs -> Env Term vars -> Guardedness ->
           List (Nat, Term vars) -> -- LHS args and their position
           Term vars -> -- Right hand side
           Core (List SCCall)
  findSC {vars} defs env g pats (Bind fc n b sc)
       = pure $
            !(findSCbinder b) ++
            !(findSC defs (b :: env) g (map (\ (p, tm) => (p, weaken tm)) pats) sc)
    where
      findSCbinder : Binder (Term vars) -> Core (List SCCall)
      findSCbinder (Let _ c val ty) = findSC defs env g pats val
      findSCbinder b = pure [] -- only types, no need to look
  -- If we're Guarded and find a Delay, continue with the argument as InDelay
  findSC defs env Guarded pats (TDelay _ _ _ tm)
      = findSC defs env InDelay pats tm
  findSC defs env g pats (TDelay _ _ _ tm)
      = findSC defs env g pats tm
  findSC defs env g pats tm
      = do let (fn, args) = getFnArgs tm
           -- if it's a 'case' or 'if' just go straight into the arguments
           Nothing <- handleCase fn args
               | Just res => pure res
           fn' <- conIfGuarded fn -- pretend it's a data constructor if
                                  -- it has the AllGuarded flag
           case (g, fn', args) of
    -- If we're InDelay and find a constructor (or a function call which is
    -- guaranteed to return a constructor; AllGuarded set), continue as InDelay
             (InDelay, Ref fc (DataCon _ _) cn, args) =>
                 do scs <- traverse (findSC defs env InDelay pats) args
                    pure (concat scs)
             -- If we're InDelay otherwise, just check the arguments, the
             -- function call is okay
             (InDelay, _, args) =>
                 do scs <- traverse (findSC defs env Unguarded pats) args
                    pure (concat scs)
             (Guarded, Ref fc (DataCon _ _) cn, args) =>
                 do scs <- traverse (findSC defs env Guarded pats) args
                    pure (concat scs)
             (Toplevel, Ref fc (DataCon _ _) cn, args) =>
                 do scs <- traverse (findSC defs env Guarded pats) args
                    pure (concat scs)
             (_, Ref fc Func fn, args) =>
                 do logC "totality" 50 $
                       pure $ "Looking up type of " ++ show !(toFullNames fn)
                    Just ty <- lookupTyExact fn (gamma defs)
                         | Nothing => do
                              log "totality" 50 $ "Lookup failed"
                              findSCcall defs env Unguarded pats fc fn 0 args
                    arity <- getArity defs [] ty
                    findSCcall defs env Unguarded pats fc fn arity args
             (_, f, args) =>
                 do scs <- traverse (findSC defs env Unguarded pats) args
                    pure (concat scs)
      where
        handleCase : Term vars -> List (Term vars) -> Core (Maybe (List SCCall))
        handleCase (Ref fc nt n) args
            = do n' <- toFullNames n
                 if caseFn n'
                    then Just <$> findSCcall defs env g pats fc n 4 args
                    else pure Nothing
        handleCase _ _ = pure Nothing

        conIfGuarded : Term vars -> Core (Term vars)
        conIfGuarded (Ref fc Func n)
            = do defs <- get Ctxt
                 Just gdef <- lookupCtxtExact n (gamma defs)
                      | Nothing => pure $ Ref fc Func n
                 if AllGuarded `elem` flags gdef
                    then pure $ Ref fc (DataCon 0 0) n
                    else pure $ Ref fc Func n
        conIfGuarded tm = pure tm

  -- Expand the size change argument list with 'Nothing' to match the given
  -- arity (i.e. the arity of the function we're calling) to ensure that
  -- it's noted that we don't know the size change relationship with the
  -- extra arguments.
  expandToArity : Nat -> List (Maybe (Nat, SizeChange)) ->
                  List (Maybe (Nat, SizeChange))
  expandToArity Z xs = xs
  expandToArity (S k) (x :: xs) = x :: expandToArity k xs
  expandToArity (S k) [] = Nothing :: expandToArity k []

  -- Return whether first argument is structurally smaller than the second.
  smaller : Bool -> -- Have we gone under a constructor yet?
            Defs ->
            Maybe (Term vars) -> -- Asserted bigger thing
            Term vars -> -- Term we're checking
            Term vars -> -- Argument it might be smaller than
            Bool
  smaller inc defs big _ (Erased _ _) = False -- Never smaller than an erased thing!
  -- for an as pattern, it's smaller if it's smaller than either part
  smaller inc defs big s (As _ _ p t)
      = smaller inc defs big s p || smaller inc defs big s t
  smaller True defs big s t
      = s == t || smallerArg True defs big s t
  smaller inc defs big s t = smallerArg inc defs big s t

  assertedSmaller : Maybe (Term vars) -> Term vars -> Bool
  assertedSmaller (Just b) a = scEq b a
  assertedSmaller _ _ = False

  smallerArg : Bool -> Defs ->
               Maybe (Term vars) -> Term vars -> Term vars -> Bool
  smallerArg inc defs big (As _ _ _ s) tm = smallerArg inc defs big s tm
  smallerArg inc defs big s tm
        -- If we hit a pattern that is equal to a thing we've asserted_smaller,
        -- the argument must be smaller
      = assertedSmaller big tm ||
                case getFnArgs tm of
                     (Ref _ (DataCon t a) cn, args)
                         => any (smaller True defs big s) args
                     _ => case s of
                               App _ f _ => smaller inc defs big f tm
                                            -- Higher order recursive argument
                               _ => False

  -- if the argument is an 'assert_smaller', return the thing it's smaller than
  asserted : Name -> Term vars -> Maybe (Term vars)
  asserted aSmaller tm
       = case getFnArgs tm of
              (Ref _ nt fn, [_, _, b, _])
                   => if fn == aSmaller
                         then Just b
                         else Nothing
              _ => Nothing

  -- Calculate the size change for the given argument.
  -- i.e., return the size relationship of the given argument with an entry
  -- in 'pats'; the position in 'pats' and the size change.
  -- Nothing if there is no relation with any of them.
  mkChange : Defs -> Name ->
             (pats : List (Nat, Term vars)) ->
             (arg : Term vars) ->
             Maybe (Nat, SizeChange)
  mkChange defs aSmaller [] arg = Nothing
  mkChange defs aSmaller ((i, As _ _ p parg) :: pats) arg
      = mkChange defs aSmaller ((i, p) :: (i, parg) :: pats) arg
  mkChange defs aSmaller ((i, parg) :: pats) arg
      = cond [(scEq arg parg, Just (i, Same)),
              (smaller False defs (asserted aSmaller arg) arg parg, Just (i, Smaller))]
          (mkChange defs aSmaller pats arg)

  -- Given a name of a case function, and a list of the arguments being
  -- passed to it, update the pattern list so that it's referring to the LHS
  -- of the case block function and return the corresponding RHS.
  -- This way, we can build case blocks directly into the size change graph
  -- rather than treating the definitions separately.
  getCasePats : {auto c : Ref Ctxt Defs} ->
                {vars : _} ->
                Defs -> Name -> List (Nat, Term vars) ->
                List (Term vars) ->
                Core (Maybe (List (vs ** (Env Term vs,
                                         List (Nat, Term vs), Term vs))))
  getCasePats {vars} defs n pats args
      = do Just (PMDef _ _ _ _ pdefs) <- lookupDefExact n (gamma defs)
             | _ => pure Nothing
           log "totality" 20 $
             unwords ["Looking at the", show (length pdefs), "cases of", show  n]
           let pdefs' = map matchArgs pdefs
           logC "totality" 20 $ do
              old <- for pdefs $ \ (_ ** (_, lhs, rhs)) => do
                       lhs <- toFullNames lhs
                       rhs <- toFullNames rhs
                       pure $ "    " ++ show lhs ++ " => " ++ show rhs
              new <- for pdefs' $ \ (_ ** (_, lhs, rhs)) => do
                       lhs <- traverse (toFullNames . snd) lhs
                       rhs <- toFullNames rhs
                       pure $ "    " ++ show lhs ++ " => " ++ show rhs
              pure $ unlines $ "Updated" :: old ++ "  to:" :: new
           pure $ Just pdefs'

    where
      updateRHS : {vs, vs' : _} ->
                  List (Term vs, Term vs') -> Term vs -> Term vs'
      updateRHS {vs} {vs'} ms tm
          = case lookupTm tm ms of
                 Nothing => urhs tm
                 Just t => t
        where
          urhs : Term vs -> Term vs'
          urhs (Local fc _ _ _) = Erased fc False
          urhs (Ref fc nt n) = Ref fc nt n
          urhs (Meta fc m i margs) = Meta fc m i (map (updateRHS ms) margs)
          urhs (App fc f a) = App fc (updateRHS ms f) (updateRHS ms a)
          urhs (As fc s a p) = As fc s (updateRHS ms a) (updateRHS ms p)
          urhs (TDelayed fc r ty) = TDelayed fc r (updateRHS ms ty)
          urhs (TDelay fc r ty tm)
              = TDelay fc r (updateRHS ms ty) (updateRHS ms tm)
          urhs (TForce fc r tm) = TForce fc r (updateRHS ms tm)
          urhs (Bind fc x b sc)
              = Bind fc x (map (updateRHS ms) b)
                  (updateRHS (map (\vt => (weaken (fst vt), weaken (snd vt))) ms) sc)
          urhs (PrimVal fc c) = PrimVal fc c
          urhs (Erased fc i) = Erased fc i
          urhs (TType fc) = TType fc

          lookupTm : Term vs -> List (Term vs, Term vs') -> Maybe (Term vs')
          lookupTm tm [] = Nothing
          lookupTm (As fc s p tm) tms -- Want to keep the pattern and the variable,
                                      -- if there was an @ in the parent
              = do tm' <- lookupTm tm tms
                   Just $ As fc s tm' (urhs tm)
          lookupTm tm ((As fc s p tm', v) :: tms)
              = if tm == p
                   then Just v
                   else do tm' <- lookupTm tm ((tm', v) :: tms)
                           Just $ As fc s (urhs p) tm'
          lookupTm tm ((tm', v) :: tms)
              = if tm == tm'
                   then Just v
                   else lookupTm tm tms

      updatePat : {vs, vs' : _} ->
                  List (Term vs, Term vs') -> (Nat, Term vs) -> (Nat, Term vs')
      updatePat ms (n, tm) = (n, updateRHS ms tm)

      matchArgs : (vs ** (Env Term vs, Term vs, Term vs)) ->
                  (vs ** (Env Term vs, List (Nat, Term vs), Term vs))
      matchArgs (_ ** (env', lhs, rhs))
         = let patMatch = reverse (zip args (getArgs lhs)) in
               (_ ** (env', map (updatePat patMatch) pats, rhs))

  caseFn : Name -> Bool
  caseFn (CaseBlock _ _) = True
  caseFn (DN _ n) = caseFn n
  caseFn (NS _ n) = caseFn n
  caseFn _ = False

  findSCcall : {vars : _} ->
               {auto c : Ref Ctxt Defs} ->
               Defs -> Env Term vars -> Guardedness ->
               List (Nat, Term vars) ->
               FC -> Name -> Nat -> List (Term vars) ->
               Core (List SCCall)
  findSCcall defs env g pats fc fn_in arity args
        -- Under 'assert_total' we assume that all calls are fine, so leave
        -- the size change list empty
      = do Just gdef <- lookupCtxtExact fn_in (gamma defs)
                | Nothing => undefinedName fc fn_in
           let fn = fullname gdef
           log "totality.termination.sizechange" 10 $ "Looking under " ++ show !(toFullNames fn)
           aSmaller <- resolved (gamma defs) (NS builtinNS (UN $ Basic "assert_smaller"))
           cond [(fn == NS builtinNS (UN $ Basic "assert_total"), pure [])
                ,(caseFn fn,
                    do scs1 <- traverse (findSC defs env g pats) args
                       mps  <- getCasePats defs fn pats args
                       scs2 <- traverse (findInCase defs g) $ fromMaybe [] mps
                       pure (concat (scs1 ++ scs2)))
              ]
              (do scs <- traverse (findSC defs env g pats) args
                  pure ([MkSCCall fn
                           (expandToArity arity
                                (map (mkChange defs aSmaller pats) args))]
                           ++ concat scs))

  findInCase : {auto c : Ref Ctxt Defs} ->
               Defs -> Guardedness ->
               (vs ** (Env Term vs, List (Nat, Term vs), Term vs)) ->
               Core (List SCCall)
  findInCase defs g (_ ** (env, pats, tm))
     = do logC "totality" 10 $
                   do ps <- traverse toFullNames (map snd pats)
                      pure ("Looking in case args " ++ show ps)
          logTermNF "totality" 10 "        =" env tm
          rhs <- normaliseOpts tcOnly defs env tm
          findSC defs env g pats (delazy defs rhs)

findCalls : {auto c : Ref Ctxt Defs} ->
            Defs -> (vars ** (Env Term vars, Term vars, Term vars)) ->
            Core (List SCCall)
findCalls defs (_ ** (env, lhs, rhs_in))
   = do let pargs = getArgs (delazy defs lhs)
        rhs <- normaliseOpts tcOnly defs env rhs_in
        findSC defs env Toplevel
               (zip (take (length pargs) [0..]) pargs) (delazy defs rhs)

getSC : {auto c : Ref Ctxt Defs} ->
        Defs -> Def -> Core (List SCCall)
getSC defs (PMDef _ args _ _ pats)
   = do sc <- traverse (findCalls defs) pats
        pure $ nub (concat sc)
getSC defs _ = pure []

export
calculateSizeChange : {auto c : Ref Ctxt Defs} ->
                      FC -> Name -> Core (List SCCall)
calculateSizeChange loc n
    = do log "totality.termination.sizechange" 5 $ "Calculating Size Change: " ++ show !(toFullNames n)
         defs <- get Ctxt
         Just def <- lookupCtxtExact n (gamma defs)
              | Nothing => undefinedName loc n
         getSC defs (definition def)

Arg : Type
Arg = Int

data APos : Type where

firstArg : Arg
firstArg = 0

nextArg : Arg -> Arg
nextArg x = x + 1

initArgs : {auto a : Ref APos Arg} ->
           Nat -> Core (List (Maybe (Arg, SizeChange)))
initArgs Z = pure []
initArgs (S k)
    = do arg <- get APos
         put APos (nextArg arg)
         args' <- initArgs k
         pure (Just (arg, Same) :: args')

data Explored : Type where

-- Cached results of exploring the size change graph, so that if we visit a
-- node again, we don't have to re-explore the whole thing
SizeChanges : Type
SizeChanges = SortedMap (Name, List (Maybe Arg)) Terminating

-- Traverse the size change graph. When we reach a point we've seen before,
-- at least one of the arguments must have got smaller, otherwise it's
-- potentially non-terminating
checkSC : {auto a : Ref APos Arg} ->
          {auto c : Ref Ctxt Defs} ->
          {auto e : Ref Explored SizeChanges} ->
          Defs ->
          Name -> -- function we're checking
          List (Maybe (Arg, SizeChange)) -> -- functions arguments and change
          List (Name, List (Maybe Arg)) -> -- calls we've seen so far
          Core Terminating
checkSC defs f args path
   = do exp <- get Explored
        log "totality.termination.sizechange" 7 $ "Checking Size Change Graph: " ++ show !(toFullNames f)
        let pos = (f, map (map Builtin.fst) args)
        case lookup pos exp of
             Just done => pure done -- already explored this bit of tree
             Nothing =>
                if pos `elem` path
                   then do log "totality.termination.sizechange.inPath" 8 $ "Checking arguments: " ++ show !(toFullNames f)
                           res <- toFullNames $ checkDesc (mapMaybe (map Builtin.snd) args) path
                           put Explored (insert pos res exp)
                           pure res
                   else case !(lookupCtxtExact f (gamma defs)) of
                             Nothing => do log "totality.termination.sizechange.isTerminating" 8 $ "Size Change Graph is Terminating for: " ++ show !(toFullNames f)
                                           pure IsTerminating
                             Just def => do log "totality.termination.sizechange.needsChecking" 8 $ "Size Change Graph needs traversing: " ++ show !(toFullNames f)
                                            continue (sizeChange def) (pos :: path)
  where
    -- Look for something descending in the list of size changes
    checkDesc : List SizeChange -> List (Name, List (Maybe Arg)) -> Terminating
    checkDesc [] path = NotTerminating (RecPath (reverse (map fst path)))
    checkDesc (Smaller :: _) _ = IsTerminating
    checkDesc (_ :: xs) path = checkDesc xs path

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

    updateArg : SizeChange -> Maybe (Arg, SizeChange) -> Maybe (Arg, SizeChange)
    updateArg c Nothing = Nothing
    updateArg c arg@(Just (i, Unknown)) = arg
    updateArg Unknown (Just (i, _)) = Just (i, Unknown)
    updateArg c (Just (i, Same)) = Just (i, c)
    updateArg c arg = arg

    mkArgs : List (Maybe (Nat, SizeChange)) -> List (Maybe (Arg, SizeChange))
    mkArgs [] = []
    mkArgs (Nothing :: xs) = Nothing :: mkArgs xs
    mkArgs (Just (pos, c) :: xs)
        = case getPos args pos of
               Nothing => Nothing :: mkArgs xs
               Just arg => updateArg c arg :: mkArgs xs

    checkCall : List (Name, List (Maybe Arg)) -> SCCall -> Core Terminating
    checkCall path sc
        = do Just gdef <- lookupCtxtExact (fnCall sc) (gamma defs)
                  | Nothing => pure IsTerminating -- nothing to check
             let Unchecked = isTerminating (totality gdef)
                  | IsTerminating => pure IsTerminating
                  | _ => pure (NotTerminating (BadCall [fnCall sc]))
             log "totality.termination.sizechange.checkCall" 8 $
                "CheckCall Size Change Graph: " ++ show !(toFullNames (fnCall sc))
             term <- checkSC defs (fnCall sc) (mkArgs (fnArgs sc)) path
             let inpath = fnCall sc `elem` map fst path
             if not inpath
                then case term of
                       NotTerminating (RecPath _) =>
                          -- might have lost information while assuming this
                          -- was mutually recursive, so start again with new
                          -- arguments (that is, where we'd start if the
                          -- function was the top level thing we were checking)
                          do log "totality.termination.sizechange.checkCall.inPathNot.restart" 9 $ "ReChecking Size Change Graph: " ++ show !(toFullNames (fnCall sc))
                             args' <- initArgs (length (fnArgs sc))
                             t <- checkSC defs (fnCall sc) args' path
                             setTerminating emptyFC (fnCall sc) t
                             pure t
                       t => do log "totality.termination.sizechange.checkCall.inPathNot.return" 9 $ "Have result: " ++ show !(toFullNames (fnCall sc))
                               pure t
                else do log "totality.termination.sizechange.checkCall.inPath" 9 $ "Have Result: " ++ show !(toFullNames (fnCall sc))
                        pure term

    getWorst : Terminating -> List Terminating -> Terminating
    getWorst term [] = term
    getWorst term (IsTerminating :: xs) = getWorst term xs
    getWorst term (Unchecked :: xs) = getWorst Unchecked xs
    getWorst term (bad :: xs) = bad

    continue : List SCCall -> List (Name, List (Maybe Arg)) -> Core Terminating
    continue scs path
        = do allTerm <- traverse (checkCall path) scs
             pure (getWorst IsTerminating allTerm)

calcTerminating : {auto c : Ref Ctxt Defs} ->
                  FC -> Name -> Core Terminating
calcTerminating loc n
    = do defs <- get Ctxt
         log "totality.termination.calc" 7 $ "Calculating termination: " ++ show !(toFullNames n)
         case !(lookupCtxtExact n (gamma defs)) of
              Nothing => undefinedName loc n
              Just def =>
                case !(totRefs defs (nub !(addCases defs (keys (refersTo def))))) of
                     IsTerminating =>
                        do let ty = type def
                           a <- newRef APos firstArg
                           args <- initArgs !(getArity defs [] ty)
                           e <- newRef Explored empty
                           checkSC defs n args []
                     bad => pure bad
  where
    addCases' : Defs -> NameMap () -> List Name -> Core (List Name)
    addCases' defs all [] = pure (keys all)
    addCases' defs all (n :: ns)
        = case lookup n all of
             Just _ => addCases' defs all ns
             Nothing =>
               if caseFn !(getFullName n)
                  then case !(lookupCtxtExact n (gamma defs)) of
                            Just def => addCases' defs (insert n () all)
                                                  (keys (refersTo def) ++ ns)
                            Nothing => addCases' defs (insert n () all) ns
                  else addCases' defs (insert n () all) ns

    addCases : Defs -> List Name -> Core (List Name)
    addCases defs ns = addCases' defs empty ns

-- Check whether a function is terminating, and record in the context
export
checkTerminating : {auto c : Ref Ctxt Defs} ->
                   FC -> Name -> Core Terminating
checkTerminating loc n
    = do tot <- getTotality loc n
         log "totality.termination" 6 $ "Checking termination: " ++ show !(toFullNames n)
         case isTerminating tot of
              Unchecked =>
                 do tot' <- calcTerminating loc n
                    setTerminating loc n tot'
                    pure tot'
              t => pure t

nameIn : {auto c : Ref Ctxt Defs} ->
         Defs -> List Name -> NF [] -> Core Bool
nameIn defs tyns (NBind fc x b sc)
    = if !(nameIn defs tyns !(evalClosure defs (binderType b)))
         then pure True
         else do let nm = Ref fc Bound (MN ("NAMEIN_" ++ show x) 0)
                 let arg = toClosure defaultOpts [] nm
                 sc' <- sc defs arg
                 nameIn defs tyns sc'
nameIn defs tyns (NApp _ _ args)
    = anyM (nameIn defs tyns)
           !(traverse (evalClosure defs . snd) args)
nameIn defs tyns (NTCon _ n _ _ args)
    = if n `elem` tyns
         then pure True
         else do args' <- traverse (evalClosure defs . snd) args
                 anyM (nameIn defs tyns) args'
nameIn defs tyns (NDCon _ n _ _ args)
    = anyM (nameIn defs tyns)
           !(traverse (evalClosure defs . snd) args)
nameIn defs tyns _ = pure False

-- Check an argument type doesn't contain a negative occurrence of any of
-- the given type names
posArg  : {auto c : Ref Ctxt Defs} ->
          Defs -> List Name -> NF [] -> Core Terminating

posArgs : {auto c : Ref Ctxt Defs} ->
          Defs -> List Name -> List (Closure []) -> Core Terminating
posArgs defs tyn [] = pure IsTerminating
posArgs defs tyn (x :: xs)
  = do xNF <- evalClosure defs x
       logNF "totality.positivity" 50 "Checking parameter for positivity" [] xNF
       IsTerminating <- posArg defs tyn xNF
          | err => pure err
       posArgs defs tyn xs

-- a tyn can only appear in the parameter positions of
-- tc; report positivity failure if it appears anywhere else
posArg defs tyns nf@(NTCon loc tc _ _ args) =
  do logNF "totality.positivity" 50 "Found a type constructor" [] nf
     testargs <- case !(lookupDefExact tc (gamma defs)) of
                    Just (TCon _ _ params _ _ _ _ _) => do
                         log "totality.positivity" 50 $
                           unwords [show tc, "has", show (length params), "parameters"]
                         pure $ splitParams 0 params (map snd args)
                    _ => throw (GenericMsg loc (show tc ++ " not a data type"))
     let (params, indices) = testargs
     False <- anyM (nameIn defs tyns) !(traverse (evalClosure defs) indices)
       | True => pure (NotTerminating NotStrictlyPositive)
     posArgs defs tyns params
  where
    splitParams : Nat -> List Nat -> List (Closure []) ->
        ( List (Closure []) -- parameters (to be checked for strict positivity)
        , List (Closure []) -- indices    (to be checked for no mention at all)
        )
    splitParams i ps [] = ([], [])
    splitParams i ps (x :: xs)
        = if i `elem` ps
             then mapFst (x ::) (splitParams (S i) ps xs)
             else mapSnd (x ::) (splitParams (S i) ps xs)
-- a tyn can not appear as part of ty
posArg defs tyns nf@(NBind fc x (Pi _ _ e ty) sc)
  = do logNF "totality.positivity" 50 "Found a Pi-type" [] nf
       if !(nameIn defs tyns !(evalClosure defs ty))
         then pure (NotTerminating NotStrictlyPositive)
         else do let nm = Ref fc Bound (MN ("POSCHECK_" ++ show x) 1)
                 let arg = toClosure defaultOpts [] nm
                 sc' <- sc defs arg
                 posArg defs tyns sc'
posArg defs tyns nf@(NApp _ _ args)
    = do logNF "totality.positivity" 50 "Found an application" [] nf
         args <- traverse (evalClosure defs . snd) args
         pure $ if !(anyM (nameIn defs tyns) args)
           then NotTerminating NotStrictlyPositive
           else IsTerminating
posArg defs tyn nf
  = do logNF "totality.positivity" 50 "Reached the catchall" [] nf
       pure IsTerminating

checkPosArgs : {auto c : Ref Ctxt Defs} ->
               Defs -> List Name -> NF [] -> Core Terminating
checkPosArgs defs tyns (NBind fc x (Pi _ _ e ty) sc)
    = case !(posArg defs tyns !(evalClosure defs ty)) of
           IsTerminating =>
               do let nm = Ref fc Bound (MN ("POSCHECK_" ++ show x) 0)
                  let arg = toClosure defaultOpts [] nm
                  checkPosArgs defs tyns !(sc defs arg)
           bad => pure bad
checkPosArgs defs tyns nf
  = do logNF "totality.positivity" 50 "Giving up on non-Pi type" [] nf
       pure IsTerminating

checkCon : {auto c : Ref Ctxt Defs} ->
           Defs -> List Name -> Name -> Core Terminating
checkCon defs tyns cn
    = case !(lookupTyExact cn (gamma defs)) of
        Nothing => do log "totality.positivity" 20 $
                        "Couldn't find constructor " ++ show cn
                      pure Unchecked
        Just ty =>
          case !(totRefsIn defs ty) of
            IsTerminating =>
              do tyNF <- nf defs [] ty
                 logNF "totality.positivity" 20 "Checking the type " [] tyNF
                 checkPosArgs defs tyns tyNF
            bad => pure bad

checkData : {auto c : Ref Ctxt Defs} ->
            Defs -> List Name -> List Name -> Core Terminating
checkData defs tyns [] = pure IsTerminating
checkData defs tyns (c :: cs)
    = do log "totality.positivity" 40 $
           "Checking positivity of constructor " ++ show c
         case !(checkCon defs tyns c) of
           IsTerminating => checkData defs tyns cs
           bad => pure bad

-- Calculate whether a type satisfies the strict positivity condition, and
-- return whether it's terminating, along with its data constructors
calcPositive : {auto c : Ref Ctxt Defs} ->
               FC -> Name -> Core (Terminating, List Name)
calcPositive loc n
    = do defs <- get Ctxt
         log "totality.positivity" 6 $ "Calculating positivity: " ++ show !(toFullNames n)
         case !(lookupDefTyExact n (gamma defs)) of
              Just (TCon _ _ _ _ _ tns dcons _, ty) =>
                  case !(totRefsIn defs ty) of
                       IsTerminating =>
                            do log "totality.positivity" 30 $
                                 "Now checking constructors of " ++ show !(toFullNames n)
                               t <- checkData defs (n :: tns) dcons
                               pure (t , dcons)
                       bad => pure (bad, dcons)
              Just _ => throw (GenericMsg loc (show n ++ " not a data type"))
              Nothing => undefinedName loc n

-- Check whether a data type satisfies the strict positivity condition, and
-- record in the context
export
checkPositive : {auto c : Ref Ctxt Defs} ->
                FC -> Name -> Core Terminating
checkPositive loc n_in
    = do n <- toResolvedNames n_in
         tot <- getTotality loc n
         log "totality.positivity" 6 $ "Checking positivity: " ++ show !(toFullNames n)
         case isTerminating tot of
              Unchecked =>
                  do (tot', cons) <- calcPositive loc n
                     setTerminating loc n tot'
                     traverse_ (\c => setTerminating loc c tot') cons
                     pure tot'
              t => pure t

-- Check and record totality of the given name; positivity if it's a data
-- type, termination if it's a function
export
checkTotal : {auto c : Ref Ctxt Defs} ->
             FC -> Name -> Core Terminating
checkTotal loc n_in
    = do defs <- get Ctxt
         let Just nidx = getNameID n_in (gamma defs)
             | Nothing => undefinedName loc n_in
         let n = Resolved nidx
         tot <- getTotality loc n
         log "totality" 5 $ "Checking totality: " ++ show !(toFullNames n)
         defs <- get Ctxt
         case isTerminating tot of
              Unchecked => do
                  mgdef <- lookupCtxtExact n (gamma defs)
                  case definition <$> mgdef of
                       Just (TCon _ _ _ _ _ _ _ _)
                           => checkPositive loc n
                       _ => do whenJust (refersToM =<< mgdef) $ \ refs =>
                                 log "totality" 5 $ "  Mutually defined with:"
                                                 ++ show !(traverse toFullNames (keys refs))
                               checkTerminating loc n
              t => pure t


text:
import Data.Vect as V
import Prelude.List as L
import Language.Reflection.Utils

%language ElabReflection

--data B = T | F
%runElab
  (do declareDatatype $
        Declare `{{B}} [] `(Type)
      defineDatatype $
        DefineDatatype `{{B}}
          [ Constructor `{{T}} [] (Var `{{B}})
            , Constructor `{{F}} [] (Var `{{B}})
            ])

imp : TTName -> Raw -> FunArg
imp n t = MkFunArg n t Implicit Erased
exp : TTName -> Raw -> FunArg
exp n t = MkFunArg n t Explicit NotErased

-- equivalent to: append : Vect n a -> Vect m a -> Vect (n + m) a
-- does not define append
appendDecl : TyDecl
appendDecl =
  Declare
    `{{append}}
    [ imp `{{a}} `(Type)
      , imp `{{n}} `(Nat)
      , imp `{{m}} `(Nat)
      , exp `{{xs}}
        `(Vect ~(Var `{{n}}) ~(Var `{{a}}))
      , exp `{{ys}}
        `(Vect ~(Var `{{m}}) ~(Var `{{a}}))
    ]
    `(Vect (plus ~(Var `{{n}})
                 ~(Var `{{m}}))
                 ~(Var `{{a}}))

-- %runElab
--   (do
--     (declareType appendDecl)
-- --    the (Elab ()) debug
--     )

-- xxx : Nat
-- xxx = let vd = Declare `{{val}} [] `(Nat)
--           x = S Z
--         in %runElab (do declareType (Declare `{{val}} [] `(Nat))
--                         fill `(Z)
--                         solve)

-- xs : List Nat
-- xs = let x = S Z
--   --valDecl = Declare `{{val}} [] `(Nat)
--      in [%runElab (do declareType (Declare `{{val}} [] `(Nat))
--                       --focus `{{val}}
--                       fill `(Z)
--                       solve),
--          x + val]

-- %runElab defineFunction $ DefineFun `{{val}} [(MkFunClause (RConstant VoidType) (RConstant (BI 42)))]

-- e0 : Elab () -> Elab ()
-- e0 x = x

-- envToErrorReport : (List (TTName, Binder TT)) -> List ErrorReportPart
-- envToErrorReport xs = map ?envToErrorReport_rhs xs

-- %runElab do env <- getEnv
--             e0 $ debugMessage [(TextPart "foo")]

quicksort : List Nat -> List Nat
quicksort [] = []
quicksort (x::xs) =
  quicksort (filter (< x) xs) ++
  x :: quicksort (filter (>= x) xs)

-- processClauses : Nat -> (List (FunClause TT)) -> Elab (List (FunClause Raw, ConstructorDefn))

-- bc : (inFun, outFun, accPred : TTName) -> Elab ()
-- bc inFun outFun accPred = do
--   (inFun', Ref, inTy) <- lookupTyExact inFun
--      | _ => fail [TextPart "Not a function"]
--   (_, args, res) <- lookupArgsExact inFun'
--   declareDatatype $ Declare accPred args `(Type)
--   let accArg = MkFunArg `{{acc}}
--                 (mkApp (Var accPred)
--                    (map (Var . name) args))
--                 Explicit
--                 NotErased
--   declareType $
--     Declare outFun (args ++ [accArg]) res
--   DefineFun _ oldClauses <- lookupFunDefnExact inFun'
--   (newClauses, ctors) <-
--     Prelude.List.unzip <$> processClauses Z oldClauses
--   defineDatatype $ DefineDatatype accPred ctors
--   defineFunction $ DefineFun outFun newClauses


text:
module Prelude.Char

import Builtins

isUpper : Char -> Bool
isUpper x = x >= 'A' && x <= 'Z'

isLower : Char -> Bool
isLower x = x >= 'a' && x <= 'z'

isAlpha : Char -> Bool
isAlpha x = isUpper x || isLower x

isDigit : Char -> Bool
isDigit x = (x >= '0' && x <= '9')

isAlphaNum : Char -> Bool
isAlphaNum x = isDigit x || isAlpha x

isSpace : Char -> Bool
isSpace x = x == ' '  || x == '\t' || x == '\r' ||
            x == '\n' || x == '\f' || x == '\v' ||
            x == '\xa0'

isNL : Char -> Bool
isNL x = x == '\r' || x == '\n'

toUpper : Char -> Char
toUpper x = if (isLower x)
               then (prim__intToChar (prim__charToInt x - 32))
               else x

toLower : Char -> Char
toLower x = if (isUpper x)
               then (prim__intToChar (prim__charToInt x + 32))
               else x

isHexDigit : Char -> Bool
isHexDigit x = elem (toUpper x) hexChars where
  hexChars : List Char
  hexChars = ['0', '1', '2', '3', '4', '5', '6', '7', '8', '9',
              'A', 'B', 'C', 'D', 'E', 'F']

max_stars_repo_name: JavascriptID/sourcerer-app

max_issues_repo_name: JavascriptID/sourcerer-app

max_forks_repo_name: JavascriptID/sourcerer-app


text:
myS : Nat -> Nat
myS n = S n

myS_crash : Nat -> Nat
myS_crash = S

main : IO ()
main = do
  printLn (S Z)
  printLn (myS Z)
  printLn (myS_crash Z)

max_stars_repo_name: boxfire/rapid

max_issues_repo_name: boxfire/rapid

max_forks_repo_name: boxfire/rapid


text:
module Data.MSF.Running

import Control.Monad.Identity
import Data.MSF.Core
import Data.MSF.Event
import Data.SOP

%default total

--------------------------------------------------------------------------------
--          Single step evaluation
--------------------------------------------------------------------------------

mutual
  export
  stepPar :  Monad m
          => MSFList m is os
          -> NP I is
          -> m (NP I os, MSFList m is os)
  stepPar []          []          = pure ([],[])
  stepPar (sf :: sfs) (vi :: vis) = do
    (vo, sf2)   <- step    sf  vi
    (vos, sfs2) <- stepPar sfs vis
    pure (vo :: vos, sf2 :: sfs2)

  export
  stepFan :  Monad m
          => FanList m i os
          -> i
          -> m (NP I os, FanList m i os)
  stepFan []          _  = pure ([],[])
  stepFan (sf :: sfs) vi = do
    (vo, sf2)   <- step    sf  vi
    (vos, sfs2) <- stepFan sfs vi
    pure (vo :: vos, sf2 :: sfs2)

  export
  stepChoice :  Monad m
             => MSFList m is os
             -> NS I is
             -> m (NS I os, MSFList m is os)
  stepChoice (sf :: sfs) (Z vi) = do
    (vo, sf2) <- step sf vi
    pure (Z vo, sf2 :: sfs)

  stepChoice (sf :: sfs) (S y) = do
    (vo, sfs2) <- stepChoice sfs y
    pure (S vo, sf :: sfs2)

  export
  stepCollect :  Monad m
              => CollectList m is o
              -> NS I is
              -> m (o, CollectList m is o)
  stepCollect (sf :: sfs) (Z vi) = do
    (vo, sf2) <- step sf vi
    pure (vo, sf2 :: sfs)

  stepCollect (sf :: sfs) (S y) = do
    (vo, sfs2) <- stepCollect sfs y
    pure (vo, sf :: sfs2)

  ||| Single step evaluation of monadic stream functions.
  ||| This is used to drive a typical application using
  ||| MSFs for processing input.
  export
  step : Monad m => MSF m i o -> i -> m (o, MSF m i o)
  step c@(Const x)  _ = pure (x, c)
  step Id           v = pure (v, Id)
  step c@(Arr f)    v = pure (f v, c)
  step c@(Lifted f) v = (,c) <$> f v

  step (Seq sf1 sf2) v = do
    (vx,sf1') <- step sf1 v
    (vo,sf2') <- step sf2 vx
    pure (vo, Seq sf1' sf2')

  step (Par sfs) v = mapSnd Par <$> stepPar sfs v

  step (Fan sfs) v = mapSnd Fan <$> stepFan sfs v

  step (Choice sfs) v = mapSnd Choice <$> stepChoice sfs v

  step (Collect sfs) v = mapSnd Collect <$> stepCollect sfs v

  step (Loop s sf) v = do
    ([s2,o], sf2) <- step sf [s,v]
    pure (o, Loop s2 sf2)

  step (Switch sf f) i = do
    (Left e,_) <- step sf i
      | (Right o,sf2) => pure (o, Switch sf2 f)
    step (f e) i

--------------------------------------------------------------------------------
--          Running MSFs
--------------------------------------------------------------------------------

||| Uses the given MSF to process a list of input
||| values. This is useful for testing MSFs.
export
embed : Monad m => List i -> MSF m i o -> m (List o)
embed [] _          = pure []
embed (vi :: is) sf = do
  (vo,sf2) <- step sf vi
  os       <- embed is sf2
  pure $ vo :: os

||| `embed` using the `Identity` monad.
export
embedI : List i -> MSF Identity i o -> List o
embedI is = runIdentity . embed is

mutual
  sizePar : MSFList m is os -> Nat
  sizePar [] = 0
  sizePar (sf :: sfs) = size sf + sizePar sfs

  sizeFan : FanList m i os -> Nat
  sizeFan [] = 0
  sizeFan (sf :: sfs) = size sf + sizeFan sfs

  sizeCol : CollectList m is o -> Nat
  sizeCol [] = 0
  sizeCol (sf :: sfs) = size sf + sizeCol sfs

  ||| Calculates the size (number of constructors)
  ||| of a MSF. This is useful for testing and
  ||| possibly optimizing applications.
  export
  size : MSF m i o -> Nat
  size Id            = 1
  size (Const x)     = 1
  size (Arr f)       = 1
  size (Lifted f)    = 1
  size (Seq x y)     = 1 + size x + size y
  size (Par x)       = 1 + sizePar x
  size (Fan x)       = 1 + sizeFan x
  size (Choice x)    = 1 + sizePar x
  size (Collect x)   = 1 + sizeCol x
  size (Loop x y)    = 1 + size y
  size (Switch x f)  = 1 + size x


text:
module University

public export
record University where
  constructor CreateUniversity
  id : Integer
  country : Integer
  city : Integer
  name : String
  faculty : Integer
  facultyName : String
  chair : Integer
  chairName : String
  graduation : Integer
  educationForm : String
  educationStatus : String

max_stars_repo_name: GrandArchTemplar/IdrisVKAPI

max_issues_repo_name: GrandArchTemplar/IdrisVKAPI

max_forks_repo_name: GrandArchTemplar/IdrisVKAPI


text:
module Main

import Text.Markdown
import Text.Markdown.Definition
import Text.Markdown.Options

main : IO ()
main = printHtml def
                 $ readMarkdown def
                                $ "# Heading 1\n" ++
                                  "\n" ++
                                  "## Heading 2\n" ++
                                  "\n" ++
                                  "Here is a list:\n" ++
                                  "* One\n" ++
                                  "* Two\n" ++
                                  "* Three\n"

max_stars_repo_name: soimort/idris-commonmark

max_issues_repo_name: soimort/idris-commonmark

max_forks_repo_name: soimort/idris-commonmark


text:
module CFT

import Data.List
import Data.Fin
import Data.Maybe
import Data.Nat
import Data.Vect

infixr 1 ~>

namespace Telescope

  public export
  data Tel : Nat -> (f : Nat -> Type) -> Type where
    Nil : Tel 0 f
    (::) : (t : f n) -> Tel n f -> Tel (S n) f

public export
data CFT : Nat -> Type where
  --- variables
  VZ : CFT (S n)
  VS : CFT n -> CFT (S n)

  -- Void
  Zero : CFT n

  -- Unit
  One : CFT n

  -- fixpoint
  Mu : CFT (S n) -> CFT n

  -- Algebraic definitions
  (+) : (a, b : CFT n) -> CFT n
  (*) : (a, b : CFT n) -> CFT n
  -- (~>) : (a, b : CFT n) -> CFT n
  App : CFT (S n) -> CFT n -> CFT n

%inline
public export
µ : CFT (S n) -> CFT n
µ = Mu

public export
var : Fin n -> CFT n
var FZ = VZ
var (FS x) = VS (var x)

public export
TyFromNat : Nat -> CFT n
TyFromNat 0 = Zero
TyFromNat (S k) = One + TyFromNat k

interface Universe u where
  El : u -> Type

public export
data Ty : CFT n -> Tel n CFT -> Type where
  Top : Ty t t' -> Ty VZ (t :: t')
  Pop : Ty t t' -> Ty (VS t) (s :: t')
  Left : Ty s t' -> Ty (s + t) t'
  Right : Ty t t' -> Ty (s + t) t'
  Def : Ty f (a :: t) -> Ty (App f a) t
  -- Fun : {k : CFT n} -> (k -> Ty t t') -> Ty (k ~> t) t'
  Unit : Ty One t
  Pair : Ty s t' -> Ty t t' -> Ty (s * t) t'
  In : Ty f (Mu f :: t') -> Ty (Mu f) t'

data Morph : (s, t : Tel n f) -> Type where

    ML : Morph s s

    MF : (f : Ty s s' -> Ty t t')
      -> (phi : Morph s' t')
      ----------------------------
      -> Morph (s :: s') (t :: t')

    Mµ : Morph s' t' -> Morph (t :: s') (t :: t')

gMap : Morph s' t' -> Ty t s' -> Ty t t'
gMap ML         (Top x) = Top x
gMap (MF f phi) (Top x) = Top (f x)
gMap (Mµ phi)   (Top x) = Top (gMap phi x)
gMap ML         (Pop x) = Pop x
gMap (MF f phi) (Pop x) = Pop (gMap phi x)
gMap (Mµ phi)   (Pop x) = Pop (gMap phi x)
gMap phi        (Left x) = Left (gMap phi x)
gMap phi        (Right x) = Right (gMap phi x)
gMap phi        (Def x) = Def (gMap (Mµ phi) x)
gMap phi        Unit = Unit
gMap phi        (Pair x y) = Pair (gMap phi x) (gMap phi y)
gMap phi        (In x) = In (gMap (Mµ phi) x)

max_stars_repo_name: andrevidela/dev-notes

max_issues_repo_name: andrevidela/dev-notes

max_forks_repo_name: andrevidela/dev-notes


text:
> module Nat.GCDOperations

> import Nat.GCD
> import Nat.Divisor

> %default total
> %access public export
> %auto_implicits on

> |||
> gcdDivisorFst : GCD d m n -> d `Divisor` m
> gcdDivisorFst {d} (MkGCD dDm dDn dG) = dDm

> |||
> gcdDivisorSnd : GCD d m n -> d `Divisor` n
> gcdDivisorSnd {d} (MkGCD dDm dDn dG) = dDn

> |||
> gcdDivisorGreatest : GCD d m n -> ((d' : Nat) -> d' `Divisor` m -> d' `Divisor` n -> d' `Divisor` d)
> gcdDivisorGreatest {d} (MkGCD dDm dDn dG) = dG

ext: lidr

max_stars_repo_name: zenntenn/IdrisLibs

max_issues_repo_name: zenntenn/IdrisLibs

max_forks_repo_name: zenntenn/IdrisLibs


text:
module Deps.Data

%default total
%access public export

-- UTILS

joinString : String -> List String -> String
joinString sep str =
  concat (intersperse sep str)

Namespace : Type
Namespace = List String

showNamespace : Namespace -> String
showNamespace ns =
  joinString "." ns

-- DATA TYPES

record Import where
  constructor MkImport
  isPublic : Bool
  ns : Namespace
  nsAs : Namespace

record IdrisHead where
  constructor MkIdrisHead
  moduleNs : Namespace
  imports : List Import

defaultModuleNs : Namespace
defaultModuleNs =
  ["Main"]

-- SHOW IMPLEMENTATIONS

Show Import where
  show (MkImport isPublic ns nsAs) =
    let
      publicSpecifier = if isPublic then "public " else ""
      nsAsSpecifier = if ns /= nsAs then " as " ++ showNamespace nsAs else ""
    in
      "import " ++ publicSpecifier ++ showNamespace ns ++ nsAsSpecifier

Show IdrisHead where
  show (MkIdrisHead mod imports) =
    let
      moduleString = show mod
      importString = unlines (map show imports)
    in
      moduleString ++ "\n\n" ++ importString

max_stars_repo_name: chrrasmussen/Idris-Deps

max_issues_repo_name: chrrasmussen/Idris-Deps

max_forks_repo_name: chrrasmussen/Idris-Deps


text:
module Idris2Rust.CaseConversion

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

-- NOTE: Maybe add another cases and move to separate library?
export
data IdentifierCase = Camel | Snake | UpperSnake

splitBy : (a -> Bool) -> List a -> List (List1 a)
splitBy p = groupBy (const (not . p))

toCharacterCase : Char -> List String -> String
toCharacterCase c cs = pack $ intercalate [c] (map (unpack . toLower) cs)

fromCharacterCase : Char -> String -> List String
fromCharacterCase c cs = toList $ split (==c) cs

export
fromCase : IdentifierCase -> String -> List String
fromCase Camel = map (pack . toList) . splitBy isUpper . unpack
fromCase Snake = fromCharacterCase '_'
fromCase UpperSnake = fromCharacterCase '_'

export
toCase : IdentifierCase -> List String -> String
-- fromCase Camel = map (pack . toList) . splitBy isUpper . unpack
toCase Snake xs = toLower $ toCharacterCase '_' xs
toCase UpperSnake xs = toUpper $ toCharacterCase '_' xs
toCase Camel [] = ""
toCase Camel (x::xs) = concat (toLower x :: map capitalize xs)
  where
    capitalize : String -> String
    capitalize s = case unpack s of
        (head::tail) => strCons (toUpper head) (toLower . pack $ tail)
        [] => ""

export
fromToCase : IdentifierCase -> IdentifierCase -> String -> String
fromToCase from to = toCase to . fromCase from


text:
module Toolkit.Data.List.Occurs.Error

%default total

namespace Occurs
  public export
  record Error where
    constructor MkError
    expected : Nat
    found    : Nat

-- [ EOF ]

max_stars_repo_name: gallais/linear-circuits

max_issues_repo_name: gallais/linear-circuits

max_forks_repo_name: gallais/linear-circuits


text:
module Dummy

import Data.Vect

namespace DList

  ||| A list construct for dependent types.
  |||
  ||| @aTy    The type of the value contained within the list element type.
  ||| @elemTy The type of the elements within the list
  ||| @as     The List used to contain the different values within the type.
  public export
  data DList : (aTy : Type)
            -> (elemTy : aTy -> Type)
            -> (as : List aTy)
            -> Type where
    ||| Create an empty List
    Nil  : DList aTy elemTy Nil
    ||| Cons
    |||
    ||| @elem The element to add
    ||| @rest The list for `elem` to be added to.
    (::) : (elem : elemTy x)
        -> (rest : DList aTy elemTy xs)
        -> DList aTy elemTy (x::xs)

namespace DVect
  ||| A list construct for dependent types.
  |||
  ||| @aTy    The type of the value contained within the list element type.
  ||| @elemTy The type of the elements within the list
  ||| @len    The length of the list.
  ||| @as     The List used to contain the different values within the type.
  public export
  data DVect : (aTy : Type)
            -> (elemTy : aTy -> Type)
            -> (len : Nat)
            -> (as : Vect len aTy)
            -> Type where
    ||| Create an empty List
    Nil  : DVect aTy elemTy Z Nil
    ||| Cons
    |||
    ||| @ex The element to add
    ||| @rest The list for `elem` to be added to.
    (::) : (ex : elemTy x)
        -> (rest : DVect aTy elemTy n xs)
        -> DVect aTy elemTy (S n) (x::xs)

namespace PList
  public export
  data PList : (aTy    : Type)
            -> (elemTy : aTy -> Type)
            -> (predTy : aTy -> Type)
            -> (as     : List aTy)
            -> (prf    : DList aTy predTy as)
            -> Type
    where
      ||| Create an empty List
      Nil  : PList aTy elemTy predTy Nil Nil

      ||| Cons
      |||
      ||| @elem The element to add and proof that the element's type satisfies a certain predicate.
      ||| @rest The list for `elem` to be added to.
      (::) : (elem : elemTy x)
          -> {prf : predTy x}
          -> (rest : PList aTy elemTy predTy xs prfs)
          -> PList aTy elemTy predTy (x :: xs) (prf :: prfs)


text:
module Functions

data Nat' = Z' | S' Nat'

plus : Nat' -> Nat' -> Nat'
plus Z' y = y
plus (S' k) y = S' (plus k y)

mult : Nat' -> Nat' -> Nat'
mult Z' y = Z'
mult (S' k) y = plus y (mult k y)

max_stars_repo_name: aztecrex/try-idris

max_issues_repo_name: aztecrex/try-idris

max_forks_repo_name: aztecrex/try-idris