text:
= Preface

== Welcome

This electronic book is a course on _Software Foundations_, the mathematical
underpinnings of reliable software. Topics include basic concepts of logic,
computer-assisted theorem proving, the Idris programming language, functional
programming, operational semantics, Hoare logic, and static type systems. The
exposition is intended for a broad range of readers, from advanced
undergraduates to PhD students and researchers. No specific background in logic
or programming languages is assumed, though a degree of mathematical maturity
will be helpful.

The principal novelty of the course is that it is one hundred percent formalized
and machine-checked: the entire text is Literate Idris. It is intended to be
read alongside an interactive session with Idris. All the details in the text
are fully formalized in Idris, and the exercises are designed to be worked using
Idris.

The files are organized into a sequence of core chapters, covering about one
semester's worth of material and organized into a coherent linear narrative,
plus a number of "appendices" covering additional topics. All the core chapters
are suitable for both upper-level undergraduate and graduate students.

== Overview

Building reliable software is hard. The scale and complexity of modern systems,
the number of people involved in building them, and the range of demands placed
on them render it extremely difficult to build software that is even
more-or-less correct, much less 100% correct. At the same time, the increasing
degree to which information processing is woven into every aspect of society
continually amplifies the cost of bugs and insecurities.

Computer scientists and software engineers have responded to these challenges by
developing a whole host of techniques for improving software reliability,
ranging from recommendations about managing software projects and organizing
programming teams (e.g., extreme programming) to design philosophies for
libraries (e.g., model-view-controller, publish-subscribe, etc.) and programming
languages (e.g., object-oriented programming, aspect-oriented programming,
functional programming, ...) to mathematical techniques for specifying and
reasoning about properties of software and tools for helping validate these
properties.

The present course is focused on this last set of techniques. The text weaves
together five conceptual threads:

1. basic tools from _logic_ for making and justifying precise claims about
   programs;
2. the use of _proof assistants_ to construct rigorous logical arguments;

3. the idea of _functional programming_, both as a method of programming that
   simplifies reasoning about programs and as a bridge between programming and
   logic;

4. formal techniques for _reasoning about the properties of specific programs_
   (e.g., the fact that a sorting function or a compiler obeys some formal
   specification); and

5. the use of _type systems_ for establishing well-behavedness guarantees for
   _all_ programs in a given programming language (e.g., the fact that
   well-typed Java programs cannot be subverted at runtime).

Each of these topics is easily rich enough to fill a whole course in its own
right, so tackling all of them together naturally means that much will be left
unsaid. Nevertheless, we hope readers will find that the themes illuminate and
amplify each other and that bringing them together creates a foundation from
which it will be easy to dig into any of them more deeply. Some suggestions for
further reading can be found in the [Postscript] chapter. Bibliographic
information for all cited works can be found in the [Bib] chapter.

=== Logic

Logic is the field of study whose subject matter is _proofs_ -- unassailable
arguments for the truth of particular propositions. Volumes have been written
about the central role of logic in computer science. Manna and Waldinger called
it "the calculus of computer science," while Halpern et al.'s paper _On the
Unusual Effectiveness of Logic in Computer Science_ catalogs scores of ways in
which logic offers critical tools and insights. Indeed, they observe that "As a
matter of fact, logic has turned out to be significantly more effective in
computer science than it has been in mathematics. This is quite remarkable,
especially since much of the impetus for the development of logic during the
past one hundred years came from mathematics."

In particular, the fundamental notion of inductive proofs is ubiquitous in all
of computer science. You have surely seen them before, in contexts from discrete
math to analysis of algorithms, but in this course we will examine them much
more deeply than you have probably done so far.

=== Proof Assistants

The flow of ideas between logic and computer science has not been in just one
direction: CS has also made important contributions to logic. One of these has
been the development of software tools for helping construct proofs of logical
propositions. These tools fall into two broad categories:

  - _Automated theorem provers_ provide "push-button" operation: you give them a
    proposition and they return either _true_, _false_, or _ran out of time_.
    Although their capabilities are limited to fairly specific sorts of
    reasoning, they have matured tremendously in recent years and are used now
    in a huge variety of settings. Examples of such tools include SAT solvers,
    SMT solvers, and model checkers.

  - _Proof assistants_ are hybrid tools that automate the more routine aspects
    of building proofs while depending on human guidance for more difficult
    aspects. Widely used proof assistants include Isabelle, Agda, Twelf, ACL2,
    PVS, Coq, and Idris among many others.

This course is based around Coq, a proof assistant that has been under
development, mostly in France, since 1983 and that in recent years has attracted
a large community of users in both research and industry. Coq provides a rich
environment for interactive development of machine-checked formal reasoning. The
kernel of the Coq system is a simple proof-checker, which guarantees that only
correct deduction steps are performed. On top of this kernel, the Coq
environment provides high-level facilities for proof development, including
powerful tactics for constructing complex proofs semi-automatically, and a large
library of common definitions and lemmas.

Coq has been a critical enabler for a huge variety of work across computer
science and mathematics:

  - As a _platform for modeling programming languages_, it has become a standard
    tool for researchers who need to describe and reason about complex language
    definitions. It has been used, for example, to check the security of the
    JavaCard platform, obtaining the highest level of common criteria
    certification, and for formal specifications of the x86 and LLVM instruction
    sets and programming languages such as C.

  - As an _environment for developing formally certified software_, Coq has been
    used, for example, to build CompCert, a fully-verified optimizing compiler
    for C, for proving the correctness of subtle algorithms involving floating
    point numbers, and as the basis for CertiCrypt, an environment for reasoning
    about the security of cryptographic algorithms.

  - As a _realistic environment for functional programming with dependent
    types_, it has inspired numerous innovations. For example, the Ynot project
    at Harvard embedded "relational Hoare reasoning" (an extension of the _Hoare
    Logic_ we will see later in this course) in Coq.

  - As a _proof assistant for higher-order logic_, it has been used to validate
    a number of important results in mathematics. For example, its ability to
    include complex computations inside proofs made it possible to develop the
    first formally verified proof of the 4-color theorem. This proof had
    previously been controversial among mathematicians because part of it
    included checking a large number of configurations using a program. In the
    Coq formalization, everything is checked, including the correctness of the
    computational part. More recently, an even more massive effort led to a Coq
    formalization of the Feit-Thompson Theorem -- the first major step in the
    classification of finite simple groups.

By the way, in case you're wondering about the name, here's what the official
Coq web site says: "Some French computer scientists have a tradition of naming
their software as animal species: Caml, Elan, Foc or Phox are examples of this
tacit convention. In French, 'coq' means rooster, and it sounds like the
initials of the Calculus of Constructions (CoC) on which it is based." The
rooster is also the national symbol of France, and C-o-q are the first three
letters of the name of Thierry Coquand, one of Coq's early developers.

=== Functional Programming

The term _functional programming_ refers both to a collection of programming
idioms that can be used in almost any programming language and to a family of
programming languages designed to emphasize these idioms, including Haskell,
OCaml, Standard ML, F#, Scala, Scheme, Racket, Common Lisp, Clojure, Erlang,
and Coq.

Functional programming has been developed over many decades -- indeed, its roots
go back to Church's lambda-calculus, which was invented in the 1930s, before
there were even any computers! But since the early '90s it has enjoyed a surge
of interest among industrial engineers and language designers, playing a key
role in high-value systems at companies like Jane St. Capital, Microsoft,
Facebook, and Ericsson.

The most basic tenet of functional programming is that, as much as possible,
computation should be _pure_, in the sense that the only effect of execution
should be to produce a result: the computation should be free from _side
effects_ such as I/O, assignments to mutable variables, redirecting pointers,
etc. For example, whereas an _imperative_ sorting function might take a list of
numbers and rearrange its pointers to put the list in order, a pure sorting
function would take the original list and return a _new_ list containing the
same numbers in sorted order.

One significant benefit of this style of programming is that it makes programs
easier to understand and reason about. If every operation on a data structure
yields a new data structure, leaving the old one intact, then there is no need
to worry about how that structure is being shared and whether a change by one
part of the program might break an invariant that another part of the program
relies on. These considerations are particularly critical in concurrent
programs, where every piece of mutable state that is shared between threads is a
potential source of pernicious bugs. Indeed, a large part of the recent interest
in functional programming in industry is due to its simpler behavior in the
presence of concurrency.

Another reason for the current excitement about functional programming is
related to the first: functional programs are often much easier to parallelize
than their imperative counterparts. If running a computation has no effect other
than producing a result, then it does not matter _where_ it is run. Similarly,
if a data structure is never modified destructively, then it can be copied
freely, across cores or across the network. Indeed, the "Map-Reduce" idiom,
which lies at the heart of massively distributed query processors like Hadoop
and is used by Google to index the entire web is a classic example of functional
programming.

For this course, functional programming has yet another significant attraction:
it serves as a bridge between logic and computer science. Indeed, Coq itself can
be viewed as a combination of a small but extremely expressive functional
programming language plus with a set of tools for stating and proving logical
assertions. Moreover, when we come to look more closely, we find that these two
sides of Coq are actually aspects of the very same underlying machinery -- i.e.,
_proofs are programs_.

=== Program Verification

Approximately the first third of the book is devoted to developing the
conceptual framework of logic and functional programming and gaining enough
fluency with Coq to use it for modeling and reasoning about nontrivial
artifacts. From this point on, we increasingly turn our attention to two broad
topics of critical importance to the enterprise of building reliable software
(and hardware): techniques for proving specific properties of particular
_programs_ and for proving general properties of whole programming _languages_.

For both of these, the first thing we need is a way of representing programs as
mathematical objects, so we can talk about them precisely, together with ways of
describing their behavior in terms of mathematical functions or relations. Our
tools for these tasks are _abstract syntax_ and _operational semantics_, a
method of specifying programming languages by writing abstract interpreters. At
the beginning, we work with operational semantics in the so-called "big-step"
style, which leads to somewhat simpler and more readable definitions when it is
applicable. Later on, we switch to a more detailed "small-step" style, which
helps make some useful distinctions between different sorts of "nonterminating"
program behaviors and is applicable to a broader range of language features,
including concurrency.

The first programming language we consider in detail is _Imp_, a tiny toy
language capturing the core features of conventional imperative programming:
variables, assignment, conditionals, and loops. We study two different ways of
reasoning about the properties of Imp programs.

First, we consider what it means to say that two Imp programs are _equivalent_
in the intuitive sense that they yield the same behavior when started in any
initial memory state. This notion of equivalence then becomes a criterion for
judging the correctness of _metaprograms_ -- programs that manipulate other
programs, such as compilers and optimizers. We build a simple optimizer for Imp
and prove that it is correct.

Second, we develop a methodology for proving that particular Imp programs
satisfy formal specifications of their behavior. We introduce the notion of
_Hoare triples_ -- Imp programs annotated with pre- and post-conditions
describing what should be true about the memory in which they are started and
what they promise to make true about the memory in which they terminate -- and
the reasoning principles of _Hoare Logic_, a "domain-specific logic" specialized
for convenient compositional reasoning about imperative programs, with concepts
like "loop invariant" built in.

This part of the course is intended to give readers a taste of the key ideas and
mathematical tools used in a wide variety of real-world software and hardware
verification tasks.

=== Type Systems

Our final major topic, covering approximately the last third of the course, is
_type systems_, a powerful set of tools for establishing properties of _all_
programs in a given language.

Type systems are the best established and most popular example of a highly
successful class of formal verification techniques known as _lightweight formal
methods_. These are reasoning techniques of modest power -- modest enough that
automatic checkers can be built into compilers, linkers, or program analyzers
and thus be applied even by programmers unfamiliar with the underlying theories.
Other examples of lightweight formal methods include hardware and software model
checkers, contract checkers, and run-time property monitoring techniques for
detecting when some component of a system is not behaving according to
specification.

This topic brings us full circle: the language whose properties we study in this
part, the _simply typed lambda-calculus_, is essentially a simplified model of
the core of Coq itself!

=== Further Reading

This text is intended to be self contained, but readers looking for a deeper
treatment of a particular topic will find suggestions for further reading in the
[Postscript] chapter.

== Practicalities

=== Chapter Dependencies

A diagram of the dependencies between chapters and some suggested
paths through the material can be found in the file [deps.html].

=== System Requirements

Coq runs on Windows, Linux, and OS X.  You will need:

  - A current installation of Coq, available from the Coq home page. Everything
    should work with version 8.4. (Version 8.5 will _not_ work, due to a few
    incompatible changes in Coq between 8.4 and 8.5.)

  - An IDE for interacting with Coq. Currently, there are two choices:

    - Proof General is an Emacs-based IDE. It tends to be preferred by users who
      are already comfortable with Emacs. It requires a separate installation
      (google "Proof General").

    - CoqIDE is a simpler stand-alone IDE. It is distributed with Coq, so it
      should "just work" once you have Coq installed. It can also be compiled
      from scratch, but on some platforms this may involve installing additional
      packages for GUI libraries and such.

=== Exercises

Each chapter includes numerous exercises. Each is marked with a "star rating,"
which can be interpreted as follows:

  - One star: easy exercises that underscore points in the text and that, for
    most readers, should take only a minute or two. Get in the habit of working
    these as you reach them.

  - Two stars: straightforward exercises (five or ten minutes).

  - Three stars: exercises requiring a bit of thought (ten minutes to half an
    hour).

  - Four and five stars: more difficult exercises (half an hour and up).

Also, some exercises are marked "advanced", and some are marked "optional."
Doing just the non-optional, non-advanced exercises should provide good coverage
of the core material. Optional exercises provide a bit of extra practice with
key concepts and introduce secondary themes that may be of interest to some
readers. Advanced exercises are for readers who want an extra challenge (and, in
return, a deeper contact with the material).

_Please do not post solutions to the exercises in any public place_: Software
Foundations is widely used both for self-study and for university courses.
Having solutions easily available makes it much less useful for courses, which
typically have graded homework assignments. The authors especially request that
readers not post solutions to the exercises anyplace where they can be found by
search engines.

=== Downloading the Coq Files

A tar file containing the full sources for the "release version" of these notes
(as a collection of Coq scripts and HTML files) is available here:

    http://www.cis.upenn.edu/~bcpierce/sf

If you are using the notes as part of a class, you may be given access to a
locally extended version of the files, which you should use instead of the
release version.

== Translations

Thanks to the efforts of a team of volunteer translators, _Software Foundations_
can now be enjoyed in Japanese at [http://proofcafe.org/sf]. A Chinese
translation is underway.

ext: lidr

max_stars_repo_name: diseraluca/software-foundations

max_issues_repo_name: diseraluca/software-foundations

max_forks_repo_name: diseraluca/software-foundations


text:
module Control.Lens.Lens

import Control.Lens.Types
import Data.Curried
import Data.Yoneda
import Data.Morphisms

public export
lens : (s -> a) -> (s -> b -> t) -> {f : Type -> Type}
    -> Functor f => Morphism a (f b) -> Morphism s (f t)
lens sa sbt (Mor afb) = Mor (\s => sbt s <$> afb (sa s))

-- | Fuse a composition of lenses using 'Yoneda' to provide 'map' fusion.
--
-- In general, given a pair of lenses 'foo' and 'bar'
--
-- @
-- fusing (foo.bar) = foo.bar
-- @
--
-- however, @foo@ and @bar@ are either going to 'map' internally or they are trivial.
--
-- 'fusing' exploits the 'Yoneda' lemma to merge these separate uses into a single 'map'.
--
-- This is particularly effective when the choice of functor 'f' is unknown at compile
-- time or when the 'Lens' @foo.bar@ in the above description is recursive or complex
-- enough to prevent inlining.
--
-- @
-- 'fusing' :: 'Lens' s t a b -> 'Lens' s t a b
-- @
public export
fusing : { f : Type -> Type } -> Functor f => LensLike (Yoneda f) s t a b -> LensLike f s t a b
fusing t = \(Mor f) => Mor ( lowerYoneda . ( applyMor . t . Mor ) ( liftYoneda . f ) )

-- | "Fuse" a 'Traversal' by reassociating all of the '\<*\>' operations to the
-- left and fusing all of the 'fmap' calls into one. This is particularly
-- useful when constructing a 'Traversal' using operations from GHC.Generics.
--
-- Given a pair of 'Traversal's 'foo' and 'bar',
--
-- @
-- 'confusing' (foo.bar) = foo.bar
-- @
--
-- However, @foo@ and @bar@ are each going to use the 'Applicative' they are given.
--
-- 'confusing' exploits the 'Yoneda' lemma to merge their separate uses of 'fmap' into a single 'fmap'.
-- and it further exploits an interesting property of the right Kan lift (or 'Curried') to left associate
-- all of the uses of '(<*>)' to make it possible to fuse together more fmaps.
--
-- This is particularly effective when the choice of functor 'f' is unknown at compile
-- time or when the 'Traversal' @foo.bar@ in the above description is recursive or complex
-- enough to prevent inlining.
--
-- 'Control.Lens.Lens.fusing' is a version of this combinator suitable for fusing lenses.
--
-- @
-- 'confusing' :: 'Traversal' s t a b -> 'Traversal' s t a b
-- @
public export
confusing : {0 f : Type -> Type } -> Applicative f => LensLike (Curried (Yoneda f) (Yoneda f)) s t a b -> LensLike f s t a b
confusing t = \(Mor f) => Mor (lowerYoneda . lowerCurried . ( applyMor . t . Mor ) (liftCurriedYoneda . f))
  where

    yap : forall a, b. Yoneda f (a -> b) -> f a -> Yoneda f b
    yap (MkYoneda k) fa = MkYoneda (\ab_r => k (ab_r .) <*> fa)

    liftCurriedYoneda : forall a. Applicative f => f a -> Curried (Yoneda f) (Yoneda f) a
    liftCurriedYoneda fa = MkCurried (flip yap fa)

ext: idr


text:
module Control.Monad.State

import public Control.Monad.Identity
import public Control.Monad.Trans

||| A computation which runs in a context and produces an output
public export
interface Monad m => MonadState stateType (m : Type -> Type) | m where
    ||| Get the context
    get : m stateType
    ||| Write a new context/output
    put : stateType -> m ()

||| The transformer on which the State monad is based
public export
record StateT (stateType : Type) (m : Type -> Type) (a : Type) where
  constructor ST
  runStateT' : stateType -> m (stateType, a)

public export
implementation Functor f => Functor (StateT stateType f) where
    map f (ST g) = ST (\st => map (map f) (g st)) where

public export
implementation Monad f => Applicative (StateT stateType f) where
    pure x = ST (\st => pure (st, x))

    (ST f) <*> (ST a)
        = ST (\st =>
                do (r, g) <- f st
                   (t, b) <- a r
                   pure (t, g b))

public export
implementation Monad m => Monad (StateT stateType m) where
    (ST f) >>= k
        = ST (\st =>
                do (st', v) <- f st
                   let ST kv = k v
                   kv st')

public export
implementation Monad m => MonadState stateType (StateT stateType m) where
    get   = ST (\x => pure (x, x))
    put x = ST (\y => pure (x, ()))

public export
implementation MonadTrans (StateT stateType) where
    lift x
        = ST (\st =>
                do r <- x
                   pure (st, r))

public export
implementation (Monad f, Alternative f) => Alternative (StateT st f) where
    empty = lift empty
    (ST f) <|> (ST g) = ST (\st => f st <|> g st)

public export
implementation HasIO m => HasIO (StateT stateType m) where
  liftIO io = ST $ \s => liftIO $ io_bind io $ \a => pure (s, a)

||| Apply a function to modify the context of this computation
public export
modify : MonadState stateType m => (stateType -> stateType) -> m ()
modify f
    = do s <- get
         put (f s)

||| Evaluate a function in the context held by this computation
public export
gets : MonadState stateType m => (stateType -> a) -> m a
gets f
    = do s <- get
         pure (f s)

||| Unwrap and apply a StateT monad computation.
public export
%inline
runStateT : stateType -> StateT stateType m a -> m (stateType, a)
runStateT s act = runStateT' act s

||| The State monad. See the MonadState interface
public export
State : (stateType : Type) -> (ty : Type) -> Type
State = \s, a => StateT s Identity a

||| Unwrap and apply a State monad computation.
public export
runState : stateType -> StateT stateType Identity a -> (stateType, a)
runState s act = runIdentity (runStateT s act)

||| Unwrap and apply a State monad computation, but discard the final state.
public export
evalState : stateType -> State stateType a -> a
evalState s = snd . runState s

||| Unwrap and apply a State monad computation, but discard the resulting value.
public export
execState : stateType -> State stateType a -> stateType
execState s = fst . runState s


text:
> module Sigma.Sigma

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

> -- %hide Sigma
> -- %hide MkSigma

> data Sigma : (A : Type) -> (P : A -> Type) -> Type where
>   MkSigma : {A : Type} -> .{P : A -> Type} -> (x : A) -> (pf : P x) -> Sigma A P

max_stars_repo_name: zenntenn/IdrisLibs

max_issues_repo_name: zenntenn/IdrisLibs

max_forks_repo_name: zenntenn/IdrisLibs


text:
module Test.TestCTimespec

import Internal.CTimespec
import Test.TestUtil

export
testClockGetTime : IO ()
testClockGetTime = do
  t <- clock_gettime
  assertGT "testCloclGetTime" (sec t) 1595330483  (show t) -- just a sanity check to make sure C api call works

max_stars_repo_name: gdevanla/idris-time

max_issues_repo_name: gdevanla/idris-time

max_forks_repo_name: gdevanla/idris-time


text:
module Main

import Effects
import Effect.State
import Effect.Exception
import Effect.Random
import Effect.StdIO

data Expr = Var String
          | Val Integer
          | Add Expr Expr
          | Random Integer

Env : Type
Env = List (String, Integer)

-- Evaluator : Type -> Type
-- Evaluator t
--    = Eff m [EXCEPTION String, RND, STATE Env] t

eval : Expr -> Eff Integer [EXCEPTION String, STDIO, RND, STATE Env]
eval (Var x) = do vs <- get
                  case lookup x vs of
                        Nothing => raise ("No such variable " ++ x)
                        Just val => pure val
eval (Val x) = pure x
eval (Add l r) = [| eval l + eval r |]
eval (Random upper) = do val <- rndInt 0 upper
                         putStrLn (show val)
                         pure val

testExpr : Expr
testExpr = Add (Add (Var "foo") (Val 42)) (Random 100)

runEval : List (String, Integer) -> Expr -> IO Integer
runEval args expr = runInit [(), (), 123456, args] (eval expr)

main : IO ()
main = do let x = 42
          val <- runEval [("foo", x)] testExpr
          putStrLn $ "Answer: " ++ show val

max_stars_repo_name: grin-compiler/idris-grin

max_issues_repo_name: grin-compiler/idris-grin

max_forks_repo_name: grin-compiler/idris-grin


text:
every_other : Stream ty -> Stream ty
every_other (skip :: value :: xs) = value :: every_other xs

max_stars_repo_name: tekerson/type-driven-development

max_issues_repo_name: tekerson/type-driven-development

max_forks_repo_name: tekerson/type-driven-development


text:
{--
Copyright 2021 Joel Berkeley

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

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

Unless required by applicable law or agreed to in writing, software
distributed under the License is distributed on an "AS IS" BASIS,
WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
See the License for the specific language governing permissions and
limitations under the License.
--}
||| This module contains the Idris API to XLA.
module XLA.Client.XlaBuilder

import XLA.FFI
import XLA.Literal
import XLA.XlaData
import Types
import System.FFI
import Util
import Data.Vect

libxla : String -> String
libxla fname = "C:" ++ fname ++ ",libxla"

{-
 -
 - XlaBuilder
 -
 -}

XlaBuilder : Type
XlaBuilder = Struct "XlaBuilder" []

%foreign (libxla "XlaBuilder_delete")
prim__XlaBuilder_delete : XlaBuilder -> PrimIO ()

delete : XlaBuilder -> IO ()
delete = primIO . prim__XlaBuilder_delete

%foreign (libxla "XlaBuilder_new")
prim__mkXlaBuilder : String -> PrimIO XlaBuilder

%foreign (libxla "XlaBuilder_OpToString")
prim__opToString : XlaBuilder -> GCAnyPtr -> String

{-
 -
 - XlaOp
 -
 -}

%foreign (libxla "XlaOp_delete")
prim__XlaOp_delete : AnyPtr -> PrimIO ()

collectXlaOp : AnyPtr -> IO GCAnyPtr
collectXlaOp op = onCollectAny op $ primIO . prim__XlaOp_delete

%foreign (libxla "ConstantLiteral")
constantLiteral : XlaBuilder -> Literal -> AnyPtr

%foreign (libxla "Broadcast")
prim__broadcast : GCAnyPtr -> Ptr Int -> Int -> PrimIO AnyPtr

%foreign (libxla "Eq")
prim__eq : GCAnyPtr -> GCAnyPtr -> PrimIO AnyPtr

%foreign (libxla "Ne")
prim__ne : GCAnyPtr -> GCAnyPtr -> PrimIO AnyPtr

%foreign (libxla "Ge")
prim__ge : GCAnyPtr -> GCAnyPtr -> PrimIO AnyPtr

%foreign (libxla "Gt")
prim__gt : GCAnyPtr -> GCAnyPtr -> PrimIO AnyPtr

%foreign (libxla "Lt")
prim__lt : GCAnyPtr -> GCAnyPtr -> PrimIO AnyPtr

%foreign (libxla "Le")
prim__le : GCAnyPtr -> GCAnyPtr -> PrimIO AnyPtr

%foreign (libxla "Add")
prim__add : GCAnyPtr -> GCAnyPtr -> PrimIO AnyPtr

%foreign (libxla "Mul")
prim__mul : GCAnyPtr -> GCAnyPtr -> PrimIO AnyPtr

{-
 -
 - XlaOp and XlaBuilder wrapper
 -
 -}

export data RawTensor = MkRawTensor (XlaBuilder -> IO GCAnyPtr)

export
const : XLAPrimitive dtype => {rank : _} -> {shape : Shape {rank}}
    -> Array shape {dtype} -> RawTensor
const arr = MkRawTensor $ \builder =>
    do literal <- mkLiteral arr
       op <- collectXlaOp (constantLiteral builder literal)
       delete literal
       pure op

export
toString : RawTensor -> IO String
toString (MkRawTensor f) =
  do builder <- primIO (prim__mkXlaBuilder "")
     let str = prim__opToString builder !(f builder)
     delete builder
     pure str

%foreign (libxla "eval")
prim__eval : GCAnyPtr -> PrimIO Literal

export
eval : XLAPrimitive dtype => {shape : _} -> RawTensor -> IO (Array shape {dtype})
eval (MkRawTensor f) =
    do builder <- primIO (prim__mkXlaBuilder "")
       lit <- primIO $ prim__eval !(f builder)
       let arr = toArray lit
       delete lit
       delete builder
       pure arr

export
broadcast : {n : _} -> RawTensor -> Vect n Nat -> RawTensor
broadcast (MkRawTensor f) broadcast_sizes = MkRawTensor $ \builder =>
    do broadcast_sizes_ptr <- mkIntArray broadcast_sizes
       op <- primIO $ prim__broadcast !(f builder) broadcast_sizes_ptr (cast n)
       op <- collectXlaOp op
       free broadcast_sizes_ptr
       pure op

%foreign (libxla "BroadcastInDim")
prim__broadcastInDim : GCAnyPtr -> Ptr Int -> Int -> Ptr Int -> Int -> PrimIO AnyPtr

export
broadcastInDim : {r : _} -> RawTensor -> Shape {rank=r} -> Shape {rank=r} -> RawTensor
broadcastInDim (MkRawTensor f) ods bcd = MkRawTensor $ \builder =>
    do ods_ptr <- mkIntArray ods
       bcd_ptr <- mkIntArray bcd
       op <- primIO $ prim__broadcastInDim !(f builder) ods_ptr (cast r) bcd_ptr (cast r)
       op <- collectXlaOp op
       free ods_ptr
       free bcd_ptr
       pure op

binOp : (GCAnyPtr -> GCAnyPtr -> PrimIO AnyPtr) -> RawTensor -> RawTensor -> RawTensor
binOp f (MkRawTensor l) (MkRawTensor r) = MkRawTensor $ \builder =>
    do op <- primIO $ f !(l builder) !(r builder)
       collectXlaOp op

export
eq : RawTensor -> RawTensor -> RawTensor
eq = binOp prim__eq

export
ne : RawTensor -> RawTensor -> RawTensor
ne = binOp prim__ne

export
ge : RawTensor -> RawTensor -> RawTensor
ge = binOp prim__ge

export
gt : RawTensor -> RawTensor -> RawTensor
gt = binOp prim__gt

export
lt : RawTensor -> RawTensor -> RawTensor
lt = binOp prim__lt

export
le : RawTensor -> RawTensor -> RawTensor
le = binOp prim__le

export
add : RawTensor -> RawTensor -> RawTensor
add = binOp prim__add

export
mul : RawTensor -> RawTensor -> RawTensor
mul = binOp prim__mul

max_stars_repo_name: joelberkeley/spidr

max_issues_repo_name: joelberkeley/spidr

max_forks_repo_name: joelberkeley/spidr


text:
module permutation

import Data.Vect
import Data.Fin

%access public export

||| Vectors of Natural numbers
total
NatVect : Nat -> Type
NatVect n = Vect n Nat

||| The type Fin n -> Fin n
total
F_Fin : Nat -> Type
F_Fin n = (Fin n) -> (Fin n)

||| Identity function
total
Idt : (t : Type) -> t -> t
Idt s a = a

||| The type of permutation/bijection of {1,...,n}.
||| Notice that for finite sets one sided inverse is enough.
||| Also I have a strong feeling that using univalence the last part of the definition is
||| equivalent to saying that (g . f) and Idt are equivalent
total
Perm : Nat -> Type
Perm n = ( f : F_Fin n ** ( g : F_Fin n ** ((a : (Fin n)) -> ((g (f a)) = a))))

||| Second definition of perm. I have strong feeling that using univalence this is equivalent
||| to the first definition.
total
Perm2 : Nat -> Type
Perm2 n = ( f : F_Fin n ** ( g : F_Fin n ** ((g . f) = (Idt (Fin n)))))

||| Nat to Fin
total
NatToFin : (k : Nat) -> (n : Nat) -> (pf : LTE (S k) n) -> (Fin n)
NatToFin k Z pf impossible
NatToFin Z (S n) pf = FZ
NatToFin (S k) (S n) (LTESucc pf) = FS (NatToFin k n pf)

||| applying a function on Finite sets on a vector
total
applyFun : (n : Nat)  -> (k : Nat) -> (v : NatVect n) ->
           (f : F_Fin n) -> (pf : (LTE k n))
            -> (NatVect k)

applyFun n Z v f pf = []
applyFun n (S k) v f pf = reverse((Vect.index (f (NatToFin k n pf)) v) :: reverse((applyFun n k v f (prop k n pf)))) where
    prop : (a : Nat) -> (b : Nat) -> (LTE (S a) b) -> (LTE a b)
    prop Z b pf2 = LTEZero
    prop (S a) (S b) (LTESucc pf2) = LTESucc (prop a b pf2)


text:
module Cordial.Model.Common.Label

%default total
%access public export

data LabelKind = ANY | NAMED | INDEXED

||| Named labels for signals.
|||
||| @kind   The kind of label.
||| @ty The type associated with each label.
data Label : (kind : LabelKind) -> (ty : Type) -> Type where
  ||| Represents 'Any' label.
  A : Label ANY ty
  ||| Represents a 'Named' label.
  N : ty -> Label NAMED ty
  ||| Represents an indexed 'Named' label.
  I : ty -> Nat -> Label INDEXED ty

Show rTy => Show (Label kind rTy) where
  show A       = "any"
  show (N x)   = show x
  show (I x k) = show x <+> "_" <+> show k

max_stars_repo_name: border-patrol/cordial

max_issues_repo_name: border-patrol/cordial

max_forks_repo_name: border-patrol/cordial


text:
module FirUnsigned

import Bits
import Bounded
import Synchronous
import Unsigned

import Data.Vect
import Data.Bits

%access export
%default total

-- The Vect implementation of Foldable breaks a proof here...
-- Let's redefine sum for now without using fold
%hide sum
sum :  Num a => Vect n a -> a
sum [] = 0
sum (x::xs) = x + sum xs

-- Proof of distributative property for `Bounded`'s ranges.
-- Required for the readability (for the IEEE reader!) of the type of `dotProd`
dotProdDistrib : (n, w, j : Nat) -> (ws : Vect j Nat)
              -> Bounded (n * (w + sum ws)) = Bounded (n * w + n * sum ws)
dotProdDistrib n w j ws = rewrite multDistributesOverPlusRight n w (sum ws) in Refl

||| Combinatorial dot product over `Bounded`s
dotProd : (ws : Vect j Nat)
       -> Vect j (Bounded n)
       -> Bounded (n * sum ws)
dotProd {j=Z} _ _ = zeros
dotProd {j=S l} {n} (w :: ws) (x :: xs) =
  let y = add (mulConst x w) (dotProd ws xs)
  in rewrite dotProdDistrib n w l ws in y

||| Synchronous FIR over `Bounded`s
fir : (ws : Vect j Nat)
   -> Stream (Bounded n)
   -> Stream (Bounded (n * sum ws))
fir {j} ws x = liftA (dotProd ws) (window j zeros x)

||| A wrapper for `fir` using `Unsigned`s`, more familiar to most IEEE readers
firU : (ws : Vect j Nat) -> Stream (Unsigned n)
    -> Stream (Unsigned (maxToBits $ (bitsToMax n) * (sum ws)))
firU ws = map toUnsigned . fir ws . map fromUnsigned

||| Example of simulating `firU`
main : IO ()
main = do let dut = firU [1,3,2]
          let inp = map (saturate {n=4}) $ counterFrom 0
          let out = take 5 $ simulate dut inp
          putStrLn $ show out

-- Local Variables:
-- idris-load-packages: ("contrib")
-- End:


text:
module Main

import Data.List

%default total

data RegExp: Type -> Type where
  Atom: a -> RegExp a
  Disj: RegExp a -> RegExp a -> RegExp a
  Seq: RegExp a -> RegExp a -> RegExp a
  Star: RegExp a -> RegExp a
  Empty: RegExp a
  Nothing: RegExp a

data RegExpSpec: RegExp a -> List a -> Type where
  AtomSpec: (x : a) -> RegExpSpec (Atom x) [x]
  DisjSpec1: (r1 : RegExp a) ->
             (r2: RegExp a) -> (xs : List a) ->
             (RegExpSpec r1 xs) ->
             RegExpSpec (Disj r1 r2) xs
  DisjSpec2: (r1 : RegExp a) ->
             (r2: RegExp a) -> (xs : List a) ->
             (RegExpSpec r2 xs) ->
             RegExpSpec (Disj r1 r2) xs
  SeqSpec: (xs : List a) -> (ys : List a) -> (zs : List a) ->
           (r1 : RegExp a) -> (r2 : RegExp a) ->
           RegExpSpec r1 xs ->
           RegExpSpec r2 ys ->
           zs = xs ++ ys ->
           RegExpSpec (Seq r1 r2) zs
  StarSpec0: (r: RegExp a) ->
             RegExpSpec (Star r) []
  StarSpecS: (xs : List a) -> (ys : List a) ->
             (zs : List a) ->
             (r : RegExp a) ->
             RegExpSpec r xs ->
             RegExpSpec (Star r) ys ->
             (zs = xs ++ ys) ->
             RegExpSpec (Star r) zs
  EmptySpec: RegExpSpec Empty []

isEmpty : RegExp a -> RegExp a
isEmpty (Atom x) = Nothing
isEmpty (Disj x y) = Disj (isEmpty x) (isEmpty y)
isEmpty (Seq x y) = Seq (isEmpty x) (isEmpty y)
isEmpty (Star x) = Empty
isEmpty Empty = Empty
isEmpty Nothing = Nothing

atom_case : (x : a) -> RegExpSpec (Atom x) [] -> Void
atom_case _ _ impossible

disj_case : (x: RegExp a) -> (y: RegExp a) ->
            (contra1: RegExpSpec x [] -> Void) ->
            (contra2: RegExpSpec y [] -> Void) ->
            RegExpSpec (Disj x y) [] -> Void
disj_case x y contra1 contra2 (DisjSpec1 x y [] z) = contra1 z
disj_case x y contra1 contra2 (DisjSpec2 x y [] z) = contra2 z

seq_yes_case : (x : RegExp a) -> (y : RegExp a) ->
               RegExpSpec x [] -> RegExpSpec y [] ->
               RegExpSpec (Seq x y) []
seq_yes_case x y prf1 prf2 = SeqSpec [] [] [] x y prf1 prf2 Refl

about_list1 : (xs : List a) -> (ys : List a) ->
              [] = xs ++ ys -> [] = xs
about_list1 [] ys prf = Refl
about_list1 (_ :: _) _ Refl impossible

about_list2 : (xs : List a) -> (ys : List a) ->
              [] = xs ++ ys -> [] = ys
about_list2 [] [] Refl = Refl
about_list2 (_ :: _) _ Refl impossible

about_list3 : (x : a) -> (y : a) -> (xs : List a) ->
              (ys : List a) -> (zs : List a) -> x :: xs = (y :: ys) ++ zs ->
              (x = y, xs = ys ++ zs)
about_list3 y y (ys ++ zs) ys zs Refl = (Refl, Refl)

about_list4 : (x : a) -> (xs : List a) -> (ys : List a) ->
              (zs : List a) -> x :: xs = ys ++ zs ->
                Either (DPair (List a) (\ys' => (ys = x :: ys', xs = ys' ++ zs)))
                       (ys = [], zs = x :: xs)
about_list4 x xs [] zs prf = Right (Refl, sym prf)
about_list4 x xs (y :: ys) zs prf =
  let (Refl, h2) = about_list3 x y xs ys zs prf in (Left (MkDPair ys (Refl, h2)))

seq_no_case1: (x : RegExp a) -> (y : RegExp a) ->
              (RegExpSpec x [] -> Void) -> RegExpSpec (Seq x y) [] -> Void
seq_no_case1 x y f (SeqSpec xs ys [] x y z w prf) =
  let h = about_list1 xs ys prf in
  f (rewrite h in z)

seq_no_case2: (x : RegExp a) -> (y : RegExp a) ->
              (RegExpSpec y [] -> Void) -> RegExpSpec (Seq x y) [] -> Void
seq_no_case2 x y f (SeqSpec xs ys [] x y z w prf) =
  let h = about_list2 xs ys prf in
  f (rewrite h in w)

match_nothing_is_false : (xs : List a) ->
                         RegExpSpec Nothing xs -> Void
match_nothing_is_false _ _ impossible

decEmpty : (r : RegExp a) -> Dec (RegExpSpec r [])
decEmpty (Atom x) = No (atom_case x)
decEmpty (Disj x y) =
  case (decEmpty x, decEmpty y) of
    (Yes prf, _) => Yes (DisjSpec1 x y [] prf)
    (_, Yes prf) => Yes (DisjSpec2 x y [] prf)
    (No contra1, No contra2) => No (disj_case x y contra1 contra2)
decEmpty (Seq x y) =
  case (decEmpty x, decEmpty y) of
    (Yes prf1, Yes prf2) => Yes (seq_yes_case x y prf1 prf2)
    (No contra, _) => No (seq_no_case1 x y contra)
    (_, No contra) =>  No (seq_no_case2 x y contra)
decEmpty (Star x) = Yes (StarSpec0 x)
decEmpty Empty = Yes EmptySpec
decEmpty Nothing = No (match_nothing_is_false [])

derive : DecEq a => (r : RegExp a) -> (x : a) -> RegExp a
derive (Atom y) x = case decEq y x of
                      Yes _ => Empty
                      No _ => Nothing
derive (Disj y z) x = Disj (derive y x) (derive z x)
derive (Seq y z) x = Disj (Seq (derive y x) z) (Seq (isEmpty y) (derive z x))
derive (Star y) x = Seq (derive y x) (Star y)
derive Empty x = Nothing
derive Nothing x = Nothing

empty_match_implies_empty_list : RegExpSpec Empty xs -> xs = []
empty_match_implies_empty_list EmptySpec = Refl

is_empty_match_implies_empty_list :
  (r : RegExp a) ->
  (xs : List a) -> RegExpSpec (isEmpty r) xs -> xs = []
is_empty_match_implies_empty_list (Atom y) xs x =
  void (match_nothing_is_false xs x)
is_empty_match_implies_empty_list (Disj y z) xs (DisjSpec1 (isEmpty y) (isEmpty z) xs x) =
  is_empty_match_implies_empty_list y xs x
is_empty_match_implies_empty_list (Disj y z) xs (DisjSpec2 (isEmpty y) (isEmpty z) xs x) =
  is_empty_match_implies_empty_list z xs x
is_empty_match_implies_empty_list (Seq y z) xs (SeqSpec ys zs xs (isEmpty y) (isEmpty z) x w prf) =
  rewrite prf in
    (let h1 = is_empty_match_implies_empty_list y ys x
         h2 = is_empty_match_implies_empty_list z zs w
     in rewrite h1 in rewrite h2 in Refl)
is_empty_match_implies_empty_list (Star y) xs x = empty_match_implies_empty_list x
is_empty_match_implies_empty_list Empty xs x = empty_match_implies_empty_list x
is_empty_match_implies_empty_list Nothing xs x = void (match_nothing_is_false xs x)

is_empty_is_sound : (r : RegExp a) -> (xs : List a) ->
         RegExpSpec (isEmpty r) xs -> RegExpSpec r []
is_empty_is_sound (Atom y) xs x = void (match_nothing_is_false xs x)
is_empty_is_sound (Disj y z) xs (DisjSpec1 (isEmpty y) (isEmpty z) xs x) =
  let h = is_empty_is_sound y xs x in (DisjSpec1 y z [] h)
is_empty_is_sound (Disj y z) xs (DisjSpec2 (isEmpty y) (isEmpty z) xs x) =
  let h = is_empty_is_sound z xs x in (DisjSpec2 y z [] h)
is_empty_is_sound (Seq y z) xs (SeqSpec ys zs xs (isEmpty y) (isEmpty z) x w prf) =
    let h1 = is_empty_is_sound y ys x in
    let h2 = is_empty_is_sound z zs w in SeqSpec [] [] [] y z h1 h2 Refl
is_empty_is_sound (Star y) xs x = StarSpec0 y
is_empty_is_sound Empty xs x = EmptySpec
is_empty_is_sound Nothing xs x = void (match_nothing_is_false xs x)

derivative_is_sound: DecEq a => (r : RegExp a) ->
                     (x : a) -> (xs : List a) ->
                     RegExpSpec (derive r x) xs -> RegExpSpec r (x :: xs)
derivative_is_sound (Atom z) x xs y with (decEq z x)
  derivative_is_sound (Atom x) x xs y | (Yes Refl) =
    rewrite (empty_match_implies_empty_list y) in AtomSpec x
  derivative_is_sound (Atom z) x xs y | (No contra) =
    void (match_nothing_is_false xs y)
derivative_is_sound (Disj z w) x xs y =
  case y of
    (DisjSpec1 (derive z x) _ xs y) =>
      let z' = (derivative_is_sound z x xs y)
      in DisjSpec1 z w (x :: xs) z'
    (DisjSpec2 _ (derive w x) xs y) =>
      let z' = (derivative_is_sound w x xs y)
      in DisjSpec2 z w (x :: xs) z'
derivative_is_sound (Seq r1 r2) x xs (DisjSpec1 (Seq _ _) (Seq _ _) xs (SeqSpec ys zs xs _ r2 y z prf)) =
  let h' = derivative_is_sound r1 x ys y
  in rewrite prf in
  SeqSpec (x :: ys) zs (x :: ys ++ zs) r1 r2 h' z Refl
derivative_is_sound (Seq r1 r2) x xs (DisjSpec2 (Seq _ r2) (Seq _ _) xs (SeqSpec ys zs xs (isEmpty r1) _ y s prf)) =
  rewrite prf in
  rewrite (is_empty_match_implies_empty_list r1 ys y) in
  let h1 = derivative_is_sound r2 x zs s in
  let h2 = is_empty_is_sound r1 ys y in
  SeqSpec [] (x :: zs) (x :: zs) r1 r2 h2 h1 Refl
derivative_is_sound (Star z) x _ (SeqSpec xs ys zs _ (Star z) y w prf) =
  rewrite prf in
  let h = derivative_is_sound z x xs y in
  StarSpecS (x :: xs) ys (x :: xs ++ ys) z h w Refl
derivative_is_sound Empty _ _ _ impossible
derivative_is_sound Nothing _ _ _ impossible

atom_match_implies: (x : a) -> (xs : List a) ->
                    RegExpSpec (Atom x) (x :: xs) -> xs = []
atom_match_implies x [] (AtomSpec x) = Refl

atom_match_implies2: (x : a) -> (y : a) -> (xs : List a) ->
                     RegExpSpec (Atom x) (y :: xs) -> x = y
atom_match_implies2 y y [] (AtomSpec y) = Refl

cons_is_not_nil : (x : a) -> (xs : List a) -> x :: xs = [] -> Void
cons_is_not_nil _ _ Refl impossible

is_empty_is_complete : (r : RegExp a) -> RegExpSpec r [] ->
                       RegExpSpec (isEmpty r) []
is_empty_is_complete (Atom _) _ impossible
is_empty_is_complete (Disj y z) (DisjSpec1 y z [] x) =
  let h = is_empty_is_complete y x in
  DisjSpec1 (isEmpty y) (isEmpty z) [] h
is_empty_is_complete (Disj y z) (DisjSpec2 y z [] x) =
  let h = is_empty_is_complete z x in
  DisjSpec2 (isEmpty y) (isEmpty z) [] h
is_empty_is_complete (Seq y z) (SeqSpec xs ys [] y z x w prf) =
  let h1 = about_list1 xs ys prf in
  let h2 = about_list2 xs ys prf in
  let ih1 = is_empty_is_complete y (rewrite h1 in x) in
  let ih2 = is_empty_is_complete z (rewrite h2 in w) in
  SeqSpec [] [] [] (isEmpty y) (isEmpty z) ih1 ih2 Refl
is_empty_is_complete (Star y) x = EmptySpec
is_empty_is_complete Empty x = x
is_empty_is_complete Nothing x = x

append_nil_neutral : (xs : List a) -> xs ++ [] = xs
append_nil_neutral [] = Refl
append_nil_neutral (x :: xs) =
  let h = append_nil_neutral xs in
  rewrite h in Refl

about_list5 : (x : a) -> (y : a) -> (xs : List a) -> (ys : List a) -> (zs : List a) ->
              x :: xs = (y :: ys) ++ zs -> (x = y, xs = ys ++ zs)
about_list5 x _ (ys ++ zs) ys zs Refl = (Refl, Refl)

mutual {
star_case : DecEq a => (r : RegExp a) -> (x : a) ->
            (xs : List a) -> RegExpSpec (Star r) xs ->
            (xs' : List a) ->
            xs = x :: xs' ->
            RegExpSpec (Seq (derive r x) (Star r)) xs'
star_case r x [] (StarSpec0 r) = \xs', contra => void (cons_is_not_nil x xs' (sym contra))
star_case r x _ (StarSpecS [] zs _ r y z Refl) = \xs', Refl =>
  star_case r x (x :: xs') z xs' Refl
star_case r x xs (StarSpecS (w :: ys) zs xs r y z prf) = \xs', Refl =>
  let (Refl, Refl) = about_list5 x w xs' ys zs prf in
  let h = derivative_is_complete r x ys y in
  SeqSpec ys zs (ys ++ zs) (derive r x) (Star r) h z Refl

derivative_is_complete : (DecEq a) => (r : RegExp a) -> (x : a) -> (xs : List a) -> RegExpSpec r (x :: xs) -> RegExpSpec (derive r x) xs
derivative_is_complete (Atom z) x xs y with (decEq z x)
  derivative_is_complete (Atom x) x xs y | (Yes Refl) =
    rewrite (atom_match_implies x xs y) in EmptySpec
  derivative_is_complete (Atom z) x xs y | (No contra) =
   void (contra (atom_match_implies2 z x xs y))
derivative_is_complete (Disj z w) x xs (DisjSpec1 z w (x :: xs) y) =
  let h = derivative_is_complete z x xs y in
  DisjSpec1 (derive z x) (derive w x) xs h
derivative_is_complete (Disj z w) x xs (DisjSpec2 z w (x :: xs) y) =
  let h = derivative_is_complete w x xs y in
  DisjSpec2 (derive z x) (derive w x) xs h
derivative_is_complete (Seq z w) x xs (SeqSpec ys zs (x :: xs) z w y s prf) =
  case about_list4 x xs ys zs prf of
    Left (ys' ** (h1, h2)) =>
      rewrite h2 in
      let h = derivative_is_complete z x ys' (rewrite sym h1 in y) in
      DisjSpec1 (Seq (derive z x) w) (Seq (isEmpty z) (derive w x)) (ys' ++ zs)
        (SeqSpec ys' zs (ys' ++ zs) (derive z x) w h s Refl)
    Right (h1, h2) =>
      let h = derivative_is_complete w x xs (rewrite sym h2 in s) in
      DisjSpec2 (Seq (derive z x) w) (Seq (isEmpty z) (derive w x)) xs
        (SeqSpec [] xs xs (isEmpty z) (derive w x) (is_empty_is_complete z (rewrite sym h1 in y)) h Refl)
derivative_is_complete (Star r) x xs prf =
  star_case r x (x :: xs) prf xs Refl
derivative_is_complete Empty x xs y =
  let h = empty_match_implies_empty_list y in void (cons_is_not_nil x xs h)
derivative_is_complete Nothing x xs y = void (match_nothing_is_false (x :: xs) y)
}

match : DecEq a => (xs : List a) -> (r : RegExp a) -> Dec (RegExpSpec r xs)
match [] r = decEmpty r
match (x :: xs) r =
  case match xs (derive r x) of
    Yes prf => Yes (derivative_is_sound r x xs prf)
    No contra => No (contra . (derivative_is_complete r x xs))

max_stars_repo_name: MathiasVP/idris-regex

max_issues_repo_name: MathiasVP/idris-regex

max_forks_repo_name: MathiasVP/idris-regex


text:
-- examples in "Type-Driven Development with Idris"
-- chapter 13, section 1, VendingMachine part

-- check that all functions are total
%default total

VendState : Type
VendState = (Nat, Nat)

data Input = COIN
           | VEND
           | CHANGE
           | REFILL Nat

strToInput : String -> Maybe Input
strToInput "insert" = Just COIN
strToInput "vend" = Just VEND
strToInput "change" = Just CHANGE
strToInput x = if all isDigit (unpack x)
                then Just (REFILL (cast x))
                else Nothing

data MachineCmd : Type ->
                  VendState ->
                  VendState ->
                  Type where
  InsertCoin : MachineCmd () (pounds,     chocs) (S pounds,        chocs)
  Vend :       MachineCmd () (S pounds, S chocs) (  pounds,        chocs)
  GetCoins :   MachineCmd () (  pounds,   chocs) (       Z,        chocs)
  Refill :     (bars : Nat) ->
               MachineCmd () (       Z,   chocs) (       Z, bars + chocs)
  Display :    String ->
               MachineCmd ()                   s                        s
  GetInput :   MachineCmd (Maybe Input)        s                        s
  Pure :       ty -> MachineCmd ty             s                        s
  (>>=) :      MachineCmd a                   s1                       s2 ->
               (a -> MachineCmd b             s2                       s3) ->
               MachineCmd b                   s1                       s3

data MachineIO : VendState -> Type where
  Do : MachineCmd a s1 s2 ->
       (a -> Inf (MachineIO s2)) -> MachineIO s1

runMachine : MachineCmd ty inState outState -> IO ty
runMachine InsertCoin = putStrLn "Coin inserted"
runMachine Vend = putStrLn "Please take your chocolate"
runMachine {inState = (pounds, _)} GetCoins = putStrLn $ (show pounds) ++ " coins returned"
runMachine (Refill bars) = putStrLn $ "Chocolate remaining: " ++ (show bars)
runMachine (Display x) = putStrLn x
runMachine {inState = (pounds, bars)} GetInput
  = do putStrLn $ "Coins: " ++ (show pounds) ++ "; " ++
                  "Stock: " ++ (show bars)
       putStr "> "
       x <- getLine
       pure (strToInput x)
runMachine (Pure x) = pure x
runMachine (x >>= f) = do x' <- runMachine x
                          runMachine (f x')

data Fuel = Dry | More (Lazy Fuel)

partial
forever : Fuel
forever = More forever

run : Fuel -> MachineIO state -> IO ()
run (More fuel) (Do c f)
     = do res <- runMachine c
          run fuel (f res)
run Dry p = pure ()

namespace MachineDo
  (>>=) : MachineCmd a s1 s2 ->
          (a -> Inf (MachineIO s2)) -> MachineIO s1
  (>>=) = Do

mutual
  vend : MachineIO (pounds, chocs)
  vend {pounds = Z} = do Display "Insert a coin"
                         machineLoop
  vend {chocs = Z} = do Display "Out of stock"
                        machineLoop
  vend {pounds = (S k)} {chocs = (S j)} = do Vend
                                             Display "Enjoy!"
                                             machineLoop

  refill : (num : Nat) -> MachineIO (pounds, chocs)
  refill {pounds = Z} num = do Refill num
                               machineLoop
  refill {pounds = (S k)} num = do Display "Cannot refill: Coins in machine"
                                   machineLoop

  machineLoop : MachineIO (pounds, chocs)
  machineLoop =
    do Just x <- GetInput
        | Nothing => do Display "Invalid input"
                        machineLoop
       case x of
         COIN => do InsertCoin
                    machineLoop
         VEND => vend
         CHANGE => do GetCoins
                      Display "Change returned"
                      machineLoop
         REFILL num => refill num

partial
main : IO ()
main = run forever (machineLoop { pounds = 0 } { chocs = 1} )

max_stars_repo_name: pascalpoizat/idris-book

max_issues_repo_name: pascalpoizat/idris-book

max_forks_repo_name: pascalpoizat/idris-book


text:
module Language.LSP.CodeAction.CaseSplit

import Core.Context
import Core.Core
import Core.Env
import Core.Metadata
import Core.UnifyState
import Data.List1
import Data.String
import Idris.IDEMode.CaseSplit
import Idris.REPL.Opts
import Idris.Syntax
import Idris.Syntax
import Language.JSON
import Language.LSP.CodeAction
import Language.LSP.Message
import Libraries.Data.List.Extra
import Libraries.Data.PosMap
import Server.Configuration
import Server.Log
import Server.Response
import Server.Utils
import System.File
import TTImp.Interactive.CaseSplit
import TTImp.TTImp

export
caseSplit : Ref LSPConf LSPConfiguration
         => Ref MD Metadata
         => Ref Ctxt Defs
         => Ref UST UState
         => Ref Syn SyntaxInfo
         => Ref ROpts REPLOpts
         => CodeActionParams -> Core (Maybe CodeAction)
caseSplit params = do
  let True = params.range.start.line == params.range.end.line
    | _ => do logString Debug "caseSplit: start and end line were different"
              pure Nothing

  [] <- searchCache params.range CaseSplit
    | action :: _ => do logString Debug "caseSplit: found cached action"
                        pure (Just action)

  let line = params.range.start.line
  let col = params.range.start.character

  Just (loc, name) <- gets MD (findInTreeLoc (cast params.range.start) (cast params.range.end) . nameLocMap)
    | Nothing => do logString Debug "caseSplit: couldn't find name at \{show (line, col)}"
                    pure Nothing

  let find = if col > 0 then within (line, col) else onLine line

  OK splits <- getSplits (anyAt find) name
     | SplitFail err => do
        logString Debug "caseSplit: found error when splitting: \{show err}"
        pure Nothing

  lines <- updateCase splits line col
  Just original <- getSourceLine (line + 1)
    | Nothing => do logString Debug $ "caseSplit: error while fetching the referenced line"
                    pure Nothing

  let docURI = params.textDocument.uri
  let rng = MkRange (MkPosition line 0)
                    (MkPosition line (cast (length original)))
  let edit = MkTextEdit rng (unlines lines)
  let workspaceEdit = MkWorkspaceEdit
        { changes           = Just (singleton docURI [edit])
        , documentChanges   = Nothing
        , changeAnnotations = Nothing
        }
  let action = MkCodeAction
        { title       = "Case split on ?\{show name}"
        , kind        = Just RefactorRewrite
        , diagnostics = Just []
        , isPreferred = Just False
        , disabled    = Nothing
        , edit        = Just workspaceEdit
        , command     = Nothing
        , data_       = Nothing
        }
  modify LSPConf (record { cachedActions $= insert (cast loc, CaseSplit, [action]) })
  pure (Just action)


text:
{-
HOW TO:
1) install cabal and idris
2) run:
$ idris hello.idr -o hello
$ ./hello
-}

module Main

main : IO ()
main = putStrLn "Hello world"

max_stars_repo_name: PiranavanShanmugavadivelu/Hello-world

max_issues_repo_name: PiranavanShanmugavadivelu/Hello-world

max_forks_repo_name: PiranavanShanmugavadivelu/Hello-world


text:
||| Tail-call optimization.
|||
||| Here is a lengthy explanation how this works at the
||| moment. Assume the following call graph of functions f1,f2,f3,f4 all
||| calling each other in tail call position:
|||
||| ```
|||       ------------ f2 ---- f4 (result)
|||      /          /     \
||| f1 ---- f1     /       -- f1
|||      \        /
|||       -- f3 --
||| ```
|||
||| Function `tailCallGraph` creates a directed graph of all toplevel
||| function calls (incoming and outgoing) in tail-call position:
|||
||| ```idris
||| MkCallGraph $ fromList [(f1,[f1,f2,f3]),(f2,[f1,f4]),(f3,[f2])]
|||             $ fromList [(f1,[f1,f2]),(f2,[f1,f3]),(f3,[f1]),(f4,[f2])]
||| ```
|||
||| Mutually tail-recursive functions form a strongly connected
||| component in such a call graph: There is a (directed) path from every function
||| to every other function. Kosaraju's algorithm is used to identify
||| these strongly connected components by mapping every function
||| of a strongly connected component to the same representative (called `root`)
||| of its component. In the above case, this would result in a sorted
||| map of the following structure:
|||
|||
||| ```idris
||| fromList [(f1,f1),(f1,f2),(f1,f3),(f4,f4)]
||| ```idris
|||
||| As can be seen, f1,f2, and f3 all point to the same root (f1), while
||| f4 points to a different root.
|||
||| Such a tail-recursive call graph is now converted to an imperative
||| loop as follows: Let `obj0={h:0, a1:...}` be a Javascript object consisting
||| of a tag `h` and an argument `a1`. `h` indicates, whether `obj0.a1`
||| contains the result of the computation (`h = 1`) or describes
||| a continuation indicating the next function to invoke
||| together with the necessary arguments. A single `step`
||| function will take such an object and use `a1` in a switch
||| statement to decide , which function
||| implementation to invoke (f1,f2,f3).
||| The result will be a new object, again indicating in tag `h`, whether
||| we arrived at a result, or we need to continue looping.
|||
||| Here is a cleaned-up and simplified version of the Javascript code
||| generated:
|||
||| ```javascript
||| function imp_gen_tailoptim_0(imp_gen_tailoptim_fusion_args_0){//EmptyFC
|||  function imp_gen_tailoptim_step_0(obj0){
|||   switch(obj0.a1.h){
|||    case 0: ... //implementation of a single step of f1
|||                //taking its arguments from the fields of `obj0.a1`.
|||    case 1: ... //implementation of a single step of f2
|||    case 2: ... //implementation of a single step of f3
|||   }
|||  }
|||
|||  // initial object containing the arguments for the first
|||  // function call
|||  obj0 = ({h:0, a1: imp_gen_tailoptim_fusion_args_0});
|||
|||  // infinite loop running until `obj0.h != 0`.
|||  while(true){
|||   switch(obj0.h){
|||    case 0: {
|||     obj0 = imp_gen_tailoptim_step_0(obj0);
|||     break; }
|||    default:
|||     return obj0.a1;
|||   }
|||  }
||| }
||| ```
module Compiler.ES.TailRec

import Data.Maybe
import Data.List
import Data.List1
import Data.Strings
import Libraries.Data.Graph
import Libraries.Data.SortedSet
import Libraries.Data.List.Extra as L
import Libraries.Data.SortedSet
import Libraries.Data.SortedMap
import Core.Name
import Core.Context
import Compiler.ES.ImperativeAst

import Debug.Trace

%default covering

data TailRecS : Type where

record TailSt where
  constructor MkTailSt
  nextName : Int

genName : {auto c : Ref TailRecS TailSt} -> Core Name
genName =
  do s <- get TailRecS
     let i = nextName s
     put TailRecS (record { nextName = i + 1 } s)
     pure $ MN "imp_gen_tailoptim" i

-- returns the set of tail calls made from a given
-- imperative statement.
allTailCalls : ImperativeStatement -> SortedSet Name
allTailCalls (SeqStatement x y)  = allTailCalls y
allTailCalls (ReturnStatement $ IEApp (IEVar n) _) = singleton n
allTailCalls (SwitchStatement e alts d) =
  concatMap allTailCalls d `union` concatMap (allTailCalls . snd) alts
allTailCalls (ForEverLoop x) = allTailCalls x
allTailCalls o = empty

argsName : Name
argsName = MN "imp_gen_tailoptim_Args" 0

stepFnName : Name
stepFnName = MN "imp_gen_tailoptim_step" 0

fusionArgsName : Name
fusionArgsName = MN "imp_gen_tailoptim_fusion_args" 0

createNewArgs : List ImperativeExp -> ImperativeExp
createNewArgs = IEConstructor (Left 0)

createArgInit : List Name -> ImperativeStatement
createArgInit names =
    LetDecl argsName (Just $ IEConstructor (Left 0) (map IEVar names))

replaceTailCall : Name -> ImperativeStatement -> ImperativeStatement
replaceTailCall n (SeqStatement x y) = SeqStatement x (replaceTailCall n y)
replaceTailCall n (ReturnStatement x) =
    let defRet = ReturnStatement $ IEConstructor (Left 1) [x]
    in case x of
        IEApp (IEVar cn) arg_vals =>
            if n == cn then ReturnStatement $ createNewArgs arg_vals
                else defRet
        _ => defRet
replaceTailCall n (SwitchStatement e alts d) =
    SwitchStatement e (map (mapSnd $ replaceTailCall n) alts)
                      (map (replaceTailCall n) d)
replaceTailCall n (ForEverLoop x) =
    ForEverLoop $ replaceTailCall n x
replaceTailCall n o = o

-- generates the tailcall-optimized function body
makeTailOptimToBody :  Name
                    -> List Name
                    -> ImperativeStatement
                    -> ImperativeStatement
makeTailOptimToBody n argNames body =
    let newArgExp = map (\x => IEConstructorArg (cast x) (IEVar argsName)) [1..length argNames]
        bodyArgsReplaced = replaceNamesExpS (zip argNames newArgExp) body
        stepBody = replaceTailCall n bodyArgsReplaced

        -- single step function. This takes a single argument
        -- and returns a new object indicating whether to continue looping
        -- or to return a result.
        stepFn = FunDecl EmptyFC stepFnName [argsName] stepBody

        -- calls the step function and mutates the loop object with the result
        loopRec = MutateStatement argsName (IEApp (IEVar stepFnName) [IEVar argsName])

        -- returns field `a1` from the loop object.
        loopReturn = ReturnStatement (IEConstructorArg 1 $ IEVar argsName)

        -- switch on the constructor head and either continue looping or
        -- return the result
        loop = ForEverLoop
             $ SwitchStatement (IEConstructorHead $ IEVar argsName)
                               [(IEConstructorTag $ Left 0, loopRec)]
                               (Just loopReturn)
    in stepFn <+> createArgInit argNames <+> loop

-- when creating the tail call graph, we only process
-- function declarations and we are only interested
-- in calls being made at tail position
tailCallGraph : ImperativeStatement -> SortedMap Name (SortedSet Name)
tailCallGraph (SeqStatement x y) =
  mergeWith union (tailCallGraph x) (tailCallGraph y)

tailCallGraph (FunDecl fc n args body) =
  singleton n $ allTailCalls body

tailCallGraph _ = empty

-- lookup up the list of values associated with
-- a given key (`Nil` if the key is not present in the list)
lookupList : k -> SortedMap k (SortedSet b) -> List b
lookupList v = maybe [] SortedSet.toList . lookup v

recursiveTailCallGroups : SortedMap Name (SortedSet Name) -> List (List Name)
recursiveTailCallGroups graph =
  [forget x | x <-tarjan graph, hasTailCalls x]

    -- in case of larger groups (more than one element)
    -- the group contains tailcalls by construction. In case
    -- of a single function, we need to check that at least one
    -- outgoing tailcall goes back to the function itself.
    where hasTailCalls : List1 Name -> Bool
          hasTailCalls (x ::: Nil) = x `elem` lookupList x graph
          hasTailCalls _           = True

-- extracts the functions belonging to the given tailcall
-- group from the given imperative statement, thereby removing
-- them from the given statement.
extractFunctions :  (tailCallGroup : SortedSet Name)
                 -> ImperativeStatement
                 -> ( ImperativeStatement
                    , SortedMap Name (FC, List Name, ImperativeStatement)
                    )
extractFunctions toExtract (SeqStatement x y) =
    let (xs, xf) = extractFunctions toExtract x
        (ys, yf) = extractFunctions toExtract y
    in (xs <+> ys, mergeLeft xf yf)
extractFunctions toExtract f@(FunDecl fc n args body) =
    if contains n toExtract then (neutral, insert n (fc, args, body) empty)
        else (f, empty)
extractFunctions toExtract x =
    (x, empty)

-- lookup a function definition, throwing a compile-time error
-- if none is found
getDef :  SortedMap Name (FC, List Name, ImperativeStatement)
       -> Name
       -> Core (FC, List Name, ImperativeStatement)
getDef defs n =
    case lookup n defs of
        Nothing => throw $ (InternalError $ "Can't find function definition in tailRecOptim")
        Just x => pure x

makeFusionBranch :  Name
                 -> List (Name, Nat)
                 -> (Nat, FC, List Name, ImperativeStatement)
                 -> (ImperativeExp, ImperativeStatement)
makeFusionBranch fusionName functionsIdx (i, _, args, body) =
    let newArgExp = map (\i => IEConstructorArg (cast i) (IEVar fusionArgsName))
                        [1..length args]
        bodyRepArgs = replaceNamesExpS (zip args newArgExp) body
    in (IEConstructorTag $ Left $ cast i, replaceExpS rep bodyRepArgs)
    where
        rep : ImperativeExp -> Maybe ImperativeExp
        rep (IEApp (IEVar n) arg_vals) =
            case lookup n functionsIdx of
                Nothing => Nothing
                Just i => Just $ IEApp
                          (IEVar fusionName)
                          [IEConstructor (Left $ cast i) arg_vals]
        rep _ = Nothing

changeBodyToUseFusion :  Name
                      -> (Nat, Name, FC, List Name, ImperativeStatement)
                      -> ImperativeStatement
changeBodyToUseFusion fusionName (i, n, (fc, args, _)) =
    FunDecl fc n args (ReturnStatement $ IEApp (IEVar fusionName)
                        [IEConstructor (Left $ cast i) (map IEVar args)])

tailRecOptimGroup :  {auto c : Ref TailRecS TailSt}
                  -> SortedMap Name (FC, List Name, ImperativeStatement)
                  -> List Name -> Core ImperativeStatement
tailRecOptimGroup defs [] = pure neutral
tailRecOptimGroup defs [n] =
    do (fc, args , body) <- getDef defs n
       pure $ FunDecl fc n args (makeTailOptimToBody n args body)

tailRecOptimGroup defs names =
    do fusionName <- genName
       d <- traverse (getDef defs) names
       let ids = [0..(length names `minus` 1)]
       let alts = map (makeFusionBranch fusionName (zip names ids)) (zip ids d)
       let fusionBody = SwitchStatement
                          (IEConstructorHead $ IEVar fusionArgsName)
                          alts
                          Nothing
       let fusionArgs = [fusionArgsName]
       let fusion = FunDecl EmptyFC
                            fusionName
                            fusionArgs
                            (makeTailOptimToBody fusionName fusionArgs fusionBody)
       let newFunctions = Prelude.concat $ map
                           (changeBodyToUseFusion fusionName)
                           (ids `zip` (names `zip` d))
       pure $ fusion <+> newFunctions

||| (Mutual) Tail recursion optimizations: Converts all groups of
||| mutually tail recursive functions to an imperative loop.
export
tailRecOptim : ImperativeStatement -> Core ImperativeStatement
tailRecOptim x =
    do ref <- newRef TailRecS (MkTailSt 0)
       let groups = recursiveTailCallGroups (tailCallGraph x)
       let functionsToOptimize = foldl SortedSet.union empty $ map SortedSet.fromList groups
       let (unchanged, defs) = extractFunctions functionsToOptimize x
       optimized <- traverse (tailRecOptimGroup defs) groups
       pure $ unchanged <+> (concat optimized)

max_stars_repo_name: mmhelloworld/idris-jvm

max_issues_repo_name: mmhelloworld/idris-jvm

max_forks_repo_name: mmhelloworld/idris-jvm


text:
module Postgres.Data.PostgresValue

import Data.Either
import Data.String
import Data.List
import Data.List1
import Postgres.Data.PostgresType
import Language.JSON

public export
data PValue : (p : PType) -> Type where
  Raw : (rawString : String) -> PValue p

export
rawString : PValue t -> String
rawString (Raw r) = r

public export
interface SafeCast ty1 ty2 where
  safeCast : ty1 -> Maybe ty2

-- Integer

export
SafeCast (PValue PInteger) Integer where
  safeCast = parseInteger . rawString

export
SafeCast (PValue PInteger) Double where
  safeCast = parseDouble . rawString

-- Double

export
SafeCast (PValue PDouble) Double where
  safeCast = parseDouble . rawString

-- Char

export
SafeCast (PValue PChar) Char where
  safeCast (Raw str) with (unpack str)
    safeCast (Raw str) | [c] = Just c
    safeCast (Raw str) | _ = Nothing

-- Boolean

export
SafeCast (PValue PBoolean) Bool where
  safeCast (Raw "t")     = Just True
  safeCast (Raw "f")     = Just False
  safeCast (Raw "true")  = Just True
  safeCast (Raw "false") = Just False
  safeCast (Raw "1")     = Just True
  safeCast (Raw "0")     = Just False
  safeCast (Raw _)       = Nothing

-- TODO: Date

-- TODO: Time

-- TODO: Datetime

-- String

export
Cast (PValue PString) String where
  cast = rawString

export
SafeCast (PValue PString) String where
  safeCast = Just . cast

-- JSON

export
SafeCast (PValue PJson) JSON where
  safeCast = parse . rawString

-- TODO: UUID

-- OID

export
SafeCast (PValue POid) Integer where
  safeCast = parseInteger . rawString

-- Arrays

parseArray : String -> Maybe (List String)
parseArray str =
  let stripped = trim str
  in
      do guard (("{" `isPrefixOf` stripped) && ("}" `isSuffixOf` stripped))
         let middle = reverse . (drop 1) . reverse . (drop 1) $ unpack stripped
         pure . forget $ pack <$> (splitOn ',' middle)

export
[SafeCastList] SafeCast (PValue from) to => SafeCast (PValue (PArray from)) (List to) where
  safeCast (Raw rawString) = (parseArray rawString) >>= (traverse (safeCast . (Raw {p=from})))

--
-- Default Types
--

public export
data HasDefaultType : Type -> Type where
  DInteger  : SafeCast (PValue PInteger) Integer => HasDefaultType Integer
  DDouble   : SafeCast (PValue PDouble)  Double  => HasDefaultType Double
  DChar     : SafeCast (PValue PChar)    Char    => HasDefaultType Char
  DBoolean  : SafeCast (PValue PBoolean) Bool    => HasDefaultType Bool
  DString   : SafeCast (PValue PString)  String  => HasDefaultType String
  DJson     : SafeCast (PValue PJson)    JSON    => HasDefaultType JSON
  DList     : HasDefaultType to => HasDefaultType (List to)

safeCastImpl : HasDefaultType to -> (p ** SafeCast (PValue p) to)
safeCastImpl (DInteger @{safe}) = (_ ** safe)
safeCastImpl (DDouble  @{safe}) = (_ ** safe)
safeCastImpl (DChar    @{safe}) = (_ ** safe)
safeCastImpl (DBoolean @{safe}) = (_ ** safe)
safeCastImpl (DString  @{safe}) = (_ ** safe)
safeCastImpl (DJson    @{safe}) = (_ ** safe)
safeCastImpl (DList    @{hdt})  = let (pType1 ** safe) = safeCastImpl hdt
                                  in
                                      (PArray pType1 ** SafeCastList)

public export
data Castable : Type -> Type where
  Cast      : HasDefaultType ty => Castable ty
  CastMaybe : HasDefaultType ty => Castable (Maybe ty)

notNothing : (context : String) -> Maybe String -> Either String String
notNothing ctx = maybeToEither ("Unexpected null when looking for " ++ ctx)

-- some gross repetition between the following two methods.
-- having a bit of brain block figuring out how to combine
-- the two right now.
parse : (p ** SafeCast (PValue p) to)
     -> Maybe String
     -> Either String to
parse (p ** safe) str =
  let ctx = (show p)
  in
      notNothing ctx str >>= ((maybeToEither $ "Failed to parse " ++ ctx) . safeCast @{safe} . Raw)

parseNullable : (p ** SafeCast (PValue p) to)
             -> Maybe String
             -> Either String (Maybe to)
parseNullable (p ** safe) str =
  let ctx = (show p) ++ "?"
  in
      case str of
        Just s  => Just <$> ((maybeToEither $ "Failed to parse " ++ ctx) $ safeCast @{safe} $ Raw s)
        Nothing => Right Nothing

||| Turn the string coming from Postgres into its default Idris type.
public export
asDefaultType : Castable t -> (columnValue : Maybe String) -> Either String t
asDefaultType (Cast      @{hdt}) = parse (safeCastImpl hdt)
asDefaultType (CastMaybe @{hdt}) = parseNullable (safeCastImpl hdt)

max_stars_repo_name: mattpolzin/pg-idris

max_issues_repo_name: mattpolzin/pg-idris

max_forks_repo_name: mattpolzin/pg-idris


text:
module Notes

add : Int -> Int -> Int
add x y = x + y

identity : a -> a
identity = id

double : Num a => a -> a
double x = x + x

twice : (a -> a) -> a -> a
twice fn a = fn (fn a)

twiceLambda: Integer
twiceLambda = twice (\x => x * x) 2

consing : List Integer
consing = 1 :: 2 :: 3 :: []

-- Exercices

palindrom : String -> Bool
palindrom str = let s = toLower str in
                    s == reverse s'

palindrom' : String -> Bool
palindrom' s = if length s > 10
                then palindrom s
                else False

palindrom'' : Nat -> String -> Bool
palindrom'' len s = if length s > len
                then palindrom s
                else False

counts : String -> (Nat, Nat)
counts s = (length (words s), length s)

top : Ord a => Nat -> List a -> List a
top n = Prelude.List.take n . reverse . sort

over_length : Nat -> List String -> Nat
over_length count = length . filter (\x => length x > count)


text:
module Datatypes

import CFT

public export
TNat : {n : _ } -> CFT n
TNat = µ (One + VZ)
-- data Nat = Zero | Succ Nat

public export
TList : {n : _} -> CFT (S n)
TList = µ (One + (var 1 * var 0))

public export
TTree : {n : _} -> CFT (S n)
TTree = µ (var 1 + (var 0 * var 0))

public export
TRoseTree : {n : _} -> CFT (S n)
TRoseTree = µ (var 1 * µ (One + (var 1 * var 0)))

public export
TRoseTree' : {n : _} -> CFT (S n)
TRoseTree' = µ (var 1 * App TList (var 0))

public export
zero : Ty TNat t
zero = In (Left Unit)

public export
succ : Ty TNat t -> Ty TNat t
succ x = In (Right (Top x))

public export
cons : Ty a t -> Ty TList (a :: t) -> Ty TList (a :: t)
cons x y = In (Right (Pair (Pop (Top x)) (Top y)))

public export
tLen : Ty TList t -> Ty TNat t
tLen (In (Left Unit)) = zero
tLen (In (Right (Pair x (Top y)))) = succ (tLen y)

public export
fromNat : Nat -> Ty TNat t
fromNat 0 = zero
fromNat (S k) = succ (fromNat k)

public export
toNat : Ty TNat t -> Nat
toNat (In (Left Unit)) = Z
toNat (In (Right (Top x))) = S (toNat x)

public export
plus : (m, n : Ty TNat t ) -> Ty TNat t
plus (In (Left Unit)) n = n
plus (In (Right (Top x))) n = succ (plus x n)

max_stars_repo_name: andrevidela/dev-notes

max_issues_repo_name: andrevidela/dev-notes

max_forks_repo_name: andrevidela/dev-notes


text:
module Main

import Control.App

printSquare : Has [Num, Show] a => a -> IO ()
printSquare x = printLn (x * x)

main : IO ()
main = printSquare 10

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:
data Tree a = Empty
            | Node (Tree a) a (Tree a)

testTree : Tree String
testTree = Node (Node (Node Empty "Jim" Empty) "Fred"
                      (Node Empty "Sheila" Empty)) "Alice"
                (Node Empty "Bob" (Node Empty "Eve" Empty))

flatten : Tree a -> List a
flatten Empty = []
flatten (Node left val right) = flatten left ++ val :: flatten right

data State : (stateType : Type) -> Type -> Type where
     Get : State stateType stateType
     Put : stateType -> State stateType ()

     Pure : ty -> State stateType ty
     Bind : State stateType a -> (a -> State stateType b) ->
             State stateType b

{-
(>>=) : State stateType a -> (a -> State stateType b) ->
        State stateType b
(>>=) = Bind
-}

mutual
  Functor (State stateType) where
      map func x = do val <- x
                      Pure (func val)

  Applicative (State stateType) where
      pure x = Pure x
      (<*>) f a = do func <- f
                     arg <- a
                     pure (func arg)

  Monad (State stateType) where
      (>>=) = Bind

runState : State stateType a -> (st : stateType) -> (a, stateType)
runState Get st = (st, st)
runState (Put newState) st = ((), newState)

runState (Pure x) st = (x, st)
runState (Bind cmd prog) st = let (val, nextState) = runState cmd st in
                                  runState (prog val) nextState

treeLabelWith : Tree a -> State (Stream labelType) (Tree (labelType, a))
treeLabelWith Empty = Pure Empty
treeLabelWith (Node left val right)
     = do left_labelled <- treeLabelWith left
          (this :: rest) <- Get
          Put rest
          right_labelled <- treeLabelWith right
          Pure (Node left_labelled (this, val) right_labelled)

treeLabel : Tree a -> Tree (Integer, a)
treeLabel tree = fst (runState (treeLabelWith tree) [1..])


text:
-- ----------------------------------------------------------- [ WordTypes.idr ]
-- Module    : WordTypes.idr
-- Copyright : (c) Jan de Muijnck-Hughes
-- License   : see LICENSE
-- --------------------------------------------------------------------- [ EOH ]
module Readability.WordTypes

import Prelude.Strings

inTwos : List a -> List (a,a)
inTwos [] = []
inTwos (x::y::xs) = (x,y) :: inTwos xs

isSomething : String -> List String -> Bool
isSomething w ws = List.elem w ws

articles : List String
articles = ["the", "a", "an"]

isArticle : String -> Bool
isArticle w = isSomething w articles

pronouns : List String
pronouns = ["i", "me", "we", "us", "you", "he", "him", "she", "her", "it", "they",
    "them", "thou", "thee", "ye", "myself", "yourself", "himself",
    "herself", "itself", "ourselves", "yourselves", "themselves",
    "oneself", "my", "mine", "his", "hers", "yours", "ours", "theirs", "its",
    "our", "that", "their", "these", "this", "those", "your"]

export
isPronoun : String -> Bool
isPronoun w = isSomething w pronouns

iter_pronouns : List String
iter_pronouns = ["why", "who", "what", "whom", "when", "where", "how"]

isInterrogativePronoun : String -> Bool
isInterrogativePronoun w = isSomething w iter_pronouns

conjunctions : List String
conjunctions = ["and", "but", "or", "yet", "nor"]

isConjunction : String -> Bool
isConjunction w = isSomething w conjunctions

nominalisation : List String
nominalisation = ["tion", "ment", "ence", "ance"]

isNominalisation : String -> Bool
isNominalisation w = elem True (map (\x => isSuffixOf (unpack x) (unpack w)) nominalisation)

subconjunction : List String
subconjunction =  ["after", "because", "lest", "till", "'til", "although", "before",
    "now that", "unless", "as", "even if", "provided that", "provided",
    "until", "as if", "even though", "since", "as long as", "so that",
    "whenever", "as much as", "if", "than", "as soon as", "inasmuch",
    "in order that", "though", "while"]

isSubconjunction : String -> Bool
isSubconjunction w = isSomething w subconjunction

preposition : List String
preposition = ["aboard", "about", "above", "according to", "across from",
    "after", "against", "alongside", "alongside of", "along with",
    "amid", "among", "apart from", "around", "aside from", "at", "away from",
    "back of", "because of", "before", "behind", "below", "beneath", "beside",
    "besides", "between", "beyond", "but", "by means of",
    "concerning", "considering", "despite", "down", "down from", "during",
    "except", "except for", "excepting for", "from among",
    "from between", "from under", "in addition to", "in behalf of",
    "in front of", "in place of", "in regard to", "inside of", "inside",
    "in spite of", "instead of", "into", "like", "near to", "off",
    "on account of", "on behalf of", "onto", "on top of", "on", "opposite",
    "out of", "out", "outside", "outside of", "over to", "over", "owing to",
    "past", "prior to", "regarding", "round about", "round",
    "since", "subsequent to", "together", "with", "throughout", "through",
    "till", "toward", "under", "underneath", "until", "unto", "up",
    "up to", "upon", "with", "within", "without", "across", "along",
    "by", "of", "in", "to", "near", "of", "from"]

isPreposition : String -> Bool
isPreposition w = isSomething w preposition

auxverbs : List String
auxverbs = ["will", "shall", "cannot", "may", "need to", "would", "should",
    "could", "might", "must", "ought", "ought to", "can't", "can"]

isAuxVerb : String -> Bool
isAuxVerb w = isSomething w auxverbs

toBeVerbs : List String
toBeVerbs = ["be", "being", "was", "were", "been", "are", "is"]

isToBeVerb : String -> Bool
isToBeVerb w = isSomething w toBeVerbs

isVowel : Char -> Bool
isVowel c = List.elem (toLower c) ['a', 'e', 'i', 'o', 'u', 'y']

export
countSyllables : String -> Int
countSyllables w =
    case length (ws) <= 2 of
      True  => 1
      False =>
        if isSuffixOf (unpack "ed") ws
          then countSyllables' (take (minus (length ws)  2) ws)
          else
            let res = countSyllables' ws in
              if res == 0
                then 1
                else res

  where
    ws : List Char
    ws = unpack w
    countSyllables' : List Char -> Int
    countSyllables' []         = 0
    countSyllables' (x::y::xs) =
      if (isVowel x) && not (isVowel y)
        then 1 + countSyllables' xs
        else countSyllables' (y::xs)
    countSyllables' x          = 0

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

max_stars_repo_name: jfdm/idris-read

max_issues_repo_name: jfdm/idris-read

max_forks_repo_name: jfdm/idris-read


text:
module Libra.Test.Parser

import Libra.Parser
import Libra.Data

import Data.Vect

import TAP

%access export  -- to make the test functions visible

testName : Lazy (IO Bool)
testName = do
  let fixture = "hello"
  let expected = MkName "hello"
  let result = out (execParserT parseExpr fixture)
  case result of
       Right actual => pure True
       Left err => pure False

testBadName : Lazy (IO Bool)
testBadName = do
  let fixture = "1hello"
  let expected = MkName "hello"
  let result = out (execParserT parseExpr fixture)
  case result of
       Right actual => pure False
       Left err => pure True

data What = Run | Name

testExpression : Lazy (IO Bool)
testExpression = do
  let fixture = "(LABEL EQUAL (LAMBDA (X Y) (COND ((ATOM X) (COND ((ATOM Y) (EQ X Y)) ((QUOTE T) (QUOTE F)))) ((EQUAL (CAR X) (CAR Y)) (EQUAL (CDR X) (CDR Y))) ((QUOTE T) (QUOTE F)))) (LAMBDA (X Y) (COND ((ATOM X) (COND ((ATOM Y) (EQ X Y)) ((QUOTE T) (QUOTE F)))) ((EQUAL (CAR X) (CAR Y)) (EQUAL (CDR X) (CDR Y))) ((QUOTE T) (QUOTE F))))(LAMBDA (X Y) (COND ((ATOM X) (COND ((ATOM Y) (EQ X Y)) ((QUOTE T) (QUOTE F)))) ((EQUAL (CAR X) (CAR Y)) (EQUAL (CDR X) (CDR Y))) ((QUOTE T) (QUOTE F)))))"
  let expected = (MkSExpr [MkName "hello", (MkSExpr [MkName "world"])])
  let result = out (execParserT parseExpr fixture)
  case result of
       Right actual => pure True
       Left err => pure False

parserTests : IO ()
parserTests = plan "Parser Tests" [
  Delay (testName),
  Delay (testBadName),
  Delay (testExpression)
]

max_stars_repo_name: ostera/libra

max_issues_repo_name: ostera/libra

max_forks_repo_name: ostera/libra


text:
module TTImp.Elab.As

import Core.Context
import Core.Context.Log
import Core.Core
import Core.Env
import Core.Metadata
import Core.Normalise
import Core.Unify
import Core.TT
import Core.Value

import TTImp.Elab.Check
import TTImp.Elab.ImplicitBind
import TTImp.TTImp

import Data.List
import Data.NameMap

%default covering

export
checkAs : {vars : _} ->
          {auto c : Ref Ctxt Defs} ->
          {auto m : Ref MD Metadata} ->
          {auto u : Ref UST UState} ->
          {auto e : Ref EST (EState vars)} ->
          RigCount -> ElabInfo ->
          NestedNames vars -> Env Term vars ->
          FC -> UseSide -> Name -> RawImp -> Maybe (Glued vars) ->
          Core (Term vars, Glued vars)
checkAs rig elabinfo nest env fc side n_in pat topexp
    = do let elabmode = elabMode elabinfo
         let InLHS _ = elabmode
             | _ => do log "elab.as" 2 $ "Bad @-pattern " ++ show pat
                       throw (GenericMsg fc "@-patterns only allowed in pattern clauses")
         est <- get EST
         let n = PV n_in (defining est)
         noteLHSPatVar elabmode n_in
         notePatVar n
         case lookup n (boundNames est) of
              Nothing =>
                 do (pattm, patty) <- check rigPat elabinfo nest env pat topexp
                    (tm, exp, bty) <- mkPatternHole fc rig n env
                                            (implicitMode elabinfo)
                                            topexp
                    log "elab.as" 5 $ "Added as pattern name " ++ show (n, (rigAs, tm, exp, bty))
                    defs <- get Ctxt
                    est <- get EST
                    put EST
                        (record { boundNames $= ((n, AsBinding rigAs Explicit tm exp pattm) :: ),
                                  toBind $= ((n, AsBinding rigAs Explicit tm bty pattm) ::) }
                                est)
                    (ntm, nty) <- checkExp rig elabinfo env fc tm (gnf env exp)
                                           (Just patty)
                    pure (As fc side ntm pattm, patty)
              Just bty => throw (NonLinearPattern fc n_in)
  where
    -- Only one side can be usable if it's linear! Normally we'd assume this
    -- to be the new variable (UseRight), but in generated case blocks it's
    -- better if it's the pattern (UseLeft)
    rigPat' : UseSide -> RigCount
    rigPat' UseLeft = if isLinear rig then linear else rig
    rigPat' UseRight = if isLinear rig then erased else rig

    rigPat : RigCount
    rigPat = rigPat' side

    rigAs' : UseSide -> RigCount
    rigAs' UseLeft = if isLinear rig then erased else rig
    rigAs' UseRight = if isLinear rig then linear else rig

    rigAs : RigCount
    rigAs = rigAs' side


text:
module Part2
import Data.String
import Debug.Trace

forward : (Int, Int, Int) -> Int -> (Int, Int, Int)
forward (a, b, c) d = (a+d, b + (d * c), c)

down : (Int, Int, Int) -> Int -> (Int, Int, Int)
down (a, b, c) d = (a, b, c + d)

up : (Int, Int, Int) -> Int -> (Int, Int, Int)
up (a, b, c) d = (a, b, c - d)

parseOp : String -> ((Int, Int, Int) -> Int -> (Int, Int, Int))
parseOp s = if s == "forward" then forward else if s == "down" then down else up

foldOp : (Int, Int, Int) -> (String, String) -> (Int, Int, Int)
foldOp (a, b) (s, t) = (parseOp s) (a, b) (fromMaybe 0 (parseInteger (trim t)))

splitInput : String -> (String, String)
splitInput s = break (== ' ') s

export
splitInputs : List(String) -> List(String, String)
splitInputs l = map splitInput l

export
solve : List(String) -> (Int, Int, Int)
solve l = foldl foldOp (0, 0, 0) (splitInputs (filter (/= "") l))


text:
module Idrlib

import Data.IORef
import System
import Idrlisp
import Idrlisp.Vec

%default covering

mod' : Double -> Double -> Double
mod' x y =
  case cast {to = Integer} y of
    0 => 0.0 / 0.0
    y' => cast (assert_total (cast x `mod` y'))

dropPure : Value -> Maybe (Sexp ())
dropPure = traverse $ const Nothing

infixl 0 ->>

data BuiltinClause : Type where
  (->>) : (sig : ValueArgsSignature) -> (handle : SignatureType sig -> VM ()) -> BuiltinClause

signature : String -> BuiltinClause -> String
signature name (sig ->> _) = show (Sym name :: sig)

mkBuiltin : String -> List BuiltinClause -> (String, Builtin)
mkBuiltin name clauses = (name, MkBuiltin (run clauses))
  where
    run : List BuiltinClause -> List Value -> VM ()
    run ((sig ->> handle) :: ps) args =
      case match sig args of
        Just x => handle x
        Nothing => run ps args
    run [] _ =
      Fail $ "Evaluation error: expected " ++ concat (intersperse " or " (map (signature name) clauses))

mkBuiltinGensym : String -> IO (String, Builtin)
mkBuiltinGensym name = do
  idRef <- newIORef 0
  pure $ mkBuiltin name
    [ [] ->> \() => do
        id <- Action $ readIORef idRef
        let id' = succ id
        Action $ writeIORef idRef id'
        Push $ Sym $ "#sym." ++ show id'
    ]

mkBuiltinTest : String -> ValueSignature -> (String, Builtin)
mkBuiltinTest name sig = mkBuiltin name
  [ [Any "expr"] ->> \expr => Push $ Bool $ isJust $ match sig expr
  ]

mkBuiltinCompare : String -> (Double -> Double -> Bool) -> (String -> String -> Bool) -> (String, Builtin)
mkBuiltinCompare name fcmp scmp = mkBuiltin name
  [ [] ->> \() => Push $ Bool True
  , (Num "num" :: Rest (Num "nums")) ->> handle fcmp
  , (Str "str" :: Rest (Str "strs")) ->> handle scmp
  ]
  where
    handle : (b -> b -> Bool) -> (b, List b) -> VM ()
    handle cmp (x, xs) = Push $ Bool $ all id $ zipWith cmp (x :: xs) xs

mkBuiltinCont : String -> Cont -> (String, Builtin)
mkBuiltinCont name cont = mkBuiltin name
  [ [] ->> \() => RestoreCont cont *> Push Nil
  , [Any "x"] ->> \x => RestoreCont cont *> Push x
  , (Any "x" :: Rest (Any "xs")) ->> \xs => Fail "Evaluation error: multiple values are not implemented"
  ]

mkBuiltinArgs : String -> List String -> (String, Builtin)
mkBuiltinArgs name args = mkBuiltin name
  [ [] ->> \() => Push $ foldr (::) Sexp.Nil (map Sexp.Str args)
  ]

export
initIdrlib : List String -> IO (List (String, Builtin))
initIdrlib args = pure
  [ mkBuiltin "cons"
      [ [Any "car", Any "cdr"] ->> \(car, cdr) => Push (car :: cdr)
      ]

  , mkBuiltin "exit"
      [ [] ->> \() => Action $ exit 0
      , [Num "exitcode"] ->> \c => Action $ exit (cast c)
      ]
  , mkBuiltin "error"
      [ [] ->> \() => Fail "Evaluation error: error called"
      , [Str "msg"] ->> \msg => Fail $ "Evaluation error: " ++ msg
      ]

  , !(mkBuiltinGensym "gensym")

  , mkBuiltin "car"
      [ [(Any "car" :: Any "cdr")] ->> \(car, _) => Push car
      ]
  , mkBuiltin "cdr"
      [ [(Any "cdr" :: Any "cdr")] ->> \(_, cdr) => Push cdr
      ]

  , mkBuiltin "apply"
      [ [Any "f", List (Any "arguments")] ->> \(f, args) => apply f args
      ]

  , mkBuiltinTest "num?" (Num "")
  , mkBuiltinTest "sym?" (Sym "")
  , mkBuiltinTest "str?" (Str "")
  , mkBuiltinTest "cons?" (Any "" :: Any "")
  , mkBuiltinTest "nil?" Nil
  , mkBuiltinTest "bool?" (Bool "")
  , mkBuiltinTest "proc?" (Pure "" NBuiltin `Or` Pure "" NFun)
  , mkBuiltinTest "meta?" (Pure "" NSyntax `Or` Pure "" NMacro)
  , mkBuiltinTest "port?" (Pure "" NPort)
  , mkBuiltinTest "vec?" (Pure "" NVec)

  , mkBuiltin "+"
      [ Rest (Num "nums") ->> \nums => Push $ Num $ sum nums
      ]
  , mkBuiltin "-"
      [ [Num "num"] ->> \num => Push $ Num $ negate num
      , (Num "num" :: Rest (Num "nums")) ->> \(num, nums) => Push $ Num $ foldl (-) num nums
      ]
  , mkBuiltin "*"
      [ Rest (Num "nums") ->> \nums => Push $ Num $ product nums
      ]
  , mkBuiltin "/"
      [ [Num "num"] ->> \num => Push $ Num $ recip num
      , (Num "num" :: Rest (Num "nums")) ->> \(num, nums) => Push $ Num $ foldl (/) num nums
      ]
  , mkBuiltin "%"
      [ (Num "num" :: Rest (Num "nums")) ->> \(num, nums) => Push $ Num $ foldl mod' num nums
      ]

  , mkBuiltin "="
      [ [] ->> \() => Push $ Bool True
      , (Any "x" :: Rest (Any "xs")) ->> \(x, xs) => do
          let x' = dropPure x
          let xs' = map dropPure xs
          Push $ Bool $ all isJust xs' && all (== x') xs'
      ]

  , mkBuiltinCompare "<" (<) (<)
  , mkBuiltinCompare ">" (>) (>)
  , mkBuiltinCompare "<=" (<=) (<=)
  , mkBuiltinCompare ">=" (>=) (>=)

  , mkBuiltin "call/cc"
      [ [Any "f"] ->> \f => do
          cont <- CaptureCont
          apply f [Pure (NBuiltin (snd (mkBuiltinCont "continuation" cont)))]
      ]

  , mkBuiltin "never"
      [ (Any "f" :: Rest (Any "arguments")) ->> \(f, args) => DropCont *> apply f args
      ]

  -- String support has limitations. please see README.md
  , mkBuiltin "str"
      [ Rest (Num "bytes") ->> \chars =>
          Push $ Str $ pack [chr $ cast c | c <- the (List Double) chars]
      ]
  , mkBuiltin "str-ref"
      [ [Str "string", Num "index"] ->> \(str, index) =>
          let i = the Int $ cast index in
          case i < 0 || i >= cast (length str) of
            True => Push $ Nil
            False => Push $ Num $ cast $ ord $ assert_total (strIndex str i)
      ]
  , mkBuiltin "str-bytesize"
      [ [Str "string"] ->> \str => Push $ Num $ cast $ length str
      ]
  , mkBuiltin "str-concat"
      [ Rest (Str "strings") ->> \strs => Push $ Str $ concat strs
      ]
  , mkBuiltin "substr"
      [ [Str "string", Num "index", Num "bytesize"] ->> \(str, index, bytesize) =>
          let index'    = the Nat $ cast $ the Integer $ cast index
              bytesize' = the Nat $ cast $ the Integer $ cast bytesize
          in
          if index' < 0 || length str < index' + bytesize'
            then Fail "Evaluation error: substr: index out of range"
            else Push $ Str $ substr index' bytesize' str
      ]
  , mkBuiltin "sym->str"
      [ [Sym "symbol"] ->> \sym => Push $ Str sym
      ]
  , mkBuiltin "num->str"
      [ [Num "number"] ->> \num => Push $ Str $ show num
      ]
  , mkBuiltin "str->num"
      [ [Str "string"] ->> \str =>
          let n = the Double $ cast str in
          if n /= 0.0 || str == "0" || str == "0.0"
            then Push $ Num n
            else Push Nil
      ]

  , mkBuiltin "vec"
      [ Rest (Any "items") ->> \items => do
          vec <- Action $ Vec.fromList items
          Push $ Pure $ NVec vec
      ]
  , mkBuiltin "vec-make"
      [ [Num "length", Any "init"] ->> \(length, init) => do
          vec <- Action $ Vec.new (cast $ the Integer $ cast length) init
          Push $ Pure $ NVec vec
      ]
  , mkBuiltin "vec-ref"
      [ [Pure "vec" NVec, Num "index"] ->> \(vec, index) =>
          case !(Action $ Vec.read (cast $ the Integer $ cast index) vec) of
            Nothing => Push Nil
            Just x => Push x
      ]
  , mkBuiltin "vec-length"
      [ [Pure "vec" NVec] ->> \vec => Push $ Num $ cast $ Vec.length vec
      ]
  , mkBuiltin "vec-set!"
      [ [Pure "vec" NVec, Num "index", Any "item"] ->> \(vec, index, item) =>
          case !(Action $ Vec.write (cast $ the Integer $ cast index) item vec) of
            True => Push Nil
            False => Fail "Evaluation error: vec-set!: index out of range"
      ]
  , mkBuiltin "vec-copy!"
      [ [Pure "dest" NVec, Num "dest-start", Pure "src" NVec, Num "src-start", Num "length"] ->>
          \(dest, destStart, src, srcStart, len) =>
            let destStart' = cast $ the Integer $ cast destStart
                srcStart' = cast $ the Integer $ cast srcStart
                len' = cast $ the Integer $ cast len
            in
            case !(Action $ Vec.copy src srcStart' dest destStart' len') of
              True => Push Nil
              False => Fail "Evaluation error: vec-copy!: index out of range"
      ]

  , mkBuiltin "open"
      [ [Str "filepath", Str "mode"] ->> \(filepath, mode) => do
          mode <- case mode of
            "w" => pure WriteTruncate
            "r" => pure Read
            m => Fail $ "Evaluation error: open: unsupported mode: " ++ m
          result <- Action $ openFile filepath mode
          case result of
            Left err => Push $ Bool False :: Str (show err)
            Right file => Push $ Bool True :: Pure (NPort file)
      ]
  , mkBuiltin "close"
      [ [Pure "port" NPort] ->> \file => do
          Action $ closeFile file
          Push $ Bool True :: Nil
      ]

  , mkBuiltin "stdin" [[] ->> \() => Push $ Pure $ NPort stdin]
  , mkBuiltin "stdout" [[] ->> \() => Push $ Pure $ NPort stdout]
  , mkBuiltin "stderr" [[] ->> \() => Push $ Pure $ NPort stderr]

  , mkBuiltin "read-byte"
      [ [Pure "port" NPort] ->> \file => do
          result <- Action $ fgetc file
          case result of
            Left err => Push $ Bool False :: Str (show err)
            Right ch =>
              if the Int (cast ch) == 0
                then Push $ Bool True :: Sym "eof"
                else Push $ Bool True :: Num (cast $ the Int $ cast ch)
      ]
  , mkBuiltin "read-str"
      [ [Num "bytesize", Pure "port" NPort] ->> \(bytesize, file) => do
          result <- Action $ fGetChars file (cast bytesize)
          case result of
            Left err => Push $ Bool False :: Str (show err)
            Right s =>
              case length s of
                Z => Push $ Bool True :: Sym "eof"
                _ => Push $ Bool True :: Str s
      ]
  , mkBuiltin "read-line"
      [ [Pure "port" NPort] ->> \file => do
          result <- Action $ fGetLine file
          case result of
            Left err => Push $ Bool False :: Str (show err)
            Right s =>
              case length s of
                Z => Push $ Bool True :: Sym "eof"
                S k => Push $ Bool True :: Str (substr 0 k s)
      ]

  , mkBuiltin "write-byte"
      [ [Num "byte", Pure "port" NPort] ->> \(ch, file) => do
          result <- Action $ fPutStr file (cast ch)
          case result of
            Left err => Push $ Bool False :: Str (show err)
            Right () => Push $ Bool True :: Num 1.0
      ]
  , mkBuiltin "write-str"
      [ [Str "str", Pure "port" NPort] ->> \(str, file) => do
          result <- Action $ fPutStr file str
          case result of
            Left err => Push $ Bool False :: Str (show err)
            Right () => Push $ Bool True :: Num (cast $ the Int $ cast $ length str)
      ]
  , mkBuiltin "write-line"
      [ [Str "str", Pure "port" NPort] ->> \(str, file) => do
          result <- Action $ fPutStrLn file str
          case result of
            Left err => Push $ Bool False :: Str (show err)
            Right () => Push $ Bool True :: Num (cast $ the Int $ cast $ length str + 1)
      ]

  , mkBuiltin "flush"
      [ [Pure "port" NPort] ->> \file => do
          Action $ fflush file
          Push $ Bool True :: Nil
      ]

  , mkBuiltinArgs "args" args

  , mkBuiltin "eval"
      [ [Any "expr"] ->> \expr => do
          ctx <- CaptureContext
          result <- Action $ evalExpr ctx expr
          case result of
            Left err => Push $ Bool False :: Str err
            Right v => Push $ Bool True :: v
      ]
  , mkBuiltin "macroexpand"
      [ [Any "expr"] ->> \expr => do
          ctx <- CaptureContext
          result <- Action $ macroExpandExpr ctx True expr
          case result of
            Left err => Push $ Bool False :: Str err
            Right v => Push $ Bool True :: v
      ]
  , mkBuiltin "macroexpand-1"
      [ [Any "expr"] ->> \expr => do
          ctx <- CaptureContext
          result <- Action $ macroExpandExpr ctx False expr
          case result of
            Left err => Push $ Bool False :: Str err
            Right v => Push $ Bool True :: v
      ]
  ]

max_stars_repo_name: yubrot/idrlisp

max_issues_repo_name: yubrot/idrlisp

max_forks_repo_name: yubrot/idrlisp