text:
module Compiler.Inline

import Compiler.CaseOpts
import Compiler.CompileExpr
import Compiler.Identity

import Core.CompileExpr
import Core.Context
import Core.Context.Log
import Core.FC
import Core.Hash
import Core.Options
import Core.TT

import Libraries.Data.LengthMatch
import Data.Maybe
import Libraries.Data.NameMap
import Data.List
import Data.Vect

%default covering

data EEnv : List Name -> List Name -> Type where
     Nil : EEnv free []
     (::) : CExp free -> EEnv free vars -> EEnv free (x :: vars)

extend : EEnv free vars -> (args : List (CExp free)) -> (args' : List Name) ->
         LengthMatch args args' -> EEnv free (args' ++ vars)
extend env [] [] NilMatch = env
extend env (a :: xs) (n :: ns) (ConsMatch w)
    = a :: extend env xs ns w

Stack : List Name -> Type
Stack vars = List (CExp vars)

unload : Stack vars -> CExp vars -> CExp vars
unload [] e = e
unload (a :: args) e = unload args (CApp (getFC e) e [a])

unloadApp : Nat -> Stack vars -> CExp vars -> CExp vars
unloadApp n args e = unload (drop n args) (CApp (getFC e) e (take n args))

getArity : CDef -> Nat
getArity (MkFun args _) = length args
getArity (MkCon _ arity _) = arity
getArity (MkForeign _ args _) = length args
getArity (MkError _) = 0

takeFromStack : EEnv free vars -> Stack free -> (args : List Name) ->
                Maybe (EEnv free (args ++ vars), Stack free)
takeFromStack env (e :: es) (a :: as)
  = do (env', stk') <- takeFromStack env es as
       pure (e :: env', stk')
takeFromStack env stk [] = pure (env, stk)
takeFromStack env [] args = Nothing

data LVar : Type where

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

refToLocal : Name -> (x : Name) -> CExp vars -> CExp (x :: vars)
refToLocal x new tm = refsToLocals (Add new x None) tm

largest : Ord a => a -> List a -> a
largest x [] = x
largest x (y :: ys)
    = if y > x
         then largest y ys
         else largest x ys

mutual
  used : {free : _} ->
         {idx : Nat} -> (0 p : IsVar n idx free) -> CExp free -> Int
  used {idx} n (CLocal _ {idx=pidx} prf) = if idx == pidx then 1 else 0
  used n (CLam _ _ sc) = used (Later n) sc
  used n (CLet _ _ False val sc)
      = let usedl = used n val + used (Later n) sc in
            if usedl > 0
               then 1000 -- Don't do any inlining of the name, because if it's
                         -- used under a non-inlinable let things might go wrong
               else usedl
  used n (CLet _ _ True val sc) = used n val + used (Later n) sc
  used n (CApp _ x args) = foldr (+) (used n x) (map (used n) args)
  used n (CCon _ _ _ _ args) = foldr (+) 0 (map (used n) args)
  used n (COp _ _ args) = foldr (+) 0 (map (used n) args)
  used n (CExtPrim _ _ args) = foldr (+) 0 (map (used n) args)
  used n (CForce _ _ x) = used n x
  used n (CDelay _ _ x) = used n x
  used n (CConCase fc sc alts def)
     = used n sc +
          largest (maybe 0 (used n) def) (map (usedCon n) alts)
  used n (CConstCase fc sc alts def)
     = used n sc +
          largest (maybe 0 (used n) def) (map (usedConst n) alts)
  used _ tm = 0

  usedCon : {free : _} ->
            {idx : Nat} -> (0 p : IsVar n idx free) -> CConAlt free -> Int
  usedCon n (MkConAlt _ _ _ args sc)
      = let MkVar n' = weakenNs (mkSizeOf args) (MkVar n) in
            used n' sc

  usedConst : {free : _} ->
              {idx : Nat} -> (0 p : IsVar n idx free) -> CConstAlt free -> Int
  usedConst n (MkConstAlt _ sc) = used n sc

mutual
  evalLocal : {vars, free : _} ->
              {auto c : Ref Ctxt Defs} ->
              {auto l : Ref LVar Int} ->
              FC -> List Name -> Stack free ->
              EEnv free vars ->
              {idx : Nat} -> (0 p : IsVar x idx (vars ++ free)) ->
              Core (CExp free)
  evalLocal {vars = []} fc rec stk env p
      = pure $ unload stk (CLocal fc p)
  evalLocal {vars = x :: xs} fc rec stk (v :: env) First
      = case stk of
             [] => pure v
             _ => eval rec env stk (weakenNs (mkSizeOf xs) v)
  evalLocal {vars = x :: xs} fc rec stk (_ :: env) (Later p)
      = evalLocal fc rec stk env p

  tryApply : {vars, free : _} ->
             {auto c : Ref Ctxt Defs} ->
             {auto l : Ref LVar Int} ->
             List Name -> Stack free -> EEnv free vars -> CDef ->
             Core (Maybe (CExp free))
  tryApply {free} {vars} rec stk env (MkFun args exp)
      = do let Just (env', stk') = takeFromStack env stk args
               | Nothing => pure Nothing
           res <- eval rec env' stk'
                     (rewrite sym (appendAssociative args vars free) in
                              embed {vars = vars ++ free} exp)
           pure (Just res)
  tryApply rec stk env _ = pure Nothing

  eval : {vars, free : _} ->
         {auto c : Ref Ctxt Defs} ->
         {auto l : Ref LVar Int} ->
         List Name -> EEnv free vars -> Stack free -> CExp (vars ++ free) ->
         Core (CExp free)
  eval rec env stk (CLocal fc p) = evalLocal fc rec stk env p
  -- This is hopefully a temporary hack, giving a special case for io_bind.
  -- Currently the elaborator is a bit cautious about inlining case blocks
  -- in case they duplicate work. We should fix that, to decide more accurately
  -- whether they're safe to inline, but until then this gives such a huge
  -- boost by removing unnecessary lambdas that we'll keep the special case.
  eval rec env stk (CRef fc n)
      = case (n == NS primIONS (UN $ Basic "io_bind"), stk) of
          (True, act :: cont :: world :: stk) =>
                 do xn <- genName "act"
                    sc <- eval rec [] [] (CApp fc cont [CRef fc xn, world])
                    pure $ unload stk $
                             CLet fc xn False (CApp fc act [world])
                                              (refToLocal xn xn sc)
          (_,_) =>
             do defs <- get Ctxt
                Just gdef <- lookupCtxtExact n (gamma defs)
                  | Nothing => pure (unload stk (CRef fc n))
                let Just def = compexpr gdef
                  | Nothing => pure (unload stk (CRef fc n))
                let arity = getArity def
                if (Inline `elem` flags gdef) && (not (n `elem` rec))
                   then do ap <- tryApply (n :: rec) stk env def
                           pure $ fromMaybe (unloadApp arity stk (CRef fc n)) ap
                   else pure $ unloadApp arity stk (CRef fc n)
  eval {vars} {free} rec env [] (CLam fc x sc)
      = do xn <- genName "lamv"
           sc' <- eval rec (CRef fc xn :: env) [] sc
           pure $ CLam fc x (refToLocal xn x sc')
  eval rec env (e :: stk) (CLam fc x sc) = eval rec (e :: env) stk sc
  eval {vars} {free} rec env stk (CLet fc x False val sc)
      = do xn <- genName "letv"
           sc' <- eval rec (CRef fc xn :: env) [] sc
           val' <- eval rec env [] val
           pure (unload stk $ CLet fc x False val' (refToLocal xn x sc'))
  eval {vars} {free} rec env stk (CLet fc x True val sc)
      = do let u = used First sc
           if u < 1 -- TODO: Can make this <= as long as we know *all* inlinings
                    -- are guaranteed not to duplicate work. (We don't know
                    -- that yet).
              then do val' <- eval rec env [] val
                      eval rec (val' :: env) stk sc
              else do xn <- genName "letv"
                      sc' <- eval rec (CRef fc xn :: env) stk sc
                      val' <- eval rec env [] val
                      pure (CLet fc x True val' (refToLocal xn x sc'))
  eval rec env stk (CApp fc f args)
      = eval rec env (!(traverse (eval rec env []) args) ++ stk) f
  eval rec env stk (CCon fc n ci t args)
      = pure $ unload stk $ CCon fc n ci t !(traverse (eval rec env []) args)
  eval rec env stk (COp fc p args)
      = pure $ unload stk $ COp fc p !(traverseVect (eval rec env []) args)
  eval rec env stk (CExtPrim fc p args)
      = pure $ unload stk $ CExtPrim fc p !(traverse (eval rec env []) args)
  eval rec env stk (CForce fc lr e)
      = case !(eval rec env [] e) of
             CDelay _ _ e' => eval rec [] stk e'
             res => pure $ unload stk (CForce fc lr res) -- change this to preserve laziness semantics
  eval rec env stk (CDelay fc lr e)
      = pure $ unload stk (CDelay fc lr !(eval rec env [] e))
  eval rec env stk (CConCase fc sc alts def)
      = do sc' <- eval rec env [] sc
           let env' = update sc env sc'
           Nothing <- pickAlt rec env' stk sc' alts def | Just val => pure val
           def' <- traverseOpt (eval rec env' stk) def
           pure $ caseOfCase $ CConCase fc sc'
                     !(traverse (evalAlt fc rec env' stk) alts)
                     def'
    where
      updateLoc : {idx, vs : _} ->
                  (0 p : IsVar x idx (vs ++ free)) ->
                  EEnv free vs -> CExp free -> EEnv free vs
      updateLoc {vs = []} p env val = env
      updateLoc {vs = (x::xs)} First (e :: env) val = val :: env
      updateLoc {vs = (y::xs)} (Later p) (e :: env) val = e :: updateLoc p env val

      update : {vs : _} ->
               CExp (vs ++ free) -> EEnv free vs -> CExp free -> EEnv free vs
      update (CLocal _ p) env sc = updateLoc p env sc
      update _ env _ = env

  eval rec env stk (CConstCase fc sc alts def)
      = do sc' <- eval rec env [] sc
           Nothing <- pickConstAlt rec env stk sc' alts def | Just val => pure val
           def' <- traverseOpt (eval rec env stk) def
           pure $ caseOfCase $ CConstCase fc sc'
                         !(traverse (evalConstAlt rec env stk) alts)
                         def'
  eval rec env stk (CPrimVal fc c) = pure $ unload stk $ CPrimVal fc c
  eval rec env stk (CErased fc) = pure $ unload stk $ CErased fc
  eval rec env stk (CCrash fc str) = pure $ unload stk $ CCrash fc str

  extendLoc : {auto l : Ref LVar Int} ->
              FC -> EEnv free vars -> (args' : List Name) ->
              Core (Bounds args', EEnv free (args' ++ vars))
  extendLoc fc env [] = pure (None, env)
  extendLoc fc env (n :: ns)
      = do xn <- genName "cv"
           (bs', env') <- extendLoc fc env ns
           pure (Add n xn bs', CRef fc xn :: env')

  evalAlt : {vars, free : _} ->
            {auto c : Ref Ctxt Defs} ->
            {auto l : Ref LVar Int} ->
            FC -> List Name -> EEnv free vars -> Stack free -> CConAlt (vars ++ free) ->
            Core (CConAlt free)
  evalAlt {free} {vars} fc rec env stk (MkConAlt n ci t args sc)
      = do (bs, env') <- extendLoc fc env args
           scEval <- eval rec env' stk
                          (rewrite sym (appendAssociative args vars free) in sc)
           pure $ MkConAlt n ci t args (refsToLocals bs scEval)

  evalConstAlt : {vars, free : _} ->
                 {auto c : Ref Ctxt Defs} ->
                 {auto l : Ref LVar Int} ->
                 List Name -> EEnv free vars -> Stack free -> CConstAlt (vars ++ free) ->
                 Core (CConstAlt free)
  evalConstAlt rec env stk (MkConstAlt c sc)
      = MkConstAlt c <$> eval rec env stk sc

  pickAlt : {vars, free : _} ->
            {auto c : Ref Ctxt Defs} ->
            {auto l : Ref LVar Int} ->
            List Name -> EEnv free vars -> Stack free ->
            CExp free -> List (CConAlt (vars ++ free)) ->
            Maybe (CExp (vars ++ free)) ->
            Core (Maybe (CExp free))
  pickAlt rec env stk (CCon fc n ci t args) [] def
      = traverseOpt (eval rec env stk) def
  pickAlt {vars} {free} rec env stk con@(CCon fc n ci t args) (MkConAlt n' _ t' args' sc :: alts) def
      = if matches n t n' t'
           then case checkLengthMatch args args' of
                     Nothing => pure Nothing
                     Just m =>
                         do let env' : EEnv free (args' ++ vars)
                                   = extend env args args' m
                            pure $ Just !(eval rec env' stk
                                    (rewrite sym (appendAssociative args' vars free) in
                                             sc))
           else pickAlt rec env stk con alts def
    where
      matches : Name -> Maybe Int -> Name -> Maybe Int -> Bool
      matches _ (Just t) _ (Just t') = t == t'
      matches n Nothing n' Nothing = n == n'
      matches _ _ _ _ = False
  pickAlt rec env stk _ _ _ = pure Nothing

  pickConstAlt : {vars, free : _} ->
                 {auto c : Ref Ctxt Defs} ->
                 {auto l : Ref LVar Int} ->
                 List Name -> EEnv free vars -> Stack free ->
                 CExp free -> List (CConstAlt (vars ++ free)) ->
                 Maybe (CExp (vars ++ free)) ->
                 Core (Maybe (CExp free))
  pickConstAlt rec env stk (CPrimVal fc c) [] def
      = traverseOpt (eval rec env stk) def
  pickConstAlt {vars} {free} rec env stk (CPrimVal fc c) (MkConstAlt c' sc :: alts) def
      = if c == c'
           then Just <$> eval rec env stk sc
           else pickConstAlt rec env stk (CPrimVal fc c) alts def
  pickConstAlt rec env stk _ _ _ = pure Nothing

-- Inlining may have messed with function arity (e.g. by adding lambdas to
-- the LHS to avoid needlessly making a closure) so fix them up here. This
-- needs to be right because typically back ends need to know whether a
-- name is under- or over-applied
fixArityTm : {vars : _} ->
             {auto c : Ref Ctxt Defs} ->
             CExp vars -> List (CExp vars) -> Core (CExp vars)
fixArityTm (CRef fc n) args
    = do defs <- get Ctxt
         Just gdef <- lookupCtxtExact n (gamma defs)
              | Nothing => pure (unload args (CRef fc n))
         let arity = case compexpr gdef of
                          Just def => getArity def
                          _ => 0
         pure $ expandToArity arity (CApp fc (CRef fc n) []) args
fixArityTm (CLam fc x sc) args
    = pure $ expandToArity Z (CLam fc x !(fixArityTm sc [])) args
fixArityTm (CLet fc x inl val sc) args
    = pure $ expandToArity Z
                 (CLet fc x inl !(fixArityTm val []) !(fixArityTm sc [])) args
fixArityTm (CApp fc f fargs) args
    = fixArityTm f (!(traverse (\tm => fixArityTm tm []) fargs) ++ args)
fixArityTm (CCon fc n ci t args) []
    = pure $ CCon fc n ci t !(traverse (\tm => fixArityTm tm []) args)
fixArityTm (COp fc op args) []
    = pure $ COp fc op !(traverseArgs args)
  where
    traverseArgs : {vs : _} ->
                   Vect n (CExp vs) -> Core (Vect n (CExp vs))
    traverseArgs [] = pure []
    traverseArgs (a :: as) = pure $ !(fixArityTm a []) :: !(traverseArgs as)
fixArityTm (CExtPrim fc p args) []
    = pure $ CExtPrim fc p !(traverse (\tm => fixArityTm tm []) args)
fixArityTm (CForce fc lr tm) args
    = pure $ expandToArity Z (CForce fc lr !(fixArityTm tm [])) args
fixArityTm (CDelay fc lr tm) args
    = pure $ expandToArity Z (CDelay fc lr !(fixArityTm tm [])) args
fixArityTm (CConCase fc sc alts def) args
    = pure $ expandToArity Z
              (CConCase fc !(fixArityTm sc [])
                           !(traverse fixArityAlt alts)
                           !(traverseOpt (\tm => fixArityTm tm []) def)) args
  where
    fixArityAlt : CConAlt vars -> Core (CConAlt vars)
    fixArityAlt (MkConAlt n ci t a sc)
        = pure $ MkConAlt n ci t a !(fixArityTm sc [])
fixArityTm (CConstCase fc sc alts def) args
    = pure $ expandToArity Z
              (CConstCase fc !(fixArityTm sc [])
                             !(traverse fixArityConstAlt alts)
                             !(traverseOpt (\tm => fixArityTm tm []) def)) args
  where
    fixArityConstAlt : CConstAlt vars -> Core (CConstAlt vars)
    fixArityConstAlt (MkConstAlt c sc)
        = pure $ MkConstAlt c !(fixArityTm sc [])
fixArityTm t [] = pure t
fixArityTm t args = pure $ expandToArity Z t args

export
fixArityExp : {vars : _} ->
              {auto c : Ref Ctxt Defs} ->
              CExp vars -> Core (CExp vars)
fixArityExp tm = fixArityTm tm []

fixArity : {auto c : Ref Ctxt Defs} ->
           CDef -> Core CDef
fixArity (MkFun args exp) = pure $ MkFun args !(fixArityTm exp [])
fixArity (MkError exp) = pure $ MkError !(fixArityTm exp [])
fixArity d = pure d

-- TODO: get rid of this `done` by making the return `args'` runtime irrelevant?
getLams : {done : _} ->
          Int -> SubstCEnv done args -> CExp (done ++ args) ->
          (args' ** (SubstCEnv args' args, CExp (args' ++ args)))
getLams {done} i env (CLam fc x sc)
    = getLams {done = x :: done} (i + 1) (CRef fc (MN "ext" i) :: env) sc
getLams {done} i env sc = (done ** (env, sc))

mkBounds : (xs : _) -> Bounds xs
mkBounds [] = None
mkBounds (x :: xs) = Add x x (mkBounds xs)

getNewArgs : {done : _} ->
             SubstCEnv done args -> List Name
getNewArgs [] = []
getNewArgs (CRef _ n :: xs) = n :: getNewArgs xs
getNewArgs {done = x :: xs} (_ :: sub) = x :: getNewArgs sub

-- Move any lambdas in the body of the definition into the lhs list of vars.
-- Annoyingly, the indices will need fixing up because the order in the top
-- level definition goes left to right (i.e. first argument has lowest index,
-- not the highest, as you'd expect if they were all lambdas).
mergeLambdas : (args : List Name) -> CExp args -> (args' ** CExp args')
mergeLambdas args (CLam fc x sc)
    = let (args' ** (env, exp')) = getLams 0 [] (CLam fc x sc)
          expNs = substs env exp'
          newArgs = reverse $ getNewArgs env
          expLocs = mkLocals (mkSizeOf args) {vars = []} (mkBounds newArgs)
                             (rewrite appendNilRightNeutral args in expNs) in
          (_ ** expLocs)
mergeLambdas args exp = (args ** exp)

doEval : {args : _} ->
         {auto c : Ref Ctxt Defs} ->
         Name -> CExp args -> Core (CExp args)
doEval n exp
    = do l <- newRef LVar (the Int 0)
         log "compiler.inline.eval" 10 (show n ++ ": " ++ show exp)
         exp' <- eval [] [] [] exp
         log "compiler.inline.eval" 10 ("Inlined: " ++ show exp')
         pure exp'

inline : {auto c : Ref Ctxt Defs} ->
         Name -> CDef -> Core CDef
inline n (MkFun args def)
    = pure $ MkFun args !(doEval n def)
inline n d = pure d

-- merge lambdas from expression into top level arguments
mergeLam : {auto c : Ref Ctxt Defs} ->
           CDef -> Core CDef
mergeLam (MkFun args def)
    = do let (args' ** exp') = mergeLambdas args def
         pure $ MkFun args' exp'
mergeLam d = pure d

mutual
  addRefs : NameMap Bool -> CExp vars -> NameMap Bool
  addRefs ds (CRef _ n) = insert n False ds
  addRefs ds (CLam _ _ sc) = addRefs ds sc
  addRefs ds (CLet _ _ _ val sc) = addRefs (addRefs ds val) sc
  addRefs ds (CApp _ f args) = addRefsArgs (addRefs ds f) args
  addRefs ds (CCon _ n _ _ args) = addRefsArgs (insert n False ds) args
  addRefs ds (COp _ _ args) = addRefsArgs ds (toList args)
  addRefs ds (CExtPrim _ _ args) = addRefsArgs ds args
  addRefs ds (CForce _ _ e) = addRefs ds e
  addRefs ds (CDelay _ _ e) = addRefs ds e
  addRefs ds (CConCase _ sc alts def)
      = let ds' = maybe ds (addRefs ds) def in
            addRefsConAlts (addRefs ds' sc) alts
  addRefs ds (CConstCase _ sc alts def)
      = let ds' = maybe ds (addRefs ds) def in
            addRefsConstAlts (addRefs ds' sc) alts
  addRefs ds tm = ds

  addRefsArgs : NameMap Bool -> List (CExp vars) -> NameMap Bool
  addRefsArgs ds [] = ds
  addRefsArgs ds (a :: as) = addRefsArgs (addRefs ds a) as

  addRefsConAlts : NameMap Bool -> List (CConAlt vars) -> NameMap Bool
  addRefsConAlts ds [] = ds
  addRefsConAlts ds (MkConAlt _ _ _ _ sc :: rest)
      = addRefsConAlts (addRefs ds sc) rest

  addRefsConstAlts : NameMap Bool -> List (CConstAlt vars) -> NameMap Bool
  addRefsConstAlts ds [] = ds
  addRefsConstAlts ds (MkConstAlt _ sc :: rest)
      = addRefsConstAlts (addRefs ds sc) rest

getRefs : CDef -> NameMap Bool
getRefs (MkFun args exp) = addRefs empty exp
getRefs _ = empty

export
inlineDef : {auto c : Ref Ctxt Defs} ->
            Name -> Core ()
inlineDef n
    = do defs <- get Ctxt
         Just def <- lookupCtxtExact n (gamma defs) | Nothing => pure ()
         let Just cexpr = compexpr def              | Nothing => pure ()
         setCompiled n !(inline n cexpr)

-- Update the names a function refers to at runtime based on the transformation
-- results (saves generating code unnecessarily).
updateCallGraph : {auto c : Ref Ctxt Defs} ->
                  Name -> Core ()
updateCallGraph n
    = do defs <- get Ctxt
         Just def <- lookupCtxtExact n (gamma defs) | Nothing => pure ()
         let Just cexpr =  compexpr def             | Nothing => pure ()
         let refs = getRefs cexpr
         ignore $ addDef n (record { refersToRuntimeM = Just refs } def)

export
fixArityDef : {auto c : Ref Ctxt Defs} ->
              Name -> Core ()
fixArityDef n
    = do defs <- get Ctxt
         Just def <- lookupCtxtExact n (gamma defs) | Nothing => pure ()
         let Just cexpr =  compexpr def             | Nothing => pure ()
         setCompiled n !(fixArity cexpr)

export
mergeLamDef : {auto c : Ref Ctxt Defs} ->
              Name -> Core ()
mergeLamDef n
    = do defs <- get Ctxt
         Just def <- lookupCtxtExact n (gamma defs)
              | Nothing => pure ()
         let PMDef pi _ _ _ _ = definition def
              | _ => pure ()
         if not (isNil (incrementalCGs !getSession)) &&
                externalDecl pi -- better keep it at arity 0
            then pure ()
            else do let Just cexpr =  compexpr def
                             | Nothing => pure ()
                    setCompiled n !(mergeLam cexpr)

export
addArityHash : {auto c : Ref Ctxt Defs} ->
               Name -> Core ()
addArityHash n
    = do defs <- get Ctxt
         Just def <- lookupCtxtExact n (gamma defs) | Nothing => pure ()
         let Just cexpr =  compexpr def             | Nothing => pure ()
         let MkFun args _ = cexpr                   | _ => pure ()
         addHash (n, length args)

export
compileAndInlineAll : {auto c : Ref Ctxt Defs} ->
                      Core ()
compileAndInlineAll
    = do defs <- get Ctxt
         let ns = keys (toIR defs)
         cns <- filterM nonErased ns

         traverse_ compileDef cns
         traverse_ setIdentity cns
         transform 3 cns -- number of rounds to run transformations.
                         -- This seems to be the point where not much useful
                         -- happens any more.
         traverse_ updateCallGraph cns
         -- in incremental mode, add the arity of the definitions to the hash,
         -- because if these change we need to recompile dependencies
         -- accordingly
         when (not (isNil (incrementalCGs !getSession))) $
           traverse_ addArityHash cns
  where
    transform : Nat -> List Name -> Core ()
    transform Z cns = pure ()
    transform (S k) cns
        = do traverse_ inlineDef cns
             traverse_ mergeLamDef cns
             traverse_ caseLamDef cns
             traverse_ fixArityDef cns
             transform k cns

    nonErased : Name -> Core Bool
    nonErased n
        = do defs <- get Ctxt
             Just gdef <- lookupCtxtExact n (gamma defs)
                  | Nothing => pure False
             pure (multiplicity gdef /= erased)


text:
module Control.Comonad.Env.Interface

import Control.Comonad
import Control.Comonad.Env.Env
import Control.Comonad.Store.Store
import Control.Comonad.Traced.Traced
import Control.Comonad.Trans

%default total

public export
interface Comonad w => ComonadEnv e w | w where
  ask : w a -> e

public export %inline
asks : ComonadEnv e w => (e -> e') -> w a -> e'
asks = (. ask)

public export %inline
lowerAsk : (ComonadEnv e w, ComonadTrans t) => t w a -> e
lowerAsk = ask . lower

--------------------------------------------------------------------------------
--          Implementations
--------------------------------------------------------------------------------

public export %inline
Comonad w => ComonadEnv e (EnvT e w) where
  ask = env

public export %inline
ComonadEnv e w => ComonadEnv e (StoreT t w) where
  ask = lowerAsk {t = StoreT t}

public export %inline
(ComonadEnv e w, Monoid m) => ComonadEnv e (TracedT m w) where
  ask = lowerAsk {t = TracedT m}

ext: idr


text:
test3ok : Nat
test3ok = case (the Nat 1, the Nat 2) of
               (x, y) => x + y

test3ok' : Nat
test3ok' = case (1, 2) of
             (x, y) => x + y


text:
module System

import public Data.So
import Data.List
import Data.Strings

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

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

%foreign support "idris2_sleep"
prim__sleep : Int -> PrimIO ()
%foreign support "idris2_usleep"
prim__usleep : Int -> PrimIO ()

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

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

-- This one is going to vary for different back ends. Probably needs a
-- better convention. Will revisit...
%foreign "scheme:blodwen-args"
         "node:lambda:() => __prim_js2idris_array(process.argv.slice(1))"
prim__getArgs : PrimIO (List String)

export
getArgs : HasIO io => io (List String)
getArgs = primIO prim__getArgs

%foreign libc "getenv"
         "node:lambda: n => process.env[n]"
prim__getEnv : String -> PrimIO (Ptr String)

%foreign support "idris2_getEnvPair"
prim__getEnvPair : Int -> PrimIO (Ptr String)
%foreign support "idris2_setenv"
prim__setEnv : String -> String -> Int -> PrimIO Int
%foreign support "idris2_unsetenv"
prim__unsetEnv : String -> PrimIO Int

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

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

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

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

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

%foreign libc "system"
         "scheme:blodwen-system"
prim__system : String -> PrimIO Int

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

%foreign support "idris2_time"
         "scheme:blodwen-time"
prim__time : PrimIO Int

export
time : HasIO io => io Integer
time = pure $ cast !(primIO prim__time)

%foreign libc "exit"
         "node:lambda:c => process.exit(Number(c))"
prim__exit : Int -> PrimIO ()

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

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

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

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


text:
module Control.Permutation.Proofs

import Control.Permutation.Mod
import Data.Nat

||| Proof that (n + 1)! >= n!
export
factorialIncr : (n : Nat) -> LTE (factorial n) (factorial (S n))
factorialIncr Z = reflexive {x = S Z}
factorialIncr n = lteAddRight (factorial n)

||| Proof that n! >= 1
export
factorialLTE : (n : Nat) -> LTE 1 (factorial n)
factorialLTE Z = ?base_hole
factorialLTE (S k) = transitive {x=S Z} (factorialLTE k) (factorialIncr k)

max_stars_repo_name: vmchale/permutations

max_issues_repo_name: vmchale/permutation

max_forks_repo_name: vmchale/permutation


text:
-- SPDX-FileCopyrightText: 2021 The ipkg-idr developers
--
-- SPDX-License-Identifier: MPL-2.0

module Language.IPKG.Parser

import Language.IPKG.Tokens
import Language.IPKG.Value

import Text.Parser
import Text.Token

import Data.List
import Data.List1

%default total

private
punct : Punctuation -> Grammar IPKGToken True ()
punct p = match $ ITPunct p

private
string : Grammar IPKGToken True String
string = match ITString

private
bare : Grammar IPKGToken True Identifier
bare = match ITBare

private
moduleIdent : Grammar IPKGToken True ModuleIdent
moduleIdent = sepBy1 (punct Dot) bare

private
keyEq : Key -> Grammar IPKGToken True ()
keyEq k = do
    k' <- match (ITKey k)
    commit
    punct Equal
    pure ()

private
keyVal : (key : Key) -> (val : Grammar IPKGToken True a) -> (update : a -> PkgDesc) -> Grammar IPKGToken True PkgDesc
keyVal key val update = do
    keyEq key
    v <- val
    pure $ update v

private
field : (p : PkgDesc) -> Grammar IPKGToken True PkgDesc
field p =
        keyVal KVersion string (\s => { version := s } p)
    <|> keyVal KAuthors string (\s => { authors := s } p)

    <|> keyVal KMaintainers string (\s => { maintainers := Just s } p)

    <|> keyVal KLicense string (\s => { license := Just s } p)
    <|> keyVal KBrief string (\s => { brief := Just s } p)
    <|> keyVal KReadme string (\s => { readme := Just s } p)
    <|> keyVal KHomepage string (\s => { homepage := Just s } p)
    <|> keyVal KSourceLoc string (\s => { sourceloc := Just s } p)
    <|> keyVal KBugtracker string (\s => { bugtracker := Just s } p)

    <|> keyVal KDepends (sepBy1 (punct Comma) bare) (\m => { depends := forget m } p)
    <|> keyVal KModules (sepBy1 (punct Comma) moduleIdent) (\m => { modules := forget m } p)

    <|> keyVal KMainMod moduleIdent (\s => { mainmod := Just s } p)

    <|> keyVal KExecutable (string <|> bare) (\s => { executable := Just s } p)
    <|> keyVal KOptions string (\s => { options := Just s } p)
    <|> keyVal KSourceDir string (\s => { sourcedir := Just s } p)
    <|> keyVal KBuildDir string (\s => { builddir := Just s } p)
    <|> keyVal KOutputDir string (\s => { outputdir := Just s } p)

    <|> keyVal KPreBuild string (\s => { prebuild := Just s } p)
    <|> keyVal KPostBuild string (\s => { postbuild := Just s } p)
    <|> keyVal KPreInstall string (\s => { preinstall := Just s } p)
    <|> keyVal KPostInstall string (\s => { postinstall := Just s } p)
    <|> keyVal KPreClean string (\s => { preclean := Just s } p)
    <|> keyVal KPostClean string (\s => { postclean := Just s } p)

private
fields : (p : PkgDesc) -> Grammar IPKGToken False PkgDesc
fields p = (eof >>= \_ => pure p)
       <|> (field p >>= fields)

private
packageDesc : Grammar IPKGToken True PkgDesc
packageDesc = do
    match ITPackage
    name <- bare

    pkg <- pure $ MkPkgDesc {
                name = name,
                version = "",
                authors = "",

                maintainers = Nothing,
                license     = Nothing,
                brief       = Nothing,
                readme      = Nothing,
                homepage    = Nothing,
                sourceloc   = Nothing,
                bugtracker  = Nothing,
                depends     = [],
                modules     = [],
                mainmod     = Nothing,
                executable  = Nothing,
                options     = Nothing,
                sourcedir   = Nothing,
                builddir    = Nothing,
                outputdir   = Nothing,
                prebuild    = Nothing,
                postbuild   = Nothing,
                preinstall  = Nothing,
                postinstall = Nothing,
                preclean    = Nothing,
                postclean   = Nothing
            }

    fields pkg <* eof

export
parseIPKGFromToks : (toks : List IPKGToken) -> Either String PkgDesc
parseIPKGFromToks toks = case parse packageDesc $ filter (not . ignored) toks of
    Right (pkg, []) => Right pkg
    Right _ => Left "unconsumed input"
    Left (Error msg _) => Left msg

max_stars_repo_name: tiatomee/ipkg-idr

max_issues_repo_name: tiatomee/ipkg-idr

max_forks_repo_name: tiatomee/ipkg-idr


text:
module Tools.AstF

public export
interface AstF (idx : Type) (f : (idx -> Type) -> (idx -> Type)) where
  localMap : (f1 : idx -> Type) -> (f2 : idx -> Type) -> ((i : idx) -> f1 i -> f2 i)
          -> (i : idx) -> f f1 i -> f f2 i
  -- TODO find a food localFold
  -- localFold : Monoid m => (i : idx) -> f (\_ => m) i -> m


text:
module Crypto.Sodium

import Crypto.RawSodium

%access public

-- Key generation

abstract data Key = MkKey ManagedPtr

newKey : (len : Int) -> IO Key
newKey l = return $ MkKey !(do_newKey l)

newSymmKey : IO Key
newSymmKey = do len <- secretbox_keyLength
                newKey len

newSecretKey : IO Key
newSecretKey = do len <- box_secretKeyLength
                  newKey len

newPublicKey : IO Key
newPublicKey = do len <- box_publicKeyLength
                  newKey len

newKeyPair : IO (Key, Key)
newKeyPair = do kp <- do_newKeyPair
                pk <- do_getPublic kp
                sk <- do_getSecret kp
                do_freeKeyPair kp
                return (MkKey pk, MkKey sk)

keyLen : Key -> Int
keyLen (MkKey k) = unsafePerformIO (do_getKeyLen k)

keyIdx : Key -> Int -> Int
keyIdx (MkKey k) i = unsafePerformIO (do_getKeyIdx k i)

setKeyIdx : Key -> Int -> Int -> IO ()
setKeyIdx (MkKey k) i b = do_setKeyIdx k i b

-- Nonces

abstract data Nonce = MkNonce ManagedPtr

newNonce : (len : Int) -> IO Nonce
newNonce l = return $ MkNonce !(do_newNonce l)

newNonceFromString : (str : String) -> IO Nonce
newNonceFromString str = return $ MkNonce !(do_newNonceFromString str)

setNonceIdx : Nonce -> Int -> Int -> IO ()
setNonceIdx (MkNonce k) i b = do_setNonceIdx k i b

-- An Encrypted box holds raw encrypted data, and its length
abstract
data EncryptedBox = MkEnc ManagedPtr | EncFailed

newSymmBox : Int -> IO EncryptedBox
newSymmBox l = return $ MkEnc !(do_newSecretBox l)

newBox : Int -> IO EncryptedBox
newBox l = return $ MkEnc !(do_newBox l)

getBoxLen : EncryptedBox -> Int
getBoxLen (MkEnc e) = unsafePerformIO $ do_getBoxLen e

getBoxIdx : EncryptedBox -> Int -> Int
getBoxIdx (MkEnc e) i = unsafePerformIO $ do_getBoxIdx e i

getBytes : EncryptedBox -> List Int
getBytes e = getAll [] 0 (getBoxLen e)
   where getAll : List Int -> Int -> Int -> List Int
         getAll acc i len
             = if i == len
                  then reverse acc
                  else getAll (getBoxIdx e i :: acc) (i + 1) len

abstract validBox : EncryptedBox -> Bool
validBox (MkEnc e) = True
validBox EncFailed = False

-- freeBox : EncryptedBox -> IO ()
-- freeBox (MkEnc e) = do_freeBox e

-- An open box holds plain text, and its length
abstract data OpenBox = MkDec ManagedPtr | DecFailed

abstract readBox : OpenBox -> String
readBox (MkDec p) = unsafePerformIO (do_readBoxOpen p)

abstract validOpenBox : OpenBox -> Bool
validOpenBox (MkDec e) = True
validOpenBox DecFailed = False

-- freeOpenBox : OpenBox -> IO ()
-- freeOpenBox (MkDec e) = do_freeBoxOpen e

-- Nonce lengths

abstract symmNonceLength : Int
symmNonceLength = unsafePerformIO secretbox_nonceLength

abstract nonceLength : Int
nonceLength = unsafePerformIO box_nonceLength

-- Symmetric key encryption

cryptoSecretBox : (plaintext : String) -> (nonce : Nonce) ->
                  (key : Key) -> IO EncryptedBox
cryptoSecretBox m (MkNonce n) (MkKey k)
    = case !(do_cryptoSecretBox m n k) of
           Just p => return (MkEnc p)
           Nothing => return EncFailed

cryptoSecretBoxOpen : (ciphertext : EncryptedBox) -> (nonce : Nonce) ->
                      (key : Key) -> IO OpenBox
cryptoSecretBoxOpen (MkEnc e) (MkNonce n) (MkKey k)
    = case !(do_cryptoSecretBoxOpen e n k) of
           Just p => return (MkDec p)
           Nothing => return DecFailed

-- Public key encryption

cryptoBox : (plaintext : String) -> (nonce : Nonce) ->
            (pkey : Key) -> (skey : Key) -> IO EncryptedBox
cryptoBox m (MkNonce n) (MkKey pk) (MkKey sk)
    = case !(do_cryptoBox m n pk sk) of
           Just p => return (MkEnc p)
           Nothing => return EncFailed

cryptoBoxOpen : (ciphertext : EncryptedBox) -> (nonce : Nonce) ->
                (pkey : Key) -> (skey : Key) -> IO OpenBox
cryptoBoxOpen (MkEnc e) (MkNonce n) (MkKey pk) (MkKey sk)
    = case !(do_cryptoBoxOpen e n pk sk) of
           Just p => return (MkDec p)
           Nothing => return DecFailed

max_stars_repo_name: edwinb/sodium-idris

max_issues_repo_name: edwinb/sodium-idris

max_forks_repo_name: edwinb/sodium-idris


text:
module Ex5

import Data.Strings
import Data.Vect
import System
import System.File

%default total

printLonger : HasIO io => io ()
printLonger = do putStr "Enter the first string: "
                 first <- getLine
                 putStr "Enter the second string: "
                 second <- getLine
                 let firstlen = length first -- no `in` here
                 let secondlen = length second
                 putStrLn $ show (max firstlen secondlen)

printLongerBind : HasIO io => io ()
printLongerBind = putStr "Enter the first string: " >>= \_ =>
                    getLine >>= \first =>
                      putStr "Enter the second string: " >>= \_ =>
                        getLine >>= \second =>
                          let firstlen = length first
                              secondlen = length second in -- `in` is used here - why the inconsistency?
                            putStrLn (show (max firstlen secondlen))

readNumber : HasIO io => io (Maybe Nat)
readNumber = do ns <- getLine
                if all isDigit (unpack ns)
                   then pure $ Just (stringToNatOrZ ns)
                   else pure Nothing

-- guess the number game
partial
guess : HasIO io => (n : Nat) -> (guesses : Nat) -> io ()
guess secret count = do putStr "Enter your guess: "
                        Just g <- readNumber
                          | Nothing => do putStrLn "Invalid input: not a number"
                                          pure ()
                        case compare g secret of
                             LT => do putStrLn "Too low!"
                                      guess secret (count + 1)
                             GT => do putStrLn "Too high!"
                                      guess secret (count + 1)
                             EQ => do putStrLn $ "You win! You took " ++ show (count + 1) ++ " guesses!"
                                      pure ()

partial
guessingGame : HasIO io => io ()
guessingGame = do currTime <- time
                  let secret = currTime `mod` 101 + 1 -- secret in [1, 100]
                  guess (integerToNat secret) 0

partial
myRepl : HasIO io => String -> (String -> String) -> io ()
myRepl prompt func = do putStr prompt
                        inp <- getLine
                        putStr (func inp)
                        myRepl prompt func

partial
reverser : HasIO io => io ()
reverser = myRepl "Enter a string: " (\s => reverse s ++ "\n")

partial
myReplWith : HasIO io => a -> String -> (a -> String -> Maybe (String, a)) -> io ()
myReplWith state prompt func = do putStr prompt
                                  inp <- getLine
                                  case func state inp of
                                       Nothing => pure ()
                                       Just (out, newState) => do putStr out
                                                                  myReplWith newState prompt func

partial
adder : HasIO io => io ()
adder = myReplWith 0 "Enter a number: " (\acc, s => case all isDigit (unpack s) of
                                                         False => Nothing
                                                         True => let n = stringToNatOrZ s in
                                                                     Just $ ("Current value: " ++ show (acc + n) ++ "\n", acc + n))

partial
readToBlank : HasIO io => io (List String)
readToBlank = do line <- getLine
                 if line == ""
                    then pure []
                    else do lines <- readToBlank
                            pure (line :: lines)

partial
readAndSave : HasIO io => io ()
readAndSave = do lines <- readToBlank
                 filename <- getLine
                 Right () <- writeFile filename (unwords (map (\line => line ++ "\n") lines))
                  | Left err => putStrLn $ "Error while writing to file: " ++ show err
                 putStrLn "Wrote to file successfully"

partial
printFile : HasIO io => io ()
printFile = do filename <- getLine
               Right contents <- readFile filename
                | Left err => putStrLn $ "Error while reading file: " ++ show err
               putStrLn contents

partial
readVectFile : (filename : String) -> IO (n ** Vect n String)
readVectFile filename = do Right handle <- openFile filename Read
                            | Left err => do putStrLn $ "error while reading file: " ++ show err
                                             pure (_ ** [])
                           readFileHelper handle
  where
    partial
    readFileHelper : File -> IO (n ** Vect n String)
    readFileHelper handle = do end <- fEOF handle
                               if end
                                  then pure (_ ** [])
                                  else do Right line <- fGetLine handle
                                            | Left err => do putStrLn $ "error while reading line from file: " ++ show err
                                                             pure (_ ** [])
                                          do (_ ** lines) <- readFileHelper handle
                                             pure (_ ** (line :: lines))

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:
module Utils.String

import Data.String.Extra

export
show_record : String -> List (String, String) -> String
show_record name x = name <+> " { " <+> (join ", " $ map (\(k, v) => k <+> " = " <+> v) x) <+> " }"


text:
module Idris.ProcessIdr

import Compiler.Inline

import Core.Binary
import Core.Context
import Core.Context.Log
import Core.Directory
import Core.Env
import Core.Hash
import Core.Metadata
import Core.Options
import Core.Unify

import Parser.Unlit

import TTImp.Elab.Check
import TTImp.ProcessDecls
import TTImp.TTImp

import Idris.Desugar
import Idris.Parser
import Idris.REPLCommon
import Idris.REPLOpts
import Idris.Syntax
import Idris.Pretty

import Data.List
import Data.NameMap

import System.File

%default covering

processDecl : {auto c : Ref Ctxt Defs} ->
              {auto u : Ref UST UState} ->
              {auto s : Ref Syn SyntaxInfo} ->
              {auto m : Ref MD Metadata} ->
              PDecl -> Core (Maybe Error)
processDecl decl
    = catch (do impdecls <- desugarDecl [] decl
                traverse (Check.processDecl [] (MkNested []) []) impdecls
                pure Nothing)
            (\err => do giveUpConstraints -- or we'll keep trying...
                        pure (Just err))

processDecls : {auto c : Ref Ctxt Defs} ->
               {auto u : Ref UST UState} ->
               {auto s : Ref Syn SyntaxInfo} ->
               {auto m : Ref MD Metadata} ->
               List PDecl -> Core (List Error)
processDecls decls
    = do xs <- traverse processDecl decls
         Nothing <- checkDelayedHoles
             | Just err => pure (case mapMaybe id xs of
                                      [] => [err]
                                      errs => errs)
         errs <- getTotalityErrors
         pure (mapMaybe id xs ++ errs)

export
readModule : {auto c : Ref Ctxt Defs} ->
             {auto u : Ref UST UState} ->
             {auto s : Ref Syn SyntaxInfo} ->
             (full : Bool) -> -- load everything transitively (needed for REPL and compiling)
             FC ->
             (visible : Bool) -> -- Is import visible to top level module?
             (imp : ModuleIdent) -> -- Module name to import
             (as : Namespace) -> -- Namespace to import into
             Core ()
readModule full loc vis imp as
    = do defs <- get Ctxt
         let False = (imp, vis, as) `elem` map snd (allImported defs)
             | True => when vis (setVisible (miAsNamespace imp))
         Right fname <- nsToPath loc imp
               | Left err => throw err
         Just (syn, hash, more) <- readFromTTC False {extra = SyntaxInfo}
                                                  loc vis fname imp as
              | Nothing => when vis (setVisible (miAsNamespace imp)) -- already loaded, just set visibility
         extendSyn syn

         defs <- get Ctxt
         modNS <- getNS
         when vis $ setVisible (miAsNamespace imp)
         traverse_ (\ mimp =>
                       do let m = fst mimp
                          let reexp = fst (snd mimp)
                          let as = snd (snd mimp)
                          when (reexp || full) $ readModule full loc reexp m as) more
         setNS modNS

readImport : {auto c : Ref Ctxt Defs} ->
             {auto u : Ref UST UState} ->
             {auto s : Ref Syn SyntaxInfo} ->
             Bool -> Import -> Core ()
readImport full imp
    = do readModule full (loc imp) True (path imp) (nameAs imp)
         addImported (path imp, reexport imp, nameAs imp)

||| Adds new import to the namespace without changing the current top-level namespace
export
addImport : {auto c : Ref Ctxt Defs} ->
            {auto u : Ref UST UState} ->
            {auto s : Ref Syn SyntaxInfo} ->
            Import -> Core ()
addImport imp
    = do topNS <- getNS
         readImport True imp
         setNS topNS

readHash : {auto c : Ref Ctxt Defs} ->
           {auto u : Ref UST UState} ->
           Import -> Core (Bool, (Namespace, Int))
readHash imp
    = do Right fname <- nsToPath (loc imp) (path imp)
               | Left err => throw err
         h <- readIFaceHash fname
         pure (reexport imp, (nameAs imp, h))

prelude : Import
prelude = MkImport (MkFC "(implicit)" (0, 0) (0, 0)) False
                     (nsAsModuleIdent preludeNS) preludeNS

export
readPrelude : {auto c : Ref Ctxt Defs} ->
              {auto u : Ref UST UState} ->
              {auto s : Ref Syn SyntaxInfo} ->
              Bool -> Core ()
readPrelude full
    = do readImport full prelude
         setNS mainNS

-- Import a TTC for use as the main file (e.g. at the REPL)
export
readAsMain : {auto c : Ref Ctxt Defs} ->
             {auto u : Ref UST UState} ->
             {auto s : Ref Syn SyntaxInfo} ->
             (fname : String) -> Core ()
readAsMain fname
    = do Just (syn, _, more) <- readFromTTC {extra = SyntaxInfo}
                                             True toplevelFC True fname (nsAsModuleIdent emptyNS) emptyNS
              | Nothing => throw (InternalError "Already loaded")
         replNS <- getNS
         replNestedNS <- getNestedNS
         extendSyn syn

         -- Read the main file's top level imported modules, so we have access
         -- to their names (and any of their public imports)
         ustm <- get UST
         traverse_ (\ mimp =>
                       do let m = fst mimp
                          let as = snd (snd mimp)
                          readModule True emptyFC True m as
                          addImported (m, True, as)) more

         -- also load the prelude, if required, so that we have access to it
         -- at the REPL.
         when (not (noprelude !getSession)) $
              readModule True emptyFC True (nsAsModuleIdent preludeNS) preludeNS

         -- We're in the namespace from the first TTC, so use the next name
         -- from that for the fresh metavariable name generation
         -- TODO: Maybe we should record this per namespace, since this is
         -- a little bit of a hack? Or maybe that will have too much overhead.
         ust <- get UST
         put UST (record { nextName = nextName ustm } ust)

         setNS replNS
         setNestedNS replNestedNS

addPrelude : List Import -> List Import
addPrelude imps
  = if not (nsAsModuleIdent preludeNS `elem` map path imps)
       then prelude :: imps
       else imps

-- Get a file's modified time. If it doesn't exist, return 0 (that is, it
-- was last modified at the dawn of time so definitely out of date for
-- rebuilding purposes...)
modTime : String -> Core Integer
modTime fname
    = do Right f <- coreLift $ openFile fname Read
             | Left err => pure 0 -- Beginning of Time :)
         Right t <- coreLift $ fileModifiedTime f
             | Left err => do coreLift $ closeFile f
                              pure 0
         coreLift $ closeFile f
         pure (cast t)

export
getParseErrorLoc : String -> ParseError Token -> FC
getParseErrorLoc fname (ParseFail _ (Just pos) _) = MkFC fname pos pos
getParseErrorLoc fname (LexFail (l, c, _)) = MkFC fname (l, c) (l, c)
getParseErrorLoc fname (LitFail (MkLitErr l c _)) = MkFC fname (l, 0) (l, 0)
getParseErrorLoc fname _ = replFC

export
readHeader : {auto c : Ref Ctxt Defs} ->
             (path : String) -> Core Module
readHeader path
    = do Right res <- coreLift (readFile path)
            | Left err => throw (FileErr path err)
         case runParserTo (isLitFile path) isColon res (progHdr path) of
              Left err => throw (ParseFail (getParseErrorLoc path err) err)
              Right mod => pure mod
  where
    -- Stop at the first :, that's definitely not part of the header, to
    -- save lexing the whole file unnecessarily
    isColon : WithBounds Token -> Bool
    isColon t
        = case t.val of
               Symbol ":" => True
               _ => False

%foreign "scheme:collect"
prim__gc : Int -> PrimIO ()

gc : IO ()
gc = primIO $ prim__gc 4

export
addPublicHash : {auto c : Ref Ctxt Defs} ->
                (Bool, (Namespace, Int)) -> Core ()
addPublicHash (True, (mod, h)) = do addHash mod; addHash h
addPublicHash _ = pure ()

-- Process everything in the module; return the syntax information which
-- needs to be written to the TTC (e.g. exported infix operators)
-- Returns 'Nothing' if it didn't reload anything
processMod : {auto c : Ref Ctxt Defs} ->
             {auto u : Ref UST UState} ->
             {auto s : Ref Syn SyntaxInfo} ->
             {auto m : Ref MD Metadata} ->
             {auto o : Ref ROpts REPLOpts} ->
             (srcf : String) -> (ttcf : String) -> (msg : Doc IdrisAnn) ->
             (sourcecode : String) ->
             Core (Maybe (List Error))
processMod srcf ttcf msg sourcecode
    = catch (do
        setCurrentElabSource sourcecode
        -- Just read the header to start with (this is to get the imports and
        -- see if we can avoid rebuilding if none have changed)
        modh <- readHeader srcf
        -- Add an implicit prelude import
        let imps =
             if (noprelude !getSession || moduleNS modh == nsAsModuleIdent preludeNS)
                then imports modh
                else addPrelude (imports modh)

        hs <- traverse readHash imps
        defs <- get Ctxt
        log "" 5 $ "Current hash " ++ show (ifaceHash defs)
        log "" 5 $ show (moduleNS modh) ++ " hashes:\n" ++
                show (sort (map snd hs))
        imphs <- readImportHashes ttcf
        log "" 5 $ "Old hashes from " ++ ttcf ++ ":\n" ++ show (sort imphs)

        -- If the old hashes are the same as the hashes we've just
        -- read from the imports, and the source file is older than
        -- the ttc, we can skip the rest.
        srctime <- modTime srcf
        ttctime <- modTime ttcf

        let ns = moduleNS modh

        if (sort (map snd hs) == sort imphs && srctime <= ttctime)
           then -- Hashes the same, source up to date, just set the namespace
                -- for the REPL
                do setNS (miAsNamespace ns)
                   pure Nothing
           else -- needs rebuilding
             do iputStrLn msg
                Right mod <- logTime ("++ Parsing " ++ srcf) $
                            pure (runParser (isLitFile srcf) sourcecode (do p <- prog srcf; eoi; pure p))
                      | Left err => pure (Just [ParseFail (getParseErrorLoc srcf err) err])
                initHash
                traverse addPublicHash (sort hs)
                resetNextVar
                when (ns /= nsAsModuleIdent mainNS) $
                   do let MkFC fname _ _ = headerloc mod
                      d <- getDirs
                      ns' <- pathToNS (working_dir d) (source_dir d) fname
                      when (ns /= ns') $
                          throw (GenericMsg (headerloc mod)
                                   ("Module name " ++ show ns ++
                                    " does not match file name " ++ fname))

                -- read import ttcs in full here
                -- Note: We should only import .ttc - assumption is that there's
                -- a phase before this which builds the dependency graph
                -- (also that we only build child dependencies if rebuilding
                -- changes the interface - will need to store a hash in .ttc!)
                logTime "++ Reading imports" $
                   traverse_ (readImport False) imps

                -- Before we process the source, make sure the "hide_everywhere"
                -- names are set to private (TODO, maybe if we want this?)
--                 defs <- get Ctxt
--                 traverse (\x => setVisibility emptyFC x Private) (hiddenNames defs)
                setNS (miAsNamespace ns)
                errs <- logTime "++ Processing decls" $
                            processDecls (decls mod)
--                 coreLift $ gc

                logTime "++ Compile defs" $ compileAndInlineAll

                -- Save the import hashes for the imports we just read.
                -- If they haven't changed next time, and the source
                -- file hasn't changed, no need to rebuild.
                defs <- get Ctxt
                put Ctxt (record { importHashes = map snd hs } defs)
                pure (Just errs))
          (\err => pure (Just [err]))

-- Process a file. Returns any errors, rather than throwing them, because there
-- might be lots of errors collected across a whole file.
export
process : {auto c : Ref Ctxt Defs} ->
          {auto m : Ref MD Metadata} ->
          {auto u : Ref UST UState} ->
          {auto s : Ref Syn SyntaxInfo} ->
          {auto o : Ref ROpts REPLOpts} ->
          Doc IdrisAnn -> FileName ->
          Core (List Error)
process buildmsg file
    = do Right res <- coreLift (readFile file)
               | Left err => pure [FileErr file err]
         catch (do ttcf <- getTTCFileName file "ttc"
                   Just errs <- logTime ("+ Elaborating " ++ file) $
                                   processMod file ttcf buildmsg res
                        | Nothing => pure [] -- skipped it
                   if isNil errs
                      then
                        do defs <- get Ctxt
                           d <- getDirs
                           ns <- pathToNS (working_dir d) (source_dir d) file
                           makeBuildDirectory ns
                           writeToTTC !(get Syn) ttcf
                           ttmf <- getTTCFileName file "ttm"
                           writeToTTM ttmf
                           pure []
                      else do pure errs)
               (\err => pure [err])


text:
module Main

import Test.Golden

%default covering

allTests : TestPool
allTests = MkTestPool []
  [ "messages001"
  ]

main : IO ()
main = runner
  [ testPaths "lsp" allTests
  ] where
    testPaths : String -> TestPool -> TestPool
    testPaths dir = record { testCases $= map ((dir ++ "/") ++) }


text:
-- ---------------------------------------------------------------- [ Effs.idr ]
-- Module    : Effs.idr
-- Copyright : (c) Jan de Muijnck-Hughes
-- License   : see LICENSE
-- --------------------------------------------------------------------- [ EOH ]
module Frigg.Effs

-- ----------------------------------------------------------------- [ Imports ]
import public Effects
import public Effect.System
import public Effect.State
import public Effect.Exception
import public Effect.File
import public Effect.StdIO

import XML.DOM

import ArgParse

import Config.INI

import Freyja

import Frigg.Options
import Frigg.Error

-- -------------------------------------------------------------- [ Directives ]

%access export

-- ------------------------------------------------------------------- [ State ]
public export
record FriggState where
  constructor MkFriggState
  opts : FriggOpts
  pdoc : Maybe PatternDoc
  xdoc : Maybe XMLDoc

Default FriggState where
  default = MkFriggState mkDefOpts Nothing Nothing

-- ----------------------------------------------------------------- [ Effects ]

public export
FriggEffs : List EFFECT
FriggEffs = [ FILE_IO ()
            , SYSTEM
            , STDIO
            , 'ferr     ::: EXCEPTION FriggError
            , 'fstate   ::: STATE FriggState
          ]

namespace Frigg
  raise : FriggError -> Eff b ['ferr ::: EXCEPTION FriggError]
  raise err = 'ferr :- Exception.raise err

public export
Frigg : Type -> Type
Frigg rTy = Eff rTy FriggEffs

getOptions : Eff FriggOpts ['fstate ::: STATE FriggState]
getOptions = pure $ opts !('fstate :- get)

putOptions : FriggOpts -> Eff () ['fstate ::: STATE FriggState]
putOptions o = 'fstate :- update (\st => record {opts = o} st)

processOptions : Frigg FriggOpts
processOptions =
    case parseArgs mkDefOpts convOpts !getArgs of
      Left err => Frigg.raise (ParseError (show err))
      Right  o => pure o

putPatternDoc : PatternDoc -> Eff () ['fstate ::: STATE FriggState]
putPatternDoc p = 'fstate :- update (\st => record {pdoc = Just p} st)

getPatternDoc : Frigg PatternDoc
getPatternDoc =
    case pdoc !('fstate :- get) of
      Nothing => Frigg.raise PatternDocMissing
      Just p  => pure p

getXMLDoc : Frigg XMLDoc
getXMLDoc =
    case xdoc !('fstate :- get) of
      Nothing => Frigg.raise PatternDocMissing
      Just x  => pure x

putXMLDoc : XMLDoc -> Eff () ['fstate ::: STATE FriggState]
putXMLDoc p = 'fstate :- update (\st => record {xdoc = Just p} st)

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

max_stars_repo_name: jfdm/frigg-tool

max_issues_repo_name: jfdm/frigg-tool

max_forks_repo_name: jfdm/frigg-tool


text:
module Main

import BTree
import Data.List
import Data.Stream

treesort : Ord a => List a -> List a
treesort xs = BTree.toList $ toTree xs

lincong : Integer -> Stream Integer
lincong = tail . (iterate (\n => (1103515245 * (fromInteger n) + 12345) `mod` 2147483648))

randishInts : Nat -> Integer -> List Integer
randishInts size seed = take size $ lincong seed

mylast : List a -> Maybe a
mylast [] = Nothing
mylast [x] = Just x
mylast (x::xs) = mylast xs

doSort : Nat -> IO ()
doSort Z     = putStrLn "Done"
doSort (S k) = do let xs = treesort $ randishInts 30000 $ natToInteger k
                  -- get last elem to make sure compiler doesn't optimise away the sort
                  putStrLn $ show $ mylast xs
                  doSort k

main : IO ()
main = do max <- getLine
          doSort (integerToNat (cast max))


text:
module Prelude.Either

||| Keep the payloads of all Left constructors in a list of Eithers
public export
lefts : List (Either a b) -> List a
lefts []      = []
lefts (x::xs) =
  case x of
    Left  l => l :: lefts xs
    Right r => lefts xs

||| Keep the payloads of all Right constructors in a list of Eithers
public export
rights : List (Either a b) -> List b
rights []      = []
rights (x::xs) =
  case x of
    Left  l => rights xs
    Right r => r :: rights xs

||| Split a list of Eithers into a list of the left elements and a list of the right elements
public export
partitionEithers : List (Either a b) -> (List a, List b)
partitionEithers l = (lefts l, rights l)

max_stars_repo_name: steshaw/hsgames

max_issues_repo_name: steshaw/hsgames

max_forks_repo_name: steshaw/hsgames


text:
module QuantityInDataDef

import Data.List

-- based on the datatype from Brady's lectures

data RunLength : (0 _ : List ty) -> Type where
  Empty : RunLength []
  Run : (n : Nat) -> (x : ty) -> RunLength more -> RunLength (replicate n x ++ more)
  Ruin : (x : List ty) -> RunLength x -- I wish I had a way to disallow this J_J

max_stars_repo_name: buzden/idris-playground

max_issues_repo_name: buzden/idris-playground

max_forks_repo_name: buzden/idris-playground


text:
> module Nat.DivisorProperties

> import Syntax.PreorderReasoning

> import Nat.Divisor
> import Nat.DivisorOperations
> import Basic.Operations
> import Nat.Operations
> import Nat.OperationsProperties
> import Sigma.Sigma
> import Pairs.Operations

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

> ||| Fundamental quotient lemma
> quotientLemma : (m : Nat) -> (d : Nat) -> (dDm : d `Divisor` m) -> d * (quotient m d dDm) = m
> quotientLemma m d (Element q prf) = prf
> %freeze quotientLemma

> ||| Fundamental quotient lemma
> quotientLemma' : (m : Nat) -> (d : Nat) -> (dDm : d `Divisor` m) -> (quotient m d dDm) * d = m
> quotientLemma' m d dDm = replace {P = \ ZUZ => ZUZ = m} (multCommutative d (quotient m d dDm)) (quotientLemma m d dDm)
> %freeze quotientLemma'

Properties of |Divisor|:

> ||| Any natural number is a divisor of zero
> anyDivisorZ : (m : Nat) -> m `Divisor` Z
> anyDivisorZ m = Element Z (multZeroRightZero m)
> %freeze anyDivisorZ

> ||| One is a divisor of any natural number
> oneDivisorAny : (m : Nat) -> (S Z) `Divisor` m
> oneDivisorAny m = Element m (multOneLeftNeutral m)
> %freeze oneDivisorAny

> ||| Any natural number is a divisor of itself
> anyDivisorAny : (m : Nat) -> m `Divisor` m
> anyDivisorAny m = Element (S Z) (multOneRightNeutral m)
> %freeze anyDivisorAny

> ||| |Divisor| is reflexive
> divisorReflexive : (m : Nat) -> m `Divisor` m
> divisorReflexive = anyDivisorAny
> %freeze divisorReflexive

> ||| |Divisor| is transitive
> divisorTransitive : l `Divisor` m -> m `Divisor` n -> l `Divisor` n
> divisorTransitive {l} {m} {n} (Element q1 p1) (Element q2 p2) = Element (q1 * q2) p where
>   s1 : (l * q1) * q2 = m * q2
>   s1 = multPreservesEq (l * q1) m q2 q2 p1 Refl
>   s2 : (l * q1) * q2 = n
>   s2 = trans s1 p2
>   p : l * (q1 * q2) = n
>   p = replace {x = (l * q1) * q2}
>               {y = l * (q1 * q2)}
>               {P = \ ZUZU => ZUZU = n}
>               (sym (multAssociative l q1 q2)) s2
> %freeze divisorTransitive

> ||| |Divisor| is antysymmetric
> divisorAntisymmetric : (m : Nat) -> (n : Nat) -> m `Divisor` n -> n `Divisor` m -> m = n
> divisorAntisymmetric  Z     Z     _               _              = Refl
> divisorAntisymmetric  Z    (S n) (Element q1 p1)  _              = absurd p1
> divisorAntisymmetric (S m)  Z     _              (Element q2 p2) = absurd p2
> divisorAntisymmetric (S m) (S n) (Element q1 p1) (Element q2 p2) = s8 where
>   s1 : (S m) * q1 = S n
>   s1 = p1
>   s2 : (S n) * q2 = S m
>   s2 = p2
>   s3 : ((S n) * q2) * q1 = S n
>   s3 = replace {x = S m}
>                {y = (S n) * q2}
>                {P = \ZUZU => ZUZU * q1 = S n}
>                (sym s2)
>                s1
>   s4 : (S n) * (q2 * q1) = S n
>   s4 = replace {x = ((S n) * q2) * q1}
>                {y = (S n) * (q2 * q1)}
>                {P = \ ZUZU => ZUZU = S n}
>                (sym (multAssociative (S n) q2 q1) ) s3
>   s5 : q2 * q1 = S Z
>   s5 = multElim1 n (q2 * q1) s4
>   s6 : q1 = S Z
>   s6 = multOneRightOne q2 q1 s5
>   s7 : (S m) * (S Z) = S n
>   s7 = replace {x = q1}
>                {y = S Z}
>                {P = \ ZUZU => (S m) * ZUZU = S n}
>                s6 s1
>   s8 : S m  = S n
>   s8 = replace {x = (S m) * (S Z)}
>                {y = S m}
>                {P = \ ZUZU => ZUZU = S n}
>                (multOneRightNeutral (S m)) s7
> %freeze divisorAntisymmetric

> ||| Any divisor of two numbers is a divisor of their sum
> divisorPlusLemma1 : (m : Nat) -> (n : Nat) -> (d : Nat) ->
>                     d `Divisor` m -> d `Divisor` n -> d `Divisor` (m + n)
> divisorPlusLemma1 m n d (Element q1 p1) (Element q2 p2) =
>   Element (q1 + q2) p where
>     s1 : d * (q1 + q2) = d * q1 + d * q2
>     s1 = multDistributesOverPlusRight d q1 q2
>     s2 : d * (q1 + q2) = m + d * q2
>     s2 = replace {x = d * q1} {y = m} {P = \ ZUZU => d * (q1 + q2) = ZUZU + d * q2} p1 s1
>     p : d * (q1 + q2) = m + n
>     p = replace {x = d * q2} {y = n} {P = \ ZUZU => d * (q1 + q2) = m + ZUZU} p2 s2
> --%freeze divisorPlusLemma1

> ||| Any divisor of two numbers is a divisor of their sum
> divisorPlusLemma2 : (m : Nat) -> (n : Nat) -> (d : Nat) ->
>                      d `Divisor` m -> d `Divisor` n -> d `Divisor` (n + m)
> divisorPlusLemma2 m n d (Element q1 p1) (Element q2 p2) =
>   Element (q1 + q2) p where
>     s1 : d * (q1 + q2) = d * q1 + d * q2
>     s1 = multDistributesOverPlusRight d q1 q2
>     s2 : d * (q1 + q2) = m + d * q2
>     s2 = replace {x = d * q1} {y = m} {P = \ ZUZU => d * (q1 + q2) = ZUZU + d * q2} p1 s1
>     s3 : d * (q1 + q2) = m + n
>     s3 = replace {x = d * q2} {y = n} {P = \ ZUZU => d * (q1 + q2) = m + ZUZU} p2 s2
>     p  : d * (q1 + q2) = n + m
>     p  = replace {x = m + n} {y = n + m} {P = \ ZUZU => d * (q1 + q2) = ZUZU} (plusCommutative m n) s3
> %freeze divisorPlusLemma2

> ||| The product of (two) divisors (of two natural numbers) is a divisor of the
> ||| product (of those numbers)
> divisorMultLemma1 : (m1 : Nat) -> (d1 : Nat) -> d1 `Divisor` m1 ->
>                     (m2 : Nat) -> (d2 : Nat) -> d2 `Divisor` m2 ->
>                     (d1 * d2) `Divisor` (m1 * m2)
> divisorMultLemma1 m1 d1 (Element q1 p1) m2 d2 (Element q2 p2) =
>   Element (q1 * q2) p where
>     s1 : (d1 * q1) * (d2 * q2) = m1 * m2
>     s1 = multPreservesEq (d1 * q1) m1 (d2 * q2) m2 p1 p2
>     p  : (d1 * d2) * (q1 * q2) = m1 * m2
>     p  = replace {x = (d1 * q1) * (d2 * q2)}
>                  {y = (d1 * d2) * (q1 * q2)}
>                  {P = \ ZUZU => ZUZU = m1 * m2}
>                  (multFlipCentre d1 q1 d2 q2) s1
> -- %freeze divisorMultLemma1

> ||| Any divisor of two numbers is a divisor of their difference
> divisorMinusLemma : (m : Nat) -> (n : Nat) -> (d : Nat) ->
>                     d `Divisor` m -> d `Divisor` n -> d `Divisor` (n - m)
> divisorMinusLemma m n d (Element q1 p1) (Element q2 p2) =
>   Element q p where
>     q : Nat
>     q = q2 - q1
>     p : d * q = n - m
>     p = s2 where
>       s1 : d * q2 - d * q1 = n - m
>       s1 = cong2 p2 p1
>       s2 : d * (q2 - q1) = n - m
>       s2 = replace {x = d * q2 - d * q1}
>                    {y = d * (q2 - q1)}
>                    {P = \ZUZU => ZUZU = n - m}
>                    (sym (multDistributesOverMinusRight d q2 q1))
>                    s1
> %freeze divisorMinusLemma

> |||
> divisorOneLemma : (d : Nat) -> (d' : Nat) -> (S d) * d' `Divisor` (S d) -> d' `Divisor` S Z
> divisorOneLemma d d' (Element q p) =
>   Element q p' where
>     s1 : ((S d) * d') * q = S d
>     s1 = p
>     s2 : (S d) * (d' * q) = S d
>     s2 = replace {x = ((S d) * d') * q} {y = (S d) * (d' * q)} {P = \ ZUZU => ZUZU = S d} (sym (multAssociative (S d) d' q)) s1
>     p' : d' * q = S Z
>     p' = multElim1 d (d' * q) s2
> %freeze divisorOneLemma

> |||
> divisorOneLemma' : (d : Nat) -> (d' : Nat) -> Not (d = Z) -> d * d' `Divisor` d -> d' `Divisor` S Z
> divisorOneLemma'  Z    _  dNotZ _  = void (dNotZ Refl)
> divisorOneLemma' (S d) d' dNotZ (Element q p) =
>   Element q p' where
>     s1 : ((S d) * d') * q = S d
>     s1 = p
>     s2 : (S d) * (d' * q) = S d
>     s2 = replace {x = ((S d) * d') * q} {y = (S d) * (d' * q)} {P = \ ZUZU => ZUZU = S d} (sym (multAssociative (S d) d' q)) s1
>     p' : d' * q = S Z
>     p' = multElim1 d (d' * q) s2
> %freeze divisorOneLemma'

> |||
> divisorOneLemma'' : (d : Nat) -> (d' : Nat) -> Z `LT` d -> d * d' `Divisor` d -> d' `Divisor` S Z
> divisorOneLemma''  Z    _  p  _             =
>   absurd p
> divisorOneLemma'' (S d) d' _ (Element q p) =
>   Element q p' where
>     s1 : ((S d) * d') * q = S d
>     s1 = p
>     s2 : (S d) * (d' * q) = S d
>     s2 = replace {x = ((S d) * d') * q} {y = (S d) * (d' * q)} {P = \ ZUZU => ZUZU = S d} (sym (multAssociative (S d) d' q)) s1
>     p' : d' * q = S Z
>     p' = multElim1 d (d' * q) s2
> %freeze divisorOneLemma''

> |||
> divisorTowerLemma: (d : Nat) -> (d' : Nat) -> (m : Nat) ->
>                    (dDm : d `Divisor` m) -> d' `Divisor` (quotient m d dDm) -> d * d' `Divisor` m
> divisorTowerLemma d d' m dDm d'DmOd = Element q' p where
>   q' : Nat
>   q' = quotient (quotient m d dDm) d' d'DmOd
>   s1 : d' * q' = quotient m d dDm
>   s1 = quotientLemma (quotient m d dDm) d' d'DmOd
>   s2 : d * (quotient m d dDm) = m
>   s2 = quotientLemma m d dDm
>   s3 : d * (d' * q') = m
>   s3 = replace {x = quotient m d dDm} {y = d' * q'} {P = \ ZUZU => d * ZUZU = m} (sym s1) s2
>   p : (d * d') * q' = m
>   p = replace {x = d * (d' * q')} {y = (d * d') * q'} {P = \ ZUZU => ZUZU = m} (multAssociative d d' q') s3
> %freeze divisorTowerLemma

Properties of |quotient|:

> |||
> quotientIsJustGetWitness : (m : Nat) -> (d : Nat) -> (dDm : d `Divisor` m) ->
>                            quotient m d dDm = getWitness dDm
> quotientIsJustGetWitness m d (Element q prf) =
>    ( quotient m d (Element q prf) )
>  ={ Refl }=
>    ( q )
>  ={ Refl }=
>    ( getWitness (Element q prf) )
>  QED
> %freeze quotientIsJustGetWitness

> |||
> quotientDivisorLemma2 : (m : Nat) ->
>                         (d1 : Nat) -> (d1Dm : d1 `Divisor` m) ->
>                         (d2 : Nat) -> (d2Dm : d2 `Divisor` m) ->
>                         d1 = d2 -> Not (d1 = Z) -> quotient m d1 d1Dm = quotient m d2 d2Dm
> quotientDivisorLemma2 m d (Element q1 dq1EQm) d (Element q2 dq2EQm) Refl NdEQZ =
>     ( quotient m d (Element q1 dq1EQm) )
>   ={ Refl }=
>     ( q1 )
>   ={ multMultElimLeft d d q1 q2 Refl NdEQZ (trans dq1EQm (sym dq2EQm)) }=
>     ( q2 )
>   ={ Refl }=
>     ( quotient m d (Element q2 dq2EQm) )
>   QED
> %freeze quotientDivisorLemma2

> ||| quotient preserves positivity
> quotientPreservesPositivity : (m : Nat) -> (d : Nat) -> (dDm : d `Divisor` m) ->
>                               Z `LT` m -> Z `LT` (quotient m d dDm)
> quotientPreservesPositivity m d dDm zLTm =
>   multLTZeroRightLTZero d q zLTdq where
>     q : Nat
>     q = quotient m d dDm
>     zLTdq : Z `LT` (d * q)
>     zLTdq = replace {x = m}
>                     {y = d * q}
>                     {P = \ ZUZU => Z `LT` ZUZU}
>                     (sym (quotientLemma m d dDm)) zLTm
> %freeze quotientPreservesPositivity

> |||
> quotientAnyOneAny : (m : Nat) -> (d : Nat) -> (dDm : d `Divisor` m) ->
>                     (d = S Z) -> quotient m d dDm = m
> quotientAnyOneAny m d (Element q p) dEQ1 =
>     ( quotient m d (Element q p) )
>   ={ Refl }=
>     ( q )
>   ={ sym (multOneLeftNeutral q) }=
>     ( (S Z) * q )
>   ={ replace {x = S Z}
>              {y = d}
>              {P = \ ZUZU => (S Z) * q = ZUZU * q}
>              (sym dEQ1) Refl }=
>     ( d * q )
>   ={ p }=
>     ( m )
>   QED
> %freeze quotientAnyOneAny

> |||
> quotientPlusLemma : (m : Nat) -> (n : Nat) -> (d : Nat) ->
>                     (dDm : d `Divisor` m) -> (dDn : d `Divisor` n) ->
>                     (quotient m d dDm) + (quotient n d dDn)
>                     =
>                     quotient (m + n) d (divisorPlusLemma1 m n d dDm dDn)
> quotientPlusLemma m n d (Element q1 p1) (Element q2 p2) =
>     ( (quotient m d (Element q1 p1)) + (quotient n d (Element q2 p2)) )
>   ={ Refl }=
>     ( q1 + q2 )
>   ={ Refl }=
>     ( quotient (m + n) d (divisorPlusLemma1 m n d (Element q1 p1) (Element q2 p2)) )
>   QED
> %freeze quotientPlusLemma

> |||
> quotientMultLemma : (m1 : Nat) -> (d1 : Nat) -> (d1Dm1 : d1 `Divisor` m1) ->
>                     (m2 : Nat) -> (d2 : Nat) -> (d2Dm2 : d2 `Divisor` m2) ->
>                     (quotient m1 d1 d1Dm1) * (quotient m2 d2 d2Dm2)
>                     =
>                     quotient (m1 * m2) (d1 * d2) (divisorMultLemma1 m1 d1 d1Dm1 m2 d2 d2Dm2)
> quotientMultLemma m1 d1 (Element q1 p1) m2 d2 (Element q2 p2) =
>     ( (quotient m1 d1 (Element q1 p1)) * (quotient m2 d2 (Element q2 p2))  )
>   ={ Refl }=
>     ( q1 * q2 )
>   ={ Refl }=
>     ( quotient (m1 * m2) (d1 * d2) (divisorMultLemma1 m1 d1 (Element q1 p1) m2 d2 (Element q2 p2)) )
>   QED
> %freeze quotientMultLemma

> |||
> quotientCancellationLemma : (m : Nat) -> (d : Nat) ->
>                             (sdDsdm : (S d) `Divisor` (S d) * m) ->
>                             quotient ((S d) * m) (S d) sdDsdm = m
> quotientCancellationLemma m d (Element q prf) =
>     ( q )
>   ={ multMultElimLeft (S d) (S d) q m Refl SIsNotZ prf }=
>     ( m )
>   QED
> %freeze quotientCancellationLemma

> quotientScaleInvariant : (m : Nat) -> (n : Nat) -> (d : Nat) -> Not (d * n = Z) ->
>                          (nDm : n `Divisor` m) -> (dnDdm : (d * n) `Divisor` (d * m)) ->
>                          quotient m n nDm = quotient (d * m) (d * n) dnDdm
> quotientScaleInvariant m n d ndnEQZ (Element p npEQm) (Element q dnqEQdm) =
>   let s1 : (d * (n * p) = d * m)
>          = multPreservesEq d d (n * p) m Refl npEQm in
>   let s2 : ((d * n) * p = d * m)
>          = replace {P = \ ZUZU => ZUZU = d * m} (multAssociative d n p) s1 in
>   let s3 : ((d * n) * p = (d * n) * q)
>          = trans s2 (sym dnqEQdm) in
>     ( quotient m n (Element p npEQm) )
>   ={ Refl }=
>     ( p )
>   ={ multMultElimLeft (d * n) (d * n) p q Refl ndnEQZ s3 }=
>     ( q )
>   ={ Refl }=
>     ( quotient (d * m) (d * n) (Element q dnqEQdm) )
>   QED
> %freeze quotientScaleInvariant

> |||
> quotientDivisorLemma : (d : Nat) -> (m : Nat) -> (n : Nat) ->
>                        (sdDm : S d `Divisor` m) ->
>                        (mDn: m `Divisor` n) ->
>                        (sdDn : S d `Divisor` n) ->
>                        (quotient m (S d) sdDm) `Divisor` (quotient n (S d) sdDn)
> quotientDivisorLemma d m n (Element x sdxEQm) (Element y myEQn) (Element z sdzEQn) =
>   Element y xyEQz where
>     sdxyEQmy    :  ((S d) * x) * y = m * y
>     sdxyEQmy    =  multPreservesEq ((S d) * x) m y y sdxEQm Refl
>     sdxyEQsdz   :  ((S d) * x) * y = (S d) * z
>     sdxyEQsdz   =  trans sdxyEQmy (trans myEQn (sym sdzEQn))
>     sdxyEQsdz'  :  (S d) * (x * y) = (S d) * z
>     sdxyEQsdz'  =  replace {x = ((S d) * x) * y}
>                            {y = (S d) * (x * y)}
>                            {P = \ ZUZU => ZUZU = (S d) * z}
>                            (sym (multAssociative (S d) x y)) sdxyEQsdz
>     xyEQz       :  x * y = z
>     xyEQz       =  multMultElimLeft (S d) (S d) (x * y) z Refl SIsNotZ sdxyEQsdz'
> %freeze quotientDivisorLemma

> |||
> quotientDivisorLemma1 : (a : Nat) -> (b : Nat) -> (c : Nat) ->
>                         (saDb : S a `Divisor` b) ->
>                         (bDc  :   b `Divisor` c) ->
>                         (quotient b (S a) saDb)
>                         `Divisor`
>                         (quotient c (S a) (divisorTransitive {l = S a} {m = b} {n = c} saDb bDc))
> quotientDivisorLemma1 a b c saDb bDc = prf where
>   x           :  Nat
>   x           =  getWitness saDb
>   saxEQb      :  (S a) * x = b
>   saxEQb      =  getProof saDb
>   y           :  Nat
>   y           =  getWitness bDc
>   byEQc       :  b * y = c
>   byEQc       =  getProof bDc
>   saDc        :  (S a) `Divisor` c
>   saDc        =  divisorTransitive {l = S a} {m = b} {n = c} saDb bDc
>   z           :  Nat
>   z           =  getWitness saDc
>   sazEQc      :  (S a) * z = c
>   sazEQc      =  getProof saDc
>   saxyEQby    :  ((S a) * x) * y = b * y
>   saxyEQby    =  multPreservesEq ((S a) * x) b y y saxEQb Refl
>   saxyEQsaz   :  ((S a) * x) * y = (S a) * z
>   saxyEQsaz   =  trans saxyEQby (trans byEQc (sym sazEQc))
>   saxyEQsaz'  :  (S a) * (x * y) = (S a) * z
>   saxyEQsaz'  =  replace {x = ((S a) * x) * y}
>                          {y = (S a) * (x * y)}
>                          {P = \ ZUZU => ZUZU = (S a) * z}
>                          (sym (multAssociative (S a) x y)) saxyEQsaz
>   xyEQz       :  x * y = z
>   xyEQz       =  multMultElimLeft (S a) (S a) (x * y) z Refl SIsNotZ saxyEQsaz'
>   prf1        :  x `Divisor` z
>   prf1        =  Element y xyEQz
>   prf2        :  (quotient b (S a) saDb)  `Divisor` z
>   prf2        =  replace {x = x}
>                          {y = quotient b (S a) saDb}
>                          {P = \ ZUZU => ZUZU `Divisor` z}
>                          (sym (quotientIsJustGetWitness b (S a) saDb)) prf1
>   prf         :  (quotient b (S a) saDb) `Divisor` (quotient c (S a) saDc)
>   prf         =  replace {x = z}
>                          {y = quotient c (S a) (divisorTransitive {l = S a} {m = b} {n = c} saDb bDc)}
>                          {P = \ ZUZU => (quotient b (S a) saDb) `Divisor` ZUZU}
>                          (sym (quotientIsJustGetWitness c (S a) saDc)) prf2
> %freeze quotientDivisorLemma1

> |||
> flipQuotientLemma : (m : Nat) -> (n : Nat) -> (d : Nat) ->
>                     (dDm : d `Divisor` m) -> (dDn : d `Divisor` n) ->
>                     (quotient m d dDm) * n = m * (quotient n d dDn)
> flipQuotientLemma m n d dDm dDn =
>   let qmd = quotient m d dDm in
>   let qnd = quotient n d dDn in
>     ( qmd * n )
>   ={ cong {f = \ ZUZU => qmd * ZUZU} (sym (quotientLemma n d dDn)) }=
>     ( qmd * (d * qnd) )
>   ={ multAssociative qmd d qnd }=
>     ( (qmd * d) * qnd )
>   ={ cong {f = \ ZUZU => ZUZU * qnd} (multCommutative qmd d) }=
>     ( (d * qmd) * qnd )
>   ={ cong {f = \ ZUZU => ZUZU * qnd} (quotientLemma m d dDm) }=
>     ( m * qnd )
>   QED
> %freeze flipQuotientLemma

> |||
> quotientEqLemma : (m1 : Nat) -> (d1 : Nat) -> (d1Dm1 : d1 `Divisor` m1) ->
>                   (m2 : Nat) -> (d2 : Nat) -> (d2Dm2 : d2 `Divisor` m2) ->
>                   m1 = m2 -> d1 = d2 -> Not (d1 = Z) ->
>                   quotient m1 d1 d1Dm1 = quotient m2 d2 d2Dm2
> quotientEqLemma m d (Element p dpEQm) m d (Element q dqEQm) Refl Refl ndEQZ =
>     ( quotient m d (Element p dpEQm) )
>   ={ Refl }=
>     ( p )
>   ={ multMultElimLeft d d p q Refl ndEQZ (trans dpEQm (sym dqEQm)) }=
>     ( q )
>   ={ Refl }=
>     ( quotient m d (Element q dqEQm) )
>   QED
> %freeze quotientEqLemma

> {-

> ---}

ext: lidr

max_stars_repo_name: zenntenn/IdrisLibs

max_issues_repo_name: zenntenn/IdrisLibs

max_forks_repo_name: zenntenn/IdrisLibs


text:
module Optics

import Data.Profunctor
import Data.List1

--------------------------------------------------------------------------------
--          Optics
--------------------------------------------------------------------------------

Optic : (p : Type -> Type -> Type) -> (a,b,s,t : Type) -> Type
Optic p a b s t = p a b -> p s t

AGetter : (a,b,s,t : Type) -> Type
AGetter a = Optic (Kleislimorphism $ Const a) a

ASetter : (a,b,s,t : Type) -> Type
ASetter = Optic Morphism

iso : Profunctor p => (s -> a) -> (b -> t) -> Optic p a b s t
iso = dimap

lens : Strong p => (s -> a) -> (s -> b -> t) -> Optic p a b s t
lens f g = dimap f' (uncurry g) . second
  where f' : s -> (s,a)
        f' s = (s, f s)

fst : Strong p => Optic p a b (a,c) (b,c)
fst = lens fst $ \(_,c),b => (b,c)

snd : Strong p => Optic p a b (c,a) (c,b)
snd = lens snd $ \(c,_),b => (c,b)

view : AGetter a b s t -> s -> a
view f = runConst . applyKleisli (f $ Kleisli MkConst)

over : ASetter a b s t -> (a -> b) -> s -> t
over f g = applyMor (f $ Mor g)

--------------------------------------------------------------------------------
--          Tests
--------------------------------------------------------------------------------

cons : Profunctor p => Optic p (a,List a) (b,List b) (List1 a) (List1 b)
cons = iso (\(h ::: t) => (h,t)) (\(h,t) => h ::: t)

uncons : Profunctor p => Optic p (List1 a) (List1 b) (a,List a) (b,List b)
uncons = iso (\(h,t) => h ::: t) (\(h ::: t) => (h,t))

headUpper : List1 Char -> List1 Char
headUpper = over (cons . fst) toUpper


text:
module Js.Electron.App

import Js

%default total
%access export

name : JS_IO String
name = js "electron.app.getName()" (JS_IO String)

setName : String -> JS_IO ()
setName = js "electron.app.setName(%0)" (String -> JS_IO ())

version : JS_IO String
version = js "electron.app.getVersion()" (JS_IO String)

path : JS_IO String
path = js "electron.app.getAppPath()" (JS_IO String)

-- macOS
show : JS_IO ()
show = js "electron.app.show()" (JS_IO ())

-- macOS
hide : JS_IO ()
hide = js "electron.app.hide()" (JS_IO ())

focus : JS_IO ()
focus = js "electron.app.focus()" (JS_IO ())

quit : JS_IO ()
quit = js "electron.app.quit()" (JS_IO ())

exit : JS_IO ()
exit = js "electron.app.exit()" (JS_IO ())

exitWith : Int -> JS_IO ()
exitWith = js "electron.app.exit(%0)" (Int -> JS_IO ())

relaunch : JS_IO ()
relaunch = js "electron.app.relaunch()" (JS_IO ())

on : String -> JS_IO () -> JS_IO ()
on event func = assert_total $ js "electron.app.on(%0, %1)" (String -> JsFn (() -> JS_IO ()) -> JS_IO ()) event (MkJsFn $ const func)

onWillFinishLaunching : JS_IO () -> JS_IO ()
onWillFinishLaunching = on "will-finish-launching"

onReady : JS_IO () -> JS_IO ()
onReady = on "ready"

onAllWindowsClosed : JS_IO () -> JS_IO ()
onAllWindowsClosed = on "window-all-closed"

max_stars_repo_name: jheiling/idris-electron

max_issues_repo_name: jheiling/idris-electron

max_forks_repo_name: jheiling/idris-electron


text:
%default total

foo : (x : Bool) -> x === True
foo = \ ? => Refl


text:
||| Courtesy of @z-snails
module Core.Ord

import Core.CompileExpr
import Core.Name
import Core.TT
import Data.Vect

infixl 5 `thenCmp`

thenCmp : Ordering -> Lazy Ordering -> Ordering
thenCmp LT _ = LT
thenCmp EQ o = o
thenCmp GT _ = GT

export
Ord Constant where
    I x `compare` I y = compare x y
    I8 x `compare` I8 y = compare x y
    I16 x `compare` I16 y = compare x y
    I32 x `compare` I32 y = compare x y
    I64 x `compare` I64 y = compare x y
    BI x `compare` BI y = compare x y
    B8 x `compare` B8 y = compare x y
    B16 x `compare` B16 y = compare x y
    B32 x `compare` B32 y = compare x y
    B64 x `compare` B64 y = compare x y
    Str x `compare` Str y = compare x y
    Ch x `compare` Ch y = compare x y
    Db x `compare` Db y = compare x y
    compare x y = compare (tag x) (tag y)
      where
        tag : Constant -> Int
        tag (I _) = 0
        tag (I8 _) = 1
        tag (I16 _) = 2
        tag (I32 _) = 3
        tag (I64 _) = 4
        tag (BI _) = 5
        tag (B8 _) = 6
        tag (B16 _) = 7
        tag (B32 _) = 8
        tag (B64 _) = 9
        tag (Str _) = 10
        tag (Ch _) = 11
        tag (Db _) = 12
        tag WorldVal = 13
        tag IntType = 14
        tag Int8Type = 15
        tag Int16Type = 16
        tag Int32Type = 17
        tag Int64Type = 18
        tag IntegerType = 19
        tag Bits8Type = 20
        tag Bits16Type = 21
        tag Bits32Type = 22
        tag Bits64Type = 23
        tag StringType = 24
        tag CharType = 25
        tag DoubleType = 26
        tag WorldType = 27

primFnEq : PrimFn a1 -> PrimFn a2 -> Maybe (a1 = a2)
primFnEq (Add t1) (Add t2) = if t1 == t2 then Just Refl else Nothing
primFnEq (Sub t1) (Sub t2) = if t1 == t2 then Just Refl else Nothing
primFnEq (Mul t1) (Mul t2) = if t1 == t2 then Just Refl else Nothing
primFnEq (Div t1) (Div t2) = if t1 == t2 then Just Refl else Nothing
primFnEq (Mod t1) (Mod t2) = if t1 == t2 then Just Refl else Nothing
primFnEq (Neg t1) (Neg t2) = if t1 == t2 then Just Refl else Nothing
primFnEq (ShiftL t1) (ShiftL t2) = if t1 == t2 then Just Refl else Nothing
primFnEq (ShiftR t1) (ShiftR t2) = if t1 == t2 then Just Refl else Nothing
primFnEq (BAnd t1) (BAnd t2) = if t1 == t2 then Just Refl else Nothing
primFnEq (BOr t1) (BOr t2) = if t1 == t2 then Just Refl else Nothing
primFnEq (BXOr t1) (BXOr t2) = if t1 == t2 then Just Refl else Nothing
primFnEq (LT t1) (LT t2) = if t1 == t2 then Just Refl else Nothing
primFnEq (LTE t1) (LTE t2) = if t1 == t2 then Just Refl else Nothing
primFnEq (EQ t1) (EQ t2) = if t1 == t2 then Just Refl else Nothing
primFnEq (GTE t1) (GTE t2) = if t1 == t2 then Just Refl else Nothing
primFnEq (GT t1) (GT t2) = if t1 == t2 then Just Refl else Nothing
primFnEq StrLength StrLength = Just Refl
primFnEq StrHead StrHead = Just Refl
primFnEq StrTail StrTail = Just Refl
primFnEq StrIndex StrIndex = Just Refl
primFnEq StrCons StrCons = Just Refl
primFnEq StrAppend StrAppend = Just Refl
primFnEq StrReverse StrReverse = Just Refl
primFnEq StrSubstr StrSubstr = Just Refl
primFnEq DoubleExp DoubleExp = Just Refl
primFnEq DoubleLog DoubleLog = Just Refl
primFnEq DoublePow DoublePow = Just Refl
primFnEq DoubleSin DoubleSin = Just Refl
primFnEq DoubleCos DoubleCos = Just Refl
primFnEq DoubleTan DoubleTan = Just Refl
primFnEq DoubleASin DoubleASin = Just Refl
primFnEq DoubleACos DoubleACos = Just Refl
primFnEq DoubleATan DoubleATan = Just Refl
primFnEq DoubleSqrt DoubleSqrt = Just Refl
primFnEq DoubleFloor DoubleFloor = Just Refl
primFnEq DoubleCeiling DoubleCeiling = Just Refl
primFnEq (Cast f1 t1) (Cast f2 t2) = if f1 == f2 && t1 == t2 then Just Refl else Nothing
primFnEq BelieveMe BelieveMe = Just Refl
primFnEq Crash Crash = Just Refl
primFnEq _ _ = Nothing

primFnCmp : PrimFn a1 -> PrimFn a2 -> Ordering
primFnCmp (Add t1) (Add t2) = compare t1 t2
primFnCmp (Sub t1) (Sub t2) = compare t1 t2
primFnCmp (Mul t1) (Mul t2) = compare t1 t2
primFnCmp (Div t1) (Div t2) = compare t1 t2
primFnCmp (Mod t1) (Mod t2) = compare t1 t2
primFnCmp (Neg t1) (Neg t2) = compare t1 t2
primFnCmp (ShiftL t1) (ShiftL t2) = compare t1 t2
primFnCmp (ShiftR t1) (ShiftR t2) = compare t1 t2
primFnCmp (BAnd t1) (BAnd t2) = compare t1 t2
primFnCmp (BOr t1) (BOr t2) = compare t1 t2
primFnCmp (BXOr t1) (BXOr t2) = compare t1 t2
primFnCmp (LT t1) (LT t2) = compare t1 t2
primFnCmp (LTE t1) (LTE t2) = compare t1 t2
primFnCmp (EQ t1) (EQ t2) = compare t1 t2
primFnCmp (GTE t1) (GTE t2) = compare t1 t2
primFnCmp (GT t1) (GT t2) = compare t1 t2
primFnCmp (Cast f1 t1) (Cast f2 t2) = compare f1 f2 `thenCmp` compare t1 t2
primFnCmp f1 f2 = compare (tag f1) (tag f2)
  where
    tag : forall ar. PrimFn ar -> Int
    tag (Add _) = 0
    tag (Sub _) = 1
    tag (Mul _) = 2
    tag (Div _) = 3
    tag (Mod _) = 4
    tag (Neg _) = 5
    tag (ShiftL _) = 6
    tag (ShiftR _) = 7
    tag (BAnd _) = 8
    tag (BOr _) = 9
    tag (BXOr _) = 10
    tag (LT _) = 11
    tag (LTE _) = 12
    tag (EQ _) = 13
    tag (GTE _) = 14
    tag (GT _) = 15
    tag StrLength = 16
    tag StrHead = 17
    tag StrTail = 18
    tag StrIndex = 19
    tag StrCons = 20
    tag StrAppend = 21
    tag StrReverse = 22
    tag StrSubstr = 23
    tag DoubleExp = 24
    tag DoubleLog = 25
    tag DoublePow = 26
    tag DoubleSin = 27
    tag DoubleCos = 28
    tag DoubleTan = 29
    tag DoubleASin = 30
    tag DoubleACos = 31
    tag DoubleATan = 32
    tag DoubleSqrt = 33
    tag DoubleFloor = 34
    tag DoubleCeiling = 35
    tag (Cast _ _) = 36
    tag BelieveMe = 37
    tag Crash = 38

lrTag : LazyReason -> Int
lrTag LInf = 0
lrTag LLazy = 1
lrTag LUnknown = 2

export
Ord LazyReason where
    compare l1 l2 = compare (lrTag l1) (lrTag l2)

export
Eq (Var vars) where
    MkVar {i=i1} _ == MkVar {i=i2} _ = i1 == i2

export
Ord (Var vars) where
    MkVar {i=i1} _ `compare` MkVar {i=i2} _ = compare i1 i2

mutual
    export
    Eq (CExp vars) where
        CLocal {idx=x1} _ _ == CLocal {idx=x2} _ _ = x1 == x2
        CRef _ n1 == CRef _ n2 = n1 == n2
        CLam _ n1 e1 == CLam _ n2 e2 = case nameEq n1 n2 of
            Just Refl => e1 == e2
            Nothing => False
        CLet _ n1 _ val1 sc1 == CLet _ n2 _ val2 sc2 = case nameEq n1 n2 of
            Just Refl => val1 == val2 && sc1 == sc2
            Nothing => False
        CApp _ f1 a1 == CApp _ f2 a2 = f1 == f2 && a1 == a2
        CCon _ n1 _ t1 a1 == CCon _ n2 _ t2 a2 = t1 == t2 && n1 == n2 && a1 == a2
        COp _ f1 a1 == COp _ f2 a2 = case primFnEq f1 f2 of
            Just Refl => a1 == a2
            Nothing => False
        CExtPrim _ f1 a1 == CExtPrim _ f2 a2 = f1 == f2 && a1 == a2
        CForce _ l1 e1 == CForce _ l2 e2 = l1 == l2 && e1 == e2
        CDelay _ l1 e1 == CDelay _ l2 e2 = l1 == l2 && e1 == e2
        CConCase _ s1 a1 d1 == CConCase _ s2 a2 d2 = s1 == s2 && a1 == a2 && d1 == d2
        CConstCase _ s1 a1 d1 == CConstCase _ s2 a2 d2 = s1 == s2 && a1 == a2 && d1 == d2
        CPrimVal _ c1 == CPrimVal _ c2 = c1 == c2
        CErased _ == CErased _ = True
        CCrash _ m1 == CCrash _ m2 = m1 == m2
        _ == _ = False

    export
    Eq (CConAlt vars) where
        MkConAlt n1 _ t1 a1 e1 == MkConAlt n2 _ t2 a2 e2 = t1 == t2 && n1 == n2 && case namesEq a1 a2 of
            Just Refl => e1 == e2
            Nothing => False

    export
    Eq (CConstAlt vars) where
        MkConstAlt c1 e1 == MkConstAlt c2 e2 = c1 == c2 && e1 == e2

mutual
    export
    Ord (CExp vars) where
        CLocal {idx=x1} _ _ `compare` CLocal {idx=x2} _ _ = x1 `compare` x2
        CRef _ n1 `compare` CRef _ n2 = n1 `compare` n2
        CLam _ n1 e1 `compare` CLam _ n2 e2 = case nameEq n1 n2 of
            Just Refl => compare e1 e2
            Nothing => compare n1 n2
        CLet _ n1 _ val1 sc1 `compare` CLet _ n2 _ val2 sc2 = case nameEq n1 n2 of
            Just Refl => compare val1 val2 `thenCmp` compare sc1 sc2
            Nothing => compare n1 n2
        CApp _ f1 a1 `compare` CApp _ f2 a2 = compare f1 f2 `thenCmp` compare a1 a2
        CCon _ n1 _ t1 a1 `compare` CCon _ n2 _ t2 a2 = compare t1 t2 `thenCmp` compare n1 n2 `thenCmp` compare a1 a2
        COp _ f1 a1 `compare` COp _ f2 a2 = case primFnEq f1 f2 of
            Just Refl => compare a1 a2
            Nothing => primFnCmp f1 f2
        CExtPrim _ f1 a1 `compare` CExtPrim _ f2 a2 = compare f1 f2 `thenCmp` compare a1 a2
        CForce _ l1 e1 `compare` CForce _ l2 e2 = compare l1 l2 `thenCmp` compare e1 e2
        CDelay _ l1 e1 `compare` CDelay _ l2 e2 = compare l1 l2 `thenCmp` compare e1 e2
        CConCase _ s1 a1 d1 `compare` CConCase _ s2 a2 d2 = compare s1 s2 `thenCmp` compare a1 a2 `thenCmp` compare d1 d2
        CConstCase _ s1 a1 d1 `compare` CConstCase _ s2 a2 d2 = compare s1 s2 `thenCmp` compare a1 a2 `thenCmp` compare d1 d2
        CPrimVal _ c1 `compare` CPrimVal _ c2 = compare c1 c2
        CErased _ `compare` CErased _ = EQ
        CCrash _ m1 `compare` CCrash _ m2 = compare m1 m2
        e1 `compare` e2 = compare (tag e1) (tag e2)
          where
            tag : forall vars . CExp vars -> Int
            tag (CLocal _ _) = 0
            tag (CRef _ _) = 1
            tag (CLam _ _ _) = 2
            tag (CLet _ _ _ _ _) = 3
            tag (CApp _ _ _) = 4
            tag (CCon _ _ _ _ _) = 5
            tag (COp _ _ _) = 6
            tag (CExtPrim _ _ _) = 7
            tag (CForce _ _ _) = 8
            tag (CDelay _ _ _) = 9
            tag (CConCase _ _ _ _) = 10
            tag (CConstCase _ _ _ _) = 11
            tag (CPrimVal _ _) = 12
            tag (CErased _) = 13
            tag (CCrash _ _) = 14

    export
    Ord (CConAlt vars) where
        MkConAlt n1 _ t1 a1 e1 `compare` MkConAlt n2 _ t2 a2 e2 =
            compare t1 t2 `thenCmp` compare n1 n2 `thenCmp` case namesEq a1 a2 of
                Just Refl => compare e1 e2
                Nothing => compare a1 a2

    export
    Ord (CConstAlt vars) where
        MkConstAlt c1 e1 `compare` MkConstAlt c2 e2 = compare c1 c2 `thenCmp` compare e1 e2


text:
module lib.Library4

import lib.Library5

export
salute4 : String
salute4 = "Hello, this is Library4 with a little help from my friend: " ++ salute5


text:
module Polunin

import Data.So

%default total

foo : (x : Int) -> {auto xBound : So (x >= 0 && x <= 10)} -> (y : Int ** y = x * 2)
foo x = (x * 2 ** Refl)

a : Int
a = 5

bf : Int
bf = fst $ foo a

b : (x : Int ** x = 10)
b = foo a


text:
module Dudo

import Data.Vect
import SillyTypes

data Die : NumDieSides -> Type where
  MkDie :
    {dieNumSides : NumDieSides} ->
    (dieConfiguration : PeanoFin dieNumSides) ->
    Die numSides

data Player : NumDice -> NumDieSides -> Type where
  MkPlayer :
    (name : NonEmptyString) ->
    {numDice : NumDice} ->
    (numDiceInPlay : Nat) ->
    (numDiceNotInPlay : Nat) ->
    {dice_consistent : (natRep numDice) = (numDiceInPlay + numDiceNotInPlay)} ->
    {dieSides : NumDieSides} ->
    (diceInPlay : Vect numDiceInPlay (Die dieSides)) ->
    (diceNotInPlay : Vect numDiceNotInPlay (Die dieSides)) ->
    Player numDice dieSides

data Table : NumPlayers -> NumDice -> NumDieSides -> Type where
  MkTable :
    {tableNumPlayers : NumPlayers} ->
    {tableNumDicePerPlayer : NumDice} ->
    {tableNumDieSides : NumDieSides} ->
    (tablePlayers : Vect (natRep tableNumPlayers)
                         (Player tableNumDicePerPlayer tableNumDieSides)) ->
    Table numPlayers numDice numDieSides

max_stars_repo_name: pharpend/dudo

max_issues_repo_name: pharpend/dudo

max_forks_repo_name: pharpend/dudo


text:
module Replica.Command.Run

import Data.List
import Data.String

import Replica.Help
import Replica.Option.Types
import public Replica.Option.Filter
import public Replica.Option.Global
import Replica.Other.Decorated

%default total

public export
record RunCommand' (f : Type -> Type) where
  constructor MkRunCommand
  workingDir : f String
  interactive : f Bool
  threads : f Nat
  hideSuccess : f Bool
  punitive : f Bool
  filter : Filter' f
  global : Global' f

public export
RunCommand : Type
RunCommand = Done RunCommand'

TyMap RunCommand' where
  tyMap func x =
    MkRunCommand
      (func x.workingDir)
      (func x.interactive)
      (func x.threads)
      (func x.hideSuccess)
      (func x.punitive)
      (tyMap func x.filter)
      (tyMap func x.global)

TyTraversable RunCommand' where
  tyTraverse func x = [|
    MkRunCommand
      (func x.workingDir)
      (func x.interactive)
      (func x.threads)
      (func x.hideSuccess)
      (func x.punitive)
      (tyTraverse func x.filter)
      (tyTraverse func x.global)
      |]

export
Show RunCommand where
  show x = unwords
    [ "MkRunCommand"
    , show x.workingDir
    , show x.interactive
    , show x.threads
    , show x.hideSuccess
    , show x.punitive
    , show x.filter
    , show x.global
    ]

interactivePart : Part (Builder RunCommand') Bool
interactivePart = inj $ MkOption
      (singleton $ MkMod (singleton "interactive") ['i'] (Left True)
            "(re)generate golden number if different/missing")
      False
      go
  where
    go : Bool -> Builder RunCommand' -> Either String (Builder RunCommand')
    go = ifSame interactive
                (\x => record {interactive = Right x})
                (const $ const "Contradictory values for interactive")

workingDirPart : Part (Builder RunCommand') String
workingDirPart = inj $ MkOption
      (singleton $ MkMod ("working-dir" ::: ["wdir"]) ['w']
          (Right $ MkValue "DIR" Just)
          "set where is the test working directory")
      "."
      go
  where
    go : String -> Builder RunCommand' -> Either String (Builder RunCommand')
    go = one workingDir
             (\x => record {workingDir = Right x})
             (\x, y => "More than one working directony were given: \{y}, \{x}")

threadsPart : Part (Builder RunCommand') Nat
threadsPart = inj $ MkOption
      (singleton $ MkMod (singleton "threads") ['n']
          (Right $ MkValue "N" parsePositive)
          "max number of threads (default 1; 0 for no thread limit)")
      1
      go
  where
    go : Nat -> Builder RunCommand' -> Either String (Builder RunCommand')
    go = one threads
             (\x => record {threads = Right x})
             (\x, y => "More than one threads values were given: \{show y}, \{show x}")

punitivePart : Part (Builder RunCommand') Bool
punitivePart = inj $ MkOption
      (singleton $ MkMod ("punitive" ::: ["fail-fast"]) ['p']
          (Left True)
          "fail fast mode: stops on the first test that fails")
      False
      go
      where
        go : Bool -> Builder RunCommand' -> Either String (Builder RunCommand')
        go = ifSame punitive
                    (\x => record {punitive = Right x})
                    (const $ const "Contradictory values for punitive mode")

hideSuccessPart : Part (Builder RunCommand') Bool
hideSuccessPart = inj $ MkOption
      (singleton $ MkMod (toList1 ["hide-success", "fail-only"]) []
          (Left True)
          "hide successful tests in the report")
      False
      go
      where
        go : Bool -> Builder RunCommand' -> Either String (Builder RunCommand')
        go = ifSame hideSuccess
                    (\x => record {hideSuccess = Right x})
                    (const $ const "Contradictory values for hide success mode")

optParseRun : OptParse (Builder RunCommand') RunCommand
optParseRun =
    [| MkRunCommand
       (liftAp workingDirPart)
       (liftAp interactivePart)
       (liftAp threadsPart)
       (liftAp hideSuccessPart)
       (liftAp punitivePart)
       (embed filter (\x => record {filter = x}) optParseFilter)
       (embed global (\x => record {global = x}) optParseGlobal)
    |]

defaultRun : Default RunCommand'
defaultRun = MkRunCommand
       (defaultPart workingDirPart)
       (defaultPart interactivePart)
       (defaultPart threadsPart)
       (defaultPart hideSuccessPart)
       (defaultPart punitivePart)
       defaultFilter
       defaultGlobal

export
parseRun : List1 String -> ParseResult RunCommand
parseRun ("run":::xs) = do
    case parse (initBuilder defaultRun) optParseRun xs of
         InvalidMix reason => InvalidMix reason
         InvalidOption ys  => InvalidMix $ "Unknown option: " ++ ys.head
         Done builder      => maybe (InvalidMix "No test file given") Done $ build builder
parseRun xs = InvalidOption xs

export
helpRun : Help
helpRun = commandHelp {b = Builder RunCommand'}
  "run" "Run tests from a Replica JSON file"
  optParseRun
  (Just "JSON_TEST_FILE")

max_stars_repo_name: teto/REPLica

max_issues_repo_name: teto/REPLica

max_forks_repo_name: teto/REPLica


text:
module Main

import Channel
import Linear
import System

TestProto : Protocol ()
TestProto
    = do b <- Request Bool
         if b
            then do Respond Char; Done
            else do Respond String; Done

testClient : (1 chan : Client TestProto) -> Any IO ()
testClient chan
    = do lift $ putStrLn "Starting client"
         lift $ sleep 1
         lift $ putStrLn "Sending value"
         chan <- send chan False
         lift $ putStrLn "Sent"
         c # chan <- recv chan
         lift $ putStrLn ("Result: " ++ c)
         close chan

testServer : (1 chan : Server TestProto) -> Any IO ()
testServer chan
    = do lift $ putStrLn "Waiting"
         cmd # chan <- recv chan
         lift $ putStrLn ("Received " ++ show cmd)
         lift $ sleep 1
         lift $ putStrLn "Sending answer"
         if cmd
            then do chan <- send chan 'a'
                    close chan
            else do chan <- send chan "Foo"
                    close chan

lmain : Any IO ()
lmain
    = do chan <- Channel.fork testServer
         testClient chan

main : IO ()
main = run lmain