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 definitions for and implementations of kernel functions, intended
||| particularly for use in Gaussian processes.
module Model.Kernel

import Tensor
import Data.Nat

||| A `Kernel` function maps pairs of points in a feature space to the covariance between those two
||| points in some target space.
|||
||| @features The shape of the feature domain.
public export 0
Kernel : (0 features : Shape) -> Type
Kernel features = {sk, sk' : _} ->
  Tensor (sk :: features) Double ->
  Tensor (sk' :: features) Double ->
  Tensor [sk, sk'] Double

scaled_l2_norm : Tensor [] Double -> {d, n, n' : _}
 -> Tensor [n, S d] Double
 -> Tensor [n', S d] Double
 -> Tensor [n, n'] Double
scaled_l2_norm len x x' = let xs = broadcast {to=[n, n', S d]} $ expand 1 x
                           in reduce_sum 2 $ ((xs - broadcast (expand 0 x')) / len) ^ fill 2.0

||| The radial basis function, or squared exponential kernel. This is a stationary kernel with form
|||
||| (\mathbf x_i, \mathbf x_j) \mapsto \exp \left(- \frac{r^2}{2l^2} \right)
|||
||| where `r^2 = (\mathbf x_i - \mathbf x_j)^ \intercal (\mathbf x_i - \mathbf x_j)` and the
||| length scale `l > 0`.
|||
||| Two points that are close in feature space will be more tightly correlated than points that
||| are further apart. The distance over which the correlation reduces is given by the length
||| scale `l`. Smaller length scales result in faster-varying target values.
|||
||| @length_scale The length scale `l`.
export
rbf : (length_scale : Tensor [] Double) -> {d : _} -> Kernel [S d]
rbf length_scale x x' = exp (- scaled_l2_norm length_scale x x' / const 2.0)

||| The Matern kernel for parameter 5/2. This is a stationary kernel with form
|||
||| (\mathbf x_i, \mathbf x_j) \mapsto \sigma^2 \left(
|||   1 + \frac{\sqrt{5}r}{l} + \frac{5 r^2}{3 l^2}
||| \right) \exp \left( -\frac{\sqrt{5}r}{l} \right)
|||
||| where `r^2 = (\mathbf x_i - \mathbf x_j)^ \intercal (\mathbf x_i - \mathbf x_j)` and the
||| length scale `l > 0`.
|||
||| @amplitude The amplitude `\sigma`.
||| @length_scale The length scale `l`.
export
matern52 : (amplitude : Tensor [] Double) -> (length_scale : Tensor [] Double)
           -> {d : _} -> Kernel [S d]
matern52 amp len x x' = let d2 = const 5.0 * scaled_l2_norm len x x'
                            d = d2 ^ fill 0.5
                         in (amp ^ const 2.0) * (d2 / fill 3.0 + d + fill 1.0) *# exp (- d)

max_stars_repo_name: joelberkeley/spidr

max_issues_repo_name: joelberkeley/spidr

max_forks_repo_name: joelberkeley/spidr


text:
module IdrisScript

%access public export

JSRef : Type
JSRef = Ptr

%inline
jscall : (fname : String) -> (ty : Type) ->
          {auto fty : FTy FFI_JS [] ty} -> ty
jscall fname ty = foreign FFI_JS fname ty

data JSType = JSNumber
            | JSString
            | JSBoolean
            | JSFunction
            | JSNull
            | JSObject String
            | JSUndefined

implementation Eq JSType where
  JSNumber      == JSNumber      = True
  JSString      == JSString      = True
  JSBoolean     == JSBoolean     = True
  JSFunction    == JSFunction    = True
  JSNull        == JSNull        = True
  (JSObject c)  == (JSObject c') = c == c'
  JSUndefined   == JSUndefined   = True
  _             == _             = False

data JSValue : JSType -> Type where
  MkJSNumber    : JSRef -> JSValue JSNumber
  MkJSString    : JSRef -> JSValue JSString
  MkJSBoolean   : JSRef -> JSValue JSBoolean
  MkJSFunction  : JSRef -> JSValue JSFunction
  MkJSNull      : JSRef -> JSValue JSNull
  MkJSObject    : JSRef -> JSValue (JSObject con)
  MkJSUndefined : JSRef -> JSValue JSUndefined

JSArray : JSType
JSArray = JSObject "Array"

typeOf : JSRef -> JS_IO JSType
typeOf JSRef = do
  res <- jscall checkType (Ptr -> JS_IO Int) JSRef
  case res of
       0 => pure JSNumber
       1 => pure JSString
       2 => pure JSBoolean
       3 => pure JSFunction
       4 => pure JSUndefined
       5 => pure (JSObject !ctrName)
       _ => pure JSNull
where
  ctrName : JS_IO String
  ctrName =
    jscall "%0.constructor.name" (Ptr -> JS_IO String) JSRef

  checkType : String
  checkType =
    """(function(arg) {
         if (typeof arg == 'number')
           return 0;
         else if (typeof arg == 'string')
           return 1;
         else if (typeof arg == 'boolean')
           return 2;
         else if (typeof arg == 'function')
           return 3;
         else if (typeof arg == 'undefined')
           return 4;
         else if (typeof arg == 'object')
           return 5;
         else
           return 6;
       })(%0)"""

interface ToJS from (to : JSType) where
  toJS : from -> JSValue to

implementation ToJS String JSString where
  toJS str = MkJSString (believe_me str)

implementation ToJS Int JSNumber where
  toJS num = MkJSNumber (believe_me num)

implementation ToJS Double JSNumber where
  toJS num = MkJSNumber (believe_me num)

implementation ToJS Bool JSBoolean where
  toJS False = MkJSBoolean (believe_me 0)
  toJS True  = MkJSBoolean (believe_me 1)

interface FromJS (from : JSType) to where
  fromJS : JSValue from -> to

implementation FromJS JSString String where
  fromJS (MkJSString str) = believe_me str

implementation FromJS JSNumber Int where
  fromJS (MkJSNumber num) = cast {from=Double} {to=Int} (believe_me num)

implementation FromJS JSNumber Double where
  fromJS (MkJSNumber num) = believe_me num

implementation FromJS JSBoolean Bool where
  fromJS (MkJSBoolean b) = check (believe_me b)
    where
      check : Int -> Bool
      check b = b >= 1

||| Unpacks a JavaScript value
total
unpack : JSValue t -> JSRef
unpack (MkJSNumber JSRef)    = JSRef
unpack (MkJSString JSRef)    = JSRef
unpack (MkJSBoolean JSRef)   = JSRef
unpack (MkJSFunction JSRef)  = JSRef
unpack (MkJSNull JSRef)      = JSRef
unpack (MkJSObject JSRef)    = JSRef
unpack (MkJSUndefined JSRef) = JSRef

||| Packs up a JavaScript referenc into a JSValue
pack : JSRef -> JS_IO (t ** JSValue t)
pack JSRef =
  case !(typeOf JSRef) of
       JSNumber   => pure (JSNumber    ** MkJSNumber    JSRef)
       JSString   => pure (JSString    ** MkJSString    JSRef)
       JSBoolean  => pure (JSBoolean   ** MkJSBoolean   JSRef)
       JSFunction => pure (JSFunction  ** MkJSFunction  JSRef)
       JSNull     => pure (JSNull      ** MkJSNull      JSRef)
       JSObject c => pure (JSObject c  ** MkJSObject    JSRef)
       _          => pure (JSUndefined ** MkJSUndefined JSRef)

||| Log a value to console
log : JSValue t -> JS_IO ()
log js = jscall "console.log(%0)" (Ptr -> JS_IO ()) (unpack js)

||| Check if a value is undefined
isUndefined : JSValue t -> JS_IO Bool
isUndefined val = do
  ty <- typeOf (unpack val)
  pure $ ty == JSUndefined

||| Check if a value is null
isNull : JSValue t -> JS_IO Bool
isNull val = do
  ty <- typeOf (unpack val)
  pure $ ty == JSNull

||| Create a new object with a constructor function
||| @ con constructor function
||| @ args constructor arguments
new : (con : JSValue JSFunction)
   -> (args : JSValue JSArray)
   -> JS_IO (c ** JSValue (JSObject c))
new con args = do
  obj <- jscall  """(function(con,args) {
                          function Con(con, args) {
                            return con.apply(this, args);
                          }
                          Con.prototype = con.prototype;
                          return new Con(con, args);
                        })(%0, %1)""" (Ptr -> Ptr -> JS_IO Ptr)
                   (unpack con) (unpack args)
  pure $ (!(ctrName obj) ** MkJSObject obj)
where
  ctrName : JSRef -> JS_IO String
  ctrName JSRef =
    jscall "%0.constructor.name" (Ptr -> JS_IO String) JSRef

ext: idr

max_stars_repo_name: jimmyhmiller/IdrisScript

max_issues_repo_name: jimmyhmiller/IdrisScript

max_forks_repo_name: jimmyhmiller/IdrisScript


text:
module GRIN.Opts.NormaliseBind

import GRIN.AST
import GRIN.GrinM

mutual
    normaliseExp : Exp name -> Exp name
    normaliseExp (SimpleExp (Do e)) = normaliseExp e
    normaliseExp e@(SimpleExp _) = e
    normaliseExp (Bind val (Do e) rest) = bind val e (normaliseExp rest)
    normaliseExp (Bind val e rest) = Bind val e $ normaliseExp rest
    normaliseExp (Case val alts) = Case val $ mapExpAlt normaliseExp <$> alts

    bind : Val name -> Exp name -> Exp name -> Exp name
    bind v0 e0 = case normaliseExp e0 of
        SimpleExp e1 => Bind v0 e1
        Bind v1 (Do e1) rest => bind v1 e1 . bind v0 rest
        Bind v1 e1 rest => Bind v1 e1 . bind v0 rest
        Case v1 alts => Bind v0 (mkDo $ Case v1 $ mapExpAlt normaliseExp <$> alts)

export
normaliseBind : Monad m => GrinT name m ()
normaliseBind = mapProg $ mapExpProg normaliseExp


text:
module Helpers

import Control.Catchable

%default total
%access export

infixl 3 <*>, <&>
infixr 1 <=<, >=>

-- Panic -----------------------------------------------------------------------

panic : String -> a
panic = idris_crash

-- List extensions -------------------------------------------------------------

replace : Nat -> a -> List a -> List a
replace Z y (_ :: xs) = y :: xs
replace n y (x :: xs) = x :: replace (pred n) y xs
replace _ _ []        = []

delete : Nat -> List a -> List a
delete Z (_ :: xs) = xs
delete n (x :: xs) = x :: delete (pred n) xs
delete _ []        = []

||| Strict version of `Foldable.and`
and : List Bool -> Bool
and = foldl (\x, y => x && y) True

-- Tuple extensions ------------------------------------------------------------

bisequence : Applicative f => ( f a, f b ) -> f ( a, b )
bisequence = uncurry (liftA2 MkPair)

-- Applicative extensions ------------------------------------------------------

unit : Applicative f => f ()
unit = pure ()

(<&>) : Applicative f => f a -> f b -> f ( a, b )
(<&>) x y = MkPair <$> x <*> y

-- Monad extensions ------------------------------------------------------------

||| Left-to-right Kleisli composition of monads.
(>=>) : Monad m => (a -> m b) -> (b -> m c) -> (a -> m c)
f >=> g = \x => f x >>= g

||| Right-to-left Kleisli composition of monads. @('>=>')@, with the arguments flipped.
|||
||| Note: this operator resembles function composition `.`:
|||
|||     (.)   ::            (b ->   c) -> (a ->   b) -> a ->   c
|||     (<=<) :: Monad m => (b -> m c) -> (a -> m b) -> a -> m c
(<=<) : Monad m => (b -> m c) -> (a -> m b) -> (a -> m c)
(<=<) = flip (>=>)

-- Catchable extensions --------------------------------------------------------

ok : Applicative f => Catchable f e => a -> f a
ok = pure

-- String decomposition --------------------------------------------------------

strSnoc : String -> Char -> String
strSnoc s c = s ++ (singleton c)

between : Char -> Char -> String -> String
between a b str = strCons a (strSnoc str b)

partial
strLast : String -> Char
strLast str = strIndex str $ cast (length str) - 1

strMid : String -> String
strMid str = substr 1 (pred $ pred $ length str) str

mutual

  public export
  data Decons : String -> Type where
    Empty  : Decons ""
    Single : (char : Char) -> Decons (singleton char)
    Multi  : (first : Char) -> (last : Char) -> (rest : String) -> Decons (between first last rest)

  -- NOTE: we need `believe_me` because the operations are primitives in the end
  -- NOTE: we need `assert_total` because we know the string will not be empty by the match on `length`
  decons : (str : String) -> Decons str
  decons str with (length str)
    decons ""  | Z   = Empty
    decons str | S Z = believe_me $ Single (assert_total $ strHead str)
    decons str | n   = believe_me $ Multi (assert_total $ strHead str) (assert_total $ strLast str) (strMid str)

{-
test : String -> IO ()
test str with (decons str)
  test ""                        | Empty          = putStr $ "<empty>"
  test (singleton char)          | (Single char)      = putStr $ "<single " ++ (singleton char) ++ ">"
  test (between first last rest) | (Multi first last rest) = putStr $ singleton first ++ "<middle " ++ rest ++ ">" ++ singleton last
-}

max_stars_repo_name: mklinik/task-semantics

max_issues_repo_name: mklinik/task-semantics

max_forks_repo_name: mklinik/task-semantics


text:
module Idrlisp.Syntax

import Idrlisp.Value

%default covering

export
def : String -> Value -> Compile ()
def sym x = do
  load x
  Do $ Def sym
  Do $ Ldc Nil

export
set : String -> Value -> Compile ()
set sym x = do
  load x
  Do $ Set sym
  Do $ Ldc Nil

export
begin : List Value -> Compile ()
begin [] = Do $ Ldc Nil
begin [x] = load x
begin (x :: xs) = do
  load x
  Do Pop
  begin xs

export
if' : Value -> Value -> Value -> Compile ()
if' c t e = do
  load c
  t <- Block $ load t *> Do Leave
  e <- Block $ load e *> Do Leave
  Do $ Sel t e

export
fun : Pattern -> List Value -> Compile ()
fun pattern body = do
  body <- Block $ begin body *> Do Leave
  Do $ Ldf pattern body

export
macro : Pattern -> List Value -> Compile ()
macro pattern body = do
  body <- Block $ begin body
  Do $ Ldm pattern body

export
builtin : String -> Compile ()
builtin name = Do $ Ldb name

export
quote : Value -> Compile ()
quote expr = Do $ Ldc expr

mkSyntax : String -> (msig : List Bool) -> (sig : ValueArgsSignature) -> (SignatureType sig -> Compile ()) -> (String, Syntax)
mkSyntax name msig sig handle = (name, MkSyntax macroExpand compile)
  where
    macroExpand : List Value -> MacroExpand (List Value)
    macroExpand args = go msig args
      where
        go : List Bool -> List Value -> MacroExpand (List Value)
        go (s :: ss) (x :: xs) = [| ifThenElse s (expand True) pure x :: go ss xs |]
        go _ xs = traverse (expand True) xs

    compile : List Value -> Compile ()
    compile args =
      case match sig args of
        Nothing => Fail $ "Compile error: expected " ++ show (Sym name :: sig)
        Just x => handle x

export
syntaxList : List (String, Syntax)
syntaxList =
  [ mkSyntax "def" [False, True] [Sym "sym", Any "x"] $ uncurry def
  , mkSyntax "set!" [False, True] [Sym "sym", Any "x"] $ uncurry set
  , mkSyntax "begin" [] (Rest (Any "body")) begin
  , mkSyntax "if" [True, True, True] [Any "cond", Any "then", Any "else"] $ \(c, t, e) => if' c t e
  , mkSyntax "fun" [False] (Pat "pattern" :: Rest (Any "body")) $ uncurry fun
  , mkSyntax "macro" [False] (Pat "pattern" :: Rest (Any "body")) $ uncurry macro
  , mkSyntax "builtin" [False] [Sym "sym"] builtin
  , mkSyntax "quote" [False] [Any "expr"] quote
  ]

max_stars_repo_name: yubrot/idrlisp

max_issues_repo_name: yubrot/idrlisp

max_forks_repo_name: yubrot/idrlisp


text:
module Bautzen.Terrain

import Bautzen.GameUnit
import Bautzen.Pos

import Data.Strings.Extra

import Data.Fin
import Data.List
import Data.Maybe
import Data.Nat
import Data.Vect

%default total

-- Map & Terrain types

||| Terrain types
public export
data Terrain : Type where
  Clear : Terrain
  Wood : Terrain
  Rough : Terrain
  RoughWood : Terrain
  Hill : (base : Terrain) -> Terrain
  Village : (base : Terrain) -> Terrain
  Town : Terrain
  SupplySource : (side : Side) -> (base : Terrain) -> Terrain

public export
Show Terrain where
  show Clear                      = "Cl"
  show Wood                       = "Wd"
  show Rough                      = "Rg"
  show RoughWood                  = "RW"
  show (Hill base)                = "H (" ++ show base ++ ")"
  show (Village base)             = "V (" ++ show base ++ ")"
  show Town                       = "T"
  show (SupplySource Axis base)   = "SX (" ++ show base ++ ")"
  show (SupplySource Allies base) = "SA (" ++ show base ++ ")"

public export
isSupplyFor : Nation -> Terrain -> Bool
isSupplyFor nation (SupplySource s _) = side nation == s
isSupplyFor nation (Hill base) = isSupplyFor nation base
isSupplyFor nation (Village base) = isSupplyFor nation base
isSupplyFor  _ _ = False

||| Terrain type between hexes (eg. edges)
public export
data Connection : Type where
  Plain : Connection
  ||| A road or rail connection
  Road : (base : Connection) -> Connection
  River : (base : Connection) -> Connection
  Lake : Connection

public export
Show Connection where
  show Plain       = ""
  show (Road base) = "Rd (" ++ show base ++ ")"
  show (River base)= "Rv (" ++ show base ++ ")"
  show Lake        = "Lk"

public export
data Cost : Type where
  Impossible : Cost
  Zero : Cost
  Half : Cost -> Cost
  One : Cost -> Cost
  Two : Cost -> Cost

public export
cost : UnitType -> Terrain ->            Connection -> Cost
cost   unitType    (SupplySource _ base) cnx        = cost unitType base cnx
cost   _           _                     Lake       = Impossible
cost   unitType    terrain               (River cx) = One (cost unitType terrain cx)
cost   Infantry    terrain               (Road cnx) = Half (cost Infantry terrain cnx)
cost   Infantry    (Hill base)           cnx        = Two (cost Infantry base cnx)
cost   unitType    (Village t)           cnx        = One (cost unitType t cnx)
cost   Infantry    RoughWood cnx                    = One (One Zero)
cost   Infantry    _                     _          = One Zero
cost   unitType    (Hill base)           (Road cnx) = Half (cost unitType base cnx)
cost   _           (Hill _)              _          = Impossible
cost   unitType    terrain               (Road cnx) = Half (cost unitType terrain cnx)
cost   unitType    RoughWood             cnx        = Two (Two Zero)
cost   unitType    Rough                 cnx        = Two Zero
cost   _           Wood                  _          = Two Zero
cost   _           _                     _          = One Zero

public export
toNat : Cost -> Nat
toNat Impossible = 10000000 -- should probably be another type?
toNat Zero       = 0
toNat (Half x)   = divNatNZ (toNat x) 2 SIsNotZ
toNat (One x)    = S (toNat x)
toNat (Two x)    = S (S (toNat x))

public export
record Map where
  constructor MkMap
  hexes : List (Pos, Terrain)
  edges : List (Pos, List (Pos, Connection))

public export
tabulate : List (Pos, a) -> Vect 13 (Vect 23 (Maybe a))
tabulate = foldr append table
  where
    append : (Pos, a) -> Vect 13 (Vect 23 (Maybe a)) -> Vect 13 (Vect 23 (Maybe a))
    append (Hex c r, z) vect with (natToFin c 23, natToFin r 13)
      append (Hex c r, z) vect | (Just c', Just r') = let row = index r' vect
                                                      in replaceAt r' (replaceAt c' (Just z) row) vect
      append (Hex c r, a) vect | (_, _) = vect

    table : Vect 13 (Vect 23 (Maybe a))
    table = replicate 13 (replicate 23 Nothing)

public export
Show Map where
  show (MkMap hexes edges) =
    "Map hexes= " ++ unlines terrain ++ "\n   edges=" ++ unlines connections
    where
      terrain : List String
      terrain = toList $ map show (tabulate hexes)

      connections : List String
      connections = toList $ map show (tabulate edges)

||| Retrieve the `Terrain`s in a position
public export
terrain : Pos -> Map -> Terrain
terrain pos map =
  case lookup pos (hexes map) of
     Nothing => Clear
     (Just ts) => ts

||| Retrieve the types of connections between 2 hexes
public export
connection : Pos -> Pos -> Map -> Connection
connection x y map =
  fromMaybe Plain (lookup x (edges map) >>= lookup y)

||| Get the `Pos`itions of all supply sources for given `Nation` on the map
public export
supplySources : Nation -> Map -> List Pos
supplySources n (MkMap hexes edges) = map fst $ filter (isSupplyFor n . snd) hexes

public export
TestMap : Map
TestMap =
  MkMap [ (Hex 3 4, Wood)
        , (Hex 4 4, Clear)
        , (Hex 4 5, Hill Rough)
        , (Hex 5 4, Clear)
        , (Hex 3 5, RoughWood)
        , (Hex 2 4, Rough)
        , (Hex 2 3, Hill (RoughWood))
        , (Hex 3 3, Wood)
        , (Hex 4 3, Town)
        , (Hex 8 6, Clear)
        , (Hex 8 7, Village Clear)
        , (Hex 7 7, Hill Rough)
        , (Hex 10 2, Village Wood)
        , (Hex 10 3, Clear)
        ]
        [ (Hex 4 4, [ (Hex 5 4, Road Plain) ])
        , (Hex 8 6, [ (Hex 8 7, Lake) ])
        , (Hex 8 7, [ (Hex 7 7, Road Plain) ])
        , (Hex 10 3, [ (Hex 10 2, Road (River Plain)) ])
        ]

max_stars_repo_name: steshaw/hsgames

max_issues_repo_name: steshaw/hsgames

max_forks_repo_name: steshaw/hsgames


text:
module Sub03LTE216t81

import ProofColDivSeqBase
import ProofColDivSeqPostulate

%default total

-- 6(36t+13)+3 --DE[3,0,-4]--> 6(2t)+3
export
lte216t81 : (m : Nat) -> LTE (S (m+m))
  (S (((S (S ((m+m+m)+(m+m+m))))+(S (S ((m+m+m)+(m+m+m))))) + ((S (S ((m+m+m)+(m+m+m))))+(S (S ((m+m+m)+(m+m+m))))) + ((S (S ((m+m+m)+(m+m+m))))+(S (S ((m+m+m)+(m+m+m)))))))
lte216t81 Z     = (lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . LTESucc) LTEZero
lte216t81 (S m) =
  let lemma = lte216t81 m in

  rewrite (sym (plusSuccRightSucc m m)) in

  rewrite (sym (plusSuccRightSucc (plus m m) m)) in

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

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

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

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

    (lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . LTESucc . LTESucc) lemma


text:
data Last : List a -> a -> Type where
    LastOne : Last [value] value
    LastCons : (prf : Last xs value) -> Last (x :: xs) value

last123 : Last [1, 2, 3] 3
last123 = LastCons (LastCons LastOne)

notInNil : Last [] value -> Void
notInNil LastOne impossible
notInNil (LastCons _) impossible

notLast : (notHere : (value = x) -> Void) -> Last [x] value -> Void
notLast notHere LastOne = notHere Refl
notLast notHere (LastCons prf) = notInNil prf

notLastInTail : (notLastPrf : Last (y :: xs) value -> Void) -> Last (x :: (y :: xs)) value -> Void
notLastInTail notLastPrf (LastCons prf) = notLastPrf prf

isLast : DecEq a => (xs : List a) -> (value : a) -> Dec (Last xs value)
isLast [] value = No notInNil
isLast (x :: []) value =
    case decEq value x of
        Yes Refl => Yes LastOne
        No notHere => No (notLast notHere)
isLast (x :: (y :: xs)) value =
    case isLast (y :: xs) value of
        Yes prf => Yes (LastCons prf)
        No notLastPrf => No (notLastInTail notLastPrf)


text:
module Default

happyPairs : List (Nat, Char)
happyPairs = map (uncurry $ \ c, n => (n, c)) [('a', 1)]

-- In Idris1 `sadPairs` is rejected with the following error:
--    |
-- 10 | sadPairs = map (\ (c, n) => (n, c)) [('a', 1)]
--    |                             ~~
-- When checking right hand side of Default.case block in sadPairs at Default.idr:10:19-24 with expected type
--         (Nat, Char)

-- When checking argument a to constructor Builtins.MkPair:
--         Type mismatch between
--                 Integer (Type of n)
--         and
--                 Nat (Expected type)

sadPairs : List (Nat, Char)
sadPairs = map (\ (c, n) => (n, c)) [('a', 1)]


text:
module GenericAdder

%default total

AdderType : (numargs : Nat) -> (elemType : Type) -> Type
AdderType Z ty = ty
AdderType (S k) ty = (next : ty) -> AdderType k ty

adder : Num elemType => (numargs : Nat) -> (acc : elemType) -> AdderType numargs elemType
adder Z acc = acc
adder (S k) acc = \next => adder k (acc + next)

max_stars_repo_name: timmyjose-study/tdd-with-idris

max_issues_repo_name: timmyjose-study/tdd-with-idris

max_forks_repo_name: timmyjose-study/tdd-with-idris


text:
module Main

import Go

-- XXX make it total

%include Go "bufio"
%include Go "net"

go : GIO () -> GIO ()
go action = gocall (Function "Go") (Raw (GIO ()) -> GIO ()) (MkRaw action)

Listener : Type
Listener = GoInterface "net.Listener"

Conn : Type
Conn = GoInterface "net.Conn"

Addr : Type
Addr = GoInterface "net.Addr"

implementation Show Addr where
  show addr = unsafePerformIO $ gocall (Method addr "String") (Addr -> GIO String) addr

GoError : Type
GoError = GoInterface "error"

toEither : (a, Maybe GoError) -> Either GoError a
toEither (_, Just e) = Left e
toEither (x, Nothing) = Right x

errorDesc : GoError -> String
errorDesc error = unsafePerformIO $ gocall (Method error "Error") (GoError -> GIO String) error

accept : Listener -> GIO (Either GoError Conn)
accept listener =
  map toEither $ gocall (Method listener "Accept") (Listener -> GIO (Conn, Maybe GoError)) listener

listen : String -> String -> GIO (Either GoError Listener)
listen net laddr =
   map toEither $ gocall (Function "net.Listen")
           (String -> String -> GIO (Listener, Maybe GoError))
           net laddr

remoteAddr : Conn -> Addr
remoteAddr conn =
  unsafePerformIO $ gocall (Method conn "RemoteAddr") (Conn -> GIO Addr) conn

Reader : Type
Reader = GoInterface "bufio.Reader"

Writer : Type
Writer = GoInterface "bufio.Writer"

-- XXX should be a reader, not a Conn
newReader : Conn -> GIO Reader
newReader conn = do
  (MkGoPtr val) <- gocall (Function "bufio.NewReader") (Conn -> GIO (GoPtr Reader)) conn
  pure val

newWriter : Conn -> GIO Writer
newWriter conn = do
  (MkGoPtr val) <- gocall (Function "bufio.NewWriter") (Conn -> GIO (GoPtr Writer)) conn
  pure val

readString : Reader -> Byte -> GIO (Either GoError String)
readString reader delim = map toEither $
  gocall (Method reader "ReadString") (Reader -> Byte -> GIO (String, Maybe GoError)) reader delim

writeString : Writer -> String -> GIO (Int, Maybe GoError)
writeString writer s =
  gocall (Method writer "WriteString") (Writer -> String -> GIO (Int, Maybe GoError)) writer s

flush : Writer -> GIO (Maybe GoError)
flush writer = gocall (Method writer "Flush") (Writer -> GIO (Maybe GoError)) writer

echoServer : Listener -> GIO ()
echoServer listener =
  do Right conn <- accept listener
       | Left e => putStrLn' ("Accepting went wrong: " ++ errorDesc e)
     putStrLn' $ "Got a client! It's " ++ show (remoteAddr conn)
     go $ do
       reader <- newReader conn
       writer <- newWriter conn
       handleLine reader writer
     echoServer listener
  where
    handleLine : Reader -> Writer -> GIO ()
    handleLine reader writer = do
      Right line <- readString reader (MkByte '\n')
        | Left e => putStrLn' ("Could not read line: " ++ errorDesc e)
      (_, Nothing) <- writeString writer line
        | (_, Just e) => putStrLn' ("Could not send line back: " ++ errorDesc e)
      flush writer
      handleLine reader writer

main : GIO ()
main = do
  Right listener <- listen "tcp" ":1234"
    | Left e => putStrLn' ("Could not create listener: " ++ errorDesc e)
  echoServer listener

max_stars_repo_name: Trundle/idris-go

max_issues_repo_name: Trundle/idris-go

max_forks_repo_name: Trundle/idris-go


text:
module WebServer

import WebServer.JS
import public WebServer.Requests

%lib Node "http"
%default total

IORequestHandler : Type
IORequestHandler = (req : Ptr) -> (res : Ptr) -> JS_IO ()

time : String -> JS_IO ()
time = js "console.time(%0)" (String -> JS_IO ())

timeLog : String -> Code -> JS_IO ()
timeLog label code =
  js "console.timeLog(%0, %1)"
     (String -> Int -> JS_IO ())
     label (cast code)

pureHandler2IOHandler : RequestHandler -> IORequestHandler
pureHandler2IOHandler f ptrReq ptrRes = do
  let req = requestFromRaw !(method ptrReq) !(url ptrReq)
  let res = f req
  let label = show (method req) ++ " " ++ path req
  time label
  setHeaders ptrRes !(parseHeader `traverse` headers res)
  writeHead ptrRes (code res)
  write ptrRes (body res)
  end ptrRes
  timeLog label (code res)

pureHandler2TwoArgChain : RequestHandler -> TwoArgChain
pureHandler2TwoArgChain f = MkJsFn $ MkJsFn . pureHandler2IOHandler f

export
partial
startServer : (port : Nat) ->
              (onListening: JS_IO ()) ->
              RequestHandler ->
              JS_IO ()
startServer port onListening onRequest = do
  server <- js "http.createServer()" (JS_IO Ptr)
  js "%0.listen(%1)" SendInt server (cast port)
  js "%0.on('request', (req, res) => { %1(req)(res)() })"
     (Ptr -> TwoArgChain -> JS_IO Ptr)
     server (pureHandler2TwoArgChain onRequest)
  js "%0.on('listening', %1)"
     (Ptr -> JsFn (() -> JS_IO ()) -> JS_IO ())
     server (MkJsFn (\_ => onListening))
  js "process.on('SIGTERM', process.exit)"
     (JS_IO ())

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

max_stars_repo_name: camelpunch/idris-web-server

max_issues_repo_name: camelpunch/idris-web-server

max_forks_repo_name: camelpunch/idris-web-server


text:
module Network.Wai
import Control.ST
import Network.Socket.Data

public export
record HttpResponseCode where
  constructor MkHttpResponseCode
  responseNumber : Nat  -- TODO: Static guarantee it is in range?
  responseText : String -- TODO: Static guarantee String has no whitespace?

public export
record HttpHeader where
  constructor MkHttpHeader
  headerName: String -- TODO: Static guarantee it doesn't have whitespace?
  headerValue: String -- TODO: Static guarantee it doesn't have newline?

public export
record HttpRequest where
  constructor MkHttpRequest
  method : String
  headers : List HttpHeader
  body : String

public export
record HttpResponse where
  constructor MkHttpResponse
  code : HttpResponseCode
  headers : List HttpHeader
  body : String

public export
data InvalidRequestOr : a -> Type where
  ValidRequest : a -> InvalidRequestOr a
  InvalidRequest : InvalidRequestOr a

public export
record HttpEngine (m : Type -> Type) where
  constructor MkHttpEngine
  Application : Type
  EngineState : Type
  httpEngineActions : EngineState -> (ty : Type) -> List (Action ty)
  pendingRequestVar : EngineState -> Var
  PendingRequest : Type
  sendResponse : (engineState: EngineState) -> HttpResponse ->
                     ST m () ((remove (pendingRequestVar engineState) PendingRequest)::
                              (httpEngineActions engineState ()))
  mkApplication : ((engineState : EngineState) ->
                   HttpRequest ->
                   ST m () ((remove (pendingRequestVar engineState) PendingRequest)::
                            (httpEngineActions engineState ()))
                  ) -> Application
  runApplication : (bindTo: Maybe SocketAddress) -> (port: Int) ->
                   (app: Application) -> ST m String []

export
getHttpHeader : (wantedHeaderName : String) -> (req : HttpRequest) -> Maybe HttpHeader
getHttpHeader hn req = find (\h => toLower (headerName h) == toLower hn) (headers req)

export
http200 : HttpResponseCode
http200 = MkHttpResponseCode 200 "OK"


text:
data BST : a -> Type where
  Leaf : BST a
  Node : (root : a) -> (lt : BST a) -> (rt : BST a) -> BST a

-- Checking that we can look under the @ to get rt and lt
total
insert : Ord a => a -> BST a -> BST a
insert p Leaf = Node p Leaf Leaf
insert p tree@(Node root lt rt) =
  case p `compare` root of
    GT => Node root lt (insert p rt)
    EQ => tree
    LT => Node root (insert p lt) rt


text:
> module Real.Postulates

> %default total
> %access public export

* Reals

> ||| Real numbers
> postulate Real : Type

* Constants

> ||| Zero
> postulate zero : Real

* Operations

> |||
> postulate fromNat : Nat -> Real

> ||| Addition of real numbers
> postulate plus : Real -> Real -> Real

> ||| Multiplication of real numbers
> postulate mult : Real -> Real -> Real

> ||| Subtrantion of real numbers
> postulate minus : Real -> Real -> Real

> ||| Division of real numbers
> postulate div : Real -> Real -> Real

> ||| Division of real numbers
> postulate abs : Real -> Real

* Relations (as predicates)

> ||| Smaller or equal
> postulate LTE : Real -> Real -> Type

> ||| Greater then
> GT : Real -> Real -> Type
> GT x y = Not (x `LTE` y)

> {-

> ---}

ext: lidr

max_stars_repo_name: zenntenn/IdrisLibs

max_issues_repo_name: zenntenn/IdrisLibs

max_forks_repo_name: zenntenn/IdrisLibs


text:
{-
(+) : Nat -> Nat -> Nat
     Z + y = y
(S k) + y = S(k+y)
 -}

 total
ascLaw : (a:Nat) -> (b:Nat) -> (c:Nat) -> (a + (b+c)) = ((a+b)+c)
{-  normal form of LHS: Z+(Z+c) = Z+c = c;
    Normal form of RHS: (Z+Z)+c = Z+c=c;
   so {c=c}=Refl proves it. -}
ascLaw Z Z c = Refl

{-LHS:  Z + ((S k)+ c) = Z+( S( k+c))=Z+(S (k+c)) = S (k+c),
    RHS: (Z+(S k)) + c = (S k)+c = S(k+c).  Again Refl. -}
ascLaw Z (S k) c = Refl

{- So now we have covered Z+(b + c) = (Z+b)+c, now change Z to S j -}
{-  normal form of LHS: (S j)+(b+c) = S(j +(b+c));
     normal form of RHS: ((S j)+b)+c = S(j+b) +c= S ( (j+b)+c);
    NOT THE SAME, but we can induct on j+(b+c)=(j+b)+c and then
    Apply S to both sides. Applying S to both side of  and equation is
    Done by “cong”  -}
ascLaw (S j) b c = cong (ascLaw j b c)

total cmLaw : (a:Nat) -> (b:Nat) -> (a+b) = (b+a)
cmLaw Z Z = Refl
cmLaw Z (S k) = cong {f=S} (left_id k) where
    left_id : (j:Nat) -> j = j+0
    left_id Z = Refl
    left_id (S d) = cong {f=S} (left_id d)
cmLaw (S j) b = rewrite sucMove b j in cong {f=S} (cmLaw j b) where
    sucMove : (j:Nat) -> (k:Nat) -> j + (S k) = S(j+k)
    sucMove Z k = Refl
    sucMove (S j) k = cong {f=S} (sucMove j k)

max_stars_repo_name: algeboy/BlackBoxType

max_issues_repo_name: algeboy/BlackBoxType

max_forks_repo_name: algeboy/BlackBoxType


text:
module PairingHeap

import Heap

%default total
%access private

export
data PairingHeap a = E | T a (List (PairingHeap a))

mutual
  mergePairs : Ord a => List (PairingHeap a) -> PairingHeap a
  mergePairs [] = E
  mergePairs [h] = h
  mergePairs (h1 :: h2 :: hs) = merge (merge h1 h2) (mergePairs hs)

  Heap PairingHeap where
    empty = E
    isEmpty E = True
    isEmpty _ = False

    insert x h = merge (T x []) h

    merge h E = h
    merge E h = h
    merge h1@(T x hs1) h2@(T y hs2) =
      if x < y then T x (h2 :: hs1) else T y (h1 :: hs2)

    findMin E = idris_crash "empty heap"
    findMin (T x hs) = x

    deleteMin E = idris_crash "empty heap"
    deleteMin (T x hs) = mergePairs hs


text:
{-
42
4.2
it works!
True
00000000-0000-0000-0000-000000000000
Void VoidFunction()
System.String exportedBoolToString(Boolean)
Void showMethod(System.Type, System.String)
before exportedVoidIO
exported!
after exportedVoidIO
exportedBoolToStringIO True
exportedBoolToStringIO => True
Alan Kay
Kay, Alan
3
-}

module Main

import CIL.FFI

AssemblyTy : CILTy
AssemblyTy = corlibTy "System.Reflection.Assembly"

Assembly : Type
Assembly = CIL AssemblyTy

MethodInfo : Type
MethodInfo = corlib "System.Reflection.MethodInfo"

instance IsA Object MethodInfo where {}

GetExecutingAssembly : CIL_IO Assembly
GetExecutingAssembly =
  invoke (CILStatic AssemblyTy "GetExecutingAssembly")
         (CIL_IO Assembly)

GetType : Assembly -> String -> Bool -> CIL_IO RuntimeType
GetType =
  invoke (CILInstance "GetType")
         (Assembly -> String -> Bool -> CIL_IO RuntimeType)

GetMethod : RuntimeType -> String -> CIL_IO MethodInfo
GetMethod =
  invoke (CILInstance "GetMethod")
         (RuntimeType -> String -> CIL_IO MethodInfo)

Invoke : MethodInfo -> Object -> ObjectArray -> CIL_IO Object
Invoke =
  invoke (CILInstance "Invoke")
         (MethodInfo -> Object -> ObjectArray -> CIL_IO Object)

%inline
SystemMathMax : CILForeign
SystemMathMax = CILStatic (CILTyRef "mscorlib" "System.Math") "Max"

namespace System.Math.Int32
  Max : Int -> Int -> CIL_IO Int
  Max = invoke SystemMathMax (Int -> Int -> CIL_IO Int)

namespace System.Math.Float32
  Max : Double -> Double -> CIL_IO Double
  Max = invoke SystemMathMax (Double -> Double -> CIL_IO Double)

namespace System.Text
  StringBuilder : Type
  StringBuilder = corlib "System.Text.StringBuilder"

  instance IsA Object StringBuilder where {}

  %inline
  invokeStringBuilder : String -> StringBuilder -> String -> CIL_IO StringBuilder
  invokeStringBuilder fn = invoke (CILInstance fn) (StringBuilder -> String -> CIL_IO StringBuilder)

  Append : StringBuilder -> String -> CIL_IO StringBuilder
  Append = invokeStringBuilder "Append"

  AppendLine : StringBuilder -> String -> CIL_IO StringBuilder
  AppendLine = invokeStringBuilder "AppendLine"

namespace System.Console
  Write : String -> CIL_IO ()
  Write = invoke (CILStatic (corlibTy "System.Console") "Write") (String -> CIL_IO ())

GuidTy : CILTy
GuidTy = corlibTyVal "System.Guid"

Guid : Type
Guid = CIL $ GuidTy

instance IsA Object Guid where {}

NewGuid : CIL_IO Guid
NewGuid =
  invoke (CILStatic GuidTy "NewGuid")
         (CIL_IO Guid)

ParseGuid : String -> CIL_IO Guid
ParseGuid =
  invoke (CILStatic GuidTy "Parse")
         (String -> CIL_IO Guid)

EmptyGuid : CIL_IO Guid
EmptyGuid =
  invoke (CILStaticField GuidTy "Empty")
         (CIL_IO Guid)

testValueType : CIL_IO ()
testValueType = do
  guid  <- NewGuid
  guid' <- ParseGuid !(ToString guid)
  printLn !(Equals guid guid')
  ToString !EmptyGuid >>= putStrLn

testExportedVoidFunction : RuntimeType -> CIL_IO ()
testExportedVoidFunction type = do
  putStrLn "before exportedVoidIO"
  exportedVoidIO' <- type `GetMethod` "VoidFunction"
  ret <- Invoke exportedVoidIO' (believe_me null) (believe_me null)
  putStrLn "after exportedVoidIO"

testExportedBoolToStringIO : RuntimeType -> CIL_IO ()
testExportedBoolToStringIO type = do
  exportedBoolToStringIO' <- type `GetMethod` "exportedBoolToStringIO"
  ret <- Invoke exportedBoolToStringIO' (believe_me null) !(fromList [True])
  putStrLn $ "exportedBoolToStringIO => " ++ !(ToString ret)

record Person where
  constructor MkPerson
  firstName, lastName : String

-- And now for something completely different...
-- Let's use the IMPORTING FFI to test the EXPORTING FFI

||| Descriptor for the type hosting all exported functions.
TheExportsTy : CILTy
TheExportsTy = CILTyRef "" "TheExports"

||| The foreign view of the exported type Person
||| is a struct with a single field `ptr`.
ExportedPerson : Type
ExportedPerson = CIL $ CILTyVal "" "Person"

||| Converts a foreign reference to an exported data type
||| into its internal representation.
unForeign : ExportedPerson -> CIL_IO Person
unForeign ep = do
 ptr <- invoke (CILInstanceField "ptr") (ExportedPerson -> CIL_IO Ptr) ep
 return $ believe_me ptr

||| Invokes the exported function `createPerson` via the FFI.
invokeCreatePerson : String -> String -> CIL_IO ExportedPerson
invokeCreatePerson =
  invoke (CILStatic TheExportsTy "createPerson")
         (String -> String -> CIL_IO ExportedPerson)

%inline
invokeAccessor : String -> ExportedPerson -> CIL_IO String
invokeAccessor n =
  invoke (CILStatic TheExportsTy n)
         (ExportedPerson -> CIL_IO String)

testExportedRecord : CIL_IO ()
testExportedRecord = do
  -- exercise the foreign view of the record
  ep <- invokeCreatePerson "Alan" "Kay"
  putStrLn $ !(invokeAccessor "firstName" ep) ++ " " ++ !(invokeAccessor "lastName" ep)
  -- internal view should work just the same
  p  <- unForeign ep
  putStrLn $ lastName p ++ ", " ++ firstName p

testOverloadedStaticMethod : CIL_IO ()
testOverloadedStaticMethod = do
  Max (the Int 42) (the Int 1) >>= printLn
  Max 4.2 1.0 >>= printLn

testInstanceMethods : CIL_IO ()
testInstanceMethods = do
  sb <- new (CIL_IO StringBuilder)
  Append sb "it "
  AppendLine sb "works!"
  ToString sb >>= Write

showMethod : RuntimeType -> String -> CIL_IO ()
showMethod t n = do
  m <- t `GetMethod` n
  ToString m >>= putStrLn

testBoxingUnboxing : RuntimeType -> CIL_IO ()
testBoxingUnboxing type = do
  meth <- type `GetMethod` "exportedIncInt"
  ret <- Invoke meth (believe_me null) !(fromList [2])
  ToString ret >>= putStrLn

main : CIL_IO ()
main = do
  testOverloadedStaticMethod
  testInstanceMethods
  testValueType

  asm <- GetExecutingAssembly
  type <- GetType asm "TheExports" True
  for_ ["VoidFunction", "exportedBoolToString", "showMethod"] $
    showMethod type

  testExportedVoidFunction type
  testExportedBoolToStringIO type
  testExportedRecord
  testBoxingUnboxing type

-- Exports

createPerson : String -> String -> Person
createPerson = MkPerson

exportedVoidIO : CIL_IO ()
exportedVoidIO = putStrLn "exported!"

exportedBoolToString : Bool -> String
exportedBoolToString = show

exportedBoolToStringIO : Bool -> CIL_IO String
exportedBoolToStringIO b = do
  putStrLn $ "exportedBoolToStringIO " ++ show b
  return $ show b

exportedIncInt : Int -> Int
exportedIncInt i = i + 1

exports : FFI_Export FFI_CIL "TheExports" [] -- declare exported functions on a type with given name
exports =
  Data Person "Person" $
  Fun createPerson CILDefault $ -- export function under original name
  Fun firstName CILDefault $ -- record field accessors are just functions and can be as easily exported
  Fun lastName CILDefault $
  Fun exportedVoidIO (CILExport "VoidFunction") $ -- export function under custom name
  Fun exportedBoolToString CILDefault $
  Fun exportedBoolToStringIO CILDefault $ -- export IO with return value
  Fun exportedIncInt CILDefault $ -- pass and get back value type
  Fun showMethod CILDefault -- export signature containing CIL type
  End

max_stars_repo_name: Despair/idris-cil

max_issues_repo_name: Despair/idris-cil

max_forks_repo_name: Despair/idris-cil


text:
module Data.Time.LocalTime.CalendarDiffTime

import Data.Fixed
import Data.Time.Clock.DiffTime
import Data.Time.Calendar.CalendarDiffDays

import Generics.Derive

%default total
%language ElabReflection

-- --------------------------------------------------------------------------

public export
record CalendarDiffTime where
  constructor MkCalendarDiffTime
  month : Integer
  time : NominalDiffTime
%runElab derive "CalendarDiffTime" [Generic, Eq, DecEq]

public export
Semigroup CalendarDiffTime where
  x <+> y = MkCalendarDiffTime (x.month + y.month) (x.time + y.time)
public export
Monoid CalendarDiffTime where
  neutral = MkCalendarDiffTime 0 0

public export
Show CalendarDiffTime where
  show x = "P" ++ show x.month ++ "MT" ++ show x.time

export calendarTimeDays : CalendarDiffDays -> CalendarDiffTime
calendarTimeDays x = MkCalendarDiffTime x.month $ daysToDiffTime x.day

export calendarTimeTime : NominalDiffTime -> CalendarDiffTime
calendarTimeTime dt = MkCalendarDiffTime 0 dt

||| Scale by a factor. Note that @scaleCalendarDiffTime (-1)@ will not perfectly invert a duration, due to variable month lengths.
export scaleCalendarDiffTime : Integer -> CalendarDiffTime -> CalendarDiffTime
scaleCalendarDiffTime k x = MkCalendarDiffTime (k * x.month) (scale k x.time)

-- --------------------------------------------------------------------------
-- vim: tw=80 sw=2 expandtab :


text:
module Data.Queue1.Properties

import Data.List
import Data.List1
import Data.SnocList
import Data.Queue1

import Syntax.WithProof

%default total

------------------
--- Properties ---
------------------

export
toList1_singleton : (x : a) -> Queue1.toList1 (singleton x) = singleton x
toList1_singleton x = Refl

export
toList1_add : (q : Queue1 a) -> (xs : List a) -> Queue1.toList1 (foldl (flip Queue1.add) q xs) === (toList1 q `appendl` xs)
toList1_add q [] with 0 (toList1 q)
  toList1_add q [] | (_:::xs) = rewrite appendNilRightNeutral xs in Refl
toList1_add (MkQueue right left@(l:::ls)) (y :: ys) = do
  rewrite toList1_add (MkQueue (right :< y) left) ys
  rewrite sym $ appendAssociative ls (right <>> [y]) ys
  rewrite chipsAsListAppend right [y]
  rewrite sym $ appendAssociative (cast right) [y] ys
  rewrite appendAssociative ls (cast right) (y::ys)
  Refl

export
toList1_filter : (f : a -> Bool) -> (q : Queue1 a) -> Queue1.toList1 <$> filter f q = filter f (Queue1.toList1 q)
toList1_filter f (MkQueue right left) = do
  rewrite toListAppendl left (cast right)
  rewrite filterAppend f (forget left) (cast right)
  rewrite fromListAppend (filter f $ forget left) (filter f $ cast right)
  case @@ fromList (filter f $ forget left) of
    (Nothing ** prfL) => do
      rewrite prfL
      rewrite toListFilter f right
      case @@ fromList (filter f $ cast right) of
        (Nothing ** prfR) => rewrite prfR in Refl
        (Just r1 ** prfR) => do
          rewrite prfR
          rewrite appendlNilRightNeutral r1
          Refl
    (Just l1 ** prfL) => do
      rewrite prfL
      rewrite toListFilter f right
      case @@ filter f (toList right) of
        ([] ** prfR) => do
          rewrite prfR
          rewrite appendlNilRightNeutral l1
          Refl
        (_::_ ** prfR) => rewrite prfR in Refl


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 definitions and utilities for datasets.
module Data

import Tensor

||| Observed pairs of data points from feature and target domains. Data sets such as this are
||| commonly used in supervised learning settings.
|||
||| @features The shape of the feature domain.
||| @targets The shape of the target domain.
public export
data Dataset : (0 features : Shape) -> (0 targets : Shape) -> Type where
  MkDataset : {s : _} -> Tensor (S s :: features) Double
           -> Tensor (S s :: targets) Double
           -> Dataset features targets

||| Concatenate two datasets along their leading axis.
export
Semigroup (Dataset features targets) where
  (MkDataset x y) <+> (MkDataset x' y') = MkDataset (concat x x') (concat y y')


text:
-- examples in "Type-Driven Development with Idris"
-- chapter 9

import Data.Vect

-- check that all functions are total
%default total

--
-- section 9.1
--

maryInVector : Elem "Mary" ["Peter", "Paul", "Mary"]
maryInVector = There (There Here)

removeElem2 : (value : a) -> (xs : Vect (S n) a) ->
             (prf : Elem value xs) ->
             Vect n a
removeElem2 value (value :: ys) Here = ys
removeElem2 {n = Z} value (y :: []) (There later) = absurd later
removeElem2 {n = (S k)} value (y :: ys) (There later)
  = y :: removeElem2 value ys later

removeElem_auto : (value : a) -> (xs : Vect (S n) a) ->
                  {auto prf : Elem value xs} ->
                  Vect n a
removeElem_auto value xs {prf} = removeElem2 value xs prf

removeElem : (value : a) -> (xs : Vect (S n) a) ->
              {auto prf : Elem value xs} ->
              Vect n a
removeElem value (value :: ys) {prf = Here} = ys
removeElem {n = Z} value (y :: []) {prf = There later} = absurd later
removeElem {n = (S k)} value (y :: ys) {prf = There later}
  = y :: removeElem value ys

--
-- section 9.2
-- see Hangman.idr
--

max_stars_repo_name: pascalpoizat/idris-book

max_issues_repo_name: pascalpoizat/idris-book

max_forks_repo_name: pascalpoizat/idris-book


text:
module CatenableList

%default total
%access private

public export
interface CatenableList (c : Type -> Type) where
  empty : c a
  isEmpty : c a -> Bool

  cons : a -> c a -> c a
  snoc : c a -> a -> c a
  (++) : c a -> c a -> c a

  head : c a -> a
  tail : c a -> c a


text:
module Problem01
-- Find the last element of a list.

myLastV : Vect (S n) a -> a
myLastV [x] = x
myLastV (_::x::xs) = myLastV (x::xs)

myIsCons : List a -> Bool
myIsCons [] = False
myIsCons (x::xs) = True

myLastL : (l : List a) -> (ok : isCons l = True) -> a
myLastL [x] _ = x
myLastL (y::x::xs) _ = myLastL (x::xs) Refl

max_stars_repo_name: jesyspa/jesyspa-s-toy-projects

max_issues_repo_name: jesyspa/jesyspa-s-toy-projects

max_forks_repo_name: jesyspa/jesyspa-s-toy-projects


text:
module Protocol.IDE.Holes

import Protocol.SExp

%default total

public export
record HolePremise where
  constructor MkHolePremise
  name : String -- Future: send more structured representation of:
                -- im/explicity (+ default value?) + quantity
  type : String -- Future: String + highlighting info

export
SExpable HolePremise where
  toSExp premise =
    SExpList [ StringAtom premise.name
             , StringAtom premise.type
             , SExpList [] -- TODO: metadata
             ]

export
FromSExpable HolePremise where
  fromSExp (SExpList [ StringAtom name
             , StringAtom type
             , SExpList [] -- TODO: metadata
             ]) = do pure $ MkHolePremise
                      {name, type}
  fromSExp _ = Nothing

public export
record HoleData where
  constructor MkHoleData
  name : String
  type : String -- Future : String + highlighting info
  context : List HolePremise

export
SExpable HoleData where
  toSExp hole = SExpList
    [ StringAtom (show  hole.name)
    , toSExp hole.context
    , SExpList [ toSExp hole.type   -- Conclusion
               , SExpList[]]        -- TODO: Highlighting information
    ]

export
FromSExpable HoleData where
  fromSExp (SExpList
    [ StringAtom name
    , context
    , SExpList [ conclusion
               , SExpList[]]        -- TODO: Highlighting information
    ]) = do pure $ MkHoleData {name, type = !(fromSExp conclusion), context = !(fromSExp context)}
  fromSExp _ = Nothing


text:
module TCPServer

import Effects
import Effect.StdIO
import IdrisNet.TCP.TCPServer
import IdrisNet.TCP.TCPCommon
import Network.Socket

forkServerLoop : (f: { TCPSERVERCLIENT ClientConnected :: effl ==>
                       TCPSERVERCLIENT () :: effl } Eff () ) ->
               Env IO effl ->
               { [STDIO, TCPSERVER (ServerListening)] ==>
                 [STDIO, TCPSERVER ()] } Eff ()
forkServerLoop f env = do
  -- Accept, and perform the "receive" program with the new socket.
  OperationSuccess _ <- forkAccept f env
       | RecoverableError _ => forkServerLoop f env
       | FatalError err => do putStr ("Error accepting: " ++ (show err))
                              finaliseServer
       | ConnectionClosed => return ()
  forkServerLoop f env

setupServer : Port ->
            (f: { TCPSERVERCLIENT ClientConnected :: effl ==>
                  TCPSERVERCLIENT () :: effl } Eff () ) ->
            Env IO effl ->
              { [STDIO, TCPSERVER ()] } Eff ()
setupServer port f env = do
  putStr "Binding\n"
  OperationSuccess _ <- bind Nothing port
    | RecoverableError _ => return ()
    | FatalError err => do putStr ("Error binding: " ++ (show err) ++ "\n")
                           return ()
    | ConnectionClosed => return ()
  putStr "Bound\n"
  OperationSuccess _ <- listen
    | RecoverableError err => do putStr ("Recoverable error: " ++ (show err))
                                 closeBound
    | FatalError err => do putStr ("Error binding: " ++ show err)
                           finaliseServer
    | ConnectionClosed => return ()
  putStr "Listening\n"
  forkServerLoop f env

receiveFunc : List EFFECT -> Type
receiveFunc eff = { TCPSERVERCLIENT ClientConnected :: eff ==>
                    TCPSERVERCLIENT () :: eff } Eff ()

max_stars_repo_name: archaeron/idris-json-rpc

max_issues_repo_name: archaeron/idris-json-rpc

max_forks_repo_name: archaeron/idris-json-rpc


text:
module Git

import Data.List
import Data.Version
import System.Console.Extra
import System.Directory.Extra
import Data.String

||| Check if there is a repo in the current working directory.
repoExists : HasIO io => io Bool
repoExists = do
  [gitRemote] <- readLines (limit 1) True "git config --get remote.origin.url" -- "git status"
    | _ => pure False
  pure $ isSuffixOf "Idris2.git" $ trim gitRemote

clone : HasIO io => (repoURL : String) -> (path : String) -> io Bool
clone repoURL path = eatOutput False "git clone '\{repoURL}' '\{path}'"

||| Clone the given repository into the given path if the path does
||| not already contain a git repository.
|||
||| Returns True if the directory already contained a repo or if the
||| repo was successfully cloned into the requested path.
export
cloneIfNeeded : HasIO io => (repoURL : String) -> (path : String) -> io Bool
cloneIfNeeded repoURL path = do
  True <- createDirIfNeeded path
    | False => pure False
  Just False <- inDir path $ repoExists
    | _ => pure True
  putStrLn "Cloning Idris 2 repository..."
  clone repoURL path

||| Fetch the repo in the current working directory.
export
fetch : HasIO io => io Bool
fetch = [ res == 0 | res <- ignoreOutput "git fetch --tags" ]

||| Pull the repo in the current working directory.
export
pull : HasIO io => io Bool
pull = [ res == 0 | res <- ignoreOutput "git pull --tags" ]

export
listTags : HasIO io => io (List String)
listTags = do
  tags <- readLines (limit 1000) False "git tag --list"
  pure tags

export
listBranches : HasIO io => io (List String)
listBranches = do
  branches <- readLines (limit 1000) False "git branch --list --all"
  pure branches

||| List the versions for the repo in the current working directory.
|||
||| Versions are all git tags formatted as <major>.<minor>.<patch> and
||| optionally prefixed with 'v'.
export
listVersions : HasIO io => io (List Version)
listVersions = pure $ mapMaybe parseVersion !listTags

||| Fetch git tags and then list versions.
export
fetchAndListVersions : HasIO io => io (List Version)
fetchAndListVersions = do
  ignore fetch
  listVersions

export
checkout : HasIO io => (tag : String) -> io Bool
checkout tag = [ res == 0 | res <- ignoreOutput "git checkout \{tag}" ]

export
checkoutAndPullBranch : HasIO io => (branch : String) -> io Bool
checkoutAndPullBranch branch =
  pure $ !(checkout branch) && !pull

max_stars_repo_name: memoryruins/idv

max_issues_repo_name: memoryruins/idv

max_forks_repo_name: memoryruins/idv


text:
module SemVar.Tokens

import public Text.Token

public export
data SemVarTokenKind
  = Tilde
  | Caret
  | Dot
  | Number
  | Hyphen
  | CmpGT
  | CmpLT
  | CmpEQ
  | CmpGTE
  | CmpLTE
  | Pipe
  | Plus
  | Text
  | Asterisk
  | Whitespace

public export
Eq SemVarTokenKind where
  (==) Tilde Tilde = True
  (==) Caret Caret = True
  (==) Dot Dot = True
  (==) Number Number = True
  (==) Hyphen Hyphen = True
  (==) CmpGT CmpGT = True
  (==) CmpLT CmpLT = True
  (==) CmpEQ CmpEQ = True
  (==) CmpGTE CmpGTE = True
  (==) CmpLTE CmpLTE = True
  (==) Pipe Pipe = True
  (==) Plus Plus = True
  (==) Text Text = True
  (==) Asterisk Asterisk = True
  (==) Whitespace Whitespace = True
  (==) _ _ = False

public export
SemVarToken : Type
SemVarToken = Token SemVarTokenKind

public export
TokenKind SemVarTokenKind where
  TokType Tilde = ()
  TokType Caret = ()
  TokType Dot = ()
  TokType Number = Int
  TokType Hyphen = ()
  TokType CmpGT = ()
  TokType CmpLT = ()
  TokType CmpEQ = ()
  TokType CmpGTE = ()
  TokType CmpLTE = ()
  TokType Pipe = ()
  TokType Plus = ()
  TokType Text = String
  TokType Asterisk = ()
  TokType Whitespace = ()

  tokValue Tilde x = ()
  tokValue Caret x = ()
  tokValue Dot x = ()
  tokValue Number x = cast x
  tokValue Hyphen x = ()
  tokValue CmpGT x = ()
  tokValue CmpLT x = ()
  tokValue CmpEQ x = ()
  tokValue CmpGTE x = ()
  tokValue CmpLTE x = ()
  tokValue Pipe x = ()
  tokValue Plus x = ()
  tokValue Text x = x
  tokValue Asterisk x = ()
  tokValue Whitespace x = ()

export
Show SemVarToken where
  show (Tok Tilde x) = "Tilde"
  show (Tok Caret x) = "Caret"
  show (Tok Dot x) = "Dot"
  show (Tok Number x) = "Number " ++ (show x)
  show (Tok Hyphen x) = "Hyphen"
  show (Tok CmpGT x) = "CmpGT"
  show (Tok CmpLT x) = "CmpLT"
  show (Tok CmpEQ x) = "CmpEQ"
  show (Tok CmpGTE x) = "CmpGTE"
  show (Tok CmpLTE x) = "CmpLTE"
  show (Tok Pipe x) = "Pipe"
  show (Tok Plus x) = "Plus"
  show (Tok Text x) = "Text " ++ x
  show (Tok Asterisk x) = "Asterisk"
  show (Tok Whitespace x) = "Whitespace"

export
Eq SemVarToken where
  (Tok Tilde x0) == (Tok Tilde x1) = True
  (Tok Caret x0) == (Tok Caret x1) = True
  (Tok Dot x0) == (Tok Dot x1) = True
  (Tok Number x0) == (Tok Number x1) = x0 == x1
  (Tok Hyphen x0) == (Tok Hyphen x1) = True
  (Tok CmpGT x0) == (Tok CmpGT x1) = True
  (Tok CmpLT x0) == (Tok CmpLT x1) = True
  (Tok CmpEQ x0) == (Tok CmpEQ x1) = True
  (Tok CmpGTE x0) == (Tok CmpGTE x1) = True
  (Tok CmpLTE x0) == (Tok CmpLTE x1) = True
  (Tok Pipe x0) == (Tok Pipe x1) = True
  (Tok Plus x0) == (Tok Plus x1) = True
  (Tok Text x0) == (Tok Text x1) = x0 == x1
  (Tok Asterisk x0) == (Tok Asterisk x1) = True
  (Tok Whitespace x0) == (Tok Whitespace x1) = True
  _ == _ = False

max_stars_repo_name: Z-snails/inigo

max_issues_repo_name: Z-snails/inigo

max_forks_repo_name: Z-snails/inigo


text:
module CH10_1

import Data.Vect
import Data.List.Views
import Data.Vect.Views
import Data.Nat.Views

equalSuffix : Eq a => List a -> List a -> List a
equalSuffix = go []
  where
    go : Eq a => List a -> List a -> List a -> List a
    go acc xs ys with (snocList xs)
      go acc [] _ | Empty = []
      go acc (xs ++ [x]) ys | (Snoc xsrev) with (snocList ys)
        go acc (xs ++ [x]) [] | (Snoc xsrev) | Empty = acc
        go acc (xs ++ [x]) (ys ++ [y]) | (Snoc xsrev) | (Snoc ysrev) =
          if x == y
          then go (x :: acc) xs ys | xsrev | ysrev
          else acc

mergeSort : Ord a => Vect n a -> Vect n a
mergeSort xs with (splitRec xs)
  mergeSort [] | SplitRecNil = []
  mergeSort [x] | SlitRecOne = [x]
  mergeSort (left ++ right) | (SplitRecPair leftView rightView) =
    merge (mergeSort left | leftView) (mergeSort right | rightView)

toBinary : Nat -> String
toBinary = go ""
  where
    go : String -> Nat -> String
    go acc n with (halfRec n)
      go acc Z | HalfRecZ = acc
      go acc (S (n + n)) | (HalfRecOdd nrec) = go (strCons '1' acc) n | nrec
      go acc (n + n) | (HalfRecEven nrec) = go (strCons '0' acc) n | nrec

palindrome : Eq a => List a -> Bool
palindrome xs with (vList xs)
  palindrome [] | Vnil = True
  palindrome [x] | (VOne) = True
  palindrome (x :: xs ++ [y]) | (VCons xsrec) =
    if x == y
    then palindrome xs | xsrec
    else False


text:
module Language.JSON.String.Tokens

import Data.List
import Data.String.Extra
import Text.Token

%default total

public export
data JSONStringTokenKind
  = JSTQuote
  | JSTChar
  | JSTSimpleEscape
  | JSTUnicodeEscape

public export
JSONStringToken : Type
JSONStringToken = Token JSONStringTokenKind

public export
Eq JSONStringTokenKind where
  (==) JSTQuote JSTQuote = True
  (==) JSTChar JSTChar = True
  (==) JSTSimpleEscape JSTSimpleEscape = True
  (==) JSTUnicodeEscape JSTUnicodeEscape = True
  (==) _ _ = False

private
charValue : String -> Char
charValue x = case index 0 x of
                   Nothing => '\NUL'
                   Just c  => c

private
simpleEscapeValue : String -> Char
simpleEscapeValue x
  = case index 1 x of
         Nothing => '\NUL'
         Just c => case c of
                        '"'  => '"'
                        '\\' => '\\'
                        '/'  => '/'
                        'b'  => '\b'
                        'f'  => '\f'
                        'n'  => '\n'
                        'r'  => '\r'
                        't'  => '\t'
                        _    => '\NUL'

private
unicodeEscapeValue : String -> Char
unicodeEscapeValue x = fromHex (drop 2 $ fastUnpack x) 0
  where hexVal : Char -> Int
        hexVal c = if c >= 'A'
                      then ord c - ord 'A' + 10
                      else ord c - ord '0'

        fromHex : List Char -> Int -> Char
        fromHex       [] acc = chr acc
        fromHex (h :: t) acc = fromHex t (hexVal h + 16 * acc)

public export
TokenKind JSONStringTokenKind where
  TokType JSTQuote = ()
  TokType JSTChar = Char
  TokType JSTSimpleEscape = Char
  TokType JSTUnicodeEscape = Char

  tokValue JSTQuote = const ()
  tokValue JSTChar = charValue
  tokValue JSTSimpleEscape = simpleEscapeValue
  tokValue JSTUnicodeEscape = unicodeEscapeValue


text:
module Applications.Example

import Common.Util
import Common.Interfaces
import Specifications.OrderedGroup
import Proofs.OrderTheory
import Proofs.GroupTheory
import Proofs.GroupCancelationLemmas
import Proofs.TranslationInvarianceTheory

%default total
%access public export

absoluteValue : (Ringops s, Decidable [s,s] leq) =>
  .OrderedGroupSpec (+) Zero Ng leq -> s -> (a ** leq Zero a)
absoluteValue spec x =
  case decision {rel = leq} x Zero of
    Yes prf => (Ng x ** invertNegative (partiallyOrderedGroup spec) x prf)
    No contra =>
        let (positive, _) = orderContra (totalOrder spec) x Zero contra
        in (x ** positive)

max_stars_repo_name: jeroennoels/verified-algebra

max_issues_repo_name: jeroennoels/verified-algebra

max_forks_repo_name: jeroennoels/verified-algebra


text:
import Data.List
import Data.Strings
import Erlang.System.File

-- Copied from `System.File`. Testing the indiviudual functions
-- like `fGetLine`. This function is not total.
-- `readLine` is tested in `erlang/erlang003`.
idrisReadFile : HasIO io => String -> io (Either FileError String)
idrisReadFile file = do
  Right h <- openFile file Read
    | Left err => pure (Left err)
  Right content <- read [] h
    | Left err => do
      closeFile h
      pure (Left err)
  closeFile h
  pure (Right (fastAppend content))
  where
    read : List String -> File -> io (Either FileError (List String))
    read acc h = do
      eof <- fEOF h
      if eof
        then pure (Right (reverse acc))
        else do
          Right str <- fGetLine h
            | Left err => pure (Left err)
          read (str :: acc) h

main : IO ()
main
    = do Right ok <- idrisReadFile "test.txt"
               | Left err => printLn err
         putStr ok
         writeFile "testout.txt" "abc\ndef\n"
         Right ok <- idrisReadFile "testout.txt"
               | Left err => printLn err
         putStr ok
         Right ok <- idrisReadFile "notfound"
               | Left err => printLn err
         putStr ok


text:
module IdrisJvm.System

import public Data.So
import IdrisJvm.IO
import Java.Util
import Java.Math
import Java.Lang

%access public export

getArgs : JVM_IO (List String)
getArgs = do
    argsList <- invokeStatic RuntimeClass "getProgramArgs" (JVM_IO JList)
    Iterator.toList !(JList.iterator argsList)

time : JVM_IO Integer
time = believe_me <$> invokeStatic RuntimeClass "time" (JVM_IO BigInteger)

getEnv : String -> JVM_IO (Maybe String)
getEnv = System.getenv

system : String -> JVM_IO Int
system = invokeStatic RuntimeClass "runCommand" (String -> JVM_IO Int)

usleep : (i : Int) -> { auto prf : So (i >= 0 && i <= 1000000) } -> JVM_IO ()
usleep interval = invokeStatic RuntimeClass "usleep" (Int -> JVM_IO ()) interval

exit : Int -> JVM_IO a
exit = believe_me . Java.Lang.System.exit

||| Programs can either terminate successfully, or end in a caught
||| failure.
data ExitCode : Type where
  ||| Terminate successfully.
  ExitSuccess : ExitCode
  ||| Program terminated for some prescribed reason.
  |||
  ||| @errNo A non-zero numerical value indicating failure.
  ||| @prf   Proof that the int value is non-zero.
  ExitFailure : (errNo    : Int)
             -> {auto prf : So (not $ errNo == 0)}
             -> ExitCode

||| Terminate the program with an `ExitCode`. This code indicates the
||| success of the program's execution, and returns the success code
||| to the program's caller.
|||
||| @code The `ExitCode` for program.
exitWith : (code : ExitCode) -> JVM_IO a
exitWith ExitSuccess         = exit 0
exitWith (ExitFailure errNo) = exit errNo

||| Exit the program indicating failure.
exitFailure : JVM_IO a
exitFailure = exitWith (ExitFailure 1)

||| Exit the program after a successful run.
exitSuccess : JVM_IO a
exitSuccess = exitWith ExitSuccess

||| Wall clock time
record Clock where
  constructor MkClock
  seconds : Integer
  nanoseconds : Integer

||| Get the system's wall clock time.
clockTime : JVM_IO Clock
clockTime =
  believe_me <$> invokeStatic (Class "io/github/mmhelloworld/idrisjvm/runtime/IdrisSystem")
    "getIdrisClock" (JVM_IO IdrisObject)


text:
module Main

import Effects
import Effect.Memory
import Control.IOExcept
import Data.Vect

MemoryIO : Type -> Type -> Type -> Type
MemoryIO td ts r = Eff r [Dst ::: RAW_MEMORY td,
                          Src ::: RAW_MEMORY ts]

inpVect : Vect 5 Bits8
inpVect = map prim__truncInt_B8 [0, 1, 2, 3, 5]

sub1 : Vect n Bits8 -> Vect n Bits8
sub1 xs = map (prim__truncInt_B8 . (\ x => x - 1) . prim__zextB8_Int) xs

testMemory : MemoryIO () () (Vect 4 Int)
testMemory = do Src :- allocate 5
                Src :- poke 0 inpVect Oh
                Dst :- allocate 5
                Dst :- initialize (prim__truncInt_B8 1) 2 Oh
                move 2 2 3 Oh Oh
                Src :- free
                end <- Dst :- peek 4 (S Z) Oh
                Dst :- poke 4 (sub1 end) Oh
                res <- Dst :- peek 1 (S(S(S(S Z)))) Oh
                Dst :- free
                pure (map (prim__zextB8_Int) res)

main : IO ()
main = ioe_run (runInit [Dst := (), Src := ()] testMemory)
               (\err => printLn err) (\ok => printLn ok)

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:
public export
interface Do (m : Type) where
  Next : m -> Type
  bind : (x : m) -> Next x

public export
Monad m => Do (m a) where
  Next x = {b : Type} -> (a -> m b) -> m b
  bind x k = x >>= k

foo : Maybe Int -> Maybe Int -> Maybe Int
foo x y
   = bind x (\x' =>
     bind y (\y' => Just (x' + y')))


text:
module CommonDef

import Compiler.VMCode
import Core.Name.Namespace
import Core.Context
import Compiler.Common
import Protocol.Hex
import System
import System.File
import Libraries.Utils.Path

-- https://github.com/idris-community/Idris2-Ocaml/blob/master/src/Ocaml/Expr.idr#L51
-- https://github.com/idris-lang/Idris2/blob/aa27ccbdb655c1c55560857ce8a92156260df62d/src/Compiler/ES/ES.idr#L99
cairoIdent : String -> String
cairoIdent s = concatMap okchar (unpack s)
  where
    okchar : Char -> String
    okchar '_' = "_"
    okchar '=' = "eq_"
    okchar '<' = "lt_"
    okchar '>' = "gt_"
    okchar '\'' = "prime_"
    okchar '(' = "lpar_"
    okchar ')' = "rpar_"
    okchar '{' = "lcurl_"
    okchar '}' = "rcurl_"
    okchar '$' = "dollar_"
    okchar ' ' = "space_" -- TODO: how can the space be part of the name? Data_Vect_map_Functor_lpar_Vectspace_dollar_nrpar_
    okchar c = if isAlphaNum c then cast c else "_" ++ asHex (cast c)

cairoUserName : UserName -> String
cairoUserName (Basic n) = cairoIdent n
cairoUserName (Field n) = "rf__" ++ cairoIdent n
cairoUserName Underscore = cairoIdent "_"

public export
cairoName : Name -> String
cairoName (NS ns x) = case cairoIdent (showNSWithSep "_" ns) of
   "" => cairoName x
   ns => ns ++ "_" ++ cairoName x
cairoName (UN x) = cairoUserName x
cairoName (MN x y) = "mn__" ++ cairoIdent x ++ "_" ++ show y
cairoName (PV x y) = "pat__" ++ cairoName x ++ "_" ++ show y
cairoName (DN x y) = cairoName y
cairoName (Nested (i, x) n) = "nested__" ++ show i ++ "_" ++ show x ++ "_" ++ cairoName n
cairoName (CaseBlock x y) = "case__" ++ cairoIdent x ++ "_" ++ show y
cairoName (WithBlock x y) = "with__" ++ cairoIdent x ++ "_" ++ show y
cairoName (Resolved x) = "fn__" ++ show x

export
makeName : String -> String -> Name
makeName ns name = NS (mkNamespace ns) (UN $ Basic name)

-- MAIN Entry
export
cairo_main : Name
cairo_main = makeName "Main" "main"

export
entry_name : Name
entry_name = NS (mkNamespace "") (UN $ Basic "main")

public export
fromZeroTo : Int -> List Int
fromZeroTo 0 = [0]
fromZeroTo n = if n < 0 then [] else fromZeroTo (n-1) ++ [n]

public export
CompilationPass : Type -> Type
CompilationPass a = List (Name, a) -> List (Name, a)

max_stars_repo_name: skyro-compiler/skyro

max_issues_repo_name: skyro-compiler/skyro

max_forks_repo_name: skyro-compiler/skyro


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

treeLabelWith : Stream labelType -> Tree a ->
                (Stream labelType, Tree (labelType, a))
treeLabelWith labels Empty = (labels, Empty)
treeLabelWith labels (Node left val right) =
    let
        (labelThis :: labelsLeft, leftLabelled) = treeLabelWith labels left
        (labelsRight, rightLabelled) = treeLabelWith labelsLeft right
    in
        (labelsRight, Node leftLabelled (labelThis, val) rightLabelled)

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


text:
module Day1
import Data.String

foldCount : (Int, Int) -> Int -> (Int, Int)
foldCount (a, b) c = (c, (if a < c then b + 1 else b))

foldCount2 : (Int, Int, Int, Int) -> Int -> (Int, Int, Int, Int)
foldCount2 (a, b, c, d) e = (b, c, e, (if (a+b+c) < (b+c+e) then d + 1 else d))

export
solve : List String -> (Int, Int, Int, Int)
solve content = foldl foldCount2 (1000000, 1000000, 100000, 0) (mapMaybe parseInteger content)


text:
module Java.Math

import IdrisJvm.FFI
import Java.Lang

%access public export

namespace BigInteger
  BigIntegerClass : JVM_NativeTy
  BigIntegerClass = Class "java/math/BigInteger"

  BigInteger : Type
  BigInteger = JVM_Native BigIntegerClass

  -- Constructor example
  new : String -> JVM_IO BigInteger
  new s = FFI.new (String -> JVM_IO BigInteger) s

  one : BigInteger
  one = unsafePerformIO $ getStaticField BigIntegerClass "ONE" (JVM_IO BigInteger)

  toString : BigInteger -> String
  toString bigInt = unsafePerformIO $ invokeInstance "toString" (BigInteger -> JVM_IO String) bigInt

  add : BigInteger -> BigInteger -> BigInteger
  add b1 b2 = unsafePerformIO $ invokeInstance "add" (BigInteger -> BigInteger -> JVM_IO BigInteger) b1 b2

  valueOf : Bits64 -> BigInteger
  valueOf val = unsafePerformIO $ invokeStatic BigIntegerClass "valueOf" (Bits64 -> JVM_IO BigInteger) val

Show BigInteger where
  show = BigInteger.toString


text:
module ZZplus

import congruence
import Quotient_Type
import ZZ_alt
import Product_Type_Eq

%access public export
%default total

plus : ZZ1 -> ZZ1 -> ZZ1
plus (a, b) (c, d) = (plus a c, plus b d)

plusCommutative : (n, m : ZZ1) -> (plus n m = plus m n)
plusCommutative (a, b) (c, d) = let

    pf1 : (plus a c = plus c a)
        = plusCommutative a c

    pf2 : (plus b d = plus d b)
        = plusCommutative b d

    in
    (Product_Eq_property_1 Nat Nat (plus (a, b) (c, d)) (plus (c, d) (a, b)) pf1 pf2)

plusPassesThrough : (a, b, c, d : ZZ1) -> (ZZ_Rel a c) -> (ZZ_Rel b d) ->
                    (ZZ_Rel (plus a b) (plus c d))

plusPassesThrough (a1, a2) (b1, b2) (c1, c2) (d1, d2) pf_ac pf_bd = let

    pf1 : (plus (plus a1 b1) (plus c2 d2) = plus a1 (plus b1 (plus c2 d2)))
        = (sym (plusAssociative a1 b1 (plus c2 d2)))

    pf2 : (plus b1 (plus c2 d2) = plus (plus b1 c2) d2)
        = (plusAssociative b1 c2 d2)

    pf3 : ((plus a1 (plus b1 (plus c2 d2))) = (plus a1 (plus (plus b1 c2) d2)))
        = congruence Nat Nat (plus b1 (plus c2 d2)) (plus (plus b1 c2) d2) (\x => (plus a1 x)) pf2

    pf4 : (plus a1 (plus (plus b1 c2) d2) = plus (plus a1 (plus b1 c2)) d2)
        = plusAssociative a1 (plus b1 c2) d2

    pf5 : (plus b1 c2 = plus c2 b1)
        = (plusCommutative b1 c2)

    pf6 : (plus (plus a1 (plus b1 c2)) d2 = plus (plus a1 (plus c2 b1)) d2)
        = congruence Nat Nat (plus b1 c2) (plus c2 b1) (\x => (plus (plus a1 x) d2)) pf5

    pf7 : (plus a1 (plus c2 b1) = plus (plus a1 c2) b1)
        = plusAssociative a1 c2 b1

    pf8 : (plus (plus a1 (plus c2 b1)) d2 = plus (plus (plus a1 c2) b1) d2)
        = congruence Nat Nat (plus a1 (plus c2 b1)) (plus (plus a1 c2) b1) (\x => (plus x d2)) pf7

    pf9 : (plus (plus (plus a1 c2) b1) d2 = plus (plus a1 c2) (plus b1 d2))
        = sym (plusAssociative (plus a1 c2) b1 d2)

    pf10 : (plus (plus a1 b1) (plus c2 d2) = plus (plus a1 c2) (plus b1 d2)) -- one part
         = trans (trans (trans (trans (trans pf1 pf3) pf4) pf6) pf8) pf9

    pf11 : (plus (plus a1 c2) (plus b1 d2) = plus (plus a2 c1) (plus b1 d2))
         = congruence Nat Nat (plus a1 c2) (plus a2 c1) (\x => (plus x (plus b1 d2))) pf_ac

    pf12 : (plus (plus a2 c1) (plus b1 d2) = plus (plus a2 c1) (plus b2 d1))
         = congruence Nat Nat (plus b1 d2) (plus b2 d1) (\x => (plus (plus a2 c1) x)) pf_bd

    pf13 : (plus (plus a2 c1) (plus b2 d1) = plus a2 (plus c1 (plus b2 d1)))
         = sym (plusAssociative a2 c1 (plus b2 d1))

    pf14 : (plus c1 (plus b2 d1) = plus (plus b2 d1) c1)
         = plusCommutative c1 (plus b2 d1)

    pf15 : (plus (plus b2 d1) c1 = plus b2 (plus d1 c1))
         = sym (plusAssociative b2 d1 c1)

    pf16 : (plus c1 (plus b2 d1) = plus b2 (plus d1 c1))
         = trans pf14 pf15

    pf17 : (plus a2 (plus c1 (plus b2 d1)) = plus a2 (plus b2 (plus d1 c1)))
         = congruence Nat Nat (plus c1 (plus b2 d1)) (plus b2 (plus d1 c1)) (\x => (plus a2 x)) pf16

    pf18 : (plus a2 (plus b2 (plus d1 c1)) = plus (plus a2 b2) (plus d1 c1))
         = plusAssociative a2 b2 (plus d1 c1)

    pf19 : (plus (plus a2 b2) (plus d1 c1) = plus (plus a2 b2) (plus c1 d1))
         = congruence Nat Nat (plus d1 c1) (plus c1 d1) (\x => (plus (plus a2 b2) x)) (plusCommutative d1 c1)

    pf20 = trans (trans (trans (trans (trans (trans pf10 pf11) pf12) pf13) pf17) pf18) pf19

    in
    pf20

isZero : (a : ZZ1) -> Type
isZero a = (n : ZZ1) -> (ZZ_Rel (plus n a)  n)

||| A proof that if a is zero then it is of the form (n,n)
ZZ_property1 : (a : ZZ1) -> (isZero a) -> (n : Nat ** (ZZ_Rel a (n,n)))
ZZ_property1 (a,b) pfZ = (Z ** (pfZ (Z,Z)))

||| A proof that if any element of the form (n,n) is a zero element
ZZ_property2 : (n : Nat) -> (isZero (n,n))
ZZ_property2 n (a, b) = let

    pf1 : (plus a n = plus n a)
        = plusCommutative a n

    pf2 : (plus (plus a n) b = plus (plus n a) b)
        = congruence Nat Nat (plus a n) (plus n a) (\c => (plus c b)) pf1

    pf3 : (plus n (plus a b) = plus (plus n a) b)
        = plusAssociative n a b

    pf4 : (plus (plus a n) b = plus n (plus a b))
        = trans pf2 (sym pf3)

    pf5 : (plus a b = plus b a)
        = plusCommutative a b

    pf6 : (plus n (plus a b) = plus n (plus b a))
        = congruence Nat Nat (plus a b) (plus b a) (\c => (plus n c)) pf5

    pf7 : (plus n (plus b a) = plus (plus n b) a)
        = plusAssociative n b a

    pf8 : (plus n b = plus b n)
        = plusCommutative n b

    pf9 : (plus (plus n b) a = plus (plus b n) a)
        = congruence Nat Nat (plus n b) (plus b n) (\c => (plus c a)) pf8

    pf10 : (plus n (plus b a) = plus (plus b n) a)
         = trans pf7 pf9

    pf11 : (plus n (plus a b) = plus (plus b n) a)
         = trans pf6 pf10

    pf12 : (plus (plus a n) b = plus (plus b n) a)
         = trans pf4 pf11

    in
    pf12


text:
module SimpleLambdaLang

import Data.Fin
import Data.Vect

data Ty = TyBool | TyFun Ty Ty

typeOf : Ty -> Type
typeOf TyBool = Bool
typeOf (TyFun x y) = typeOf x -> typeOf y

using (n : Nat, ctx : Vect n Ty)
  data Expr : Vect n Ty -> Ty -> Type where
    T     : Expr ctx TyBool
    F     : Expr ctx TyBool
    IF    : Expr ctx TyBool -> Expr ctx t -> Expr ctx t -> Expr ctx t
    Var'  : (i : Fin n) -> Expr ctx (index i ctx)
    Lam'  : Expr (a :: ctx) b -> Expr ctx (TyFun a b)
    App'  : Expr ctx (TyFun a b) -> Expr ctx a -> Expr ctx b

data Env : Vect n Ty -> Type where
  Nil  : Env []
  (::) : typeOf t -> Env ctx -> Env (t::ctx)

lookup : (i : Fin n) -> (env : Env ctx) -> typeOf (index i ctx)
lookup FZ     (x :: xs) = x
lookup (FS x) (y :: xs) = lookup x xs

eval : Env ctx -> Expr ctx t -> typeOf t
eval env (Var' i) = lookup i env
eval env (Lam' body) = \x => eval (x :: env) body
eval env (App' f x) = eval env f $ eval env x
eval env T = True
eval env F = False
eval env (IF expr expr' expr'') = if eval env expr then eval env expr' else eval env expr''

not'' : Expr ctx (TyFun TyBool TyBool)
not'' = Lam' $ IF (Var' 0) F T

max_stars_repo_name: tgrospic/dependently-typed-slides

max_issues_repo_name: tgrospic/dependently-typed-slides

max_forks_repo_name: tgrospic/dependently-typed-slides