text:
module tipos

import Data.SortedMap

%access public export

data Id = ValID String

data AExp = Sum AExp AExp | Sub AExp AExp | Div AExp AExp | Mul AExp AExp | N Int | ID Id

data BExp = Equal AExp AExp | Not BExp | LT AExp AExp | GT AExp AExp | LE AExp AExp | GE AExp AExp | And BExp BExp | OR BExp BExp | Boo Bool

data Exp = AExpR AExp | BExpR BExp | Ref Exp | DeRef Id | ValRef Id

data Dec = Bind Id Exp | DSeq Dec Dec

data Cmd = Assign Id Exp | Loop BExp Cmd | Cond BExp Cmd Cmd | CSeq Cmd Cmd | Blk Dec Cmd | NOP

data CmdOp = CtrlAssign | CtrlLoop | CtrlCond | CtrlCSeq | CtrlBlkDec | CtrlBlkCmd

data ExpOp = CtrlSum | CtrlSub | CtrlDiv | CtrlMul | CtrlNot | CtrlLT | CtrlGT | CtrlLE | CtrlGE | CtrlAnd | CtrlOR | CtrlEqual | CtrlRef | CtrlCns

data DecOp = CtrlBind | CtrlDSeq

data Ctrl = CtExp Exp | CtExpOp ExpOp | CtCmd Cmd | CtDec Dec | CtCmdOp CmdOp | CtDecOp DecOp

data Loc = L Int

data Val = ValInt Int | ValBool Bool | ValId String | ValCmd Cmd | ValLoc Loc | ValListLoc (List Loc) | ValEnv (SortedMap Val Loc) |ValNop

--
-- implementation Equal Loc where
--   (L a) == (L b) = a == b
--   (L a) /= (L b) = a /= b
--
-- implementation Ord Loc where
--   compare (L a) (L b) = compare a b
--
--
-- implementation Equal Val where
--     (ValId a) == (ValId b) = a == b
--
-- implementation Ord Val where
--     compare (ValId a) (ValId b) = compare a b

implementation Show Id where
  show (ValID x) = "ValID " ++ show x

implementation Show AExp where
  show (Sum a b) = "Sum (" ++ show a ++ ") " ++ "(" ++ show b ++ ")"
  show (Sub a b) = "Sub (" ++ show a ++ ") " ++ "(" ++ show b ++ ")"
  show (Mul a b) = "Mul (" ++ show a ++ ") " ++ "(" ++ show b ++ ")"
  show (Div a b) = "Div (" ++ show a ++ ") " ++ "(" ++ show b ++ ")"
  show (N a) = "N " ++ show a
  show (ID a) = "ID " ++ show a

implementation Show BExp where
  show (Equal a b) = "Equal (" ++ show a ++ ") " ++ "(" ++ show b ++ ")"
  show (GT a b) = "GT (" ++ show a ++ ") " ++ "(" ++ show b ++ ")"
  show (LT a b) = "LT (" ++ show a ++ ") " ++ "(" ++ show b ++ ")"
  show (LE a b) = "LE (" ++ show a ++ ") " ++ "(" ++ show b ++ ")"
  show (GE a b) = "GE (" ++ show a ++ ") " ++ "(" ++ show b ++ ")"
  show (And a b) = "And (" ++ show a ++ ") " ++ "(" ++ show b ++ ")"
  show (OR a b) = "OR (" ++ show a ++ ") " ++ "(" ++ show b ++ ")"
  show (Boo a) = "Boo " ++ show a
  show (Not a) = "Not " ++ show a

implementation Show Exp where
  show (AExpR a) = "AExpR (" ++ show a ++ ")"
  show (BExpR a) = "BExpR " ++ show a
  show (Ref a) = "Ref " ++ show a
  show (DeRef id) = "DeRef " ++ show id
  show (ValRef id) = "ValRef " ++ show id

implementation Show Dec where
  show (Bind a b) = "Bind " ++ show a ++ " " ++ show b
  show (DSeq a b) = "DSeq " ++ show a ++ " " ++ show b

implementation Show Cmd where
  show (Assign id exp) = "Assign " ++ show id ++ " " ++ show exp
  show (Loop b c) = "Loop " ++ show b ++ " " ++ show c
  show (Cond b c1 c2) = "Cond " ++ show b ++ " " ++ show c1 ++ " " ++ show c2
  show (CSeq c1 c2) = "CSeq " ++ show c1 ++ " " ++ show c2
  show (Blk d c) = "Blk " ++ show d ++ " " ++ show c
  show (NOP) = "NOP"

implementation Show CmdOp where
  show CtrlAssign = "CtrlAssign"
  show CtrlLoop = "CtrlLoop"
  show CtrlCond = "CtrlCond"
  show CtrlCSeq = "CtrlCSeq"
  show CtrlBlkDec = "CtrlBlkDec"
  show CtrlBlkCmd = "CtrlBlkCmd"

implementation Show ExpOp where
  show CtrlSum = "CtrlSum"
  show CtrlSub = "CtrlSub"
  show CtrlDiv = "CtrlDiv"
  show CtrlMul = "CtrlMul"
  show CtrlNot = "CtrlNot"
  show CtrlLT = "CtrlLT"
  show CtrlGT = "CtrlGT"
  show CtrlLE = "CtrlLE"
  show CtrlGE = "CtrlGE"
  show CtrlAnd = "CtrlAnd"
  show CtrlOR = "CtrlOR"
  show CtrlEqual = "CtrlEqual"
  show CtrlRef = "CtrlRef"
  show CtrlCns = "CtrlCns"

implementation Show DecOp where
  show CtrlBind = "CtrlBind"
  show CtrlDSeq = "CtrlDSeq"

implementation Show Ctrl where
  show (CtExp a) = "CtExp (" ++ show a ++ ")"
  show (CtExpOp a) = "CtExpOp " ++ show a
  show (CtCmd a) = "CtCmd " ++ show a
  show (CtDec a) = "CtDec " ++ show a
  show (CtCmdOp a) = "CtCmdOp " ++ show a
  show (CtDecOp a) = "CtDecOp " ++ show a

implementation Show Loc where
  show (L a) = "L " ++ show a

implementation Show Val where
  show (ValInt a) = "ValInt " ++ show a
  show (ValBool b) = "ValBool " ++ show b
  show (ValId a) = "ValId " ++ show a
  show (ValCmd a) = "ValCmd " ++ show a
  show (ValLoc a) = "ValLoc " ++ show a
  show (ValListLoc a) = "ValListLoc " ++ show a
  show (ValEnv map) = "ValEnv" ++ show (toList map)
  show ValNop = "ValNop"

max_stars_repo_name: RonaldCamp/ImpCompiler

max_issues_repo_name: RonaldCamp/ImpCompiler

max_forks_repo_name: RonaldCamp/ImpCompiler


text:
import Process

import Data.Vect

data Counter : Type -> Type where
     GetIdle : Counter Int
     Append : Vect n a -> Vect m a -> Counter $ Vect (n + m) a

data Maths : Type -> Type where
     Factorial : Nat -> Maths Nat

count_process : Int -> Counter t -> Response (t, Int) Counter [] p
count_process x GetIdle = Pure (x, x)
count_process x (Append xs ys) = Pure (xs ++ ys, x)

countServer : Int -> Running () Counter
countServer secs = do s' <- TimeoutRespond 1 (secs + 1) (count_process secs)
                      Loop (countServer s')

mathsServer : Running () Maths
mathsServer = do Lift $ putStrLn "Serving maths!"
                 TimeoutRespond 5 () (\val => case val of
                                                   Factorial k =>
                                                        Pure (fact k, ()))
                 Loop mathsServer

-- Start up a couple of servers, send them requests
testProg1 : Program () (const Void)
testProg1 = do -- with Process do
               mpid <- Fork mathsServer
               cpid <- Fork (countServer 0)
               putStr "Number1: "
               x1 <- getLine
               putStr "Number2: "
               x2 <- getLine

               fac1h <- Request mpid (Factorial (cast (trim x1)))
               fac2h <- Request mpid (Factorial (cast (trim x2)))

               fac2 <- GetReply fac2h -- {pending = PendingHere}
               fac1 <- GetReply fac1h -- {pending = PendingHere}

               Disconnect cpid
               Disconnect mpid

main : IO ()
main = run testProg1

ext: idr

max_stars_repo_name: grin-compiler/idris-grin

max_issues_repo_name: grin-compiler/idris-grin

max_forks_repo_name: grin-compiler/idris-grin


text:
module Main

import Control.Monad.State
import Data.List
import Data.Nat
import Data.Nat.Views
import Data.Strings
import Data.Vect
import System.File

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

data Bit = Zero
         | One

Eq Bit where
  Zero == Zero = True
  One == One = True
  _ == _ = False

Ord Bit where
  compare Zero Zero = EQ
  compare Zero One = LT
  compare One Zero = GT
  compare One One = EQ

Show Bit where
  show Zero = "Zero"
  show One = "One"

Bits : Type
Bits = Vect 36 Bit

record Mask where
  constructor MkMask
  bits : Vect 36 (Maybe Bit)

Show Mask where
  show (MkMask bits) = "Mask " ++ show bits

record Mem where
  constructor MkMem
  address : Nat
  value : Bits

Show Mem where
  show (MkMem address value) = "Mem " ++ show address ++ " " ++ show value

Line : Type
Line = Either Mask Mem

Program : Type
Program = List Line

Memory : Type
Memory = SortedMap Nat Bits

applyMask : Mask -> Bits -> Bits
applyMask (MkMask maskBits) valBits = f <$> maskBits <*> valBits where
  f : Maybe Bit -> Bit -> Bit
  f Nothing x = x
  f (Just x) _ = x

initState : (Mask, Memory)
initState = (MkMask $ pure Nothing, empty)

progLine : Line -> State (Mask,Memory) ()
progLine (Left mask) = do
  (oldMask, memory) <- get
  put (mask, memory)
progLine (Right (MkMem address value)) = do
  (mask, oldMemory) <- get
  let memory = insert address (applyMask mask value) oldMemory
  put (mask, memory)

bitsToNat : Bits -> Nat
bitsToNat = bitsToNat' . reverse where
  bitsToNat' : Vect n Bit -> Nat
  bitsToNat' [] = 0
  bitsToNat' (One :: xs) = 1 + 2 * bitsToNat' xs
  bitsToNat' (Zero :: xs) = 0 + 2 * bitsToNat' xs

integerToBits : {n : Nat} -> Integer -> Vect n Bit
integerToBits x with (n)
  integerToBits x | Z = []
  integerToBits x | (S k) = if x `mod` 2 == 0
                           then Zero :: integerToBits (x `div` 2)
                           else One :: integerToBits (x `div` 2)

natToBits : Nat -> Bits
natToBits n = integerToBits $ natToInteger n

Memory' : Type
Memory' = SortedMap Bits Bits

initState' : (Mask, Memory')
initState' = (MkMask $ pure Nothing, empty)

applyMaskToAddress' : Vect n (Maybe Bit) -> Vect n Bit -> Vect n (Maybe Bit)
applyMaskToAddress' [] [] = []
applyMaskToAddress' (Just Zero :: ms) (a :: as) = Just a :: applyMaskToAddress' ms as
applyMaskToAddress' (Just One :: ms) (_ :: as) = Just One :: applyMaskToAddress' ms as
applyMaskToAddress' (Nothing :: ms) (_ :: as) = Nothing :: applyMaskToAddress' ms as

floatingAddresses : Vect n (Maybe Bit) -> List (Vect n Bit)
floatingAddresses [] = pure []
floatingAddresses (Nothing :: xs) = (::) <$> [ Zero, One ] <*> floatingAddresses xs
floatingAddresses (Just x :: xs) = (x ::) <$> floatingAddresses xs

applyMaskToAddress : Mask -> Bits -> List Bits
applyMaskToAddress (MkMask mask) bs = floatingAddresses $ applyMaskToAddress' mask bs

inserter : Bits -> (key : Bits) -> State (Mask,Memory') ()
inserter value k = do
  (mask, memory) <- get
  let newMemory = insert k value memory
  put (mask, newMemory)

progLine' : Line -> State (Mask,Memory') ()
progLine' (Left mask) = do
  (oldMask, memory) <- get
  put (mask, memory)
progLine' (Right (MkMem address value)) = do
  (mask, memory) <- get
  let addresses = applyMaskToAddress mask $ natToBits address
  traverse_ (inserter value) addresses
  pure ()

namespace Parsing
  data DataKind = DKMask
                | DKMem
                | DKBracketOpen
                | DKBracketClose
                | DKSpace
                | DKEquals
                | DKNewline
                | DKNoBit
                | DKDigit

  Eq DataKind where
    (==) DKMask DKMask = True
    (==) DKMem DKMem = True
    (==) DKBracketOpen DKBracketOpen = True
    (==) DKBracketClose DKBracketClose = True
    (==) DKSpace DKSpace = True
    (==) DKEquals DKEquals = True
    (==) DKNewline DKNewline = True
    (==) DKNoBit DKNoBit = True
    (==) DKDigit DKDigit = True
    (==) _ _ = False

  export
  Show DataKind where
    show DKMask = "DKMask"
    show DKMem = "DKMem"
    show DKBracketOpen = "DKBracketOpen"
    show DKBracketClose = "DKBracketClose"
    show DKSpace = "DKSpace"
    show DKEquals = "DKEquals"
    show DKNewline = "DKNewline"
    show DKNoBit = "DKNoBit"
    show DKDigit = "DKDigit"

  data Digit = D0
             | D1
             | D2
             | D3
             | D4
             | D5
             | D6
             | D7
             | D8
             | D9

  Cast String Digit where
    cast "0" = D0
    cast "1" = D1
    cast "2" = D2
    cast "3" = D3
    cast "4" = D4
    cast "5" = D5
    cast "6" = D6
    cast "7" = D7
    cast "8" = D8
    cast "9" = D9
    cast _ = ?cantCastNonDigit

  TokenKind DataKind where
    TokType DKMask = ()
    TokType DKMem = ()
    TokType DKBracketOpen = ()
    TokType DKBracketClose = ()
    TokType DKSpace = ()
    TokType DKEquals = ()
    TokType DKNewline = ()
    TokType DKNoBit = ()
    TokType DKDigit = Digit
    tokValue DKMask _ = ()
    tokValue DKMem _ = ()
    tokValue DKBracketOpen _ = ()
    tokValue DKBracketClose _ = ()
    tokValue DKSpace _ = ()
    tokValue DKEquals _ = ()
    tokValue DKNewline _ = ()
    tokValue DKNoBit _ = ()
    tokValue DKDigit str = cast str

  export
  tokenMap : TokenMap $ Token DataKind
  tokenMap = toTokenMap
    [ (exact "mask", DKMask)
    , (exact "mem", DKMem)
    , (is '[', DKBracketOpen)
    , (is ']', DKBracketClose)
    , (newline, DKNewline)
    , (space, DKSpace)
    , (is '=', DKEquals)
    , (is 'X', DKNoBit)
    , (digit, DKDigit)
    ]

  digitsToNat : List Digit -> Nat
  digitsToNat [] = 0
  digitsToNat (x :: xs) = digitToNat x + 10 * digitsToNat xs where
    digitToNat : Digit -> Nat
    digitToNat D0 = 0
    digitToNat D1 = 1
    digitToNat D2 = 2
    digitToNat D3 = 3
    digitToNat D4 = 4
    digitToNat D5 = 5
    digitToNat D6 = 6
    digitToNat D7 = 7
    digitToNat D8 = 8
    digitToNat D9 = 9

  grammarMem : Grammar (Token DataKind) True Mem
  grammarMem = do
    match DKMem
    match DKBracketOpen
    digitsAddress <- some $ match DKDigit
    let address = digitsToNat $ reverse digitsAddress
    match DKBracketClose
    match DKSpace
    match DKEquals
    match DKSpace
    MkMem address <$> grammarVal where
      grammarVal : Grammar (Token DataKind) True Bits
      grammarVal = (reverse . natToBits . digitsToNat . reverse) <$> (some $ match DKDigit)

  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 |]

  grammarMbBit : Grammar (Token DataKind) True (Maybe Bit)
  grammarMbBit = Just <$> grammarDig <|> grammarX where
    grammarDig : Grammar (Token DataKind) True Bit
    grammarDig = do
      n <- match DKDigit
      f n where
        f : Digit -> Grammar (Token DataKind) False Bit
        f D0 = pure Zero
        f D1 = pure One
        f _ = fail "Can't parser bit other than 0 or 1"
    grammarX : Grammar (Token DataKind) True (Maybe Bit)
    grammarX = match DKNoBit *> pure Nothing

  grammarMask : Grammar (Token DataKind) True Mask
  grammarMask = do
    match DKMask
    match DKSpace
    match DKEquals
    match DKSpace
    bits <- countExactly 36 $ grammarMbBit
    pure $ MkMask bits

  grammarLine : Grammar (Token DataKind) True Line
  grammarLine = (Left <$> grammarMask <|> Right <$> grammarMem) <* match DKNewline

  export
  grammarData : Grammar (Token DataKind) True Program
  grammarData = some grammarLine <* eof

main : IO ()
main = do
  inputData <- readFile "./data"
  case inputData of
       Left err => print err
       Right actualData => do
         let (lexed, debugLexed) = lex tokenMap actualData
             parsed = parse grammarData $ tok <$> lexed
         case parsed of
              Left (Error err restToks) => do
                print $ text <$> restToks
                print err
              Right (prog, rest) => do
                --let (endMask, endMemory) = execState initState (traverse_ progLine prog)
                let (endMask, endMemory) = execState initState' (traverse_ progLine' prog)
                print $ sum $ bitsToNat <$> endMemory
         pure ()
  pure ()


text:
module TTImp.Elab.Local

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

import TTImp.Elab.Check
import TTImp.Elab.Utils
import TTImp.TTImp

import Libraries.Data.NameMap
import Data.List

%default covering

export
localHelper : {vars : _} ->
             {auto c : Ref Ctxt Defs} ->
             {auto m : Ref MD Metadata} ->
             {auto u : Ref UST UState} ->
             {auto e : Ref EST (EState vars)} ->
             NestedNames vars -> Env Term vars ->
             List ImpDecl -> (NestedNames vars -> Core a) ->
             Core a
localHelper {vars} nest env nestdecls_in func
    = do est <- get EST
         let f = defining est
         defs <- get Ctxt
         gdef <- lookupCtxtExact (Resolved (defining est)) (gamma defs)
         let vis  = maybe Public visibility gdef
         let mult = maybe linear GlobalDef.multiplicity gdef

         -- If the parent function is public, the nested definitions need
         -- to be public too
         let nestdeclsVis =
               if vis == Public
                  then map setPublic nestdecls_in
                  else nestdecls_in

         -- If the parent function is erased, then the nested definitions
         -- will be erased too
         let nestdeclsMult =
           if mult == erased
              then map setErased nestdeclsVis
              else nestdeclsVis

         let defNames = definedInBlock emptyNS nestdeclsMult
         names' <- traverse (applyEnv f)
                            (nub defNames) -- binding names must be unique
                                           -- fixes bug #115
         let nest' = record { names $= (names' ++) } nest
         let env' = dropLinear env
         -- We don't want to keep rechecking delayed elaborators in the
         -- locals  block, because they're not going to make progress until
         -- we come out again, so save them
         ust <- get UST
         let olddelayed = delayedElab ust
         put UST (record { delayedElab = [] } ust)
         defs <- get Ctxt
         -- store the local hints, so we can reset them after we've elaborated
         -- everything
         let oldhints = localHints defs

         let nestdecls = map (updateName nest') nestdeclsMult
         log "elab.def.local" 20 $ show nestdecls

         traverse_ (processDecl [] nest' env') nestdecls
         ust <- get UST
         put UST (record { delayedElab = olddelayed } ust)
         defs <- get Ctxt
         res <- func nest'
         defs <- get Ctxt
         put Ctxt (record { localHints = oldhints } defs)
         pure res
  where
    -- For the local definitions, don't allow access to linear things
    -- unless they're explicitly passed.
    -- This is because, at the moment, we don't have any mechanism of
    -- ensuring the nested definition is used exactly once
    dropLinear : Env Term vs -> Env Term vs
    dropLinear [] = []
    dropLinear (b :: bs)
        = if isLinear (multiplicity b)
             then setMultiplicity b erased :: dropLinear bs
             else b :: dropLinear bs

    applyEnv : Int -> Name ->
               Core (Name, (Maybe Name, List (Var vars), FC -> NameType -> Term vars))
    applyEnv outer inner
          = do ust <- get UST
               put UST (record { nextName $= (+1) } ust)
               let nestedName_in = Nested (outer, nextName ust) inner
               nestedName <- inCurrentNS nestedName_in
               n' <- addName nestedName
               pure (inner, (Just nestedName, reverse (allVars env),
                        \fc, nt => applyToFull fc
                               (Ref fc nt (Resolved n')) env))

    -- Update the names in the declarations to the new 'nested' names.
    -- When we encounter the names in elaboration, we'll update to an
    -- application of the nested name.
    newName : NestedNames vars -> Name -> Name
    newName nest n
        = case lookup n (names nest) of
               Just (Just n', _) => n'
               _ => n

    updateTyName : NestedNames vars -> ImpTy -> ImpTy
    updateTyName nest (MkImpTy loc' nameLoc n ty)
        = MkImpTy loc' nameLoc (newName nest n) ty

    updateDataName : NestedNames vars -> ImpData -> ImpData
    updateDataName nest (MkImpData loc' n tycons dopts dcons)
        = MkImpData loc' (newName nest n) tycons dopts
                         (map (updateTyName nest) dcons)
    updateDataName nest (MkImpLater loc' n tycons)
        = MkImpLater loc' (newName nest n) tycons

    updateName : NestedNames vars -> ImpDecl -> ImpDecl
    updateName nest (IClaim loc' r vis fnopts ty)
         = IClaim loc' r vis fnopts (updateTyName nest ty)
    updateName nest (IDef loc' n cs)
         = IDef loc' (newName nest n) cs
    updateName nest (IData loc' vis d)
         = IData loc' vis (updateDataName nest d)
    updateName nest i = i

    setPublic : ImpDecl -> ImpDecl
    setPublic (IClaim fc c _ opts ty) = IClaim fc c Public opts ty
    setPublic (IData fc _ d) = IData fc Public d
    setPublic (IRecord fc c _ r) = IRecord fc c Public r
    setPublic (IParameters fc ps decls)
        = IParameters fc ps (map setPublic decls)
    setPublic (INamespace fc ps decls)
        = INamespace fc ps (map setPublic decls)
    setPublic d = d

    setErased : ImpDecl -> ImpDecl
    setErased (IClaim fc _ v opts ty) = IClaim fc erased v opts ty
    setErased (IParameters fc ps decls)
        = IParameters fc ps (map setErased decls)
    setErased (INamespace fc ps decls)
        = INamespace fc ps (map setErased decls)
    setErased d = d

export
checkLocal : {vars : _} ->
             {auto c : Ref Ctxt Defs} ->
             {auto m : Ref MD Metadata} ->
             {auto u : Ref UST UState} ->
             {auto e : Ref EST (EState vars)} ->
             RigCount -> ElabInfo ->
             NestedNames vars -> Env Term vars ->
             FC -> List ImpDecl -> (scope : RawImp) ->
             (expTy : Maybe (Glued vars)) ->
             Core (Term vars, Glued vars)
checkLocal {vars} rig elabinfo nest env fc nestdecls_in scope expty
    = localHelper nest env nestdecls_in $ \nest' => check rig elabinfo nest' env scope expty

getLocalTerm : {vars : _} ->
               {auto c : Ref Ctxt Defs} ->
               FC -> Env Term vars -> Term vars -> List Name ->
               Core (Term vars, List (Var vars))
getLocalTerm fc env f [] = pure (f, [])
getLocalTerm fc env f (a :: as)
    = case defined a env of
           Just (MkIsDefined rigb lv) =>
                do (tm, vs) <- getLocalTerm fc env
                                   (App fc f (Local fc Nothing _ lv)) as
                   pure (tm, MkVar lv :: vs)
           Nothing => throw (InternalError "Case Local failed")

export
checkCaseLocal : {vars : _} ->
                 {auto c : Ref Ctxt Defs} ->
                 {auto m : Ref MD Metadata} ->
                 {auto u : Ref UST UState} ->
                 {auto e : Ref EST (EState vars)} ->
                 RigCount -> ElabInfo ->
                 NestedNames vars -> Env Term vars ->
                 FC -> Name -> Name -> List Name -> RawImp ->
                 (expTy : Maybe (Glued vars)) ->
                 Core (Term vars, Glued vars)
checkCaseLocal {vars} rig elabinfo nest env fc uname iname args sc expty
    = do defs <- get Ctxt
         Just def <- lookupCtxtExact iname (gamma defs)
              | Nothing => check rig elabinfo nest env sc expty
         let nt = fromMaybe Func (defNameType $ definition def)
         let name = Ref fc nt iname
         (app, args) <- getLocalTerm fc env name args
         log "elab.local" 5 $ "Updating case local " ++ show uname ++ " " ++ show args
         logTermNF "elab.local" 5 "To" env app
         let nest' = record { names $= ((uname, (Just iname, args,
                                                (\fc, nt => app))) :: ) }
                            nest
         check rig elabinfo nest' env sc expty


text:
module A

public export
defA : Int -> Int


text:
||| Magic/Virtual files
module System.File.Virtual

import System.File.Support
import public System.File.Types

%default total

%foreign support "idris2_stdin"
         "node:lambda:x=>({fd:0, buffer: Buffer.alloc(0), name:'<stdin>', eof: false})"
prim__stdin : FilePtr

%foreign support "idris2_stdout"
         "node:lambda:x=>({fd:1, buffer: Buffer.alloc(0), name:'<stdout>', eof: false})"
prim__stdout : FilePtr

%foreign support "idris2_stderr"
         "node:lambda:x=>({fd:2, buffer: Buffer.alloc(0), name:'<stderr>', eof: false})"
prim__stderr : FilePtr

||| The standard input.
export
stdin : File
stdin = FHandle prim__stdin

||| The standard output.
export
stdout : File
stdout = FHandle prim__stdout

||| The standard error.
export
stderr : File
stderr = FHandle prim__stderr


text:
module DecOrderNat

%access public export
%default total

||| The type of proof that between two elements one is less than
||| equal to another

data DecMin : (m , n : Nat) -> Type where
    Left : (LTE m n) -> DecMin m n
    Right : (LTE n m) -> DecMin m n

||| Decides which of the two numbers is smaller and gives the
||| proof along with the decision

decideSucc : (m , n : Nat) -> (DecMin m n) -> (DecMin (S m) (S n))
decideSucc m n (Left pf) = Left (LTESucc pf)
decideSucc m n (Right pf) = Right (LTESucc pf)

decMin : (m , n : Nat) -> (DecMin m n)
decMin Z n = Left LTEZero
decMin n Z = Right LTEZero
decMin (S m) (S n) = decideSucc m n (decMin m n)


text:
module WebAssembly.Validation.Modules

import public WebAssembly.Validation.Modules.Functions
import public WebAssembly.Validation.Modules.Tables
import public WebAssembly.Validation.Modules.Memories
import public WebAssembly.Validation.Modules.Globals
import public WebAssembly.Validation.Modules.ElementSegments
import public WebAssembly.Validation.Modules.DataSegments
import public WebAssembly.Validation.Modules.Imports
import public WebAssembly.Validation.Modules.Exports

max_stars_repo_name: RaoulSchaffranek/idris-webassembly

max_issues_repo_name: RaoulSchaffranek/idris-webassembly

max_forks_repo_name: RaoulSchaffranek/idris-webassembly


text:
import Data.Vect

export
data StackCmd : Type -> Nat -> Nat -> Type where
  Push : Integer -> StackCmd ()      height     (S height)
  Pop :             StackCmd Integer (S height) height
  Top :             StackCmd Integer (S height) (S height)

  GetStr : StackCmd String height height
  PutStr : String -> StackCmd () height height

  Pure : ty -> StackCmd ty height height
  (>>=) : StackCmd a height1 height2 ->
          (a -> StackCmd b height2 height3) ->
          StackCmd b height1 height3

runStack : (stk : Vect inHeight Integer) ->
           StackCmd ty inHeight outHeight ->
           IO (ty, Vect outHeight Integer)
runStack stk (Push val) = pure ((), val :: stk)
runStack (val :: stk) Pop = pure (val, stk)
runStack (val :: stk) Top = pure (val, val :: stk)
runStack stk GetStr = do x <- getLine
                         pure (x, stk)
runStack stk (PutStr x) = do putStr x
                             pure ((), stk)
runStack stk (Pure x) = pure (x, stk)
runStack stk (x >>= f) = do (x', newStk) <- runStack stk x
                            runStack newStk (f x')

testAdd : StackCmd () 0 0
testAdd = do Push 10
             x <- GetStr
             Push (cast x)
             val1 <- Pop
             val2 <- Pop
             PutStr (show (val1 + val2) ++ "\n")

export
data StackIO : Nat -> Type where
  Do : StackCmd a height1 height2 ->
       (a -> Inf (StackIO height2)) -> StackIO height1

namespace StackDo
  export
  (>>=) : StackCmd a height1 height2 ->
          (a -> Inf (StackIO height2)) -> StackIO height1
  (>>=) = Do

data Fuel = Dry | More (Lazy Fuel)

partial
forever : Fuel
forever = More forever

run : Fuel -> Vect height Integer -> StackIO height -> IO ()
run Dry _ _ = pure ()
run (More fuel) stk (Do c f) = do (res, newStk) <- runStack stk c
                                  run fuel newStk (f res)

doAdd : StackCmd () (S (S height)) (S height)
doAdd = do val1 <- Pop
           val2 <- Pop
           Push (val1 + val2)

data StkInput = Number Integer
              | Add

strToInput : String -> Maybe StkInput
strToInput "" = Nothing
strToInput "add" = Just Add
strToInput x = if all isDigit (unpack x)
                  then Just (Number $ cast x)
                  else Nothing

mutual
  tryAdd : {height : _} -> StackIO height
  tryAdd {height = S (S h)} = do doAdd
                                 result <- Top
                                 PutStr (show result ++ "\n")
                                 stackCalc
  tryAdd = do PutStr "Fewer than two items on the stack\n"
              stackCalc

  stackCalc : {height : _} -> StackIO height
  stackCalc = do PutStr "> "
                 input <- GetStr
                 case strToInput input of
                      Nothing => do PutStr "Invalid input\n"
                                    stackCalc
                      Just (Number x) => do Push x
                                            stackCalc
                      Just Add => tryAdd

main : IO ()
main = run forever [] stackCalc


text:
module Client.Action.Pull

import Client.Server
import Data.Buffer
import Extra.Buffer
import Fmt
import Inigo.Archive.Path
import Inigo.Async.Archive
import Inigo.Async.Base
import Inigo.Async.Fetch
import Inigo.Async.FS
import Inigo.Async.Promise
import Inigo.Package.Package
import Inigo.Util.Url.Url
import System.Path
import SemVar

getPath : String -> String -> (Maybe Version) -> String
getPath ns package Nothing = getPackageUrl ns package
getPath ns package (Just version) = getPackageVersionUrl ns package version

getPackage : Server -> String -> String -> (Maybe Version) -> Promise Package
getPackage server packageNS packageName maybeVersion =
  do
    let path = getPath packageNS packageName maybeVersion
    let url = toString (fromHostPath (host server) path)
    log ("Requesting " ++ url ++ "...")
    contents <- fetch url
    let Right package = parsePackage contents
      | Left err => reject ("Invalid package: " ++ err)
    pure package

getArchive : Server -> Package -> Promise Buffer
getArchive server pkg =
  do
    let url = toString (fromHostPath (host server) (getArchiveUrl pkg))
    log ("Requesting " ++ url ++ "...")
    contents <- fetchBuf url
    pure contents

export
pull : Server -> String -> String -> (Maybe Version) -> Promise ()
pull server packageNS packageName maybeVersion =
  do
    pkg <- getPackage server packageNS packageName maybeVersion
    archive <- getArchive server pkg
    let depPath = Archive.Path.depPath pkg
    extractArchive archive depPath
    let iPkgFile = depPath </> "Inigo.ipkg"
    log (fmt "Writing %s..." iPkgFile)
    fs_writeFile iPkgFile (Package.Package.generateIPkg False (Just "../../../../build") pkg)

max_stars_repo_name: Z-snails/inigo

max_issues_repo_name: Z-snails/inigo

max_forks_repo_name: Z-snails/inigo


text:
module Main

import Test.Golden

prefixFolder : String -> List String -> List String
prefixFolder pref paths =
  map ((pref ++ "/") ++) paths

lexerTests : TestPool
lexerTests = MkTestPool "Lexer Tests" [] Nothing $ prefixFolder "lexer"
  ["call", "all", "readme"]

main : IO ()
main = runner $ [ lexerTests ]

max_stars_repo_name: felipegchi/Yurei

max_issues_repo_name: felipegchi/Yurei

max_forks_repo_name: felipegchi/Yurei


text:
module Cordial.Model.Interface.PortGroup.Views

import Data.Vect
import Data.DList
import Data.Ranged

import Text.Markup.Edda

import Cordial.Model.Common
import Cordial.Model.Specification
import Cordial.Model.Projection

import Cordial.Model.Interface.Kinds
import Cordial.Model.Interface.Ports
import Cordial.Model.Interface.PortGroup

%default total
%access public export

{-

data PortGroup : (annot    : Type)
              -> (labelTy    : Type)
              -> (endpoint : Endpoint)
              -> (endian   : Maybe Endian)
              -> (ps       : PortGroupTy annot labelTy)
              -> (pportTys : DList (PortTy annot labelTy) (ProjectedPortTy labelTy endpoint) ps)
              -> Type
  where

-}
namespace System
  data SystemPortGroup : (portGroup : PortGroup annot labelTy endpoint endian types projectedTypes)
                      -> Type
    where
      Empty : SystemPortGroup Empty
      Add : (port : Port annot labelTy type projectedType endpoint endian)
         -> (prf  : SystemPort port)
         -> (rest : SystemPortGroup ports)
         -> SystemPortGroup (Add port ports)

      NotSystemPort : (prf : SystemPort port -> Void)
                   -> (rest : SystemPortGroup ports)
                   -> SystemPortGroup (Add port ports)
      Skip : (rest : SystemPortGroup ports)
          -> SystemPortGroup (Skip ports prf)

  toSystemPortGroup : (portGroup : PortGroup annot labelTy endpoint endian types projectedTypes)
                   -> SystemPortGroup portGroup
  toSystemPortGroup Empty = Empty
  toSystemPortGroup (Add port rest {projectedType} {type}) with (isProjectedPortSystem projectedType)
    toSystemPortGroup (Add port rest {projectedType = projectedType} {type = type}) | (Yes prf) = Add port (PortIsSystem prf) (toSystemPortGroup rest)
    toSystemPortGroup (Add port rest {projectedType = projectedType} {type = type}) | (No contra) = NotSystemPort (contra) (toSystemPortGroup rest)

  toSystemPortGroup (Skip rest prf) = Skip (toSystemPortGroup rest)

max_stars_repo_name: border-patrol/cordial

max_issues_repo_name: border-patrol/cordial

max_forks_repo_name: border-patrol/cordial


text:
||| Low-Level C Sockets bindings for Idris. Used by higher-level, cleverer things.
||| Types used by Network.Socket.Raw and Network.Socket.
|||
||| Original (C) SimonJF, MIT Licensed, 2014
||| Modified (C) The Idris Community, 2015, 2016, 2019
module Network.Socket.Data

import Data.List
import Data.List1
import Data.String
import System.FFI

-- ------------------------------------------------------------ [ Type Aliases ]

public export
ByteLength : Type
ByteLength = Int

public export
ResultCode : Type
ResultCode = Int

||| Protocol Number.
|||
||| Generally good enough to just set it to 0.
public export
ProtocolNumber : Type
ProtocolNumber = Int

||| SocketError: Error thrown by a socket operation
public export
SocketError : Type
SocketError = Int

||| SocketDescriptor: Native C Socket Descriptor
public export
data SocketDescriptor : Type where [external]

public export
Port : Type
Port = Int

-- --------------------------------------------------------------- [ Constants ]

||| Backlog used within listen() call -- number of incoming calls
export
BACKLOG : Int
BACKLOG = 20

idrisSocketClass : String
idrisSocketClass = "io/github/mmhelloworld/idrisjvm/runtime/IdrisSocket"

-- Repeat to avoid a dependency cycle
%foreign "C:idrnet_geteagain, libidris2_support, idris_net.h"
         "jvm:getEagain(int),io/github/mmhelloworld/idrisjvm/runtime/IdrisSocket"
prim__idrnet_geteagain : PrimIO Int

export
EAGAIN : Int
EAGAIN =
  -- I'm sorry
  -- maybe
  unsafePerformIO $ primIO $ prim__idrnet_geteagain

-- ---------------------------------------------------------------- [ Error Code ]

-- repeat without export to avoid dependency cycles
%foreign "C:idrnet_errno, libidris2_support, idris_net.h"
         jvm' runtimeClass "getErrorNumber" "java/lang/Object" "int"
prim__idrnet_errno : PrimIO Int

%foreign "C:isNull, libidris2_support, idris_support.h"
         "jvm:isNull,io/github/mmhelloworld/idrisjvm/runtime/Objects"
prim__idrnet_isNull : (ptr : AnyPtr) -> PrimIO Int

export
getErrno : HasIO io => io SocketError
getErrno = primIO $ prim__idrnet_errno

export
nullPtr : HasIO io => AnyPtr -> io Bool
nullPtr p = do 0 <- primIO  $ prim__idrnet_isNull p
               | _ => pure True
               pure False

-- -------------------------------------------------------------- [ Interfaces ]

public export
interface ToCode a where
  toCode : a -> Int

-- --------------------------------------------------------- [ Socket Families ]

||| Socket Families
|||
||| The ones that people might actually use. We're not going to need US
||| Government proprietary ones.
public export
data SocketFamily : Type where
  ||| Unspecified
  AF_UNSPEC : SocketFamily

  ||| Unix type sockets
  AF_UNIX : SocketFamily

  ||| IP / UDP etc. IPv4
  AF_INET : SocketFamily

  |||  IP / UDP etc. IPv6
  AF_INET6 : SocketFamily

Show SocketFamily where
  show AF_UNSPEC = "AF_UNSPEC"
  show AF_UNIX   = "AF_UNIX"
  show AF_INET   = "AF_INET"
  show AF_INET6  = "AF_INET6"

-- This is a bit of a hack to get the OS-dependent magic constants out of C and
-- into Idris without having to faff around on the preprocessor on the Idris
-- side.
%foreign "C:idrnet_af_unspec, libidris2_support, idris_net.h"
         "jvm:getAfUnspec(int),io/github/mmhelloworld/idrisjvm/runtime/IdrisSocket"
prim__idrnet_af_unspec : PrimIO Int

%foreign "C:idrnet_af_unix, libidris2_support, idris_net.h"
         "jvm:getAfUnix(int),io/github/mmhelloworld/idrisjvm/runtime/IdrisSocket"
prim__idrnet_af_unix : PrimIO Int

%foreign "C:idrnet_af_inet, libidris2_support, idris_net.h"
         "jvm:getAfInet(int),io/github/mmhelloworld/idrisjvm/runtime/IdrisSocket"
prim__idrnet_af_inet : PrimIO Int

%foreign "C:idrnet_af_inet6, libidris2_support, idris_net.h"
         "jvm:getAfInet6(int),io/github/mmhelloworld/idrisjvm/runtime/IdrisSocket"
prim__idrnet_af_inet6 : PrimIO Int

export
ToCode SocketFamily where
  toCode AF_UNSPEC = unsafePerformIO $ primIO $ prim__idrnet_af_unspec
  toCode AF_UNIX   = unsafePerformIO $ primIO $ prim__idrnet_af_unix
  toCode AF_INET   = unsafePerformIO $ primIO $ prim__idrnet_af_inet
  toCode AF_INET6  = unsafePerformIO $ primIO $ prim__idrnet_af_inet6

export
getSocketFamily : Int -> Maybe SocketFamily
getSocketFamily i =
    lookup i [ (toCode AF_UNSPEC, AF_UNSPEC)
             , (toCode AF_UNIX, AF_UNIX)
             , (toCode AF_INET, AF_INET)
             , (toCode AF_INET6, AF_INET6)
             ]

-- ------------------------------------------------------------ [ Socket Types ]

||| Socket Types.
public export
data SocketType : Type where
  ||| Not a socket, used in certain operations
  NotASocket : SocketType

  ||| TCP
  Stream : SocketType

  ||| UDP
  Datagram : SocketType

  ||| Raw sockets
  RawSocket : SocketType

export
Show SocketType where
  show NotASocket = "Not a socket"
  show Stream     = "Stream"
  show Datagram   = "Datagram"
  show RawSocket  = "Raw"

export
ToCode SocketType where
  toCode NotASocket = 0
  toCode Stream     = 1
  toCode Datagram   = 2
  toCode RawSocket  = 3

-- --------------------------------------------------------------- [ Addresses ]

||| Network Addresses
public export
data SocketAddress : Type where
  IPv4Addr : Int -> Int -> Int -> Int -> SocketAddress

  ||| Not implemented (yet)
  IPv6Addr : SocketAddress

  Hostname : String -> SocketAddress

  ||| Used when there's a parse error
  InvalidAddress : SocketAddress

export
Show SocketAddress where
  show (IPv4Addr i1 i2 i3 i4) = concat $ intersperse "." (map show [i1, i2, i3, i4])
  show IPv6Addr               = "NOT IMPLEMENTED YET"
  show (Hostname host)        = host
  show InvalidAddress         = "Invalid"

||| Parses a textual representation of an IPv4 address into a SocketAddress
export
parseIPv4 : String -> SocketAddress
parseIPv4 str =
    case splitted of
      (i1 ::: i2 :: i3 :: i4 :: _) => IPv4Addr i1 i2 i3 i4
      _ => InvalidAddress
  where
    toInt' : String -> Integer
    toInt' = cast

    toInt : String -> Int
    toInt s = fromInteger $ toInt' s

    splitted : List1 Int
    splitted = map toInt (split (\c => c == '.') str)

-- --------------------------------------------------------- [ UDP Information ]

-- TODO: Expand to non-string payloads
public export
record UDPRecvData where
  constructor MkUDPRecvData
  remote_addr : SocketAddress
  remote_port : Port
  recv_data   : String
  data_len    : Int

public export
record UDPAddrInfo where
  constructor MkUDPAddrInfo
  remote_addr : SocketAddress
  remote_port : Port

-- ----------------------------------------------------------------- [ Sockets ]
||| The metadata about a socket
public export
record Socket where
  constructor MkSocket
  descriptor     : SocketDescriptor
  family         : SocketFamily
  socketType     : SocketType
  protocolNumber : ProtocolNumber


text:
module LLVM.Pretty

import Data.String.Builder


text:
module Idris.REPLOpts

import Compiler.Common
import Idris.Syntax
import Parser.Unlit
import TTImp.Interactive.ExprSearch
import TTImp.TTImp

import Data.List
import Data.Strings
import System.File

%default total

public export
data OutputMode
  = IDEMode Integer File File
  | REPL Bool -- quiet flag (ignore iputStrLn)

public export
record REPLOpts where
  constructor MkREPLOpts
  showTypes : Bool
  evalMode : REPLEval
  mainfile : Maybe String
  literateStyle : Maybe LiterateStyle
  source : String
  editor : String
  errorLine : Maybe Int
  idemode : OutputMode
  currentElabSource : String
  psResult : Maybe (Name, Core (Search RawImp)) -- last proof search continuation (and name)
  gdResult : Maybe (Int, Core (Search (FC, List ImpClause))) -- last generate def continuation (and line number)
  -- TODO: Move extraCodegens from here, it doesn't belong, but there's nowhere
  -- better to stick it now.
  extraCodegens : List (String, Codegen)
  consoleWidth : Maybe Nat -- Nothing is auto
  color : Bool

export
defaultOpts : Maybe String -> OutputMode -> List (String, Codegen) -> REPLOpts
defaultOpts fname outmode cgs
    = MkREPLOpts False NormaliseAll fname (litStyle fname) "" "vim"
                 Nothing outmode "" Nothing Nothing cgs Nothing True
  where
    litStyle : Maybe String -> Maybe LiterateStyle
    litStyle Nothing = Nothing
    litStyle (Just fn) = isLitFile fn

export
data ROpts : Type where

export
replFC : FC
replFC = MkFC "(interactive)" (0, 0) (0, 0)

export
setOutput : {auto o : Ref ROpts REPLOpts} ->
            OutputMode -> Core ()
setOutput m
    = do opts <- get ROpts
         put ROpts (record { idemode = m } opts)

export
getOutput : {auto o : Ref ROpts REPLOpts} -> Core OutputMode
getOutput = do opts <- get ROpts
               pure (idemode opts)

export
setMainFile : {auto o : Ref ROpts REPLOpts} ->
              Maybe String -> Core ()
setMainFile src
    = do opts <- get ROpts
         put ROpts (record { mainfile = src,
                             literateStyle = litStyle src } opts)
  where
    litStyle : Maybe String -> Maybe LiterateStyle
    litStyle Nothing = Nothing
    litStyle (Just fn) = isLitFile fn

export
resetProofState : {auto o : Ref ROpts REPLOpts} ->
                  Core ()
resetProofState
    = do opts <- get ROpts
         put ROpts (record { psResult = Nothing,
                             gdResult = Nothing } opts)

export
setSource : {auto o : Ref ROpts REPLOpts} ->
            String -> Core ()
setSource src
    = do opts <- get ROpts
         put ROpts (record { source = src } opts)

export
getSource : {auto o : Ref ROpts REPLOpts} ->
            Core String
getSource
    = do opts <- get ROpts
         pure (source opts)

export
getSourceLine : {auto o : Ref ROpts REPLOpts} ->
                Int -> Core (Maybe String)
getSourceLine l
    = do src <- getSource
         pure $ findLine (integerToNat (cast (l-1))) (lines src)
  where
    findLine : Nat -> List String -> Maybe String
    findLine Z (l :: ls) = Just l
    findLine (S k) (l :: ls) = findLine k ls
    findLine _ [] = Nothing

export
getLitStyle : {auto o : Ref ROpts REPLOpts} ->
              Core (Maybe LiterateStyle)
getLitStyle
    = do opts <- get ROpts
         pure (literateStyle opts)

export
setCurrentElabSource : {auto o : Ref ROpts REPLOpts} ->
                       String -> Core ()
setCurrentElabSource src
    = do opts <- get ROpts
         put ROpts (record { currentElabSource = src } opts)

export
getCurrentElabSource : {auto o : Ref ROpts REPLOpts} ->
                       Core String
getCurrentElabSource
     = do opts <- get ROpts
          pure (currentElabSource opts)

addCodegen : {auto o : Ref ROpts REPLOpts} ->
             String -> Codegen -> Core ()
addCodegen s cg = do opts <- get ROpts
                     put ROpts (record { extraCodegens $= ((s,cg)::) } opts)

export
getCodegen : {auto o : Ref ROpts REPLOpts} ->
             String -> Core (Maybe Codegen)
getCodegen s = do opts <- get ROpts
                  pure $ lookup s (extraCodegens opts)

export
getConsoleWidth : {auto o : Ref ROpts REPLOpts} -> Core (Maybe Nat)
getConsoleWidth = do opts <- get ROpts
                     pure $ opts.consoleWidth

export
setConsoleWidth : {auto o : Ref ROpts REPLOpts} -> Maybe Nat -> Core ()
setConsoleWidth n = do opts <- get ROpts
                       put ROpts (record { consoleWidth = n } opts)

export
getColor : {auto o : Ref ROpts REPLOpts} -> Core Bool
getColor = do opts <- get ROpts
              pure $ opts.color

export
setColor : {auto o : Ref ROpts REPLOpts} -> Bool -> Core ()
setColor b = do opts <- get ROpts
                put ROpts (record { color = b } opts)


text:
module Examples.CSS.Balls

import Data.Vect
import Examples.CSS.Colors
import public Examples.CSS.Core
import Rhone.JS
import Text.CSS

--------------------------------------------------------------------------------
--          IDs
--------------------------------------------------------------------------------

public export
out : ElemRef HTMLCanvasElement
out = Id Canvas "balls_out"

public export
btnRun : ElemRef HTMLButtonElement
btnRun = Id Button "balls_run"

public export
txtCount : ElemRef HTMLInputElement
txtCount = Id Input "balls_numballs"

public export
log : ElemRef HTMLDivElement
log = Id Div "balls_log"

--------------------------------------------------------------------------------
--          Rules
--------------------------------------------------------------------------------

export
ballsContent : String
ballsContent = "balls_content"

export
lblCount : String
lblCount = "balls_lblcount"

data Tag = LNum | INum | BRun | LFPS | Anim | Dot

AreaTag Tag where
  showTag LNum = "LNum"
  showTag INum = "INum"
  showTag BRun = "BRun"
  showTag LFPS = "LFPS"
  showTag Anim = "Anim"
  showTag Dot  = "."

export
css : List (Rule 1)
css =
  [ Media "min-width: 300px"
      [ class ballsContent !!
          [ Display             .= Area
              (replicate 4 MinContent)
              [MaxContent, MaxContent]
              [ [LNum, INum]
              , [Dot,  BRun]
              , [LFPS, LFPS]
              , [Anim, Anim]
              ]

          , ColumnGap           .= px 10
          , RowGap              .= px 10
          , Padding             .= VH (px 20) (px 10)
          ]
      ]

  , Media "min-width: 800px"
      [ class ballsContent !!
          [ Display             .= Area
              (replicate 4 MinContent)
              [MaxContent, MaxContent, fr 1]
              [ [LNum, INum, Anim]
              , [Dot,  BRun, Anim]
              , [LFPS, LFPS, Anim]
              , [Dot,  Dot,  Anim]
              ]

          , ColumnGap           .= px 10
          , RowGap              .= px 10
          , Padding             .= VH (px 20) (px 10)
          ]
      ]

  , class lblCount !! [ GridArea .= LNum ]

  , idRef txtCount !!
      [ GridArea        .= INum
      , TextAlign       .= End
      ]

  , idRef btnRun !! [ GridArea .= BRun ]

  , idRef log !! [ GridArea .= LFPS ]

  , idRef out !!
      [ JustifySelf     .= Center
      , GridArea        .= Anim
      , MaxWidth        .= px 500
      , Width           .= px 500
      ]
  ]


text:
--    Copyright 2017, the blau.io contributors
--
--    Licensed under the Apache License, Version 2.0 (the "License");
--    you may not use this file except in compliance with the License.
--    You may obtain a copy of the License at
--
--        http://www.apache.org/licenses/LICENSE-2.0
--
--    Unless required by applicable law or agreed to in writing, software
--    distributed under the License is distributed on an "AS IS" BASIS,
--    WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
--    See the License for the specific language governing permissions and
--    limitations under the License.

module API.Web.DOM.Element

import API.Web.HTML.HTMLElement
import API.Web.Infra.Namespaces
import IdrisScript

%access public export
%default total

||| An Element represents an object of a Document.
|||
||| The original specification can be found at
||| https://dom.spec.whatwg.org/#interface-element
data Element : Type where
  FromHTMLElement : HTMLElement          -> Element
  New             : (localName : String) -> (self : JSRef) -> Element

||| elementFromPointer is a helper function for easily creating Elements from
||| JavaScript references.
|||
||| @ ref A pointer to an element
elementFromPointer : (ref : JSRef) -> JS_IO $ Maybe Element
elementFromPointer ref = case !maybeNamespace of
    Nothing   => pure Nothing
    (Just ns) => case !maybeLocalName of
      Nothing          => pure Nothing
      (Just localName) => case ns of
        API.Web.Infra.Namespaces.html => case !(htmlElementFromPointer ref) of
          Nothing            => pure Nothing
          (Just htmlElement) => pure $ Just $ FromHTMLElement htmlElement
        _                             => pure $ Just $ New localName ref
  where
    maybeNamespace : JS_IO $ Maybe String
    maybeNamespace = let
        getNameSpace = jscall "%0.namespaceURI" (JSRef -> JS_IO JSRef) ref
      in
        case !(IdrisScript.pack !getNameSpace) of
             (JSString ** str) => pure $ Just $ fromJS str
             _                 => pure Nothing

    maybeLocalName : JS_IO $ Maybe String
    maybeLocalName = let
        getLocalName = jscall "%0.localName" (JSRef -> JS_IO JSRef) ref
      in
        case !(IdrisScript.pack !getLocalName) of
             (JSString ** str) => pure $ Just $ fromJS str
             _                 => pure Nothing

max_stars_repo_name: blau-io/idris-web

max_issues_repo_name: pierrebeaucamp/idris-dom

max_forks_repo_name: pierrebeaucamp/idris-dom


text:
module Idris.IDEMode.Holes

import Core.Env
import Core.Context.Log

import Data.String

import Idris.Resugar
import Idris.Syntax
import Idris.Pretty

import Idris.IDEMode.Commands

import Libraries.Data.String.Extra as L

%default covering

public export
record Premise where
  constructor MkHolePremise
  name         : Name
  type         : IPTerm
  multiplicity : RigCount
  isImplicit   : Bool

public export
record Data where
  constructor MkHoleData
  name : Name
  type : IPTerm
  context : List Holes.Premise

export
prettyHoles : List Holes.Data -> Doc IdrisSyntax
prettyHoles holes = case holes of
  []  => "No holes"
  [x] => "1 hole" <+> colon <++> prettyHole x
  xs  => vcat $ (pretty (length xs) <++> pretty "holes" <+> colon)
              :: map (indent 2 . prettyHole) xs

  where

   prettyHole : Holes.Data -> Doc IdrisSyntax
   prettyHole x = pretty x.name <++> colon <++> prettyTerm x.type

||| If input is a hole, return number of locals in scope at binding
||| point
export
isHole : GlobalDef -> Maybe Nat
isHole def
    = case definition def of
           Hole locs _ => Just locs
           PMDef pi _ _ _ _ =>
                 case holeInfo pi of
                      NotHole => Nothing
                      SolvedHole n => Just n
           None => Just 0
           _ => Nothing

-- Bring these back into REPL.idr
showName : Name -> Bool
showName (UN Underscore) = False
showName (MN _ _) = False
showName _ = True

impBracket : Bool -> String -> String
impBracket False str = str
impBracket True str = "{" ++ str ++ "}"

prettyImpBracket : Bool -> Doc ann -> Doc ann
prettyImpBracket False = id
prettyImpBracket True = braces

tidy : Name -> String
tidy (MN n _) = n
tidy n = show n

prettyName : Name -> Doc ann
prettyName (MN n _) = pretty n
prettyName n = pretty n

export
extractHoleData : {vars : _} ->
          {auto c : Ref Ctxt Defs} ->
          {auto s : Ref Syn SyntaxInfo} ->
          Defs -> Env Term vars -> Name -> Nat -> Term vars ->
          Core Holes.Data
extractHoleData defs env fn (S args) (Bind fc x (Let _ c val ty) sc)
  = extractHoleData defs env fn args (subst val sc)
extractHoleData defs env fn (S args) (Bind fc x b sc)
  = do rest <- extractHoleData defs (b :: env) fn args sc
       let True = showName x
         | False => do log "idemode.hole" 10 $ "Not showing name: " ++ show x
                       pure rest
       log "idemode.hole" 10 $ "Showing name: " ++ show x
       ity <- resugar env !(normalise defs env (binderType b))
       let premise = MkHolePremise x ity (multiplicity b) (isImplicit b)
       pure $ { context $= (premise ::)  } rest
extractHoleData defs env fn args ty
  = do nty <- normalise defs env ty
       ity <- resugar env nty
       log "idemode.hole" 20 $
          "Return type: " ++ show !(toFullNames ty)
          ++ "\n  Evaluated to: " ++ show !(toFullNames nty)
          ++ "\n  Resugared to: " ++ show ity
       pure $ MkHoleData fn ity []

export
holeData : {vars : _} ->
           {auto c : Ref Ctxt Defs} ->
           {auto s : Ref Syn SyntaxInfo} ->
           Defs -> Env Term vars -> Name -> Nat -> Term vars ->
           Core Holes.Data

holeData gam env fn args ty
  = do hdata <- extractHoleData gam env fn args ty
       pp <- getPPrint
       pure $ if showImplicits pp
              then hdata
              else { context $= dropShadows } hdata
  where
    dropShadows : List Holes.Premise -> List Holes.Premise
    dropShadows [] = []
    dropShadows (premise :: rest)
        = if premise.name `elem` map name rest
             then            dropShadows rest
             else premise :: dropShadows rest

export
getUserHolesData :
  {auto c : Ref Ctxt Defs} ->
  {auto s : Ref Syn SyntaxInfo} ->
  Core (List Holes.Data)
getUserHolesData
    = do defs <- get Ctxt
         let ctxt = gamma defs
         ms  <- getUserHoles
         let globs = concat !(traverse (\n => lookupCtxtName n ctxt) ms)
         let holesWithArgs = mapMaybe (\(n, i, gdef) => do args <- isHole gdef
                                                           pure (n, gdef, args))
                                      globs
         traverse (\n_gdef_args =>
                     -- Inference can't deal with this for now :/
                     let (n, gdef, args) = the (Name, GlobalDef, Nat) n_gdef_args in
                     holeData defs [] n args (type gdef))
                  holesWithArgs

export
showHole : {vars : _} ->
          {auto c : Ref Ctxt Defs} ->
          {auto s : Ref Syn SyntaxInfo} ->
          Defs -> Env Term vars -> Name -> Nat -> Term vars ->
          Core String

showHole defs env fn args ty
    = do hdata <- holeData defs env fn args ty
         case hdata.context of
           [] => pure $ show (hdata.name) ++ " : " ++ show hdata.type
           _  => pure $ concat
              (map (\ premise : Holes.Premise => " " ++ showCount premise.multiplicity ++ " "
                             ++ (impBracket premise.isImplicit $
                                 tidy premise.name ++ " : " ++ (show premise.type) ++ "\n" )
                   ) hdata.context)
              ++ "-------------------------------------\n"
              ++ nameRoot (hdata.name) ++ " : " ++ show hdata.type

export
prettyRigHole : RigCount -> Doc ann
prettyRigHole = elimSemi (pretty '0' <+> space)
                         (pretty '1' <+> space)
                         (const $ space <+> space)

export
prettyHole : {vars : _} ->
             {auto c : Ref Ctxt Defs} ->
             {auto s : Ref Syn SyntaxInfo} ->
             Defs -> Env Term vars -> Name -> Nat -> Term vars ->
             Core (Doc IdrisSyntax)
prettyHole defs env fn args ty
  = do hdata <- holeData defs env fn args ty
       case hdata.context of
            [] => pure $ pretty hdata.name <++> colon <++> prettyTerm hdata.type
            _  => pure $ (indent 1 $ vsep $
                            map (\premise => prettyRigHole premise.multiplicity
                                    <+> prettyImpBracket premise.isImplicit (prettyName premise.name <++> colon <++> prettyTerm premise.type))
                                    hdata.context) <+> hardline
                    <+> (pretty $ L.replicate 30 '-') <+> hardline
                    <+> pretty (nameRoot $ hdata.name) <++> colon <++> prettyTerm hdata.type

premiseIDE : Holes.Premise -> HolePremise
premiseIDE premise = IDE.MkHolePremise
  { name = " " ++ showCount premise.multiplicity ++ " "
               ++ (impBracket premise.isImplicit $
                  tidy premise.name)
  , type = show premise.type
  }

export
holeIDE : Holes.Data -> IDE.HoleData
holeIDE hole = IDE.MkHoleData
  { name = show hole.name
  , type = show hole.type
  , context = map premiseIDE hole.context
  }


text:
record Foo where
  constructor MkFoo
  (^) : Nat

AFoo : Foo
AFoo = MkFoo { (^) = 42}


text:
module Average

||| Calculate the average length of words in a string
||| @str a string containing words separated by whitespace
export
average : (str : String) -> Double
average str = let numWords = wordCount str
                  totalLength = sum (allLengths (words str)) in
                  cast totalLength / cast numWords
    where
        wordCount : String -> Nat
        wordCount str = length (words str)

        allLengths : List String -> List Nat
        allLengths strs = map length strs

max_stars_repo_name: curtisalexander/tdd-idris

max_issues_repo_name: curtisalexander/tdd-idris

max_forks_repo_name: curtisalexander/tdd-idris


text:
-- examples in "Type-Driven Development with Idris"
-- chapter 7

-- check that all functions are total
%default total

--
-- Binary Search Trees
--

data BST elem = Empty
              | Node (BST elem) elem (BST elem)

-- from Haskell's Data.Tree
shift : String -> String -> List String -> List String
shift str1 str2 strings
  = zipWith (++) (take (length strings) $ str1 :: repeat str2) strings

-- from Haskell's Data.Tree
partial
draw : Show elem => BST elem -> List String
draw Empty = ["*"]
draw (Node left x right) = (show x) :: helper [left, right]
where
  partial
  helper : List (BST elem) -> List String
  helper [] = []
  helper (t :: []) = "|" :: shift "`- " "   " (draw t)
  helper (t :: ts) = "|" :: shift "+- " "|  " (draw t) ++ helper ts

-- from Haskell's Data.Tree
partial
drawTree : Show elem => BST elem -> String
drawTree = unlines . draw

partial
Show elem => Show (BST elem) where
  show x = drawTree x

insert : Ord elem => elem -> BST elem -> BST elem
insert x Empty = Node Empty x Empty
insert x orig@(Node left val right)
 = case compare x val of
     LT => Node (insert x left) val right
     EQ => orig
     GT => Node left val (insert x right)

listToTree : Ord a => List a -> BST a
listToTree [] = Empty
listToTree (x :: xs) = insert x $ listToTree xs

treeToList : BST a -> List a
treeToList Empty = []
treeToList (Node left val right) = treeToList left ++ [val] ++ treeToList right

Functor BST where
  map func Empty = Empty
  map func (Node left val right) =
    Node (map func left) (func val) (map func right)

-- we have two alternatives to implement Foldable for BST
-- one here: following https://hackage.haskell.org/package/base-4.11.1.0/docs/Data-Foldable.html
-- one in chapter 7 of the book
--
-- > :let tree = listToTree [1,4,6,7,3]
-- > foldr (::) [] tree
-- [1, 3, 4, 6, 7] : List Integer
-- > foldl (\x,y => x ++ [y]) [] tree
-- [1, 3, 4, 6, 7] : List Integer
--
-- > foldr @{chapter} (::) [] tree
-- [3, 7, 6, 4, 1] : List Integer
-- > foldl @{chapter} (\x,y => x ++ [y]) [] tree
-- [3, 7, 6, 4, 1] : List Integer

-- following https://hackage.haskell.org/package/base-4.11.1.0/docs/Data-Foldable.html
-- foldr func (func e (foldr func acc right)) left
--
Foldable BST where
  foldr func acc Empty = acc
  foldr func acc (Node left e right) =
    let rightVal = foldr func acc right
        eVal = func e rightVal
    in
        foldr func eVal left

-- following the chapter
-- func e (foldr func (foldr func acc left) right)
--
[chapter] Foldable BST where
  foldr func acc Empty = acc
  foldr func acc (Node left e right) =
    let leftVal = foldr func acc left
        rightVal = foldr func leftVal right
    in
        func e rightVal

-- call with:
-- > :exec printTree $ listToTree [1,4,6,3,7]
-- 7
-- |
-- +- 3
-- |  |
-- |  +- 1
-- |  |  |
-- |  |  +- *
-- |  |  |
-- |  |  `- *
-- |  |
-- |  `- 6
-- |     |
-- |     +- 4
-- |     |  |
-- |     |  +- *
-- |     |  |
-- |     |  `- *
-- |     |
-- |     `- *
-- |
-- `- *
partial
printTree : Show elem => (BST elem) -> IO ()
printTree t = do putStrLn (show t)

max_stars_repo_name: pascalpoizat/idris-book

max_issues_repo_name: pascalpoizat/idris-book

max_forks_repo_name: pascalpoizat/idris-book


text:
module Data.Prim.Int16

import public Control.WellFounded
import public Data.DPair
import public Data.Prim.Ord
import public Algebra.Solver.Ring
import Syntax.PreorderReasoning

%default total

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

||| Lower bound of `Int16`
public export
MinInt16 : Int16
MinInt16 = -0x8000

||| Upper bound of `Int16`
public export
MaxInt16 : Int16
MaxInt16 = 0x7fff

||| `m >= MinInt16` for all `m` of type `Int16`.
export
0 GTE_MinInt16 : (m : Int16) -> m >= MinInt16
GTE_MinInt16 m = case comp MinInt16 m of
  LT x f g => %search
  EQ f x g => %search
  GT f g x => assert_total
            $ idris_crash "IMPOSSIBLE: Int16 smaller than \{show MinInt16}"

||| Not value of type `Int16` is less than zero.
export
0 Not_LT_MinInt16 : m < MinInt16 -> Void
Not_LT_MinInt16 = GTE_not_LT (GTE_MinInt16 m)

||| `m <= MaxInt16` for all `m` of type `Int16`.
export
0 LTE_MaxInt16 : (m : Int16) -> m <= MaxInt16
LTE_MaxInt16 m = case comp m MaxInt16 of
  LT x f g => %search
  EQ f x g => %search
  GT f g x => assert_total
            $ idris_crash "IMPOSSIBLE: Int16 greater than \{show MaxInt16}"

||| Not value of type `Int16` is greater than `MaxInt16`.
export
0 Not_GT_MaxInt16 : m > MaxInt16 -> Void
Not_GT_MaxInt16 = LTE_not_GT (LTE_MaxInt16 m)

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

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

||| Every value of type `Int16` is accessible with relation
||| to `(>)`.
export
accessGT : (m : Int16) -> Accessible (>) m
accessGT m = Access $ \n,gt => accessGT (assert_smaller m n)

||| `(>)` is well founded.
export %inline
[GT] WellFounded Int16 (>) where
  wellFounded = accessGT

--------------------------------------------------------------------------------
--          Arithmetics
--------------------------------------------------------------------------------

||| Safe division.
export %inline
sdiv : (n,d : Int16) -> (0 prf : d /= 0) => Int16
sdiv n d = n `div` d

||| Safe modulo.
export %inline
smod : (n,d : Int16) -> (0 prf : d /= 0) => Int16
smod n d = n `mod` d


text:
module Core.Env

import Core.TT
import Data.List

%default total

-- Environment containing types and values of local variables
public export
data Env : (tm : List Name -> Type) -> List Name -> Type where
     Nil : Env tm []
     (::) : Binder (tm vars) -> Env tm vars -> Env tm (x :: vars)

export
extend : (x : Name) -> Binder (tm vars) -> Env tm vars -> Env tm (x :: vars)
extend x = (::) {x}

export
length : Env tm xs -> Nat
length [] = 0
length (_ :: xs) = S (length xs)

export
lengthNoLet : Env tm xs -> Nat
lengthNoLet [] = 0
lengthNoLet (Let _ _ _ _ :: xs) = lengthNoLet xs
lengthNoLet (_ :: xs) = S (lengthNoLet xs)

export
namesNoLet : {xs : _} -> Env tm xs -> List Name
namesNoLet [] = []
namesNoLet (Let _ _ _ _ :: xs) = namesNoLet xs
namesNoLet {xs = x :: _} (_ :: env) = x :: namesNoLet env

public export
data IsDefined : Name -> List Name -> Type where
  MkIsDefined : {idx : Nat} -> RigCount -> (0 p : IsVar n idx vars) ->
                IsDefined n vars

export
defined : {vars : _} ->
          (n : Name) -> Env Term vars ->
          Maybe (IsDefined n vars)
defined n [] = Nothing
defined {vars = x :: xs} n (b :: env)
    = case nameEq n x of
           Nothing => do MkIsDefined rig prf <- defined n env
                         pure (MkIsDefined rig (Later prf))
           Just Refl => Just (MkIsDefined (multiplicity b) First)

export
bindEnv : {vars : _} -> FC -> Env Term vars -> (tm : Term vars) -> ClosedTerm
bindEnv loc [] tm = tm
bindEnv loc (b :: env) tm
    = bindEnv loc env (Bind loc _ b tm)

revOnto : (xs, vs : _) -> reverseOnto xs vs = reverse vs ++ xs
revOnto xs [] = Refl
revOnto xs (v :: vs)
    = rewrite revOnto (v :: xs) vs in
        rewrite appendAssociative (reverse vs) [v] xs in
				  rewrite revOnto [v] vs in Refl

revNs : (vs, ns : List a) -> reverse ns ++ reverse vs = reverse (vs ++ ns)
revNs [] ns = rewrite appendNilRightNeutral (reverse ns) in Refl
revNs (v :: vs) ns
    = rewrite revOnto [v] vs in
        rewrite revOnto [v] (vs ++ ns) in
          rewrite sym (revNs vs ns) in
            rewrite appendAssociative (reverse ns) (reverse vs) [v] in
              Refl

-- Weaken by all the names at once at the end, to save multiple traversals
-- in big environments
-- Also reversing the names at the end saves significant time over concatenating
-- when environments get fairly big.
getBinderUnder : Weaken tm =>
                 {vars : _} -> {idx : Nat} ->
                 (ns : List Name) ->
                 (0 p : IsVar x idx vars) -> Env tm vars ->
                 Binder (tm (reverseOnto vars ns))
getBinderUnder {idx = Z} {vars = v :: vs} ns First (b :: env)
    = rewrite revOnto vs (v :: ns) in map (weakenNs (reverse (mkSizeOf (v :: ns)))) b
getBinderUnder {idx = S k} {vars = v :: vs} ns (Later lp) (b :: env)
    = getBinderUnder (v :: ns) lp env

export
getBinder : Weaken tm =>
            {vars : _} -> {idx : Nat} ->
            (0 p : IsVar x idx vars) -> Env tm vars -> Binder (tm vars)
getBinder el env = getBinderUnder [] el env

-- For getBinderLoc, we are not reusing getBinder because there is no need to
-- needlessly weaken stuff;
export
getBinderLoc : {vars : _} -> {idx : Nat} -> (0 p : IsVar x idx vars) -> Env tm vars -> FC
getBinderLoc {idx = Z}   First     (b :: _)   = binderLoc b
getBinderLoc {idx = S k} (Later p) (_ :: env) = getBinderLoc p env

-- Make a type which abstracts over an environment
-- Don't include 'let' bindings, since they have a concrete value and
-- shouldn't be generalised
export
abstractEnvType : {vars : _} ->
                  FC -> Env Term vars -> (tm : Term vars) -> ClosedTerm
abstractEnvType fc [] tm = tm
abstractEnvType fc (Let fc' c val ty :: env) tm
    = abstractEnvType fc env (Bind fc _ (Let fc' c val ty) tm)
abstractEnvType fc (Pi fc' c e ty :: env) tm
    = abstractEnvType fc env (Bind fc _ (Pi fc' c e ty) tm)
abstractEnvType fc (b :: env) tm
    = let bnd = Pi (binderLoc b) (multiplicity b) Explicit (binderType b)
       in abstractEnvType fc env (Bind fc _ bnd tm)

-- As above, for the corresponding term
export
abstractEnv : {vars : _} ->
              FC -> Env Term vars -> (tm : Term vars) -> ClosedTerm
abstractEnv fc [] tm = tm
abstractEnv fc (Let fc' c val ty :: env) tm
    = abstractEnv fc env (Bind fc _ (Let fc' c val ty) tm)
abstractEnv fc (b :: env) tm
    = let bnd = Lam (binderLoc b) (multiplicity b) Explicit (binderType b)
      in abstractEnv fc env (Bind fc _ bnd tm)

-- As above, but abstract over all binders including lets
export
abstractFullEnvType : {vars : _} ->
                      FC -> Env Term vars -> (tm : Term vars) -> ClosedTerm
abstractFullEnvType fc [] tm = tm
abstractFullEnvType fc (Pi fc' c e ty :: env) tm
    = abstractFullEnvType fc env (Bind fc _ (Pi fc' c e ty) tm)
abstractFullEnvType fc (b :: env) tm
    = let bnd = Pi fc (multiplicity b) Explicit (binderType b)
      in abstractFullEnvType fc env (Bind fc _ bnd tm)

export
letToLam : Env Term vars -> Env Term vars
letToLam [] = []
letToLam (Let fc c val ty :: env) = Lam fc c Explicit ty :: letToLam env
letToLam (b :: env) = b :: letToLam env

mutual
	-- Quicker, if less safe, to store variables as a Nat, for quick comparison
  findUsed : {vars : _} ->
             Env Term vars -> List Nat -> Term vars -> List Nat
  findUsed env used (Local fc r idx p)
      = if elemBy eqNat idx used
           then used
           else assert_total (findUsedInBinder env (idx :: used)
                                               (getBinder p env))
    where
      eqNat : Nat -> Nat -> Bool
      eqNat i j = natToInteger i == natToInteger j
  findUsed env used (Meta _ _ _ args)
      = findUsedArgs env used args
    where
      findUsedArgs : Env Term vars -> List Nat -> List (Term vars) -> List Nat
      findUsedArgs env u [] = u
      findUsedArgs env u (a :: as)
          = findUsedArgs env (findUsed env u a) as
  findUsed env used (Bind fc x b tm)
      = assert_total $
          dropS (findUsed (b :: env)
                          (map S (findUsedInBinder env used b))
                          tm)
    where
      dropS : List Nat -> List Nat
      dropS [] = []
      dropS (Z :: xs) = dropS xs
      dropS (S p :: xs) = p :: dropS xs
  findUsed env used (App fc fn arg)
      = findUsed env (findUsed env used fn) arg
  findUsed env used (As fc s a p)
      = findUsed env (findUsed env used a) p
  findUsed env used (TDelayed fc r tm)
      = findUsed env used tm
  findUsed env used (TDelay fc r ty tm)
      = findUsed env (findUsed env used ty) tm
  findUsed env used (TForce fc r tm)
      = findUsed env used tm
  findUsed env used _ = used

  findUsedInBinder : {vars : _} ->
                     Env Term vars -> List Nat ->
                     Binder (Term vars) -> List Nat
  findUsedInBinder env used (Let _ _ val ty)
    = findUsed env (findUsed env used val) ty
  findUsedInBinder env used (PLet _ _ val ty)
    = findUsed env (findUsed env used val) ty
  findUsedInBinder env used b = findUsed env used (binderType b)

toVar : (vars : List Name) -> Nat -> Maybe (Var vars)
toVar (v :: vs) Z = Just (MkVar First)
toVar (v :: vs) (S k)
   = do MkVar prf <- toVar vs k
        Just (MkVar (Later prf))
toVar _ _ = Nothing

export
findUsedLocs : {vars : _} ->
               Env Term vars -> Term vars -> List (Var vars)
findUsedLocs env tm
    = mapMaybe (toVar _) (findUsed env [] tm)

isUsed : Nat -> List (Var vars) -> Bool
isUsed n [] = False
isUsed n (v :: vs) = n == varIdx v || isUsed n vs

mkShrinkSub : {n : _} ->
              (vars : _) -> List (Var (n :: vars)) ->
              (newvars ** SubVars newvars (n :: vars))
mkShrinkSub [] els
    = if isUsed 0 els
         then (_ ** KeepCons SubRefl)
         else (_ ** DropCons SubRefl)
mkShrinkSub (x :: xs) els
    = let (_ ** subRest) = mkShrinkSub xs (dropFirst els) in
					if isUsed 0 els
				     then (_ ** KeepCons subRest)
				     else (_ ** DropCons subRest)

mkShrink : {vars : _} ->
           List (Var vars) ->
           (newvars ** SubVars newvars vars)
mkShrink {vars = []} xs = (_ ** SubRefl)
mkShrink {vars = v :: vs} xs = mkShrinkSub _ xs

-- Find the smallest subset of the environment which is needed to type check
-- the given term
export
findSubEnv : {vars : _} ->
             Env Term vars -> Term vars ->
						 (vars' : List Name ** SubVars vars' vars)
findSubEnv env tm = mkShrink (findUsedLocs env tm)

export
shrinkEnv : Env Term vars -> SubVars newvars vars -> Maybe (Env Term newvars)
shrinkEnv env SubRefl = Just env
shrinkEnv (b :: env) (DropCons p) = shrinkEnv env p
shrinkEnv (b :: env) (KeepCons p)
    = do env' <- shrinkEnv env p
         b' <- assert_total (shrinkBinder b p)
         pure (b' :: env')

-- Make a dummy environment, if we genuinely don't care about the values
-- and types of the contents.
-- We use this when building and comparing case trees.
export
mkEnv : FC -> (vs : List Name) -> Env Term vs
mkEnv fc [] = []
mkEnv fc (n :: ns) = PVar fc top Explicit (Erased fc False) :: mkEnv fc ns

-- Update an environment so that all names are guaranteed unique. In the
-- case of a clash, the most recently bound is left unchanged.
export
uniqifyEnv : {vars : _} ->
             Env Term vars ->
             (vars' ** (Env Term vars', CompatibleVars vars vars'))
uniqifyEnv env = uenv [] env
  where
    next : Name -> Name
    next (MN n i) = MN n (i + 1)
    next (UN n) = MN n 0
    next (NS ns n) = NS ns (next n)
    next n = MN (show n) 0

    uniqueLocal : List Name -> Name -> Name
    uniqueLocal vs n
       = if n `elem` vs
                 -- we'll find a new name eventualy since the list of names
                 -- is empty, and next generates something new. But next has
                 -- to be correct... an exercise for someone: this could
                 -- probebly be done without an assertion by making a stream of
                 -- possible names...
            then assert_total (uniqueLocal vs (next n))
            else n

    uenv : {vars : _} ->
           List Name -> Env Term vars ->
           (vars' ** (Env Term vars', CompatibleVars vars vars'))
    uenv used [] = ([] ** ([], CompatPre))
    uenv used {vars = v :: vs} (b :: bs)
        = if v `elem` used
             then let v' = uniqueLocal used v
                      (vs' ** (env', compat)) = uenv (v' :: used) bs
                      b' = map (renameVars compat) b in
                  (v' :: vs' ** (b' :: env', CompatExt compat))
             else let (vs' ** (env', compat)) = uenv (v :: used) bs
                      b' = map (renameVars compat) b in
                  (v :: vs' ** (b' :: env', CompatExt compat))

export
allVars : {vars : _} -> Env Term vars -> List (Var vars)
allVars [] = []
allVars (v :: vs) = MkVar First :: map weaken (allVars vs)

export
allVarsNoLet : {vars : _} -> Env Term vars -> List (Var vars)
allVarsNoLet [] = []
allVarsNoLet (Let _ _ _ _ :: vs) = map weaken (allVars vs)
allVarsNoLet (v :: vs) = MkVar First :: map weaken (allVars vs)


text:
||| Storable objects
|||
||| Copyright 2021, HATTORI, Hiroki
||| This file is released under the MIT license, see LICENSE for more detail.
|||
module Foreign.Memory.Storable

%default total

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

public export
interface Storable ty where
  %inline sizeOf : Nat
  %inline alignOf : Nat
  unsafeLoad : HasIO io => (ofs:Nat) -> Ptr ty -> io ty
  unsafeStore : HasIO io => (ofs:Nat) -> ty -> Ptr ty -> io ()

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

%foreign "scheme,chez:foreign-ref 'short"
prim__foreignRef_Short : (addr:AnyPtr) -> (ofs:Int) -> PrimIO Int

%foreign "scheme,chez:foreign-ref 'unsigned-short"
prim__foreignRef_UShort : (addr:AnyPtr) -> (ofs:Int) -> PrimIO Int

%foreign "scheme,chez:foreign-sizeof 'int"
prim__foreignSizeOf_Int : Int
%foreign "scheme,chez:foreign-ref 'int"
prim__foreignRef_Int : (addr:Ptr Int) -> (ofs:Int) -> PrimIO Int
%foreign "scheme,chez:foreign-set! 'int"
prim__foreignSet_Int : (addr:Ptr Int) -> (ofs:Int) -> Int -> PrimIO ()

-- %foreign "scheme,chez:foreign-ref unsigned"
-- prim__foreignRef_UInt : (addr:AnyPtr) -> (ofs:Int) -> PrimIO Int

%foreign "scheme,chez:foreign-ref 'size_t"
prim__foreignRef_SizeT : (addr:AnyPtr) -> (ofs:Int) -> PrimIO Int

%foreign "scheme,chez:foreign-sizeof 'double"
prim__foreignSizeOf_Double : Int
%foreign "scheme,chez:foreign-ref 'double"
prim__foreignRef_Double : (addr:Ptr Double) -> (ofs:Int) -> PrimIO Double
%foreign "scheme,chez:foreign-set! 'double"
prim__foreignSet_Double : (addr:Ptr Double) -> (ofs:Int) -> Double -> PrimIO ()

%foreign "scheme,chez:foreign-sizeof 'void*"
prim__foreignSizeOf_Ptr : Int
%foreign "scheme,chez:foreign-ref 'void*"
prim__foreignRef_Ptr : (addr:AnyPtr) -> (ofs:Int) -> PrimIO AnyPtr
%foreign "scheme,chez:foreign-set! 'void*"
prim__foreignSet_Ptr : (addr:AnyPtr) -> (ofs:Int) -> AnyPtr -> PrimIO ()

%foreign "scheme,chez:foreign-ref 'integer-8"
prim__foreignRef_I8 : (addr:Ptr Bits8) -> (ofs:Int) -> PrimIO Bits8
%foreign "scheme,chez:foreign-set! 'integer-8"
prim__foreignSet_I8 : (addr:Ptr Bits8) -> (ofs:Int) -> Bits8 -> PrimIO ()

%foreign "scheme,chez:foreign-ref 'unsigned-8"
prim__foreignRef_U8 : (addr:Ptr Bits8) -> (ofs:Int) -> PrimIO Bits8
%foreign "scheme,chez:foreign-set! 'unsigned-8"
prim__foreignSet_U8 : (addr:Ptr Bits8) -> (ofs:Int) -> Bits8 -> PrimIO ()

%foreign "scheme,chez:foreign-ref 'integer-16"
prim__foreignRef_I16 : (addr:Ptr Bits16) -> (ofs:Int) -> PrimIO Bits16
%foreign "scheme,chez:foreign-set! 'integer-16"
prim__foreignSet_I16 : (addr:Ptr Bits16) -> (ofs:Int) -> Bits16 -> PrimIO ()

%foreign "scheme,chez:foreign-ref 'unsigned-16"
prim__foreignRef_U16 : (addr:Ptr Bits16) -> (ofs:Int) -> PrimIO Bits16
%foreign "scheme,chez:foreign-set! 'unsigned-16"
prim__foreignSet_U16 : (addr:Ptr Bits16) -> (ofs:Int) -> Bits16 -> PrimIO ()

%foreign "scheme,chez:foreign-ref 'integer-132"
prim__foreignRef_I32 : (addr:Ptr Bits32) -> (ofs:Int) -> PrimIO Bits32
%foreign "scheme,chez:foreign-set! 'integer-132"
prim__foreignSet_I32 : (addr:Ptr Bits32) -> (ofs:Int) -> Bits32 -> PrimIO ()

%foreign "scheme,chez:foreign-ref 'unsigned-132"
prim__foreignRef_U32 : (addr:Ptr Bits32) -> (ofs:Int) -> PrimIO Bits32
%foreign "scheme,chez:foreign-set! 'unsigned-132"
prim__foreignSet_U32 : (addr:Ptr Bits32) -> (ofs:Int) -> Bits32 -> PrimIO ()

%foreign "scheme,chez:foreign-ref 'integer-164"
prim__foreignRef_I64 : (addr:Ptr Bits64) -> (ofs:Int) -> PrimIO Bits64
%foreign "scheme,chez:foreign-set! 'integer-164"
prim__foreignSet_I64 : (addr:Ptr Bits64) -> (ofs:Int) -> Bits64 -> PrimIO ()

%foreign "scheme,chez:foreign-ref 'unsigned-164"
prim__foreignRef_U64 : (addr:Ptr Bits64) -> (ofs:Int) -> PrimIO Bits64
%foreign "scheme,chez:foreign-set! 'unsigned-164"
prim__foreignSet_U64 : (addr:Ptr Bits64) -> (ofs:Int) -> Bits64 -> PrimIO ()

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

public export
Storable Int where
  sizeOf = fromInteger $ cast{to=Integer} prim__foreignSizeOf_Int
  alignOf = fromInteger $ cast{to=Integer} prim__foreignSizeOf_Int
  unsafeLoad o p = primIO $ prim__foreignRef_Int p (cast o)
  unsafeStore o v p = primIO $ prim__foreignSet_Int p (cast o) v

public export
Storable Double where
  sizeOf = fromInteger $ cast{to=Integer} prim__foreignSizeOf_Double
  alignOf = alignOf{ty=Int}
  unsafeLoad o p = primIO $ prim__foreignRef_Double p (cast o)
  unsafeStore o v p = primIO $ prim__foreignSet_Double p (cast o) v

public export
Storable Bits8 where
  sizeOf = 1
  alignOf = 1
  unsafeLoad o p = primIO $ prim__foreignRef_U8 p (cast o)
  unsafeStore o v p = primIO $ prim__foreignSet_U8 p (cast o) v

public export
Storable Bits16 where
  sizeOf = 2
  alignOf = 2
  unsafeLoad o p = primIO $ prim__foreignRef_U16 p (cast o)
  unsafeStore o v p = primIO $ prim__foreignSet_U16 p (cast o) v

public export
Storable Bits32 where
  sizeOf = 4
  alignOf = 4
  unsafeLoad o p = primIO $ prim__foreignRef_U32 p (cast o)
  unsafeStore o v p = primIO $ prim__foreignSet_U32 p (cast o) v

public export
Storable Bits64 where
  sizeOf = 8
  alignOf = 8
  unsafeLoad o p = primIO $ prim__foreignRef_U64 p (cast o)
  unsafeStore o v p = primIO $ prim__foreignSet_U64 p (cast o) v

public export
Storable AnyPtr where
  sizeOf = fromInteger $ cast {to=Integer} prim__foreignSizeOf_Ptr
  alignOf = fromInteger $ cast {to=Integer} prim__foreignSizeOf_Ptr
  unsafeLoad o p = primIO $ prim__foreignRef_Ptr (prim__forgetPtr p) (cast o)
  unsafeStore o v p = primIO $ prim__foreignSet_Ptr (prim__forgetPtr p) (cast o) v

public export
Storable (Ptr a) where
  sizeOf = fromInteger $ cast {to=Integer} prim__foreignSizeOf_Ptr
  alignOf = fromInteger $ cast {to=Integer} prim__foreignSizeOf_Ptr
  unsafeLoad o p =
    pure prim__castPtr <*> primIO (prim__foreignRef_Ptr (prim__forgetPtr p) (cast o))
  unsafeStore o v p =
    primIO $ prim__foreignSet_Ptr (prim__forgetPtr p) (cast o) (prim__forgetPtr v)

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


text:
module Dart.FFI.Elab

import public Dart.FFI.Elab.Dsl
import public Dart.FFI.Elab.Implementation
import public Dart.FFI.Elab.Types


text:
module Data.Optics.Prism

||| Prism
data Prism s a =
  MkPrism (s -> Maybe a)  (a -> s)

%name Prism prism, prism1, prism2

%default total

to : Prism s a -> (s -> Maybe a)
to (MkPrism f g) s = f s

from: Prism s a -> (a -> s)
from (MkPrism f g) a = g a

infixr 9 <:+
||| compose two prisms
(<:+) : Prism a b -> Prism s a -> Prism s b
p1 <:+ p2 = MkPrism newTo newFrom
  where
    newTo: s -> Maybe b
    newTo s = case (to p2 s) of
              Nothing => Nothing
              Just a  => (to p1 a)
    newFrom: b -> s
    newFrom = with Prelude.Basics (from p2 . from p1)

infixr 9 :+>
(:+>) : Prism s a -> Prism a b -> Prism s b
(:+>) = flip (<:+)

--
-- Functions
--

||| focus on the left of an Either
left: Prism (Either a b) a
left = MkPrism to from
  where
    to: (Either a b) -> Maybe a
    to (Left x) = Just x
    to (Right x) = Nothing

    from: a -> (Either a b)
    from x = Left x

||| focus on the right of an Either
right: Prism (Either a b) b
right = MkPrism to from
  where
    to : Either a b -> Maybe b
    to (Left x) = Nothing
    to (Right x) = Just x

    from: b -> Either a b
    from x = Right x

||| focus on Just of a Maybe
just: Prism (Maybe a) a
just = MkPrism to from
  where
    to: Maybe a -> Maybe a
    to Nothing = Nothing
    to (Just x) = Just x

    from: a -> Maybe a
    from x = Just x

max_stars_repo_name: justjoheinz/idris-optics

max_issues_repo_name: justjoheinz/idris-optics

max_forks_repo_name: justjoheinz/idris-optics


text:
module Data.Profunctor.Morphism

import public Data.Morphisms
import Data.Profunctor
import Data.Profunctor.Choice

public export
by : (Morphism a b -> Morphism c d) -> (a -> b) -> (c -> d)
by f = applyMor . f . Mor

export
Profunctor Morphism where
  lmap pre  = Mor . (. pre) . applyMor
  rmap post = Mor . (post .) . applyMor

export
Choice Morphism where
  right' = Mor . map . applyMor


text:
module AssRecRule

import Data.Fin
import Data.Vect

{-
 The recursion function for lists of type `a`. Define this by pattern matching
-}
recList : (a: Type) ->  (x: Type) -> x -> (a -> List a -> x -> x) -> (List a -> x)
recList a x y f [] = y
recList a x y f (z :: xs) = f z xs (recList a x y f xs)

{-
Given a list of type `a` and a function `f: a -> b` get a list of type `b`
by applying `f` to each element.
Note: Define using `recList` and without pattern matching on lists.
-}
mapList : (a: Type) -> (b: Type) -> (f: a -> b) -> List a -> List b
mapList a b f xs = recList a (List b) [] g xs where
  g: a -> List a -> List b -> List b
  g x l m = (f x) :: m

{-
Given a list of type `a`, an initial value `init: a` and an operation `op: a -> a -> a`,
get an element of `a` by starting with init and repeatedly applying the elements of the
list,
e.g. fold Nat 1 (*) ([22] :: [3] :: [])  = 1 * 22 * 3
Note: Define using `recList` and without pattern matching on lists.
(op(22,op(3,1))) is the output here
-}
foldList : (a: Type) ->  (init: a) -> (op : a -> a -> a) -> List a -> a
foldList a init op xs = recList a a init g xs where
  g: a -> List a -> a -> a
  g x l y = op x y

{-
The induction function on the `Fin` indexed type family. Define this by pattern matching.
-}
inducFin : (xs : (n: Nat) -> Fin n -> Type) ->
  (base : (m: Nat) -> xs (S m) FZ) ->
  (step : (p: Nat) -> (k: Fin p) ->  (prev: xs p k) -> (xs (S p) (FS k))) ->
  (q: Nat) -> (j: Fin q) -> xs q j
inducFin xs base step (S k) FZ = base k
inducFin xs base step (S k) (FS x) = step k x (inducFin xs base step k x)

{-
Given a type `a`, a natural number `q`, an element `j : Fin q` and a vector `v` of length q with entries of type `a`,
get the element in position `j` of `v`. Note that this is always well defined.

Note: Define using `inducList` and without pattern matching on the `Fin` family. You may pattern match on Vectors.
The definition should have only one case, and there should be no case splitting on `Fin`.
-}
fetchElem : (a: Type) -> (q: Nat) -> (j: Fin q) -> (Vect q a -> a)
fetchElem a q j ys = inducFin xs base step q j ys where
  xs: (n: Nat) -> Fin n -> Type
  xs n j = Vect n a -> a
  base: (m: Nat) -> xs (S m) FZ
  base m = f where
    f: Vect (S m) a -> a
    f (x :: xs) = x
  step: (p: Nat) -> (k: Fin p) ->  (prev: xs p k) -> (xs (S p) (FS k))
  step p k prev = g where
    g: Vect (S p) a -> a
    g (x :: xs) = prev xs


text:
||| Test if :typeat can report the type of variables in interface definitions
||| and implementations

interface Nattable a where
  toNat : a -> Nat

Nattable Bool where
  -- Create some variables just to test
  toNat True  = let x = 0 in S x
  toNat False = let y = 0 in y


text:
= Data.Ix

> ||| A partial port of Haskell's Data.Ix to Idris.
> module Data.Ix
>
> import Debug.Error
>
> %language ElabReflection

== Errors

> %access export
>
> indexError : Show a => (a,a) -> a -> String -> b
> indexError rng i tp =
>     error $ "Ix{" ++ show tp ++ "}.index: Index " ++
>             "(" ++ show i ++ ") out of range " ++
>             "(" ++ show rng ++ ")"
>
> hopelessIndexError : Int         -- Try to use 'indexError' instead!
> hopelessIndexError = error "Error in array index"

== Interface

> %access public export
>
> interface (Ord a) => Ix a where
>   range                   : (a,a) -> List a
>   index                   : (a,a) -> a -> Int
>   unsafeIndex             : (a,a) -> a -> Int
>   inRange                 : (a,a) -> a -> Bool
>   rangeSize               : (a,a) -> Int
>   unsafeRangeSize         : (a,a) -> Int
>
>   index b i               = if inRange b i
>                                then unsafeIndex b i
>                                else hopelessIndexError
>
>   unsafeIndex b i         = index b i
>
>   rangeSize b@(_,h)       = if inRange b h
>                                then unsafeIndex b h + 1
>                                else 0   -- This case is only here to
>                                         -- check for an empty range
>
>   unsafeRangeSize b@(_,h) = unsafeIndex b h + 1

== Implementations

> implementation Ix Nat where
>   range (m,n)             = [m .. n]
>   unsafeIndex (m,_) i     = cast $ i `minus` m
>   index b i               = if inRange b i
>                                then unsafeIndex b i
>                                else indexError b i "Nat"
>   inRange (m,n) i         = m <= i && i <= n

ext: lidr

max_stars_repo_name: yurrriq/advent-of-code


text:
module Main

import Interp
import Ast
import Examples
import Data.List

%default partial

nil : Term
nil = Comp "nil" []

cons : Term -> Term -> Term
cons head tail = Comp "cons" [head, tail]

append : Term -> Term -> Term -> Term
append xs ys res = Comp "append" [xs, ys, res]

Xs : Term
Xs = Var "Xs"

Y : Term
Y = Var "Y"

Ys : Term
Ys = Var "Ys"

Rec : Term
Rec = Var "Rec"

program2 : Program
program2 = unDSL
  [ append nil Ys Ys
  , append (cons X Xs) Ys (cons X Rec) :- [append Xs Ys Rec]
  ]

-- Some tests
main : IO ()
main = do
  putStrLn "\n--------------- append empty right"
  print $ (nub $ bfs $ makeReportTree program2 [append (cons X nil) nil Rec])
  putStrLn "\n--------------- append empty left"
  print $ (nub $ bfs $ makeReportTree program2 [append nil Xs Rec])
  putStrLn "\n--------------- append example"
  printLn $ (nub $ bfs $ makeReportTree program2 [append (cons X nil) (cons Y (cons p nil)) Rec])


text:
-- examples in "Type-Driven Development with Idris"
-- chapter 10

import Data.Vect
import Data.List.Views
import Data.Vect.Views
import Data.Nat.Views

-- check that all functions are total
%default total

--
-- section 10.1
--

-- first a function using a view, without `with`
-- we have:
-- - a view V : Tin -> Type
-- - a covering function covV : (x : Tin) -> V x
-- - a helper fHelp : (x : Tin) -> (form : V x) -> Tout
-- - the function f : Tin -> Tout, with f in = fHelp in (covV in)

||| A view
data ListLast : List a -> Type where
  Empty : ListLast []
  NonEmpty : (xs : List a) -> (x : a) -> ListLast (xs ++ [x])

||| The covering function of the ListLast view
listLast : (xs : List a) -> ListLast xs
listLast [] = Empty
listLast (x :: xs) = case listLast xs of
                          Empty => NonEmpty [] x
                          (NonEmpty ys y) => NonEmpty (x :: ys) y

||| The helper of the function, defined in terms of the view
describeHelperInt : (input : List Int) -> (form : ListLast input) -> String
describeHelperInt [] Empty = "Empty"
describeHelperInt (xs ++ [x]) (NonEmpty xs x)
  = "Non-empty, initial portion = " ++ show xs

||| generalized version of the helper (from Int to a)
describeHelper : Show a => (input : List a) -> (form : ListLast input) -> String
describeHelper [] Empty = "Empty"
describeHelper (xs ++ [x]) (NonEmpty xs x)
  = "Non-empty, initial portion = " ++ show xs

||| The function using the view
describeListEndInt : List Int -> String
describeListEndInt xs = describeHelperInt xs (listLast xs)

||| generalized version of the helper (from Int to a)
describeListEnd : Show a => List a -> String
describeListEnd xs = describeHelper xs (listLast xs)

-- ok:
-- > describeListEndInt [1,2,3]
-- "Non-empty, initial portion = [1, 2]" : String
-- > describeListEndInt [1]
-- "Non-empty, initial portion = []" : String
-- > describeListEndInt []
-- "Empty" : String
-- > describeListEnd [1,2,3]
-- "Non-empty, initial portion = [1, 2]" : String
-- > describeListEnd [1]
-- "Non-empty, initial portion = []" : String
-- > describeListEnd $ the (List Int) []
-- "Empty" : String
-- if a is not known:
-- > describeListEnd []
-- Can't find implementation for Show a

-- a version with `with`
-- we have:
-- - a view V : Tin -> Type
-- - a covering function covV : (x : Tin) -> V x
-- - the function f : Tin -> Tout, using the "with covV" construct

describeListEnd2 : List Int -> String
describeListEnd2 xs with (listLast xs)
  describeListEnd2 [] | Empty = "Empty"
  describeListEnd2 (ys ++ [x]) | (NonEmpty ys x)
    = "Non-empty, initial portion = " ++ show ys

partial
myReversePartial : List Int -> List Int
myReversePartial xs with (listLast xs)
  myReversePartial [] | Empty = []
  myReversePartial (ys ++ [x]) | (NonEmpty ys x) = x :: myReversePartial ys

data SplitList : List a -> Type where
  SplitNil : SplitList []
  SplitOne : SplitList [x]
  SplitPair : (lefts : List a) -> (rights : List a) -> SplitList (lefts ++ pairs)

splitList : (input : List a) -> SplitList input
splitList input = splitListHelper input input
  where
    splitListHelper : List a -> (input : List a) -> SplitList input
    splitListHelper _ [] = SplitNil
    splitListHelper _ [x] = SplitOne
    splitListHelper (_ :: _ :: counter) (item :: items)
      = case splitListHelper counter items of
         SplitNil => SplitOne
         SplitOne {x} => SplitPair [item] [x]
         SplitPair lefts rights => SplitPair (item :: lefts) rights
    splitListHelper _ items = SplitPair [] items

partial
mergeSort : Ord a => List a -> List a
mergeSort xs with (splitList xs)
  mergeSort [] | SplitNil = []
  mergeSort [x] | SplitOne = [x]
  mergeSort (lefts ++ pairs) | (SplitPair lefts rights)
    = merge (mergeSort lefts) (mergeSort rights)

--
-- section 10.2
--

data SnocList0 ty = SnocEmpty0 | Snoc0 (SnocList0 ty) ty

reverseSnoc0 : SnocList0 ty -> List ty
reverseSnoc0 SnocEmpty0 = []
reverseSnoc0 (Snoc0 xs x) = x :: reverseSnoc0 xs

data MySnocList : List a -> Type where
  MySnocEmpty : MySnocList []
  MySnoc : (rec : MySnocList xs) -> MySnocList (xs ++ [x])

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

mySnocList : (xs : List a) -> MySnocList xs
mySnocList xs = snocListHelp MySnocEmpty xs

myReverseHelper : (input : List a) -> MySnocList input -> List a
myReverseHelper [] MySnocEmpty = []
myReverseHelper (xs ++ [x]) (MySnoc rec) = myReverseHelper xs rec

myReverse : List a -> List a
myReverse input with (mySnocList input)
  myReverse [] | MySnocEmpty = []
  myReverse (xs ++ [x]) | (MySnoc rec) = x :: myReverse xs | rec

isSuffix : Eq a => List a -> List a -> Bool
isSuffix input1 input2 with (mySnocList input1)
  isSuffix [] input2 | MySnocEmpty = True
  isSuffix (xs ++ [x]) input2 | (MySnoc xsrec) with (mySnocList input2)
    isSuffix (xs ++ [x]) [] | (MySnoc xsrec) | MySnocEmpty = False
    isSuffix (xs ++ [x]) (ys ++ [y]) | (MySnoc xsrec) | (MySnoc ysrec)
      = if x == y then isSuffix xs ys | xsrec | ysrec
                  else False

mergeSort2 : Ord a => List a -> List a
mergeSort2 input with (splitRec input)
  mergeSort2 [] | SplitRecNil = []
  mergeSort2 [x] | SplitRecOne = [x]
  mergeSort2 (lefts ++ rights) | (SplitRecPair lrec rrec)
    = merge (mergeSort lefts | lrec)
            (mergeSort rights | rrec)


text:
double : Num a => a -> a
double x = x * x

twice : (a -> a) -> a -> a
twice f x = f (f x)

quadruple : Num a => a -> a
quadruple = twice double

max_stars_repo_name: wdomitrz/Coq-Exercises

max_issues_repo_name: wdomitrz/Coq-Exercises

max_forks_repo_name: wdomitrz/Coq-Exercises


text:
module Control.Effect.Lift

import Control.EffectAlgebra

namespace Algebra
  public export
  [Lift] Monad m => Algebra (Lift m) m where
    alg ctxx hdl (MkLift x) = x >>= hdl . ( <$ ctxx)

  %hint public export
  HintLift : Monad m => Algebra (Lift m) m
  HintLift = Lift

||| Lift a computation to the underlying effect stack.
public export
lift : Monad n => Inj (Lift n) sig => Algebra sig m => n a -> m a
lift x = send {eff = Lift n} $ MkLift (map pure x)


text:
module Python.IO

import Python.Objects

%default total
%access public export

unRaw : FFI_C.Raw a -> a
unRaw (MkRaw x) = x

||| Supported Python foreign types.
data PyTypes : Type -> Type where

  -- Primitive types
  PyInt_io     : PyTypes Int
  PyNat_io     : PyTypes Nat
  PyInteger_io : PyTypes Integer
  PyDouble_io   : PyTypes Double
  PyBool_io    : PyTypes Bool
  PyChar_io    : PyTypes Char
  PyString_io  : PyTypes String

  -- Other types
  PyUnit_io  : PyTypes ()
  PyPair_io  : PyTypes a -> PyTypes b -> PyTypes (a, b)
  PyList_io  : PyTypes a -> PyTypes (List a)
  PyFun_io   : PyTypes a -> PyTypes b -> PyTypes (a -> b)
  PyMaybe_io : PyTypes a -> PyTypes (Maybe a)

  ||| Python objects, opaque to Idris.
  PyPtr_io       : PyTypes Ptr

  ||| Arbitrary Idris objects, opaque to Python.
  PyAny_io : PyTypes (FFI_C.Raw a)

  ||| Python objects with a signature known to Idris.
  PyObj_io : PyTypes (Obj sig)

FFI_Py : FFI
FFI_Py = MkFFI PyTypes String String

||| Python IO. Read "pie-oh".
PIO : Type -> Type
PIO = IO' FFI_Py

max_stars_repo_name: ziman/idris-py

max_issues_repo_name: ziman/idris-py

max_forks_repo_name: ziman/idris-py


text:
-- Prototype of RealizedFunction as described in
-- https://blog.singularitynet.io/ai-dsl-toward-a-general-purpose-description-language-for-ai-agents-21459f691b9e

module RealizedFunction

-- NEXT: used dependent types to type check attributes in realized
-- function, take inspiration from NonDTRealizedFunction.idr and
-- SimpleRealizedFunction.idr