text:
module Core.TT

import public Core.FC
import public Core.Name

import Data.Bool.Extra
import Data.List
import Data.NameMap
import Data.Vect
import Decidable.Equality
import Text.PrettyPrint.Prettyprinter
import Text.PrettyPrint.Prettyprinter.Util

import public Algebra

%default covering

public export
data NameType : Type where
     Bound   : NameType
     Func    : NameType
     DataCon : (tag : Int) -> (arity : Nat) -> NameType
     TyCon   : (tag : Int) -> (arity : Nat) -> NameType

public export
data Constant
    = I Int
    | BI Integer
    | B8 Int -- For now, since we don't have Bits types. We need to
                -- make sure the Integer remains in range
    | B16 Int
    | B32 Int
    | B64 Integer
    | Str String
    | Ch Char
    | Db Double
    | WorldVal

    | IntType
    | IntegerType
    | Bits8Type
    | Bits16Type
    | Bits32Type
    | Bits64Type
    | StringType
    | CharType
    | DoubleType
    | WorldType

export
constantEq : (x, y : Constant) -> Maybe (x = y)
constantEq (I x) (I y) = case decEq x y of
                              Yes Refl => Just Refl
                              No contra => Nothing
constantEq (BI x) (BI y) = case decEq x y of
                                Yes Refl => Just Refl
                                No contra => Nothing
constantEq (Str x) (Str y) = case decEq x y of
                                  Yes Refl => Just Refl
                                  No contra => Nothing
constantEq (Ch x) (Ch y) = case decEq x y of
                                Yes Refl => Just Refl
                                No contra => Nothing
constantEq (Db x) (Db y) = Nothing -- no DecEq for Doubles!
constantEq WorldVal WorldVal = Just Refl
constantEq IntType IntType = Just Refl
constantEq IntegerType IntegerType = Just Refl
constantEq StringType StringType = Just Refl
constantEq CharType CharType = Just Refl
constantEq DoubleType DoubleType = Just Refl
constantEq WorldType WorldType = Just Refl
constantEq _ _ = Nothing

export
Show Constant where
  show (I x) = show x
  show (BI x) = show x
  show (B8 x) = show x
  show (B16 x) = show x
  show (B32 x) = show x
  show (B64 x) = show x
  show (Str x) = show x
  show (Ch x) = show x
  show (Db x) = show x
  show WorldVal = "%MkWorld"
  show IntType = "Int"
  show IntegerType = "Integer"
  show Bits8Type = "Bits8"
  show Bits16Type = "Bits16"
  show Bits32Type = "Bits32"
  show Bits64Type = "Bits64"
  show StringType = "String"
  show CharType = "Char"
  show DoubleType = "Double"
  show WorldType = "%World"

export
Pretty Constant where
  pretty (I x) = pretty x
  pretty (BI x) = pretty x
  pretty (B8 x) = pretty x
  pretty (B16 x) = pretty x
  pretty (B32 x) = pretty x
  pretty (B64 x) = pretty x
  pretty (Str x) = dquotes (pretty x)
  pretty (Ch x) = squotes (pretty x)
  pretty (Db x) = pretty x
  pretty WorldVal = pretty "%MkWorld"
  pretty IntType = pretty "Int"
  pretty IntegerType = pretty "Integer"
  pretty Bits8Type = pretty "Bits8"
  pretty Bits16Type = pretty "Bits16"
  pretty Bits32Type = pretty "Bits32"
  pretty Bits64Type = pretty "Bits64"
  pretty StringType = pretty "String"
  pretty CharType = pretty "Char"
  pretty DoubleType = pretty "Double"
  pretty WorldType = pretty "%World"

export
Eq Constant where
  (I x) == (I y) = x == y
  (BI x) == (BI y) = x == y
  (B8 x) == (B8 y) = x == y
  (B16 x) == (B16 y) = x == y
  (B32 x) == (B32 y) = x == y
  (B64 x) == (B64 y) = x == y
  (Str x) == (Str y) = x == y
  (Ch x) == (Ch y) = x == y
  (Db x) == (Db y) = x == y
  WorldVal == WorldVal = True
  IntType == IntType = True
  IntegerType == IntegerType = True
  Bits8Type == Bits8Type = True
  Bits16Type == Bits16Type = True
  Bits32Type == Bits32Type = True
  Bits64Type == Bits64Type = True
  StringType == StringType = True
  CharType == CharType = True
  DoubleType == DoubleType = True
  WorldType == WorldType = True
  _ == _ = False

-- for typecase
export
constTag : Constant -> Int
-- 1 = ->, 2 = Type
constTag IntType = 3
constTag IntegerType = 4
constTag Bits8Type = 5
constTag Bits16Type = 6
constTag Bits32Type = 7
constTag Bits64Type = 8
constTag StringType = 9
constTag CharType = 10
constTag DoubleType = 11
constTag WorldType = 12
constTag _ = 0

-- All the internal operators, parameterised by their arity
public export
data PrimFn : Nat -> Type where
     Add : (ty : Constant) -> PrimFn 2
     Sub : (ty : Constant) -> PrimFn 2
     Mul : (ty : Constant) -> PrimFn 2
     Div : (ty : Constant) -> PrimFn 2
     Mod : (ty : Constant) -> PrimFn 2
     Neg : (ty : Constant) -> PrimFn 1
     ShiftL : (ty : Constant) -> PrimFn 2
     ShiftR : (ty : Constant) -> PrimFn 2

     BAnd : (ty : Constant) -> PrimFn 2
     BOr : (ty : Constant) -> PrimFn 2
     BXOr : (ty : Constant) -> PrimFn 2

     LT  : (ty : Constant) -> PrimFn 2
     LTE : (ty : Constant) -> PrimFn 2
     EQ  : (ty : Constant) -> PrimFn 2
     GTE : (ty : Constant) -> PrimFn 2
     GT  : (ty : Constant) -> PrimFn 2

     StrLength : PrimFn 1
     StrHead : PrimFn 1
     StrTail : PrimFn 1
     StrIndex : PrimFn 2
     StrCons : PrimFn 2
     StrAppend : PrimFn 2
     StrReverse : PrimFn 1
     StrSubstr : PrimFn 3

     DoubleExp : PrimFn 1
     DoubleLog : PrimFn 1
     DoubleSin : PrimFn 1
     DoubleCos : PrimFn 1
     DoubleTan : PrimFn 1
     DoubleASin : PrimFn 1
     DoubleACos : PrimFn 1
     DoubleATan : PrimFn 1
     DoubleSqrt : PrimFn 1
     DoubleFloor : PrimFn 1
     DoubleCeiling : PrimFn 1

     Cast : Constant -> Constant -> PrimFn 1
     BelieveMe : PrimFn 3
     Crash : PrimFn 2

export
Show (PrimFn arity) where
  show (Add ty) = "+" ++ show ty
  show (Sub ty) = "-" ++ show ty
  show (Mul ty) = "*" ++ show ty
  show (Div ty) = "/" ++ show ty
  show (Mod ty) = "%" ++ show ty
  show (Neg ty) = "neg " ++ show ty
  show (ShiftL ty) = "shl " ++ show ty
  show (ShiftR ty) = "shr " ++ show ty
  show (BAnd ty) = "and " ++ show ty
  show (BOr ty) = "or " ++ show ty
  show (BXOr ty) = "xor " ++ show ty
  show (LT ty) = "<" ++ show ty
  show (LTE ty) = "<=" ++ show ty
  show (EQ ty) = "==" ++ show ty
  show (GTE ty) = ">=" ++ show ty
  show (GT ty) = ">" ++ show ty
  show StrLength = "op_strlen"
  show StrHead = "op_strhead"
  show StrTail = "op_strtail"
  show StrIndex = "op_strindex"
  show StrCons = "op_strcons"
  show StrAppend = "++"
  show StrReverse = "op_strrev"
  show StrSubstr = "op_strsubstr"
  show DoubleExp = "op_doubleExp"
  show DoubleLog = "op_doubleLog"
  show DoubleSin = "op_doubleSin"
  show DoubleCos = "op_doubleCos"
  show DoubleTan = "op_doubleTan"
  show DoubleASin = "op_doubleASin"
  show DoubleACos = "op_doubleACos"
  show DoubleATan = "op_doubleATan"
  show DoubleSqrt = "op_doubleSqrt"
  show DoubleFloor = "op_doubleFloor"
  show DoubleCeiling = "op_doubleCeiling"
  show (Cast x y) = "cast-" ++ show x ++ "-" ++ show y
  show BelieveMe = "believe_me"
  show Crash = "crash"

public export
data PiInfo t = Implicit | Explicit | AutoImplicit | DefImplicit t

export
eqPiInfoBy : (t -> u -> Bool) -> PiInfo t -> PiInfo u -> Bool
eqPiInfoBy eqT = go where

  go : PiInfo t -> PiInfo u -> Bool
  go Implicit Implicit = True
  go Explicit Explicit = True
  go AutoImplicit AutoImplicit = True
  go (DefImplicit t) (DefImplicit t') = eqT t t'
  go _ _ = False

-- There's few places where we need the default - it's just when checking if
-- there's a default during elaboration - so often it's easier just to erase it
-- to a normal implicit
export
forgetDef : PiInfo t -> PiInfo t'
forgetDef Explicit = Explicit
forgetDef Implicit = Implicit
forgetDef AutoImplicit = AutoImplicit
forgetDef (DefImplicit t) = Implicit

export
Show t => Show (PiInfo t) where
  show Implicit = "Implicit"
  show Explicit = "Explicit"
  show AutoImplicit = "AutoImplicit"
  show (DefImplicit t) = "DefImplicit " ++ show t

export
Eq t => Eq (PiInfo t) where
  (==) = eqPiInfoBy (==)

public export
data Binder : Type -> Type where
     -- Lambda bound variables with their implicitness
     Lam : FC -> RigCount -> PiInfo type -> (ty : type) -> Binder type
     -- Let bound variables with their value
     Let : FC -> RigCount -> (val : type) -> (ty : type) -> Binder type
     -- Forall/pi bound variables with their implicitness
     Pi : FC -> RigCount -> PiInfo type -> (ty : type) -> Binder type
     -- pattern bound variables. The PiInfo gives the implicitness at the
     -- point it was bound (Explicit if it was explicitly named in the
     -- program)
     PVar : FC -> RigCount -> PiInfo type -> (ty : type) -> Binder type
     -- variable bound for an as pattern (Like a let, but no computational
     -- force, and only used on the lhs. Converted to a let on the rhs because
     -- we want the computational behaviour.)
     PLet : FC -> RigCount -> (val : type) -> (ty : type) -> Binder type
     -- the type of pattern bound variables
     PVTy : FC -> RigCount -> (ty : type) -> Binder type

export
isLet : Binder t -> Bool
isLet (Let _ _ _ _) = True
isLet _ = False

export
isImplicit : Binder t -> Bool
isImplicit (Pi _ _ Explicit _) = False
isImplicit (Pi _ _ _ _) = True
isImplicit (Lam _ _ Explicit _) = False
isImplicit (Lam _ _ _ _) = True
isImplicit _ = False

export
binderLoc : Binder tm -> FC
binderLoc (Lam fc _ x ty) = fc
binderLoc (Let fc _ val ty) = fc
binderLoc (Pi fc _ x ty) = fc
binderLoc (PVar fc _ p ty) = fc
binderLoc (PLet fc _ val ty) = fc
binderLoc (PVTy fc _ ty) = fc

export
binderType : Binder tm -> tm
binderType (Lam _ _ x ty) = ty
binderType (Let _ _ val ty) = ty
binderType (Pi _ _ x ty) = ty
binderType (PVar _ _ _ ty) = ty
binderType (PLet _ _ val ty) = ty
binderType (PVTy _ _ ty) = ty

export
multiplicity : Binder tm -> RigCount
multiplicity (Lam _ c x ty) = c
multiplicity (Let _ c val ty) = c
multiplicity (Pi _ c x ty) = c
multiplicity (PVar _ c p ty) = c
multiplicity (PLet _ c val ty) = c
multiplicity (PVTy _ c ty) = c

export
piInfo : Binder tm -> PiInfo tm
piInfo (Lam _ c x ty) = x
piInfo (Let _ c val ty) = Explicit
piInfo (Pi _ c x ty) = x
piInfo (PVar _ c p ty) = p
piInfo (PLet _ c val ty) = Explicit
piInfo (PVTy _ c ty) = Explicit

export
setMultiplicity : Binder tm -> RigCount -> Binder tm
setMultiplicity (Lam fc _ x ty) c = Lam fc c x ty
setMultiplicity (Let fc _ val ty) c = Let fc c val ty
setMultiplicity (Pi fc _ x ty) c = Pi fc c x ty
setMultiplicity (PVar fc _ p ty) c = PVar fc c p ty
setMultiplicity (PLet fc _ val ty) c = PLet fc c val ty
setMultiplicity (PVTy fc _ ty) c = PVTy fc c ty

showCount : RigCount -> String
showCount = elimSemi "0 " "1 " (const "")

Show ty => Show (Binder ty) where
	show (Lam _ c _ t) = "\\" ++ showCount c ++ show t
	show (Pi _ c _ t) = "Pi " ++ showCount c ++ show t
	show (Let _ c v t) = "let " ++ showCount c ++ show v ++ " : " ++ show t
	show (PVar _ c _ t) = "pat " ++ showCount c ++ show t
	show (PLet _ c v t) = "plet " ++ showCount c ++ show v ++ " : " ++ show t
	show (PVTy _ c t) = "pty " ++ showCount c ++ show t

export
setType : Binder tm -> tm -> Binder tm
setType (Lam fc c x _) ty = Lam fc c x ty
setType (Let fc c val _) ty = Let fc c val ty
setType (Pi fc c x _) ty = Pi fc c x ty
setType (PVar fc c p _) ty = PVar fc c p ty
setType (PLet fc c val _) ty = PLet fc c val ty
setType (PVTy fc c _) ty = PVTy fc c ty

export
Functor PiInfo where
  map func Explicit = Explicit
  map func Implicit = Implicit
  map func AutoImplicit = AutoImplicit
  map func (DefImplicit t) = (DefImplicit (func t))

export
Functor Binder where
  map func (Lam fc c x ty) = Lam fc c (map func x) (func ty)
  map func (Let fc c val ty) = Let fc c (func val) (func ty)
  map func (Pi fc c x ty) = Pi fc c (map func x) (func ty)
  map func (PVar fc c p ty) = PVar fc c (map func p) (func ty)
  map func (PLet fc c val ty) = PLet fc c (func val) (func ty)
  map func (PVTy fc c ty) = PVTy fc c (func ty)

public export
data IsVar : Name -> Nat -> List Name -> Type where
     First : IsVar n Z (n :: ns)
     Later : IsVar n i ns -> IsVar n (S i) (m :: ns)

public export
dropVar : (ns : List Name) -> {idx : Nat} -> (0 p : IsVar name idx ns) -> List Name
dropVar (n :: xs) First = xs
dropVar (n :: xs) (Later p) = n :: dropVar xs p

public export
data Var : List Name -> Type where
     MkVar : {i : Nat} -> (0 p : IsVar n i vars) -> Var vars

export
sameVar : Var xs -> Var xs -> Bool
sameVar (MkVar {i=x} _) (MkVar {i=y} _) = x == y

export
varIdx : Var xs -> Nat
varIdx (MkVar {i} _) = i

export
dropFirst : List (Var (v :: vs)) -> List (Var vs)
dropFirst [] = []
dropFirst (MkVar First :: vs) = dropFirst vs
dropFirst (MkVar (Later p) :: vs) = MkVar p :: dropFirst vs

export
Show (Var ns) where
  show (MkVar {i} _) = show i

namespace CList
  -- A list correspoding to another list
  public export
  data CList : List a -> Type -> Type where
       Nil : CList [] ty
       (::) : (x : ty) -> CList cs ty -> CList (c :: cs) ty

-- Typechecked terms
-- These are guaranteed to be well-scoped wrt local variables, because they are
-- indexed by the names of local variables in scope
public export
data LazyReason = LInf | LLazy | LUnknown

-- For as patterns matching linear arguments, select which side is
-- consumed
public export
data UseSide = UseLeft | UseRight

public export
data Term : List Name -> Type where
     Local : FC -> (isLet : Maybe Bool) ->
             (idx : Nat) -> (0 p : IsVar name idx vars) -> Term vars
     Ref : FC -> NameType -> (name : Name) -> Term vars
     -- Metavariables and the scope they are applied to
     Meta : FC -> Name -> Int -> List (Term vars) -> Term vars
     Bind : FC -> (x : Name) ->
            (b : Binder (Term vars)) ->
            (scope : Term (x :: vars)) -> Term vars
     App : FC -> (fn : Term vars) -> (arg : Term vars) -> Term vars
     -- as patterns; since we check LHS patterns as terms before turning
     -- them into patterns, this helps us get it right. When normalising,
     -- we just reduce the inner term and ignore the 'as' part
     -- The 'as' part should really be a Name rather than a Term, but it's
     -- easier this way since it gives us the ability to work with unresolved
     -- names (Ref) and resolved names (Local) without having to define a
     -- special purpose thing. (But it'd be nice to tidy that up, nevertheless)
     As : FC -> UseSide -> (as : Term vars) -> (pat : Term vars) -> Term vars
     -- Typed laziness annotations
     TDelayed : FC -> LazyReason -> Term vars -> Term vars
     TDelay : FC -> LazyReason -> (ty : Term vars) -> (arg : Term vars) -> Term vars
     TForce : FC -> LazyReason -> Term vars -> Term vars
     PrimVal : FC -> (c : Constant) -> Term vars
     Erased : FC -> (imp : Bool) -> -- True == impossible term, for coverage checker
              Term vars
     TType : FC -> Term vars

export
getLoc : Term vars -> FC
getLoc (Local fc _ _ _) = fc
getLoc (Ref fc _ _) = fc
getLoc (Meta fc _ _ _) = fc
getLoc (Bind fc _ _ _) = fc
getLoc (App fc _ _) = fc
getLoc (As fc _ _ _) = fc
getLoc (TDelayed fc _ _) = fc
getLoc (TDelay fc _ _ _) = fc
getLoc (TForce fc _ _) = fc
getLoc (PrimVal fc _) = fc
getLoc (Erased fc i) = fc
getLoc (TType fc) = fc

export
Eq LazyReason where
  (==) LInf LInf = True
  (==) LLazy LLazy = True
  (==) LUnknown LUnknown = True
  (==) _ _ = False

export
compatible : LazyReason -> LazyReason -> Bool
compatible LUnknown _ = True
compatible _ LUnknown = True
compatible x y = x == y

export
eqBinderBy : (t -> u -> Bool) -> (Binder t -> Binder u -> Bool)
eqBinderBy eqTU = go where

  go : Binder t -> Binder u -> Bool
  go (Lam _ c p ty) (Lam _ c' p' ty') = c == c' && eqPiInfoBy eqTU p p' && eqTU ty ty'
  go (Let _ c v ty) (Let _ c' v' ty') = c == c' && eqTU v v' && eqTU ty ty'
  go (Pi _ c p ty) (Pi _ c' p' ty')   = c == c' && eqPiInfoBy eqTU p p' && eqTU ty ty'
  go (PVar _ c p ty) (PVar _ c' p' ty') = c == c' && eqPiInfoBy eqTU p p' && eqTU ty ty'
  go (PLet _ c v ty) (PLet _ c' v' ty') = c == c' && eqTU v v' && eqTU ty ty'
  go (PVTy _ c ty) (PVTy _ c' ty') = c == c' && eqTU ty ty'
  go _ _ = False

export
Eq a => Eq (Binder a) where
  (==) = eqBinderBy (==)

export
Eq (Term vars) where
  (==) (Local _ _ idx _) (Local _ _ idx' _) = idx == idx'
  (==) (Ref _ _ n) (Ref _ _ n') = n == n'
  (==) (Meta _ _ i args) (Meta _ _ i' args')
      = assert_total (i == i' && args == args')
  (==) (Bind _ _ b sc) (Bind _ _ b' sc')
      = assert_total (b == b' && sc == believe_me sc')
  (==) (App _ f a) (App _ f' a') = f == f' && a == a'
  (==) (As _ _ a p) (As _ _ a' p') = a == a' && p == p'
  (==) (TDelayed _ _ t) (TDelayed _ _ t') = t == t'
  (==) (TDelay _ _ t x) (TDelay _ _ t' x') = t == t' && x == x'
  (==) (TForce _ _ t) (TForce _ _ t') = t == t'
  (==) (PrimVal _ c) (PrimVal _ c') = c == c'
  (==) (Erased _ i) (Erased _ i') = i == i'
  (==) (TType _) (TType _) = True
  (==) _ _ = False

-- Check equality, ignoring variable naming
export
eqTerm : Term vs -> Term vs' -> Bool
eqTerm (Local _ _ idx _) (Local _ _ idx' _) = idx == idx'
eqTerm (Ref _ _ n) (Ref _ _ n') = n == n'
eqTerm (Meta _ _ i args) (Meta _ _ i' args')
    = assert_total (i == i' && allTrue (zipWith eqTerm args args'))
eqTerm (Bind _ _ b sc) (Bind _ _ b' sc')
    = assert_total (eqBinderBy eqTerm b b') && eqTerm sc sc'
eqTerm (App _ f a) (App _ f' a') = eqTerm f f' && eqTerm a a'
eqTerm (As _ _ a p) (As _ _ a' p') = eqTerm a a' && eqTerm p p'
eqTerm (TDelayed _ _ t) (TDelayed _ _ t') = eqTerm t t'
eqTerm (TDelay _ _ t x) (TDelay _ _ t' x') = eqTerm t t' && eqTerm x x'
eqTerm (TForce _ _ t) (TForce _ _ t') = eqTerm t t'
eqTerm (PrimVal _ c) (PrimVal _ c') = c == c'
eqTerm (Erased _ i) (Erased _ i') = i == i'
eqTerm (TType _) (TType _) = True
eqTerm _ _ = False

public export
interface Weaken (tm : List Name -> Type) where
  weaken : {n, vars : _} -> tm vars -> tm (n :: vars)
  weakenNs : {vars : _} -> (ns : List Name) -> tm vars -> tm (ns ++ vars)

  weakenNs [] t = t
  weakenNs (n :: ns) t = weaken (weakenNs ns t)

  weaken = weakenNs [_]

public export
data Visibility = Private | Export | Public

export
Show Visibility where
  show Private = "private"
  show Export = "export"
  show Public = "public export"

export
Pretty Visibility where
  pretty Private = pretty "private"
  pretty Export = pretty "export"
  pretty Public = pretty "public" <+> pretty "export"

export
Eq Visibility where
  Private == Private = True
  Export == Export = True
  Public == Public = True
  _ == _ = False

export
Ord Visibility where
  compare Private Export = LT
  compare Private Public = LT
  compare Export Public = LT

  compare Private Private = EQ
  compare Export Export = EQ
  compare Public Public = EQ

  compare Export Private = GT
  compare Public Private = GT
  compare Public Export = GT

public export
data TotalReq = Total | CoveringOnly | PartialOK

export
Eq TotalReq where
    (==) Total Total = True
    (==) CoveringOnly CoveringOnly = True
    (==) PartialOK PartialOK = True
    (==) _ _ = False

export
Show TotalReq where
    show Total = "total"
    show CoveringOnly = "covering"
    show PartialOK = "partial"

public export
data PartialReason
       = NotStrictlyPositive
       | BadCall (List Name)
       | RecPath (List Name)

export
Show PartialReason where
  show NotStrictlyPositive = "not strictly positive"
  show (BadCall [n])
      = "possibly not terminating due to call to " ++ show n
  show (BadCall ns)
      = "possibly not terminating due to calls to " ++ showSep ", " (map show ns)
  show (RecPath ns)
      = "possibly not terminating due to recursive path " ++ showSep " -> " (map show ns)

export
Pretty PartialReason where
  pretty NotStrictlyPositive = reflow "not strictly positive"
  pretty (BadCall [n])
    = reflow "possibly not terminating due to call to" <++> pretty n
  pretty (BadCall ns)
    = reflow "possibly not terminating due to calls to" <++> concatWith (surround (comma <+> space)) (pretty <$> ns)
  pretty (RecPath ns)
    = reflow "possibly not terminating due to recursive path" <++> concatWith (surround (pretty " -> ")) (pretty <$> ns)

public export
data Terminating
       = Unchecked
       | IsTerminating
       | NotTerminating PartialReason

export
Show Terminating where
  show Unchecked = "not yet checked"
  show IsTerminating = "terminating"
  show (NotTerminating p) = show p

export
Pretty Terminating where
  pretty Unchecked = reflow "not yet checked"
  pretty IsTerminating = pretty "terminating"
  pretty (NotTerminating p) = pretty p

public export
data Covering
       = IsCovering
       | MissingCases (List (Term []))
       | NonCoveringCall (List Name)

export
Show Covering where
  show IsCovering = "covering"
  show (MissingCases c) = "not covering all cases"
  show (NonCoveringCall [f])
     = "not covering due to call to function " ++ show f
  show (NonCoveringCall cs)
     = "not covering due to calls to functions " ++ showSep ", " (map show cs)

export
Pretty Covering where
  pretty IsCovering = pretty "covering"
  pretty (MissingCases c) = reflow "not covering all cases"
  pretty (NonCoveringCall [f])
     = reflow "not covering due to call to function" <++> pretty f
  pretty (NonCoveringCall cs)
     = reflow "not covering due to calls to functions" <++> concatWith (surround (comma <+> space)) (pretty <$> cs)

-- Totality status of a definition. We separate termination checking from
-- coverage checking.
public export
record Totality where
     constructor MkTotality
     isTerminating : Terminating
     isCovering : Covering

export
Show Totality where
  show tot
    = let t = isTerminating tot
          c = isCovering tot in
        showTot t c
    where
      showTot : Terminating -> Covering -> String
      showTot IsTerminating IsCovering = "total"
      showTot IsTerminating c = show c
      showTot t IsCovering = show t
      showTot t c = show c ++ "; " ++ show t

export
Pretty Totality where
  pretty (MkTotality IsTerminating IsCovering) = pretty "total"
  pretty (MkTotality IsTerminating c) = pretty c
  pretty (MkTotality t IsCovering) = pretty t
  pretty (MkTotality t c) = pretty c <+> semi <++> pretty t

export
unchecked : Totality
unchecked = MkTotality Unchecked IsCovering

export
isTotal : Totality
isTotal = MkTotality Unchecked IsCovering

export
notCovering : Totality
notCovering = MkTotality Unchecked (MissingCases [])

public export
data NVar : Name -> List Name -> Type where
     MkNVar : {i : Nat} -> (0 p : IsVar n i vars) -> NVar n vars

export
weakenNVar : (ns : List Name) ->
             {idx : Nat} -> (0 p : IsVar name idx inner) ->
             NVar name (ns ++ inner)
weakenNVar [] x = MkNVar x
weakenNVar (y :: xs) x
   = let MkNVar x' = weakenNVar xs x in
         MkNVar (Later x')

export
insertNVar : {outer : List Name} ->
            (idx : Nat) ->
            (0 p : IsVar name idx (outer ++ inner)) ->
            NVar name (outer ++ n :: inner)
insertNVar {outer = []} idx x = MkNVar (Later x)
insertNVar {outer = (name :: xs)} Z First = MkNVar First
insertNVar {n} {outer = (x :: xs)} (S i) (Later y)
    = let MkNVar prf = insertNVar {n} i y in
          MkNVar (Later prf)

export
insertVar : {outer : _} ->
            (idx : Nat) ->
            (0 p : IsVar name idx (outer ++ inner)) ->
            Var (outer ++ n :: inner)
insertVar {outer = []} idx x = MkVar (Later x)
insertVar {outer = (name :: xs)} Z First = MkVar First
insertVar {n} {outer = (x :: xs)} (S i) (Later y)
    = let MkVar prf = insertVar {n} i y in
          MkVar (Later prf)

export
weakenVar : (ns : List Name) -> {idx : Nat} -> (0 p : IsVar name idx inner) ->
            Var (ns ++ inner)
weakenVar [] x = MkVar x
weakenVar (y :: xs) x
   = let MkVar x' = weakenVar xs x in
         MkVar (Later x')

export
insertVarNames : {outer, ns : _} ->
                 (idx : Nat) ->
                 (0 p : IsVar name idx (outer ++ inner)) ->
                 Var (outer ++ (ns ++ inner))
insertVarNames {ns} {outer = []} idx prf = weakenVar ns prf
insertVarNames {outer = (y :: xs)} Z First = MkVar First
insertVarNames {ns} {outer = (y :: xs)} (S i) (Later x)
    = let MkVar prf = insertVarNames {ns} i x in
          MkVar (Later prf)

export
insertNVarNames : {outer, ns : _} ->
                  (idx : Nat) ->
                  (0 p : IsVar name idx (outer ++ inner)) ->
                  NVar name (outer ++ (ns ++ inner))
insertNVarNames {ns} {outer = []} idx prf = weakenNVar ns prf
insertNVarNames {outer = (y :: xs)} Z First = MkNVar First
insertNVarNames {ns} {outer = (y :: xs)} (S i) (Later x)
    = let MkNVar prf = insertNVarNames {ns} i x in
          MkNVar (Later prf)

export
insertNames : {outer, inner : _} ->
              (ns : List Name) -> Term (outer ++ inner) ->
              Term (outer ++ (ns ++ inner))
insertNames ns (Local fc r idx prf)
    = let MkNVar prf' = insertNVarNames {ns} idx prf in
          Local fc r _ prf'
insertNames ns (Ref fc nt name) = Ref fc nt name
insertNames ns (Meta fc name idx args)
    = Meta fc name idx (map (insertNames ns) args)
insertNames {outer} {inner} ns (Bind fc x b scope)
    = Bind fc x (assert_total (map (insertNames ns) b))
           (insertNames {outer = x :: outer} {inner} ns scope)
insertNames ns (App fc fn arg)
    = App fc (insertNames ns fn) (insertNames ns arg)
insertNames ns (As fc s as tm)
    = As fc s (insertNames ns as) (insertNames ns tm)
insertNames ns (TDelayed fc r ty) = TDelayed fc r (insertNames ns ty)
insertNames ns (TDelay fc r ty tm)
    = TDelay fc r (insertNames ns ty) (insertNames ns tm)
insertNames ns (TForce fc r tm) = TForce fc r (insertNames ns tm)
insertNames ns (PrimVal fc c) = PrimVal fc c
insertNames ns (Erased fc i) = Erased fc i
insertNames ns (TType fc) = TType fc

export
Weaken Term where
  weakenNs ns tm = insertNames {outer = []} ns tm

export
Weaken Var where
  weaken (MkVar p) = MkVar (Later p)

export
varExtend : IsVar x idx xs -> IsVar x idx (xs ++ ys)
-- What Could Possibly Go Wrong?
-- This relies on the runtime representation of the term being the same
-- after embedding! It is just an identity function at run time, though, and
-- we don't need its definition at compile time, so let's do it...
varExtend p = believe_me p

export
embed : Term vars -> Term (vars ++ more)
embed tm = believe_me tm

public export
ClosedTerm : Type
ClosedTerm = Term []

export
apply : FC -> Term vars -> List (Term vars) -> Term vars
apply loc fn [] = fn
apply loc fn (a :: args) = apply loc (App loc fn a) args

-- Build a simple function type
export
fnType : {vars : _} -> FC -> Term vars -> Term vars -> Term vars
fnType fc arg scope = Bind emptyFC (MN "_" 0) (Pi fc top Explicit arg) (weaken scope)

export
linFnType : {vars : _} -> FC -> Term vars -> Term vars -> Term vars
linFnType fc arg scope = Bind emptyFC (MN "_" 0) (Pi fc linear Explicit arg) (weaken scope)

export
getFnArgs : Term vars -> (Term vars, List (Term vars))
getFnArgs tm = getFA [] tm
  where
    getFA : List (Term vars) -> Term vars ->
            (Term vars, List (Term vars))
    getFA args (App _ f a) = getFA (a :: args) f
    getFA args tm = (tm, args)

export
getFn : Term vars -> Term vars
getFn (App _ f a) = getFn f
getFn tm = tm

export
getArgs : Term vars -> (List (Term vars))
getArgs = snd . getFnArgs

public export
data CompatibleVars : List Name -> List Name -> Type where
     CompatPre : CompatibleVars xs xs
     CompatExt : CompatibleVars xs ys -> CompatibleVars (n :: xs) (m :: ys)

export
areVarsCompatible : (xs : List Name) -> (ys : List Name) ->
                    Maybe (CompatibleVars xs ys)
areVarsCompatible [] [] = pure CompatPre
areVarsCompatible (x :: xs) (y :: ys)
    = do compat <- areVarsCompatible xs ys
         pure (CompatExt compat)
areVarsCompatible _ _ = Nothing

extendCompats : (args : List Name) ->
                CompatibleVars xs ys ->
                CompatibleVars (args ++ xs) (args ++ ys)
extendCompats [] prf = prf
extendCompats (x :: xs) prf = CompatExt (extendCompats xs prf)

renameLocalRef : CompatibleVars xs ys ->
                 {idx : Nat} ->
                 (0 p : IsVar name idx xs) ->
                 Var ys
renameLocalRef prf p = believe_me (MkVar p)
-- renameLocalRef CompatPre First = (MkVar First)
-- renameLocalRef (CompatExt x) First = (MkVar First)
-- renameLocalRef CompatPre (Later p) = (MkVar (Later p))
-- renameLocalRef (CompatExt y) (Later p)
--     = let (MkVar p') = renameLocalRef y p in MkVar (Later p')

renameVarList : CompatibleVars xs ys -> Var xs -> Var ys
renameVarList prf (MkVar p) = renameLocalRef prf p

export
renameVars : CompatibleVars xs ys -> Term xs -> Term ys
renameVars compat tm = believe_me tm -- no names in term, so it's identity
-- This is how we would define it:
-- renameVars CompatPre tm = tm
-- renameVars prf (Local fc r idx vprf)
--     = let MkVar vprf' = renameLocalRef prf vprf in
--           Local fc r _ vprf'
-- renameVars prf (Ref fc x name) = Ref fc x name
-- renameVars prf (Meta fc n i args)
--     = Meta fc n i (map (renameVars prf) args)
-- renameVars prf (Bind fc x b scope)
--     = Bind fc x (map (renameVars prf) b) (renameVars (CompatExt prf) scope)
-- renameVars prf (App fc fn arg)
--     = App fc (renameVars prf fn) (renameVars prf arg)
-- renameVars prf (As fc s as tm)
--     = As fc s (renameVars prf as) (renameVars prf tm)
-- renameVars prf (TDelayed fc r ty) = TDelayed fc r (renameVars prf ty)
-- renameVars prf (TDelay fc r ty tm)
--     = TDelay fc r (renameVars prf ty) (renameVars prf tm)
-- renameVars prf (TForce fc r x) = TForce fc r (renameVars prf x)
-- renameVars prf (PrimVal fc c) = PrimVal fc c
-- renameVars prf (Erased fc i) = Erased fc i
-- renameVars prf (TType fc) = TType fc

export
renameTop : (m : Name) -> Term (n :: vars) -> Term (m :: vars)
renameTop m tm = renameVars (CompatExt CompatPre) tm

public export
data SubVars : List Name -> List Name -> Type where
     SubRefl  : SubVars xs xs
     DropCons : SubVars xs ys -> SubVars xs (y :: ys)
     KeepCons : SubVars xs ys -> SubVars (x :: xs) (x :: ys)

export
subElem : {idx : Nat} -> (0 p : IsVar name idx xs) ->
          SubVars ys xs -> Maybe (Var ys)
subElem prf SubRefl = Just (MkVar prf)
subElem First (DropCons p) = Nothing
subElem (Later x) (DropCons p)
    = do MkVar prf' <- subElem x p
         Just (MkVar prf')
subElem First (KeepCons p) = Just (MkVar First)
subElem (Later x) (KeepCons p)
    = do MkVar prf' <- subElem x p
         Just (MkVar (Later prf'))

export
subExtend : (ns : List Name) -> SubVars xs ys -> SubVars (ns ++ xs) (ns ++ ys)
subExtend [] sub = sub
subExtend (x :: xs) sub = KeepCons (subExtend xs sub)

export
subInclude : (ns : List Name) -> SubVars xs ys -> SubVars (xs ++ ns) (ys ++ ns)
subInclude ns SubRefl = SubRefl
subInclude ns (DropCons p) = DropCons (subInclude ns p)
subInclude ns (KeepCons p) = KeepCons (subInclude ns p)

mutual
  export
  shrinkPi : PiInfo (Term vars) -> SubVars newvars vars ->
             Maybe (PiInfo (Term newvars))
  shrinkPi Explicit prf = pure Explicit
  shrinkPi Implicit prf = pure Implicit
  shrinkPi AutoImplicit prf = pure AutoImplicit
  shrinkPi (DefImplicit t) prf = pure (DefImplicit !(shrinkTerm t prf))

  export
  shrinkBinder : Binder (Term vars) -> SubVars newvars vars ->
                 Maybe (Binder (Term newvars))
  shrinkBinder (Lam fc c p ty) prf
      = Just (Lam fc c !(shrinkPi p prf) !(shrinkTerm ty prf))
  shrinkBinder (Let fc c val ty) prf
      = Just (Let fc c !(shrinkTerm val prf) !(shrinkTerm ty prf))
  shrinkBinder (Pi fc c p ty) prf
      = Just (Pi fc c !(shrinkPi p prf) !(shrinkTerm ty prf))
  shrinkBinder (PVar fc c p ty) prf
      = Just (PVar fc c !(shrinkPi p prf) !(shrinkTerm ty prf))
  shrinkBinder (PLet fc c val ty) prf
      = Just (PLet fc c !(shrinkTerm val prf) !(shrinkTerm ty prf))
  shrinkBinder (PVTy fc c ty) prf
      = Just (PVTy fc c !(shrinkTerm ty prf))

  export
  shrinkVar : Var vars -> SubVars newvars vars -> Maybe (Var newvars)
  shrinkVar (MkVar x) prf = subElem x prf

  export
  shrinkTerm : Term vars -> SubVars newvars vars -> Maybe (Term newvars)
  shrinkTerm (Local fc r idx loc) prf
     = case subElem loc prf of
            Nothing => Nothing
            Just (MkVar loc') => Just (Local fc r _ loc')
  shrinkTerm (Ref fc x name) prf = Just (Ref fc x name)
  shrinkTerm (Meta fc x y xs) prf
     = do xs' <- traverse (\x => shrinkTerm x prf) xs
          Just (Meta fc x y xs')
  shrinkTerm (Bind fc x b scope) prf
     = Just (Bind fc x !(shrinkBinder b prf) !(shrinkTerm scope (KeepCons prf)))
  shrinkTerm (App fc fn arg) prf
     = Just (App fc !(shrinkTerm fn prf) !(shrinkTerm arg prf))
  shrinkTerm (As fc s as tm) prf
     = Just (As fc s !(shrinkTerm as prf) !(shrinkTerm tm prf))
  shrinkTerm (TDelayed fc x y) prf
     = Just (TDelayed fc x !(shrinkTerm y prf))
  shrinkTerm (TDelay fc x t y) prf
     = Just (TDelay fc x !(shrinkTerm t prf) !(shrinkTerm y prf))
  shrinkTerm (TForce fc r x) prf
     = Just (TForce fc r !(shrinkTerm x prf))
  shrinkTerm (PrimVal fc c) prf = Just (PrimVal fc c)
  shrinkTerm (Erased fc i) prf = Just (Erased fc i)
  shrinkTerm (TType fc) prf = Just (TType fc)

varEmbedSub : SubVars small vars ->
              {idx : Nat} -> (0 p : IsVar n idx small) ->
              Var vars
varEmbedSub SubRefl y = MkVar y
varEmbedSub (DropCons prf) y
    = let MkVar y' = varEmbedSub prf y in
          MkVar (Later y')
varEmbedSub (KeepCons prf) First = MkVar First
varEmbedSub (KeepCons prf) (Later p)
    = let MkVar p' = varEmbedSub prf p in
          MkVar (Later p')

export
embedSub : SubVars small vars -> Term small -> Term vars
embedSub sub (Local fc x idx y)
    = let MkVar y' = varEmbedSub sub y in Local fc x _ y'
embedSub sub (Ref fc x name) = Ref fc x name
embedSub sub (Meta fc x y xs)
    = Meta fc x y (map (embedSub sub) xs)
embedSub sub (Bind fc x b scope)
    = Bind fc x (map (embedSub sub) b) (embedSub (KeepCons sub) scope)
embedSub sub (App fc fn arg)
    = App fc (embedSub sub fn) (embedSub sub arg)
embedSub sub (As fc s nm pat)
    = As fc s (embedSub sub nm) (embedSub sub pat)
embedSub sub (TDelayed fc x y) = TDelayed fc x (embedSub sub y)
embedSub sub (TDelay fc x t y)
    = TDelay fc x (embedSub sub t) (embedSub sub y)
embedSub sub (TForce fc r x) = TForce fc r (embedSub sub x)
embedSub sub (PrimVal fc c) = PrimVal fc c
embedSub sub (Erased fc i) = Erased fc i
embedSub sub (TType fc) = TType fc

namespace Bounds
  public export
  data Bounds : List Name -> Type where
       None : Bounds []
       Add : (x : Name) -> Name -> Bounds xs -> Bounds (x :: xs)

export
addVars : {later, bound : _} ->
          {idx : Nat} ->
          Bounds bound -> (0 p : IsVar name idx (later ++ vars)) ->
          NVar name (later ++ (bound ++ vars))
addVars {later = []} {bound} bs p = weakenNVar bound p
addVars {later = (x :: xs)} bs First = MkNVar First
addVars {later = (x :: xs)} bs (Later p)
  = let MkNVar p' = addVars {later = xs} bs p in
        MkNVar (Later p')

resolveRef : {later : _} ->
             (done : List Name) -> Bounds bound -> FC -> Name ->
             Maybe (Term (later ++ (done ++ bound ++ vars)))
resolveRef done None fc n = Nothing
resolveRef {later} {vars} done (Add {xs} new old bs) fc n
    = if n == old
         then rewrite appendAssociative later done (new :: xs ++ vars) in
              let MkNVar p = weakenNVar {inner = new :: xs ++ vars}
                                        (later ++ done) First in
                     Just (Local fc Nothing _ p)
         else rewrite appendAssociative done [new] (xs ++ vars)
                in resolveRef (done ++ [new]) bs fc n

mkLocals : {later, bound : _} ->
           Bounds bound ->
           Term (later ++ vars) -> Term (later ++ (bound ++ vars))
mkLocals bs (Local fc r idx p)
    = let MkNVar p' = addVars bs p in Local fc r _ p'
mkLocals bs (Ref fc Bound name)
    = maybe (Ref fc Bound name) id (resolveRef [] bs fc name)
mkLocals bs (Ref fc nt name)
    = Ref fc nt name
mkLocals bs (Meta fc name y xs)
    = maybe (Meta fc name y (map (mkLocals bs) xs))
            id (resolveRef [] bs fc name)
mkLocals {later} bs (Bind fc x b scope)
    = Bind fc x (map (mkLocals bs) b)
           (mkLocals {later = x :: later} bs scope)
mkLocals bs (App fc fn arg)
    = App fc (mkLocals bs fn) (mkLocals bs arg)
mkLocals bs (As fc s as tm)
    = As fc s (mkLocals bs as) (mkLocals bs tm)
mkLocals bs (TDelayed fc x y)
    = TDelayed fc x (mkLocals bs y)
mkLocals bs (TDelay fc x t y)
    = TDelay fc x (mkLocals bs t) (mkLocals bs y)
mkLocals bs (TForce fc r x)
    = TForce fc r (mkLocals bs x)
mkLocals bs (PrimVal fc c) = PrimVal fc c
mkLocals bs (Erased fc i) = Erased fc i
mkLocals bs (TType fc) = TType fc

export
refsToLocals : {bound : _} ->
               Bounds bound -> Term vars -> Term (bound ++ vars)
refsToLocals None y = y
refsToLocals bs y = mkLocals {later = []} bs y

-- Replace any reference to 'x' with a locally bound name 'new'
export
refToLocal : (x : Name) -> (new : Name) -> Term vars -> Term (new :: vars)
refToLocal x new tm = refsToLocals (Add new x None) tm

export
isVar : (n : Name) -> (ns : List Name) -> Maybe (Var ns)
isVar n [] = Nothing
isVar n (m :: ms)
    = case nameEq n m of
           Nothing => do MkVar p <- isVar n ms
                         pure (MkVar (Later p))
           Just Refl => pure (MkVar First)

-- Replace any Ref Bound in a type with appropriate local
export
resolveNames : (vars : List Name) -> Term vars -> Term vars
resolveNames vars (Ref fc Bound name)
    = case isVar name vars of
           Just (MkVar prf) => Local fc (Just False) _ prf
           _ => Ref fc Bound name
resolveNames vars (Meta fc n i xs)
    = Meta fc n i (map (resolveNames vars) xs)
resolveNames vars (Bind fc x b scope)
    = Bind fc x (map (resolveNames vars) b) (resolveNames (x :: vars) scope)
resolveNames vars (App fc fn arg)
    = App fc (resolveNames vars fn) (resolveNames vars arg)
resolveNames vars (As fc s as pat)
    = As fc s (resolveNames vars as) (resolveNames vars pat)
resolveNames vars (TDelayed fc x y)
    = TDelayed fc x (resolveNames vars y)
resolveNames vars (TDelay fc x t y)
    = TDelay fc x (resolveNames vars t) (resolveNames vars y)
resolveNames vars (TForce fc r x)
    = TForce fc r (resolveNames vars x)
resolveNames vars tm = tm

-- Substitute some explicit terms for names in a term, and remove those
-- names from the scope
namespace SubstEnv
  public export
  data SubstEnv : List Name -> List Name -> Type where
       Nil : SubstEnv [] vars
       (::) : Term vars ->
              SubstEnv ds vars -> SubstEnv (d :: ds) vars

  findDrop : {drop : _} -> {idx : Nat} ->
             FC -> Maybe Bool -> (0 p : IsVar name idx (drop ++ vars)) ->
             SubstEnv drop vars -> Term vars
  findDrop {drop = []} fc r var env = Local fc r _ var
  findDrop {drop = x :: xs} fc r First (tm :: env) = tm
  findDrop {drop = x :: xs} fc r (Later p) (tm :: env)
      = findDrop fc r p env

  find : {drop, vars, outer : _} -> {idx : Nat} ->
         FC -> Maybe Bool -> (0 p : IsVar name idx (outer ++ (drop ++ vars))) ->
         SubstEnv drop vars ->
         Term (outer ++ vars)
  find {outer = []} fc r var env = findDrop fc r var env
  find {outer = x :: xs} fc r First env = Local fc r _ First
  find {outer = x :: xs} fc r (Later p) env = weaken (find fc r p env)

  substEnv : {drop, vars, outer : _} ->
             SubstEnv drop vars -> Term (outer ++ (drop ++ vars)) ->
             Term (outer ++ vars)
  substEnv env (Local fc r _ prf)
      = find fc r prf env
  substEnv env (Ref fc x name) = Ref fc x name
  substEnv env (Meta fc n i xs)
      = Meta fc n i (map (substEnv env) xs)
  substEnv {outer} env (Bind fc x b scope)
      = Bind fc x (map (substEnv env) b)
                  (substEnv {outer = x :: outer} env scope)
  substEnv env (App fc fn arg)
      = App fc (substEnv env fn) (substEnv env arg)
  substEnv env (As fc s as pat)
      = As fc s (substEnv env as) (substEnv env pat)
  substEnv env (TDelayed fc x y) = TDelayed fc x (substEnv env y)
  substEnv env (TDelay fc x t y)
      = TDelay fc x (substEnv env t) (substEnv env y)
  substEnv env (TForce fc r x) = TForce fc r (substEnv env x)
  substEnv env (PrimVal fc c) = PrimVal fc c
  substEnv env (Erased fc i) = Erased fc i
  substEnv env (TType fc) = TType fc

  export
  substs : {drop, vars : _} ->
           SubstEnv drop vars -> Term (drop ++ vars) -> Term vars
  substs env tm = substEnv {outer = []} env tm

  export
  subst : {vars, x : _} -> Term vars -> Term (x :: vars) -> Term vars
  subst val tm = substEnv {outer = []} {drop = [_]} [val] tm

-- Replace an explicit name with a term
export
substName : {vars : _} -> Name -> Term vars -> Term vars -> Term vars
substName x new (Ref fc nt name)
    = case nameEq x name of
           Nothing => Ref fc nt name
           Just Refl => new
substName x new (Meta fc n i xs)
    = Meta fc n i (map (substName x new) xs)
-- ASSUMPTION: When we substitute under binders, the name has always been
-- resolved to a Local, so no need to check that x isn't shadowing
substName x new (Bind fc y b scope)
    = Bind fc y (map (substName x new) b) (substName x (weaken new) scope)
substName x new (App fc fn arg)
    = App fc (substName x new fn) (substName x new arg)
substName x new (As fc s as pat)
    = As fc s as (substName x new pat)
substName x new (TDelayed fc y z)
    = TDelayed fc y (substName x new z)
substName x new (TDelay fc y t z)
    = TDelay fc y (substName x new t) (substName x new z)
substName x new (TForce fc r y)
    = TForce fc r (substName x new y)
substName x new tm = tm

export
addMetas : NameMap Bool -> Term vars -> NameMap Bool
addMetas ns (Local fc x idx y) = ns
addMetas ns (Ref fc x name) = ns
addMetas ns (Meta fc n i xs) = addMetaArgs (insert n False ns) xs
  where
    addMetaArgs : NameMap Bool -> List (Term vars) -> NameMap Bool
    addMetaArgs ns [] = ns
    addMetaArgs ns (t :: ts) = addMetaArgs (addMetas ns t) ts
addMetas ns (Bind fc x (Let _ c val ty) scope)
    = addMetas (addMetas (addMetas ns val) ty) scope
addMetas ns (Bind fc x b scope)
    = addMetas (addMetas ns (binderType b)) scope
addMetas ns (App fc fn arg)
    = addMetas (addMetas ns fn) arg
addMetas ns (As fc s as tm) = addMetas ns tm
addMetas ns (TDelayed fc x y) = addMetas ns y
addMetas ns (TDelay fc x t y)
    = addMetas (addMetas ns t) y
addMetas ns (TForce fc r x) = addMetas ns x
addMetas ns (PrimVal fc c) = ns
addMetas ns (Erased fc i) = ns
addMetas ns (TType fc) = ns

-- Get the metavariable names in a term
export
getMetas : Term vars -> NameMap Bool
getMetas tm = addMetas empty tm

export
addRefs : (underAssert : Bool) -> (aTotal : Name) ->
          NameMap Bool -> Term vars -> NameMap Bool
addRefs ua at ns (Local fc x idx y) = ns
addRefs ua at ns (Ref fc x name) = insert name ua ns
addRefs ua at ns (Meta fc n i xs)
    = addRefsArgs ns xs
  where
    addRefsArgs : NameMap Bool -> List (Term vars) -> NameMap Bool
    addRefsArgs ns [] = ns
    addRefsArgs ns (t :: ts) = addRefsArgs (addRefs ua at ns t) ts
addRefs ua at ns (Bind fc x (Let _ c val ty) scope)
    = addRefs ua at (addRefs ua at (addRefs ua at ns val) ty) scope
addRefs ua at ns (Bind fc x b scope)
    = addRefs ua at (addRefs ua at ns (binderType b)) scope
addRefs ua at ns (App _ (App _ (Ref fc _ name) x) y)
    = if name == at
         then addRefs True at (insert name True ns) y
         else addRefs ua at (addRefs ua at (insert name ua ns) x) y
addRefs ua at ns (App fc fn arg)
    = addRefs ua at (addRefs ua at ns fn) arg
addRefs ua at ns (As fc s as tm) = addRefs ua at ns tm
addRefs ua at ns (TDelayed fc x y) = addRefs ua at ns y
addRefs ua at ns (TDelay fc x t y)
    = addRefs ua at (addRefs ua at ns t) y
addRefs ua at ns (TForce fc r x) = addRefs ua at ns x
addRefs ua at ns (PrimVal fc c) = ns
addRefs ua at ns (Erased fc i) = ns
addRefs ua at ns (TType fc) = ns

-- As above, but for references. Also flag whether a name is under an
-- 'assert_total' because we may need to know that in coverage/totality
-- checking
export
getRefs : (aTotal : Name) -> Term vars -> NameMap Bool
getRefs at tm = addRefs False at empty tm

export
nameAt : {vars : _} ->
         (idx : Nat) -> (0 p : IsVar n idx vars) -> Name
nameAt {vars = n :: ns} Z First = n
nameAt {vars = n :: ns} (S k) (Later p) = nameAt k p

export
{vars : _} -> Show (Term vars) where
  show tm = let (fn, args) = getFnArgs tm in showApp fn args
    where
      showApp : {vars : _} -> Term vars -> List (Term vars) -> String
      showApp (Local {name} _ c idx p) []
         = show (nameAt idx p) ++ "[" ++ show idx ++ "]"
      showApp (Ref _ _ n) [] = show n
      showApp (Meta _ n i args) []
          = "?" ++ show n ++ "_" ++ show args
      showApp (Bind _ x (Lam _ c p ty) sc) []
          = "\\" ++ showCount c ++ show x ++ " : " ++ show ty ++
            " => " ++ show sc
      showApp (Bind _ x (Let _ c val ty) sc) []
          = "let " ++ showCount c ++ show x ++ " : " ++ show ty ++
            " = " ++ show val ++ " in " ++ show sc
      showApp (Bind _ x (Pi _ c Explicit ty) sc) []
          = "((" ++ showCount c ++ show x ++ " : " ++ show ty ++
            ") -> " ++ show sc ++ ")"
      showApp (Bind _ x (Pi _ c Implicit ty) sc) []
          = "{" ++ showCount c ++ show x ++ " : " ++ show ty ++
            "} -> " ++ show sc
      showApp (Bind _ x (Pi _ c AutoImplicit ty) sc) []
          = "{auto " ++ showCount c ++ show x ++ " : " ++ show ty ++
            "} -> " ++ show sc
      showApp (Bind _ x (Pi _ c (DefImplicit tm) ty) sc) []
          = "{default " ++ show tm ++ " "
                ++ showCount c ++ show x ++ " : " ++ show ty ++
            "} -> " ++ show sc
      showApp (Bind _ x (PVar _ c Explicit ty) sc) []
          = "pat " ++ showCount c ++ show x ++ " : " ++ show ty ++
            " => " ++ show sc
      showApp (Bind _ x (PVar _ c Implicit ty) sc) []
          = "{pat " ++ showCount c ++ show x ++ " : " ++ show ty ++
            "} => " ++ show sc
      showApp (Bind _ x (PVar _ c AutoImplicit ty) sc) []
          = "{auto pat " ++ showCount c ++ show x ++ " : " ++ show ty ++
            "} => " ++ show sc
      showApp (Bind _ x (PLet _ c val ty) sc) []
          = "plet " ++ showCount c ++ show x ++ " : " ++ show ty ++
            " = " ++ show val ++ " in " ++ show sc
      showApp (Bind _ x (PVTy _ c ty) sc) []
          = "pty " ++ showCount c ++ show x ++ " : " ++ show ty ++
            " => " ++ show sc
      showApp (App _ _ _) [] = "[can't happen]"
      showApp (As _ _ n tm) [] = show n ++ "@" ++ show tm
      showApp (TDelayed _ _ tm) [] = "%Delayed " ++ show tm
      showApp (TDelay _ _ _ tm) [] = "%Delay " ++ show tm
      showApp (TForce _ _ tm) [] = "%Force " ++ show tm
      showApp (PrimVal _ c) [] = show c
      showApp (Erased _ _) [] = "[__]"
      showApp (TType _) [] = "Type"
      showApp _ [] = "???"
      showApp f args = "(" ++ assert_total (show f) ++ " " ++
                        assert_total (showSep " " (map show args))
                     ++ ")"


text:
%nomangle
foo : Int -> Int
foo x = x

%nomangle "$_baz"
baz : Int -> Int
baz x = x

%nomangle "refc:idr_another_name"
          "javascript:another_name"
anotherName : Int -> Int
anotherName x = x

main : IO ()
main = pure ()

ext: idr


text:
||| This library provides facilities for parsing the command-line options
||| in a standalone program. It is essentially an Idris port of the GNU getopt library.
||| (Actually, it is an Idris port of the [corresponding Haskell module]
||| (http://hackage.haskell.org/package/base-4.14.1.0/docs/System-Console-GetOpt.html)).
module System.Console.GetOpt

import Control.Monad.Reader
import Control.Monad.State

import Data.List
import Data.List1
import Data.Maybe
import Data.String

%default total

||| What to do with options following non-options
public export
data ArgOrder a =
  ||| no option processing after first non-option
  RequireOrder                |
  ||| freely intersperse options and non-options
  Permute                     |
  ||| wrap non-options into options
  ReturnInOrder (String -> a)

export
Functor ArgOrder where
  map _ RequireOrder      = RequireOrder
  map _ Permute           = Permute
  map f (ReturnInOrder g) = ReturnInOrder (f . g)

||| Describes whether an option takes an argument or not, and if so
||| how the argument is injected into a value of type `a`.
public export
data ArgDescr a =
   ||| no argument expected
   NoArg                   a         |
   ||| option requires argument
   ReqArg (String       -> a) String |
   ||| optional argument
   OptArg (Maybe String -> a) String

export
Functor ArgDescr where
  map f (NoArg x)    = NoArg (f x)
  map f (ReqArg g x) = ReqArg (f . g) x
  map f (OptArg g x) = OptArg (f . g) x

||| Each `OptDescr` describes a single option.
|||
||| The arguments to 'Option' are:
|||
||| * list of short option characters
||| * list of long option strings (without \"--\")
||| * argument descriptor
||| * explanation of option for user
public export
record OptDescr a where
  constructor MkOpt
  ||| list of short option characters
  shortNames  : List Char
  ||| list of long option strings (without "--")
  longNames   : List String
  ||| argument descriptor
  argDescr    : ArgDescr a
  ||| explanation of option for user
  description : String

export
Functor OptDescr where
  map f = record { argDescr $= map f }

-- kind of cmd line arg (internal use only):
data OptKind a
   = Opt       a                --    an option
   | UnreqOpt  String           --    an un-recognized option
   | NonOpt    String           --    a non-option
   | EndOfOpts                  --    end-of-options marker (i.e. "--")
   | OptErr    String           --    something went wrong...

--------------------------------------------------------------------------------
--          Printing Usage Info
--------------------------------------------------------------------------------

fmtShort : ArgDescr a -> Char -> String
fmtShort (NoArg  _   ) so = "-" ++ singleton so
fmtShort (ReqArg _ ad) so = "-" ++ singleton so ++ " " ++ ad
fmtShort (OptArg _ ad) so = "-" ++ singleton so ++ "[" ++ ad ++ "]"

fmtLong : ArgDescr a -> String -> String
fmtLong (NoArg  _   ) lo = "--" ++ lo
fmtLong (ReqArg _ ad) lo = "--" ++ lo ++ "=" ++ ad
fmtLong (OptArg _ ad) lo = "--" ++ lo ++ "[=" ++ ad ++ "]"

fmtOpt : OptDescr a -> List (String,String,String)
fmtOpt (MkOpt sos los ad descr) =
  let sosFmt = concat $ intersperse ", " (map (fmtShort ad) sos)
      losFmt = concat $ intersperse ", " (map (fmtLong ad) los)
      (h ::: t) = lines1 descr in
      (sosFmt,losFmt,h) :: map (\s => ("","",s)) t
  where lines1 : String -> List1 String
        lines1 s = case lines s of
                        [] => "" ::: []
                        (x :: xs) => x ::: xs

||| Return a string describing the usage of a command, derived from
||| the header (first argument) and the options described by the
||| second argument.
public export
usageInfo : (header : String) -> List (OptDescr a) -> String
usageInfo header optDescr =
  let (ss,ls,ds)   = (unzip3 . concatMap fmtOpt) optDescr
      paste        = \x,y,z => "  " ++ x ++ "  " ++ y ++ "  " ++ z
      table        = zipWith3 paste (sameLen ss) (sameLen ls) ds
   in unlines $ header :: table

  where flushLeft : Nat -> String -> String
        flushLeft n s = s ++ pack (replicate (n `minus` length s) ' ')

        sameLen : List String -> List String
        sameLen ss = let len = foldl (\n => max n . length) 0 ss
                      in map (flushLeft len) ss

--------------------------------------------------------------------------------
--          Error Formatting
--------------------------------------------------------------------------------

errAmbig : List (OptDescr a) -> (optStr : String) -> OptKind a
errAmbig ods s = let h = "option `" ++ s ++ "' is ambiguous; could be one of:"
                  in OptErr (usageInfo h ods)

errReq : String -> (optStr : String) -> OptKind a
errReq d s = OptErr ("option `" ++ s ++ "' requires an argument " ++ d ++ "\n")

errNoArg : (optStr : String) -> OptKind a
errNoArg s = OptErr ("option `" ++ s ++ "' doesn't allow an argument\n")

--------------------------------------------------------------------------------
--          Parsing Options
--------------------------------------------------------------------------------

||| Result of parsing the command line arguments accoring to a list
||| of `OptDescr`s. (see also function `getOpt`).
public export
record Result a where
  constructor MkResult
  ||| List of successfully parsed options
  options      : List a

  ||| List of non-options (other command line arguments)
  nonOptions   : List String

  ||| List of unrecognized options.
  unrecognized : List String

  ||| Errors during option parsing. These occur, for instance, when
  ||| an option requires an additional argument but none was given.
  errors       : List String

public export
emptyRes : Result a
emptyRes = MkResult [] [] [] []

export
Functor Result where
  map f = record { options $= map f }

OptFun : Type -> Type
OptFun a = List String -> List (OptDescr a) -> (OptKind a,List String)

longOpt : String -> OptFun a
longOpt ls rs descs =
  let (opt,arg) = break ('=' ==) ls
      getWith   = \p => filter (any (p opt) . longNames) descs
      exact     = getWith (==)
      options   = if null exact then getWith isPrefixOf else exact
      ads       = map argDescr options
      os        = "--" ++ opt
   in case (ads,unpack arg,rs) of
           (_ :: _ :: _ , _      ,  r        ) => (errAmbig options os, r)
           ([NoArg  a  ], []     ,  r        ) => (Opt a, r)
           ([NoArg  a  ], c :: _ ,  r        ) => (errNoArg os,r)
--                        ^ this is known (but not proven) to be '='

           ([ReqArg _ d], []     ,  []       ) => (errReq d os,[])
           ([ReqArg f _], []     ,  (r::rest)) => (Opt $ f r,rest)
           ([ReqArg f _], c :: xs,  r        ) => (Opt $ f (pack xs),r)
--                        ^ this is known (but not proven) to be '='

           ([OptArg f _], []     ,  r        ) => (Opt $ f Nothing,r)
           ([OptArg f _], c :: xs,  r        ) => (Opt . f . Just $ pack xs,r)
--                        ^ this is known (but not proven) to be '='

           ([]          , _      ,  r        ) => (UnreqOpt $ "--" ++ ls,r)

shortOpt : Char -> String -> OptFun a
shortOpt y ys rs descs =
  let options = filter (elem y . shortNames) descs
      ads     = map argDescr options
      mkOs    = strCons '-'
      os      = mkOs (singleton y)
   in case (ads,ys,rs) of
           (_ :: _ :: _ , _ ,  r        ) => (errAmbig options os, r)
           ([NoArg  a  ], "",  r        ) => (Opt a,r)
           ([NoArg  a  ], s ,  r        ) => (Opt a, mkOs s :: r)
           ([ReqArg _ d], "",  []       ) => (errReq d os, [])
           ([ReqArg f _], "",  (r::rest)) => (Opt $ f r, rest)
           ([ReqArg f _], s ,  r        ) => (Opt $ f s, r)
           ([OptArg f _], "",  r        ) => (Opt $ f Nothing, r)
           ([OptArg f _], s ,  r        ) => (Opt . f $ Just s, r)
           ([]          , "",  r        ) => (UnreqOpt os, r)
           ([]          , s ,  r        ) => (UnreqOpt os, mkOs s :: r)

-- take a look at the next cmd line arg and decide what to do with it
getNext : List Char -> OptFun a
getNext ('-'::'-'::[]) r _        = (EndOfOpts,r)
getNext ('-'::'-'::xs) r descs    = longOpt (pack xs) r descs
getNext ('-':: x ::xs) r descs    = shortOpt x (pack xs) r descs
getNext a              r _        = (NonOpt $ pack a,r)

||| Process the command-line, and return the list of values that matched
||| (and those that didn't). The arguments are:
|||
||| * The order requirements (see `ArgOrder`)
|||
||| * The option descriptions (see `OptDescr`)
|||
||| * The actual command line arguments (presumably got from
|||   `System.getArgs`).
export
getOpt :  ArgOrder a                         -- non-option handling
       -> List (OptDescr a)                  -- option descriptors
       -> (args : List String)               -- the command-line arguments
       -> Result a
getOpt _        _        []         =  emptyRes
getOpt ordering descs (arg::args)   =
  let (opt,rest) = getNext (unpack arg) args descs
      res        = getOpt ordering descs (assert_smaller args rest)
   in case (opt,ordering) of
           (Opt x, _)                   => {options $= (x::)} res
           (UnreqOpt x, _)              => {unrecognized $= (x::)} res
           (NonOpt x, RequireOrder)     => MkResult [] (x::rest) [] []
           (NonOpt x, Permute)          => {nonOptions $= (x::)} res
           (NonOpt x, ReturnInOrder f)  => {options $= (f x::)} res
           (EndOfOpts, RequireOrder)    => MkResult [] rest [] []
           (EndOfOpts, Permute)         => MkResult [] rest [] []
           (EndOfOpts, ReturnInOrder f) => MkResult (map f rest) [] [] []
           (OptErr e, _)                => {errors $= (e::)} res


text:
%default partial

data Foo : Type -> Type where
     IsNat : Foo Nat
     IsBool : Foo Bool

okay : a -> Foo a -> Bool
okay Z IsNat = False
okay True IsBool = True

bad : a -> Foo a -> Bool
bad Z IsNat = False
bad True IsBool = True
bad (Just 0) _ = False


text:
module CodeGen.CurryingBasedClosures

import Core.Name.Namespace
import Core.Context
import CodeGen.CodeGenHelper
import CairoCode.CairoCode
import CairoCode.CairoCodeUtils
import Data.SortedMap
import Data.SortedSet
import CommonDef
import CairoCode.Traversal.Base
import Utils.Helpers

%hide Prelude.toList

allClosures : List (Name, CairoDef) -> SortedMap Name Int
allClosures defs = snd $ runVisitConcatCairoDefs (pureTraversal closureInfoTraversal) defs
    where closureInfoTraversal : InstVisit CairoReg -> SortedMap Name Int
          closureInfoTraversal (VisitMkClosure _ name missing _) = singleton name (cast missing)
          closureInfoTraversal _ = empty
          Semigroup Int where (<+>) = min

extractOrderedImpls : CairoDef -> List LinearImplicit
extractOrderedImpls (FunDef _ impls _ _) = keys impls
extractOrderedImpls (ForeignDef (MkForeignInfo _ _ impls _ _) _ _) = impls

extractImpls : (Name, CairoDef) -> (Name, SortedSet LinearImplicit)
extractImpls (n, def) = (n, fromList $ extractOrderedImpls def)

extractClosureImplicits : List (Name, CairoDef) -> SortedSet LinearImplicit
extractClosureImplicits defs = snd $ runVisitConcatCairoDefs (pureTraversal closureImplicitsTraversal) defs
    where implicitLookup : SortedMap Name (SortedSet LinearImplicit)
          implicitLookup = fromList $ map extractImpls defs
          closureImplicitsTraversal : InstVisit CairoReg -> SortedSet LinearImplicit
          closureImplicitsTraversal (VisitMkClosure _ name _ _) = fromMaybe empty (lookup name implicitLookup)
          closureImplicitsTraversal _ = empty

deriveCurriedClosureName : Name -> Int -> Name
deriveCurriedClosureName name miss = MN ("curried_"++(cairoName name)) miss

generateCurriedBody : SortedMap LinearImplicit CairoReg -> Name -> Int -> List CairoInst
generateCurriedBody outerImpls callTarget params = projects ++ [MKCLOSURE retReg callTarget 1 (paramRegs ++ [(Param 1)]), RETURN [retReg] outerImpls]
    where retReg : CairoReg
          retReg = Unassigned (Just "ret") 0 0
          paramRegs : List CairoReg
          paramRegs = map (\r => Unassigned (Just "arg") r 0) (fromZeroTo (params - 1))
          projects : List CairoInst
          projects = zipWith (\r,i => PROJECT r (Param 0) (cast i)) paramRegs (fromZeroTo (params - 1) )

generateCallBody : SortedMap LinearImplicit CairoReg -> SortedSet LinearImplicit -> Name -> Int -> List CairoInst
generateCallBody outerImpls innerImpls callTarget params = projects ++ [CALL retRegs implRegs callTarget (paramRegs ++ [(Param 1)]), RETURN retRegs retImpls]
    where retRegs : List CairoReg
          retRegs = [Unassigned (Just "ret") 0 0]
          implRegs : SortedMap LinearImplicit (CairoReg,CairoReg)
          implRegs = mapMap (\(k,v) => (k, (v,Unassigned (Just (implicitName k)) 0 0))) (keyFilter (\k => contains k innerImpls) outerImpls)
          retImpls : SortedMap LinearImplicit CairoReg
          retImpls = foldl (\acc,(i,(_,r)) => insert i r acc) outerImpls (toList implRegs)
          paramRegs : List CairoReg
          paramRegs = map (\r => Unassigned (Just "arg") r 0) (fromZeroTo (params - 1))
          projects : List CairoInst
          projects = zipWith (\r,i => PROJECT r (Param 0) (cast i)) paramRegs (fromZeroTo (params - 1) )

generateClosureWrapperDefs : SortedSet LinearImplicit -> ((Name, CairoDef), Int) -> List (Name, CairoDef)
generateClosureWrapperDefs impls ((name, FunDef params callImpls [_] _), 1) = (deriveCurriedClosureName name 1, FunDef [Param 0, Param 1] nImpls ["applied_ret"] body)::Nil
   where nImpls : SortedMap LinearImplicit CairoReg
         nImpls = fromList $ map (\i => (i, implicitReg i)) (toList impls)
         body : List CairoInst
         body = generateCallBody nImpls (fromList $ keys callImpls) name ((cast $ length params) - 1)

generateClosureWrapperDefs impls (def@(name, FunDef params callImpls [_] _), n) = (deriveCurriedClosureName name n, FunDef [Param 0, Param 1] nImpls ["applied_ret"] body)::(generateClosureWrapperDefs impls (def, n-1))
   where nImpls : SortedMap LinearImplicit CairoReg
         nImpls = fromList $ map (\i => (i, implicitReg i)) (toList impls)
         body : List CairoInst
         body = generateCurriedBody nImpls (deriveCurriedClosureName name (n-1)) ((cast $ length params) - n)

generateClosureWrapperDefs impls ((name, ForeignDef (MkForeignInfo _ _ callImpls _ _) params 1), 1) =  (deriveCurriedClosureName name 1, FunDef [Param 0, Param 1] nImpls ["applied_ret"] body)::Nil
    where nImpls : SortedMap LinearImplicit CairoReg
          nImpls = fromList $ map (\i => (i, implicitReg i)) (toList impls)
          body : List CairoInst
          body = generateCallBody nImpls (fromList callImpls) name ((cast params) - 1)

generateClosureWrapperDefs impls (def@(name, ForeignDef (MkForeignInfo _ _ callImpls _ _) params 1), n) =  (deriveCurriedClosureName name n, FunDef [Param 0, Param 1] nImpls ["applied_ret"] body)::(generateClosureWrapperDefs impls (def, n-1))
    where nImpls : SortedMap LinearImplicit CairoReg
          nImpls = fromList $ map (\i => (i, implicitReg i)) (toList impls)
          body : List CairoInst
          body = generateCurriedBody nImpls (deriveCurriedClosureName name (n-1)) ((cast params) - n)

generateClosureWrapperDefs impls _ = assert_total $ idris_crash "ClosureGen: Closure targets must return a single values"

generateClosureWrappers : SortedSet LinearImplicit -> List (Name, CairoDef) -> List (Name, CairoDef)
generateClosureWrappers impls defs = affectedFunctions >>= (generateClosureWrapperDefs impls)
    where affectedFunctions : List ((Name, CairoDef), Int)
          affectedFunctions = map (\(n,m) => ((n, resolveDef n),m)) (toList $ allClosures defs)
            where defLookup : SortedMap Name CairoDef
                  defLookup = fromList defs
                  resolveDef : Name -> CairoDef
                  resolveDef name = fromMaybe (assert_total $ idris_crash "Currying: Should not happen") (lookup name defLookup)

replaceClosureTarget : List (Name, CairoDef) -> List (Name, CairoDef)
replaceClosureTarget defs = snd $ runVisitTransformCairoDefs (pureTraversal rewireTransform) defs
    where rewireTransform : InstVisit CairoReg -> List (InstVisit CairoReg)
          rewireTransform inst@(VisitMkClosure res name miss args) = [VisitMkClosure res (deriveCurriedClosureName name (cast miss)) 1 args]
          rewireTransform inst = [inst]

export
preprocessClosures : List (Name, CairoDef) -> List (Name, CairoDef)
preprocessClosures cairocode = (generateClosureWrappers impls cairocode) ++ nCairoCode
    where impls : SortedSet LinearImplicit
          impls = extractClosureImplicits cairocode
          nCairoCode : List (Name, CairoDef)
          nCairoCode = replaceClosureTarget cairocode

export
genMkClosure : (res:CairoReg) -> Name -> (missing : Nat) -> (args : List CairoReg) -> String
genMkClosure reg name 1 args = """
    #MKCLOSURE
    let (\{ compileReg reg }_ptr) = alloc()
    \{ compileRegDecl reg } = cast(\{ compileReg reg }_ptr,felt)
    const \{ targetAddr } = \{ targetName } - programStart
    \{ fst res }

    """
    {-
    -- More efficient but not starknet compatible (because it uses hints)
    #MKCLOSURE
    \{ compileRegManifest reg }
    %{ ids.\{regName} = segments.add() %}
    const \{ targetAddr } = \{ targetName } - programStart
    \{ fst res }
    -}
    where regName : String
          regName = compileReg reg
          targetName : String
          targetName = cairoName name
          targetAddr : String
          targetAddr = targetName ++ "_addr"
          offset : Int -> String
          offset n = if n < 0 then " - " ++ show (-n) else " + " ++ show n
          res : (String, Int)
          res = foldl (\(acc, cnt), comp => (acc ++ "assert [\{ regName }\{ offset cnt }] = \{ comp }\n", cnt+1)) ("", 0) (targetAddr::(map compileReg args))
genMkClosure _ name _ _ = assert_total $ idris_crash "CurriedClosureGen: Target \{cairoName name} is not in curried form"

export
genMkApply : (res:CairoReg) -> LinearImplicitArgs -> (f : CairoReg) -> (a : CairoReg) -> String
genMkApply r impls f a = """
    #APPLY closure
    \{ fst mf } tempvar dispatcher = [\{ snd mf }] - (\{jmpPointName} - programStart)
    \{ fst ma } \{concatMap fst mImpls}
    \{ concatMap (\(_,r) => "[ap] = \{ r } ; ap++\n") mImpls}
    [ap] = \{ snd mf }; ap++
    [ap] = \{ snd ma }; ap++
    \{jmpPointName}:
    call rel dispatcher
    \{ compileRegDeclRef r ++ " = [ap-" ++ show (1+numImpls) ++ "]" }
    \{ rImpls }
    """
    where jmpPointName : String
          jmpPointName = (regName r) ++ "_" ++ "jumpPoint"
          mf : (String, String)
          mf = ensureManifested f "closure"
          ma : (String, String)
          ma = ensureManifested a "argument"
          mImpls : List (String, String)
          mImpls = map (\(i,(f,_)) => ensureManifested f ("manifest_"++(implicitName i))) (toList impls)
          numImpls : Int
          numImpls = cast $ length mImpls
          rImpls : String
          rImpls = snd $ foldl (\(idx,acc),(_,r) => (idx-1, acc ++ (compileRegDeclRef r) ++ " = [ap-" ++ show idx ++ "]\n") ) (numImpls,"") (values impls)

max_stars_repo_name: skyro-compiler/skyro

max_issues_repo_name: skyro-compiler/skyro

max_forks_repo_name: skyro-compiler/skyro


text:
module Control.Effect.Labelled

import Control.EffectAlgebra

||| Wrap an effect in a label.
||| This can help disambiguate between multiple identical effects and
||| lessen the number of type annotations.
public export
data Labelled : (label : k)
             -> (sub : (Type -> Type) -> (Type -> Type))
             -> (m : Type -> Type) -> (Type -> Type) where
  MkLabelled : (eff : sub m a) -> Labelled label sub m a

public export
runLabelled : Labelled label sub m a -> sub m a
runLabelled (MkLabelled eff) = eff

public export
Functor (sub m) => Functor (Labelled label sub m) where
  map f (MkLabelled x) = MkLabelled (map f x)

public export
Applicative (sub m) => Applicative (Labelled label sub m) where
  pure x = MkLabelled (pure x)

  (MkLabelled f) <*> (MkLabelled x) = MkLabelled (f <*> x)

public export
Monad (sub m) => Monad (Labelled label sub m) where
  (MkLabelled x) >>= f = MkLabelled (x >>= runLabelled . f)

public export
Algebra (eff :+: sig) (sub m)
  => Algebra (Labelled label eff :+: sig)
             (Labelled label sub m) where
  alg ctxx hdl (Inl (MkLabelled x)) = MkLabelled $
    alg {sig = eff :+: sig, m = sub m}
        ctxx (runLabelled . hdl) (Inl x)
  alg ctxx hdl (Inr x) = MkLabelled $
    alg {sig = eff :+: sig, m = sub m}
        ctxx (runLabelled . hdl) (Inr x)

||| Higher-order injections where signatures are inferred from the label.
public export
interface InjL (0 label : k)
               (0 sub : (Type -> Type) -> (Type -> Type))
               (0 sup : (Type -> Type) -> (Type -> Type)) | label where
  constructor MkSubL
  injLabelled : Labelled label sub m a -> sup m a

public export
[LabelAuto] Inj sub sup => InjL label sub sup where
  injLabelled (MkLabelled x) = inj x

public export
Label : Inj sub sup -> InjL label sub sup
Label x = LabelAuto @{x}

public export
labelled : (label : k)
        -> InjL label sub sig
        => Algebra sig m
        => sub m a -> m a
labelled label @{sub} x =
  let y = injLabelled (MkLabelled {label} x) in
  alg {ctx = id} () id y


text:
module Data.Compress.Utils.Bytes

import Syntax.WithProof
import Data.Bits
import Data.DPair
import Data.Fin
import Data.Fin.Extra
import Data.Nat
import Data.List
import Data.Vect
import Data.Nat.Factor
import Data.Nat.Order.Properties

weakenN' : {m : Nat} -> (0 n : Nat) -> Fin m -> Fin (n + m)
weakenN' n m' = rewrite plusCommutative n m in weakenN n m'

fix_fin : (m : Nat) -> (n : Nat) -> (S m) = n -> S (S (S (S (S (S (S (S (mult m 8)))))))) = mult n 8
fix_fin m n prf = rewrite sym prf in Refl

export
to_le : (FiniteBits a, Cast a Bits8) => {n : _} -> {auto 0 no0 : NonZero n} -> {auto 0 prf : n * 8 = (bitSize {a})} -> a -> Vect n Bits8
to_le x = let (S m) = n; nmeq = Refl in map (go nmeq x) Fin.range
  where
    go : {m : Nat} -> ((S m) = n) -> a -> Fin (S m) -> Bits8
    go nmeq b i = cast $ shiftR b (bitsToIndex $ coerce prf $ coerce (fix_fin m n nmeq) $ weakenN' 7 $ i * 8)

export
from_le : (FiniteBits a, Cast Bits8 a) => {n : _} -> {auto 0 no0 : NonZero n} -> {auto 0 prf : n * 8 = (bitSize {a})} -> Vect n Bits8 -> a
from_le p = let (S m) = n; nmeq = Refl in foldl (.|.) zeroBits $ zipWith (go nmeq) p Fin.range
  where
    go : {m : Nat} -> ((S m) = n) -> Bits8 -> Fin (S m) -> a
    go nmeq b i = shiftL (cast b) (bitsToIndex $ coerce prf $ coerce (fix_fin m n nmeq) $ weakenN' 7 $ i * 8)

export
le_to_integer : Foldable t => t Bits8 -> Integer
le_to_integer = go . toList
  where
  go : List Bits8 -> Integer
  go v = foldr (.|.) 0 $ zipWith shiftL (cast {to=Integer} <$> v) ((*8) <$> [0..(length v)])

export
integer_to_le : (n : Nat) -> Integer -> Vect n Bits8
integer_to_le n v = (cast . shiftR v) <$> (((*8) . finToNat) <$> Fin.range)

export
string_to_ascii : (x : String) -> List Bits8
string_to_ascii = map (cast . ord) . unpack

export
ascii_to_string : List Bits8 -> String
ascii_to_string = pack . map cast


text:
-- exercises in "Type-Driven Development with Idris"
-- chapter 12, section 3 (with added things to update difficulty)

import System
import Data.Primitives.Views

-- check that all functions are total
%default total

record Score where
  constructor MkScore
  correct : Nat
  attempted : Nat

record GameState where
  constructor MkGameState
  score : Score
  difficulty : Int

%name GameState state, state1, state2

Show GameState where
  show s = show (correct (score s)) ++ " / " ++
           show (attempted (score s)) ++ "\n" ++
           "Difficulty: " ++ show (difficulty s)

setDifficulty : Int -> GameState -> GameState
setDifficulty k = record { difficulty = k }

addWrong : GameState -> GameState
addWrong = record { score->attempted $= (+1) }

addCorrect : GameState -> GameState
addCorrect = record { score->attempted $= (+1), score->correct $= (+1) }

initState : Int -> GameState
initState level = MkGameState (MkScore 0 0) level

data Command : Type -> Type where
  PutStr : String -> Command ()
  GetLine : Command String
  GetRandom : Command Int
  GetGameState : Command GameState
  PutGameState : GameState -> Command ()
  Pure : ty -> Command ty
  Bind : Command a -> (a -> Command b) -> Command b

%name Command cmd, cmd1, cmd2

namespace CommandDo
  mutual
    Functor Command where
      map f fa = fa >>= Pure . f

    Applicative Command where
      pure = Pure
      f <*> fa = do f' <- f
                    fa' <- fa
                    Pure (f' fa')

    Monad Command where
      (>>=) = Bind

updateGameState : (GameState -> GameState) -> Command ()
updateGameState f = GetGameState >>= PutGameState . f

data ConsoleIO : Type -> Type where
  Quit : a -> ConsoleIO a
  Do : Command a -> (a -> Inf (ConsoleIO b)) -> ConsoleIO b

namespace ConsoleDo
  (>>=) : Command a -> (a -> Inf (ConsoleIO b)) -> ConsoleIO b
  (>>=) = Do

data Fuel = Dry | More (Lazy Fuel)

partial
forever : Fuel
forever = More forever

runCommand : Stream Int ->
             GameState ->
             Command a ->
             IO (a, Stream Int, GameState)
runCommand xs state (PutStr x)
  = do putStr x
       pure ((), xs, state)
runCommand xs state GetLine
  = do str <- getLine
       pure (str, xs, state)
runCommand (value :: xs) state GetRandom
  = pure (getRandom value (difficulty state), xs, state)
    where
      getRandom : Int -> Int -> Int
      getRandom val max with (divides val max)
        getRandom val 0 | DivByZero = 1
        getRandom ((max * div) + rem) max | (DivBy prf) = abs rem + 1
runCommand xs state GetGameState
  = pure (state, xs, state)
runCommand xs state (PutGameState state1)
  = pure ((), xs, state1)
runCommand xs state (Pure x) = pure (x, xs, state)
runCommand xs state (Bind cmd f)
  = do (res, xs', state') <- runCommand xs state cmd
       runCommand xs' state' (f res)

run : Fuel -> Stream Int -> GameState -> ConsoleIO a ->
      IO (Maybe a, Stream Int, GameState)
run fuel xs state (Quit val)
  = do pure (Just val, xs, state)
run (More fuel) xs state (Do cmd f)
  = do (res, xs', state') <- runCommand xs state cmd
       run fuel xs' state' (f res)
run Dry xs state p
  = pure (Nothing, xs, state)

data Input = Answer Int
           | QuitCmd
           | SetDifficulty Int

mutual
  correct : ConsoleIO GameState
  correct = do PutStr "Correct!\n"
               updateGameState addCorrect
               quiz

  wrong : Int -> ConsoleIO GameState
  wrong ans = do PutStr ("Wrong, the answer is " ++ show ans ++ "\n")
                 updateGameState addWrong
                 quiz

  newDifficulty : Int -> ConsoleIO GameState
  newDifficulty level = do updateGameState (setDifficulty level)
                           PutStr ("Difficulty changed to " ++ show level ++ "\n")
                           PutGameState $ initState level
                           PutStr ("Counters reset to 0\n")
                           quiz

  readInput : (prompt : String) -> Command Input
  readInput prompt = do PutStr prompt
                        input <- GetLine
                        parts <- Pure $ words input
                        case parts of
                          ["quit"] => Pure QuitCmd
                          ["diff", level] => Pure . SetDifficulty . cast $ level
                          _ => Pure . Answer . cast $ input

  quiz : ConsoleIO GameState
  quiz = do num1 <- GetRandom
            num2 <- GetRandom
            st <- GetGameState
            PutStr (show st ++ "\n")
            input <- readInput (show num1 ++ " * " ++ show num2 ++ "? ")
            case input of
              Answer answer => if answer == num1 * num2
                                  then correct
                                  else wrong (num1 * num2)
              SetDifficulty level => newDifficulty level
              QuitCmd => Quit st

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

partial
main : IO ()
main = do seed <- time
          (Just score, _, state) <-
            run forever (randoms (fromInteger seed)) (initState 12) quiz
              | _ => putStrLn "Ran out of fuel"
          putStrLn ("Final score: " ++ show state)

max_stars_repo_name: pascalpoizat/idris-book

max_issues_repo_name: pascalpoizat/idris-book

max_forks_repo_name: pascalpoizat/idris-book


text:
||| A Reversed List
module Data.SnocList

import Decidable.Equality
import Data.List
import Data.Fin

%default total

infixl 7 <><
infixr 6 <>>

||| 'fish': Action of lists on snoc-lists
public export
(<><) : SnocList a -> List a -> SnocList a
sx <>< [] = sx
sx <>< (x :: xs) = sx :< x <>< xs

||| 'chips': Action of snoc-lists on lists
public export
(<>>) : SnocList a -> List a -> List a
Lin       <>> xs = xs
(sx :< x) <>> xs = sx <>> x :: xs

export
Cast (SnocList a) (List a) where
  cast sx = sx <>> []

export
Cast (List a) (SnocList a) where
  cast xs = Lin <>< xs

||| Transform to a list but keeping the contents in the spine order (term depth).
public export
asList : SnocList type -> List type
asList = (reverse . cast)

public export
Eq a => Eq (SnocList a) where
  (==) Lin Lin = True
  (==) (sx :< x) (sy :< y) = x == y && sx == sy
  (==) _ _ = False

public export
Ord a => Ord (SnocList a) where
  compare Lin Lin = EQ
  compare Lin (sx :< x) = LT
  compare (sx :< x) Lin = GT
  compare (sx :< x) (sy :< y)
    = case compare sx sy of
        EQ => compare x y
        c  => c

||| True iff input is Lin
public export
isLin : SnocList a -> Bool
isLin Lin = True
isLin (sx :< x) = False

||| True iff input is (:<)
public export
isSnoc : SnocList a -> Bool
isSnoc Lin     = False
isSnoc (sx :< x) = True

public export
(++) : (sx, sy : SnocList a) -> SnocList a
(++) sx Lin = sx
(++) sx (sy :< y) = (sx ++ sy) :< y

public export
length : SnocList a -> Nat
length Lin = Z
length (sx :< x) = S $ length sx

export
Show a => Show (SnocList a) where
  show xs = concat ("[< " :: intersperse ", " (show' [] xs) ++ ["]"])
    where
      show' : List String -> SnocList a -> List String
      show' acc Lin       = acc
      show' acc (xs :< x) = show' (show x :: acc) xs

public export
Functor SnocList where
  map f Lin = Lin
  map f (sx :< x) = (map f sx) :< (f x)

public export
Semigroup (SnocList a) where
  (<+>) = (++)

public export
Monoid (SnocList a) where
  neutral = Lin

public export
Foldable SnocList where
  foldr f z = foldr f z . (<>> [])

  foldl f z xs = h xs where
    h : SnocList elem -> acc
    h Lin = z
    h (xs :< x) = f (h xs) x

  null Lin      = True
  null (_ :< _) = False

  toList = (<>> [])

  foldMap f = foldl (\xs, x => xs <+> f x) neutral

public export
Applicative SnocList where
  pure = (:<) Lin
  fs <*> xs = concatMap (flip map xs) fs

public export
Monad SnocList where
  xs >>= k = concatMap k xs

public export
Traversable SnocList where
  traverse _ Lin = pure Lin
  traverse f (xs :< x) = [| traverse f xs :< f x |]

public export
Alternative SnocList where
  empty = Lin
  xs <|> ys = xs ++ ys

||| Check if something is a member of a snoc-list using the default Boolean equality.
public export
elem : Eq a => a -> SnocList a -> Bool
elem x Lin = False
elem x (sx :< y) = x == y || elem x sx

||| Find the first element of the snoc-list that satisfies the predicate.
public export
find : (a -> Bool) -> SnocList a -> Maybe a
find p Lin = Nothing
find p (xs :< x) = if p x then Just x else find p xs

||| Satisfiable if `k` is a valid index into `xs`.
|||
||| @ k  the potential index
||| @ xs the snoc-list into which k may be an index
public export
data InBounds : (k : Nat) -> (xs : SnocList a) -> Type where
    ||| Z is a valid index into any cons cell
    InFirst : InBounds Z (xs :< x)
    ||| Valid indices can be extended
    InLater : InBounds k xs -> InBounds (S k) (xs :< x)

||| Find the index and proof of InBounds of the first element (if exists) of a
||| snoc-list that satisfies the given test, else `Nothing`.
public export
findIndex : (a -> Bool) -> (xs : SnocList a) -> Maybe $ Fin (length xs)
findIndex _ Lin = Nothing
findIndex p (xs :< x) = if p x
  then Just FZ
  else FS <$> findIndex p xs


text:
module Compiler.Erlang.Utils.CompositeString

import Data.List

%default total

public export
data CompositeString : Type where
  Str : String -> CompositeString
  Nested : List CompositeString -> CompositeString

export
flatten : CompositeString -> List String
flatten xs = reverse (go xs [])
  where
    go : CompositeString -> List String -> List String
    go (Str str) acc = str :: acc
    go (Nested []) acc = acc
    go (Nested (x :: xs)) acc = assert_total $ go (Nested xs) (go x acc)


text:
module Calc.Mul

%default total

export
multiply : Int -> Int -> Int
multiply x y = x * y

max_stars_repo_name: timmyjose-study/idris-from-the-docs

max_issues_repo_name: timmyjose-study/idris-from-the-docs

max_forks_repo_name: timmyjose-study/idris-from-the-docs


text:
module NatTk

import Tk

Equ Nat where
  Z     ==. Z     = True
  (S n) ==. (S m) = n ==. m
  _     ==. _     = False

  eqRefl Z     = Oh
  eqRefl (S n) = eqRefl n

  eqSymm Z     Z     = Refl
  eqSymm Z     (S _) = Refl
  eqSymm (S _) Z     = Refl
  eqSymm (S n) (S m) = eqSymm n m

  eqTrans Z     Z     Z     Oh Oh = Oh
  eqTrans (S i) (S j) (S k) p  q  = eqTrans i j k p q

  neqIsNotEq n m with (n ==. m)
    | True  = Refl
    | False = Refl

Ordu Nat where
  Z     <. (S _) = True
  (S n) <. (S m) = n <. m
  _     <. Z     = False

  ltArefl Z     = Oh
  ltArefl (S k) = ltArefl k

  ltAsymm Z     Z     _ = Oh
  ltAsymm Z     (S _) _ = Oh
  ltAsymm (S k) (S j) p = ltAsymm k j p

  ltTrans Z     (S _) (S _) Oh _ = Oh
  ltTrans (S i) (S j) (S k) p  q = ltTrans i j k p q

  lteIsLtOrE _ _ = Refl

  gtInverseOfLt _ _ = Refl

  gteIsGtOrE n m = rewrite eqSymm n m in Refl

max_stars_repo_name: buzden/code-in-lectures

max_issues_repo_name: buzden/code-in-lectures

max_forks_repo_name: buzden/code-in-lectures


text:
module Main

import Data.Vect as V

infixr 5 .+.

data Schema = SString
            | SInt
            | SChar
            | (.+.) Schema Schema

SchemaType : Schema -> Type
SchemaType SString = String
SchemaType SInt = Int
SchemaType SChar = Char
SchemaType (x .+. y) = (SchemaType x, SchemaType y)

data Command : Schema -> Type where
     SetSchema : (newSchema : Schema) -> Command schema
     Add : SchemaType schema -> Command schema
     Get : Maybe Integer -> Command schema
     Quit : Command schema

record DataStore where
       constructor MkData
       schema : Schema
       size : Nat
       items : Vect size (SchemaType schema)

-- Writing definitons like below to extract fields for types will become tedious.
-- Instead we can use Idris' record syntax (above), which gives accessor functions as default.
{-
data DataStore : Type where
     MkData : (schema : Schema) ->
              (size : Nat) ->
              (items : Vect size (SchemaType schema)) ->
              DataStore

size : DataStore -> Nat
size (MkData schema size items) = size

schema : DataStore -> Schema
schema (MkData schema size items) = schema

items : (store : DataStore) -> Vect (size store) (SchemaType (schema store))
items (MkData schema size items) = items
-}

parseSchema : List String -> Maybe Schema
parseSchema ("String" :: xs) = case xs of
                                   [] => Just SString
                                   _  => do xs_sch <- parseSchema xs
                                            Just (SString .+. xs_sch)
parseSchema ("Int" :: xs) = case xs of
                                [] => Just SInt
                                _ => do xs_sch <- parseSchema xs
                                        Just (SInt .+. xs_sch)
parseSchema ("Char" :: xs) = case xs of
                                 [] => Just SChar
                                 _  => do xs_sch <- parseSchema xs
                                          Just (SChar .+. xs_sch)
parseSchema _ = Nothing

addToStore : (store : DataStore) -> (SchemaType (schema store)) -> DataStore
addToStore (MkData schema size store) newItem = MkData schema _ (addToData store)
           where
            addToData : Vect oldSize (SchemaType schema) -> Vect (S oldSize) (SchemaType schema)
            addToData [] = [newItem]
            addToData (item :: items) = item :: (addToData items)

display : SchemaType schema -> String
display {schema = SString} item = item
display {schema = SInt} item = cast item
display {schema = SChar} item = cast item
display {schema = (x .+. y)} (iteml, itemr) = "(" ++ (display $ iteml) ++ "," ++ (display $ itemr) ++ ")"

getItem : (id : Integer) -> (store : DataStore) -> Maybe (String, DataStore)
getItem id store = let storeItems = items store in
                       case integerToFin id (size store) of
                            Nothing    => Just $ ("Out of range\n", store)
                            (Just pos) => Just $ ((display (V.index pos storeItems)) ++ "\n", store)

parsePrefix : (schema : Schema) -> String -> Maybe (SchemaType schema, String)
parsePrefix SString input   = getQuoted (unpack input)
            where
            getQuoted : List Char -> Maybe (String, String)
            getQuoted ('"' :: xs)
                      = case span (/= '"') xs of
                             (quoted, '"' :: rest) => Just (pack quoted, ltrim (pack rest))
                             _                     => Nothing
            getQuoted _ = Nothing
parsePrefix SChar input     = case unpack input of
                                   (c :: ' ' :: rest) => Just (c, ltrim (pack rest))
                                   _ => Nothing
parsePrefix SInt input      = case span isDigit input of
                                   ("", rest)  => Nothing
                                   (num, rest) => Just (cast num, ltrim rest)
parsePrefix (schemal .+. schemar) input = case parsePrefix schemal input of
                                               Nothing => Nothing
                                               Just (l_val, input') =>
                                                    case parsePrefix schemar input' of
                                                         Nothing => Nothing
                                                         Just (r_val, input'') => Just ((l_val, r_val), input'')

parseBySchema : (schema : Schema) -> (value : String) -> Maybe (SchemaType schema)
parseBySchema schema input = case parsePrefix schema input of
                                  Just (res, "") => Just res
                                  Just _         => Nothing
                                  Nothing        => Nothing

setSchema : (store : DataStore) -> Schema -> Maybe DataStore
setSchema store schema = case size store of
                              Z     => Just (MkData schema _ [])
                              (S k) => Nothing

total parseCommand : (schema : Schema) -> (cmd : String) -> (args : String) -> Maybe (Command schema)
parseCommand schema "add" value  = do schemaType <- parseBySchema schema value
                                      Just $ Add schemaType
parseCommand schema "get" id     = case unpack id of
                                        [] => Just $ Get Nothing
                                        l  => case all isDigit l of
                                                  False => Nothing
                                                  True  => Just $ Get (Just $ cast id)
-- parseCommand "size" _     = Just Size
parseCommand schema "quit" _     = Just Quit
-- parseCommand "search" str = Just $ Search str
{- ... rest of definition as before ... -}
parseCommand schema "schema" rest
             = do schemaok <- parseSchema (words rest)
                  Just (SetSchema schemaok)
parseCommand _ _ _          = Nothing

parse : (schema : Schema) ->
        (input : String) ->
        Maybe (Command schema)
parse schema input = case span (/= ' ') input of
                     (cmd, args) => parseCommand schema cmd (ltrim args)

processInput : DataStore -> String -> Maybe (String, DataStore)
processInput store input
             = case parse (schema store) input of
                    Nothing         => Just ("Invalid command\n", store)
                    Just (Add item) =>
                      Just ("ID " ++ show (size store) ++ "\n", addToStore store item)
                    Just (SetSchema schema') =>
                      case setSchema store schema' of
                           Nothing     => Just ("Can't update schema\n", store)
                           Just store' => Just ("OK\n", store')
                    Just (Get pos)  => case pos of
                                           Just position => getItem position store
                                           Nothing       => Just $ (unlines $ toList $ map display (items store), store)
                    Just Quit       => Nothing

main : IO ()
main = replWith (MkData (SString .+. SString .+. SInt) _ []) "Command: " processInput

{-

-- Below seems unnecessarily long and verbose to me, need to refactor!
searchStoreItems : (str : String) -> (storeItems : Vect size String) -> (count : Int) -> (acc : String) -> String
searchStoreItems str [] count acc = acc
searchStoreItems str (x :: xs) count acc = if (isInfixOf str x) then searchStoreItems str xs (count + 1) (acc ++ (show count) ++ ": " ++ x ++ "\n")
                                           else searchStoreItems str xs (count + 1) acc

searchStore : (str : String) -> (store : DataStore) -> String
searchStore str store = let storeItems = items store in (searchStoreItems str storeItems 0 "")

processCommand : (command : Command) -> (store : DataStore) -> Maybe (String, DataStore)
processCommand (Add str) store    = Just $ ("Added " ++ str ++ " to store at id " ++ show (size store) ++ "\n", addToStore store str)
processCommand (Get id) store     = getItem id store
processCommand Size store         = Just $ ("No. of Items in Store is " ++ show (size store) ++ "\n", store)
processCommand (Search str) store = Just $ (searchStore str store, store)
processCommand Quit store         = Nothing

processInput : DataStore -> String -> Maybe (String, DataStore)
processInput store input = case parse input of
                                Nothing        => Just $ ("Invalid Command\n", store)
                                (Just command) => processCommand command store
-}

max_stars_repo_name: balajisivaraman/idris-book

max_issues_repo_name: balajisivaraman/idris-book

max_forks_repo_name: balajisivaraman/idris-book


text:
module System.File

import Data.Buffer

import public System.File.Buffer
import public System.File.Error
import public System.File.Handle
import public System.File.Meta
import public System.File.Mode
import public System.File.Permissions
import public System.File.Process
import public System.File.ReadWrite
import public System.File.Types
import public System.File.Virtual

export
copyFile : HasIO io => String -> String -> io (Either FileError ())
copyFile src dest
    = do Right buf <- createBufferFromFile src
             | Left err => pure (Left err)
         writeBufferToFile dest buf !(rawSize buf)