text:
module Web.Raw.File

import JS
import Web.Internal.FilePrim
import Web.Internal.Types

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

namespace Blob

  export
  new :  (0 _ : JSType t1)
      => {auto 0 _ : Elem BlobPropertyBag (Types t1)}
      -> (blobParts : Optional (Array (Union13 Int8Array
                                               Int16Array
                                               Int32Array
                                               UInt8Array
                                               UInt8Array
                                               UInt8Array
                                               UInt8ClampedArray
                                               Float32Array
                                               Float64Array
                                               DataView
                                               ArrayBuffer
                                               Blob
                                               String)))
      -> (options : Optional t1)
      -> JSIO Blob
  new a b = primJS $ Blob.prim__new (toFFI a) (optUp b)

  export
  new' : JSIO Blob
  new' = primJS $ Blob.prim__new undef undef

  export
  size :  (0 _ : JSType t1)
       => {auto 0 _ : Elem Blob (Types t1)}
       -> (obj : t1)
       -> JSIO JSBits64
  size a = primJS $ Blob.prim__size (up a)

  export
  type :  (0 _ : JSType t1)
       => {auto 0 _ : Elem Blob (Types t1)}
       -> (obj : t1)
       -> JSIO String
  type a = primJS $ Blob.prim__type (up a)

  export
  arrayBuffer :  (0 _ : JSType t1)
              => {auto 0 _ : Elem Blob (Types t1)}
              -> (obj : t1)
              -> JSIO (Promise ArrayBuffer)
  arrayBuffer a = primJS $ Blob.prim__arrayBuffer (up a)

  export
  slice :  (0 _ : JSType t1)
        => {auto 0 _ : Elem Blob (Types t1)}
        -> (obj : t1)
        -> (start : Optional JSInt64)
        -> (end : Optional JSInt64)
        -> (contentType : Optional String)
        -> JSIO Blob
  slice a b c d = primJS $ Blob.prim__slice (up a) (toFFI b) (toFFI c) (toFFI d)

  export
  slice' :  (0 _ : JSType t1)
         => {auto 0 _ : Elem Blob (Types t1)}
         -> (obj : t1)
         -> JSIO Blob
  slice' a = primJS $ Blob.prim__slice (up a) undef undef undef

  export
  stream :  (0 _ : JSType t1)
         => {auto 0 _ : Elem Blob (Types t1)}
         -> (obj : t1)
         -> JSIO ReadableStream
  stream a = primJS $ Blob.prim__stream (up a)

  export
  text :  (0 _ : JSType t1)
       => {auto 0 _ : Elem Blob (Types t1)}
       -> (obj : t1)
       -> JSIO (Promise String)
  text a = primJS $ Blob.prim__text (up a)

namespace File

  export
  new :  (0 _ : JSType t1)
      => {auto 0 _ : Elem FilePropertyBag (Types t1)}
      -> (fileBits : Array (Union13 Int8Array
                                    Int16Array
                                    Int32Array
                                    UInt8Array
                                    UInt8Array
                                    UInt8Array
                                    UInt8ClampedArray
                                    Float32Array
                                    Float64Array
                                    DataView
                                    ArrayBuffer
                                    Blob
                                    String))
      -> (fileName : String)
      -> (options : Optional t1)
      -> JSIO File
  new a b c = primJS $ File.prim__new a b (optUp c)

  export
  new' :  (fileBits : Array (Union13 Int8Array
                                     Int16Array
                                     Int32Array
                                     UInt8Array
                                     UInt8Array
                                     UInt8Array
                                     UInt8ClampedArray
                                     Float32Array
                                     Float64Array
                                     DataView
                                     ArrayBuffer
                                     Blob
                                     String))
       -> (fileName : String)
       -> JSIO File
  new' a b = primJS $ File.prim__new a b undef

  export
  lastModified : (obj : File) -> JSIO JSInt64
  lastModified a = primJS $ File.prim__lastModified a

  export
  name : (obj : File) -> JSIO String
  name a = primJS $ File.prim__name a

namespace FileList

  export
  length : (obj : FileList) -> JSIO Bits32
  length a = primJS $ FileList.prim__length a

  export
  item : (obj : FileList) -> (index : Bits32) -> JSIO (Maybe File)
  item a b = tryJS "FileList.item" $ FileList.prim__item a b

namespace FileReader

  public export
  DONE : Bits16
  DONE = 2

  public export
  EMPTY : Bits16
  EMPTY = 0

  public export
  LOADING : Bits16
  LOADING = 1

  export
  new : JSIO FileReader
  new = primJS $ FileReader.prim__new

  export
  error : (obj : FileReader) -> JSIO (Maybe DOMException)
  error a = tryJS "FileReader.error" $ FileReader.prim__error a

  export
  onabort : FileReader -> Attribute False Maybe EventHandlerNonNull
  onabort v = fromNullablePrim "FileReader.getonabort"
                               prim__onabort
                               prim__setOnabort
                               v

  export
  onerror : FileReader -> Attribute False Maybe EventHandlerNonNull
  onerror v = fromNullablePrim "FileReader.getonerror"
                               prim__onerror
                               prim__setOnerror
                               v

  export
  onload : FileReader -> Attribute False Maybe EventHandlerNonNull
  onload v = fromNullablePrim "FileReader.getonload"
                              prim__onload
                              prim__setOnload
                              v

  export
  onloadend : FileReader -> Attribute False Maybe EventHandlerNonNull
  onloadend v = fromNullablePrim "FileReader.getonloadend"
                                 prim__onloadend
                                 prim__setOnloadend
                                 v

  export
  onloadstart : FileReader -> Attribute False Maybe EventHandlerNonNull
  onloadstart v = fromNullablePrim "FileReader.getonloadstart"
                                   prim__onloadstart
                                   prim__setOnloadstart
                                   v

  export
  onprogress : FileReader -> Attribute False Maybe EventHandlerNonNull
  onprogress v = fromNullablePrim "FileReader.getonprogress"
                                  prim__onprogress
                                  prim__setOnprogress
                                  v

  export
  readyState : (obj : FileReader) -> JSIO Bits16
  readyState a = primJS $ FileReader.prim__readyState a

  export
  result : (obj : FileReader) -> JSIO (Maybe (Union2 String ArrayBuffer))
  result a = tryJS "FileReader.result" $ FileReader.prim__result a

  export
  abort : (obj : FileReader) -> JSIO ()
  abort a = primJS $ FileReader.prim__abort a

  export
  readAsArrayBuffer :  (0 _ : JSType t1)
                    => {auto 0 _ : Elem Blob (Types t1)}
                    -> (obj : FileReader)
                    -> (blob : t1)
                    -> JSIO ()
  readAsArrayBuffer a b = primJS $ FileReader.prim__readAsArrayBuffer a (up b)

  export
  readAsBinaryString :  (0 _ : JSType t1)
                     => {auto 0 _ : Elem Blob (Types t1)}
                     -> (obj : FileReader)
                     -> (blob : t1)
                     -> JSIO ()
  readAsBinaryString a b = primJS $ FileReader.prim__readAsBinaryString a (up b)

  export
  readAsDataURL :  (0 _ : JSType t1)
                => {auto 0 _ : Elem Blob (Types t1)}
                -> (obj : FileReader)
                -> (blob : t1)
                -> JSIO ()
  readAsDataURL a b = primJS $ FileReader.prim__readAsDataURL a (up b)

  export
  readAsText :  (0 _ : JSType t1)
             => {auto 0 _ : Elem Blob (Types t1)}
             -> (obj : FileReader)
             -> (blob : t1)
             -> (encoding : Optional String)
             -> JSIO ()
  readAsText a b c = primJS $ FileReader.prim__readAsText a (up b) (toFFI c)

  export
  readAsText' :  (0 _ : JSType t1)
              => {auto 0 _ : Elem Blob (Types t1)}
              -> (obj : FileReader)
              -> (blob : t1)
              -> JSIO ()
  readAsText' a b = primJS $ FileReader.prim__readAsText a (up b) undef

namespace FileReaderSync

  export
  new : JSIO FileReaderSync
  new = primJS $ FileReaderSync.prim__new

  export
  readAsArrayBuffer :  (0 _ : JSType t1)
                    => {auto 0 _ : Elem Blob (Types t1)}
                    -> (obj : FileReaderSync)
                    -> (blob : t1)
                    -> JSIO ArrayBuffer
  readAsArrayBuffer a b = primJS
                        $ FileReaderSync.prim__readAsArrayBuffer a (up b)

  export
  readAsBinaryString :  (0 _ : JSType t1)
                     => {auto 0 _ : Elem Blob (Types t1)}
                     -> (obj : FileReaderSync)
                     -> (blob : t1)
                     -> JSIO String
  readAsBinaryString a b = primJS
                         $ FileReaderSync.prim__readAsBinaryString a (up b)

  export
  readAsDataURL :  (0 _ : JSType t1)
                => {auto 0 _ : Elem Blob (Types t1)}
                -> (obj : FileReaderSync)
                -> (blob : t1)
                -> JSIO String
  readAsDataURL a b = primJS $ FileReaderSync.prim__readAsDataURL a (up b)

  export
  readAsText :  (0 _ : JSType t1)
             => {auto 0 _ : Elem Blob (Types t1)}
             -> (obj : FileReaderSync)
             -> (blob : t1)
             -> (encoding : Optional String)
             -> JSIO String
  readAsText a b c = primJS $ FileReaderSync.prim__readAsText a (up b) (toFFI c)

  export
  readAsText' :  (0 _ : JSType t1)
              => {auto 0 _ : Elem Blob (Types t1)}
              -> (obj : FileReaderSync)
              -> (blob : t1)
              -> JSIO String
  readAsText' a b = primJS $ FileReaderSync.prim__readAsText a (up b) undef

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

namespace BlobPropertyBag

  export
  new :  (type : Optional String)
      -> (endings : Optional EndingType)
      -> JSIO BlobPropertyBag
  new a b = primJS $ BlobPropertyBag.prim__new (toFFI a) (toFFI b)

  export
  new' : JSIO BlobPropertyBag
  new' = primJS $ BlobPropertyBag.prim__new undef undef

  export
  endings :  (0 _ : JSType t)
          => {auto 0 _ : Elem BlobPropertyBag (Types t)}
          -> t
          -> Attribute False Optional EndingType
  endings v = fromUndefOrPrimNoDefault "BlobPropertyBag.getendings"
                                       prim__endings
                                       prim__setEndings
                                       (v :> BlobPropertyBag)

  export
  type :  (0 _ : JSType t)
       => {auto 0 _ : Elem BlobPropertyBag (Types t)}
       -> t
       -> Attribute True Optional String
  type v = fromUndefOrPrim "BlobPropertyBag.gettype"
                           prim__type
                           prim__setType
                           ""
                           (v :> BlobPropertyBag)

namespace FilePropertyBag

  export
  new : (lastModified : Optional JSInt64) -> JSIO FilePropertyBag
  new a = primJS $ FilePropertyBag.prim__new (toFFI a)

  export
  new' : JSIO FilePropertyBag
  new' = primJS $ FilePropertyBag.prim__new undef

  export
  lastModified :  (0 _ : JSType t)
               => {auto 0 _ : Elem FilePropertyBag (Types t)}
               -> t
               -> Attribute False Optional JSInt64
  lastModified v = fromUndefOrPrimNoDefault "FilePropertyBag.getlastModified"
                                            prim__lastModified
                                            prim__setLastModified
                                            (v :> FilePropertyBag)


text:
module Data.List.Extra

||| Find the first element of a list that satisfies a predicate, or `Nothing` if none do.
|||
||| Renamed to `find'` because Idris2 gets confused between Vect find and List find
public export
find' : (a -> Bool) -> List a -> Maybe a
find' p []      = Nothing
find' p (x::xs) =
  if p x then
    Just x
  else
    find' p xs

ext: idr

max_stars_repo_name: steshaw/hsgames

max_issues_repo_name: steshaw/hsgames

max_forks_repo_name: steshaw/hsgames


text:
module Language.LSP.Message.Markup

import Language.JSON
import Language.LSP.Message.Derive
import Language.LSP.Message.Utils
import Language.Reflection

%language ElabReflection
%default total

namespace MarkupKind
  ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#markupContent
  public export
  data MarkupKind = PlainText | Markdown

export
ToJSON MarkupKind where
  toJSON PlainText = JString "plaintext"
  toJSON Markdown  = JString "markdown"

export
FromJSON MarkupKind where
  fromJSON (JString "plaintext") = pure PlainText
  fromJSON (JString "markdown")  = pure Markdown
  fromJSON _ = neutral

||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#markupContent
public export
record MarkupContent where
  constructor MkMarkupContent
  kind : MarkupKind
  value : String
%runElab deriveJSON defaultOpts `{{MarkupContent}}

namespace MarkedString
  ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_hover
  public export
  record MarkedStringWithLanguage where
    constructor MkMarkedStringWithLanguage
    language : String
    value : String
  %runElab deriveJSON defaultOpts `{{MarkedStringWithLanguage}}

||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_hover
public export
MarkedString : Type
MarkedString = OneOf [String, MarkedStringWithLanguage]

||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#markupContent
public export
record MarkdownClientCapabilities where
  constructor MkMarkdownClientCapabilities
  parser  : String
  version : Maybe String
%runElab deriveJSON defaultOpts `{{MarkdownClientCapabilities}}


text:
module Data.Precision

import Data.Fin
import Data.List
import Data.Vect

-- TODO: this needs to be accessible (maybe from Data.Nat?)
private
greaterNat : Nat -> Nat -> Nat
greaterNat k j with (compare k j)
  greaterNat k j | LT = j
  greaterNat k j | EQ = k
  greaterNat k j | GT = k

-- Can construct all x with:
--   b > x >= 1
export
data Coefficient : (b : Nat) -> (n : Nat) -> Type where
  Coeff : (Fin (S b)) -> -- 0 - (b - 1) => 1 - b
          Vect n (Fin (S (S b))) ->
          Coefficient (S (S b)) n

export
Show (Coefficient 10 n) where
  show (Coeff x xs) =
    show (finToNat (weaken x)) ++ "." ++ concat (show . finToNat <$> xs)

private
eqDigits : Vect n (Fin (S (S b))) -> Vect m (Fin (S (S b))) -> Bool
eqDigits [] ys = all (== 0) ys
eqDigits xs [] = all (== 0) xs
eqDigits (x :: xs) (y :: ys) = x == y && eqDigits xs ys

private
eqCoeffs : Coefficient b n -> Coefficient b m -> Bool
eqCoeffs (Coeff x xs) (Coeff y ys) = x == y && eqDigits xs ys

private
compareDigits : Vect n (Fin (S (S b))) -> Vect m (Fin (S (S b))) -> Ordering
compareDigits [] ys =
  if all (== 0) ys
     then EQ
     else LT
compareDigits xs [] =
  if all (== 0) xs
     then EQ
     else GT
compareDigits (x :: xs) (y :: ys) =
  case compare x y of
       LT => LT
       EQ => compareDigits xs ys
       GT => GT

export
compareCoeffs : Coefficient b n -> Coefficient b m -> Ordering
compareCoeffs (Coeff x xs) (Coeff y ys) =
  case compare x y of
       LT => LT
       EQ => compareDigits xs ys
       GT => GT

private
plusCoeffs : Coefficient b n -> Coefficient b m -> (Coefficient b (greaterNat n m), Bool)

||| Can construct all x with:
|||   x > 0
public export
data Precision : (b : Nat) -> (n : Nat) -> Type where
  Prec : Coefficient b n -> Integer -> Precision b n

export
Show (Precision 10 n) where
  show (Prec coeff expon) = show coeff ++ "e" ++ show expon

-- TODO: export?
export
eqPrecs : Precision b n -> Precision b m -> Bool
eqPrecs (Prec coeff expon) (Prec coeff' expon') = expon == expon' && eqCoeffs coeff coeff'

-- TODO: export?
export
comparePrecs : Precision b n -> Precision b m -> Ordering
comparePrecs (Prec coeff expon) (Prec coeff' expon') =
  case compare expon expon' of
       LT => LT
       EQ => compareCoeffs coeff coeff'
       GT => GT

export
plusPrecs : Precision b n -> Precision b m -> Precision b (greaterNat n m)
plusPrecs (Prec x expon) (Prec y expon') with (compare expon expon')
  plusPrecs (Prec x expon) (Prec y expon') | LT = ?plusPrecs_rhs_1
  plusPrecs (Prec x expon) (Prec y expon') | EQ with (plusCoeffs x y)
    plusPrecs (Prec x expon) (Prec y expon') | EQ | (coeff, overhead) =
      Prec coeff $ if overhead
                      then expon + 1
                      else expon
  plusPrecs (Prec x expon) (Prec y expon') | GT = ?plusPrecs_rhs_3

export
multPrecs : Precision b n -> Precision b m -> Precision b (greaterNat n m)


text:
module Typing.TypeChecking

import Typing.Common
import Typing.Util
import Typing.Unification

export
inferify : Term -> TypeChecker Inferred
export
checkify : Term -> Term -> TypeChecker Term

export
checkifyCaseMotive : CaseMotive -> TypeChecker CaseMotive
export
checkifyPattern : Pattern -> Term -> TypeChecker (Pattern >< Term)
export
checkifyClause : Clause -> CaseMotive -> TypeChecker Clause
export
checkifyClauses : List Clause -> CaseMotive -> TypeChecker (List Clause)

-- Y8Y 8o  0 8YYYY 8YYYY 8YYYo Y8Y 8YYYY 0   0
--  0  8Yo 8 8___  8___  8___P  0  8___  "o o"
--  0  8 Yo8 8"""  8"""  8""Yo  0  8"""    0
-- o8o 0   8 0     8oooo 0   0 o8o 0       0

--         8_   _8 8YYYY YY8YY  o8o
-- ____    8"o_o"8 8___    0   8   8
-- """"    0  8  0 8"""    0   8YYY8
--         0     0 8oooo   0   0   0

inferify (Meta i) = throw $ "The metavariable " ++ show (Meta i)
	++ " appears in checkable code, when it should not."

--         0   0  o8o  8YYYo
-- ____    0   0 8   8 8___P
-- """"    "o o" 8YYY8 8""Yo
--          "8"  0   0 0   0

inferify (Var (Name x0)) = do
	((m,x),t) <- typeInDefinitions x0
	pure $ AbsoluteDottedVar m x <:> t

inferify (Var (Generated x i)) = do
	t <- typeInContext i
	pure $ Var (Generated x i) <:> t

inferify (DottedVar m x) = do
	((m',x'),t) <- dottedTypeInDefinitions m x
	pure $ AbsoluteDottedVar m' x' <:> t

inferify (AbsoluteDottedVar m x) = do
	((m',x'),t) <- absoluteDottedTypeInDefinitions m x
	pure $ AbsoluteDottedVar m' x'<:> t

--          o8o  8o  0 8o  0
-- ____    8   8 8Yo 8 8Yo 8
-- """"    8YYY8 8 Yo8 8 Yo8
--         0   0 0   8 0   8

inferify (Ann m t) = do
	t' <- checkify t Star
	et' <- evaluate t'
	m' <- checkify m et'
	subs <- substitution
	pure $ instantiateMetas subs m' <:> instantiateMetas subs et'

--         oYYYo YY8YY  o8o  8YYYo
-- ____    %___    0   8   8 8___P
-- """"    `"""p   0   8YYY8 8""Yo
--         YoooY   0   0   0 0   0

inferify Star = pure $ Star <:> Star

--         8YYYo Y8Y
-- ____    8___P  0
-- """"    8"""   0
--         0     o8o

inferify (Pi plic arg sc) = do
	arg' <- checkify arg Star
	i <- newName
	case head' (names sc) of
		Nothing => throw "Should not happen"
		Just hsc => do
			ret' <- extendContext [(i, hsc, arg')] $ checkify (instantiate sc [Var (Generated hsc i)]) Star
			let sc' = the (Scope Term Term) $ NewScope (names sc) (abstractOver [i] ret')
			subs <- substitution
			pure $ instantiateMetas subs (Pi plic arg' sc') <:> Star

--         0     o8o  8_   _8
-- ____    0    8   8 8"o_o"8
-- """"    0    8YYY8 0  8  0
--         8ooo 0   0 0     0

inferify (Lam _ _) = throw "Cannot infer the type of a lambda expression."

--          o8o  8YYYo 8YYYo
-- ____    8   8 8___P 8___P
-- """"    8YYY8 8"""  8"""
--         0   0 0     0

inferify (App plic f a) = do
	(f0 <:> t0) <- inferify f
	et0 <- evaluate t0
	(app' <:> t') <- insertImplicits f0 plic et0
	subs <- substitution
	pure $ instantiateMetas subs app' <:> instantiateMetas subs t'
where
	insertImplicits : Term -> Plict -> Term -> TypeChecker Inferred
	insertImplicits f' Expl (Pi Expl arg sc) = do
		earg <- evaluate arg
		a' <- checkify a earg
		pure $ App Expl f' a' <:> instantiate sc [a']
	insertImplicits f' Impl (Pi Impl arg sc) = do
		earg <- evaluate arg
		a' <- checkify a earg
		pure $ App Impl f' a' <:> instantiate sc [a']
	insertImplicits f' Expl (Pi Impl _ sc) = do
		meta <- newMetaVar
		let impla = Meta meta
		let newF' = App Impl f' impla
		newT' <- evaluate (instantiate sc [impla])
		insertImplicits newF' Expl newT'
	insertImplicits _ Impl (Pi Expl _ _)
		= throw $ "Expected an explicit argument but found an implicit argument "
					++ "when applying " ++ show f ++ " to " ++ show a ++ " in "
					++ "the expression " ++ show (App plic f a)
	insertImplicits _ _ t
		= throw $ "Cannot insert implicit arguments for non-function type " ++ show t

--          oYYo _YYY_ 8o  0
-- ____    0   " 0   0 8Yo 8
-- """"    0   , 0   0 8 Yo8
--          YooY "ooo" 0   8

inferify (Con c as) = do
	(unaliasedC,consig) <- typeInSignature c
	(as' <:> ret) <- inferifyConArgs consig as consig
	subs <- substitution
	pure $ instantiateMetas subs (Con unaliasedC as') <:> instantiateMetas subs ret
where
	inferifyConArgs : ConSig Term ->
		List (Plict >< Term) ->
		ConSig Term ->
		TypeChecker (InferredF (List (Plict >< Term)) Term)

	inferifyConArgs _ [] (ConSigNil ret) = pure $ [] <:> ret

	inferifyConArgs consig ((Expl, m) :: ms) (ConSigCons Expl arg sc) = do
		subs <- substitution
		earg <- evaluate (instantiateMetas subs arg)
		m' <- checkify m earg
		(ms' <:> ret) <- inferifyConArgs consig ms (instantiate sc [m])
		pure $ ((Expl,m') :: ms') <:> ret

	inferifyConArgs consig ((Impl, m) :: ms) (ConSigCons Impl arg sc) = do
		subs <- substitution
		earg <- evaluate (instantiateMetas subs arg)
		m' <- checkify m earg
		(ms' <:> ret) <- inferifyConArgs consig ms (instantiate sc [m])
		pure $ ((Impl,m') :: ms') <:> ret

	inferifyConArgs consig ms (ConSigCons Impl _ sc) = do
		meta <- newMetaVar
		let implm = Meta meta
		(ms' <:> ret) <- inferifyConArgs consig ms (instantiate sc [implm])
		pure $ ((Impl,implm) :: ms') <:> ret

	inferifyConArgs consig ((Impl,_) :: _) (ConSigCons Expl _ _)
		= throw $ "Expected an explicit argument but found an implicit argument "
					++ "when checking " ++ show (Con c as)
					++ " matches the signature " ++ showConSig (Var . Name) consig

	inferifyConArgs consig _ _ = do
		let las = length as
		let lsig = conSigLength (Var . Name) consig
		throw $ show c ++ " expects " ++ show lsig ++ " "
				++ (if lsig == 1 then "arg" else "args")
				++ " but was given " ++ show las

--          oYYo  o8o  oYYYo 8YYYY
-- ____    0   " 8   8 %___  8___
-- """"    0   , 8YYY8 `"""p 8"""
--          YooY 0   0 YoooY 8oooo

inferify (Case ms0 mot cs) = do
	mot' <- checkifyCaseMotive mot
	ms0' <- checkifyCaseArgs ms0 mot'
	cs' <- checkifyClauses cs mot'
	ret <- auxMotive ms0' mot'
	subs <- substitution
	pure $ instantiateMetas subs (Case ms0' mot' cs') <:> instantiateMetas subs ret
where
	checkifyCaseArgs : List Term -> CaseMotive -> TypeChecker (List Term)
	checkifyCaseArgs [] (CaseMotiveNil _) = pure []
	checkifyCaseArgs (m :: ms) (CaseMotiveCons a sc) = do
		ea <- evaluate a
		m' <- checkify m ea
		ms' <- checkifyCaseArgs ms (instantiate sc [m])
		pure $ (m' :: ms')
	checkifyCaseArgs _ _ = do
		let lms = length ms0
		let lmot = caseMotiveLength mot
		throw $ "Motive " ++ show mot ++ " expects " ++ show lmot ++ " case "
					++ (if lmot == 1 then "arg" else "args")
					++ " but was given " ++ show lms

	auxMotive : List Term -> CaseMotive -> TypeChecker Term
	auxMotive [] (CaseMotiveNil a) = pure a
	auxMotive (m :: ms) (CaseMotiveCons _ sc) = auxMotive ms (instantiate sc [m])
	auxMotive _ _ = do
		let lms = length ms0
		let lmot = caseMotiveLength mot
		throw $ "Motive " ++ show mot ++ " expects " ++ show lmot ++ " case "
					++ (if lmot == 1 then "arg" else "args")
					++ " but was given " ++ show lms

--         8YYYo 8YYYY  oYYo _YYY_ 8YYYo 8888_ YY8YY 0   0 8YYYo 8YYYY
-- ____    8___P 8___  0   " 0   0 8___P 0   0   0   "o o" 8___P 8___
-- """"    8""Yo 8"""  0   , 0   0 8""Yo 0   0   0     0   8"""  8"""
--         0   0 8oooo  YooY "ooo" 0   0 8oooY   0     0   0     8oooo

inferify (RecordType tele) = do
	tele' <- checkifyTelescope tele
	pure $ RecordType tele' <:> Star
where
	checkifyTelescope : Telescope -> TypeChecker Telescope
	checkifyTelescope TelescopeNil = pure TelescopeNil
	checkifyTelescope (TelescopeCons t sc) = do
		t' <- checkify t Star
		i <- newName
		case head' (names sc) of
			Nothing => throw "Should not happen"
			Just hsc => do
				m' <- extendContext [(i, hsc, t')]
					$ checkifyTelescope (instantiate sc [Var (Generated hsc i)])
				pure $ TelescopeCons t' (NewScope (names sc) (abstractOver [i] m'))

--         8YYYo 8YYYY  oYYo _YYY_ 8YYYo 8888_  oYYo _YYY_ 8o  0
-- ____    8___P 8___  0   " 0   0 8___P 0   0 0   " 0   0 8Yo 8
-- """"    8""Yo 8"""  0   , 0   0 8""Yo 0   0 0   , 0   0 8 Yo8
--         0   0 8oooo  YooY "ooo" 0   0 8oooY  YooY "ooo" 0   8

inferify (RecordCon _) = throw "Cannot infer the type of a record expression."

--         8YYYo 8YYYY  oYYo _YYY_ 8YYYo 8888_ 8888_ _YYY_ YY8YY
-- ____    8___P 8___  0   " 0   0 8___P 0   0 0   0 0   0   0
-- """"    8""Yo 8"""  0   , 0   0 8""Yo 0   0 0   0 0   0   0
--         0   0 8oooo  YooY "ooo" 0   0 8oooY 8oooY "ooo"   0

inferify (Project m x) = do
	(m' <:> t) <- inferify m
	et <- evaluate t
	case et of
		RecordType tele => case lookupField m' x tele of
			Nothing => throw $ "Missing field " ++ x
			Just t' => pure $ Project m' x <:> t'
		t' => throw $ "Expecting a record type but found " ++ show t'
where
	lookupField : Term -> String -> Telescope -> Maybe Term
	lookupField _ _ TelescopeNil = Nothing
	lookupField m' f (TelescopeCons t sc) with (head' $ names sc)
		| Nothing = Nothing
		| Just (hsc) with (f == hsc)
			| True = Just t
			| _    = lookupField m' f $ instantiate sc [Project m' hsc]

--  oYYo 0   0 8YYYY  oYYo 0  oY Y8Y 8YYYY 0   0
-- 0   " 8___8 8___  0   " 8_oY   0  8___  "o o"
-- 0   , 8"""8 8"""  0   , 8"Yo   0  8"""    0
--  YooY 0   0 8oooo  YooY 0  Yo o8o 0       0

--         8_   _8 8YYYY YY8YY  o8o
-- ____    8"o_o"8 8___    0   8   8
-- """"    0  8  0 8"""    0   8YYY8
--         0     0 8oooo   0   0   0

checkify (Meta i) _ = throw $ "The metavariable " ++ show (Meta i)
						++ " appears in checkable code, when it should not."

--         0     o8o  8_   _8          8YYYo Y8Y
-- ____    0    8   8 8"o_o"8    88    8___P  0
-- """"    0    8YYY8 0  8  0          8"""   0
--         8ooo 0   0 0     0    88    0     o8o

checkify (Lam plic sc) t = do
	et <- evaluate t
	case (head' (names sc), plic, et) of
		(Just hsc, Expl, Pi Expl arg sc') => do-- \x -> M : (x : A) -> B
			i <- newName
			eret <- evaluate (instantiate sc' [Var (Generated hsc i)])
			m' <- extendContext [(i, hsc, arg)] $ checkify (instantiate sc [Var (Generated hsc i)]) eret
			subs <- substitution
			pure $ instantiateMetas subs (Lam Expl (NewScope (names sc) (abstractOver [i] m')))
		(Just hsc, Impl, Pi Impl arg sc') => do -- \{y} -> M : {y : A} -> B
			i <- newName
			eret <- evaluate (instantiate sc' [Var (Generated hsc i)])
			m' <- extendContext [(i, hsc, arg)] $ checkify (instantiate sc [Var (Generated hsc i)]) eret
			subs <- substitution
			pure $ instantiateMetas subs (Lam Impl (NewScope (names sc) (abstractOver [i] m')))
		(Just hsc, Expl, Pi Impl arg sc') => do -- \x -> M : {y : A} -> B
			i <- newName
			eret <- evaluate (instantiate sc' [Var (Generated hsc i)])
			f' <- extendContext [(i, hsc, arg)] $ checkify (Lam Expl sc) eret
			subs <- substitution
			pure $ instantiateMetas subs (Lam Impl (NewScope ["_"] (abstractOver (the (List String) []) f')))
		(Just hsc, Impl, Pi Expl _ _) => -- \{y} -> M : (x : A) -> B
			throw $ "Expected an explicit argument but found an implicit argument "
				++ "when checking " ++ show (Lam plic sc)
				++ " matches the signature " ++ show t
		_ => throw $ "Cannot check term: " ++ show (Lam plic sc) ++ "\n"
			++ "Against non-function type: " ++ show t

--          oYYo _YYY_ 8o  0          YY8YY
-- ____    0   " 0   0 8Yo 8    88      0
-- """"    0   , 0   0 8 Yo8            0
--          YooY "ooo" 0   8    88      0

checkify (Con c as) t = do
	(unaliasedC,consig) <- typeInSignature c
	(ats, ret) <- dropConArgs as consig
	unify t ret
	as' <- traverse checkifyConArg ats
	subs <- substitution
	pure $ instantiateMetas subs (Con unaliasedC as')
where
	dropConArgs : List (Plict >< Term) -> ConSig Term ->
		TypeChecker (List ((Plict >< Term) \/ (Plict >< Term >< Term)) >< Term)

	dropConArgs [] (ConSigNil ret) = pure ([], ret)
	dropConArgs ((Expl,m) :: ms) (ConSigCons Expl arg sc) = do
		(ats,ret) <- dropConArgs ms (instantiate sc [m])
		pure (Right (Expl,m,arg) :: ats, ret)
	dropConArgs ((Impl,m) :: ms) (ConSigCons Impl arg sc) = do
		(ats,ret) <- dropConArgs ms (instantiate sc [m])
		pure (Right (Impl,m,arg) :: ats, ret)
	dropConArgs ms (ConSigCons Impl _ sc) = do
		meta <- newMetaVar
		let x = Meta meta
		(ats, ret) <- dropConArgs ms (instantiate sc [x])
		pure (Left (Impl,x) :: ats,ret)
	dropConArgs ((Impl,_) :: _) (ConSigCons Expl _ _)
		= throw $ "Mismatching plicits when checking " ++ show (Con c as)
					++ " has type " ++ show t
	dropConArgs _ _
		= throw $ "Mismatching number of arguments when checking " ++ show (Con c as)
					++ " has type " ++ show t

	checkifyConArg : (Plict >< Term) \/ (Plict >< Term >< Term) -> TypeChecker (Plict >< Term)
	checkifyConArg (Left pm) = pure pm
	checkifyConArg (Right (plic, m, arg)) = do
		subs <- substitution
		earg <- evaluate (instantiateMetas subs arg)
		m' <- checkify m earg
		pure (plic,m')

--         8YYYo 8YYYY  oYYo _YYY_ 8YYYo 8888_
-- ____    8___P 8___  0   " 0   0 8___P 0   0
-- """"    8""Yo 8"""  0   , 0   0 8""Yo 0   0
--         0   0 8oooo  YooY "ooo" 0   0 8oooY

checkify (RecordCon fields) t = case t of
	RecordType tele => do
		fields' <- checkifyFields fields tele
		pure $ RecordCon fields'
	_ => throw $ "Cannot check a record against type " ++ show t
where
	checkifyFields : List (String >< Term) -> Telescope -> TypeChecker (List (String >< Term))
	checkifyFields [] TelescopeNil = pure []
	checkifyFields [] (TelescopeCons _ sc) = throw $ "Missing record field " ++ unwords (names sc)
	checkifyFields _ TelescopeNil = throw $ "Mismatching number of record fields."
	checkifyFields xs (TelescopeCons t' sc) with (head' (names sc))
		| Nothing = throw "Incorrect record field."
		| Just hsc with (extract (\(x',_) => x' == hsc) xs)
			| Nothing = throw $ "Missing record field " ++ unwords (names sc)
			| Just ((x',m),xs') = do
				et' <- evaluate t'
				m' <- checkify m et'
				fields' <- checkifyFields xs' (instantiate sc [m'])
				pure $ (x',m') :: fields'

--          oYYo 8YYYY 8o  0 8YYYY 8YYYo  o8o  0
-- ____    0  __ 8___  8Yo 8 8___  8___P 8   8 0
-- """"    0  "8 8"""  8 Yo8 8"""  8""Yo 8YYY8 0
--          YooY 8oooo 0   8 8oooo 0   0 0   0 8ooo

checkify m t = do
	(m' <:> t') <- inferify m
	et <- evaluate t
	et' <- evaluate t'
	m'' <- subtype m' et' et
	subs <- substitution
	pure $ instantiateMetas subs m''
where
	subtype : Term -> Term -> Term -> TypeChecker Term
	subtype m (Pi Expl a sc) (Pi Expl a' sc') = do
		unify a a'
		subs <- substitution
		i <- newName
		case (head' $ names sc) of
			Just hsc => do
				let b = instantiateMetas subs (instantiate sc [Var (Generated hsc i)])
				let b' = instantiateMetas subs (instantiate sc' [Var (Generated hsc i)])
				subtype m b b'
			Nothing => throw "Should not happen"
	subtype m (Pi Expl a sc) (Pi Impl a' sc')
		= throw $ "The type " ++ show (Pi Expl a sc)
			++ " is not a subtype of " ++ show (Pi Impl a' sc')
	subtype m (Pi Impl a sc) (Pi Expl a' sc') = do
		i <- newMetaVar
		subs <- substitution
		let b = instantiate sc [Meta i]
		subtype (App Impl m (Meta i)) b (Pi Expl a' sc')
	subtype m (Pi Impl a sc) (Pi Impl a' sc') = do
		unify a a'
		i <- newName
		subs <- substitution
		case (head' $ names sc) of
			Just hsc => do
				let b = instantiateMetas subs (instantiate sc [Var (Generated hsc i)])
				let b' = instantiateMetas subs (instantiate sc' [Var (Generated hsc i)])
				subtype m b b'
			Nothing => throw "Should not happen"
	subtype m t t' = do
		unify t t'
		pure m

--  oYYo 0   0 8YYYY  oYYo 0  oY Y8Y 8YYYY 0   0  oYYo  o8o  oYYYo 8YYYY 8_   _8 _YYY_ YY8YY Y8Y 0   0 8YYYY
-- 0   " 8___8 8___  0   " 8_oY   0  8___  "o o" 0   " 8   8 %___  8___  8"o_o"8 0   0   0    0  0   0 8___
-- 0   , 8"""8 8"""  0   , 8"Yo   0  8"""    0   0   , 8YYY8 `"""p 8"""  0  8  0 0   0   0    0  "o o" 8"""
--  YooY 0   0 8oooo  YooY 0  Yo o8o 0       0    YooY 0   0 YoooY 8oooo 0     0 "ooo"   0   o8o  "8"  8oooo

checkifyCaseMotive (CaseMotiveNil a) = do
	a' <- checkify a Star
	pure $ CaseMotiveNil a'
checkifyCaseMotive (CaseMotiveCons a sc) with (head' $ names sc)
	| Just hsc = do
		a' <- checkify a Star
		i <- newName
		b' <- extendContext [(i, hsc, a')]
				$ checkifyCaseMotive (instantiate sc [Var (Generated hsc i)])
		subs <- substitution
		pure $ instantiateMetasCaseMotive subs
			$ CaseMotiveCons a' $ NewScope (names sc) (abstractOver [i] b')
	| Nothing = throw "Should not happen"

--  oYYo 0   0 8YYYY  oYYo 0  oY Y8Y 8YYYY 0   0 8YYYo  o8o  YY8YY YY8YY 8YYYY 8YYYo 8o  0
-- 0   " 8___8 8___  0   " 8_oY   0  8___  "o o" 8___P 8   8   0     0   8___  8___P 8Yo 8
-- 0   , 8"""8 8"""  0   , 8"Yo   0  8"""    0   8"""  8YYY8   0     0   8"""  8""Yo 8 Yo8
--  YooY 0   0 8oooo  YooY 0  Yo o8o 0       0   0     0   0   0     0   8oooo 0   0 0   8

checkifyPattern (VarPat (Name x)) _ = pure (VarPat (Name x), Var (Name x))
checkifyPattern (VarPat (Generated x i)) t = do
	t' <- typeInContext i
	unify t t'
	pure (VarPat (Generated x i), Var (Generated x i))
checkifyPattern (ConPat _ _) Star = throw "Cannot pattern match on a type."
checkifyPattern (ConPat c ps0) t = do
	(unaliasedC,sig) <- typeInSignature c
	(ps',xs,ret) <- checkifyPatConArgs sig ps0 sig
	subs <- substitution
	et <- evaluate (instantiateMetas subs t)
	eret <- evaluate (instantiateMetas subs ret)
	unify et eret
	subs' <- substitution
	pure (instantiateMetasPat subs' (ConPat unaliasedC ps'), instantiateMetas subs' (Con unaliasedC xs))
where
	checkifyPatConArgs : ConSig Term -> List (Plict >< Pattern) ->
		ConSig Term -> TypeChecker (List (Plict >< Pattern) >< List (Plict >< Term) >< Term)
	checkifyPatConArgs _ [] (ConSigNil ret) = pure ([],[],ret)
	checkifyPatConArgs consig ((Expl,p) :: ps) (ConSigCons Expl arg sc') = do
		earg <- evaluate arg
		(p',x) <- checkifyPattern p earg
		(ps', xs, ret) <- checkifyPatConArgs consig ps (instantiate sc' [x])
		pure ((Expl,p') :: ps', (Expl,x) :: xs, ret)
	checkifyPatConArgs consig ((Impl,p) :: ps) (ConSigCons Impl arg sc') = do
		earg <- evaluate arg
		(p',x) <- checkifyPattern p earg
		(ps',xs,ret) <- checkifyPatConArgs consig ps (instantiate sc' [x])
		pure ((Impl,p') :: ps', (Impl,x) :: xs, ret)
	checkifyPatConArgs consig ps (ConSigCons Impl _ sc') = do
		meta <- newMetaVar
		let x = Meta meta
		(ps',xs,ret) <- checkifyPatConArgs consig ps (instantiate sc' [x])
		pure ((Impl,AssertionPat x) :: ps', (Impl,x) :: xs, ret)
	checkifyPatConArgs consig ((Impl,_) :: _) (ConSigCons Expl _ _)
		= throw $ "Expected an explicit argument but found an implicit argument "
					++ "when checking " ++ show (ConPat c ps0)
					++ " matches the signature " ++ showConSig (Var . Name) consig
	checkifyPatConArgs consig _ _ = do
		let lps = length ps0
		let lsig = conSigLength (Var . Name) consig
		throw $ show c ++ " expects " ++ show lsig ++ " case "
				++ (if lsig == 1 then "arg" else "args")
				++ " but was given " ++ show lps
checkifyPattern (AssertionPat m) t = do
	m' <- checkify m t
	subs <- substitution
	let m'' = instantiateMetas subs m'
	pure (AssertionPat m'', m'')
checkifyPattern MakeMeta _ = throw $ show MakeMeta ++ " should not appear in a checkable pattern."

--  oYYo 0   0 8YYYY  oYYo 0  oY Y8Y 8YYYY 0   0  oYYo 0     o8o  0   0 oYYYo 8YYYY
-- 0   " 8___8 8___  0   " 8_oY   0  8___  "o o" 0   " 0    8   8 0   0 %___  8___
-- 0   , 8"""8 8"""  0   , 8"Yo   0  8"""    0   0   , 0    8YYY8 0   0 `"""p 8"""
--  YooY 0   0 8oooo  YooY 0  Yo o8o 0       0    YooY 8ooo 0   0 "ooo" YoooY 8oooo

checkifyClause (NewClause psc sc0) motive = do
	ctx <- Traversable.for (names psc) $ \x => do
		i <- newName
		m <- newMetaVar
		pure (i, x, Meta m)
	let is = [ i | (i,_,_) <- ctx ]
	let xs1 = zipWith Generated (names psc) is
	let xs2 = map Var (removeByDummies (names psc) xs1)
	extendContext ctx $ do
		let ps = instantiate psc xs1
		(ps',ret) <- checkPatternsMotive ps motive
		subs <- substitution
		eret <- evaluate (instantiateMetas subs ret)
		m' <- checkify (instantiate sc0 xs2) eret
		subs' <- substitution
		let ps'' = map (instantiateMetasPat subs') ps'
		let psWithMsToBind = [ p | (MakeMeta, AssertionPat p) <- zip ps ps'' ]
		let msToBind = nub (psWithMsToBind >>= metas)
		newSubs <- Traversable.for msToBind $ \m => do
			i <- newName
			pure (m, Var (Generated ("_" ++ show i) i))
		addSubstitutions newSubs
		subs'' <- substitution
		let newPs = bindersByNewMetas ps (map (instantiateMetasPat subs'') ps'')
		let newVars = newPs >>= patternVars
		let (newNames, newIs) = unzip $ the (List $ String >< Int) $ do
			Generated x i <- newVars | _ => []
			pure (x, i)
		let newM = instantiateMetas subs'' m'
		pure $ NewClause (NewScope newNames (abstractOver newIs newPs))
			$ NewScope (removeByDummies newNames newNames)
				$ abstractOver (removeByDummies newNames newIs) newM
where
	bindersByNewMetas : List Pattern -> List Pattern -> List Pattern
	bindersByNewMetas [] [] = []
	bindersByNewMetas (MakeMeta :: guides) (AssertionPat x :: ps)
		= termToPattern x :: bindersByNewMetas guides ps
	bindersByNewMetas (_ :: guides) (p :: ps) = p :: bindersByNewMetas guides ps

	checkPatternsMotive : List Pattern -> CaseMotive -> TypeChecker (List Pattern >< Term)
	checkPatternsMotive [] (CaseMotiveNil ret) = pure ([],ret)
	checkPatternsMotive (MakeMeta :: ps) (CaseMotiveCons _ sc') = do
		m <- newMetaVar
		(ps',ret) <- checkPatternsMotive ps (instantiate sc' [Meta m])
		pure (AssertionPat (Meta m) :: ps', ret)
	checkPatternsMotive (p :: ps) (CaseMotiveCons arg sc') = do
		earg <- evaluate arg
		(p', x) <- checkifyPattern p earg
		(ps', ret) <- checkPatternsMotive ps (instantiate sc' [x])
		pure (p'::ps', ret )
	checkPatternsMotive _ _ = do
		let lps = length (descope Name psc)
		let lmot = caseMotiveLength motive
		throw $ "Motive " ++ show motive ++ " expects " ++ show lmot ++ " case "
				++ (if lmot == 1 then "arg" else "args")
				++ " but was given " ++ show lps

--  oYYo 0   0 8YYYY  oYYo 0  oY Y8Y 8YYYY 0   0  oYYo 0     o8o  0   0 oYYYo 8YYYY oYYYo
-- 0   " 8___8 8___  0   " 8_oY   0  8___  "o o" 0   " 0    8   8 0   0 %___  8___  %___
-- 0   , 8"""8 8"""  0   , 8"Yo   0  8"""    0   0   , 0    8YYY8 0   0 `"""p 8"""  `"""p
--  YooY 0   0 8oooo  YooY 0  Yo o8o 0       0    YooY 8ooo 0   0 "ooo" YoooY 8oooo YoooY

checkifyClauses [] _ = pure []
checkifyClauses (c :: cs) motive = do
	c' <- checkifyClause c motive
	cs' <- checkifyClauses cs motive
	pure $ c' :: cs'

--  oYYo 0   0 8YYYY  oYYo 0  oY Y8Y 8YYYY 0   0  oYYo _YYY_ 8o  0 oYYYo Y8Y  oYYo
-- 0   " 8___8 8___  0   " 8_oY   0  8___  "o o" 0   " 0   0 8Yo 8 %___   0  0  __
-- 0   , 8"""8 8"""  0   , 8"Yo   0  8"""    0   0   , 0   0 8 Yo8 `"""p  0  0  "8
--  YooY 0   0 8oooo  YooY 0  Yo o8o 0       0    YooY "ooo" 0   8 YoooY o8o  YooY

export
checkifyConSig : ConSig Term -> TypeChecker (ConSig Term)
checkifyConSig (ConSigNil ret) = do
	ret' <- checkify ret Star
	pure $ ConSigNil ret'
checkifyConSig (ConSigCons plic arg sc) with (head' $ names sc)
	| Just hsc = do
		arg' <- checkify arg Star
		i <- newName
		t <- extendContext [(i, hsc, arg')]
				$ checkifyConSig (instantiate sc [Var (Generated hsc i)])
		pure $ ConSigCons plic arg' (NewScope (names sc) (abstractOver [i] t))
	| Nothing = throw "Should not happen"

-- 8YYYo 0   0 8888. 0    Y8Y  oYYo    8YYYY 0   0 8o  0  oYYo YY8YY Y8Y _YYY_ 8o  0 oYYYo
-- 8___P 0   0 8___Y 0     0  0   "    8___  0   0 8Yo 8 0   "   0    0  0   0 8Yo 8 %___
-- 8"""  0   0 8"""o 0     0  0   ,    8"""  0   0 8 Yo8 0   ,   0    0  0   0 8 Yo8 `"""p
-- 0     "ooo" 8ooo" 8ooo o8o  YooY    0     "ooo" 0   8  YooY   0   o8o "ooo" 0   8 YoooY

export
metasSolved : TypeChecker ()
metasSolved = do
	s <- get
	unless (tcNextMeta s == cast (length $ tcSubs s))
		$ throw "Not all metavariables have been solved."

export
check : Term -> Term -> TypeChecker Term
check m t = do
	et <- evaluate t
	m' <- checkify m et
	metasSolved
	subs <- substitution
	pure $ instantiateMetas subs m'

export
infer : Term -> TypeChecker Inferred
infer m = do
	(m' <:> t) <- inferify m
	metasSolved
	subs <- substitution
	et <- evaluate (instantiateMetas subs t)
	pure $ instantiateMetas subs m' <:> et

max_stars_repo_name: totalscript/totalscript

max_issues_repo_name: totalscript/totalscript

max_forks_repo_name: totalscript/totalscript


text:
> module FastSimpleProb.Predicates

> import FastSimpleProb.SimpleProb
> import FastSimpleProb.MonadicOperations
> import NonNegDouble.NonNegDouble
> import NonNegDouble.Predicates
> import Functor.Predicates

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

> {-
> ||| Monotonicity of |SimpleProb| measures
> Monotone : (SimpleProb NonNegDouble -> NonNegDouble) -> Type
> Monotone meas = {A : Type} ->
>                 (f : A -> NonNegDouble) -> (g : A -> NonNegDouble) ->
>                 (p : (a : A) -> f a `LTE` g a) -> (sp : SimpleProb A) ->
>                 meas (fmap f sp) `LTE` meas (fmap g sp)
> Monotone = Functor.Predicates.Monotone {B = NonNegDouble} {C = NonNegDouble} {F = SimpleProb} LTE LTE
> -}

ext: lidr

max_stars_repo_name: zenntenn/IdrisLibs

max_issues_repo_name: zenntenn/IdrisLibs

max_forks_repo_name: zenntenn/IdrisLibs


text:
> module SequentialDecisionProblems.applications.GoodOrBad

> import Data.Fin
> import Control.Isomorphism

> import Finite.Predicates
> import Finite.Operations
> import Finite.Properties
> import Sigma.Sigma

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

* Good / Bad options:

> data GoodOrBad = Good | Bad

* |GoodOrBad| is finite and non-empty:

> to : GoodOrBad -> Fin 2
> to Good   =    FZ
> to Bad = FS FZ

> from : Fin 2 -> GoodOrBad
> from             FZ   = Good
> from         (FS FZ)  = Bad
> from     (FS (FS  k)) = absurd k

> toFrom : (k : Fin 2) -> to (from k) = k
> toFrom             FZ   = Refl
> toFrom         (FS FZ)  = Refl
> toFrom     (FS (FS  k)) = absurd k

> fromTo : (a : GoodOrBad) -> from (to a) = a
> fromTo Good = Refl
> fromTo  Bad = Refl

> |||
> finiteGoodOrBad : Finite GoodOrBad
> finiteGoodOrBad = MkSigma 2 (MkIso to from toFrom fromTo)

> |||
> cardNotZGoodOrBad : CardNotZ finiteGoodOrBad
> cardNotZGoodOrBad = cardNotZLemma finiteGoodOrBad Good

> {-

> ---}


text:
module Core.Normalise

import public Core.Normalise.Convert
import public Core.Normalise.Eval
import public Core.Normalise.Quote

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

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

%default covering

-- Expand all the pi bindings at the start of a term, but otherwise don't
-- reduce
export
normalisePis : {auto c : Ref Ctxt Defs} ->
               {vars : List Name} ->
               Defs -> Env Term vars -> Term vars -> Core (Term vars)
normalisePis defs env tm
    = do tmnf <- nf defs env tm
         case tmnf of
              NBind _ _ (Pi _ _ _ _) _ => quoteWithPi defs env tmnf
              _ => pure tm

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

export
glueClosure : {auto c : Ref Ctxt Defs} ->
              {vars : _} ->
              Defs -> Env Term vars -> Closure vars -> Glued vars
glueClosure defs env clos
    = MkGlue False
             (do empty <- clearDefs defs
                 quote empty env clos)
             (const (evalClosure defs clos))

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

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

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

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

-- The size limit here is the depth of stuck applications. If it gets past
-- that size, return the original
export
tryNormaliseSizeLimit : {auto c : Ref Ctxt Defs} ->
                     {free : _} ->
                     Defs -> Nat ->
                     Env Term free -> Term free -> Core (Term free)
tryNormaliseSizeLimit defs limit env tm
    = do tm' <- nf defs env tm
         quoteOpts (MkQuoteOpts False False (Just limit)) defs env tm'

export
normaliseSizeLimit : {auto c : Ref Ctxt Defs} ->
                     {free : _} ->
                     Defs -> Nat ->
                     Env Term free -> Term free -> Core (Term free)
normaliseSizeLimit defs limit env tm
    = catch (do tm' <- nf defs env tm
                quoteOpts (MkQuoteOpts False False (Just limit)) defs env tm')
            (\err => pure tm)

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

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

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

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

   where

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

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

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

-- Log message with a value, translating back to human readable names first
export
logNF : {vars : _} ->
        {auto c : Ref Ctxt Defs} ->
        (s : String) ->
        {auto 0 _ : KnownTopic s} ->
        Nat -> Lazy String -> Env Term vars -> NF vars -> Core ()
logNF str n msg env tmnf
    = when !(logging str n) $
        do defs <- get Ctxt
           tm <- quote defs env tmnf
           tm' <- toFullNames tm
           logString str n (msg ++ ": " ++ show tm')

-- Log message with a term, reducing holes and translating back to human
-- readable names first
export
logTermNF' : {vars : _} ->
             {auto c : Ref Ctxt Defs} ->
             (s : String) ->
             {auto 0 _ : KnownTopic s} ->
             Nat -> Lazy String -> Env Term vars -> Term vars -> Core ()
logTermNF' str n msg env tm
    = do defs <- get Ctxt
         tmnf <- normaliseHoles defs env tm
         tm' <- toFullNames tmnf
         logString str n (msg ++ ": " ++ show tm')

export
logTermNF : {vars : _} ->
            {auto c : Ref Ctxt Defs} ->
            (s : String) ->
            {auto 0 _ : KnownTopic s} ->
            Nat -> Lazy String -> Env Term vars -> Term vars -> Core ()
logTermNF str n msg env tm
    = when !(logging str n) $ logTermNF' str n msg env tm

export
logGlue : {vars : _} ->
          {auto c : Ref Ctxt Defs} ->
          (s : String) ->
          {auto 0 _ : KnownTopic s} ->
          Nat -> Lazy String -> Env Term vars -> Glued vars -> Core ()
logGlue str n msg env gtm
    = when !(logging str n) $
        do defs <- get Ctxt
           tm <- getTerm gtm
           tm' <- toFullNames tm
           logString str n (msg ++ ": " ++ show tm')

export
logGlueNF : {vars : _} ->
            {auto c : Ref Ctxt Defs} ->
            (s : String) ->
            {auto 0 _ : KnownTopic s} ->
            Nat -> Lazy String -> Env Term vars -> Glued vars -> Core ()
logGlueNF str n msg env gtm
    = when !(logging str n) $
        do defs <- get Ctxt
           tm <- getTerm gtm
           tmnf <- normaliseHoles defs env tm
           tm' <- toFullNames tmnf
           logString str n (msg ++ ": " ++ show tm')

export
logEnv : {vars : _} ->
         {auto c : Ref Ctxt Defs} ->
         (s : String) ->
         {auto 0 _ : KnownTopic s} ->
         Nat -> String -> Env Term vars -> Core ()
logEnv str n msg env
    = when !(logging str n) $
        do logString str n msg
           dumpEnv env

  where

    dumpEnv : {vs : List Name} -> Env Term vs -> Core ()
    dumpEnv [] = pure ()
    dumpEnv {vs = x :: _} (Let _ c val ty :: bs)
        = do logTermNF' str n (msg ++ ": let " ++ show x) bs val
             logTermNF' str n (msg ++ ":" ++ show c ++ " " ++ show x) bs ty
             dumpEnv bs
    dumpEnv {vs = x :: _} (b :: bs)
        = do logTermNF' str n (msg ++ ":" ++ show (multiplicity b) ++ " " ++
                           show (piInfo b) ++ " " ++
                           show x) bs (binderType b)
             dumpEnv bs
replace' : {auto c : Ref Ctxt Defs} ->
           {vars : _} ->
           Int -> Defs -> Env Term vars ->
           (lhs : NF vars) -> (parg : Term vars) -> (exp : NF vars) ->
           Core (Term vars)
replace' {vars} tmpi defs env lhs parg tm
    = if !(convert defs env lhs tm)
         then pure parg
         else repSub tm
  where
    repArg : (Closure vars) -> Core (Term vars)
    repArg c
        = do tmnf <- evalClosure defs c
             replace' tmpi defs env lhs parg tmnf

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

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

-- If the term is an application of a primitive conversion (fromInteger etc)
-- and it's applied to a constant, fully normalise the term.
export
normalisePrims : {auto c : Ref Ctxt Defs} -> {vs : _} ->
                 -- size heuristic for when to unfold
                 (Constant -> Bool) ->
                 -- view to check whether an argument is a constant
                 (arg -> Maybe Constant) ->
                 -- Reduce everything (True) or just public export (False)
                 Bool ->
                 -- list of primitives
                 List Name ->
                 -- view of the potential redex
                 (n : Name) ->          -- function name
                 (args : List arg) ->   -- arguments from inside out (arg1, ..., argk)
                 -- actual term to evaluate if needed
                 (tm : Term vs) ->      -- original term (n arg1 ... argk)
                 Env Term vs ->         -- evaluation environment
                 -- output only evaluated if primitive
                 Core (Maybe (Term vs))
normalisePrims boundSafe viewConstant all prims n args tm env
   = do let True = isPrimName prims !(getFullName n) -- is a primitive
              | _ => pure Nothing
        let (mc :: _) = reverse args -- with at least one argument
              | _ => pure Nothing
        let (Just c) = viewConstant mc -- that is a constant
              | _ => pure Nothing
        let True = boundSafe c -- that we should expand
              | _ => pure Nothing
        defs <- get Ctxt
        tm <- if all
                 then normaliseAll defs env tm
                 else normalise defs env tm
        pure (Just tm)


text:
module Proofs.RingTheory

import Specifications.Ring
import Proofs.GroupCancelationLemmas
import Proofs.GroupTheory
import Symmetry.Opposite

%default total
%access export

zeroAbsorbsL : {(+) : Binop s} -> {(*) : Binop s} ->
  RingSpec (+) zero neg (*) -> (x : s) -> zero * x = zero
zeroAbsorbsL {zero} spec x = o4 where
  o1 : zero + zero = zero
  o1 = neutralL (monoid (group spec)) zero
  o2 : (zero + zero) * x = zero * x + zero * x
  o2 = distributativeR spec zero zero x
  o3 : zero * x = zero * x + zero * x
  o3 = cong {f = (* x)} o1 @== o2
  o4 : zero * x = zero
  o4 = groupCancelGivesNeutral (group spec) _ _ (sym o3)

zeroAbsorbsR : {(*) : Binop s} ->
  RingSpec _ zero _ (*) -> (x : s) -> x * zero = zero
zeroAbsorbsR spec = zeroAbsorbsL (multiplicativeOpposite spec)

negatedMultiplication : {(+) : Binop s} -> {(*) : Binop s} ->
  RingSpec (+) zero neg (*) -> (x,y : s) ->
    neg (x * y) = x * neg y
negatedMultiplication spec x y = o4 where
  o1 : x * (y + neg y) = x * y + x * neg y
  o1 = distributativeL spec x y _
  o2 : x * (y + neg y) = x * zero
  o2 = cong $ inverseR (group spec) y
  o3 : x * y + x * neg y = zero
  o3 = o1 @== o2 === zeroAbsorbsR spec x
  o4 : neg (x * y) = x * neg y
  o4 = groupInverseUnique (group spec) (x * y) _ o3

max_stars_repo_name: jeroennoels/verified-algebra

max_issues_repo_name: jeroennoels/verified-algebra

max_forks_repo_name: jeroennoels/verified-algebra


text:
module Group_property2

import congruence
import Monoid
import Group
import Group_property

%access public export

||| Property 8 - If f : g -> h is group homomorphism then f(inv(a)) = inv(f(a))
total
Group_property_8 : (dom : Type) -> ((*) : dom -> dom -> dom) -> (pfdom : IsGroup dom (*)) ->
                    (cod : Type) -> ((+) : cod -> cod -> cod) -> (pfcod : IsGroup cod (+)) ->
                    (f : dom -> cod) -> (pfhom : (Hom dom (*) pfdom cod (+) pfcod f)) ->
                    (a : dom) -> ( (f (Inv dom (*) pfdom a)) = (Inv cod (+) pfcod (f a)) )

Group_property_8 dom (*) pfdom cod (+) pfcod f pfhom a = let
                                                         pfid1_dom = (fst (snd pfdom))
                                                         e_dom1 = (fst pfid1_dom) -- identity in the IdentityExists
                                                         e_dom1_pf = (snd pfid1_dom) -- proof that e_dom1 is the identity

                                                         pfid2_dom = (fst (snd (snd pfdom)))
                                                         e_dom2 = (fst pfid2_dom) -- identity in the InverseExists
                                                         e_dom2_pf = (snd pfid2_dom) -- prood that it is the identity

                                                         pf_eq_dom_id12 = (Group_property_1 dom (*) pfdom e_dom1 e_dom2
                                                                            e_dom1_pf e_dom2_pf) -- proof that e_dom1 and e_dom2 are equal

                                                         pfid1_cod = (fst (snd pfcod))
                                                         e_cod1 = (fst pfid1_cod) -- identity in the IdentityExists
                                                         e_cod1_pf = (snd pfid1_cod) -- proof that e_cod1 is the identity

                                                         pfid2_cod = (fst (snd (snd pfcod)))
                                                         e_cod2 = (fst pfid2_cod) -- identity in the InverseExists
                                                         e_cod2_pf = (snd pfid2_cod) -- prood that it is the identity

                                                         pf_eq_cod_id12 = (Group_property_1 cod (+) pfcod e_cod1 e_cod2
                                                                            e_cod1_pf e_cod2_pf) -- proof that e_cod1 and e_cod2 are equal

                                                         a_inv_with_pf = snd (snd (snd pfdom)) a -- (Inv_with_pf dom (*) pfdom a)
                                                         a_inv = fst a_inv_with_pf
                                                         b = (f a_inv)
                                                         c = (Inv cod (+) pfcod (f a))

                                                         pf_id_to_id = (fst pfhom)
                                                         pf_res = (snd pfhom)

                                                         --aux_pf1 : ( ( Group_id dom (*) pfdom ) = (fst (snd pfdom)) )
                                                         --aux_pf1 = Refl -- proof that fst (Group_id dom (*) pfdom) = fst (fst (snd pfdom))

                                                         pf1 = (pf_res a a_inv) -- proof that f(a * a_inv) = f a + f a_inv
                                                         pf2 = (fst (snd a_inv_with_pf)) -- proof that a * a_inv = e_dom2
                                                         pf3 = congruence dom cod (a * a_inv) e_dom2 f pf2 -- proof that a * a_inv = e_dom2
                                                         pf4 = trans (sym pf1) pf3 -- proof that f(a * a_inv) = f e_dom2
                                                         pf5 = (Group_property_1 cod (+) pfcod
                                                               (f e_dom1) e_cod1 pf_id_to_id e_cod1_pf) -- proof that f e_dom1 = e_cod1
                                                         pf6 = congruence dom cod e_dom1 e_dom2 f pf_eq_dom_id12-- proof that f e_dom1 = f e_dom2
                                                         pf7 = trans (trans pf4 (sym pf6)) pf5 -- proof that (f a) + (f a_inv) = e_cod1
                                                         pf8 = Group_property_7 cod (+) pfcod (f a) (f a_inv) pf7 -- proof that inverse of (f a)
                                                                                -- is (f a_inv)
                                                         pf9 = snd (Inv_with_pf cod (+) pfcod (f a)) -- proof that c is a inverse of (f a) with
                                                                                -- e_cod2 as identity
                                                         pf9.1 = fst pf9 -- proof that (f a) + c = e_cod2
                                                         pf9.2 = snd pf9 -- proof that c + (f a) = e_cod2
                                                         pf10.1 = trans pf9.1 (sym pf_eq_cod_id12) -- proof that (f a) + c = e_cod1
                                                         pf10.2 = trans pf9.2 (sym pf_eq_cod_id12) -- -- proof that c + (f a) = e_cod1
                                                         pf10 = (pf10.1, pf10.2)

                                                         in
                                                         (Group_property_2 cod (+) pfcod (f a) b c pf8 pf10)

||| Property 9 - If a*b = c then b = Inv(a) * c
total
Group_property_9 : (grp : Type) -> ((*) : grp -> grp -> grp) -> (pfgrp : IsGroup grp (*)) ->
                   (a, b, c : grp) -> (a*b = c) -> (b = (Inv grp (*) pfgrp a)*c)

Group_property_9 grp (*) pfgrp a b c pfEq = ?rhs


text:
module Main

import Data.String
import System

total
foo : Maybe Int -> Int
foo x = let Just x' = x | Nothing => 100 in x'

main : IO ()
main = do [p, a] <- getArgs | [p] => putStrLn "No arguments!"
                            | (x :: y :: _) => putStrLn "Too many arguments!"
          let Just a' = parseInteger {a = Int} a | Nothing => putStrLn "Not an integer!"
          printLn (foo (Just a'))

{-

let pat = val | <alternatives> in x'

...becomes...

case val of
     pat => x'
     <alternatives>

do pat <- val | <alternatives>
   p

...becomes...

do x <- val
   case x of
        pat => p
        <alternatives>

do let pat = val | <alternatives>
   p

...becomes...

do case val of
        pat => p
        <alternatives>

-}

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 WebAssembly.Structure

import public WebAssembly.Structure.Values
import public WebAssembly.Structure.Types
import public WebAssembly.Structure.Instructions
import public WebAssembly.Structure.Modules

max_stars_repo_name: RaoulSchaffranek/idris-webassembly

max_issues_repo_name: RaoulSchaffranek/idris-webassembly

max_forks_repo_name: RaoulSchaffranek/idris-webassembly


text:
module Main
import Data.Vect

data DataStore : Type where
  MkData : (size : Nat) ->
           (items : Vect size String) ->
           DataStore

size : DataStore -> Nat
size (MkData size' items') = size'

items : (store : DataStore) -> Vect (size store) String
items (MkData size' items') = items'

addToStore : DataStore -> String -> DataStore
addToStore (MkData size items) newitem = MkData _ (addToData items)
  where
    addToData : Vect old String -> Vect (S old) String
    addToData [] = [newitem]
    addToData (x :: xs) = newitem :: x :: xs

sumInputs : Integer -> String -> Maybe (String, Integer)
sumInputs tot inp = let val = cast inp in
                        if val < 0
                           then Nothing
                        else let newVal = tot + val in
                            Just ("Subtotal: " ++ show newVal ++ "\n", newVal)

data Command = Add String
             | Get Integer
             | Size
             | Search String
             | Quit

parseCommand : (cmd : String) -> (args : String) -> Maybe Command
parseCommand "add" str = Just (Add str)
parseCommand "search" str = Just (Search str)
parseCommand "get" val = case all isDigit (unpack val) of
                            False => Nothing
                            True => Just (Get (cast val))
parseCommand "quit" "" = Just Quit
parseCommand "size" "" = Just Size
parseCommand _ _ = Nothing

parse : (input : String) -> Maybe Command
parse input = case span (/= ' ') input of
                   (cmd, args) => parseCommand cmd (ltrim args)

getEntry : (pos : Integer) -> (store : DataStore) -> Maybe (String, DataStore)
getEntry pos store = let store_items = items store in
                         case integerToFin pos (size store) of
                              Nothing => Just ("Out of range\n", store)
                              Just id => Just (index id store_items ++ "\n", store)

searchEntryHelper : (searchStr : String) -> (store : Vect n String) -> (currentResults : List (Nat,String)) -> List (Nat, String)
searchEntryHelper searchStr [] res = res
searchEntryHelper {n = S k} searchStr (x :: xs) res =
  let newResults =
    case Strings.isInfixOf searchStr x of
         True => (k,x) :: res
         False => res
  in searchEntryHelper searchStr xs newResults

searchEntry : (value : String) -> (store : DataStore) -> Maybe (String, DataStore)
searchEntry value store @ (MkData size items) = let search_result = searchEntryHelper value items Nil in
                                            Just ("Search results " ++ show (search_result) ++ "\n", store)

processCmd : (command : Command) -> (store : DataStore) -> Maybe (String, DataStore)
processCmd (Add value) store = Just ("ID " ++ show (size store) ++ "\n", addToStore store value)
processCmd (Get pos) store = getEntry pos store
processCmd Quit store = Nothing
processCmd Size store = Just ("Size " ++ show (size store) ++ "\n", store)
processCmd (Search value) store = searchEntry value store

processInput : DataStore -> String -> Maybe (String, DataStore)
processInput store input = case parse input of
                              Just cmd => processCmd cmd store
                              Nothing => Just ("Invalid commnad\n", store)

main : IO ()
main = replWith (MkData _ []) "Command: " processInput

max_stars_repo_name: janschultecom/idris-examples

max_issues_repo_name: janschultecom/idris-examples

max_forks_repo_name: janschultecom/idris-examples