text:
module TTImp.Interactive.ExprSearch

-- Expression search for interactive editing. There's a lot of similarities
-- with Core.AutoSearch (and we reuse some of it) but I think it's better for
-- them to be entirely separate: AutoSearch is a crucial part of the core
-- therefore it's good for it to be well defined and cleanly separated from
-- everything else, whereas this search mechanism is about finding plausible
-- candidates for programs.

-- We try to find as many results as possible, within the given search
-- depth.

import Core.AutoSearch
import Core.CaseTree
import Core.Context
import Core.Context.Log
import Core.Env
import Core.LinearCheck
import Core.Metadata
import Core.Normalise
import Core.Options
import Core.Unify
import Core.TT
import Core.Value

import TTImp.Elab.Check
import TTImp.Interactive.CaseSplit
import TTImp.TTImp
import TTImp.TTImp.Functor
import TTImp.Unelab
import TTImp.Utils

import Data.Either
import Data.List

%default covering

-- Data for building recursive calls - the function name, and the structure
-- of the LHS. Only recursive calls with a different structure are okay.
record RecData where
  constructor MkRecData
  {localVars : List Name}
  recname : Name -- resolved name
  lhsapp : Term localVars

-- Additional definitions required to support the result
ExprDefs : Type
ExprDefs = List ImpDecl

export
data Search : Type -> Type where
     NoMore : Search a -- no more results
     Result : a -> Core (Search a) -> Search a
       -- ^ a result, and what to do if the result is considered
       -- unacceptable

export
Functor Search where
  map fn NoMore = NoMore
  map fn (Result res next)
      = Result (fn res)
               (do next' <- next
                   pure (map fn next'))

export
one : a -> Core (Search a)
one res = pure $ Result res (pure NoMore)

export
noResult : Core (Search a)
noResult = pure NoMore

export
traverse : (a -> Core b) -> Search a -> Core (Search b)
traverse f NoMore = pure NoMore
traverse f (Result r next)
    = do r' <- f r
         pure (Result r' (do next' <- next
                             traverse f next'))

export
filterS : (a -> Bool) -> Search a -> Core (Search a)
filterS p NoMore = pure NoMore
filterS p (Result r next)
    = do next' <- next
         let fnext = filterS p next'
         if p r
            then pure $ Result r fnext
            else fnext

export
searchN : {auto c : Ref Ctxt Defs} ->
          {auto u : Ref UST UState} ->
          Nat -> Core (Search a) -> Core (List a, Core (Search a))
searchN max s
    = do startTimer (searchTimeout !getSession) "expression search"
         tryUnify
           (do res <- s
               xs <- count max res
               clearTimer
               pure xs)
           (do clearTimer
               pure ([], pure NoMore))
  where
    count : Nat -> Search a -> Core (List a, Core (Search a))
    count k NoMore = pure ([], pure NoMore)
    count Z _ = pure ([], pure NoMore)
    count (S Z) (Result a next) = pure ([a], next)
    count (S k) (Result a next)
        = do (rest, cont) <- count k !next
             pure $ (a :: rest, cont)

-- Generate definitions in batches, and sort according to some user provided
-- heuristic (highest proportion of bound variables used is a good one!)
export
searchSort : {auto c : Ref Ctxt Defs} ->
             {auto u : Ref UST UState} ->
             Nat -> Core (Search a) ->
             (a -> a -> Ordering) ->
             Core (Search a)
searchSort max s ord
    = do (batch, next) <- searchN max s
         if isNil batch
            then pure NoMore
            else returnBatch (sortBy ord batch) next
  where
    returnBatch : List a -> Core (Search a) -> Core (Search a)
    returnBatch [] res = searchSort max res ord
    returnBatch (res :: xs) x
        = pure (Result res (returnBatch xs x))

export
nextResult : {auto c : Ref Ctxt Defs} ->
             {auto u : Ref UST UState} ->
             Core (Search a) -> Core (Maybe (a, Core (Search a)))
nextResult s
    = tryUnify
         (do res <- s
             case res of
                  NoMore => pure Nothing
                  Result r next => pure (Just (r, next)))
         (pure Nothing)

public export
record SearchOpts where
  constructor MkSearchOpts
  holesOK : Bool -- add a hole on getting stuck, rather than an error
  getRecData : Bool -- update the LHS data
  recData : Maybe RecData -- LHS, to help build recursive calls
  depth : Nat -- maximum search depth
  inArg : Bool -- in an argument (not top level). Here, try recursive calls
               -- before constructors, otherwise try recursive calls last
  inUnwrap : Bool
  ltor : Bool -- case split left to right
              -- (right to left is good for auxiliary definitions, because
              -- then we split on the new pattern first)
  mustSplit : Bool -- must begin with a case split (in a case helper)
  doneSplit : Bool -- definitely under a case split
  genExpr : Maybe (SearchOpts -> Name -> Nat -> ClosedTerm ->
                   Core (Search (FC, List ImpClause)))

export
initSearchOpts : (rec : Bool) -> (maxDepth : Nat) -> SearchOpts
initSearchOpts rec depth
    = MkSearchOpts False rec Nothing depth
                   False False True False False
                   Nothing

search : {auto c : Ref Ctxt Defs} ->
         {auto m : Ref MD Metadata} ->
         {auto u : Ref UST UState} ->
         FC -> RigCount ->
         SearchOpts -> ClosedTerm ->
         Name -> Core (Search (ClosedTerm, ExprDefs))

getAllEnv : {vars : _} -> FC ->
            SizeOf done ->
            Env Term vars ->
            List (Term (done ++ vars), Term (done ++ vars))
getAllEnv fc done [] = []
getAllEnv {vars = v :: vs} {done} fc p (b :: env)
   = let rest = getAllEnv fc (sucR p) env
         MkVar var = weakenVar p (MkVar First)
         usable = usableName v in
         if usable
            then (Local fc Nothing _ var,
                     rewrite appendAssociative done [v] vs in
                        weakenNs (sucR p) (binderType b)) ::
                             rewrite appendAssociative done [v] vs in rest
            else rewrite appendAssociative done [v] vs in rest
  where
    usableName : Name -> Bool
    usableName (UN _) = True
    usableName _ = False

-- Search recursively, but only if the given name wasn't solved by unification
searchIfHole : {vars : _} ->
               {auto c : Ref Ctxt Defs} ->
               {auto m : Ref MD Metadata} ->
               {auto u : Ref UST UState} ->
               FC -> SearchOpts -> ClosedTerm ->
               Env Term vars -> ArgInfo vars ->
               Core (Search (Term vars, ExprDefs))
searchIfHole fc opts topty env arg
    = case depth opts of
           Z => noResult
           S k =>
              do let hole = holeID arg
                 let rig = argRig arg
                 defs <- get Ctxt
                 Just gdef <- lookupCtxtExact (Resolved hole) (gamma defs)
                      | Nothing => noResult
                 let Hole _ _ = definition gdef
                      | _ => one (!(normaliseHoles defs env (metaApp arg)), [])
                                -- already solved
                 res <- search fc rig (record { depth = k,
                                                inArg = True } opts)
                               topty (Resolved hole)
                 -- When we solve an argument, we're also building a lambda
                 -- expression for its environment, so we need to apply it to
                 -- the current environment to use it as an argument.
                 traverse (\(tm, ds) =>
                    pure (!(normaliseHoles defs env
                             (applyTo fc (embed tm) env)), ds)) res

explicit : ArgInfo vars -> Bool
explicit ai
    = case plicit ai of
           Explicit => True
           _ => False

firstSuccess : {auto c : Ref Ctxt Defs} ->
               {auto u : Ref UST UState} ->
               List (Core (Search a)) ->
               Core (Search a)
firstSuccess [] = noResult
firstSuccess (elab :: elabs)
    = do ust <- get UST
         defs <- get Ctxt
         catch (do Result res more <- elab
                      | NoMore => continue ust defs elabs
                   pure (Result res (continue ust defs (more :: elabs))))
               (\err =>
                    case err of
                         -- Give up on timeout, or we'll keep trying all the
                         -- other branches.
                         Timeout _ => noResult
                         _ => continue ust defs elabs)
  where
    continue : UState -> Defs -> List (Core (Search a)) ->
               Core (Search a)
    continue ust defs elabs
        = do put UST ust
             put Ctxt defs
             firstSuccess elabs

-- Take the first successful result of the two given searches
export
trySearch : {auto c : Ref Ctxt Defs} ->
            {auto u : Ref UST UState} ->
            Core (Search a) ->
            Core (Search a) ->
            Core (Search a)
trySearch s1 s2 = firstSuccess [s1, s2]

export
combine : {auto c : Ref Ctxt Defs} ->
          {auto u : Ref UST UState} ->
          (a -> b -> t) -> Search a -> Search b -> Core (Search t)
combine f NoMore y = pure NoMore
combine f (Result x next) NoMore = pure NoMore
combine f (Result x nextx) (Result y nexty)
    = pure $ Result (f x y) $
                     (do nexty' <- nexty
                         combine f !(one x) nexty')
                         `trySearch`
                     ((do nextx' <- nextx
                          combine f nextx' !(one y))
                          `trySearch`
                      (do nextx' <- nextx
                          nexty' <- nexty
                          combine f nextx' nexty'))

mkCandidates : {vars : _} ->
               {auto c : Ref Ctxt Defs} ->
               {auto u : Ref UST UState} ->
               FC -> Term vars -> ExprDefs ->
               List (Search (Term vars, ExprDefs)) ->
               Core (Search (Term vars, ExprDefs))
-- out of arguments, we have a candidate
mkCandidates fc f ds [] = one (f, ds)
-- argument has run out of ideas, we're stuck
mkCandidates fc f ds (NoMore :: argss) = noResult
-- make a candidate from 'f arg' applied to the rest of the arguments
mkCandidates fc f ds (Result (arg, ds') next :: argss)
    = firstSuccess
           [mkCandidates fc (App fc f arg) (ds ++ ds') argss,
            do next' <- next
               mkCandidates fc f ds (next' :: argss)]

-- Apply the name to arguments and see if the result unifies with the target
-- type, then try to automatically solve any holes which were generated.
-- If there are any remaining holes, search fails.
searchName : {vars : _} ->
             {auto c : Ref Ctxt Defs} ->
             {auto m : Ref MD Metadata} ->
             {auto u : Ref UST UState} ->
             FC -> RigCount -> SearchOpts ->
             Env Term vars -> NF vars -> ClosedTerm ->
             (Name, GlobalDef) ->
             Core (Search (Term vars, ExprDefs))
searchName fc rigc opts env target topty (n, ndef)
    = do defs <- get Ctxt
         checkTimer
         let True = visibleInAny (!getNS :: !getNestedNS)
                                 (fullname ndef) (visibility ndef)
             | _ => noResult
         let ty = type ndef
         let True = usableName (fullname ndef)
             | _ => noResult
         let namety : NameType
                 = case definition ndef of
                        DCon tag arity _ => DataCon tag arity
                        TCon tag arity _ _ _ _ _ _ => TyCon tag arity
                        _ => Func
         log "interaction.search" 5 $ "Trying " ++ show (fullname ndef)
         nty <- nf defs env (embed ty)
         (args, appTy) <- mkArgs fc rigc env nty
         logNF "interaction.search" 5 "Target" env target
         logNF "interaction.search" 10 "App type" env appTy
         ures <- unify inSearch fc env target appTy
         let [] = constraints ures
             | _ => noResult
         -- Search the explicit arguments first, they may resolve other holes
         traverse_ (searchIfHole fc opts topty env)
                   (filter explicit args)
         args' <- traverse (searchIfHole fc opts topty env)
                           args
         mkCandidates fc (Ref fc namety n) [] args'
  where
    -- we can only use the name in a search result if it's a user writable
    -- name (so, no recursive with blocks or case blocks, for example)
    usableName : Name -> Bool
    usableName (UN _) = True
    usableName (NS _ n) = usableName n
    usableName (Nested _ n) = usableName n
    usableName _ = False

getSuccessful : {vars : _} ->
                {auto c : Ref Ctxt Defs} ->
                {auto m : Ref MD Metadata} ->
                {auto u : Ref UST UState} ->
                FC -> RigCount -> SearchOpts -> Bool ->
                Env Term vars -> Term vars -> ClosedTerm ->
                List (Core (Search (Term vars, ExprDefs))) ->
                Core (Search (Term vars, ExprDefs))
getSuccessful {vars} fc rig opts mkHole env ty topty all
    = do res <- firstSuccess all
         case res of
              NoMore => -- If no successful search, make a hole
                if mkHole && holesOK opts
                   then do defs <- get Ctxt
                           let base = maybe "arg"
                                            (\r => nameRoot (recname r) ++ "_rhs")
                                            (recData opts)
                           hn <- uniqueName defs (map nameRoot vars) base
                           (idx, tm) <- newMeta fc rig env (UN $ Basic hn) ty
                                                (Hole (length env) (holeInit False))
                                                False
                           one (tm, [])
                   else noResult
              r => pure r

searchNames : {vars : _} ->
              {auto c : Ref Ctxt Defs} ->
              {auto m : Ref MD Metadata} ->
              {auto u : Ref UST UState} ->
              FC -> RigCount -> SearchOpts -> Env Term vars ->
              Term vars -> ClosedTerm ->
              List Name -> Core (Search (Term vars, ExprDefs))
searchNames fc rig opts env ty topty []
    = noResult
searchNames fc rig opts env ty topty (n :: ns)
    = do defs <- get Ctxt
         checkTimer
         vis <- traverse (visible (gamma defs) (currentNS defs :: nestedNS defs)) (n :: ns)
         let visns = mapMaybe id vis
         nfty <- nf defs env ty
         logTerm "interaction.search" 10 ("Searching " ++ show (map fst visns) ++ " for ") ty
         getSuccessful fc rig opts False env ty topty
            (map (searchName fc rig opts env nfty topty) visns)
  where
    visible : Context -> List Namespace -> Name ->
              Core (Maybe (Name, GlobalDef))
    visible gam nspace n
        = do Just def <- lookupCtxtExact n gam
                  | Nothing => pure Nothing
             if visibleInAny nspace n (visibility def)
                then pure (Just (n, def))
                else pure Nothing

tryRecursive : {vars : _} ->
               {auto c : Ref Ctxt Defs} ->
               {auto m : Ref MD Metadata} ->
               {auto u : Ref UST UState} ->
               FC -> RigCount -> SearchOpts ->
               Env Term vars -> Term vars -> ClosedTerm ->
               RecData -> Core (Search (Term vars, ExprDefs))
tryRecursive fc rig opts env ty topty rdata
    = do defs <- get Ctxt
         case !(lookupCtxtExact (recname rdata) (gamma defs)) of
              Nothing => noResult
              Just def =>
                do res <- searchName fc rig (record { recData = Nothing } opts)
                                     env !(nf defs env ty)
                                     topty (recname rdata, def)
                   defs <- get Ctxt
                   res' <- traverse (\ (t, ds) => pure (!(toFullNames t), ds)) res
                   filterS (structDiffTm (lhsapp rdata)) res'
  where
    mutual
      -- A fairly simple superficialy syntactic check to make sure that
      -- the recursive call is structurally different from the lhs
      -- (Essentially, meaning that there's a constructor application in
      -- one where there's a local in another, or that constructor applications
      -- differ somewhere)
      argDiff : Term vs -> Term vs' -> Bool
      argDiff (Local _ _ _ _) _ = False
      argDiff (Ref _ _ fn) (Ref _ _ fn') = fn /= fn'
      argDiff (Bind _ _ _ _) _ = False
      argDiff _ (Bind _ _ _ _) = False
      argDiff (App _ f a) (App _ f' a')
         = structDiff f f' || structDiff a a'
      argDiff (PrimVal _ c) (PrimVal _ c') = c /= c'
      argDiff (Erased _ _) _ = False
      argDiff _ (Erased _ _) = False
      argDiff (TType _) (TType _) = False
      argDiff (As _ _ _ x) y = argDiff x y
      argDiff x (As _ _ _ y) = argDiff x y
      argDiff _ _ = True

      appsDiff : Term vs -> Term vs' -> List (Term vs) -> List (Term vs') ->
                 Bool
      appsDiff (Ref _ (DataCon _ _) f) (Ref _ (DataCon _ _) f') args args'
         = f /= f' || any (uncurry argDiff) (zip args args')
      appsDiff (Ref _ (TyCon _ _) f) (Ref _ (TyCon _ _) f') args args'
         = f /= f' || any (uncurry argDiff) (zip args args')
      appsDiff (Ref _ _ f) (Ref _ _ f') args args'
         = f == f'
           && length args == length args'
           && any (uncurry argDiff) (zip args args')
      appsDiff (Ref _ (DataCon _ _) f) (Local _ _ _ _) _ _ = True
      appsDiff (Local _ _ _ _) (Ref _ (DataCon _ _) f) _ _ = True
      appsDiff f f' [] [] = argDiff f f'
      appsDiff _ _ _ _ = False -- can't be sure...

      -- Reject if the recursive call is the same in structure as the lhs
      structDiff : Term vs -> Term vs' -> Bool
      structDiff tm tm'
         = let (f, args) = getFnArgs tm
               (f', args') = getFnArgs tm' in
               appsDiff f f' args args'

      structDiffTm : Term vs -> (Term vs', ExprDefs) -> Bool
      structDiffTm tm (tm', _) = structDiff tm tm'

-- A local is usable as long as its type isn't a hole
usableLocal : FC -> Env Term vars -> NF vars -> Bool
usableLocal loc env (NApp _ (NMeta _ _ _) args) = False
usableLocal loc _ _ = True

searchLocalWith : {vars : _} ->
                  {auto c : Ref Ctxt Defs} ->
                  {auto m : Ref MD Metadata} ->
                  {auto u : Ref UST UState} ->
                  FC -> Bool ->
                  RigCount -> SearchOpts -> Env Term vars ->
                  List (Term vars, Term vars) ->
                  Term vars -> ClosedTerm ->
                  Core (Search (Term vars, ExprDefs))
searchLocalWith fc nofn rig opts env [] ty topty
    = noResult
searchLocalWith {vars} fc nofn rig opts env ((p, pty) :: rest) ty topty
    = do defs <- get Ctxt
         checkTimer
         nty <- nf defs env ty
         getSuccessful fc rig opts False env ty topty
                       [findPos defs p id !(nf defs env pty) nty,
                        searchLocalWith fc nofn rig opts env rest ty
                                        topty]
  where
    findDirect : Defs -> Term vars ->
                 (Term vars -> Term vars) ->
                 NF vars -> -- local variable's type
                 NF vars -> -- type we're looking for
                 Core (Search (Term vars, ExprDefs))
    findDirect defs prf f nty ty
        = do (args, appTy) <- mkArgs fc rig env nty
             -- We can only use a local variable if it's not an unsolved
             -- hole
             if usableLocal fc env nty
                then
                  tryUnify -- try with no arguments first
                    (do when (not (isNil args) && nofn) $
                             throw (InternalError "Must apply function")
                        ures <- unify inTerm fc env ty nty
                        let [] = constraints ures
                            | _ => throw (InternalError "Can't use directly")
                        mkCandidates fc (f prf) [] [])
                    (do ures <- unify inTerm fc env ty appTy
                        let [] = constraints ures
                            | _ => noResult
                        args' <- traverse (searchIfHole fc opts topty env)
                                          args
                        mkCandidates fc (f prf) [] args')
                else noResult

    findPos : Defs -> Term vars ->
              (Term vars -> Term vars) ->
              NF vars -> NF vars -> Core (Search (Term vars, ExprDefs))
    findPos defs prf f x@(NTCon pfc pn _ _ [(fc1, xty), (fc2, yty)]) target
        = getSuccessful fc rig opts False env ty topty
              [findDirect defs prf f x target,
                 (do fname <- maybe (throw (InternalError "No fst"))
                                    pure
                                    !fstName
                     sname <- maybe (throw (InternalError "No snd"))
                                    pure
                                    !sndName
                     if !(isPairType pn)
                        then do empty <- clearDefs defs
                                xtytm <- quote empty env xty
                                ytytm <- quote empty env yty
                                getSuccessful fc rig opts False env ty topty
                                  [(do xtynf <- evalClosure defs xty
                                       findPos defs prf
                                         (\arg => applyWithFC (Ref fc Func fname)
                                                          [(fc1, xtytm),
                                                           (fc2, ytytm),
                                                           (fc, f arg)])
                                         xtynf target),
                                   (do ytynf <- evalClosure defs yty
                                       findPos defs prf
                                           (\arg => applyWithFC (Ref fc Func sname)
                                                          [(fc1, xtytm),
                                                           (fc2, ytytm),
                                                           (fc, f arg)])
                                           ytynf target)]
                         else noResult)]
    findPos defs prf f nty target = findDirect defs prf f nty target

searchLocal : {vars : _} ->
              {auto c : Ref Ctxt Defs} ->
              {auto m : Ref MD Metadata} ->
              {auto u : Ref UST UState} ->
              FC -> RigCount -> SearchOpts ->
              Env Term vars -> Term vars -> ClosedTerm ->
              Core (Search (Term vars, ExprDefs))
searchLocal fc rig opts env ty topty
    = -- Reverse the environment so we try the patterns left to right.
      -- This heuristic is just so arguments appear the same order in
      -- recursive calls
      searchLocalWith fc False rig opts env (reverse (getAllEnv fc zero env))
                      ty topty

makeHelper : {vars : _} ->
             {auto c : Ref Ctxt Defs} ->
             {auto m : Ref MD Metadata} ->
             {auto u : Ref UST UState} ->
             FC -> RigCount -> SearchOpts ->
             Env Term vars ->
             Term vars -> Term vars -> Search (Term vars, ExprDefs) ->
             Core (Search (Term vars, ExprDefs))
makeHelper fc rig opts env letty targetty NoMore
    = pure NoMore
makeHelper fc rig opts env letty targetty (Result (locapp, ds) next)
    = do let S depth' = depth opts
             | Z => noResult
         logTerm "interaction.search" 10 "Local app" locapp
         let Just gendef = genExpr opts
             | Nothing => noResult
         defs <- get Ctxt
         intn <- genVarName "cval"
         helpern_in <- genCaseName "search"
         helpern <- inCurrentNS helpern_in
         let env' = Lam fc top Explicit letty :: env
         scopeMeta <- metaVar fc top env' helpern
                             (weaken {n = intn} targetty)
         let scope = toApp scopeMeta
         updateDef helpern (const (Just None))
         -- Apply the intermediate result to the helper function we're
         -- about to generate.
         let def = App fc (Bind fc intn (Lam fc top Explicit letty) scope)
                          locapp

         logTermNF "interaction.search" 10 "Binding def" env def
         defs <- get Ctxt
         Just ty <- lookupTyExact helpern (gamma defs)
             | Nothing => throw (InternalError "Can't happen")
         logTermNF "interaction.search" 10 "Type of scope name" [] ty

         -- Generate a definition for the helper, but with more restrictions.
         -- Always take the first result, to avoid blowing up search space.
         -- Go right to left on variable split, to get the variable we just
         -- added first.
         -- There must be at least one case split.
         ((helper :: _), nextdef) <-
                    searchN 1 $ gendef (record { getRecData = False,
                                                 inUnwrap = True,
                                                 depth = depth',
                                                 ltor = False,
                                                 mustSplit = True } opts)
                                       helpern 0 ty
              | _ => do log "interaction.search" 10 "No results"
                        noResult

         let helperdef = IDef fc helpern (snd helper)
         log "interaction.search" 10 $ "Def: " ++ show helperdef
         pure (Result (def, helperdef :: ds) -- plus helper
                      (do next' <- next
                          makeHelper fc rig opts env letty targetty next'))
  where
    -- convert a metavar application (as created by 'metaVar') to a normal
    -- application (as required by a case block)
    toApp : forall vars . Term vars -> Term vars
    toApp (Meta fc n i args) = apply fc (Ref fc Func (Resolved i)) args
    toApp tm = tm

tryIntermediateWith : {vars : _} ->
                      {auto c : Ref Ctxt Defs} ->
                      {auto m : Ref MD Metadata} ->
                      {auto u : Ref UST UState} ->
                      FC -> RigCount -> SearchOpts ->
                      Env Term vars -> List (Term vars, Term vars) ->
                      Term vars -> ClosedTerm ->
                      Core (Search (Term vars, ExprDefs))
tryIntermediateWith fc rig opts env [] ty topty = noResult
tryIntermediateWith fc rig opts env ((p, pty) :: rest) ty topty
    = do defs <- get Ctxt
         getSuccessful fc rig opts False env ty topty
                       [applyLocal defs p !(nf defs env pty) ty,
                        tryIntermediateWith fc rig opts env rest ty
                                            topty]
  where
    matchable : Defs -> NF vars -> Core Bool
    matchable defs (NBind fc x (Pi _ _ _ _) sc)
        = matchable defs !(sc defs (toClosure defaultOpts env
                                              (Erased fc False)))
    matchable defs (NTCon _ _ _ _ _) = pure True
    matchable _ _ = pure False

    applyLocal : Defs -> Term vars ->
                 NF vars -> Term vars -> Core (Search (Term vars, ExprDefs))
    applyLocal defs tm locty@(NBind _ x (Pi fc' _ _ _) sc) targetty
        = -- If the local has a function type, and the return type is
          -- something we can pattern match on (so, NTCon) then apply it,
          -- let bind the result, and try to generate a definition for
          -- the scope of the let binding
          do True <- matchable defs
                           !(sc defs (toClosure defaultOpts env
                                                (Erased fc False)))
                 | False => noResult
             intnty <- genVarName "cty"
             letty <- metaVar fc' erased env intnty (TType fc)
             let opts' = record { inUnwrap = True } opts
             locsearch <- searchLocalWith fc True rig opts' env [(p, pty)]
                                          letty topty
             makeHelper fc rig opts env letty targetty locsearch
    applyLocal defs tm _ _ = noResult

-- Try to make progress by applying a local variable or the recursive
-- definition to an argument, then making a helper function to complete
-- the job
tryIntermediate : {vars : _} ->
                  {auto c : Ref Ctxt Defs} ->
                  {auto m : Ref MD Metadata} ->
                  {auto u : Ref UST UState} ->
                  FC -> RigCount -> SearchOpts ->
                  Env Term vars -> Term vars -> ClosedTerm ->
                  Core (Search (Term vars, ExprDefs))
tryIntermediate fc rig opts env ty topty
    = tryIntermediateWith fc rig opts env (reverse (getAllEnv fc zero env))
                          ty topty

-- Try making a recursive call and unpacking the result. Only do this if
-- the return type is a single constructor data type, otherwise it massively
-- increases the search space, and the intention is for unpacking
-- things like dependent pairs and singleton types before proceeding.
tryIntermediateRec : {vars : _} ->
                     {auto c : Ref Ctxt Defs} ->
                     {auto m : Ref MD Metadata} ->
                     {auto u : Ref UST UState} ->
                     FC -> RigCount -> SearchOpts ->
                     Env Term vars ->
                     Term vars -> ClosedTerm ->
                     Maybe RecData -> Core (Search (Term vars, ExprDefs))
tryIntermediateRec fc rig opts env ty topty Nothing = noResult
tryIntermediateRec fc rig opts env ty topty (Just rd)
    = do defs <- get Ctxt
         Just rty <- lookupTyExact (recname rd) (gamma defs)
              | Nothing => noResult
         True <- isSingleCon defs !(nf defs [] rty)
              | _ => noResult
         intnty <- genVarName "cty"
         letty <- metaVar fc erased env intnty (TType fc)
         let opts' = record { inUnwrap = True,
                              recData = Nothing } opts
         logTerm "interaction.search" 10 "Trying recursive search for" ty
         log "interaction.search" 10 $ show !(toFullNames (recname rd))
         logTerm "interaction.search" 10 "LHS" !(toFullNames (lhsapp rd))
         recsearch <- tryRecursive fc rig opts' env letty topty rd
         makeHelper fc rig opts' env letty ty recsearch
  where
    isSingleCon : Defs -> NF [] -> Core Bool
    isSingleCon defs (NBind fc x (Pi _ _ _ _) sc)
        = isSingleCon defs !(sc defs (toClosure defaultOpts []
                                              (Erased fc False)))
    isSingleCon defs (NTCon _ n _ _ _)
        = do Just (TCon _ _ _ _ _ _ [con] _) <- lookupDefExact n (gamma defs)
                  | _ => pure False
             pure True
    isSingleCon _ _ = pure False

searchType : {vars : _} ->
             {auto c : Ref Ctxt Defs} ->
             {auto m : Ref MD Metadata} ->
             {auto u : Ref UST UState} ->
             FC -> RigCount -> SearchOpts -> Env Term vars ->
             ClosedTerm ->
             Nat -> Term vars -> Core (Search (Term vars, ExprDefs))
searchType fc rig opts env topty (S k) (Bind bfc n b@(Pi fc' c info ty) sc)
    = do let env' : Env Term (n :: _) = b :: env
         log "interaction.search" 10 $ "Introduced lambda, search for " ++ show sc
         scVal <- searchType fc rig opts env' topty k sc
         pure (map (\ (sc, ds) => (Bind bfc n (Lam fc' c info ty) sc, ds)) scVal)
searchType {vars} fc rig opts env topty Z (Bind bfc n b@(Pi fc' c info ty) sc)
    = -- try a local before creating a lambda...
      getSuccessful fc rig opts False env ty topty
           [searchLocal fc rig opts env (Bind bfc n b sc) topty,
            (do defs <- get Ctxt
                let n' = UN $ Basic !(getArgName defs n [] vars !(nf defs env ty))
                let env' : Env Term (n' :: _) = b :: env
                let sc' = renameTop n' sc
                log "interaction.search" 10 $ "Introduced lambda, search for " ++ show sc'
                scVal <- searchType fc rig opts env' topty Z sc'
                pure (map (\ (sc, ds) =>
                             (Bind bfc n' (Lam fc' c info ty) sc, ds)) scVal))]
searchType fc rig opts env topty _ ty
    = case getFnArgs ty of
           (Ref rfc (TyCon t ar) n, args) =>
                do defs <- get Ctxt
                   if length args == ar
                     then do sd <- getSearchData fc False n
                             let allHints = concat (map snd (hintGroups sd))
                             -- Solutions is either:
                             -- First try the locals,
                             -- Then try the hints in order
                             -- Then try a recursive call
                             log "interaction.search" 10 $ "Hints found for " ++ show n ++ " "
                                         ++ show allHints
                             let tries =
                                   [searchLocal fc rig opts env ty topty,
                                    searchNames fc rig opts env ty topty allHints]
                             let tryRec =
                                   case recData opts of
                                        Nothing => []
                                        Just rd => [tryRecursive fc rig opts env ty topty rd]
                             let tryIntRec =
                                   if doneSplit opts
                                      then [tryIntermediateRec fc rig opts env ty topty (recData opts)]
                                      else []
                             let tryInt = if not (inUnwrap opts)
                                             then [tryIntermediate fc rig opts env ty topty]
                                             else []
                             -- if we're in an argument, try the recursive call
                             -- first. We're more likely to want that than nested
                             -- constructors.
                             let allns : List _
                                     = if inArg opts
                                          then tryRec ++ tryInt ++ tries
                                          else tryInt ++ tries ++ tryRec ++ tryIntRec
                             getSuccessful fc rig opts True env ty topty allns
                     else noResult
           _ => do logTerm "interaction.search" 10 "Searching locals only at" ty
                   let tryInt = if not (inUnwrap opts)
                                   then [tryIntermediate fc rig opts env ty topty]
                                   else []
                   let tryIntRec = if inArg opts || not (doneSplit opts)
                                      then []
                                      else [tryIntermediateRec fc rig opts env ty topty (recData opts)]
                   getSuccessful fc rig opts True env ty topty
                           (tryInt ++ [searchLocal fc rig opts env ty topty]
                             ++ case recData opts of
                                     Nothing => []
                                     Just rd => [tryRecursive fc rig opts env ty topty rd]
                             ++ tryIntRec)

searchHole : {auto c : Ref Ctxt Defs} ->
             {auto m : Ref MD Metadata} ->
             {auto u : Ref UST UState} ->
             FC -> RigCount -> SearchOpts -> Name ->
             Nat -> ClosedTerm ->
             Defs -> GlobalDef -> Core (Search (ClosedTerm, ExprDefs))
searchHole fc rig opts n locs topty defs glob
    = do searchty <- normalise defs [] (type glob)
         logTerm "interaction.search" 10 "Normalised type" searchty
         checkTimer
         searchType fc rig opts [] topty locs searchty

-- Declared at the top
search fc rig opts topty n_in
    = do defs <- get Ctxt
         case !(lookupHoleName n_in (gamma defs)) of
              Just (n, i, gdef) =>
                   -- The definition should be 'BySearch' at this stage,
                   -- if it's arising from an auto implicit
                   case definition gdef of
                        Hole locs _ => searchHole fc rig opts n locs topty defs gdef
                        BySearch _ _ _ => searchHole fc rig opts n
                                                   !(getArity defs [] (type gdef))
                                                   topty defs gdef
                        _ => do log "interaction.search" 10 $ show n_in ++ " not a hole"
                                throw (InternalError $ "Not a hole: " ++ show n ++ " in " ++
                                        show (map recname (recData opts)))
              _ => do log "interaction.search" 10 $ show n_in ++ " not found"
                      undefinedName fc n_in
  where
    lookupHoleName : Name -> Context ->
                     Core (Maybe (Name, Int, GlobalDef))
    lookupHoleName n defs
        = case !(lookupCtxtExactI n defs) of
               Just (i, res) => pure $ Just (n, i, res)
               Nothing => case !(lookupCtxtName n defs) of
                               [res] => pure $ Just res
                               _ => pure Nothing

getLHSData : {auto c : Ref Ctxt Defs} ->
             Defs -> Maybe ClosedTerm -> Core (Maybe RecData)
getLHSData defs Nothing = pure Nothing
getLHSData defs (Just tm)
    = pure $ getLHS !(toFullNames !(normaliseHoles defs [] tm))
  where
    getLHS : {vars : _} -> Term vars -> Maybe RecData
    getLHS (Bind _ _ (PVar _ _ _ _) sc) = getLHS sc
    getLHS (Bind _ _ (PLet _ _ _ _) sc) = getLHS sc
    getLHS sc
        = case getFn sc of
               Ref _ _ n => Just (MkRecData n sc)
               _ => Nothing

firstLinearOK : {auto c : Ref Ctxt Defs} ->
                {auto m : Ref MD Metadata} ->
                {auto u : Ref UST UState} ->
                FC -> Search (ClosedTerm, ExprDefs) ->
                Core (Search RawImp)
firstLinearOK fc NoMore = noResult
firstLinearOK fc (Result (t, ds) next)
    = handleUnify
            (do unless (isNil ds) $
                   traverse_ (processDecl [InCase] (MkNested []) []) ds
                ignore $ linearCheck fc linear False [] t
                defs <- get Ctxt
                nft <- normaliseHoles defs [] t
                raw <- unelab [] !(toFullNames nft)
                pure (Result (map rawName raw) (firstLinearOK fc !next)))
            (\err =>
                do next' <- next
                   firstLinearOK fc next')

export
exprSearchOpts : {auto c : Ref Ctxt Defs} ->
                 {auto m : Ref MD Metadata} ->
                 {auto u : Ref UST UState} ->
                 SearchOpts -> FC -> Name -> List Name ->
                 Core (Search RawImp)
exprSearchOpts opts fc n_in hints
    = do defs <- get Ctxt
         Just (n, idx, gdef) <- lookupHoleName n_in defs
             | Nothing => undefinedName fc n_in
         -- the REPL does this step, but doing it here too because
         -- expression search might be invoked some other way
         let Hole _ _ = definition gdef
             | PMDef pi [] (STerm _ tm) _ _
                 => do raw <- unelab [] !(toFullNames !(normaliseHoles defs [] tm))
                       one (map rawName raw)
             | _ => throw (GenericMsg fc "Name is already defined")
         lhs <- findHoleLHS !(getFullName (Resolved idx))
         log "interaction.search" 10 $ "LHS hole data " ++ show (n, lhs)
         opts' <- if getRecData opts
                     then do d <- getLHSData defs lhs
                             pure (record { recData = d } opts)
                     else pure opts
         res <- search fc (multiplicity gdef) opts' (type gdef) n
         firstLinearOK fc res
  where
    lookupHoleName : Name -> Defs -> Core (Maybe (Name, Int, GlobalDef))
    lookupHoleName n defs
        = case !(lookupCtxtExactI n (gamma defs)) of
               Just (idx, res) => pure $ Just (n, idx, res)
               Nothing => case !(lookupCtxtName n (gamma defs)) of
                               [res] => pure $ Just res
                               _ => pure Nothing

exprSearch' : {auto c : Ref Ctxt Defs} ->
              {auto m : Ref MD Metadata} ->
              {auto u : Ref UST UState} ->
              FC -> Name -> List Name ->
              Core (Search RawImp)
exprSearch' = exprSearchOpts (initSearchOpts True 5)

export
exprSearch : {auto c : Ref Ctxt Defs} ->
             {auto m : Ref MD Metadata} ->
             {auto u : Ref UST UState} ->
             FC -> Name -> List Name ->
             Core (Search RawImp)
exprSearch fc n hints
    = do startTimer (searchTimeout !getSession) "expression search"
         res <- exprSearch' fc n hints
         clearTimer
         pure res

export
exprSearchN : {auto c : Ref Ctxt Defs} ->
              {auto m : Ref MD Metadata} ->
              {auto u : Ref UST UState} ->
              FC -> Nat -> Name -> List Name ->
              Core (List RawImp)
exprSearchN fc max n hints
    = do (res, _) <- searchN max (exprSearch fc n hints)
         pure res


text:
> module Nat.GCD

> import Nat.Divisor

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

> |||
> data GCD : (d : Nat) -> (m : Nat) -> (n : Nat) -> Type where
>   MkGCD : d `Divisor` m ->
>           d `Divisor` n ->
>           ((d' : Nat) -> d' `Divisor` m -> d' `Divisor` n -> d' `Divisor` d) ->
>           GCD d m n

ext: lidr

max_stars_repo_name: zenntenn/IdrisLibs

max_issues_repo_name: zenntenn/IdrisLibs

max_forks_repo_name: zenntenn/IdrisLibs


text:
module Main

import Average

showAverage : String -> String
showAverage str = "The average word length is: " ++
		  show (average str) ++ "\n"

main : IO ()
main = repl "Enter a string:  " showAverage

palindrome : String -> Bool
palindrome str =
	if length str > 10
		then toLower str == reverse (toLower str)
		else False

invert : Bool -> Bool
invert False = True
invert True = False

ext: idr


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

import Data.Strings

import Lightyear
import Lightyear.Strings

-- %access  export
%default total

||| Simple data structure to store the result of a parsing test.
export
data TestReport : Type where
  Pass : (title : String) -> TestReport

  ParseFailure : (title : String)
              -> (report : String)
              -> TestReport

  ResultFailure : (title : String) -> (made : String) -> TestReport

  ||| Report a parsing failure with expected failure
  AdvParseFailure : Show a
                 => (title    : String)
                 -> (input    : String)
                 -> (expected : a)
                 -> (report   : String)
                 -> TestReport

  ||| Report a wrong result failure with expected failure.
  AdvResultFailure : Show a
                 => (title    : String)
                 -> (input    : String)
                 -> (expected : a)
                 -> (actual   : a)
                 -> TestReport

||| Run a parsing test that is expected to pass and discard result.
|||
||| @title    Name of the test.
||| @p        The parser to test.
||| @input    The input string to parse.
export
parseTest : Show a
         => (title    : String)
         -> (p        : Parser a)
         -> (input    : String)
         -> TestReport
parseTest title p input = do
  case parse p input of
    Left err     => ParseFailure title err
    Right actual => Pass title

||| Run a parsing test that is expected to fail and discard result.
|||
||| @title    Name of the test.
||| @p        The parser to test.
||| @input    The input string to parse.
export
parseTestNot : Show a
            => (title    : String)
            -> (p        : Parser a)
            -> (input    : String)
            -> TestReport
parseTestNot title p input = do
  case parse p input of
    Left err     => Pass title
    Right actual => ResultFailure title (show actual)

||| Run a parsing test that is expected to pass and compare result to
||| an expected value.
|||
||| @title    Name of the test.
||| @p        The parser to test.
||| @input    The input string to parse.
||| @expected The expected output from a successful parsing.
||| @eq       A comparison function.
export
parseTestCmp : Show a
            => (title    : String)
            -> (p        : Parser a)
            -> (eq       : a -> a -> Bool)
            -> (input    : String)
            -> (expected : a)
            -> TestReport
parseTestCmp title p test input expected = do
  case parse p input of
    Left err     => AdvParseFailure title input expected err
    Right actual => if test actual expected
                      then Pass title
                      else AdvResultFailure title input expected actual

||| Run a parsing test that is expected to fail.
|||
||| @title    Name of the test.
||| @p        The parser to test.
||| @input    The input string to parse.
||| @expected The expected parsing error message.
export
parseTestCmpNot : Show a
               => (title    : String)
               -> (p        : Parser a)
               -> (input    : String)
               -> (expected : String)
               -> TestReport
parseTestCmpNot title p input expected = do
  case parse p input of
    Left actual  => if trim actual == trim expected
                      then Pass title
                      else AdvParseFailure title input expected actual
    Right result => AdvResultFailure title input result result

||| Run a parsing test that is expected to pass and compare showing
||| the result to an expected value.
|||
||| @title    Name of the test.
||| @p        The parser to test.
||| @input    The input string to parse.
||| @expected The expected output from a successful parsing.
export
parseTestCmpShow : Show a
                => (title    : String)
                -> (p        : Parser a)
                -> (input    : String)
                -> (expected : String)
                -> TestReport
parseTestCmpShow title p input expected = do
  case parse p input of
    Left err     => ParseFailure title  err
    Right actual => if show actual == expected
                      then Pass title
                      else ResultFailure title (show actual)

||| Turn the test report into a string.
private
showReport : TestReport -> String
showReport (Pass title) = unwords ["[PASS]", title]

showReport (ParseFailure title report) =
  unlines [ unwords ["[FAIL]", "[PARSING]", title]
          , unwords ["\t", "Gave error:"]
          , report
          ]
showReport (ResultFailure title made) =
  unlines [ unwords ["[FAIL]", "[RESULT]", title]
            , unwords ["\t", "I was able to parse, when I shouldn't and made:"]
            , unwords ["\t\t", made]
           ]

showReport (AdvParseFailure title input expected report) =
  unlines [ unwords ["[FAIL]", "[PARSING]", title]
          , unwords ["\t", "Given input:"]
          , unwords ["\t\t", input]
          , unwords ["\t", "Gave error:"]
          , report
          ]
showReport (AdvResultFailure title input expected actual) =
    unlines $ head ++ footer
  where
    head : List String
    head = [ unwords ["[FAIL]", "[RESULT]", title]
            , unwords ["\t", "Given input:"]
            , unwords ["\t\t", input]
           ]
    footer : List String
    footer = [ unwords ["\t", "I made:"]
             , unwords ["\t\t", show actual]
             , unwords ["\t", "But was expected to make:"]
             , unwords ["\t\t", show expected]
             ]

||| Run an individual test.
export
runTest : TestReport -> IO ()
runTest = (putStrLn . showReport)

||| Run a sequence of tests.
export
runTests : List TestReport -> IO ()
runTests = traverse_ runTest

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

max_stars_repo_name: Mr-Andersen/lightyear

max_issues_repo_name: Mr-Andersen/lightyear

max_forks_repo_name: Mr-Andersen/lightyear


text:
module System.Bindings.LibUSB.Data

data Buffer = MkBuffer Nat Ptr

-- XXX this is ugly, make it more like the Raw memory effect
-- XXX with type guarantees for space. length, etc

allocate : Nat -> IO Buffer
allocate s = do
  b <- mkForeign (FFun "malloc" [FInt] FPtr) (fromNat s)
  return (MkBuffer s b)

free : Buffer -> IO ()
free (MkBuffer _ b) = mkForeign (FFun "free" [FPtr] FUnit) b

string_from_buffer : Buffer -> IO String
string_from_buffer (MkBuffer s b) =
  mkForeign (FFun "string_from_buffer" [FInt, FPtr] FString) (fromNat s) b

peek : Buffer -> Nat -> IO Bits8
peek (MkBuffer l b) i = mkForeign (FFun "idris_libusb_peek" [FPtr, FInt] FBits8) b (fromNat i)

poke : Buffer -> Nat -> Bits8 -> IO ()
poke (MkBuffer l b) i d = mkForeign (FFun "idris_libusb_poke" [FPtr, FInt, FBits8] FUnit) b (fromNat i) d

--
fill_buffer : Buffer -> List Bits8 -> IO ()
fill_buffer _ [] = do return ()
fill_buffer b (x::xs) = fill_buffer' b 0 (x::xs)
  where fill_buffer' : Buffer -> Nat -> List Bits8 -> IO ()
        fill_buffer' _ _ []      = do return ()
        fill_buffer' b i (x::xs) = do
          poke b i x
          fill_buffer' b (i+1) xs

read_buffer : Buffer -> Nat -> IO (List Bits8)
read_buffer b Z = return []
read_buffer b (S n) = traverse (peek b) [0..n]

bits_to_int : Bits8 -> IO Int
bits_to_int b = mkForeign (FFun "idris_bits_to_int" [FBits8] FInt) b

data UsbClass = PerInterface
              | Audio
              | Comm
              | HID
              | Physical
              | Printer
              | PTP
              | Image
              | MassStorage
              | Data
              | SmartCard
              | ContentSecurity
              | Video
              | PersonalHealthCare
              | DiagnosticDevice
              | Wireless
              | Application
              | VendorSpec

max_stars_repo_name: idris-hackers/usb

max_issues_repo_name: idris-hackers/usb

max_forks_repo_name: idris-hackers/usb


text:
import Data.Vect

distrL : a -> List b -> List (a, b)
distrL a = map (a,)

distrR : b -> List a -> List (a, b)
distrR b = map (, b)

-- closeVect : List (n ** Vect n Nat)
-- closeVect = map (** flip replicate 3) [0..10]

insert : List (Nat,Nat,Nat,Nat)
insert = map (\ f => f (the Nat 0) (the Nat 1))
         [(,,2,3), (2,,,3), (2,3,,)]


text:
module Main

import Common.Util
import Common.Interfaces
import Specifications.DiscreteOrderedGroup
import Specifications.OrderedRing
import Proofs.GroupTheory
import Proofs.TranslationInvarianceTheory
import Proofs.DiscreteOrderTheory
import Proofs.Interval
import Instances.Notation
import Instances.TrustInteger
import Instances.ZZ
import Addition.Carry
import Addition.Absorb
import Addition.Reduce

%default total

testCarry : Integer -> String
testCarry x =
  case decideBetween {leq = IntegerLeq} (-18) 18 x of
    Yes inRange => show $ result $
      computeCarry integerDiscreteOrderedGroup 9 (CheckIntegerLeq Oh) x inRange
    No _ => "Error"

testCarryZZ : ZZ -> String
testCarryZZ x =
  case decideBetween {leq = LTEZ} (-18) 18 x of
    Yes inRange => show $ result $
      computeCarry zzDiscreteOrderedGroup 9 bound x inRange
    No _ => "Error"
  where
    bound : LTEZ 1 8
    bound = LtePosPos (LTESucc LTEZero)

integerDigits : Vect n Integer -> Maybe (Vect n (Digit IntegerLeq Ng 18))
integerDigits = maybeDigits {leq = IntegerLeq} Ng 18

testAddition : Vect (S k) (Digit {s = Integer} IntegerLeq Ng 18) ->
  (Carry, Vect (S k) Integer)
testAddition inputs = outputs $
  reduce integerDiscreteOrderedRing 9 (CheckIntegerLeq Oh) inputs

main : IO ()
main = do printLn $ map testCarry [(-20)..20]
          printLn $ map testCarryZZ (map fromInteger [(-21)..21])
          printLn $ liftA testAddition
                      (integerDigits (reverse [17,2,13,4,5,-15,0]))

||| compile time test
test1 : testCarryZZ (-15) = testCarry (-15)
test1 = Refl

||| compile time test
test2 : testCarryZZ 12 = "(P, 2)"
test2 = Refl

max_stars_repo_name: jeroennoels/verified-exact-real

max_issues_repo_name: jeroennoels/verified-exact-real

max_forks_repo_name: jeroennoels/verified-exact-real


text:
module Main

import BashCompletion
import Config as Cfg
import Data.Config
import Data.Date
import Data.List
import Data.Promise
import Data.PullRequest
import Data.String
import Data.String.Extra
import Data.User
import FFI.Concurrency
import FFI.Git
import FFI.GitHub
import Help
import Language.JSON
import Language.JSON.Accessors
import PullRequest as PR
import Reviewer
import System
import System.File
import Text.PrettyPrint.Prettyprinter
import Text.PrettyPrint.Prettyprinter.Render.Terminal
import User

%default total

exitError : HasIO io =>
            String
         -> io a
exitError err =
  do stderrColors <- isTTY stderr
     if stderrColors
          then ignore $ fPutStrLn stderr . renderString . layoutPretty defaultLayoutOptions . annotate (color Red) . pretty $ trim err
          else ignore $ fPutStrLn stderr err
     exitFailure

covering
bashCompletion : HasIO io =>
                 (curWord : String)
              -> (prevWord : String)
              -> io ()
bashCompletion curWord prevWord =
  do Right config <- loadConfig False
       | Left _ => pure ()
     let completions = BashCompletion.opts curWord prevWord
     putStr $ unlines completions

resolve'' : Promise () -> IO ()
resolve'' = resolve' pure exitError

assign : Config => Git => Octokit =>
         (assignArgs : List String)
      -> {default False dry : Bool}
      -> Promise ()
assign args {dry} =
  do (_, openPr) <- identifyOrCreatePR !currentBranch
     let (forcedReviewers, teamNames) = partitionedArgs
     requestReviewers openPr teamNames forcedReviewers {dry}
  where
    -- partition args into user logins and team slugs
    partitionedArgs : (List String, List String)
    partitionedArgs =
      let part = partition (isPrefixOf "+") args
      in  mapFst (map $ drop 1) part

listTeam : Config => Octokit =>
           (team : String)
        -> Promise ()
listTeam @{config} team =
  do teamMemberLogins <- sort <$> listTeamMembers config.org team
     teamMembersJson <- promiseAll =<< traverse forkedUser teamMemberLogins
     teamMembers <- traverse (either . parseUser) teamMembersJson
     liftIO . putDoc . vsep $ putNameLn <$> teamMembers
  where
    forkedUser : (login : String) -> Promise Future
    forkedUser = fork . ("user --json " ++)

    putNameLn : User -> Doc AnsiStyle
    putNameLn user =
      hsep [(fillBreak 15 . annotate italic $ pretty user.login), "-", (pretty user.name)]

graphTeam : Config => Octokit =>
            (team : String)
         -> Promise ()
graphTeam @{config} team =
  do teamMemberLogins <- listTeamMembers config.org team
     (openReviewers, closedReviewers) <- listReviewers 100 {pageBreaks=4}
     liftIO . putDoc . maybeDecorated $ reviewsGraph closedReviewers openReviewers teamMemberLogins
  where
    maybeDecorated : Doc AnsiStyle -> Doc AnsiStyle
    maybeDecorated = if config.colors then id else unAnnotate

contribute : Config => Octokit =>
             Nat
          -> Promise ()
contribute @{config} skip =
  do openPrs <- listPullRequests config.org config.repo (Just Open) 100
     myLogin <- login <$> getSelf
     let filtered = filter (not . isAuthor myLogin) openPrs
     let parted = partition (isRequestedReviewer myLogin) filtered
     let (mine, theirs) = (mapHom $ sortBy (compare `on` .createdAt)) parted
     let url = map (.webURI) . head' . drop skip $ mine ++ theirs
     printResult url
  where
    printResult : Maybe String -> Promise ()
    printResult Nothing    = reject "No open PRs to review!"
    printResult (Just url) = putStrLn url

handleConfiguredArgs : Config => Git => Octokit =>
                       List String
                    -> Promise ()
handleConfiguredArgs @{config} [] =
  putStrLn $ help config.colors

-- internal-use commands for forking process:
handleConfiguredArgs @{config} ["reviews", "--json", prNumber] =
  whenJust (parsePositive prNumber) $ \pr => do
    reviewsJsonStr <- listPullReviewsJsonStr config.org config.repo pr
    putStr reviewsJsonStr
handleConfiguredArgs @{config} ["pulls", "--json", pageLimit, page] =
  let args : Maybe (Fin 101, Nat) = bitraverse parseLim parsePg (pageLimit, page)
  in  whenJust args $ \(lim, pg) => do
        pullsJsonStr <- listPullRequestsJsonStr config.org config.repo Nothing lim {page=pg}
        putStr pullsJsonStr
  where
    parseLim : String -> Maybe (Fin 101)
    parseLim = (\x => natToFin x 101) <=< parsePositive

    parsePg  : String -> Maybe Nat
    parsePg = parsePositive
handleConfiguredArgs @{config} ["user", "--json", username] =
  print $ json !(getUser username)

-- user-facing commands:
handleConfiguredArgs ["sync"] =
  ignore $ syncConfig True
handleConfiguredArgs ["pr"] =
  do (Identified, pr) <- identifyOrCreatePR !currentBranch
       | _ => pure ()
     putStrLn pr.webURI
handleConfiguredArgs ["reflect"] =
  reflectOnSelf
handleConfiguredArgs ["config", prop] =
  do value <- getConfig prop
     putStrLn value
handleConfiguredArgs ["config", prop, value] =
  ignore $ setConfig prop value
handleConfiguredArgs ["contribute"] =
  contribute 0
handleConfiguredArgs ["contribute", skipArg] =
  case unpack skipArg of
       ('-' :: skip) => do
         let (Just num) : Maybe Nat = map cast . parsePositive $ pack skip
           | Nothing => exitError "contribute's argument must be -<num> where <num> is an integer."
         contribute num
       _             => exitError "contribute's argument must be -<num> where <num> is an integer."
handleConfiguredArgs ["list"] =
  reject "The list command expects the name of a GitHub Team as an argument."
handleConfiguredArgs @{config} ["list", teamName] =
  listTeam teamName
handleConfiguredArgs ["graph"] =
  reject "The graph command expects the name of a GitHub Team as an argument."
handleConfiguredArgs @{config} ["graph", teamName] =
  graphTeam teamName
handleConfiguredArgs ["assign"] =
  reject "The assign commaand expects one or more names of GitHub Teams or Users as arguments."
handleConfiguredArgs ["assign", "--dry"] =
  reject "The assign commaand expects one or more names of GitHub Teams or Users as arguments."
handleConfiguredArgs ("assign" :: "--dry" :: assign1 :: assignRest) =
  assign (assign1 :: assignRest) {dry=True}
handleConfiguredArgs ("assign" :: assign1 :: assignRest) =
  assign (assign1 :: assignRest)

-- error case:
handleConfiguredArgs args =
  reject "Unexpected command line arguments: \{show args}."

-- bash completion is a special case where we don't want to create the config
-- if it doesn't exist yet so we handle it up front before loading config and then
-- handling any other input.
covering
handleArgs : Git => Octokit =>
             (terminalColors : Bool)
          -> List String
          -> IO ()
handleArgs _ ["--bash-completion", curWord, prevWord] = bashCompletion curWord prevWord
handleArgs _ ["--bash-completion-script"] = putStrLn BashCompletion.script
handleArgs terminalColors args =
  resolve'' $
    do -- create the config file before continuing if it does not exist yet
       _ <- syncIfOld =<< loadOrCreateConfig terminalColors
       -- then handle any arguments given
       handleConfiguredArgs args

covering
main : IO ()
main =
  do terminalColors <- isTTY stdout
     -- drop 2 for `node` and `harmony.js`
     args <- drop 2 <$> getArgs
     -- short circuit for help
     when (args == ["help"] || args == ["--help"]) $ do
       putStrLn $ help terminalColors
       exitSuccess
     -- otherwise get a GitHub Personal Access Token and continue.
     Just pat <- getEnv "GITHUB_PAT"
       | Nothing => exitError "GITHUB_PAT environment variable must be set to a personal access token."
     _ <- octokit pat
     _ <- git
     handleArgs terminalColors args

max_stars_repo_name: mattpolzin/harmony

max_issues_repo_name: mattpolzin/harmony

max_forks_repo_name: mattpolzin/harmony


text:
data Bool = False | True

data Direction = North | South | East | West

turnClockwize : Direction -> Direction
turnClockwize North = East
turnClockwize South = South
turnClockwize East = West
turnClockwize West = North

||| Represents shapes
data Shape = |||A triangle with its base length and height
             Triangle Double Double
           | ||| A rectangle, with its length and height
             Rectangle Double Double
           | ||| A circle with its radius
             Circle Double

{-
data Shape : Type where
     Triangle : Double -> Double -> Shape
     Rectangle : Double -> Double -> Shape
     Circle : Double -> Shape
-}

area : Shape -> Double
area (Triangle base height) = 0.5 * base * height
area (Rectangle length height) = length * height
area (Circle radius) = pi * radius * radius

data Picture = Primitive Shape
             | Combine Picture Picture
             | Rotate Double Picture
             | Translate Double Double Picture

rectangle : Picture
rectangle = Primitive (Rectangle 20 10)

circle : Picture
circle = Primitive (Circle 5)

triangle : Picture
triangle = Primitive (Triangle 10 10)

testPicture : Picture
testPicture = Combine (Translate 5 5 rectangle)
                      (Combine (Translate 35 5 circle)
                      (Translate 15 25 triangle))

pictureArea : Picture -> Double
pictureArea (Primitive shape) = area shape
pictureArea (Combine pic pic1) = pictureArea pic + pictureArea pic1
pictureArea (Rotate x pic) = pictureArea pic
pictureArea (Translate x y pic) = pictureArea pic

data Infinite = Forever Infinite

safeDivide : Double -> Double -> Maybe Double
safeDivide x y = if y == 0 then Nothing
                           else Just (x / y)

data Either a b = Left a | Right b

data Tree elem = Empty
               | Node (Tree elem) elem (Tree elem)
%name Tree tree, tree1

maxMaybe : Ord a => Maybe a -> Maybe a -> Maybe a
maxMaybe Nothing Nothing = Nothing
maxMaybe Nothing (Just x) = Just x
maxMaybe (Just x) Nothing = Just x
maxMaybe (Just x) (Just y) = Just (max x y)

biggestTriangle : Picture -> Maybe Double
biggestTriangle (Primitive triangle@(Triangle x y)) = Just (area triangle)
biggestTriangle (Primitive (Rectangle x y)) = Nothing
biggestTriangle (Primitive (Circle x)) = Nothing
biggestTriangle (Combine x y) = maxMaybe (biggestTriangle x) (biggestTriangle y)
biggestTriangle (Rotate x y) = biggestTriangle y
biggestTriangle (Translate x y z) = biggestTriangle z

testPic1 : Picture
testPic1 = Combine (Primitive (Triangle 2 3))
                   (Primitive (Triangle 2 4))

testPic2 : Picture
testPic2 = Combine (Primitive (Rectangle 1 3))
                   (Primitive (Circle 4))


text:
> module Functor.Operations

> %default total
> %access public export
> %hide elem

Cezar's membership test:

> |||
> elem : {A : Type} -> {F : Type -> Type} ->
>        (Functor F) => Eq A => Eq (F Bool) =>
>        A -> F A -> Bool
> elem a fa = map (const True) fa /= map (a /=) fa

> |||
> Elem : {A : Type} -> {F : Type -> Type} ->
>        (Functor F) => Eq A => Eq (F Bool) =>
>        A -> F A -> Type
> Elem a fa with (elem a fa)
>   | True  = Unit
>   | False = Void

> |||
> decElem : {A : Type} -> {F : Type -> Type} ->
>           (Functor F) => Eq A => Eq (F Bool) =>
>           (a : A) -> (fa : F A) -> Dec (a `Elem` fa)
> decElem a fa with (elem a fa)
>   |  True = Yes ()
>   | False =  No id


text:
module Toolkit.Data.List.Subset

import Toolkit.Decidable.Informative

%default total

public export
data Subset : (eq   : a -> b -> Type)
           -> (this : List a)
           -> (that : List b)
                   -> Type
  where
    Empty : Subset eq Nil Nil

    EmptyThis : Subset eq Nil xs

    Keep : {eq : a -> b -> Type}
        -> (prf  :        eq  x       y)
        -> (rest : Subset eq    xs      ys)
                -> Subset eq (x::xs) (y::ys)

    Skip : (rest : Subset eq xs     ys)
                -> Subset eq xs (y::ys)

public export
data Error : Type -> Type where
  EmptyThat : Error a
  Fail : a -> Error a
  FailThere : Error a -> Error a

emptyThat : Subset eq (x :: xs) [] -> Void
emptyThat Empty impossible

yesButNo : {eq : a -> b -> Type}
        -> {x : a} -> {xs : List a}
        -> {y : b} -> {ys : List b}
        -> (h : Subset eq     xs       ys -> Void)
        -> (t : Subset eq (x::xs)      ys -> Void)
             -> Subset eq (x::xs) (y::ys)
             -> Void
yesButNo h t (Keep prf rest) = h rest
yesButNo h t (Skip rest) = t rest

justNot : {eq : a -> b -> Type}
       -> {x : a} -> {xs : List a}
       -> {y : b} -> {ys : List b}
       -> (eq x y -> Void)
       -> (Subset eq (x :: xs) ys -> Void   )
       -> Subset eq (x :: xs) (y :: ys)
       -> Void
justNot f g (Keep prf rest) = f prf
justNot f g (Skip rest) = g rest

export
subset : {eq   : a -> b -> Type}
      -> (test : (x : a) -> (y : b) -> DecInfo err (eq x y))
      -> (this : List a)
      -> (that : List b)
              -> DecInfo (Error err) (Subset eq this that)
subset test [] []
  = Yes Empty

subset test [] (x :: xs)
  = Yes EmptyThis

subset test (x :: xs) []
  = No EmptyThat emptyThat

subset test (x :: xs) (y :: ys) with (test x y)
  subset test (x :: xs) (y :: ys) | (Yes prfHere) with (subset test xs ys)
    subset test (x :: xs) (y :: ys) | (Yes prfHere) | (Yes prfThere)
      = Yes (Keep prfHere prfThere)
    subset test (x :: xs) (y :: ys) | (Yes prfHere) | (No msgWhyNot prfWhyNot) with (subset test (x::xs) ys)
      subset test (x :: xs) (y :: ys) | (Yes prfHere) | (No msgWhyNot prfWhyNot) | (Yes prfThere)
        = Yes (Skip prfThere)
      subset test (x :: xs) (y :: ys) | (Yes prfHere) | (No msgWhyNotHere prfWhyNotHere) | (No msgWhyNotThere prfWhyNotThere)
        = No (FailThere msgWhyNotThere)
             (yesButNo prfWhyNotHere prfWhyNotThere)

  subset test (x :: xs) (y :: ys) | (No msgWhyNotHere prfWhyNotHere) with (subset test (x::xs) ys)
    subset test (x :: xs) (y :: ys) | (No msgWhyNotHere prfWhyNotHere) | (Yes prfThere)
      = Yes (Skip prfThere)
    subset test (x :: xs) (y :: ys) | (No msgWhyNotHere prfWhyNotHere) | (No msgWhyNotThere prfWhyNotThere)
      = No (FailThere msgWhyNotThere)
           (justNot prfWhyNotHere prfWhyNotThere)

max_stars_repo_name: gallais/linear-circuits

max_issues_repo_name: gallais/linear-circuits

max_forks_repo_name: gallais/linear-circuits


text:
module Chapter5

import Data.Vect

%default total

printLength : HasIO io => io ()
printLength = putStr "Enter a string: " >>= \_ =>
                getLine >>= \input =>
                  let len = length input in
                    putStrLn $ "\"" ++ input ++ "\" has length " ++ show len

printTwoThings : HasIO io => io ()
printTwoThings = do putStrLn "Hello"
                    putStrLn "World"

printThreeThings : HasIO io => io ()
printThreeThings = putStrLn "Hello" >>= \_ =>
                    putStrLn "World" >>= \_ =>
                      putStrLn "Again"

printInput : HasIO io => io ()
printInput = do x <- getLine
                putStrLn x

printLengthAgain : HasIO io => io ()
printLengthAgain = do putStr "Enter a string: "
                      string <- getLine
                      let len = length string -- no `in` here
                      putStrLn $ "\"" ++ string ++ "\" has length " ++ show len

readPair : HasIO io => io (String, String)
readPair = do f <- getLine
              s <- getLine
              pure (f, s)

usePair : HasIO io => io ()
usePair = do p <- readPair
             case p of
                  (f, s) => putStrLn $ "You entered the following strings: " ++ f ++ ", " ++ s

-- destructuring pattern-matching

usePairImproved : HasIO io => io ()
usePairImproved = do (f, s) <- readPair
                     putStrLn $ "You entered the following strings: " ++ f ++ ", " ++ s

-- reading and validating dependent types

myZip : Vect n a -> Vect n b -> Vect n (a, b)
myZip [] [] = []
myZip (x :: xs) (y :: ys) = (x, y) :: myZip xs ys

partial
readVect : HasIO io => io (n : Nat ** Vect n String)
readVect = do x <- getLine
              if x == ""
                 then pure $ (_ ** [])
                 else do (_ ** xs) <- readVect
                         pure $ (_ ** (x :: xs))

partial
zipInputs : HasIO io => io ()
zipInputs = do putStrLn "Enter the first vector (blank line to end)"
               (len1 ** xs) <- readVect
               putStrLn "Enter the second vector (blank line to end)"
               (len2 ** ys) <- readVect
               case exactLength len1 ys of -- exactLength is needed here to ensure type safety (== check would not work)
                    Nothing => putStrLn "Vectors are of different lengths"
                    Just ys' => printLn $ zip xs ys'

max_stars_repo_name: timmyjose-study/tdd-with-idris

max_issues_repo_name: timmyjose-study/tdd-with-idris

max_forks_repo_name: timmyjose-study/tdd-with-idris


text:
data Vect : Nat -> Type -> Type where
     Nil : Vect Z a
     (::) : a -> Vect k a -> Vect (S k) a

append : Vect n a -> Vect m a -> Vect (n + m) a
append [] ys = ys
append (x :: xs) ys = x :: append xs ys


text:
module Graphs1
import Data.Vect

%access public export

{-This program works only for simple undirected graphs. and whenever I use "am" it means adjacency matrix.
Please give a symmetric matrix for am. The important functions in this program are
EdgeisPath
ConnectedComponents
PathWithProof
AdjacentsAreConnected
-}
|||Checks whether 2 numbers are equal and returns nothing or a proof of equality
checkEqNat: (num1:Nat)->(num2:Nat)->Maybe (num1=num2)
checkEqNat Z Z = Just Refl
checkEqNat Z (S k) = Nothing
checkEqNat (S k) Z = Nothing
checkEqNat (S k) (S j) = case checkEqNat k j of
                              Nothing => Nothing
                              (Just x) => Just (cong x)
|||Returns the i j element of an m by n matrix and nothing if ij is out of bounds.
Access : Vect m (Vect n Nat)->(i:Nat)->(j:Nat)->Maybe Nat
Access {n}{m} xs i j = case ((integerToFin  ((cast j)-1) n),(integerToFin  ((cast i)-1) m)) of
                         (Nothing, _) => Nothing
                         (_ ,Nothing) => Nothing
                         (Just x, Just y) => Just ((Vect.index x (Vect.index y xs)))

|||Returns the i j element of an n by n matrix with 0 if it is out of bounds
Accessnum:Vect n (Vect n Nat)->(i:Nat)->(j:Nat)-> Nat
Accessnum xs i j = case Access xs i j of
                    Nothing => 0
                    (Just x) => x
|||A type inhabited if only if vertices i and j are connected by an edge
data Edge :(am:(Vect n (Vect n Nat)))-> (i:Nat)->(j:Nat)->Type where
    Thereisanedge :(am:(Vect n (Vect n Nat)))-> (i:Nat)->(j:Nat)->(Accessnum am i j) =1 ->Edge am i j
|||A type inhabited iff vertices i and j are connected by a path
data Path : (am:(Vect n (Vect n Nat)))-> (i:Nat)->(j:Nat)->Type where
  Self : (i:Nat)->Path am i i
  Adjacent : (Edge am i j) ->Path am i j
  Thereispath: (am:(Vect n (Vect n Nat)))-> (i:Nat)->(k:Nat) ->Path am i k->(Edge am j i)->Path am j k
|||Returns Nothing if there is no edge or a proof that Accessnum am i j =1
Isthereanedge: (am:(Vect n (Vect n Nat)))-> (i:Nat)->(j:Nat)->Maybe ( (Accessnum am i j ) = 1)
Isthereanedge am i j = case Access am i j of
                            Nothing => Nothing
                            (Just x) => (case checkEqNat (Accessnum am i j ) 1 of
                                              Nothing => Nothing
                                              (Just y) => (Just y))
|||Returns a proof that 2 adjacent vertices are connected or nothing if they are not connected.
AdjacentsAreConnected:(am:(Vect n (Vect n Nat)))-> (i:Nat)->(j:Nat)->Maybe (Path am i j)
AdjacentsAreConnected am i j = case Isthereanedge am i j of
                                    Nothing => Nothing
                                    (Just x) => Just (Adjacent (Thereisanedge am i j x))
|||Proves that adjacent vertices (ie vertices that have an edge between them are connected)
EdgeisPath :(am:(Vect n (Vect n Nat)))-> (Edge am i j)->Path am i j
EdgeisPath am (Thereisanedge am i j prf) = Adjacent (Thereisanedge am i j prf)

|||Checks whether a Natural number is in the list or not
isInList  : (i:Nat)->List Nat ->Bool
isInList i [] = False
isInList i (x :: xs) = case (x==i) of
                            False => isInList i xs
                            True => True
|||Updates an adjacency list if there is an edge between i and (S j) and calls the same function with j
adja :(am:(Vect n (Vect n Nat)))-> (i:Nat)->(j:Nat)  ->List (s:Nat**Path am i s)->List (s:Nat**Path am i s)
adja am i Z xs = xs
adja am i (S k) xs = case AdjacentsAreConnected am i (S k) of
                      Nothing => adja am i k xs
                      (Just x) => adja am i k (((S k )**x)::xs)
|||Returns a list of adjacent vectors to i with a proof that they are connected
Adjacents :(am:(Vect n (Vect n Nat)))-> (i:Nat)->List (s:Nat**Path am i s)
Adjacents {n} am i = adja am i n []
Adjacentlist:(am:(Vect n (Vect n Nat)))-> (i:Nat)->List Nat
Adjacentlist am i = map fst (Adjacents am i)
|||Returns the list of elements in the first list, but not in the second
Complement: List Nat ->List Nat ->List Nat
Complement [] ys = []
Complement (x :: xs) ys = case isInList x ys of
                               False => x::(Complement xs ys)
                               True => Complement xs ys

|||Does Depth first search of i and returns the list of elements connected to i
Dfs :(am:(Vect n (Vect n Nat)))-> (i:Nat) ->List Nat->List Nat
Dfs am i xs = case Complement (Adjacentlist am i) xs of
                     []=>xs
                     (j::ys)=>Dfs am i (Dfs am j (j::xs))

|||A helper function for ConnectedComponents
Connectedcompos: (am:(Vect n (Vect n Nat)))->List Nat ->List (List Nat)->(List (List Nat))
Connectedcompos{n} am xs ys = case Complement [1..n] xs of
                                [] => ys
                                (x :: zs) => Connectedcompos am (xs++(Dfs am x [x])) ((Dfs am x [x])::ys)

|||Gives the connected components of a graph as a list of lists
ConnectedComponents :  (am:(Vect n (Vect n Nat)))->(List (List Nat))
ConnectedComponents am = Connectedcompos am [] []

|||Modified depth first search which searches for a path between i and k. When there is no path, it behaves just like a depth first search from i
Dfss :(am:(Vect n (Vect n Nat)))-> (i:Nat) ->(k:Nat)->(Found:Bool)->List Nat->List Nat->((List Nat,List Nat),Bool)
Dfss am i k True path visit = ((path,visit),True)
Dfss am i k False path visit = case Complement (Adjacentlist am i) visit of
                     []=>(([],visit),False)
                     (j::ys)=>(case (k==j) of
                       True =>(((k::path),(j::visit)),True)
                       False =>  let dps =(Dfss am j k False (j::path) (j::visit)) in (let pathn = (case (snd(dps)) of
                                                                                False => path
                                                                                True => (fst (fst (dps)))) in (Dfss am i k  (snd(dps)) pathn (snd (fst (dps))))))

||| Ruturns a path between 2 vertices and returns Nothing if there is no path.
FindPath :(am:(Vect n (Vect n Nat)))->(k:Nat)->(i:Nat)->Maybe (List Nat)
FindPath am k i = case (k==i) of
                  True => Just [i]
                  False =>   (case isInList k (Dfs am  i [i])  of
                     False => Nothing
                     True => Just (fst (fst (Dfss am i k False [i] [i]))))
|||Gives the proof that there is a path between i and k when the path is not just one vertex long
Proofcon2 :(am:(Vect n (Vect n Nat)))-> List Nat -> (i:Nat)->(k:Nat)-> Path am i k
Proofcon2 am [j,p] i k = case checkEqNat p k of
                           (Just Refl) => (case AdjacentsAreConnected am i k of
                                                (Just x) => x)
Proofcon2 am (x::y::z::xs) i k =case AdjacentsAreConnected am i y of
                                                           (Just (Adjacent x)) => (let loop = Proofcon2 am (y::z::xs) y k in
                                                                 Thereispath am y k loop x )

|||Gives proof for 1 vertex long paths and calls proofcon2 when there are at least 2 vertices in the path
Proofcon :(am:(Vect n (Vect n Nat)))-> List Nat -> (i:Nat)->(k:Nat)-> Path am i k
Proofcon am xs i k = case checkEqNat i k of
                          (Just Refl) => Self i
                          Nothing => Proofcon2 am xs i k
|||Gives a path with proof when there is a path between k and i and Nothing when there is no path.
PathWithProof :(am:(Vect n (Vect n Nat)))->(k:Nat)->(i:Nat)->Maybe((List Nat),Path am k i )
PathWithProof am k i = case FindPath am k i of
                        Nothing => Nothing
                        Just x => Just (x,Proofcon am x k i)


text:
module Inigo.Archive.Archive

import Toml
import Data.List

export
encode : List (List String, String) -> String
encode =
	Toml.encode . map (\(k, v) => (k, Str v))

export
decode : String -> Maybe (List (List String, String))
decode toml =
	do
		doc <- parseToml toml
		res <- foldl accumulate (Just []) doc
		pure (reverse res)
	where
		accumulate : Maybe (List (List String, String)) -> (List String, Value) -> Maybe (List (List String, String))
		accumulate Nothing _ = Nothing
		accumulate (Just acc) (key, Str str) = Just ((key, str) :: acc)
		accumulate _ _ = Nothing

max_stars_repo_name: Z-snails/inigo

max_issues_repo_name: Z-snails/inigo

max_forks_repo_name: Z-snails/inigo


text:
module Door

import Effects
import Effect.StdIO

data DoorState = Closed | Open

data DoorInfo : DoorState -> Type where
     DI : DoorInfo s

data Jam = Jammed | OK

data Door : Effect where
      OpenDoor : sig Door Jam (DoorInfo Closed)
                           (\jammed =>
                            DoorInfo (case jammed of
                                           Jammed => Closed
                                           OK => Open))
      CloseDoor : sig Door () (DoorInfo Open) (DoorInfo Closed)
      Knock : sig Door () (DoorInfo Closed)

DOOR : DoorState -> EFFECT
DOOR t = MkEff (DoorInfo t) Door

openDoor : Eff Jam [DOOR Closed]
                   (\jammed => [DOOR (case jammed of
                                        Jammed => Closed
                                        OK => Open)])
openDoor = call OpenDoor

closeDoor : Eff () [DOOR Open] [DOOR Closed]
closeDoor = call CloseDoor

knock : Eff () [DOOR Closed]
knock = call Knock

doorProg : Eff () [STDIO, DOOR Closed]
doorProg = do OK <- openDoor | Jammed => putStrLn "It's stuck!"
              closeDoor
              knock
              OK <- openDoor | Jammed => putStrLn "It's stuck!"
              closeDoor

max_stars_repo_name: idris-hackers/idris-demos

max_issues_repo_name: idris-hackers/idris-demos

max_forks_repo_name: idris-hackers/idris-demos


text:
module IdrisNet2.PacketLang
import Language.Reflection
import Data.So
import Data.Vect

%access public

-- Propositions about data
data Proposition : Type where
  P_LT : Nat -> Nat -> Proposition
  P_EQ : DecEq a => a -> a -> Proposition
  P_BOOL : Bool -> Proposition
  P_AND : Proposition -> Proposition -> Proposition
  P_OR : Proposition -> Proposition -> Proposition

Length : Type
Length = Int

-- grrrrr, hackity hack
natToInt : Nat -> Int
natToInt Z = 0
natToInt (S k) = 1 + (natToInt k)

intToNat : Int -> Nat
intToNat 0 = Z
intToNat i = if i < 0 then Z else (assert_total (S (intToNat (i - 1))))

strLen : String -> Int
strLen s = natToInt $ length s

data Bounded : Nat -> Type where
  BInt : (x : Int) -> (prf : So (x < (pow 2 i))) -> Bounded i

instance Show (Bounded i) where
  show (BInt x _) = show x

val : Bounded i -> Int
val (BInt i p) = i

mkBounded : (bound : Nat) -> Int -> Maybe (Bounded bound)
mkBounded b i_n =
  case choose (i_n < (pow 2 b)) of
      Left yes => Just (BInt i_n yes)
      Right _ => Nothing

NonZero : Nat -> Type
NonZero n = n `GT` 0

-- Primitive Binary Chunks
data Chunk : Type where
  -- Bits must be at least 1 wide
  Bit : (width : Nat) -> NonZero width -> Chunk
  -- Boolean value, stored as one bit.
  -- Convenience, so we can marshal / unmarshal directly as a Bool
  CBool : Chunk
  -- Native C String, null terminated
  CString : Chunk
  -- String with fixed bounded length
  LString : Nat -> Chunk
  -- String with dynamic bounded length
  --LString : ((length s) ** (s : String)) -> Chunk
  -- Proposition about data
  Prop : (P : Proposition) -> Chunk
  -- Custom chunk of binary data.
  -- Can be used to make cleverer things without having
  -- to add to the core PL each time.
  Decodable : (n : Nat) ->
              (t : Type) ->
              (Bounded n -> Maybe t) ->
              (t -> Bounded n) -> Chunk

infixl 5 //
--infixl 5 ##

mutual
  -- Requires two propositions, and evidence that they're true.
  -- For example, if we have P_AND P_BOOL P_BOOL, we'd need two 'oh' proofs.
  -- If we had two P_EQ propositions, we'd need two reflexivity proofs.
  data Both : Proposition -> Proposition -> Type where
    MkBoth : (propTy a) -> (propTy b) -> Both a b

  -- Decode propositions into Idris types.
  propTy : Proposition -> Type
  propTy (P_LT x y) = LT x y
  propTy (P_EQ x y) = x=y
  propTy (P_BOOL b) = So b
  propTy (P_AND s t) = Both s t
  propTy (P_OR s t) = Either (propTy s) (propTy t)

-- Decode chunks into Idris types
-- TODO <<
chunkTy : Chunk -> Type
chunkTy (Bit w p) = Bounded w
chunkTy CString = String
chunkTy (LString i) = String
chunkTy (Prop p) = propTy p
chunkTy (CBool) = Bool
chunkTy (Decodable n t encode_fn decode_fn) = t

-- Packet Language
mutual
  data PacketLang : Type where
    CHUNK : (c : Chunk) -> PacketLang
    IF : (test : Bool) -> (yes : PacketLang) -> (no : PacketLang) -> PacketLang
    -- // : or
    (//) : PacketLang -> PacketLang -> PacketLang
    LIST : PacketLang -> PacketLang
    LISTN : (n : Nat) -> PacketLang -> PacketLang
    NULL : PacketLang -- Sometimes, we want to signify that there's nothing there
    (>>=) : (p : PacketLang) -> (mkTy p -> PacketLang) -> PacketLang

  -- Packet language decoding
  mkTy : PacketLang -> Type
  mkTy (CHUNK c) = chunkTy c
  mkTy (IF x t e) = if x then (mkTy t) else (mkTy e)
  mkTy (l // r) = Either (mkTy l) (mkTy r)
  mkTy (LIST x) = List (mkTy x)
  mkTy (LISTN n a) = Vect n (mkTy a)
  mkTy NULL = ()
  mkTy (c >>= k) = (x ** mkTy (k x))

{- Chunk length in bits -}
bitLength : (pl : PacketLang) -> mkTy pl -> Length
chunkLength : (c : Chunk) -> chunkTy c -> Length
chunkLength (Bit w p) _ = natToInt w
chunkLength CBool _ = 1
chunkLength CString str = 8 * ((strLen str) + 1)
chunkLength (LString len) str = 8 * (natToInt len)
chunkLength (Prop _) p = 0 -- Not written to the packet
chunkLength (Decodable n _ _ _) _ = natToInt n

listLength : (pl : PacketLang) -> List (mkTy pl) -> Length
listLength pl [] = 0
listLength pl (x :: xs) = bitLength pl x + (listLength pl xs)

vectLength : (pl : PacketLang) -> Vect n (mkTy pl) -> Length
vectLength pl [] = 0
vectLength pl (x :: xs) = bitLength pl x + (vectLength pl xs)

bitLength (CHUNK c) x = chunkLength c x
bitLength (IF True yes _) x = bitLength yes x
bitLength (IF False _ no) x = bitLength no x
bitLength (y // z) x = either (\l_x => bitLength y l_x) (\r_x => bitLength z r_x) x
bitLength (LIST pl) x = listLength pl x
bitLength (LISTN n pl) x = vectLength pl x
bitLength NULL _ = 0
bitLength (c >>= k) (a ** b) = bitLength c a + bitLength (k a) b

-- Syntax rules, so it's nicer to write these things...
bit : (w : Nat) -> {auto p : NonZero w} -> Chunk
bit w {p} = Bit w p

-- syntax bit [x] = Bit x oh
--syntax bytes [n] = CHUNK (bit (n * 8))
--syntax bounded [x] = BInt x oh

-- PacketLang DSL syntax
syntax bits [n] = (CHUNK (bit n))
syntax check [b] = (CHUNK (Prop (P_BOOL b)))
syntax lstring [n] = (CHUNK (LString n))
syntax cstring = (CHUNK (CString))
syntax listn [n] [t] = (LISTN n t)
syntax list [t] = (LIST t)
syntax p_if [b1] then [b2] else [b3] = (IF b1 b2 b3)
syntax p_either [t1] [t2] = (t1 // t2)
syntax bool = (CHUNK (CBool))
syntax prop [p] = (CHUNK (Prop p))
syntax null = NULL
syntax decodable [n] [ty] [fn1] [fn2] = (CHUNK (Decodable n ty fn1 fn2))
-- Propositions
syntax prop_bool [p] = (P_BOOL p)
syntax prop_or [p1] [p2] = (P_OR p1 p2)
syntax prop_and [p1] [p2] = (P_AND p1 p2)
syntax prop_eq [p1] [p2] = (P_EQ p1 p2)

-- Additional sugar
syntax [x] "##" [y] = (x ** y)


text:
module Language.JSON.Decode

import Data.List

import Language.JSON
import Language.JSON.Data

||| JavaScript types as values for specifing schemas and types without attaching a value.
public export
data JType
   = JTNull
   | JTBoolean
   | JTNumber
   | JTString
   | JTArray
   | JTObject

public export
Eq JType where
 (==) JTNull JTNull = True
 (==) JTBoolean JTBoolean = True
 (==) JTNumber JTNumber = True
 (==) JTString JTString = True
 (==) JTArray JTArray = True
 (==) JTObject JTObject = True
 (==) _ _ = False

public export
Show JType where
  show JTNull = "JTNull"
  show JTBoolean = "JBoolean"
  show JTNumber = "JTNumber"
  show JTString = "JTString"
  show JTArray = "JTArray"
  show JTObject = "JTObject"

public export
valToType : JSON -> JType
valToType JNull = JTNull
valToType (JBoolean _) = JTBoolean
valToType (JNumber _) = JTNumber
valToType (JString _) = JTString
valToType (JArray _) = JTArray
valToType (JObject _) = JTObject

||| Represent the various errors that may happen when trying to decode JSON.
public export
data JSONError : Type where
  JSONParseErr : JSONError      -- Represent errors from Language.JSON.parse
  JSONGenericErr : String -> JSONError -- for incremental refactoring from old errors
  JSONTypeErr : (expected : JType) -> (actual : JType) -> JSONError
  JSONDeliberateFail : JSONError -> JSONError -- to cover `fail`
  JSONNoSuchField : (expected : String) -> (actualObj : String) -> JSONError

public export
Show JSONError where
  show JSONParseErr = "JSONParseErr"
  show (JSONGenericErr x) = x
  show (JSONTypeErr x y) = "JSONTypeErr expected " ++ (show x) ++ " actual " ++ (show y)
  show (JSONDeliberateFail x) = "JSONDeliberateFail " ++ (show x)
  show (JSONNoSuchField e a) = "JSONNoSuchField expected " ++ e ++ " in " ++ a

public export
Eq JSONError where
  (==) JSONParseErr JSONParseErr = True
  (==) (JSONGenericErr a) (JSONGenericErr b) = a == b
  (==) (JSONTypeErr a b) (JSONTypeErr c d) = a == c && b == d
  (==) (JSONDeliberateFail a) (JSONDeliberateFail b) = a == b
  (==) (JSONNoSuchField e1 a1) (JSONNoSuchField e2 a2) = e1 == e2 && a1 == a2
  (==) _ _ = False

||| Describes how to turn a `JSON` into a `v`.
||| Use with `decodeJSON` or `decodeString`.
public export
Decoder : Type -> Type
Decoder = \v => JSON -> Either JSONError v

private
error : String -> Decoder a
error expected actual =
    Left $ JSONGenericErr $ "Expected " ++ expected ++ ", got: " ++ format 0 actual

||| Run a `Decoder` on some `JSON`.
public export
decodeJSON : Decoder a -> JSON -> Either JSONError a
decodeJSON decoder json =
    decoder json

||| Parse a `String` to `JSON` and run a `Decoder` on it
public export
decodeString : Decoder a -> String -> Either JSONError a
decodeString decoder str =
    case parse str of
        Just json => decoder json
        Nothing => Left JSONParseErr

||| Given a function, transform a decoder's result
public export
map : (a -> b) -> Decoder a -> Decoder b
map f decoder =
    \json =>
    case decoder json of
        Right x => Right (f x)
        Left x => Left x

||| Always decode the given value. Alias of `pure`.
public export
succeed : a -> Decoder a
succeed x _ =
    Right x

||| Always fail with the given error.
public export
fail : JSONError -> Decoder a
fail err _ =
    Left $ JSONDeliberateFail err

||| Apply a function to the result of a decoder to get another decoder, then run that
public export
andThen : (a -> Decoder b) -> Decoder a -> Decoder b
andThen f decoder json =
    case decoder json of
        Right x => (f x) json
        Left x => Left x

||| Always decode the given value
public export
pure : a -> Decoder a
pure x json =
    Right x

||| Given a decoder of function and one argument, return a decoder of result
public export
ap : Decoder (a -> b) -> Decoder a -> Decoder b
ap df dx json =
    case (df json, dx json) of
        (Right f, Right x) => Right $ f x
        (Right f, Left err) => Left err
        (Left err, _ ) => Left err

||| Alias of apply
public export
(<*>) : Decoder (a -> b) -> Decoder a -> Decoder b
(<*>) = ap

||| Alias of map
public export
(<$>) : (a -> b) -> Decoder a -> Decoder b
(<$>) = map

||| Avoid infinite loops in recursive decoders by wrapping the recursive call with lazy
public export
lazy : (() -> Decoder a) -> Decoder a
lazy thunk =
  andThen thunk (succeed ())

||| Decode the given value when encountering JNull
public export
null' : a -> Decoder a
null' x JNull = Right x
null' _ json = Left $ JSONTypeErr JTNull (valToType json)

||| Decode a known null value, returning True if it was null, otherwise a type error.
public export
null : Decoder Bool
null (JNull) = Right True
null json = Left $ JSONTypeErr JTNull (valToType json)

||| Decode a JString
public export
string : Decoder String
string (JString str) = Right str
string json = Left $ JSONTypeErr JTString (valToType json)

||| Decode JBoolean
||| Renamed from "bool" because causing "INTERNAL ERROR: $bool is not a function application"
public export
bol : Decoder Bool
bol (JBoolean bool) = Right bool
bol json = Left $ JSONTypeErr JTBoolean (valToType json)

||| Decode a `JNumber` by casting it to `Int`
public export
int : Decoder Int
int (JNumber x) =
    if floor x == x
    then Right (cast x)
    else error {a = Int } "int" (JNumber x)
int json = Left $ JSONTypeErr JTNumber (valToType json)

||| Decode a `JNumber` as `Double`
public export
float : Decoder Double
float (JNumber x) = Right x
float json = Left $ JSONTypeErr JTNumber (valToType json)

||| Given a list of decoders, use the first one that succeeds
public export
oneOf : List (Decoder a) -> Decoder a
oneOf [] json = error "oneOf" json -- TODO improve
oneOf (d :: ds) json =
    case d json of
        Right v => Right v
        Left err => oneOf ds json

||| Decode a list of elements
||| If it encounters one or more errors, it returns the last error.
public export
list : Decoder a -> Decoder (List a)
list decoder (JArray lst) =
    foldr f (Right []) $ map decoder $ lst
    where
       f : Either JSONError a -> Either JSONError (List a) -> Either JSONError (List a)  -- FIXME
       f (Right v) (Right l) = Right (v :: l)
       f (Left err) _ = Left err
       f (Right v) (Left err) = Left err
list _ json = error "list" json

||| Decode a JObject as key-value pairs
public export
keyValuePairs : Decoder a -> Decoder (List (String, a))
keyValuePairs decoder (JObject o) =
    foldr f (Right []) $ map (\( k, v ) => ( k, decoder v)) $ o
    where
        f : ( String, Either JSONError a ) -> Either JSONError (List ( String, a )) -> Either JSONError (List ( String, a ))
        f ( k, Right v ) (Right lst) = Right (( k, v ) :: lst)
        f ( k, Right v) (Left err) = Left err
        f ( k, Left err ) _ = Left err
keyValuePairs _ json = error "keyValuePairs" json

||| Decode the given field in a `JObject`
public export
field : String -> Decoder a -> Decoder a
field key decoder json@(JObject fields) =
    case filter ((== key) . fst) fields of
        ( _, v ) :: _ => decoder v
        _ => Left $ JSONNoSuchField key (format 0 json)
field key _ json = Left $ JSONTypeErr JTObject (valToType json)

||| Decode a nested `JObject` field
public export
at : List String -> Decoder a -> Decoder a
at fields decoder =
    foldr field decoder fields

||| Temporarily borrow from Idris1 Prelude:
||| Attempt to find a particular element of a list.
|||
||| If the provided index is out of bounds, return Nothing.
index' : (n : Nat) -> (l : List a) -> Maybe a
index' Z     (x::xs) = Just x
index' (S n) (x::xs) = index' n xs
index' _     []      = Nothing

||| Decode the `n`th element of a `JArray`
public export
index : Int -> Decoder a -> Decoder a
index n decoder json@(JArray lst) =
    case index' (integerToNat (cast n)) lst of -- Int->Nat via Integer, no direct cast in Idris2.
        Just j => decoder j
        Nothing => error ("list of length > " ++ cast n ) json
index n decoder json =
      Left $ JSONTypeErr JTArray (valToType json)

||| Decode `Just` a value if the given decoder succeeds, `Nothing` otherwise
public export
maybe : Decoder a -> Decoder (Maybe a)
maybe decoder json =
    Right $ either (const Nothing) Just (decoder json)

||| Decode `Just` a value or `Nothing` in case of `JNull`
public export
nullable : Decoder a -> Decoder (Maybe a)
nullable decoder =
  oneOf
    [ null' Nothing
    , map Just decoder
    ]

max_stars_repo_name: scotek/idris-json-decode

max_issues_repo_name: scotek/idris-json-decode

max_forks_repo_name: scotek/idris-json-decode


text:
module HackyLang
-- Warning: only briefly tested, may have bugs

-- An expression
data Exp : Type where
  N : Nat -> Exp -- a literal natural number
  B : Bool -> Exp -- a literal boolean
  LTE : Exp -> Exp -> Exp
  EQ : Exp -> Exp -> Exp
  If :  Exp -> Exp -> Exp -> Exp -- if expression
  Var : (name: String) -> Exp -- a variable
  Lam :  (var : Exp) -> (value : Exp) -> Exp -- a lambda expression
  App : (f : Exp ) -> (arg: Exp) -> Exp -- function application
  Sum :  Exp -> Exp -> Exp -- sum
  Prod: Exp -> Exp -> Exp  -- product
  Pred: Exp -> Exp -- predecessor of a natural number
  Null : Exp
  Cons: Exp -> Exp -> Exp
  Left: Exp -> Exp
  Right : Exp -> Exp

-- substitute `x` by `y` in `base`
subs:  (base: Exp) -> (x: Exp) -> (y: Exp) -> Exp
subs  (N k) x y = N k
subs  (B z) x y = B z
subs  (LTE z w) x y = LTE (subs z x y) (subs  w x y)
subs  (EQ z w) x y = EQ (subs  z x y) (subs  w x y)
subs (If z w s) x y =
  If (subs z x y) (subs w x y) (subs s x y)
subs (Var name) (Var other) y =
  if name == other
    then y
    else Var name
subs (Var name) x y = Var name
subs (Lam var value) x y =
  Lam (subs var x y) (subs value x y)
subs (App f arg) x y =
  App (subs f x y) (subs arg x y)
subs  (Sum z w) x y = Sum (subs  z x y) (subs  w x y)
subs  (Pred z) x y = Pred (subs   z x y)
subs  (Prod z w) x y = Prod (subs  z x y) (subs w x y)
subs Null x y = Null
subs (Left a) x y = Left (subs a x y)
subs (Right a) x y = Right (subs a x y)
subs (Cons a b) x y = Cons (subs a x y) (subs b x y)

data Defn : Type where
  Let : (name: String) -> (value: Exp) -> Defn

-- A list of definitions of variables
Context : Type
Context = List Defn

varValue: Context -> (name: String) -> Maybe (Exp)
varValue [] name = Nothing
varValue ((Let x value) :: xs) name =
  if x == name then Just value else Nothing

{-
Simplify an expression in context by one step if possible. The simplifications are:
  * if an expression is a variable defined in the context, it is replaced by its value
  * sums, products and predecessors of _literals_ are simplifed, e.g. `Sum (N 2) (N 3)` becomes `N 5`
  * a lambda function `x :-> y` applied to `z` simplifies to the result of subtituting `x` by `z` in `y`.
  * for any other composite term, we simplify the components.
-}
simplify : (ctx: Context) -> (exp : Exp) -> Exp
simplify ctx  (N k) = N k
simplify ctx  (B x) = B x
simplify ctx  Null = Null
simplify ctx  (LTE (N x) (N y)) = B (x <= y)
simplify ctx  (LTE x y) = LTE (simplify ctx  x) (simplify ctx  y)
simplify ctx  (EQ (N x) (N y)) = B (x == y)
simplify ctx  (EQ (B x) (B y)) = B (x == y)
simplify ctx  (EQ Null Null) = B True
simplify ctx  (EQ Null (N _)) = B False
simplify ctx  (EQ Null (B _)) = B False
simplify ctx  (EQ Null (Cons _ _)) = B False
simplify ctx  (EQ (N _) Null) = B False
simplify ctx  (EQ (B _) Null) = B False
simplify ctx  (EQ (Cons _ _) Null) = B False
simplify ctx  (EQ (B _) (N _)) = B False
simplify ctx  (EQ (N _) (B _)) = B False
simplify ctx  (EQ x y) = EQ (simplify ctx  x) (simplify ctx  y)
simplify ctx (If (B True) y z) = y
simplify ctx  (If (B False) y z) = z
simplify ctx  (If x y z) = If (simplify ctx x) (simplify ctx  y) (simplify ctx  z)
simplify ctx  (Var name) = (case varValue ctx name of
                              Nothing => Var name
                              (Just x) => x)
simplify ctx (Lam var value) = Lam var value
simplify ctx (App (Lam var value) arg) = subs value var arg
simplify ctx (App f arg) = App (simplify ctx f) (simplify ctx arg)
simplify ctx  (Sum (N x) (N y)) = N (x + y)
simplify ctx  (Sum x y) = Sum (simplify ctx  x) (simplify ctx  y)
simplify ctx  (Pred (N x)) = N (pred x)
simplify ctx  (Pred x) = Pred (simplify ctx  x)
simplify ctx  (Prod (N x) (N y)) = N (x * y)
simplify ctx  (Prod x y) = Prod (simplify ctx  x) (simplify ctx  y)
simplify ctx (Left (Cons a b)) = a
simplify ctx (Right (Cons a b)) = b
simplify ctx (Left a) = Left (simplify ctx a)
simplify ctx (Right a) = Right (simplify ctx a)
simplify ctx (Cons a b) = Cons (simplify ctx a) (simplify ctx b)

data Program: Type where
  Code: (context: Context) -> (main: Exp) -> Program

-- repeatedly simplify an expression till we get a literal natural (or loop forever)
getNat : Context -> Exp -> Nat
getNat ctx exp = case (simplify ctx  exp) of
                  (N k) => k
                  x => getNat ctx x

steps: Context -> Exp -> Nat -> Exp
steps x y Z = y
steps x y (S k) = simplify x (steps x y k)

run: Program -> Exp -> Nat
run (Code context main) exp = getNat context (App main exp)

-- An example
not: Exp
not = Lam (Var "x" ) (If (Var "x" ) (B False) (B True))

-- a variable
n: Exp
n = Var "n"

-- a variable for the factorial function
fac : Exp
fac = Var "fac"

-- the expression `fac(n - 1)`
prev: Exp
prev = Prod (App fac (Pred n)) n

-- the expression `if n == 0 then 1 else fac(n-1)`
rhs : Exp
rhs = If (EQ n (N Z)) (N 1) prev

{- the context with definition:
  fac := n :-> (if (n == 0) then 1 else fac(n - 1)
-}
ctx: Context
ctx = (Let "fac" (Lam n rhs)) :: []

-- function computing factorial
facFn: Nat -> Nat
facFn n = getNat ctx (App fac (N n))

facProg: Program
facProg = Code ctx fac

--- Another program, summing lists
sm: Exp
sm = Var "sum"

l: Exp
l = Var "l"

sid: Exp
sid = If (EQ Null l) (N 0) (Sum (Left l) (App sm (Right l)))

sctx : Context
sctx = (Let "sum" (Lam l sid)) :: []

sumProg: Program
sumProg = Code sctx sm

egList: Exp
egList = Cons (N 5) (Cons (N 3) (Cons (N 4) Null ))
--- Run `run sumProg egList` to see lists being added