text:
myfib : Integer -> Integer
myfib 0 = 1
myfib 1 = 1
myfib n = myfib (n - 1) + myfib (n - 2)

main : IO ()
main = putStrLn $ show $ myfib 40

ext: idr

max_stars_repo_name: ioanluca/real-world-idris

max_issues_repo_name: ioanluca/real-world-idris

max_forks_repo_name: ioanluca/real-world-idris


text:
module Test.Markdown.LexerTest

import IdrTest.Test
import IdrTest.Expectation

import Markdown.Lexer

lexerSpecs : List (String, String, Maybe (List MarkdownToken))
lexerSpecs =
  [
    (
      "Complex Example",
      "## My _Heading_\n\nThis is some [text](https://text.com) and it's **cool**.\n\nBut there's more and it's interesting.\n# There's other things, too.\nBut that's not for today!",
      Just $
      [ Tok HeadingSym "##"
      , Tok MdText " My "
      , Tok ItalicsSym ""
      , Tok MdText "Heading"
      , Tok ItalicsSym ""
      , Tok NewLine ""
      , Tok NewLine ""
      , Tok MdText "This is some "
      , Tok MdLink "[text](https://text.com)"
      , Tok MdText " and it's "
      , Tok BoldSym ""
      , Tok MdText "cool"
      , Tok BoldSym ""
      , Tok MdText "."
      , Tok NewLine ""
      , Tok NewLine ""
      , Tok MdText "But there's more and it's interesting."
      , Tok NewLine ""
      , Tok HeadingSym "#"
      , Tok MdText " There's other things, "
      , Tok HtmlOpenTag ""
      , Tok MdText "too"
      , Tok HtmlCloseTag ""
      , Tok MdText "."
      , Tok NewLine ""
      , Tok MdText "But that's not for today!"
      ]
    ),
    (
      "Brackets Example",
      "A  C <D E> >F< << >>",
      Just $
      [ Tok MdText "A  C <D E> >F< << >>"
      ]
    ),
    (
      "Preformatted Text",
      "# Hello `john`\n```how\nare\nyou```",
      Just $
      [ Tok HeadingSym "#"
      , Tok MdText " Hello "
      , Tok MdPre "`john`"
      , Tok NewLine ""
      , Tok MdCodeBlock "```how\nare\nyou```"
      ]
    )
  ]

export
suite : Test
suite =
  let
    lexerTests =
      map (\(name, text, result) =>
        test name (\_ => assertEq (lexMarkdown text) result)
      ) lexerSpecs
  in
    describe "Lexer Tests"
      [ describe "Lexer Specs" lexerTests
      , describe "tokValue Tests"
          [ test "Heading" (\_ => assertEq (value $ (Tok HeadingSym "##")) 2)
          , test "Text" (\_ => assertEq (value $ (Tok MdText "Hello")) "Hello")
          , test "NewLine" (\_ => assertEq (value $ (Tok NewLine "\n")) ())
          , test "ItalicsSym" (\_ => assertEq (value $ (Tok ItalicsSym "_")) ())
          , test "BoldSym" (\_ => assertEq (value $ (Tok BoldSym "**")) ())
          , test "Link" (\_ => assertEq (value $ (Tok MdLink "[cool](https://cool.com)")) ("cool", "https://cool.com"))
          , test "HtmlOpenTag" (\_ => assertEq (value $ (Tok HtmlOpenTag "")) "sup")
          , test "HtmlCloseTag" (\_ => assertEq (value $ (Tok HtmlCloseTag "")) "sup")
          ]
      ]

max_stars_repo_name: Z-snails/inigo

max_issues_repo_name: Z-snails/inigo

max_forks_repo_name: Z-snails/inigo


text:
module Game

import Quantities
import Quantities.Screen

ScreenSpeed : Quantity
ScreenSpeed = ScreenLength </> Time

Pxs : Unit ScreenSpeed
Pxs = Pixel <//> Second

record PlayerState where
  constructor MkPlayerState
  xSpeed : F Pxs
  ySpeed : F Pxs
  xPos   : F Px
  yPos   : F Px

gravity : Quantities.Core.F (Pxs <//> Second)
gravity = -800 =| (Pxs <//> Second)

-- Update player position and speed after a given duration
updatePlayerState : F Second -> PlayerState -> PlayerState
updatePlayerState dt (MkPlayerState xs ys xp yp) =
  let newYPos = yp <+> ys |*| dt
  in if newYPos <= (0 =| Px)
       then MkPlayerState (0 =| Pxs) (0 =| Pxs) xp (0 =| Px)
       else MkPlayerState xs (ys <+> gravity |*| dt)
                          (xp <+> xs |*| dt) newYPos

max_stars_repo_name: timjb/quantities

max_issues_repo_name: timjb/quantities

max_forks_repo_name: timjb/quantities


text:
data Usage = Once | Many

data Use : Usage -> (Type -> Type) -> Type -> Type where
     Pure : (1 x : a) -> Use t m a
     BindOnce : (1 act : Use Once m a) -> (1 k : (1 x : a) -> Use t m b) -> Use t m b
     BindMany : (1 act : Use Many m a) -> (1 k : (x : a) -> Use t m b) -> Use t m b

contType : (Type -> Type) -> Usage -> Usage -> Type -> Type -> Type
contType m Once q a b = ((1 x : a) -> Use q m b)
contType m Many q a b = ((x : a) -> Use q m b)

(>>=) : {p : _} -> (1 f : Use p m a) -> (1 k : contType m p q a b) -> Use q m b
(>>=) {p = Once} = BindOnce
(>>=) {p = Many} = BindMany

pure : (1 x : a) -> Use t m a
pure = Pure

One : (Type -> Type) -> Type -> Type
One = Use Once

Any : (Type -> Type) -> Type -> Type
Any = Use Many

data DoorState = Closed | Open

data Door : DoorState -> Type where
     MkDoor : (isOpen : Bool) -> Door (if isOpen then Open else Closed)

newDoor : One m (Door Closed)
newDoor = pure (MkDoor False)

knock : (1 d : Door Closed) -> One m (Door Closed)
openDoor : (1 d : Door Closed) ->
           One m (Res Bool (\r => Door (if r then Open else Closed)))

closeDoor : (1 d : Door Open) -> One m (Door Closed)

deleteDoor : (1 d : Door Closed) -> Any m ()

doorProg : Any m ()
doorProg
    = do d <- newDoor
         r <- openDoor d
         let x = 42
         case r of
              what => ?now

doorProg2 : Any m ()
doorProg2
    = do d <- newDoor
         r <- openDoor d
         let x = 42
         case r of
              (res # d) => ?now_1

doorProg3 : Any m ()
doorProg3
    = do d <- newDoor
         r <- openDoor d
         let x = 42
         case r of
              (True # d) => ?now_2
              (False # d) => ?now_3


text:
> module BoundedNat.Operations

> import Data.Fin
> import Data.Vect

> import BoundedNat.BoundedNat
> import Fin.Properties
> import Nat.LTProperties
> import Sigma.Sigma
> import Pairs.Operations

> %default total
> %access public export

> ||| Mapping bounded |Nat|s to |Fin|s
> toFin : {b : Nat} -> LTB b -> Fin b
> toFin {b = Z}   (MkSigma  _     nLT0        ) = void (succNotLTEzero nLT0)
> toFin {b = S m} (MkSigma  Z     _           ) = FZ
> toFin {b = S m} (MkSigma (S n) (LTESucc prf)) = FS (toFin (MkSigma n prf))

> ||| Mapping |Fin|s to bounded |Nat|s
> fromFin : {b : Nat} -> Fin b -> LTB b
> fromFin k = MkSigma (finToNat k) (finToNatLemma k)

> |||
> toVect : {b : Nat} -> {A : Type} -> (LTB b -> A) -> Vect b A
> toVect {b = Z}        _ = Nil
> toVect {b = S b'} {A} f = (f (MkSigma Z (ltZS b'))) :: toVect f' where
>   f' : LTB b' -> A
>   f' (MkSigma k q) = f (MkSigma (S k) (LTESucc q))

ext: lidr

max_stars_repo_name: zenntenn/IdrisLibs

max_issues_repo_name: zenntenn/IdrisLibs

max_forks_repo_name: zenntenn/IdrisLibs


text:
module Main

import Baseline

loop : IO ()
loop = do
  str <- baseline "$> "
  case str of
       Just "" => loop
       Just s  => do
         putStrLn ("You typed: " ++ s)
         loop
       otherwise => pure ()

main : IO ()
main = do
  readHistory ".history"
  addDictEntries
    [ "lexicographic"
    , "mexico"
    , "existentialism" ]
  loop
  writeHistory ".history"
  putStrLn "Exit!"

max_stars_repo_name: laserpants/baseline-idris

max_issues_repo_name: laserpants/baseline-idris

max_forks_repo_name: laserpants/baseline-idris


text:
module Circuits.Idealised.Pretty

import System.File

import Data.String

import Text.Lexer
import Text.Parser

import Toolkit.Data.DList
import Toolkit.Data.Whole
import Toolkit.Data.Location
import Toolkit.Text.Lexer.Run
import Toolkit.Text.Parser.Run

import Toolkit.Data.List.Occurs
import Toolkit.Data.Graph.EdgeBounded
import Toolkit.Data.Graph.EdgeBounded.HasExactDegree.All

import Toolkit.DeBruijn.Context.Item
import Toolkit.DeBruijn.Context

import public Circuits.Common.Pretty
import        Circuits.Idealised.Error
import        Circuits.Idealised.Lexer
import        Circuits.Idealised.Types

%default total

export
Show Direction where
  show INPUT  = "input"
  show OUTPUT = "output"

export
Show Ty where
  show TyUnit = "()"
  show (TyPort (d,t)) = concat ["TyPort(", show d, ",", show t, ")"]
  show TyGate = "TyGate"

export
Show GateKind where
  show AND  = "and"
  show IOR  = "or"
  show XOR  = "xor"
  show ANDN = "nand"
  show IORN = "nor"
  show XORN = "xnor"
  show JOIN = "join"

showEnv : Context (Ty,Usage) type -> String
showEnv [] = ""
showEnv ((I name (type, FREE)) :: rest)
  = name <+> " : " <+> show type <+> "\n" <+> (showEnv rest)
showEnv ((I name (type, USED)) :: rest) = showEnv rest

export
Show FailingEdgeCase where
  show (InvalidSplit p s l r) = "Pivot (" <+> show p <+> ") is wrong do not add up: " <+> unwords [show s, "!= 1 + ", show l, "+", show r]
  show (InvalidEdge  s l r) = "Indices do not add up: " <+> unwords [show s, "= 1 + ", show l, "+", show r]

export
Show Check.Error where
  show (Mismatch x y)
    = "Type Mismatch:\n\n"
      <+> unlines [unwords ["\tExpected:",show x], unwords ["\tGiven:", show y]]

  show (MismatchGate x y)
    = "Type Mismatch:\n\n"
     <+> unlines [unwords ["\tExpected:",show x], unwords ["\tGiven:", show y]]

  show (ElemFail x (NotSatisfied ()))
    = unwords ["Port is used:", x]

  show (ElemFail x NotFound)
    = "\{x} not found."

  show (NotEdgeCase r)  = "Not an edge case:\n\n" <+> show r
  show (PortExpected INPUT) = "Expected an Input Port"
  show (PortExpected OUTPUT) = "Expected an Output Port"
  show (LinearityError env) = "Dangling Ports:\n\n" <+> showEnv env
  show (VectorExpected) = "Vector Expected"
  show (VectorTooShort) = "Output Vector must be a length greater or equal to two."
  show (VectorSizeMismatch o a b)
    = unlines [ "Output Vector and input are wrong sizes:"
              , unwords ["\t" <+> show o, "!=", show a, "+", show b]]
  show (Err x y) = unwords [show x, show y]

export
Show (Idealised.Error) where
  show (TyCheck x) = show x
  show (Parse f n) = show @{circuitspe} n
  show (Sound g e)
    = unlines ["// LOG : Soundness Error:", showErr (g, e)]

-- [ EOF ]

max_stars_repo_name: border-patrol/linear-circuits

max_issues_repo_name: border-patrol/linear-circuits

max_forks_repo_name: border-patrol/linear-circuits


text:
{--
Copyright 2021 Joel Berkeley

Licensed under the Apache License, Version 2.0 (the "License");
you may not use this file except in compliance with the License.
You may obtain a copy of the License at

    http://www.apache.org/licenses/LICENSE-2.0

Unless required by applicable law or agreed to in writing, software
distributed under the License is distributed on an "AS IS" BASIS,
WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
See the License for the specific language governing permissions and
limitations under the License.
--}
||| This module defines functionality for Bayesian optimization, the data-efficient optimization of
||| objective functions. Bayesian optimization recommends new points at which to query your
||| objective by placing a probabilistic model over historic data then, typically, optimizing an
||| _acquisition function_ which quantifies how useful it would be to evaluate the objective at any
||| given set of points.
module BayesianOptimization

import public Data.Stream
import Tensor

import public BayesianOptimization.Acquisition as BayesianOptimization
import public BayesianOptimization.Morphisms as BayesianOptimization

||| A Bayesian optimization loop as a (potentially infinite) stream of values. The values are
||| typically the observed data, and the models of that data. The loop iteratively finds new points
||| with the specified `tactic` then updates the values with these new points (assuming some
||| implicit objective function).
|||
||| @tactic The tactic which which to recommend new points. This could be optimizing an acquisition
|||   function, for example. Note this is a `Morphism`, not a function.
||| @observer A function which evaluates the optimization objective at the recommended points, then
|||   updates the values (typically data and models).
export
loop : (tactic : i ~> Tensor shape dtype)
  -> (observer : Tensor shape dtype -> i -> i) -> i -> Stream i
loop tactic observer = iterate (\ii => observer (run tactic ii) ii)

max_stars_repo_name: joelberkeley/spidr

max_issues_repo_name: joelberkeley/spidr

max_forks_repo_name: joelberkeley/spidr


text:
module TTImp.ProcessType

import Core.Context
import Core.Context.Log
import Core.Core
import Core.Env
import Core.Hash
import Core.Metadata
import Core.Normalise
import Core.TT
import Core.UnifyState
import Core.Value

import TTImp.BindImplicits
import TTImp.Elab.Check
import TTImp.Elab.Utils
import TTImp.Elab
import TTImp.TTImp
import TTImp.Utils

import Data.List
import Data.String
import Libraries.Data.NameMap

%default covering

getRetTy : Defs -> NF [] -> Core Name
getRetTy defs (NBind fc _ (Pi _ _ _ _) sc)
    = getRetTy defs !(sc defs (toClosure defaultOpts [] (Erased fc False)))
getRetTy defs (NTCon _ n _ _ _) = pure n
getRetTy defs ty
    = throw (GenericMsg (getLoc ty)
             "Can only add hints for concrete return types")

processFnOpt : {auto c : Ref Ctxt Defs} ->
               FC -> Bool -> -- ^ top level name?
               Name -> FnOpt -> Core ()
processFnOpt fc _ ndef Inline
    = setFlag fc ndef Inline
processFnOpt fc _ ndef TCInline
    = setFlag fc ndef TCInline
processFnOpt fc True ndef (Hint d)
    = do defs <- get Ctxt
         Just ty <- lookupTyExact ndef (gamma defs)
              | Nothing => undefinedName fc ndef
         target <- getRetTy defs !(nf defs [] ty)
         addHintFor fc target ndef d False
processFnOpt fc _ ndef (Hint d)
    = do log "elab" 5 $ "Adding local hint " ++ show !(toFullNames ndef)
         addLocalHint ndef
processFnOpt fc True ndef (GlobalHint a)
    = addGlobalHint ndef a
processFnOpt fc _ ndef (GlobalHint a)
    = throw (GenericMsg fc "%globalhint is not valid in local definitions")
processFnOpt fc _ ndef ExternFn
    = setFlag fc ndef Inline -- if externally defined, inline when compiling
processFnOpt fc _ ndef (ForeignFn _)
    = setFlag fc ndef Inline -- if externally defined, inline when compiling
processFnOpt fc _ ndef Invertible
    = setFlag fc ndef Invertible
processFnOpt fc _ ndef (Totality tot)
    = setFlag fc ndef (SetTotal tot)
processFnOpt fc _ ndef Macro
    = setFlag fc ndef Macro
processFnOpt fc _ ndef (SpecArgs ns)
    = do defs <- get Ctxt
         Just gdef <- lookupCtxtExact ndef (gamma defs)
              | Nothing => undefinedName fc ndef
         nty <- nf defs [] (type gdef)
         ps <- getNamePos 0 nty
         ddeps <- collectDDeps nty
         specs <- collectSpec [] ddeps ps nty
         ignore $ addDef ndef (record { specArgs = specs } gdef)
  where
    insertDeps : List Nat -> List (Name, Nat) -> List Name -> List Nat
    insertDeps acc ps [] = acc
    insertDeps acc ps (n :: ns)
        = case lookup n ps of
               Nothing => insertDeps acc ps ns
               Just pos => if pos `elem` acc
                              then insertDeps acc ps ns
                              else insertDeps (pos :: acc) ps ns

    -- Collect the argument names which the dynamic args depend on
    collectDDeps : NF [] -> Core (List Name)
    collectDDeps (NBind tfc x (Pi _ _ _ nty) sc)
        = do defs <- get Ctxt
             empty <- clearDefs defs
             sc' <- sc defs (toClosure defaultOpts [] (Ref tfc Bound x))
             if x `elem` ns
                then collectDDeps sc'
                else do aty <- quote empty [] nty
                        -- Get names depended on by nty
                        let deps = keys (getRefs (UN Underscore) aty)
                        rest <- collectDDeps sc'
                        pure (rest ++ deps)
    collectDDeps _ = pure []

    -- Return names the type depends on, and whether it's a parameter
    mutual
      getDepsArgs : Bool -> List (NF []) -> NameMap Bool ->
                    Core (NameMap Bool)
      getDepsArgs inparam [] ns = pure ns
      getDepsArgs inparam (a :: as) ns
          = do ns' <- getDeps inparam a ns
               getDepsArgs inparam as ns'

      getDeps : Bool -> NF [] -> NameMap Bool ->
                Core (NameMap Bool)
      getDeps inparam (NBind _ x (Pi _ _ _ pty) sc) ns
          = do defs <- get Ctxt
               ns' <- getDeps inparam !(evalClosure defs pty) ns
               sc' <- sc defs (toClosure defaultOpts [] (Erased fc False))
               getDeps inparam sc' ns'
      getDeps inparam (NBind _ x b sc) ns
          = do defs <- get Ctxt
               ns' <- getDeps False !(evalClosure defs (binderType b)) ns
               sc' <- sc defs (toClosure defaultOpts [] (Erased fc False))
               getDeps False sc' ns
      getDeps inparam (NApp _ (NRef Bound n) args) ns
          = do defs <- get Ctxt
               ns' <- getDepsArgs False !(traverse (evalClosure defs . snd) args) ns
               pure (insert n inparam ns')
      getDeps inparam (NDCon _ n t a args) ns
          = do defs <- get Ctxt
               getDepsArgs False !(traverse (evalClosure defs . snd) args) ns
      getDeps inparam (NTCon _ n t a args) ns
          = do defs <- get Ctxt
               params <- case !(lookupDefExact n (gamma defs)) of
                              Just (TCon _ _ ps _ _ _ _ _) => pure ps
                              _ => pure []
               let (ps, ds) = splitPs 0 params (map snd args)
               ns' <- getDepsArgs True !(traverse (evalClosure defs) ps) ns
               getDepsArgs False !(traverse (evalClosure defs) ds) ns'
        where
          -- Split into arguments in parameter position, and others
          splitPs : Nat -> List Nat -> List (Closure []) ->
                    (List (Closure []), List (Closure []))
          splitPs n params [] = ([], [])
          splitPs n params (x :: xs)
              = let (ps', ds') = splitPs (1 + n) params xs in
                    if n `elem` params
                       then (x :: ps', ds')
                       else (ps', x :: ds')
      getDeps inparam (NDelayed _ _ t) ns = getDeps inparam t ns
      getDeps inparams nf ns = pure ns

    -- If the name of an argument is in the list of specialisable arguments,
    -- record the position. Also record the position of anything the argument
    -- depends on which is only dependend on by declared static arguments.
    collectSpec : List Nat -> -- specialisable so far
                  List Name -> -- things depended on by dynamic args
                               -- We're assuming  it's a short list, so just use
                               -- List and don't worry about duplicates.
                  List (Name, Nat) -> NF [] -> Core (List Nat)
    collectSpec acc ddeps ps (NBind tfc x (Pi _ _ _ nty) sc)
        = do defs <- get Ctxt
             empty <- clearDefs defs
             sc' <- sc defs (toClosure defaultOpts [] (Ref tfc Bound x))
             if x `elem` ns
                then do deps <- getDeps True !(evalClosure defs nty) NameMap.empty
                        -- Get names depended on by nty
                        -- Keep the ones which are either:
                        --  * parameters
                        --  * not depended on by a dynamic argument (the ddeps)
                        let rs = filter (\x => snd x ||
                                               not (fst x `elem` ddeps))
                                        (toList deps)
                        let acc' = insertDeps acc ps (x :: map fst rs)
                        collectSpec acc' ddeps ps sc'
                else collectSpec acc ddeps ps sc'
    collectSpec acc ddeps ps _ = pure acc

    getNamePos : Nat -> NF [] -> Core (List (Name, Nat))
    getNamePos i (NBind tfc x (Pi _ _ _ _) sc)
        = do defs <- get Ctxt
             ns' <- getNamePos (1 + i) !(sc defs (toClosure defaultOpts [] (Erased tfc False)))
             pure ((x, i) :: ns')
    getNamePos _ _ = pure []

getFnString : {auto c : Ref Ctxt Defs} ->
              {auto m : Ref MD Metadata} ->
              {auto u : Ref UST UState} ->
              RawImp -> Core String
getFnString (IPrimVal _ (Str st)) = pure st
getFnString tm
    = do inidx <- resolveName (UN $ Basic "[foreign]")
         let fc = getFC tm
         let gstr = gnf [] (PrimVal fc StringType)
         etm <- checkTerm inidx InExpr [] (MkNested []) [] tm gstr
         defs <- get Ctxt
         case !(nf defs [] etm) of
              NPrimVal fc (Str st) => pure st
              _ => throw (GenericMsg fc "%foreign calling convention must evaluate to a String")

-- If it's declared as externally defined, set the definition to
-- ExternFn <arity>, where the arity is assumed to be fixed (i.e.
-- not dependent on any of the arguments)
-- Similarly set foreign definitions. Possibly combine these?
initDef : {vars : _} ->
          {auto c : Ref Ctxt Defs} ->
          {auto m : Ref MD Metadata} ->
          {auto u : Ref UST UState} ->
          Name -> Env Term vars -> Term vars -> List FnOpt -> Core Def
initDef n env ty []
    = do addUserHole False n
         pure None
initDef n env ty (ExternFn :: opts)
    = do defs <- get Ctxt
         a <- getArity defs env ty
         pure (ExternDef a)
initDef n env ty (ForeignFn cs :: opts)
    = do defs <- get Ctxt
         a <- getArity defs env ty
         cs' <- traverse getFnString cs
         pure (ForeignDef a cs')
initDef n env ty (_ :: opts) = initDef n env ty opts

-- Find the inferrable argument positions in a type. This is useful for
-- generalising partially evaluated definitions and (potentially) in interactive
-- editing
findInferrable : {auto c : Ref Ctxt Defs} ->
                 Defs -> NF [] -> Core (List Nat)
findInferrable defs ty = fi 0 0 [] [] ty
  where
    mutual
      -- Add to the inferrable arguments from the given type. An argument is
      -- inferrable if it's guarded by a constructor, or on its own
      findInf : List Nat -> List (Name, Nat) ->
                NF [] -> Core (List Nat)
      findInf acc pos (NApp _ (NRef Bound n) [])
          = case lookup n pos of
                 Nothing => pure acc
                 Just p => if p `elem` acc then pure acc else pure (p :: acc)
      findInf acc pos (NDCon _ _ _ _ args)
          = do args' <- traverse (evalClosure defs . snd) args
               findInfs acc pos args'
      findInf acc pos (NTCon _ _ _ _ args)
          = do args' <- traverse (evalClosure defs . snd) args
               findInfs acc pos args'
      findInf acc pos (NDelayed _ _ t) = findInf acc pos t
      findInf acc _ _ = pure acc

      findInfs : List Nat -> List (Name, Nat) -> List (NF []) -> Core (List Nat)
      findInfs acc pos [] = pure acc
      findInfs acc pos (n :: ns) = findInf !(findInfs acc pos ns) pos n

    fi : Nat -> Int -> List (Name, Nat) -> List Nat -> NF [] -> Core (List Nat)
    fi pos i args acc (NBind fc x (Pi _ _ _ aty) sc)
        = do let argn = MN "inf" i
             sc' <- sc defs (toClosure defaultOpts [] (Ref fc Bound argn))
             acc' <- findInf acc args !(evalClosure defs aty)
             rest <- fi (1 + pos) (1 + i) ((argn, pos) :: args) acc' sc'
             pure rest
    fi pos i args acc ret = findInf acc args ret

export
processType : {vars : _} ->
              {auto c : Ref Ctxt Defs} ->
              {auto m : Ref MD Metadata} ->
              {auto u : Ref UST UState} ->
              List ElabOpt -> NestedNames vars -> Env Term vars ->
              FC -> RigCount -> Visibility ->
              List FnOpt -> ImpTy -> Core ()
processType {vars} eopts nest env fc rig vis opts (MkImpTy tfc nameFC n_in ty_raw)
    = do n <- inCurrentNS n_in

         addNameLoc nameFC n

         log "declare.type" 1 $ "Processing " ++ show n
         log "declare.type" 5 $ unwords ["Checking type decl:", show rig, show n, ":", show ty_raw]
         idx <- resolveName n

         -- Check 'n' is undefined
         defs <- get Ctxt
         Nothing <- lookupCtxtExact (Resolved idx) (gamma defs)
              | Just gdef => throw (AlreadyDefined fc n)

         ty <-
             wrapErrorC eopts (InType fc n) $
                   checkTerm idx InType (HolesOkay :: eopts) nest env
                             (IBindHere fc (PI erased) ty_raw)
                             (gType fc)
         logTermNF "declare.type" 3 ("Type of " ++ show n) [] (abstractFullEnvType tfc env ty)

         def <- initDef n env ty opts
         let fullty = abstractFullEnvType tfc env ty

         (erased, dterased) <- findErased fullty
         defs <- get Ctxt
         empty <- clearDefs defs
         infargs <- findInferrable empty !(nf defs [] fullty)

         ignore $ addDef (Resolved idx)
                (record { eraseArgs = erased,
                          safeErase = dterased,
                          inferrable = infargs }
                        (newDef fc n rig vars fullty vis def))
         -- Flag it as checked, because we're going to check the clauses
         -- from the top level.
         -- But, if it's a case block, it'll be checked as part of the top
         -- level check so don't set the flag.
         unless (InCase `elem` eopts) $ setLinearCheck idx True

         log "declare.type" 2 $ "Setting options for " ++ show n ++ ": " ++ show opts
         let name = Resolved idx
         let isNested : Name -> Bool
             isNested (Nested _ _) = True
             isNested (NS _ n) = isNested n
             isNested _ = False
         let nested = not (isNested n)
         traverse_ (processFnOpt fc (not (isNested n)) name) opts
         -- If no function-specific totality pragma has been used, attach the default totality
         unless (any isTotalityReq opts) $
           setFlag fc name (SetTotal !getDefaultTotalityOption)

         -- Add to the interactive editing metadata
         addTyDecl fc (Resolved idx) env ty -- for definition generation

         log "metadata.names" 7 $ "processType is adding ↓"
         addNameType nameFC (Resolved idx) env ty -- for looking up types

         traverse_ addToSave (keys (getMetas ty))
         addToSave n
         log "declare.type" 10 $ "Saving from " ++ show n ++ ": " ++ show (keys (getMetas ty))

         when (vis /= Private) $
              do addHashWithNames n
                 addHashWithNames ty


text:
module Starfield

-- Background starfield effect

import Effects
import Effect.SDL
import Effect.StdIO
import Effect.State

import Rnd

%access public export

data Starfield : Type where -- for labelling state

StarEff : Type -> Type
StarEff t = { [Starfield ::: STATE (List (Int, Int)), RND] } Eff t

initStarfield : List (Int, Int) -> Nat -> StarEff ()
initStarfield acc Z = Starfield :- put acc
initStarfield acc n
    = do x <- rndInt 0 639
         y <- rndInt 0 479
         initStarfield ((x, y) :: acc) (minus n 1)

updateStarfield : StarEff ()
updateStarfield = do xs <- Starfield :- get
                     xs' <- upd [] xs
                     Starfield :- put xs'
 where
  upd : List (Int, Int) -> List (Int, Int) -> { [RND] } Eff (List (Int, Int))
  upd acc [] = pure acc
  upd acc ((x, y) :: xs)
      = if (y > 479) then do
             x <- rndInt 0 639
             upd ((x, 0) :: acc) xs
           else
             upd ((x, y+1) :: acc) xs

drawStarfield : List (Int, Int) -> { [SDL_ON] } Eff ()
drawStarfield [] = pure ()
drawStarfield ((x, y) :: xs) = do line white x y x y
                                  drawStarfield xs

max_stars_repo_name: ajnavarro/language-dataset

max_issues_repo_name: ajnavarro/language-dataset

max_forks_repo_name: ajnavarro/language-dataset


text:
import Data.Vect
import Data.Vect.Views

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

testList : Int -> Int -> List Int -> List Int
testList 0 seed acc = acc
-- Need to explicitly mod since different back ends overflow differently
testList x seed acc = let seed' = (seed * 12345 + 768) `mod` 65536 in
                          testList (x - 1) seed'
                               ((seed' `mod` 100) :: acc)

myhead : List a -> a
myhead (x :: xs) = x

main : IO ()
main = do let list = fromList (testList 100 12345 [])
          putStrLn "Sorting list"
          let list' = mergeSort list
          printLn list'

max_stars_repo_name: grin-compiler/idris-grin

max_issues_repo_name: grin-compiler/idris-grin

max_forks_repo_name: grin-compiler/idris-grin


text:
module Language.LSP.Message.DocumentLink

import Language.JSON
import Language.LSP.Message.Derive
import Language.LSP.Message.Location
import Language.LSP.Message.Progress
import Language.LSP.Message.TextDocument
import Language.LSP.Message.URI
import Language.LSP.Message.Utils
import Language.Reflection

%language ElabReflection
%default total

||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_documentLink
public export
record DocumentLinkClientCapabilities where
  constructor MkDocumentLinkClientCapabilities
  dynamicRegistration : Maybe Bool
  tooltipSupport      : Maybe Bool
%runElab deriveJSON defaultOpts `{DocumentLinkClientCapabilities}

||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_documentLink
public export
record DocumentLinkOptions where
  constructor MkDocumentLinkOptions
  workDoneProgress : Maybe Bool
  resolveProvider  : Maybe Bool
%runElab deriveJSON defaultOpts `{DocumentLinkOptions}

||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_documentLink
public export
record DocumentLinkRegistrationOptions where
  constructor MkDocumentLinkRegistrationOptions
  workDoneProgress : Maybe Bool
  resolveProvider  : Maybe Bool
  documentSelector : OneOf [DocumentSelector, Null]
%runElab deriveJSON defaultOpts `{DocumentLinkRegistrationOptions}

||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_documentLink
public export
record DocumentLinkParams where
  constructor MkDocumentLinkParams
  workDoneToken      : Maybe ProgressToken
  partialResultToken : Maybe ProgressToken
  textDocument       : TextDocumentIdentifier
%runElab deriveJSON defaultOpts `{DocumentLinkParams}

||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_documentLink
public export
record DocumentLink where
  constructor MkDocumentLink
  range   : Range
  target  : Maybe DocumentURI
  tooltip : Maybe String
  data_   : Maybe JSON
%runElab deriveJSON ({renames := [("data_", "data")]} defaultOpts) `{DocumentLink}


text:
||| Test if :typeat can report the type of variables in record definitions
||| and record updates

-- `pet` is an excuse to have a type variable
record Person animal where
  name : String
  age : Nat
  pet : animal

-- Record update syntax with the record keyword

singleFieldUpdate : Person a -> Person a
singleFieldUpdate p = { age $= (+one) } p
-- Not making it point free to keep a var here ^
  where
    -- A variable to use in the update
    one : Nat
    one = 1

multiFieldUpdate : Person a -> Person a
multiFieldUpdate p = { name := emptyString, age := zero } p
-- Not point free just like above, in order to have a var here ^
  where
    -- Variables to use in the update
    emptyString : String
    emptyString = ""

    zero : Nat
    zero = 0

-- :typeat in a record update using the syntax without the `record` keyword
-- doesn't yet work


text:
module Main

import Cairo

public export
%foreign
  """
  code:
  func Main_knowsSecretFactors(x) -> (result):
      tempvar a
      tempvar b
      %{
          ids.a = program_input['a']
          ids.b = program_input['b']
      %}
      if x == a * b:
        return (1)
      else:
        return (0)
      end
  end
  """
knowsSecretFactors : Felt -> Felt

%noinline
main : Cairo ()
main = output $ knowsSecretFactors 10967535067

max_stars_repo_name: skyro-compiler/skyro

max_issues_repo_name: skyro-compiler/skyro

max_forks_repo_name: skyro-compiler/skyro


text:
module IntegerGroupTheory

plusAssociativeBigInt : (left : Integer) ->
                  (centre : Integer) ->
                  (right : Integer) ->
                  left + (centre + right) = left + centre + right
plusAssociativeBigInt = believe_me "Integer addition is associative."

rdivBigInt : (x : Integer) -> (y : Integer) -> (x+y)-y = x
rdivBigInt x y = believe_me "Integer addition is right divisible."

unRDivBigInt : (x : Integer) -> (y : Integer) -> (x-y)+y = x
unRDivBigInt = believe_me "Integer (right) subtraction is right divisible."

lcancBigInt: (left1 : Integer) -> (left2 : Integer) -> (right : Integer) -> (left1+right = left2+right) -> (left1 = left2)
lcancBigInt left1 left2 right = ?lcancBigIntpr

lcancBigIntpr = proof
  intro
  intro
  intro
  intro prsum
  rewrite sym (sym $ rdivBigInt left1 right)
  rewrite sym (sym $ rdivBigInt left2 right)
  exact cong {f=\x => x-right} prsum

plusRightIdBigInt : (x : Integer) -> x = x+0
-- plusRightIdBigInt x = believe_me "assume x=x+0"
plusRightIdBigInt x = ?plusRightIdBigIntPr

plusRightIdBigIntPr = proof
  intro
  claim addZeroTwice (x+0=(x+0)+0)
  unfocus
  exact lcancBigInt x (x+0) 0 addZeroTwice
  exact trans Refl (plusAssociativeBigInt x 0 0)

negSumImedBigInt : (x : Integer) -> (y : Integer) -> (x-y)+y = (x+(negate y))+y
negSumImedBigInt = proof
  intros
  rewrite sym (unRDivBigInt x y)
  rewrite sym (sym $ plusAssociativeBigInt x (negate y) y)
  rewrite sym (unRDivBigInt 0 y)
  rewrite sym (plusRightIdBigInt x)
  trivial

differenceAsSum : (x : Integer) -> (y : Integer) -> x-y = x+(negate y)
differenceAsSum x y = ?differenceAsSumPr

differenceAsSumPr = proof
  intros
  claim pr0 ((x-y)+y = (x+(negate y))+y)
  unfocus
  let prf1 = replace pr0 {P= \t => t-y=x-y}
  claim prf1Arg (((x - y) + y)-y = x - y)
  unfocus
  rewrite sym (sym $ prf1 prf1Arg)
  rewrite sym ( rdivBigInt (x+(0-y)) y )
  exact Refl
  claim prmainReAssoc (x = x + negate y + y)
  unfocus
  exact trans (unRDivBigInt x y) prmainReAssoc
  exact rdivBigInt (x-y) y
  claim prmain (x = x + (negate y + y))
  unfocus
  exact trans prmain (plusAssociativeBigInt x (negate y) y)
  claim prmainPlusZ (x+0 = x+(negate y + y))
  unfocus
  exact trans (plusRightIdBigInt x) prmainPlusZ
  exact cong (sym $ unRDivBigInt 0 y)

plusCommutativeBigInt : (left : Integer) ->
                  (right : Integer) ->
                  left + right = right + left
plusCommutativeBigInt = believe_me "Integer addition is commutative."

subtractionexchange : (x : Integer) -> (y : Integer) -> (z : Integer)
	-> (x-y)+z = x+(z-y)
subtractionexchange = ?subtractionexchangepr

subtractionexchangepr = proof
  intros
  rewrite sym (differenceAsSum x y)
  rewrite sym (sym $ plusAssociativeBigInt x (0-y) z)
  rewrite sym (plusCommutativeBigInt (0-y) z)
  rewrite sym (sym $ differenceAsSum z y)
  trivial


text:
module Parcomb

data Parser a = MkParser (Lazy (String -> (Maybe a, String)))

parse : Parser a -> String -> (Maybe a, String)
parse p = case p of
  MkParser x => x

class Applicative f => LazyAlternative (f : Type -> Type) where
    empty : f a
    alt : Lazy (f a) -> Lazy (f a) -> f a

instance Functor Parser where
  map f p = MkParser $ \str => case (parse p str) of
    (Nothing, rest) => (Nothing, rest)
    (Just x, rest) => (Just (f x), rest)

mutual
  instance Applicative Parser where
    pure a = MkParser $ \str => (Just a, str)
    mf <$> mp = do
      p <- mp
      f <- mf
      return (f p)

  instance Monad Parser where
    p >>= g = MkParser $ \str => case (parse p str) of
      (Nothing, rest) => (Nothing, rest)
      (Just x, rest) => parse (g x) rest

instance LazyAlternative Parser where
  empty = MkParser $ \str => (Nothing, str)
  alt f s = MkParser $ \str => case (parse f str) of
    (Nothing, rest) => parse s str
    (Just x, rest) => (Just x, rest)

fail : Parser a
fail = MkParser $ \str => (Nothing, "")

item : Parser Char
item = MkParser $ \str =>
  case str of
    "" => (Nothing, "")
    _ => (Just (strHead str), strTail str)

sat : (Char -> Bool) -> Parser Char
sat p = do
  c <- item
  if p c
  then return c
  else fail

char : Char -> Parser Char
char c = sat (c ==)

string : String -> Parser String
string "" = return ""
string str = do
  char c
  string cs
  return str
where c = strHead str
      cs = strTail str

mutual
  many : Parser a -> (Parser (List a))
  many p = alt (some p) (return [])

  some : Parser a -> (Parser (List a))
  some p = do
    a <- p
    as <- many p
    return (a :: as)

namespace Main
  main : IO ()
  main = putStrLn . show $ parse (many $ char 'p') "pppa"

max_stars_repo_name: defanor/parcomb

max_issues_repo_name: defanor/parcomb

max_forks_repo_name: defanor/parcomb


text:
nat_induction :
    (prop : Nat -> Type) ->                -- Property to show
    (prop Z) ->                            -- Base case
    ((k : Nat) -> prop k -> prop (S k)) -> -- Inductive step
    (x : Nat) ->                           -- Show for all x
    prop x
nat_induction prop p_Z p_S Z = p_Z
nat_induction prop p_Z p_S (S k) = p_S k (nat_induction prop p_Z p_S k)

plus_ind : Nat -> Nat -> Nat
plus_ind n m
   = nat_induction (\x => Nat)
                   m                      -- Base case, plus_ind Z m
                   (\k, k_rec => S k_rec) -- Inductive step plus_ind (S k) m
                                          -- where k_rec = plus_ind k m
                   n


text:
module Palindrome

export
palindrome : String -> Bool
palindrome str =
    let lstr = toLower str
        lenstr = length str in
        ((reverse lstr) == lstr) && (lenstr > 10)

max_stars_repo_name: curtisalexander/tdd-idris

max_issues_repo_name: curtisalexander/tdd-idris

max_forks_repo_name: curtisalexander/tdd-idris


text:
module Test.Assertions

%access export
%default total

describe : String -> IO () -> IO ()
describe label body = do
  putStrLn ""
  putStr label
  body

assert : Bool -> Lazy (List String) -> IO ()
assert False report = do
  putStrLn "*FAIL*"
  traverse_ (\x => putStrLn ("  " ++ x)) report
assert True report =
  putStr "."

shouldBe : (Eq a, Show a) => a -> a -> IO ()
shouldBe a expected =
  assert (a == expected) [
    "Expected " ++ show expected,
    "But got  " ++ show a
  ]

shouldShow : Show a => a -> String -> IO ()
shouldShow a expected =
  assert (show a == expected) [
    "Expected to show " ++ expected,
    "But got          " ++ show a
  ]

shouldSatisfy : Show a => a -> (a -> Bool) -> IO ()
shouldSatisfy a pred =
  assert (pred a) [
    "Expectation unsatisfied: " ++ show a
  ]

castIdentical : (Cast a b, Cast b a, Eq a, Eq b) => (a, b) -> Bool
castIdentical (a, b) = cast a == b && cast b == a

shouldBe' : (Eq a, Show a) => IO a -> a -> IO ()
shouldBe' a b = a >>= (`shouldBe` b)

shouldShow' : Show a => IO a -> String -> IO ()
shouldShow' a b = a >>= (`shouldShow` b)

shouldSatisfy' : Show a => IO a -> (a -> Bool) -> IO ()
shouldSatisfy' a b = a >>= (`shouldSatisfy` b)

max_stars_repo_name: yubrot/idrlisp

max_issues_repo_name: yubrot/idrlisp

max_forks_repo_name: yubrot/idrlisp


text:
module Compiler.LambdaLift

import Core.CompileExpr
import Core.Context
import Core.Core
import Core.TT

import Data.List
import Data.Vect
import Data.Maybe

%default covering

mutual
  public export
  -- lazy (lazy reason) represents if a function application is lazy (Just _)
  -- and if so why (eg. Just LInf, Just LLazy)
  data Lifted : List Name -> Type where
       LLocal : {idx : Nat} -> FC -> (0 p : IsVar x idx vars) -> Lifted vars
       -- A known function applied to exactly the right number of arguments,
       -- so the runtime can Just Go
       LAppName : FC -> (lazy : Maybe LazyReason) -> Name -> List (Lifted vars) -> Lifted vars
       -- A known function applied to too few arguments, so the runtime should
       -- make a closure and wait for the remaining arguments
       LUnderApp : FC -> Name -> (missing : Nat) ->
                   (args : List (Lifted vars)) -> Lifted vars
       -- A closure applied to one more argument (so, for example a closure
       -- which is waiting for another argument before it can run).
       -- The runtime should add the argument to the closure and run the result
       -- if it is now fully applied.
       LApp : FC -> (lazy : Maybe LazyReason) -> (closure : Lifted vars) -> (arg : Lifted vars) -> Lifted vars
       LLet : FC -> (x : Name) -> Lifted vars ->
              Lifted (x :: vars) -> Lifted vars
       LCon : FC -> Name -> ConInfo -> (tag : Maybe Int) ->
              List (Lifted vars) -> Lifted vars
       LOp : {arity : _} ->
             FC -> (lazy : Maybe LazyReason) -> PrimFn arity -> Vect arity (Lifted vars) -> Lifted vars
       LExtPrim : FC -> (lazy : Maybe LazyReason) -> (p : Name) -> List (Lifted vars) -> Lifted vars
       LConCase : FC -> Lifted vars ->
                  List (LiftedConAlt vars) ->
                  Maybe (Lifted vars) -> Lifted vars
       LConstCase : FC -> Lifted vars ->
                    List (LiftedConstAlt vars) ->
                    Maybe (Lifted vars) -> Lifted vars
       LPrimVal : FC -> Constant -> Lifted vars
       LErased : FC -> Lifted vars
       LCrash : FC -> String -> Lifted vars

  public export
  data LiftedConAlt : List Name -> Type where
       MkLConAlt : Name -> ConInfo -> (tag : Maybe Int) -> (args : List Name) ->
                   Lifted (args ++ vars) -> LiftedConAlt vars

  public export
  data LiftedConstAlt : List Name -> Type where
       MkLConstAlt : Constant -> Lifted vars -> LiftedConstAlt vars

public export
data LiftedDef : Type where
     -- We take the outer scope and the function arguments separately so that
     -- we don't have to reshuffle de Bruijn indices, which is expensive.
     -- This should be compiled as a function which takes 'args' first,
     -- then 'reverse scope'.
     -- (Sorry for the awkward API - it's to do with how the indices are
     -- arranged for the variables, and it oculd be expensive to reshuffle them!
     -- See Compiler.ANF for an example of how they get resolved to names)
     MkLFun : (args : List Name) -> -- function arguments
              (scope : List Name) -> -- outer scope
              Lifted (scope ++ args) -> LiftedDef
     MkLCon : (tag : Maybe Int) -> (arity : Nat) -> (nt : Maybe Nat) -> LiftedDef
     MkLForeign : (ccs : List String) ->
                  (fargs : List CFType) ->
                  CFType ->
                  LiftedDef
     MkLError : Lifted [] -> LiftedDef

showLazy : Maybe LazyReason -> String
showLazy = maybe "" $ (" " ++) . show

mutual
  export
  {vs : _} -> Show (Lifted vs) where
    show (LLocal {idx} _ p) = "!" ++ show (nameAt p)
    show (LAppName fc lazy n args)
        = show n ++ showLazy lazy ++ "(" ++ showSep ", " (map show args) ++ ")"
    show (LUnderApp fc n m args)
        = "<" ++ show n ++ " underapp " ++ show m ++ ">(" ++
          showSep ", " (map show args) ++ ")"
    show (LApp fc lazy c arg)
        = show c ++ showLazy lazy ++ " @ (" ++ show arg ++ ")"
    show (LLet fc x val sc)
        = "%let " ++ show x ++ " = " ++ show val ++ " in " ++ show sc
    show (LCon fc n _ t args)
        = "%con " ++ show n ++ "(" ++ showSep ", " (map show args) ++ ")"
    show (LOp fc lazy op args)
        = "%op " ++ show op ++ showLazy lazy ++ "(" ++ showSep ", " (toList (map show args)) ++ ")"
    show (LExtPrim fc lazy p args)
        = "%extprim " ++ show p ++ showLazy lazy ++ "(" ++ showSep ", " (map show args) ++ ")"
    show (LConCase fc sc alts def)
        = "%case " ++ show sc ++ " of { "
             ++ showSep "| " (map show alts) ++ " " ++ show def
    show (LConstCase fc sc alts def)
        = "%case " ++ show sc ++ " of { "
             ++ showSep "| " (map show alts) ++ " " ++ show def
    show (LPrimVal _ x) = show x
    show (LErased _) = "___"
    show (LCrash _ x) = "%CRASH(" ++ show x ++ ")"

  export
  {vs : _} -> Show (LiftedConAlt vs) where
    show (MkLConAlt n _ t args sc)
        = "%conalt " ++ show n ++
             "(" ++ showSep ", " (map show args) ++ ") => " ++ show sc

  export
  {vs : _} -> Show (LiftedConstAlt vs) where
    show (MkLConstAlt c sc)
        = "%constalt(" ++ show c ++ ") => " ++ show sc

export
Show LiftedDef where
  show (MkLFun args scope exp)
      = show args ++ show (reverse scope) ++ ": " ++ show exp
  show (MkLCon tag arity pos)
      = "Constructor tag " ++ show tag ++ " arity " ++ show arity ++
        maybe "" (\n => " (newtype by " ++ show n ++ ")") pos
  show (MkLForeign ccs args ret)
      = "Foreign call " ++ show ccs ++ " " ++
        show args ++ " -> " ++ show ret
  show (MkLError exp) = "Error: " ++ show exp

data Lifts : Type where

record LDefs where
  constructor MkLDefs
  basename : Name -- top level name we're lifting from
  defs : List (Name, LiftedDef) -- new definitions we made
  nextName : Int -- name of next definition to lift

genName : {auto l : Ref Lifts LDefs} ->
          Core Name
genName
    = do ldefs <- get Lifts
         let i = nextName ldefs
         put Lifts (record { nextName = i + 1 } ldefs)
         pure $ mkName (basename ldefs) i
  where
    mkName : Name -> Int -> Name
    mkName (NS ns b) i = NS ns (mkName b i)
    mkName (UN n) i = MN (displayUserName n) i
    mkName (DN _ n) i = mkName n i
    mkName (CaseBlock outer inner) i = MN ("case block in " ++ outer ++ " (" ++ show inner ++ ")") i
    mkName (WithBlock outer inner) i = MN ("with block in " ++ outer ++ " (" ++ show inner ++ ")") i
    mkName n i = MN (show n) i

unload : FC -> (lazy : Maybe LazyReason) -> Lifted vars -> List (Lifted vars) -> Core (Lifted vars)
unload fc _ f [] = pure f
-- only outermost LApp must be lazy as rest will be closures
unload fc lazy f (a :: as) = unload fc Nothing (LApp fc lazy f a) as

record Used (vars : List Name) where
  constructor MkUsed
  used : Vect (length vars) Bool

initUsed : {vars : _} -> Used vars
initUsed {vars} = MkUsed (replicate (length vars) False)

lengthDistributesOverAppend
  : (xs, ys : List a)
  -> length (xs ++ ys) = length xs + length ys
lengthDistributesOverAppend [] ys = Refl
lengthDistributesOverAppend (x :: xs) ys =
  cong S $ lengthDistributesOverAppend xs ys

weakenUsed : {outer : _} -> Used vars -> Used (outer ++ vars)
weakenUsed {outer} (MkUsed xs) =
  MkUsed (rewrite lengthDistributesOverAppend outer vars in
         (replicate (length outer) False ++ xs))

contractUsed : (Used (x::vars)) -> Used vars
contractUsed (MkUsed xs) = MkUsed (tail xs)

contractUsedMany : {remove : _} ->
                   (Used (remove ++ vars)) ->
                   Used vars
contractUsedMany {remove=[]} x = x
contractUsedMany {remove=(r::rs)} x = contractUsedMany {remove=rs} (contractUsed x)

markUsed : {vars : _} ->
           (idx : Nat) ->
           {0 prf : IsVar x idx vars} ->
           Used vars ->
           Used vars
markUsed {vars} {prf} idx (MkUsed us) =
  let newUsed = replaceAt (finIdx prf) True us in
  MkUsed newUsed
    where
    finIdx : {vars : _} -> {idx : _} ->
               (0 prf : IsVar x idx vars) ->
               Fin (length vars)
    finIdx {idx=Z} First = FZ
    finIdx {idx=S x} (Later l) = FS (finIdx l)

getUnused : Used vars ->
            Vect (length vars) Bool
getUnused (MkUsed uv) = map not uv

total
dropped : (vars : List Name) ->
          (drop : Vect (length vars) Bool) ->
          List Name
dropped [] _ = []
dropped (x::xs) (False::us) = x::(dropped xs us)
dropped (x::xs) (True::us) = dropped xs us

mutual
  makeLam : {auto l : Ref Lifts LDefs} ->
            {vars : _} ->
            {doLazyAnnots : Bool} ->
            {default Nothing lazy : Maybe LazyReason} ->
            FC -> (bound : List Name) ->
            CExp (bound ++ vars) -> Core (Lifted vars)
  makeLam fc bound (CLam _ x sc') = makeLam fc {doLazyAnnots} {lazy} (x :: bound) sc'
  makeLam {vars} fc bound sc
      = do scl <- liftExp {doLazyAnnots} {lazy} sc
           -- Find out which variables aren't used in the new definition, and
           -- do not abstract over them in the new definition.
           let scUsedL = usedVars initUsed scl
               unusedContracted = contractUsedMany {remove=bound} scUsedL
               unused = getUnused unusedContracted
               scl' = dropUnused {outer=bound} unused scl
           n <- genName
           ldefs <- get Lifts
           put Lifts (record { defs $= ((n, MkLFun (dropped vars unused) bound scl') ::) } ldefs)
           pure $ LUnderApp fc n (length bound) (allVars fc vars unused)
    where
        allPrfs : (vs : List Name) -> (unused : Vect (length vs) Bool) -> List (Var vs)
        allPrfs [] _ = []
        allPrfs (v :: vs) (False::uvs) = MkVar First :: map weaken (allPrfs vs uvs)
        allPrfs (v :: vs) (True::uvs) = map weaken (allPrfs vs uvs)

        -- apply to all the variables. 'First' will be first in the last, which
        -- is good, because the most recently bound name is the first argument to
        -- the resulting function
        allVars : FC -> (vs : List Name) -> (unused : Vect (length vs) Bool) -> List (Lifted vs)
        allVars fc vs unused = map (\ (MkVar p) => LLocal fc p) (allPrfs vs unused)

-- if doLazyAnnots = True then annotate function application with laziness
-- otherwise use old behaviour (thunk is a function)
  liftExp : {vars : _} ->
            {auto l : Ref Lifts LDefs} ->
            {doLazyAnnots : Bool} ->
            {default Nothing lazy : Maybe LazyReason} ->
            CExp vars -> Core (Lifted vars)
  liftExp (CLocal fc prf) = pure $ LLocal fc prf
  liftExp (CRef fc n) = pure $ LAppName fc lazy n [] -- probably shouldn't happen!
  liftExp (CLam fc x sc) = makeLam {doLazyAnnots} {lazy} fc [x] sc
  liftExp (CLet fc x _ val sc) = pure $ LLet fc x !(liftExp {doLazyAnnots} val) !(liftExp {doLazyAnnots} sc)
  liftExp (CApp fc (CRef _ n) args) -- names are applied exactly in compileExp
      = pure $ LAppName fc lazy n !(traverse (liftExp {doLazyAnnots}) args)
  liftExp (CApp fc f args)
      = unload fc lazy !(liftExp {doLazyAnnots} f) !(traverse (liftExp {doLazyAnnots}) args)
  liftExp (CCon fc n ci t args) = pure $ LCon fc n ci t !(traverse (liftExp {doLazyAnnots}) args)
  liftExp (COp fc op args)
      = pure $ LOp fc lazy op !(traverseArgs args)
    where
      traverseArgs : Vect n (CExp vars) -> Core (Vect n (Lifted vars))
      traverseArgs [] = pure []
      traverseArgs (a :: as) = pure $ !(liftExp {doLazyAnnots} a) :: !(traverseArgs as)
  liftExp (CExtPrim fc p args) = pure $ LExtPrim fc lazy p !(traverse (liftExp {doLazyAnnots}) args)
  liftExp (CForce fc lazy tm) = if doLazyAnnots
    then liftExp {doLazyAnnots} {lazy = Nothing} tm
    else liftExp {doLazyAnnots} (CApp fc tm [CErased fc])
  liftExp (CDelay fc lazy tm) = if doLazyAnnots
    then liftExp {doLazyAnnots} {lazy = Just lazy} tm
    else liftExp {doLazyAnnots} (CLam fc (MN "act" 0) (weaken tm))
  liftExp (CConCase fc sc alts def)
      = pure $ LConCase fc !(liftExp {doLazyAnnots} sc) !(traverse (liftConAlt {lazy}) alts)
                           !(traverseOpt (liftExp {doLazyAnnots}) def)
    where
      liftConAlt : {default Nothing lazy : Maybe LazyReason} ->
                   CConAlt vars -> Core (LiftedConAlt vars)
      liftConAlt (MkConAlt n ci t args sc) = pure $ MkLConAlt n ci t args !(liftExp {doLazyAnnots} {lazy} sc)
  liftExp (CConstCase fc sc alts def)
      = pure $ LConstCase fc !(liftExp {doLazyAnnots} sc) !(traverse liftConstAlt alts)
                             !(traverseOpt (liftExp {doLazyAnnots}) def)
    where
      liftConstAlt : {default Nothing lazy : Maybe LazyReason} ->
                     CConstAlt vars -> Core (LiftedConstAlt vars)
      liftConstAlt (MkConstAlt c sc) = pure $ MkLConstAlt c !(liftExp {doLazyAnnots} {lazy} sc)
  liftExp (CPrimVal fc c) = pure $ LPrimVal fc c
  liftExp (CErased fc) = pure $ LErased fc
  liftExp (CCrash fc str) = pure $ LCrash fc str

  usedVars : {vars : _} ->
             {auto l : Ref Lifts LDefs} ->
             Used vars ->
             Lifted vars ->
             Used vars
  usedVars used (LLocal {idx} fc prf) =
    markUsed {prf} idx used
  usedVars used (LAppName fc lazy n args) =
    foldl (usedVars {vars}) used args
  usedVars used (LUnderApp fc n miss args) =
    foldl (usedVars {vars}) used args
  usedVars used (LApp fc lazy c arg) =
    usedVars (usedVars used arg) c
  usedVars used (LLet fc x val sc) =
    let innerUsed = contractUsed $ usedVars (weakenUsed {outer=[x]} used) sc in
        usedVars innerUsed val
  usedVars used (LCon fc n ci tag args) =
    foldl (usedVars {vars}) used args
  usedVars used (LOp fc lazy fn args) =
    foldl (usedVars {vars}) used args
  usedVars used (LExtPrim fc lazy fn args) =
    foldl (usedVars {vars}) used args
  usedVars used (LConCase fc sc alts def) =
      let defUsed = maybe used (usedVars used {vars}) def
          scDefUsed = usedVars defUsed sc in
          foldl usedConAlt scDefUsed alts
    where
      usedConAlt : {default Nothing lazy : Maybe LazyReason} ->
                   Used vars -> LiftedConAlt vars -> Used vars
      usedConAlt used (MkLConAlt n ci tag args sc) =
        contractUsedMany {remove=args} (usedVars (weakenUsed used) sc)

  usedVars used (LConstCase fc sc alts def) =
      let defUsed = maybe used (usedVars used {vars}) def
          scDefUsed = usedVars defUsed sc in
          foldl usedConstAlt scDefUsed alts
    where
      usedConstAlt : {default Nothing lazy : Maybe LazyReason} ->
                     Used vars -> LiftedConstAlt vars -> Used vars
      usedConstAlt used (MkLConstAlt c sc) = usedVars used sc
  usedVars used (LPrimVal _ _) = used
  usedVars used (LErased _) = used
  usedVars used (LCrash _ _) = used

  dropIdx : {vars : _} ->
            {idx : _} ->
            (outer : List Name) ->
            (unused : Vect (length vars) Bool) ->
            (0 p : IsVar x idx (outer ++ vars)) ->
            Var (outer ++ (dropped vars unused))
  dropIdx [] (False::_) First = MkVar First
  dropIdx [] (True::_) First = assert_total $
    idris_crash "INTERNAL ERROR: Referenced variable marked as unused"
  dropIdx [] (False::rest) (Later p) = Var.later $ dropIdx [] rest p
  dropIdx [] (True::rest) (Later p) = dropIdx [] rest p
  dropIdx (_::xs) unused First = MkVar First
  dropIdx (_::xs) unused (Later p) = Var.later $ dropIdx xs unused p

  dropUnused : {vars : _} ->
               {auto l : Ref Lifts LDefs} ->
               {outer : List Name} ->
               (unused : Vect (length vars) Bool) ->
               (l : Lifted (outer ++ vars)) ->
               Lifted (outer ++ (dropped vars unused))
  dropUnused _ (LPrimVal fc val) = LPrimVal fc val
  dropUnused _ (LErased fc) = LErased fc
  dropUnused _ (LCrash fc msg) = LCrash fc msg
  dropUnused {outer} unused (LLocal fc p) =
    let (MkVar p') = dropIdx outer unused p in LLocal fc p'
  dropUnused unused (LCon fc n ci tag args) =
    let args' = map (dropUnused unused) args in
        LCon fc n ci tag args'
  dropUnused {outer} unused (LLet fc n val sc) =
    let val' = dropUnused unused val
        sc' = dropUnused {outer=n::outer} (unused) sc in
        LLet fc n val' sc'
  dropUnused unused (LApp fc lazy c arg) =
    let c' = dropUnused unused c
        arg' = dropUnused unused arg in
        LApp fc lazy c' arg'
  dropUnused unused (LOp fc lazy fn args) =
    let args' = map (dropUnused unused) args in
        LOp fc lazy fn args'
  dropUnused unused (LExtPrim fc lazy n args) =
    let args' = map (dropUnused unused) args in
        LExtPrim fc lazy n args'
  dropUnused unused (LAppName fc lazy n args) =
    let args' = map (dropUnused unused) args in
        LAppName fc lazy n args'
  dropUnused unused (LUnderApp fc n miss args) =
    let args' = map (dropUnused unused) args in
        LUnderApp fc n miss args'
  dropUnused {vars} {outer} unused (LConCase fc sc alts def) =
    let alts' = map dropConCase alts in
        LConCase fc (dropUnused unused sc) alts' (map (dropUnused unused) def)
    where
      dropConCase : LiftedConAlt (outer ++ vars) ->
                    LiftedConAlt (outer ++ (dropped vars unused))
      dropConCase (MkLConAlt n ci t args sc) =
        let sc' = (rewrite sym $ appendAssociative args outer vars in sc)
            droppedSc = dropUnused {vars=vars} {outer=args++outer} unused sc' in
        MkLConAlt n ci t args (rewrite appendAssociative args outer (dropped vars unused) in droppedSc)
  dropUnused {vars} {outer} unused (LConstCase fc sc alts def) =
    let alts' = map dropConstCase alts in
        LConstCase fc (dropUnused unused sc) alts' (map (dropUnused unused) def)
    where
      dropConstCase : LiftedConstAlt (outer ++ vars) ->
                      LiftedConstAlt (outer ++ (dropped vars unused))
      dropConstCase (MkLConstAlt c val) = MkLConstAlt c (dropUnused unused val)

export
liftBody : {vars : _} -> {doLazyAnnots : Bool} ->
           Name -> CExp vars -> Core (Lifted vars, List (Name, LiftedDef))
liftBody n tm
    = do l <- newRef Lifts (MkLDefs n [] 0)
         tml <- liftExp {doLazyAnnots} {l} tm
         ldata <- get Lifts
         pure (tml, defs ldata)

export
lambdaLiftDef : (doLazyAnnots : Bool) -> Name -> CDef -> Core (List (Name, LiftedDef))
lambdaLiftDef doLazyAnnots n (MkFun args exp)
    = do (expl, defs) <- liftBody {doLazyAnnots} n exp
         pure ((n, MkLFun args [] expl) :: defs)
lambdaLiftDef _ n (MkCon t a nt) = pure [(n, MkLCon t a nt)]
lambdaLiftDef _ n (MkForeign ccs fargs ty) = pure [(n, MkLForeign ccs fargs ty)]
lambdaLiftDef doLazyAnnots n (MkError exp)
    = do (expl, defs) <- liftBody {doLazyAnnots} n exp
         pure ((n, MkLError expl) :: defs)

-- Return the lambda lifted definitions required for the given name.
-- If the name hasn't been compiled yet (via CompileExpr.compileDef) then
-- this will return an empty list
-- An empty list an error, because on success you will always get at least
-- one definition, the lifted definition for the given name.
export
lambdaLift :  {auto c : Ref Ctxt Defs}
           -> (doLazyAnnots : Bool)
           -> (Name,FC,CDef)
           -> Core (List (Name, LiftedDef))
lambdaLift doLazyAnnots (n,_,def) = lambdaLiftDef doLazyAnnots n def


text:
module Part2.Sec9_2_hangman
import Data.Vect
import Part2.Sec9_1_elem

%default total

data WordState : (guesses_remaining : Nat) -> (letters : Nat) -> Type where
     MkWordState : (word : String) ->
                   (missing : Vect letters Char) ->
                   WordState guesses_remaining letters

data Finished : Type where
             Lost : (game : WordState 0 (S letters)) -> Finished
             Won  : (game : WordState (S guesses) 0) -> Finished

processGuess : (letter : Char) -> WordState (S guesses) (S letters) -> Either (WordState guesses (S letters)) (WordState (S guesses) letters)
processGuess letter (MkWordState word missing) = case isElem letter missing of
          Yes prf => Right (MkWordState word (removeElem_auto letter missing))
          No contra => Left (MkWordState word missing)

{- the rest is user interface code -}

data ValidInput : List Char -> Type where
     Letter : (c : Char) -> ValidInput [c]

invalidNil : ValidInput [] -> Void
invalidNil (Letter _) impossible

invalidTwo : ValidInput (x :: y :: xs) -> Void
invalidTwo (Letter _) impossible

isValidInput : (cs : List Char) -> Dec (ValidInput cs)
isValidInput [] = No invalidNil
isValidInput (x :: []) = Yes (Letter x)
isValidInput (x :: (y :: xs)) = No invalidTwo

isValidString : (s : String) -> Dec (ValidInput (unpack s))
isValidString s = isValidInput (unpack s)

covering
readGuess : IO (x ** ValidInput x)
readGuess = do putStr "Guess:"
               x <- getLine
               case isValidString (toUpper x) of
                  Yes prf => pure (_ ** prf)
                  No contra => do putStrLn "Invalid guess"
                                  readGuess

covering
game : WordState (S guesses) (S letters) -> IO Finished
game {guesses} {letters} st
             = do (_ ** Letter letter) <- readGuess
                  case processGuess letter st of
                    Left l => do putStrLn "Wrong!"
                                 case guesses of
                                      Z => pure (Lost l)
                                      S k => game l
                    Right r => do putStrLn "Right!"
                                  case letters of
                                       Z => pure (Won r)
                                       S k => game r

{- To execute in repl, idrs repl from src folder, :l this file and use :exec sec_9_2 -}
covering
sec_9_2 : IO ()
sec_9_2 = do result <- game {guesses=2} (MkWordState "Test" ['T', 'E', 'S'])
             case result of
               Lost (MkWordState word missing) =>
                  putStrLn ("You lose. The word was " ++ word)
               Won game =>
                  putStrLn "You win!"

max_stars_repo_name: rpeszek/IdrisTddNotes

max_issues_repo_name: rpeszek/IdrisTddNotes

max_forks_repo_name: rpeszek/IdrisTddNotes


text:
||| Spec: https://webassembly.github.io/spec/core/syntax/instructions.html#control-instructions
module WebAssembly.Structure.Instructions.Control

import WebAssembly.Structure.Types
import WebAssembly.Structure.Modules.Indices

-- Definition
-- Hint: Actual control-instructions are defined in
-- WebAssembly.Structure.Instructions.Definitions

public export
data BlockType : Type where
  BlockTypeTypeIdx   : TypeIdx -> BlockType
  BlockTypeEmpty     : BlockType
  BlockTypeSingelton : ValType -> BlockType

total public export
lemma_blocktypetypeindex_not_blocktypeempty : ((BlockTypeTypeIdx ti) = BlockTypeEmpty) -> Void
lemma_blocktypetypeindex_not_blocktypeempty Refl impossible

total public export
lemma_blocktypetypeindex_not_blocktypesingelton : ((BlockTypeTypeIdx ti) = (BlockTypeSingelton vt)) -> Void
lemma_blocktypetypeindex_not_blocktypesingelton Refl impossible

total public export
lemma_blocktypeempty_not_blocktypesingelton : (BlockTypeEmpty = (BlockTypeSingelton vt)) -> Void
lemma_blocktypeempty_not_blocktypesingelton Refl impossible

total public export
lemma_blocktype__typeindex_injective : ((i = j) -> Void) -> (BlockTypeTypeIdx i = BlockTypeTypeIdx j) -> Void
lemma_blocktype__typeindex_injective i_not_j Refl = i_not_j Refl

total public export
lemma_blocktype__singelton_injective : ((vt1 = vt2) -> Void) -> (BlockTypeSingelton vt1 = BlockTypeSingelton vt2) -> Void
lemma_blocktype__singelton_injective vt1_not_vt2 Refl = vt1_not_vt2 Refl

-- Decidable Equality

public export
implementation DecEq BlockType where
  decEq (BlockTypeTypeIdx k)   (BlockTypeTypeIdx j) with (decEq k j)
    decEq (BlockTypeTypeIdx k)   (BlockTypeTypeIdx j) | No contra = No $ lemma_blocktype__typeindex_injective contra
    decEq (BlockTypeTypeIdx k)   (BlockTypeTypeIdx k) | Yes Refl = Yes Refl
  decEq (BlockTypeTypeIdx k)   BlockTypeEmpty         = No lemma_blocktypetypeindex_not_blocktypeempty
  decEq (BlockTypeTypeIdx k)   (BlockTypeSingelton x) = No lemma_blocktypetypeindex_not_blocktypesingelton
  decEq BlockTypeEmpty         (BlockTypeTypeIdx k)   = No $ negEqSym lemma_blocktypetypeindex_not_blocktypeempty
  decEq BlockTypeEmpty         BlockTypeEmpty         = Yes Refl
  decEq BlockTypeEmpty         (BlockTypeSingelton x) = No lemma_blocktypeempty_not_blocktypesingelton
  decEq (BlockTypeSingelton x) (BlockTypeTypeIdx k)   = No $ negEqSym lemma_blocktypetypeindex_not_blocktypesingelton
  decEq (BlockTypeSingelton x) BlockTypeEmpty         = No $ negEqSym lemma_blocktypeempty_not_blocktypesingelton
  decEq (BlockTypeSingelton x) (BlockTypeSingelton y) with (decEq x y)
    decEq (BlockTypeSingelton x) (BlockTypeSingelton y) | No contra = No $ lemma_blocktype__singelton_injective contra
    decEq (BlockTypeSingelton x) (BlockTypeSingelton x) | Yes Refl = Yes Refl

max_stars_repo_name: RaoulSchaffranek/idris-webassembly

max_issues_repo_name: RaoulSchaffranek/idris-webassembly

max_forks_repo_name: RaoulSchaffranek/idris-webassembly


text:
-- ------------------------------------------------------------ [ Literals.idr ]
||| Module    : Literals.idr
||| Copyright : (c) Jan de Muijnck-Hughes
||| License   : see LICENSE
|||
||| Deal with literal values at the type-level.
module Commons.Data.Literals

%default total
%access public export

||| Proof that the given value level `b` of type `ty` has value `a`.
data Literal : (ty : Type)
            -> (a : ty)
            -> Type
  where
    MkLiteral : (b : ty)
             -> (prf : b = a)
             -> Literal ty a

newLiteral : (b : ty) -> Literal ty b
newLiteral b = MkLiteral b Refl

||| Representation of String literals.
LitString : String -> Type
LitString str = Literal String str

||| Proof that the given natural `o` is the successor of `n`.
data Next : (n : Nat) -> Type where
  MkNext : (o : Nat) -> (prf : o = S n) -> Next n

newNext : (o,n : Nat) -> (prf : o = S n) -> Next n
newNext o _ prf = MkNext o prf

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

max_stars_repo_name: jfdm/idris-common

max_issues_repo_name: jfdm/idris-common

max_forks_repo_name: jfdm/idris-common


text:
module Libra.Constants

import Data.Vect

%access export
%default total

{-
  Constants
-}

||| Lowercase and uppercase alphabetic characters
Alphabet : Vect 52 Char
Alphabet = [ 'a', 'b', 'c', 'd', 'e', 'f', 'g', 'h', 'i', 'j', 'k', 'l', 'm',
             'n', 'o', 'p', 'q', 'r', 's', 't', 'u', 'v', 'w', 'x', 'y', 'z',
             'A', 'B', 'C', 'D', 'E', 'F', 'G', 'H', 'I', 'J', 'K', 'L', 'M',
             'N', 'O', 'P', 'Q', 'R', 'S', 'T', 'U', 'V', 'W', 'X', 'Y', 'Z' ]

||| Numerical characters from 0 through 9
Digits : Vect 10 Char
Digits = [ '0', '1', '2', '3', '4', '5', '6', '7', '8', '9' ]

||| Alphanumerical characters corresponding to: [a-zA-Z0-9]
Alphanumeric : Vect 62 Char
Alphanumeric = Alphabet ++ Digits

max_stars_repo_name: ostera/libra

max_issues_repo_name: ostera/libra

max_forks_repo_name: ostera/libra


text:
module OfficialCrashCourse.DepTypes

import Data.Vect

-- isSingle : Type
isSingleton : Bool -> Type
isSingleton True = Nat
isSingleton False = List Nat

mkSingle : (x : Bool) -> isSingleton x
mkSingle True = 0
mkSingle False = []

-- Vect is like a List having length Nat elements
data Vector : Nat -> Type -> Type where
    NilVec  : Vector Z a
    (::) : a -> Vector k a -> Vector (S k) a

-- Defining a set of Nat many elems like above
data FinSet : Nat -> Type where
    FZ : FinSet (S k) -- zeroth element
    FS : FinSet k -> FinSet (S k) -- k + 1 th element from k th element

-- using implicit arguments and proofs
appVec: Ord a => Vector n a -> Vector m a -> Vector (n + m) a
appVec NilVec vecm = vecm -- 0 + left  = left
appVec {n} vecn NilVec = rewrite plusZeroRightNeutral n in vecn -- left + 0 = left
appVec {n=(S n)} {m=(S m)} ( x :: xs) (y :: ys) =
    rewrite sym $ plusSuccRightSucc n m in -- using sym to flip args, S (left + right) = left + S right
    x :: y :: (appVec xs ys)

-- what is the i th element in a n sized Vector with i <= n?
indexer : Fin n -> Vect n a -> a
indexer FZ (x :: _) = x
indexer (FS i) (_ :: xs) = indexer i xs

isEmpty : {n: Nat} -> Vect n a -> Bool
isEmpty {n = Z} _ = True
isEmpty _ = False

max_stars_repo_name: umbrela-academy/idrusti

max_issues_repo_name: umbrela-academy/idrusti

max_forks_repo_name: umbrela-academy/idrusti


text:
module Accumulate

export
accumulate : (a -> b) -> List a -> List b
accumulate f [] = []
accumulate f (x::xs) = f x :: accumulate f xs


text:
module Solutions.IO

import Data.List1
import Data.String

import System.File

%default total

--------------------------------------------------------------------------------
--          Pure Side Effects?
--------------------------------------------------------------------------------

-- 1
rep : (String -> String) -> IO ()
rep f = do
  s <- getLine
  putStrLn (f s)

-- 2
covering
repl : (String -> String) -> IO ()
repl f = do
  _ <- rep f
  repl f

-- 3
covering
replTill : (String -> Either String String) -> IO ()
replTill f = do
  s <- getLine
  case f s of
    Left  msg => putStrLn msg
    Right msg => do
      _ <- putStrLn msg
      replTill f

-- 4
data Error : Type where
  NotAnInteger    : (value : String) -> Error
  UnknownOperator : (value : String) -> Error
  ParseError      : (input : String) -> Error

dispError : Error -> String
dispError (NotAnInteger v)    = "Not an integer: " ++ v ++ "."
dispError (UnknownOperator v) = "Unknown operator: " ++ v ++ "."
dispError (ParseError v)      = "Invalid expression: " ++ v ++ "."

readInteger : String -> Either Error Integer
readInteger s = maybe (Left $ NotAnInteger s) Right $ parseInteger s

readOperator : String -> Either Error (Integer -> Integer -> Integer)
readOperator "+" = Right (+)
readOperator "*" = Right (*)
readOperator s   = Left (UnknownOperator s)

eval : String -> Either Error Integer
eval s =
  let [x,y,z]  := forget $ split isSpace s | _ => Left (ParseError s)
      Right v1 := readInteger x  | Left e => Left e
      Right op := readOperator y | Left e => Left e
      Right v2 := readInteger z  | Left e => Left e
   in Right $ op v1 v2

covering
exprProg : IO ()
exprProg = replTill prog
  where prog : String -> Either String String
        prog "done" = Left "Goodbye!"
        prog s      = Right . either dispError show $ eval s

-- 5
covering
replWith :  (state      : s)
         -> (next       : s -> String -> Either res s)
         -> (dispState  : s -> String)
         -> (dispResult : res -> s -> String)
         -> IO ()
replWith state next dispState dispResult = do
  _     <- putStrLn (dispState state)
  input <- getLine
  case next state input of
    Left  result => putStrLn (dispResult result state)
    Right state' => replWith state' next dispState dispResult

-- 6
data Abort : Type where
  NoNat : (input : String) -> Abort
  Done  : Abort

printSum : Nat -> String
printSum n =
  "Current sum: " ++ show n ++ "\nPlease enter a natural number:"

printRes : Abort -> Nat -> String
printRes (NoNat input) _ =
  "Not a natural number: " ++ input ++ ". Aborting..."
printRes Done k =
  "Final sum: " ++ show k ++ "\nHave a nice day."

readInput : Nat -> String -> Either Abort Nat
readInput _ "done" = Left Done
readInput n s      = case parseInteger {a = Integer} s of
  Nothing => Left $ NoNat s
  Just v  => if v >= 0 then Right (cast v + n) else Left (NoNat s)

covering
sumProg : IO ()
sumProg = replWith 0 readInput printSum printRes

--------------------------------------------------------------------------------
--          Do Blocks, Desugared
--------------------------------------------------------------------------------

-- 1
ex1a : IO String
ex1a = do
  s1 <- getLine
  s2 <- getLine
  s3 <- getLine
  pure $ s1 ++ reverse s2 ++ s3

ex1aBind : IO String
ex1aBind =
  getLine >>= (\s1 =>
    getLine >>= (\s2 =>
      getLine >>= (\s3 =>
        pure $ s1 ++ reverse s2 ++ s3
      )
    )
  )

ex1aBang : IO String
ex1aBang =
  pure $ !getLine ++ reverse !getLine ++ !getLine

ex1b : Maybe Integer
ex1b = do
  n1 <- parseInteger "12"
  n2 <- parseInteger "300"
  Just $ n1 + n2 * 100

ex1bBind : Maybe Integer
ex1bBind =
  parseInteger "12" >>= (\n1 =>
    parseInteger "300" >>= (\n2 =>
      Just $ n1 + n2 * 100
    )
  )

ex1bBang : Maybe Integer
ex1bBang =
  Just $ !(parseInteger "12") + !(parseInteger "300") * 100

-- 2
data List01 : (nonEmpty : Bool) -> Type -> Type where
  Nil  : List01 False a
  (::) : a -> List01 False a -> List01 ne a

head : List01 True a -> a
head (x :: _) = x

weaken : List01 ne a -> List01 False a
weaken []       = []
weaken (h :: t) = h :: t

map01 : (a -> b) -> List01 ne a -> List01 ne b
map01 _ []       = []
map01 f (x :: y) = f x :: map01 f y

tail : List01 True a -> List01 False a
tail (_ :: t) = weaken t

(++) : List01 ne1 a -> List01 ne2 a -> List01 (ne1 || ne2) a
(++) []       []       = []
(++) []       (h :: t) = h :: t
(++) (h :: t) xs       = h :: weaken (t ++ xs)

concat' : List01 ne1 (List01 ne2 a) -> List01 False a
concat' []       = []
concat' (x :: y) = weaken (x ++ concat' y)

concat :  {ne1, ne2 : _}
       -> List01 ne1 (List01 ne2 a)
       -> List01 (ne1 && ne2) a
concat {ne1 = True}  {ne2 = True}  (x :: y) = x ++ concat' y
concat {ne1 = True}  {ne2 = False} x        = concat' x
concat {ne1 = False} {ne2 = _}     x        = concat' x

namespace List01
  export
  (>>=) :  {ne1, ne2 : _}
        -> List01 ne1 a
        -> (a -> List01 ne2 b)
        -> List01 (ne1 && ne2) b
  as >>= f = concat (map01 f as)

--------------------------------------------------------------------------------
--          Working with Files
--------------------------------------------------------------------------------

-- 1
namespace IOErr
  export
  pure : a -> IO (Either e a)
  pure = pure . Right

  export
  fail : e -> IO (Either e a)
  fail = pure . Left

  export
  lift : IO a -> IO (Either e a)
  lift = map Right

  export
  catch : IO (Either e1 a) -> (e1 -> IO (Either e2 a)) -> IO (Either e2 a)
  catch io f = do
    Left err <- io | Right v => pure v
    f err

  export
  (>>=) : IO (Either e a) -> (a -> IO (Either e b)) -> IO (Either e b)
  io >>= f = Prelude.do
    Right v <- io | Left err => fail err
    f v

  export
  (>>) : IO (Either e ()) -> Lazy (IO (Either e a)) -> IO (Either e a)
  iou >> ioa = Prelude.do
    Right _ <- iou | Left err => fail err
    ioa

covering
countEmpty'' : (path : String) -> IO (Either FileError Nat)
countEmpty'' path = withFile path Read pure (go 0)
  where covering go : Nat -> File -> IO (Either FileError Nat)
        go k file = do
          False <- lift (fEOF file) | True => pure k
          "\n"  <- fGetLine file    | _  => go k file
          go (k + 1) file

-- 2
covering
countWords : (path : String) -> IO (Either FileError Nat)
countWords path = withFile path Read pure (go 0)
  where covering go : Nat -> File -> IO (Either FileError Nat)
        go k file = do
          False <- lift (fEOF file) | True => pure k
          s     <- fGetLine file
          go (k + length (words s)) file

-- 3
covering
withLines :  (path : String)
          -> (accum : s -> String -> s)
          -> (initialState : s)
          -> IO (Either FileError s)
withLines path accum ini = withFile path Read pure (go ini)
  where covering go : s -> File -> IO (Either FileError s)
        go st file = do
          False <- lift (fEOF file) | True => pure st
          line  <- fGetLine file
          go (accum st line) file

covering
countEmpty3 : (path : String) -> IO (Either FileError Nat)
countEmpty3 path = withLines path acc 0
  where acc : Nat -> String -> Nat
        acc k "\n" = k + 1
        acc k _    = k

covering
countWords2 : (path : String) -> IO (Either FileError Nat)
countWords2 path = withLines path (\n,s => n + length (words s)) 0

-- 4
covering
foldLines :  Monoid s
          => (path : String)
          -> (f    : String -> s)
          -> IO (Either FileError s)
foldLines path f = withLines path (\vs => (vs <+>) . f) neutral

-- 5

-- Instead of returning a triple of natural numbers,
-- it is better to make the semantics clear and use
-- a custom record type to store the result.
--
-- In a larger, more-complex application it might be
-- even better to make things truly type safe and
-- define a single field record together with an instance
-- of monoid for each kind of count.
record WC where
  constructor MkWC
  lines : Nat
  words : Nat
  chars : Nat

Semigroup WC where
  MkWC l1 w1 c1 <+> MkWC l2 w2 c2 = MkWC (l1 + l2) (w1 + w2) (c1 + c2)

Monoid WC where
  neutral = MkWC 0 0 0

covering
toWC : String -> WC
toWC s = MkWC 1 (length (words s)) (length s)

covering
wordCount : (path : String) -> IO (Either FileError WC)
wordCount path = foldLines path toWC

-- this is for testing the `wordCount` example.
covering
testWC : (path : String) -> IO ()
testWC path = Prelude.do
  Right (MkWC ls ws cs) <- wordCount path
    | Left err => putStrLn "Error: \{show err}"
  putStrLn "\{show ls} lines, \{show ws} words, \{show cs} characters"


text:
module Json

import public Lightyear
import public Lightyear.Char
import public Lightyear.Strings

import public Data.SortedMap

%access public export

data JsonValue = JsonString String
               | JsonNumber Double
               | JsonBool Bool
               | JsonNull
               | JsonArray (List JsonValue)
               | JsonObject (SortedMap String JsonValue)

Show JsonValue where
  show (JsonString s)   = show s
  show (JsonNumber x)   = show x
  show (JsonBool True ) = "true"
  show (JsonBool False) = "false"
  show  JsonNull        = "null"
  show (JsonArray  xs)  = show xs
  show (JsonObject xs)  =
      "{" ++ intercalate ", " (map fmtItem $ SortedMap.toList xs) ++ "}"
    where
      intercalate : String -> List String -> String
      intercalate sep [] = ""
      intercalate sep [x] = x
      intercalate sep (x :: xs) = x ++ sep ++ intercalate sep xs

      fmtItem (k, v) = show k ++ ": " ++ show v

hex : Parser Int
hex = do
  c <- map (ord . toUpper) $ satisfy isHexDigit
  pure $ if c >= ord '0' && c <= ord '9' then c - ord '0'
                                         else 10 + c - ord 'A'

hexQuad : Parser Int
hexQuad = do
  a <- hex
  b <- hex
  c <- hex
  d <- hex
  pure $ a * 4096 + b * 256 + c * 16 + d

specialChar : Parser Char
specialChar = do
  c <- anyChar
  case c of
    '"'  => pure '"'
    '\\' => pure '\\'
    '/'  => pure '/'
    'b'  => pure '\b'
    'f'  => pure '\f'
    'n'  => pure '\n'
    'r'  => pure '\r'
    't'  => pure '\t'
    'u'  => map chr hexQuad
    _    => fail "expected special char"

jsonString' : Parser (List Char)
jsonString' = (char '"' *!> pure Prelude.List.Nil) <|> do
  c <- satisfy (/= '"')
  if (c == '\\') then map (::) specialChar <*> jsonString'
                 else map (c ::) jsonString'

jsonString : Parser String
jsonString = char '"' *> map pack jsonString' <?> "JSON string"

-- inspired by Haskell's Data.Scientific module
record Scientific where
  constructor MkScientific
  coefficient : Integer
  exponent : Integer

scientificToDouble : Scientific -> Double
scientificToDouble (MkScientific c e) = fromInteger c * exp
  where exp = if e < 0 then 1 / pow 10 (fromIntegerNat (- e))
                       else pow 10 (fromIntegerNat e)

parseScientific : Parser Scientific
parseScientific = do sign <- maybe 1 (const (-1)) `map` opt (char '-')
                     digits <- some digit
                     hasComma <- isJust `map` opt (char '.')
                     decimals <- if hasComma then some digit else pure Prelude.List.Nil
                     hasExponent <- isJust `map` opt (char 'e')
                     exponent <- if hasExponent then integer else pure 0
                     pure $ MkScientific (sign * fromDigits (digits ++ decimals))
                                         (exponent - cast (length decimals))
  where fromDigits : List (Fin 10) -> Integer
        fromDigits = foldl (\a, b => 10 * a + cast b) 0

jsonNumber : Parser Double
jsonNumber = map scientificToDouble parseScientific

jsonBool : Parser Bool
jsonBool  =  (char 't' >! string "rue"  *> return True)
         <|> (char 'f' >! string "alse" *> return False) <?> "JSON Bool"

jsonNull : Parser ()
jsonNull = (char 'n' >! string "ull" >! return ()) <?> "JSON Null"

mutual
  jsonArray : Parser (List JsonValue)
  jsonArray = char '[' *!> (jsonValue `sepBy` (char ',')) <* char ']'

  keyValuePair : Parser (String, JsonValue)
  keyValuePair = do
    key <- spaces *> jsonString <* spaces
    char ':'
    value <- jsonValue
    pure (key, value)

  jsonObject : Parser (SortedMap String JsonValue)
  jsonObject = map fromList (char '{' >! (keyValuePair `sepBy` char ',') <* char '}')

  jsonValue' : Parser JsonValue
  jsonValue' =  (map JsonString jsonString)
            <|> (map JsonNumber jsonNumber)
            <|> (map JsonBool   jsonBool)
            <|> (pure JsonNull <* jsonNull)
            <|>| map JsonArray  jsonArray
            <|>| map JsonObject jsonObject

  jsonValue : Parser JsonValue
  jsonValue = spaces *> jsonValue' <* spaces

jsonToplevelValue : Parser JsonValue
jsonToplevelValue = (map JsonArray jsonArray) <|> (map JsonObject jsonObject)

max_stars_repo_name: david-christiansen/lightyear

max_issues_repo_name: david-christiansen/lightyear

max_forks_repo_name: david-christiansen/lightyear


text:
module Mergesort

import Data.Vect

import Evens

-- import SortingWithProof

total
NatVect : Nat -> Type
NatVect n = Vect n Nat

total
SortProof : (n : Nat) -> (NatVect n) -> (Fin n) -> Type
SortProof Z v a impossible
SortProof (S k) v l = LTE (Vect.index (pred l) v) (Vect.index l v)

total
IsSorted : (n : Nat) -> (v : (NatVect n)) -> Type
IsSorted n v = (k : Fin n) -> (SortProof n v k)

--Takes the first m elements from a vector
Vecttake : (m:Nat)->Vect n elem -> LTE m n -> Vect m  elem
Vecttake Z xs LTEZero = []
Vecttake (S k) (x::xs) (LTESucc pf) = x::(Vecttake k xs pf)

--Takes the last m elements from a vector
Vecttakefromlast :(m:Nat)->Vect n elem -> LTE m n ->Vect m elem
Vecttakefromlast m xs pf = reverse (Vecttake  m (reverse xs) pf)

-- Inserts an element at the end of the vector
insertend : (x:elem)->Vect n elem->Vect (S n) elem
insertend x [] = [x]
insertend x (y :: xs) = y::(insertend x xs)

--apNat as defined in class. Lemma that proves that if n = m, then f(n) = f(m)
apNat : (f: Nat -> Nat) -> (n: Nat) -> (m: Nat) -> n = m -> f n = f m
apNat f m m Refl = Refl

--defined in class. Returns n/2 if n is even
half : (n: Nat) -> IsEven n -> Nat
half Z ZEven = 0
half (S (S k)) (SSEven k x) = S (half k x)

--returns (n - 1)/2 if (n + 1) is odd
halfnMinusone : (n : Nat) -> (IsEven (S n)) -> Nat
halfnMinusone (S Z) (SSEven Z ZEven) = Z
halfnMinusone (S (S k)) (SSEven (S k) pf) = S(halfnMinusone k pf)

-- lemma that proves that n is LTE S n
nLTESn : (n : Nat) -> LTE n (S n)
nLTESn Z = LTEZero
nLTESn (S k) = LTESucc (nLTESn k)

-- lemma that proves that if n is even, then half n is LTE n
halfnLTEn : (n: Nat) -> (pf : IsEven n) -> LTE (half n pf) n
halfnLTEn Z ZEven = LTEZero
halfnLTEn (S (S k)) (SSEven k p) =  lteTransitive (LTESucc (halfnLTEn k p)) (nLTESn (S k))

-- lemma that proves that if S n is even, then half S n is LTE n
halfSnLTEn : (n : Nat) -> (pf : IsEven (S n)) -> LTE (half (S n) pf) n
halfSnLTEn (S Z) (SSEven Z ZEven) = LTESucc LTEZero
halfSnLTEn (S (S k)) (SSEven (S k) pf) = lteTransitive (LTESucc (halfSnLTEn k pf)) (nLTESn (S k))

-- lemma that proves that if S n is even, then (n - 1)/2 is LTE n
halfnMinusoneLTEn : (n : Nat) -> (pf : IsEven (S n)) -> LTE (halfnMinusone n pf) n
halfnMinusoneLTEn (S Z) (SSEven Z ZEven) = LTEZero
halfnMinusoneLTEn (S (S k)) (SSEven (S k) pf) = lteTransitive (LTESucc (halfnMinusoneLTEn k pf)) (nLTESn (S k))

-- lemma that proves that if a = b, then a is LTE b
-- IMPORTANT : this is not Total
equalImpliesLTE : (a : Nat) -> (b : Nat) -> (a = b) -> LTE a b
equalImpliesLTE Z Z Refl = LTEZero
equalImpliesLTE (S k) (S k) Refl = LTESucc (equalImpliesLTE k k Refl)

-- proof that if n is even, then (n/2 + n/2) = n
nEqualhalfnplushalfn : (n : Nat) -> (pf : IsEven n) -> ((half n pf) + (half n pf)) = n
nEqualhalfnplushalfn Z ZEven = Refl
nEqualhalfnplushalfn (S (S k)) (SSEven k x) = rewrite (sym (plusSuccRightSucc (S (half k x)) (half k x))) in (cong {f = \l => (S (S l))} (nEqualhalfnplushalfn k x))

-- proof that if n is even, then n is LTE (n/2 + n/2)
nLTEhalfnplushalfn : (n : Nat) -> (pf : IsEven n) -> LTE n ((half n pf) + (half n pf))
nLTEhalfnplushalfn n pf = equalImpliesLTE n ((half n pf) + (half n pf)) (sym (nEqualhalfnplushalfn n pf))

-- proof that if S n is even, then ((n + 1)/2 + (n - 1)/2) = n
nEqualhalfOddn : (n : Nat) -> (pf : IsEven (S n)) -> ((half (S n) pf) + (halfnMinusone n pf)) = n
nEqualhalfOddn (S Z) (SSEven Z ZEven) = Refl
nEqualhalfOddn (S (S k)) (SSEven (S k) pf) = rewrite (sym (plusSuccRightSucc (S (half (S k) pf)) (halfnMinusone k pf))) in (cong {f = \l => (S (S l))} (nEqualhalfOddn k pf))

-- proof that if S n is even, then n is LTE ((n + 1)/2 + (n - 1)/2)
nLTEhalfOddn : (n : Nat) -> (pf : IsEven (S n)) -> LTE n ((half (S n) pf) + (halfnMinusone n pf))
nLTEhalfOddn n pf = equalImpliesLTE n ((half (S n) pf) + (halfnMinusone n pf)) (sym (nEqualhalfOddn n pf))

-- proof the n is either odd or even (done in class)
nOrSnEven: (n: Nat) -> Either (IsEven n) (IsEven (S n))
nOrSnEven Z = Left ZEven
nOrSnEven (S k) = case (nOrSnEven k) of
                       (Left l) => Right (SSEven k l)
                       (Right r) => Left r

-- function that takes a vector of even length, and divides it into two equal halves
halfVectEven : Vect n elem -> (pf : IsEven n) -> ((Vect (half n pf) elem), (Vect (half n pf) elem))
halfVectEven {n} xs pf = ((Vecttake (half n pf) xs (halfnLTEn n pf)), (Vecttakefromlast (half n pf) xs (halfnLTEn n pf)))

-- function that takes a vector of odd length, and divides it into two unequal parts ((n + 1)/2 and (n - 1)/2)
halfVectOdd : Vect n elem -> (pf : IsEven (S n)) -> ((Vect (half (S n) pf) elem), (Vect (halfnMinusone n pf) elem))
halfVectOdd {n} xs pf = ((Vecttake (half (S n) pf) xs (halfSnLTEn n pf)), (Vecttakefromlast (halfnMinusone n pf) xs (halfnMinusoneLTEn n pf)))

-- proof that n is LTE n (proved in class)
reflLTE : (n: Nat) -> LTE n n
reflLTE Z = LTEZero
reflLTE (S k) = LTESucc (reflLTE k)

-- lemma that a is LTE ((S a) + b)
lemma1 : (a : Nat) -> (b: Nat) -> LTE a ((S a) + b)
lemma1 Z b = LTEZero
lemma1 (S k) b = LTESucc (lemma1 k b)

-- lemma that (S (a + b)) is LTE (a + S b)
lemma2 : (a : Nat) -> (b : Nat) -> LTE (S (a + b)) (a + (S b))
lemma2 Z b = reflLTE (S b)
lemma2 (S k) b = LTESucc (lemma2 k b)

-- lemma that (S b) is LTE ((S a) + b)
lemma3 : (a : Nat) -> (b : Nat) -> LTE (S b) ((S a) + b)
lemma3 a Z = LTESucc LTEZero
lemma3 a (S k) = lteTransitive (LTESucc (lemma3 a k)) (lemma2 (S a) k)

--these are functions to cast a vector from one type to another
sillycast: (Vect ((S k) + j) elem) ->( Vect (k+ (S j)) elem)
sillycast {k} {j} v1 = (Vecttake k v1 (lemma1 k j)) ++ (Vecttakefromlast (S j) v1 (lemma3 k j))

sillycastEven : (n : Nat) -> (pf : IsEven n) -> (Vect ((half n pf) + (half n pf)) elem) -> Vect n elem
sillycastEven n pf xs = Vecttake n xs (nLTEhalfnplushalfn n pf)

sillycastOdd : (n : Nat) -> (pf : IsEven (S n)) -> (Vect ((half (S n) pf) + (halfnMinusone n pf)) elem) -> Vect n elem
sillycastOdd n pf xs = Vecttake n xs (nLTEhalfOddn n pf)

--The merge function
merge1 :Ord elem =>Vect  n elem ->Vect  m elem ->Vect (n+m) elem
merge1 [] ys = ys
merge1  (x :: xs) [] =  (x::xs)++[]
merge1 {n= (S k)}{m= (S j)} (x :: xs) (y :: ys) = case x<=y of
                                 False => y::(sillycast( (merge1  (x::xs) ys)))
                                 True => x::(merge1 xs (y::ys))

mergeNat : (v1 : (NatVect n)) -> (v2 : (NatVect m)) -> (NatVect (n + m))
mergeNat v1 v2 = merge1 v1 v2

--The mergesort function
-- working of mergesort :
-- Step 1 : Checks if the lenght of the vector is odd or Even
-- Step 2 : if Even -> split into two equal parts (n/2 , n/2 )
--          if Odd -> split into two unequal parts ( (n + 1)/2 , (n - 1)/2)
-- Step 3 : apply mergesort recursively on the two parts
-- Step 4 : merge the two sorted parts according to the merge1 function
-- Step 5 : The vector obtained from merge will be of the type Vect (a + b) elem,
--  where (a + b) = n. The Vector is cast into the type Vect n elem by the
--  sillycast functions.
mergesort :Ord elem => Vect n elem -> Vect n elem
mergesort [] = []
mergesort [x] = [x]
mergesort {n} xs = case (nOrSnEven n) of
                    (Left nEven) => sillycastEven n nEven (merge1 (mergesort (fst(halfVectEven xs nEven))) (mergesort (snd(halfVectEven xs nEven))))
                    (Right snEven) => sillycastOdd n snEven (merge1 (mergesort (fst(halfVectOdd xs snEven))) (mergesort (snd(halfVectOdd xs snEven))))

--GOAL : To prove that mergesort v is sorted for all vectors v with elem = Nat

-- Given a sorted vector (call it v) and an element (call it x) that is LTE the first element of v, proof that (x :: v) is sorted
total
addElemSorted : (x : Nat) -> (v : NatVect (S k)) -> (LTE x (Vect.index (FZ) v)) -> IsSorted (S k) v -> IsSorted (S (S k)) (x :: v)
addElemSorted x v pf1 pf2 FZ = reflLTE (Vect.index (FZ) (x :: v))
addElemSorted x v pf1 pf2 (FS FZ) = pf1
addElemSorted x v pf1 pf2 (FS (FS j)) = (pf2 (FS j))

-- mergeNatIsSorted : (v1 : Vect n Nat) -> (IsSorted n v1) -> (v2 : Vect m Nat) -> (IsSorted m v2) -> IsSorted (n + m) (mergeNat v1 v2)
-- mergeNatIsSorted {n = (S k)} {m = (S j)} (z :: xs) x (w :: ys) y = case (isLTE z w) of
--                                                                   (Yes pf) => addElemSorted z (mergeNat xs (w :: ys)) pf (mergeNatIsSorted xs x (w :: ys) y)
--                                                                   (No contra) => ?rhs