text:
module TTImp.ProcessDef

import Core.CaseBuilder
import Core.CaseTree
import Core.Context
import Core.Context.Log
import Core.Core
import Core.Coverage
import Core.Env
import Core.Hash
import Core.LinearCheck
import Core.Metadata
import Core.Normalise
import Core.Termination
import Core.Transform
import Core.Value
import Core.UnifyState

import TTImp.BindImplicits
import TTImp.Elab
import TTImp.Elab.Check
import TTImp.Elab.Utils
import TTImp.Impossible
import TTImp.PartialEval
import TTImp.TTImp
import TTImp.TTImp.Functor
import TTImp.Unelab
import TTImp.Utils
import TTImp.WithClause

import Data.Either
import Data.List
import Libraries.Data.NameMap
import Data.String
import Data.Maybe
import Libraries.Text.PrettyPrint.Prettyprinter
import Libraries.Data.String.Extra

%hide Data.String.lines
%hide Data.String.lines'
%hide Data.String.unlines
%hide Data.String.unlines'

%default covering

mutual
  mismatchNF : {auto c : Ref Ctxt Defs} ->
               {vars : _} ->
               Defs -> NF vars -> NF vars -> Core Bool
  mismatchNF defs (NTCon _ xn xt _ xargs) (NTCon _ yn yt _ yargs)
      = if xn /= yn
           then pure True
           else anyM (mismatch defs) (zipWith (curry $ mapHom snd) xargs yargs)
  mismatchNF defs (NDCon _ _ xt _ xargs) (NDCon _ _ yt _ yargs)
      = if xt /= yt
           then pure True
           else anyM (mismatch defs) (zipWith (curry $ mapHom snd) xargs yargs)
  mismatchNF defs (NPrimVal _ xc) (NPrimVal _ yc) = pure (xc /= yc)
  mismatchNF defs (NDelayed _ _ x) (NDelayed _ _ y) = mismatchNF defs x y
  mismatchNF defs (NDelay _ _ _ x) (NDelay _ _ _ y)
      = mismatchNF defs !(evalClosure defs x) !(evalClosure defs y)

  -- NPrimVal is apart from NDCon, NTCon, NBind, and NType
  mismatchNF defs (NPrimVal _ _) (NDCon _ _ _ _ _) = pure True
  mismatchNF defs (NDCon _ _ _ _ _) (NPrimVal _ _) = pure True
  mismatchNF defs (NPrimVal _ _) (NBind _ _ _ _) = pure True
  mismatchNF defs (NBind _ _ _ _) (NPrimVal _ _) = pure True
  mismatchNF defs (NPrimVal _ _) (NTCon _ _ _ _ _) = pure True
  mismatchNF defs (NTCon _ _ _ _ _) (NPrimVal _ _) = pure True
  mismatchNF defs (NPrimVal _ _) (NType _) = pure True
  mismatchNF defs (NType _) (NPrimVal _ _) = pure True

-- NTCon is apart from NBind, and NType
  mismatchNF defs (NTCon _ _ _ _ _) (NBind _ _ _ _) = pure True
  mismatchNF defs (NBind _ _ _ _) (NTCon _ _ _ _ _) = pure True
  mismatchNF defs (NTCon _ _ _ _ _) (NType _) = pure True
  mismatchNF defs (NType _) (NTCon _ _ _ _ _) = pure True

-- NBind is apart from NType
  mismatchNF defs (NBind _ _ _ _) (NType _) = pure True
  mismatchNF defs (NType _) (NBind _ _ _ _) = pure True

  mismatchNF _ _ _ = pure False

  mismatch : {auto c : Ref Ctxt Defs} ->
             {vars : _} ->
             Defs -> (Closure vars, Closure vars) -> Core Bool
  mismatch defs (x, y)
      = mismatchNF defs !(evalClosure defs x) !(evalClosure defs y)

-- If the terms have the same type constructor at the head, and one of
-- the argument positions has different constructors at its head, then this
-- is an impossible case, so return True
export
impossibleOK : {auto c : Ref Ctxt Defs} ->
               {vars : _} ->
               Defs -> NF vars -> NF vars -> Core Bool
impossibleOK defs (NTCon _ xn xt xa xargs) (NTCon _ yn yt ya yargs)
    = if xn /= yn
         then pure True
         else anyM (mismatch defs) (zipWith (curry $ mapHom snd) xargs yargs)
-- If it's a data constructor, any mismatch will do
impossibleOK defs (NDCon _ _ xt _ xargs) (NDCon _ _ yt _ yargs)
    = if xt /= yt
         then pure True
         else anyM (mismatch defs) (zipWith (curry $ mapHom snd) xargs yargs)
impossibleOK defs (NPrimVal _ x) (NPrimVal _ y) = pure (x /= y)

-- NPrimVal is apart from NDCon, NTCon, NBind, and NType
impossibleOK defs (NPrimVal _ _) (NDCon _ _ _ _ _) = pure True
impossibleOK defs (NDCon _ _ _ _ _) (NPrimVal _ _) = pure True
impossibleOK defs (NPrimVal _ _) (NBind _ _ _ _) = pure True
impossibleOK defs (NBind _ _ _ _) (NPrimVal _ _) = pure True
impossibleOK defs (NPrimVal _ _) (NTCon _ _ _ _ _) = pure True
impossibleOK defs (NTCon _ _ _ _ _) (NPrimVal _ _) = pure True
impossibleOK defs (NPrimVal _ _) (NType _) = pure True
impossibleOK defs (NType _) (NPrimVal _ _) = pure True

-- NTCon is apart from NBind, and NType
impossibleOK defs (NTCon _ _ _ _ _) (NBind _ _ _ _) = pure True
impossibleOK defs (NBind _ _ _ _) (NTCon _ _ _ _ _) = pure True
impossibleOK defs (NTCon _ _ _ _ _) (NType _) = pure True
impossibleOK defs (NType _) (NTCon _ _ _ _ _) = pure True

-- NBind is apart from NType
impossibleOK defs (NBind _ _ _ _) (NType _) = pure True
impossibleOK defs (NType _) (NBind _ _ _ _) = pure True

impossibleOK defs x y = pure False

export
impossibleErrOK : {auto c : Ref Ctxt Defs} ->
                  Defs -> Error -> Core Bool
impossibleErrOK defs (CantConvert fc gam env l r)
    = do let defs = record { gamma = gam } defs
         impossibleOK defs !(nf defs env l)
                           !(nf defs env r)
impossibleErrOK defs (CantSolveEq fc gam env l r)
    = do let defs = record { gamma = gam } defs
         impossibleOK defs !(nf defs env l)
                           !(nf defs env r)
impossibleErrOK defs (BadDotPattern _ _ ErasedArg _ _) = pure True
impossibleErrOK defs (CyclicMeta _ _ _ _) = pure True
impossibleErrOK defs (AllFailed errs)
    = anyM (impossibleErrOK defs) (map snd errs)
impossibleErrOK defs (WhenUnifying _ _ _ _ _ err)
    = impossibleErrOK defs err
impossibleErrOK defs _ = pure False

-- If it's a clause we've generated, see if the error is recoverable. That
-- is, if we have a concrete thing, and we're expecting the same concrete
-- thing, or a function of something, then we might have a match.
export
recoverable : {auto c : Ref Ctxt Defs} ->
              {vars : _} ->
              Defs -> NF vars -> NF vars -> Core Bool
-- Unlike the above, any mismatch will do

-- TYPE CONSTRUCTORS
recoverable defs (NTCon _ xn xt xa xargs) (NTCon _ yn yt ya yargs)
    = if xn /= yn
         then pure False
         else pure $ not !(anyM (mismatch defs) (zipWith (curry $ mapHom snd) xargs yargs))
-- Type constructor vs. primitive type
recoverable defs (NTCon _ _ _ _ _) (NPrimVal _ _) = pure False
recoverable defs (NPrimVal _ _) (NTCon _ _ _ _ _) = pure False
-- Type constructor vs. type
recoverable defs (NTCon _ _ _ _ _) (NType _) = pure False
recoverable defs (NType _) (NTCon _ _ _ _ _) = pure False
-- Type constructor vs. binder
recoverable defs (NTCon _ _ _ _ _) (NBind _ _ _ _) = pure False
recoverable defs (NBind _ _ _ _) (NTCon _ _ _ _ _) = pure False

recoverable defs (NTCon _ _ _ _ _) _ = pure True
recoverable defs _ (NTCon _ _ _ _ _) = pure True

-- DATA CONSTRUCTORS
recoverable defs (NDCon _ _ xt _ xargs) (NDCon _ _ yt _ yargs)
    = if xt /= yt
         then pure False
         else pure $ not !(anyM (mismatch defs) (zipWith (curry $ mapHom snd) xargs yargs))
-- Data constructor vs. primitive constant
recoverable defs (NDCon _ _ _ _ _) (NPrimVal _ _) = pure False
recoverable defs (NPrimVal _ _) (NDCon _ _ _ _ _) = pure False

recoverable defs (NDCon _ _ _ _ _) _ = pure True
recoverable defs _ (NDCon _ _ _ _ _) = pure True

-- FUNCTION CALLS
recoverable defs (NApp _ (NRef _ f) fargs) (NApp _ (NRef _ g) gargs)
    = pure True -- both functions; recoverable

-- PRIMITIVES
recoverable defs (NPrimVal _ x) (NPrimVal _ y) = pure (x == y)
-- primitive vs. binder
recoverable defs (NPrimVal _ _) (NBind _ _ _ _) = pure False
recoverable defs (NBind _ _ _ _) (NPrimVal _ _) = pure False

-- OTHERWISE: no
recoverable defs x y = pure False

export
recoverableErr : {auto c : Ref Ctxt Defs} ->
                 Defs -> Error -> Core Bool
recoverableErr defs (CantConvert fc gam env l r)
  = do let defs = record { gamma = gam } defs
       l <- nf defs env l
       r <- nf defs env r
       log "coverage.recover" 10 $ unlines
         [ "Recovering from CantConvert?"
         , "Checking:"
         , "  " ++ show l
         , "  " ++ show r
         ]
       recoverable defs l r

recoverableErr defs (CantSolveEq fc gam env l r)
  = do let defs = record { gamma = gam } defs
       recoverable defs !(nf defs env l)
                        !(nf defs env r)
recoverableErr defs (BadDotPattern _ _ ErasedArg _ _) = pure True
recoverableErr defs (CyclicMeta _ _ _ _) = pure True
recoverableErr defs (AllFailed errs)
    = anyM (recoverableErr defs) (map snd errs)
recoverableErr defs (WhenUnifying _ _ _ _ _ err)
    = recoverableErr defs err
recoverableErr defs _ = pure False

-- Given a type checked LHS and its type, return the environment in which we
-- should check the RHS, the LHS and its type in that environment,
-- and a function which turns a checked RHS into a
-- pattern clause
-- The 'SubVars' proof contains a proof that refers to the *inner* environment,
-- so all the outer things are marked as 'DropCons'
extendEnv : {vars : _} ->
            Env Term vars -> SubVars inner vars ->
            NestedNames vars ->
            Term vars -> Term vars ->
            Core (vars' **
                    (SubVars inner vars',
                     Env Term vars', NestedNames vars',
                     Term vars', Term vars'))
extendEnv env p nest (Bind _ n (PVar fc c pi tmty) sc) (Bind _ n' (PVTy _ _ _) tysc) with (nameEq n n')
  extendEnv env p nest (Bind _ n (PVar fc c pi tmty) sc) (Bind _ n' (PVTy _ _ _) tysc) | Nothing
      = throw (InternalError "Can't happen: names don't match in pattern type")
  extendEnv env p nest (Bind _ n (PVar fc c pi tmty) sc) (Bind _ n (PVTy _ _ _) tysc) | (Just Refl)
      = extendEnv (PVar fc c pi tmty :: env) (DropCons p) (weaken nest) sc tysc
extendEnv env p nest (Bind _ n (PLet fc c tmval tmty) sc) (Bind _ n' (PLet _ _ _ _) tysc) with (nameEq n n')
  extendEnv env p nest (Bind _ n (PLet fc c tmval tmty) sc) (Bind _ n' (PLet _ _ _ _) tysc) | Nothing
      = throw (InternalError "Can't happen: names don't match in pattern type")
  -- PLet on the left becomes Let on the right, to give it computational force
  extendEnv env p nest (Bind _ n (PLet fc c tmval tmty) sc) (Bind _ n (PLet _ _ _ _) tysc) | (Just Refl)
      = extendEnv (Let fc c tmval tmty :: env) (DropCons p) (weaken nest) sc tysc
extendEnv env p nest tm ty
      = pure (_ ** (p, env, nest, tm, ty))

-- Find names which are applied to a function in a Rig1/Rig0 position,
-- so that we know how they should be bound on the right hand side of the
-- pattern.
-- 'bound' counts the number of variables locally bound; these are the
-- only ones we're checking linearity of (we may be shadowing names if this
-- is a local definition, so we need to leave the earlier ones alone)
findLinear : {vars : _} ->
             {auto c : Ref Ctxt Defs} ->
             Bool -> Nat -> RigCount -> Term vars ->
             Core (List (Name, RigCount))
findLinear top bound rig (Bind fc n b sc)
    = findLinear top (S bound) rig sc
findLinear top bound rig (As fc _ _ p)
    = findLinear top bound rig p
findLinear top bound rig tm
    = case getFnArgs tm of
           (Ref _ _ n, []) => pure []
           (Ref _ nt n, args)
              => do defs <- get Ctxt
                    Just nty <- lookupTyExact n (gamma defs)
                         | Nothing => pure []
                    findLinArg (accessible nt rig) !(nf defs [] nty) args
           _ => pure []
    where
      accessible : NameType -> RigCount -> RigCount
      accessible Func r = if top then r else erased
      accessible _ r = r

      findLinArg : {vars : _} ->
                   RigCount -> NF [] -> List (Term vars) ->
                   Core (List (Name, RigCount))
      findLinArg rig ty (As fc UseLeft _ p :: as)
          = findLinArg rig ty (p :: as)
      findLinArg rig ty (As fc UseRight p _ :: as)
          = findLinArg rig ty (p :: as)
      findLinArg rig (NBind _ x (Pi _ c _ _) sc) (Local {name=a} fc _ idx prf :: as)
          = do defs <- get Ctxt
               let a = nameAt prf
               if idx < bound
                 then do sc' <- sc defs (toClosure defaultOpts [] (Ref fc Bound x))
                         pure $ (a, rigMult c rig) ::
                                    !(findLinArg rig sc' as)
                 else do sc' <- sc defs (toClosure defaultOpts [] (Ref fc Bound x))
                         findLinArg rig sc' as
      findLinArg rig (NBind fc x (Pi _ c _ _) sc) (a :: as)
          = do defs <- get Ctxt
               pure $ !(findLinear False bound (c |*| rig) a) ++
                      !(findLinArg rig !(sc defs (toClosure defaultOpts [] (Ref fc Bound x))) as)
      findLinArg rig ty (a :: as)
          = pure $ !(findLinear False bound rig a) ++ !(findLinArg rig ty as)
      findLinArg _ _ [] = pure []

setLinear : List (Name, RigCount) -> Term vars -> Term vars
setLinear vs (Bind fc x b@(PVar _ _ _ _) sc)
    = case lookup x vs of
           Just c' => Bind fc x (setMultiplicity b c') (setLinear vs sc)
           _ => Bind fc x b (setLinear vs sc)
setLinear vs (Bind fc x b@(PVTy _ _ _) sc)
    = case lookup x vs of
           Just c' => Bind fc x (setMultiplicity b c') (setLinear vs sc)
           _ => Bind fc x b (setLinear vs sc)
setLinear vs tm = tm

-- Combining multiplicities on LHS:
-- Rig1 + Rig1/W not valid, since it means we have repeated use of name
-- Rig0 + RigW = RigW
-- Rig0 + Rig1 = Rig1
combineLinear : FC -> List (Name, RigCount) ->
                Core (List (Name, RigCount))
combineLinear loc [] = pure []
combineLinear loc ((n, count) :: cs)
    = case lookupAll n cs of
           [] => pure $ (n, count) :: !(combineLinear loc cs)
           counts => do count' <- combineAll count counts
                        pure $ (n, count') ::
                               !(combineLinear loc (filter notN cs))
  where
    notN : (Name, RigCount) -> Bool
    notN (n', _) = n /= n'

    lookupAll : Name -> List (Name, RigCount) -> List RigCount
    lookupAll n [] = []
    lookupAll n ((n', c) :: cs)
       = if n == n' then c :: lookupAll n cs else lookupAll n cs

    -- Those combine rules are obtuse enough that they are worth investigating
    combine : RigCount -> RigCount -> Core RigCount
    combine l r = if l |+| r == top && not (isErased $ l `glb` r) && (l `glb` r) /= top
                     then throw (LinearUsed loc 2 n)
                     -- if everything is fine, return the linearity that has the
                     -- highest bound
                     else pure (l `lub` r)

    combineAll : RigCount -> List RigCount -> Core RigCount
    combineAll c [] = pure c
    combineAll c (c' :: cs)
        = do newc <- combine c c'
             combineAll newc cs

export -- also used by Transforms
checkLHS : {vars : _} ->
           {auto c : Ref Ctxt Defs} ->
           {auto m : Ref MD Metadata} ->
           {auto u : Ref UST UState} ->
           Bool -> -- in transform
           (mult : RigCount) -> (hashit : Bool) ->
           Int -> List ElabOpt -> NestedNames vars -> Env Term vars ->
           FC -> RawImp ->
           Core (RawImp, -- checked LHS with implicits added
                 (vars' ** (SubVars vars vars',
                           Env Term vars', NestedNames vars',
                           Term vars', Term vars')))
checkLHS {vars} trans mult hashit n opts nest env fc lhs_in
    = do defs <- get Ctxt
         logRaw "declare.def.lhs" 30 "Raw LHS: " lhs_in
         lhs_raw <- if trans
                       then pure lhs_in
                       else lhsInCurrentNS nest lhs_in
         logRaw "declare.def.lhs" 30 "Raw LHS in current NS: " lhs_raw

         autoimp <- isUnboundImplicits
         setUnboundImplicits True
         (_, lhs_bound) <- bindNames False lhs_raw
         setUnboundImplicits autoimp
         logRaw "declare.def.lhs" 30 "Raw LHS with implicits bound" lhs_bound

         lhs <- if trans
                   then pure lhs_bound
                   else implicitsAs n defs vars lhs_bound

         logC "declare.def.lhs" 5 $ do pure $ "Checking LHS of " ++ show !(getFullName (Resolved n))
-- todo: add Pretty RawImp instance
--         logC "declare.def.lhs" 5 $ do pure $ show $ indent {ann = ()} 2 $ pretty lhs
         log "declare.def.lhs" 10 $ show lhs
         logEnv "declare.def.lhs" 5 "In env" env
         let lhsMode = if trans
                          then InTransform
                          else InLHS mult
         (lhstm, lhstyg) <-
             wrapErrorC opts (InLHS fc !(getFullName (Resolved n))) $
                     elabTerm n lhsMode opts nest env
                                (IBindHere fc PATTERN lhs) Nothing
         logTerm "declare.def.lhs" 5 "Checked LHS term" lhstm
         lhsty <- getTerm lhstyg

         defs <- get Ctxt
         let lhsenv = letToLam env
         -- we used to fully normalise the LHS, to make sure fromInteger
         -- patterns were allowed, but now they're fully normalised anyway
         -- so we only need to do the holes. If there's a lot of type level
         -- computation, this is a huge saving!
         lhstm <- normaliseHoles defs lhsenv lhstm
         lhsty <- normaliseHoles defs env lhsty
         linvars_in <- findLinear True 0 linear lhstm
         logTerm "declare.def.lhs" 10 "Checked LHS term after normalise" lhstm
         log "declare.def.lhs" 5 $ "Linearity of names in " ++ show n ++ ": " ++
                 show linvars_in

         linvars <- combineLinear fc linvars_in
         let lhstm_lin = setLinear linvars lhstm
         let lhsty_lin = setLinear linvars lhsty

         logTerm "declare.def.lhs" 3 "LHS term" lhstm_lin
         logTerm "declare.def.lhs" 5 "LHS type" lhsty_lin
         setHoleLHS (bindEnv fc env lhstm_lin)

         ext <- extendEnv env SubRefl nest lhstm_lin lhsty_lin
         pure (lhs, ext)

-- Return whether any of the pattern variables are in a trivially empty
-- type, where trivally empty means one of:
--  * No constructors
--  * Every constructor of the family has a return type which conflicts with
--    the given constructor's type
hasEmptyPat : {vars : _} ->
              {auto c : Ref Ctxt Defs} ->
              Defs -> Env Term vars -> Term vars -> Core Bool
hasEmptyPat defs env (Bind fc x b sc)
   = pure $ !(isEmpty defs env !(nf defs env (binderType b)))
            || !(hasEmptyPat defs (b :: env) sc)
hasEmptyPat defs env _ = pure False

-- For checking with blocks as nested names
applyEnv : {vars : _} ->
           {auto c : Ref Ctxt Defs} ->
           Env Term vars -> Name ->
           Core (Name, (Maybe Name, List (Var vars), FC -> NameType -> Term vars))
applyEnv env withname
    = do n' <- resolveName withname
         pure (withname, (Just withname, reverse (allVarsNoLet env),
                  \fc, nt => applyTo fc
                         (Ref fc nt (Resolved n')) env))

-- Check a pattern clause, returning the component of the 'Case' expression it
-- represents, or Nothing if it's an impossible clause
export
checkClause : {vars : _} ->
              {auto c : Ref Ctxt Defs} ->
              {auto m : Ref MD Metadata} ->
              {auto u : Ref UST UState} ->
              (mult : RigCount) -> (vis : Visibility) ->
              (totreq : TotalReq) -> (hashit : Bool) ->
              Int -> List ElabOpt -> NestedNames vars -> Env Term vars ->
              ImpClause -> Core (Either RawImp Clause)
checkClause mult vis totreq hashit n opts nest env (ImpossibleClause fc lhs)
    = do lhs_raw <- lhsInCurrentNS nest lhs
         handleUnify
           (do autoimp <- isUnboundImplicits
               setUnboundImplicits True
               (_, lhs) <- bindNames False lhs_raw
               setUnboundImplicits autoimp

               log "declare.def.clause.impossible" 5 $ "Checking " ++ show lhs
               logEnv "declare.def.clause.impossible" 5 "In env" env
               (lhstm, lhstyg) <-
                           elabTerm n (InLHS mult) opts nest env
                                      (IBindHere fc PATTERN lhs) Nothing
               defs <- get Ctxt
               lhs <- normaliseHoles defs env lhstm
               if !(hasEmptyPat defs env lhs)
                  then pure (Left lhs_raw)
                  else throw (ValidCase fc env (Left lhs)))
           (\err =>
              case err of
                   ValidCase _ _ _ => throw err
                   _ => do defs <- get Ctxt
                           if !(impossibleErrOK defs err)
                              then pure (Left lhs_raw)
                              else throw (ValidCase fc env (Right err)))
checkClause {vars} mult vis totreq hashit n opts nest env (PatClause fc lhs_in rhs)
    = do (_, (vars'  ** (sub', env', nest', lhstm', lhsty'))) <-
             checkLHS False mult hashit n opts nest env fc lhs_in
         let rhsMode = if isErased mult then InType else InExpr
         log "declare.def.clause" 5 $ "Checking RHS " ++ show rhs
         logEnv "declare.def.clause" 5 "In env" env'

         rhstm <- logTime ("+++ Check RHS " ++ show fc) $
                    wrapErrorC opts (InRHS fc !(getFullName (Resolved n))) $
                       checkTermSub n rhsMode opts nest' env' env sub' rhs (gnf env' lhsty')
         clearHoleLHS

         logTerm "declare.def.clause" 3 "RHS term" rhstm
         when hashit $
           do addHashWithNames lhstm'
              addHashWithNames rhstm

         -- If the rhs is a hole, record the lhs in the metadata because we
         -- might want to split it interactively
         case rhstm of
              Meta _ _ _ _ =>
                 addLHS (getFC lhs_in) (length env) env' lhstm'
              _ => pure ()

         pure (Right (MkClause env' lhstm' rhstm))
-- TODO: (to decide) With is complicated. Move this into its own module?
checkClause {vars} mult vis totreq hashit n opts nest env
    (WithClause ifc lhs_in wval_raw mprf flags cs)
    = do (lhs, (vars'  ** (sub', env', nest', lhspat, reqty))) <-
             checkLHS False mult hashit n opts nest env ifc lhs_in
         let wmode
               = if isErased mult then InType else InExpr

         (wval, gwvalTy) <- wrapErrorC opts (InRHS ifc !(getFullName (Resolved n))) $
                elabTermSub n wmode opts nest' env' env sub' wval_raw Nothing
         clearHoleLHS

         logTerm "declare.def.clause.with" 5 "With value" wval
         logTerm "declare.def.clause.with" 3 "Required type" reqty
         wvalTy <- getTerm gwvalTy
         defs <- get Ctxt
         wval <- normaliseHoles defs env' wval
         wvalTy <- normaliseHoles defs env' wvalTy

         let (wevars ** withSub) = keepOldEnv sub' (snd (findSubEnv env' wval))
         logTerm "declare.def.clause.with" 5 "With value type" wvalTy
         log "declare.def.clause.with" 5 $ "Using vars " ++ show wevars

         let Just wval = shrinkTerm wval withSub
             | Nothing => throw (InternalError "Impossible happened: With abstraction failure #1")
         let Just wvalTy = shrinkTerm wvalTy withSub
             | Nothing => throw (InternalError "Impossible happened: With abstraction failure #2")
         -- Should the env be normalised too? If the following 'impossible'
         -- error is ever thrown, that might be the cause!
         let Just wvalEnv = shrinkEnv env' withSub
             | Nothing => throw (InternalError "Impossible happened: With abstraction failure #3")

         -- Abstracting over 'wval' in the scope of bNotReq in order
         -- to get the 'magic with' behaviour
         (wargs ** (scenv, var, binder)) <- bindWithArgs wvalTy ((,wval) <$> mprf) wvalEnv

         let bnr = bindNotReq vfc 0 env' withSub [] reqty
         let notreqns = fst bnr
         let notreqty = snd bnr

         rdefs <- if Syntactic `elem` flags
                     then clearDefs defs
                     else pure defs
         wtyScope <- replace rdefs scenv !(nf rdefs scenv (weakenNs (mkSizeOf wargs) wval))
                            var
                            !(nf rdefs scenv
                                 (weakenNs (mkSizeOf wargs) notreqty))
         let bNotReq = binder wtyScope

         -- The environment has some implicit and some explcit args, potentially,
         -- which is inconvenient since we have to know which is which when
         -- elaborating the application of the rhs function. So it's easier
         -- if we just make them all explicit - this type isn't visible to
         -- users anyway!
         let env' = mkExplicit env'

         let Just (reqns, envns, wtype) = bindReq vfc env' withSub [] bNotReq
             | Nothing => throw (InternalError "Impossible happened: With abstraction failure #4")

         -- list of argument names - 'Just' means we need to match the name
         -- in the with clauses to find out what the pattern should be.
         -- 'Nothing' means it's the with pattern (so wargn)
         let wargNames
                 = map Just reqns ++
                   Nothing :: map Just notreqns

         logTerm "declare.def.clause.with" 3 "With function type" wtype
         log "declare.def.clause.with" 5 $ "Argument names " ++ show wargNames

         wname <- genWithName !(prettyName !(toFullNames (Resolved n)))
         widx <- addDef wname (record {flags $= (SetTotal totreq ::)}
                                    (newDef vfc wname (if isErased mult then erased else top)
                                      vars wtype vis None))

         let toWarg : Maybe (PiInfo RawImp, Name) -> List (Maybe Name, RawImp)
               := flip maybe (\pn => [(Nothing, IVar vfc (snd pn))]) $
                    (Nothing, wval_raw) ::
                    case mprf of
                      Nothing => []
                      Just _  =>
                       let fc = emptyFC in
                       let refl = IVar fc (NS builtinNS (UN $ Basic "Refl")) in
                       [(mprf, INamedApp fc refl (UN $ Basic "x") wval_raw)]

         let rhs_in = gapply (IVar vfc wname)
                    $ map (\ nm => (Nothing, IVar vfc nm)) envns
                   ++ concatMap toWarg wargNames

         log "declare.def.clause" 3 $ "Applying to with argument " ++ show rhs_in
         rhs <- wrapErrorC opts (InRHS ifc !(getFullName (Resolved n))) $
             checkTermSub n wmode opts nest' env' env sub' rhs_in
                          (gnf env' reqty)

         -- Generate new clauses by rewriting the matched arguments
         cs' <- traverse (mkClauseWith 1 wname wargNames lhs) cs
         log "declare.def.clause.with" 3 $ "With clauses: " ++ show cs'

         -- Elaborate the new definition here
         nestname <- applyEnv env wname
         let nest'' = record { names $= (nestname ::) } nest

         let wdef = IDef ifc wname cs'
         processDecl [] nest'' env wdef

         pure (Right (MkClause env' lhspat rhs))
  where
    vfc : FC
    vfc = virtualiseFC ifc

    mkExplicit : forall vs . Env Term vs -> Env Term vs
    mkExplicit [] = []
    mkExplicit (Pi fc c _ ty :: env) = Pi fc c Explicit ty :: mkExplicit env
    mkExplicit (b :: env) = b :: mkExplicit env

    bindWithArgs :
       (wvalTy : Term xs) -> Maybe (Name, Term xs) ->
       (wvalEnv : Env Term xs) ->
       Core (ext : List Name
         ** ( Env Term (ext ++ xs)
            , Term (ext ++ xs)
            , (Term (ext ++ xs) -> Term xs)
            ))
    bindWithArgs {xs} wvalTy Nothing wvalEnv =
      let wargn : Name
          wargn = MN "warg" 0
          wargs : List Name
          wargs = [wargn]

          scenv : Env Term (wargs ++ xs)
                := Pi vfc top Explicit wvalTy :: wvalEnv

          var : Term (wargs ++ xs)
              := Local vfc (Just False) Z First

          binder : Term (wargs ++ xs) -> Term xs
                 := Bind vfc wargn (Pi vfc top Explicit wvalTy)

      in pure (wargs ** (scenv, var, binder))

    bindWithArgs {xs} wvalTy (Just (name, wval)) wvalEnv = do
      defs <- get Ctxt

      let eqName = NS builtinNS (UN $ Basic "Equal")
      Just (TCon t ar _ _ _ _ _ _) <- lookupDefExact eqName (gamma defs)
        | _ => throw (InternalError "Cannot find builtin Equal")
      let eqTyCon = Ref vfc (TyCon t ar) !(toResolvedNames eqName)

      let wargn : Name
          wargn = MN "warg" 0
          wargs : List Name
          wargs = [name, wargn]

          wvalTy' := weaken wvalTy
          eqTy : Term (MN "warg" 0 :: xs)
               := apply vfc eqTyCon
                           [ wvalTy'
                           , wvalTy'
                           , weaken wval
                           , Local vfc (Just False) Z First
                           ]

          scenv : Env Term (wargs ++ xs)
                := Pi vfc top Implicit eqTy
                :: Pi vfc top Explicit wvalTy
                :: wvalEnv

          var : Term (wargs ++ xs)
              := Local vfc (Just False) (S Z) (Later First)

          binder : Term (wargs ++ xs) -> Term xs
                 := \ t => Bind vfc wargn (Pi vfc top Explicit wvalTy)
                         $ Bind vfc name  (Pi vfc top Implicit eqTy) t

      pure (wargs ** (scenv, var, binder))

    -- If it's 'KeepCons/SubRefl' in 'outprf', that means it was in the outer
    -- environment so we need to keep it in the same place in the 'with'
    -- function. Hence, turn it to KeepCons whatever
    keepOldEnv : {0 outer : _} -> {vs : _} ->
                 (outprf : SubVars outer vs) -> SubVars vs' vs ->
                 (vs'' : List Name ** SubVars vs'' vs)
    keepOldEnv {vs} SubRefl p = (vs ** SubRefl)
    keepOldEnv {vs} p SubRefl = (vs ** SubRefl)
    keepOldEnv (DropCons p) (DropCons p')
        = let (_ ** rest) = keepOldEnv p p' in
              (_ ** DropCons rest)
    keepOldEnv (DropCons p) (KeepCons p')
        = let (_ ** rest) = keepOldEnv p p' in
              (_ ** KeepCons rest)
    keepOldEnv (KeepCons p) (DropCons p')
        = let (_ ** rest) = keepOldEnv p p' in
              (_ ** KeepCons rest)
    keepOldEnv (KeepCons p) (KeepCons p')
        = let (_ ** rest) = keepOldEnv p p' in
              (_ ** KeepCons rest)

    -- Rewrite the clauses in the block to use an updated LHS.
    -- 'drop' is the number of additional with arguments we expect
    -- (i.e. the things to drop from the end before matching LHSs)
    mkClauseWith : (drop : Nat) -> Name ->
                   List (Maybe (PiInfo RawImp, Name)) ->
                   RawImp -> ImpClause ->
                   Core ImpClause
    mkClauseWith drop wname wargnames lhs (PatClause ploc patlhs rhs)
        = do log "declare.def.clause.with" 20 "PatClause"
             newlhs <- getNewLHS ploc drop nest wname wargnames lhs patlhs
             newrhs <- withRHS ploc drop wname wargnames rhs lhs
             pure (PatClause ploc newlhs newrhs)
    mkClauseWith drop wname wargnames lhs (WithClause ploc patlhs rhs prf flags ws)
        = do log "declare.def.clause.with" 20 "WithClause"
             newlhs <- getNewLHS ploc drop nest wname wargnames lhs patlhs
             newrhs <- withRHS ploc drop wname wargnames rhs lhs
             ws' <- traverse (mkClauseWith (S drop) wname wargnames lhs) ws
             pure (WithClause ploc newlhs newrhs prf flags ws')
    mkClauseWith drop wname wargnames lhs (ImpossibleClause ploc patlhs)
        = do log "declare.def.clause.with" 20 "ImpossibleClause"
             newlhs <- getNewLHS ploc drop nest wname wargnames lhs patlhs
             pure (ImpossibleClause ploc newlhs)

nameListEq : (xs : List Name) -> (ys : List Name) -> Maybe (xs = ys)
nameListEq [] [] = Just Refl
nameListEq (x :: xs) (y :: ys) with (nameEq x y)
  nameListEq (x :: xs) (x :: ys) | (Just Refl) with (nameListEq xs ys)
    nameListEq (x :: xs) (x :: xs) | (Just Refl) | Just Refl= Just Refl
    nameListEq (x :: xs) (x :: ys) | (Just Refl) | Nothing = Nothing
  nameListEq (x :: xs) (y :: ys) | Nothing = Nothing
nameListEq _ _ = Nothing

-- Calculate references for the given name, and recursively if they haven't
-- been calculated already
calcRefs : {auto c : Ref Ctxt Defs} ->
           (runtime : Bool) -> (aTotal : Name) -> (fn : Name) -> Core ()
calcRefs rt at fn
    = do defs <- get Ctxt
         Just gdef <- lookupCtxtExact fn (gamma defs)
              | _ => pure ()
         let PMDef r cargs tree_ct tree_rt pats = definition gdef
              | _ => pure () -- not a function definition
         let refs : Maybe (NameMap Bool)
                  = if rt then refersToRuntimeM gdef else refersToM gdef
         let Nothing = refs
              | Just _ => pure () -- already done
         let tree : CaseTree cargs = if rt then tree_rt else tree_ct
         let metas = CaseTree.getMetas tree
         traverse_ addToSave (keys metas)
         let refs_all = addRefs at metas tree
         refs <- ifThenElse rt
                    (dropErased (keys refs_all) refs_all)
                    (pure refs_all)
         ignore $ ifThenElse rt
            (addDef fn (record { refersToRuntimeM = Just refs } gdef))
            (addDef fn (record { refersToM = Just refs } gdef))
         traverse_ (calcRefs rt at) (keys refs)
  where
    dropErased : List Name -> NameMap Bool -> Core (NameMap Bool)
    dropErased [] refs = pure refs
    dropErased (n :: ns) refs
        = do defs <- get Ctxt
             Just gdef <- lookupCtxtExact n (gamma defs)
                  | Nothing => dropErased ns refs
             if multiplicity gdef /= erased
                then dropErased ns refs
                else dropErased ns (delete n refs)

-- Compile run time case trees for the given name
mkRunTime : {auto c : Ref Ctxt Defs} ->
            {auto m : Ref MD Metadata} ->
            {auto u : Ref UST UState} ->
            FC -> Name -> Core ()
mkRunTime fc n
    = do log "compile.casetree" 5 $ "Making run time definition for " ++ show !(toFullNames n)
         defs <- get Ctxt
         Just gdef <- lookupCtxtExact n (gamma defs)
              | _ => pure ()
         let cov = gdef.totality.isCovering
         -- If it's erased at run time, don't build the tree
         when (not (isErased $ multiplicity gdef)) $ do
           let PMDef r cargs tree_ct _ pats = definition gdef
                | _ => pure () -- not a function definition
           let ty = type gdef
           -- Prepare RHS of definitions, by erasing 0-multiplicities, and
           -- finding any applications to specialise (partially evaluate)
           pats' <- traverse (toErased (location gdef) (getSpec (flags gdef)))
                             pats

           let clauses_init = map (toClause (location gdef)) pats'
           let clauses = case cov of
                              MissingCases _ => addErrorCase clauses_init
                              _ => clauses_init

           (rargs ** (tree_rt, _)) <- getPMDef (location gdef) RunTime n ty clauses
           logC "compile.casetree" 5 $ pure $ unlines
             [ show cov ++ ":"
             , "Runtime tree for " ++ show (fullname gdef) ++ ":"
             , show (indent 2 $ pretty {ann = ()} !(toFullNames tree_rt))
             ]
           log "compile.casetree" 10 $ show tree_rt
           log "compile.casetree.measure" 15 $ show (measure tree_rt)

           let Just Refl = nameListEq cargs rargs
                   | Nothing => throw (InternalError "WAT")
           ignore $ addDef n $
                       record { definition = PMDef r rargs tree_ct tree_rt pats
                              } gdef
           -- If it's a case block, and not already set as inlinable,
           -- check if it's safe to inline
           when (caseName !(toFullNames n) && noInline (flags gdef)) $
             do inl <- canInlineCaseBlock n
                when inl $ setFlag fc n Inline
  where
    noInline : List DefFlag -> Bool
    noInline (Inline :: _) = False
    noInline (x :: xs) = noInline xs
    noInline _ = True

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

    mkCrash : {vars : _} -> String -> Term vars
    mkCrash msg
       = apply fc (Ref fc Func (NS builtinNS (UN $ Basic "idris_crash")))
               [Erased fc False, PrimVal fc (Str msg)]

    matchAny : Term vars -> Term vars
    matchAny (App fc f a) = App fc (matchAny f) (Erased fc False)
    matchAny tm = tm

    makeErrorClause : {vars : _} -> Env Term vars -> Term vars -> Clause
    makeErrorClause env lhs
        = MkClause env (matchAny lhs)
             (mkCrash ("Unhandled input for " ++ show n ++ " at " ++ show fc))

    addErrorCase : List Clause -> List Clause
    addErrorCase [] = []
    addErrorCase [MkClause env lhs rhs]
        = MkClause env lhs rhs :: makeErrorClause env lhs :: []
    addErrorCase (x :: xs) = x :: addErrorCase xs

    getSpec : List DefFlag -> Maybe (List (Name, Nat))
    getSpec [] = Nothing
    getSpec (PartialEval n :: _) = Just n
    getSpec (x :: xs) = getSpec xs

    toErased : FC -> Maybe (List (Name, Nat)) ->
               (vars ** (Env Term vars, Term vars, Term vars)) ->
               Core (vars ** (Env Term vars, Term vars, Term vars))
    toErased fc spec (_ ** (env, lhs, rhs))
        = do lhs_erased <- linearCheck fc linear True env lhs
             -- Partially evaluate RHS here, where appropriate
             rhs' <- applyTransforms env rhs
             rhs' <- applySpecialise env spec rhs'
             rhs_erased <- linearCheck fc linear True env rhs'
             pure (_ ** (env, lhs_erased, rhs_erased))

    toClause : FC -> (vars ** (Env Term vars, Term vars, Term vars)) -> Clause
    toClause fc (_ ** (env, lhs, rhs))
        = MkClause env lhs rhs

compileRunTime : {auto c : Ref Ctxt Defs} ->
                 {auto m : Ref MD Metadata} ->
                 {auto u : Ref UST UState} ->
                 FC -> Name -> Core ()
compileRunTime fc atotal
    = do defs <- get Ctxt
         traverse_ (mkRunTime fc) (toCompileCase defs)
         traverse_ (calcRefs True atotal) (toCompileCase defs)

         defs <- get Ctxt
         put Ctxt (record { toCompileCase = [] } defs)

toPats : Clause -> (vs ** (Env Term vs, Term vs, Term vs))
toPats (MkClause {vars} env lhs rhs)
    = (_ ** (env, lhs, rhs))

warnUnreachable : {auto c : Ref Ctxt Defs} ->
                  Clause -> Core ()
warnUnreachable (MkClause env lhs rhs)
    = recordWarning (UnreachableClause (getLoc lhs) env lhs)

export
processDef : {vars : _} ->
             {auto c : Ref Ctxt Defs} ->
             {auto m : Ref MD Metadata} ->
             {auto u : Ref UST UState} ->
             List ElabOpt -> NestedNames vars -> Env Term vars -> FC ->
             Name -> List ImpClause -> Core ()
processDef opts nest env fc n_in cs_in
    = do n <- inCurrentNS n_in
         defs <- get Ctxt
         Just gdef <- lookupCtxtExact n (gamma defs)
              | Nothing => noDeclaration fc n
         let None = definition gdef
              | _ => throw (AlreadyDefined fc n)
         let ty = type gdef
         let hashit = visibility gdef == Public
         let mult = if isErased (multiplicity gdef)
                       then erased
                       else linear
         nidx <- resolveName n

         -- Dynamically rebind default totality requirement to this function's totality requirement
         -- and use this requirement when processing `with` blocks
         log "declare.def" 5 $ "Traversing clauses of " ++ show n ++ " with mult " ++ show mult
         let treq = fromMaybe !getDefaultTotalityOption (findSetTotal (flags gdef))
         cs <- withTotality treq $
               traverse (checkClause mult (visibility gdef) treq
                                     hashit nidx opts nest env) cs_in

         let pats = map toPats (rights cs)

         (cargs ** (tree_ct, unreachable)) <-
             getPMDef fc (CompileTime mult) n ty (rights cs)

         traverse_ warnUnreachable unreachable

         logC "declare.def" 2 $
                 do t <- toFullNames tree_ct
                    pure ("Case tree for " ++ show n ++ ": " ++ show t)

         -- check whether the name was declared in a different source file
         defs <- get Ctxt
         let pi = case lookup n (userHoles defs) of
                        Nothing => defaultPI
                        Just e => record { externalDecl = e } defaultPI
         -- Add compile time tree as a placeholder for the runtime tree,
         -- but we'll rebuild that in a later pass once all the case
         -- blocks etc are resolved
         ignore $ addDef (Resolved nidx)
                  (record { definition = PMDef pi cargs tree_ct tree_ct pats
                          } gdef)

         when (visibility gdef == Public) $
             do let rmetas = getMetas tree_ct
                log "declare.def" 10 $ "Saving from " ++ show n ++ ": " ++ show (keys rmetas)
                traverse_ addToSave (keys rmetas)
         when (isUserName n && visibility gdef /= Private) $
             do let tymetas = getMetas (type gdef)
                traverse_ addToSave (keys tymetas)
         addToSave n

         -- Flag this name as one which needs compiling
         defs <- get Ctxt
         put Ctxt (record { toCompileCase $= (n ::) } defs)

         atotal <- toResolvedNames (NS builtinNS (UN $ Basic "assert_total"))
         when (not (InCase `elem` opts)) $
             do calcRefs False atotal (Resolved nidx)
                sc <- calculateSizeChange fc n
                setSizeChange fc n sc
                checkIfGuarded fc n

         md <- get MD -- don't need the metadata collected on the coverage check

         cov <- logTime ("+++ Checking Coverage " ++ show n) $ checkCoverage nidx ty mult cs
         setCovering fc n cov
         put MD md

         -- If we're not in a case tree, compile all the outstanding case
         -- trees.
         when (not (elem InCase opts)) $
              compileRunTime fc atotal
  where
    -- Move `withTotality` to Core.Context if we need it elsewhere
    ||| Temporarily rebind the default totality requirement (%default total/partial/covering).
    withTotality : TotalReq -> Lazy (Core a) -> Core a
    withTotality tot c = do
         defaultTotality <- getDefaultTotalityOption
         setDefaultTotalityOption tot
         x <- catch c (\error => do setDefaultTotalityOption defaultTotality
                                    throw error)
         setDefaultTotalityOption defaultTotality
         pure x

    simplePat : forall vars . Term vars -> Bool
    simplePat (Local _ _ _ _) = True
    simplePat (Erased _ _) = True
    simplePat (As _ _ _ p) = simplePat p
    simplePat _ = False

    -- Is the clause returned from 'checkClause' a catch all clause, i.e.
    -- one where all the arguments are variables? If so, no need to do the
    -- (potentially expensive) coverage check
    catchAll : Clause -> Bool
    catchAll (MkClause env lhs _)
       = all simplePat (getArgs lhs)

    -- Return 'Nothing' if the clause is impossible, otherwise return the
    -- checked clause (with implicits filled in, so that we can see if they
    -- match any of the given clauses)
    checkImpossible : Int -> RigCount -> ClosedTerm ->
                      Core (Maybe ClosedTerm)
    checkImpossible n mult tm
        = do itm <- unelabNoPatvars [] tm
             let itm = map rawName itm
             handleUnify
               (do ctxt <- get Ctxt
                   log "declare.def.impossible" 3 $ "Checking for impossibility: " ++ show itm
                   autoimp <- isUnboundImplicits
                   setUnboundImplicits True
                   (_, lhstm) <- bindNames False itm
                   setUnboundImplicits autoimp
                   (lhstm, _) <- elabTerm n (InLHS mult) [] (MkNested []) []
                                    (IBindHere fc PATTERN lhstm) Nothing
                   defs <- get Ctxt
                   lhs <- normaliseHoles defs [] lhstm
                   if !(hasEmptyPat defs [] lhs)
                      then do log "declare.def.impossible" 5 "No empty pat"
                              put Ctxt ctxt
                              pure Nothing
                      else do log "declare.def.impossible" 5 "Some empty pat"
                              empty <- clearDefs ctxt
                              rtm <- closeEnv empty !(nf empty [] lhs)
                              put Ctxt ctxt
                              pure (Just rtm))
               (\err => do defs <- get Ctxt
                           if not !(recoverableErr defs err)
                              then pure Nothing
                              else pure (Just tm))
      where
        closeEnv : Defs -> NF [] -> Core ClosedTerm
        closeEnv defs (NBind _ x (PVar _ _ _ _) sc)
            = closeEnv defs !(sc defs (toClosure defaultOpts [] (Ref fc Bound x)))
        closeEnv defs nf = quote defs [] nf

    getClause : Either RawImp Clause -> Core (Maybe Clause)
    getClause (Left rawlhs)
        = catch (do lhsp <- getImpossibleTerm env nest rawlhs
                    log "declare.def.impossible" 3 $ "Generated impossible LHS: " ++ show lhsp
                    pure $ Just $ MkClause [] lhsp (Erased (getFC rawlhs) True))
                (\e => do log "declare.def" 5 $ "Error in getClause " ++ show e
                          pure Nothing)
    getClause (Right c) = pure (Just c)

    checkCoverage : Int -> ClosedTerm -> RigCount ->
                    List (Either RawImp Clause) ->
                    Core Covering
    checkCoverage n ty mult cs
        = do covcs' <- traverse getClause cs -- Make stand in LHS for impossible clauses
             log "declare.def" 5 $ unlines
               $ "Using clauses :"
               :: map (("  " ++) . show) !(traverse toFullNames covcs')
             let covcs = mapMaybe id covcs'
             (_ ** (ctree, _)) <-
                 getPMDef fc (CompileTime mult) (Resolved n) ty covcs
             log "declare.def" 3 $ "Working from " ++ show !(toFullNames ctree)
             missCase <- if any catchAll covcs
                            then do log "declare.def" 3 $ "Catch all case in " ++ show n
                                    pure []
                            else getMissing fc (Resolved n) ctree
             logC "declare.def" 3 $
                     do mc <- traverse toFullNames missCase
                        pure ("Initially missing in " ++
                                 show !(getFullName (Resolved n)) ++ ":\n" ++
                                showSep "\n" (map show mc))
             -- Filter out the ones which are impossible
             missImp <- traverse (checkImpossible n mult) missCase
             -- Filter out the ones which are actually matched (perhaps having
             -- come up due to some overlapping patterns)
             missMatch <- traverse (checkMatched covcs) (mapMaybe id missImp)
             let miss = mapMaybe id missMatch
             if isNil miss
                then do [] <- getNonCoveringRefs fc (Resolved n)
                           | ns => toFullNames (NonCoveringCall ns)
                        pure IsCovering
                else pure (MissingCases miss)


text:
reshape : Vector (x1::(m * x2)::xs) t ->
          Vector((x1 * m)::x2::xs) t
reshape [] = []
reshape (v::vs) = incDim v ++ reshape' vs

ext: idr

max_stars_repo_name: RossMeikleham/MSci-Project

max_issues_repo_name: RossMeikleham/MSci-Project

max_forks_repo_name: RossMeikleham/MSci-Project


text:
module Test

interface Foo a where
  bar : a -> {auto ok: ()} -> a

foo : Void -> {auto ok: ()} -> Void
foo = ?foo_hole

baz : a -> b -> c -> {auto x : a} -> a
baz {} = x


text:
module Props.Util

import public Data.List

%access public export

private
mkNo : {xs' : List a} ->
       ((x' = y') -> Void) ->
       (Elem x' xs' -> Void) ->
       Elem x' (y' :: xs') -> Void
mkNo f g Here = f Refl
mkNo f g (There x) = g x

-- Use this until https://github.com/idris-lang/Idris-dev/issues/4161
fastIsElem : DecEq a => (x : a) -> (xs : List a) -> Dec (Elem x xs)
fastIsElem x [] = No absurd
fastIsElem x (y :: xs) with (decEq x y)
  fastIsElem x (x :: xs) | (Yes Refl) = Yes Here
  fastIsElem x (y :: xs) | (No contra) with (fastIsElem x xs)
    fastIsElem x (y :: xs) | (No contra) | (Yes prf) = Yes (There prf)
    fastIsElem x (y :: xs) | (No contra) | (No f) = No (mkNo contra f)

using (a: Type, P : a -> Type, Q: a -> Type)

  data EitherK : { a : Type } -> ( P : a -> Type ) -> ( Q : a -> Type) -> a -> Type where
    LeftK : ( prf : P c ) -> EitherK P Q c
    RightK : ( prf : Q c ) -> EitherK P Q c

-- Add these to not depend on contrib
data Given : Dec x -> Type where
  Always : Given (Yes prf)

data Denied : Dec x -> Type where
  Never : Denied (No contra)

max_stars_repo_name: janschultecom/idris-refined

max_issues_repo_name: janschultecom/idris-refined

max_forks_repo_name: janschultecom/idris-refined


text:
module Deps.Lexer

-- Implementation heavily inspired by Idris' Language.JSON and Blodwen

import public Text.Lexer

%default total
%access public export

data IdrisTokenKind
  = Ignore
  | Symbol
  | Identifier

Show a => Show (Token a) where
  show (Tok x _) = show x

Show IdrisTokenKind where
  show Ignore = " "
  show Symbol = "symbol"
  show Identifier = "identifier"

Eq IdrisTokenKind where
  (==) Ignore Ignore = True
  (==) Symbol Symbol = True
  (==) Identifier Identifier = True
  (==) _ _ = False

TokenKind IdrisTokenKind where
  TokType Ignore = ()
  TokType Symbol = String
  TokType Identifier = String

  tokValue Ignore x = ()
  tokValue Symbol x = x
  tokValue Identifier x = x

IdrisToken : Type
IdrisToken = Token IdrisTokenKind

comment : Lexer
comment = is '-' <+> is '-' <+> many (isNot '\n')

commentAuxStyle : Lexer
commentAuxStyle = is '|' <+> is '|' <+> is '|' <+> many (isNot '\n')

toEndComment : (k : Nat) -> Recognise (k /= 0)
toEndComment Z = empty
toEndComment (S k) =
  some (pred (\c => c /= '-' && c /= '{')) <+> toEndComment (S k) <|>
    is '{' <+> is '-' <+> toEndComment (S (S k)) <|>
    is '-' <+> is '}' <+> toEndComment k <|>
    is '{' <+> toEndComment (S k) <|>
    is '-' <+> toEndComment (S k)

blockComment : Lexer
blockComment = is '{' <+> is '-' <+> toEndComment 1

ident : Lexer
ident = pred startIdent <+> many (pred validIdent)
  where
    startIdent : Char -> Bool
    startIdent '_' = True
    startIdent x = isAlpha x

    validIdent : Char -> Bool
    validIdent '_' = True
    validIdent '\'' = True
    validIdent x = isAlphaNum x

tokenMap : TokenMap IdrisToken
tokenMap = toTokenMap
  [ (comment, Ignore)
  , (commentAuxStyle, Ignore)
  , (blockComment, Ignore)
  , (spaces, Ignore)
  , (symbols, Symbol)
  , (ident, Identifier)
  ]

runLexer : String -> List (TokenData IdrisToken)
runLexer str =
  let (res, _) = lex tokenMap str
  in res

ignored : IdrisToken -> Bool
ignored (Tok Ignore _) = True
ignored _ = False

max_stars_repo_name: chrrasmussen/Idris-Deps

max_issues_repo_name: chrrasmussen/Idris-Deps

max_forks_repo_name: chrrasmussen/Idris-Deps


text:
module Algebraic

-- Example functions

or : Bool -> Bool -> Bool
or p q = p || q

xor : Bool -> Bool -> Bool
xor p q = (p || q) && not (p && q)

-- Idempotency

Idempotent : (a -> a) -> a -> Type
Idempotent f a = f (f a) = f a

-- Involution

notNotTrue : not (not True) = True
notNotTrue = ?notNotTrue

notNotFalse : not (not False) = False
notNotFalse = ?notNotFalse

notNot : (b : Bool) -> not (not b) = b
notNot b = ?notNot

Involution : (a -> a) -> a -> Type
Involution f a = f (f a) = a

xorInvolution : (a : Bool) -> (b : Bool) -> Involution (xor a) b
xorInvolution a b = ?xorInvolution

-- Uninhabited

notNotIdempotent : (b : Bool) -> Idempotent not b -> Void
notNotIdempotent b prf = ?notNotIdempotent

succNotIdempotent : (n : Nat) -> Idempotent S n -> Void
succNotIdempotent n prf = ?succNotIdempotent

-- Both

idempotentInvolution : Idempotent f a -> Involution f a -> f a = a
idempotentInvolution idem invo = ?idempotentInvolution


text:
module Fix

%access public export

data Fix : (f : Type -> Type) -> Type where
    In : f (Fix f) -> Fix f

Show (f (Fix f)) => Show (Fix f) where
    show x = "In " ++ show x

inop : Fix f -> f (Fix f)
inop (In x) = x

cata : Functor f => (f a -> a) -> Fix f -> a
cata alg = alg . map (cata alg) . inop

max_stars_repo_name: BakerSmithA/alacarte-idris

max_issues_repo_name: BakerSmithA/alacarte-idris

max_forks_repo_name: BakerSmithA/alacarte-idris


text:
module Rhone.JS.Input

import Control.Monad.Dom
import Data.MSF
import JS
import Rhone.JS.Sink
import Rhone.JS.Source
import Web.Dom
import Web.Html

fireAndHold : o -> MSF m (Event o) (NP I [o, Event o])
fireAndHold v = fan [hold v, id <|> once v]

export
input :  LiftJSIO m
      => (getInput : ev -> Event String)
      -> (read     : String -> Either String a)
      -> (ref      : ElemRef HTMLInputElement)
      -> MSF m ev (Either String a)
input get read ref =
      map read . get
  ^>> fireAndHold (read "")
  >>> par [id, ifEvent (leftInvalid ref)]
  >>> hd

export
getInput :  LiftJSIO m
         => Eq ev
         => ev
         -> (read     : String -> Either String a)
         -> (ref      : ElemRef HTMLInputElement)
         -> MSF m ev (Either String a)
getInput e read ref =
      bool (e ==)
  >>> collect [valueOf ref >>^ Ev . read, never]
  >>> fireAndHold (read "")
  >>> par [id, ifEvent (leftInvalid ref)]
  >>> hd


text:
module GTK.Utils

export
nullanyptr : AnyPtr
nullanyptr = prim__getNullAnyPtr

export
nullptr : Ptr a
nullptr = prim__castPtr $ nullanyptr

export
cast : Ptr a -> Ptr b
cast = believe_me

public export
CBool : Type
CBool = Bits8

public export
false, true : CBool
false = 0
true = 1


text:
module Issue1328A
%default total

infix 4 `InCtx`
data InCtx : (a, b : Type) -> Type where

prop0 : a `InCtx` b
prop0 = ?undef_0

prop1 : (`InCtx` b) a
prop1 = ?undef_1

prop2 : (a `InCtx`) b
prop2 = ?undef_2

def0 : (m, n : Integer) -> Integer
def0 m n = m `div` n

def1 : (m, n : Integer) -> Integer
def1 m n = (`div` n) m

def2 : (m, n : Integer) -> Integer
def2 m n = (m `div`) n

infix 4 |-
data (|-) : (a, b : Type) -> Type where

inProp0 : a |- b
inProp0 = ?undef_3

inProp1 : (|- b) a
inProp1 = ?undef_4

inProp2 : (a |-) b
inProp2 = ?undef_5

inDef0 : Nat
inDef0 = 42 + 21

inDef1 : Nat
inDef1 = (+ 21) 42

inDef2 : Nat
inDef2 = (42 +) 21


text:
module Toml

import Data.List
import Data.String
import Extra.String
import Toml.Parser
import Toml.Lexer

import Text.Bounded

import public Toml.Data

||| Parse a Toml document
export
parseToml : String -> Maybe Toml
parseToml x = parseTomlToks !(lexToml x)

||| Encode a Toml document with raw keys
export
encode : Toml -> String
encode =
  join "\n" . map showVal
  where
    showKeyPart : String -> String
    showKeyPart k =
      if includesAny ".=\"'" k
        then quote k
        else k

    showKey : List String -> String
    showKey =
      join "." . map showKeyPart

    showVal : (List String, Value) -> String
    showVal (key, ArrTab l) =
      let
        heading = (++) ("[[" ++ (showKey key) ++ "]]\n")
        contents = map (heading . encode) l
      in
        join "\n\n" contents

    showVal (key, value) =
      let
        k = showKey key
        v = show value
      in
        k ++ "=" ++ v

export
get : List String -> Toml -> Maybe Value
get key =
  (map snd) . (find ((== key) . fst))

export
getToml : List String -> Toml -> Toml
getToml key =
  (map (mapFst (drop (length key)))) . (filter (isPrefixOf key . fst))

max_stars_repo_name: Z-snails/inigo

max_issues_repo_name: Z-snails/inigo

max_forks_repo_name: Z-snails/inigo


text:
module Text.Html

import public Data.SOP
import public Text.Html.Attribute as Html
import public Text.Html.Event as Html
import public Text.Html.Node as Html


text:
module Inigo.Async.CloudFlare.Worker

import Data.Buffer
import Data.List
import Inigo.Async.Promise

public export
Headers : Type
Headers = List (String, String)

public export
Response : Type
Response = (Int, String, Headers)

export
html : String -> Response
html content =
  (200, content, [("Content-Type", "text/html")])

-- Could maybe make use of `__prim_js2idris_array`
%foreign "javascript:lambda:(status,body,headers)=>{let toArray=((list)=>Object.fromEntries([...Array(list.h).keys()].map((i)=>{let x=list['a'+(i+1)];return [x.a1,x.a2]})));return new Response(body, {status: status, headers: toArray(headers)});}"
prim__response : Int -> String -> List (String, String) -> PrimIO ()

-- Note: can't use "Buffer" body here, needs to be an ArrayBuffer
%foreign "javascript:lambda:(handler,w)=>addEventListener('fetch',e=>e.respondWith(e.request.text().then((r)=>handler((url=new URL(e.request.url)).pathname)(r || '')(__prim_js2idris_array([...url.searchParams.entries()].flat()))(__prim_js2idris_array([...e.request.headers.entries()].flat()))(w))))"
prim__httpServer : (String -> String -> List String -> List String -> IO ()) -> PrimIO ()

handleResponse : (Int, String, Headers) -> PrimIO ()
handleResponse (status, err, headers) =
  prim__response status err headers

primHandler : Promise Response -> IO ()
primHandler handler =
  resolve handler (primIO . handleResponse) (primIO . (\err => handleResponse (500, err, [])))

pairList : List a -> List (a, a)
pairList =
  fst . foldl accumulate ([], Nothing) . Data.List.reverse
  where
    accumulate : (List (a, a), Maybe a) -> a -> (List (a, a), Maybe a)
    accumulate (acc, Nothing) x = (acc, Just x)
    accumulate (acc, Just y) x = ((x, y) :: acc, Nothing)

httpServer : (String -> String -> List (String, String) -> List (String, String) -> Promise Response) -> Promise ()
httpServer handler =
  do
    liftIO $ (primIO $ prim__httpServer ioHandler)
    pure ()
  where
    -- Not sure why this wouldn't compile in point-free style
    ioHandler : String -> String -> List String -> List String -> IO ()
    ioHandler path body params headers = primHandler (handler path body (pairList params) (pairList headers))

export
serve : (String -> String -> List (String, String) -> List (String, String) -> Promise Response) -> Promise ()
serve handler =
  httpServer handler


text:
module Idris.Codegen.ExtSTG.STG

import public Data.List
import public Idris.Codegen.ExtSTG.GHCPrimOp
import public Idris.Codegen.ExtSTG.Prelude
import public Idris.Codegen.ExtSTG.Representation

{-
This module contains the definitions of the STG. We mirror the current internals of GHC.
-}

public export
Name : Type
Name = String

public export
IdInfo : Type
IdInfo = String

||| Unique identifier for different things, such as TyConId, DataConId, BinderId, etc
|||
||| The character parameter is used in the different phases of
||| the code generator by GHC and it can be used at will.
public export
data Unique
  = MkUnique Char Int

Eq Unique where
  (MkUnique c0 i0) == (MkUnique c1 i1) = (c0,i0) == (c1,i1)

export
Show Unique where
  show (MkUnique c i) = "(MkUnique " ++ show c ++ " " ++ show i ++ ")"

public export
record RealSrcSpan where
  constructor MkRealSrcSpan
  SpanFile  : Name
  SpanSLine : Int
  SpanSCol  : Int
  SpanELine : Int
  SpanECol  : Int

public export
record BufSpan where
  constructor MkBufSpan
  BufSpanStart : Int
  BufSpanEnd   : Int

public export
data SrcSpan
  = SsRealSrcSpan   RealSrcSpan (Maybe BufSpan)
  | SsUnhelpfulSpan Name

public export
data TyConId = MkTyConId Unique

export
tyConUnique : TyConId -> Unique
tyConUnique (MkTyConId u) = u

export
Eq TyConId where
  (MkTyConId t0) == (MkTyConId t1) = t0 == t1

export
Show TyConId where
  show (MkTyConId t0) = "(MkTyConId " ++ show t0 ++ ")"

public export
data DataConRep
  = AlgDataCon      (List PrimRep)
  | UnboxedTupleCon Nat
  -- TODO: Add the PrimRep list here, or a different constructor.

export
Show DataConRep where
  showPrec p (AlgDataCon reps) = showCon p "AlgDataCon" $ showArg reps
  showPrec p (UnboxedTupleCon n) = showCon p "UnboxedTupleCon" $ showArg n

export
SemiDecEq DataConRep where
  semiDecEq (AlgDataCon xs) (AlgDataCon ys) = do
    Refl <- semiDecEq xs ys
    Just Refl
  semiDecEq (UnboxedTupleCon x) (UnboxedTupleCon y) = do
    Refl <- semiDecEq x y
    Just Refl
  semiDecEq _ _ = Nothing

public export
data DataConId : DataConRep -> Type where
  MkDataConId : {0 r : DataConRep} -> Unique -> DataConId r

export
Show (DataConId q) where
  show (MkDataConId u) = show u

public export
DataConIdSg : Type
DataConIdSg = (r : DataConRep ** DataConId r)

public export
mkDataConIdSg : {r : DataConRep} -> DataConId r -> DataConIdSg
mkDataConIdSg {r} d = (r ** d)

export
unsafeMkDataConIdSg : (r : DataConRep) -> Unique -> (r ** DataConId r)
unsafeMkDataConIdSg r u = (r ** MkDataConId u)

export
checkDataConIdRep : (r : DataConRep) -> DataConIdSg -> Maybe (DataConId r)
checkDataConIdRep r (q ** d) = case semiDecEq r q of
  Nothing   => Nothing
  Just Refl => Just d

export
dataConUnique : DataConId r -> Unique
dataConUnique (MkDataConId u) = u

public export
record ModuleName where
  constructor MkModuleName
  GetModuleName : Name

||| The package name of the module.
public export
record UnitId where
  constructor MkUnitId
  GetUnitId : Name

public export
data IdDetails
  = VanillaId
  | FExportedId
  | RecSelId
  | DataConWorkId DataConIdSg
  | DataConWrapId DataConIdSg
  | ClassOpId
  | PrimOpId
  | TickBoxOpId
  | DFunId
  | CoVarId
  | JoinId Int

public export
data Scope
  = LocalScope      -- visible for expression body
  | GlobalScope     -- visible for a single haskell module
  | HaskellExported -- visible for every haskell module
  | ForeignExported -- visible for foreign libraries

-- NOTE: TypeSig is used only in FFI
-- The parameters should be TODO: ...

public export
data BinderId : RepType -> Type where
  MkBinderId : {0 r : RepType} -> Unique -> BinderId r

export
getBinderIdUnique : BinderId r -> Unique
getBinderIdUnique (MkBinderId u) = u

public export
BinderIdSg : Type
BinderIdSg = (r : RepType ** BinderId r)

%hint
export
mkBinderIdSg : {r : RepType} -> BinderId r -> BinderIdSg
mkBinderIdSg {r} b = (r ** b)

namespace SBinder

  -- TODO: Use record
  public export
  data SBinder : RepType -> Type where
    MkSBinder
      :  (binderName : Name)
      -> (binderRep : RepType)
      -> (binderId : BinderId binderRep)
      -> (binderTypeSig : String)
      -> (binderScope : Scope)
      -> (binderDetails : IdDetails)
      -> (binderInfo : IdInfo)
      -> (binderDefLoc : SrcSpan)
      -> SBinder binderRep

  public export
  SBinderSg : Type
  SBinderSg = (r : RepType ** SBinder r)

  public export
  LiftedRepBinder : Type
  LiftedRepBinder = SBinder (SingleValue LiftedRep)

  %hint
  export
  mkSBinderSg : {r : RepType} -> SBinder r -> SBinderSg
  mkSBinderSg {r} s = (r ** s)

  export
  binderName : SBinder r -> Name
  binderName (MkSBinder n r i t s d f c) = n

  export
  binderId : SBinder r -> BinderId r
  binderId (MkSBinder n r i t s d f c) = i

  export
  binderRep : SBinder r -> RepType
  binderRep (MkSBinder n r i t s d f c) = r

  export
  binderTypeSig : SBinder r -> Name
  binderTypeSig (MkSBinder n r i t s d f c) = t

  export
  binderScope : SBinder r -> Scope
  binderScope (MkSBinder n r i t s d f c) = s

  export
  binderDetails : SBinder r -> IdDetails
  binderDetails (MkSBinder n r i t s d f c) = d

  export
  binderInfo : SBinder r -> IdInfo
  binderInfo (MkSBinder n r i t s d f c) = f

  export
  binderDefLoc : SBinder r -> SrcSpan
  binderDefLoc (MkSBinder n r i t s d f c) = c

export
getSBinderIdSg : SBinderSg -> BinderIdSg
getSBinderIdSg (r ** b) = (r ** binderId b)

namespace SDataCon

  -- TODO: Use record
  public export
  data SDataCon : DataConRep -> Type where
    MkSDataCon
      :  (dataConName : Name)
      -> (dataConRep  : DataConRep)
      -> (dataConId   : DataConId dataConRep)
      -> (dataConWorker : LiftedRepBinder) -- TODO: It needs for the codegen, but it is not clear its real purpose.
      -> (dataConDefLoc : SrcSpan)
      -> SDataCon dataConRep

  export
  name : SDataCon r -> Name
  name (MkSDataCon n i r b s) = n

  export
  ident : SDataCon r -> DataConId r
  ident (MkSDataCon n r i b s) = i

  export
  rep : SDataCon r -> DataConRep
  rep (MkSDataCon n r i b s) = r

  export
  worker : SDataCon r -> LiftedRepBinder
  worker (MkSDataCon n r i b s) = b

  export
  defLoc : SDataCon r -> SrcSpan
  defLoc (MkSDataCon n r i b s) = s

  public export
  SDataConSg : Type
  SDataConSg = (r ** SDataCon r)

  export
  mkSDataConSg : {r : DataConRep} -> SDataCon r -> SDataConSg
  mkSDataConSg {r} d = (r ** d)

export
Show (SDataCon r) where
  show s = show (name s)

export
Show SDataConSg where
  show (r ** d) = show d

public export
record STyCon where
  constructor MkSTyCon
  Name     : Name
  Id       : TyConId
  DataCons : (List SDataConSg)
  DefLoc   : SrcSpan

export
Show STyCon where
  show (MkSTyCon n i _ _) = "(MkSTyCon " ++ show n ++ " " ++ show i ++ " _ _)"

public export
data LitNumType
  = LitNumInt    -- Int#   according to target machine
  | LitNumInt64  -- Int64# exactly 64 bits
  | LitNumWord   -- Word#  according to target machine
  | LitNumWord64 -- Word64 exactly 64 bits

public export
data LabelSpec
  = FunctionLabel (Maybe Int) -- only for stdcall convention
    -- ^^ Can be called, CCallTarge, foreign call op.
  | DataLabel
    -- ^^ Can not be called.

public export
data Lit
  = LitChar     Char
  | LitString   String
    -- ^^ The String literal in STG is not the String literal in Haskell. This stands for literals which are byte strings.
    -- TODO: Describe how top level strings are the real String literals in STG programs, and how Strings are represented
    --       as ByteArrays.
    -- In Argument and expression literal when evaluated it will be put on the static data segment, same as
    -- top literals, but without binders. And the AddrRep is returned without any allocation.
    -- String literals are forbidden in matching alts, they should be represented as primitive
    -- functions
    -- Worker-Wrapper transformation, build a lazy-list Char.
  | LitNullAddr
  | LitFloat    Double -- TODO: Represent floats
  | LitDouble   Double
  | LitLabel    String LabelSpec
    -- ^^ Its representation type is AddrRep
    -- Label in assembly, which is a pointer. Static array from FFI, static string from FFI
    -- It contains the name of the symbol.
  | LitNumber   LitNumType Integer

export
Show Lit where
  showPrec d (LitChar     c) = showCon d "LitChar" $ showArg c
  showPrec d (LitString   s) = showCon d "LitString" $ showArg s
  showPrec d LitNullAddr     = "LitNullAddr"
  showPrec d (LitFloat    x) = showCon d "LitFloat" $ showArg x
  showPrec d (LitDouble   x) = showCon d "LitDouble" $ showArg x
  showPrec d (LitLabel    s l) = showCon d "LitLabel" $ showArg s ++ " ..."
  showPrec d (LitNumber   l i) = showCon d "LitNumber" $ "... " ++ showArg i

public export
data AltType
  = PolyAlt -- Instead of ForceBoxed
  | MultiValAlt Nat
  | PrimAlt     PrimRep
  | AlgAlt      TyConId

public export
litRepType : Lit -> RepType
litRepType (LitChar   _) = SingleValue Word8Rep
litRepType (LitString _) = SingleValue AddrRep
litRepType (LitNullAddr) = SingleValue AddrRep
litRepType (LitFloat  _) = SingleValue FloatRep
litRepType (LitDouble _) = SingleValue DoubleRep
litRepType (LitLabel _ _) = SingleValue AddrRep
litRepType (LitNumber LitNumInt    _) = SingleValue IntRep
litRepType (LitNumber LitNumInt64  _) = SingleValue Int64Rep
litRepType (LitNumber LitNumWord   _) = SingleValue WordRep
litRepType (LitNumber LitNumWord64 _) = SingleValue Word64Rep

public export
data Arg : RepType -> Type where
  StgVarArg : BinderId r -> Arg r
  StgLitArg : {0 r : RepType} -> (l : Lit) -> (0 _ : r = litRepType l) => Arg r
  StgVoid   : Arg (SingleValue VoidRep)

public export
ArgSg : Type
ArgSg = (r : RepType ** Arg r)

%hint
export
mkArgSg : {r : RepType} -> Arg r -> ArgSg
mkArgSg {r} a = (r ** a)

namespace ArgList
  public export
  data ArgList : List PrimRep -> Type where
    Nil  : ArgList []
    (::) : Arg (SingleValue r) -> ArgList rs -> ArgList (r :: rs)

public export
StgConAppArgType : DataConRep -> Type
StgConAppArgType (AlgDataCon [])  = ()
StgConAppArgType (AlgDataCon [p]) = Arg (SingleValue p)
StgConAppArgType (AlgDataCon (p0 :: p1 :: ps)) = ArgList (p0 :: p1 :: ps)
StgConAppArgType (UnboxedTupleCon n) = Void

public export
StgOpArgType : List PrimRep -> Type
StgOpArgType [] = ()
StgOpArgType [r] = Arg (SingleValue r)
StgOpArgType (r1 :: r2 :: rs) = ArgList (r1 :: r2 :: rs)

namespace BinderList
  public export
  data BinderList : List PrimRep -> Type where
    Nil  : BinderList []
    (::) : SBinder (SingleValue r) -> BinderList rs -> BinderList (r :: rs)

  export
  toArgList : BinderList rs -> ArgList rs
  toArgList [] = []
  toArgList (x :: xs) = StgVarArg (binderId x) :: toArgList xs

public export
data IsAltLit : Lit -> Type where
  CharAltLit   : IsAltLit (LitChar c)
  FloatAltLit  : IsAltLit (LitFloat f)
  DoubleAltLit : IsAltLit (LitDouble d)
  NumberAltLit : IsAltLit (LitNumber t n)

export
decAltLit : (l : Lit) -> Maybe (IsAltLit l)
decAltLit (LitChar c)     = Just CharAltLit
decAltLit (LitFloat f)    = Just FloatAltLit
decAltLit (LitDouble d)   = Just DoubleAltLit
decAltLit (LitNumber t n) = Just NumberAltLit
decAltLit other = Nothing

public export
data AltCon : RepType -> Type where
  AltDataCon : DataConIdSg                     -> AltCon (SingleValue LiftedRep)
  AltLit     : (l : Lit) -> (0 _ : IsAltLit l) => AltCon (litRepType l)
  AltDefault : {0 r : RepType}                 -> AltCon r

public export
data UpdateFlag
  = ReEntrant
  | Updatable
  | SingleEntry

public export
data CCallConv
  = MkCCallConv
  | CApiConv
  | StdCallConv
  | PrimCallConv
  | JavaScriptCallConv

public export
data SourceText
  = MkSourceText String
  | NoSourceText

public export
data CCallTarget
  = StaticTarget SourceText String (Maybe UnitId) Bool
  | DynamicTarget

public export
data Safety
  = PlaySafe
  | PlayInterruptible
  | PlayRisky

public export
record ForeignCall where
  constructor MkForeignCall
  CTarget : CCallTarget
  CConv   : CCallConv
  CSafety : Safety

public export
data PrimCall = MkPrimCall String UnitId

-- TODO: Make a name and type description of STG primitive operations
-- as in Idris PrimOp
public export
data StgOp
  = StgPrimOp     Name
  | StgPrimCallOp PrimCall
  | StgFCallOp    ForeignCall

namespace BList
  ||| BinderList, specialized list for storing special Binders in STG alternatives.
  public export
  data BList : List PrimRep -> Type where
    Nil  : BList []
    (::) : SBinder (SingleValue p) -> BList ps -> BList (p :: ps)

public export
DataConRepType : DataConRep -> Type
DataConRepType (AlgDataCon [])     = ()
DataConRepType (AlgDataCon [p])    = SBinder (SingleValue p)
DataConRepType (AlgDataCon (p0 :: p1 :: ps)) = BList (p0 :: p1 :: ps)
DataConRepType (UnboxedTupleCon n) = Void

public export
AltBinderType : AltCon r -> Type
AltBinderType (AltDataCon d) = DataConRepType (fst d)
AltBinderType (AltLit l)     = ()
AltBinderType AltDefault     = ()

public export
altRepType : AltType -> RepType
altRepType PolyAlt         = SingleValue LiftedRep -- Used only for forced values
altRepType (MultiValAlt 0) = SingleValue VoidRep -- For VoidRep PrimOps
altRepType (MultiValAlt n) = UnboxedTuple (replicate n VoidRep) -- Invalid, but unused
altRepType (PrimAlt p)     = SingleValue p
altRepType (AlgAlt t)      = SingleValue LiftedRep

public export
decLitRepType : (l : Lit) -> (r : RepType) -> Maybe (litRepType l = r)
decLitRepType (LitChar   _)              (SingleValue Word8Rep)  = Just Refl
decLitRepType (LitString _)              (SingleValue AddrRep)   = Just Refl
decLitRepType (LitNullAddr)              (SingleValue AddrRep)   = Just Refl
decLitRepType (LitFloat  _)              (SingleValue FloatRep)  = Just Refl
decLitRepType (LitDouble _)              (SingleValue DoubleRep) = Just Refl
decLitRepType (LitLabel _ _)             (SingleValue AddrRep)   = Just Refl
decLitRepType (LitNumber LitNumInt    _) (SingleValue IntRep)    = Just Refl
decLitRepType (LitNumber LitNumInt64  _) (SingleValue Int64Rep)  = Just Refl
decLitRepType (LitNumber LitNumWord   _) (SingleValue WordRep)   = Just Refl
decLitRepType (LitNumber LitNumWord64 _) (SingleValue Word64Rep) = Just Refl
decLitRepType _ _ = Nothing

mutual

  public export
  data Expr : RepType {- Representation of return value -} -> Type where
    StgApp
      :  {q : RepType}
      -> BinderId q    -- function
      -> (List ArgSg)  -- arguments; may be empty, when arguments are empty, the application
                       -- is interpreted as variable lookup.
      -> (r : RepType) -- result type
      -> Expr r

    StgLit : (l : Lit) -> Expr (litRepType l)

      -- StgConApp is vital for returning unboxed tuples or sums
      -- which can't be let-bound first
    StgConApp
         -- TODO: Use the DataConRep info to determine the representation of the arguments
         -- and the content of the unboxed sum parameter
      :  {r : DataConRep}
      -> (DataConId r)        -- DataCon
      -> (StgConAppArgType r) -- Saturated
      -> Expr (SingleValue LiftedRep)

    StgOpApp
      :  {name : String} -> {args : List PrimRep} -> {ret : PrimRep}
      -> PrimOp name args ret
      -> StgOpArgType args
      -- Maybe TyConId -- Result type name (required only for tagToEnum wrapper generator)
      --               -- which we dont want to use in IdrisExtSTG
      -> Expr (SingleValue ret)

    StgCase
      :  {r : RepType}
      -> (a : AltType)
      -> Expr (altRepType a)
         -- The thing to examine
      -> SBinder (altRepType a)
         -- binds the result of evaluating the scrutinee
         -- The Representation of the Binder should have the same SingleValue as the PrimAlt
      -> (List (Alt (altRepType a) r))
         -- The DEFAULT case is always the first one, if there is any
      -> Expr r

    StgLet
      :  Binding -- right hand sides -- TODO
      -> Expr r  -- body
      -> Expr r

    StgLetNoEscape
      :  Binding -- right hand sides -- TODO
      -> Expr r  -- body
      -> Expr r

    -- Helper data constructor when deep investigation is needed.
    -- StgUndefined : (r : RepType) -> Expr r

  public export
  data Alt : (altConRep : RepType) -> (exprRep : RepType) -> Type where
    MkAlt
      :  (a : AltCon ar)
      -> (bs : AltBinderType a)
      -> Expr er
      -> Alt ar er

  public export
  data Rhs : Type where
    StgRhsClosure
      :  {r : RepType}
      -> UpdateFlag
        -- TODO: Use
      -> (List SBinderSg) -- arguments; if empty, then not a function. The order is important
      -> (Expr r) -- body
      -> Rhs
        -- (Expr r) -> Rhs r
    StgRhsCon
      : -- TODO: Use the DataConRep to determine the Argument list
         DataConIdSg -- DataCon
      -> (List ArgSg) -- Args
      -> Rhs
      -- LiftedRep, because we don't need to introduce Unlifted < Lifted subtyping relation

  public export
  data Binding
    = StgNonRec (SBinder (SingleValue LiftedRep)) Rhs
    | StgRec    (List (SBinder (SingleValue LiftedRep), Rhs))

  public export
  data TopBinding
    = StgTopLifted Binding -- SingleValue Lifted OR UnLifted, in HAskell is LiftedOnly
    | StgTopStringLit (SBinder (SingleValue AddrRep)) String
      -- SBinder binds a variable which will hold an Address in STG: AddrRep or Addr#

public export
data ForeignSrcLang
  = LangC
  | LangCxx
  | LangObjc
  | LangObjxcc
  | LangAsm
  | RawObject

||| These modules are the responsible for STG boxing the values that come from C.
public export
data ForeignStubs
  = NoStubs
  | MkForeignStubs
      String -- CHeader
      String -- CSource

public export
record Module where
  constructor MkModule
  Phase              : String       -- For Debug only
  ModuleUnitId       : UnitId       -- Haskell package, could be main
  Name               : ModuleName   -- It should be Main
  SourceFilePath     : String       -- For Debug only
  ForeignStubs       : ForeignStubs -- For FFI, to be improved
  HasForeignExported : Bool         -- Is Idris function exported through FFI
  Dependency         : List (UnitId, List ModuleName)
                       -- It should be empty for now
  ExternalTopIds     : List (UnitId, List (ModuleName, List SBinderSg))
                       -- Same as above, just referred named included
  TyCons             : List (UnitId, List (ModuleName, List STyCon))
                       -- The types that are referred in the module, even if they are defined here or somewhere else
  TopBindings        : List TopBinding
                       -- Definition of functions, found in top bindings.
  ForeignFiles       : List (ForeignSrcLang, FilePath)
                       -- To be clarified, this is something internal to GHC codegen. It should be empty for now.

max_stars_repo_name: andorp/IdrisExtSTGCodegen

max_issues_repo_name: andorp/IdrisExtSTGCodegen

max_forks_repo_name: andorp/IdrisExtSTGCodegen


text:
module Test.Util

import JS
import Hedgehog
import Data.Either

--------------------------------------------------------------------------------
--          Undefined
--------------------------------------------------------------------------------

prop_int_notUndefined : Property
prop_int_notUndefined =
  property $ do n <- forAll (int (linear 0 1000))
                assert (not $ isUndefined n)

prop_string_notUndefined : Property
prop_string_notUndefined =
  property $ do n <- forAll (string (linear 0 20) unicode)
                assert (not $ isUndefined n)

prop_undefinedIsUndefined : Property
prop_undefinedIsUndefined =
  withTests 1 . property $ do u <- forAll (pure undefined)
                              assert (isUndefined u)

prop_int_notNull : Property
prop_int_notNull =
  property $ do n <- forAll (int (linear 0 1000))
                assert (not $ isNull n)

prop_string_notNull : Property
prop_string_notNull =
  property $ do n <- forAll (string (linear 0 20) unicode)
                assert (not $ isNull n)

prop_undefinedIsNull : Property
prop_undefinedIsNull =
  withTests 1 . property $ do u <- forAllWith (const "null") (pure $ null {a = Int})
                              assert (isNull u)

invalidJSON : Gen String
invalidJSON = ("{" ++) <$> string (linear 0 10) alphaNum

%foreign "javascript:lambda:s => JSON.parse(s)"
prim__parse : String -> AnyPtr

prop_try : Property
prop_try = property $ do s <- forAll invalidJSON
                         assert $ isLeft (try prim__parse s)

undefinedProps : Group
undefinedProps = MkGroup "Undefined and Null"
                   [ ("prop_int_notUndefined", prop_int_notUndefined)
                   , ("prop_string_notUndefined", prop_string_notUndefined)
                   , ("prop_undefinedIsUndefined", prop_undefinedIsUndefined)
                   , ("prop_int_notNull", prop_int_notNull)
                   , ("prop_string_notNull", prop_string_notNull)
                   , ("prop_undefinedIsNull", prop_undefinedIsNull)
                   , ("prop_try", prop_try)
                   ]

export
test : IO ()
test = do ignore $ checkGroup undefinedProps


text:
module Data.Time.Clock.Internal.NominalDiffTime

import Data.Time.Clock.Internal.Fixed as F

public export
data NominalDiffTime = MkNominalDiffTime Pico

export
Enum NominalDiffTime where
  pred (MkNominalDiffTime x) = MkNominalDiffTime (pred x)
  toNat (MkNominalDiffTime x) = toNat x
  fromNat x = MkNominalDiffTime (fromNat x)

export
Show NominalDiffTime where
    show (MkNominalDiffTime t) = show t

export
Eq NominalDiffTime where
  (MkNominalDiffTime a) == (MkNominalDiffTime b) = a == b

export
Ord NominalDiffTime where
  compare (MkNominalDiffTime a) (MkNominalDiffTime b) = compare a b

add: NominalDiffTime -> NominalDiffTime -> NominalDiffTime
add (MkNominalDiffTime x) (MkNominalDiffTime y) = MkNominalDiffTime (x + y)

(+) : NominalDiffTime -> NominalDiffTime -> NominalDiffTime
(+) = add

minus: NominalDiffTime -> NominalDiffTime -> NominalDiffTime
minus (MkNominalDiffTime x) (MkNominalDiffTime y) = MkNominalDiffTime (x - y)

negate: NominalDiffTime -> NominalDiffTime
negate (MkNominalDiffTime x) = MkNominalDiffTime (negate x)

abs : NominalDiffTime-> NominalDiffTime
abs (MkNominalDiffTime x) = MkNominalDiffTime (abs x)

fromInteger : Integer -> NominalDiffTime
fromInteger x = MkNominalDiffTime (MkFixed x)

mult: NominalDiffTime -> NominalDiffTime -> NominalDiffTime
mult (MkNominalDiffTime x) (MkNominalDiffTime y) = MkNominalDiffTime (x * y)

(*): NominalDiffTime -> NominalDiffTime -> NominalDiffTime
(*) = mult

toRational: NominalDiffTime -> Double
toRational (MkNominalDiffTime x) = (toRational x)

fracDiv: NominalDiffTime -> NominalDiffTime -> NominalDiffTime
fracDiv (MkNominalDiffTime x) (MkNominalDiffTime y) = MkNominalDiffTime (fracDiv x y)

(/): NominalDiffTime -> NominalDiffTime -> NominalDiffTime
(/) = fracDiv

recip : NominalDiffTime -> NominalDiffTime
recip (MkNominalDiffTime x) = MkNominalDiffTime (recip x)

secondsToNominalDiffTime: Integer -> NominalDiffTime
secondsToNominalDiffTime = fromInteger

picosecondsToNominalDiffTime: Integer -> NominalDiffTime
picosecondsToNominalDiffTime x = MkNominalDiffTime (MkFixed x)

diffTimeToPicoseconds : NominalDiffTime -> Integer
diffTimeToPicoseconds (MkNominalDiffTime (MkFixed x)) = x

-- | One day in 'NominalDiffTime'.
export
nominalDay: NominalDiffTime
nominalDay = 86400

max_stars_repo_name: gdevanla/idris-time

max_issues_repo_name: gdevanla/idris-time

max_forks_repo_name: gdevanla/idris-time


text:
module Minesweeper.Board

import Data.Vect
import Data.Fin

import Effects
import Effect.Random
import Effect.StdIO
import Effect.System

-- |X,Y co-ordinate
public export
data Pos = MkPos Nat Nat

-- | Two positions are the same if their x and y co-oridinates
--   are equal
implementation Eq Pos where
  (MkPos x1 y1) == (MkPos x2 y2) = (x1 == x2) && (y1 == y2)

implementation Show Pos where
  show (MkPos x y) = "(x : " ++ show x ++ ", y : " ++ show y ++ ")"

-- | A Square can either contain a mine or be adjacent to
--   0 - 8 mines
data SqState = Mine | Safe Nat

-- | A Square can be hidden (not yet pressed) or
--   revealed
data Visibility = Hidden | Revealed

data Square = MkSquare Visibility SqState

-- | Board is m * n squares
export
data Board : Nat -> Nat -> Type where
   MkBoard : (Vect m (Vect n Square)) -> Board m n

strRepeat : Nat -> String -> String
strRepeat Z s = ""
strRepeat (S n) s = s ++ strRepeat n s

concatSV : Vect n String -> String
concatSV Nil = ""
concatSV (v :: vs) = v ++ (concatSV vs)

-- | Display the board, hiding any hidden squares
export
showBoard : (Board rows cols) -> String
showBoard {rows} {cols} board = if rows == 0
  then "Empty"
  else  firstRow ++ "\n" ++ (showRows board)

  where firstRow = strRepeat (2 * cols + 1) "-"

        showRows : (Board rows cols) -> String
        showRows (MkBoard vs) = concatSV $ map (\v => (showRow v) ++ "\n") vs

        where showRow : Vect k Square -> String
              showRow v = "|" ++ rowStr ++ "\n" ++ endStr
                where rowStr = concatSV $ map (\(MkSquare vis st) => case (vis, st) of
                                    (Hidden, _) => "?|"
                                    (Revealed, Mine) => "m|"
                                    (Revealed, Safe Z) => " |"
                                    (Revealed, Safe n) => (show n) ++ "|" ) v

                      -- Line under each Row
                      endStr = (concatSV $ map (\_ => "--") v) ++ "-"

-- | Display the board, revealing all hidden squares
export
showRevealed : (Board rows cols) -> String
showRevealed {rows} {cols} board = if rows == 0
  then "Empty"
  else  firstRow ++ "\n" ++ (showRows board)

  where firstRow = strRepeat (2 * cols + 1) "-"

        showRows : (Board rows cols) -> String
        showRows (MkBoard vs) = concatSV $ map (\v => (showRow v) ++ "\n") vs

        where showRow : Vect k Square -> String
              showRow v = "|" ++ rowStr ++ "\n" ++ endStr
                where rowStr = concatSV $ map (\(MkSquare _ st) => case st of
                                    Mine => "m|"
                                    (Safe Z) => " |"
                                    (Safe n) => (show n) ++ "|" ) v

                      -- Line under each Row
                      endStr = (concatSV $ map (\_ => "--") v) ++ "-"

-- | Prove n = plus n 0
natPlusZ : (n : Nat) -> n = plus n 0
natPlusZ Z = Refl
natPlusZ (S o) = rewrite natPlusZ o in Refl

-- | Apply the given function (k - 1) times to a given value and return
--   all the intermediate values as a vector
iterateV : (k : Nat) -> (a -> a) -> a -> Vect k a
iterateV k f b = rewrite (natPlusZ k) in (reverse $ iterateV' k b Nil)
  where iterateV' : (m : Nat) -> a -> (Vect n a) -> (Vect (m + n) a)
        iterateV' Z _ v = v
        iterateV' (S l) a v {n} = rewrite (plusSuccRightSucc l n) in
                                    iterateV' l (f a) (a :: v)

-- | Given an index, element and vector create a new
--   vector with the given element at that index.
--   If the index is >= the vector size then the same
--   vector is returned
replaceV : Nat -> a -> Vect n a -> Vect n a
replaceV = replaceV' Z
  where replaceV' : Nat -> Nat -> a -> Vect n a -> Vect n a
        replaceV' _ _ _ Nil = Nil
        replaceV' cur pos a (v :: vs) =
          if (cur == pos)
            then a :: vs
            else v :: (replaceV' (cur + 1) pos a vs)

-- | Given row and column number and a Board, attempts
--   to increment the bomb adjacency value of the given
--   square in the board, if the row/col numbers are out
--   of range returns nothing, if the square selected is
--   a mine then the same Board is returned
incBoardSquare : Nat -> Nat -> (Board rows cols) -> Maybe (Board rows cols)
incBoardSquare {rows} {cols} y x (MkBoard v) = do
  rowPos <- natToFin y rows
  colPos <- natToFin x cols
  let row  =index rowPos v
  let square = index colPos row

  let newSquare = case square of
    (MkSquare vis (Safe n)) => (MkSquare vis (Safe (S n)))
    sq => sq

  pure $ MkBoard (replaceV y (replaceV x newSquare row) v)

-- | Attempt to increment the mine adjacency value for all 8 adjacent squares
--   of a given mine position, if the bomb position given is out of bounds then
--   Nothing is returned. Any adjacent squares which aren't on the board are
--   not incremented
incAdjacentSquares : Pos -> (Board rows cols) -> Maybe (Board rows cols)
incAdjacentSquares {rows} {cols} (MkPos x y) board = do
    -- Increment squares to the left of the mine
    leftSide <- incLeftSide board x
    -- Increment squares to the right side of the mine
    rightSide <- incRightSide leftSide cols
    -- Increment squares above and below the mine
    top <- incTop rightSide y
    bot <- incBot top rows

    pure bot

  where
        incTopLeft : (Board rows cols) -> Nat -> Nat -> Maybe (Board rows cols)
        incTopLeft prev Z _ = pure prev
        incTopLeft prev _ Z = pure prev
        incTopLeft prev (S y) (S x) = incBoardSquare y x prev

        incBotLeft : (Board rows cols) -> Nat -> Nat -> Maybe (Board rows cols)
        incBotLeft prev Z _ = pure prev
        incBotLeft prev _ Z = pure prev
        incBotLeft prev (S r) (S x) = if y < r then incBoardSquare (y + 1) x prev else pure prev

        incLeftSide : (Board rows cols) -> Nat -> Maybe (Board rows cols)
        incLeftSide prev Z = pure prev
        incLeftSide prev (S x) = do
            left <- incBoardSquare y x prev
            topLeft <- incTopLeft left y (S x)
            incBotLeft topLeft rows (S x)

        incTopRight : (Board rows cols) -> Nat -> Maybe (Board rows cols)
        incTopRight prev Z = pure prev
        incTopRight prev (S y) = incBoardSquare y (x + 1) prev

        incBotRight : (Board rows cols) -> Nat -> Maybe (Board rows cols)
        incBotRight prev Z = pure prev
        incBotRight prev (S r) = if y < r then incBoardSquare (y + 1) (x + 1) prev else pure prev

        incRightSide : (Board rows cols) -> Nat -> Maybe (Board rows cols)
        incRightSide prev Z = pure prev
        incRightSide prev (S c) = if x < c
          then do
            right <- incBoardSquare y (x + 1) prev
            topRight <- incTopRight right y
            incBotRight topRight rows
          else
            pure prev

        incTop : (Board rows cols) -> Nat -> Maybe (Board rows cols)
        incTop prev Z = pure prev
        incTop prev (S y) = incBoardSquare y x prev

        incBot : Board rows cols -> Nat -> Maybe (Board rows cols)
        incBot prev Z = pure prev
        incBot prev (S r) = if y < r then incBoardSquare (y + 1) x prev else pure prev

-- | Given row and column  dimensions of board with mines generate
--   the board
export
createBoard : (n : Nat) ->  (m : Nat) -> Vect k Pos -> Maybe (Board m n)
createBoard cols rows mines = do
      let initialBoard = MkBoard $ map (\row => generateRow row cols) (iterateV rows (+1) 0)
      calculateState initialBoard

    where generateRow : Nat -> (n : Nat) -> Vect n Square
          generateRow row cols = map (\col => generateSquare row col) (iterateV cols (+1) 0)

          where generateSquare : Nat -> Nat -> Square
                generateSquare row col = MkSquare Hidden sqState
                -- Check if Square is a mine
                where sqState = if (MkPos col row) `elem` mines
                                then Mine
                                else Safe 0

         -- For each non mine square work out the number of adjacent
         -- bombs
          calculateState : Board m n -> Maybe (Board m n)
          calculateState board = calculateState' board mines
            where calculateState' : Board m n -> Vect k Pos -> Maybe (Board m n)
                  calculateState' board Nil = pure board
                  calculateState' board (x :: xs) = do
                    res <- (incAdjacentSquares x board)
                    calculateState' res xs

-- | Determines if the Board is in a "Win" State
--   i.e. all hidden squares are mines
export
checkWin : Board m n -> Bool
checkWin (MkBoard v) = foldl (\b, v => (checkRow v) && b) True v -- Check each row matches win condition
  where checkRow : Vect n Square -> Bool
        checkRow v = foldl (\b, (MkSquare vis st) => case (vis, st) of
                      (Revealed, Safe m) => b -- All safe squares must be revealed
                      (Hidden, Mine) => b  -- Hidden mines are still a win condition
                      _ => b && False) True v

-- | Determines if the Board is in a "Lose" State
--   i.e. a revealed square is a mine
export
checkLose : Board m n -> Bool
checkLose (MkBoard v) = foldl(\b, v => (checkRow v) || b) False v
  where checkRow v = foldl (\b, (MkSquare vis st) => case (vis, st) of
                      (Revealed, Mine) => True -- If any mines are revealed, the player loses
                      _ => b || False) False v

-- Reveals the given position, returns the new Board state
-- if a square is revealed, otherwise returns an error message
-- if the square has already been revealed or it's out of bounds
export
reveal : Pos -> Board rows cols -> Either String (Board rows cols)
reveal (MkPos x y) board@(MkBoard v) = do
  rowPos <- maybeToEither "Out Of Bounds." (natToFin y rows)
  colPos <- maybeToEither "Out Of Bounds." (natToFin x cols)
  let row  =index rowPos v
  let square = index colPos row

  case square of
    (MkSquare Revealed _) => Left "Square has already been revealed"

    -- No surrounding mines, reveal all squares surrounding the revealed square
    (MkSquare Hidden (Safe Z)) => do
        let newSq = MkSquare Revealed (Safe Z)
        pure (MkBoard (replaceV y (replaceV x newSq row) v)) >>=

          \b => pure (revealTop b y) >>=
          \b => pure (revealLeft b x) >>=
          \b => pure (revealTopLeft b y x) >>=
          \b => pure (revealNoErr (MkPos x       (y + 1)) b) >>=
          \b => pure (revealNoErr (MkPos (x + 1) y      ) b) >>=
          \b => pure (revealNoErr (MkPos (x + 1) (y + 1)) b)

    (MkSquare Hidden sq) => do
        let newSq = MkSquare Revealed sq
        pure $ MkBoard (replaceV y (replaceV x newSq row) v)

 -- Reveals the given position, returns the new Board state
 -- if a square is revealed, otherwise returns the old board state
 where revealNoErr : Pos -> Board rows cols -> Board rows cols
       revealNoErr p b = case reveal p b of
                           (Right newB) => newB
                           (Left _) => b

       revealLeft : Board rows cols -> Nat -> Board rows cols
       revealLeft prev Z = prev
       revealLeft prev (S x) = revealNoErr (MkPos x (y + 1)) (revealNoErr (MkPos x y) prev)

       revealTop : Board rows cols -> Nat -> Board rows cols
       revealTop prev Z = prev
       revealTop prev (S y) = revealNoErr (MkPos (x + 1) y) (revealNoErr (MkPos x y) prev)

       revealTopLeft : Board rows cols -> Nat -> Nat -> Board rows cols
       revealTopLeft prev Z _ = prev
       revealTopLeft prev _ Z = prev
       revealTopLeft prev y x = revealNoErr (MkPos x y) prev

-- | Given x and y dimensions and a vector containing
--   the positions of already generated mines, places a mine
--   in a position which isn't contained in the given vector
generateMine : Nat -> Nat -> (Vect n Pos) -> {[RND]} Eff Pos
generateMine x y mines = do
  xPos <- rndInt 0 (toIntegerNat x)
  yPos <- rndInt 0 (toIntegerNat y)
  let mine = MkPos (fromIntegerNat xPos) (fromIntegerNat yPos)

  -- If position already taken then attempt to regenerate
  if mine `elem` mines
    then pure $ placeRightMine mine
    else pure mine

 where placeRightMine : Pos -> Pos
       placeRightMine (MkPos col row) =
            if nextPos `elem` mines
              then placeRightMine nextPos
              else nextPos

           -- Modulo giving strange division by 0 runtime error,
           -- so calculate next square to the right manually
           where nextCol : Nat
                 nextCol = if (S col) == x then Z else (S col)
                 nextRow : Nat
                 nextRow = if nextCol == Z
                              then if ((S row) == y) then Z else (S row)
                              else row
                 nextPos = (MkPos nextCol nextRow)

-- | Given x and y dimensions and number of mines to create
--   creates a vector containing positions of randomly placed mines.
--  if there are more mines than x * y spaces then Nothing is returned.
--  To guarantee termination if a collision occurs then a mine is attempted
--  to be placed to the right of the mine until a free space is hit
generateMines' : Nat -> Nat -> (n : Nat) -> {[RND]} Eff (Vect (n) Pos)
generateMines' x y nMines = rewrite (natPlusZ nMines) in
                                generateMines'' nMines Nil

  where generateMines'' : (m : Nat) -> (Vect k Pos) -> {[RND]} Eff (Vect (m + k)  Pos)
        generateMines'' Z v = pure v
        generateMines'' {k} (S l) mines =
					(generateMine x y mines) >>=
					\mine => rewrite (plusSuccRightSucc l k) in generateMines'' l (mine ::mines)

export
generateMines : Nat -> Nat -> (n : Nat) -> {[SYSTEM, RND]} Eff (Maybe (Vect n Pos))
generateMines x y nMines =
  if (x * y < nMines)
    then pure Nothing
    else do
      -- Use current system time as RNG seed
      t <- time
      srand t
      pure $ Just !(generateMines' x y nMines)

max_stars_repo_name: RossMeikleham/Idris-Minesweeper

max_issues_repo_name: RossMeikleham/Idris-Minesweeper

max_forks_repo_name: RossMeikleham/Idris-Minesweeper