text:
module Control.Linear.LIO

||| Like `Monad`, but the action and continuation must be run exactly once
||| to ensure that the computation is linear.
public export
interface LinearBind io where
  bindL : (1 _ : io a) -> (1 _ : a -> io b) -> io b

export
LinearBind IO where
  bindL = io_bind

||| Required usage on the result value of a computation
public export
data Usage = None | Linear | Unrestricted

-- Not sure about this, it is a horrible hack, but it makes the notation
-- a bit nicer
public export
fromInteger : (x : Integer) -> {auto _ : Either (x = 0) (x = 1)} -> Usage
fromInteger 0 = None
fromInteger 1 = Linear
fromInteger x = Unrestricted

public export
0 ContType : (Type -> Type) -> Usage -> Usage -> Type -> Type -> Type

||| A wrapper which allows operations to state the multiplicity of the value
||| they return. For example, `L IO {use=1} File` is an IO operation which
||| returns a file that must be used exactly once.
-- This is uglier than I'd like. Perhaps multiplicity polymorphism would make
-- it neater, but we don't have that (yet?), and fortunately none of this
-- horror has to be exposed to the user!
export
data L : (io : Type -> Type) ->
         {default Unrestricted use : Usage} ->
         (ty : Type) -> Type where
     [search ty]
     -- Three separate Pures, because we need to distinguish how they are
     -- used, and this is neater than a continuation.
     Pure0 : (0 _ : a) -> L io {use=0} a
     Pure1 : (1 _ : a) -> L io {use=1} a
     PureW : a -> L io a
     -- The action is always run once, and the type makes an assertion about
     -- how often it's safe to use the result.
     Action : (1 _ : io a) -> L io {use} a
     Bind : {u_act : _} ->
            (1 _ : L io {use=u_act} a) ->
            (1 _ : ContType io u_act u_k a b) ->
            L io {use=u_k} b

public export
L0 : (io : Type -> Type) -> (ty : Type) -> Type
L0 io ty = L io {use = 0} ty

public export
L1 : (io : Type -> Type) -> (ty : Type) -> Type
L1 io ty = L io {use = 1} ty

ContType io None u_k a b = (0 _ : a) -> L io {use=u_k} b
ContType io Linear u_k a b = (1 _ : a) -> L io {use=u_k} b
ContType io Unrestricted u_k a b = a -> L io {use=u_k} b

RunCont : Usage -> Type -> Type -> Type
RunCont None t b = (0 _ : t) -> b
RunCont Linear t b = (1 _ : t) -> b
RunCont Unrestricted t b = t -> b

-- The repetition here is annoying, but necessary because we don't have
-- multiplicity polymorphism. We need to look at the usage to know what the
-- concrete type of the continuation is.
runK : {use : _} ->
       LinearBind io =>
       (1 _ : L io {use} a) -> (1 _ : RunCont use a (io b)) -> io b
runK (Pure0 x) k = k x
runK (Pure1 x) k = k x
runK (PureW x) k = k x
runK {use = None} (Action x) k = bindL x $ \x' => k x'
runK {use = Linear} (Action x) k = bindL x $ \x' => k x'
runK {use = Unrestricted} (Action x) k = bindL x $ \x' => k x'
runK (Bind {u_act = None} act next) k = runK act (\x => runK (next x) k)
runK (Bind {u_act = Linear} act next) k = runK act (\x => runK (next x) k)
runK (Bind {u_act = Unrestricted} act next) k = runK act (\x => runK (next x) k)

||| Run a linear program exactly once, with unrestricted return value in the
||| underlying context
export
run : (Applicative io, LinearBind io) =>
      (1 _ : L io a) -> io a
run prog = runK prog pure

export
Functor io => Functor (L io) where
  map fn act = Bind act $ \a' => PureW (fn a')

export
Applicative io => Applicative (L io) where
  pure = PureW
  (<*>) f a
      = f `Bind` \f' =>
        a `Bind` \a' =>
        PureW (f' a')

export
(Applicative m, LinearBind m) => Monad (L m) where
  (>>=) a k = Bind a k

-- prioritise this one for concrete LIO, so we get the most useful
-- linearity annotations.
export %inline
(>>=) : {u_act : _} ->
        LinearBind io =>
        (1 _ : L io {use=u_act} a) ->
        (1 _ : ContType io u_act u_k a b) -> L io {use=u_k} b
(>>=) = Bind

export
delay : {u_act : _} -> (1 _ : L io {use=u_k} b) -> ContType io u_act u_k () b
delay mb = case u_act of
  None => \ _ => mb
  Linear => \ () => mb
  Unrestricted => \ _ => mb

export %inline
(>>) : {u_act : _} ->
        LinearBind io =>
        (1 _ : L io {use=u_act} ()) ->
        (1 _ : L io {use=u_k} b) -> L io {use=u_k} b
ma >> mb = ma >>= delay mb

export %inline
pure0 : (0 x : a) -> L io {use=0} a
pure0 = Pure0

export %inline
pure1 : (1 x : a) -> L io {use=1} a
pure1 = Pure1

export
(LinearBind io, HasLinearIO io) => HasLinearIO (L io) where
  liftIO1 p = Action (liftIO1 p)

public export
LinearIO : (Type -> Type) -> Type
LinearIO io = (LinearBind io, HasLinearIO io)


text:
module Main

import System.IO.Terminal as Terminal

%default total

partial main : IO ()
main = do
  True <- Terminal.setup
          | _ => Prelude.putStrLn "Init failed."
  Terminal.getScreenSize >>= Terminal.putStrLn . show
  Terminal.putStr "01234567890"
  Terminal.putStrLn "ABCDEFGHIJKL"
  s <- Terminal.getLine
  Terminal.putStrLn $ "It's \"" ++ show s ++ "\""

ext: idr


text:
module GRIN.Var

import Control.Monad.State
import Data.SortedMap

import GRIN.GrinM
import GRIN.AST

public export
interface Monad m => MonadVar m where
    putVars : SortedMap Var Var -> m ()
    getVars : m (SortedMap Var Var)
    updateVar : Var -> m Var

export
resetVars : MonadVar m => m ()
resetVars = putVars empty

public export
record VarState where
    constructor MkVS
    varMap : SortedMap Var Var
    nextVar : Var

public export
VarM : Type -> Type
VarM = State VarState

export
MonadVar VarM where
    putVars vm = modify $ record { varMap = vm }
    getVars = gets varMap
    updateVar v = do
        vm <- gets varMap
        case lookup v vm of
            Just v' => pure v'
            Nothing => do
                v' <- gets nextVar
                modify $ record { varMap $= insert v v', nextVar $= incVar }
                pure v'

export
Monad m => MonadVar (GrinT name m) where
    putVars vm = modify $ record { varMap = vm }
    getVars = gets varMap
    updateVar v = do
        vm <- gets varMap
        case lookup v vm of
            Just v' => pure v'
            Nothing => do
                v' <- gets nextVar
                modify $ record { varMap $= insert v v', nextVar $= incVar }
                pure v'
      where
        newVar : GrinT name m Var
        newVar = do
            v <- gets nextVar
            modify $ record { nextVar $= incVar }
            pure v

||| Interface for types that contains `Var`s.
public export
interface HasVars a where
    updateVars : MonadVar m => a -> m a

export
HasVars Var where
    updateVars = updateVar

export
HasVars SVal where
    updateVars (SVar v) = SVar <$> updateVar v
    updateVars v = pure v

export
HasVars (Val name) where
    updateVars (SimpleVal v) = SimpleVal <$> updateVars v
    updateVars (ConstTagNode tag vs) = ConstTagNode tag <$> traverse updateVars vs
    updateVars (ConstTag tag) = pure $ ConstTag tag
    updateVars (VarTagNode v vs) = VarTagNode <$> updateVar v <*> traverse updateVars vs
    updateVars VUnit = pure VUnit

export
HasVars (CasePat name) where
    updateVars (NodePat tag vs) = NodePat tag <$> traverse updateVar vs
    updateVars (TagPat tag) = pure $ TagPat tag
    updateVars (LitPat l) = pure $ LitPat l
    updateVars DefaultPat = pure DefaultPat

mutual
    export
    HasVars (SExp name) where
        updateVars (Do e) = mkDo <$> updateVars e
        updateVars (App fn vs) = App fn <$> traverse updateVars vs
        updateVars (Pure v) = Pure <$> updateVars v
        updateVars (Store v) = Store <$> updateVars v
        updateVars (Fetch i v) = Fetch i <$> updateVar v
        updateVars (FetchI i idx v) = FetchI i idx <$> updateVar v
        updateVars (Update var val) = Update <$> updateVar var <*> updateVars val

    export
    HasVars (Exp name) where
        updateVars (SimpleExp e) = mkSimpleExp <$> updateVars e
        updateVars (Bind val rhs rest) = Bind <$> updateVars val <*> updateVars rhs <*> updateVars rest
        updateVars (Case val alts) = Case <$> updateVars val <*> traverse updateVars alts

    export
    HasVars (Alt name) where
        updateVars (MkAlt pat e) = MkAlt <$> updateVars pat <*> updateVars e

export
HasVars (Def name) where
    updateVars (MkDef fn vs e ty) =
        MkDef
            fn
            <$> traverse updateVar vs
            <*> updateVars e
            <*> pure ty

export
HasVars (Prog name) where
    updateVars (MkProg es ds m) = MkProg es <$> traverse updateVars ds <*> pure m


text:
module Main

total
T : Type -> Type
T a = a -> a

f : String -> { ty : Type } -> { auto prf : ty } -> ty
f n a = a

g : { ty : Type } -> T ty
g { ty } = f "what" { ty = (T ty) }

max_stars_repo_name: ostera/asdf

max_issues_repo_name: ostera/asdf

max_forks_repo_name: ostera/asdf


text:
module TTImp.PartialEval

import Core.CaseTree
import Core.Context
import Core.Context.Log
import Core.Core
import Core.Env
import Core.Hash
import Core.Metadata
import Core.Normalise
import Core.Value
import Core.UnifyState

import TTImp.Elab.Check
import TTImp.TTImp
import TTImp.TTImp.Functor
import TTImp.Unelab

import Libraries.Utils.Hex

import Data.List
import Libraries.Data.NameMap

%default covering

data ArgMode = Static ClosedTerm | Dynamic

Show ArgMode where
  show (Static tm) = "Static " ++ show tm
  show Dynamic = "Dynamic"

getStatic : ArgMode -> Maybe (Term [])
getStatic Dynamic = Nothing
getStatic (Static t) = Just t

specialiseTy : {vars : _} ->
               Nat -> List (Nat, Term []) -> Term vars -> Term vars
specialiseTy i specs (Bind fc x (Pi fc' c p ty) sc)
    = case lookup i specs of
           Nothing => Bind fc x (Pi fc' c Explicit ty) $ -- easier later if everything explicit
                        specialiseTy (1 + i) specs sc
           Just tm => specialiseTy (1 + i) specs (subst (embed tm) sc)
specialiseTy i specs tm = tm

substLoc : {vs : _} ->
           Nat -> Term vs -> Term vs -> Term vs
substLoc i tm (Local fc l idx p)
    = if i == idx then tm else (Local fc l idx p)
substLoc i tm (Bind fc x b sc)
    = Bind fc x (map (substLoc i tm) b) (substLoc (1 + i) (weaken tm) sc)
substLoc i tm (Meta fc n r args)
    = Meta fc n r (map (substLoc i tm) args)
substLoc i tm (App fc f a) = App fc (substLoc i tm f) (substLoc i tm a)
substLoc i tm (As fc s f a) = As fc s (substLoc i tm f) (substLoc i tm a)
substLoc i tm (TDelayed fc r d) = TDelayed fc r (substLoc i tm d)
substLoc i tm (TDelay fc r ty d) = TDelay fc r (substLoc i tm ty) (substLoc i tm d)
substLoc i tm (TForce fc r d) = TForce fc r (substLoc i tm d)
substLoc i tm x = x

substLocs : {vs : _} ->
            List (Nat, Term vs) -> Term vs -> Term vs
substLocs [] tm = tm
substLocs ((i, tm') :: subs) tm = substLocs subs (substLoc i tm' tm)

mkSubsts : Nat -> List (Nat, Term []) ->
           List (Term vs) -> Term vs -> Maybe (List (Nat, Term vs))
mkSubsts i specs [] rhs = Just []
mkSubsts i specs (arg :: args) rhs
    = do subs <- mkSubsts (1 + i) specs args rhs
         case lookup i specs of
              Nothing => Just subs
              Just tm => case arg of
                              Local _ _ idx _ =>
                                   Just ((idx, embed tm) :: subs)
                              As _ _ (Local _ _ idx1 _) (Local _ _ idx2 _) =>
                                   Just ((idx1, embed tm) :: (idx2, embed tm) :: subs)
                              As _ _ _ (Local _ _ idx _) =>
                                   Just ((idx, embed tm) :: subs)
                              _ => Nothing

-- In the case where all the specialised positions are variables on the LHS,
-- substitute the term in on the RHS
specPatByVar : List (Nat, Term []) ->
                (vs ** (Env Term vs, Term vs, Term vs)) ->
                Maybe (vs ** (Env Term vs, Term vs, Term vs))
specPatByVar specs (vs ** (env, lhs, rhs))
    = do let (fn, args) = getFnArgs lhs
         psubs <- mkSubsts 0 specs args rhs
         let lhs' = apply (getLoc fn) fn args
         pure (vs ** (env, substLocs psubs lhs', substLocs psubs rhs))

specByVar : List (Nat, Term []) ->
            List (vs ** (Env Term vs, Term vs, Term vs)) ->
            Maybe (List (vs ** (Env Term vs, Term vs, Term vs)))
specByVar specs [] = pure []
specByVar specs (p :: ps)
    = do p' <- specPatByVar specs p
         ps' <- specByVar specs ps
         pure (p' :: ps')

dropSpec : Nat -> List (Nat, Term []) -> List a -> List a
dropSpec i sargs [] = []
dropSpec i sargs (x :: xs)
    = case lookup i sargs of
           Nothing => x :: dropSpec (1 + i) sargs xs
           Just _ => dropSpec (1 + i) sargs xs

getSpecPats : {auto c : Ref Ctxt Defs} ->
              FC -> Name ->
              (fn : Name) -> (stk : List (FC, Term vars)) ->
              NF [] -> -- Type of 'fn'
              List (Nat, ArgMode) -> -- All the arguments
              List (Nat, Term []) -> -- Just the static ones
              List (vs ** (Env Term vs, Term vs, Term vs)) ->
              Core (Maybe (List ImpClause))
getSpecPats fc pename fn stk fnty args sargs pats
   = do -- First, see if all the specialised positions are variables. If so,
        -- substitute the arguments directly into the RHS
        let Nothing = specByVar sargs pats
            | Just specpats =>
                   do ps <- traverse (unelabPat pename) specpats
                      pure (Just ps)
        -- Otherwise, build a new definition by taking the remaining arguments
        -- on the lhs, and using the specialised function application on the rhs.
        -- Then, this will get evaluated on elaboration.
        let dynnames = mkDynNames 0 args
        let lhs = apply (IVar fc pename) (map (IBindVar fc) dynnames)
        rhs <- mkRHSargs fnty (IVar fc fn) dynnames args
        pure (Just [PatClause fc lhs rhs])
  where
    mkDynNames : Int -> List (Nat, ArgMode) -> List String
    mkDynNames i [] = []
    mkDynNames i ((_, Dynamic) :: as)
        = ("_pe" ++ show i) :: mkDynNames (1 + i) as
    mkDynNames i (_ :: as) = mkDynNames i as

    -- Build a RHS from the type of the function to be specialised, the
    -- dynamic argument names, and the list of given arguments. We assume
    -- the latter two correspond appropriately.
    mkRHSargs : NF [] -> RawImp -> List String -> List (Nat, ArgMode) ->
                Core RawImp
    mkRHSargs (NBind _ x (Pi _ _ Explicit _) sc) app (a :: as) ((_, Dynamic) :: ds)
        = do defs <- get Ctxt
             sc' <- sc defs (toClosure defaultOpts [] (Erased fc False))
             mkRHSargs sc' (IApp fc app (IVar fc (UN $ Basic a))) as ds
    mkRHSargs (NBind _ x (Pi _ _ _ _) sc) app (a :: as) ((_, Dynamic) :: ds)
        = do defs <- get Ctxt
             sc' <- sc defs (toClosure defaultOpts [] (Erased fc False))
             mkRHSargs sc' (INamedApp fc app x (IVar fc (UN $ Basic a))) as ds
    mkRHSargs (NBind _ x (Pi _ _ Explicit _) sc) app as ((_, Static tm) :: ds)
        = do defs <- get Ctxt
             sc' <- sc defs (toClosure defaultOpts [] (Erased fc False))
             tm' <- unelabNoSugar [] tm
             mkRHSargs sc' (IApp fc app (map rawName tm')) as ds
    mkRHSargs (NBind _ x (Pi _ _ _ _) sc) app as ((_, Static tm) :: ds)
        = do defs <- get Ctxt
             sc' <- sc defs (toClosure defaultOpts [] (Erased fc False))
             tm' <- unelabNoSugar [] tm
             mkRHSargs sc' (INamedApp fc app x (map rawName tm')) as ds
    -- Type will depend on the value here (we assume a variadic function) but
    -- the argument names are still needed
    mkRHSargs ty app (a :: as) ((_, Dynamic) :: ds)
        = mkRHSargs ty (IApp fc app (IVar fc (UN $ Basic a))) as ds
    mkRHSargs _ app _ _
        = pure app

    getRawArgs : List (Maybe Name, RawImp) -> RawImp -> List (Maybe Name, RawImp)
    getRawArgs args (IApp _ f arg) = getRawArgs ((Nothing, arg) :: args) f
    getRawArgs args (INamedApp _ f n arg)
        = getRawArgs ((Just n, arg) :: args) f
    getRawArgs args tm = args

    reapply : RawImp -> List (Maybe Name, RawImp) -> RawImp
    reapply f [] = f
    reapply f ((Nothing, arg) :: args) = reapply (IApp fc f arg) args
    reapply f ((Just t, arg) :: args)
        = reapply (INamedApp fc f t arg) args

    dropArgs : Name -> RawImp -> RawImp
    dropArgs pename tm = reapply (IVar fc pename) (dropSpec 0 sargs (getRawArgs [] tm))

    unelabPat : Name -> (vs ** (Env Term vs, Term vs, Term vs)) ->
                Core ImpClause
    unelabPat pename (_ ** (env, lhs, rhs))
        = do lhsapp <- unelabNoSugar env lhs
             let lhs' = dropArgs pename (map rawName lhsapp)
             defs <- get Ctxt
             rhsnf <- normaliseArgHoles defs env rhs
             rhs' <- unelabNoSugar env rhsnf
             pure (PatClause fc lhs' (map rawName rhs'))

    unelabLHS : Name -> (vs ** (Env Term vs, Term vs, Term vs)) ->
                Core RawImp
    unelabLHS pename (_ ** (env, lhs, rhs))
        = do lhsapp <- unelabNoSugar env lhs
             pure $ dropArgs pename (map rawName lhsapp)

-- Get the reducible names in a function to be partially evaluated. In practice,
-- that's all the functions it refers to
-- TODO: May want to take care with 'partial' names?
getReducible : List Name -> -- calls to check
               NameMap Nat -> -- which nodes have been visited. If the entry is
                              -- present, it's visited
               Defs -> Core (NameMap Nat)
getReducible [] refs defs = pure refs
getReducible (n :: rest) refs defs
  = do let Nothing = lookup n refs
           | Just _ => getReducible rest refs defs
       case !(lookupCtxtExact n (gamma defs)) of
            Nothing => getReducible rest refs defs
            Just def =>
              do let refs' = insert n 65536 refs
                 let calls = refersTo def
                 getReducible (keys calls ++ rest) refs' defs

mkSpecDef : {auto c : Ref Ctxt Defs} ->
            {auto m : Ref MD Metadata} ->
            {auto u : Ref UST UState} ->
            FC -> GlobalDef ->
            Name -> List (Nat, ArgMode) -> Name -> List (FC, Term vars) ->
            Core (Term vars)
mkSpecDef {vars} fc gdef pename sargs fn stk
    = handleUnify
       (do defs <- get Ctxt
           setAllPublic True
           let staticargs
                 = mapMaybe (\ (x, s) => case s of
                                              Dynamic => Nothing
                                              Static t => Just (x, t)) sargs
           let peapp = applyWithFC (Ref fc Func pename) (dropSpec 0 staticargs stk)
           Nothing <- lookupCtxtExact pename (gamma defs)
               | Just _ => -- already specialised
                           do log "specialise" 5 $ "Already specialised " ++ show pename
                              pure peapp
           logC "specialise" 5 $
                   do fnfull <- toFullNames fn
                      args' <- traverse (\ (i, arg) =>
                                   do arg' <- the (Core ArgMode) $ case arg of
                                                   Static a =>
                                                      pure $ Static !(toFullNames a)
                                                   Dynamic => pure Dynamic
                                      pure (show (i, arg'))) sargs
                      pure $ "Specialising " ++ show fnfull ++
                             " (" ++ show fn ++ ") by " ++
                             showSep ", " args'
           let sty = specialiseTy 0 staticargs (type gdef)
           logTermNF "specialise" 3 ("Specialised type " ++ show pename) [] sty

           -- Add as RigW - if it's something else, we don't need it at
           -- runtime anyway so this is wasted effort, therefore a failure
           -- is okay!
           peidx <- addDef pename (newDef fc pename top [] sty Public None)
           addToSave (Resolved peidx)

           -- Reduce the function to be specialised, and reduce any name in
           -- the arguments at most once (so that recursive definitions aren't
           -- unfolded forever)
           let specnames = getAllRefs empty (map snd sargs)
           specLimits <- traverse (\n => pure (n, 1))
                                  (keys specnames)

           defs <- get Ctxt
           reds <- getReducible [fn] empty defs
           setFlag fc (Resolved peidx) (PartialEval (specLimits ++ toList reds))

           let PMDef pminfo pmargs ct tr pats = definition gdef
               | _ => pure (applyWithFC (Ref fc Func fn) stk)
           logC "specialise" 5 $
                   do inpats <- traverse unelabDef pats
                      pure $ "Attempting to specialise:\n" ++
                             showSep "\n" (map showPat inpats)

           Just newpats <- getSpecPats fc pename fn stk !(nf defs [] (type gdef))
                                       sargs staticargs pats
                | Nothing => pure (applyWithFC (Ref fc Func fn) stk)
           log "specialise" 5 $ "New patterns for " ++ show pename ++ ":\n" ++
                    showSep "\n" (map showPat newpats)
           processDecl [InPartialEval] (MkNested []) []
                       (IDef fc (Resolved peidx) newpats)
           setAllPublic False
           pure peapp)
           -- If the partially evaluated definition fails, just use the initial
           -- application. It might indicates a bug in the P.E. function generation
           -- if it fails, but I don't want the whole system to be dependent on
           -- the correctness of PE!
        (\err =>
           do log "specialise" 1 $ "Partial evaluation of " ++ show !(toFullNames fn) ++ " failed" ++
                      "\n" ++ show err
              defs <- get Ctxt
              put Ctxt (record { peFailures $= insert pename () } defs)
              pure (applyWithFC (Ref fc Func fn) stk))
  where
    getAllRefs : NameMap Bool -> List ArgMode -> NameMap Bool
    getAllRefs ns (Dynamic :: xs) = getAllRefs ns xs
    getAllRefs ns (Static t :: xs)
        = addRefs False (UN Underscore) (getAllRefs ns xs) t
    getAllRefs ns [] = ns

    updateApp : Name -> RawImp -> RawImp
    updateApp n (IApp fc f a) = IApp fc (updateApp n f) a
    updateApp n (IAutoApp fc f a) = IAutoApp fc (updateApp n f) a
    updateApp n (INamedApp fc f m a) = INamedApp fc (updateApp n f) m a
    updateApp n f = IVar fc n

    unelabDef : (vs ** (Env Term vs, Term vs, Term vs)) ->
                Core ImpClause
    unelabDef (_ ** (env, lhs, rhs))
        = do lhs' <- unelabNoSugar env lhs
             defs <- get Ctxt
             rhsnf <- normaliseArgHoles defs env rhs
             rhs' <- unelabNoSugar env rhsnf
             pure (PatClause fc (map rawName lhs') (map rawName rhs'))

    showPat : ImpClause -> String
    showPat (PatClause _ lhs rhs) = show lhs ++ " = " ++ show rhs
    showPat _ = "Can't happen"

eraseInferred : {auto c : Ref Ctxt Defs} ->
                Term vars -> Core (Term vars)
eraseInferred (Bind fc x b tm)
    = do b' <- traverse eraseInferred b
         tm' <- eraseInferred tm
         pure (Bind fc x b' tm')
eraseInferred tm
    = case getFnArgs tm of
           (f, []) => pure f
           (Ref fc Func n, args) =>
                do defs <- get Ctxt
                   Just gdef <- lookupCtxtExact n (gamma defs)
                        | Nothing => pure tm
                   let argsE = dropErased fc 0 (inferrable gdef) args
                   argsE' <- traverse eraseInferred argsE
                   pure (apply fc (Ref fc Func n) argsE')
           (f, args) =>
                do args' <- traverse eraseInferred args
                   pure (apply (getLoc f) f args)
  where
    dropErased : FC -> Nat -> List Nat -> List (Term vars) -> List (Term vars)
    dropErased fc pos ps [] = []
    dropErased fc pos ps (n :: ns)
        = if pos `elem` ps
             then Erased fc False :: dropErased fc (1 + pos) ps ns
             else n :: dropErased fc (1 + pos) ps ns

-- Specialise a function name according to arguments. Return the specialised
-- application on success, or Nothing if it's not specialisable (due to static
-- arguments not being concrete)
specialise : {vars : _} ->
             {auto c : Ref Ctxt Defs} ->
             {auto m : Ref MD Metadata} ->
             {auto u : Ref UST UState} ->
             FC -> Env Term vars -> GlobalDef ->
             Name -> List (FC, Term vars) ->
             Core (Maybe (Term vars))
specialise {vars} fc env gdef fn stk
    = case specArgs gdef of
        [] => pure Nothing
        specs =>
            do fnfull <- toFullNames fn
               -- If all the arguments are concrete (meaning, no local variables
               -- or holes in them, so they can be a Term []) we can specialise
               Just sargs <- getSpecArgs 0 specs stk
                   | Nothing => pure Nothing
               let nhash = hash (mapMaybe getStatic (map snd sargs))
                              `hashWithSalt` fn -- add function name to hash to avoid namespace clashes
               let pename = NS partialEvalNS
                            (UN $ Basic ("PE_" ++ nameRoot fnfull ++ "_" ++ asHex nhash))
               defs <- get Ctxt
               case lookup pename (peFailures defs) of
                    Nothing => Just <$> mkSpecDef fc gdef pename sargs fn stk
                    Just _ => pure Nothing
  where
    dropAll : {vs : _} -> SubVars [] vs
    dropAll {vs = []} = SubRefl
    dropAll {vs = v :: vs} = DropCons dropAll

    concrete : {vars : _} ->
               Term vars -> Maybe (Term [])
    concrete tm = shrinkTerm tm dropAll

    getSpecArgs : Nat -> List Nat -> List (FC, Term vars) ->
                  Core (Maybe (List (Nat, ArgMode)))
    getSpecArgs i specs [] = pure (Just [])
    getSpecArgs i specs ((_, x) :: xs)
        = do Just xs' <- getSpecArgs (1 + i) specs xs
                 | Nothing => pure Nothing
             if i `elem` specs
                then do defs <- get Ctxt
                        x' <- normaliseHoles defs env x
                        x' <- eraseInferred x'
                        let Just xok = concrete x'
                            | Nothing => pure Nothing
                        pure $ Just ((i, Static xok) :: xs')
                else pure $ Just ((i, Dynamic) :: xs')

findSpecs : {vars : _} ->
            {auto c : Ref Ctxt Defs} ->
            {auto m : Ref MD Metadata} ->
            {auto u : Ref UST UState} ->
            Env Term vars -> List (FC, Term vars) -> Term vars ->
            Core (Term vars)
findSpecs env stk (Ref fc Func fn)
    = do defs <- get Ctxt
         Just gdef <- lookupCtxtExact fn (gamma defs)
              | Nothing => pure (applyWithFC (Ref fc Func fn) stk)
         Just r <- specialise fc env gdef fn stk
              | Nothing => pure (applyWithFC (Ref fc Func fn) stk)
         pure r
findSpecs env stk (Meta fc n i args)
    = do args' <- traverse (findSpecs env []) args
         pure $ applyWithFC (Meta fc n i args') stk
findSpecs env stk (Bind fc x b sc)
    = do b' <- traverse (findSpecs env []) b
         sc' <- findSpecs (b' :: env) [] sc
         pure $ applyWithFC (Bind fc x b' sc') stk
findSpecs env stk (App fc fn arg)
    = do arg' <- findSpecs env [] arg
         findSpecs env ((fc, arg') :: stk) fn
findSpecs env stk (TDelayed fc r tm)
    = do tm' <- findSpecs env [] tm
         pure $ applyWithFC (TDelayed fc r tm') stk
findSpecs env stk (TDelay fc r ty tm)
    = do ty' <- findSpecs env [] ty
         tm' <- findSpecs env [] tm
         pure $ applyWithFC (TDelay fc r ty' tm') stk
findSpecs env stk (TForce fc r tm)
    = do tm' <- findSpecs env [] tm
         pure $ applyWithFC (TForce fc r tm') stk
findSpecs env stk tm = pure $ applyWithFC tm stk

bName : {auto q : Ref QVar Int} -> String -> Core Name
bName n
    = do i <- get QVar
         put QVar (i + 1)
         pure (MN n i)

-- This is like 'quote' in 'Normalise', except that when we encounter a
-- function name we need to check whether to specialise.
-- (Sorry about all the repetition - I don't really want to export those
-- internal details, and there is a small but crucial change where we call
-- quoteHead as compared with the version in Core.Normalise, to deal with
-- checking for specialised applications.)
mutual
  quoteArgs : {bound, free : _} ->
              {auto c : Ref Ctxt Defs} ->
              {auto m : Ref MD Metadata} ->
              {auto u : Ref UST UState} ->
              Ref QVar Int -> Defs -> Bounds bound ->
              Env Term free -> List (Closure free) ->
              Core (List (Term (bound ++ free)))
  quoteArgs q defs bounds env [] = pure []
  quoteArgs q defs bounds env (a :: args)
      = pure $ (!(quoteGenNF q defs bounds env !(evalClosure defs a)) ::
                !(quoteArgs q defs bounds env args))

  quoteArgsWithFC : {auto c : Ref Ctxt Defs} ->
                    {auto m : Ref MD Metadata} ->
                    {auto u : Ref UST UState} ->
                    {bound, free : _} ->
                    Ref QVar Int -> Defs -> Bounds bound ->
                    Env Term free -> List (FC, Closure free) ->
                    Core (List (FC, Term (bound ++ free)))
  quoteArgsWithFC q defs bounds env terms
      = pure $ zip (map fst terms) !(quoteArgs q defs bounds env (map snd terms))

  quoteHead : {bound, free : _} ->
              {auto c : Ref Ctxt Defs} ->
              {auto m : Ref MD Metadata} ->
              {auto u : Ref UST UState} ->
              Ref QVar Int -> Defs ->
              FC -> Bounds bound -> Env Term free -> NHead free ->
              Core (Term (bound ++ free))
  quoteHead {bound} q defs fc bounds env (NLocal mrig _ prf)
      = let MkVar prf' = addLater bound prf in
            pure $ Local fc mrig _ prf'
    where
      addLater : {idx : _} -> (ys : List Name) -> (0 p : IsVar n idx xs) ->
                 Var (ys ++ xs)
      addLater [] isv = MkVar isv
      addLater (x :: xs) isv
          = let MkVar isv' = addLater xs isv in
                MkVar (Later isv')
  quoteHead q defs fc bounds env (NRef Bound (MN n i))
      = case findName bounds of
             Just (MkVar p) => pure $ Local fc Nothing _ (varExtend p)
             Nothing => pure $ Ref fc Bound (MN n i)
    where
      findName : Bounds bound' -> Maybe (Var bound')
      findName None = Nothing
      findName (Add x (MN n' i') ns)
          = if i == i' -- this uniquely identifies it, given how we
                       -- generated the names, and is a faster test!
               then Just (MkVar First)
               else do MkVar p <-findName ns
                       Just (MkVar (Later p))
      findName (Add x _ ns)
          = do MkVar p <-findName ns
               Just (MkVar (Later p))
  quoteHead q defs fc bounds env (NRef nt n) = pure $ Ref fc nt n
  quoteHead q defs fc bounds env (NMeta n i args)
      = do args' <- quoteArgs q defs bounds env args
           pure $ Meta fc n i args'

  quotePi : {bound, free : _} ->
            {auto c : Ref Ctxt Defs} ->
            {auto m : Ref MD Metadata} ->
            {auto u : Ref UST UState} ->
            Ref QVar Int -> Defs -> Bounds bound ->
            Env Term free -> PiInfo (Closure free) ->
            Core (PiInfo (Term (bound ++ free)))
  quotePi q defs bounds env Explicit = pure Explicit
  quotePi q defs bounds env Implicit = pure Implicit
  quotePi q defs bounds env AutoImplicit = pure AutoImplicit
  quotePi q defs bounds env (DefImplicit t)
      = do t' <- quoteGenNF q defs bounds env !(evalClosure defs t)
           pure (DefImplicit t')

  quoteBinder : {bound, free : _} ->
                {auto c : Ref Ctxt Defs} ->
                {auto m : Ref MD Metadata} ->
                {auto u : Ref UST UState} ->
                Ref QVar Int -> Defs -> Bounds bound ->
                Env Term free -> Binder (Closure free) ->
                Core (Binder (Term (bound ++ free)))
  quoteBinder q defs bounds env (Lam fc r p ty)
      = do ty' <- quoteGenNF q defs bounds env !(evalClosure defs ty)
           p' <- quotePi q defs bounds env p
           pure (Lam fc r p' ty')
  quoteBinder q defs bounds env (Let fc r val ty)
      = do val' <- quoteGenNF q defs bounds env !(evalClosure defs val)
           ty' <- quoteGenNF q defs bounds env !(evalClosure defs ty)
           pure (Let fc r val' ty')
  quoteBinder q defs bounds env (Pi fc r p ty)
      = do ty' <- quoteGenNF q defs bounds env !(evalClosure defs ty)
           p' <- quotePi q defs bounds env p
           pure (Pi fc r p' ty')
  quoteBinder q defs bounds env (PVar fc r p ty)
      = do ty' <- quoteGenNF q defs bounds env !(evalClosure defs ty)
           p' <- quotePi q defs bounds env p
           pure (PVar fc r p' ty')
  quoteBinder q defs bounds env (PLet fc r val ty)
      = do val' <- quoteGenNF q defs bounds env !(evalClosure defs val)
           ty' <- quoteGenNF q defs bounds env !(evalClosure defs ty)
           pure (PLet fc r val' ty')
  quoteBinder q defs bounds env (PVTy fc r ty)
      = do ty' <- quoteGenNF q defs bounds env !(evalClosure defs ty)
           pure (PVTy fc r ty')

  quoteGenNF : {bound, vars : _} ->
               {auto c : Ref Ctxt Defs} ->
               {auto m : Ref MD Metadata} ->
               {auto u : Ref UST UState} ->
               Ref QVar Int ->
               Defs -> Bounds bound ->
               Env Term vars -> NF vars -> Core (Term (bound ++ vars))
  quoteGenNF q defs bound env (NBind fc n b sc)
      = do var <- bName "qv"
           sc' <- quoteGenNF q defs (Add n var bound) env
                       !(sc defs (toClosure defaultOpts env (Ref fc Bound var)))
           b' <- quoteBinder q defs bound env b
           pure (Bind fc n b' sc')
  -- IMPORTANT CASE HERE
  -- If fn is to be specialised, quote the args directly (no further
  -- reduction) then call specialise. Otherwise, quote as normal
  quoteGenNF q defs bound env (NApp fc (NRef Func fn) args)
      = do Just gdef <- lookupCtxtExact fn (gamma defs)
                | Nothing => do args' <- quoteArgsWithFC q defs bound env args
                                pure $ applyWithFC (Ref fc Func fn) args'
           case specArgs gdef of
                [] => do args' <- quoteArgsWithFC q defs bound env args
                         pure $ applyWithFC (Ref fc Func fn) args'
                _ => do empty <- clearDefs defs
                        args' <- quoteArgsWithFC q defs bound env args
                        Just r <- specialise fc (extendEnv bound env) gdef fn args'
                             | Nothing =>
                                  -- can't specialise, keep the arguments
                                  -- unreduced
                                  do args' <- quoteArgsWithFC q empty bound env args
                                     pure $ applyWithFC (Ref fc Func fn) args'
                        pure r
     where
       extendEnv : Bounds bs -> Env Term vs -> Env Term (bs ++ vs)
       extendEnv None env = env
       extendEnv (Add x n bs) env
           -- We're just using this to evaluate holes in the right scope, so
           -- a placeholder binder is fine
           = Lam fc top Explicit (Erased fc False) :: extendEnv bs env
  quoteGenNF q defs bound env (NApp fc f args)
      = do f' <- quoteHead q defs fc bound env f
           args' <- quoteArgsWithFC q defs bound env args
           pure $ applyWithFC f' args'
  quoteGenNF q defs bound env (NDCon fc n t ar args)
      = do args' <- quoteArgsWithFC q defs bound env args
           pure $ applyWithFC (Ref fc (DataCon t ar) n) args'
  quoteGenNF q defs bound env (NTCon fc n t ar args)
      = do args' <- quoteArgsWithFC q defs bound env args
           pure $ applyWithFC (Ref fc (TyCon t ar) n) args'
  quoteGenNF q defs bound env (NAs fc s n pat)
      = do n' <- quoteGenNF q defs bound env n
           pat' <- quoteGenNF q defs bound env pat
           pure (As fc s n' pat')
  quoteGenNF q defs bound env (NDelayed fc r arg)
      = do argQ <- quoteGenNF q defs bound env arg
           pure (TDelayed fc r argQ)
  quoteGenNF q defs bound env (NDelay fc r ty arg)
      -- unlike main evaluator, we want to look under Delays
      = do argNF <- evalClosure defs arg
           argQ <- quoteGenNF q defs bound env argNF
           tyNF <- evalClosure defs ty
           tyQ <- quoteGenNF q defs bound env tyNF
           pure (TDelay fc r tyQ argQ)
    where
      toHolesOnly : Closure vs -> Closure vs
      toHolesOnly (MkClosure _ locs env tm)
          = MkClosure withHoles locs env tm
      toHolesOnly c = c
  quoteGenNF q defs bound env (NForce fc r arg args)
      = do args' <- quoteArgsWithFC q defs bound env args
           case arg of
                NDelay fc _ _ arg =>
                   do argNF <- evalClosure defs arg
                      pure $ applyWithFC !(quoteGenNF q defs bound env argNF) args'
                _ => do arg' <- quoteGenNF q defs bound env arg
                        pure $ applyWithFC (TForce fc r arg') args'
  quoteGenNF q defs bound env (NPrimVal fc c) = pure $ PrimVal fc c
  quoteGenNF q defs bound env (NErased fc i) = pure $ Erased fc i
  quoteGenNF q defs bound env (NType fc) = pure $ TType fc

evalRHS : {vars : _} ->
          {auto c : Ref Ctxt Defs} ->
          {auto m : Ref MD Metadata} ->
          {auto u : Ref UST UState} ->
          Env Term vars -> NF vars -> Core (Term vars)
evalRHS env nf
    = do q <- newRef QVar 0
         defs <- get Ctxt
         quoteGenNF q defs None env nf

export
applySpecialise : {vars : _} ->
                  {auto c : Ref Ctxt Defs} ->
                  {auto m : Ref MD Metadata} ->
                  {auto u : Ref UST UState} ->
                  Env Term vars ->
                  Maybe (List (Name, Nat)) ->
                        -- ^ If we're specialising, names to reduce in the RHS
                        -- with their reduction limits
                  Term vars -> -- initial RHS
                  Core (Term vars)
applySpecialise env Nothing tm
    = findSpecs env [] tm -- not specialising, just search through RHS
applySpecialise env (Just ls) tmin -- specialising, evaluate RHS while looking
                                 -- for names to specialise
    = do defs <- get Ctxt
         tm <- toResolvedNames tmin
         nf <- nf defs env tm
         tm' <- evalRHS env nf
         tmfull <- toFullNames tm'
         logTermNF "specialise" 5 ("New RHS") env tmfull
         pure tmfull


text:
module Circuits.Common

import System

import Decidable.Equality

import Data.Nat
import Toolkit.Data.Whole

%default total

export
processArgs : List String -> IO String
processArgs [exe,fname] = pure fname
processArgs _
  = do putStrLn "Exactly one file at a time."
       exitFailure

public export
data DType = LOGIC | BVECT Whole DType

public export
size : DType -> Nat
size LOGIC = (S Z)
size (BVECT (W (S n) ItIsSucc) type)
  = mult (S n) (size type)

Uninhabited (LOGIC = BVECT n k) where
  uninhabited Refl impossible

export
DecEq DType where
  decEq LOGIC LOGIC = Yes Refl
  decEq LOGIC (BVECT k x) = No absurd

  decEq (BVECT k x) LOGIC = No (negEqSym absurd)
  decEq (BVECT k x) (BVECT j y) with (decEq k j)
    decEq (BVECT k x) (BVECT k y) | (Yes Refl) with (decEq x y)
      decEq (BVECT k x) (BVECT k x) | (Yes Refl) | (Yes Refl)
        = Yes Refl
      decEq (BVECT k x) (BVECT k y) | (Yes Refl) | (No contra)
        = No (\Refl => contra Refl)

    decEq (BVECT k x) (BVECT j y) | (No contra)
      = No (\Refl => contra Refl)

public export
data Usage = USED | FREE

Uninhabited (USED = FREE) where
  uninhabited Refl impossible

export
DecEq Usage where
  decEq USED USED = Yes Refl
  decEq USED FREE = No absurd
  decEq FREE USED = No (negEqSym absurd)
  decEq FREE FREE = Yes Refl

-- [ EOF ]

max_stars_repo_name: border-patrol/linear-circuits

max_issues_repo_name: border-patrol/linear-circuits

max_forks_repo_name: border-patrol/linear-circuits


text:
module Network.HTTP.Path

import Data.String
import Data.String.Extra
import Data.List1
import Data.List
import Generics.Derive

%language ElabReflection

data PathComponent : Type where
  Root : PathComponent
  Parent : PathComponent
  Current : PathComponent
  End : PathComponent
  Named : String -> PathComponent

%runElab derive "PathComponent" [Generic, Meta, Eq]

export
record Path where
  constructor MkPath
  components : List1 PathComponent

zip_with_last : List a -> List (a, Maybe a)
zip_with_last list =
  let (_ :: xs) = map Just list
  | [] => []
  in zip list (snoc xs Nothing)

export
normalize : Path -> Path
normalize path = decompose $ trim_root path.components where
  is_current : PathComponent -> Bool
  is_current Current = True
  is_current (Named "") = True
  is_current _ = False

  rid_current : List PathComponent -> List PathComponent
  rid_current components = filter (not . is_current) components

  rid_parent : List PathComponent -> List PathComponent -> List PathComponent
  rid_parent acc [] = reverse acc
  rid_parent acc@(Parent :: as) (Parent :: xs) = rid_parent (Parent :: acc) xs
  rid_parent acc@(Root :: as) (Parent :: xs) = rid_parent acc xs
  rid_parent (a :: as) (Parent :: xs) = rid_parent as xs
  rid_parent acc (x :: xs) = rid_parent (x :: acc) xs

  append_current : List PathComponent -> List1 PathComponent
  append_current (Named x :: xs) = Current ::: (Named x :: xs)
  append_current [] = Current ::: []
  append_current (x :: xs) = (x ::: xs)

  decompose : List1 PathComponent -> Path
  decompose (x ::: xs) = MkPath $ append_current $ rid_parent [] (x :: rid_current xs)

  trim_root : List1 PathComponent -> List1 PathComponent
  trim_root list = case dropWhile (/= Root) $ forget list of [] => list; (x :: xs) => x ::: xs

concat : List a -> List1 a -> List1 a
concat [] y = y
concat (x :: xs) (y ::: ys) = x ::: (xs <+> (y :: ys))

export
Semigroup Path where
  a <+> b =
    let as = (normalize a).components
        ai = init as
    in normalize $ MkPath $ concat ai (normalize b).components

export
Show Path where
  show path = trim_leading_roots $ join "/" $ map component_to_string path.components
    where
      trim_leading_roots : String -> String
      trim_leading_roots str = assert_total $ if isPrefixOf "//" str then strTail str else str

      component_to_string : PathComponent -> String
      component_to_string Root = "/"
      component_to_string End = "/"
      component_to_string Parent = ".."
      component_to_string Current = "."
      component_to_string (Named x) = x

export
FromString Path where
  fromString "" = MkPath $ singleton Current
  fromString string =
    MkPath $ case split ('/' ==) string of
      ("" ::: xs) => Root ::: (map string_to_component xs)
      (x ::: xs) => map string_to_component $ (x ::: xs)
  where
    string_to_component : String -> PathComponent
    string_to_component "" = End
    string_to_component "." = Current
    string_to_component ".." = Parent
    string_to_component x = Named x


text:
-- Find the sum of all the multiples of 3 or 5 below 1000.

{- A more optimal solution would be to calulate the sum of numbers divisible by
 - 3 plus the numbers divisible by 5. This way you added multiples by 15 twice.
 -
 - Example:
 - 3 +  6 +  9 + ... + 999 = 3 * (1 + 2 + 3 + ... + 333)
 - 5 + 10 + 15 + ... + 199 = 5 * (1 + 2 + 3 + ... + 199)
 - 1 +  2 +  3 + ... +   n = (n * (n + 1)) / 2
 - -> for more info search for 'triangular number'.
 -}
sum' : Int -> Int -> Int
sum' n m = div (n * t * (t + 1)) 2 where
  t : Int
  t = div m n

main : IO ()
main = print ((sum' 3 999) + (sum' 5 999) - (sum' 15 999))

max_stars_repo_name: edu-di-wu/project-euler

max_issues_repo_name: edu-di-wu/project-euler

max_forks_repo_name: edu-di-wu/project-euler


text:
module Extra.Scientific

private
pow : Integer -> Integer -> Integer
pow a 0 = 1
pow a b = if b < 0 then 0 else a * pow a (b - 1)

private
bin10Index : Integer -> Integer
bin10Index n = helper 0
  where
  helper : Integer -> Integer
  helper a = if n < pow 10 a then a else helper (a + 1)

||| Scientific notation representation in the form of `coefficient*10^(exponentation)`
public export
data Scientific : Type where
  MkScientific : (coefficient : Integer) -> (exponentation : Integer) -> Scientific

export
Show Scientific where
  show (MkScientific m n) = show m <+> "e" <+> show n

export
Num Scientific where
  (MkScientific c1 e1) + (MkScientific c2 e2) =
    if e1 < e2
    then MkScientific (c1 + c2 * (10 `pow` (e2 - e1))) e1
    else MkScientific (c1 * (10 `pow` (e1 - e2)) + c2) e2
  (MkScientific m n) * (MkScientific m' n') = MkScientific (m * m') (n * n')
  fromInteger i = MkScientific i 0

export
Neg Scientific where
  negate (MkScientific c e) = MkScientific (-c) e

||| Convert a integer into a `Scientific` with its most significant digit moved to just after the decimal point
export
asDecimal : Integer -> Scientific
asDecimal n = MkScientific n (negate (bin10Index n))

export
toDouble : Scientific -> Double
toDouble (MkScientific m n) = cast m * (10 `pow` cast n)


text:
module Issue710b

data r : Type where


text:
module vadd

-- :addclause
vadd : Num a => Vect n a -> Vect n a -> Vect n a

max_stars_repo_name: lynn/idris-sublime

max_issues_repo_name: lynn/idris-sublime

max_forks_repo_name: lynn/idris-sublime


text:
data Vect : Nat -> Type -> Type where
  Nil : Vect Z a
  (::) : (x : a) -> (xs : Vect k a) -> Vect (S k) a
%name Vect xs, ys, zs

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

data VectUnknown : Type -> Type where
  MkVect : (len : Nat) -> Vect len a -> VectUnknown a

read_vect : IO (VectUnknown String)
read_vect = do x <- getLine
               if (x == "")
                  then pure (MkVect _ [])
                  else do MkVect _ xs <- read_vect
                          pure (MkVect _ (x :: xs))

Show a => Show (Vect n a) where
  show [] = ""
  show (x :: xs) = show x ++ show xs

printVect : Show a => VectUnknown a -> IO ()
printVect (MkVect len xs) = let xss : String = show xs
                                lengths : String = show len in
                                putStrLn (xss ++ " (length " ++ lengths ++ ")")

Eq a => Eq (Vect n a) where
  (==) [] [] = True
  (==) (x :: xs) (y :: ys) = case x == y of
                                  True => xs == ys
                                  False => False

max_stars_repo_name: janschultecom/idris-examples

max_issues_repo_name: janschultecom/idris-examples

max_forks_repo_name: janschultecom/idris-examples


text:
-- exercises in "Type-Driven Development with Idris"
-- chapter 14, section 2, Security part

-- check that all functions are total
%default total

data Access = LoggedOut | LoggedIn
data PwdCheck = Correct | Incorrect

data ShellCmd : (ty : Type) -> Access -> (ty -> Access) -> Type where
  Password : String -> ShellCmd PwdCheck LoggedOut
                                         (\res => case res of
                                                    Correct => LoggedIn
                                                    Incorrect => LoggedOut)
  Logout : ShellCmd () LoggedIn (const LoggedOut)
  GetSecret : ShellCmd String LoggedIn (const LoggedIn)
  PutStr : String -> ShellCmd () state (const state)
  Pure : (res : ty) -> ShellCmd ty (state res) state
  (>>=) : ShellCmd a state1 state2 ->
          ((res : a) -> ShellCmd b (state2 res) state3) ->
          ShellCmd b state1 state3

session : ShellCmd () LoggedOut (const LoggedOut)
session = do Correct <- Password "wurzel"
             | Incorrect => PutStr "Wrong password"
             msg <- GetSecret
             PutStr ("Secret code: " ++ show msg ++ "\n")
             Logout

-- sessionBad : ShellCmd () LoggedOut (const LoggedOut)
-- sessionBad = do Password "wurzel"
--                 msg <- GetSecret
--                 PutStr ("Secret code: " ++ show msg ++ "\n")
--                 Logout

-- noLogout : ShellCmd () LoggedOut (const LoggedOut)
-- noLogout = do Correct <- Password "wurzel"
--               | Incorrect => PutStr "Wrong password"
--               msg <- GetSecret
--               PutStr ("Secret code: " ++ show msg ++ "\n")

max_stars_repo_name: pascalpoizat/idris-book

max_issues_repo_name: pascalpoizat/idris-book

max_forks_repo_name: pascalpoizat/idris-book


text:
module Vehicle

%default total

data PowerSource = Petrol | Pedal

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

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

refuel : Vehicle Petrol -> Vehicle Petrol
refuel (Car _) = Car 50
refuel (Bus _) = Bus 100
refuel Bicycle impossible

max_stars_repo_name: timmyjose-study/tdd-with-idris

max_issues_repo_name: timmyjose-study/tdd-with-idris

max_forks_repo_name: timmyjose-study/tdd-with-idris


text:
= ImpParser: Lexing and Parsing in Idris

> module ImpParser
>

The development of the Imp language in `Imp.lidr` completely ignores issues of
concrete syntax -- how an ASCII string that a programmer might write gets
translated into abstract syntax trees defined by the datatypes \idr{AExp},
\idr{BExp}, and \idr{Com}. In this chapter, we illustrate how the rest of the
story can be filled in by building a simple lexical analyzer and parser using
Idris's functional programming facilities.

It is not important to understand all the details here (and accordingly, the
explanations are fairly terse and there are no exercises). The main point is
simply to demonstrate that it can be done. You are invited to look through the
code -- most of it is not very complicated, though the parser relies on some
"monadic" programming idioms that may require a little work to make out -- but
most readers will probably want to just skim down to the `Examples` section at
the very end to get the punchline.

> import Maps
> import Imp
>

== Internals

=== Lexical Analysis

> data Chartype = White | Alpha | Digit | Other
>
> classifyChar : (c : Char) -> Chartype
> classifyChar c =
>   if isSpace c then
>     White
>   else if isAlpha c then
>     Alpha
>   else if isDigit c then
>     Digit
>   else
>     Other
>
> Token : Type
> Token = String
>
> tokenizeHelper : (cls : Chartype) -> (acc, xs : List Char) -> List (List Char)
> tokenizeHelper cls acc xs =
>   case xs of
>     []       => tk
>     (x::xs') =>
>       case (cls, classifyChar x, x) of
>         (_, _, '(')       =>
>           tk ++ ['('] :: (tokenizeHelper Other [] xs')
>         (_, _, ')')       =>
>           tk ++ [')'] :: (tokenizeHelper Other [] xs')
>         (_, White, _)     =>
>           tk ++ (tokenizeHelper White [] xs')
>         (Alpha, Alpha, x) =>
>           tokenizeHelper Alpha (x::acc) xs'
>         (Digit, Digit, x) =>
>           tokenizeHelper Digit (x::acc) xs'
>         (Other, Other, x) =>
>           tokenizeHelper Other (x::acc) xs'
>         (_, tp, x)        =>
>           tk ++ (tokenizeHelper tp [x] xs')
>  where
>   tk : List (List Char)
>   tk = case acc of
>          []     => []
>          (_::_) => [reverse acc]
>
> tokenize : (s : String) -> List String
> tokenize s = map pack (tokenizeHelper White [] (unpack s))
>
> tokenizeEx1 : tokenize "abc12==3  223*(3+(a+c))" = ["abc","12","==","3","223","*","(","3","+","(","a","+","c",")",")"]
> tokenizeEx1 = Refl
>

=== Parsing

==== Options With Errors

An \idr{Option} type with error messages:

> data OptionE : (x : Type) -> Type where
>   SomeE : x -> OptionE x
>   NoneE : String -> OptionE x
>

Some interface instances to make writing nested match-expressions on
\idr{OptionE} more convenient.

\todo[inline]{Explain these/link to Haskell etc?}

> Functor OptionE where
>   map f (SomeE x)   = SomeE (f x)
>   map _ (NoneE err) = NoneE err
>
> Applicative OptionE where
>   pure = SomeE
>   (SomeE f) <*> (SomeE x) = SomeE (f x)
>   (SomeE _) <*> (NoneE e) = NoneE e
>   (NoneE e) <*> _         = NoneE e
>
> Alternative OptionE where
>   empty = NoneE ""
>   (SomeE x) <|> _ = SomeE x
>   (NoneE _) <|> v = v
>
> Monad OptionE where
>   (NoneE e) >>= _ = NoneE e
>   (SomeE x) >>= k = k x
>

==== Generic Combinators for Building Parsers

> Parser : (t : Type) -> Type
> Parser t = List Token -> OptionE (t, List Token)
>
> manyHelper : (p : Parser t) -> (acc : List t) -> (steps : Nat) -> Parser (List t)
> manyHelper p acc Z _ = NoneE "Too many recursive calls"
> manyHelper p acc (S steps') xs with (p xs)
>  | NoneE _        = SomeE (reverse acc, xs)
>  | SomeE (t', xs') = manyHelper p (t'::acc) steps' xs'
>

A (step-indexed) parser that expects zero or more \idr{p}s:

> many : (p : Parser t) -> (steps : Nat) -> Parser (List t)
> many p steps = manyHelper p [] steps
>

A parser that expects a given token, followed by \idr{p}:

> firstExpect : (a : Token) -> (p : Parser t) -> Parser t
> firstExpect a p (x::xs) = if x == a then p xs else NoneE ("Expected '" ++ a ++ "'")
> firstExpect a _ [] = NoneE ("Expected '" ++ a ++ "'")
>

A parser that expects a particular token:

> expect : (t : Token) -> Parser ()
> expect t = firstExpect t (\xs => SomeE ((), xs))
>

==== A Recursive-Descent Parser for Imp

Identifiers:

> parseIdentifier : Parser Id
> parseIdentifier [] = NoneE "Expected identifier"
> parseIdentifier (x::xs) =
>   if all isLower (unpack x)
>     then SomeE (MkId x, xs)
>     else NoneE ("Illegal identifier:'" ++ x ++ "'")
>

Numbers:

> parseNumber : Parser Nat
> parseNumber [] = NoneE "Expected number"
> parseNumber (x::xs) =
>   if all isDigit (unpack x)
>     then SomeE (foldl (\n, d => 10 * n + (cast (ord d - ord '0'))) 0 (unpack x), xs)
>     else NoneE "Expected number"
>

Parse arithmetic expressions

> mutual
>   parsePrimaryExp : (steps : Nat) -> Parser AExp
>   parsePrimaryExp Z _ = NoneE "Too many recursive calls"
>   parsePrimaryExp (S steps') xs =
>     (do (i, rest) <- parseIdentifier xs
>         pure (AId i, rest))
>     <|>
>     (do (n, rest) <- parseNumber xs
>         pure (ANum n, rest))
>     <|>
>     (do (e, rest)  <- firstExpect "(" (parseSumExp steps') xs
>         (u, rest') <- expect ")" rest
>         pure (e, rest'))
>
>   parseProductExp : (steps : Nat) -> Parser AExp
>   parseProductExp Z _ = NoneE "Too many recursive calls"
>   parseProductExp (S steps') xs =
>     do (e, rest) <- parsePrimaryExp steps' xs
>        (es, rest') <- many (firstExpect "*" (parsePrimaryExp steps')) steps' rest
>        pure (foldl AMult e es, rest')
>
>   parseSumExp : (steps : Nat) -> Parser AExp
>   parseSumExp Z _ = NoneE "Too many recursive calls"
>   parseSumExp (S steps') xs =
>     do (e, rest) <- parseProductExp steps' xs
>        (es, rest') <- many psum steps' rest
>        pure (foldl (\e0, term =>
>                      case term of
>                        (True,  e) => APlus e0 e
>                        (False, e) => AMinus e0 e
>                    ) e es, rest')
>     where
>     psum : Parser (Bool, AExp)
>     psum xs =
>       let p = parseProductExp steps' in
>       (do (e, r) <- firstExpect "+" p xs
>           pure ((True, e), r))
>       <|>
>       (do (e, r) <- firstExpect "-" p xs
>           pure ((False, e), r))
>
> parseAExp : (steps : Nat) -> Parser AExp
> parseAExp = parseSumExp
>

Parsing boolean expressions:

> mutual
>   parseAtomicExp : (steps : Nat) -> Parser BExp
>   parseAtomicExp Z _ = NoneE "Too many recursive calls"
>   parseAtomicExp (S steps') xs =
>     (do (_, rest) <- expect "true" xs
>         pure (BTrue, rest))
>     <|>
>     (do (_, rest) <- expect "false" xs
>         pure (BFalse, rest))
>     <|>
>     (do (e, rest) <- firstExpect "not" (parseAtomicExp steps') xs
>         pure (BNot e, rest))
>     <|>
>     (do (e, rest) <- firstExpect "(" (parseConjunctionExp steps') xs
>         (_, rest') <- expect ")" rest
>         pure (e, rest'))
>     <|>
>     (do (e, rest) <- parseProductExp steps' xs
>         ((do (e', rest') <- firstExpect "==" (parseAExp steps') rest
>              pure (BEq e e', rest'))
>          <|>
>          (do (e', rest') <- firstExpect "<=" (parseAExp steps') rest
>              pure (BLe e e', rest'))
>          <|>
>          (NoneE "Expected '==' or '<=' after arithmetic expression")))
>
>   parseConjunctionExp : (steps : Nat) -> Parser BExp
>   parseConjunctionExp Z _ = NoneE "Too many recursive calls"
>   parseConjunctionExp (S steps') xs =
>     do (e, rest) <- parseAtomicExp steps' xs
>        (es, rest') <- many (firstExpect "&&" (parseAtomicExp steps')) steps' rest
>        pure (foldl BAnd e es, rest')
>
> parseBExp : (steps : Nat) -> Parser BExp
> parseBExp = parseConjunctionExp
>
> testParsing : (p : Nat -> Parser t) -> (s : String) -> OptionE (t, List Token)
> testParsing p s = p 100 (tokenize s)
>

\todo[inline]{The second one seems designed to fail}

```idris
λΠ> testParsing parseProductExp "x*y*(x*x)*x"

λΠ> testParsing parseConjunctionExp "not((x==x||x*x<=(x*x)*x)&&x==x"
```

Parsing commands:

> mutual
>   parseSimpleCommand : (steps : Nat) -> Parser Com
>   parseSimpleCommand Z _ = NoneE "Too many recursive calls"
>   parseSimpleCommand (S steps') xs =
>     (do (_, rest) <- expect "SKIP" xs
>         pure (SKIP, rest))
>     <|>
>     (do (e, rest) <- firstExpect "IF" (parseBExp steps') xs
>         (c, rest') <- firstExpect "THEN" (parseSequencedCommand steps') rest
>         (c', rest'') <- firstExpect "ELSE" (parseSequencedCommand steps') rest'
>         (_, rest''') <- expect "END" rest''
>         pure (IFB e THEN c ELSE c' FI, rest'''))
>     <|>
>     (do (e, rest) <- firstExpect "WHILE" (parseBExp steps') xs
>         (c, rest') <- firstExpect "DO" (parseSequencedCommand steps') rest
>         (_, rest'') <- expect "END" rest'
>         pure (WHILE e c, rest''))
>     <|>
>     (do (i, rest) <- parseIdentifier xs;
>         (e, rest') <- firstExpect ":=" (parseAExp steps') rest
>         pure (i ::= e, rest'))
>
>   parseSequencedCommand : (steps : Nat) -> Parser Com
>   parseSequencedCommand Z _ = NoneE "Too many recursive calls"
>   parseSequencedCommand (S steps') xs =
>     do (c, rest) <- parseSimpleCommand steps' xs
>        ((do (c', rest') <- firstExpect ";;" (parseSequencedCommand steps') rest
>             pure ((do c; c'), rest'))
>         <|>
>         (pure (c, rest)))
>
> bignumber : Nat
> bignumber = 1000
>
> parse : (str : String) -> OptionE (Com, List Token)
> parse str = parseSequencedCommand bignumber (tokenize str)
>

== Examples

```idris
λΠ> parse "IF x == y + 1 + 2 - y * 6 + 3 THEN x := x * 1;; y := 0 ELSE SKIP END"
SomeE (CIf (BEq (AId (MkId "x")) (APlus (AMinus (APlus (APlus (AId (MkId "y")) (ANum 1)) (ANum 2)) (AMult (AId (MkId "y")) (ANum 6))) (ANum 3)))
           (CSeq (CAss (MkId "x") (AMult (AId (MkId "x")) (ANum 1))) (CAss (MkId "y") (ANum 0)))
           CSkip,
       []) : OptionE (Com, List String)

λΠ> parse "SKIP;; z:=x*y*(x*x);; WHILE x==x DO IF z <= z*z && not x == 2 THEN x := z;; y := z ELSE SKIP END;; SKIP END;; x:=z"
```

\todo[inline]{This one is repeated twice in the book for some reason}

```idris
λΠ> parse "SKIP;; z:=x*y*(x*x);; WHILE x==x DO IF z <= z*z && not x == 2 THEN x := z;; y := z ELSE SKIP END;; SKIP END;; x:=z"
SomeE (CSeq CSkip
            (CSeq (CAss (MkId "z") (AMult (AMult (AId (MkId "x")) (AId (MkId "y"))) (AMult (AId (MkId "x")) (AId (MkId "x")))))
                  (CSeq (CWhile (BEq (AId (MkId "x")) (AId (MkId "x")))
                                (CSeq (CIf (BAnd (BLe (AId (MkId "z")) (AMult (AId (MkId "z")) (AId (MkId "z")))) (BNot (BEq (AId (MkId "x")) (ANum 2))))
                                           (CSeq (CAss (MkId "x") (AId (MkId "z"))) (CAss (MkId "y") (AId (MkId "z"))))
                                           CSkip)
                                      CSkip))
                        (CAss (MkId "x") (AId (MkId "z"))))),
       []) : OptionE (Com, List String)
```

ext: lidr

max_stars_repo_name: diseraluca/software-foundations

max_issues_repo_name: diseraluca/software-foundations

max_forks_repo_name: diseraluca/software-foundations


text:
-- exercises in "Type-Driven Development with Idris"
-- chapter 11, section 2

-- check that all functions are total
%default total

data InfIO : Type where
  Do : IO a
       -> (a -> Inf InfIO)
       -> InfIO

data LazyFuel = LDry | LMore (Lazy LazyFuel)

partial
forever : LazyFuel
forever = LMore forever

runOnLazyFuel : LazyFuel -> InfIO -> IO ()
runOnLazyFuel (LMore fuel) (Do act gen) = do res <- act
                                             runOnLazyFuel fuel (gen res)
runOnLazyFuel LDry ios = putStrLn "Out of fuel"

(>>=) : IO a -> (a -> Inf InfIO)  -> InfIO
(>>=) = Do

totalREPL : String -> (String -> String) -> InfIO
totalREPL prompt action =
  do putStr prompt
     input <- getLine
     putStr $ action input
     totalREPL prompt action

partial
mainREPL : IO ()
mainREPL = runOnLazyFuel forever (totalREPL "\n: " toUpper)


text:
module CairoCode.Traversal.ValueTracker

import Data.SortedSet
import Data.SortedMap
import CairoCode.CairoCode
import Core.Context
import CairoCode.Traversal.Base
import CairoCode.Traversal.Composition
import CairoCode.Traversal.Defaults
import Utils.Helpers
import Utils.Lens
import Debug.Trace

%hide Prelude.toList

public export
ValBindType : InstVisit a -> Type -> Type
ValBindType (VisitFunction _ _ _ _) a = (List a, SortedMap LinearImplicit a)
ValBindType (VisitForeignFunction _ _ _ _) a = ()
ValBindType (VisitAssign _ _) a = a
ValBindType (VisitMkCon _ _ _) a = a
ValBindType (VisitMkClosure _ _ _ _) a = a
ValBindType (VisitApply _ _ _ _) a = (a, SortedMap LinearImplicit a)
ValBindType (VisitMkConstant _ _) a = a
ValBindType (VisitCall _ _ _ _) a = (List a, SortedMap LinearImplicit a)
ValBindType (VisitOp _ _ _ _) a = (a, SortedMap LinearImplicit a)
ValBindType (VisitExtprim _ _ _ _) a = (List a, SortedMap LinearImplicit a)
ValBindType (VisitCase _) a = ()
ValBindType (VisitConBranch _) a = Maybe a
ValBindType (VisitConstBranch _) a = Maybe a
ValBindType VisitBranchEnd a = ()
ValBindType VisitCaseEnd a = ()
ValBindType (VisitProject _ _ _) a = a
ValBindType (VisitReturn _ _) a = ()
ValBindType (VisitNull _) a = a
ValBindType (VisitError _ _) a = a
ValBindType VisitEndFunction a = ()

public export
NoImplValBindType : InstVisit a -> Type -> Type
NoImplValBindType (VisitApply _ _ _ _) a = a
NoImplValBindType (VisitCall _ _ _ _) a = List a
NoImplValBindType (VisitOp _ _ _ _) a = a
NoImplValBindType (VisitExtprim _ _ _ _) a = List a
NoImplValBindType inst a = ValBindType inst a

export
passThroughImpls : ((v:InstVisit a) -> Traversal s (NoImplValBindType v a)) -> ((v:InstVisit a) -> Traversal s (ValBindType v a))
passThroughImpls fn = processImpls
    where procImpls : (v:InstVisit a) -> SortedMap LinearImplicit (a, CairoReg) -> Traversal s (NoImplValBindType v a, SortedMap LinearImplicit a)
          procImpls inst linImps = do
              res <- fn inst
              pure (res, mapValueMap fst linImps)
          processImpls : (v:InstVisit a) -> Traversal s (ValBindType v a)
          processImpls inst@(VisitApply _ linImpls _ _) = procImpls inst linImpls
          processImpls inst@(VisitCall _ linImpls _ _) = procImpls inst linImpls
          processImpls inst@(VisitOp _ linImpls _ _) = procImpls inst linImpls
          processImpls inst@(VisitExtprim _ linImpls _ _) = procImpls inst linImpls
          -- Sadly idris needs full pattern for the case where: NoImplValBindType inst a = ValBindType inst a
          processImpls inst@(VisitFunction _ _ _ _) = fn inst
          processImpls inst@(VisitForeignFunction _ _ _ _) = fn inst
          processImpls inst@(VisitAssign _ _) = fn inst
          processImpls inst@(VisitMkCon _ _ _) = fn inst
          processImpls inst@(VisitMkClosure _ _ _ _) = fn inst
          processImpls inst@(VisitMkConstant _ _) = fn inst
          processImpls inst@(VisitCase _) = fn inst
          processImpls inst@(VisitConBranch _) = fn inst
          processImpls inst@(VisitConstBranch _) = fn inst
          processImpls inst@VisitBranchEnd = fn inst
          processImpls inst@VisitCaseEnd = fn inst
          processImpls inst@(VisitProject _ _ _) = fn inst
          processImpls inst@(VisitReturn _ _) = fn inst
          processImpls inst@(VisitNull _) = fn inst
          processImpls inst@(VisitError _ _) = fn inst
          processImpls inst@VisitEndFunction = fn inst

export
data BindingScope : Type -> Type where
     CaseScope : CairoReg -> SortedMap CairoReg a -> BindingScope a
     BlockScope : SortedMap CairoReg a -> BindingScope a

Show (BindingScope a) where
  show (CaseScope reg _) = "Case " ++ (show reg)
  show (BlockScope _ ) = "Block"

public export
ScopedBindings : Type -> Type
ScopedBindings a = List (BindingScope a)

findBinding : CairoReg -> ScopedBindings a -> Maybe (Int, a)
findBinding _ Nil = Nothing
findBinding reg ((CaseScope _ _)::xs) = map (\(d,res) => (d+1, res)) (findBinding reg xs)
findBinding reg ((BlockScope binds)::xs) = case lookup reg binds of
    Nothing => map (\(d,res) => (d+1, res)) (findBinding reg xs)
    (Just res) => Just (0,res)

findCaseReg : ScopedBindings a -> Maybe CairoReg
findCaseReg Nil = Nothing
findCaseReg ((CaseScope a _)::xs) = Just a
findCaseReg ((BlockScope _)::xs) = findCaseReg xs

allCaseRegs : ScopedBindings a -> List CairoReg
allCaseRegs Nil = Nil
allCaseRegs ((CaseScope a _)::xs) = a::(allCaseRegs xs)
allCaseRegs ((BlockScope _)::xs) = allCaseRegs xs

addBinding : CairoReg -> a -> ScopedBindings a -> ScopedBindings a
addBinding reg val ((BlockScope binds)::xs) = (BlockScope (insert reg val binds))::xs
addBinding _ _ _ = assert_total $ idris_crash "Can not add binding to empty or case Scope"

allCaseBindings : ScopedBindings a -> List a
allCaseBindings binds = allCaseRegs binds >>= (\reg => flatten $ findBinding reg binds)
    where flatten : Maybe (Int, a) -> List a
          flatten Nothing = Nil
          flatten (Just (_, av)) = [av]

findCaseBinding : ScopedBindings a -> Maybe (Int, a)
findCaseBinding binds = (findCaseReg binds >>= (\reg => findBinding reg binds))

export
getBinding : CairoReg -> Traversal (ScopedBindings a) (Maybe a)
getBinding reg = do
    state <- readState
    let res = findBinding reg state
    pure $ map snd res

export
getAllCaseReg : Traversal (ScopedBindings a) (List CairoReg)
getAllCaseReg = pure $ allCaseRegs !readState

export
getAllCaseBindings : Traversal (ScopedBindings a) (List a)
getAllCaseBindings = pure $ allCaseBindings !readState

export
getCaseReg : Traversal (ScopedBindings a) (Maybe CairoReg)
getCaseReg = pure $ findCaseReg !readState

export
getCaseBinding : Traversal (ScopedBindings a) (Maybe a)
getCaseBinding = do
    state <- readState
    let res = findCaseBinding state
    pure $ map snd res

export
getDistance : CairoReg -> Traversal (ScopedBindings a) (Maybe Int)
getDistance reg = do
    state <- readState
    let res = findBinding reg state
    pure $ map (\(dist,_) => dist) res

export
getDepth : Traversal (ScopedBindings a) Int
getDepth = pure (div (cast $  length !readState) 2)

export
bindReg : CairoReg -> a -> Traversal (ScopedBindings a) ()
bindReg reg val = updateState (addBinding reg val)

descendCase : CairoReg -> Traversal (ScopedBindings a) ()
descendCase reg = updateState update
    where update : ScopedBindings a -> ScopedBindings a
          update old@((BlockScope binds)::xs) = (CaseScope reg binds)::old
          update _ = assert_total $ idris_crash "Wrong stack structure for case descending"

descendBranch : Traversal (ScopedBindings a) ()
descendBranch = updateState update
    where update : ScopedBindings a -> ScopedBindings a
          update old@((CaseScope _ _)::(BlockScope binds)::xs) = (BlockScope binds)::old
          update _ = assert_total $ idris_crash "Wrong stack structure for branch descending"

ascendBranch : Semigroup a => Traversal (ScopedBindings a) ()
ascendBranch = updateState update
    where update : ScopedBindings a -> ScopedBindings a
          update (((BlockScope blockBinds)::(CaseScope cv caseBinds)::xs)) = (CaseScope cv (blockBinds <+> caseBinds))::xs
          update _ = assert_total $ idris_crash "Wrong stack structure for branch ascending"

ascendCase : Traversal (ScopedBindings a) ()
ascendCase = updateState update
    where update : ScopedBindings a -> ScopedBindings a
          update (((CaseScope cv caseBinds)::(BlockScope _)::xs)) = (BlockScope caseBinds)::xs
          update _ = assert_total $ idris_crash "Wrong stack structure for case ascending"

{-
 Executes looks up bindings for registers and replace with the bound value then use tracker to compute the bindings for the instruction and adds them to the lexical scope
 -- Light Version
 start - value (Reg) & state -> substitute (Reg-> a) |- value (a) & state -> tracker => bindResult - value -> _
                                | ---------------------use same binding state ------------------|
 --- Full Version ---
 start - value (Reg) & state ---------------> manage lexical scope - value (Reg) -> _
     | - value (Reg) -> substitute (Reg-> a) <- state -----------|
                        | - value (a) & state -> tracker => bindResult - value -> _
                                                                     | - state -> end
-}
export
valueTracker : Semigroup a => Lens os (ScopedBindings a) ->(CairoReg -> a) -> ((v:InstVisit a) -> Traversal os (ValBindType v a)) -> (InstVisit CairoReg -> Traversal os ())
valueTracker lens defaultCase tracker = seqTraversal handleCase (substituteInstVisitValue substitute doTracking)
    where lift : Traversal (ScopedBindings a) b -> Traversal os b
          lift = composeState lens
          substitute : CairoReg -> Traversal os a
          substitute Eliminated = tracker (VisitNull Eliminated)
          substitute inst@(Const c) = tracker (VisitMkConstant inst c)
          substitute reg = map (fromMaybe (defaultCase reg)) (lift $ getBinding reg)
          bindSingle : CairoReg -> a -> Traversal os ()
          bindSingle r v = lift $ bindReg r v
          bindAll : List (CairoReg, a) -> Traversal os ()
          bindAll binds = foldlM (\_,(r,v) => bindSingle r v) () binds
          getPlainImplBindings : SortedMap LinearImplicit CairoReg -> SortedMap LinearImplicit a -> List (CairoReg, a)
          getPlainImplBindings implRegs implVals = map (\linImpl => genMayBind (lookup linImpl implRegs) (lookup linImpl implVals)) (keys implRegs)
            where genMayBind: Maybe CairoReg -> Maybe a -> (CairoReg, a)
                  genMayBind (Just reg) (Just v) = (reg, v)
                  genMayBind _ _ = assert_total $ idris_crash "No impl Binding was provided"
          getImplBindings : SortedMap LinearImplicit (a, CairoReg) -> SortedMap LinearImplicit a -> List (CairoReg, a)
          getImplBindings implRegs implVals = getPlainImplBindings (mapValueMap snd implRegs) implVals
          handleCase : InstVisit CairoReg -> Traversal os ()
          handleCase (VisitCase caseReg) = lift $ descendCase caseReg
          handleCase _ = pure ()
          rebindCaseReg : Maybe a -> Traversal os ()
          rebindCaseReg Nothing = pure ()
          rebindCaseReg (Just av) = lift getCaseReg >>= (\mReg => fromMaybe (pure ()) (map (\reg => bindSingle reg av) mReg))
          doTracking : InstVisit a -> Traversal os ()
          doTracking inst@(VisitFunction _ params impls _) = do
            _ <- writeStateL lens ((BlockScope empty)::Nil)    -- start with a fresh block (we can not use descend as this expect a parent vlock
            (pramVs, implVs) <- tracker inst
            bindAll ((zip params pramVs) ++ getPlainImplBindings impls implVs)
          doTracking inst@(VisitForeignFunction _ _ _ _ ) = writeStateL lens ((BlockScope empty)::Nil)  -- start with a fresh block (we can not use descend as this expect a parent vlock
          doTracking inst@(VisitAssign res _) = tracker inst >>= bindSingle res
          doTracking inst@(VisitMkCon res _ _) = tracker inst >>= bindSingle res
          doTracking inst@(VisitMkClosure res _ _ _) = tracker inst >>= bindSingle res
          doTracking inst@(VisitApply res impls _ _) = tracker inst >>= (\(resV, implVs) => bindAll ((res,resV)::(getImplBindings impls implVs)))
          doTracking inst@(VisitMkConstant res _) = tracker inst >>= bindSingle res
          doTracking inst@(VisitCall res impls _ _) = tracker inst >>= (\(resV, implVs) => bindAll ((zip res resV) ++ (getImplBindings impls implVs)))
          doTracking inst@(VisitOp res impls _ _) = tracker inst >>= (\(resV, implVs) => bindAll ((res,resV)::(getImplBindings impls implVs)))
          doTracking inst@(VisitExtprim res impls _ _) = tracker inst >>= (\(resV, implVs) => bindAll ((zip res resV) ++ (getImplBindings impls implVs)))
          doTracking (VisitCase caseReg) = pure () -- Already handled by handleCase
          doTracking inst@(VisitConBranch _) = (lift descendBranch) >>= (\_ => tracker inst >>= rebindCaseReg)
          doTracking inst@(VisitConstBranch _) = (lift descendBranch) >>= (\_ => tracker inst >>= rebindCaseReg)
          doTracking VisitBranchEnd = lift ascendBranch
          doTracking VisitCaseEnd = lift ascendCase
          doTracking inst@(VisitProject res _ _) = tracker inst >>= (bindSingle res)
          doTracking inst@(VisitReturn _ _ ) = tracker inst -- Maybe the tracker wants to record the return in the state
          doTracking inst@(VisitNull res) = tracker inst >>= (bindSingle res)
          doTracking inst@(VisitError res _ ) = tracker inst >>= (bindSingle res)
          doTracking VisitEndFunction = writeStateL lens Nil

export
initialTrackerState : ScopedBindings a
initialTrackerState = Nil

{-
 Uses valueTracker to manage bindings and then executes collector on substituted values
 -- Light Version
 start - value (Reg) & state -> valueTracker - value (Reg) -> substitute (Reg-> a) - value (a) & state -> collector - value (a) & state -> end
                                | --use same binding state ---|
 --- Full Version ---
 start - value (Reg) & state -------------> valueTracker (tracker) - value -> _
     | - value (Reg) -> substitute (Reg-> a) <- state -|
                        | - value (a) & state -> collector - value (b) & state -> end
-}
export
valueCollector : Semigroup a => Lens os (ScopedBindings a) -> (CairoReg -> a) -> ((v:InstVisit a) -> Traversal os (ValBindType v a))  -> (InstVisit a -> Traversal os b) -> (InstVisit CairoReg -> Traversal os b)
valueCollector lens defaultCase tracker collector = seqTraversal (valueTracker lens defaultCase tracker) (substituteInstVisitValue substitute collector)
    where substitute : CairoReg -> Traversal os a
          substitute Eliminated = tracker (VisitNull Eliminated)
          substitute inst@(Const c) = tracker (VisitMkConstant inst c)
          substitute reg = map (fromMaybe (defaultCase reg)) (composeState lens (getBinding reg))
{-
 A value tracker with an added transformation step in front of the tracking which is used to produce the result and tracking input
                                                    | --------------------------- use same binding state --------------------------- |
 start - value (Reg) & state --> substitute (Reg-> a) - state & value (a) -> transformer - state & [value (Reg)] -> for each value : valueTracker (tracker) - [value] -> _
                                                                                | - [value (Reg)] ------> end <------ state ------------ |
-}
export
valueTransformer : Semigroup a => Lens os (ScopedBindings a) -> (CairoReg -> a) -> ((v:InstVisit a) -> Traversal os (ValBindType v a)) -> (InstVisit a -> Traversal os (List (InstVisit CairoReg))) -> (InstVisit CairoReg -> Traversal os (List (InstVisit CairoReg)))
valueTransformer lens defaultCase tracker transformer = traverseTransform (substituteInstVisitValue substitute transformer) plainTracker
    where substitute : CairoReg -> Traversal os a
          substitute Eliminated = tracker (VisitNull Eliminated)
          substitute inst@(Const c) = tracker (VisitMkConstant inst c)
          substitute reg = map (fromMaybe (defaultCase reg)) (composeState lens (getBinding reg))
          plainTracker : InstVisit CairoReg -> Traversal os ()
          plainTracker = valueTracker lens defaultCase tracker

export
defaultNoImplValBind : (CairoReg -> a) -> ((v1:InstVisit a) -> Traversal s (Maybe (NoImplValBindType v1 a))) -> ((v2:InstVisit a) -> Traversal s (NoImplValBindType v2 a))
defaultNoImplValBind defaultGen specific = (\inst => map (fromMaybe (fallback inst)) (specific inst))
    where fallback : (v1:InstVisit a) -> NoImplValBindType v1 a
          fallback (VisitFunction _ params impl _) = (map defaultGen params, fromList $  map (\(k,v) => (k, defaultGen v))(toList impl))
          fallback (VisitForeignFunction _ _ _ _)  = ()
          fallback (VisitAssign res _)  = defaultGen res
          fallback (VisitMkCon res _ _)  = defaultGen res
          fallback (VisitMkClosure res _ _ _) = defaultGen res
          fallback (VisitApply res impl _ _) = defaultGen res
          fallback (VisitMkConstant res _) = defaultGen res
          fallback (VisitCall res impl _ _) = map defaultGen res
          fallback (VisitOp res impl _ _) = defaultGen res
          fallback (VisitExtprim res impl _ _) =map defaultGen res
          fallback (VisitCase _)  = ()
          fallback (VisitConBranch _) = Nothing
          fallback (VisitConstBranch _) = Nothing
          fallback VisitBranchEnd = ()
          fallback VisitCaseEnd = ()
          fallback (VisitProject res _ _) = defaultGen res
          fallback (VisitReturn _ _) = ()
          fallback (VisitNull res) = defaultGen res
          fallback (VisitError res _) = defaultGen res
          fallback VisitEndFunction = ()

export
defaultValBind : (CairoReg -> a) -> ((v1:InstVisit a) -> Traversal s (Maybe (ValBindType v1 a))) -> ((v2:InstVisit a) -> Traversal s (ValBindType v2 a))
defaultValBind defaultGen specific = (\inst => map (fromMaybe (fallback inst)) (specific inst))
    where fallback : (v1:InstVisit a) -> ValBindType v1 a
          fallback (VisitFunction _ params impl _) = (map defaultGen params, mapValueMap defaultGen impl)
          fallback (VisitForeignFunction _ _ _ _)  = ()
          fallback (VisitAssign res _)  = defaultGen res
          fallback (VisitMkCon res _ _)  = defaultGen res
          fallback (VisitMkClosure res _ _ _) = defaultGen res
          fallback (VisitApply res impl _ _) = (defaultGen res, mapValueMap (defaultGen . snd) impl)
          fallback (VisitMkConstant res _) = defaultGen res
          fallback (VisitCall res impl _ _) = (map defaultGen res, mapValueMap (defaultGen . snd) impl)
          fallback (VisitOp res impl _ _) = (defaultGen res,  mapValueMap (defaultGen . snd) impl)
          fallback (VisitExtprim res impl _ _) = (map defaultGen res,  mapValueMap (defaultGen . snd) impl)
          fallback (VisitCase _)  = ()
          fallback (VisitConBranch _) = Nothing
          fallback (VisitConstBranch _) = Nothing
          fallback VisitBranchEnd = ()
          fallback VisitCaseEnd = ()
          fallback (VisitProject res _ _) = defaultGen res
          fallback (VisitReturn _ _) = ()
          fallback (VisitNull res) = defaultGen res
          fallback (VisitError res _) = defaultGen res
          fallback VisitEndFunction = ()

-- To make the signature of generalizeTrack more readable
public export
ParamInit : Type -> Type
ParamInit a = Maybe LinearImplicit -> CairoReg -> a

public export
ResGeneral : Type -> Type -> Type
ResGeneral s a = (ret: List CairoReg) -> (params:List a) -> Traversal s (List a)

public export
ImplicitGeneral : Type -> Type -> Type
ImplicitGeneral s a = SortedMap LinearImplicit (a, CairoReg) -> Traversal s (SortedMap LinearImplicit a)

export
generalizeTrack : ParamInit a -> ResGeneral s a -> ImplicitGeneral s a -> ((v:(InstVisit a)) -> Traversal s (ValBindType v a))
generalizeTrack paramInit resGen implGen = generalized
    where failHead : List a -> a
          failHead (x::xs) = x
          failHead _ = assert_total $ idris_crash "Expected non empty list"
          generalized : (v:(InstVisit a)) -> Traversal s (ValBindType v a)
          generalized (VisitFunction _ params impls _) = pure (map (paramInit Nothing) params, mapMap (\(impl,reg) => (impl, paramInit (Just impl) reg)) impls)
          generalized (VisitForeignFunction _ _ _ _) = pure ()
          generalized (VisitAssign res reg) = map failHead (resGen [res] [reg])
          generalized (VisitMkCon res _ args) = map failHead (resGen [res] args)
          generalized (VisitMkClosure res _ _ args) = map failHead (resGen [res] args)
          generalized (VisitApply res linImpls clo arg) = pure (failHead !(resGen [res] [clo,arg]), !(implGen linImpls))
          generalized (VisitMkConstant res _) = map failHead (resGen [res] [])
          generalized (VisitCall res linImpls _ args) = pure (!(resGen res args), !(implGen linImpls))
          generalized (VisitOp res linImpls _ args) = pure (failHead  !(resGen [res] args), !(implGen linImpls))
          generalized (VisitExtprim res linImpls _ args) = pure (!(resGen res args), !(implGen linImpls))
          generalized (VisitCase _) = pure ()
          generalized (VisitConBranch _) = pure Nothing
          generalized (VisitConstBranch _) = pure Nothing
          generalized VisitBranchEnd = pure ()
          generalized VisitCaseEnd = pure ()
          generalized VisitEndFunction = pure ()
          generalized (VisitReturn _ _) = pure ()
          generalized (VisitProject res src _) = map failHead (resGen [res] [src])
          generalized (VisitNull res) = map failHead (resGen [res] [])
          generalized (VisitError res _) = map failHead (resGen [res] [])

max_stars_repo_name: skyro-compiler/skyro

max_issues_repo_name: skyro-compiler/skyro

max_forks_repo_name: skyro-compiler/skyro


text:
-- module Main

data N = Zero | Suc N

addOne : N -> N
addOne Zero = Suc Zero
addOne (Suc n) = Suc (Suc n)

One : N
One = Suc Zero
Two : N
Two = (Suc (Suc Zero))
Three : N
Three = addOne Two
Four : N
Four = addOne Three
Five : N
Five = addOne Four

add : N -> N -> N
add Zero s = s
add (Suc a) b = add a (Suc b)

data Vec : (a : Type) -> N -> Type where
  Nil : Vec a Zero
  Cons : {n : N} -> a -> Vec a n -> Vec a (Suc n)

empt : Vec N Zero
empt = Nil

test : Vec N Two
test = Cons One (Cons Two Nil)

test2 : Vec N Three
test2 = Cons Three (Cons Four (Cons Five Nil))

concat : {g : Type} -> {a : N} -> {b : N} -> Vec g a -> Vec g b -> Vec g (add a b)
concat Nil rest = rest
concat (Cons a rest) b = concat rest (Cons a b)

t3 : Vec N (addOne (addOne (addOne (addOne One))))
t3 = concat test test2

max_stars_repo_name: hjorthjort/IdrisToAgda

max_issues_repo_name: hjorthjort/IdrisToAgda

max_forks_repo_name: hjorthjort/IdrisToAgda


text:
module Extra.Either

import Data.Maybe

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

export
expect : a -> Maybe b -> Either a b
expect left =
  (fromMaybe $ Left left) . (map Right)

export
flipEither : Either a b -> Either b a
flipEither (Left x) = Right x
flipEither (Right x) = Left x

max_stars_repo_name: Z-snails/inigo

max_issues_repo_name: Z-snails/inigo

max_forks_repo_name: Z-snails/inigo


text:
import Data.Vect

-- Exercise 1
myPlusCommutes : (n : Nat) -> (m : Nat) -> n + m = m + n
myPlusCommutes Z m = rewrite plusZeroRightNeutral m in Refl
myPlusCommutes (S k) m = rewrite myPlusCommutes k m in
                         rewrite plusSuccRightSucc m k in Refl

-- Exercise 2
reverseProof_nil : (acc : Vect n1 a) -> Vect (plus n1 0) a
reverseProof_nil {n1} acc = rewrite plusZeroRightNeutral n1 in acc

reverseProof_xs : Vect (S n + k) a -> Vect (plus n (S k)) a
reverseProof_xs {n} {k} xs = rewrite sym (plusSuccRightSucc n k) in xs

myReverse : Vect n a -> Vect n a
myReverse xs = reverse' [] xs
  where
    reverse' : Vect n a -> Vect m a -> Vect (n + m) a
    reverse' acc [] = reverseProof_nil acc
    reverse' acc (x :: xs) = reverseProof_xs (reverse' (x::acc) xs)


text:
module SkewBinomialHeap

import Heap

%default total
%access private

data Tree a = Node Int a (List a) (List (Tree a))

export
data SkewBinomialHeap a = SBH (List (Tree a))

rank : Tree a -> Int
rank (Node r x xs c) = r

root : Tree a -> a
root (Node r x xs c) = x

link : Ord a => Tree a -> Tree a -> Tree a
link t1@(Node r x1 xs1 c1) t2@(Node _ x2 xs2 c2) =
  if x1 <= x2 then Node (r + 1) x1 xs1 (t2 :: c1)
  else Node (r + 1) x2 xs2 (t1 :: c2)

skewLink : Ord a => a -> Tree a -> Tree a -> Tree a
skewLink x t1 t2 =
  let Node r y ys c = link t1 t2
  in if x <= y then Node r x (y :: ys) c else Node r y (x :: ys) c

insTree : Ord a => Tree a -> List (Tree a) -> List (Tree a)
insTree t    []          = [t]
insTree t ts@(t' :: ts') =
  if rank t < rank t' then t :: ts else insTree (link t t') ts'

mrg : Ord a => List (Tree a) -> List (Tree a) -> List (Tree a)
mrg ts1                  []           = ts1
mrg     []           ts2              = ts2
mrg ts1@(t1 :: ts1') ts2@(t2 :: ts2') = case compare (rank t1) (rank t2) of
  LT => t1 :: mrg ts1' ts2
  GT => t2 :: mrg ts1 ts2'
  EQ => insTree (link t1 t2) (mrg ts1' ts2')

normalize : Ord a => List (Tree a) -> List (Tree a)
normalize []        = []
normalize (t :: ts) = insTree t ts

removeMinTree : Ord a => List (Tree a) -> (Tree a, List (Tree a))
removeMinTree [] = idris_crash "empty heap"
removeMinTree [t] = (t, [])
removeMinTree (t :: ts) = let (t', ts') = removeMinTree ts in
  if root t < root t' then (t, ts) else (t', t :: ts')

nlInsert : a -> List (Tree a) -> SkewBinomialHeap a
nlInsert x ts = SBH (Node 0 x [] [] :: ts)

export
Heap SkewBinomialHeap where
  empty = SBH []
  isEmpty (SBH ts) = isNil ts

  insert x (SBH ts@(t1 :: t2 :: ts')) =
    if rank t1 == rank t2 then SBH (skewLink x t1 t2 :: ts')
    else nlInsert x ts
  insert x (SBH ts) = nlInsert x ts

  merge (SBH ts1) (SBH ts2) = SBH (mrg (normalize ts1) (normalize ts2))

  findMin (SBH ts) = root (fst (removeMinTree ts))

  deleteMin (SBH ts) = let (Node _ x xs ts1, ts2) = removeMinTree ts
                           ts' = mrg (reverse ts1) (normalize ts2)
                       in foldr insert (SBH ts') xs


text:
module Specdris.Data.SpecState

import Specdris.Data.ConsoleColor

%access export
%default total

||| Global state of all spec cases which are executed
||| together (monadicly combined).
public export
record SpecState where
  constructor MkState

  totalNum : Nat
  failed   : Nat
  pending  : Nat

  output   : Maybe (List String)

Eq SpecState where
  (==) (MkState lTotal lFailed lPend lOut) (MkState rTotal rFailed rPend rOut)
    = (lTotal == rTotal) && (lFailed == rFailed) && (lPend == rPend) && (lOut == rOut)

Show SpecState where
  show (MkState totalNum failed pending _)
    = "Total = " ++ show totalNum
        ++ ", Failed = " ++ show failed
        ++ ", Pending = " ++ show pending

Semigroup SpecState where
  (<+>) (MkState lt lf lp lo) (MkState rt rf rp ro) = MkState (lt + rt) (lf + rf) (lp + rp) (lo <+> ro)

Monoid SpecState where
  neutral = MkState 0 0 0 Nothing

addSpec : SpecState -> SpecState
addSpec state = record {totalNum $= (+ 1)} state

addFailure : SpecState -> SpecState
addFailure state = record {totalNum $= (+ 1), failed $= (+ 1)} state

addPending : SpecState -> SpecState
addPending state = record {totalNum $= (+ 1), pending $= (+ 1)} state

private
mergeOutput: Maybe (List String) -> Maybe (List String) -> Maybe (List String)
mergeOutput (Just left) (Just right) = Just $ left <+> right
mergeOutput a@(Just left) Nothing    = a
mergeOutput Nothing b@(Just left)    = b
mergeOutput Nothing Nothing          = Nothing

addLine : (line : String) -> SpecState -> SpecState
addLine line state = record {output $= (\o => mergeOutput o (Just [line]))} state

outputToStr : SpecState -> Maybe String
outputToStr state = case output state of
                      (Just out) => Just $ foldl (\acc, line => acc ++ line ++ "\n") "" out
                      Nothing    => Nothing

stateToStr : SpecState -> String
stateToStr state
  = colorise (if failed state == 0 then Green else Red) $
      indent 1
         ++ (if failed state == 0 then "Passed" else "Failed") ++ ": "
         ++ show state

max_stars_repo_name: pheymann/specdris

max_issues_repo_name: pheymann/specdris

max_forks_repo_name: pheymann/specdris


text:
module UninhabitedRec

import Data.Nat
import Data.List.Elem

--Either (Uninhabited a) (Uninhabited b) => Uninhabited (a, b) where
--  uninhabited (x, _) @{Left  _} = uninhabited x
--  uninhabited (_, y) @{Right _} = uninhabited y

ff : Uninhabited (a, b) => Int
ff = 4

callF : Int
callF = ff {b = (Left 4 = Right 4)} {a = 5 = 4}

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

data Lookup : a -> List (a, b) -> Type where
  Here : (y : b) -> Lookup x $ (x, y)::xys
  There : (0 _ : Uninhabited $ x === z) => Lookup z xys -> Lookup z $ (x, y)::xys

fff : (xs : List (Nat, String)) -> (n : Nat) -> (0 _ : Lookup n xs) => String

xxs : List (Nat, String)
xxs = [(1, "one"), (2, "two"), (4, "four")]

lkup1 : String
lkup1 = fff xxs 1

--export
--Uninhabited (a = b) => Uninhabited (S a = S b) where
--  uninhabited Refl @{ab} = uninhabited @{ab} Refl

lkup2 : String
lkup2 = fff xxs 2

lkup3 : String
lkup3 = fff xxs 3

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

data Uniq : Type -> Type

toList : Uniq a -> List a

data Uniq : Type -> Type where
  Nil  : Uniq a
  (::) : (x : a) -> (xs : Uniq a) -> Uninhabited (Elem x $ toList xs) => Uniq a

toList [] = []
toList (x::xs) = x :: toList xs

uniqGood : Uniq Nat
uniqGood = [1, 2, 3]

uniqBad : Uniq Nat
uniqBad = [1, 2, 1]

max_stars_repo_name: buzden/idris-playground

max_issues_repo_name: buzden/idris-playground

max_forks_repo_name: buzden/idris-playground


text:
module Node.HTTP.Server

import public Node.HTTP

export
data IncomingMessage : Type where [external]

export
data ServerResponse : Type where [external]

namespace Request

  export
  %foreign "node:lambda: req => req.headers"
  (.headers) : IncomingMessage -> Headers

  export
  %foreign "node:lambda: req => req.httpVersion"
  (.httpVersion) : IncomingMessage -> String

  export
  %foreign "node:lambda: req => req.method"
  (.method) : IncomingMessage -> String

  export
  %foreign "node:lambda: req => req.url"
  (.url) : IncomingMessage -> String

  %foreign "node:lambda: (ty, req, data) => { req.on('data', a => data(a)()) }"
  ffi_onData : IncomingMessage -> (a -> PrimIO ()) -> PrimIO ()

  export
  (.onData) : HasIO io => IncomingMessage -> (a -> IO ()) -> io ()
  (.onData) req cb = primIO $ ffi_onData req $ \a => toPrim $ cb a

  %foreign "node:lambda: (req, end) => { req.on('end', () => end()()) }"
  ffi_onEnd : IncomingMessage -> (() -> PrimIO ()) -> PrimIO ()

  export
  (.onEnd) : HasIO io => IncomingMessage -> (() -> IO ()) -> io ()
  (.onEnd) req cb = primIO $ ffi_onEnd req $ \_ => toPrim $ cb ()

  %foreign "node:lambda: (ty, req, error) => { req.on('error', e => error(e)()) }"
  ffi_onError : IncomingMessage -> (e -> PrimIO ()) -> PrimIO ()

  export
  (.onError) : HasIO io => IncomingMessage -> (e -> IO ()) -> io ()
  (.onError) req cb = primIO $ ffi_onError req $ \e => toPrim $ cb e

namespace Response

  %foreign "node:lambda: res => res.end()"
  ffi_end : ServerResponse -> PrimIO ()

  export
  (.end) : HasIO io => ServerResponse -> io ()
  (.end) res = primIO $ ffi_end res

  %foreign "node:lambda: (ty, res, data) => res.write(data)"
  ffi_write : { 0 a : _ } -> ServerResponse -> a -> PrimIO ()

  export
  (.write) : HasIO io => ServerResponse -> a -> io ()
  (.write) res a = primIO $ ffi_write res a

  %foreign "node:lambda: (res, status, headers) => res.writeHead(status, headers)"
  ffi_writeHead : ServerResponse -> Int -> Headers -> PrimIO ()

  export
  (.writeHead) : HasIO io => ServerResponse -> Int -> Headers -> io ()
  (.writeHead) res status headers = primIO $ ffi_writeHead res status headers

export
data Server : Type where [external]

%foreign "node:lambda: http => http.createServer()"
ffi_createServer : HTTP -> PrimIO Server

export
(.createServer) : HasIO io => HTTP -> io Server
(.createServer) http = primIO $ ffi_createServer http

%foreign "node:lambda: (server, handler) => server.on('request', (req, res) => handler(req)(res)())"
ffi_onRequest : Server -> (IncomingMessage -> ServerResponse -> PrimIO ()) -> PrimIO ()

export
(.onRequest) : HasIO io => Server -> (IncomingMessage -> ServerResponse -> IO()) -> io ()
(.onRequest) server callback =
  let primCallback = \req => \res => toPrim $ callback req res
  in primIO $ ffi_onRequest server primCallback

%foreign "node:lambda: (server, port) => server.listen(port)"
ffi_listen : Server -> Int -> PrimIO ()

export
(.listen) : HasIO io => Server -> Int -> io ()
(.listen) server port = primIO $ ffi_listen server port

%foreign "node:lambda: server => server.close()"
ffi_close : Server -> PrimIO ()

export
(.close) : HasIO io => Server -> io ()
(.close) server = primIO $ ffi_close server

max_stars_repo_name: kbertalan/tyttp

max_issues_repo_name: kbertalan/tyttp

max_forks_repo_name: kbertalan/tyttp


text:
data Expr
  = Tr
  | Fl
  | IsZero Expr
  | Succ Expr
  | Pred Expr
  | If Expr Expr Expr
  | Zero

data TType
  = TBool
  | TNat
  | TArr TType TType

Eq TType where
  (==) TBool TBool = True
  (==) TNat TNat = True
  (==) (TArr x z) (TArr y w) = ((x == y) && (z ==w))
  (==) _ _ = False

isNum : Expr -> Bool
isNum Zero     = True
isNum (Succ t) = isNum t
isNum _        = False

isVal : Expr -> Bool
isVal Tr = True
isVal Fl = True
isVal Zero = True
isVal (Succ t) = isVal t
isVal _ = False

partial
eval1 : Expr -> Maybe Expr
eval1 t =
  case t of
       Succ t          => Succ <$> (eval1 t)
       Pred Zero       => Just Zero
       Pred (Succ t)   => case isNum t of
                               False => Nothing
                               True => Just t
       Pred t          => Pred <$> (eval1 t)
       IsZero Zero     => Just Tr
       IsZero (Succ t) => case isNum t of
                               False => Nothing -- might be wrong
                               True => Just Fl
       IsZero t        => IsZero <$> (eval1 t)
       If Tr  c _      => Just c
       If Fl _ a       => Just a
       If t c a        => (\t' => If t' c a) <$> eval1 t
       _               => Nothing

partial
nf : Expr -> Expr
nf t = fromMaybe t (nf <$> eval1 t)

partial
eval : Expr -> Maybe Expr
eval t = case (isVal t) of
              False => Just (nf t)
              True => Nothing

data TypeError
  = TypeMismatch TType TType

check : Expr -> Either TypeError TType

typeof : Expr -> Either TypeError TType
typeof t =
  case t of
       (IsZero a) => do
         ta <- typeof a
         case ta of
              TNat => Right TNat
              _ => Left (TypeMismatch ta TNat)
       (Succ a) => do
         ta <- typeof a
         case ta of
              TNat => Right TNat
              _ => Left (TypeMismatch ta TNat)
       (Pred a) => do
         ta <- typeof a
         case ta of
              TNat => Right TNat
              _ => Left (TypeMismatch ta TNat)
       (If a b c) => do
         ta <- typeof a
         tb <- typeof b
         tc <- typeof c
         case ta of
              TBool => case tb == tc of
                            True => Right tc
                            False => Left (TypeMismatch tb tc)
              _ => Left (TypeMismatch ta TBool)
       Zero => Right TNat
       Tr => Right TBool
       Fl => Right TBool

max_stars_repo_name: alexhumphreys/pl-playground

max_issues_repo_name: alexhumphreys/pl-playground

max_forks_repo_name: alexhumphreys/pl-playground


text:
module Test

corecord Stream' : Type -> Type where
  hd : Stream' a -> a
  tl : Stream' a -> Later' (Stream' a)
  constructor StreamCons

fix : (Later' a -> a) -> a
fix f = f(Next (fix f))

pfix : ((a -> Later' b) -> (a -> b)) -> (a -> b)
pfix f = fix(\g => f (\x => compose {n=Now} g (Next x)))

max_stars_repo_name: sualitu/thesis

max_issues_repo_name: sualitu/thesis

max_forks_repo_name: sualitu/thesis


text:
module LazyFoldlM

import Data.List.Lazy

import Debug.Trace

foldlM' : Monad m => (fm : b -> a -> m b) -> (init : b) -> LazyList a -> m b
foldlM' fm init xs = foldrLazy (\x, k, z => fm z x >>= k) pure xs init

l : LazyList Nat
l = (\n => trace "gen \{show n}" n) <$> iterateN 10000 (+1) 0

-- Both should be actually short-cutting (i.e., not many `gen *` should be printed)

x : Maybe Nat
x = foldlM' (\m, n => if m <= 1 then Just n else Nothing) 0 l

y : Maybe Nat
y = foldlM (\m, n => if m <= 1 then Just n else Nothing) 0 l


text:
module TooFewArgs

import IdrisPrelude

myFun : (a : Type) -> a -> a -> a
myFun a x y = x

myApp : Nat
myApp = myFun _ Zero

max_stars_repo_name: JoeyEremondi/lambda-pi-constraint

max_issues_repo_name: JoeyEremondi/lambda-pi-constraint

max_forks_repo_name: JoeyEremondi/lambda-pi-constraint