text:
module Core.Normalise

import Core.CaseTree
import Core.Context
import Core.Context.Log
import Core.Core
import Core.Env
import Core.Options
import Core.Primitives
import Core.TT
import Core.Value

import Data.IntMap
import Data.List
import Data.Maybe
import Data.Nat
import Data.Vect

%default covering

-- A pair of a term and its normal form. This could be constructed either
-- from a term (via 'gnf') or a normal form (via 'glueBack') but the other
-- part will only be constructed when needed, because it's in Core.
public export
data Glued : List Name -> Type where
     MkGlue : (fromTerm : Bool) -> -- is it built from the term; i.e. can
                                   -- we read the term straight back?
              Core (Term vars) -> (Ref Ctxt Defs -> Core (NF vars)) -> Glued vars

export
isFromTerm : Glued vars -> Bool
isFromTerm (MkGlue ft _ _) = ft

export
getTerm : Glued vars -> Core (Term vars)
getTerm (MkGlue _ tm _) = tm

export
getNF : {auto c : Ref Ctxt Defs} -> Glued vars -> Core (NF vars)
getNF {c} (MkGlue _ _ nf) = nf c

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

evalWithOpts : {auto c : Ref Ctxt Defs} ->
               {free, vars : _} ->
               Defs -> EvalOpts ->
               Env Term free -> LocalEnv free vars ->
               Term (vars ++ free) -> Stack free -> Core (NF free)

export
evalClosure : {auto c : Ref Ctxt Defs} ->
              {free : _} -> Defs -> Closure free -> Core (NF free)

export
evalArg : {auto c : Ref Ctxt Defs} -> {free : _} -> Defs -> Closure free -> Core (NF free)
evalArg defs c = evalClosure defs c

export
toClosure : EvalOpts -> Env Term outer -> Term outer -> Closure outer
toClosure opts env tm = MkClosure opts [] env tm

useMeta : Bool -> FC -> Name -> Defs -> EvalOpts -> Core (Maybe EvalOpts)
useMeta False _ _ _ opts = pure $ Just opts
useMeta True fc (Resolved i) defs opts
    = case lookup i (usedMetas opts) of
           Nothing => pure (Just (record { usedMetas $= insert i () } opts))
           Just _ => pure Nothing
useMeta True fc n defs opts
    = do let Just i = getNameID n (gamma defs)
              | Nothing => throw (UndefinedName fc n)
         useMeta True fc (Resolved i) defs opts

updateLimit : NameType -> Name -> EvalOpts -> Core (Maybe EvalOpts)
updateLimit Func n opts
    = if not (isNil (reduceLimit opts))
         then case lookup n (reduceLimit opts) of
                   Nothing => pure Nothing
                   Just Z => pure Nothing
                   Just (S k) =>
                      pure (Just (record { reduceLimit $= set n k } opts))
         else pure (Just opts)
  where
    set : Name -> Nat -> List (Name, Nat) -> List (Name, Nat)
    set n v [] = []
    set n v ((x, l) :: xs)
        = if x == n
             then (x, v) :: xs
             else (x, l) :: set n v xs
updateLimit t n opts = pure (Just opts)

data CaseResult a
     = Result a
     | NoMatch -- case alternative didn't match anything
     | GotStuck -- alternative matched, but got stuck later

parameters (defs : Defs, topopts : EvalOpts)
  mutual
    eval : {auto c : Ref Ctxt Defs} ->
           {free, vars : _} ->
           Env Term free -> LocalEnv free vars ->
           Term (vars ++ free) -> Stack free -> Core (NF free)
    eval env locs (Local fc mrig idx prf) stk
        = evalLocal env fc mrig idx prf stk locs
    eval env locs (Ref fc nt fn) stk
        = evalRef env False fc nt fn stk (NApp fc (NRef nt fn) stk)
    eval {vars} {free} env locs (Meta fc name idx args) stk
        = evalMeta env fc name idx (closeArgs args) stk
      where
        -- Yes, it's just a map, but specialising it by hand since we
        -- use this a *lot* and it saves the run time overhead of making
        -- a closure and calling APPLY.
        closeArgs : List (Term (vars ++ free)) -> List (Closure free)
        closeArgs [] = []
        closeArgs (t :: ts) = MkClosure topopts locs env t :: closeArgs ts
    eval env locs (Bind fc x (Lam _ r _ ty) scope) (thunk :: stk)
        = eval env (thunk :: locs) scope stk
    eval env locs (Bind fc x b@(Let _ r val ty) scope) stk
        = if (holesOnly topopts || argHolesOnly topopts) && not (tcInline topopts)
             then do b' <- traverse (\tm => eval env locs tm []) b
                     pure $ NBind fc x b'
                        (\defs', arg => evalWithOpts defs' topopts
                                                env (arg :: locs) scope stk)
             else eval env (MkClosure topopts locs env val :: locs) scope stk
    eval env locs (Bind fc x b scope) stk
        = do b' <- traverse (\tm => eval env locs tm []) b
             pure $ NBind fc x b'
                      (\defs', arg => evalWithOpts defs' topopts
                                              env (arg :: locs) scope stk)
    eval env locs (App fc fn arg) stk
        = eval env locs fn (MkClosure topopts locs env arg :: stk)
    eval env locs (As fc s n tm) stk
        = if removeAs topopts
             then eval env locs tm stk
             else do n' <- eval env locs n stk
                     tm' <- eval env locs tm stk
                     pure (NAs fc s n' tm')
    eval env locs (TDelayed fc r ty) stk
        = do ty' <- eval env locs ty stk
             pure (NDelayed fc r ty')
    eval env locs (TDelay fc r ty tm) stk
        = pure (NDelay fc r (MkClosure topopts locs env ty)
                            (MkClosure topopts locs env tm))
    eval env locs (TForce fc r tm) stk
        = do tm' <- eval env locs tm []
             case tm' of
                  NDelay fc r _ arg =>
                      eval env (arg :: locs) (Local {name = UN "fvar"} fc Nothing _ First) stk
                  _ => pure (NForce fc r tm' stk)
    eval env locs (PrimVal fc c) stk = pure $ NPrimVal fc c
    eval env locs (Erased fc i) stk = pure $ NErased fc i
    eval env locs (TType fc) stk = pure $ NType fc

    evalLocClosure : {auto c : Ref Ctxt Defs} ->
                     {free : _} ->
                     Env Term free ->
                     FC -> Maybe Bool ->
                     Stack free ->
                     Closure free ->
                     Core (NF free)
    evalLocClosure env fc mrig stk (MkClosure opts locs' env' tm')
        = evalWithOpts defs opts env' locs' tm' stk
    evalLocClosure {free} env fc mrig stk (MkNFClosure nf)
        = applyToStack nf stk
      where
        applyToStack : NF free -> Stack free -> Core (NF free)
        applyToStack (NBind fc _ (Lam _ _ _ _) sc) (arg :: stk)
            = do arg' <- sc defs arg
                 applyToStack arg' stk
        applyToStack (NApp fc (NRef nt fn) args) stk
            = evalRef env False fc nt fn (args ++ stk)
                      (NApp fc (NRef nt fn) args)
        applyToStack (NApp fc (NLocal mrig idx p) args) stk
          = evalLocal env fc mrig _ p (args ++ stk) []
        applyToStack (NDCon fc n t a args) stk
            = pure $ NDCon fc n t a (args ++ stk)
        applyToStack (NTCon fc n t a args) stk
            = pure $ NTCon fc n t a (args ++ stk)
        applyToStack nf _ = pure nf

    evalLocal : {auto c : Ref Ctxt Defs} ->
                {free, vars : _} ->
                Env Term free ->
                FC -> Maybe Bool ->
                (idx : Nat) -> (0 p : IsVar name idx (vars ++ free)) ->
                Stack free ->
                LocalEnv free vars ->
                Core (NF free)
    -- If it's one of the free variables, we are done unless the free
    -- variable maps to a let-binding
    evalLocal {vars = []} env fc mrig idx prf stk locs
        = if not (holesOnly topopts || argHolesOnly topopts)
             -- if we know it's not a let, no point in even running `getBinder`
             && fromMaybe True mrig
             then
               case getBinder prf env of
                    Let _ _ val _ => eval env [] val stk
                    _ => pure $ NApp fc (NLocal mrig idx prf) stk
             else pure $ NApp fc (NLocal mrig idx prf) stk
    evalLocal env fc mrig Z First stk (x :: locs)
        = evalLocClosure env fc mrig stk x
    evalLocal {vars = x :: xs} {free}
              env fc mrig (S idx) (Later p) stk (_ :: locs)
        = evalLocal {vars = xs} env fc mrig idx p stk locs

    updateLocal : (idx : Nat) -> (0 p : IsVar name idx (vars ++ free)) ->
                  LocalEnv free vars -> NF free ->
                  LocalEnv free vars
    updateLocal Z First (x :: locs) nf = MkNFClosure nf :: locs
    updateLocal (S idx) (Later p) (x :: locs) nf = x :: updateLocal idx p locs nf
    updateLocal _ _ locs nf = locs

    evalMeta : {auto c : Ref Ctxt Defs} ->
               {free : _} ->
               Env Term free ->
               FC -> Name -> Int -> List (Closure free) ->
               Stack free -> Core (NF free)
    evalMeta env fc nm i args stk
        = evalRef env True fc Func (Resolved i) (args ++ stk)
                  (NApp fc (NMeta nm i args) stk)

    evalRef : {auto c : Ref Ctxt Defs} ->
              {free : _} ->
              Env Term free ->
              (isMeta : Bool) ->
              FC -> NameType -> Name -> Stack free -> (def : Lazy (NF free)) ->
              Core (NF free)
    evalRef env meta fc (DataCon tag arity) fn stk def
        = pure $ NDCon fc fn tag arity stk
    evalRef env meta fc (TyCon tag arity) fn stk def
        = pure $ NTCon fc fn tag arity stk
    evalRef env meta fc Bound fn stk def
        = pure def
    evalRef env meta fc nt@Func n stk def
        = do Just res <- lookupCtxtExact n (gamma defs)
                  | Nothing => pure def
             let redok1 = evalAll topopts
             let redok2 = reducibleInAny (currentNS defs :: nestedNS defs)
                                         (fullname res)
                                         (visibility res)
             let redok = redok1 || redok2
             unless redok2 $ logC "eval.stuck" 5 $ pure $ "Stuck function: " ++ show !(toFullNames n)
             if redok
                then do
                   Just opts' <- useMeta (noCycles res) fc n defs topopts
                        | Nothing => pure def
                   Just opts' <- updateLimit nt n opts'
                        | Nothing => do log "eval.stuck" 10 $ "Function " ++ show n ++ " past reduction limit"
                                        pure def -- name is past reduction limit
                   evalDef env opts' meta fc
                           (multiplicity res) (definition res) (flags res) stk def
                else pure def

    getCaseBound : List (Closure free) ->
                   (args : List Name) ->
                   LocalEnv free more ->
                   Maybe (LocalEnv free (args ++ more))
    getCaseBound []            []        loc = Just loc
    getCaseBound []            (_ :: _)  loc = Nothing -- mismatched arg length
    getCaseBound (arg :: args) []        loc = Nothing -- mismatched arg length
    getCaseBound (arg :: args) (n :: ns) loc = (arg ::) <$> getCaseBound args ns loc

    evalConAlt : {auto c : Ref Ctxt Defs} ->
                 {more, free : _} ->
                 Env Term free ->
                 LocalEnv free more -> EvalOpts -> FC ->
                 Stack free ->
                 (args : List Name) ->
                 List (Closure free) ->
                 CaseTree (args ++ more) ->
                 Core (CaseResult (NF free))
    evalConAlt env loc opts fc stk args args' sc
         = do let Just bound = getCaseBound args' args loc
                   | Nothing => pure GotStuck
              evalTree env bound opts fc stk sc

    tryAlt : {auto c : Ref Ctxt Defs} ->
             {free, more : _} ->
             Env Term free ->
             LocalEnv free more -> EvalOpts -> FC ->
             Stack free -> NF free -> CaseAlt more ->
             Core (CaseResult (NF free))
    -- Ordinary constructor matching
    tryAlt {more} env loc opts fc stk (NDCon _ nm tag' arity args') (ConCase x tag args sc)
         = if tag == tag'
              then evalConAlt env loc opts fc stk args args' sc
              else pure NoMatch
    -- Type constructor matching, in typecase
    tryAlt {more} env loc opts fc stk (NTCon _ nm tag' arity args') (ConCase nm' tag args sc)
         = if nm == nm'
              then evalConAlt env loc opts fc stk args args' sc
              else pure NoMatch
    -- Primitive type matching, in typecase
    tryAlt env loc opts fc stk (NPrimVal _ c) (ConCase nm tag [] sc)
         = if UN (show c) == nm
              then evalTree env loc opts fc stk sc
              else pure NoMatch
    -- Type of type matching, in typecase
    tryAlt env loc opts fc stk (NType _) (ConCase (UN "Type") tag [] sc)
         = evalTree env loc opts fc stk sc
    -- Arrow matching, in typecase
    tryAlt {more}
           env loc opts fc stk (NBind pfc x (Pi fc' r e aty) scty) (ConCase (UN "->") tag [s,t] sc)
       = evalConAlt {more} env loc opts fc stk [s,t]
                  [MkNFClosure aty,
                   MkNFClosure (NBind pfc x (Lam fc' r e aty) scty)]
                  sc
    -- Delay matching
    tryAlt env loc opts fc stk (NDelay _ _ ty arg) (DelayCase tyn argn sc)
         = evalTree env (ty :: arg :: loc) opts fc stk sc
    -- Constant matching
    tryAlt env loc opts fc stk (NPrimVal _ c') (ConstCase c sc)
         = if c == c' then evalTree env loc opts fc stk sc
                      else pure NoMatch
    -- Default case matches against any *concrete* value
    tryAlt env loc opts fc stk val (DefaultCase sc)
         = if concrete val
              then evalTree env loc opts fc stk sc
              else pure GotStuck
      where
        concrete : NF free -> Bool
        concrete (NDCon _ _ _ _ _) = True
        concrete (NTCon _ _ _ _ _) = True
        concrete (NPrimVal _ _) = True
        concrete (NBind _ _ _ _) = True
        concrete (NType _) = True
        concrete _ = False
    tryAlt _ _ _ _ _ _ _ = pure GotStuck

    findAlt : {auto c : Ref Ctxt Defs} ->
              {args, free : _} ->
              Env Term free ->
              LocalEnv free args -> EvalOpts -> FC ->
              Stack free -> NF free -> List (CaseAlt args) ->
              Core (CaseResult (NF free))
    findAlt env loc opts fc stk val [] = do
      log "eval.casetree.stuck" 2 "Ran out of alternatives"
      pure GotStuck
    findAlt env loc opts fc stk val (x :: xs)
         = do Result val <- tryAlt env loc opts fc stk val x
                   | NoMatch => findAlt env loc opts fc stk val xs
                   | GotStuck => do
                       logC "eval.casetree.stuck" 5 $
                         pure $ "Got stuck matching " ++ show val ++ " against " ++ show !(toFullNames x)
                       pure GotStuck
              pure (Result val)

    evalTree : {auto c : Ref Ctxt Defs} ->
               {args, free : _} -> Env Term free -> LocalEnv free args ->
               EvalOpts -> FC ->
               Stack free -> CaseTree args ->
               Core (CaseResult (NF free))
    evalTree env loc opts fc stk (Case {name} idx x _ alts)
      = do xval <- evalLocal env fc Nothing idx (varExtend x) [] loc
           -- we have not defined quote yet (it depends on eval itself) so we show the NF
           -- i.e. only the top-level constructor.
           log "eval.casetree" 5 $ "Evaluated " ++ show name ++ " to " ++ show xval
           let loc' = updateLocal idx (varExtend x) loc xval
           findAlt env loc' opts fc stk xval alts
    evalTree env loc opts fc stk (STerm _ tm)
          = case fuel opts of
                 Nothing => do res <- evalWithOpts defs opts env loc (embed tm) stk
                               pure (Result res)
                 Just Z => pure GotStuck
                 Just (S k) =>
                      do let opts' = record { fuel = Just k } opts
                         res <- evalWithOpts defs opts' env loc (embed tm) stk
                         pure (Result res)
    evalTree env loc opts fc stk _ = pure GotStuck

    -- Take arguments from the stack, as long as there's enough.
    -- Returns the arguments, and the rest of the stack
    takeFromStack : (arity : Nat) -> Stack free ->
                    Maybe (Vect arity (Closure free), Stack free)
    takeFromStack arity stk = takeStk arity stk []
      where
        takeStk : (remain : Nat) -> Stack free ->
                  Vect got (Closure free) ->
                  Maybe (Vect (got + remain) (Closure free), Stack free)
        takeStk {got} Z stk acc = Just (rewrite plusZeroRightNeutral got in
                                    reverse acc, stk)
        takeStk (S k) [] acc = Nothing
        takeStk {got} (S k) (arg :: stk) acc
           = rewrite sym (plusSuccRightSucc got k) in
                     takeStk k stk (arg :: acc)

    argsFromStack : (args : List Name) ->
                    Stack free ->
                    Maybe (LocalEnv free args, Stack free)
    argsFromStack [] stk = Just ([], stk)
    argsFromStack (n :: ns) [] = Nothing
    argsFromStack (n :: ns) (arg :: args)
         = do (loc', stk') <- argsFromStack ns args
              pure (arg :: loc', stk')

    evalOp : {auto c : Ref Ctxt Defs} ->
             {arity, free : _} ->
             (Vect arity (NF free) -> Maybe (NF free)) ->
             Stack free -> (def : Lazy (NF free)) ->
             Core (NF free)
    evalOp {arity} fn stk def
        = case takeFromStack arity stk of
               -- Stack must be exactly the right height
               Just (args, []) =>
                  do argsnf <- evalAll args
                     case fn argsnf of
                          Nothing => pure def
                          Just res => pure res
               _ => pure def
      where
        -- No traverse for Vect in Core...
        evalAll : Vect n (Closure free) -> Core (Vect n (NF free))
        evalAll [] = pure []
        evalAll (c :: cs) = pure $ !(evalClosure defs c) :: !(evalAll cs)

    evalDef : {auto c : Ref Ctxt Defs} ->
              {free : _} ->
              Env Term free -> EvalOpts ->
              (isMeta : Bool) -> FC ->
              RigCount -> Def -> List DefFlag ->
              Stack free -> (def : Lazy (NF free)) ->
              Core (NF free)
    evalDef env opts meta fc rigd (PMDef r args tree _ _) flags stk def
       -- If evaluating the definition fails (e.g. due to a case being
       -- stuck) return the default.
       -- We can use the definition if one of the following is true:
       --   + The 'alwayReduce' flag (r) is set
       --   + We're not in 'holesOnly', 'argHolesOnly' or 'tcInline'
       --         (that's the default mode)
       --   + It's a metavariable and not in Rig0
       --   + It's a metavariable and we're not in 'argHolesOnly'
       --   + It's inlinable and we're in 'tcInline'
        = if alwaysReduce r
             || (not (holesOnly opts || argHolesOnly opts || tcInline opts))
             || (meta && not (isErased rigd))
             || (meta && holesOnly opts)
             || (tcInline opts && elem TCInline flags)
             then case argsFromStack args stk of
                       Nothing => pure def
                       Just (locs', stk') =>
                            do Result res <- evalTree env locs' opts fc stk' tree
                                    | _ => pure def
                               pure res
             else pure def
    evalDef env opts meta fc rigd (Builtin op) flags stk def
        = evalOp (getOp op) stk def
    -- All other cases, use the default value, which is already applied to
    -- the stack
    evalDef env opts _ _ _ _ _ stk def = pure def

-- Make sure implicit argument order is right... 'vars' is used so we'll
-- write it explicitly, but it does appear after the parameters in 'eval'!
evalWithOpts {vars} defs opts = eval {vars} defs opts

evalClosure defs (MkClosure opts locs env tm)
    = eval defs opts env locs tm []
evalClosure defs (MkNFClosure nf) = pure nf

export
nf : {auto c : Ref Ctxt Defs} ->
     {vars : _} ->
     Defs -> Env Term vars -> Term vars -> Core (NF vars)
nf defs env tm = eval defs defaultOpts env [] tm []

export
nfOpts : {auto c : Ref Ctxt Defs} ->
         {vars : _} ->
         EvalOpts -> Defs -> Env Term vars -> Term vars -> Core (NF vars)
nfOpts opts defs env tm = eval defs opts env [] tm []

export
gnf : {vars : _} ->
      Env Term vars -> Term vars -> Glued vars
gnf env tm
    = MkGlue True
             (pure tm)
             (\c => do defs <- get Ctxt
                       nf defs env tm)

export
gnfOpts : {vars : _} ->
          EvalOpts -> Env Term vars -> Term vars -> Glued vars
gnfOpts opts env tm
    = MkGlue True
             (pure tm)
             (\c => do defs <- get Ctxt
                       nfOpts opts defs env tm)

export
gType : FC -> Glued vars
gType fc = MkGlue True (pure (TType fc)) (const (pure (NType fc)))

export
gErased : FC -> Glued vars
gErased fc = MkGlue True (pure (Erased fc False)) (const (pure (NErased fc False)))

export
data QVar : Type where

public export
interface Quote (tm : List Name -> Type) where
    quote : {auto c : Ref Ctxt Defs} ->
            {vars : _} ->
            Defs -> Env Term vars -> tm vars -> Core (Term vars)
    quoteGen : {auto c : Ref Ctxt Defs} ->
               {vars : _} ->
               Ref QVar Int -> Defs -> Env Term vars -> tm vars -> Core (Term vars)

    quote defs env tm
        = do q <- newRef QVar 0
             quoteGen q defs env tm

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

mutual
  quoteArgs : {auto c : Ref Ctxt Defs} ->
              {bound, free : _} ->
              Ref QVar Int -> Defs -> Bounds bound ->
              Env Term free -> List (Closure free) ->
              Core (List (Term (bound ++ free)))
  quoteArgs q defs bounds env [] = pure []
  quoteArgs q defs bounds env (a :: args)
      = pure $ (!(quoteGenNF q defs bounds env !(evalClosure defs a)) ::
                !(quoteArgs q defs bounds env args))

  quoteHead : {auto c : Ref Ctxt Defs} ->
              {bound, free : _} ->
              Ref QVar Int -> Defs ->
              FC -> Bounds bound -> Env Term free -> NHead free ->
              Core (Term (bound ++ free))
  quoteHead {bound} q defs fc bounds env (NLocal mrig _ prf)
      = let MkVar prf' = addLater bound prf in
            pure $ Local fc mrig _ prf'
    where
      addLater : {idx : _} ->
                 (ys : List Name) -> (0 p : IsVar n idx xs) ->
                 Var (ys ++ xs)
      addLater [] isv = MkVar isv
      addLater (x :: xs) isv
          = let MkVar isv' = addLater xs isv in
                MkVar (Later isv')
  quoteHead q defs fc bounds env (NRef Bound (MN n i))
      = case findName bounds of
             Just (MkVar p) => pure $ Local fc Nothing _ (varExtend p)
             Nothing => pure $ Ref fc Bound (MN n i)
    where
      findName : Bounds bound' -> Maybe (Var bound')
      findName None = Nothing
      findName (Add x (MN n' i') ns)
          = if i == i' -- this uniquely identifies it, given how we
                       -- generated the names, and is a faster test!
               then Just (MkVar First)
               else do MkVar p <-findName ns
                       Just (MkVar (Later p))
      findName (Add x _ ns)
          = do MkVar p <-findName ns
               Just (MkVar (Later p))
  quoteHead q defs fc bounds env (NRef nt n) = pure $ Ref fc nt n
  quoteHead q defs fc bounds env (NMeta n i args)
      = do args' <- quoteArgs q defs bounds env args
           pure $ Meta fc n i args'

  quotePi : {auto c : Ref Ctxt Defs} ->
            {bound, free : _} ->
            Ref QVar Int -> Defs -> Bounds bound ->
            Env Term free -> PiInfo (NF free) ->
            Core (PiInfo (Term (bound ++ free)))
  quotePi q defs bounds env Explicit = pure Explicit
  quotePi q defs bounds env Implicit = pure Implicit
  quotePi q defs bounds env AutoImplicit = pure AutoImplicit
  quotePi q defs bounds env (DefImplicit t)
      = do t' <- quoteGenNF q defs bounds env t
           pure (DefImplicit t')

  quoteBinder : {auto c : Ref Ctxt Defs} ->
                {bound, free : _} ->
                Ref QVar Int -> Defs -> Bounds bound ->
                Env Term free -> Binder (NF free) ->
                Core (Binder (Term (bound ++ free)))
  quoteBinder q defs bounds env (Lam fc r p ty)
      = do ty' <- quoteGenNF q defs bounds env ty
           p' <- quotePi q defs bounds env p
           pure (Lam fc r p' ty')
  quoteBinder q defs bounds env (Let fc r val ty)
      = do val' <- quoteGenNF q defs bounds env val
           ty' <- quoteGenNF q defs bounds env ty
           pure (Let fc r val' ty')
  quoteBinder q defs bounds env (Pi fc r p ty)
      = do ty' <- quoteGenNF q defs bounds env ty
           p' <- quotePi q defs bounds env p
           pure (Pi fc r p' ty')
  quoteBinder q defs bounds env (PVar fc r p ty)
      = do ty' <- quoteGenNF q defs bounds env ty
           p' <- quotePi q defs bounds env p
           pure (PVar fc r p' ty')
  quoteBinder q defs bounds env (PLet fc r val ty)
      = do val' <- quoteGenNF q defs bounds env val
           ty' <- quoteGenNF q defs bounds env ty
           pure (PLet fc r val' ty')
  quoteBinder q defs bounds env (PVTy fc r ty)
      = do ty' <- quoteGenNF q defs bounds env ty
           pure (PVTy fc r ty')

  quoteGenNF : {auto c : Ref Ctxt Defs} ->
               {bound, vars : _} ->
               Ref QVar Int ->
               Defs -> Bounds bound ->
               Env Term vars -> NF vars -> Core (Term (bound ++ vars))
  quoteGenNF q defs bound env (NBind fc n b sc)
      = do var <- genName "qv"
           sc' <- quoteGenNF q defs (Add n var bound) env
                       !(sc defs (toClosure defaultOpts env (Ref fc Bound var)))
           b' <- quoteBinder q defs bound env b
           pure (Bind fc n b' sc')
  quoteGenNF q defs bound env (NApp fc f args)
      = do f' <- quoteHead q defs fc bound env f
           args' <- quoteArgs q defs bound env args
           pure $ apply fc f' args'
  quoteGenNF q defs bound env (NDCon fc n t ar args)
      = do args' <- quoteArgs q defs bound env args
           pure $ apply fc (Ref fc (DataCon t ar) n) args'
  quoteGenNF q defs bound env (NTCon fc n t ar args)
      = do args' <- quoteArgs q defs bound env args
           pure $ apply fc (Ref fc (TyCon t ar) n) args'
  quoteGenNF q defs bound env (NAs fc s n pat)
      = do n' <- quoteGenNF q defs bound env n
           pat' <- quoteGenNF q defs bound env pat
           pure (As fc s n' pat')
  quoteGenNF q defs bound env (NDelayed fc r arg)
      = do argQ <- quoteGenNF q defs bound env arg
           pure (TDelayed fc r argQ)
  quoteGenNF q defs bound env (NDelay fc r ty arg)
      = do argNF <- evalClosure defs (toHolesOnly arg)
           argQ <- quoteGenNF q defs bound env argNF
           tyNF <- evalClosure defs (toHolesOnly ty)
           tyQ <- quoteGenNF q defs bound env tyNF
           pure (TDelay fc r tyQ argQ)
    where
      toHolesOnly : Closure vs -> Closure vs
      toHolesOnly (MkClosure opts locs env tm)
          = MkClosure (record { holesOnly = True,
                                argHolesOnly = True } opts)
                      locs env tm
      toHolesOnly c = c
  quoteGenNF q defs bound env (NForce fc r arg args)
      = do args' <- quoteArgs q defs bound env args
           case arg of
                NDelay fc _ _ arg =>
                   do argNF <- evalClosure defs arg
                      pure $ apply fc !(quoteGenNF q defs bound env argNF) args'
                _ => do arg' <- quoteGenNF q defs bound env arg
                        pure $ apply fc (TForce fc r arg') args'
  quoteGenNF q defs bound env (NPrimVal fc c) = pure $ PrimVal fc c
  quoteGenNF q defs bound env (NErased fc i) = pure $ Erased fc i
  quoteGenNF q defs bound env (NType fc) = pure $ TType fc

export
Quote NF where
  quoteGen q defs env tm = quoteGenNF q defs None env tm

export
Quote Term where
  quoteGen q defs env tm = pure tm

export
Quote Closure where
  quoteGen q defs env c = quoteGen q defs env !(evalClosure defs c)

export
glueBack : {auto c : Ref Ctxt Defs} ->
           {vars : _} ->
           Defs -> Env Term vars -> NF vars -> Glued vars
glueBack defs env nf
    = MkGlue False
             (do empty <- clearDefs defs
                 quote empty env nf)
             (const (pure nf))

export
normalise : {auto c : Ref Ctxt Defs} ->
            {free : _} ->
            Defs -> Env Term free -> Term free -> Core (Term free)
normalise defs env tm = quote defs env !(nf defs env tm)

export
normaliseOpts : {auto c : Ref Ctxt Defs} ->
                {free : _} ->
                EvalOpts -> Defs -> Env Term free -> Term free -> Core (Term free)
normaliseOpts opts defs env tm
    = quote defs env !(nfOpts opts defs env tm)

export
normaliseHoles : {auto c : Ref Ctxt Defs} ->
                 {free : _} ->
                 Defs -> Env Term free -> Term free -> Core (Term free)
normaliseHoles defs env tm
    = quote defs env !(nfOpts withHoles defs env tm)

export
normaliseLHS : {auto c : Ref Ctxt Defs} ->
               {free : _} ->
               Defs -> Env Term free -> Term free -> Core (Term free)
normaliseLHS defs env (Bind fc n b sc)
    = pure $ Bind fc n b !(normaliseLHS defs (b :: env) sc)
normaliseLHS defs env tm
    = quote defs env !(nfOpts onLHS defs env tm)

export
normaliseArgHoles : {auto c : Ref Ctxt Defs} ->
                    {free : _} ->
                    Defs -> Env Term free -> Term free -> Core (Term free)
normaliseArgHoles defs env tm
    = quote defs env !(nfOpts withArgHoles defs env tm)

export
normaliseAll : {auto c : Ref Ctxt Defs} ->
               {free : _} ->
               Defs -> Env Term free -> Term free -> Core (Term free)
normaliseAll defs env tm
    = quote defs env !(nfOpts withAll defs env tm)

-- Normalise, but without normalising the types of binders. Dealing with
-- binders is the slow part of normalisation so whenever we can avoid it, it's
-- a big win
export
normaliseScope : {auto c : Ref Ctxt Defs} ->
                 {free : _} ->
                 Defs -> Env Term free -> Term free -> Core (Term free)
normaliseScope defs env (Bind fc n b sc)
    = pure $ Bind fc n b !(normaliseScope defs (b :: env) sc)
normaliseScope defs env tm = normalise defs env tm

export
etaContract : {auto _ : Ref Ctxt Defs} ->
              {vars : _} -> Term vars -> Core (Term vars)
etaContract tm = do
  defs <- get Ctxt
  logTerm "eval.eta" 5 "Attempting to eta contract subterms of" tm
  nf <- normalise defs (mkEnv EmptyFC _) tm
  logTerm "eval.eta" 5 "Evaluated to" nf
  res <- mapTermM act tm
  logTerm "eval.eta" 5 "Result of eta-contraction" res
  pure res

   where

    act : {vars : _} -> Term vars -> Core (Term vars)
    act tm = do
      logTerm "eval.eta" 10 "  Considering" tm
      case tm of
        (Bind _ x (Lam _ _ _ _) (App _ fn (Local _ _ Z _))) => do
          logTerm "eval.eta" 10 "  Shrinking candidate" fn
          let shrunk = shrinkTerm fn (DropCons SubRefl)
          case shrunk of
            Nothing => do
              log "eval.eta" 10 "  Failure!"
              pure tm
            Just tm' => do
              logTerm "eval.eta" 10 "  Success!" tm'
              pure tm'
        _ => pure tm

public export
interface Convert (tm : List Name -> Type) where
  convert : {auto c : Ref Ctxt Defs} ->
            {vars : _} ->
            Defs -> Env Term vars ->
            tm vars -> tm vars -> Core Bool
  convGen : {auto c : Ref Ctxt Defs} ->
            {vars : _} ->
            Ref QVar Int ->
            Defs -> Env Term vars ->
            tm vars -> tm vars -> Core Bool

  convert defs env tm tm'
      = do q <- newRef QVar 0
           convGen q defs env tm tm'

tryUpdate : {vars, vars' : _} ->
            List (Var vars, Var vars') ->
            Term vars -> Maybe (Term vars')
tryUpdate ms (Local fc l idx p)
    = do MkVar p' <- findIdx ms idx
         pure $ Local fc l _ p'
  where
    findIdx : List (Var vars, Var vars') -> Nat -> Maybe (Var vars')
    findIdx [] _ = Nothing
    findIdx ((MkVar {i} _, v) :: ps) n
        = if i == n then Just v else findIdx ps n
tryUpdate ms (Ref fc nt n) = pure $ Ref fc nt n
tryUpdate ms (Meta fc n i args) = pure $ Meta fc n i !(traverse (tryUpdate ms) args)
tryUpdate ms (Bind fc x b sc)
    = do b' <- tryUpdateB b
         pure $ Bind fc x b' !(tryUpdate (map weakenP ms) sc)
  where
    tryUpdatePi : PiInfo (Term vars) -> Maybe (PiInfo (Term vars'))
    tryUpdatePi Explicit = pure Explicit
    tryUpdatePi Implicit = pure Implicit
    tryUpdatePi AutoImplicit = pure AutoImplicit
    tryUpdatePi (DefImplicit t) = pure $ DefImplicit !(tryUpdate ms t)

    tryUpdateB : Binder (Term vars) -> Maybe (Binder (Term vars'))
    tryUpdateB (Lam fc r p t) = pure $ Lam fc r !(tryUpdatePi p) !(tryUpdate ms t)
    tryUpdateB (Let fc r v t) = pure $ Let fc r !(tryUpdate ms v) !(tryUpdate ms t)
    tryUpdateB (Pi fc r p t) = pure $ Pi fc r !(tryUpdatePi p) !(tryUpdate ms t)
    tryUpdateB _ = Nothing

    weakenP : {n : _} -> (Var vars, Var vars') ->
              (Var (n :: vars), Var (n :: vars'))
    weakenP (v, vs) = (weaken v, weaken vs)
tryUpdate ms (App fc f a) = pure $ App fc !(tryUpdate ms f) !(tryUpdate ms a)
tryUpdate ms (As fc s a p) = pure $ As fc s !(tryUpdate ms a) !(tryUpdate ms p)
tryUpdate ms (TDelayed fc r tm) = pure $ TDelayed fc r !(tryUpdate ms tm)
tryUpdate ms (TDelay fc r ty tm) = pure $ TDelay fc r !(tryUpdate ms ty) !(tryUpdate ms tm)
tryUpdate ms (TForce fc r tm) = pure $ TForce fc r !(tryUpdate ms tm)
tryUpdate ms (PrimVal fc c) = pure $ PrimVal fc c
tryUpdate ms (Erased fc i) = pure $ Erased fc i
tryUpdate ms (TType fc) = pure $ TType fc

mutual
  allConv : {auto c : Ref Ctxt Defs} ->
            {vars : _} ->
            Ref QVar Int -> Defs -> Env Term vars ->
            List (Closure vars) -> List (Closure vars) -> Core Bool
  allConv q defs env [] [] = pure True
  allConv q defs env (x :: xs) (y :: ys)
      = pure $ !(convGen q defs env x y) && !(allConv q defs env xs ys)
  allConv q defs env _ _ = pure False

  -- If the case trees match in structure, get the list of variables which
  -- have to match in the call
  getMatchingVarAlt : {auto c : Ref Ctxt Defs} ->
                      {args, args' : _} ->
                      Defs ->
                      List (Var args, Var args') ->
                      CaseAlt args -> CaseAlt args' ->
                      Core (Maybe (List (Var args, Var args')))
  getMatchingVarAlt defs ms (ConCase n tag cargs t) (ConCase n' tag' cargs' t')
      = if n == n'
           then do let Just ms' = extend cargs cargs' ms
                        | Nothing => pure Nothing
                   Just ms <- getMatchingVars defs ms' t t'
                        | Nothing => pure Nothing
                   -- drop the prefix from cargs/cargs' since they won't
                   -- be in the caller
                   pure (Just (mapMaybe (dropP cargs cargs') ms))
           else pure Nothing
    where
      weakenP : {c, c', args, args' : _} ->
                (Var args, Var args') ->
                (Var (c :: args), Var (c' :: args'))
      weakenP (v, vs) = (weaken v, weaken vs)

      extend : (cs : List Name) -> (cs' : List Name) ->
               (List (Var args, Var args')) ->
               Maybe (List (Var (cs ++ args), Var (cs' ++ args')))
      extend [] [] ms = pure ms
      extend (c :: cs) (c' :: cs') ms
          = do rest <- extend cs cs' ms
               pure ((MkVar First, MkVar First) :: map weakenP rest)
      extend _ _ _ = Nothing

      dropV : forall args .
              (cs : List Name) -> Var (cs ++ args) -> Maybe (Var args)
      dropV [] v = Just v
      dropV (c :: cs) (MkVar First) = Nothing
      dropV (c :: cs) (MkVar (Later x))
          = dropV cs (MkVar x)

      dropP : (cs : List Name) -> (cs' : List Name) ->
              (Var (cs ++ args), Var (cs' ++ args')) ->
              Maybe (Var args, Var args')
      dropP cs cs' (x, y) = pure (!(dropV cs x), !(dropV cs' y))

  getMatchingVarAlt defs ms (ConstCase c t) (ConstCase c' t')
      = if c == c'
           then getMatchingVars defs ms t t'
           else pure Nothing
  getMatchingVarAlt defs ms (DefaultCase t) (DefaultCase t')
      = getMatchingVars defs ms t t'
  getMatchingVarAlt defs _ _ _ = pure Nothing

  getMatchingVarAlts : {auto c : Ref Ctxt Defs} ->
                       {args, args' : _} ->
                       Defs ->
                       List (Var args, Var args') ->
                       List (CaseAlt args) -> List (CaseAlt args') ->
                       Core (Maybe (List (Var args, Var args')))
  getMatchingVarAlts defs ms [] [] = pure (Just ms)
  getMatchingVarAlts defs ms (a :: as) (a' :: as')
      = do Just ms <- getMatchingVarAlt defs ms a a'
                | Nothing => pure Nothing
           getMatchingVarAlts defs ms as as'
  getMatchingVarAlts defs _ _ _ = pure Nothing

  getMatchingVars : {auto c : Ref Ctxt Defs} ->
                    {args, args' : _} ->
                    Defs ->
                    List (Var args, Var args') ->
                    CaseTree args -> CaseTree args' ->
                    Core (Maybe (List (Var args, Var args')))
  getMatchingVars defs ms (Case _ p _ alts) (Case _ p' _ alts')
      = getMatchingVarAlts defs ((MkVar p, MkVar p') :: ms) alts alts'
  getMatchingVars defs ms (STerm i tm) (STerm i' tm')
      = do let Just tm'' = tryUpdate ms tm
               | Nothing => pure Nothing
           if !(convert defs (mkEnv (getLoc tm) args') tm'' tm')
              then pure (Just ms)
              else pure Nothing
  getMatchingVars defs ms (Unmatched _) (Unmatched _) = pure (Just ms)
  getMatchingVars defs ms Impossible Impossible = pure (Just ms)
  getMatchingVars _ _ _ _ = pure Nothing

  chkSameDefs : {auto c : Ref Ctxt Defs} ->
                {vars : _} ->
                Ref QVar Int -> Defs -> Env Term vars ->
                Name -> Name ->
                List (Closure vars) -> List (Closure vars) -> Core Bool
  chkSameDefs q defs env n n' nargs nargs'
     = do Just (PMDef _ args ct rt _) <- lookupDefExact n (gamma defs)
               | _ => pure False
          Just (PMDef _ args' ct' rt' _) <- lookupDefExact n' (gamma defs)
               | _ => pure False

          -- If the two case blocks match in structure, get which variables
          -- correspond. If corresponding variables convert, the two case
          -- blocks convert.
          Just ms <- getMatchingVars defs [] ct ct'
               | Nothing => pure False
          convertMatches ms
     where
       -- We've only got the index into the argument list, and the indices
       -- don't match up, which is annoying. But it'll always be there!
       getArgPos : Nat -> List (Closure vars) -> Maybe (Closure vars)
       getArgPos _ [] = Nothing
       getArgPos Z (c :: cs) = pure c
       getArgPos (S k) (c :: cs) = getArgPos k cs

       convertMatches : {vs, vs' : _} ->
                        List (Var vs, Var vs') ->
                        Core Bool
       convertMatches [] = pure True
       convertMatches ((MkVar {i} p, MkVar {i=i'} p') :: vs)
          = do let Just varg = getArgPos i nargs
                   | Nothing => pure False
               let Just varg' = getArgPos i' nargs'
                   | Nothing => pure False
               pure $ !(convGen q defs env varg varg') &&
                      !(convertMatches vs)

  -- If two names are standing for case blocks, check the blocks originate
  -- from the same place, and have the same scrutinee
  chkConvCaseBlock : {auto c : Ref Ctxt Defs} ->
                     {vars : _} ->
                     FC -> Ref QVar Int -> Defs -> Env Term vars ->
                     NHead vars -> List (Closure vars) ->
                     NHead vars -> List (Closure vars) -> Core Bool
  chkConvCaseBlock fc q defs env (NRef _ n) nargs (NRef _ n') nargs'
      = do NS _ (CaseBlock _ _) <- full (gamma defs) n
              | _ => pure False
           NS _ (CaseBlock _ _) <- full (gamma defs) n'
              | _ => pure False
           False <- chkSameDefs q defs env n n' nargs nargs'
              | True => pure True
           -- both case operators. Due to the way they're elaborated, two
           -- blocks might arise from the same source but have different
           -- names. So we consider them the same if the scrutinees convert,
           -- and the functions are defined at the same location. This is a
           -- bit of a hack - and relies on the location being stored in the
           -- term accurately - but otherwise it's a quick way to find out!
           Just def <- lookupCtxtExact n (gamma defs)
                | _ => pure False
           Just def' <- lookupCtxtExact n' (gamma defs)
                | _ => pure False
           let PMDef _ _ tree _ _ = definition def
                | _ => pure False
           let PMDef _ _ tree' _ _ = definition def'
                | _ => pure False
           let Just scpos = findArgPos tree
                | Nothing => pure False
           let Just scpos' = findArgPos tree'
                | Nothing => pure False
           let Just sc = getScrutinee scpos nargs
                | Nothing => pure False
           let Just sc' = getScrutinee scpos' nargs'
                | Nothing => pure False
           convGen q defs env sc sc'
           pure (location def == location def')
    where
      -- Need to find the position of the scrutinee to see if they are the
      -- same
      findArgPos : CaseTree as -> Maybe Nat
      findArgPos (Case idx p _ _) = Just idx
      findArgPos _ = Nothing

      getScrutinee : Nat -> List (Closure vs) -> Maybe (Closure vs)
      getScrutinee Z (x :: xs) = Just x
      getScrutinee (S k) (x :: xs) = getScrutinee k xs
      getScrutinee _ _ = Nothing
  chkConvCaseBlock _ _ _ _ _ _ _ _ = pure False

  chkConvHead : {auto c : Ref Ctxt Defs} ->
                {vars : _} ->
                Ref QVar Int -> Defs -> Env Term vars ->
                NHead vars -> NHead vars -> Core Bool
  chkConvHead q defs env (NLocal _ idx _) (NLocal _ idx' _) = pure $ idx == idx'
  chkConvHead q defs env (NRef _ n) (NRef _ n') = pure $ n == n'
  chkConvHead q defs env (NMeta n i args) (NMeta n' i' args')
     = if i == i'
          then allConv q defs env args args'
          else pure False
  chkConvHead q defs env _ _ = pure False

  -- Comparing multiplicities when converting pi binders
  subRig : RigCount -> RigCount -> Bool
  subRig x y = (isLinear x && isRigOther y) ||
               x == y

  convBinders : {auto c : Ref Ctxt Defs} ->
                {vars : _} ->
                Ref QVar Int -> Defs -> Env Term vars ->
                Binder (NF vars) -> Binder (NF vars) -> Core Bool
  convBinders q defs env (Pi _ cx ix tx) (Pi _ cy iy ty)
      = if not (subRig cx cy)
           then pure False
           else convGen q defs env tx ty
  convBinders q defs env (Lam _ cx ix tx) (Lam _ cy iy ty)
      = if cx /= cy
           then pure False
           else convGen q defs env tx ty
  convBinders q defs env bx by
      = if multiplicity bx /= multiplicity by
           then pure False
           else convGen q defs env (binderType bx) (binderType by)

  export
  Convert NF where
    convGen q defs env (NBind fc x b sc) (NBind _ x' b' sc')
        = do var <- genName "conv"
             let c = MkClosure defaultOpts [] env (Ref fc Bound var)
             bok <- convBinders q defs env b b'
             if bok
                then do bsc <- sc defs c
                        bsc' <- sc' defs c
                        convGen q defs env bsc bsc'
                else pure False

    convGen q defs env tmx@(NBind fc x (Lam fc' c ix tx) scx) tmy
        = do empty <- clearDefs defs
             etay <- nf defs env
                        (Bind fc x (Lam fc' c !(traverse (quote empty env) ix) !(quote empty env tx))
                           (App fc (weaken !(quote empty env tmy))
                                (Local fc Nothing _ First)))
             convGen q defs env tmx etay
    convGen q defs env tmx tmy@(NBind fc y (Lam fc' c iy ty) scy)
        = do empty <- clearDefs defs
             etax <- nf defs env
                        (Bind fc y (Lam fc' c !(traverse (quote empty env) iy) !(quote empty env ty))
                           (App fc (weaken !(quote empty env tmx))
                                (Local fc Nothing _ First)))
             convGen q defs env etax tmy

    convGen q defs env (NApp fc val args) (NApp _ val' args')
        = if !(chkConvHead q defs env val val')
             then allConv q defs env args args'
             else chkConvCaseBlock fc q defs env val args val' args'

    convGen q defs env (NDCon _ nm tag _ args) (NDCon _ nm' tag' _ args')
        = if tag == tag'
             then allConv q defs env args args'
             else pure False
    convGen q defs env (NTCon _ nm tag _ args) (NTCon _ nm' tag' _ args')
        = if nm == nm'
             then allConv q defs env args args'
             else pure False
    convGen q defs env (NAs _ _ _ tm) (NAs _ _ _ tm')
        = convGen q defs env tm tm'

    convGen q defs env (NDelayed _ r arg) (NDelayed _ r' arg')
        = if compatible r r'
             then convGen q defs env arg arg'
             else pure False
    convGen q defs env (NDelay _ r _ arg) (NDelay _ r' _ arg')
        = if compatible r r'
             then do -- if it's codata, don't reduce the argument or we might
                     -- go for ever, if it's infinite
                     adefs <- case r of
                                   LLazy => pure defs
                                   _ => clearDefs defs
                     convGen q adefs env arg arg'
             else pure False
    convGen q defs env (NForce _ r arg args) (NForce _ r' arg' args')
        = if compatible r r'
             then if !(convGen q defs env arg arg')
                     then allConv q defs env args args'
                     else pure False
             else pure False

    convGen q defs env (NPrimVal _ c) (NPrimVal _ c') = pure (c == c')
    convGen q defs env (NErased _ _) _ = pure True
    convGen q defs env _ (NErased _ _) = pure True
    convGen q defs env (NType _) (NType _) = pure True
    convGen q defs env x y = pure False

  export
  Convert Term where
    convGen q defs env x y
        = convGen q defs env !(nf defs env x) !(nf defs env y)

  export
  Convert Closure where
    convGen q defs env x y
        = convGen q defs env !(evalClosure defs x) !(evalClosure defs y)

export
getValArity : Defs -> Env Term vars -> NF vars -> Core Nat
getValArity defs env (NBind fc x (Pi _ _ _ _) sc)
    = pure (S !(getValArity defs env !(sc defs (toClosure defaultOpts env (Erased fc False)))))
getValArity defs env val = pure 0

export
getArity : {auto c : Ref Ctxt Defs} ->
           {vars : _} ->
           Defs -> Env Term vars -> Term vars -> Core Nat
getArity defs env tm = getValArity defs env !(nf defs env tm)

-- Log message with a value, translating back to human readable names first
export
logNF : {vars : _} ->
        {auto c : Ref Ctxt Defs} ->
        String -> Nat -> Lazy String -> Env Term vars -> NF vars -> Core ()
logNF str n msg env tmnf
    = do opts <- getSession
         let lvl = mkLogLevel str n
         if keepLog lvl (logLevel opts)
            then do defs <- get Ctxt
                    tm <- quote defs env tmnf
                    tm' <- toFullNames tm
                    coreLift $ putStrLn $ "LOG " ++ show lvl ++ ": " ++ msg
                                          ++ ": " ++ show tm'
            else pure ()

-- Log message with a term, reducing holes and translating back to human
-- readable names first
export
logTermNF' : {vars : _} ->
             {auto c : Ref Ctxt Defs} ->
             LogLevel -> Lazy String -> Env Term vars -> Term vars -> Core ()
logTermNF' lvl msg env tm
    = do opts <- getSession
         if keepLog lvl (logLevel opts)
            then do defs <- get Ctxt
                    tmnf <- normaliseHoles defs env tm
                    tm' <- toFullNames tmnf
                    coreLift $ putStrLn $ "LOG " ++ show lvl ++ ": " ++ msg
                                          ++ ": " ++ show tm'
            else pure ()

export
logTermNF : {vars : _} ->
            {auto c : Ref Ctxt Defs} ->
            String -> Nat -> Lazy String -> Env Term vars -> Term vars -> Core ()
logTermNF str n msg env tm
    = do let lvl = mkLogLevel str n
         logTermNF' lvl msg env tm

export
logGlue : {vars : _} ->
          {auto c : Ref Ctxt Defs} ->
          String -> Nat -> Lazy String -> Env Term vars -> Glued vars -> Core ()
logGlue str n msg env gtm
    = do opts <- getSession
         let lvl = mkLogLevel str n
         if keepLog lvl (logLevel opts)
            then do defs <- get Ctxt
                    tm <- getTerm gtm
                    tm' <- toFullNames tm
                    coreLift $ putStrLn $ "LOG " ++ show lvl ++ ": " ++ msg
                                          ++ ": " ++ show tm'
            else pure ()

export
logGlueNF : {vars : _} ->
            {auto c : Ref Ctxt Defs} ->
            String -> Nat -> Lazy String -> Env Term vars -> Glued vars -> Core ()
logGlueNF str n msg env gtm
    = do opts <- getSession
         let lvl = mkLogLevel str n
         if keepLog lvl (logLevel opts)
            then do defs <- get Ctxt
                    tm <- getTerm gtm
                    tmnf <- normaliseHoles defs env tm
                    tm' <- toFullNames tmnf
                    coreLift $ putStrLn $ "LOG " ++ show lvl ++ ": " ++ msg
                                          ++ ": " ++ show tm'
            else pure ()

export
logEnv : {vars : _} ->
         {auto c : Ref Ctxt Defs} ->
         String -> Nat -> String -> Env Term vars -> Core ()
logEnv str n msg env
    = do opts <- getSession
         if keepLog lvl (logLevel opts)
            then dumpEnv env
            else pure ()
  where
    lvl : LogLevel
    lvl = mkLogLevel str n

    dumpEnv : {vs : List Name} -> Env Term vs -> Core ()
    dumpEnv [] = pure ()
    dumpEnv {vs = x :: _} (Let _ c val ty :: bs)
        = do logTermNF' lvl (msg ++ ": let " ++ show x) bs val
             logTermNF' lvl (msg ++ ":" ++ show c ++ " " ++
                             show x) bs ty
             dumpEnv bs
    dumpEnv {vs = x :: _} (b :: bs)
        = do logTermNF' lvl (msg ++ ":" ++ show (multiplicity b) ++ " " ++
                             show (piInfo b) ++ " " ++
                             show x) bs (binderType b)
             dumpEnv bs

replace' : {auto c : Ref Ctxt Defs} ->
           {vars : _} ->
           Int -> Defs -> Env Term vars ->
           (lhs : NF vars) -> (parg : Term vars) -> (exp : NF vars) ->
           Core (Term vars)
replace' {vars} tmpi defs env lhs parg tm
    = if !(convert defs env lhs tm)
         then pure parg
         else repSub tm
  where
    repArg : (Closure vars) -> Core (Term vars)
    repArg c
        = do tmnf <- evalClosure defs c
             replace' tmpi defs env lhs parg tmnf

    repSub : NF vars -> Core (Term vars)
    repSub (NBind fc x b scfn)
        = do b' <- traverse repSub b
             let x' = MN "tmp" tmpi
             sc' <- replace' (tmpi + 1) defs env lhs parg
                             !(scfn defs (toClosure defaultOpts env (Ref fc Bound x')))
             pure (Bind fc x b' (refsToLocals (Add x x' None) sc'))
    repSub (NApp fc hd [])
        = do empty <- clearDefs defs
             quote empty env (NApp fc hd [])
    repSub (NApp fc hd args)
        = do args' <- traverse repArg args
             pure $ apply fc
                        !(replace' tmpi defs env lhs parg (NApp fc hd []))
                        args'
    repSub (NDCon fc n t a args)
        = do args' <- traverse repArg args
             empty <- clearDefs defs
             pure $ apply fc
                        !(quote empty env (NDCon fc n t a []))
                        args'
    repSub (NTCon fc n t a args)
        = do args' <- traverse repArg args
             empty <- clearDefs defs
             pure $ apply fc
                        !(quote empty env (NTCon fc n t a []))
                        args'
    repSub (NAs fc s a p)
        = do a' <- repSub a
             p' <- repSub p
             pure (As fc s a' p')
    repSub (NDelayed fc r tm)
        = do tm' <- repSub tm
             pure (TDelayed fc r tm')
    repSub (NDelay fc r ty tm)
        = do ty' <- replace' tmpi defs env lhs parg !(evalClosure defs ty)
             tm' <- replace' tmpi defs env lhs parg !(evalClosure defs tm)
             pure (TDelay fc r ty' tm')
    repSub (NForce fc r tm args)
        = do args' <- traverse repArg args
             tm' <- repSub tm
             pure $ apply fc (TForce fc r tm') args'
    repSub tm = do empty <- clearDefs defs
                   quote empty env tm

export
replace : {auto c : Ref Ctxt Defs} ->
          {vars : _} ->
          Defs -> Env Term vars ->
          (orig : NF vars) -> (new : Term vars) -> (tm : NF vars) ->
          Core (Term vars)
replace = replace' 0

export
normaliseErr : {auto c : Ref Ctxt Defs} ->
               Error -> Core Error
normaliseErr (CantConvert fc env l r)
    = do defs <- get Ctxt
         pure $ CantConvert fc env !(normaliseHoles defs env l)
                                   !(normaliseHoles defs env r)
normaliseErr (CantSolveEq fc env l r)
    = do defs <- get Ctxt
         pure $ CantSolveEq fc env !(normaliseHoles defs env l)
                                   !(normaliseHoles defs env r)
normaliseErr (WhenUnifying fc env l r err)
    = do defs <- get Ctxt
         pure $ WhenUnifying fc env !(normaliseHoles defs env l)
                                    !(normaliseHoles defs env r)
                                    !(normaliseErr err)
normaliseErr (CantSolveGoal fc env g)
    = do defs <- get Ctxt
         pure $ CantSolveGoal fc env !(normaliseHoles defs env g)
normaliseErr (AllFailed errs)
    = pure $ AllFailed !(traverse (\x => pure (fst x, !(normaliseErr (snd x)))) errs)
normaliseErr (InType fc n err)
    = pure $ InType fc n !(normaliseErr err)
normaliseErr (InCon fc n err)
    = pure $ InCon fc n !(normaliseErr err)
normaliseErr (InLHS fc n err)
    = pure $ InLHS fc n !(normaliseErr err)
normaliseErr (InRHS fc n err)
    = pure $ InRHS fc n !(normaliseErr err)
normaliseErr err = pure err


text:
module ClassDataEx

||| An arbitrary demonstration type.
|||
||| Running apropos on Doo will show you which classes it has instances of.
||| Note the presence of an instance of Fee and Bai, though def.d w/in a function body.
||| This is not the intended result, but it will do for this example.
||| On the upside, those names are not put in the module namespace.
||| Perhaps the instances can be erased?
|||
data Doo = Da

||| A class declaration generates a datatype by that name,
||| seen from running printdef on the class name in the REPL.
||| We ask how far that lets you go towards using instances as values.
||| We deal with the problem of calling member functions like by getfoo.
|||
class Foo a where
	fooval : a

||| Applies this member function of this class to a value of the datatype for the class.
|||
{- The (with) keyword here is a disambiguator.
It is covered in the documentation under Miscellaneous at
	http://docs.idris-lang.org/en/latest/reference/misc.html
Coverage suitable for the Modules & Namespaces Ch. of the Tutorial?
-}
getfoo : Foo a -> a
getfoo x = with x fooval

||| Same as Foo, but with an independent type for the method.
||| We construct a value of type (Bar a) for some (a),
||| so that it can have functions of (Bar a) applied to it.
|||
class Bar a where
	barval : Nat

{-
Error:

	When checking right hand side of getbar:
	Can't resolve type class Bar a

Why an error here and not with getfoo?

getbar : Bar a -> Nat
getbar x = with x barval
-}

getbar : Bar a -> Nat
getbar x = ?getbar'

getbar' = proof
  intro a
  intro bara
  exact (with bara barval)
  exact a
  exact bara

{-
These don't work, Bar isn't the name of the constructor of a (Bar x).
You see this constructor registered when you print the definition of Bar.

mkBar : Bar Doo
mkBar = ?mkBar'

> mkBar = Bar barval

> mkBar = Bar Z

> mkBar = _ Z

Not this either:

> mkBar : Bar Doo where barval = Z

If it's impossible to implement this variable instance, but named terms are needed, it would be better to switch to record types, such as a built-in option or Vinyl records.

This blog post speaks as if this constructor were real and called instanceC for class C:

https://edwinb.wordpress.com/2011/11/09/type-classes-in-idris/

The Idris tutorial says some helpful things.

It may also be possible to use the Elab shell to fill the hole, but I don't know that for sure.
-}

instance [mkBar] Bar Doo where
	barval = Z

getbarDoo : Nat
getbarDoo = getbar mkBar

||| The Idris tutorial's section on Named Instances tells us
||| we can write: instance [?inst] ?C Doo; ?memberC @{inst}.
||| (?memberC @{inst}) equals (with inst ?memberC) where compile & used here.
|||
class Baez a where
	baezval : Nat

instance [mkBaez] Baez Doo where
	baezval = Z

getbaezDoo : Nat
getbaezDoo = baezval @{mkBaez}

||| Since Idris is liberal with what you can declare within a function body,
||| for Fee we construct the instance of the class so.
||| Since the instance being referred to now depends on the computation,
||| yet member functions of the class can be called on it, our goal looks solved.
|||
class Fee a where
	feeval : Nat

getfeeDoo : Nat
getfeeDoo = feeval @{mkFee}
	where
		instance [mkFee] Fee Doo where
			feeval = Z

||| Same as Fee but with implementation by a function of instances like getfoo is.
|||
class Bai a where
	baival : a

getbai : Bai a -> a
getbai x = baival @{x}

getbaiDoo : Doo
getbaiDoo = getbai mkBai
	where
		instance [mkBai] Bai Doo where
			baival = Da

||| Anonymous instances
||| using Doc's Miscellaneous - Existence of an instance.
|||
class Bau a where
	bauval : a

getbauDoo : Doo
getbauDoo = getbau %instance
	where
		getbau : Bau a -> a
		getbau x = bauval @{x}
		instance Bau Doo where
			bauval = Da

||| Anonymous instances with ambiguous type.
|||
class Fju a where
	fjuval : Nat

getfjuDoo : Nat
getfjuDoo = the (Fju Doo -> Nat) getfju %instance
	where
		getfju : Fju a -> Nat
		getfju x = fjuval @{x}
		instance Fju Doo where
			fjuval = Z

||| Parametric instances phase 1
|||
class Beh a where
	behval : a

data Lift : (a : t) -> Type where
	HasLift : Lift a

{-
This also works

> getbehval = the (Beh (Lift Da) -> Lift Da) getbeh %instance

but only if you make the instance of Beh anonymous (delete [mkBeh])
-}
getbehval : Lift Da
getbehval = getbeh mkBeh
	where
		getbeh : Beh a -> a
		getbeh x = behval @{x}
		instance [mkBeh] Beh (Lift Da) where
			behval = HasLift

||| Parametric instances phase 2
|||
class Beu a where
	beuval : a

-- Where block scoping this doesn't affect getbeuval(1..3)
getbeu : Beu a -> a
getbeu x = beuval @{x}

data Lifty : (a : t) -> Type where
	HasLifty : Lifty a

getclval : (x : Doo) -> Beu (Lifty x)
getclval x = mkBeu
	where
		-- > the (Beu (Lifty Da)) mkBeu : Beu (Lifty Da)
		-- > mkBeu {x=Da}
		instance [mkBeu] Beu (Lifty x) where
			beuval = HasLifty

getbeuval1 : (dar : Doo) -> Lifty dar
getbeuval1 dar = getbeu (getclval dar)

getbeuval2 : (dar : Doo) -> Lifty dar
getbeuval2 dar = getbeu (mkBeu {x=dar})

getbeuval3 : (dar : Doo) -> Lifty dar
getbeuval3 dar = getbeu (with dar mkBeu)

||| Parametric anonymous instances phase 1
|||
class Foi a where
	foival : a

getfoi : Foi a -> a
getfoi x = foival @{x}

data Liftful : (a : t) -> Type where
	HasLiftful : Liftful a

getfoiinst : (x : Doo) -> Foi (Liftful x)
getfoiinst x = %instance
	where
		instance Foi (Liftful x) where
			foival = HasLiftful

getfoival : (dar : Doo) -> Liftful dar
getfoival dar = getfoi (getfoiinst dar)

||| Parametric anonymous instances phase 2
|||
class Bua a where
	buaval : a

getbua : Bua a -> a
getbua x = buaval @{x}

data Liftish : (a : t) -> Type where
	HasLiftish : Liftish a

getbuainst : (x : t) -> Bua (Liftish x)
getbuainst x = %instance
	where
		instance Bua (Liftish x) where
			buaval = HasLiftish

getbuaval : (x : t) -> Liftish x
getbuaval x = getbua (getbuainst x)

||| Parametric anonymous instances phase 3
|||
class Fizfyz a where
	fizfyzval : Nat

getfizfyz : Fizfyz a -> Nat
getfizfyz x = fizfyzval @{x}

data Liftsome : (a : t) -> Type where
	HasLiftsome : Liftsome a

getfizfyzinst : (x : t) -> Fizfyz (Liftsome x)
getfizfyzinst x = %instance
	where
		instance Fizfyz (Liftsome x) where
			fizfyzval = Z

getfizfyzval : (x : t) -> Nat
getfizfyzval x = getfizfyz (getfizfyzinst x)

ext: idr

max_stars_repo_name: runKleisli/idris-classdata

max_issues_repo_name: runKleisli/idris-classdata

max_forks_repo_name: runKleisli/idris-classdata


text:
%default total

data Tag =  A | B | C | Unknown | Unchecked

data Doutput : Tag -> Type where
  Ca : Doutput A
  Cb : Doutput B
  Cc : Doutput C
  Cu : Doutput Unknown
  Cs : String -> Doutput Unchecked

{- Based on output from database you construct type -}
typelevel : (a : Doutput Unchecked) -> Type
typelevel (Cs "A") = Doutput A
typelevel (Cs "B") = Doutput B
typelevel (Cs "C") = Doutput C
typelevel (Cs s) = Doutput Unknown

{- Check value takes a type of Doutput Unchecked and transforms into one the known or unknown file format -}
checkValue : (a : Doutput Unchecked) -> typelevel a
checkValue (Cs "A") = Ca
checkValue (Cs "B") = Cb
checkValue (Cs "C") = Cc
checkValue (Cs s) = ?Cu {- I am leaving it as meta variable beacause Idris is refusing to simplify it -}

{-

*Typefromdatabase> :r
Type checking ./Typefromdatabase.idr
Holes: Main.Cu1
*Typefromdatabase> ch
changeDir   check       checkValue  choice      choiceMap   chr
*Typefromdatabase> checkValue (Cs "A")
Ca : Doutput A
Holes: Main.Cu1
*Typefromdatabase> checkValue (Cs "B")
Cb : Doutput B
Holes: Main.Cu1
*Typefromdatabase> checkValue (Cs "C")
Cc : Doutput C
Holes: Main.Cu1
*Typefromdatabase> checkValue (Cs "Hello Wrold")
?Cu1 : Doutput Unknown
Holes: Main.Cu1
*Typefromdatabase>  -}

max_stars_repo_name: mukeshtiwari/Typelevel-Haskell

max_issues_repo_name: mukeshtiwari/Typelevel-Haskell

max_forks_repo_name: mukeshtiwari/Typelevel-Haskell


text:
module Main

import Data.IORef

import Data.Buffer
import Network.Curl.Easy

writeFunction : Buffer -> (len : Int) -> IORef (List Buffer) -> PrimIO Int
writeFunction buf len ref = toPrim $ do
    lst <- readIORef ref
    writeIORef ref $ lst ++ [buf]
    rawSize buf

main : IO ()
main = do
    CURLE_OK <- curl_global_init | c => do
        putStrLn $ "error in curl_global_init: " ++ show c

    Just cli <- curlEasyInit | Nothing => putStrLn "error in curlEasyInit"

    CURLE_OK <- curlEasySetopt cli CURLOPT_URL "https://www.google.com/" | c => do
        putStrLn $ "error in curlEasySetopt: " ++ show c

    ref <- newIORef []
    CURLE_OK <- curlEasySetopt cli CURLOPT_WRITEFUNCTION
        (\b,_,l,_ => writeFunction b l ref) | c => do
          putStrLn $ "error in curlEasySetopt: " ++ show c

    CURLE_OK <- curlEasyPerform cli | c => do
        putStrLn $ "error in curlEasyPerform: " ++ show c

    buffers <- readIORef ref
    putStrLn $ "rawSize buffers = " ++ show (length buffers)
    Just buffer <- concatBuffers buffers | Nothing => putStrLn "concatBuffers returned Nothing"
    bufferSize <- rawSize buffer
    body <- getString buffer 0 bufferSize
    putStrLn body
    -- traverse freeBuffer buffers
    -- freeBuffer buffer

    curlEasyCleanup cli
    curl_global_cleanup


text:
module X

public export
data Ty : Type where
  A : Ty
  B : Ty

public export
f : (d : Ty) => Nat -> Ty
f _ = d

g : f 0 = B
g = Refl

max_stars_repo_name: buzden/idris-playground

max_issues_repo_name: buzden/idris-playground

max_forks_repo_name: buzden/idris-playground


text:
||| Copyright 2016 Google Inc.
|||
||| Licensed under the Apache License, Version 2.0 (the "License");
||| you may not use this file except in compliance with the License.
||| You may obtain a copy of the License at
|||
|||     http://www.apache.org/licenses/LICENSE-2.0
|||
||| Unless required by applicable law or agreed to in writing, software
||| distributed under the License is distributed on an "AS IS" BASIS,
||| WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
||| See the License for the specific language governing permissions and
||| limitations under the License.

module Test.Protobuf

import Test.UnitTest
import Test.Utils
import Protobuf.Core

%access export

allTests : IO ()
allTests = runTests (MkTestFixture "Protobuf" [
  MkTestCase "GetName" (assertEq (getName John) "John Doe"),
  MkTestCase "GetId" (assertEq (getId John) 1234),
  MkTestCase "GetEmail" (assertEq (getEmail John) (Just "jdoe@example.com"))
])

max_stars_repo_name: google/idris-protobuf

max_issues_repo_name: google/idris-protobuf

max_forks_repo_name: google/idris-protobuf


text:
module Proofs.DiscreteOrderTheory

import Common.Util
import Specifications.DiscreteOrderedGroup
import Proofs.GroupCancelationLemmas
import Proofs.GroupTheory
import Proofs.GroupCancelMisc
import Proofs.OrderTheory
import Proofs.TranslationInvarianceTheory

%default total
%access export

infixl 8 #

lemmaOrder : {(#) : Binop s} ->
  PartiallyOrderedGroupSpec (#) e inv leq -> (a,b,c : s) ->
    a # (b # inv c) `leq` e -> a # b `leq` c
lemmaOrder spec a b c given = rewriteRelation leq o2 o3 o1 where
  o1 : a # (b # inv c) # c `leq` e # c
  o1 = translationInvariantR (invariantOrder spec) (a # (b # inv c)) e c given
  o2 : a # (b # inv c) # c = a # b
  o2 = groupCancelMisc1 (group spec) _ b c
  o3 : e # c = c
  o3 = neutralL (monoid (group spec)) c

strictOrderSeparates : {(+) : Binop s} -> {(<=) : Binrel s} ->
  DiscreteOrderedGroupSpec (+) zero neg (<=) unit -> (a,b : s) ->
    Not (a = b) -> a <= b -> unit + a <= b
strictOrderSeparates spec a b diff given = o4 where
  o1 : a + neg b <= zero
  o1 = groupInverseAndOrder (partiallyOrderedGroup spec) a b given
  o2 : a + neg b = zero -> a = b
  o2 = groupInverseAndEquality (group spec) a b
  o3 : unit + (a + neg b) <= zero
  o3 = discreteOrder spec (a + neg b) (contraposition o2 diff) o1
  o4 : unit + a <= b
  o4 = lemmaOrder (partiallyOrderedGroup spec) unit a b o3

public export
separate : Decidable [s,s] leq => {(+) : Binop s} ->
  DiscreteOrderedGroupSpec (+) zero neg leq unit ->
    (a,b : s) ->
    EitherErased (a `leq` b) (unit + b `leq` a)
separate spec a b =
  case decision {rel = leq} a b of
    Yes prf => Left prf
    No contra =>
      let (baLeq, diff) = orderContra (totalOrder spec) a b contra
          prf = strictOrderSeparates spec b a (diff . sym) baLeq
      in Right prf

public export
separateBis : Decidable [s,s] leq => {(+) : Binop s} ->
  DiscreteOrderedGroupSpec (+) zero neg leq unit ->
    (a,b : s) ->
    EitherErased (a `leq` neg unit + b) (b `leq` a)
separateBis spec a b =
  case separate spec b a of
    Left ba => Right ba
    Right ab => Left (orderInverseL (partiallyOrderedGroup spec) unit b a ab)

max_stars_repo_name: jeroennoels/verified-algebra

max_issues_repo_name: jeroennoels/verified-algebra

max_forks_repo_name: jeroennoels/verified-algebra


text:
data MyNat : Type where
     MyZ : MyNat
     MyS : (1 _ : MyNat) -> MyNat

lplus : (1 x : MyNat) -> (1 y : MyNat) -> MyNat
lplus MyZ y = y
lplus (MyS k) y = MyS (lplus k y)

foo : (1 x : MyNat) -> (1 y : MyNat) -> MyNat -> MyNat
foo x y z
    = let 1 test = the MyNat $ case z of
                        MyZ => MyZ
                        (MyS k) => MyS z
            in
          lplus test x


text:
module Text.Bounded

%default total

public export
record WithBounds ty where
  constructor MkBounded
  val : ty
  isIrrelevant : Bool
  startLine : Int
  startCol : Int
  endLine : Int
  endCol : Int

export
start : WithBounds ty -> (Int, Int)
start b = (b.startLine, b.startCol)

export
end : WithBounds ty -> (Int, Int)
end b = (b.endLine, b.endCol)

export
Eq ty => Eq (WithBounds ty) where
  (MkBounded val ir sl sc el ec) == (MkBounded val' ir' sl' sc' el' ec') =
    val == val' && ir == ir' && sl == sl' && sc == sc' && el == el' && ec == ec'

export
Show ty => Show (WithBounds ty) where
  showPrec d (MkBounded val ir sl sc el ec) =
    showCon d "MkBounded" (concat [showArg ir, showArg val, showArg sl, showArg sc, showArg el, showArg ec])

export
Functor WithBounds where
  map f (MkBounded val ir sl sc el ec) = MkBounded (f val) ir sl sc el ec

export
irrelevantBounds : ty -> WithBounds ty
irrelevantBounds x = MkBounded x True (-1) (-1) (-1) (-1)

export
mergeBounds : WithBounds ty -> WithBounds ty' -> WithBounds ty'
mergeBounds (MkBounded _ True _ _ _ _) (MkBounded val True _ _ _ _) = irrelevantBounds val
mergeBounds (MkBounded _ True _ _ _ _) b2 = b2
mergeBounds b1 (MkBounded val True _ _ _ _) = const val <$> b1
mergeBounds b1 b2 =
  let (ur, uc) = min (start b1) (start b2)
      (lr, lc) = max (end b1) (end b2) in
      MkBounded b2.val False ur uc lr lc

export
joinBounds : WithBounds (WithBounds ty) -> WithBounds ty
joinBounds b = mergeBounds b b.val


text:
module Data.InSet.Equality

import Data.Lawful.Eqv

import Decidable.Equality

import public Syntax.WithProof

%default total

infix 6 =?=

||| Generalization of user-defined lawful equality (`Eq`, `Eqv` and `==`) and propositional equality (`DecEq` and `=`).
public export
interface Equality a where

  -- Type-level equality proofs

  EqPrf : a -> a -> Type
  NeqPrf : a -> a -> Type

  cant_eq_neq : {x, y : a} -> EqPrf x y -> NeqPrf x y -> Void

  -- Runtime equality operator

  (=?=) : (x, y : a) -> Bool

  -- Correspondence between type-level and runtime

  eq_prf_to_val : {x, y : a} -> EqPrf x y -> x =?= y = True
  eq_val_to_prf : {x, y : a} -> x =?= y = True -> EqPrf x y

  neq_prf_to_val : {x, y : a} -> NeqPrf x y -> x =?= y = False
  neq_val_to_prf : {x, y : a} -> x =?= y = False -> NeqPrf x y

  -- Properties of equality for equality operator

  equ_reflexive : (x : a) -> x =?= x = True

  equ_commutative : (x, y : a) -> x =?= y = y =?= x

  equ_transitive : (x, y, z : a) -> x =?= y = True -> y =?= z = True -> x =?= z = True

-- TODO Maybe, to split `Equality` interface to two: one for equality relation, another to equivalence properties.
--      Then, equality relation interace's implementations should be exported publicly, but properties proofs should not.

0 decEq_refl : DecEq a => (x : a) -> decEq x x = Yes Refl
decEq_refl x = case @@(decEq x x) of
  (Yes Refl ** p) => p
  (No nn ** _) => absurd $ nn Refl

trueNotFalse : Not (True = False)
trueNotFalse Refl impossible

public export
[PropositionalEq] DecEq a => Equality a where

  -- Type-level equality

  EqPrf x y = x = y
  NeqPrf x y = x = y -> Void

  cant_eq_neq xy nxy = nxy xy

  -- Value-level equality

  x =?= y = case decEq x y of
    Yes pxy => True
    No nxy => False

  -- Correspondence between type-level and runtime

  eq_prf_to_val eq_prf = rewrite eq_prf in
                         rewrite decEq_refl y in
                         Refl

  neq_prf_to_val neq_prf = case @@(decEq x y) of
    (No _ ** prf) => rewrite prf in Refl
    (Yes yy ** _) => absurd $ neq_prf yy

  eq_val_to_prf = case @@(decEq x y) of
    (Yes yy ** _) => \_ => yy
    (No _ ** prf) => rewrite prf in \ft => absurd $ trueNotFalse $ sym ft

  neq_val_to_prf = case @@(decEq x y) of
    (No nn ** _) => \_ => nn
    (Yes _ ** prf) => rewrite prf in \tf => absurd $ trueNotFalse tf

  -- Properties of value-level equality

  equ_reflexive x = rewrite decEq_refl x in Refl

  equ_commutative x y = case @@(decEq x y) of
    (Yes yy ** _) => rewrite yy in Refl
    (No _ ** no_xy) => case @@(decEq y x) of
      (Yes yy ** _) => rewrite yy in
                       rewrite decEq_refl x in
                       Refl
      (No _ ** no_yx) => rewrite no_xy in
                         rewrite no_yx in
                         Refl

  equ_transitive x y z xy yz = case (@@(decEq x y), @@(decEq y z)) of
    ((Yes eq_xy ** _), (Yes eq_yz ** _)) => rewrite eq_xy in
                                            rewrite sym eq_yz in
                                            rewrite decEq_refl y in
                                            Refl
    ((No _ ** no_xy), _) => absurd $ trueNotFalse $ sym $ rewrite sym xy in rewrite no_xy in Refl
    (_, (No _ ** no_yz)) => absurd $ trueNotFalse $ sym $ rewrite sym yz in rewrite no_yz in Refl

public export
[StandardEq] Eqv a => Equality a where

  -- Type-level equality

  EqPrf x y = x == y = True
  NeqPrf x y = x == y = False

  cant_eq_neq xy nxy = trueNotFalse rewrite sym xy in nxy

  -- Value-level equality

  x =?= y = x == y

  -- Correspondence between type-level and runtime

  eq_prf_to_val = id
  eq_val_to_prf = id

  neq_prf_to_val = id
  neq_val_to_prf = id

  -- Properties of value-level equality

  equ_reflexive x = rewrite eqvReflexive x in Refl
  equ_commutative x y = rewrite eqvCommutative x y in Refl
  equ_transitive x y z xy yz = rewrite eqvTransitive x y z xy yz in Refl

max_stars_repo_name: buzden/prog-prove-exercises

max_issues_repo_name: buzden/prog-prove-exercises

max_forks_repo_name: buzden/prog-prove-exercises


text:
module Data.Bytes

import Data.ByteArray as BA

%access public export
%default total

-- Structure of the allocated ByteArray
--   [used_size][.....data.....]
-- used_size is an int and it takes up BA.bytesPerInt bytes
-- at the beginning of the array

export
record Bytes where
  constructor B
  arr : ByteArray
  ofs : Int
  end : Int  -- first offset not included in the array

minimalCapacity : Int
minimalCapacity = 16

private
dataOfs : Int
dataOfs = 1 * BA.bytesPerInt

private
allocate : Int -> IO Bytes
allocate capacity = do
  arr <- BA.allocate (BA.bytesPerInt + capacity)
  BA.pokeInt 0 dataOfs arr
  BA.fill dataOfs capacity 0 arr  -- zero the array
  pure $ B arr dataOfs dataOfs

export
length : Bytes -> Int
length (B arr ofs end) = end - ofs

export
empty : Bytes
empty = unsafePerformIO $ allocate minimalCapacity

export
null : Bytes -> Bool
null (B arr ofs end) = (ofs == end)

%freeze empty

-- factor=1 ~ copy
-- factor=2 ~ grow
private
grow : Int -> Bytes -> IO Bytes
grow factor (B arr ofs end) = do
  maxUsed <- BA.peekInt 0 arr
  let bytesUsed = end - ofs
  let bytesAvailable =
        if maxUsed > end
          then bytesUsed
          else BA.size arr - ofs
  B arr' ofs' end' <- allocate $ (factor*bytesAvailable) `max` minimalCapacity
  BA.copy (arr, ofs) (arr', ofs') bytesUsed
  pure $ B arr' ofs' (ofs' + bytesUsed)

export
snoc : Bytes -> Byte -> Bytes
snoc bs@(B arr ofs end) byte
    = assert_total $
       if end >= BA.size arr
        then unsafePerformIO $ do  -- need more space
          grown <- grow 2 bs
          pure $ snoc grown byte
        else unsafePerformIO $ do
          maxUsed <- BA.peekInt 0 arr
          if maxUsed > end
            then do  -- someone already took the headroom, need copying
              copy <- grow 2 bs
              pure $ snoc copy byte
            else do  -- can mutate
              BA.pokeInt 0 (end+1) arr
              BA.poke end byte arr
              pure $ B arr ofs (end+1)

infixl 7 |>
export
(|>) : Bytes -> Byte -> Bytes
(|>) = snoc

namespace SnocView
  data SnocView : Type where
    Nil : SnocView
    Snoc : (bs : Bytes) -> (b : Byte) -> SnocView

  export
  snocView : Bytes -> SnocView
  snocView (B arr ofs end) =
    if end == ofs
      then SnocView.Nil
      else unsafePerformIO $ do
        last <- BA.peek (end-1) arr
        pure $ SnocView.Snoc (B arr ofs (end-1)) last

namespace ConsView
  data ConsView : Type where
    Nil : ConsView
    Cons : (b : Byte) -> (bs : Bytes) -> ConsView

  export
  consView : Bytes -> ConsView
  consView (B arr ofs end) =
    if end == ofs
      then ConsView.Nil
      else unsafePerformIO $ do
        first <- BA.peek ofs arr
        pure $ ConsView.Cons first (B arr (ofs+1) end)

infixr 7 ++
export
(++) : Bytes -> Bytes -> Bytes
(++) bsL@(B arrL ofsL endL) bsR@(B arrR ofsR endR)
  = assert_total $ let countR = endR - ofsR in
      if endL + countR > BA.size arrL
        then unsafePerformIO $ do  -- need more space
          grown <- grow 2 bsL
          pure $ grown ++ bsR
        else unsafePerformIO $ do
          maxUsedL <- BA.peekInt 0 arrL
          if maxUsedL > endL
            then do  -- headroom taken
              copyL <- grow 2 bsL
              pure $ copyL ++ bsR
            else do  -- can mutate
              BA.pokeInt 0 (endL + countR) arrL
              BA.copy (arrR, ofsR) (arrL, endL) countR
              pure $ B arrL ofsL (endL + countR)

export
dropPrefix : Int -> Bytes -> Bytes
dropPrefix n (B arr ofs end) = B arr (((ofs + n) `min` end) `max` dataOfs) end

export
takePrefix : Int -> Bytes -> Bytes
takePrefix n (B arr ofs end) = B arr ofs (((ofs + n) `min` end) `max` dataOfs)

export
pack : List Byte -> Bytes
pack = fromList empty
  where
    fromList : Bytes -> List Byte -> Bytes
    fromList bs []        = bs
    fromList bs (x :: xs) = fromList (bs `snoc` x) xs

export
unpack : Bytes -> List Byte
unpack bs with (consView bs)
  | Nil       = []
  | Cons x xs = x :: unpack (assert_smaller bs xs)

export
slice : Int -> Int -> Bytes -> Bytes
slice ofs' end' (B arr ofs end)
  = B arr
        (((ofs + ofs') `min` end) `max` dataOfs)
        (((ofs + end') `min` end) `max` dataOfs)

-- Folds with early exit.
-- If Bytes were a Functor, this would be equivalent
-- to a Traversable implementation interpreted in the Either monad.
data Result : Type -> Type where
  Stop : (result : a) -> Result a
  Cont : (acc : a) -> Result a

export
iterateR : (Byte -> a -> Result a) -> a -> Bytes -> a
iterateR f acc bs with (snocView bs)
  | Nil       = acc
  | Snoc ys y with (f y acc)
    | Stop result = result
    | Cont acc'   = iterateR f acc' (assert_smaller bs ys)

export
iterateL : (a -> Byte -> Result a) -> a -> Bytes -> a
iterateL f acc bs with (consView bs)
  | Nil       = acc
  | Cons y ys with (f acc y)
    | Stop result = result
    | Cont acc'   = iterateL f acc' (assert_smaller bs ys)

infixl 3 .:
private
(.:) : (a -> b) -> (c -> d -> a) -> (c -> d -> b)
(.:) g f x y = g (f x y)

export
foldr : (Byte -> a -> a) -> a -> Bytes -> a
foldr f = iterateR (Cont .: f)

export
foldl : (a -> Byte -> a) -> a -> Bytes -> a
foldl f = iterateL (Cont .: f)

export
spanLength : (Byte -> Bool) -> Bytes -> Int
spanLength p = iterateL step 0
  where
    step : Int -> Byte -> Result Int
    step n b with (p b)
      | True  = Cont (1 + n)
      | False = Stop n

find : Byte -> Bytes -> Maybe Int
find b (B arr ofs end) = unsafePerformIO $ BA.find b arr ofs end

export
splitAt : Int -> Bytes -> (Bytes, Bytes)
splitAt n bs = (takePrefix n bs, dropPrefix n bs)

export
splitOn : Byte -> Bytes -> (Bytes, Bytes)
splitOn b bs with (find b bs)
  | Nothing  = (bs, empty)
  | Just ofs = (takePrefix ofs bs, dropPrefix (ofs+1) bs)

export
splitsOn : Byte -> Bytes -> List Bytes
splitsOn b bs with (find b bs)
  | Nothing  = [bs]
  | Just ofs = takePrefix ofs bs :: splitsOn b (assert_smaller bs $ dropPrefix (ofs+1) bs)

export
asciiLines : Bytes -> List Bytes
asciiLines = splitsOn 0x0A

export
span : (Byte -> Bool) -> Bytes -> (Bytes, Bytes)
span p bs = splitAt (spanLength p bs) bs

export
break : (Byte -> Bool) -> Bytes -> (Bytes, Bytes)
break p bs = span (not . p) bs

private
cmp : Bytes -> Bytes -> Ordering
cmp (B arrL ofsL endL) (B arrR ofsR endR) = unsafePerformIO $ do
    let countL = endL - ofsL
    let countR = endR - ofsR
    let commonCount = countL `min` countR
    result <- BA.compare (arrL, ofsL) (arrR, ofsR) commonCount
    pure $
      if result /= 0
        then i2o result
        else compare countL countR
  where
    i2o : Int -> Ordering
    i2o 0 = EQ
    i2o i = if i < 0 then LT else GT

implementation Eq Bytes where
  xs == ys = (Bytes.cmp xs ys == EQ)

implementation Ord Bytes where
  compare = Bytes.cmp

export
toString : Bytes -> String
toString = foldr (strCons . chr . toInt) ""

export
fromString : String -> Bytes
fromString = foldl (\bs, c => bs |> fromInt (ord c)) empty . unpack

implementation Show Bytes where
  show = ("b" ++) . show . toString

implementation Semigroup Bytes where
  (<+>) = (++)

implementation Monoid Bytes where
  neutral = empty

-- todo:
--
-- make indices Nats
-- Build a ByteString on top of Bytes?
-- migrate to (Bits 8)?
--
-- bidirectional growth?

max_stars_repo_name: grin-compiler/idris-grin

max_issues_repo_name: grin-compiler/idris-grin

max_forks_repo_name: grin-compiler/idris-grin


text:
module Data.Entropy
import Data.Vect

%default total

data Solfege = Do | Re | Mi | Fa | So | La | Ti

entropy : Solfege -> Solfege -> Nat
entropy Do Do = 2
entropy Re Do = 2
entropy Mi Do = 3
entropy Fa Do = 7
entropy So Do = 3
entropy La Do = 5
entropy Ti Do = 8 -- boosted from 2 because of wrap-around affect

entropy Do Re = 2
entropy Re Re = 2
entropy Mi Re = 2
entropy Fa Re = 3
entropy So Re = 5
entropy La Re = 5
entropy Ti Re = 4

entropy Do Mi = 3
entropy Re Mi = 2
entropy Mi Mi = 2
entropy Fa Mi = 1
entropy So Mi = 3
entropy La Mi = 7
entropy Ti Mi = 7

entropy Do Fa = 6
entropy Re Fa = 4
entropy Mi Fa = 3
entropy Fa Fa = 3
entropy So Fa = 2
entropy La Fa = 4
entropy Ti Fa = 8

entropy Do So = 3
entropy Re So = 4
entropy Mi So = 3
entropy Fa So = 2
entropy So So = 2
entropy La So = 1
entropy Ti So = 4

entropy Do La = 4
entropy Re La = 6
entropy Mi La = 6
entropy Fa La = 4
entropy So La = 3
entropy La La = 2
entropy Ti La = 1

entropy Do Ti = 8 -- boosted from 2 because of wrap-around affect
entropy Re Ti = 4
entropy Mi Ti = 9
entropy Fa Ti = 6
entropy So Ti = 6
entropy La Ti = 3
entropy Ti Ti = 4

Range : Type
Range = (Nat, Nat)

data Series : (t -> t -> Nat) -> (t, t) -> Range -> Type where
  Pure   : (x : t2) -> Series cost (x, x) (0, 0)
  (>>=)  : Series cost (w, x) (l, u) ->
           (() -> Series cost (y, z) (l', u')) ->
           Series cost (w, z) (cost x y + l + l', (cost x y + u + u'))
  Widen  : Series cost (x, y) (l' + dl, u) -> Series cost (x, y) (l', u + du)

Interval : Type
Interval = (Solfege, Solfege)

Melody : Interval -> Range -> Type
Melody = Series entropy

conventional : Melody (Do, So) (8, 16)
conventional = Widen $ do Pure Do; Pure Re; Pure Mi; Pure Fa; Pure So

unconventional : Melody (Do, So) (12, 24)
unconventional = Widen $ do Pure Do; Pure Ti; Pure Mi; Pure Fa; Pure So

song : Melody (Do, So) (20, 50)
song = Widen $ do conventional; unconventional

max_stars_repo_name: ctford/it-aint-necessarily-so

max_issues_repo_name: ctford/it-aint-necessarily-so

max_forks_repo_name: ctford/it-aint-necessarily-so


text:
module Test.Toml.DataTest

import IdrTest.Test
import IdrTest.Expectation

import Data.List
import Toml.Data

export
suite : Test
suite =
  describe "Toml Data Tests" []

max_stars_repo_name: Z-snails/inigo

max_issues_repo_name: Z-snails/inigo

max_forks_repo_name: Z-snails/inigo


text:
module Main

import Lib

test : List Int
test = accMap (1+) [1,2,3]

-- refl : Main.test = [2,3,4]
-- refl = Refl


text:
module Test

import Effects
import DB.SQLite.Effect

import Provider
import Database
import Queries
import Schema
import SQLiteTypes

%language TypeProviders

-- Use the SQLite dependencies in generated code
%link C "sqlite3api.o"
%include C "sqlite3api.h"
%lib C "sqlite3"

%auto_implicits off
%provide (db : DB "test.sqlite")
  with run {m = IO} (getSchemas "test.sqlite")

speakers : Query db ["name":::TEXT, "bio":::NULLABLE TEXT]
speakers = SELECT ["name":::TEXT, "bio":::NULLABLE TEXT]
           FROM "speaker"
           WHERE 1

talks : Query db ["title":::TEXT, "abstract":::TEXT]
talks = SELECT ["title":::TEXT, "abstract":::TEXT]
        FROM "talk"
        WHERE 1

program : Query db ["name":::TEXT, "title":::TEXT, "abstract":::TEXT]
program = SELECT ["name":::TEXT, "title":::TEXT, "abstract":::TEXT]
          FROM "speaker" * "talk"
          WHERE Col "id" == Col "speaker"

printRes : {s : Schema} -> Query db s -> IO ()
printRes q = do res <- runInit {m = IO} [()] (query q)
                case res of
                  Left err => putStrLn (show err)
                  Right table => putStrLn (showTable _ table)

namespace Main
  main : IO ()
  main = do putStrLn "The speakers are:"
            printRes speakers
            putStrLn "The talks are:"
            printRes talks
            putStrLn "Conference program"
            printRes program
            putStrLn "ok"

max_stars_repo_name: ethansr/IdrisSqlite

max_issues_repo_name: ethansr/IdrisSqlite

max_forks_repo_name: ethansr/IdrisSqlite


text:
module ShapeExercises

import Shape

area : Shape -> Double
area s with (shapeView s)
  area (triangle x y) | STriangle   = 0.5 * x * y
  area (rectangle x y) | SRectangle = x * y
  area (circle x) | SCircle         = pi * x * x


text:
> module Rel.TotalPreorder

> -- import Rel.Preorder

> %default total

> %access public export

> ||| TotalPreorder
> data TotalPreorder : {A : Type} -> (A -> A -> Type) -> Type where
>   MkTotalPreorder : {A : Type} ->
>                     (R : A -> A -> Type) ->
>                     (reflexive : (x : A) -> R x x) ->
>                     (transitive : (x : A) -> (y : A) -> (z : A) -> R x y -> R y z -> R x z) ->
>                     (totalPre : (x : A) -> (y : A) -> Either (R x y) (R y x)) ->
>                     TotalPreorder R

> {-

> ||| TotalPreorder
> data TotalPreorder : Type -> Type where
>   MkTotalPreorder : {A : Type} ->
>                     (R : A -> A -> Type) ->
>                     (reflexive : (x : A) -> R x x) ->
>                     (transitive : (x : A) -> (y : A) -> (z : A) -> R x y -> R y z -> R x z) ->
>                     (totalPre : (x : A) -> (y : A) -> Either (R x y) (R y x)) ->
>                     TotalPreorder A

> ---}

ext: lidr

max_stars_repo_name: zenntenn/IdrisLibs

max_issues_repo_name: zenntenn/IdrisLibs

max_forks_repo_name: zenntenn/IdrisLibs


text:
||| An AST for represening a subset of systemverilog.
|||
||| We assume that modules cannot be nested.
module Language.SystemVerilog.Micro

import Data.Vect

import Toolkit.Data.DList
import Toolkit.Data.DVect
import Toolkit.Data.Vect.Extra

import public Language.SystemVerilog.MetaTypes
import public Language.SystemVerilog.Direction
import public Language.SystemVerilog.Gates

%default total

public export
data Expr : (lctxt : Context)
         -> (gctxt : Context)
         -> (type : Ty)
         -> Type
  where
    End : Expr ctxt gctxt UNIT

    Local : (  label : String)
         -> (  idx   : Index lctxt (label, type))
         -> Expr lctxt gctxt type

    Global : {ty : Ty}
          -> (label : String)
          -> (idx   : Index gctxt (label, ty))
          -> Expr lctxt gctxt ty

    Let : (  this     : String)
       -> (  beThis   : Expr ctxt gctxt typeE)
       -> (  withType : Expr ctxt gctxt type)
       -> (  prf      : ValidLet typeE type)
       -> (  inThis   : Expr ((this,typeE)::ctxt) gctxt typeB)
       -> Expr ctxt gctxt typeB

    Seq : {typeA,typeB : Ty}
       -> (this : Expr ctxt gctxt typeA)
       -> (that : Expr ctxt gctxt typeB)
       -> Expr ctxt gctxt typeB

    TYPE : Expr lctxt gctxt TYPE

    GATE : Expr lctxt gctxt GATE

    -- Decls
    DataLogic : Expr lctxt gctxt DATA

    DataArray : (type : Expr lctxt gctxt DATA)
             -> (size : Nat)
             -> Expr lctxt gctxt DATA

    DataStruct : (xs : Vect (S n) (Pair String (Expr lctxt gctxt DATA)))
              -> Expr lctxt gctxt DATA

    DataUnion : (xs : Vect (S n) (Pair String (Expr lctxt gctxt DATA)))
             -> Expr lctxt gctxt DATA

    Port : (label : String)
        -> (dir   : Direction)
        -> (type  : Expr lctxt gctxt DATA)
        -> Expr lctxt gctxt (PORT label)

    MDecl : (ports : DList String (\s => Expr lctxt gctxt (PORT s)) names)
         -> Expr lctxt gctxt (MODULE names)

    -- Ctors
    NewChan : Expr ctxt gctxt CHAN
    NewModule : List (Pair String (Expr ctxt gctxt CHAN))
             -> Expr ctxt gctxt (MINST names)

    -- Gates
    Not : (out : Expr ctxt gctxt CHAN)
       -> (ins : Expr ctxt gctxt CHAN)
       -> Expr ctxt gctxt GINST

    Gate : {n : Nat}
        -> (type : TyGateComb)
        -> (out  : Expr ctxt gctxt CHAN)
        -> (ins  : Vect (S (S n)) (Expr ctxt gctxt CHAN))
                -> Expr ctxt gctxt GINST

public export
data Decls : (global : Context) -> Type where
  Empty   : Decls Nil
  DeclAdd : (binder : String)
         -> (expr   : Expr Nil global type)
         -> (prf    : ValidDecl type TYPE)
         -> (rest   : Decls global)
         -> Decls ((MkPair binder type) :: global)

public export
record Spec where
  constructor MkSpec
  decls : Decls gtypes
  expr  : Expr Nil gtypes UNIT

export
getMetaType : {type : _} -> Expr local global type -> Ty
getMetaType {type} _ = type

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

max_stars_repo_name: border-patrol/lightclick

max_issues_repo_name: border-patrol/lightclick

max_forks_repo_name: border-patrol/lightclick


text:
main : IO ()
main = putStr "Hello, World!"

max_stars_repo_name: Andaraz/hello-world

max_issues_repo_name: Andaraz/hello-world

max_forks_repo_name: Andaraz/hello-world


text:
module Toolkit.Data.List.Occurs.Does.Not

import Decidable.Equality

import Toolkit.Decidable.Informative

import Toolkit.Data.List.Occurs.Error

%default total

public export
data Occurs : (type : Type)
                 -> (p    : type -> Type)
                 -> (xs   : List type)
                 -> (cy   : Nat)
                         -> Type
  where
    End : Occurs type p Nil Z

    Yes : (holds : p x)
       -> (rest  : Occurs type p     xs  cn)
                -> Occurs type p (x::xs) cn

    No : (nope : Not (p x))
      -> (rest : Occurs type p     xs     cn)
              -> Occurs type p (x::xs) (S cn)

export
Uninhabited (Occurs type p Nil (S x)) where
  uninhabited End impossible
  uninhabited (Yes holds rest) impossible
  uninhabited (No nope rest) impossible

namespace Exactly

  shouldBeZero : (p x -> Void)
              -> Does.Not.Occurs type p (x :: xs) 0 -> Void
  shouldBeZero f (Yes holds rest) = f holds

  shouldNotOccurMore : (Does.Not.Occurs type p xs k -> Void)
                    -> (p x -> Void)
                    -> Does.Not.Occurs type p (x :: xs) (S k) -> Void
  shouldNotOccurMore f g (Yes holds rest) = g holds
  shouldNotOccurMore f g (No nope rest) = f rest

  wrongOccursNot : (Does.Not.Occurs type p xs cn -> Void)
                 -> p x
                 -> Does.Not.Occurs type p (x :: xs) cn -> Void
  wrongOccursNot f y (Yes holds rest) = f rest
  wrongOccursNot f y (No nope rest) = nope y

  export
  doesNotExactlyOccur : {type : Type}
              -> {p    : type -> Type}
              -> (f    : (this : type) -> Dec (p this))
              -> (xs   : List type)
              -> (cn   : Nat)
                      -> DecInfo Occurs.Error
                                 (Does.Not.Occurs type p xs cn)
  doesNotExactlyOccur f [] Z
    = Yes End

  doesNotExactlyOccur f [] (S k)
    = No (MkError Z (S k))
         absurd

  doesNotExactlyOccur f (x :: xs) cn with (f x)
    doesNotExactlyOccur f (x :: xs) cn | (Yes prf) with (doesNotExactlyOccur f xs cn)
      doesNotExactlyOccur f (x :: xs) cn | (Yes prf) | (Yes y)
        = Yes (Yes prf y)

      doesNotExactlyOccur f (x :: xs) cn | (Yes prf) | (No msg contra)
        = No (MkError cn (found msg))
             (wrongOccursNot contra prf)

    doesNotExactlyOccur f (x :: xs) cn | (No contra) with (cn)

      doesNotExactlyOccur f (x :: xs) cn | (No contra) | 0
        = No (MkError cn Z)
             (shouldBeZero contra)

      doesNotExactlyOccur f (x :: xs) cn | (No contra) | (S k) with (doesNotExactlyOccur f xs k)
        doesNotExactlyOccur f (x :: xs) cn | (No contra) | (S k) | (Yes prf)
          = Yes (No contra prf)

        doesNotExactlyOccur f (x :: xs) cn | (No contra) | (S k) | (No msg g)
          = No (MkError cn (S k))
               (shouldNotOccurMore g contra)

-- [ EOF ]

max_stars_repo_name: gallais/linear-circuits

max_issues_repo_name: gallais/linear-circuits

max_forks_repo_name: gallais/linear-circuits


text:
foo : Int -> Int
foo x with (x + 1)
  foo x | y = y + x

foo2 : Int
foo2 = foo 5


text:
module Test.Data.CatQueue

import Test.Assert
import Data.CatQueue

%access public export

-------------------------------------------------------------------------------

foo : CatQueue Nat
foo = MkCatQueue [1,2,3] []

bar : CatQueue Nat
bar = MkCatQueue [] [3,2,1]

baz : CatQueue Nat
baz = MkCatQueue [] []

x : CatQueue Nat
x = MkCatQueue [1] [2,3,4]

y : CatQueue Nat
y = MkCatQueue [5,6] [7,8,9]

z : CatQueue Nat
z = MkCatQueue [10,11,12] [13]

showZ : IO ()
showZ =
  assertEq
    (show z)
    "MkCatQueue [10, 11, 12] [13]"

fooIsBar : IO ()
fooIsBar = assertEq foo bar

fooIsNotBaz : IO ()
fooIsNotBaz = assertNotEq foo baz

nullIsEmpty : IO ()
nullIsEmpty = assertTrue $ null (the (CatQueue String) neutral)

xyzAssociative : IO ()
xyzAssociative = do
  putStrLn $ show $ x <+> (y <+> z)
  putStrLn $ show $ (x <+> y) <+> z
  assertTrue $ x <+> (y <+> z) == (x <+> y) <+> z

max_stars_repo_name: Risto-Stevcev/idris-catenatable-lists

max_issues_repo_name: Risto-Stevcev/idris-catenable-lists

max_forks_repo_name: Risto-Stevcev/idris-catenatable-lists


text:
module Basen

import Data.Fin

%access public export
--Fin to Nat
tonatFin: (n: Nat) -> Fin(n) -> Nat
tonatFin (S k) FZ = Z
tonatFin (S k) (FS x) = S (tonatFin k x)

--List Fin to Nat
tonat: (n: Nat) -> List (Fin(n)) -> Nat
tonat n [] = Z
tonat n (x :: xs) = (tonatFin n x)*(power n (length xs)) + (tonat n xs)

--Euclid's div
Eucl: (a: Nat) -> (b: Nat) -> (Nat, Nat)
Eucl Z b = (0,0)
Eucl (S k) b = case (lte (S (S k)) b) of
                    False => (S(fst(Eucl (minus (S k) b) b)), snd(Eucl (minus (S k) b) b))
                    True => (0, S k)

--Nat to Fin (modular values)
tofinNat: (a: Nat) -> (n: Nat) -> Fin n
tofinNat Z (S j) = FZ
tofinNat (S k) (S j) = case lte (S k) (S j) of
                True => FS (tofinNat k j)
                False =>  (tofinNat (snd(Eucl (S k) (S j))) (S j))

--left strips FZ from lists
strp: List (Fin n) -> List (Fin n)
strp [] = []
strp (x :: xs) = case x of
                      FZ => strp(xs)
                      (FS y) => x::xs

-- Nat to List Fin n (base n representation)
tofin: Nat -> (n: Nat) -> List (Fin n)
tofin Z (S j) = [FZ]
tofin (S k) (S j) = strp(reverse(rem :: reverse(tofin q (S j)))) where
                    rem = tofinNat (snd(Eucl (S k) (S j))) (S j)
                    q = fst(Eucl (S k) (S j))

--adding two Fin n's
addfin: (n: Nat) -> Fin (S n) -> Fin (S n) -> Fin (S n) -> (Fin (S n), Fin (S n))
addfin n x y z = case (tofin ((tonatFin (S n) x)+ (tonatFin (S n) y) + (tonatFin (S n) z)) (S n)) of
                    [l] => (FZ, l)
                    [k, l] => (k,l)

--adding two reversed lists as specified
addfinl: (n: Nat) -> List (Fin (S n)) -> List (Fin (S n)) -> List (Fin (S n))
addfinl n [] ys = strp(ys)
addfinl n (x :: xs) [] = strp(x::xs)
addfinl n (x :: xs) (y :: ys) = (snd(addfin n FZ x y)::(addfinl n (addfinl n [fst(addfin n FZ x y)] xs) ys))

--adding two lists
addfinlist: (n: Nat) -> List (Fin (S n)) -> List (Fin (S n)) -> List (Fin (S n))
addfinlist n xs ys = reverse(addfinl n (reverse xs) (reverse ys))

--embedding Fin n in Fin S n vertically
embn: (n: Nat) -> Fin n -> Fin (S n)
embn (S k) FZ = FZ
embn (S k) (FS x) = FS (embn k x)

--Unused mulfinNat - multiplies two Fin n's
mulfinNat: (n: Nat) -> Fin (n) -> Fin (n) -> (Fin (n), Fin (n))
mulfinNat (S n) x y =  case tofin ((tonatFin (S n) x)*(tonatFin (S n) y)) (S n) of
                    [l] => (FZ, l)
                    [k,l] => (k,l)

--multiply two reversed lists in Fin S n
mulfinl: (n: Nat) -> List (Fin (S n)) -> List (Fin (S n)) -> List (Fin (S n))
mulfinl n xs [] = []
mulfinl n xs (FZ :: ys) = FZ :: (mulfinl n xs ys)
mulfinl n xs ((FS x) :: ys) = addfinl n (mulfinl n xs ((embn n x)::ys)) xs

--multpily two lists
mulfinList: (n: Nat) -> List (Fin (S n)) -> List (Fin (S n)) -> List (Fin (S n))
mulfinList n xs ys = reverse(mulfinl n (reverse xs) (reverse ys))

--proof that right addition preserves equality (somehow cong was messing up)
addl: (x: Type) -> (z: List x) -> (l = y) -> (l ++ z = y ++ z)
addl x z Refl = Refl

-- Proof that the auxiliary reverseOnto used to define rev behaves the way it should (semi-pseudo-contravariantly as I choose to call it)
revontoeq: (x: Type) -> (y: List x) -> (l: List x) -> ((reverseOnto y l)  = ((reverseOnto [] l) ++ y))
revontoeq x y [] = Refl
revontoeq x [] (z :: xs) = sym (appendNilRightNeutral (reverseOnto [] (z::xs)))
revontoeq x (y :: ys) (z :: xs) = trans (trans (revontoeq x (z::y::ys) xs) ((appendAssociative (reverseOnto [] xs) [z] (y::ys)))) (sym (addl x (y::ys) (revontoeq x [z] xs)))

--Proof that reverse is pseudo-contravariant on concatenation
reviscontra: (x: Type) -> (y: List x) -> (l: List x) -> (reverse(y++l) =  reverse(l)++reverse(y))
reviscontra x [] z = sym (appendNilRightNeutral (reverseOnto [] z))
reviscontra x (y :: xs) z = trans (trans (trans (revontoeq x [y] (xs++z)) (addl x [y] (reviscontra x xs z))) (sym (appendAssociative (reverse z) (reverse xs) [y]))) (cong(sym (revontoeq x [y] xs)))

-- Proof that the reverse function is self-inverse
reveq: (x: Type) -> (l: List x) -> (l = reverse(reverse l))
reveq x [] = Refl
reveq x (y :: xs) = sym (trans (trans (cong(reviscontra x [y] xs)) (reviscontra x (reverse xs) (reverse [y]))) (cong(sym (reveq x xs))))