text:
module Circuits.NetList.Linear.Usage.TermType.Use.Port

import Decidable.Equality

import Data.Nat
import Data.List.Elem
import Data.List.Quantifiers

import Data.Vect
import Data.Vect.AtIndex
import Data.Vect.Quantifiers

import Data.String

import Toolkit.Data.Whole
import Toolkit.Data.DList
import Toolkit.Data.DList.Elem

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

import Circuits.Common

import Circuits.NetList.Types

import Circuits.NetList.Linear.Usage.DataType
import Circuits.NetList.Linear.Usage.DataType.Use.Full
import Circuits.NetList.Linear.Usage.DataType.Use.Partial

import Circuits.NetList.Linear.Usage.TermType

%default total

namespace Full
  public export
  data Use : (type : Ty)
          -> (free : Usage type)
          -> (prfF : IsFree type free)
          -> (used : Usage type)
          -> (prfU : IsUsed type used)
                  -> Type
    where
      U : Use               type           free         pf          used         pu
       -> Use (TyPort (flow,type)) (TyPort free) (FreeP pf) (TyPort used) (UsedP pu)

  public export
  data Result : (free : Usage  (TyPort (f,dtype)))
             -> (prfF : IsFree (TyPort (f,dtype)) free)
                     -> Type
    where
     R : (used : Usage  (TyPort (f,dtype)))
      -> (prfU : IsUsed (TyPort (f,dtype)) used)
      -> (prf  : Use    (TyPort (f,dtype)) free prfF used prfU)
              -> Result free prfF

  export
  use : {dtype : DType}
     -> {free : Usage  (TyPort (f,dtype))}
     -> (prfF : IsFree (TyPort (f,dtype)) free)
             -> Result free prfF
  use (FreeP prf) with (use prf)
    use (FreeP prf) | (R x used result)
      = (R (TyPort x) (UsedP used) (U result))

namespace Partial

  public export
  data Use : (idx : Fin m)
          -> (type : Ty)
          -> (free : Usage type)
          -> (prfF : IsFreeAt idx type free)
          -> (used : Usage type)
          -> (prfU : IsUsedAt idx type used)
                  -> Type

    where
      U : Use idx                                         type            f          pF          u          pU
       -> Use idx (TyPort (flow,(BVECT (W (S n) ItIsSucc) type))) (TyPort f) (FreeAt pF) (TyPort u) (UsedAt pU)

  public export
  data Result : (idx : Fin m)
             -> (type : Ty)
             -> (free : Usage type)
             -> (prfF : IsFreeAt idx type free)
                     -> Type

    where
      R : (used  : Usage type)
       -> (prfU  : IsUsedAt idx type used)
       -> (holds : Use   idx type free prfF used prfU)
               -> Result idx type free prfF

  export
  use : (idx : Fin m)
     -> {type : Ty}
     -> {free : Usage type}
     -> (prfF : IsFreeAt idx type free)
             -> Result idx type free prfF
  use idx (FreeAt (FreeAt prf)) with (use idx prf)
    use idx (FreeAt (FreeAt prf)) | (R new prfU holds)
      = R (TyPort (Array new)) (UsedAt (UsedAt prfU)) (U (UA holds))

-- [ EOF ]

max_stars_repo_name: gallais/linear-circuits

max_issues_repo_name: gallais/linear-circuits

max_forks_repo_name: gallais/linear-circuits


text:
> module NonNegRational.Predicates

> import NonNegRational.NonNegRational
> import NonNegRational.BasicOperations
> import Fraction.Fraction
> import Fraction.Predicates

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

> ||| Proofs that `x` is less than or equal to `y`
> ||| @ x the smaller number
> ||| @ y the larger number
> LTE : (x, y : NonNegRational) -> Type
> LTE x y = Fraction.Predicates.LTE (toFraction x) (toFraction y)

ext: lidr

max_stars_repo_name: zenntenn/IdrisLibs

max_issues_repo_name: zenntenn/IdrisLibs

max_forks_repo_name: zenntenn/IdrisLibs


text:
module Verified.Algebra.Bool

import Classes.Verified
import Prelude.Algebra

%default total

instance Semigroup Bool where
  -- Laziness intereferes with the types
  (<+>) = \b1, b2 => b1 || b2

instance VerifiedSemigroup Bool where
  semigroupOpIsAssociative True _ _ = Refl
  semigroupOpIsAssociative False True _ = Refl
  semigroupOpIsAssociative False False True = Refl
  semigroupOpIsAssociative False False False = Refl

instance Monoid Bool where
  neutral = False

instance VerifiedMonoid Bool where
  monoidNeutralIsNeutralL True = Refl
  monoidNeutralIsNeutralL False = Refl
  monoidNeutralIsNeutralR r = Refl

ext: idr

max_stars_repo_name: yurrriq/idris-verified

max_issues_repo_name: yurrriq/idris-verified

max_forks_repo_name: yurrriq/idris-verified


text:
module Tree

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

data BSTree : Type -> Type where
     BSEmpty : Ord elem => BSTree elem
     BSNode : Ord elem => (left : BSTree elem) -> (val: elem) -> (right : BSTree elem) -> BSTree elem

insert : elem -> BSTree elem -> BSTree elem
insert x BSEmpty = BSNode BSEmpty x BSEmpty
insert x orig@(BSNode left val right) = case compare x val of
                                             LT => BSNode (insert x left) val right
                                             EQ => orig
                                             GT => BSNode left val (insert x right)

listToTree : Ord a => List a -> BSTree a
listToTree [] = BSEmpty
listToTree (x :: xs) = insert x (listToTree xs)

treeToList : BSTree a -> List a
treeToList BSEmpty = []
treeToList (BSNode left val right) = (treeToList left) ++ (val :: treeToList right)

max_stars_repo_name: balajisivaraman/idris-book

max_issues_repo_name: balajisivaraman/idris-book

max_forks_repo_name: balajisivaraman/idris-book


text:
||| Pretty Printing of Elab Data-Types
|||
||| This has not been cleaned-up so, it actually might not
||| look very pretty.
|||
||| This module can be used in the repl to evaluate, how
||| syntax is translated to TTImp and Decl representations.
||| Use `putPretty` together with a quoted expression and
||| inspect the underlying implementation.
|||
||| REPL Examples:
|||
|||   :exec putPretty `{{ Name.In.A.Namespace }}
|||   :exec putPretty `(Just (7 * x))
|||   :exec putPretty `((1 index : Fin n) -> Vect n t -> t)
module Language.Reflection.Pretty

import public Data.HVect
import Data.String
import public Language.Reflection
import public Text.PrettyPrint.Prettyprinter
import Text.PrettyPrint.Prettyprinter.Render.String

%default total

--------------------------------------------------------------------------------
--          Utils
--------------------------------------------------------------------------------

||| Pretty but uncolored output to the terminal
export
putPretty : Pretty t => t -> IO ()
putPretty t = putDoc (indent 2 $ vsep ["", pretty {ann = ()} t, "",""])

||| Constraint, witnessing that all types in the given
||| `Vect` of types have a `Pretty` instance.
public export
AllPretty : Vect n Type -> Type
AllPretty []        = ()
AllPretty (x :: xs) = (Pretty x, AllPretty xs)

||| Convert all values in a heterogeneous vector
||| to `Doc`s using their `Pretty` instances.
export
prettyPrecAll : AllPretty ts => Prec -> HVect ts -> List (Doc ann)
prettyPrecAll _ []       = []
prettyPrecAll p (x :: y) = prettyPrec p x :: prettyPrecAll p y

||| Alias for `prettyPrecAll Open`
export
prettyAll : AllPretty ts => HVect ts -> List (Doc ann)
prettyAll = prettyPrecAll Open

||| Alias for `prettyPrecAll App`
export
prettyAppAll : AllPretty ts => HVect ts -> List (Doc ann)
prettyAppAll = prettyPrecAll App

||| Alias for `hsep . prettyAll`
export
hsepH : AllPretty ts => HVect ts -> Doc ann
hsepH = hsep . prettyAll

||| Alias for `vsep . prettyAll`
export
vsepH : AllPretty ts => HVect ts -> Doc ann
vsepH = vsep . prettyAll

||| Alias for `hcat . prettyAll`
export
hcatH : AllPretty ts => HVect ts -> Doc ann
hcatH = hcat . prettyAll

||| Alias for `vcat . prettyAll`
export
vcatH : AllPretty ts => HVect ts -> Doc ann
vcatH = vcat . prettyAll

||| Alias for `sep . prettyAll`
export
sepH : AllPretty ts => HVect ts -> Doc ann
sepH = sep . prettyAll

||| Prettifies a list of values and concatenates the
||| results using dots as separators.
|||
||| Example: >> `dotted ["a","b","c"]
|||          "a.b.c"
export
dotted : Pretty t => (args : List t) -> Doc ann
dotted = hcat . punctuate "." . map pretty

||| Alias for `prettyPrec App`
export
prettyApp : Pretty t => t -> Doc ann
prettyApp = prettyPrec App

||| Alias for `prettyPrec Backtick`
|||
||| This is used to prettify infixed functions (`IApp`) and
||| set parentheses correctly.
export
prettyBacktick : Pretty t => t -> Doc ann
prettyBacktick = prettyPrec Backtick

||| Wraps a the given `Doc` in parenthesis if the
||| boolean flag is `True`.
export
docParens : Bool -> Doc ann -> Doc ann
docParens False doc = doc
docParens True  doc = parens doc

||| Wraps a the given `Doc` in parenthesis if `p >= App`.
export
appParens : (p : Prec) -> Doc ann -> Doc ann
appParens p = docParens (p >= App)

||| Wraps a the given `Doc` in parenthesis if `p >= Backtick`.
export
backtickParens : (p : Prec) -> Doc ann -> Doc ann
backtickParens p = docParens (p >= Backtick)

||| Data constructor application: Applies the given constructor `con`
||| to a list of arguments. Arguments will be wrapped in parentheses
||| if necessary and aligned properly.
export
applyDoc : (p : Prec) -> (con : Doc ann) -> (args : List (Doc ann)) -> Doc ann
applyDoc p con args = appParens p $ con <++> align (sep args)

export
apply : Pretty t => (p : Prec) -> (con : Doc ann) -> (args : List t) -> Doc ann
apply p con args = applyDoc p con (map prettyApp args)

export
applyH :  AllPretty ts
       => (p    : Prec)
       -> (con  : Doc ann)
       -> (args : HVect ts)
       -> Doc ann
applyH p con args = applyDoc p con (prettyAppAll args)

export
alignInfix :  (fun : String)
           -> (symbol : String)
           -> (args : List (Doc ann))
           -> Doc ann
alignInfix fun _ []       = pretty fun
alignInfix fun _ [type]   = pretty fun <++> type
alignInfix fun symbol (h :: t) =
  let h' = "." <++> flatAlt (spaces (cast (length symbol) - 1) <+> h) h
   in pretty fun <+> align (sep (h' :: map (pretty symbol <++>) t))

export
indentLines : (header : Doc ann) -> (lines : List (Doc ann)) -> Doc ann
indentLines header lines = align $ vsep [header, indent 2 $ vsep lines]

--------------------------------------------------------------------------------
--          Pretty instances for TT Types
--------------------------------------------------------------------------------

export
Pretty Count where
  pretty M0 = "M0"
  pretty M1 = "M1"
  pretty MW = "MW"

export
Pretty t => Pretty (PiInfo t) where
  prettyPrec _ ImplicitArg     = "ImplicitArg"
  prettyPrec _ ExplicitArg     = "ExplicitArg"
  prettyPrec _ AutoImplicit    = "AutoImplicit"
  prettyPrec p (DefImplicit x) = apply p "DefImplicit" [x]

export
Pretty LazyReason where
  pretty LInf     = "Inf"
  pretty LLazy    = "Lazy"
  pretty LUnknown = "Unknown"

export
Pretty TotalReq where
  pretty Total        = "Total"
  pretty CoveringOnly = "Covering"
  pretty PartialOK    = "Partial"

export
Pretty Visibility where
  pretty Private = "Private"
  pretty Export  = "Export"
  pretty Public  = "Public"

export
Pretty Namespace where
  pretty (MkNS xs) = dotted (reverse xs)

export
Pretty Name where
  pretty = pretty . show

export
Pretty Constant where
  pretty (I x)       = pretty x
  pretty (BI x)      = pretty x
  -- TODO : use `pretty` directly, once #1648 is merged
  pretty (I8 x)      = pretty $ show x
  pretty (I16 x)     = pretty $ show x
  pretty (I32 x)     = pretty $ show x
  pretty (I64 x)     = pretty $ show x
  pretty (B8 x)      = pretty x
  pretty (B16 x)     = pretty x
  pretty (B32 x)     = pretty x
  pretty (B64 x)     = pretty x
  pretty (Str x)     = pretty x
  pretty (Ch x)      = pretty x
  pretty (Db x)      = pretty x
  pretty WorldVal    = "%World"
  pretty IntType     = "Int"
  pretty IntegerType = "Integer"
  pretty Int8Type    = "Int8"
  pretty Int16Type   = "Int16"
  pretty Int32Type   = "Int32"
  pretty Int64Type   = "Int64"
  pretty Bits8Type   = "Bits8"
  pretty Bits16Type  = "Bits16"
  pretty Bits32Type  = "Bits32"
  pretty Bits64Type  = "Bits64"
  pretty StringType  = "String"
  pretty CharType    = "Char"
  pretty DoubleType  = "Double"
  pretty WorldType   = "World"

--------------------------------------------------------------------------------
--          Pretty instance for TTImp
--------------------------------------------------------------------------------

export
Pretty BindMode where
  prettyPrec p (PI x)   = apply p "PI" [x]
  prettyPrec _ PATTERN  = "PATTERN"
  prettyPrec _ NONE     = "NONE"
  prettyPrec _ COVERAGE = "COVERAGE"

export
Pretty UseSide where
  pretty UseLeft  = "UseLeft"
  pretty UseRight = "UseRight"

export
Pretty DotReason where
  pretty NonLinearVar    = "NonLinearVar"
  pretty VarApplied      = "VarApplied"
  pretty NotConstructor  = "NotConstructor"
  pretty ErasedArg       = "ErasedArg"
  pretty UserDotted      = "UserDotted"
  pretty UnknownDot      = "UnknownDot"
  pretty UnderAppliedCon = "UnderAppliedCon"

export
Pretty BuiltinType where
  pretty BuiltinNatural = "BuiltinNatural"
  pretty NaturalToInteger = "NaturalToInteger"
  pretty IntegerToNatural = "IntegerToNatural"

export
Pretty WithFlag where
  pretty Syntactic = "Syntactic"

export
Pretty DataOpt where
  prettyPrec p (SearchBy xs) = apply p "SearchBy" xs
  prettyPrec _ NoHints       = "NoHints"
  prettyPrec _ UniqueSearch  = "UniqueSearch"
  prettyPrec _ External      = "External"
  prettyPrec _ NoNewtype     = "NoNewtype"

mutual

  %default covering

  export
  Pretty IFieldUpdate where
    prettyPrec p (ISetField path x) =
      applyDoc p "ISetField" [dotted path, prettyApp x]

    prettyPrec p (ISetFieldApp path x) =
      applyDoc p "ISetFieldApp" [dotted path, prettyApp x]

  export
  Pretty AltType where
    prettyPrec _ FirstSuccess      = "FirstSuccess"
    prettyPrec _ Unique            = "Unique"
    prettyPrec p (UniqueDefault x) = apply p "UniqueDefault" [x]

  export
  Pretty NoMangleDirective where
    prettyPrec p (CommonName x)   = apply p "CommonName" [x]
    prettyPrec p (BackendNames x) = apply p "BackendNames" [x]

  export
  Pretty FnOpt where
    prettyPrec _ Inline         = "Inline"
    prettyPrec _ NoInline       = "NoInline"
    prettyPrec p (NoMangle x)   = apply p "NoMangle" [x]
    prettyPrec _ TCInline       = "TCInline"
    prettyPrec _ Deprecate      = "Deprecate"
    prettyPrec p (Hint x)       = apply p "Hint" [x]
    prettyPrec p (GlobalHint x) = apply p "GlobalHint" [x]
    prettyPrec _ ExternFn       = "ExternFn"
    prettyPrec p (ForeignFn xs) = apply p "ForeignFn" xs
    prettyPrec _ Invertible     = "Invertible"
    prettyPrec p (Totality x)   = apply p "Totality" [x]
    prettyPrec _ Macro          = "Macro"
    prettyPrec p (SpecArgs xs)  = apply p "SpecArgs" xs

  export
  Pretty ITy where
    prettyPrec p (MkTy _ _ n t) = applyH p "MkTy" [n, t]

  export
  Pretty Data where
    prettyPrec p (MkData _ n t o cs) = applyH p "MkData" [n,t,o,cs]
    prettyPrec p (MkLater _ n tycon) = applyH p "MkLater" [n, tycon]

  export
  Pretty IField where
    prettyPrec p (MkIField _ c pi n t) = applyH p "MkIField" [c,pi,n,t]

  export
  Pretty Record where
    prettyPrec p (MkRecord _ n ps c fs) = applyH p "MkRecord" [n,ps,c,fs]

  export
  Pretty Clause where
    prettyPrec p (PatClause _ l r) = applyH p "PatClause" [l, r]
    prettyPrec p (ImpossibleClause _ l) = applyH p "Impossible" [l]
    prettyPrec p (WithClause _ l w prf fs cs) = applyH p "WithClause" [l,w,prf,fs,cs]

  export
  Pretty Decl where
    prettyPrec p (IBuiltin _ b n) = applyH p "IBuiltin" [b,n]
    prettyPrec p (IRunElabDecl _ t) = applyH p "IRunElabDecl" [t]
    prettyPrec p (IClaim _ c v o t) = applyH p "IClaim" [c,v,o,t]
    prettyPrec p (IData _ v d t) = applyH p "IData" [v,d,t]
    prettyPrec p (IDef _ n cs) = applyH p "IDef" [n,cs]
    prettyPrec p (IParameters _ ps decs) = applyH p "IParameters" [ps,decs]
    prettyPrec p (IRecord _ n v t r) = applyH p "IRecord" [n, v, t, r]
    prettyPrec p (INamespace _ (MkNS ns) ds) =
      indentLines (applyDoc p "INamespace" [dotted ns]) (map pretty ds)

    prettyPrec p (ITransform _ n a b) = applyH p "ITransform" [n,a,b]
    prettyPrec p (ILog k) = apply p "ILog" [k]

  export
  Pretty TTImp where
    prettyPrec p (IVar _ y) = apply p "IVar" [y]

    prettyPrec p x@(IPi _ _ _ _ _ _) =
      backtickParens p (alignInfix "IPi" "->" $ args x)
      where args : TTImp -> List (Doc ann)
            args (IPi _ c i n at rt) =
              parens (hsepH [c,i,maybe ":" ((++ " :") . show) n,at]) :: args rt

            args rt = [prettyBacktick rt]

    prettyPrec p x@(ILam _ _ _ _ _ _) =
      backtickParens p (alignInfix "ILam" "=>" $ args x)
      where args : TTImp -> List (Doc ann)
            args (ILam _ c i n at rt) =
              parens (hsepH [c,i,maybe ":" ((++ " :") . show) n,at]) :: args rt

            args rt = [prettyBacktick rt]

    prettyPrec p (ILet _ _ cnt name nTy nVal scope) =
      applyH p "ILet" [cnt,name,nTy,nVal,scope]

    prettyPrec p (ICase _ arg ty cs) = applyH p "ICase" [arg,ty,cs]

    prettyPrec p (ILocal _ decls tt) =
      indentLines (apply p "ILocal" [tt]) (map pretty decls)

    prettyPrec p (IUpdate _ ups tt) = applyH p"IUpdate" [ups,tt]

    prettyPrec p x@(IApp _ _ _) =
      backtickParens p (alignInfix "IApp" "$" $ reverse (args x))
      where args : TTImp -> List (Doc ann)
            args (IApp _ f t) = prettyBacktick t :: args f
            args t            = [prettyBacktick t]

    prettyPrec p x@(IAutoApp _ _ _) =
      backtickParens p (alignInfix "IAutoApp" "$" $ reverse (args x))
      where args : TTImp -> List (Doc ann)
            args (IAutoApp _ f t) = prettyBacktick t :: args f
            args t                = [prettyBacktick t]

    prettyPrec p x@(INamedApp _ _ _ _) =
      backtickParens p (alignInfix "INamedApp" "$" $ reverse (args x))
      where args : TTImp -> List (Doc ann)
            args (INamedApp _ f n t) = prettyBacktick t :: args f
            args t                   = [prettyBacktick t]

--    prettyPrec p x@(IImplicitApp _ _ _ _) =
--      backtickParens p (alignInfix "IImplicitApp" "$" $ reverse (args x))
--      where args : TTImp -> List (Doc ann)
--            args (IImplicitApp _ f n t) = parens (hsepH[n,":",t]) :: args f
--            args t                      = [prettyBacktick t]

    prettyPrec p x@(IWithApp _ _ _) =
      backtickParens p (alignInfix "IWithApp" "$" $ reverse (args x))
      where args : TTImp -> List (Doc ann)
            args (IWithApp _ f t) = prettyBacktick t :: args f
            args t                = [prettyBacktick t]

    prettyPrec p (ISearch _ depth) = applyH p "ISearch" [depth]

    prettyPrec p (IAlternative _ alt xs) = applyH p "IAlternative" [alt,xs]

    prettyPrec p (IRewrite _ y z)   = applyH p "IRewrite" [y, z]
    prettyPrec p (IBindHere _ y z)  = applyH p "IBindHere" [y, z]
    prettyPrec p (IBindVar _ y)     = apply p "IBindVar" [y]
    prettyPrec p (IAs _ _ use n w)  = applyH p "IAs" [use,n,w]
    prettyPrec p (IMustUnify _ y z) = applyH p "IMustUnify" [y,z]
    prettyPrec p (IDelayed _ y z)   = applyH p "IDelayed" [y,z]
    prettyPrec p (IDelay _ y)       = apply p "IDelay" [y]
    prettyPrec p (IForce _ y)       = apply p "IForce" [y]
    prettyPrec p (IQuote _ y)       = apply p "IQuote" [y]
    prettyPrec p (IQuoteName _ y)   = apply p "IQuoteName" [y]
    prettyPrec p (IQuoteDecl _ y)   = apply p "IQuoteDecl" [y]
    prettyPrec p (IUnquote _ y)     = apply p "IUnquote" [y]
    prettyPrec p (IPrimVal _ y)     = apply p "IPrimVal" [y]
    prettyPrec _ (IType _)          = "IType"
    prettyPrec p (IHole _ y)        = apply p "IHole" [y]
    prettyPrec p (Implicit _ y)     = apply p "Implicit" [y]
    prettyPrec p (IWithUnambigNames _ xs y) = applyH p "IWithUnabigNames" [xs,y]


text:
module Inigo.Archive.Path

import Data.List
import Data.String
import Extra.String
import Inigo.Package.Package
import Inigo.Paths

isIPkg : String -> Bool
isIPkg =
  isSuffixOf ".ipkg"

isBuild : String -> Bool
isBuild =
  isInfixOf "/build/"

isDep : String -> Bool
isDep =
  isInfixOf inigoDepDir

isDisallowed : String -> Bool
isDisallowed x =
  isIPkg x || isBuild x || isDep x

export
ignoreFiles : List String -> List String
ignoreFiles =
  filter (not . isDisallowed)

export
depPath : Package -> String
depPath pkg =
  let
    modPath = joinPath (split '.' (package pkg))
  in
    inigoDepDir </> (ns pkg) </> modPath

max_stars_repo_name: Z-snails/inigo

max_issues_repo_name: Z-snails/inigo

max_forks_repo_name: Z-snails/inigo


text:
import Data.Bits

class Masher m where
  blockLength : Nat

class Masher h => Hash h where
  outputLength : Nat
  initialContext : Bits blockLength
  updateContext : Bits blockLength -> Bits blockLength -> Bits blockLength
  finalize : Bits blockLength -> Vect (div outputLength blockLength) (Bits blockLength)

hashMessage : Hash h => h -> List (Bits blockLength) -> Vect (div outputLength blockLength) (Bits blockLength)
hashMessage hash = finalize . foldl updateContext initialContext

class Masher c => Cipher c where
  encryptMessage : e -> List (Bits blockLength) -> List (Bits blockLength)
  decryptMessage : d -> List (Bits blockLength) -> List (Bits blockLength)

class (Cipher c) => SymmetricCipher c where

class Masher s => Signer s where
  signMessage : e -> List (Bits blockLength) -> List (Bits blockLength)

class Masher v => Verifier v where
  verifyMessage : v -> List (Bits blockLength) -> List (Bits blockLength) -> Bool

class (Signer m, Verifier m) => MAC m where
  instance Verifier m where
    verifyMessage key message digest = digest == signMessage key message

class (Signer s, Verifier v) => Signature s v where
  buildKeyPair : (s, v)

class Cipher pk => PrivateKey pk where

class Cipher pk => PublicKey pk where

instance (Hash h, PrivateKey p) => Masher (h, p) where
  blockLength = blockLength

instance (Hash h, PrivateKey p) => Signer (h, p) where
  signMessage (hash, pk) message = encryptMessage pk (toList (hashMessage hash message))

instance (Hash h, PublicKey p) => Masher (h, p) where
  blockLength = blockLength

instance (Hash h, PublicKey v) => Verifier (h, v) where
  verifyMessage (hash, pk) message signature =
    decryptMessage pk signature == toList (hashMessage hash message)

class (PrivateKey p, PublicKey v) => AsymmetricCipher p v where

instance (AsymmetricCipher p v, Hash h) => Signature (h, p) (h, v) where
  buildKeyPair = buildKeyPair

max_stars_repo_name: idris-hackers/idris-crypto

max_issues_repo_name: idris-hackers/idris-crypto

max_forks_repo_name: idris-hackers/idris-crypto


text:
module ResourceProtocols

%default total

data DoorState = Open | Closed

data Door : DoorState -> Type where
  MkDoor : (doorId : Int) -> Door st

openDoor : (1 d : Door Closed) -> Door Open

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

newDoor : (1 p : (1 d : Door Closed) -> IO ()) -> IO ()

deleteDoor : (1 d : Door Closed) -> IO ()

doorProg : IO ()
doorProg = newDoor $ \d => let d' = openDoor d
                               d'' = closeDoor d' in
                               deleteDoor d''

max_stars_repo_name: timmyjose-study/idris-from-the-docs

max_issues_repo_name: timmyjose-study/idris-from-the-docs

max_forks_repo_name: timmyjose-study/idris-from-the-docs


text:
import Data.Vect

tryIndex : Integer -> Vect n a -> Maybe a
tryIndex {n} i xs = case integerToFin i n of
                         Nothing => Nothing
                         (Just idx) => Just (index idx xs)

vectTake : (n : Nat) -> Vect (n + m) a -> Vect n a
vectTake Z xs = []
vectTake (S k) (x :: xs) = x :: vectTake k xs

sumEntries : Num a => (pos : Integer) -> Vect n a -> Vect n a -> Maybe a
sumEntries pos [] [] = Nothing
sumEntries 0 (x :: xs) (y :: ys) = Just (x + y)
sumEntries pos (x :: xs) (y :: ys) = sumEntries (pos - 1) xs ys

altSumEntries : Num a => (pos : Integer) -> Vect n a -> Vect n a -> Maybe a
altSumEntries {n} pos xs ys = case integerToFin pos n of
                                   Nothing => Nothing
                                   (Just x) => Just (index x xs + index x ys)


text:
module Chapter3

import Data.Bool
import Data.InSet
import Data.Lawful.Eqv
import Data.List
import Data.Nat
import Data.So

import Syntax.WithProof

%default total

-- Exercise 3.1

public export
data Tree a = Tip
            | Node (Tree a) a (Tree a)

-- Telling once that here we're using the `Eq`-based equality for sets.
export %hint %inline
UsedEquality : Eqv a => Equality a
UsedEquality = StandardEq

public export
set : Eqv a => Tree a -> InSet a
set Tip          = []
set (Node l x r) = [x] + set l + set r

public export
all_satisfy : (a -> Bool) -> Tree a -> Bool
all_satisfy _ Tip          = True
all_satisfy p (Node l x r) = p x && all_satisfy p l && all_satisfy p r

public export
ord : Ord a => Tree a -> Bool
ord Tip = True
ord (Node l x r) = ord l && ord r && all_satisfy (<= x) l && all_satisfy (>= x) r

public export
ins : Ord a => a -> Tree a -> Tree a
ins n Tip = Node Tip n Tip
ins n t@(Node l x r) with (x == n)
  ins n t@(Node _ _ _) | True = t
  ins n t@(Node l x r) | False with (x < n)
    ins n t@(Node l x r) | False | True  = Node (ins n l) x r
    ins n t@(Node l x r) | False | False = Node l x (ins n r)

  -- Such verbose with-matching is done because else Idris suspects non-totality somewhy.

export
ins_adds : (Ord a, Eqv a) => (n : a) -> (t : Tree a) -> set (ins n t) == [n] + set t
ins_adds n Tip p = let u = union_empty_neutral ([n] + []) p in
                   rewrite u in -- what's the f**k? why should I do this?
                   rewrite union_empty_neutral [n] p in
                   Refl
ins_adds n (Node l x r) p with (@@(x =?= n))
  ins_adds n (Node l x r) p | (True ** prf) = ?ins_adds_rhs_1
  ins_adds n (Node l x r) p | (False ** prf) = ?ins_adds_rhs_2

split_and : {a, b : Bool} -> a && b = True -> (a = True, b = True)
split_and {a=True} {b=True} Refl = (Refl, Refl)

export
ins_preserves_ord : Ord a => (i : a) -> (t : Tree a) -> ord t = True -> ord (ins i t) = True
ins_preserves_ord i Tip prf = prf
ins_preserves_ord i (Node l x r) prf with (x == i)
  ins_preserves_ord i (Node l x r) prf | True = prf
  ins_preserves_ord i (Node l x r) prf | False with (x < i)
    ins_preserves_ord i (Node l x r) prf | False | True =
                                                          let v = ins_preserves_ord i l (fst $ split_and prf) in
                                                          let u = fst $ split_and $ snd $ split_and prf in
                                                          ?ins_preserves_ord_rhs_3
    ins_preserves_ord i (Node l x r) prf | False | False = ?ins_preserves_ord_rhs_4

-- Examples from section 3.5.1

public export
data Ev : Nat -> Type where
  Ev0  : Ev 0
  EvSS : Ev n -> Ev (S $ S n)

export
ev4 : Ev 4
ev4 = EvSS (EvSS Ev0)

public export
evn : Nat -> Bool
evn Z         = True
evn (S Z)     = False
evn (S (S n)) = evn n

export
ev_thus_evn_true : (n : Nat) -> Ev n -> evn n = True
ev_thus_evn_true 0         Ev0      = Refl
ev_thus_evn_true (S (S n)) (EvSS x) = ev_thus_evn_true n x

export
evn_true_thus_ev : (n : Nat) -> evn n = True -> Ev n
evn_true_thus_ev 0         _   = Ev0
evn_true_thus_ev (S (S n)) prf = EvSS $ evn_true_thus_ev n prf

export
ev_minus : (m : Nat) -> Ev m -> Ev (m `minus` 2)
ev_minus Z         Ev0      = Ev0
ev_minus (S (S n)) (EvSS x) = rewrite minusZeroRight n in x

export
not_ev_thus_evn_false : (n : Nat) -> Not $ Ev n -> evn n = False
not_ev_thus_evn_false 0         f = absurd $ f Ev0
not_ev_thus_evn_false (S 0)     _ = Refl
not_ev_thus_evn_false (S (S k)) f = not_ev_thus_evn_false k $ f . EvSS

export
evn_false_thus_not_ev : (n : Nat) -> evn n = False -> Not $ Ev n
evn_false_thus_not_ev (S (S k)) prf (EvSS x) = evn_false_thus_not_ev k prf x

-- Example from section 3.5.2

public export
data Star : (a -> a -> Type) -> a -> a -> Type where
  Refl : Star r x x
  Step : {0 r : a -> a -> Type} -> r x y -> Star r y z -> Star r x z

export
star_trans : Star r x y -> Star r y z -> Star r x z
star_trans Refl       y = y
star_trans (Step x w) y = Step x (star_trans w y)

-- Exercise 3.2

public export
data Palindrome : List a -> Type where
  Nil  : Palindrome []
  (::) : (x : a) -> Palindrome xs -> Palindrome $ x :: xs ++ [x]

export
rev_of_palindrome : (xs : List a) -> Palindrome xs -> reverse xs = xs
rev_of_palindrome []               []     = Refl
rev_of_palindrome (x::(xs ++ [x])) (x::y) = rewrite sym $ revAppend (x::xs) [x] in
                                            rewrite sym $ revAppend [x] xs in
                                            rewrite rev_of_palindrome xs y in
                                            Refl

-- Exercise 3.3

public export
data Star' : (a -> a -> Type) -> a -> a -> Type where
  Refl' : Star' r x x
  Step' : {0 r : a -> a -> Type} -> Star' r x y -> r y z -> Star' r x z

export
star'_is_star : Star' r n m -> Star r n m
star'_is_star Refl'              = Refl
star'_is_star (Step' s'_ny r_ym) = star'_is_star s'_ny `star_trans` Step r_ym Refl

export
star'_trans : Star' r x y -> Star' r y z -> Star' r x z
star'_trans x Refl'       = x
star'_trans x (Step' y w) = Step' (star'_trans x y) w

export
star_is_star' : Star r x y -> Star' r x y
star_is_star' Refl       = Refl'
star_is_star' (Step x z) = Step' Refl' x `star'_trans` star_is_star' z

-- Execrise 3.4

public export
data Iter : (a -> a -> Type) -> Nat -> a -> a -> Type where
  IterZ : Iter r 0 x x
  IterS : {0 r : a -> a -> Type} -> r x y -> Iter r n y z -> Iter r (S n) x z

export
iter_then_star : Iter r n x y -> Star r x y
iter_then_star IterZ       = Refl
iter_then_star (IterS x z) = Step x (iter_then_star z)

export
star_then_some_iter : Star r x y -> (n ** Iter r n x y)
star_then_some_iter Refl       = (_ ** IterZ)
star_then_some_iter (Step x z) = (_ ** IterS x $ snd $ star_then_some_iter z)

-- Exercise 3.5

public export
data Alpha = A | B

namespace S
  public export
  data S : List Alpha -> Type where
    Empty : S []
    Asb   : {w : List Alpha} -> S w -> S $ [A] ++ w ++ [B]
    Ss    : {w, v : List Alpha} -> S w -> S v -> S $ w ++ v

namespace T
  public export
  data T : List Alpha -> Type where
    Empty : T []
    Tatb  : {w, v : List Alpha} -> T w -> T v -> T $ w ++ [A] ++ v ++ [B]

export
s_to_t : T w -> S w
s_to_t Empty              = Empty
s_to_t (Tatb {w} {v} x y) = Ss (s_to_t x) $ Asb $ s_to_t y

t_conj : {w : List Alpha} -> T w -> T v -> T (w ++ v)
t_conj x Empty = rewrite appendNilRightNeutral w in x
t_conj x (Tatb {v=a} {w=b} y z) = rewrite appendAssociative w b ([A] ++ a ++ [B]) in Tatb (t_conj x y) z

export
t_to_s : S w -> T w
t_to_s Empty    = Empty
t_to_s (Asb x)  = Tatb Empty $ t_to_s x
t_to_s (Ss x y) = t_conj (t_to_s x) (t_to_s y)

max_stars_repo_name: buzden/prog-prove-exercises

max_issues_repo_name: buzden/prog-prove-exercises

max_forks_repo_name: buzden/prog-prove-exercises


text:
module Sub10Apply108x18

import ProofColDivSeqBase
import ProofColDivSeqPostulate

%default total
-- %language ElabReflection

-- 3(36x+6) --F[5,-2]->E[2,-4]--> 3(8x+1)
fe108x18To24x3 :
  (o:Nat) ->  P (S (S (S (S (plus (plus (plus (plus (plus (plus o o) o) (plus (plus o o) o)) (plus (plus (plus o o) o) (plus (plus o o) o)))
                                  (S (plus (plus (plus (plus o o) o) (plus (plus o o) o)) (plus (plus (plus o o) o) (plus (plus o o) o)))))
                            (S (plus (plus (plus (plus o o) o) (plus (plus o o) o)) (plus (plus (plus o o) o) (plus (plus o o) o))))))))) 2
    -> P (S (plus (plus (plus o o) (plus o o)) (plus (plus o o) (plus o o)))) 2
fe108x18To24x3 o prf =
  let prf2 = lvDown (S (S (S (S (plus (plus (plus (plus (plus (plus o o) o) (plus (plus o o) o)) (plus (plus (plus o o) o) (plus (plus o o) o)))
                                  (S (plus (plus (plus (plus o o) o) (plus (plus o o) o)) (plus (plus (plus o o) o) (plus (plus o o) o)))))
                            (S (plus (plus (plus (plus o o) o) (plus (plus o o) o)) (plus (plus (plus o o) o) (plus (plus o o) o))))))))) 2
                    prf in
    let prf3 = fe108x18To24x3' o prf2 in lvDown (S (plus (plus (plus o o) (plus o o)) (plus (plus o o) (plus o o)))) 3 prf3

export
apply108x18 : P (S (S (S (S (plus (plus (plus (plus (plus (plus o o) o) (plus (plus o o) o)) (plus (plus (plus o o) o) (plus (plus o o) o)))
                                  (S (plus (plus (plus (plus o o) o) (plus (plus o o) o)) (plus (plus (plus o o) o) (plus (plus o o) o)))))
                            (S (plus (plus (plus (plus o o) o) (plus (plus o o) o)) (plus (plus (plus o o) o) (plus (plus o o) o))))))))) 2
    -> (m : Nat **
        (LTE (S m)
             (S (S (S (S (plus (plus (plus (plus (plus (plus o o) o) (plus (plus o o) o)) (plus (plus (plus o o) o) (plus (plus o o) o)))
                                     (S (plus (plus (plus (plus o o) o) (plus (plus o o) o)) (plus (plus (plus o o) o) (plus (plus o o) o)))))
                               (S (plus (plus (plus (plus o o) o) (plus (plus o o) o)) (plus (plus (plus o o) o) (plus (plus o o) o))))))))),
         P m 2))
apply108x18 {o} col = let col2 = fe108x18To24x3 o col in ((S (plus (plus (plus o o) (plus o o)) (plus (plus o o) (plus o o))))
                                                           ** (lte108x18 o, col2)) where
  lte108x18 : (o:Nat) -> LTE (S (S (plus (plus (plus o o) (plus o o)) (plus (plus o o) (plus o o)))))
          (S (S (S (S (plus (plus (plus (plus (plus (plus o o) o) (plus (plus o o) o)) (plus (plus (plus o o) o) (plus (plus o o) o)))
                                  (S (plus (plus (plus (plus o o) o) (plus (plus o o) o)) (plus (plus (plus o o) o) (plus (plus o o) o)))))
                            (S (plus (plus (plus (plus o o) o) (plus (plus o o) o)) (plus (plus (plus o o) o) (plus (plus o o) o)))))))))
  lte108x18 Z = (lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . LTESucc . LTESucc) LTEZero
  lte108x18 (S o) = let lemma = lte108x18 o in
    rewrite (sym (plusSuccRightSucc o o)) in
    rewrite (sym (plusSuccRightSucc (plus o o)  (S (plus o o)))) in
    rewrite (sym (plusSuccRightSucc (plus o o)  (plus o o))) in
    rewrite (sym (plusSuccRightSucc (plus (plus o o) (plus o o))  (S (S (S (plus (plus o o) (plus o o))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus o o) (plus o o))  (S (S (plus (plus o o) (plus o o)))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus o o) (plus o o))  (S (plus (plus o o) (plus o o))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus o o) (plus o o))  (plus (plus o o) (plus o o)))) in

    rewrite (sym (plusSuccRightSucc (plus o o)  o)) in
    rewrite (sym (plusSuccRightSucc (plus (plus o o) o)  (S (S (plus (plus o o) o))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus o o) o)  (S (plus (plus o o) o)))) in
    rewrite (sym (plusSuccRightSucc (plus (plus o o) o)  (plus (plus o o) o))) in

    rewrite (sym (plusSuccRightSucc (plus (plus (plus o o) o) (plus (plus o o) o))  (S (S (S (S (S (plus (plus (plus o o) o) (plus (plus o o) o))))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus o o) o) (plus (plus o o) o))  (S (S (S (S (plus (plus (plus o o) o) (plus (plus o o) o)))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus o o) o) (plus (plus o o) o))  (S (S (S (plus (plus (plus o o) o) (plus (plus o o) o))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus o o) o) (plus (plus o o) o))  (S (S (plus (plus (plus o o) o) (plus (plus o o) o)))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus o o) o) (plus (plus o o) o))  (S (plus (plus (plus o o) o) (plus (plus o o) o))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus o o) o) (plus (plus o o) o))  (plus (plus (plus o o) o) (plus (plus o o) o)))) in

    rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus o o) o) (plus (plus o o) o))
                                                                            (plus (plus (plus o o) o) (plus (plus o o) o)))
                                    (S (S (S (S (S (S (S (S (S (S (S (S (plus (plus (plus (plus o o) o) (plus (plus o o) o))
                                                                                (plus (plus (plus o o) o)
                                                                                (plus (plus o o) o))))))))))))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus o o) o) (plus (plus o o) o))
                                                                            (plus (plus (plus o o) o) (plus (plus o o) o)))
                                    (S (S (S (S (S (S (S (S (S (S (S (plus (plus (plus (plus o o) o) (plus (plus o o) o))
                                                                                (plus (plus (plus o o) o)
                                                                                (plus (plus o o) o)))))))))))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus o o) o) (plus (plus o o) o))
                                                                            (plus (plus (plus o o) o) (plus (plus o o) o)))
                                    (S (S (S (S (S (S (S (S (S (S (plus (plus (plus (plus o o) o) (plus (plus o o) o))
                                                                                (plus (plus (plus o o) o)
                                                                                (plus (plus o o) o))))))))))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus o o) o) (plus (plus o o) o))
                                                                            (plus (plus (plus o o) o) (plus (plus o o) o)))
                                    (S (S (S (S (S (S (S (S (S (plus (plus (plus (plus o o) o) (plus (plus o o) o))
                                                                                (plus (plus (plus o o) o)
                                                                                (plus (plus o o) o)))))))))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus o o) o) (plus (plus o o) o))
                                                                            (plus (plus (plus o o) o) (plus (plus o o) o)))
                                    (S (S (S (S (S (S (S (S (plus (plus (plus (plus o o) o) (plus (plus o o) o))
                                                                                (plus (plus (plus o o) o)
                                                                                (plus (plus o o) o))))))))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus o o) o) (plus (plus o o) o))
                                                                            (plus (plus (plus o o) o) (plus (plus o o) o)))
                                    (S (S (S (S (S (S (S (plus (plus (plus (plus o o) o) (plus (plus o o) o))
                                                                                (plus (plus (plus o o) o)
                                                                                (plus (plus o o) o)))))))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus o o) o) (plus (plus o o) o))
                                                                            (plus (plus (plus o o) o) (plus (plus o o) o)))
                                    (S (S (S (S (S (S (plus (plus (plus (plus o o) o) (plus (plus o o) o))
                                                                                (plus (plus (plus o o) o)
                                                                                (plus (plus o o) o))))))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus o o) o) (plus (plus o o) o))
                                                                            (plus (plus (plus o o) o) (plus (plus o o) o)))
                                    (S (S (S (S (S (plus (plus (plus (plus o o) o) (plus (plus o o) o))
                                                                                (plus (plus (plus o o) o)
                                                                                (plus (plus o o) o)))))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus o o) o) (plus (plus o o) o))
                                                                            (plus (plus (plus o o) o) (plus (plus o o) o)))
                                    (S (S (S (S (plus (plus (plus (plus o o) o) (plus (plus o o) o))
                                                                                (plus (plus (plus o o) o)
                                                                                (plus (plus o o) o))))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus o o) o) (plus (plus o o) o))
                                                                            (plus (plus (plus o o) o) (plus (plus o o) o)))
                                    (S (S (S (plus (plus (plus (plus o o) o) (plus (plus o o) o))
                                                                                (plus (plus (plus o o) o)
                                                                                (plus (plus o o) o)))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus o o) o) (plus (plus o o) o))
                                                                            (plus (plus (plus o o) o) (plus (plus o o) o)))
                                    (S (S (plus (plus (plus (plus o o) o) (plus (plus o o) o))
                                                                                (plus (plus (plus o o) o)
                                                                                (plus (plus o o) o))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus o o) o) (plus (plus o o) o))
                                                                            (plus (plus (plus o o) o) (plus (plus o o) o)))
                                    (S (plus (plus (plus (plus o o) o) (plus (plus o o) o))
                                                                                (plus (plus (plus o o) o)
                                                                                (plus (plus o o) o)))))) in

    rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus (plus o o) o)
                                                                                (plus (plus o o) o))
                                                                                (plus (plus (plus o o) o) (plus (plus o o) o)))
                                                                                (S (plus (plus (plus (plus o o) o) (plus (plus o o) o))
                                                                                (plus (plus (plus o o) o) (plus (plus o o) o)))))
                                    (S (S (S (S (S (S (S (S (S (S (S (S (plus (plus (plus (plus o o) o)
                                                                                (plus (plus o o) o))
                                                                                (plus (plus (plus o o) o)
                                                                                (plus (plus o o)
                                                      o))))))))))))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus (plus o o) o)
                                                                                (plus (plus o o) o))
                                                                                (plus (plus (plus o o) o) (plus (plus o o) o)))
                                                                                (S (plus (plus (plus (plus o o) o) (plus (plus o o) o))
                                                                                (plus (plus (plus o o) o) (plus (plus o o) o)))))
                                    (S (S (S (S (S (S (S (S (S (S (S (plus (plus (plus (plus o o) o)
                                                                                (plus (plus o o) o))
                                                                                (plus (plus (plus o o) o)
                                                                                (plus (plus o o)
                                                      o)))))))))))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus (plus o o) o)
                                                                                (plus (plus o o) o))
                                                                                (plus (plus (plus o o) o) (plus (plus o o) o)))
                                                                                (S (plus (plus (plus (plus o o) o) (plus (plus o o) o))
                                                                                (plus (plus (plus o o) o) (plus (plus o o) o)))))
                                    (S (S (S (S (S (S (S (S (S (S (plus (plus (plus (plus o o) o)
                                                                                (plus (plus o o) o))
                                                                                (plus (plus (plus o o) o)
                                                                                (plus (plus o o)
                                                      o))))))))))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus (plus o o) o)
                                                                                (plus (plus o o) o))
                                                                                (plus (plus (plus o o) o) (plus (plus o o) o)))
                                                                                (S (plus (plus (plus (plus o o) o) (plus (plus o o) o))
                                                                                (plus (plus (plus o o) o) (plus (plus o o) o)))))
                                    (S (S (S (S (S (S (S (S (S (plus (plus (plus (plus o o) o)
                                                                                (plus (plus o o) o))
                                                                                (plus (plus (plus o o) o)
                                                                                (plus (plus o o)
                                                      o)))))))))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus (plus o o) o)
                                                                                (plus (plus o o) o))
                                                                                (plus (plus (plus o o) o) (plus (plus o o) o)))
                                                                                (S (plus (plus (plus (plus o o) o) (plus (plus o o) o))
                                                                                (plus (plus (plus o o) o) (plus (plus o o) o)))))
                                    (S (S (S (S (S (S (S (S (plus (plus (plus (plus o o) o)
                                                                                (plus (plus o o) o))
                                                                                (plus (plus (plus o o) o)
                                                                                (plus (plus o o)
                                                      o))))))))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus (plus o o) o)
                                                                                (plus (plus o o) o))
                                                                                (plus (plus (plus o o) o) (plus (plus o o) o)))
                                                                                (S (plus (plus (plus (plus o o) o) (plus (plus o o) o))
                                                                                (plus (plus (plus o o) o) (plus (plus o o) o)))))
                                    (S (S (S (S (S (S (S (plus (plus (plus (plus o o) o)
                                                                                (plus (plus o o) o))
                                                                                (plus (plus (plus o o) o)
                                                                                (plus (plus o o)
                                                      o)))))))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus (plus o o) o)
                                                                                (plus (plus o o) o))
                                                                                (plus (plus (plus o o) o) (plus (plus o o) o)))
                                                                                (S (plus (plus (plus (plus o o) o) (plus (plus o o) o))
                                                                                (plus (plus (plus o o) o) (plus (plus o o) o)))))
                                    (S (S (S (S (S (S (plus (plus (plus (plus o o) o)
                                                                                (plus (plus o o) o))
                                                                                (plus (plus (plus o o) o)
                                                                                (plus (plus o o)
                                                      o))))))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus (plus o o) o)
                                                                                (plus (plus o o) o))
                                                                                (plus (plus (plus o o) o) (plus (plus o o) o)))
                                                                                (S (plus (plus (plus (plus o o) o) (plus (plus o o) o))
                                                                                (plus (plus (plus o o) o) (plus (plus o o) o)))))
                                    (S (S (S (S (S (plus (plus (plus (plus o o) o)
                                                                                (plus (plus o o) o))
                                                                                (plus (plus (plus o o) o)
                                                                                (plus (plus o o)
                                                      o)))))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus (plus o o) o)
                                                                                (plus (plus o o) o))
                                                                                (plus (plus (plus o o) o) (plus (plus o o) o)))
                                                                                (S (plus (plus (plus (plus o o) o) (plus (plus o o) o))
                                                                                (plus (plus (plus o o) o) (plus (plus o o) o)))))
                                    (S (S (S (S (plus (plus (plus (plus o o) o)
                                                                                (plus (plus o o) o))
                                                                                (plus (plus (plus o o) o)
                                                                                (plus (plus o o)
                                                      o))))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus (plus o o) o)
                                                                                (plus (plus o o) o))
                                                                                (plus (plus (plus o o) o) (plus (plus o o) o)))
                                                                                (S (plus (plus (plus (plus o o) o) (plus (plus o o) o))
                                                                                (plus (plus (plus o o) o) (plus (plus o o) o)))))
                                    (S (S (S (plus (plus (plus (plus o o) o)
                                                                                (plus (plus o o) o))
                                                                                (plus (plus (plus o o) o)
                                                                                (plus (plus o o)
                                                      o)))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus (plus o o) o)
                                                                                (plus (plus o o) o))
                                                                                (plus (plus (plus o o) o) (plus (plus o o) o)))
                                                                                (S (plus (plus (plus (plus o o) o) (plus (plus o o) o))
                                                                                (plus (plus (plus o o) o) (plus (plus o o) o)))))
                                    (S (S (plus (plus (plus (plus o o) o)
                                                                                (plus (plus o o) o))
                                                                                (plus (plus (plus o o) o)
                                                                                (plus (plus o o)
                                                      o))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus (plus o o) o)
                                                                                (plus (plus o o) o))
                                                                                (plus (plus (plus o o) o) (plus (plus o o) o)))
                                                                                (S (plus (plus (plus (plus o o) o) (plus (plus o o) o))
                                                                                (plus (plus (plus o o) o) (plus (plus o o) o)))))
                                    (S (plus (plus (plus (plus o o) o)
                                                                                (plus (plus o o) o))
                                                                                (plus (plus (plus o o) o)
                                                                                (plus (plus o o)
                                                      o)))))) in
      (lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . LTESucc . LTESucc . LTESucc . LTESucc . LTESucc . LTESucc . LTESucc . LTESucc) lemma


text:
module Prelude.Types

import Builtin
import PrimIO
import Prelude.Basics
import Prelude.EqOrd
import Prelude.Interfaces
import Prelude.Num
import Prelude.Uninhabited

%default total

-----------
-- NATS ---
-----------

||| Natural numbers: unbounded, unsigned integers which can be pattern matched.
public export
data Nat =
  ||| Zero.
    Z
  | ||| Successor.
  S Nat

%name Nat k, j, i

-- This is used in the compiler as an efficient substitute for integerToNat.
prim__integerToNat : Integer -> Nat
prim__integerToNat i
  = if intToBool (prim__lte_Integer 0 i)
      then believe_me i
      else Z

public export
integerToNat : Integer -> Nat
integerToNat 0 = Z -- Force evaluation and hence caching of x at compile time
integerToNat x
  = if intToBool (prim__lte_Integer x 0)
       then Z
       else S (assert_total (integerToNat (prim__sub_Integer x 1)))

-- %builtin IntegerToNatural Prelude.Types.integerToNat

-- Define separately so we can spot the name when optimising Nats
||| Add two natural numbers.
||| @ x the number to case-split on
||| @ y the other numberpublic export
public export
plus : (x : Nat) -> (y : Nat) -> Nat
plus Z y = y
plus (S k) y = S (plus k y)

||| Subtract natural numbers.  If the second number is larger than the first,
||| return 0.
public export
minus : (left : Nat) -> Nat -> Nat
minus Z        right     = Z
minus left     Z         = left
minus (S left) (S right) = minus left right

||| Multiply natural numbers.
public export
mult : (x : Nat) -> Nat -> Nat
mult Z y = Z
mult (S k) y = plus y (mult k y)

public export
Num Nat where
  (+) = plus
  (*) = mult

  fromInteger x = integerToNat x

-- used for nat hack
public export
equalNat : (m, n : Nat) -> Bool
equalNat Z Z = True
equalNat (S j) (S k) = equalNat j k
equalNat _ _ = False

public export
Eq Nat where
  (==) = equalNat

-- used for nat hack
public export
compareNat : (m, n : Nat) -> Ordering
compareNat Z Z = EQ
compareNat Z (S k) = LT
compareNat (S k) Z = GT
compareNat (S j) (S k) = compareNat j k

public export
Ord Nat where
  compare = compareNat

public export
natToInteger : Nat -> Integer
natToInteger Z = 0
natToInteger (S k) = 1 + natToInteger k
                         -- integer (+) may be non-linear in second
                         -- argument

-- %builtin NaturalToInteger Prelude.Types.natToInteger

||| Counts the number of elements that satify a predicate.
public export
count : (Foldable t) => (predicate : a -> Bool) -> (t a) -> Nat
count predicate = foldMap @{%search} @{Additive} (\x => if predicate x then 1 else 0)

-----------
-- PAIRS --
-----------

%inline
public export
Bifunctor Pair where
  bimap f g (x, y) = (f x, g y)

%inline
public export
Bifoldable Pair where
  bifoldr f g acc (x, y) = f x (g y acc)
  bifoldl f g acc (x, y) = g (f acc x) y
  binull _ = False

%inline
public export
Bitraversable Pair where
  bitraverse f g (a,b) = [| (,) (f a) (g b) |]

%inline
public export
Functor (Pair a) where
  map = mapSnd

%inline
public export
Monoid a => Applicative (Pair a) where
  pure = (neutral,)
  (a1,f) <*> (a2,v) = (a1 <+> a2, f v)

%inline
public export
Monoid a => Monad (Pair a) where
  (a1,a) >>= f = let (a2,b) = f a in (a1 <+> a2, b)

-----------
-- MAYBE --
-----------

||| An optional value.  This can be used to represent the possibility of
||| failure, where a function may return a value, or not.
public export
data Maybe : (ty : Type) -> Type where
  ||| No value stored
  Nothing : Maybe ty

  ||| A value of type `ty` is stored
  Just : (x : ty) -> Maybe ty

public export
Uninhabited (Nothing = Just x) where
  uninhabited Refl impossible

public export
Uninhabited (Just x = Nothing) where
  uninhabited Refl impossible

public export
maybe : Lazy b -> Lazy (a -> b) -> Maybe a -> b
maybe n j Nothing  = n
maybe n j (Just x) = j x

||| Execute an applicative expression when the Maybe is Just
%inline public export
whenJust : Applicative f => Maybe a -> (a -> f ()) -> f ()
whenJust (Just a) k = k a
whenJust Nothing k = pure ()

public export
Eq a => Eq (Maybe a) where
  Nothing  == Nothing  = True
  Nothing  == (Just _) = False
  (Just _) == Nothing  = False
  (Just a) == (Just b) = a == b

public export
Ord a => Ord (Maybe a) where
  compare Nothing  Nothing  = EQ
  compare Nothing  (Just _) = LT
  compare (Just _) Nothing  = GT
  compare (Just a) (Just b) = compare a b

public export
Semigroup (Maybe a) where
  Nothing   <+> m = m
  (Just x)  <+> _ = Just x

public export
Monoid (Maybe a) where
  neutral = Nothing

public export
Functor Maybe where
  map f (Just x) = Just (f x)
  map f Nothing  = Nothing

public export
Applicative Maybe where
  pure = Just

  Just f <*> Just a = Just (f a)
  _      <*> _      = Nothing

public export
Alternative Maybe where
  empty = Nothing

  (Just x) <|> _ = Just x
  Nothing  <|> v = v

public export
Monad Maybe where
  Nothing  >>= k = Nothing
  (Just x) >>= k = k x

public export
Foldable Maybe where
  foldr _ z Nothing  = z
  foldr f z (Just x) = f x z
  null Nothing = True
  null (Just _) = False

public export
Traversable Maybe where
  traverse f Nothing = pure Nothing
  traverse f (Just x) = Just <$> f x

---------
-- DEC --
---------

||| Decidability.  A decidable property either holds or is a contradiction.
public export
data Dec : Type -> Type where
  ||| The case where the property holds.
  ||| @ prf the proof
  Yes : (prf : prop) -> Dec prop

  ||| The case where the property holding would be a contradiction.
  ||| @ contra a demonstration that prop would be a contradiction
  No  : (contra : Not prop) -> Dec prop

export Uninhabited (Yes p === No q) where uninhabited eq impossible
export Uninhabited (No p === Yes q) where uninhabited eq impossible

------------
-- EITHER --
------------

||| A sum type.
public export
data Either : (a : Type) -> (b : Type) -> Type where
  ||| One possibility of the sum, conventionally used to represent errors.
  Left : forall a, b. (x : a) -> Either a b

  ||| The other possibility, conventionally used to represent success.
  Right : forall a, b. (x : b) -> Either a b

export Uninhabited (Left p === Right q) where uninhabited eq impossible
export Uninhabited (Right p === Left q) where uninhabited eq impossible

export
Either (Uninhabited a) (Uninhabited b) => Uninhabited (a, b) where
  uninhabited (x, _) @{Left  _} = uninhabited x
  uninhabited (_, y) @{Right _} = uninhabited y

export
Uninhabited a => Uninhabited b => Uninhabited (Either a b) where
  uninhabited (Left l)  = uninhabited l
  uninhabited (Right r) = uninhabited r

||| Simply-typed eliminator for Either.
||| @ f the action to take on Left
||| @ g the action to take on Right
||| @ e the sum to analyze
public export
either : (f : Lazy (a -> c)) -> (g : Lazy (b -> c)) -> (e : Either a b) -> c
either l r (Left x) = l x
either l r (Right x) = r x

public export
(Eq a, Eq b) => Eq (Either a b) where
  Left x == Left x' = x == x'
  Right x == Right x' = x == x'
  _ == _ = False

public export
(Ord a, Ord b) => Ord (Either a b) where
  compare (Left x) (Left x') = compare x x'
  compare (Left _) (Right _) = LT
  compare (Right _) (Left _) = GT
  compare (Right x) (Right x') = compare x x'

%inline
public export
Functor (Either e) where
  map f (Left x) = Left x
  map f (Right x) = Right (f x)

%inline
public export
Bifunctor Either where
  bimap f _ (Left x) = Left (f x)
  bimap _ g (Right y) = Right (g y)

%inline
public export
Bifoldable Either where
  bifoldr f _ acc (Left a)  = f a acc
  bifoldr _ g acc (Right b) = g b acc

  bifoldl f _ acc (Left a)  = f acc a
  bifoldl _ g acc (Right b) = g acc b

  binull _ = False

%inline
public export
Bitraversable Either where
  bitraverse f _ (Left a)  = Left <$> f a
  bitraverse _ g (Right b) = Right <$> g b

%inline
public export
Applicative (Either e) where
  pure = Right

  (Left a) <*> _          = Left a
  (Right f) <*> (Right r) = Right (f r)
  (Right _) <*> (Left l)  = Left l

public export
Monad (Either e) where
  (Left n) >>= _ = Left n
  (Right r) >>= f = f r

public export
Foldable (Either e) where
  foldr f acc (Left _) = acc
  foldr f acc (Right x) = f x acc
  null (Left _) = True
  null (Right _) = False

public export
Traversable (Either e) where
  traverse f (Left x)  = pure (Left x)
  traverse f (Right x) = Right <$> f x

-----------
-- LISTS --
-----------

public export
Eq a => Eq (List a) where
  [] == [] = True
  x :: xs == y :: ys = x == y && xs == ys
  _ == _ = False

public export
Ord a => Ord (List a) where
  compare [] [] = EQ
  compare [] (x :: xs) = LT
  compare (x :: xs) [] = GT
  compare (x :: xs) (y ::ys)
     = case compare x y of
            EQ => compare xs ys
            c => c

namespace List
  public export
  (++) : (xs, ys : List a) -> List a
  [] ++ ys = ys
  (x :: xs) ++ ys = x :: xs ++ ys

  public export
  length : List a -> Nat
  length []        = Z
  length (x :: xs) = S (length xs)

  public export
  reverseOnto : List a -> List a -> List a
  reverseOnto acc [] = acc
  reverseOnto acc (x::xs) = reverseOnto (x::acc) xs

  public export
  reverse : List a -> List a
  reverse = reverseOnto []

  ||| Tail-recursive append. Uses of (++) are automatically transformed to
  ||| this. The only reason this is exported is that the proof of equivalence
  ||| lives in a different module.
  public export
  tailRecAppend : (xs, ys : List a) -> List a
  tailRecAppend xs ys = reverseOnto ys (reverse xs)

  -- Always use tailRecAppend at runtime. Data.List.tailRecAppendIsAppend
  -- proves these are equivalent.
  %transform "tailRecAppend" (++) = tailRecAppend

public export
Functor List where
  map f [] = []
  map f (x :: xs) = f x :: map f xs

public export
Semigroup (List a) where
  (<+>) = (++)

public export
Monoid (List a) where
  neutral = []

public export
Foldable List where
  foldr c n [] = n
  foldr c n (x::xs) = c x (foldr c n xs)

  foldl f q [] = q
  foldl f q (x::xs) = foldl f (f q x) xs

  null [] = True
  null (_::_) = False

  toList = id

  foldMap f = foldl (\acc, elem => acc <+> f elem) neutral

public export
Applicative List where
  pure x = [x]
  fs <*> vs = concatMap (\f => map f vs) fs

public export
Alternative List where
  empty = []
  xs <|> ys = xs ++ ys

public export
Monad List where
  m >>= f = concatMap f m

public export
Traversable List where
  traverse f [] = pure []
  traverse f (x::xs) = [| f x :: traverse f xs |]

-- This works quickly because when string-concat builds the result, it allocates
-- enough room in advance so there's only one allocation, rather than lots!
--
-- Like fastUnpack, this function won't reduce at compile time.
-- If you need to concatenate strings at compile time, use Prelude.concat.
%foreign
  "scheme:string-concat"
  "RefC:fastConcat"
  "javascript:lambda:(xs)=>''.concat(...__prim_idris2js_array(xs))"
  "jvm:concat(io/github/mmhelloworld/idrisjvm/runtime/IdrisList java/lang/String),io/github/mmhelloworld/idrisjvm/runtime/Strings"
export
fastConcat : List String -> String

%transform "fastConcat" concat {t = List} {a = String} = fastConcat

||| Check if something is a member of a list using the default Boolean equality.
public export
elem : Eq a => a -> List a -> Bool
x `elem` [] = False
x `elem` (y :: ys) = x == y ||  elem x ys

||| Lookup a value at a given position
export
getAt : Nat -> List a -> Maybe a
getAt Z     (x :: xs) = Just x
getAt (S k) (x :: xs) = getAt k xs
getAt _     []        = Nothing

-------------
-- STREAMS --
-------------

namespace Stream
  ||| An infinite stream.
  public export
  data Stream : Type -> Type where
       (::) : a -> Inf (Stream a) -> Stream a

%name Stream xs, ys, zs

public export
Functor Stream where
  map f (x :: xs) = f x :: map f xs

||| The first element of an infinite stream.
public export
head : Stream a -> a
head (x :: xs) = x

||| All but the first element.
public export
tail : Stream a -> Stream a
tail (x :: xs) = xs

||| Take precisely n elements from the stream.
||| @ n how many elements to take
||| @ xs the stream
public export
take : (n : Nat) -> (xs : Stream a) -> List a
take Z xs = []
take (S k) (x :: xs) = x :: take k xs

-------------
-- STRINGS --
-------------

namespace String
  public export
  (++) : (x : String) -> (y : String) -> String
  x ++ y = prim__strAppend x y

  ||| Returns the length of the string.
  |||
  ||| ```idris example
  ||| length ""
  ||| ```
  ||| ```idris example
  ||| length "ABC"
  ||| ```
  public export
  length : String -> Nat
  length str = fromInteger (prim__cast_IntInteger (prim__strLength str))

||| Reverses the elements within a string.
|||
||| ```idris example
||| reverse "ABC"
||| ```
||| ```idris example
||| reverse ""
||| ```
public export
reverse : String -> String
reverse = prim__strReverse

||| Returns a substring of a given string
|||
||| @ index The (zero based) index of the string to extract.  If this is beyond
|||         the end of the string, the function returns the empty string.
||| @ len The desired length of the substring.  Truncated if this exceeds the
|||       length of the input
||| @ subject The string to return a portion of
public export
substr : (index : Nat) -> (len : Nat) -> (subject : String) -> String
substr s e subj
    = if natToInteger s < natToInteger (length subj)
         then prim__strSubstr (prim__cast_IntegerInt (natToInteger s))
                              (prim__cast_IntegerInt (natToInteger e))
                              subj
         else ""

||| Adds a character to the front of the specified string.
|||
||| ```idris example
||| strCons 'A' "B"
||| ```
||| ```idris example
||| strCons 'A' ""
||| ```
public export
strCons : Char -> String -> String
strCons = prim__strCons

public export
strUncons : String -> Maybe (Char, String)
strUncons "" = Nothing
strUncons str = assert_total $ Just (prim__strHead str, prim__strTail str)

||| Turns a list of characters into a string.
public export
pack : List Char -> String
pack [] = ""
pack (x :: xs) = strCons x (pack xs)

%foreign
    "scheme:string-pack"
    "RefC:fastPack"
    "javascript:lambda:(xs)=>''.concat(...__prim_idris2js_array(xs))"
    "jvm:pack(io/github/mmhelloworld/idrisjvm/runtime/IdrisList java/lang/String),io/github/mmhelloworld/idrisjvm/runtime/Strings"
export
fastPack : List Char -> String

-- always use 'fastPack' at run time
%transform "fastPack" pack = fastPack

||| Turns a string into a list of characters.
|||
||| ```idris example
||| unpack "ABC"
||| ```
public export
unpack : String -> List Char
unpack str = unpack' (prim__cast_IntegerInt (natToInteger (length str)) - 1) str []
  where
    unpack' : Int -> String -> List Char -> List Char
    unpack' pos str acc
        = if pos < 0
             then acc
             else unpack' (assert_smaller pos (pos - 1)) str $ (assert_total $ prim__strIndex str pos) :: acc

-- This function runs fast when compiled but won't compute at compile time.
-- If you need to unpack strings at compile time, use Prelude.unpack.
%foreign
  "scheme:string-unpack"
  "RefC:fastUnpack"
  "javascript:lambda:(str)=>__prim_js2idris_array(Array.from(str))"
  "jvm:unpack(java/lang/String io/github/mmhelloworld/idrisjvm/runtime/IdrisList),io/github/mmhelloworld/idrisjvm/runtime/Strings"
export
fastUnpack : String -> List Char

-- always use 'fastPack' at run time
%transform "fastUnpack" unpack = fastUnpack

public export
Semigroup String where
  (<+>) = (++)

public export
Monoid String where
  neutral = ""

----------------
-- CHARACTERS --
----------------

||| Returns true if the character is in the range [A-Z].
public export
isUpper : Char -> Bool
isUpper x = x >= 'A' && x <= 'Z'

||| Returns true if the character is in the range [a-z].
public export
isLower : Char -> Bool
isLower x = x >= 'a' && x <= 'z'

||| Returns true if the character is in the ranges [A-Z][a-z].
public export
isAlpha : Char -> Bool
isAlpha x = isUpper x || isLower x

||| Returns true if the character is in the range [0-9].
public export
isDigit : Char -> Bool
isDigit x = (x >= '0' && x <= '9')

||| Returns true if the character is in the ranges [A-Z][a-z][0-9].
public export
isAlphaNum : Char -> Bool
isAlphaNum x = isDigit x || isAlpha x

||| Returns true if the character is a whitespace character.
public export
isSpace : Char -> Bool
isSpace x
    = x == ' '  || x == '\t' || x == '\r' ||
      x == '\n' || x == '\f' || x == '\v' ||
      x == '\xa0'

||| Returns true if the character represents a new line.
public export
isNL : Char -> Bool
isNL x = x == '\r' || x == '\n'

||| Convert a letter to the corresponding upper-case letter, if any.
||| Non-letters are ignored.
public export
toUpper : Char -> Char
toUpper x
    = if (isLower x)
         then prim__cast_IntChar (prim__cast_CharInt x - 32)
         else x

||| Convert a letter to the corresponding lower-case letter, if any.
||| Non-letters are ignored.
public export
toLower : Char -> Char
toLower x
    = if (isUpper x)
         then prim__cast_IntChar (prim__cast_CharInt x + 32)
         else x

||| Returns true if the character is a hexadecimal digit i.e. in the range
||| [0-9][a-f][A-F].
public export
isHexDigit : Char -> Bool
isHexDigit x = elem (toUpper x) hexChars where
  hexChars : List Char
  hexChars
      = ['0', '1', '2', '3', '4', '5', '6', '7', '8', '9',
         'A', 'B', 'C', 'D', 'E', 'F']

||| Returns true if the character is an octal digit.
public export
isOctDigit : Char -> Bool
isOctDigit x = (x >= '0' && x <= '7')

||| Returns true if the character is a control character.
public export
isControl : Char -> Bool
isControl x
    = (x >= '\x0000' && x <= '\x001f')
       || (x >= '\x007f' && x <= '\x009f')

||| Convert the number to its backend dependent (usually Unicode) Char
||| equivalent.
public export
chr : Int -> Char
chr = prim__cast_IntChar

||| Return the backend dependent (usually Unicode) numerical equivalent of the Char.
public export
ord : Char -> Int
ord = prim__cast_CharInt

-----------------------
-- DOUBLE PRIMITIVES --
-----------------------

public export
pi : Double
pi = 3.14159265358979323846

public export
euler : Double
euler = 2.7182818284590452354

public export
exp : Double -> Double
exp x = prim__doubleExp x

public export
log : Double -> Double
log x = prim__doubleLog x

public export
pow : Double -> Double -> Double
pow x y = exp (y * log x) -- prim__doublePow x y

public export
sin : Double -> Double
sin x = prim__doubleSin x

public export
cos : Double -> Double
cos x = prim__doubleCos x

public export
tan : Double -> Double
tan x = prim__doubleTan x

public export
asin : Double -> Double
asin x = prim__doubleASin x

public export
acos : Double -> Double
acos x = prim__doubleACos x

public export
atan : Double -> Double
atan x = prim__doubleATan x

public export
sinh : Double -> Double
sinh x = (exp x - exp (-x)) / 2

public export
cosh : Double -> Double
cosh x = (exp x + exp (-x)) / 2

public export
tanh : Double -> Double
tanh x = sinh x / cosh x

public export
sqrt : Double -> Double
sqrt x = prim__doubleSqrt x

public export
floor : Double -> Double
floor x = prim__doubleFloor x

public export
ceiling : Double -> Double
ceiling x = prim__doubleCeiling x

------------
-- RANGES --
------------

-- These functions are here to support the range syntax:
-- range expressions like `[a..b]` are desugared to `rangeFromXXX` calls.

public export
countFrom : n -> (n -> n) -> Stream n
countFrom start diff = start :: countFrom (diff start) diff

public export
covering
takeUntil : (n -> Bool) -> Stream n -> List n
takeUntil p (x :: xs)
    = if p x
         then [x]
         else x :: takeUntil p xs

public export
covering
takeBefore : (n -> Bool) -> Stream n -> List n
takeBefore p (x :: xs)
    = if p x
         then []
         else x :: takeBefore p xs

public export
interface Range a where
  constructor MkRange
  rangeFromTo : a -> a -> List a
  rangeFromThenTo : a -> a -> a -> List a

  rangeFrom : a -> Stream a
  rangeFromThen : a -> a -> Stream a

-- Idris 1 went to great lengths to prove that these were total. I don't really
-- think it's worth going to those lengths! Let's keep it simple and assert.
public export
Range Nat where
  rangeFromTo x y = case compare x y of
    LT => assert_total $ takeUntil (>= y) (countFrom x S)
    EQ => pure x
    GT => assert_total $ takeUntil (<= y) (countFrom x (\n => minus n 1))
  rangeFromThenTo x y z = case compare x y of
    LT => if z >= x
             then assert_total $ takeBefore (> z) (countFrom x (plus (minus y x)))
             else Nil
    EQ => if x == z then pure x else Nil
    GT => assert_total $ takeBefore (< z) (countFrom x (\n => minus n (minus x y)))
  rangeFrom x = countFrom x S
  rangeFromThen x y
      = if y > x
           then countFrom x (plus (minus y x))
           else countFrom x (\n => minus n (minus x y))

public export
(Integral a, Ord a, Neg a) => Range a where
  rangeFromTo x y = case compare x y of
    LT => assert_total $ takeUntil (>= y) (countFrom x (+1))
    EQ => pure x
    GT => assert_total $ takeUntil (<= y) (countFrom x (\x => x-1))
  rangeFromThenTo x y z = case compare (z - x) (z - y) of
    -- Go down
    LT => assert_total $ takeBefore (< z) (countFrom x (\n => n - (x - y)))
    -- Meaningless
    EQ => if x == y && y == z then pure x else Nil
    -- Go up
    GT => assert_total $ takeBefore (> z) (countFrom x (+ (y-x)))
  rangeFrom x = countFrom x (1+)
  rangeFromThen x y
      = if y > x
           then countFrom x (+ (y - x))
           else countFrom x (\n => n - (x - y))


text:
module Protocol.IDE.Command
import Protocol.SExp

%default total

-- TODO: introduce SExpable DocMode and refactor below to use it
public export
data DocMode = Overview | Full

public export
record Hints where
  constructor MkHints
  list : List String

export
SExpable Hints where
  toSExp hs = toSExp hs.list

export
FromSExpable Hints where
  fromSExp hs = MkHints <$> fromSExp hs

public export
data IDECommand
     = Interpret String
     | LoadFile String (Maybe Integer)
     | TypeOf String (Maybe (Integer, Integer))
     | NameAt String (Maybe (Integer, Integer))
     | CaseSplit Integer Integer String
     | AddClause Integer String
     -- deprecated: | AddProofClause
     | AddMissing Integer String
     | ExprSearch Integer String Hints Bool
     | ExprSearchNext
     | GenerateDef Integer String
     | GenerateDefNext
     | MakeLemma Integer String
     | MakeCase Integer String
     | MakeWith Integer String
     | DocsFor String (Maybe DocMode)
     | Directive String
     | Apropos String
     | Metavariables Integer
     | WhoCalls String
     | CallsWho String
     | BrowseNamespace String
     | NormaliseTerm     String -- TODO: implement a Binary lib
     | ShowTermImplicits String -- and implement Binary (Term)
     | HideTermImplicits String -- for these four defintions,
     | ElaborateTerm     String -- then change String to Term, as in idris1
     | PrintDefinition String
     | ReplCompletions String
     | EnableSyntax Bool
     | Version
     | GetOptions

getIDECommand : SExp -> Maybe IDECommand
getIDECommand (SExpList [SymbolAtom "interpret", StringAtom cmd])
    = Just $ Interpret cmd
getIDECommand (SExpList [SymbolAtom "load-file", StringAtom fname])
    = Just $ LoadFile fname Nothing
getIDECommand (SExpList [SymbolAtom "load-file", StringAtom fname, IntegerAtom l])
    = Just $ LoadFile fname (Just l)
getIDECommand (SExpList [SymbolAtom "type-of", StringAtom n])
    = Just $ TypeOf n Nothing
getIDECommand (SExpList [SymbolAtom "type-of", StringAtom n,
                         IntegerAtom l, IntegerAtom c])
    = Just $ TypeOf n (Just (l, c))
getIDECommand (SExpList [SymbolAtom "name-at", StringAtom n])
    = Just $ NameAt n Nothing
getIDECommand (SExpList [SymbolAtom "name-at", StringAtom n,
                         IntegerAtom l, IntegerAtom c])
    = Just $ NameAt n (Just (l, c))
getIDECommand (SExpList [SymbolAtom "case-split", IntegerAtom l, IntegerAtom c,
                         StringAtom n])
    = Just $ CaseSplit l c n
getIDECommand (SExpList [SymbolAtom "case-split", IntegerAtom l, StringAtom n])
    = Just $ CaseSplit l 0 n
getIDECommand (SExpList [SymbolAtom "add-clause", IntegerAtom l, StringAtom n])
    = Just $ AddClause l n
getIDECommand (SExpList [SymbolAtom "add-missing", IntegerAtom line, StringAtom n])
    = Just $ AddMissing line n
getIDECommand (SExpList [SymbolAtom "proof-search", IntegerAtom l, StringAtom n])
    = Just $ ExprSearch l n (MkHints []) False
getIDECommand (SExpList [SymbolAtom "proof-search", IntegerAtom l, StringAtom n, hs])
    = (\hs' => ExprSearch l n hs' False) <$> fromSExp hs
getIDECommand (SExpList [SymbolAtom "proof-search", IntegerAtom l, StringAtom n, hs, SymbolAtom mode])
    = (\hs' => ExprSearch l n hs' (getMode mode)) <$> fromSExp hs
  where
    getMode : String -> Bool
    getMode m = m == "all"
getIDECommand (SymbolAtom "proof-search-next") = Just ExprSearchNext
getIDECommand (SExpList [SymbolAtom "generate-def", IntegerAtom l, StringAtom n])
    = Just $ GenerateDef l n
getIDECommand (SymbolAtom "generate-def-next") = Just GenerateDefNext
getIDECommand (SExpList [SymbolAtom "make-lemma", IntegerAtom l, StringAtom n])
    = Just $ MakeLemma l n
getIDECommand (SExpList [SymbolAtom "make-case", IntegerAtom l, StringAtom n])
    = Just $ MakeCase l n
getIDECommand (SExpList [SymbolAtom "make-with", IntegerAtom l, StringAtom n])
    = Just $ MakeWith l n
getIDECommand (SExpList (SymbolAtom "docs-for" ::  StringAtom n :: modeTail))
    = do -- Maybe monad
         modeOpt <- case modeTail of
                      []                      => Just Nothing
                      [SymbolAtom "overview"] => Just $ Just Overview
                      [SymbolAtom "full"    ] => Just $ Just Full
                      _ => Nothing
         Just $ DocsFor n modeOpt
getIDECommand (SExpList [SymbolAtom "apropos", StringAtom n])
    = Just $ Apropos n
getIDECommand (SExpList [SymbolAtom "directive", StringAtom n])
    = Just $ Directive n
getIDECommand (SExpList [SymbolAtom "metavariables", IntegerAtom n])
    = Just $ Metavariables n
getIDECommand (SExpList [SymbolAtom "who-calls", StringAtom n])
    = Just $ WhoCalls n
getIDECommand (SExpList [SymbolAtom "calls-who", StringAtom n])
    = Just $ CallsWho n
getIDECommand (SExpList [SymbolAtom "browse-namespace", StringAtom ns])
    = Just $ BrowseNamespace ns
getIDECommand (SExpList [SymbolAtom "normalise-term", StringAtom tm])
    = Just $ NormaliseTerm     tm
getIDECommand (SExpList [SymbolAtom "show-term-implicits", StringAtom tm])
    = Just $ ShowTermImplicits tm
getIDECommand (SExpList [SymbolAtom "hide-term-implicits", StringAtom tm])
    = Just $ HideTermImplicits tm
getIDECommand (SExpList [SymbolAtom "elaborate-term", StringAtom tm])
    = Just $ ElaborateTerm     tm
getIDECommand (SExpList [SymbolAtom "print-definition", StringAtom n])
    = Just $ PrintDefinition n
getIDECommand (SExpList [SymbolAtom "repl-completions", StringAtom n])
    = Just $ ReplCompletions n
getIDECommand (SExpList [SymbolAtom "enable-syntax", BoolAtom b])
    = Just $ EnableSyntax b
getIDECommand (SymbolAtom "version") = Just Version
getIDECommand (SExpList [SymbolAtom "get-options"]) = Just GetOptions
getIDECommand _ = Nothing

export
FromSExpable IDECommand where
  fromSExp = getIDECommand

putIDECommand : IDECommand -> SExp
putIDECommand (Interpret cmd)                 = (SExpList [SymbolAtom "interpret", StringAtom cmd])
putIDECommand (LoadFile fname Nothing)        = (SExpList [SymbolAtom "load-file", StringAtom fname])
putIDECommand (LoadFile fname (Just line))    = (SExpList [SymbolAtom "load-file", StringAtom fname, IntegerAtom line])
putIDECommand (TypeOf cmd Nothing)            = (SExpList [SymbolAtom "type-of", StringAtom cmd])
putIDECommand (TypeOf cmd (Just (line, col))) = (SExpList [SymbolAtom "type-of", StringAtom cmd, IntegerAtom line, IntegerAtom col])
putIDECommand (NameAt cmd Nothing)            = (SExpList [SymbolAtom "name-at", StringAtom cmd])
putIDECommand (NameAt cmd (Just (line, col))) = (SExpList [SymbolAtom "name-at", StringAtom cmd, IntegerAtom line, IntegerAtom col])
putIDECommand (CaseSplit line col n)          = (SExpList [SymbolAtom "case-split", IntegerAtom line, IntegerAtom col, StringAtom n])
putIDECommand (AddClause line n)              = (SExpList [SymbolAtom "add-clause", IntegerAtom line, StringAtom n])
putIDECommand (AddMissing line n)             = (SExpList [SymbolAtom "add-missing", IntegerAtom line, StringAtom n])
putIDECommand (ExprSearch line n hints mode)  = (SExpList [SymbolAtom "proof-search", IntegerAtom line, StringAtom n, toSExp hints, getMode mode])
  where
  getMode : Bool -> SExp
  getMode True  = SymbolAtom "all"
  getMode False = SymbolAtom "other"
putIDECommand ExprSearchNext                  = SymbolAtom "proof-search-next"
putIDECommand (GenerateDef line n)            = (SExpList [SymbolAtom "generate-def", IntegerAtom line, StringAtom n])
putIDECommand GenerateDefNext                 = SymbolAtom "generate-def-next"
putIDECommand (MakeLemma line n)              = (SExpList [SymbolAtom "make-lemma", IntegerAtom line, StringAtom n])
putIDECommand (MakeCase line n)               = (SExpList [SymbolAtom "make-case", IntegerAtom line, StringAtom n])
putIDECommand (MakeWith line n)               = (SExpList [SymbolAtom "make-with", IntegerAtom line, StringAtom n])
putIDECommand (DocsFor n modeOpt)             = let modeTail = case modeOpt of
                                                                 Nothing       => []
                                                                 Just Overview => [SymbolAtom "overview"]
                                                                 Just Full     => [SymbolAtom "full"] in
                                                (SExpList (SymbolAtom "docs-for" ::  StringAtom n :: modeTail))
putIDECommand (Apropos n)                     = (SExpList [SymbolAtom "apropos", StringAtom n])
putIDECommand (Metavariables n)               = (SExpList [SymbolAtom "metavariables", IntegerAtom n])
putIDECommand (WhoCalls n)                    = (SExpList [SymbolAtom "who-calls", StringAtom n])
putIDECommand (CallsWho n)                    = (SExpList [SymbolAtom "calls-who", StringAtom n])
putIDECommand (BrowseNamespace ns)            = (SExpList [SymbolAtom "browse-namespace", StringAtom ns])
putIDECommand (NormaliseTerm     tm)          = (SExpList [SymbolAtom "normalise-term", StringAtom tm])
putIDECommand (ShowTermImplicits tm)          = (SExpList [SymbolAtom "show-term-implicits", StringAtom tm])
putIDECommand (HideTermImplicits tm)          = (SExpList [SymbolAtom "hide-term-implicits", StringAtom tm])
putIDECommand (ElaborateTerm     tm)          = (SExpList [SymbolAtom "elaborate-term", StringAtom tm])
putIDECommand (PrintDefinition n)             = (SExpList [SymbolAtom "print-definition", StringAtom n])
putIDECommand (ReplCompletions n)             = (SExpList [SymbolAtom "repl-completions", StringAtom n])
putIDECommand (Directive n)             = (SExpList [SymbolAtom "directive", StringAtom n])
putIDECommand (EnableSyntax b)                = (SExpList [SymbolAtom "enable-syntax", BoolAtom b])
putIDECommand GetOptions                      = (SExpList [SymbolAtom "get-options"])
putIDECommand Version                         = SymbolAtom "version"

export
SExpable IDECommand where
  toSExp = putIDECommand


text:
%default total

data Command : Type -> Type where
    Empty : Command ()
    Pure : t -> Command t

test : Command (List a) -> ()
test (Pure x) = ()

test2 : Command (a -> b) -> ()
test2 (Pure x) = ()

test3 : Command Type -> ()
test3 (Pure x) = ()


text:
module Idrlisp.Sexp

%default total

public export
data Sexp : Type -> Type where
  Num : Double -> Sexp a
  Sym : String -> Sexp a
  Str : String -> Sexp a -- For now we don't treat idrlisp strings as byte sequences.
  Bool : Bool -> Sexp a
  Nil : Sexp a
  (::) : (car : Sexp a) -> (cdr : Sexp a) -> Sexp a
  Pure : a -> Sexp a

public export
data SList a
  = Proper (List (Sexp a))
  | Improper (Sexp a)

namespace Syntax
  infixr 6 :.:

  public export
  data SSyn : Type -> Type where
    Num : Double -> SSyn a
    Sym : String -> SSyn a
    Str : String -> SSyn a
    Bool : Bool -> SSyn a
    Nil : SSyn a
    Quote : SSyn a -> SSyn a
    Quasiquote : SSyn a -> SSyn a
    Unquote : SSyn a -> SSyn a
    UnquoteSplicing : SSyn a -> SSyn a
    App : (xs : List (SSyn a)) -> {auto ok : NonEmpty xs} -> SSyn a
    (:.:) : (xs : List (SSyn a)) -> {auto ok : NonEmpty xs} -> SSyn a -> SSyn a
    Pure : a -> SSyn a

export
Eq a => Eq (Sexp a) where
  (==) (Num x) (Num y) = x == y
  (==) (Sym x) (Sym y) = x == y
  (==) (Str x) (Str y) = x == y
  (==) (Bool x) (Bool y) = x == y
  (==) Nil Nil = True
  (==) (x :: x') (y :: y') = x == y && x' == y'
  (==) (Pure x) (Pure y) = x == y
  (==) _ _ = False

export
Eq a => Eq (SList a) where
  (==) (Proper xs) (Proper ys) = xs == ys
  (==) (Improper x) (Improper y) = x == y
  (==) _ _ = False

export
Eq a => Eq (SSyn a) where
  x == y = assert_total (eq x y)
    where
      covering
      eq : SSyn a -> SSyn a -> Bool
      eq (Num x) (Num y) = x == y
      eq (Sym x) (Sym y) = x == y
      eq (Str x) (Str y) = x == y
      eq (Bool x) (Bool y) = x == y
      eq Nil Nil = True
      eq (Quote x) (Quote y) = x == y
      eq (Quasiquote x) (Quasiquote y) = x == y
      eq (Unquote x) (Unquote y) = x == y
      eq (UnquoteSplicing x) (UnquoteSplicing y) = x == y
      eq (App xs) (App ys) = xs == ys
      eq (xs :.: x) (ys :.: y) = xs == ys && x == y
      eq (Pure x) (Pure y) = x == y
      eq _ _ = False

export
Functor Sexp where
  map f (Num x) = Num x
  map f (Sym x) = Sym x
  map f (Str x) = Str x
  map f (Bool x) = Bool x
  map f [] = []
  map f (car :: cdr) = map f car :: map f cdr
  map f (Pure x) = Pure (f x)

export
Foldable Sexp where
  foldr f init (Num x) = init
  foldr f init (Sym x) = init
  foldr f init (Str x) = init
  foldr f init (Bool x) = init
  foldr f init [] = init
  foldr f init (car :: cdr) = foldr f (foldr f init cdr) car
  foldr f init (Pure x) = f x init

export
Traversable Sexp where
  traverse f (Num x) = pure $ Num x
  traverse f (Sym x) = pure $ Sym x
  traverse f (Str x) = pure $ Str x
  traverse f (Bool x) = pure $ Bool x
  traverse f [] = pure []
  traverse f (car :: cdr) = (::) <$> traverse f car <*> traverse f cdr
  traverse f (Pure x) = Pure <$> f x

export
Cast (Sexp a) (SList a) where
  cast (x :: xs) with (cast {to = SList a} xs)
    | Proper xs' = Proper (x :: xs')
    | Improper xs' = Improper (x :: xs')
  cast [] = Proper []
  cast x = Improper x

export
Cast (SList a) (Sexp a) where
  cast (Proper xs) = foldr (::) Nil xs
  cast (Improper x) = x

export
Cast (Sexp a) (SSyn a) where
  cast x = assert_total (cast x)
    where
      covering
      cast : Sexp a -> SSyn a
      cast (Num x) = Num x
      cast (Sym x) = Sym x
      cast (Str x) = Str x
      cast (Bool x) = Bool x
      cast Nil = Nil
      cast [Sym "quote", x] = Quote (cast x)
      cast [Sym "quasiquote", x] = Quasiquote (cast x)
      cast [Sym "unquote", x] = Unquote (cast x)
      cast [Sym "unquote-splicing", x] = UnquoteSplicing (cast x)
      cast (x :: y) with (cast y)
        | App ys = App (cast x :: ys)
        | Nil = App [cast x]
        | (ys :.: z) = cast x :: ys :.: z
        | y' = [cast x] :.: y'
      cast (Pure x) = Pure x

export
Cast (SSyn a) (Sexp a) where
  cast x = assert_total (cast x)
    where
      covering
      cast : SSyn a -> Sexp a
      cast (Num x) = Num x
      cast (Sym x) = Sym x
      cast (Str x) = Str x
      cast (Bool x) = Bool x
      cast Nil = Nil
      cast (Quote x) = [Sym "quote", cast x]
      cast (Quasiquote x) = [Sym "quasiquote", cast x]
      cast (Unquote x) = [Sym "unquote", cast x]
      cast (UnquoteSplicing x) = [Sym "unquote-splicing", cast x]
      cast (App xs) = foldr (::) Nil (map cast xs)
      cast (xs :.: x) = foldr (::) (cast x) (map cast xs)
      cast (Pure x) = Pure x

export
Show a => Show (SSyn a) where
  show x = assert_total (show' x)
    where
      covering
      show' : SSyn a -> String
      show' (Num x) = show x
      show' (Sym x) = x
      show' (Str x) = show x
      show' (Bool x) = if x then "#t" else "#f"
      show' Nil = "()"
      show' (Quote x) = "'" ++ show x
      show' (Quasiquote x) = "`" ++ show x
      show' (Unquote x) = "," ++ show x
      show' (UnquoteSplicing x) = ",@" ++ show x
      show' (App xs) = "(" ++ unwords (map show xs) ++ ")"
      show' (xs :.: x) = "(" ++ unwords (map show xs) ++ " . " ++ show x ++ ")"
      show' (Pure x) = show x

export
Show a => Show (Sexp a) where
  show x = show (the (SSyn a) (cast x))

export
Show a => Show (SList a) where
  show x = show (the (Sexp a) (cast x))

max_stars_repo_name: yubrot/idrlisp

max_issues_repo_name: yubrot/idrlisp

max_forks_repo_name: yubrot/idrlisp


text:
||| An open union implementation as first introduced
||| in chapter *Predicates and Proof Search*
module Data.Union

import Data.Vect

%default total

--------------------------------------------------------------------------------
--          Predicates
--------------------------------------------------------------------------------

||| Predicate witnessing that a value is an element
||| of a vector.
public export
data Has : (v : a) -> (vs : Vect n a) -> Type where
  Z : Has v (v :: vs)
  S : Has v vs -> Has v (w :: vs)

||| Predicate witnessing that a value is an element
||| of a vector and listing the result of removing
||| said element from the vector.
public export
data Rem : (v : a) -> (vs : Vect (S n) a) -> (rem : Vect n a) -> Type where
  [search v vs]
  RZ : Rem v (v :: vs) vs
  RS : Rem v vs rem -> Rem v (w :: vs) (w :: rem)

--------------------------------------------------------------------------------
--          Union
--------------------------------------------------------------------------------

||| An *open union*, holding a single value of one
||| of the types listed in the index.
public export
data Union : (ts : Vect n Type) -> Type where
  U : (prf : Has t ts) -> (v : t) -> Union ts

||| Inject a value into an open union.
public export
inj : (v : t) -> Has t ts => Union ts
inj v = U %search v

--------------------------------------------------------------------------------
--          Decomposing Unions
--------------------------------------------------------------------------------

projImpl : Has t1 ts -> Has t2 ts -> t2 -> Maybe t1
projImpl Z     Z     v = Just v
projImpl (S x) (S y) v = projImpl x y v
projImpl Z     (S _) _ = Nothing
projImpl (S _)  Z    _ = Nothing

||| Try to extract a value of the given type
||| from a union.
public export
proj : (0 t : Type) -> Has t ts => Union ts -> Maybe t
proj _ (U ix v) = projImpl %search ix v

||| Like `proj` but with an implicit type argument.
public export
proj' : Has t ts => Union ts -> Maybe t
proj' = proj t

||| Decomposes a union: Either returns a value
||| of the given type or a new union where the
||| given type is no longer in the index.
public export
decomp :  (0 t : Type)
       -> (prf : Rem t ts rem )
       => Union ts
       -> Either t (Union rem)
decomp _ {prf = RZ}   (U Z v)     = Left v
decomp _ {prf = RZ}   (U (S x) v) = Right (U x v)
decomp _ {prf = RS x} (U Z v)     = Right (U Z v)
decomp t {prf = RS x} (U (S y) v) = case decomp t (U y v) of
  Left z          => Left z
  Right (U prf z) => Right (U (S prf) z)

||| Like `decomp` but with an implicit type argument.
public export
decomp' : Rem t ts rem => Union ts -> Either t (Union rem)
decomp' = decomp t

--------------------------------------------------------------------------------
--          Embedding Unions
--------------------------------------------------------------------------------

extendHasR : Has v vs -> Has v (vs ++ r)
extendHasR Z     = Z
extendHasR (S x) = S (extendHasR x)

||| Extends a union by appending additional types
||| to the list of possibilities.
public export
extendR : Union ts -> Union (ts ++ r)
extendR (U prf v) = U (extendHasR prf) v

extendHasL : {n : _} -> {0 r : Vect n _} -> Has v vs -> Has v (r ++ vs)
extendHasL {n = Z}   {r = []}     prf = prf
extendHasL {n = S k} {r = _ :: _} prf = S (extendHasL prf)

||| Extends a union by prepending additional types
||| to the list of possibilities. In order to implement this,
||| we need to shift the current index, therefore the
||| number of new types must be known a runtime.
public export
extendL : {n : _} -> {0 r : Vect n _} -> Union ts -> Union (r ++ ts)
extendL (U prf v) = U (extendHasL prf) v


text:
NatOrError : Nat -> Type
NatOrError Z = String
NatOrError (S k) = Nat

divide : (x:Nat) -> (y:Nat) -> NatOrError y
divide x Z = "Error: Division by zero"
divide x (S k) = div x (S k)


text:
module Term

-- Untyped lambda calculus with built-in natural numbers.
--
-- Note that variables in the lambda calculus are not
-- named but identified by their de Bruijn index.

import Data.Fin
import public Data.Vect

%default total
%access public export

--------------------------------------
-- Begin: TERMS OF THE LAMBDA CALCULUS

-- Data type of well-scoped terms
-- in the lambda calculus:
data Term : Nat -> Type where
  -- Variable:
  -- The data constructor for variables ('Var') takes
  -- as arguments a de Bruijn index ('i').
  TVar  : (i : Fin n) -> Term n
  -- Abstraction:
  TAbs  : Term (S n) -> Term n
  -- Application:
  TApp  : Term n -> Term n -> Term n
  -- Constant 'Zero' (natural number):
  TZero : Term n
  -- Successor:
  TSucc : Term n -> Term n
  -- Predecessor:
  TPred : Term n -> Term n
  -- Test for equality with 'Zero'
  -- (with terms for the "then" and
  -- "else" branches):
  TIfz  : Term n -> Term n -> Term n ->
          Term n

-- End: TERMS OF THE LAMBDA CALCULUS
------------------------------------

---------------------------------------
-- Begin: VALUES IN THE LAMBDA CALCULUS

-- The following lambda calculus terms
-- are values (i.e. normal forms for
-- reduction under the "Step" relation):
--   (1) lambda abstractions (that are
--       not applied),
--   (2) the constant 'Zero',
--   (3) the natural number constants
--       (formed by applying 'Succ' to
--       another value).
data Value : Term 0 -> Type where
  VZero : Value TZero
  VSucc : Value e -> Value (TSucc e)
  VAbs  : Value (TAbs e)

valueTerm : {e : Term 0} -> Value e -> Term 0
valueTerm {e = e} _ = e

-- End: VALUES IN THE LAMBDA CALCULUS
-------------------------------------

max_stars_repo_name: normanrink/PCF

max_issues_repo_name: normanrink/PCF

max_forks_repo_name: normanrink/PCF


text:
nth_error : (l : List Nat) -> (n : Nat) -> Maybe Nat
nth_error [] n = Nothing
nth_error (x :: xs) n =
    case n == 0 of
        True => Just x
        False => nth_error xs (pred n)

test_nth_error1 : nth_error [4, 5, 6, 7] 0 = Just 4
test_nth_error1 = Refl

test_nth_error2 : nth_error [4, 5, 6, 7] 3 = Just 7
test_nth_error2 = Refl

test_nth_error3 : nth_error [4, 5, 6, 7] 9 = Nothing
test_nth_error3 = Refl

option_elim : (default : Nat) -> (o : Maybe Nat) -> Nat
option_elim default Nothing = default
option_elim default (Just x) = x

hd_error : (l : List Nat) -> Maybe Nat
hd_error [] = Nothing
hd_error (x :: xs) = Just x

test_hd_error1 : hd_error [] = Nothing
test_hd_error1 = Refl

test_hd_error2 : hd_error [1] = Just 1
test_hd_error2 = Refl

test_hd_error3 : hd_error [5, 6] = Just 5
test_hd_error3 = Refl

hd : (default : Nat) -> (l : List Nat) -> Nat
hd default [] = default
hd default (x :: xs) = x

option_elim_hd : (l : List Nat) -> (default : Nat) -> hd default l = option_elim default (hd_error l)
option_elim_hd [] default = Refl
option_elim_hd (x :: xs) default = Refl