text:
module TTImp.Reflect

import Core.Context
import Core.Env
import Core.Normalise
import Core.Reflect
import Core.TT
import Core.Value

import TTImp.TTImp

%default covering

export
Reify BindMode where
  reify defs val@(NDCon _ n _ _ args)
      = case (dropAllNS !(full (gamma defs) n), args) of
             (UN (Basic "PI"), [(_, c)])
                 => do c' <- reify defs !(evalClosure defs c)
                       pure (PI c')
             (UN (Basic "PATTERN"), _) => pure PATTERN
             (UN (Basic "NONE"), _) => pure NONE
             _ => cantReify val "BindMode"
  reify deva val = cantReify val "BindMode"

export
Reflect BindMode where
  reflect fc defs lhs env (PI c)
      = do c' <- reflect fc defs lhs env c
           appCon fc defs (reflectionttimp "PI") [c']
  reflect fc defs lhs env PATTERN
      = getCon fc defs (reflectionttimp "PATTERN")
  reflect fc defs lhs env NONE
      = getCon fc defs (reflectionttimp "NONE")

export
Reify UseSide where
  reify defs val@(NDCon _ n _ _ args)
      = case (dropAllNS !(full (gamma defs) n), args) of
             (UN (Basic "UseLeft"), _) => pure UseLeft
             (UN (Basic "UseRight"), _) => pure UseRight
             _ => cantReify val "UseSide"
  reify defs val = cantReify val "UseSide"

export
Reflect UseSide where
  reflect fc defs lhs env UseLeft
      = getCon fc defs (reflectionttimp "UseLeft")
  reflect fc defs lhs env UseRight
      = getCon fc defs (reflectionttimp "UseRight")

export
Reify DotReason where
  reify defs val@(NDCon _ n _ _ args)
      = case (dropAllNS !(full (gamma defs) n), args) of
             (UN (Basic "NonLinearVar"), _) => pure NonLinearVar
             (UN (Basic "VarApplied"), _) => pure VarApplied
             (UN (Basic "NotConstructor"), _) => pure NotConstructor
             (UN (Basic "ErasedArg"), _) => pure ErasedArg
             (UN (Basic "UserDotted"), _) => pure UserDotted
             (UN (Basic "UnknownDot"), _) => pure UnknownDot
             (UN (Basic "UnderAppliedCon"), _) => pure UnderAppliedCon
             _ => cantReify val "DotReason"
  reify defs val = cantReify val "DotReason"

export
Reflect DotReason where
  reflect fc defs lhs env NonLinearVar
      = getCon fc defs (reflectionttimp "NonLinearVar")
  reflect fc defs lhs env VarApplied
      = getCon fc defs (reflectionttimp "VarApplied")
  reflect fc defs lhs env NotConstructor
      = getCon fc defs (reflectionttimp "NotConstructor")
  reflect fc defs lhs env ErasedArg
      = getCon fc defs (reflectionttimp "ErasedArg")
  reflect fc defs lhs env UserDotted
      = getCon fc defs (reflectionttimp "UserDotted")
  reflect fc defs lhs env UnknownDot
      = getCon fc defs (reflectionttimp "UnknownDot")
  reflect fc defs lhs env UnderAppliedCon
      = getCon fc defs (reflectionttimp "UnderAppliedCon")

mutual
  export
  Reify RawImp where
    reify defs val@(NDCon _ n _ _ args)
        = case (dropAllNS !(full (gamma defs) n), map snd args) of
               (UN (Basic "IVar"), [fc, n])
                    => do fc' <- reify defs !(evalClosure defs fc)
                          n' <- reify defs !(evalClosure defs n)
                          pure (IVar fc' n')
               (UN (Basic "IPi"), [fc, c, p, mn, aty, rty])
                    => do fc' <- reify defs !(evalClosure defs fc)
                          c' <- reify defs !(evalClosure defs c)
                          p' <- reify defs !(evalClosure defs p)
                          mn' <- reify defs !(evalClosure defs mn)
                          aty' <- reify defs !(evalClosure defs aty)
                          rty' <- reify defs !(evalClosure defs rty)
                          pure (IPi fc' c' p' mn' aty' rty')
               (UN (Basic "ILam"), [fc, c, p, mn, aty, lty])
                    => do fc' <- reify defs !(evalClosure defs fc)
                          c' <- reify defs !(evalClosure defs c)
                          p' <- reify defs !(evalClosure defs p)
                          mn' <- reify defs !(evalClosure defs mn)
                          aty' <- reify defs !(evalClosure defs aty)
                          lty' <- reify defs !(evalClosure defs lty)
                          pure (ILam fc' c' p' mn' aty' lty')
               (UN (Basic "ILet"), [fc, lhsFC, c, n, ty, val, sc])
                    => do fc' <- reify defs !(evalClosure defs fc)
                          lhsFC' <- reify defs !(evalClosure defs lhsFC)
                          c' <- reify defs !(evalClosure defs c)
                          n' <- reify defs !(evalClosure defs n)
                          ty' <- reify defs !(evalClosure defs ty)
                          val' <- reify defs !(evalClosure defs val)
                          sc' <- reify defs !(evalClosure defs sc)
                          pure (ILet fc' lhsFC' c' n' ty' val' sc')
               (UN (Basic "ICase"), [fc, sc, ty, cs])
                    => do fc' <- reify defs !(evalClosure defs fc)
                          sc' <- reify defs !(evalClosure defs sc)
                          ty' <- reify defs !(evalClosure defs ty)
                          cs' <- reify defs !(evalClosure defs cs)
                          pure (ICase fc' sc' ty' cs')
               (UN (Basic "ILocal"), [fc, ds, sc])
                    => do fc' <- reify defs !(evalClosure defs fc)
                          ds' <- reify defs !(evalClosure defs ds)
                          sc' <- reify defs !(evalClosure defs sc)
                          pure (ILocal fc' ds' sc')
               (UN (Basic "IUpdate"), [fc, ds, sc])
                    => do fc' <- reify defs !(evalClosure defs fc)
                          ds' <- reify defs !(evalClosure defs ds)
                          sc' <- reify defs !(evalClosure defs sc)
                          pure (IUpdate fc' ds' sc')
               (UN (Basic "IApp"), [fc, f, a])
                    => do fc' <- reify defs !(evalClosure defs fc)
                          f' <- reify defs !(evalClosure defs f)
                          a' <- reify defs !(evalClosure defs a)
                          pure (IApp fc' f' a')
               (UN (Basic "INamedApp"), [fc, f, m, a])
                    => do fc' <- reify defs !(evalClosure defs fc)
                          f' <- reify defs !(evalClosure defs f)
                          m' <- reify defs !(evalClosure defs m)
                          a' <- reify defs !(evalClosure defs a)
                          pure (INamedApp fc' f' m' a')
               (UN (Basic "IAutoApp"), [fc, f, a])
                    => do fc' <- reify defs !(evalClosure defs fc)
                          f' <- reify defs !(evalClosure defs f)
                          a' <- reify defs !(evalClosure defs a)
                          pure (IAutoApp fc' f' a')
               (UN (Basic "IWithApp"), [fc, f, a])
                    => do fc' <- reify defs !(evalClosure defs fc)
                          f' <- reify defs !(evalClosure defs f)
                          a' <- reify defs !(evalClosure defs a)
                          pure (IWithApp fc' f' a')
               (UN (Basic "ISearch"), [fc, d])
                    => do fc' <- reify defs !(evalClosure defs fc)
                          d' <- reify defs !(evalClosure defs d)
                          pure (ISearch fc' d')
               (UN (Basic "IAlternative"), [fc, t, as])
                    => do fc' <- reify defs !(evalClosure defs fc)
                          t' <- reify defs !(evalClosure defs t)
                          as' <- reify defs !(evalClosure defs as)
                          pure (IAlternative fc' t' as')
               (UN (Basic "IRewrite"), [fc, t, sc])
                    => do fc' <- reify defs !(evalClosure defs fc)
                          t' <- reify defs !(evalClosure defs t)
                          sc' <- reify defs !(evalClosure defs sc)
                          pure (IRewrite fc' t' sc')
               (UN (Basic "IBindHere"), [fc, t, sc])
                    => do fc' <- reify defs !(evalClosure defs fc)
                          t' <- reify defs !(evalClosure defs t)
                          sc' <- reify defs !(evalClosure defs sc)
                          pure (IBindHere fc' t' sc')
               (UN (Basic "IBindVar"), [fc, n])
                    => do fc' <- reify defs !(evalClosure defs fc)
                          n' <- reify defs !(evalClosure defs n)
                          pure (IBindVar fc' n')
               (UN (Basic "IAs"), [fc, nameFC, s, n, t])
                    => do fc' <- reify defs !(evalClosure defs fc)
                          nameFC' <- reify defs !(evalClosure defs nameFC)
                          s' <- reify defs !(evalClosure defs s)
                          n' <- reify defs !(evalClosure defs n)
                          t' <- reify defs !(evalClosure defs t)
                          pure (IAs fc' nameFC' s' n' t')
               (UN (Basic "IMustUnify"), [fc, r, t])
                    => do fc' <- reify defs !(evalClosure defs fc)
                          r' <- reify defs !(evalClosure defs r)
                          t' <- reify defs !(evalClosure defs t)
                          pure (IMustUnify fc' r' t')
               (UN (Basic "IDelayed"), [fc, r, t])
                    => do fc' <- reify defs !(evalClosure defs fc)
                          r' <- reify defs !(evalClosure defs r)
                          t' <- reify defs !(evalClosure defs t)
                          pure (IDelayed fc' r' t')
               (UN (Basic "IDelay"), [fc, t])
                    => do fc' <- reify defs !(evalClosure defs fc)
                          t' <- reify defs !(evalClosure defs t)
                          pure (IDelay fc' t')
               (UN (Basic "IForce"), [fc, t])
                    => do fc' <- reify defs !(evalClosure defs fc)
                          t' <- reify defs !(evalClosure defs t)
                          pure (IForce fc' t')
               (UN (Basic "IQuote"), [fc, t])
                    => do fc' <- reify defs !(evalClosure defs fc)
                          t' <- reify defs !(evalClosure defs t)
                          pure (IQuote fc' t')
               (UN (Basic "IQuoteName"), [fc, t])
                    => do fc' <- reify defs !(evalClosure defs fc)
                          t' <- reify defs !(evalClosure defs t)
                          pure (IQuoteName fc' t')
               (UN (Basic "IQuoteDecl"), [fc, t])
                    => do fc' <- reify defs !(evalClosure defs fc)
                          t' <- reify defs !(evalClosure defs t)
                          pure (IQuoteDecl fc' t')
               (UN (Basic "IUnquote"), [fc, t])
                    => do fc' <- reify defs !(evalClosure defs fc)
                          t' <- reify defs !(evalClosure defs t)
                          pure (IUnquote fc' t')
               (UN (Basic "IPrimVal"), [fc, t])
                    => do fc' <- reify defs !(evalClosure defs fc)
                          t' <- reify defs !(evalClosure defs t)
                          pure (IPrimVal fc' t')
               (UN (Basic "IType"), [fc])
                    => do fc' <- reify defs !(evalClosure defs fc)
                          pure (IType fc')
               (UN (Basic "IHole"), [fc, n])
                    => do fc' <- reify defs !(evalClosure defs fc)
                          n' <- reify defs !(evalClosure defs n)
                          pure (IHole fc' n')
               (UN (Basic "Implicit"), [fc, n])
                    => do fc' <- reify defs !(evalClosure defs fc)
                          n' <- reify defs !(evalClosure defs n)
                          pure (Implicit fc' n')
               (UN (Basic "IWithUnambigNames"), [fc, ns, t])
                    => do fc' <- reify defs !(evalClosure defs fc)
                          ns' <- reify defs !(evalClosure defs ns)
                          t' <- reify defs !(evalClosure defs t)
                          pure (IWithUnambigNames fc' ns' t')
               _ => cantReify val "TTImp"
    reify defs val = cantReify val "TTImp"

  export
  Reify IFieldUpdate where
    reify defs val@(NDCon _ n _ _ args)
        = case (dropAllNS !(full (gamma defs) n), args) of
               (UN (Basic "ISetField"), [(_, x), (_, y)])
                    => do x' <- reify defs !(evalClosure defs x)
                          y' <- reify defs !(evalClosure defs y)
                          pure (ISetField x' y')
               (UN (Basic "ISetFieldApp"), [(_, x), (_, y)])
                    => do x' <- reify defs !(evalClosure defs x)
                          y' <- reify defs !(evalClosure defs y)
                          pure (ISetFieldApp x' y')
               _ => cantReify val "IFieldUpdate"
    reify defs val = cantReify val "IFieldUpdate"

  export
  Reify AltType where
    reify defs val@(NDCon _ n _ _ args)
        = case (dropAllNS !(full (gamma defs) n), args) of
               (UN (Basic "FirstSuccess"), _)
                    => pure FirstSuccess
               (UN (Basic "Unique"), _)
                    => pure Unique
               (UN (Basic "UniqueDefault"), [(_, x)])
                    => do x' <- reify defs !(evalClosure defs x)
                          pure (UniqueDefault x')
               _ => cantReify val "AltType"
    reify defs val = cantReify val "AltType"

  export
  Reify FnOpt where
    reify defs val@(NDCon _ n _ _ args)
        = case (dropAllNS !(full (gamma defs) n), args) of
               (UN (Basic "Inline"), _) => pure Inline
               (UN (Basic "TCInline"), _) => pure TCInline
               (UN (Basic "Hint"), [(_, x)])
                    => do x' <- reify defs !(evalClosure defs x)
                          pure (Hint x')
               (UN (Basic "GlobalHint"), [(_, x)])
                    => do x' <- reify defs !(evalClosure defs x)
                          pure (GlobalHint x')
               (UN (Basic "ExternFn"), _) => pure ExternFn
               (UN (Basic "ForeignFn"), [(_, x)])
                    => do x' <- reify defs !(evalClosure defs x)
                          pure (ForeignFn x')
               (UN (Basic "Invertible"), _) => pure Invertible
               (UN (Basic "Totality"), [(_, x)])
                    => do x' <- reify defs !(evalClosure defs x)
                          pure (Totality x')
               (UN (Basic "Macro"), _) => pure Macro
               (UN (Basic "SpecArgs"), [(_, x)])
                    => do x' <- reify defs !(evalClosure defs x)
                          pure (SpecArgs x')
               _ => cantReify val "FnOpt"
    reify defs val = cantReify val "FnOpt"

  export
  Reify ImpTy where
    reify defs val@(NDCon _ n _ _ args)
        = case (dropAllNS !(full (gamma defs) n), map snd args) of
               (UN (Basic "MkTy"), [w, x, y, z])
                    => do w' <- reify defs !(evalClosure defs w)
                          x' <- reify defs !(evalClosure defs x)
                          y' <- reify defs !(evalClosure defs y)
                          z' <- reify defs !(evalClosure defs z)
                          pure (MkImpTy w' x' y' z')
               _ => cantReify val "ITy"
    reify defs val = cantReify val "ITy"

  export
  Reify DataOpt where
    reify defs val@(NDCon _ n _ _ args)
        = case (dropAllNS !(full (gamma defs) n), args) of
               (UN (Basic "SearchBy"), [(_, x)])
                    => do x' <- reify defs !(evalClosure defs x)
                          pure (SearchBy x')
               (UN (Basic "NoHints"), _) => pure NoHints
               (UN (Basic "UniqueSearch"), _) => pure UniqueSearch
               (UN (Basic "External"), _) => pure External
               (UN (Basic "NoNewtype"), _) => pure NoNewtype
               _ => cantReify val "DataOpt"
    reify defs val = cantReify val "DataOpt"

  export
  Reify ImpData where
    reify defs val@(NDCon _ n _ _ args)
        = case (dropAllNS !(full (gamma defs) n), map snd args) of
               (UN (Basic "MkData"), [v,w,x,y,z])
                    => do v' <- reify defs !(evalClosure defs v)
                          w' <- reify defs !(evalClosure defs w)
                          x' <- reify defs !(evalClosure defs x)
                          y' <- reify defs !(evalClosure defs y)
                          z' <- reify defs !(evalClosure defs z)
                          pure (MkImpData v' w' x' y' z')
               (UN (Basic "MkLater"), [x,y,z])
                    => do x' <- reify defs !(evalClosure defs x)
                          y' <- reify defs !(evalClosure defs y)
                          z' <- reify defs !(evalClosure defs z)
                          pure (MkImpLater x' y' z')
               _ => cantReify val "Data"
    reify defs val = cantReify val "Data"

  export
  Reify IField where
    reify defs val@(NDCon _ n _ _ args)
        = case (dropAllNS !(full (gamma defs) n), map snd args) of
               (UN (Basic "MkIField"), [v,w,x,y,z])
                    => do v' <- reify defs !(evalClosure defs v)
                          w' <- reify defs !(evalClosure defs w)
                          x' <- reify defs !(evalClosure defs x)
                          y' <- reify defs !(evalClosure defs y)
                          z' <- reify defs !(evalClosure defs z)
                          pure (MkIField v' w' x' y' z')
               _ => cantReify val "IField"
    reify defs val = cantReify val "IField"

  export
  Reify ImpRecord where
    reify defs val@(NDCon _ n _ _ args)
        = case (dropAllNS !(full (gamma defs) n), map snd args) of
               (UN (Basic "MkRecord"), [v,w,x,y,z])
                    => do v' <- reify defs !(evalClosure defs v)
                          w' <- reify defs !(evalClosure defs w)
                          x' <- reify defs !(evalClosure defs x)
                          y' <- reify defs !(evalClosure defs y)
                          z' <- reify defs !(evalClosure defs z)
                          pure (MkImpRecord v' w' x' y' z')
               _ => cantReify val "Record"
    reify defs val = cantReify val "Record"

  export
  Reify WithFlag where
    reify defs val@(NDCon _ n _ _ args)
        = case (dropAllNS !(full (gamma defs) n), map snd args) of
               (UN (Basic "Syntactic"), [])
                    => pure Syntactic
               _ => cantReify val "WithFlag"
    reify defs val = cantReify val "WithFlag"

  export
  Reify ImpClause where
    reify defs val@(NDCon _ n _ _ args)
        = case (dropAllNS !(full (gamma defs) n), map snd args) of
               (UN (Basic "PatClause"), [x,y,z])
                    => do x' <- reify defs !(evalClosure defs x)
                          y' <- reify defs !(evalClosure defs y)
                          z' <- reify defs !(evalClosure defs z)
                          pure (PatClause x' y' z')
               (UN (Basic "WithClause"), [u,v,w,x,y,z])
                    => do u' <- reify defs !(evalClosure defs u)
                          v' <- reify defs !(evalClosure defs v)
                          w' <- reify defs !(evalClosure defs w)
                          x' <- reify defs !(evalClosure defs x)
                          y' <- reify defs !(evalClosure defs y)
                          z' <- reify defs !(evalClosure defs z)
                          pure (WithClause u' v' w' x' y' z')
               (UN (Basic "ImpossibleClause"), [x,y])
                    => do x' <- reify defs !(evalClosure defs x)
                          y' <- reify defs !(evalClosure defs y)
                          pure (ImpossibleClause x' y')
               _ => cantReify val "Clause"
    reify defs val = cantReify val "Clause"

  export
  Reify ImpDecl where
    reify defs val@(NDCon _ n _ _ args)
        = case (dropAllNS !(full (gamma defs) n), map snd args) of
               (UN (Basic "IClaim"), [v,w,x,y,z])
                    => do v' <- reify defs !(evalClosure defs v)
                          w' <- reify defs !(evalClosure defs w)
                          x' <- reify defs !(evalClosure defs x)
                          y' <- reify defs !(evalClosure defs y)
                          z' <- reify defs !(evalClosure defs z)
                          pure (IClaim v' w' x' y' z')
               (UN (Basic "IData"), [x,y,z])
                    => do x' <- reify defs !(evalClosure defs x)
                          y' <- reify defs !(evalClosure defs y)
                          z' <- reify defs !(evalClosure defs z)
                          pure (IData x' y' z')
               (UN (Basic "IDef"), [x,y,z])
                    => do x' <- reify defs !(evalClosure defs x)
                          y' <- reify defs !(evalClosure defs y)
                          z' <- reify defs !(evalClosure defs z)
                          pure (IDef x' y' z')
               (UN (Basic "IParameters"), [x,y,z])
                    => do x' <- reify defs !(evalClosure defs x)
                          y' <- reify defs !(evalClosure defs y)
                          z' <- reify defs !(evalClosure defs z)
                          pure (IParameters x' y' z')
               (UN (Basic "IRecord"), [w, x,y,z])
                    => do w' <- reify defs !(evalClosure defs w)
                          x' <- reify defs !(evalClosure defs x)
                          y' <- reify defs !(evalClosure defs y)
                          z' <- reify defs !(evalClosure defs z)
                          pure (IRecord w' x' y' z')
               (UN (Basic "INamespace"), [w,x,y])
                    => do w' <- reify defs !(evalClosure defs w)
                          x' <- reify defs !(evalClosure defs x)
                          y' <- reify defs !(evalClosure defs y)
                          pure (INamespace w' x' y')
               (UN (Basic "ITransform"), [w,x,y,z])
                    => do w' <- reify defs !(evalClosure defs w)
                          x' <- reify defs !(evalClosure defs x)
                          y' <- reify defs !(evalClosure defs y)
                          z' <- reify defs !(evalClosure defs z)
                          pure (ITransform w' x' y' z')
               (UN (Basic "ILog"), [x])
                    => do x' <- reify defs !(evalClosure defs x)
                          pure (ILog x')
               _ => cantReify val "Decl"
    reify defs val = cantReify val "Decl"

mutual
  export
  Reflect RawImp where
    reflect fc defs lhs env (IVar tfc n)
        = do fc' <- reflect fc defs lhs env tfc
             n' <- reflect fc defs lhs env n
             appCon fc defs (reflectionttimp "IVar") [fc', n']
    reflect fc defs lhs env (IPi tfc c p mn aty rty)
        = do fc' <- reflect fc defs lhs env tfc
             c' <- reflect fc defs lhs env c
             p' <- reflect fc defs lhs env p
             mn' <- reflect fc defs lhs env mn
             aty' <- reflect fc defs lhs env aty
             rty' <- reflect fc defs lhs env rty
             appCon fc defs (reflectionttimp "IPi") [fc', c', p', mn', aty', rty']
    reflect fc defs lhs env (ILam tfc c p mn aty rty)
        = do fc' <- reflect fc defs lhs env tfc
             c' <- reflect fc defs lhs env c
             p' <- reflect fc defs lhs env p
             mn' <- reflect fc defs lhs env mn
             aty' <- reflect fc defs lhs env aty
             rty' <- reflect fc defs lhs env rty
             appCon fc defs (reflectionttimp "ILam") [fc', c', p', mn', aty', rty']
    reflect fc defs lhs env (ILet tfc lhsFC c n aty aval sc)
        = do fc' <- reflect fc defs lhs env tfc
             lhsFC' <- reflect fc defs lhs env lhsFC
             c' <- reflect fc defs lhs env c
             n' <- reflect fc defs lhs env n
             aty' <- reflect fc defs lhs env aty
             aval' <- reflect fc defs lhs env aval
             sc' <- reflect fc defs lhs env sc
             appCon fc defs (reflectionttimp "ILet") [fc', lhsFC', c', n', aty', aval', sc']
    reflect fc defs lhs env (ICase tfc sc ty cs)
        = do fc' <- reflect fc defs lhs env tfc
             sc' <- reflect fc defs lhs env sc
             ty' <- reflect fc defs lhs env ty
             cs' <- reflect fc defs lhs env cs
             appCon fc defs (reflectionttimp "ICase") [fc', sc', ty', cs']
    reflect fc defs lhs env (ILocal tfc ds sc)
        = do fc' <- reflect fc defs lhs env tfc
             ds' <- reflect fc defs lhs env ds
             sc' <- reflect fc defs lhs env sc
             appCon fc defs (reflectionttimp "ILocal") [fc', ds', sc']
    reflect fc defs lhs env (ICaseLocal tfc u i args t)
        = reflect fc defs lhs env t -- shouldn't see this anyway...
    reflect fc defs lhs env (IUpdate tfc ds sc)
        = do fc' <- reflect fc defs lhs env tfc
             ds' <- reflect fc defs lhs env ds
             sc' <- reflect fc defs lhs env sc
             appCon fc defs (reflectionttimp "IUpdate") [fc', ds', sc']
    reflect fc defs lhs env (IApp tfc f a)
        = do fc' <- reflect fc defs lhs env tfc
             f' <- reflect fc defs lhs env f
             a' <- reflect fc defs lhs env a
             appCon fc defs (reflectionttimp "IApp") [fc', f', a']
    reflect fc defs lhs env (IAutoApp tfc f a)
        = do fc' <- reflect fc defs lhs env tfc
             f' <- reflect fc defs lhs env f
             a' <- reflect fc defs lhs env a
             appCon fc defs (reflectionttimp "IAutoApp") [fc', f', a']
    reflect fc defs lhs env (INamedApp tfc f m a)
        = do fc' <- reflect fc defs lhs env tfc
             f' <- reflect fc defs lhs env f
             m' <- reflect fc defs lhs env m
             a' <- reflect fc defs lhs env a
             appCon fc defs (reflectionttimp "INamedApp") [fc', f', m', a']
    reflect fc defs lhs env (IWithApp tfc f a)
        = do fc' <- reflect fc defs lhs env tfc
             f' <- reflect fc defs lhs env f
             a' <- reflect fc defs lhs env a
             appCon fc defs (reflectionttimp "IWithApp") [fc', f', a']
    reflect fc defs lhs env (ISearch tfc d)
        = do fc' <- reflect fc defs lhs env tfc
             d' <- reflect fc defs lhs env d
             appCon fc defs (reflectionttimp "ISearch") [fc', d']
    reflect fc defs lhs env (IAlternative tfc t as)
        = do fc' <- reflect fc defs lhs env tfc
             t' <- reflect fc defs lhs env t
             as' <- reflect fc defs lhs env as
             appCon fc defs (reflectionttimp "IAlternative") [fc', t', as']
    reflect fc defs lhs env (IRewrite tfc t sc)
        = do fc' <- reflect fc defs lhs env tfc
             t' <- reflect fc defs lhs env t
             sc' <- reflect fc defs lhs env sc
             appCon fc defs (reflectionttimp "IRewrite") [fc', t', sc']
    reflect fc defs lhs env (ICoerced tfc d) = reflect fc defs lhs env d
    reflect fc defs lhs env (IBindHere tfc n sc)
        = do fc' <- reflect fc defs lhs env tfc
             n' <- reflect fc defs lhs env n
             sc' <- reflect fc defs lhs env sc
             appCon fc defs (reflectionttimp "IBindHere") [fc', n', sc']
    reflect fc defs lhs env (IBindVar tfc n)
        = do fc' <- reflect fc defs lhs env tfc
             n' <- reflect fc defs lhs env n
             appCon fc defs (reflectionttimp "IBindVar") [fc', n']
    reflect fc defs lhs env (IAs tfc nameFC s n t)
        = do fc' <- reflect fc defs lhs env tfc
             nameFC' <- reflect fc defs lhs env nameFC
             s' <- reflect fc defs lhs env s
             n' <- reflect fc defs lhs env n
             t' <- reflect fc defs lhs env t
             appCon fc defs (reflectionttimp "IAs") [fc', nameFC', s', n', t']
    reflect fc defs lhs env (IMustUnify tfc r t)
        = do fc' <- reflect fc defs lhs env tfc
             r' <- reflect fc defs lhs env r
             t' <- reflect fc defs lhs env t
             appCon fc defs (reflectionttimp "IMustUnify") [fc', r', t']
    reflect fc defs lhs env (IDelayed tfc r t)
        = do fc' <- reflect fc defs lhs env tfc
             r' <- reflect fc defs lhs env r
             t' <- reflect fc defs lhs env t
             appCon fc defs (reflectionttimp "IDelayed") [fc', r', t']
    reflect fc defs lhs env (IDelay tfc t)
        = do fc' <- reflect fc defs lhs env tfc
             t' <- reflect fc defs lhs env t
             appCon fc defs (reflectionttimp "IDelay") [fc', t']
    reflect fc defs lhs env (IForce tfc t)
        = do fc' <- reflect fc defs lhs env tfc
             t' <- reflect fc defs lhs env t
             appCon fc defs (reflectionttimp "IForce") [fc', t']
    reflect fc defs lhs env (IQuote tfc t)
        = do fc' <- reflect fc defs lhs env tfc
             t' <- reflect fc defs lhs env t
             appCon fc defs (reflectionttimp "IQuote") [fc', t']
    reflect fc defs lhs env (IQuoteName tfc t)
        = do fc' <- reflect fc defs lhs env tfc
             t' <- reflect fc defs lhs env t
             appCon fc defs (reflectionttimp "IQuoteName") [fc', t']
    reflect fc defs lhs env (IQuoteDecl tfc t)
        = do fc' <- reflect fc defs lhs env tfc
             t' <- reflect fc defs lhs env t
             appCon fc defs (reflectionttimp "IQuoteDecl") [fc', t']
    reflect fc defs lhs env (IUnquote tfc (IVar _ t))
        = pure (Ref tfc Bound t)
    reflect fc defs lhs env (IUnquote tfc t)
        = throw (InternalError "Can't reflect an unquote: escapes should be lifted out")
    reflect fc defs lhs env (IRunElab tfc t)
        = throw (InternalError "Can't reflect a %runelab")
    reflect fc defs lhs env (IPrimVal tfc t)
        = do fc' <- reflect fc defs lhs env tfc
             t' <- reflect fc defs lhs env t
             appCon fc defs (reflectionttimp "IPrimVal") [fc', t']
    reflect fc defs lhs env (IType tfc)
        = do fc' <- reflect fc defs lhs env tfc
             appCon fc defs (reflectionttimp "IType") [fc']
    reflect fc defs lhs env (IHole tfc t)
        = do fc' <- reflect fc defs lhs env tfc
             t' <- reflect fc defs lhs env t
             appCon fc defs (reflectionttimp "IHole") [fc', t']
    reflect fc defs lhs env (IUnifyLog tfc _ t)
        = reflect fc defs lhs env t
    reflect fc defs True env (Implicit tfc t)
        = pure (Erased fc False)
    reflect fc defs lhs env (Implicit tfc t)
        = do fc' <- reflect fc defs lhs env tfc
             t' <- reflect fc defs lhs env t
             appCon fc defs (reflectionttimp "Implicit") [fc', t']
    reflect fc defs lhs env (IWithUnambigNames tfc ns t)
        = do fc' <- reflect fc defs lhs env tfc
             ns' <- reflect fc defs lhs env ns
             t' <- reflect fc defs lhs env t
             appCon fc defs (reflectionttimp "WithUnambigNames") [fc', ns', t']

  export
  Reflect IFieldUpdate where
    reflect fc defs lhs env (ISetField p t)
        = do p' <- reflect fc defs lhs env p
             t' <- reflect fc defs lhs env t
             appCon fc defs (reflectionttimp "ISetField") [p', t']
    reflect fc defs lhs env (ISetFieldApp p t)
        = do p' <- reflect fc defs lhs env p
             t' <- reflect fc defs lhs env t
             appCon fc defs (reflectionttimp "ISetFieldApp") [p', t']

  export
  Reflect AltType where
    reflect fc defs lhs env FirstSuccess = getCon fc defs (reflectionttimp "FirstSuccess")
    reflect fc defs lhs env Unique = getCon fc defs (reflectionttimp "Unique")
    reflect fc defs lhs env (UniqueDefault x)
        = do x' <- reflect fc defs lhs env x
             appCon fc defs (reflectionttimp "UniqueDefault") [x']

  export
  Reflect FnOpt where
    reflect fc defs lhs env Inline = getCon fc defs (reflectionttimp "Inline")
    reflect fc defs lhs env TCInline = getCon fc defs (reflectionttimp "TCInline")
    reflect fc defs lhs env (Hint x)
        = do x' <- reflect fc defs lhs env x
             appCon fc defs (reflectionttimp "Hint") [x']
    reflect fc defs lhs env (GlobalHint x)
        = do x' <- reflect fc defs lhs env x
             appCon fc defs (reflectionttimp "GlobalHint") [x']
    reflect fc defs lhs env ExternFn = getCon fc defs (reflectionttimp "ExternFn")
    reflect fc defs lhs env (ForeignFn x)
        = do x' <- reflect fc defs lhs env x
             appCon fc defs (reflectionttimp "ForeignFn") [x']
    reflect fc defs lhs env Invertible = getCon fc defs (reflectionttimp "Invertible")
    reflect fc defs lhs env (Totality r)
        = do r' <- reflect fc defs lhs env r
             appCon fc defs (reflectionttimp "Totality") [r']
    reflect fc defs lhs env Macro = getCon fc defs (reflectionttimp "Macro")
    reflect fc defs lhs env (SpecArgs r)
        = do r' <- reflect fc defs lhs env r
             appCon fc defs (reflectionttimp "SpecArgs") [r']

  export
  Reflect ImpTy where
    reflect fc defs lhs env (MkImpTy w x y z)
        = do w' <- reflect fc defs lhs env w
             x' <- reflect fc defs lhs env x
             y' <- reflect fc defs lhs env y
             z' <- reflect fc defs lhs env z
             appCon fc defs (reflectionttimp "MkTy") [w', x', y', z']

  export
  Reflect DataOpt where
    reflect fc defs lhs env (SearchBy x)
        = do x' <- reflect fc defs lhs env x
             appCon fc defs (reflectionttimp "SearchBy") [x']
    reflect fc defs lhs env NoHints = getCon fc defs (reflectionttimp "NoHints")
    reflect fc defs lhs env UniqueSearch = getCon fc defs (reflectionttimp "UniqueSearch")
    reflect fc defs lhs env External = getCon fc defs (reflectionttimp "External")
    reflect fc defs lhs env NoNewtype = getCon fc defs (reflectionttimp "NoNewtype")

  export
  Reflect ImpData where
    reflect fc defs lhs env (MkImpData v w x y z)
        = do v' <- reflect fc defs lhs env v
             w' <- reflect fc defs lhs env w
             x' <- reflect fc defs lhs env x
             y' <- reflect fc defs lhs env y
             z' <- reflect fc defs lhs env z
             appCon fc defs (reflectionttimp "MkData") [v', w', x', y', z']
    reflect fc defs lhs env (MkImpLater x y z)
        = do x' <- reflect fc defs lhs env x
             y' <- reflect fc defs lhs env y
             z' <- reflect fc defs lhs env z
             appCon fc defs (reflectionttimp "MkLater") [x', y', z']

  export
  Reflect IField where
    reflect fc defs lhs env (MkIField v w x y z)
        = do v' <- reflect fc defs lhs env v
             w' <- reflect fc defs lhs env w
             x' <- reflect fc defs lhs env x
             y' <- reflect fc defs lhs env y
             z' <- reflect fc defs lhs env z
             appCon fc defs (reflectionttimp "MkIField") [v', w', x', y', z']

  export
  Reflect ImpRecord where
    reflect fc defs lhs env (MkImpRecord v w x y z)
        = do v' <- reflect fc defs lhs env v
             w' <- reflect fc defs lhs env w
             x' <- reflect fc defs lhs env x
             y' <- reflect fc defs lhs env y
             z' <- reflect fc defs lhs env z
             appCon fc defs (reflectionttimp "MkRecord") [v', w', x', y', z']

  export
  Reflect WithFlag where
    reflect fc defs lhs env Syntactic
        = getCon fc defs (reflectionttimp "Syntactic")

  export
  Reflect ImpClause where
    reflect fc defs lhs env (PatClause x y z)
        = do x' <- reflect fc defs lhs env x
             y' <- reflect fc defs lhs env y
             z' <- reflect fc defs lhs env z
             appCon fc defs (reflectionttimp "PatClause") [x', y', z']
    reflect fc defs lhs env (WithClause u v w x y z)
        = do u' <- reflect fc defs lhs env u
             v' <- reflect fc defs lhs env v
             w' <- reflect fc defs lhs env w
             x' <- reflect fc defs lhs env x
             y' <- reflect fc defs lhs env y
             z' <- reflect fc defs lhs env z
             appCon fc defs (reflectionttimp "WithClause") [u', v', w', x', y', z']
    reflect fc defs lhs env (ImpossibleClause x y)
        = do x' <- reflect fc defs lhs env x
             y' <- reflect fc defs lhs env y
             appCon fc defs (reflectionttimp "ImpossibleClause") [x', y']

  export
  Reflect ImpDecl where
    reflect fc defs lhs env (IClaim v w x y z)
        = do v' <- reflect fc defs lhs env v
             w' <- reflect fc defs lhs env w
             x' <- reflect fc defs lhs env x
             y' <- reflect fc defs lhs env y
             z' <- reflect fc defs lhs env z
             appCon fc defs (reflectionttimp "IClaim") [v', w', x', y', z']
    reflect fc defs lhs env (IData x y z)
        = do x' <- reflect fc defs lhs env x
             y' <- reflect fc defs lhs env y
             z' <- reflect fc defs lhs env z
             appCon fc defs (reflectionttimp "IData") [x', y', z']
    reflect fc defs lhs env (IDef x y z)
        = do x' <- reflect fc defs lhs env x
             y' <- reflect fc defs lhs env y
             z' <- reflect fc defs lhs env z
             appCon fc defs (reflectionttimp "IDef") [x', y', z']
    reflect fc defs lhs env (IParameters x y z)
        = do x' <- reflect fc defs lhs env x
             y' <- reflect fc defs lhs env y
             z' <- reflect fc defs lhs env z
             appCon fc defs (reflectionttimp "IParameters") [x', y', z']
    reflect fc defs lhs env (IRecord w x y z)
        = do w' <- reflect fc defs lhs env w
             x' <- reflect fc defs lhs env x
             y' <- reflect fc defs lhs env y
             z' <- reflect fc defs lhs env z
             appCon fc defs (reflectionttimp "IRecord") [w', x', y', z']
    reflect fc defs lhs env (INamespace x y z)
        = do x' <- reflect fc defs lhs env x
             y' <- reflect fc defs lhs env y
             z' <- reflect fc defs lhs env z
             appCon fc defs (reflectionttimp "INamespace") [x', y', z']
    reflect fc defs lhs env (ITransform w x y z)
        = do w' <- reflect fc defs lhs env w
             x' <- reflect fc defs lhs env x
             y' <- reflect fc defs lhs env y
             z' <- reflect fc defs lhs env z
             appCon fc defs (reflectionttimp "ITransform") [w', x', y', z']
    reflect fc defs lhs env (IRunElabDecl w x)
        = throw (GenericMsg fc "Can't reflect a %runElab")
    reflect fc defs lhs env (IPragma _ x)
        = throw (GenericMsg fc "Can't reflect a pragma")
    reflect fc defs lhs env (ILog x)
        = do x' <- reflect fc defs lhs env x
             appCon fc defs (reflectionttimp "ILog") [x']
    reflect fc defs lhs env (IBuiltin _ _ _)
        = throw (GenericMsg fc "Can't reflect a %builtin")


text:
module On2

on2 : forall f, t. (t a -> t b -> c) -> (forall z. f z -> t z) -> f a -> f b -> c
on2 g h = \x, y => h x `g` h y

ext: idr

max_stars_repo_name: buzden/idris-playground

max_issues_repo_name: buzden/idris-playground

max_forks_repo_name: buzden/idris-playground


text:
||| Commands Rules
||| Section 6
module Bautzen.Game.Command

import public Bautzen.GameUnit
import Bautzen.Game.Core
import Bautzen.Pos

import Data.Maybe.Extra

import Data.Fin
import Data.Nat
import Data.List

%default total

public export
atCommandDistance : Maybe Pos -> (Pos, Nat) -> Bool
atCommandDistance Nothing y = False
atCommandDistance (Just posUnit) (posHQ, commandDistance) =
  distance posUnit posHQ <= commandDistance

public export
withinCommandDistance : (unit : GameUnit) -> (hqs : List GameUnit) -> (pos : List (GameUnit, Pos)) -> Bool
withinCommandDistance unit hqs pos =
  any (atCommandDistance (lookup unit pos)) (catMaybes $ map positionAndDistance hqs)
  where
    positionAndDistance : GameUnit -> Maybe (Pos, Nat)
    positionAndDistance unit =
      case unitType unit of
        HQ => (\ p => (p, supportDistance unit)) <$> lookup unit pos
        _ => Nothing

||| Find the HQ for a given formation
public export
findHQ : GameUnit -> List (GameUnit, Pos) -> List GameUnit
findHQ unit units = map fst $ filter (flip isHQFor unit . fst) units

||| Check given `unit` is under command of its HQ or a corps/army HQ
public export
underCommand : (units : List (GameUnit, Pos)) -> (unit : GameUnit) -> Bool
underCommand units unit =
  withinCommandDistance unit hqs units
  where
    hqs : List GameUnit
    hqs = findHQ unit units

namespace CommandTest

  positions : List (GameUnit, Pos)
  positions = [ (Bautzen.GameUnit.p15_5dp, Hex 2 2)
              , (Bautzen.GameUnit.r857_294, Hex 2 3)
              , (Bautzen.GameUnit.p13_5dp, Hex 3 4)
              , (Bautzen.GameUnit.p5dp, Hex 3 6)
              , (Bautzen.GameUnit.p2awp, Hex 4 6)
              ]

  -- unit_is_under_command_if_with_command_distance_of_own_hq :
  --   underCommand CommandTest.positions GameUnit.p13_5dp = True
  -- unit_is_under_command_if_with_command_distance_of_own_hq = Refl

  -- unit_is_under_command_if_with_command_distance_of_army_or_corps_hq :
  --   underCommand CommandTest.positions GameUnit.p15_5dp = True
  -- unit_is_under_command_if_with_command_distance_of_army_or_corps_hq = Refl

  -- unit_is_not_under_command_of_hq_with_different_nationality :
  --   underCommand CommandTest.positions GameUnit.r857_294 = False
  -- unit_is_not_under_command_of_hq_with_different_nationality = Refl

max_stars_repo_name: steshaw/hsgames

max_issues_repo_name: steshaw/hsgames

max_forks_repo_name: steshaw/hsgames


text:
import readNum
import System

guess : (iteration : Nat) -> (target : Nat) -> IO ()
guess iteration target = let itn = iteration + 1 in
                      do putStrLn $ "This is attempt number: " ++ (show itn)
                         putStrLn "Guess a number"
                         Just g <- readNumber | Nothing => (putStrLn "Error: Only input digits" >>= \_ => (guess itn target))
                         case compare g target of
                             LT => putStrLn "Too low!" >>= \_ => guess itn target
                             EQ => putStrLn "Got it!"
                             GT => putStrLn "Too high!" >>= \_ => guess itn target

main : IO ()
main = do n <- map ((-) 20000) $ time
          guess 0 $ cast n


text:
--- Data declarations ---

infix 0 =%=

public export
data (=%=) : (a -> b) -> (a -> b) -> Type where
  ExtEq : {0 f, g : a -> b} -> ((x : a) -> f x = g x) -> f =%= g

infix 0 %%

public export
data (%%) a b = Equs (a = b) (b = a)

--- Records ---

infix 0 =%%=

public export
record (=%%=) {a : Type} {b : Type} (f : a -> b) (g : a -> b) where
  constructor ExtEqR
  fa : (x : a) -> f x = g x

--- Interfaces ---

infix 0 =%%%=

public export
interface (=%%%=) (x : a) (y : a) (b : Type) (i : Type) where
  idx : a -> i -> b
  eq : (ix : i) -> idx x ix = idx y ix


text:
module Tokenizer

%default total
%access public export

record MacroHeader where
  constructor MacroH
  indent : Nat
  name : String
  params : List String

space : Nat -> Char -> Maybe Nat
space x y =
  if isSpace y
  then Just (x + 1)
  else Nothing

startsWith : List Char -> List Char -> Maybe (List Char)
startsWith [] [] = Just []
startsWith [] (x :: xs) = Just (x :: xs)
startsWith (y :: xs) [] = Nothing
startsWith (y :: xs) (x :: ys) =
  if y == x
  then startsWith xs ys
  else Nothing

parseHeaderWith : String -> Nat -> List Char -> Maybe MacroHeader
parseHeaderWith kw x ('/' :: '/' :: '#' :: cs) =
  startsWith (unpack kw) cs
  >>= \cs' =>
    case words $ pack cs' of
    [] => Nothing
    name :: params => Just $ MacroH x name params
parseHeaderWith _ _ _ = Nothing

parseHeaderTok' : String -> Nat -> List Char -> Maybe MacroHeader
parseHeaderTok' _ x [] = Nothing
parseHeaderTok' kw x (c :: cs) =
  case space x c of
    Nothing => parseHeaderWith kw x (c :: cs)
    Just x => parseHeaderTok' kw x cs

parseHeaderTok : String -> String -> Maybe MacroHeader
parseHeaderTok kw = parseHeaderTok' kw 0 . unpack

parseFooter : String -> String -> Bool
parseFooter x = (==) ("//#end" ++ x) . trim

max_stars_repo_name: Kazark/fspp

max_issues_repo_name: Kazark/fspp

max_forks_repo_name: Kazark/fspp


text:
> module Fun.FunExp

from https://github.com/DSLsofMath/DSLsofMath/blob/master/L/DSLsofMath/FunExp.lhs

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

> ||| Functions as expressions
> data FunExp : Type -> Type where
>   Const : t -> FunExp t
>   Id    : FunExp t
>   (+)   : FunExp t -> FunExp t -> FunExp t
>   (-)   : FunExp t -> FunExp t -> FunExp t
>   (*)   : FunExp t -> FunExp t -> FunExp t
>   (/)   : FunExp t -> FunExp t -> FunExp t
>   (.)   : FunExp t -> FunExp t -> FunExp t
>   Exp   : FunExp t -> FunExp t
>   -- etc.

> interface (Num ty) => Math ty where
>   exp : ty -> ty

> ||| Evaluation
> eval : (Num t, Fractional t, Neg t, Math t) => FunExp t -> t -> t
> eval (Const c) x = (const c) x
> eval Id        x = id x
> eval (e1 + e2) x = (eval e1 x) + (eval e2 x)
> eval (e1 - e2) x = (eval e1 x) - (eval e2 x)
> eval (e1 * e2) x = (eval e1 x) * (eval e2 x)
> eval (e1 / e2) x = (eval e1 x) / (eval e2 x)
> eval (e1 . e2) x = (eval e1 (eval e2 x))
> eval (Exp e)   x = exp (eval e x)

> ||| Differentiation
> derivative : (Num t, Fractional t, Neg t) => FunExp t -> FunExp t
> derivative (Const c) = Const 0
> derivative Id        = Const 1
> derivative (e1 + e2) = derivative e1 + derivative e2
> derivative (e1 - e2) = derivative e1 - derivative e2
> derivative (e1 * e2) = (derivative e1) * e2 + e1 * (derivative e2)
> derivative (e1 / e2) = (derivative e1) / e2 - e1 * (derivative e2) / (e2 * e2)
> derivative (e1 . e2) = ((derivative e1) . e2) * (derivative e2)
> derivative (Exp e)   = (Exp e) * (derivative e)

This needs to be tested!

ext: lidr

max_stars_repo_name: zenntenn/IdrisLibs

max_issues_repo_name: zenntenn/IdrisLibs

max_forks_repo_name: zenntenn/IdrisLibs


text:
module JS.Record

import JS.Marshall

export
data Record : Type -> Type -> Type where [external]

export
ToFFI (Record a b) (Record a b) where toFFI = id

export
FromFFI (Record a b) (Record a b) where fromFFI = Just


text:
module IdrisJvm.FileChannelIo

import IdrisJvm.IO
import Java.Nio

%access public export

namespace FileChannelIo
  FileChannelIoClass : JVM_NativeTy
  FileChannelIoClass = Class "io/github/mmhelloworld/idrisjvm/io/FileChannelIo"

  FileChannelIo : Type
  FileChannelIo = JVM_Native FileChannelIoClass

  open : Path -> JVM_Array OpenOption -> JVM_IO (Either Throwable FileChannelIo)
  open = invokeStatic FileChannelIoClass "open" (Path -> JVM_Array OpenOption -> JVM_IO (Either Throwable FileChannelIo))

  getChar : FileChannelIo -> JVM_IO Char
  getChar = invokeInstance "getChar" (FileChannelIo -> JVM_IO Char)

  getLine : FileChannelIo -> JVM_IO String
  getLine = invokeInstance "getLine" (FileChannelIo -> JVM_IO String)

  writeString : FileChannelIo -> String -> JVM_IO ()
  writeString = invokeInstance "writeString" (FileChannelIo -> String -> JVM_IO ())

  getPath : FileChannelIo -> JVM_IO Path
  getPath = invokeInstance "getPath" (FileChannelIo -> JVM_IO Path)

  isEof : FileChannelIo -> JVM_IO Bool
  isEof = invokeInstance "isEof" (FileChannelIo -> JVM_IO Bool)

  size : FileChannelIo -> JVM_IO (Either Throwable Bits64)
  size = invokeInstance "size" (FileChannelIo -> JVM_IO (Either Throwable Bits64))

  getFileModifiedTime : FileChannelIo -> JVM_IO (Either Throwable Integer)
  getFileModifiedTime = invokeInstance "getFileModifiedTime" (FileChannelIo -> JVM_IO (Either Throwable Integer))

  getFileAccessTime : FileChannelIo -> JVM_IO (Either Throwable Integer)
  getFileAccessTime = invokeInstance "getFileAccessTime" (FileChannelIo -> JVM_IO (Either Throwable Integer))

  getFileStatusTime : FileChannelIo -> JVM_IO (Either Throwable Integer)
  getFileStatusTime = invokeInstance "getFileStatusTime" (FileChannelIo -> JVM_IO (Either Throwable Integer))

  flush : FileChannelIo -> JVM_IO ()
  flush = invokeInstance "flush" (FileChannelIo -> JVM_IO ())

  close : FileChannelIo -> JVM_IO ()
  close = invokeInstance "close" (FileChannelIo -> JVM_IO ())

  Inherits Channel FileChannelIo where {}
  Inherits ReadableByteChannel FileChannelIo where {}
  Inherits WritableByteChannel FileChannelIo where {}


text:
import Data.Bits
import Data.DPair
import Data.List
import Data.Stream
import Decidable.Equality

import Data.Fin

--------------------------------------------------------------------------------
--          Utilities
--------------------------------------------------------------------------------

shl1 : Int -> Int
shl1 = prim__shl_Int 1

b8max : Bits8
b8max = 0xff

b16max : Bits16
b16max = 0xffff

b32max : Bits32
b32max = 0xffffffff

b64max : Bits64
b64max = 18446744073709551615

-- the only way to create -2^63
intmin : Int
intmin = shl1 63

intmax : Int
intmax = 0x7fffffffffffffff

powsOf2 : Num a => Nat -> List a
powsOf2 n = take n (iterate (*2) 1)

--------------------------------------------------------------------------------
--          shiftR
--------------------------------------------------------------------------------

shiftRBits8 : List Bits8
shiftRBits8 = map (`shiftR` 1) (powsOf2 8 ++ [b8max])

shiftRBits16 : List Bits16
shiftRBits16 = map (`shiftR` 1) (powsOf2 16 ++ [b16max])

shiftRBits32 : List Bits32
shiftRBits32 = map (`shiftR` 1) (powsOf2 32 ++ [b32max])

shiftRInt : List Int
shiftRInt = map (`shiftR` 1) (powsOf2 63 ++ [intmax])

shiftRNegativeInt : List Int
shiftRNegativeInt = map (`shiftR` 1) (map negate (powsOf2 63) ++ [intmin])

--------------------------------------------------------------------------------
--          shiftL
--------------------------------------------------------------------------------

shiftLBits8 : List Bits8
shiftLBits8 = map (`shiftL` 1) (0 :: powsOf2 7)

shiftLBits16 : List Bits16
shiftLBits16 = map (`shiftL` 1) (0 :: powsOf2 15)

shiftLBits32 : List Bits32
shiftLBits32 = map (`shiftL` 1) (0 :: powsOf2 31)

shiftLInt : List Int
shiftLInt = map (`shiftL` 1) (0 :: powsOf2 62)

shiftLNegativeInt : List Int
shiftLNegativeInt = map (`shiftL` 1) (map negate (powsOf2 62))

--------------------------------------------------------------------------------
--          Bitwise AND
--------------------------------------------------------------------------------

andBits8 : List Bits8
andBits8 = [ 11 .&. b8max
           , 11 .&. 0
           , 11 .&. 1
           , 11 .&. 2
           , 11 .&. 4
           , 11 .&. 11
           ]

andBits16 : List Bits16
andBits16 = [ 11 .&. b16max
            , 11 .&. 0
            , 11 .&. 1
            , 11 .&. 2
            , 11 .&. 4
            , 11 .&. 11
            ]

andBits32 : List Bits32
andBits32 = [ 11 .&. b32max
            , 11 .&. 0
            , 11 .&. 1
            , 11 .&. 2
            , 11 .&. 4
            , 11 .&. 11
            ]

andInt : List Int
andInt = [ 11 .&. intmax
         , 11 .&. 0
         , 11 .&. 1
         , 11 .&. 2
         , 11 .&. 4
         , 11 .&. 11
         ]

andNegativeInt : List Int
andNegativeInt = [ (-11) .&. intmax
                 , (-11) .&. 0
                 , (-11) .&. 1
                 , (-11) .&. 2
                 , (-11) .&. 4
                 , (-11) .&. 11
                 , (-11) .&. intmin
                 , (-11) .&. (-1)
                 , (-11) .&. (-2)
                 , (-11) .&. (-4)
                 , (-11) .&. (-11)
                 ]

--------------------------------------------------------------------------------
--          Bitwise OR
--------------------------------------------------------------------------------

orBits8 : List Bits8
orBits8 = [ 11 .|. b8max
          , 11 .|. 0
          , 11 .|. 1
          , 11 .|. 2
          , 11 .|. 4
          , 11 .|. 11
          ]

orBits16 : List Bits16
orBits16 = [ 11 .|. b16max
           , 11 .|. 0
           , 11 .|. 1
           , 11 .|. 2
           , 11 .|. 4
           , 11 .|. 11
           ]

orBits32 : List Bits32
orBits32 = [ 11 .|. b32max
           , 11 .|. 0
           , 11 .|. 1
           , 11 .|. 2
           , 11 .|. 4
           , 11 .|. 11
           ]

orInt : List Int
orInt = [ 11 .|. intmax
        , 11 .|. 0
        , 11 .|. 1
        , 11 .|. 2
        , 11 .|. 4
        , 11 .|. 11
        ]

orNegativeInt : List Int
orNegativeInt = [ (-11) .|. intmax
                , (-11) .|. 0
                , (-11) .|. 1
                , (-11) .|. 2
                , (-11) .|. 4
                , (-11) .|. 11
                , (-11) .|. intmin
                , (-11) .|. (-1)
                , (-11) .|. (-2)
                , (-11) .|. (-4)
                , (-11) .|. (-11)
                ]

--------------------------------------------------------------------------------
--          Bitwise XOR
--------------------------------------------------------------------------------

xorBits8 : List Bits8
xorBits8 = [ 11 `xor` b8max
           , 11 `xor` 0
           , 11 `xor` 1
           , 11 `xor` 2
           , 11 `xor` 4
           , 11 `xor` 11
           ]

xorBits16 : List Bits16
xorBits16 = [ 11 `xor` b16max
            , 11 `xor` 0
            , 11 `xor` 1
            , 11 `xor` 2
            , 11 `xor` 4
            , 11 `xor` 11
            ]

xorBits32 : List Bits32
xorBits32 = [ 11 `xor` b32max
            , 11 `xor` 0
            , 11 `xor` 1
            , 11 `xor` 2
            , 11 `xor` 4
            , 11 `xor` 11
            ]

xorInt : List Int
xorInt = [ 11 `xor` intmax
         , 11 `xor` 0
         , 11 `xor` 1
         , 11 `xor` 2
         , 11 `xor` 4
         , 11 `xor` 11
         ]

xorNegativeInt : List Int
xorNegativeInt = [ (-11) `xor` intmax
                 , (-11) `xor` 0
                 , (-11) `xor` 1
                 , (-11) `xor` 2
                 , (-11) `xor` 4
                 , (-11) `xor` 11
                 , (-11) `xor` intmin
                 , (-11) `xor` (-1)
                 , (-11) `xor` (-2)
                 , (-11) `xor` (-4)
                 , (-11) `xor` (-11)
                 ]

--------------------------------------------------------------------------------
--          bit
--------------------------------------------------------------------------------

bitBits8 : List Bits8
bitBits8 = map bit $ mapMaybe (`natToFin` 8) [0..7]

bitBits16 : List Bits16
bitBits16 = map bit $ mapMaybe (`natToFin` 16) [0..15]

bitBits32 : List Bits32
bitBits32 = map bit $ mapMaybe (`natToFin` 32) [0..31]

bitInt : List Int
bitInt = map bit $ mapMaybe (`natToFin` 64) [0..63]

--------------------------------------------------------------------------------
--          complementBit
--------------------------------------------------------------------------------

complementBitBits8 : List Bits8
complementBitBits8 = map (`complementBit` 1) bitBits8

complementBitBits16 : List Bits16
complementBitBits16 = map (`complementBit` 1) bitBits16

complementBitBits32 : List Bits32
complementBitBits32 = map (`complementBit` 1) bitBits32

complementBitInt : List Int
complementBitInt = map (`complementBit` 1) bitInt

--------------------------------------------------------------------------------
--          clearBit
--------------------------------------------------------------------------------

clearBitBits8 : List Bits8
clearBitBits8 = map (`clearBit` 5) bitBits8

clearBitBits16 : List Bits16
clearBitBits16 = map (`clearBit` 5) bitBits16

clearBitBits32 : List Bits32
clearBitBits32 = map (`clearBit` 5) bitBits32

clearBitInt : List Int
clearBitInt = map (`clearBit` 5) bitInt

--------------------------------------------------------------------------------
--          setBit
--------------------------------------------------------------------------------

setBitBits8 : List Bits8
setBitBits8 = map (`setBit` 1) bitBits8

setBitBits16 : List Bits16
setBitBits16 = map (`setBit` 1) bitBits16

setBitBits32 : List Bits32
setBitBits32 = map (`setBit` 1) bitBits32

setBitInt : List Int
setBitInt = map (`setBit` 1) bitInt

--------------------------------------------------------------------------------
--          testBit
--------------------------------------------------------------------------------

testBitBits8 : List Bool
testBitBits8 = map (testBit (the Bits8 0xaa))
             $ mapMaybe (`natToFin` 8) [0..7]

testBitBits16 : List Bool
testBitBits16 = map (testBit (the Bits16 0xaaaa))
              $ mapMaybe (`natToFin` 16) [0..15]

testBitBits32 : List Bool
testBitBits32 = map (testBit (the Bits32 0xaaaaaaaa))
              $ mapMaybe (`natToFin` 32) [0..31]

testBitInt : List Bool
testBitInt = map (testBit (the Int 0xaaaaaaaaaaaaaaa))
           $ mapMaybe (`natToFin` 64) [0..63]

testBitNegInt : List Bool
testBitNegInt = map (testBit (negate $ the Int 0xaaaaaaaaaaaaaaa))
              $ mapMaybe (`natToFin` 64) [0..63]

--------------------------------------------------------------------------------
--          popCount
--------------------------------------------------------------------------------

popCountBits8 : List Nat
popCountBits8 = map popCount [the Bits8 0, 0xaa, 0xff]

popCountBits16 : List Nat
popCountBits16 = map popCount [the Bits16 0, 0xaaaa, 0xffff]

popCountBits32 : List Nat
popCountBits32 = map popCount [the Bits32 0, 0xaaaaaaaa, 0xffffffff]

popCountInt : List Nat
popCountInt = map popCount [ the Int 0

                           -- 0101 0101 ... 0101
                           -- => 32
                           , 0x5555555555555555

                           , -1

                           -- 1010 1010 ... 1011
                           -- => 33
                           , negate 0x5555555555555555
                           ]

--------------------------------------------------------------------------------
--          Running Tests
--------------------------------------------------------------------------------

main : IO ()
main = do printLn shiftRBits8
          printLn shiftRBits16
          printLn shiftRBits32
          printLn shiftRInt
          printLn shiftRNegativeInt

          putStrLn ""

          printLn shiftLBits8
          printLn shiftLBits16
          printLn shiftLBits32
          printLn shiftLInt
          printLn shiftLNegativeInt

          putStrLn ""

          printLn andBits8
          printLn andBits16
          printLn andBits32
          printLn andInt
          printLn andNegativeInt

          putStrLn ""

          printLn orBits8
          printLn orBits16
          printLn orBits32
          printLn orInt
          printLn orNegativeInt

          putStrLn ""

          printLn xorBits8
          printLn xorBits16
          printLn xorBits32
          printLn xorInt
          printLn xorNegativeInt

          putStrLn ""

          printLn bitBits8
          printLn bitBits16
          printLn bitBits32
          printLn bitInt

          putStrLn ""

          printLn complementBitBits8
          printLn complementBitBits16
          printLn complementBitBits32
          printLn complementBitInt

          putStrLn ""

          printLn clearBitBits8
          printLn clearBitBits16
          printLn clearBitBits32
          printLn clearBitInt

          putStrLn ""

          printLn setBitBits8
          printLn setBitBits16
          printLn setBitBits32
          printLn setBitInt

          putStrLn ""

          printLn testBitBits8
          printLn testBitBits16
          printLn testBitBits32
          printLn testBitInt
          printLn testBitNegInt

          putStrLn ""

          printLn popCountBits8
          printLn popCountBits16
          printLn popCountBits32
          printLn popCountInt


text:
module Label

labelFrom : Integer -> List a -> List (Integer, a)
labelFrom n [] = []
labelFrom n (y :: ys) = (n, y) :: labelFrom (n+1) ys

label : List a -> List (Integer, a)
label = labelFrom 0

max_stars_repo_path: Chapter 11/Label.idr

max_issues_repo_path: Chapter 11/Label.idr

max_forks_repo_path: Chapter 11/Label.idr


text:
module User

import Objects.Career
import Objects.City
import Objects.Contact
import Objects.Counters
import Objects.Country
import Objects.CropPhoto
import Objects.Education
import Objects.LastSeen
import Objects.Military
import Objects.Occupation
import Objects.Personal
import Objects.Relative
import Objects.School
import Objects.University
import Utils.Types
-- Util --
-- This type used in many field for showing permission of any action or simple show existense any field --
--IsIt : Type
--IsIt = Types.IsIt

record User where
  constructor CreateUser
  -- Basic fields --
  id : Integer
  hidden : Integer
  firstName : String
  lastName : String
  deactivated : String
  -- Optional fields --
  about : Maybe String
  activities : Maybe String
  bdate : Maybe String
  blacklisted : Integer -> Maybe IsIt
  blacklistedByMe : Integer -> Maybe IsIt
  books : Maybe String
  canPost : Integer -> Maybe IsIt
  canSeeAllPosts : Integer -> Maybe IsIt
  canSeeAudio : Integer -> Maybe IsIt
  canSendFriendRequest : Integer -> Maybe IsIt
  canWritePrivateMessages : Integer -> Maybe IsIt
  career : Maybe Career.Career
  city : Maybe City.City
  connections : Maybe String
  contacts : Maybe Contact.Contact
  counters : Maybe Counters.Counters
  country : Maybe Country.Country
  cropPhoto : Maybe CropPhoto
  domain : Maybe String
  education : Maybe Education.Education
  exports : Maybe String
  firstNameNom : Maybe String
  firstNameGen : Maybe String
  firstNameDat : Maybe String
  firstNameAcc : Maybe String
  firstNameInc : Maybe String
  firstNameAbl : Maybe String
  followersCount : Maybe Integer
  friendStatus : Maybe Integer
  games : Maybe String
  hasMobile : Maybe IsIt
  hasPhoto : Maybe IsIt
  homeTown : Maybe IsIt
  interests : Maybe $ String
  isFavourite : Maybe $ Integer -> IsIt
  isFriend : Maybe $ Integer -> IsIt
  isHiddenFromFeed : Maybe $ Integer -> IsIt
  lastNameNom : Maybe String
  lastNameGen : Maybe String
  lastNameDat : Maybe String
  lastNameAcc : Maybe String
  lastNameInc : Maybe String
  lastNameAbl : Maybe String
  lastSeen : Maybe LastSeen.LastSeen
  lists : Maybe String
  maidenName : Maybe String
  military : Maybe Military.Military
  movies : Maybe String
  music : Maybe String
  nickname : Maybe String
  occupation : Maybe Occupation.Occupation
  online : Maybe IsIt
  onlineMobile : Maybe IsIt
  onlineApp : Maybe Integer
  personal : Maybe Personal.Personal
  photo50 : Maybe String
  photo100 : Maybe String
  photo200 : Maybe String
  photo200Orig : Maybe String -- bad name
  photo400Orig : Maybe String -- bad name
  photoID : Maybe Integer
  photoMax : Maybe String
  photoMaxOrig : Maybe String
  quotes : Maybe String
  relatives : Maybe $ List Relative.Relative
  relation : Maybe Integer
  schools : Maybe $ List School.School
  screenName : Maybe String
  sex : Integer -> Maybe Integer
  site : Maybe String
  status : Maybe String
  timeZone : Maybe Integer
  tv : Maybe String
  universities : Maybe $ List University.University
  verified : Integer -> Maybe IsIt
  wallComments : Integer -> Maybe IsIt

max_stars_repo_name: GrandArchTemplar/IdrisVKAPI

max_issues_repo_name: GrandArchTemplar/IdrisVKAPI

max_forks_repo_name: GrandArchTemplar/IdrisVKAPI


text:
import System.Concurrency.Channels

data Message = Add Nat Nat

adder : IO ()
adder = do Just sender_chan <- listen 1
              | Nothing => adder
           Just msg <- unsafeRecv Message sender_chan
              | Nothing => adder
           case msg of
                Add x y => do ok <- unsafeSend sender_chan (x + y)
                              adder

main : IO ()
main = do Just adder_id <- spawn adder
               | Nothing => putStrLn "Spawn failed"
          Just chan <- connect adder_id
               | Nothing => putStrLn "Connection failed"
          ok <- unsafeSend chan (Add 2 3)
          Just answer <- unsafeRecv String chan
               | Nothing => putStrLn "Send failed"
          printLn answer

max_issues_repo_name: gdevanla/TypeDD-Samples

max_forks_repo_name: gdevanla/TypeDD-Samples


text:
-- --------------------------------------------------------- [ Combinators.idr ]
-- Module      : Lightyear.Combinators
-- Description : Generic Combinators
--
-- This code is distributed under the BSD 2-clause license.
-- See the file LICENSE in the root directory for its full text.
-- --------------------------------------------------------------------- [ EOH ]
module Lightyear.Combinators

import Data.Vect

import Lightyear.Core

-- %access export

-- --------------------------------------------------------------- [ Operators ]
infixr 3 :::
private
(:::) : a -> List a -> List a
(:::) x xs = x :: xs

infixr 3 ::.
private
(::.) : a -> Vect n a -> Vect (S n) a
(::.) x xs = x :: xs

-- -------------------------------------------------- [ Any Token and No Token ]

||| Parse a single arbitrary token. Returns the parsed token.
|||
||| This parser will fail if and only if the input stream is empty.
export
anyToken : (Monad m, Stream tok str) => ParserT str m tok
anyToken = satisfy (const True) <?> "any token"

||| Parse the end of input.
|||
||| This parser will succeed if and only if the input stream is empty.
export
eof : (Monad m, Stream tok str) => ParserT str m ()
eof = requireFailure anyToken <?> "end of input"

-- ---------------------------------------------------- [ Multiple Expressions ]

||| Run some parser as many times as possible, collecting a list of
||| successes.
export
many : Monad m => ParserT str m a -> ParserT str m (List a)
many p = (pure (:::) <*> p <*>| many p) <|> pure []

||| Run the specified parser precisely `n` times, returning a vector
||| of successes.
export
ntimes : Monad m => (n : Nat)
                 -> ParserT str m a
                 -> ParserT str m (Vect n a)
ntimes    Z  p = pure Vect.Nil
ntimes (S n) p = [| p ::. ntimes n p |]

||| Like `many`, but the parser must succeed at least once
export
some : Monad m => ParserT str m a -> ParserT str m (List a)
some p = [| p ::: many p |]

-- --------------------------------------------------- [ Separated Expressions ]

||| Parse repeated instances of at least one `p`, separated by `s`,
||| returning a list of successes.
|||
||| @ p the parser for items
||| @ s the parser for separators
export
sepBy1 : Monad m => (p : ParserT str m a)
                 -> (s : ParserT str m b)
                 -> ParserT str m (List a)
sepBy1 p s = [| p ::: many (s *> p) |]

||| Parse zero or more `p`s, separated by `s`s, returning a list of
||| successes.
|||
||| @ p the parser for items
||| @ s the parser for separators
export
sepBy : Monad m => (p : ParserT str m a)
                -> (s : ParserT str m b)
                -> ParserT str m (List a)
sepBy p s = (p `sepBy1` s) <|> pure []

||| Parse precisely `n` `p`s, separated by `s`s, returning a vect of
||| successes.
|||
||| @ n how many to parse
||| @ p the parser for items
||| @ s the parser for separators
export
sepByN : Monad m => (n : Nat)
                 -> (p : ParserT str m a)
                 -> (s : ParserT str m b)
                 -> ParserT str m (Vect n a)
sepByN    Z  p s = pure Vect.Nil
sepByN (S n) p s = [| p ::. ntimes n (s *> p) |]

||| Parse one or more `p`s, separated by `op`s. Return a value that is
||| the left associative application of the functions returned by `op`.
|||
||| @ p  the parser
||| @ op the parser for operators
export
chainl1 : Monad m => (p : ParserT str m a)
                  -> (op: ParserT str m (a -> a -> a))
                  -> ParserT str m a
chainl1 p op = p >>= rest
  where rest : a -> ParserT str m a
        rest a1 = (do f <- op
                      a2 <- p
                      rest (f a1 a2)) <|> pure a1

||| Parse zero or more `p`s, separated by `op`s. Return a value that is
||| the left associative application of the functions returned by `op`.
||| Return `a` when there are zero occurences of `p`.
|||
||| @ p  the parser
||| @ op the parser for operators
export
chainl : Monad m => (p : ParserT str m a)
                 -> (op : ParserT str m (a -> a -> a))
                 -> a
                 -> ParserT str m a
chainl p op a = (p `chainl1` op) <|> pure a

||| Parse one or more `p`s, separated by `op`s. Return a value that is
||| the right associative application of the functions returned by `op`.
|||
||| @ p  the parser
||| @ op the parser for operators
export
chainr1 : Monad m => (p : ParserT str m a)
                  -> (op: ParserT str m (a -> a -> a))
                  -> ParserT str m a
chainr1 p op = p >>= rest
  where rest : a -> ParserT str m a
        rest a1 = (do f <- op
                      a2 <- p >>= rest
                      rest (f a1 a2)) <|> pure a1

||| Parse zero or more `p`s, separated by `op`s. Return a value that is
||| the right associative application of the functions returned by `op`.
||| Return `a` when there are zero occurences of `p`.
|||
||| @ p  the parser
||| @ op the parser for operators
export
chainr : Monad m => (p : ParserT str m a)
                 -> (op : ParserT str m (a -> a -> a))
                 -> a
                 -> ParserT str m a
chainr p op a = (p `chainr1` op) <|> pure a

||| Alternate between matches of `p` and `s`, starting with `p`,
||| returning a list of successes from both.
export
alternating : Monad m => (p : ParserT str m a)
                      -> (s : ParserT str m a)
                      -> ParserT str m (List a)
alternating p s = (pure (:::) <*> p <*>| alternating s p) <|> pure []

||| Throw away the result from a parser
export
skip : Monad m => ParserT str m a -> ParserT str m ()
skip = map (const ())

||| Attempt to parse `p`. If it succeeds, then return the value. If it
||| fails, continue parsing.
export
opt : Monad m => (p : ParserT str m a) -> ParserT str m (Maybe a)
opt p = map Just p <|> pure Nothing

||| Parse open, then p, then close. Returns the result of `p`.
|||
||| @open The opening parser.
||| @close The closing parser.
||| @p The parser for the middle part.
export
between : Monad m => (open' : ParserT str m a)
                  -> (close : ParserT str m c)
                  -> (p : ParserT str m b)
                  -> ParserT str m b
between open' close p = open' *> p <* close

-- The following names are inspired by the cut operator from Prolog

-- ---------------------------------------------------- [ Monad-like Operators ]

infixr 5 >!=
||| Committing bind
export
(>!=) : Monad m => ParserT str m a
                -> (a -> ParserT str m b)
                -> ParserT str m b
x >!= f = x >>= commitTo . f

infixr 5 >!
||| Committing sequencing
export
(>!) : Monad m => ParserT str m a
               -> ParserT str m b
               -> ParserT str m b
x >! y = x >>= \_ => commitTo y

-- ---------------------------------------------- [ Applicative-like Operators ]

infixl 2 <*!>
||| Committing application
export
(<*!>) : Monad m => ParserT str m (a -> b)
                 -> ParserT str m a
                 -> ParserT str m b
f <*!> x = f <*> commitTo x

infixl 2 <*!
export
(<*!) : Monad m => ParserT str m a
                -> ParserT str m b
                -> ParserT str m a
x <*! y = x <* commitTo y

infixl 2 *!>
export
(*!>) : Monad m => ParserT str m a
                -> ParserT str m b
                -> ParserT str m b
x *!> y = x *> commitTo y

-- ---------------------------------------------------------- [ Lazy Operators ]

infixl 2 <*|
export
(<*|) : Monad m => ParserT str m a
                -> Lazy (ParserT str m b)
                -> ParserT str m a
x <*| y = pure const <*> x <*>| y

infixl 2 *>|
export
(*>|) : Monad m => ParserT str m a
                -> Lazy (ParserT str m b)
                -> ParserT str m b
x *>| y = pure (const id) <*> x <*>| y
-- ---------------------------------------------------------------------- [ EF ]

max_stars_repo_name: Mr-Andersen/lightyear

max_issues_repo_name: Mr-Andersen/lightyear

max_forks_repo_name: Mr-Andersen/lightyear


text:
-- -------------------------------------------------------------- [ Parser.idr ]
-- Module      : Text.Kindle.Clippings.Parser
-- Description : Parse Kinddle clippings.
--
-- License     : This code is distributed under the MIT license. See the
--               file LICENSE in the root directory for its full text.
-- --------------------------------------------------------------------- [ EOH ]
module Text.Kindle.Clippings.Parser

import public Text.Kindle.Clippings.Types

import TParsec
import TParsec.Running

-- FIXME: Handle this (better)
%access public export
%default total

-- ----------------------------------------------------------------- [ Parsers ]

||| Parse a series of one or more non-whitespace characters,
||| packing them into a string.
word : Parser String

||| Parse a series of characters up to the end of a line.
line : Parser String

||| Parse an parenthesized author name in reverse.
author' : Parser Author

||| Parse a title, i.e. the rest of a line, in reverse.
title' : Parser Title

||| Parse a document, i.e. a title, followed by
||| a possibly absent parenthesized author, in reverse.
||| N.B. This will consider `"bar"` in `"Foo (bar)"` to be an author.
document' : Parser Document

||| Parse a document, i.e. a title, followed by
||| a possibly absent parenthesized author.
||| N.B. This will consider `"bar"` in `"Foo (bar)"` to be an author.
document : Parser Document

||| Parse the beginning of the second line of a clipping for its content type.
contentType : Parser String

||| Parse a singleton interval, i.e. a single page or location number.
singletonInterval : Parser Interval

-- TODO: enforce from =< to
||| Parse a proper interval, i.e. a range of pages or locations.
properInterval : Parser Interval

||| Parse an proper or singleton interval.
interval : Parser Interval

||| Parse a reference to a page number or range of pages.
page : Parser Page

||| Parse a reference to a location or range of locations.
location : Parser Location

||| Parse date of the form, `"%A, %B %d, %Y %T"`.
||| N.B. For now, this ignores the time.
date : Parser Date

||| Parse the end of a clipping record, i.e. zero or more newlines,
||| followed by `"=========="`.
eor : Parser ()

||| Parse some content, i.e. empty lines for a `Bookmark`, the `selection` of a
||| `Highlight` or the `body` of a `Note`.
content : Parser String

||| Parse an entire clipping.
clipping : Parser (Maybe Clipping)

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

max_stars_repo_name: yurrriq/my-clippings

max_issues_repo_name: yurrriq/my-clippings

max_forks_repo_name: yurrriq/my-clippings


text:
module Web.Internal.UIEventsPrim

import JS
import Web.Internal.Types

--------------------------------------------------------------------------------
--          Interfaces
--------------------------------------------------------------------------------

namespace CompositionEvent

  export
  %foreign "browser:lambda:x=>x.data"
  prim__data : CompositionEvent -> PrimIO String

namespace FocusEvent

  export
  %foreign "browser:lambda:x=>x.relatedTarget"
  prim__relatedTarget : FocusEvent -> PrimIO (Nullable EventTarget)

namespace InputEvent

  export
  %foreign "browser:lambda:x=>x.data"
  prim__data : InputEvent -> PrimIO (Nullable String)

  export
  %foreign "browser:lambda:x=>x.inputType"
  prim__inputType : InputEvent -> PrimIO String

  export
  %foreign "browser:lambda:x=>x.isComposing"
  prim__isComposing : InputEvent -> PrimIO Boolean

namespace KeyboardEvent

  export
  %foreign "browser:lambda:x=>x.altKey"
  prim__altKey : KeyboardEvent -> PrimIO Boolean

  export
  %foreign "browser:lambda:x=>x.charCode"
  prim__charCode : KeyboardEvent -> PrimIO Bits32

  export
  %foreign "browser:lambda:x=>x.code"
  prim__code : KeyboardEvent -> PrimIO String

  export
  %foreign "browser:lambda:x=>x.ctrlKey"
  prim__ctrlKey : KeyboardEvent -> PrimIO Boolean

  export
  %foreign "browser:lambda:x=>x.isComposing"
  prim__isComposing : KeyboardEvent -> PrimIO Boolean

  export
  %foreign "browser:lambda:x=>x.key"
  prim__key : KeyboardEvent -> PrimIO String

  export
  %foreign "browser:lambda:x=>x.keyCode"
  prim__keyCode : KeyboardEvent -> PrimIO Bits32

  export
  %foreign "browser:lambda:x=>x.location"
  prim__location : KeyboardEvent -> PrimIO Bits32

  export
  %foreign "browser:lambda:x=>x.metaKey"
  prim__metaKey : KeyboardEvent -> PrimIO Boolean

  export
  %foreign "browser:lambda:x=>x.repeat"
  prim__repeat : KeyboardEvent -> PrimIO Boolean

  export
  %foreign "browser:lambda:x=>x.shiftKey"
  prim__shiftKey : KeyboardEvent -> PrimIO Boolean

  export
  %foreign "browser:lambda:(x,a)=>x.getModifierState(a)"
  prim__getModifierState : KeyboardEvent -> String -> PrimIO Boolean

namespace MouseEvent

  export
  %foreign "browser:lambda:x=>x.altKey"
  prim__altKey : MouseEvent -> PrimIO Boolean

  export
  %foreign "browser:lambda:x=>x.button"
  prim__button : MouseEvent -> PrimIO Int16

  export
  %foreign "browser:lambda:x=>x.buttons"
  prim__buttons : MouseEvent -> PrimIO Bits16

  export
  %foreign "browser:lambda:x=>x.clientX"
  prim__clientX : MouseEvent -> PrimIO Int32

  export
  %foreign "browser:lambda:x=>x.clientY"
  prim__clientY : MouseEvent -> PrimIO Int32

  export
  %foreign "browser:lambda:x=>x.ctrlKey"
  prim__ctrlKey : MouseEvent -> PrimIO Boolean

  export
  %foreign "browser:lambda:x=>x.metaKey"
  prim__metaKey : MouseEvent -> PrimIO Boolean

  export
  %foreign "browser:lambda:x=>x.relatedTarget"
  prim__relatedTarget : MouseEvent -> PrimIO (Nullable EventTarget)

  export
  %foreign "browser:lambda:x=>x.screenX"
  prim__screenX : MouseEvent -> PrimIO Int32

  export
  %foreign "browser:lambda:x=>x.screenY"
  prim__screenY : MouseEvent -> PrimIO Int32

  export
  %foreign "browser:lambda:x=>x.shiftKey"
  prim__shiftKey : MouseEvent -> PrimIO Boolean

  export
  %foreign "browser:lambda:(x,a)=>x.getModifierState(a)"
  prim__getModifierState : MouseEvent -> String -> PrimIO Boolean

namespace UIEvent

  export
  %foreign "browser:lambda:x=>x.detail"
  prim__detail : UIEvent -> PrimIO Int32

  export
  %foreign "browser:lambda:x=>x.view"
  prim__view : UIEvent -> PrimIO (Nullable Window)

  export
  %foreign "browser:lambda:x=>x.which"
  prim__which : UIEvent -> PrimIO Bits32

namespace WheelEvent

  export
  %foreign "browser:lambda:x=>x.deltaMode"
  prim__deltaMode : WheelEvent -> PrimIO Bits32

  export
  %foreign "browser:lambda:x=>x.deltaX"
  prim__deltaX : WheelEvent -> PrimIO Double

  export
  %foreign "browser:lambda:x=>x.deltaY"
  prim__deltaY : WheelEvent -> PrimIO Double

  export
  %foreign "browser:lambda:x=>x.deltaZ"
  prim__deltaZ : WheelEvent -> PrimIO Double

--------------------------------------------------------------------------------
--          Dictionaries
--------------------------------------------------------------------------------

namespace CompositionEventInit

  export
  %foreign "browser:lambda:(a)=> {data: a}"
  prim__new : UndefOr String -> PrimIO CompositionEventInit

  export
  %foreign "browser:lambda:x=>x.data"
  prim__data : CompositionEventInit -> PrimIO (UndefOr String)

  export
  %foreign "browser:lambda:(x,v)=>{x.data = v}"
  prim__setData : CompositionEventInit -> UndefOr String -> PrimIO ()

namespace EventModifierInit

  export
  %foreign "browser:lambda:(a,b,c,d,e,f,g,h,i,j,k,l,m,n)=> {ctrlKey: a,shiftKey: b,altKey: c,metaKey: d,modifierAltGraph: e,modifierCapsLock: f,modifierFn: g,modifierFnLock: h,modifierHyper: i,modifierNumLock: j,modifierScrollLock: k,modifierSuper: l,modifierSymbol: m,modifierSymbolLock: n}"
  prim__new :  UndefOr Boolean
            -> UndefOr Boolean
            -> UndefOr Boolean
            -> UndefOr Boolean
            -> UndefOr Boolean
            -> UndefOr Boolean
            -> UndefOr Boolean
            -> UndefOr Boolean
            -> UndefOr Boolean
            -> UndefOr Boolean
            -> UndefOr Boolean
            -> UndefOr Boolean
            -> UndefOr Boolean
            -> UndefOr Boolean
            -> PrimIO EventModifierInit

  export
  %foreign "browser:lambda:x=>x.altKey"
  prim__altKey : EventModifierInit -> PrimIO (UndefOr Boolean)

  export
  %foreign "browser:lambda:(x,v)=>{x.altKey = v}"
  prim__setAltKey : EventModifierInit -> UndefOr Boolean -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.ctrlKey"
  prim__ctrlKey : EventModifierInit -> PrimIO (UndefOr Boolean)

  export
  %foreign "browser:lambda:(x,v)=>{x.ctrlKey = v}"
  prim__setCtrlKey : EventModifierInit -> UndefOr Boolean -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.metaKey"
  prim__metaKey : EventModifierInit -> PrimIO (UndefOr Boolean)

  export
  %foreign "browser:lambda:(x,v)=>{x.metaKey = v}"
  prim__setMetaKey : EventModifierInit -> UndefOr Boolean -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.modifierAltGraph"
  prim__modifierAltGraph : EventModifierInit -> PrimIO (UndefOr Boolean)

  export
  %foreign "browser:lambda:(x,v)=>{x.modifierAltGraph = v}"
  prim__setModifierAltGraph : EventModifierInit -> UndefOr Boolean -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.modifierCapsLock"
  prim__modifierCapsLock : EventModifierInit -> PrimIO (UndefOr Boolean)

  export
  %foreign "browser:lambda:(x,v)=>{x.modifierCapsLock = v}"
  prim__setModifierCapsLock : EventModifierInit -> UndefOr Boolean -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.modifierFn"
  prim__modifierFn : EventModifierInit -> PrimIO (UndefOr Boolean)

  export
  %foreign "browser:lambda:(x,v)=>{x.modifierFn = v}"
  prim__setModifierFn : EventModifierInit -> UndefOr Boolean -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.modifierFnLock"
  prim__modifierFnLock : EventModifierInit -> PrimIO (UndefOr Boolean)

  export
  %foreign "browser:lambda:(x,v)=>{x.modifierFnLock = v}"
  prim__setModifierFnLock : EventModifierInit -> UndefOr Boolean -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.modifierHyper"
  prim__modifierHyper : EventModifierInit -> PrimIO (UndefOr Boolean)

  export
  %foreign "browser:lambda:(x,v)=>{x.modifierHyper = v}"
  prim__setModifierHyper : EventModifierInit -> UndefOr Boolean -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.modifierNumLock"
  prim__modifierNumLock : EventModifierInit -> PrimIO (UndefOr Boolean)

  export
  %foreign "browser:lambda:(x,v)=>{x.modifierNumLock = v}"
  prim__setModifierNumLock : EventModifierInit -> UndefOr Boolean -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.modifierScrollLock"
  prim__modifierScrollLock : EventModifierInit -> PrimIO (UndefOr Boolean)

  export
  %foreign "browser:lambda:(x,v)=>{x.modifierScrollLock = v}"
  prim__setModifierScrollLock :  EventModifierInit
                              -> UndefOr Boolean
                              -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.modifierSuper"
  prim__modifierSuper : EventModifierInit -> PrimIO (UndefOr Boolean)

  export
  %foreign "browser:lambda:(x,v)=>{x.modifierSuper = v}"
  prim__setModifierSuper : EventModifierInit -> UndefOr Boolean -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.modifierSymbol"
  prim__modifierSymbol : EventModifierInit -> PrimIO (UndefOr Boolean)

  export
  %foreign "browser:lambda:(x,v)=>{x.modifierSymbol = v}"
  prim__setModifierSymbol : EventModifierInit -> UndefOr Boolean -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.modifierSymbolLock"
  prim__modifierSymbolLock : EventModifierInit -> PrimIO (UndefOr Boolean)

  export
  %foreign "browser:lambda:(x,v)=>{x.modifierSymbolLock = v}"
  prim__setModifierSymbolLock :  EventModifierInit
                              -> UndefOr Boolean
                              -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.shiftKey"
  prim__shiftKey : EventModifierInit -> PrimIO (UndefOr Boolean)

  export
  %foreign "browser:lambda:(x,v)=>{x.shiftKey = v}"
  prim__setShiftKey : EventModifierInit -> UndefOr Boolean -> PrimIO ()

namespace FocusEventInit

  export
  %foreign "browser:lambda:(a)=> {relatedTarget: a}"
  prim__new : UndefOr (Nullable EventTarget) -> PrimIO FocusEventInit

  export
  %foreign "browser:lambda:x=>x.relatedTarget"
  prim__relatedTarget :  FocusEventInit
                      -> PrimIO (UndefOr (Nullable EventTarget))

  export
  %foreign "browser:lambda:(x,v)=>{x.relatedTarget = v}"
  prim__setRelatedTarget :  FocusEventInit
                         -> UndefOr (Nullable EventTarget)
                         -> PrimIO ()

namespace InputEventInit

  export
  %foreign "browser:lambda:(a,b,c)=> {data: a,isComposing: b,inputType: c}"
  prim__new :  UndefOr (Nullable String)
            -> UndefOr Boolean
            -> UndefOr String
            -> PrimIO InputEventInit

  export
  %foreign "browser:lambda:x=>x.data"
  prim__data : InputEventInit -> PrimIO (UndefOr (Nullable String))

  export
  %foreign "browser:lambda:(x,v)=>{x.data = v}"
  prim__setData : InputEventInit -> UndefOr (Nullable String) -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.inputType"
  prim__inputType : InputEventInit -> PrimIO (UndefOr String)

  export
  %foreign "browser:lambda:(x,v)=>{x.inputType = v}"
  prim__setInputType : InputEventInit -> UndefOr String -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.isComposing"
  prim__isComposing : InputEventInit -> PrimIO (UndefOr Boolean)

  export
  %foreign "browser:lambda:(x,v)=>{x.isComposing = v}"
  prim__setIsComposing : InputEventInit -> UndefOr Boolean -> PrimIO ()

namespace KeyboardEventInit

  export
  %foreign "browser:lambda:(a,b,c,d,e)=> {key: a,code: b,location: c,repeat: d,isComposing: e}"
  prim__new :  UndefOr String
            -> UndefOr String
            -> UndefOr Bits32
            -> UndefOr Boolean
            -> UndefOr Boolean
            -> PrimIO KeyboardEventInit

  export
  %foreign "browser:lambda:x=>x.code"
  prim__code : KeyboardEventInit -> PrimIO (UndefOr String)

  export
  %foreign "browser:lambda:(x,v)=>{x.code = v}"
  prim__setCode : KeyboardEventInit -> UndefOr String -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.isComposing"
  prim__isComposing : KeyboardEventInit -> PrimIO (UndefOr Boolean)

  export
  %foreign "browser:lambda:(x,v)=>{x.isComposing = v}"
  prim__setIsComposing : KeyboardEventInit -> UndefOr Boolean -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.key"
  prim__key : KeyboardEventInit -> PrimIO (UndefOr String)

  export
  %foreign "browser:lambda:(x,v)=>{x.key = v}"
  prim__setKey : KeyboardEventInit -> UndefOr String -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.location"
  prim__location : KeyboardEventInit -> PrimIO (UndefOr Bits32)

  export
  %foreign "browser:lambda:(x,v)=>{x.location = v}"
  prim__setLocation : KeyboardEventInit -> UndefOr Bits32 -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.repeat"
  prim__repeat : KeyboardEventInit -> PrimIO (UndefOr Boolean)

  export
  %foreign "browser:lambda:(x,v)=>{x.repeat = v}"
  prim__setRepeat : KeyboardEventInit -> UndefOr Boolean -> PrimIO ()

namespace MouseEventInit

  export
  %foreign "browser:lambda:(a,b,c,d,e,f,g)=> {screenX: a,screenY: b,clientX: c,clientY: d,button: e,buttons: f,relatedTarget: g}"
  prim__new :  UndefOr Int32
            -> UndefOr Int32
            -> UndefOr Int32
            -> UndefOr Int32
            -> UndefOr Int16
            -> UndefOr Bits16
            -> UndefOr (Nullable EventTarget)
            -> PrimIO MouseEventInit

  export
  %foreign "browser:lambda:x=>x.button"
  prim__button : MouseEventInit -> PrimIO (UndefOr Int16)

  export
  %foreign "browser:lambda:(x,v)=>{x.button = v}"
  prim__setButton : MouseEventInit -> UndefOr Int16 -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.buttons"
  prim__buttons : MouseEventInit -> PrimIO (UndefOr Bits16)

  export
  %foreign "browser:lambda:(x,v)=>{x.buttons = v}"
  prim__setButtons : MouseEventInit -> UndefOr Bits16 -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.clientX"
  prim__clientX : MouseEventInit -> PrimIO (UndefOr Int32)

  export
  %foreign "browser:lambda:(x,v)=>{x.clientX = v}"
  prim__setClientX : MouseEventInit -> UndefOr Int32 -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.clientY"
  prim__clientY : MouseEventInit -> PrimIO (UndefOr Int32)

  export
  %foreign "browser:lambda:(x,v)=>{x.clientY = v}"
  prim__setClientY : MouseEventInit -> UndefOr Int32 -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.relatedTarget"
  prim__relatedTarget :  MouseEventInit
                      -> PrimIO (UndefOr (Nullable EventTarget))

  export
  %foreign "browser:lambda:(x,v)=>{x.relatedTarget = v}"
  prim__setRelatedTarget :  MouseEventInit
                         -> UndefOr (Nullable EventTarget)
                         -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.screenX"
  prim__screenX : MouseEventInit -> PrimIO (UndefOr Int32)

  export
  %foreign "browser:lambda:(x,v)=>{x.screenX = v}"
  prim__setScreenX : MouseEventInit -> UndefOr Int32 -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.screenY"
  prim__screenY : MouseEventInit -> PrimIO (UndefOr Int32)

  export
  %foreign "browser:lambda:(x,v)=>{x.screenY = v}"
  prim__setScreenY : MouseEventInit -> UndefOr Int32 -> PrimIO ()

namespace UIEventInit

  export
  %foreign "browser:lambda:(a,b)=> {view: a,detail: b}"
  prim__new : UndefOr (Nullable Window) -> UndefOr Int32 -> PrimIO UIEventInit

  export
  %foreign "browser:lambda:x=>x.detail"
  prim__detail : UIEventInit -> PrimIO (UndefOr Int32)

  export
  %foreign "browser:lambda:(x,v)=>{x.detail = v}"
  prim__setDetail : UIEventInit -> UndefOr Int32 -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.view"
  prim__view : UIEventInit -> PrimIO (UndefOr (Nullable Window))

  export
  %foreign "browser:lambda:(x,v)=>{x.view = v}"
  prim__setView : UIEventInit -> UndefOr (Nullable Window) -> PrimIO ()

namespace WheelEventInit

  export
  %foreign "browser:lambda:(a,b,c,d)=> {deltaX: a,deltaY: b,deltaZ: c,deltaMode: d}"
  prim__new :  UndefOr Double
            -> UndefOr Double
            -> UndefOr Double
            -> UndefOr Bits32
            -> PrimIO WheelEventInit

  export
  %foreign "browser:lambda:x=>x.deltaMode"
  prim__deltaMode : WheelEventInit -> PrimIO (UndefOr Bits32)

  export
  %foreign "browser:lambda:(x,v)=>{x.deltaMode = v}"
  prim__setDeltaMode : WheelEventInit -> UndefOr Bits32 -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.deltaX"
  prim__deltaX : WheelEventInit -> PrimIO (UndefOr Double)

  export
  %foreign "browser:lambda:(x,v)=>{x.deltaX = v}"
  prim__setDeltaX : WheelEventInit -> UndefOr Double -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.deltaY"
  prim__deltaY : WheelEventInit -> PrimIO (UndefOr Double)

  export
  %foreign "browser:lambda:(x,v)=>{x.deltaY = v}"
  prim__setDeltaY : WheelEventInit -> UndefOr Double -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.deltaZ"
  prim__deltaZ : WheelEventInit -> PrimIO (UndefOr Double)

  export
  %foreign "browser:lambda:(x,v)=>{x.deltaZ = v}"
  prim__setDeltaZ : WheelEventInit -> UndefOr Double -> PrimIO ()


text:
module Main
import Data.Vect
%hide natToFin
%hide cmp
%hide index
%default total

public export
interface Indexable c i where
    eltype : Type
    index' : i -> c -> eltype

implementation Indexable (Vect k t) (Fin k) where
    eltype = t
    index' FZ (x :: xs) = x
    index' (FS k) (x :: xs) = index' k xs

int_vec : Vect 2 Int
int_vec = [2, 3]

cmp : Nat -> Nat -> Ordering
cmp Z Z = EQ
cmp Z _ = LT
cmp _ Z = GT
cmp (S k1) (S k2) = cmp k1 k2

-- -> {auto p: cmp m n = LT}

filter' : (a -> Bool) -> Vect n a -> (p ** Vect p a)
filter' p [] = ( 0 ** [] )
filter' p (x :: xs) with (filter' p xs)
   | ( a ** xs' ) = if (p x) then ( (S a) ** x :: xs' ) else ( a ** xs' )

-- fin : {n : Nat} -> (m: Nat) -> {default 0 p: Nat} -> Fin n
-- fin {n = S k} Z {p = 0}= FZ
-- fin {n = S k2} (S k1) =  FS (fin {n = k2} k1)
-- fin {n=Z} m {p=(S _, Z)} impossible

-- z : Int
-- z = index' (fin 1) int_vec

-- main : IO ()
-- main = putStrLn . show $ z

max_stars_repo_name: thautwarm/idris-cam

max_issues_repo_name: thautwarm/idris-cam

max_forks_repo_name: thautwarm/idris-cam


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

import Edda
import Edda.Reader.Org

import XML.DOM
import XML.XPath
import XML.XPath.Query

import Freyja
import Freyja.Error
import Freyja.Utils

%access export
-- ----------------------------------------------------------------- [ Queries ]

getNodes : (node : Document ty)
        -> {auto prf : CanQuery ty}
        -> (qstr : String)
        -> Extract (List XMLNode)
getNodes doc qstr = Query.getNodes ExtractionError qstr doc

getNode : (node : Document ty)
       -> {auto prf : CanQuery ty}
       -> (qstr : String)
       -> Extract XMLNode
getNode doc qstr = Query.getNode ExtractionError qstr doc

getNamedAttrs : (node : Document ty)
             -> {auto prf : CanQuery ty}
             -> (name : String)
             -> (qstr : String)
             -> Extract (List String)
getNamedAttrs doc name qstr = Query.getNamedAttrs name ExtractionError qstr doc

getNamedAttr : (node : Document ty)
            -> {auto prf : CanQuery ty}
            -> (name : String)
            -> (qstr : String)
            -> Extract String
getNamedAttr doc name qstr = Query.getNamedAttr name ExtractionError qstr doc

getTextNodes : (node : Document ty)
            -> {auto prf : CanQuery ty}
            -> (qstr : String)
            -> Extract (List String)
getTextNodes doc qstr = Query.getTextNodes ExtractionError qstr doc

getTextNode : (node : Document ty)
           -> {auto prf : CanQuery ty}
           -> (qstr : String)
           -> Extract String
getTextNode doc qstr = Query.getTextNode ExtractionError qstr doc

getCDataNode : (node : Document ty)
            -> {auto prf : CanQuery ty}
            -> (qstr : String)
            -> Extract String
getCDataNode doc qstr = Query.getCDataNode ExtractionError qstr doc

-- -------------------------------------------------- [ Markup Related Queries ]

getEddaStrings : Document ty
             -> {auto prf : CanQuery ty}
             -> String
             -> Extract (List EddaString)
getEddaStrings e qstr = do
    res <- getTextNodes ExtractionError qstr e
    ss  <- mapEither getString res
    pure ss
  where
    getString : String -> Extract $ EddaString
    getString s =
      case readOrgInline s of
        Left err  => Left $ TextConvError err
        Right str => Right str

getEddaString : Document ty
             -> {auto prf : CanQuery ty}
             -> String
             -> Extract EddaString
getEddaString e qstr = do
  res <- getTextNode ExtractionError qstr e
  case readOrgInline res of
    Left err  => Left $ TextConvError err
    Right str => Right str

getEddaBlock : Document ty
            -> {auto prf : CanQuery ty}
            -> String
            -> Extract EddaBody
getEddaBlock e qstr = do
  res <- getTextNode ExtractionError qstr e
  case readOrgBody res of
    Left err  => Left $ TextConvError err
    Right str => Right str

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

max_stars_repo_name: jfdm/freyja-schema

max_issues_repo_name: jfdm/freyja-schema

max_forks_repo_name: jfdm/freyja-schema