berewt

module Main

||| The smart consturctor tool:
||| Check whether an element belongs to a given subset
subset : ((x: a) -> Dec (prop x)) -> a -> Either a (Subset a prop)
subset dec y with (dec y)
  | (Yes prf) = pure (Element y prf)
  | (No contra) = Left y

-- Example

berewt

module Audit

import Control.Monad.Syntax

import Data.Fin
import Data.String
import Data.Vect
import Data.Vect.Sub

import Leon.DataFrame.Columns

berewt

module TennisDT

%default total

data Player = Player1 | Player2


||| Prove that the game is not over after a point
data NotWinning : Nat -> Nat -> Type where
  ||| Game is not over because the winning player is below 40

berewt

||| A Straightforward translation of the
||| [ArduinoML](https://github.com/mosser/ArduinoML-kernel) use case
||| with a bit of syntax extension for a smooth DSL experience
module ArduinoBasic

import Data.Union

namespace model

  data SIGNAL = LOW | HIGH

berewt

module Pipes.ITE where

import Pipes
import qualified Pipes.Prelude as P

ite :: Monad m => (a -> Bool) -> Pipe a b m () -> Pipe a c m () -> Pipe (Either b c) d m ()  -> Pipe a d m r
ite predicate l r j = for cat $ \x -> yield x >-> if predicate x
  then l >-> P.map Left >-> j
  else r >-> P.map Right >-> j

berewt

module NodeLeafTree where

import Data.Bifunctor
import Data.List.NonEmpty

data Tree a b
   = Leaf a
   | Node b (NonEmpty (Tree a b))
   
instance Bifunctor Tree where

berewt

$ node --version
v6.9.1
$ node
> bar = {MyClass: function (x) {this.x = x}}
{ MyClass: [Function: MyClass] }
> foo = {MyClass(x) {this.x = x}}
{ MyClass: [Function: MyClass] }
> new bar.MyClass(2)
MyClass { x: 2 }
> new foo.MyClass(2)

berewt

module Data.Union

import Data.Vect

data Sum : {n: Nat} -> Vect n Type -> Type where
  isA: t -> {auto e: Elem t ts} -> Sum ts

data Orange = AnOrange String
data Apple = AnApple String

berewt

{import Control.Applicative ((<|>))
import Control.Monad
import Data.Data
import Data.Generics.Aliases
import Data.Monoid

trans ::  (MonadPlus m, Typeable a, Typeable b) => (b -> r) -> a -> m r
trans = mkQ mzero . (return .)

mcast :: (Typeable b, Typeable r) => (a -> Maybe b) -> a -> Maybe r