text:
module IdrisJvm.Core.Codegen

import IdrisJvm.IO
import IdrisJvm.Core.Asm
import IdrisJvm.IR.Types
import IdrisJvm.Core.Common
import IdrisJvm.Core.Constant
import IdrisJvm.Core.Function
import IdrisJvm.Core.JAsm
import IdrisJvm.Core.Inference
import IdrisJvm.IR.Exports
import Data.SortedMap

%access public export

generateDependencyMethods : Assembler -> AsmState -> JVM_IO (SortedMap JMethodName InferredFunctionType)
generateDependencyMethods assembler state@(MkAsmState [] _ _ _) = pure (functionTypes state)
generateDependencyMethods assembler state@(MkAsmState (subroutine :: restSubroutines) _ _ _) = do
  let asmState = record { subroutines = [] } state
  (_, newState) <- runAsm asmState assembler subroutine
  let nextState = record { subroutines $= (restSubroutines ++) } newState
  generateDependencyMethods assembler nextState

generateMethod : Assembler -> SortedMap JMethodName InferredFunctionType -> SDecl
              -> JVM_IO (SortedMap JMethodName InferredFunctionType)
generateMethod assembler functionTypes (SFun name args locs def) = do
  let jmethodName = jname name
  let fname = jmethName jmethodName
  let clsName = jmethClsName jmethodName
  let asmState = MkAsmState [] functionTypes SortedMap.empty IUnknown
  (_, newState) <- runAsm asmState assembler $ cgFun [Public, Static] name clsName fname args locs def
  generateDependencyMethods assembler newState

group : Nat -> List a -> List (List a)
group _ [] = []
group n xs =
    let (ys, zs) = splitAt n xs
    in  ys :: group n zs

splitApplyFunction : String -> List String -> Int -> LVar -> List SAlt -> List SDecl
splitApplyFunction fname args n var cases =
  let cs = group 100 cases
      len = List.length cs
  in map (callNextFn fname args n var len) . List.zip [0 .. pred len] $ cs where

    callNextFn : String -> List String -> Int -> LVar -> Nat -> (Nat, List SAlt) -> SDecl
    callNextFn fname args n caseVar last (index, cs) = SFun currFn args n body where
      nextFn : String
      nextFn = fname ++ "$" ++ show (index + 1)

      currFn : String
      currFn = if index == 0 then fname else (fname ++ "$" ++ show index)

      body = SChkCase caseVar $ if index + 1 == last then cs else (cs ++ [SDefaultCase (SApp True nextFn [Loc 0, Loc 1])])

splitLargeFunctions : List SDecl -> List SDecl
splitLargeFunctions decls = decls >>= f where
  f : SDecl -> List SDecl
  f decl@(SFun "{APPLY_0}" args n (SChkCase var cases)) = splitApplyFunction "{APPLY_0}" args n var cases
  f decl = [decl]

inferFuns : SortedMap JMethodName InferredFunctionType
         -> List SDecl
         -> SortedMap JMethodName InferredFunctionType
inferFuns initial decls = go SortedMap.empty decls where
    go : SortedMap JMethodName InferredFunctionType
      -> List SDecl
      -> SortedMap JMethodName InferredFunctionType
    go acc [] = acc
    go acc (decl :: rest) =
        let ftype = inferFun initial decl
            newAcc = SortedMap.insert (functionName ftype) ftype acc
        in go newAcc rest

createMainMethod : Asm ()
createMainMethod = do
    let signature = "()Lio/github/mmhelloworld/idrisjvm/runtime/Thunk;"
    let MkJMethodName className methodName = jname "{runMain_0}"
    CreateMethod [Public, Static] className "main" "([Ljava/lang/String;)V" Nothing Nothing [] []
    MethodCodeStart
    Aload 0
    InvokeMethod InvokeStatic (rtClass "Runtime") "setProgramArgs" "([Ljava/lang/String;)V" False
    InvokeMethod InvokeStatic className methodName signature False
    Pop
    Return
    MaxStackAndLocal (-1) (-1)
    MethodCodeEnd

generateMethods : Assembler -> List SDecl -> List ExportIFace -> JVM_IO ()
generateMethods assembler decls exports = do
    let smallDecls = splitLargeFunctions decls
    let functionTypesByNameStage1 = inferFuns SortedMap.empty smallDecls
    let functionTypesByName = inferFuns functionTypesByNameStage1 smallDecls
    types <- generateMethodsWithTypes functionTypesByName smallDecls
    generateExportsWithTypes types exports
    let asmState = MkAsmState [] types SortedMap.empty IUnknown
    _ <- runAsm asmState assembler createMainMethod
    pure ()
  where
    generateMethodsWithTypes : SortedMap JMethodName InferredFunctionType -> List SDecl
                            -> JVM_IO (SortedMap JMethodName InferredFunctionType)
    generateMethodsWithTypes types [] = pure types
    generateMethodsWithTypes types (decl :: rest) = do
        newTypes <- generateMethod assembler types decl
        generateMethodsWithTypes newTypes rest

    generateExportsWithTypes : SortedMap JMethodName InferredFunctionType -> List ExportIFace -> JVM_IO ()
    generateExportsWithTypes types [] = pure ()
    generateExportsWithTypes types (exportIface :: exports) = do
        let asmState = MkAsmState [] types SortedMap.empty IUnknown
        (_, _) <- runAsm asmState assembler $ exportCode types exportIface
        generateExportsWithTypes types exports

exports : FFI_Export FFI_JVM "IdrisJvm/Core/export/Codegen" []
exports =
  Data SDecl "IdrisJvm/IR/export/SDecl" $
  Data FDesc "IdrisJvm/IR/export/FDesc" $
  Data SExp "IdrisJvm/IR/export/SExp" $
  Data Const "IdrisJvm/IR/export/Const" $
  Data LVar "IdrisJvm/IR/export/LVar" $
  Data CaseType "IdrisJvm/IR/export/CaseType" $
  Data Export "IdrisJvm/IR/export/Export" $
  Data NativeTy "IdrisJvm/IR/export/NativeTy" $
  Data ExportIFace "IdrisJvm/IR/export/ExportIFace" $
  Data IntTy ("IdrisJvm/IR/export/IntTy") $
  Data ArithTy ("IdrisJvm/IR/export/ArithTy") $
  Data PrimFn ("IdrisJvm/IR/export/PrimFn") $
  Data SAlt "IdrisJvm/IR/export/SAlt" $
  Data (FDesc, LVar) "IdrisJvm/IR/export/SForeignArg" $
  Data (List SAlt) "idris/prelude/list/ListSAlt" $
  Data (List (FDesc, LVar)) "IdrisJvm/IR/export/SForeignArgs" $
  Data (Maybe LVar) "IdrisJvm/IR/export/MaybeLVar" $
  Data (List String) "idris/prelude/list/ListString" $
  Data (List FDesc) "idris/prelude/list/ListFDesc" $
  Data (List LVar) "idris/prelude/list/ListLVar" $
  Data (List Export) "idris/prelude/list/ListExport" $
  Data (List SDecl) "IdrisJvm/IR/export/ListSDecl" $
  Data (List ExportIFace) "IdrisJvm/IR/export/ListExportIFace" $

  Fun consSDecl (ExportStatic "consSDecl") $
  Fun emptySDecl (ExportStatic "emptySDecl") $

  Fun consExportIFace (ExportStatic "consExportIFace") $
  Fun emptyExportIFace (ExportStatic "emptyExportIFace") $

  Fun consFDesc (ExportStatic "consFDesc") $
  Fun emptyFDesc (ExportStatic "emptyFDesc") $

  Fun consString (ExportStatic "consString") $
  Fun emptyListString (ExportStatic "emptyListString") $

  Fun fcon (ExportStatic "fcon") $
  Fun fstr (ExportStatic "fstr") $
  Fun fapp (ExportStatic "fapp") $
  Fun fio (ExportStatic "fio") $
  Fun funknown (ExportStatic "funknown") $

  Fun loc (ExportStatic "loc") $
  Fun glob (ExportStatic "glob") $

  Fun consLVar (ExportStatic "consLVar") $
  Fun emptyLVar (ExportStatic "emptyLVar") $

  Fun consExport (ExportStatic "consExport") $
  Fun emptyExport (ExportStatic "emptyExport") $
  Fun exportData (ExportStatic "exportData") $
  Fun Exports.exportFun (ExportStatic "exportFun") $

  Fun mkExportIFace (ExportStatic "mkExportIFace") $

  Fun it8 (ExportStatic "it8") $
  Fun it16 (ExportStatic "it16") $
  Fun it32 (ExportStatic "it32") $
  Fun it64 (ExportStatic "it64") $

  Fun itFixed (ExportStatic "itFixed") $
  Fun itNative (ExportStatic "itNative") $
  Fun itBig (ExportStatic "itBig") $
  Fun itChar (ExportStatic "itChar") $

  Fun atInt (ExportStatic "atInt") $
  Fun atFloat (ExportStatic "atFloat") $

  Fun lFExp (ExportStatic "lFExp") $
  Fun lFLog (ExportStatic "lFLog") $
  Fun lFSin (ExportStatic "lFSin") $
  Fun lFCos (ExportStatic "lFCos") $
  Fun lFTan (ExportStatic "lFTan") $
  Fun lFASin (ExportStatic "lFASin") $
  Fun lFACos (ExportStatic "lFACos") $
  Fun lFATan (ExportStatic "lFATan") $
  Fun lFSqrt (ExportStatic "lFSqrt") $
  Fun lFFloor (ExportStatic "lFFloor") $
  Fun lFCeil (ExportStatic "lFCeil") $
  Fun lFNegate (ExportStatic "lFNegate") $
  Fun lStrHead (ExportStatic "lStrHead") $
  Fun lStrTail (ExportStatic "lStrTail") $
  Fun lStrCons (ExportStatic "lStrCons") $
  Fun lStrIndex (ExportStatic "lStrIndex") $
  Fun lStrRev (ExportStatic "lStrRev") $
  Fun lStrSubstr (ExportStatic "lStrSubstr") $
  Fun lReadStr (ExportStatic "lReadStr") $
  Fun lWriteStr (ExportStatic "lWriteStr") $
  Fun lSystemInfo (ExportStatic "lSystemInfo") $
  Fun lFork (ExportStatic "lFork") $
  Fun lPar (ExportStatic "lPar") $
  Fun lCrash (ExportStatic "lCrash") $
  Fun lNoOp (ExportStatic "lNoOp") $
  Fun lStrConcat (ExportStatic "lStrConcat") $
  Fun lStrLt (ExportStatic "lStrLt") $
  Fun lStrEq (ExportStatic "lStrEq") $
  Fun lStrLen (ExportStatic "lStrLen") $
  Fun lFloatStr (ExportStatic "lFloatStr") $
  Fun lStrFloat (ExportStatic "lStrFloat") $
  Fun lPlus (ExportStatic "lPlus") $
  Fun lMinus (ExportStatic "lMinus") $
  Fun lTimes (ExportStatic "lTimes") $
  Fun lSDiv (ExportStatic "lSDiv") $
  Fun lSRem (ExportStatic "lSRem") $
  Fun lEq (ExportStatic "lEq") $
  Fun lSLt (ExportStatic "lSLt") $
  Fun lSLe (ExportStatic "lSLe") $
  Fun lSGt (ExportStatic "lSGt") $
  Fun lSGe (ExportStatic "lSGe") $
  Fun lUDiv (ExportStatic "lUDiv") $
  Fun lURem (ExportStatic "lURem") $
  Fun lAnd (ExportStatic "lAnd") $
  Fun lOr (ExportStatic "lOr") $
  Fun lXOr (ExportStatic "lXOr") $
  Fun lCompl (ExportStatic "lCompl") $
  Fun lSHL (ExportStatic "lSHL") $
  Fun lLSHR (ExportStatic "lLSHR") $
  Fun lASHR (ExportStatic "lASHR") $
  Fun lLt (ExportStatic "lLt") $
  Fun lLe (ExportStatic "lLe") $
  Fun lGt (ExportStatic "lGt") $
  Fun lGe (ExportStatic "lGe") $
  Fun lIntFloat (ExportStatic "lIntFloat") $
  Fun lFloatInt (ExportStatic "lFloatInt") $
  Fun lIntStr (ExportStatic "lIntStr") $
  Fun lStrInt (ExportStatic "lStrInt") $
  Fun lChInt (ExportStatic "lChInt") $
  Fun lIntCh (ExportStatic "lIntCh") $
  Fun lSExt (ExportStatic "lSExt") $
  Fun lZExt (ExportStatic "lZExt") $
  Fun lTrunc (ExportStatic "lTrunc") $
  Fun lBitCast (ExportStatic "lBitCast") $
  Fun lExternal (ExportStatic "lExternal") $

  Fun sConCase (ExportStatic "sConCase") $
  Fun sConstCase (ExportStatic "sConstCase") $
  Fun sDefaultCase (ExportStatic "sDefaultCase") $
  Fun consSAlt (ExportStatic "consSAlt") $
  Fun emptySAlt (ExportStatic "emptySAlt") $

  Fun mkSForeignArg (ExportStatic "mkSForeignArg") $

  Fun consSForeignArg (ExportStatic "consSForeignArg") $
  Fun emptySForeignArg (ExportStatic "emptySForeignArg") $

  Fun nothingLVar (ExportStatic "nothingLVar") $
  Fun justLVar (ExportStatic "justLVar") $

  Fun constI (ExportStatic "constI") $
  Fun constBI (ExportStatic "constBI") $
  Fun constFl (ExportStatic "constFl") $
  Fun constCh (ExportStatic "constCh") $
  Fun constStr (ExportStatic "constStr") $
  Fun constB8 (ExportStatic "constB8") $
  Fun constB16 (ExportStatic "constB16") $
  Fun constB32 (ExportStatic "constB32") $
  Fun constB64 (ExportStatic "constB64") $
  Fun aType (ExportStatic "aType") $
  Fun strType (ExportStatic "strType") $
  Fun worldType (ExportStatic "worldType") $
  Fun theWorld (ExportStatic "theWorld") $
  Fun voidType (ExportStatic "voidType") $
  Fun forgot (ExportStatic "forgot") $

  Fun sV (ExportStatic "sV") $
  Fun sApp (ExportStatic "sApp") $
  Fun sLet (ExportStatic "sLet") $
  Fun sUpdate (ExportStatic "sUpdate") $
  Fun sCon (ExportStatic "sCon") $
  Fun sCase (ExportStatic "sCase") $
  Fun sChkCase (ExportStatic "sChkCase") $
  Fun sProj (ExportStatic "sProj") $
  Fun sConst (ExportStatic "sConst") $
  Fun sForeign (ExportStatic "sForeign") $
  Fun sOp (ExportStatic "sOp") $
  Fun sNothing (ExportStatic "sNothing") $
  Fun sError (ExportStatic "sError") $

  Fun sFun (ExportStatic "sFun") $

  Fun updatable (ExportStatic "updatable") $
  Fun shared (ExportStatic "shared") $

  Fun generateMethods (ExportStatic "generateMethods") $
  End


text:
module BaseN

import Data.Fin
import ZZ
import GCDZZ
import gcd
import ZZUtils
import NatUtils
import NatOrder

%access public export

--Defines a data type Base that behaves like a list
data Base: (n: Nat) -> Type where
  Ones: (n: Nat) -> (Fin n) -> Base n
  Next: (n: Nat) -> (Fin n) -> (Base n) -> (Base n)

--Auxiliary function that reverses a Base (S n) onto anpther given Base (S n)
total
Revonto: (n: Nat) -> (Base (S n)) -> (Base (S n)) -> (Base (S n))
Revonto n accum (Ones (S n) x) = Next (S n) x accum
Revonto n accum (Next (S n) x y) = Revonto n (Next (S n) x accum) y

--Reverses a Base (S n)
total
Rev: (n: Nat) -> (Base (S n)) -> (Base (S n))
Rev n (Ones (S n) x) = Ones (S n) x
Rev n (Next (S n) x y) = Revonto n (Ones (S n) x) y

--Concatenates two values in Base (S n)
total
concat: (n: Nat) -> (Base (S n)) -> (Base (S n)) -> (Base (S n))
concat n (Ones (S n) x) y = Next (S n) x y
concat n (Next (S n) x z) y = Next (S n) x (concat n z y)

--Fin to Nat
total
tonatFin: (n: Nat) -> Fin(S n) -> Nat
tonatFin Z FZ = Z
tonatFin (S k) FZ = Z
tonatFin (S k) (FS x) = S (tonatFin k x)

--Outputs the length of a number in base n
total
len: (n: Nat) -> Base (S n) -> Nat
len n (Ones (S n) x) = S Z
len n (Next (S n) x y) = S(len n y)

--List Fin to Nat
total
tonat: (n: Nat) -> Base (S n) -> Nat
tonat Z y = case y of
            (Ones (S Z) x) => case x of
                              FZ => Z
                              FS x impossible
            (Next (S Z) x z) => case x of
                              FZ => Z
                              FS x impossible
tonat (S k) y = case y of
            (Ones (S (S k)) x) => case x of
                                  FZ => Z
                                  FS x => S(tonat k (Ones (S k) x))
            (Next (S (S k)) x z) => case x of
                                    FZ => tonat (S k) z
                                    FS w => (S(tonat k (Ones (S k) w)))*(pow (S (S k)) (len (S k) z)) + (tonat (S k) z)

total
tonatFindef: tonatFin (S Z) FZ = Z
tonatFindef = Refl

total
tonatdef: tonat Z (Ones (S Z) FZ) = Z
tonatdef = Refl

--Nat to Fin (modular values)
total
tofinNath: (a: Nat) -> (n: Nat) -> (k: Nat) -> Fin (S n)
tofinNath r Z k = FZ
tofinNath r (S j) Z = FZ
tofinNath Z (S j) (S r) = FZ
tofinNath (S k) (S j) (S r) = f k j r (lte (S k) (S j)) where
          f: (k: Nat) -> (j: Nat) -> (r: Nat) -> (t: Bool) -> Fin (S (S j))
          f k j r True = FS (tofinNath k j r)
          f k j r False = let qrem = eculidDivideAux (S k) (S j) (SIsNotZ) in
                (tofinNath (DPair.fst(DPair.snd(qrem))) (S j) r)

total
tofinNat: (a: Nat) -> (n: Nat) -> Fin (S n)
tofinNat a n = tofinNath a n (n+2)

total
tonatfinlte: (n: Nat) -> (a: Fin (S n)) -> (lte (tonatFin n a) n) = True
tonatfinlte Z FZ = Refl
tonatfinlte Z (FS x) impossible
tonatfinlte (S k) FZ = Refl
tonatfinlte (S k) (FS x) = (tonatfinlte k x)

total
FinNatop: (n: Nat) -> (a: Fin (S n)) -> (tofinNat (tonatFin n a) n) = a
FinNatop Z FZ = Refl
FinNatop Z (FS x) impossible
FinNatop (S k) FZ = Refl
FinNatop (S k) (FS x) = trans (cong(tonatfinlte (S k) (FS x))) (cong(FinNatop k x))

total
Remn: (a: Nat) -> (n: Nat) -> (r: Nat ** (lte r (S n) = True))
Remn a n = let
            qrem = eculidDivideAux a (S n) (SIsNotZ)
            rem = DPair.fst(DPair.snd(qrem))
            in
            MkDPair rem (LTEmeanslteTrue rem (S n) (ltImpliesLTE (Basics.snd(DPair.snd(DPair.snd(qrem))))))

total
strp: (Base (S n)) -> (Base (S n))
strp (Ones (S n) x) = (Ones (S n) x)
strp (Next (S n) x y) = case x of
                  FZ => strp(y)
                  FS z => Next (S n) x y

-- Nat to List Fin n (base n representation)
total
tofinh: Nat -> (n: Nat) -> (r: Nat) -> Base (S n)
tofinh Z n r = Ones (S n) FZ
tofinh k n Z = Ones (S n) FZ
tofinh (S k) n (S r) = strp(concat n (tofinh q n r) (Ones (S n) rem)) where
                    qrem: (q : Nat ** (r : Nat ** (((S k) = r + (q * (S n))), LT r (S n))))
                    qrem = eculidDivideAux (S k) (S n) (SIsNotZ)
                    rem: Fin (S n)
                    rem = tofinNat (DPair.fst(DPair.snd(qrem))) n
                    q: Nat
                    q = DPair.fst(qrem)

total
tofin: Nat -> (n: Nat) -> Base (S n)
tofin k n = tofinh k n k

--embedding Fin n in Fin S n vertically
total
embn: (n: Nat) -> Fin n -> Fin (S n)
embn (S k) FZ = FZ
embn (S k) (FS x) = FS (embn k x)

--Generates n in (Fin (S n))
total
Genn: (n: Nat) -> (Fin (S n))
Genn Z = FZ
Genn (S k) = FS (Genn k)

--Checks if a given element of Fin (S n) is in fact n
total
Isn: (n: Nat) -> (p: Fin (S n)) -> Bool
Isn Z x = True
Isn (S k) FZ = False
Isn (S k) (FS x) = Isn k x

--Proves that the definitional equality for Isn holds
total
IsnisIsn: (n: Nat) -> (p: Fin (S n)) -> (Isn (S n) (FS p)) = (Isn n p)
IsnisIsn n p = Refl

--Proves that if a given (FS x) is not n in (Fin (S n)), then x is not n-1 in (Fin n)
total
IsNotnPf:  (n: Nat) -> (p: Fin (S n)) ->  ((Isn (S n) (FS p)) = False) -> ((Isn n p) = False)
IsNotnPf Z _ Refl impossible
IsNotnPf (S k) FZ prf = Refl
IsNotnPf (S k) (FS x) prf = trans (sym (IsnisIsn (S k) (FS x))) prf

--Gives a back embedding whenever the value is not Genn
total
Predec: (n: Nat) -> (p: Fin (S n)) -> ((Isn n p) = False) -> (Fin n)
Predec Z _ Refl impossible
Predec (S k) FZ Refl = FZ
Predec (S k) (FS x) prf = FS (Predec k x (IsNotnPf (S k) (FS x) prf))

--Decidable type for Isn
total
DecIsn: (n: Nat) -> (p: (Fin (S n))) -> Either (Isn n p = True) (Isn n p = False)
DecIsn Z p = Left Refl
DecIsn (S k) FZ = Right Refl
DecIsn (S k) (FS x) = case (DecIsn k x) of
                        Left l => Left (trans (IsnisIsn k x) l)
                        Right r => Right (trans (IsnisIsn k x) r)

--adding two Fin n's
total
addfinh: (n: Nat) -> (k: Nat) -> Fin (S n) -> Fin (S n) -> (Fin (S n), Fin (S n))
addfinh k Z x y = (FZ, FZ)
addfinh Z (S r) x y = (FZ, FZ)
addfinh (S k) (S r) FZ y = (FZ, y)
addfinh (S k) (S r) (FS x) y = let
                    a = Genn (S k)
                    b = the (Fin (S (S k))) FZ
                    c = the (Fin (S k)) FZ
                    w = fst(addfinh (S k) r (embn (S k) x) y)
                    z = snd(addfinh (S k) r (embn (S k) x) y)
                    in
                    case (DecIsn (S k) z) of
                             Left l => (FS c, b)
                             Right r => (w, FS(Predec (S k) z r))

total
addfin: (n: Nat) -> Fin (S n) -> Fin (S n) -> (Fin (S n), Fin (S n))
addfin n x y = addfinh n (n+1) x y

--adding two reversed lists as specified
total
addfinlh: (n: Nat) -> (k: Nat) -> Base (S n) -> Base (S n) -> Base (S n)
addfinlh n Z a b = (Ones (S n) FZ)
addfinlh n (S k) (Ones (S n) x) (Ones (S n) y) = case (addfin n x y) of
                              (FZ, a) => Ones (S n) a
                              (FS c, a) => Next (S n) a (Ones (S n) (FS c))
addfinlh n (S k) (Ones (S n) x) (Next (S n) y z) = Next (S n) (snd (addfin n x y)) (addfinlh n k (Ones (S n) (fst (addfin n x y))) z)
addfinlh n (S k) (Next (S n) x z) (Ones (S n) y) = Next (S n) (snd (addfin n x y)) (addfinlh n k (Ones (S n) (fst (addfin n x y))) z)
addfinlh n (S k) (Next (S n) x z) (Next (S n) y w) = Next (S n) (snd (addfin n x y)) (addfinlh n k (Ones (S n) (fst (addfin n x y))) (addfinlh n k z w))

total
addfinl: (n: Nat) -> Base (S n) -> Base (S n) -> Base (S n)
addfinl n x y = addfinlh n (4*((len n x)+(len n y))) x y

--adding two lists
total
addfinlist: (n: Nat) -> Base (S n) -> Base (S n) -> Base (S n)
addfinlist n xs ys = (Rev n (addfinl n (Rev n xs) (Rev n ys)))

--multiply two reversed lists in Fin S n
total
mulfinlh: (n: Nat) -> (k: Nat) -> Base (S n) -> Base (S n) -> Base (S n)
mulfinlh n Z a b = Ones (S n) FZ
mulfinlh n (S k) (Ones (S n) FZ) y = Ones (S n) FZ
mulfinlh n (S k) (Ones (S n) (FS x)) y = addfinl n y (mulfinlh n k (Ones (S n) (embn n x)) y)
mulfinlh n (S k) (Next (S n) FZ z) y = Next (S n) FZ (mulfinlh n k z y)
mulfinlh n (S k) (Next (S n) (FS x) z) y = addfinl n y (mulfinlh n k (Next (S n) (embn n x) z) y)

total
mulfinl: (n: Nat) -> Base (S n) -> Base (S n) -> Base (S n)
mulfinl n x y = mulfinlh n (tonat n x) x y

--multiply two lists
total
mulfinList: (n: Nat) -> (Base (S n)) -> (Base (S n)) -> (Base (S n))
mulfinList n xs ys = Rev n (mulfinl n (Rev n xs) (Rev n ys))

--Custom "functions are functors" function
total
ap: (x: Type) -> (y: Type) -> (f: x->y) -> (n = m) -> (f n = f m)
ap x y f Refl = Refl

ext: idr


text:
module readNum

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

public export
readNumbers : IO (Maybe (Nat, Nat))
readNumbers = do
            Just n1ok <- readNumber | Nothing => pure Nothing
            Just n2ok <- readNumber | Nothing => pure Nothing
            pure (Just (n1ok, n2ok))


text:
> module Fin.Properties

> import Data.Fin
> import Data.Vect
> import Control.Isomorphism

> import Fun.Properties
> import Fin.Operations
> import Basic.Operations

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

> -- %hide Prelude.List.tail
> -- %hide Prelude.Stream.tail
> -- %hide Data.VectType.Vect.tail

|Fin 0| properties:

> fin0Lemma : (i : Fin Z) -> (j : Fin Z) -> i = j
> fin0Lemma i j = absurd i
> %freeze fin0Lemma -- frozen

|Fin 1| properties:

> fin1Lemma : (i : Fin (S Z)) -> (j : Fin (S Z)) -> i = j
> fin1Lemma FZ      FZ    = Refl
> fin1Lemma FZ     (FS k) = absurd k
> fin1Lemma (FS k)  FZ    = absurd k
> fin1Lemma (FS k) (FS j) = absurd k
> %freeze fin1Lemma -- frozen

> ||| Fin 1 is isomorphic to Unit
> isoFin1Unit : Iso (Fin (S Z)) Unit
> isoFin1Unit = MkIso to from toFrom fromTo where
>   to : Fin (S Z) -> Unit
>   to FZ = ()
>   to (FS k) = absurd k
>   from : Unit -> Fin (S Z)
>   from () = FZ
>   toFrom : (u : Unit) -> to (from u) = u
>   toFrom () = Refl
>   fromTo : (k : Fin (S Z)) -> from (to k) = k
>   fromTo FZ = Refl
>   fromTo (FS k) = absurd k
> %freeze isoFin1Unit -- frozen

Injectivity of FS

> ||| FS is injective (one direction)
> fsInjective1 : (left : Fin n) -> (right : Fin n) -> FS left = FS right -> left = right
> fsInjective1 = FSInjective
> %freeze fsInjective1 -- frozen

> ||| FS is injective (the other way round)
> fsInjective2 : (left : Fin n) -> (right : Fin n) -> Not (left = right) -> Not (FS left = FS right)
> -- fsInjective2 left right contra = contra . (FSInjective left right)
> fsInjective2 = injectiveLemma FS fsInjective1
> %freeze fsInjective2 -- frozen

> ||| FS preserves equality
> fsPreservesEq : (left : Fin n) -> (right : Fin n) -> left = right -> FS left = FS right
> fsPreservesEq left right = cong
> %freeze fsPreservesEq -- frozen

|finToNat| properties:

> ||| |finToNat (k : Fin n)| is LT bounded by |n|
> finToNatLemma : {n : Nat} -> (k : Fin n) -> LT (finToNat k) n
> finToNatLemma {n = Z}   k       =  absurd k
> finToNatLemma {n = S m} FZ      =  LTESucc LTEZero
> finToNatLemma {n = S m} (FS k)  =  LTESucc (finToNatLemma k)
> %freeze finToNatLemma -- frozen

|weaken| properties:

> |||
> weakenPreservesEq : (i : Fin n) -> (j : Fin n) -> (i = j) -> (weaken i = weaken j)
> weakenPreservesEq left _ Refl = Refl
> %freeze weakenPreservesEq -- frozen

> |||
> weakenInjective : (i : Fin n) -> (j : Fin n) -> (weaken i = weaken j) -> (i = j)
> weakenInjective  FZ     FZ    Refl = Refl
> weakenInjective  FZ    (FS k) Refl impossible
> weakenInjective (FS k)  FZ    Refl impossible
> weakenInjective (FS k) (FS j) prf = s5 where
>   s1 : weaken (FS k) = weaken (FS j)
>   s1 = prf
>   s2 : FS (weaken k) = FS (weaken j)
>   s2 = s1
>   s3 : weaken k = weaken j
>   s3 = FSInjective (weaken k) (weaken j) s2
>   s4 : k = j
>   s4 = weakenInjective k j s3
>   s5 : FS k = FS j
>   s5 = cong s4
> %freeze weakenInjective -- frozen

> |||
> notWeakenLemma : (i : Fin n) -> (j : Fin n) -> Not (i = j) -> Not (weaken i = weaken j)
> notWeakenLemma i j contra = \ prf => contra (weakenInjective i j prf)
> %freeze notWeakenLemma -- frozen

|tail| properties:

> |||
> tailSuccLemma : {A : Type} -> (f : Fin (S n) -> A) -> (i : Fin n) -> (tail f) i = f (FS i)
> tailSuccLemma f i = Refl
> %freeze tailSuccLemma -- frozen

> |||
> tailSuccEqLemma : {n : Nat} -> {A : Type} ->
>                   (i : Fin n) -> (j : Fin n) -> (f : Fin (S n) -> A) ->
>                   (tail f) i = (tail f) j ->
>                   f (FS i) = f (FS j)
> tailSuccEqLemma i j f prf = replace2 (tailSuccLemma f i) (tailSuccLemma f j) prf
> %freeze tailSuccEqLemma -- frozen

|toVect| properties:

> ||| |toVect| representations of finite functions are complete
> toVectComplete : {n : Nat} -> {A : Type} -> (f : Fin n -> A) -> (k : Fin n) -> Elem (f k) (toVect f)
> toVectComplete {n = Z} _  k     = void (uninhabited k)
> toVectComplete         f  FZ    = Here
> toVectComplete         f (FS j) = There (toVectComplete (tail f) j)
> %freeze toVectComplete -- frozen

> |||
> toVectRepr : {A : Type} -> (f : Fin n -> A) -> (k : Fin n) -> index k (toVect f) = f k
> toVectRepr {n = Z}   f k  = absurd k
> toVectRepr {n = S m} f FZ     = Refl
> toVectRepr {n = S m} f (FS k) = toVectRepr (tail f) k
> %freeze toVectRepr -- frozen

> {-

> ---}

ext: lidr

max_stars_repo_name: zenntenn/IdrisLibs

max_issues_repo_name: zenntenn/IdrisLibs

max_forks_repo_name: zenntenn/IdrisLibs


text:
module Test.Suite

import IdrTest.Test

import Test.Test

suite : IO ()
suite = do
  runSuites
    [ Test.Test.suite
    ]


text:
s : String
s = """
  First line

  Third line
  """

ss : String
ss = "First line\nThird line"

sss : Main.s = Main.ss
sss = Refl

prS : IO ()
prS = putStrLn s

t : String
t = """
  First line

  Third line
  """

tt : String
tt = "First line\n\nThird line"

ttt : Main.t = Main.tt
ttt = Refl

prT : IO ()
prT = putStrLn t

max_stars_repo_name: buzden/idris-playground

max_issues_repo_name: buzden/idris-playground

max_forks_repo_name: buzden/idris-playground


text:
module System

import public Data.So
import Data.List
import Data.String

%default total

support : String -> String
support fn = "C:" ++ fn ++ ", libidris2_support, idris_support.h"

libc : String -> String
libc fn = "C:" ++ fn ++ ", libc 6"

-- `sleep` and `usleep` need to be tied to `blodwen-[u]sleep` for threading
-- reasons (see support/racket/support.rkt)

%foreign "scheme,racket:blodwen-sleep"
         support "idris2_sleep"
         "jvm:sleep(int void),io/github/mmhelloworld/idrisjvm/runtime/IdrisSystem"
prim__sleep : Int -> PrimIO ()

%foreign "scheme,racket:blodwen-usleep"
         support "idris2_usleep"
         "jvm:usleep(int void),io/github/mmhelloworld/idrisjvm/runtime/IdrisSystem"
prim__usleep : Int -> PrimIO ()

export
sleep : HasIO io => Int -> io ()
sleep sec = primIO (prim__sleep sec)

export
usleep : HasIO io => (x : Int) -> So (x >= 0) => io ()
usleep sec = primIO (prim__usleep sec)

-- Get the number of arguments
%foreign "scheme:blodwen-arg-count"
         support "idris2_getArgCount"
         "node:lambda:() => process.argv.length"
         "jvm:getProgramArgCount(int),io/github/mmhelloworld/idrisjvm/runtime/Runtime"
prim__getArgCount : PrimIO Int

-- Get argument number `n`
%foreign "scheme:blodwen-arg"
         support "idris2_getArg"
         "node:lambda:n => process.argv[n]"
         "jvm:getProgramArg(int java/lang/String),io/github/mmhelloworld/idrisjvm/runtime/Runtime"
prim__getArg : Int -> PrimIO String

export
getArgs : HasIO io => io (List String)
getArgs = do
            n <- primIO prim__getArgCount
            if n > 0
              then for [0..n-1] $ primIO . prim__getArg
              else pure []

%foreign libc "getenv"
         "node:lambda: n => process.env[n]"
         "jvm:getEnv(java/lang/String java/lang/String),io/github/mmhelloworld/idrisjvm/runtime/IdrisSystem"
prim__getEnv : String -> PrimIO (Ptr String)

%foreign
  support "idris2_getEnvPair"
  "jvm:getEnvPair(int java/lang/String),io/github/mmhelloworld/idrisjvm/runtime/IdrisSystem"
prim__getEnvPair : Int -> PrimIO (Ptr String)
%foreign
  support "idris2_setenv"
  "jvm:setEnv(java/lang/String java/lang/String int int),io/github/mmhelloworld/idrisjvm/runtime/IdrisSystem"
prim__setEnv : String -> String -> Int -> PrimIO Int
%foreign
  support "idris2_unsetenv"
  "jvm:clearEnv(java/lang/String int),io/github/mmhelloworld/idrisjvm/runtime/IdrisSystem"
prim__unsetEnv : String -> PrimIO Int

export
getEnv : HasIO io => String -> io (Maybe String)
getEnv var
   = do env <- primIO $ prim__getEnv var
        if prim__nullPtr env /= 0
           then pure Nothing
           else pure (Just (prim__getString env))

export
covering
getEnvironment : HasIO io => io (List (String, String))
getEnvironment = getAllPairs 0 []
  where
    splitEq : String -> (String, String)
    splitEq str
        = let (k, v)  = break (== '=') str
              (_, v') = break (/= '=') v in
              (k, v')

    getAllPairs : Int -> List String -> io (List (String, String))
    getAllPairs n acc = do
      envPair <- primIO $ prim__getEnvPair n
      if prim__nullPtr envPair /= 0
         then pure $ reverse $ map splitEq acc
         else getAllPairs (n + 1) (prim__getString envPair :: acc)

export
setEnv : HasIO io => String -> String -> Bool -> io Bool
setEnv var val overwrite
   = do ok <- primIO $ prim__setEnv var val (if overwrite then 1 else 0)
        pure $ ok == 0

export
unsetEnv : HasIO io => String -> io Bool
unsetEnv var
   = do ok <- primIO $ prim__unsetEnv var
        pure $ ok == 0

%foreign "C:idris2_system, libidris2_support, idris_system.h"
         "jvm:runCommand(java/lang/String int),io/github/mmhelloworld/idrisjvm/runtime/IdrisSystem"
prim__system : String -> PrimIO Int

export
system : HasIO io => String -> io Int
system cmd = primIO (prim__system cmd)

%foreign support "idris2_time"
         "javascript:lambda:() => Math.floor(new Date().getTime() / 1000)"
         "jvm:time(java/lang/Object int),io/github/mmhelloworld/idrisjvm/runtime/IdrisSystem"
prim__time : PrimIO Int

||| Return the number of seconds since epoch.
export
time : HasIO io => io Integer
time = pure $ cast !(primIO prim__time)

%foreign
  support "idris2_getPID"
  "jvm:getPid(int),io/github/mmhelloworld/idrisjvm/runtime/Runtime"
prim__getPID : PrimIO Int

||| Get the ID of the currently running process.
export
getPID : HasIO io => io Int
getPID = primIO prim__getPID

%foreign libc "exit"
         "node:lambda:c => process.exit(c)"
         "jvm:exit(int void),io/github/mmhelloworld/idrisjvm/runtime/IdrisSystem"
prim__exit : Int -> PrimIO ()

||| Programs can either terminate successfully, or end in a caught
||| failure.
public export
data ExitCode : Type where
  ||| Terminate successfully.
  ExitSuccess : ExitCode
  ||| Program terminated for some prescribed reason.
  |||
  ||| @errNo A non-zero numerical value indicating failure.
  ||| @prf   Proof that the int value is non-zero.
  ExitFailure : (errNo    : Int) -> (So (not $ errNo == 0)) => ExitCode

export
exitWith : HasIO io => ExitCode -> io a
exitWith ExitSuccess = primIO $ believe_me $ prim__exit 0
exitWith (ExitFailure code) = primIO $ believe_me $ prim__exit code

||| Exit the program indicating failure.
export
exitFailure : HasIO io => io a
exitFailure = exitWith (ExitFailure 1)

||| Exit the program after a successful run.
export
exitSuccess : HasIO io => io a
exitSuccess = exitWith ExitSuccess


text:
||| Functions for working with installed Idris 2 versions.
||| These are the things found in the ./versions directory
||| under the Idv install.
module Installed

import Data.Either
import Data.List
import Data.Version
import Data.String
import System.Console.Extra
import System.Directory
import System.Directory.Extra
import System.File.Extra
import System.Path

import IdvPaths
import Interp

versionsDir : String
versionsDir =
  idvLocation </> relativeVersionsPath

||| List the local (i.e. installed) versions of Idris 2.
export
listVersions : HasIO io => io (Maybe (List Version))
listVersions = let (>>=) = Prelude.(>>=) @{Monad.Compose} in do
  pathExpansion versionsDir >>= versions
    where
      replaceUnderscores : String -> String
      replaceUnderscores = pack . replaceOn '_' '.' . unpack

      parseFolderEntries : List String -> List Version
      parseFolderEntries = mapMaybe (parseVersion . replaceUnderscores)

      versionFolders : (path : String) -> io (Maybe (List String))
      versionFolders = (map eitherToMaybe) . listDir

      versions : (path : String) -> io (Maybe (List Version))
      versions path = map parseFolderEntries <$> versionFolders path

||| Check if the given version is installed.
export
isInstalled : HasIO io => Version -> io (Either String Bool)
isInstalled version = do
  Just localVersions <- listVersions
    | Nothing => pure $ Left "Could not look up local versions."
  pure $
    case find (== version) localVersions of
         Nothing      => Right False
         Just version => Right True

||| Check if the given Idris version has the Idris 2 API package installed.
export
hasApiInstalled : HasIO io => Version -> io (Either String Bool)
hasApiInstalled version = do
  versionInstalled <- isInstalled version
  Just libPath <- pathExpansion (idrisApiLibPath version)
    | Nothing => pure $ Left "could not locate Idris 2 libdir."
  pure $ Right !(exists libPath)

||| Remove the symlink that points to the "selected" Idris 2 executable.
export
unselect : HasIO io => io (Either String ())
unselect = do
  Just lnFile <- pathExpansion $ idrisSymlinkedPath
    | Nothing => pure $ Left "Could not resolve Idris 2 symlink path."
  Just lnLspFile <- pathExpansion $ idrisLspSymlinkedPath
    | Nothing => pure $ Left "Could not resolve Idris 2 LSP symlink path."
  Right () <- removeFile lnFile
    | Left FileNotFound => pure $ Right () -- no problem here, job done.
    | Left err => pure $ Left "Failed to remove symlink file (to let system Idris 2 installation take precedence): \{err}."
  Right () <- removeFile lnLspFile
    | Left FileNotFound => pure $ Right () -- no problem here, job done.
    | Left err => pure $ Left "Failed to remove LSP symlink file (to let system Idris 2 installation take precedence): \{err}."
  pure $ Right ()

||| Attempt to select the given version. Fails if the version
||| requested is not installed.
export
selectVersion : HasIO io => Version -> io (Either String ())
selectVersion proposedVersion = do
  Just localVersions <- listVersions
    | Nothing => pure $ Left "Could not look up local versions."
  case find (== proposedVersion) localVersions of
       Nothing      => pure $ Left "Idris 2 version \{proposedVersion} is not installed.\nInstalled versions: \{sort localVersions}."
       Just version => do
         Right () <- unselect
           | Left err => pure $ Left err
         let proposedIdrisInstalled = installedIdrisPath version
         let proposedIdrisSymlinked = idrisSymlinkedPath
         let proposedLspInstalled = installedLspPath version
         let proposedLspSymlinked = idrisLspSymlinkedPath
         Prelude.(>>) @{Monad.Compose}
           (setLink version proposedIdrisInstalled proposedIdrisSymlinked)
           (setLink version proposedLspInstalled proposedLspSymlinked)

  where
    setLink : Version -> (proposedInstalledLocation : String) -> (proposedSymlinkedLocation : String) -> io (Either String ())
    setLink version proposedInstalledLocation proposedSymlinkedLocation =  do
      Just installed <- pathExpansion proposedInstalledLocation
        | Nothing => pure $ Left "Could not resolve install location: \{proposedInstalledLocation}."
      Just linked <- pathExpansion proposedSymlinkedLocation
        | Nothing => pure $ Left "Could not resolve symlinked location: \{proposedSymlinkedLocation}."
      True <- exists installed
        | False => pure $ Right () -- nothing to link to
      True <- symlink installed linked
        | False => pure $ Left "Failed to create symlink for Idris 2 version \{version}."
      pure $ Right ()

||| Get the version of the Idris installed at the given path.
export
getVersion : HasIO io => (idrisExecPath : String) -> io (Maybe Version)
getVersion idrisExecPath = do
  Just symPath <- pathExpansion idrisExecPath
    | Nothing => pure Nothing
  True <- exists symPath
    | False => pure Nothing
  out <- (map trim) <$> readLines (limit 1) True "\{symPath} --version"
  pure $ head' out >>= parseSpokenVersion

export
getSystemVersion : HasIO io => io (Maybe Version)
getSystemVersion =
  let (=<<) = Prelude.(=<<) @{Monad.Compose}
  in  getVersion =<< systemIdrisPath

export
getSelectedVersion : HasIO io => io (Maybe Version)
getSelectedVersion = getVersion idrisSymlinkedPath

||| Use the given version for an operation and then switch back.
export
withVersion : HasIO io => Version -> io (Either String a) -> io (Either String a)
withVersion version op = do
  previousVersion <- getSelectedVersion
  Right () <- selectVersion version
    | Left err => pure $ Left err
  res <- op
  Right () <- undoSelect previousVersion
    | Left err => pure $ Left err
  pure res
    where
      undoSelect : (previous : Maybe Version) -> io (Either String ())
      undoSelect Nothing  = unselect
      undoSelect (Just v) = selectVersion version

max_stars_repo_name: memoryruins/idv

max_issues_repo_name: memoryruins/idv

max_forks_repo_name: memoryruins/idv


text:
module Mmhelloworld.IdrisJackson.Databind

import IdrisJvm.IO

%access public export

SerializerProvider : Type
SerializerProvider = JVM_Native (Class "com/fasterxml/jackson/databind/SerializerProvider")

JsonDeserializer : Type
JsonDeserializer = JVM_Native (Class "com/fasterxml/jackson/databind/JsonDeserializer")

JsonSerializer : Type
JsonSerializer = JVM_Native (Class "com/fasterxml/jackson/databind/JsonSerializer")

DeserializationContext : Type
DeserializationContext = JVM_Native (Class "com/fasterxml/jackson/databind/DeserializationContext")

JsonNode : Type
JsonNode = JVM_Native (Class "com/fasterxml/jackson/databind/JsonNode")

max_stars_repo_name: mmhelloworld/idris-jackson

max_issues_repo_name: mmhelloworld/idris-jackson

max_forks_repo_name: mmhelloworld/idris-jackson


text:
module Parser.Support

import public Libraries.Text.Lexer.Tokenizer
import public Libraries.Text.Lexer
import public Libraries.Text.Parser
import Libraries.Data.String.Extra
import public Libraries.Text.PrettyPrint.Prettyprinter
import Libraries.Text.PrettyPrint.Prettyprinter.Util

import Core.TT
import Core.Core
import Data.List
import Data.List.Views
import Data.String
import Parser.Unlit
import System.File

%default total

export
fromLitError : OriginDesc -> LiterateError -> Error
fromLitError origin (MkLitErr l c _) = LitFail (MkFC origin (l, c) (l, c + 1))

export
fromLexError : OriginDesc -> (StopReason, Int, Int, String) -> Error
fromLexError origin (ComposeNotClosing begin end, _, _, _)
    = LexFail (MkFC origin begin end) "Bracket is not properly closed."
fromLexError origin (_, l, c, _)
    = LexFail (MkFC origin (l, c) (l, c + 1)) "Can't recognise token."

export
fromParsingErrors : (Show token, Pretty token) =>
                    OriginDesc -> List1 (ParsingError token) -> Error
fromParsingErrors origin = ParseFail . (map fromError)
  where
    fromError : ParsingError token -> (FC, String)
    fromError (Error msg Nothing)
        = (MkFC origin (0, 0) (0, 0), msg +> '.')
    fromError (Error msg (Just t))
        = let start = startBounds t; end = endBounds t in
            let fc = if start == end
                      then MkFC origin start (mapSnd (+1) start)
                      else MkFC origin start end
            in (fc, msg +> '.')

export
hex : Char -> Maybe Int
hex '0' = Just 0
hex '1' = Just 1
hex '2' = Just 2
hex '3' = Just 3
hex '4' = Just 4
hex '5' = Just 5
hex '6' = Just 6
hex '7' = Just 7
hex '8' = Just 8
hex '9' = Just 9
hex 'a' = Just 10
hex 'b' = Just 11
hex 'c' = Just 12
hex 'd' = Just 13
hex 'e' = Just 14
hex 'f' = Just 15
hex _ = Nothing

export
dec : Char -> Maybe Int
dec '0' = Just 0
dec '1' = Just 1
dec '2' = Just 2
dec '3' = Just 3
dec '4' = Just 4
dec '5' = Just 5
dec '6' = Just 6
dec '7' = Just 7
dec '8' = Just 8
dec '9' = Just 9
dec _ = Nothing

export
oct : Char -> Maybe Int
oct '0' = Just 0
oct '1' = Just 1
oct '2' = Just 2
oct '3' = Just 3
oct '4' = Just 4
oct '5' = Just 5
oct '6' = Just 6
oct '7' = Just 7
oct _ = Nothing

export
getEsc : String -> Maybe Char
getEsc "NUL" = Just '\NUL'
getEsc "SOH" = Just '\SOH'
getEsc "STX" = Just '\STX'
getEsc "ETX" = Just '\ETX'
getEsc "EOT" = Just '\EOT'
getEsc "ENQ" = Just '\ENQ'
getEsc "ACK" = Just '\ACK'
getEsc "BEL" = Just '\BEL'
getEsc "BS" = Just '\BS'
getEsc "HT" = Just '\HT'
getEsc "LF" = Just '\LF'
getEsc "VT" = Just '\VT'
getEsc "FF" = Just '\FF'
getEsc "CR" = Just '\CR'
getEsc "SO" = Just '\SO'
getEsc "SI" = Just '\SI'
getEsc "DLE" = Just '\DLE'
getEsc "DC1" = Just '\DC1'
getEsc "DC2" = Just '\DC2'
getEsc "DC3" = Just '\DC3'
getEsc "DC4" = Just '\DC4'
getEsc "NAK" = Just '\NAK'
getEsc "SYN" = Just '\SYN'
getEsc "ETB" = Just '\ETB'
getEsc "CAN" = Just '\CAN'
getEsc "EM" = Just '\EM'
getEsc "SUB" = Just '\SUB'
getEsc "ESC" = Just '\ESC'
getEsc "FS" = Just '\FS'
getEsc "GS" = Just '\GS'
getEsc "RS" = Just '\RS'
getEsc "US" = Just '\US'
getEsc "SP" = Just '\SP'
getEsc "DEL" = Just '\DEL'
getEsc str = Nothing

escape' : List Char -> List Char -> Maybe (List Char)
escape' _ [] = pure []
escape' escapeChars (x::xs)
    = assert_total $ if escapeChars `isPrefixOf` (x::xs)
         then case drop (length escapeChars) (x::xs) of
                   ('\\' :: xs) => pure $ '\\' :: !(escape' escapeChars xs)
                   ('\n' :: xs) => pure !(escape' escapeChars xs)
                   ('&' :: xs) => pure !(escape' escapeChars xs)
                   ('a' :: xs) => pure $ '\a' :: !(escape' escapeChars xs)
                   ('b' :: xs) => pure $ '\b' :: !(escape' escapeChars xs)
                   ('f' :: xs) => pure $ '\f' :: !(escape' escapeChars xs)
                   ('n' :: xs) => pure $ '\n' :: !(escape' escapeChars xs)
                   ('r' :: xs) => pure $ '\r' :: !(escape' escapeChars xs)
                   ('t' :: xs) => pure $ '\t' :: !(escape' escapeChars xs)
                   ('v' :: xs) => pure $ '\v' :: !(escape' escapeChars xs)
                   ('\'' :: xs) => pure $ '\'' :: !(escape' escapeChars xs)
                   ('"' :: xs) => pure $ '"' :: !(escape' escapeChars xs)
                   ('x' :: xs) => case span isHexDigit xs of
                                       ([], rest) => escape' escapeChars rest
                                       (ds, rest) => pure $ cast !(toHex 1 (reverse ds)) ::
                                                             !(escape' escapeChars rest)
                   ('o' :: xs) => case span isOctDigit xs of
                                       ([], rest) => escape' escapeChars rest
                                       (ds, rest) => pure $ cast !(toOct 1 (reverse ds)) ::
                                                             !(escape' escapeChars rest)
                   xs => case span isDigit xs of
                              ([], (a :: b :: c :: rest)) =>
                                case getEsc (fastPack [a, b, c]) of
                                     Just v => Just (v :: !(escape' escapeChars rest))
                                     Nothing => case getEsc (fastPack [a, b]) of
                                                     Just v => Just (v :: !(escape' escapeChars (c :: rest)))
                                                     Nothing => escape' escapeChars xs
                              ([], (a :: b :: [])) =>
                                case getEsc (fastPack [a, b]) of
                                     Just v => Just (v :: [])
                                     Nothing => escape' escapeChars xs
                              ([], rest) => escape' escapeChars rest
                              (ds, rest) => Just $ cast (cast {to=Int} (fastPack ds)) ::
                                              !(escape' escapeChars rest)
         else Just $ x :: !(escape' escapeChars xs)
  where
    toHex : Int -> List Char -> Maybe Int
    toHex _ [] = Just 0
    toHex m (d :: ds)
        = pure $ !(hex (toLower d)) * m + !(toHex (m*16) ds)

    toOct : Int -> List Char -> Maybe Int
    toOct _ [] = Just 0
    toOct m (d :: ds)
        = pure $ !(oct (toLower d)) * m + !(toOct (m*8) ds)

export
escape : Nat -> String -> Maybe String
escape hashtag x = let escapeChars = '\\' :: replicate hashtag '#' in
                       fastPack <$> (escape' escapeChars (unpack x))

export
getCharLit : String -> Maybe Char
getCharLit str
   = do e <- escape 0 str
        if length e == 1
           then Just (assert_total (prim__strHead e))
           else if length e == 0 -- parsed the NULL character that terminated the string!
                   then Just '\0000'
                   else Nothing


text:
module Utils

public export
data Image = mkImage

public export
fetchImage : (url : String) -> (1 _ : ((1 _ : Image) -> Image)) -> Image
fetchImage = believe_me

public export
cropImage : (1 _ : Image) -> Image
cropImage image = image

public export
transposeImage : (1 _ : Image) -> Image
transposeImage image = image

data FileHandle = MkFileHandle

public export
openFile : (1 _ : String) -> IO FileHandle

public export
read : (1 _ : FileHandle) -> IO (LPair String FileHandle)

public export
closeFile : (1 _ : FileHandle) -> IO ()

public export
seq : (1 _ : IO ()) -> IO String -> IO String

public export
utf8Decode : String -> String

public export
myBind : (1 _ : IO a) -> (1 _ : ((1 _ : a) -> IO b)) -> IO b


text:
module JS.Callback

import JS.Util

||| Interface for converting Idris functions to
||| an external callback type.
|||
||| @cb  external callback type (for instance `EventListener`
||| @fun Idris function type
public export
interface Callback cb fun | cb where
  callback : fun -> JSIO cb


text:
-- Borrowed from Botta at https://gitlab.pik-potsdam.de/botta/IdrisLibs/blob/master/Nat/LTEProperties.lidr

module Positive

%default total
%access public export
%auto_implicits on

|||
data Positive : Nat -> Type where
  MkPositive  : {n : Nat} -> Positive (S n)

|||
fromSucc : (m : Nat) -> (n : Nat) -> S m = n -> Positive n
fromSucc m n prf = s2 where
  s1 : Positive (S m)
  s1 = MkPositive
  s2 : Positive n
  s2 = replace prf s1

|||
implementation Uninhabited (Positive Z) where
  uninhabited (MkPositive {n}) impossible

|||
positiveNotZ : {n : Nat} -> Positive n -> Not (n = Z)
positiveNotZ {n = Z}   p = absurd p
positiveNotZ {n = S m} _ = SIsNotZ

|||
plusPreservesPositivity : Positive m -> Positive n -> Positive (m + n)
plusPreservesPositivity {m = Z  } {n      } MkPositive _            impossible
plusPreservesPositivity {m      } {n = Z  } _          MkPositive   impossible
plusPreservesPositivity {m = S m} {n = S n} _          _          = MkPositive

|||
multPreservesPositivity : Positive m -> Positive n -> Positive (m * n)
multPreservesPositivity {m = Z  } {n      } MkPositive _            impossible
multPreservesPositivity {m      } {n = Z  } _          MkPositive   impossible
multPreservesPositivity {m = S m} {n = S n} _          _          = MkPositive

max_stars_repo_name: zenntenn/Idris-NumericProofs

max_issues_repo_name: zenntenn/Idris-NumericProofs

max_forks_repo_name: zenntenn/Idris-NumericProofs


text:
module Toolkit.Data.Vect.Leanings

import Data.Vect

import Toolkit.Data.DVect

namespace Index
  public export
  data Leans : (o,l,c,r : Nat) -> Type where
    Empty : Leans Z Z Z Z

    Left : Leans    os     ls  cs rs
        -> Leans (S os) (S ls) cs rs

    Center : Leans    os  ls    cs  rs
          -> Leans (S os) ls (S cs) rs

    Right : Leans    os  ls cs    rs
         -> Leans (S os) ls cs (S rs)

public export
data IsCenter : (type    : Type)
             -> (goLeft  : type -> Type)
             -> (goRight : type -> Type)
             -> (o       : type)
                        -> Type
  where
    C : (noLeft  : left  o -> Void)
     -> (noRight : right o -> Void)
                -> IsCenter type left right o

public export
data Leaning : (type    : Type)
            -> (goLeft  : type -> Type)
            -> (goRight : type -> Type)
            -> (idx     : Leans o l c r)
            -> (os      : Vect  o        type)
            -> (ls      : Vect    l      type)
            -> (cs      : Vect      c    type)
            -> (rs      : Vect        r  type)
                       -> Type
  where
    Empty : Leaning type left right Empty Nil Nil Nil Nil

    Left : {o : type}
        -> (prf  : left o)
        -> (rest : Leaning type left right       idx      os      ls  cs rs)
                -> Leaning type left right (Left idx) (o::os) (o::ls) cs rs

    Center : {o : type}
          -> (prf  : IsCenter type left right o)
          -> (rest : Leaning  type left right         idx      os  ls     cs  rs)
                  -> Leaning  type left right (Center idx) (o::os) ls (o::cs) rs

    Right : {o : type}
         -> (prf  : right o)
         -> (rest : Leaning type left right        idx      os  ls cs     rs)
                 -> Leaning type left right (Right idx) (o::os) ls cs (o::rs)

public export
data Result : (type    : Type)
           -> (isLeft  : (o : type) -> Type)
           -> (isRight : (o : type) -> Type)
           -> (os      : Vect o type)
                      -> Type
  where
    R : (lefts   : Vect l type)
     -> (centers : Vect c type)
     -> (rights  : Vect r type)
     -> (idx     : Leans o l c r)

     -> (leaning   : Leaning type isLeft isRight idx os lefts centers rights)
     -> (prfLeft   : DVect type isLeft l lefts)
     -> (prfCenter : DVect type (IsCenter type isLeft isRight) c centers)
     -> (prfRight  : DVect type isRight r rights)
                  -> Result type isLeft isRight os

export
leans : {type  : Type}
     -> {left  : type -> Type}
     -> {right : type -> Type}
     -> (isLeft  : (o : type) -> Dec (left  o))
     -> (isRight : (o : type) -> Dec (right o))
     -> (os      : Vect o type)
                -> Result type left right os
leans isLeft isRight []
  = R [] [] [] Empty Empty [] [] []

leans l r (x :: xs) with (l x)
  leans l r (x :: xs) | (Yes prf) with (leans l r xs)
    leans l r (x :: xs) | (Yes prf) | (R lefts centers rights idx lean prfLeft prfCenter prfRight)
      = R (x::lefts) centers rights (Left idx) (Left prf lean) (prf :: prfLeft) prfCenter prfRight

  leans l r (x :: xs) | (No noL) with (r x)
    leans l r (x :: xs) | (No noL) | (Yes prf) with (leans l r xs)
      leans l r (x :: xs) | (No noL) | (Yes prf) | (R ls cs rs idx lean pLs pCs pRs)
        = R ls cs (x::rs) (Right idx) (Right prf lean) pLs pCs (prf :: pRs)

    leans l r (x :: xs) | (No noL) | (No noR) with (leans l r xs)
      leans l r (x :: xs) | (No noL) | (No noR) | (R ls cs rs idx lean pLs pCs pRs)
        = R ls (x::cs) rs (Center idx) (Center (C noL noR) lean) pLs (C noL noR :: pCs) pRs

namespace Poll

  public export
  data LeansLeft : (poll : Leaning type l r i os ls rs cs)
                        -> Type
    where
      EmptyL : LeansLeft Empty

      IsLeft : {rest  : Leaning type l r i os ls cs rs}
            -> {prf   : l o}
            -> (later : LeansLeft           rest)
                     -> LeansLeft (Left prf rest)

  Uninhabited (LeansLeft (Center prf rest)) where
    uninhabited EmptyL impossible
    uninhabited (IsLeft later) impossible

  Uninhabited (LeansLeft (Right prf rest)) where
    uninhabited EmptyL impossible
    uninhabited (IsLeft later) impossible

  export
  leansLeft : (poll : Leaning type l r i os ls cs rs)
                   -> Dec (LeansLeft poll)
  leansLeft Empty
    = Yes EmptyL

  leansLeft (Left prf rest) with (leansLeft rest)
    leansLeft (Left prf rest) | (Yes x)
      = Yes (IsLeft x)

    leansLeft (Left prf rest) | (No contra)
      = No (\(IsLeft later) => contra later)

  leansLeft (Center prf rest)
    = No absurd

  leansLeft (Right prf rest)
    = No absurd

  public export
  data LeansRight : (poll : Leaning type l r i os ls cs rs)
                        -> Type
    where
      EmptyR : LeansRight Empty

      IsRight : {rest  : Leaning type l r i os ls cs rs}
             -> {prf   : r o}
             -> (later : LeansRight rest)
                      -> LeansRight (Right prf rest)

  Uninhabited (LeansRight (Center prf rest)) where
    uninhabited EmptyR impossible
    uninhabited (IsRight later) impossible

  Uninhabited (LeansRight (Left prf rest)) where
    uninhabited EmptyR impossible
    uninhabited (IsRight later) impossible

  export
  leansRight : (poll : Leaning type l r i os ls cs rs)
                    -> Dec (LeansRight poll)
  leansRight Empty
    = Yes EmptyR

  leansRight (Right prf rest) with (leansRight rest)
    leansRight (Right prf rest) | (Yes x)
      = Yes (IsRight x)

    leansRight (Right prf rest) | (No contra)
      = No (\(IsRight later) => contra later)

  leansRight (Center prf rest)
    = No absurd

  leansRight (Left prf rest)
    = No absurd

  public export
  data LeansCenter : (poll : Leaning type l r i os ls cs rs)
                        -> Type
    where
      EmptyC : LeansCenter Empty

      IsCenter : {rest  : Leaning type l r i os ls cs rs}
              -> {prf   : IsCenter type l r o}
              -> (later : LeansCenter rest)
                       -> LeansCenter (Center prf rest)

  Uninhabited (LeansCenter (Right prf rest)) where
    uninhabited EmptyC impossible
    uninhabited (IsCenter later) impossible

  Uninhabited (LeansCenter (Left prf rest)) where
    uninhabited EmptyC impossible
    uninhabited (IsCenter later) impossible

  export
  leansCenter : (poll : Leaning type l r i os ls cs rs)
                     -> Dec (LeansCenter poll)
  leansCenter Empty
    = Yes EmptyC

  leansCenter (Center prf rest) with (leansCenter rest)
    leansCenter (Center prf rest) | (Yes x)
      = Yes (IsCenter x)

    leansCenter (Center prf rest) | (No contra)
      = No (\(IsCenter later) => contra later)

  leansCenter (Right prf rest)
    = No absurd

  leansCenter (Left prf rest)
    = No absurd

public export
data HowLeans : (poll : Leaning type l r i os ls cs rs) -> Type where
  LE : HowLeans Empty
  LL : LeansLeft poll -> HowLeans poll

  LC : (LeansLeft  poll -> Void)
    -> (LeansRight poll -> Void)
    -> HowLeans poll

  LR : LeansRight poll -> HowLeans poll

export
howLeans : (poll : Leaning type l r i os ls cs rs) -> HowLeans poll
howLeans {ls=Nil} {cs=Nil} {rs=Nil} Empty = LE

howLeans {ls} {cs} {rs} poll with (leansLeft poll)
  howLeans {ls = ls} {cs = cs} {rs = rs} poll | (Yes prf)
    = LL prf

  howLeans {ls = ls} {cs = cs} {rs = rs} poll | (No noL) with (leansRight poll)
    howLeans {ls = ls} {cs = cs} {rs = rs} poll | (No noL) | (Yes prf)
      = LR prf

    howLeans {ls = ls} {cs = cs} {rs = rs} poll | (No noL) | (No noR)
      = LC noL noR

-- [ EOF ]

max_stars_repo_name: gallais/linear-circuits

max_issues_repo_name: gallais/linear-circuits

max_forks_repo_name: gallais/linear-circuits


text:
module System.File.Mode

import System.Info

%default total

public export
data Mode = Read | WriteTruncate | Append | ReadWrite | ReadWriteTruncate | ReadAppend

export
modeStr : Mode -> String
modeStr Read              = if isWindows then "rb" else "r"
modeStr WriteTruncate     = if isWindows then "wb" else "w"
modeStr Append            = if isWindows then "ab" else "a"
modeStr ReadWrite         = if isWindows then "rb+" else "r+"
modeStr ReadWriteTruncate = if isWindows then "wb+" else "w+"
modeStr ReadAppend        = if isWindows then "ab+" else "a+"


text:
import Data.Vect

total allLengths : Vect len String -> Vect len Nat
allLengths [] = []
allLengths (x :: xs) = length x :: allLengths xs

max_stars_repo_name: brunoflores/type-driven-with-idris

max_issues_repo_name: brunoflores/type-driven-with-idris

max_forks_repo_name: brunoflores/type-driven-with-idris


text:
module Main

data RLE : Vect n Char -> Type where
     REnd  : RLE []
     RChar : {xs : Vect k Char} ->
             (n : Nat) -> (c : Char) -> (rs : RLE xs) ->
             RLE (replicate (S n) c ++ xs)

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

rle : (xs : Vect n Char) -> RLE xs
rle [] = REnd
rle (x :: xs) with (rle xs)
  rle (x :: []) | REnd = RChar 0 x REnd
  rle (x :: (c :: (replicate n c ++ ys))) | (RChar n c rs) with (decEq x c)
    rle (x :: (x :: (replicate n x ++ ys))) | (RChar n x rs) | (Yes refl)
        = RChar (S n) x rs
    rle (x :: (c :: (replicate n c ++ ys))) | (RChar n c rs) | (No f)
        = RChar 0 x (RChar n c rs)

compress : Vect n Char -> String
compress xs with (rle xs)
  compress [] | REnd = ""
  compress (c :: (replicate n c ++ xs1)) | (RChar n c rs)
       = show (the Integer (cast (S n))) ++
           strCons c (compress xs1)

compressString : String -> String
compressString xs = compress (fromList (unpack xs))

main : IO ()
main = putStrLn (compressString "foooobaaaarbaaaz")

max_stars_repo_name: silky/idris-demos

max_issues_repo_name: silky/idris-demos

max_forks_repo_name: silky/idris-demos


text:
module Salo.Language.Parser

import Salo.Language.Lexer
import Salo.Language.TT
import Salo.Language.AST

import Text.Lexer
import Text.Parser

import Data.SortedMap

Rule : Type -> Type
Rule = Grammar (TokenData Token) True

record Globals where
  constructor MkGlobals
  definitions : SortedMap Name (Definition)

implementation Show Globals where
  show x = "Globals: " ++ show x.definitions

token : Token -> Rule ()
token t = terminal ("expecting " ++ show t) $ \t' =>
  if t == tok t'
    then Just ()
    else Nothing

kwd : String -> Rule ()
kwd s = token (Keyword s)

dataDecl : Rule Definition
dataDecl = do
  kwd "data"
  pure (MkDef (B "AAA" (P)) Postulate)

export
parse : String -> Either ParseError (Definition)
parse src = case lex src of
  Left err => Left err
  Right ts => case Text.Parser.Core.parse (dataDecl <* eof) ts of
    Left (Error msg []) => Left $ SyntaxError 0 0 msg []
    Left (Error msg (tt :: tts)) => Left $ SyntaxError (line tt) (col tt) msg (tt :: tts)
    Right (gs, []) => Right gs
    Right (gs, t::ts) => Left $ SyntaxError (line t) (col t) "eof expected" (t :: ts)

namespace Test
  namespace Examples
    export
    exampleData : List (TokenData Token)
    exampleData = [MkToken 0 0 (Keyword "data")]

  ParserType : Type
  ParserType = Either ParseError (Definition)

  parseData : ParserType
  parseData = parse "data"

  testHarness : ParserType -> IO ()
  testHarness t = case t of
    Left err => putStrLn $ "  -> Error: "   ++ (show err)
    Right gs => putStrLn $ "  -> Success: " ++ (show gs)

  export
  test : IO ()
  test = do putStrLn "Parser:"
            testHarness parseData

max_stars_repo_name: semissioncontrol/semcos

max_issues_repo_name: semissioncontrol/semcos

max_forks_repo_name: semissioncontrol/semcos


text:
import Data.List

data Color = White | Yellow | Orange | Red | Green | Blue
data Piece = Up | Down | Left | Right | Front | Back -- только для наглядности
           | UpFL | UpFR | UpBL | UpBR | DownFL | DownFR | DownBL | DownBR
           | LeftFU | LeftFD | LeftBU | LeftBD | RightFU | RightFD | RightBU | RightBD
           | FrontUL | FrontUR | FrontDL | FrontDR | BackUL | BackUR | BackDL | BackDR

record Cube where
    constructor MkCube
    stickers : List Color
    pieces : List Piece
    groups : List ( -- список возможных поворотов
                   List ( -- список групп перемещений наклеек
                         List Piece)) -- группа перемещений наклеек
    blocks : List (List Piece)

cube1x1x1 : Cube
cube1x1x1 = MkCube [White, Yellow, Orange, Red, Green, Blue]
                   [Up, Down, Left, Right, Front, Back]
                   [ [ [Up, Back, Down, Front] ], -- x
                     [ [Up, Right, Down, Left] ], -- y
                     [ [Front, Right, Back, Left] ] ] -- z
                   []

cube2x2x2 : Cube
cube2x2x2 = MkCube [White, White, White, White, Yellow, Yellow, Yellow, Yellow,
                    Orange, Orange, Orange, Orange, Red, Red, Red, Red,
                    Green, Green, Green, Green, Blue, Blue, Blue, Blue]
                   [UpFL, UpFR, UpBL, UpBR, DownFL, DownFR, DownBL, DownBR,
                    LeftFU, LeftFD, LeftBU, LeftBD, RightFU, RightFD, RightBU, RightBD,
                    FrontUL, FrontUR, FrontDL, FrontDR, BackUL, BackUR, BackDL, BackDR]
                   [ [ [UpFL, BackUL, DownBL, FrontDL],
                       [UpFR, BackUR, DownBR, FrontDR],
                       [UpBL, BackDL, DownFL, FrontUL],
                       [UpBR, BackDR, DownFR, FrontUR],
                       [LeftFU, LeftBU, LeftBD, LeftFD],
                       [RightFU, RightBU, RightBD, RightFD] ], -- x
                     [ [UpFL, RightFU, DownFR, LeftFD],
                       [UpFR, RightFD, DownFL, LeftFU],
                       [UpBL, RightBU, DownBR, LeftBD],
                       [UpBR, RightBD, DownBL, LeftBU],
                       [FrontUL, FrontUR, FrontDR, FrontDL],
                       [BackUL, BackUR, BackDR, BackDL] ], -- y
                     [ [UpFL, BackUL, DownBL, FrontDL],
                       [UpBL, BackDL, DownFL, FrontUL],
                       [LeftFU, LeftBU, LeftBD, LeftFD] ] ] -- L
                   []

cube1x2x2 : Cube
cube1x2x2 = ?hole122
-- cube1x2x2 = record {blocks = []} cube2x2x2

toNat : Piece -> Nat
toNat Up = 0
toNat Down = 1
toNat Left = 2
toNat Right = 3
toNat Front = 4
toNat Back = 5
toNat UpFL = 0 -- zn as indexation list
toNat UpFR = 1
toNat UpBL = 2
toNat UpBR = 3
toNat DownFL = 4
toNat DownFR = 5
toNat DownBL = 6
toNat DownBR = 7
toNat LeftFU = 8
toNat LeftFD = 9
toNat LeftBU = 10
toNat LeftBD = 11
toNat RightFU = 12
toNat RightFD = 13
toNat RightBU = 14
toNat RightBD = 15
toNat FrontUL = 16
toNat FrontUR = 17
toNat FrontDL = 18
toNat FrontDR = 19
toNat BackUL = 20
toNat BackUR = 21
toNat BackDL = 22
toNat BackDR = 23

Cast Piece Nat where
    cast piece = toNat piece

Eq Piece where
    x == y = (toNat x) == (toNat y)

Cast (List Piece) (List Nat) where
    cast [] = []
    cast (x :: xs) = cast x :: cast xs

Cast (List (List Piece)) (List (List Nat)) where
    cast [] = []
    cast (x :: xs) = cast x :: cast xs

Eq (Nat, Color) where
    (n1,_) == (n2,_) = n1 == n2

Ord (Nat, Color) where
    compare (n1,_) (n2,_) = compare n1 n2

Show Color where
    show White = "White"
    show Yellow = "Yellow"
    show Orange = "Orange"
    show Red = "Red"
    show Green = "Green"
    show Blue = "Blue"

Show Cube where
    show cube = show (stickers cube)

rotate : Nat -> Cube -> Maybe Cube
rotate n cube =
    let group = indexT n (groups cube) in
        case checkBlocked group (blocks cube) of
            True => Nothing
            False => Just (record {stickers = multiperm (cast group) (stickers cube)} cube) where

    -- TODO stdlib
    indexT : Nat -> List (List a) -> List a
    indexT _ [] = []
    indexT Z (x :: xs) = x
    indexT (S k) (_ :: xs) = indexT k xs

    checkBlocked : List (List Piece) -> List (List Piece) -> Bool
    checkBlocked xs ys = alienElem (flat xs) (flat ys) where

        -- TODO stdlib
        flat : List (List a) -> List a
        flat [] = []
        flat ([] :: xxs) = flat xxs
        flat (l@(x :: xs) :: xxs) = l ++ flat xxs

        -- TODO stdlib
        isElem : Eq a => a -> List a -> Bool
        isElem _ [] = False
        isElem x (y :: ys) =
            if x == y
                then True
                else isElem x ys

        alienElem : Eq a => (checked : List a) -> (checker : List a) -> Bool
        alienElem [] _ = True -- not alien in first list
        alienElem _ [] = False -- find alien in first list
        alienElem (x :: xs) ys =
            if isElem x ys
                then alienElem xs ys
                else False

    multiperm : List (List Nat) -> List Color -> List Color
    multiperm [] xs = xs
    multiperm (i :: is) xs = multiperm is (perm i xs) where

        perm : List Nat -> List Color -> List Color
        perm is xs = new 0 xs . sort . get 0 xs . sort $ zip is (shift is) where

            new : (index : Nat) -> (elems : List Color) -> (saved : List (Nat, Color)) -> List Color
            new _ elems [] = elems
            new n (elem :: elems) saved@((i, savedElem) :: saveds) =
                if n == i
                    then savedElem :: new (n+1) elems saveds
                    else elem :: new (n+1) elems saved
            new _ _ _ = []

            get : (index : Nat) -> (elems : List Color) -> (indexs : List (Nat, Nat)) -> List (Nat, Color)
            get i (elem :: elems) indexs@((indexFrom, indexDest) :: indexsFromDest) =
                if i == indexFrom
                    then (indexDest, elem) :: get (i + 1) elems indexsFromDest
                    else get (i + 1) elems indexs
            get _ _ _ = []

            -- TODO stdlib
            shift : List Nat -> List Nat
            shift [] = []
            shift (x :: xs) = xs ++ [x]

main : IO ()
main = putStrLn . show . rotate 1 $ cube2x2x2

max_stars_repo_name: mjdtdw/rubik

max_issues_repo_name: mjdtdw/rubik

max_forks_repo_name: mjdtdw/rubik


text:
module Rohitkumar.Odds

import Evens

import Intro

{-1-}
public export
data IsOdd : Nat -> Type where
  OneOdd : IsOdd 1
  SSOdd : (n : Nat) -> IsOdd n -> IsOdd (S (S n))
{-2-}
threeIsOdd : IsOdd 3
threeIsOdd = SSOdd (S Z) OneOdd
{-3-}
twonotOdd : IsOdd 2 -> Void
twonotOdd (SSOdd Z OneOdd) impossible
twonotOdd (SSOdd Z (SSOdd _ _)) impossible
{-4-}
nOddThenSnEven : (n : Nat) -> IsOdd n -> IsEven (S n)
nOddThenSnEven (S Z) OneOdd = SSEven Z ZEven
nOddThenSnEven (S (S k)) (SSOdd k x) = SSEven (S k) (nOddThenSnEven k x)
{-5-}
nEvenThenSnOdd : (n : Nat) -> IsEven n -> IsOdd (S n)
nEvenThenSnOdd Z ZEven = OneOdd
nEvenThenSnOdd (S (S k)) (SSEven k x) = SSOdd (S k) (nEvenThenSnOdd k x)
{-6-}
nEitherEvenorOdd : (n : Nat) -> Either (IsEven n) (IsOdd n)
nEitherEvenorOdd Z = Left ZEven
nEitherEvenorOdd (S k) = case (nEitherEvenorOdd k) of
                          (Left l) => Right (nEvenThenSnOdd k l)
                          (Right r) => Left (nOddThenSnEven k r)
{-7-}
nNotEvenandOdd : (n: Nat) -> IsEven n -> IsOdd n -> void
nNotEvenandOdd Z ZEven OneOdd impossible
nNotEvenandOdd Z ZEven (SSOdd _ _) impossible
nNotEvenandOdd (S (S k)) (SSEven k x) (SSOdd k y) = nNotEvenandOdd k x y

{-8-}
nmOddThennmEven : (n : Nat) -> IsOdd n -> (m : Nat) -> IsOdd m -> IsEven (add n m)
nmOddThennmEven (S Z) OneOdd j y = nOddThenSnEven j y
nmOddThennmEven (S (S k)) (SSOdd k x) j y = (SSEven (add k j) (nmOddThennmEven k x j y))
{-9-}
genRefl : (f : (Nat -> Nat)) -> (n : Nat) -> (m : Nat) -> n = m -> f n = f m
genRefl f m m Refl = Refl

halfTheOdd : (n : Nat) -> IsOdd n -> (m : Nat ** ((S (double m)) = n))
halfTheOdd (S Z) OneOdd = (Z ** Refl)
halfTheOdd (S (S k)) (SSOdd k x) = case (halfTheOdd k x) of
                                    (m ** pf) => ((S m) ** (genRefl (\l => S (S l)) (S (double m)) k pf))


text:
import Data.Vect

myLength : List a -> Nat
myLength [] = 0
myLength (x :: xs) = 1 + myLength xs

myReverse' : (acc : List a) -> (xs : List a) -> List a
myReverse' acc [] = acc
myReverse' acc (x :: xs) = let acc' = x :: acc in myReverse' acc' xs

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

myMap : (a -> b) -> List a -> List b
myMap f [] = []
myMap f (x :: xs) = f x :: myMap f xs

myMapVect : (a -> b) -> Vect n a -> Vect n b
myMapVect f [] = []
myMapVect f (x :: xs) = f x :: myMapVect f xs


text:
module Inputs
import Data.Primitives.Views

public export
randoms : Int -> Stream Int
randoms seed = let seed' = 1664525 * seed + 1013904223 in
                   (seed' `shiftR` 2) :: randoms seed'

public export
arithInputs : Int -> Stream Int
arithInputs seed = map bound (randoms seed)
  where
    bound : Int -> Int
    bound num with (divides num 12)
      bound ((12 * div) + rem) | (DivBy prf) = rem + 1

max_stars_repo_name: tekerson/type-driven-development

max_issues_repo_name: tekerson/type-driven-development

max_forks_repo_name: tekerson/type-driven-development


text:
{-
0
1
0
-}
module Main

testInt : String -> IO ()
testInt s = do
  let x : Int = cast s
  putStrLn $ cast x

testInteger : String -> IO ()
testInteger s = do
  let x : Integer = cast s
  putStrLn $ cast x

main : IO ()
main = do
  traverse_ testInt ["0", "1", "abc"]
  --traverse_ testInteger ["0", "1", "abc"]

max_stars_repo_name: timjs/iris-clean

max_issues_repo_name: timjs/iris-clean

max_forks_repo_name: timjs/iris-clean