text:
module Core.TTC

import Core.Binary.Prims
import Core.CaseTree
import Core.CompileExpr
import Core.Context
import Core.Core
import Core.Env
import Core.FC
import Core.Name
import Core.Options
import Core.TT

import Libraries.Data.NameMap
import Libraries.Data.PosMap

import Libraries.Data.IOArray
import Data.Vect

import Libraries.Utils.Binary

%default covering

export
TTC Namespace where
  toBuf b = toBuf b . unsafeUnfoldNamespace
  fromBuf = Core.map unsafeFoldNamespace . fromBuf

export
TTC ModuleIdent where
  toBuf b = toBuf b . unsafeUnfoldModuleIdent
  fromBuf = Core.map unsafeFoldModuleIdent . fromBuf

export
TTC VirtualIdent where
  toBuf b Interactive = tag 0
  fromBuf b =
    case !getTag of
      0 => pure Interactive
      _ => corrupt "VirtualIdent"

export
TTC OriginDesc where
  toBuf b (PhysicalIdrSrc ident) = do tag 0; toBuf b ident
  toBuf b (PhysicalPkgSrc fname) = do tag 1; toBuf b fname
  toBuf b (Virtual ident) = do tag 2; toBuf b ident

  fromBuf b =
    case !getTag of
      0 => [| PhysicalIdrSrc (fromBuf b) |]
      1 => [| PhysicalPkgSrc (fromBuf b) |]
      2 => [| Virtual        (fromBuf b) |]
      _ => corrupt "OriginDesc"

export
TTC FC where
  toBuf b (MkFC file startPos endPos)
      = do tag 0; toBuf b file; toBuf b startPos; toBuf b endPos
  toBuf b (MkVirtualFC file startPos endPos)
      = do tag 2; toBuf b file; toBuf b startPos; toBuf b endPos
  toBuf b EmptyFC = tag 1

  fromBuf b
      = case !getTag of
             0 => do f <- fromBuf b;
                     s <- fromBuf b; e <- fromBuf b
                     pure (MkFC f s e)
             1 => pure EmptyFC
             2 => do f <- fromBuf b;
                     s <- fromBuf b; e <- fromBuf b
                     pure (MkVirtualFC f s e)
             _ => corrupt "FC"

export
TTC Name where
  -- for efficiency reasons we do not encode UserName separately
  -- hence the nested pattern matches on UN (Basic/Hole/Field)
  toBuf b (NS xs x) = do tag 0; toBuf b xs; toBuf b x
  toBuf b (UN (Basic x)) = do tag 1; toBuf b x
  toBuf b (MN x y) = do tag 2; toBuf b x; toBuf b y
  toBuf b (PV x y) = do tag 3; toBuf b x; toBuf b y
  toBuf b (DN x y) = do tag 4; toBuf b x; toBuf b y
  toBuf b (UN (Field x)) = do tag 5; toBuf b x
  toBuf b (Nested x y) = do tag 6; toBuf b x; toBuf b y
  toBuf b (CaseBlock x y) = do tag 7; toBuf b x; toBuf b y
  toBuf b (WithBlock x y) = do tag 8; toBuf b x; toBuf b y
  toBuf b (Resolved x)
      = throw (InternalError ("Can't write resolved name " ++ show x))
  toBuf b (UN Underscore) = tag 9

  fromBuf b
      = case !getTag of
             0 => do xs <- fromBuf b
                     x <- fromBuf b
                     pure (NS xs x)
             1 => do x <- fromBuf b
                     pure (UN $ Basic x)
             2 => do x <- fromBuf b
                     y <- fromBuf b
                     pure (MN x y)
             3 => do x <- fromBuf b
                     y <- fromBuf b
                     pure (PV x y)
             4 => do x <- fromBuf b
                     y <- fromBuf b
                     pure (DN x y)
             5 => do x <- fromBuf b
                     pure (UN $ Field x)
             6 => do x <- fromBuf b
                     y <- fromBuf b
                     pure (Nested x y)
             7 => do x <- fromBuf b
                     y <- fromBuf b
                     pure (CaseBlock x y)
             8 => do x <- fromBuf b
                     y <- fromBuf b
                     pure (WithBlock x y)
             9 => pure (UN Underscore)
             _ => corrupt "Name"

export
TTC RigCount where
  toBuf b = elimSemi
              (tag 0)
              (tag 1)
              (const $ tag 2)

  fromBuf b
      = case !getTag of
             0 => pure erased
             1 => pure linear
             2 => pure top
             _ => corrupt "RigCount"

export
TTC t => TTC (PiInfo t) where
  toBuf b Implicit = tag 0
  toBuf b Explicit = tag 1
  toBuf b AutoImplicit = tag 2
  toBuf b (DefImplicit r) = do tag 3; toBuf b r

  fromBuf b
      = case !getTag of
             0 => pure Implicit
             1 => pure Explicit
             2 => pure AutoImplicit
             3 => do t <- fromBuf b; pure (DefImplicit t)
             _ => corrupt "PiInfo"

export
TTC Constant where
  toBuf b (I x) = do tag 0; toBuf b x
  toBuf b (BI x) = do tag 1; toBuf b x
  toBuf b (B8 x) = do tag 2; toBuf b x
  toBuf b (B16 x) = do tag 3; toBuf b x
  toBuf b (B32 x) = do tag 4; toBuf b x
  toBuf b (B64 x) = do tag 5; toBuf b x
  toBuf b (Str x) = do tag 6; toBuf b x
  toBuf b (Ch x) = do tag 7; toBuf b x
  toBuf b (Db x) = do tag 8; toBuf b x

  toBuf b WorldVal = tag 9
  toBuf b IntType = tag 10
  toBuf b IntegerType = tag 11
  toBuf b Bits8Type = tag 12
  toBuf b Bits16Type = tag 13
  toBuf b Bits32Type = tag 14
  toBuf b Bits64Type = tag 15
  toBuf b StringType = tag 16
  toBuf b CharType = tag 17
  toBuf b DoubleType = tag 18
  toBuf b WorldType = tag 19

  toBuf b (I32 x) = do tag 20; toBuf b x
  toBuf b (I64 x) = do tag 21; toBuf b x
  toBuf b Int32Type = tag 22
  toBuf b Int64Type = tag 23
  toBuf b (I8 x) = do tag 24; toBuf b x
  toBuf b (I16 x) = do tag 25; toBuf b x
  toBuf b Int8Type = tag 26
  toBuf b Int16Type = tag 27

  fromBuf b
      = case !getTag of
             0 => do x <- fromBuf b; pure (I x)
             1 => do x <- fromBuf b; pure (BI x)
             2 => do x <- fromBuf b; pure (B8 x)
             3 => do x <- fromBuf b; pure (B16 x)
             4 => do x <- fromBuf b; pure (B32 x)
             5 => do x <- fromBuf b; pure (B64 x)
             6 => do x <- fromBuf b; pure (Str x)
             7 => do x <- fromBuf b; pure (Ch x)
             8 => do x <- fromBuf b; pure (Db x)
             9 => pure WorldVal
             10 => pure IntType
             11 => pure IntegerType
             12 => pure Bits8Type
             13 => pure Bits16Type
             14 => pure Bits32Type
             15 => pure Bits64Type
             16 => pure StringType
             17 => pure CharType
             18 => pure DoubleType
             19 => pure WorldType
             20 => do x <- fromBuf b; pure (I32 x)
             21 => do x <- fromBuf b; pure (I64 x)
             22 => pure Int32Type
             23 => pure Int64Type
             24 => do x <- fromBuf b; pure (I8 x)
             25 => do x <- fromBuf b; pure (I16 x)
             26 => pure Int8Type
             27 => pure Int16Type
             _ => corrupt "Constant"

export
TTC LazyReason where
  toBuf b LInf = tag 0
  toBuf b LLazy = tag 1
  toBuf b LUnknown = tag 2

  fromBuf b
      = case !getTag of
             0 => pure LInf
             1 => pure LLazy
             2 => pure LUnknown
             _ => corrupt "LazyReason"

export
TTC NameType where
  toBuf b Bound = tag 0
  toBuf b Func = tag 1
  toBuf b (DataCon t arity) = do tag 2; toBuf b t; toBuf b arity
  toBuf b (TyCon t arity) = do tag 3; toBuf b t; toBuf b arity

  fromBuf b
      = case !getTag of
             0 => pure Bound
             1 => pure Func
             2 => do x <- fromBuf b; y <- fromBuf b; pure (DataCon x y)
             3 => do x <- fromBuf b; y <- fromBuf b; pure (TyCon x y)
             _ => corrupt "NameType"

-- Assumption is that it was type safe when we wrote it out, so believe_me
-- to rebuild proofs is fine.
-- We're just making up the implicit arguments - this is only fine at run
-- time because those arguments get erased!
-- (Indeed, we're expecting the whole IsVar proof to be erased because
-- we have the idx...)
mkPrf : (idx : Nat) -> IsVar n idx ns
mkPrf {n} {ns} Z = believe_me (First {n} {ns = n :: ns})
mkPrf {n} {ns} (S k) = believe_me (Later {m=n} (mkPrf {n} {ns} k))

getName : (idx : Nat) -> List Name -> Maybe Name
getName Z (x :: xs) = Just x
getName (S k) (x :: xs) = getName k xs
getName _ [] = Nothing

mutual
  export
  {vars : _} -> TTC (Binder (Term vars)) where
    toBuf b (Lam _ c x ty) = do tag 0; toBuf b c; toBuf b x; toBuf b ty
    toBuf b (Let _ c val ty) = do tag 1; toBuf b c; toBuf b val -- ; toBuf b ty
    toBuf b (Pi _ c x ty) = do tag 2; toBuf b c; toBuf b x; toBuf b ty
    toBuf b (PVar _ c p ty) = do tag 3; toBuf b c; toBuf b p; toBuf b ty
    toBuf b (PLet _ c val ty) = do tag 4; toBuf b c; toBuf b val -- ; toBuf b ty
    toBuf b (PVTy _ c ty) = do tag 5; toBuf b c -- ; toBuf b ty

    fromBuf b
        = case !getTag of
               0 => do c <- fromBuf b; x <- fromBuf b; ty <- fromBuf b; pure (Lam emptyFC c x ty)
               1 => do c <- fromBuf b; x <- fromBuf b; pure (Let emptyFC c x (Erased emptyFC False))
               2 => do c <- fromBuf b; x <- fromBuf b; y <- fromBuf b; pure (Pi emptyFC c x y)
               3 => do c <- fromBuf b; p <- fromBuf b; ty <- fromBuf b; pure (PVar emptyFC c p ty)
               4 => do c <- fromBuf b; x <- fromBuf b; pure (PLet emptyFC c x (Erased emptyFC False))
               5 => do c <- fromBuf b; pure (PVTy emptyFC c (Erased emptyFC False))
               _ => corrupt "Binder"

  export
  TTC UseSide where
    toBuf b UseLeft = tag 0
    toBuf b UseRight = tag 1

    fromBuf b
        = case !getTag of
               0 => pure UseLeft
               1 => pure UseRight
               _ => corrupt "UseSide"

  export
  {vars : _} -> TTC (Term vars) where
    toBuf b (Local {name} fc c idx y)
        = if idx < 243
             then do tag (13 + cast idx)
                     toBuf b c
             else do tag 0
                     toBuf b c
                     toBuf b idx
    toBuf b (Ref fc nt name)
        = do tag 1;
             toBuf b nt; toBuf b name
    toBuf b (Meta fc n i xs)
        = do tag 2;
             toBuf b n; toBuf b xs
    toBuf b (Bind fc x bnd scope)
        = do tag 3;
             toBuf b x;
             toBuf b bnd; toBuf b scope
    toBuf b (App fc fn arg)
        = do let (fn, args) = getFnArgs (App fc fn arg)
             case args of
                  [arg] => do tag 4
                              toBuf b fn
                              toBuf b arg
                  args => do tag 12
                             toBuf b fn
                             toBuf b args
    toBuf b (As fc s as tm)
        = do tag 5;
             toBuf b as; toBuf b s; toBuf b tm
    toBuf b (TDelayed fc r tm)
        = do tag 6;
             toBuf b r; toBuf b tm
    toBuf b (TDelay fc r ty tm)
        = do tag 7;
             toBuf b r; toBuf b ty; toBuf b tm
    toBuf b (TForce fc r tm)
        = do tag 8;
             toBuf b r; toBuf b tm
    toBuf b (PrimVal fc c)
        = do tag 9;
             toBuf b c
    toBuf b (Erased fc _)
        = tag 10
    toBuf b (TType fc)
        = tag 11

    fromBuf {vars} b
        = case !getTag of
               0 => do c <- fromBuf b
                       idx <- fromBuf b
                       name <- maybe (corrupt "Term") pure
                                     (getName idx vars)
                       pure (Local {name} emptyFC c idx (mkPrf idx))
               1 => do nt <- fromBuf b; name <- fromBuf b
                       pure (Ref emptyFC nt name)
               2 => do n <- fromBuf b
                       xs <- fromBuf b
                       pure (Meta emptyFC n 0 xs) -- needs resolving
               3 => do x <- fromBuf b
                       bnd <- fromBuf b; scope <- fromBuf b
                       pure (Bind emptyFC x bnd scope)
               4 => do fn <- fromBuf b
                       arg <- fromBuf b
                       pure (App emptyFC fn arg)
               5 => do as <- fromBuf b; s <- fromBuf b; tm <- fromBuf b
                       pure (As emptyFC s as tm)
               6 => do lr <- fromBuf b; tm <- fromBuf b
                       pure (TDelayed emptyFC lr tm)
               7 => do lr <- fromBuf b;
                       ty <- fromBuf b; tm <- fromBuf b
                       pure (TDelay emptyFC lr ty tm)
               8 => do lr <- fromBuf b; tm <- fromBuf b
                       pure (TForce emptyFC lr tm)
               9 => do c <- fromBuf b
                       pure (PrimVal emptyFC c)
               10 => pure (Erased emptyFC False)
               11 => pure (TType emptyFC)
               12 => do fn <- fromBuf b
                        args <- fromBuf b
                        pure (apply emptyFC fn args)
               idxp => do c <- fromBuf b
                          let idx : Nat = fromInteger (cast (idxp - 13))
                          let Just name = getName idx vars
                              | Nothing => corrupt "Term"
                          pure (Local {name} emptyFC c idx (mkPrf idx))

export
TTC Pat where
  toBuf b (PAs fc x y)
      = do tag 0; toBuf b fc; toBuf b x; toBuf b y
  toBuf b (PCon fc x t arity xs)
      = do tag 1; toBuf b fc; toBuf b x; toBuf b t; toBuf b arity; toBuf b xs
  toBuf b (PTyCon fc x arity xs)
      = do tag 2; toBuf b fc; toBuf b x; toBuf b arity; toBuf b xs
  toBuf b (PConst fc c)
      = do tag 3; toBuf b fc; toBuf b c
  toBuf b (PArrow fc x s t)
      = do tag 4; toBuf b fc; toBuf b x; toBuf b s; toBuf b t
  toBuf b (PDelay fc x t y)
      = do tag 5; toBuf b fc; toBuf b x; toBuf b t; toBuf b y
  toBuf b (PLoc fc x)
      = do tag 6; toBuf b fc; toBuf b x
  toBuf b (PUnmatchable fc x)
      = do tag 7; toBuf b fc; toBuf b x

  fromBuf b
      = case !getTag of
             0 => do fc <- fromBuf b; x <- fromBuf b;
                     y <- fromBuf b
                     pure (PAs fc x y)
             1 => do fc <- fromBuf b; x <- fromBuf b
                     t <- fromBuf b; arity <- fromBuf b
                     xs <- fromBuf b
                     pure (PCon fc x t arity xs)
             2 => do fc <- fromBuf b; x <- fromBuf b
                     arity <- fromBuf b
                     xs <- fromBuf b
                     pure (PTyCon fc x arity xs)
             3 => do fc <- fromBuf b; c <- fromBuf b
                     pure (PConst fc c)
             4 => do fc <- fromBuf b; x <- fromBuf b
                     s <- fromBuf b; t <- fromBuf b
                     pure (PArrow fc x s t)
             5 => do fc <- fromBuf b; x <- fromBuf b;
                     t <- fromBuf b; y <- fromBuf b
                     pure (PDelay fc x t y)
             6 => do fc <- fromBuf b; x <- fromBuf b
                     pure (PLoc fc x)
             7 => do fc <- fromBuf b; x <- fromBuf b
                     pure (PUnmatchable fc x)
             _ => corrupt "Pat"

mutual
  export
  {vars : _} -> TTC (CaseTree vars) where
    toBuf b (Case {name} idx x scTy xs)
        = do tag 0; toBuf b name; toBuf b idx; toBuf b xs
    toBuf b (STerm _ x)
        = do tag 1; toBuf b x
    toBuf b (Unmatched msg)
        = do tag 2; toBuf b msg
    toBuf b Impossible = tag 3

    fromBuf b
        = case !getTag of
               0 => do name <- fromBuf b; idx <- fromBuf b
                       xs <- fromBuf b
                       pure (Case {name} idx (mkPrf idx) (Erased emptyFC False) xs)
               1 => do x <- fromBuf b
                       pure (STerm 0 x)
               2 => do msg <- fromBuf b
                       pure (Unmatched msg)
               3 => pure Impossible
               _ => corrupt "CaseTree"

  export
  {vars : _} -> TTC (CaseAlt vars) where
    toBuf b (ConCase x t args y)
        = do tag 0; toBuf b x; toBuf b t; toBuf b args; toBuf b y
    toBuf b (DelayCase ty arg y)
        = do tag 1; toBuf b ty; toBuf b arg; toBuf b y
    toBuf b (ConstCase x y)
        = do tag 2; toBuf b x; toBuf b y
    toBuf b (DefaultCase x)
        = do tag 3; toBuf b x

    fromBuf b
        = case !getTag of
               0 => do x <- fromBuf b; t <- fromBuf b
                       args <- fromBuf b; y <- fromBuf b
                       pure (ConCase x t args y)
               1 => do ty <- fromBuf b; arg <- fromBuf b; y <- fromBuf b
                       pure (DelayCase ty arg y)
               2 => do x <- fromBuf b; y <- fromBuf b
                       pure (ConstCase x y)
               3 => do x <- fromBuf b
                       pure (DefaultCase x)
               _ => corrupt "CaseAlt"

export
{vars : _} -> TTC (Env Term vars) where
  toBuf b [] = pure ()
  toBuf b ((::) bnd env)
      = do toBuf b bnd; toBuf b env

  -- Length has to correspond to length of 'vars'
  fromBuf {vars = []} b = pure Nil
  fromBuf {vars = x :: xs} b
      = do bnd <- fromBuf b
           env <- fromBuf b
           pure (bnd :: env)

export
TTC Visibility where
  toBuf b Private = tag 0
  toBuf b Export = tag 1
  toBuf b Public = tag 2

  fromBuf b
      = case !getTag of
             0 => pure Private
             1 => pure Export
             2 => pure Public
             _ => corrupt "Visibility"

export
TTC PartialReason where
  toBuf b NotStrictlyPositive = tag 0
  toBuf b (BadCall xs) = do tag 1; toBuf b xs
  toBuf b (RecPath xs) = do tag 2; toBuf b xs

  fromBuf b
      = case !getTag of
             0 => pure NotStrictlyPositive
             1 => do xs <- fromBuf b
                     pure (BadCall xs)
             2 => do xs <- fromBuf b
                     pure (RecPath xs)
             _ => corrupt "PartialReason"

export
TTC Terminating where
  toBuf b Unchecked = tag 0
  toBuf b IsTerminating = tag 1
  toBuf b (NotTerminating p) = do tag 2; toBuf b p

  fromBuf b
      = case !getTag of
             0 => pure Unchecked
             1 => pure IsTerminating
             2 => do p <- fromBuf b
                     pure (NotTerminating p)
             _ => corrupt "Terminating"

export
TTC Covering where
  toBuf b IsCovering = tag 0
  toBuf b (MissingCases ms)
      = do tag 1
           toBuf b ms
  toBuf b (NonCoveringCall ns)
      = do tag 2
           toBuf b ns

  fromBuf b
      = case !getTag of
             0 => pure IsCovering
             1 => do ms <- fromBuf b
                     pure (MissingCases ms)
             2 => do ns <- fromBuf b
                     pure (NonCoveringCall ns)
             _ => corrupt "Covering"

export
TTC Totality where
  toBuf b (MkTotality term cov) = do toBuf b term; toBuf b cov

  fromBuf b
      = do term <- fromBuf b
           cov <- fromBuf b
           pure (MkTotality term cov)

export
{n : _} -> TTC (PrimFn n) where
  toBuf b (Add ty) = do tag 0; toBuf b ty
  toBuf b (Sub ty) = do tag 1; toBuf b ty
  toBuf b (Mul ty) = do tag 2; toBuf b ty
  toBuf b (Div ty) = do tag 3; toBuf b ty
  toBuf b (Mod ty) = do tag 4; toBuf b ty
  toBuf b (Neg ty) = do tag 5; toBuf b ty
  toBuf b (ShiftL ty) = do tag 35; toBuf b ty
  toBuf b (ShiftR ty) = do tag 36; toBuf b ty
  toBuf b (BAnd ty) = do tag 37; toBuf b ty
  toBuf b (BOr ty) = do tag 38; toBuf b ty
  toBuf b (BXOr ty) = do tag 39; toBuf b ty
  toBuf b (LT ty) = do tag 6; toBuf b ty
  toBuf b (LTE ty) = do tag 7; toBuf b ty
  toBuf b (EQ ty) = do tag 8; toBuf b ty
  toBuf b (GTE ty) = do tag 9; toBuf b ty
  toBuf b (GT ty) = do tag 10; toBuf b ty
  toBuf b StrLength = tag 11
  toBuf b StrHead = tag 12
  toBuf b StrTail = tag 13
  toBuf b StrIndex = tag 14
  toBuf b StrCons = tag 15
  toBuf b StrAppend = tag 16
  toBuf b StrReverse = tag 17
  toBuf b StrSubstr = tag 18

  toBuf b DoubleExp = tag 19
  toBuf b DoubleLog = tag 20
  toBuf b DoublePow = tag 21
  toBuf b DoubleSin = tag 22
  toBuf b DoubleCos = tag 23
  toBuf b DoubleTan = tag 24
  toBuf b DoubleASin = tag 25
  toBuf b DoubleACos = tag 26
  toBuf b DoubleATan = tag 27
  toBuf b DoubleSqrt = tag 32
  toBuf b DoubleFloor = tag 33
  toBuf b DoubleCeiling = tag 34

  toBuf b (Cast x y) = do tag 99; toBuf b x; toBuf b y
  toBuf b BelieveMe = tag 100
  toBuf b Crash = tag 101

  fromBuf {n} b
      = case n of
             S Z => fromBuf1
             S (S Z) => fromBuf2
             S (S (S Z)) => fromBuf3
             _ => corrupt "PrimFn"
    where
      fromBuf1 : Core (PrimFn 1)
      fromBuf1
          = case !getTag of
                 5 => do ty <- fromBuf b; pure (Neg ty)
                 11 => pure StrLength
                 12 => pure StrHead
                 13 => pure StrTail
                 17 => pure StrReverse
                 19 => pure DoubleExp
                 20 => pure DoubleLog
                 22 => pure DoubleSin
                 23 => pure DoubleCos
                 24 => pure DoubleTan
                 25 => pure DoubleASin
                 26 => pure DoubleACos
                 27 => pure DoubleATan
                 32 => pure DoubleSqrt
                 33 => pure DoubleFloor
                 34 => pure DoubleCeiling

                 99 => do x <- fromBuf b; y <- fromBuf b; pure (Cast x y)
                 _ => corrupt "PrimFn 1"

      fromBuf2 : Core (PrimFn 2)
      fromBuf2
          = case !getTag of
                 0 => do ty <- fromBuf b; pure (Add ty)
                 1 => do ty <- fromBuf b; pure (Sub ty)
                 2 => do ty <- fromBuf b; pure (Mul ty)
                 3 => do ty <- fromBuf b; pure (Div ty)
                 4 => do ty <- fromBuf b; pure (Mod ty)
                 6 => do ty <- fromBuf b; pure (LT ty)
                 7 => do ty <- fromBuf b; pure (LTE ty)
                 8 => do ty <- fromBuf b; pure (EQ ty)
                 9 => do ty <- fromBuf b; pure (GTE ty)
                 10 => do ty <- fromBuf b; pure (GT ty)
                 14 => pure StrIndex
                 15 => pure StrCons
                 16 => pure StrAppend
                 21 => pure DoublePow
                 35 => do ty <- fromBuf b; pure (ShiftL ty)
                 36 => do ty <- fromBuf b; pure (ShiftR ty)
                 37 => do ty <- fromBuf b; pure (BAnd ty)
                 38 => do ty <- fromBuf b; pure (BOr ty)
                 39 => do ty <- fromBuf b; pure (BXOr ty)
                 101 => pure Crash
                 _ => corrupt "PrimFn 2"

      fromBuf3 : Core (PrimFn 3)
      fromBuf3
          = case !getTag of
                 18 => pure StrSubstr
                 100 => pure BelieveMe
                 _ => corrupt "PrimFn 3"

export
TTC ConInfo where
  toBuf b DATACON = tag 0
  toBuf b TYCON = tag 1
  toBuf b NIL = tag 2
  toBuf b CONS = tag 3
  toBuf b ENUM = tag 4
  toBuf b NOTHING = tag 5
  toBuf b JUST = tag 6
  toBuf b RECORD = tag 7
  toBuf b ZERO = tag 8
  toBuf b SUCC = tag 9

  fromBuf b
      = case !getTag of
             0 => pure DATACON
             1 => pure TYCON
             2 => pure NIL
             3 => pure CONS
             4 => pure ENUM
             5 => pure NOTHING
             6 => pure JUST
             7 => pure RECORD
             8 => pure ZERO
             9 => pure SUCC
             _ => corrupt "ConInfo"

mutual
  export
  {vars : _} -> TTC (CExp vars) where
    toBuf b (CLocal fc {x} {idx} h) = do tag 0; toBuf b fc; toBuf b idx
    toBuf b (CRef fc n) = do tag 1; toBuf b fc; toBuf b n
    toBuf b (CLam fc x sc) = do tag 2; toBuf b fc; toBuf b x; toBuf b sc
    toBuf b (CLet fc x inl val sc) = do tag 3; toBuf b fc; toBuf b x; toBuf b inl; toBuf b val; toBuf b sc
    toBuf b (CApp fc f as) = assert_total $ do tag 4; toBuf b fc; toBuf b f; toBuf b as
    toBuf b (CCon fc t n ci as) = assert_total $ do tag 5; toBuf b fc; toBuf b t; toBuf b n; toBuf b ci; toBuf b as
    toBuf b (COp {arity} fc op as) = assert_total $ do tag 6; toBuf b fc; toBuf b arity; toBuf b op; toBuf b as
    toBuf b (CExtPrim fc f as) = assert_total $ do tag 7; toBuf b fc; toBuf b f; toBuf b as
    toBuf b (CForce fc lr x) = assert_total $ do tag 8; toBuf b fc; toBuf b lr; toBuf b x
    toBuf b (CDelay fc lr x) = assert_total $ do tag 9; toBuf b fc; toBuf b lr; toBuf b x
    toBuf b (CConCase fc sc alts def) = assert_total $ do tag 10; toBuf b fc; toBuf b sc; toBuf b alts; toBuf b def
    toBuf b (CConstCase fc sc alts def) = assert_total $ do tag 11; toBuf b fc; toBuf b sc; toBuf b alts; toBuf b def
    toBuf b (CPrimVal fc c) = do tag 12; toBuf b fc; toBuf b c
    toBuf b (CErased fc) = do tag 13; toBuf b fc
    toBuf b (CCrash fc msg) = do tag 14; toBuf b fc; toBuf b msg

    fromBuf b
        = assert_total $ case !getTag of
               0 => do fc <- fromBuf b
                       idx <- fromBuf b
                       let Just x = getName idx vars
                           | Nothing => corrupt "CExp"
                       pure (CLocal {x} fc (mkPrf idx))
               1 => do fc <- fromBuf b
                       n <- fromBuf b
                       pure (CRef fc n)
               2 => do fc <- fromBuf b
                       x <- fromBuf b; sc <- fromBuf b
                       pure (CLam fc x sc)
               3 => do fc <- fromBuf b
                       x <- fromBuf b; inl <- fromBuf b; val <- fromBuf b; sc <- fromBuf b
                       pure (CLet fc x inl val sc)
               4 => do fc <- fromBuf b
                       f <- fromBuf b; as <- fromBuf b
                       pure (CApp fc f as)
               5 => do fc <- fromBuf b
                       t <- fromBuf b; n <- fromBuf b; ci <- fromBuf b; as <- fromBuf b
                       pure (CCon fc t n ci as)
               6 => do fc <- fromBuf b
                       arity <- fromBuf b; op <- fromBuf b; args <- fromBuf b
                       pure (COp {arity} fc op args)
               7 => do fc <- fromBuf b
                       p <- fromBuf b; as <- fromBuf b
                       pure (CExtPrim fc p as)
               8 => do fc <- fromBuf b
                       lr <- fromBuf b
                       x <- fromBuf b
                       pure (CForce fc lr x)
               9 => do fc <- fromBuf b
                       lr <- fromBuf b
                       x <- fromBuf b
                       pure (CDelay fc lr x)
               10 => do fc <- fromBuf b
                        sc <- fromBuf b; alts <- fromBuf b; def <- fromBuf b
                        pure (CConCase fc sc alts def)
               11 => do fc <- fromBuf b
                        sc <- fromBuf b; alts <- fromBuf b; def <- fromBuf b
                        pure (CConstCase fc sc alts def)
               12 => do fc <- fromBuf b
                        c <- fromBuf b
                        pure (CPrimVal fc c)
               13 => do fc <- fromBuf b
                        pure (CErased fc)
               14 => do fc <- fromBuf b
                        msg <- fromBuf b
                        pure (CCrash fc msg)
               _ => corrupt "CExp"

  export
  {vars : _} -> TTC (CConAlt vars) where
    toBuf b (MkConAlt n ci t as sc) = do toBuf b n; toBuf b ci; toBuf b t; toBuf b as; toBuf b sc

    fromBuf b
        = do n <- fromBuf b; ci <- fromBuf b; t <- fromBuf b
             as <- fromBuf b; sc <- fromBuf b
             pure (MkConAlt n ci t as sc)

  export
  {vars : _} -> TTC (CConstAlt vars) where
    toBuf b (MkConstAlt c sc) = do toBuf b c; toBuf b sc

    fromBuf b
        = do c <- fromBuf b; sc <- fromBuf b
             pure (MkConstAlt c sc)

export
TTC CFType where
  toBuf b CFUnit = tag 0
  toBuf b CFInt = tag 1
  toBuf b CFUnsigned8 = tag 2
  toBuf b CFUnsigned16 = tag 3
  toBuf b CFUnsigned32 = tag 4
  toBuf b CFUnsigned64 = tag 5
  toBuf b CFString = tag 6
  toBuf b CFDouble = tag 7
  toBuf b CFChar = tag 8
  toBuf b CFPtr = tag 9
  toBuf b CFWorld = tag 10
  toBuf b (CFFun s t) = do tag 11; toBuf b s; toBuf b t
  toBuf b (CFIORes t) = do tag 12; toBuf b t
  toBuf b (CFStruct n a) = do tag 13; toBuf b n; toBuf b a
  toBuf b (CFUser n a) = do tag 14; toBuf b n; toBuf b a
  toBuf b CFGCPtr = tag 15
  toBuf b CFBuffer = tag 16
  toBuf b CFInt8 = tag 17
  toBuf b CFInt16 = tag 18
  toBuf b CFInt32 = tag 19
  toBuf b CFInt64 = tag 20
  toBuf b CFForeignObj = tag 21
  toBuf b CFInteger = tag 22

  fromBuf b
      = case !getTag of
             0 => pure CFUnit
             1 => pure CFInt
             2 => pure CFUnsigned8
             3 => pure CFUnsigned16
             4 => pure CFUnsigned32
             5 => pure CFUnsigned64
             6 => pure CFString
             7 => pure CFDouble
             8 => pure CFChar
             9 => pure CFPtr
             10 => pure CFWorld
             11 => do s <- fromBuf b; t <- fromBuf b; pure (CFFun s t)
             12 => do t <- fromBuf b; pure (CFIORes t)
             13 => do n <- fromBuf b; a <- fromBuf b; pure (CFStruct n a)
             14 => do n <- fromBuf b; a <- fromBuf b; pure (CFUser n a)
             15 => pure CFGCPtr
             16 => pure CFBuffer
             17 => pure CFInt8
             18 => pure CFInt16
             19 => pure CFInt32
             20 => pure CFInt64
             21 => pure CFForeignObj
             22 => pure CFInteger
             _ => corrupt "CFType"

export
TTC CDef where
  toBuf b (MkFun args cexpr) = do tag 0; toBuf b args; toBuf b cexpr
  toBuf b (MkCon t arity pos) = do tag 1; toBuf b t; toBuf b arity; toBuf b pos
  toBuf b (MkForeign cs args ret) = do tag 2; toBuf b cs; toBuf b args; toBuf b ret
  toBuf b (MkError cexpr) = do tag 3; toBuf b cexpr

  fromBuf b
      = case !getTag of
             0 => do args <- fromBuf b; cexpr <- fromBuf b
                     pure (MkFun args cexpr)
             1 => do t <- fromBuf b; arity <- fromBuf b; pos <- fromBuf b
                     pure (MkCon t arity pos)
             2 => do cs <- fromBuf b; args <- fromBuf b; ret <- fromBuf b
                     pure (MkForeign cs args ret)
             3 => do cexpr <- fromBuf b
                     pure (MkError cexpr)
             _ => corrupt "CDef"

export
TTC CG where
  toBuf b Chez = tag 0
  toBuf b ChezSep = tag 1
  toBuf b Racket = tag 2
  toBuf b Gambit = tag 3
  toBuf b (Other s) = do tag 4; toBuf b s
  toBuf b Node = tag 5
  toBuf b Javascript = tag 6
  toBuf b RefC = tag 7
  toBuf b VMCodeInterp = tag 8
  toBuf b Jvm = tag 9

  fromBuf b
      = case !getTag of
             0 => pure Chez
             1 => pure ChezSep
             2 => pure Racket
             3 => pure Gambit
             4 => do s <- fromBuf b
                     pure (Other s)
             5 => pure Node
             6 => pure Javascript
             7 => pure RefC
             8 => pure VMCodeInterp
             9 => pure Jvm
             _ => corrupt "CG"

export
TTC PairNames where
  toBuf b l
      = do toBuf b (pairType l)
           toBuf b (fstName l)
           toBuf b (sndName l)
  fromBuf b
      = do ty <- fromBuf b
           d <- fromBuf b
           f <- fromBuf b
           pure (MkPairNs ty d f)

export
TTC RewriteNames where
  toBuf b l
      = do toBuf b (equalType l)
           toBuf b (rewriteName l)
  fromBuf b
      = do ty <- fromBuf b
           l <- fromBuf b
           pure (MkRewriteNs ty l)

export
TTC PrimNames where
  toBuf b l
      = do toBuf b (fromIntegerName l)
           toBuf b (fromStringName l)
           toBuf b (fromCharName l)
           toBuf b (fromDoubleName l)
  fromBuf b
      = do i <- fromBuf b
           str <- fromBuf b
           c <- fromBuf b
           d <- fromBuf b
           pure (MkPrimNs i str c d)

export
TTC HoleInfo where
  toBuf b NotHole = tag 0
  toBuf b (SolvedHole n) = do tag 1; toBuf b n

  fromBuf b
      = case !getTag of
             0 => pure NotHole
             1 => do n <- fromBuf b; pure (SolvedHole n)
             _ => corrupt "HoleInfo"

export
TTC PMDefInfo where
  toBuf b l
      = do toBuf b (holeInfo l)
           toBuf b (alwaysReduce l)
           toBuf b (externalDecl l)
  fromBuf b
      = do h <- fromBuf b
           r <- fromBuf b
           e <- fromBuf b
           pure (MkPMDefInfo h r e)

export
TTC TypeFlags where
  toBuf b l
      = do toBuf b (uniqueAuto l)
           toBuf b (external l)
  fromBuf b
      = do u <- fromBuf b
           e <- fromBuf b
           pure (MkTypeFlags u e)

export
TTC Def where
  toBuf b None = tag 0
  toBuf b (PMDef pi args ct rt pats)
      = do tag 1; toBuf b pi; toBuf b args; toBuf b ct; toBuf b pats
  toBuf b (ExternDef a)
      = do tag 2; toBuf b a
  toBuf b (ForeignDef a cs)
      = do tag 3; toBuf b a; toBuf b cs
  toBuf b (Builtin a)
      = throw (InternalError "Trying to serialise a Builtin")
  toBuf b (DCon t arity nt) = do tag 4; toBuf b t; toBuf b arity; toBuf b nt
  toBuf b (TCon t arity parampos detpos u ms datacons dets)
      = do tag 5; toBuf b t; toBuf b arity; toBuf b parampos
           toBuf b detpos; toBuf b u; toBuf b ms; toBuf b datacons
           toBuf b dets
  toBuf b (Hole locs p)
      = do tag 6; toBuf b locs; toBuf b (implbind p)
  toBuf b (BySearch c depth def)
      = do tag 7; toBuf b c; toBuf b depth; toBuf b def
  toBuf b (Guess guess envb constraints)
      = do tag 8; toBuf b guess; toBuf b envb; toBuf b constraints
  toBuf b ImpBind = tag 9
  toBuf b Delayed = tag 10

  fromBuf b
      = case !getTag of
             0 => pure None
             1 => do pi <- fromBuf b
                     args <- fromBuf b
                     ct <- fromBuf b
                     pats <- fromBuf b
                     pure (PMDef pi args ct (Unmatched "") pats)
             2 => do a <- fromBuf b
                     pure (ExternDef a)
             3 => do a <- fromBuf b
                     cs <- fromBuf b
                     pure (ForeignDef a cs)
             4 => do t <- fromBuf b; a <- fromBuf b; nt <- fromBuf b
                     pure (DCon t a nt)
             5 => do t <- fromBuf b; a <- fromBuf b
                     ps <- fromBuf b; dets <- fromBuf b;
                     u <- fromBuf b
                     ms <- fromBuf b; cs <- fromBuf b
                     detags <- fromBuf b
                     pure (TCon t a ps dets u ms cs detags)
             6 => do l <- fromBuf b
                     p <- fromBuf b
                     pure (Hole l (holeInit p))
             7 => do c <- fromBuf b; depth <- fromBuf b
                     def <- fromBuf b
                     pure (BySearch c depth def)
             8 => do g <- fromBuf b; envb <- fromBuf b; cs <- fromBuf b
                     pure (Guess g envb cs)
             9 => pure ImpBind
             10 => pure Context.Delayed
             _ => corrupt "Def"

export
TTC TotalReq where
  toBuf b Total = tag 0
  toBuf b CoveringOnly = tag 1
  toBuf b PartialOK = tag 2

  fromBuf b
      = case !getTag of
             0 => pure Total
             1 => pure CoveringOnly
             2 => pure PartialOK
             _ => corrupt "TotalReq"

TTC DefFlag where
  toBuf b Inline = tag 2
  toBuf b Invertible = tag 3
  toBuf b Overloadable = tag 4
  toBuf b TCInline = tag 5
  toBuf b (SetTotal x) = do tag 6; toBuf b x
  toBuf b BlockedHint = tag 7
  toBuf b Macro = tag 8
  toBuf b (PartialEval x) = tag 9 -- names not useful any more
  toBuf b AllGuarded = tag 10
  toBuf b (ConType ci) = do tag 11; toBuf b ci
  toBuf b (Identity x) = do tag 12; toBuf b x

  fromBuf b
      = case !getTag of
             2 => pure Inline
             3 => pure Invertible
             4 => pure Overloadable
             5 => pure TCInline
             6 => do x <- fromBuf b; pure (SetTotal x)
             7 => pure BlockedHint
             8 => pure Macro
             9 => pure (PartialEval [])
             10 => pure AllGuarded
             11 => do ci <- fromBuf b; pure (ConType ci)
             12 => do x <- fromBuf b; pure (Identity x)
             _ => corrupt "DefFlag"

export
TTC SizeChange where
  toBuf b Smaller = tag 0
  toBuf b Same = tag 1
  toBuf b Unknown = tag 2

  fromBuf b
      = case !getTag of
             0 => pure Smaller
             1 => pure Same
             2 => pure Unknown
             _ => corrupt "SizeChange"

export
TTC SCCall where
  toBuf b c = do toBuf b (fnCall c); toBuf b (fnArgs c)
  fromBuf b
      = do fn <- fromBuf b
           args <- fromBuf b
           pure (MkSCCall fn args)

export
TTC GlobalDef where
  toBuf b gdef
      = -- Only write full details for user specified names. The others will
        -- be holes where all we will ever need after loading is the definition
        do toBuf b (compexpr gdef)
           toBuf b (map NameMap.toList (refersToRuntimeM gdef))
           toBuf b (location gdef)
           -- We don't need any of the rest for code generation, so if
           -- we're decoding then, we can skip these (see Compiler.Common
           -- for how it's decoded minimally there)
           toBuf b (multiplicity gdef)
           toBuf b (fullname gdef)
           toBuf b (map NameMap.toList (refersToM gdef))
           toBuf b (definition gdef)
           when (isUserName (fullname gdef) || cwName (fullname gdef)) $
              do toBuf b (type gdef)
                 toBuf b (eraseArgs gdef)
                 toBuf b (safeErase gdef)
                 toBuf b (specArgs gdef)
                 toBuf b (inferrable gdef)
                 toBuf b (localVars gdef)
                 toBuf b (visibility gdef)
                 toBuf b (totality gdef)
                 toBuf b (flags gdef)
                 toBuf b (invertible gdef)
                 toBuf b (noCycles gdef)
                 toBuf b (sizeChange gdef)
    where
      cwName : Name -> Bool
      cwName (CaseBlock _ _) = True
      cwName (WithBlock _ _) = True
      cwName _ = False
  fromBuf b
      = do cdef <- fromBuf b
           refsRList <- fromBuf b
           let refsR = map fromList refsRList
           loc <- fromBuf b
           mul <- fromBuf b
           name <- fromBuf b
           refsList <- fromBuf b
           let refs = map fromList refsList
           def <- fromBuf b
           if isUserName name
              then do ty <- fromBuf b
                      eargs <- fromBuf b;
                      seargs <- fromBuf b; specargs <- fromBuf b
                      iargs <- fromBuf b;
                      vars <- fromBuf b
                      vis <- fromBuf b; tot <- fromBuf b
                      fl <- fromBuf b
                      inv <- fromBuf b
                      c <- fromBuf b
                      sc <- fromBuf b
                      pure (MkGlobalDef loc name ty eargs seargs specargs iargs
                                        mul vars vis
                                        tot fl refs refsR inv c True def cdef sc)
              else pure (MkGlobalDef loc name (Erased loc False) [] [] [] []
                                     mul [] Public unchecked [] refs refsR
                                     False False True def cdef [])

export
TTC Transform where
  toBuf b (MkTransform {vars} n env lhs rhs)
      = do toBuf b vars
           toBuf b n
           toBuf b env
           toBuf b lhs
           toBuf b rhs

  fromBuf b
      = do vars <- fromBuf b
           n <- fromBuf b
           env <- fromBuf b
           lhs <- fromBuf b
           rhs <- fromBuf b
           pure (MkTransform {vars} n env lhs rhs)

-- decode : Context -> Int -> (update : Bool) -> ContextEntry -> Core GlobalDef
Core.Context.decode gam idx update (Coded ns bin)
    = do b <- newRef Bin bin
         def <- fromBuf b
         let a = getContent gam
         arr <- get Arr
         def' <- resolved gam (restoreNS ns def)
         when update $ coreLift $ writeArray arr idx (Decoded def')
         pure def'
Core.Context.decode gam idx update (Decoded def) = pure def


text:
module Main

import Control.Monad.State

update : (stateType -> stateType) -> State stateType ()
update f = do
  x <- get
  put (f x)

increase : Nat -> State Nat ()
increase n = update (+n)

data Tree a = Empty
            | Node (Tree a) a (Tree a)

testTree : Tree String
testTree = Node (Node (Node Empty "Jim" Empty)
                      "Fred"
                      (Node Empty "Sheila" Empty))
                "Alice"
                (Node Empty "Bob" (Node Empty "Eve" Empty))

countEmpty : Tree a -> State Nat ()
countEmpty Empty = update (+1)
countEmpty (Node left val right) = do
  countEmpty left
  countEmpty right

foundEmpty : State (Nat, Nat) ()
foundEmpty = do
  (e,n) <- get
  put (e + 1, n)

foundNode : State (Nat, Nat) ()
foundNode = do
  (e,n) <- get
  put (e, n + 1)

countEmptyNode : Tree a -> State (Nat, Nat) ()
countEmptyNode Empty = foundEmpty
countEmptyNode (Node left var right) = do
  foundNode
  countEmptyNode left
  countEmptyNode right

main : IO ()
main = do
  printLn $ runState (increase 5) 89
  printLn $ runState (countEmpty testTree) 0
  printLn $ runState (countEmptyNode testTree) (0,0)

ext: idr

max_stars_repo_name: luc-tielen/idris-grin

max_issues_repo_name: luc-tielen/idris-grin

max_forks_repo_name: luc-tielen/idris-grin


text:
module Ifui.Dom

export
data DomNode = MkNode AnyPtr

export
data DomEvent = MkEvent AnyPtr

%foreign "browser:lambda: x => console.log(x)"
prim__consoleLog : AnyPtr -> PrimIO ()
export
consoleLog : HasIO io => a -> io ()
consoleLog x = primIO $ prim__consoleLog (believe_me x)

%foreign "browser:lambda: tag => document.createElement(tag)"
prim__createElement : String -> PrimIO AnyPtr
export
createElement : HasIO io => String -> io DomNode
createElement tag = MkNode <$> (primIO $ prim__createElement tag)

%foreign "browser:lambda: txt => document.createTextNode(txt)"
prim__createTextNode : String -> PrimIO AnyPtr
export
createTextNode : HasIO io => String -> io DomNode
createTextNode txt = MkNode <$> (primIO $ prim__createTextNode txt)

%foreign "browser:lambda: (node, child) => node.appendChild(child)"
prim__appendChild : AnyPtr -> AnyPtr -> PrimIO ()
export
appendChild : HasIO io => DomNode -> DomNode -> io ()
appendChild (MkNode n) (MkNode c) = primIO $ prim__appendChild n c

%foreign "browser:lambda: (node, replacement) => node.replaceWith(replacement)"
prim__replaceWith : AnyPtr -> AnyPtr -> PrimIO ()
export
replaceWith : HasIO io => DomNode -> DomNode -> io ()
replaceWith (MkNode n) (MkNode r) = primIO $ prim__replaceWith n r

%foreign "browser:lambda: () => document.body"
prim__body : () -> PrimIO AnyPtr
export
body : HasIO io => io DomNode
body = MkNode <$> (primIO $ prim__body ())

%foreign "browser:lambda: (n, k, v) => n.setAttribute(k,v)"
prim__setAttribute : AnyPtr -> String -> String -> PrimIO ()
export
setAttribute : HasIO io => DomNode -> String -> String -> io ()
setAttribute (MkNode n) k v = primIO $ prim__setAttribute n k v

%foreign "browser:lambda: (n, k) => n.getAttribute(k)"
prim__getAttribute : AnyPtr -> String -> PrimIO String
export
getAttribute : HasIO io => DomNode -> String -> io String
getAttribute (MkNode n) k = primIO $ prim__getAttribute n k

%foreign "browser:lambda: n => n.value"
prim__getValue : AnyPtr -> PrimIO String
export
getValue : HasIO io => DomNode -> io String
getValue (MkNode n) = primIO $ prim__getValue n

%foreign "browser:lambda: (n, v) => n.value = v"
prim__setValue : AnyPtr -> String -> PrimIO ()
export
setValue : HasIO io => DomNode -> String -> io ()
setValue (MkNode n) v = primIO $ prim__setValue n v

%foreign "browser:lambda: (event, callback, node) =>{const f = x=>callback(x)(); node.addEventListener(event, f); return () => node.removeEventListener(event, f);}"
prim__addEventListener : String -> (AnyPtr -> PrimIO ()) -> AnyPtr -> PrimIO (PrimIO ())
export
addEventListener : HasIO io => String -> (DomEvent -> IO ()) -> DomNode -> io (IO ())
addEventListener event callback (MkNode n) =
  do
    remove <- primIO $ prim__addEventListener event (\ptr => toPrim  $ callback $ MkEvent ptr) n
    pure $ primIO remove

%foreign "browser:lambda: e => e.target.value"
prim__targetValue : AnyPtr -> PrimIO String
export
targetValue : HasIO io => DomEvent -> io String
targetValue (MkEvent x) = primIO $ prim__targetValue x

%foreign "browser:lambda: n => BigInt(n.length)"
prim__length : AnyPtr -> PrimIO Int
%foreign "browser:lambda: (i,xs) => xs[i]"
prim__get : Int -> AnyPtr -> PrimIO AnyPtr

%foreign "browser:lambda: n => n.children"
prim__getChildren : AnyPtr -> PrimIO AnyPtr
export
getChildren : HasIO io => DomNode -> io (List DomNode)
getChildren (MkNode x) =
  do
    childrenPtr <- primIO $ prim__getChildren x
    len <- primIO $ prim__length childrenPtr
    nodesPtr <- traverse (\i => primIO $ prim__get i childrenPtr) [0..(len-1)]
    pure $ map MkNode nodesPtr

%foreign "browser:lambda: n => n.childNodes"
prim__getChildNodes : AnyPtr -> PrimIO AnyPtr
export
getChildNodes : HasIO io => DomNode -> io (List DomNode)
getChildNodes (MkNode x) =
  do
    childsPtr <- primIO $ prim__getChildNodes x
    len <- primIO $ prim__length childsPtr
    nodesPtr <- traverse (\i => primIO $ prim__get i childsPtr) [0..(len-1)]
    pure $ map MkNode nodesPtr

%foreign "browser:lambda: n => n.firstElementChild"
prim__firstElementChild : AnyPtr -> PrimIO AnyPtr
export
firstElementChild : HasIO io => DomNode -> io DomNode
firstElementChild (MkNode x) = map MkNode $ primIO $ prim__firstElementChild x

%foreign "browser:lambda: n => n.firstChild"
prim__firstChild : AnyPtr -> PrimIO AnyPtr
export
firstChild : HasIO io => DomNode -> io DomNode
firstChild (MkNode x) = map MkNode $ primIO $ prim__firstChild x

%foreign "browser:lambda: n => n.innerHTML=''"
prim__removeAllChildren : AnyPtr -> PrimIO ()
export
removeAllChildren : HasIO io => DomNode -> io ()
removeAllChildren (MkNode x) = primIO $ prim__removeAllChildren x

%foreign "browser:lambda: (n, t) => n.textContent=t"
prim__setTextContent : AnyPtr -> String -> PrimIO ()
export
setTextContent : HasIO io => DomNode -> String -> io ()
setTextContent (MkNode x) s = primIO $ prim__setTextContent x s

%foreign "browser:lambda: n => n.remove()"
prim__removeNode : AnyPtr -> PrimIO ()
export
removeNode : HasIO io => DomNode -> io ()
removeNode (MkNode x) = primIO $ prim__removeNode x

max_stars_repo_name: rbarreiro/ifui

max_issues_repo_name: rbarreiro/ifui

max_forks_repo_name: rbarreiro/ifui


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

import GRL.Lang.GLang

import Sif.Types
import Sif.Pattern

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

%access export
%default partial

-- --------------------------------------------------- [ Interpretation Result ]

SifMetaModel GModel where
  toString x = GLang.toString x

public export
data InterpRes : SifTy -> Type where
  IReq    : GLang ELEM -> InterpRes TyREQ
  IProb   : GLang ELEM -> GModel               -> InterpRes TyPROBLEM
  IAffect : GLang ELEM -> CValue               -> InterpRes TyAFFECTS
  ITrait  : GLang ELEM -> List (GLang INTENT)  -> InterpRes TyTRAIT
  IProp   : GLang ELEM -> DList GTy GLang es   -> InterpRes TyPROPERTY
  ISolt   : GLang ELEM -> DList GTy GLang ss   -> InterpRes TySOLUTION
  IPatt   : GModel                             -> InterpRes TyPATTERN

interpReq : String -> InterpRes TyREQ
interpReq s = IReq root
  where
    root : GLang ELEM
    root = mkGoal ("Requirement: " ++ s)

interpProb : String -> List (InterpRes TyREQ) -> InterpRes TyPROBLEM
interpProb s ps = IProb root (model' \= (root &= cs))
  where
    root : GLang ELEM
    root = mkGoal ("Problem: " ++ s)

    cs : List (GLang ELEM)
    cs = map (\(IReq x) => x) ps

    model : GModel
    model = (emptyModel \= root)

    model' : GModel
    model' = insertMany cs model

interpAffect : CValue -> InterpRes TyREQ -> InterpRes TyAFFECTS
interpAffect c (IReq r) = IAffect r c

interpTrait : String
           -> SValue
           -> List (InterpRes TyAFFECTS)
           -> TTy
           -> InterpRes TyTRAIT
interpTrait s m es ty = ITrait node cs
  where
    sVal : SValue -> SValue
    sVal v = case ty of  -- Disadvantages...
               GEN => v
               ADV => v
               DIS => v -- invertEval v

    tVal : String
    tVal = case ty of
             GEN => "Trait General:"
             ADV => "Trait Advantage: "
             DIS => "Trait Disadvantage: "

    node : GLang ELEM
    node = mkSatTask (tVal ++ s) (sVal m)

    cs : List (GLang INTENT)
    cs = map (\(IAffect r c) => node ==> r | c) es

interpProp : String
          -> List (InterpRes TyTRAIT)
          -> InterpRes TyPROPERTY
interpProp s ts = IProp pelem (snd elems)
  where
    pelem : GLang ELEM
    pelem = mkTask ("Property: " ++ s)

    newTS : List (GLang ELEM, List (GLang INTENT))
    newTS = map (\(ITrait x ys) => (x, ys)) ts

    newCS : GLang STRUCT
    newCS = (pelem &= map fst newTS)

    newIS : (is ** DList GTy GLang is)
    newIS = fromList $ concat $ map snd newTS

    newES : (es ** DList GTy GLang es)
    newES = fromList $ map fst newTS

    elems : (fs ** DList GTy GLang fs)
    elems =  (_ ** [pelem]
                ++ snd newES
                ++ snd newIS
                ++ [newCS])

interpSolt : String
          -> List (InterpRes TyPROPERTY)
          -> InterpRes TySOLUTION
interpSolt s ps = ISolt root (snd elems)
  where
    root : GLang ELEM
    root = mkTask ("Solution: " ++ s)

    cs : GLang STRUCT
    cs = (root &= map (\(IProp x ys) => x) ps)

    doGet : InterpRes TyPROPERTY
         -> (is ** DList GTy GLang is)
         -> (xs ** DList GTy GLang xs)
    doGet (IProp x ys) (is ** res) = (_ ** ys ++ res)

    getDecls : (as ** DList GTy GLang as)
    getDecls = foldr (\e,res => doGet e res) (_ ** DList.Nil)  ps

    elems : (es ** DList GTy GLang es)
    elems = (_ ** [root, cs] ++ (snd getDecls))

interpPatt : InterpRes TyPROBLEM
          -> InterpRes TySOLUTION
          -> InterpRes TyPATTERN
interpPatt (IProb rP m) (ISolt rS is) = IPatt (insertDecls is m)

-- --------------------------------------------------------------- [ Filtering ]

getGNodes : List GoalNode -> List GoalNode
getGNodes = filter (\x => getNodeTy x == GOALty)

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

max_stars_repo_name: jfdm/sif-lang

max_issues_repo_name: jfdm/sif-lang

max_forks_repo_name: jfdm/sif-lang


text:
module Replica.Core.Types

import Data.String
import Data.List
import Data.List1
import Language.JSON
import System.Clock

%default total

public export
data OrderSensitive = Ordered | Whatever

export
Show OrderSensitive where
  show Ordered = "Ordered"
  show Whatever = "Whatever"

public export
data Part = StdOut | StdErr | FileName String

export
Show Part where
  show StdOut = "StdOut"
  show StdErr = "StdErr"
  show (FileName x) = "(File \{x})"

public export
data Expectation
   = Exact String
   | StartsWith String
   | EndsWith String
   | Partial OrderSensitive (List String)
   | Generated

public export
ExpectationError : Expectation -> Type
ExpectationError Generated = Maybe String
ExpectationError (Partial Ordered xs) = String
ExpectationError (Partial Whatever xs) = List1 String
ExpectationError x = Unit

export
Show Expectation where
  show (Exact x) = "Exact \{show x}"
  show (StartsWith x) = "StartsWith x"
  show (EndsWith x) = "EndsWith \{show x}"
  show (Partial x xs) = "Partial \{show x} \{show xs}"
  show Generated = "Generated"

public export
record Test where
  constructor MkTest
  name: String
  pending : Bool
  description: Maybe String
  require : List String
  workingDir : Maybe String
  tags: List String
  suite : Maybe String
  beforeTest : List String
  afterTest : List String
  command: String
  input : Maybe String
  status : Maybe (Either Bool Nat)
  spaceSensitive : Bool
  stdOut : List Expectation
  stdErr : List Expectation
  files : List (String, List Expectation)

export
(.expectations) : Test -> List (Part, List Expectation)
(.expectations) t = (StdOut, t.stdOut) :: (StdErr, t.stdErr) :: (mapFst FileName <$> t.files)

export
Show Test where
  show x = unwords
    [ "MkTest"
    , show x.name
    , show x.pending
    , show x.description
    , show x.require
    , show x.workingDir
    , show x.tags
    , show x.beforeTest
    , show x.afterTest
    , show x.command
    , show x.input
    , show x.status
    , show x.spaceSensitive
    , show x.stdOut
    , show x.stdErr
    , show x.files
    ]

export
defaultExpectedOutput : String
defaultExpectedOutput = "expected"

export
defaultExpectedError : String
defaultExpectedError = "expected.err"

export
defaultFile : String
defaultFile = "file"

export
defaultError : String
defaultError = "error"

export
defaultOutput : String
defaultOutput = "output"

export
defaultInput : String
defaultInput = "input"

export
defaultStatus : String
defaultStatus = "status"

public export
record Replica where
  constructor MkReplica
  tests: List Test

public export
data FailReason : Type where
  WrongStatus : (status : Nat) -> (expected : Either Bool Nat) -> FailReason
  WrongOutput : Part -> String -> List1 (e : Expectation **  ExpectationError e) -> FailReason
  ExpectedFileNotFound : String -> FailReason

export
isNoGolden : FailReason -> Bool
isNoGolden (WrongOutput source given xs) = hasGolden $ forget xs
  where
    hasGolden : List (e : Expectation ** ExpectationError e) -> Bool
    hasGolden [] = False
    hasGolden ((Generated ** Nothing) :: _) = True
    hasGolden (_ :: xs) = hasGolden xs
isNoGolden _ = False

export
isMismatch : FailReason -> Bool
isMismatch (WrongOutput source given xs) = hasMismatch $ forget xs
  where
    hasMismatch : List (e : Expectation ** ExpectationError e) -> Bool
    hasMismatch [] = False
    hasMismatch ((Generated ** Nothing) :: xs) = hasMismatch xs
    hasMismatch (_ :: xs) = True
isMismatch _ = False

export
displaySource : Part -> String
displaySource StdOut = "standard output"
displaySource StdErr = "standard error"
displaySource (FileName x) = "file \{show x}"

export
Eq Part where
  (==) StdOut StdOut = True
  (==) StdErr StdErr = True
  (==) (FileName x) (FileName y) = x == y
  (==) _ _ = False

export
displayFailReason : FailReason -> List String
displayFailReason (WrongStatus x (Left True)) = pure "[Fails while it should pass : \{show x}]"
displayFailReason (WrongStatus _ (Left False)) = pure "[Pass but it should fail]"
displayFailReason (WrongStatus x (Right y)) = pure "[Status error: got \{show x}, expected \{show y}]"
displayFailReason (ExpectedFileNotFound src) = pure "[Missing expected file \"\{src}\"]"
displayFailReason w@(WrongOutput src given reasons) = join
  [ guard (isNoGolden w) $> "[Missing Golden for \{displaySource src}]"
  , guard (isNoGolden w) $> "[Unexpected content for \{displaySource src}]"
  ]

namespace FailReason

  encodePart : Part -> (String, JSON)
  encodePart StdOut = ("source", JString "stdout")
  encodePart StdErr = ("source", JString "stderr")
  encodePart (FileName x) = ("source", JObject [("file", JString x)])

  encodeFailure : (e : Expectation ** ExpectationError e) -> List (String, JSON)
  encodeFailure (MkDPair (Exact x) ()) = [("exact", JString x)]
  encodeFailure (MkDPair (StartsWith x) ()) = [("start", JString x)]
  encodeFailure (MkDPair (EndsWith x) ()) = [("end", JString x)]
  encodeFailure (MkDPair (Partial Ordered xs) snd) =
    [("consecutive", JArray $ JString <$> xs), ("notFound", JString snd)]
  encodeFailure (MkDPair (Partial Whatever xs) snd) =
    [("contains", JArray $ JString <$> xs), ("notFound", JArray $ forget $ JString <$> snd)]
  encodeFailure (MkDPair Generated Nothing) = [("generated", JNull)]
  encodeFailure (MkDPair Generated (Just x)) = [("generated", JString x)]

  export
  toJSON : FailReason -> JSON
  toJSON (WrongStatus x y) = JObject
    [("type", JString "status"), ("expected", either JBoolean (JNumber . cast) y), ("given", JNumber $ cast x)]
  toJSON (ExpectedFileNotFound src) = JObject
    [("type", JString "missing"), ("expected", JString src)]
  toJSON (WrongOutput src given err) = JObject $
    encodePart src :: ("type", JString "output") :: ("given", JString given) ::
    [("errors", JArray $ map (JObject . encodeFailure) $ forget err)]

public export
data TestResult
  = Success (Clock Duration)
  | Fail (List FailReason)
  | Skipped

namespace TestResult

  export
  toJSON : TestResult -> JSON
  toJSON (Success d) = JObject [("Success", JString $ show d)]
  toJSON (Fail xs) = JObject [("Fail", JArray $ map toJSON xs)]
  toJSON Skipped = JString "Skipped"

  export
  isSuccess : TestResult -> Bool
  isSuccess (Success _) = True
  isSuccess _ = False

public export
data TestError
  = FileSystemError String
  | InitializationFailed String
  | WrapUpFailed TestResult String
  | RequirementsFailed String
  | Inaccessible

namespace TestError

  export
  toJSON : TestError -> JSON
  toJSON (FileSystemError x) =
    JObject [("type", JString "FileSystemError") , ("content", JString x)]
  toJSON (InitializationFailed x) =
    JObject [("type", JString "InitializationFailed") , ("content", JString x)]
  toJSON (WrapUpFailed x y) =
    JObject [("type", JString "WrapUpFailed"),  ("result", toJSON x), ("content", JString y)]
  toJSON (RequirementsFailed x) =
    JObject [("type", JString "RequirementsFailed"), ("content", JString x)]
  toJSON Inaccessible =
    JObject [("type", JString "Inaccessible")]

export
displayTestError : TestError -> String
displayTestError (FileSystemError x) = "File error: \{x}"
displayTestError (InitializationFailed x) = "Before test action failed: \{x}"
displayTestError (WrapUpFailed x y) =  "After test action failed: \{y}"
displayTestError (RequirementsFailed x) = "Test rely on test \{x}, which failed"
displayTestError Inaccessible = "Test rely on other tests that weren't run"

export
isFullSuccess : Either TestError TestResult -> Bool
isFullSuccess (Right (Success _)) = True
isFullSuccess _ = False

public export
record Stats where
  constructor MkStats
  successes : Nat
  failures  : Nat
  errors    : Nat
  skipped   : Nat

export
Semigroup Stats where
  (<+>) x y = MkStats
    (x.successes + y.successes)
    (x.failures + y.failures)
    (x.errors + y.errors)
    (x.skipped + y.skipped)

export
Monoid Stats where
  neutral = MkStats 0 0 0 0

export
asStats : List (Either TestError TestResult) -> Stats
asStats = foldMap go
  where
    go : Either TestError TestResult -> Stats
    go (Left x) = record {errors = 1} neutral
    go (Right (Success _)) = record {successes = 1} neutral
    go (Right (Fail xs)) = record {failures = 1} neutral
    go (Right Skipped) = record {skipped = 1} neutral

export
countTests : Stats -> Nat
countTests x = x.successes + x.failures + x.errors + x.skipped

export
resultToJSON : Either TestError TestResult -> JSON
resultToJSON (Left x) = JObject [("Error", toJSON x)]
resultToJSON (Right x) = toJSON x

export
reportToJSON : List (String, Either TestError TestResult) -> JSON
reportToJSON = JObject . map (map resultToJSON)

max_stars_repo_name: claymager/REPLica

max_issues_repo_name: claymager/REPLica

max_forks_repo_name: claymager/REPLica


text:
{- Ctrl-Alt-A: Add definition
   Ctrl-Alt-C: Case split
   Ctrl-Alt-D: Documentation
   Ctrl-Alt-L: Lift hole: Lifts a hole to the top level as a new function definition
   Ctrl-Alt-M: Match: Replaces a hole with a case expression that matches on an intermediate result
   Ctrl-Alt-R: Reloads and typechecks the current buffer
   Ctrl-Alt-S: Search
   Ctrl-Alt-T: Type-check: Displays the type under cursor
   Ctrl-Alt-W: Add With View -}
module Main

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

{-
O(n) in time: because we travel the lists twice
O(n) in space: because we build a helper SnocList structures.
-}
total
equalSuffix : Eq a => List a -> List a -> List a
equalSuffix input1 input2 with (snocList input1)
  equalSuffix [] input2 | Empty = []
  equalSuffix (xs ++ [x]) input2 | (Snoc xsrec) with (snocList input2)
    equalSuffix (xs ++ [x]) [] | (Snoc xsrec) | Empty = []
    equalSuffix (xs ++ [x]) (ys ++ [y]) | (Snoc xsrec) | (Snoc ysrec) =
      case x == y of
        True => (equalSuffix xs ys | xsrec | ysrec) ++ [x]
        False => []

total
mergeSort : (Ord a) => Vect n a -> Vect n a
mergeSort xs with (splitRec xs)
  mergeSort [] | SplitRecNil = []
  mergeSort [x] | SplitRecOne = [x]
  mergeSort (ys ++ zs) | (SplitRecPair lrec rrec) =
    merge (mergeSort ys | lrec) (mergeSort zs | rrec)

total
toBinary : Nat -> String
toBinary n with (halfRec n)
  toBinary Z | HalfRecZ = ""
  toBinary (x + x) | (HalfRecEven rec) = (toBinary x | rec) ++ "0"
  toBinary (S (x + x)) | (HalfRecOdd rec) = (toBinary x | rec) ++ "1"

total
palindrome : List Char -> Bool
palindrome xs with (vList xs)
  palindrome [] | VNil = True
  palindrome [x] | VOne = True
  palindrome (x :: (ys ++ [y])) | (VCons rec) =
    case x == y of
      False => False
      True => palindrome ys | rec

main : IO ()
main = do
  printLn $ equalSuffix [] [1] -- []
  printLn $ equalSuffix [1,2,4,5] [1..5] -- [4,5]
  printLn $ equalSuffix [1,2,4,5,6] [1..5] -- []
  printLn $ equalSuffix [1,2,4,5,6] [1..6] -- [4,5,6]
  printLn $ mergeSort [1,2,3,8,4,3,6,7,9,7]
  putStrLn $ toBinary 42 -- "101010"
  putStrLn $ toBinary 94 -- "1011110"
  printLn $ palindrome (unpack "abccba") -- True
  printLn $ palindrome (unpack "abcba") -- True
  printLn $ palindrome (unpack "abcb") -- False

max_stars_repo_name: pdani/idris-grin

max_issues_repo_name: pdani/idris-grin

max_forks_repo_name: pdani/idris-grin


text:
module Main

import CFFI

%dynamic "/usr/local/opt/libpq/lib/libpq.dylib"
%include C  "/usr/local/opt/libpq/include/libpq-fe.h"
%lib C "pq"

pqConnectDb : String -> IO Ptr
pqConnectDb s
    = foreign FFI_C "PQconnectdb" (String -> IO Ptr) s

pqErrorMessage : String -> IO String
pqErrorMessage s
    = foreign FFI_C "PQerrorMessage" (String -> IO String) s

pqFinish : Ptr -> IO ()
pqFinish p
    = foreign FFI_C "PQfinish" (Ptr -> IO ()) p

pqStatus : Ptr -> IO Int
pqStatus p
    = foreign FFI_C "PQstatus" (Ptr -> IO Int) p

export data ConnectionStatus
    = OK
    | BAD
    | STARTED
    | MADE
    | AWAITING_RESPONSE
    | AUTH_OK
    | SETENV
    | SSL_STARTUP
    | NEEDED
    | OTHER Int

mkConnectionStatus: Int -> ConnectionStatus
mkConnectionStatus i
    = case i of
        0 => OK
        1 => BAD
        2 => STARTED
        3 => MADE
        4 => AWAITING_RESPONSE
        5 => AUTH_OK
        6 => SETENV
        7 => SSL_STARTUP
        8 => NEEDED
        _ => OTHER i

Show ConnectionStatus where
    show x = case x of
        OK => "OK"
        BAD => "BAD"
        STARTED => "STARTED"
        MADE => "MADE"
        AWAITING_RESPONSE => "AWAITING_RESPONSE"
        AUTH_OK => "AUTH_OK"
        SETENV => "SETENV"
        SSL_STARTUP => "SSL_STARTUP"
        NEEDED => "NEEDED"
        OTHER i => "OTHER " ++ show i

main : IO ()
main = do
    putStrLn "connecting to db"
    let connection = "host=localhost port=5432 dbname=idris user=idris"
    p <- pqConnectDb connection
    status <- pqStatus p
    putStr "connection status: "
    let statusMsg = mkConnectionStatus status
    putStrLn $ show statusMsg
    pqFinish p
    putStrLn "exiting"

max_stars_repo_name: cpritcha/Idris-libpq

max_issues_repo_name: cpritcha/Idris-libpq

max_forks_repo_name: cpritcha/Idris-libpq


text:
import Data.Bits
import Data.DPair
import Data.Nat
import Data.So

namespace SubsetNat

  public export
  fromInteger : (x : Integer) ->
                {0 n : Nat} ->
                {auto 0 prf : fromInteger x `LT` n} ->
                Subset Nat (`LT` n)
  fromInteger x = Element (integerToNat x) prf

f : Int -> Int
f x = shiftR x 1

max_stars_repo_name: buzden/idris-playground

max_issues_repo_name: buzden/idris-playground

max_forks_repo_name: buzden/idris-playground


text:
plus_commutes : (n, m : Nat) -> plus n m = plus m n
plus_assoc : (n, m, p : Nat) -> plus n (plus m p) = plus (plus n m) p


text:
module Queries

import SQLiteTypes
import Schema
import Database

import Decidable.Equality
import Language.Reflection
import Language.Reflection.Errors
import Language.Reflection.Utils

%access public export
%default total
%language ErrorReflection

namespace Row0
  data Row : Schema -> Type where
    Nil : Row []
    (::) : (x : interpSql t) -> (xs : Row s) -> Row ((c:::t) :: s)
  %name Row r1,r2,r3

  getSchema : Row s -> Schema
  getSchema {s} _ = s

  getCol : HasCol s attr -> Row s -> interpSql (getTy attr)
  getCol Here (x :: xs) = x
  getCol (There at) (y :: xs) = getCol at xs

  projectRow : (SubSchema s1 s2) -> Row s2 -> Row s1
  projectRow Empty r1 = []
  projectRow {s1=(attr::small)} (Head tailSub alsoThere) r ?= {projectRow_lemma}
     let head = getCol alsoThere r in
     let tail = projectRow tailSub r in
     the (Row ((getName attr ::: getTy attr)::small)) (head::tail)

  showRow : (s : Schema) -> Row s -> String
  showRow []               []  = "\n"
  showRow ((_ ::: t) :: s) (x :: xs) = showSql t x ++ "|" ++ showRow s xs

namespace Table
  data Table : Schema -> Type where
    Nil : Table s
    (::) : (r : Row s) -> (rs : Table s) -> Table s

  showTable' : (s : Schema) -> Table s -> String
  showTable' s [] = ""
  showTable' s (r :: rs) = showRow s r ++ showTable' s rs

  showHeader : Schema -> String
  showHeader [] = "\n"
  showHeader ((col ::: _) :: s) = col ++ "|" ++ showHeader s

  showTable : (s : Schema) -> Table s -> String
  showTable s t = showHeader s ++ showTable' s t

namespace Expr

  data Expr : Schema -> SQLiteType -> Type where
    Col : (c : String) -> {t : SQLiteType} ->
          {auto ok : HasCol s (c:::t)} ->
          Expr s t
    (==) : Expr s t -> Expr s t -> Expr s INTEGER
    (>) : Expr s INTEGER -> Expr s INTEGER -> Expr s INTEGER
    (<) : Expr s INTEGER -> Expr s INTEGER -> Expr s INTEGER
    (>=) : Expr s INTEGER -> Expr s INTEGER -> Expr s INTEGER
    (<=) : Expr s INTEGER -> Expr s INTEGER -> Expr s INTEGER
    Length : Expr s TEXT -> Expr s INTEGER
    Not : Expr s INTEGER -> Expr s INTEGER
    CstI : Integer -> Expr s INTEGER

  compileOp : String -> String -> String -> String
  compileOp op x y = "(" ++ x ++ ") " ++ op ++ " (" ++ y ++ ")"

  compileExpr : Expr s t -> String
  compileExpr (Col c) = "`" ++ c ++ "`"
  compileExpr (x == y) = compileOp "==" (compileExpr x) (compileExpr y)
  compileExpr (x > y) = compileOp ">" (compileExpr x) (compileExpr y)
  compileExpr (x < y) = compileOp "<" (compileExpr x) (compileExpr y)
  compileExpr (x >= y) = compileOp ">=" (compileExpr x) (compileExpr y)
  compileExpr (x <= y) = compileOp "<=" (compileExpr x) (compileExpr y)
  compileExpr (Length x) = "LENGTH(" ++ compileExpr x ++ ")"
  compileExpr (Not x) = "NOT(" ++ compileExpr x ++ ")"
  compileExpr (CstI i) = show i

  fromInteger : Integer -> Expr s INTEGER
  fromInteger = CstI

namespace Query
  %reflection
  reflectListPrf : List a -> Tactic
  reflectListPrf [] = Refine (UN "Here") `Seq` Solve
  reflectListPrf (x :: xs)
       = Try (Refine (UN "Here") `Seq` Solve)
             (Refine (UN "There") `Seq` (Solve `Seq` reflectListPrf xs))
  -- TMP HACK! FIXME!
  -- The evaluator needs a 'function case' to know its a reflection function
  -- until we propagate that information! Without this, the _ case won't get
  -- matched.
  --reflectListPrf (x ++ y) = Refine "Here" `Seq` Solve
  reflectListPrf _ = Refine (UN "Here") `Seq` Solve

  %reflection
  solveHasTable : Type -> Tactic
  solveHasTable (HasTable ts n s) = reflectListPrf ts `Seq` Solve
  solveHasTable (HasTable (x ++ y) n s) = Solve

  data Tables : DB file -> Schema -> Type where
    T : (name : String) ->
        {default tactics { byReflection solveHasTable; }
         ok : HasTable db name s} ->
        Tables (MkDB file db) s
    (*) : (t1 : String) ->
          {auto
           ok : HasTable db t1 s1} ->
          Tables (MkDB file db) s2 ->
          {auto disj : isDisjoint s1 s2 = Disjoint} ->
          Tables (MkDB file db) (append s1 s2)

  implicit
  toTables : (tbl : String) ->
             {auto
              ok : HasTable db tbl s} ->
             Tables (MkDB name db) s
  toTables tbl {ok = ok} = T tbl {ok = ok}

  compileTables : {db : DB f} -> Tables db s -> String
  compileTables (T n) = n
  compileTables (x * y) = x ++ ", " ++ compileTables y

  data Cmd : DB f -> Type where
    Insert : (into : String) -> (s : Schema) ->
             {default tactics { byReflection solveHasTable; }
              ok : HasTable db into s} ->
             (values : Table s) ->
             Cmd (MkDB f db)
    Delete : (from : String) -> (s : Schema) ->
             {default tactics { byReflection solveHasTable; }
              ok : HasTable db from s} ->
             (when : Expr s INTEGER) ->
             Cmd (MkDB f db)

  syntax INSERT INTO [table] AS [schema] VALUES [values] = Insert table schema values
  syntax DELETE FROM [table] AS [schema] WHEN [when] = Delete table schema when

  data Query : DB f -> Schema -> Type where
    Select : {db : DB f} -> Tables db s -> Expr s INTEGER -> (s' : Schema) ->
             {auto ok : SubSchema s' s} ->
             Query db s'

  syntax SELECT [schema] FROM [tables] WHERE [expr] = Select tables expr schema

  compileQuery : {db : DB f} -> Query db proj -> String
  compileQuery (Select ts expr proj) = "SELECT " ++
                                       cols ++
                                       " FROM " ++
                                       compileTables ts ++
                                       " WHERE " ++
                                       compileExpr expr ++
                                       ";"
    where cols : String
          cols = Foldable.concat . List.intersperse ", " . colNames $ proj

---------- Proofs ----------

Queries.Row0.projectRow_lemma = proof
  intros
  rewrite (attrEta attr)
  exact value

max_stars_repo_name: ethansr/IdrisSqlite

max_issues_repo_name: ethansr/IdrisSqlite

max_forks_repo_name: ethansr/IdrisSqlite


text:
module Program

import CommonTestingStuff

export
beforeString : String
beforeString = "before coop"

long : PrintString m => CanSleep m => Zippable m => (offset : Time) -> m String
long offset = do
  printTime offset "long proc, first"
  for 5 $ do
    printTime offset "long proc, before 1000"
    sleepFor 1.seconds
    printTime offset "long proc, before 2000"
    sleepFor 2.seconds
  "long" <$ printTime offset "long proc, last"

short : PrintString m => CanSleep m => Zippable m => (offset : Time) -> m String
short offset = do
  printTime offset "                       short proc, first"
  for 5 $ do
    printTime offset "                       short proc, before 350"
    sleepFor 350.millis
    printTime offset "                       short proc, before 750"
    sleepFor 750.millis
  "short" <$ printTime offset "                       short proc, last"

export
program : PrintString m => CanSleep m => Zippable m => Alternative m => m Unit
program = do
  offset <- currentTime
  printTime offset "start"

  res <- long offset <|> short offset
  printTime offset "top: \{res}"

  sleepFor 1.seconds
  printTime offset "------"

  res <- short offset <|> long offset
  printTime offset "top: \{res}"

  printTime offset "end"


text:
module WebAssembly.Validation.Modules.Imports

import WebAssembly.Structure
import WebAssembly.Validation.Conventions
import WebAssembly.Validation.Types

||| [🔗 Spec](https://webassembly.github.io/spec/core/valid/modules.html#imports)
public export
data ValidImportDesc : Context -> ImportDesc -> ExternType -> Type where

  ||| [🔗 Spec](https://webassembly.github.io/spec/core/valid/modules.html#xref-syntax-modules-syntax-importdesc-mathsf-func-x)
  |||
  ||| ```
  ||| C.types[x] = [t1*] -> [t2*]
  ||| --------------------------------
  ||| C ⊢ func x : func [t1*] -> [t2*]
  ||| ```
  ValidImportFunc  : (c : Context)
                  -> (x : TypeIdx)
                  -> {auto in_bounds: InBounds x (types c)}
                  -> ValidImportDesc c (FuncImport x) (Func (index x (types c)))

  ||| [🔗 Spec](https://webassembly.github.io/spec/core/valid/modules.html#xref-syntax-modules-syntax-importdesc-mathsf-table-xref-syntax-types-syntax-tabletype-mathit-tabletype)
  |||
  ||| ```
  ||| tabletype ok
  ||| -------------------------------------
  ||| C ⊢ table tabletype : table tabletype
  ||| ```
  MkValidImportTable : (c : Context)
                    -> (tabletype : TableType)
                    -> ValidTableType tabletype
                    -> ValidImportDesc c (TableImport tabletype) (Table tabletype)

  ||| [🔗 Spec](https://webassembly.github.io/spec/core/valid/modules.html#xref-syntax-modules-syntax-importdesc-mathsf-mem-xref-syntax-types-syntax-memtype-mathit-memtype)
  |||
  ||| ```
  ||| memtype ok
  ||| -----------------------------
  ||| C ⊢ mem memtype : mem memtype
  ||| ```
  MkValidImportMem : (c : Context)
                  -> (memtype : MemType)
                  -> ValidMemoryType memtype
                  -> ValidImportDesc c (MemImport memtype) (Mem memtype)

  ||| [🔗 Spec](https://webassembly.github.io/spec/core/valid/modules.html#xref-syntax-modules-syntax-importdesc-mathsf-global-xref-syntax-types-syntax-globaltype-mathit-globaltype)
  |||
  ||| ```
  ||| globaltype ok
  ||| -----------------------------
  ||| C ⊢ global globaltype : global globaltype
  ||| ```
  MkValidImportGlobal  : (c : Context)
                      -> (globaltype : GlobalType)
                      -> ValidGlobalType globaltype
                      -> ValidImportDesc c (GlobalImport globaltype) (Global globaltype)

||| [🔗 Spec](https://webassembly.github.io/spec/core/valid/modules.html#imports)
public export
data ValidImport : Context -> Import -> ExternType -> Type where
  ||| [🔗 Spec](https://webassembly.github.io/spec/core/valid/modules.html#xref-syntax-modules-syntax-import-mathsf-module-xref-syntax-values-syntax-name-mathit-name-1-xref-syntax-modules-syntax-import-mathsf-name-xref-syntax-values-syntax-name-mathit-name-2-xref-syntax-modules-syntax-import-mathsf-desc-xref-syntax-modules-syntax-importdesc-mathit-importdesc)
  |||
  ||| ```
  ||| C ⊢ importdesc : externtype
  ||| ------------------------------------------------------------
  ||| C ⊢ {module name1, name name2, desc importdesc} : externtype
  ||| ```
  MkValidImport  : (c : Context)
                -> (name1 : Name)
                -> (name2 : Name)
                -> (importdesc : ImportDesc)
                -> (externtype : ExternType)
                -> ValidImportDesc c importdesc externtype
                -> ValidImport c (MkImport name1 name2 importdesc) externtype

max_stars_repo_name: RaoulSchaffranek/idris-webassembly

max_issues_repo_name: RaoulSchaffranek/idris-webassembly

max_forks_repo_name: RaoulSchaffranek/idris-webassembly


text:
module Invincy.Invertible

import Invincy.Core
import Invincy.Parsing
import Invincy.Printing

%access public export

(<$>) : (Functor f, Contravariant g) => ((a -> b), (b -> a)) -> (f a, g a) -> (f b, g b)
(<$>) (f', c') (f, c) = (map f' f, contramap c' c)

(<*>) : (Applicative f, Divisible g) => (f a, g a) -> (f b, g b) -> (f (a, b), g (a, b))
(<*>) (fa, ga) (fb, gb) = (MkPair <$> fa <*> fb, divided ga gb)

(<*) : (Applicative f, Divisible g) => (f a, g a) -> (f b, g ()) -> (f a, g a)
(<*) (fa, ga) (fb, gb) = (fa <* fb, ga <* gb)

(*>) : (Applicative f, Divisible g) => (f a, g ()) -> (f b, g b) -> (f b, g b)
(*>) (fa, ga) (fb, gb) = (fa *> fb, ga *> gb)

(<|>) : LazyAlternative f => {g: Type -> Type} -> (f a, g a) -> Lazy (f a) -> (f a, g a)
(<|>) (fa, ga) fb = (fa <|> fb, ga)

either' : (Functor f, LazyAlternative f, Decidable g) =>
  (f a, g a) -> (f b, g b) -> (f (Either a b), g (Either a b))
either' (fa, ga) (fb, gb) = (map Left fa <|> map Right fb, chosen ga gb)

choice' : (Functor f, LazyAlternative f, Decidable g) =>
  (a -> Either a a) -> (f a, g a) -> Lazy (f a, g a) -> (f a, g a)
choice' e (fa, ga) b = (fa <|> fst b, choose e ga (snd b))

||| Parser and printer
PP : Type -> Type -> Type
PP a b = (Parser a b, Printer a b)

data LazyList : Type -> Type where
  Nil : LazyList a
  (::) : a -> Lazy (LazyList a) -> LazyList a

||| Generates choices
||| @t data type
||| @e enumeration of constructors
||| @f provides constructor arguments
||| @c constructor
||| @d destructor
||| @l "enumerated" printers/parsers
choices' : (DecEq e, Stream t' s)
   => {f: e -> Type}
   -> (c: (x: e) -> f x -> t)
   -> (d: t -> (x: e ** f x))
   -> (l: LazyList (x:e ** PP s (f x)))
   -> PP s t
choices' dtc dte [] = (fail "Out of alternatives", MkPrinter $ const neutral)
choices' dtc dte ((v ** p)::xs) =
  choice' (\val => let (v' ** p') = dte val in (case decEq v' v of Yes _ => Left; No _ => Right) val)
    ((dtc v, (\val => let (v' ** p') = dte val in (case decEq v' v of Yes eq => replace eq p'))) <$> p)
    (choices' dtc dte xs)

choices : (DecEq e, Stream t' s)
   => {f: e -> (a ** a -> t)}
   -> (d: t -> (x: e ** getWitness (f x)))
   -> (l: LazyList (x:e ** PP s (getWitness (f x))))
   -> PP s t
choices dte [] = (fail "Out of alternatives", MkPrinter $ const neutral)
choices {f} dte ((v ** p)::xs) =
  choice' (\val => let (v' ** p') = dte val in (case decEq v' v of Yes _ => Left; No _ => Right) val)
    ((getProof (f v),
       (\val => let (v' ** p') = dte val in (case decEq v' v of Yes eq => replace eq p')))
     <$> p)
    (choices dte xs)

print' : PP i a -> a -> i
print' = runPrinter . snd

parse' : PP i a -> i -> Result i a
parse' = runParser . fst

parseWith' : Monad m => PP i r -> m i -> m (Result i r)
parseWith' = parseWith . fst

||| Parse or print a single item
item' : PP (List a) a
item' = (item, itemP)

||| Parse an item satisfying a predicate, or put any item
sat' : (a -> Bool) -> PP (List a) a
sat' p = (sat p, itemP)

||| Ignore an item on parsing, use a fixed one on printing
ignore' : Stream t s => Parser s a -> s -> PP s ()
ignore' p x = (ignore p, ignoreP x)

||| Parse or print a fixed item
val' : (Eq t, Stream t s) => t -> PP s ()
val' x = (val x, valP x)

||| Just as val, but for multiple tokens
raw' : (Eq t, Stream t s) => s -> PP s ()
raw' l = (raw l, ignoreP l)

||| An optional item
||| @a What to print in case if the value is Nothing
option' : Stream t s => a -> PP s a -> PP s (Maybe a)
option' x (par, pr) = (option par, optionP x pr)

many' : Stream t s => PP s a -> PP s (List a)
many' (par, pr) = (many par, manyP pr)

manyTill' : Stream t s => PP s a -> PP s () -> PP s (List a)
manyTill' (par, pr) (par', pr') = (manyTill par par', manyTillP pr pr')

some' : Stream t s => PP s a -> PP s (x:List a ** NonEmpty x)
some' (par, pr) = (some par, someP pr)

sepBy' : Stream t s => PP s a -> PP s () -> PP s (List a)
sepBy' (par, pr) (par', pr') = (sepBy par par', sepByP pr pr')

sepBy1' : Stream t s => PP s a -> PP s () -> PP s (x:List a ** NonEmpty x)
sepBy1' (par, pr) (par', pr') = (sepBy1 par par', sepBy1P pr pr')

integer' : PP (List Char) Integer
-- would be better to use `some'` here, but it'd require to cast
-- integers into non-empty lists, which is not in the library
integer' = (cast . pack, unpack . cast) <$> many' (digit, itemP)

spaces' : Stream Char s => PP s ()
spaces' = ignore' (many (oneOf [' ', '\n', '\t', '\r'])) (single ' ')

max_stars_repo_name: defanor/invincy

max_issues_repo_name: defanor/invincy

max_forks_repo_name: defanor/invincy


text:
module Crypto.Hash.SHA1

import Crypto.Hash.Interfaces
import Data.Bits
import Data.DPair
import Data.Fin
import Data.Fin.Extra
import Data.List
import Data.Nat
import Data.Nat.Factor
import Data.Vect
import Utils.Misc
import Utils.Bytes
import Data.Stream
import Crypto.Hash.MerkleDamgard

export
data Sha1 : Type where
  MkSha1 : MerkleDamgard 5 64 Bits32 -> Sha1

sha1_init_hash_values : Vect 5 Bits32
sha1_init_hash_values =
  [ 0x67452301, 0xEFCDAB89, 0x98BADCFE, 0x10325476, 0xC3D2E1F0 ]

sha1_extend_message : Vect 16 Bits32 -> Stream Bits32
sha1_extend_message xs = prepend (toList xs) $ go xs
  where
  go : Vect 16 Bits32 -> Stream Bits32
  go xs =
    let
      [wi_16, wi_14, wi_8, wi_3] = the (Vect 4 _) $ map (flip index xs) [0, 2, 8, 13]
      w = rotl 1 (wi_16 `xor` wi_14 `xor` wi_8 `xor` wi_3)
    in
      w :: go (tail xs `snoc` w)

sha1_compress : (block : Vect 64 Bits8) -> (h : Vect 5 Bits32) -> Vect 5 Bits32
sha1_compress block hash_values = zipWith (+) hash_values $ go Z (sha1_extend_message $ map (from_be {a = Bits32} {n = 4}) $ group 16 4 block) hash_values
  where
  loop : Bits32 -> Bits32 -> Bits32 -> Bits32 -> Bits32 -> Bits32 -> Bits32 -> Bits32 -> Vect 5 Bits32
  loop f k wi a b c d e =
    let temp = (rotl 5 a) + f + e + k + wi
        e = d
        d = c
        c = rotl 30 b
        b = a
        a = temp
    in [a, b, c, d, e]
  go :  Nat -> Stream Bits32 -> Vect 5 Bits32 -> Vect 5 Bits32
  go n (wi :: ws) abc@[a, b, c, d, e] =
    case n `div` 20 of
      0 => go (S n) ws $ loop ((b .&. c) .|. ((complement b) .&. d))  0x5A827999 wi a b c d e
      1 => go (S n) ws $ loop (b `xor` c `xor` d)                     0x6ED9EBA1 wi a b c d e
      2 => go (S n) ws $ loop ((b .&. c) .|. (b .&. d) .|. (c .&. d)) 0x8F1BBCDC wi a b c d e
      3 => go (S n) ws $ loop (b `xor` c `xor` d)                     0xCA62C1D6 wi a b c d e
      _ => abc

sha1_update : List Bits8 -> Sha1 -> Sha1
sha1_update input (MkSha1 s) =
  let
    Fraction _ 64 nblocks residue_nbyte prf = divMod (s.buffer_nbyte + length input) 64
    (blocks, residue) = splitAt (mult nblocks 64) (replace_vect (sym prf) (s.buffer ++ fromList input))
  in
    MkSha1 $ {buffer := residue, buffer_nbyte := _, buffer_nbyte_constraint := elemSmallerThanBound residue_nbyte }
      ( foldl (\s_, block_ => {hash_values $= sha1_compress block_, npassed_blocks $= S} s_) s (group nblocks 64 blocks) )

sha1_finalize : Sha1 -> Vect 20 Bits8
sha1_finalize (MkSha1 s) =
  concat $ map (to_be {n = 4}) $
    case pad_theorem {block_nbyte = 64} {residue_max_nbyte = 55} {length_nbyte = 8} (LTESucc LTEZero) Refl s.buffer_nbyte_constraint s.buffer (integer_to_be _ $ 8 * (cast s.npassed_blocks * 64 + cast s.buffer_nbyte)) of
      Left block => sha1_compress block s.hash_values
      Right blocks => let (x1, x2) = splitAt 64 blocks in sha1_compress x2 $ sha1_compress x1 s.hash_values

export
Digest Sha1 where
  digest_nbyte = 20
  update = sha1_update
  finalize = sha1_finalize

export
Hash Sha1 where
  block_nbyte = 64
  initialize = MkSha1 $ mk_merkle_damgard sha1_init_hash_values


text:
module Control.Monad.Algebra

import Control.Algebra
import Control.Monad.Identity

%default total

public export
SemigroupV ty => SemigroupV (Identity ty) where
  semigroupOpIsAssociative (Id l) (Id c) (Id r) =
    rewrite semigroupOpIsAssociative l c r in Refl

public export
MonoidV ty => MonoidV (Identity ty) where
  monoidNeutralIsNeutralL (Id l) =
    rewrite monoidNeutralIsNeutralL l in Refl
  monoidNeutralIsNeutralR (Id r) =
    rewrite monoidNeutralIsNeutralR r in Refl


text:
module Data.Functor.Of

infixl 0 :>

public export
record Of a b where
  constructor (:>)
  fst : a
  snd : Lazy b

export
Bifunctor Of where
  mapFst f (a :> b) = f a :> b
  mapSnd f (a :> b) = a :> f b
  bimap f g (a :> b) = f a :> g b

export
Functor (Of a) where
  map = mapSnd

export
from_pair : Pair a b -> Of a b
from_pair (a, b) = a :> b

export
to_pair : Of a b -> Pair a b
to_pair (a :> b) = (a, b)


text:
module Transversals

import Group
import GroupCosets
import GroupCosetRep
%access public export

--Proof that the definitional equality for Transversal multiplication holds
MulTransDefPf: (h: Type) -> ((+) : h -> h -> h) -> (pf1: IsGroup h (+)) ->
                (g: Type) -> ((*) : g -> g -> g) -> (pf2: IsGroup g (*)) ->
                (sbgrp: Subgroup h (MkGroup h (+) pf1) g (MkGroup g (*) pf2)) -> (trav: Type) ->
                (pftrav: IsTransversal h (MkGroup h (+) pf1) g (MkGroup g (*) pf2) sbgrp trav) -> (y: trav) -> (z: trav) ->
                (MulTrans trav (MkTransversal h (MkGroup h (+) pf1) g (MkGroup g (*) pf2) sbgrp trav pftrav) y z) =
                  ((DPair.fst (DPair.snd ((Basics.snd (DPair.snd pftrav)) (((DPair.fst pftrav) y)*((DPair.fst pftrav) z))) )))
MulTransDefPf h (+) pf1 g (*) pf2 sbgrp trav pftrav y z = Refl

--Proof that the function from g to trav recovered from CosetAll is in some sense a magma homorphism
MulTransHomPf: (h: Type) -> ((+) : h -> h -> h) -> (pf1: IsGroup h (+)) ->
                (g: Type) -> ((*) : g -> g -> g) -> (pf2: IsGroup g (*)) ->
                (sbgrp: Subgroup h (MkGroup h (+) pf1) g (MkGroup g (*) pf2)) -> (trav: Type) ->
                (pftrav: IsTransversal h (MkGroup h (+) pf1) g (MkGroup g (*) pf2) sbgrp trav) -> (y: trav) -> (z: trav) ->
                ((DPair.fst (DPair.snd ((Basics.snd (DPair.snd pftrav)) (((DPair.fst pftrav) y)*((DPair.fst pftrav) z))) ))) = (MulTrans trav (MkTransversal h (MkGroup h (+) pf1) g (MkGroup g (*) pf2) sbgrp trav pftrav) ((DPair.fst (DPair.snd ((Basics.snd (DPair.snd pftrav)) (((DPair.fst pftrav) y))) ))) ((DPair.fst (DPair.snd ((Basics.snd (DPair.snd pftrav)) (((DPair.fst pftrav) z))) ))))
MulTransHomPf h (+) pf1 g (*) pf2 sbgrp trav pftrav y z = trans (sym (MulTravDefProof)) (trans (cong {f = f1} (sym CorepFInverseY)) (cong {f = f2} (sym CorepFInverseZ))) where

  MulTravDefProof: (MulTrans trav (MkTransversal h (MkGroup h (+) pf1) g (MkGroup g (*) pf2) sbgrp trav pftrav) y z) = ((fst (snd ((snd (snd pftrav)) (((fst pftrav) y)*((fst pftrav) z))) )))
  MulTravDefProof = (MulTransDefPf h (+) pf1 g (*) pf2 sbgrp trav pftrav y z )

  f1: trav -> trav
  f1 x = MulTrans trav (MkTransversal h (MkGroup h (+) pf1) g (MkGroup g (*) pf2) sbgrp trav pftrav) x z

  f2: trav -> trav
  f2 x = MulTrans trav (MkTransversal h (MkGroup h (+) pf1) g (MkGroup g (*) pf2) sbgrp trav pftrav) ((DPair.fst (DPair.snd ((Basics.snd (DPair.snd pftrav)) (((DPair.fst pftrav) y) ) )) )) x

  CorepFInverseY: (((fst (snd ((snd (snd pftrav)) ((fst pftrav) y) ) )) ) = y)
  CorepFInverseY = CorepFinv trav (MkTransversal h (MkGroup h (+) pf1) g (MkGroup g (*) pf2) sbgrp trav pftrav) y

  CorepFInverseZ: (((fst (snd ((snd (snd pftrav)) ((fst pftrav) z) ) )) ) = z)
  CorepFInverseZ = CorepFinv trav (MkTransversal h (MkGroup h (+) pf1) g (MkGroup g (*) pf2) sbgrp trav pftrav) z


text:
module SillyTypes

record Peano where
  constructor MkPeano
  natRep : Nat
  {gt0 : natRep `GT` 0}

data PeanoFin : Peano -> Type where
  MkPeanoFin :
    {lessThanThis : Peano} ->
    (peanoNumber : Peano) ->
    {ltN : (natRep peanoNumber) `LT` (natRep lessThanThis)} ->
    PeanoFin lessThanThis

record NonEmptyString where
  constructor MkNonEmptyString
  strRep : String
  nonEmpty : length strRep `GT` 0

NumPlayers : Type
NumPlayers = Peano

NumDice : Type
NumDice = Peano

NumDieSides : Type
NumDieSides = Peano

max_stars_repo_name: pharpend/dudo

max_issues_repo_name: pharpend/dudo

max_forks_repo_name: pharpend/dudo


text:
module Language.SystemVerilog.Utilities

import Data.List

%default total

export
newName : (xs  : List String)
       -> (prf : NonEmpty xs)
              => String
newName (x::xs) {prf=IsNonEmpty} = concat (intersperse "_" (x::xs))

max_stars_repo_name: border-patrol/lightclick

max_issues_repo_name: border-patrol/lightclick

max_forks_repo_name: border-patrol/lightclick


text:
module GridIO

import Effects
import Effect.File

import Grid

%access public export

LIFE_CHAR : Char
LIFE_CHAR = 'o'

readGrid : Int -> Int -> Eff Grid [FILE R]
readGrid columnN rowN = do
    lines <- mapE (\_ => tryReadLine) [1 .. rowN]
    let numberedLines = zip lines (the (List Int) [0 .. (columnN - 1)])
    pure $ foldl addLine (MkGrid 0 0 columnN rowN empty) numberedLines
  where
    tryReadLine : Eff String [FILE R]
    tryReadLine = do
        Result line <- readLine | FError _ => pure ""
        pure line

    addChar : Int -> Grid -> (Char, Int) -> Grid
    addChar row grid (c, column) =
        if c == 'o'
            then addLife (column, row) grid
            else grid

    addLine : Grid -> (String, Int) -> Grid
    addLine grid (line, row) = foldl (addChar row) grid $ zip (unpack line) (the (List Int) [0 .. (rowN - 1)])

writeGrid : Grid -> Eff () [FILE W]
writeGrid grid = do
    Success <- writeString toString | FError _ => pure ()
    pure ()
  where
    coords : List (List (Int, Int))
    coords = map (\row => map (\column => (column, row)) [0 .. (columnN grid - 1)]) [0 .. (rowN grid - 1)]

    lines : List String
    lines = map (\q => pack (map (\point => if containsLife point grid then 'o' else '.') q)) coords

    toString : String
    toString = unlines lines

max_stars_repo_name: artemohanjanyan/game-of-life

max_issues_repo_name: artemohanjanyan/game-of-life

max_forks_repo_name: artemohanjanyan/game-of-life


text:
readNumber : IO (Maybe Nat)
readNumber = do
  input <- getLine
  if all isDigit (unpack input)
     then pure (Just (cast input))
     else pure Nothing

{-readNumbers : IO (Maybe (Nat, Nat))
readNumbers = do
  num1 <- readNumber
  case num1 of
       Nothing => pure Nothing
       Just num1_ok =>
        do num2 <- readNumber
           case num2 of
                Nothing => pure Nothing
                Just num2_ok => pure (Just (num1_ok, num2_ok))-}

readNumbers : IO (Maybe (Nat, Nat))
readNumbers =
  do Just num1_ok <- readNumber | Nothing => pure Nothing
     Just num2_ok <- readNumber | Nothing => pure Nothing
     pure (Just (num1_ok, num2_ok))

readPair : IO (String, String)
readPair = do str1 <- getLine
              str2 <- getLine
              pure (str1, str2)

{-usePair: IO ()
usePair= do pair <- readPair
                        (case pair of
                              (str1, str2) => putStrLn("You entered" ++
                                             str1 ++ " and " ++ str2))-}

usePair : IO ()
usePair = do (str1, str2) <- readPair
             putStrLn ("You entered " ++ str1 ++ " and " ++ str2)


text:
module Libraries.System.Directory.Tree

import Control.Monad.Either
import Data.Buffer
import Data.DPair
import Data.List
import Data.Nat
import Data.String
import System.Directory
import System.File
import Libraries.Utils.Path

%default total

------------------------------------------------------------------------------
-- Filenames

||| A `Filename root` is anchored in `root`.
||| We use a `data` type so that Idris can easily infer `root` when passing
||| a `FileName` around. We do not use a `record` because we do not want to
||| allow users to manufacture their own `FileName`.
||| To get an absolute path, we need to append said filename to the root.
export
data FileName : Path -> Type where
  MkFileName : String -> FileName root

||| Project the string out of a `FileName`.
export
fileName : FileName root -> String
fileName (MkFileName str) = str

namespace FileName
  export
  toRelative : FileName root -> FileName (parse "")
  toRelative (MkFileName x) = MkFileName x

||| Convert a filename anchored in `root` to a filepath by appending the name
||| to the root path.
export
toFilePath : {root : Path} -> FileName root -> String
toFilePath file = show (root /> fileName file)

export
directoryExists : {root : Path} -> FileName root -> IO Bool
directoryExists fp = do
  Right dir <- openDir (toFilePath fp)
    | Left _ => pure False
  closeDir dir
  pure True

------------------------------------------------------------------------------
-- Directory trees

||| A `Tree root` is the representation of a directory tree anchored in `root`.
||| Each directory contains a list of files and a list of subtrees waiting to be
||| explored. The fact these subtrees are IO-bound means the subtrees will be
||| lazily constructed on demand.
public export
SubTree : Path -> Type

public export
record Tree (root : Path) where
  constructor MkTree
  files    : List (FileName root)
  subTrees : List (SubTree root)

SubTree root = (dir : FileName root ** IO (Tree (root /> fileName dir)))

||| An empty tree contains no files and has no sub-directories.
export
emptyTree : Tree root
emptyTree = MkTree [] []

namespace Tree
  ||| No run time information is changed,
  ||| so we assert the identity.
  export
  toRelative : Tree root -> Tree (parse "")
  toRelative x = believe_me x

||| Filter out files and directories that do not satisfy a given predicate.
export
filter : (filePred, dirPred : {root : _} -> FileName root -> Bool) ->
         {root : _} -> Tree root -> Tree root
filter filePred dirPred (MkTree files dirs) = MkTree files' dirs' where

  files' : List (FileName root)
  files' = filter filePred files

  dirs' : List (SubTree root)
  dirs' = flip mapMaybe dirs $ \ (dname ** iot) => do
            guard (dirPred dname)
            pure (dname ** map (assert_total (filter filePred dirPred)) iot)

||| Sort the lists of files and directories using the given comparison functions
export
sortBy : (fileCmp, dirCmp : {root : _} -> FileName root -> FileName root -> Ordering) ->
         {root : _} -> Tree root -> Tree root
sortBy fileCmp dirCmp (MkTree files dirs) = MkTree files' dirs' where

  files' : List (FileName root)
  files' = sortBy fileCmp files

  dirs' : List (SubTree root)
  dirs' = sortBy (\ d1, d2 => dirCmp (fst d1) (fst d2))
        $ flip map dirs $ \ (dname ** iot) =>
          (dname ** map (assert_total (sortBy fileCmp dirCmp)) iot)

||| Sort the list of files and directories alphabetically
export
sort : {root : _} -> Tree root -> Tree root
sort = sortBy cmp cmp where

  cmp : {root : _} -> FileName root -> FileName root -> Ordering
  cmp a b = compare (fileName a) (fileName b)

||| Exploring a filesystem from a given root to produce a tree
export
explore : (root : Path) -> IO (Tree root)

go : {root : Path} -> Directory -> Tree root -> IO (Tree root)

explore root = do
  Right dir <- openDir (show root)
    | Left err => pure emptyTree
  assert_total (go dir emptyTree)

go dir acc = case !(dirEntry dir) of
  -- If there is no next entry then we are done and can return the accumulator.
  Left err => acc <$ closeDir dir
  -- Otherwise we have an entry and need to categorise it
  Right entry => do
    -- ignore aliases for current and parent directories
    let False = elem entry [".", ".."]
         | _ => assert_total (go dir acc)
    -- if the entry is a directory, add it to the (lazily explored)
    -- list of subdirectories
    let entry : FileName root = MkFileName entry
    let acc = if !(directoryExists entry)
                then { subTrees $= ((entry ** explore _) ::) } acc
                else { files    $= (entry                ::) } acc
    assert_total (go dir acc)

||| Depth first traversal of all of the files in a tree
export
covering
depthFirst : ({root : Path} -> FileName root -> Lazy (IO a) -> IO a) ->
             {root : Path} -> Tree root -> IO a -> IO a
depthFirst check t k =
  let next = foldr (\ (dir ** iot), def => depthFirst check !iot def) k t.subTrees in
  foldr (\ fn, def => check fn def) next t.files

||| Display a tree by printing it procedurally. Note that because directory
||| trees contain suspended computations corresponding to their subtrees this
||| has to be an `IO` function. We make it return Unit rather than a String
||| because we do not want to assume that the tree is finite.
export
covering
print : Tree root -> IO ()
print t = go [([], ".", Evidence root (pure t))] where

  -- This implementation is unadulterated black magic.
  -- Do NOT touch it if nothing is broken.

  padding : Bool -> List Bool -> String
  padding isDir = fastConcat . go [] where

    go : List String -> List Bool -> List String
    go acc [] = acc
    go acc (b :: bs) = go (hd :: acc) bs where
      hd : String
      hd = if isDir && isNil acc
           then if b then " ├ " else " └ "
           else if b then " │"  else "  "

  prefixes : Nat -> List Bool
  prefixes n = snoc (replicate (pred n) True) False

  covering
  go : List (List Bool, String, Exists (IO . Tree)) -> IO ()
  go [] = pure ()
  go ((bs, fn, Evidence _ iot) :: iots) = do
    t <- iot
    putStrLn (padding True bs ++ fn)
    let pad = padding False bs
    let pads = prefixes (length t.files + length t.subTrees)
    for_ (zip pads t.files) $ \ (b, fp) =>
      putStrLn (pad ++ (if b then " ├ " else " └ ") ++ fileName fp)
    let bss = map (:: bs) (prefixes (length t.subTrees))
    go (zipWith (\ bs, (dir ** iot) => (bs, fileName dir, Evidence _ iot)) bss t.subTrees)
    go iots

-- This function is deprecated; to be removed after the next version bump
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)

||| Copy a directory and its contents recursively
||| Returns a FileError if the target directory already exists, or if any of
||| the source files fail to be copied.
export
covering
copyDir : HasIO io => (src : Path) -> (target : Path) -> io (Either FileError ())
copyDir src target = runEitherT $ do
    MkEitherT $ createDir $ show target
    copyDirContents !(liftIO $ explore src) target
  where
    copyFile' : (srcDir : Path) -> (targetDir : Path) -> (fileName : String) -> EitherT FileError io ()
    copyFile' srcDir targetDir fileName = do
      MkEitherT $ Tree.copyFile (show $ srcDir /> fileName) (show $ targetDir /> fileName)

    covering
    copyDirContents : {srcDir : Path} -> Tree srcDir -> (targetDir : Path) -> EitherT FileError io ()
    copyDirContents (MkTree files subTrees) targetDir = do
      traverse_ (copyFile' srcDir targetDir) (map fileName files)
      traverse_ (\(subDir ** subDirTree) => do
          let targetSubDir = targetDir /> fileName subDir
          MkEitherT $ createDir $ show $ targetSubDir
          copyDirContents !(liftIO subDirTree) targetSubDir
        ) subTrees