text:
--------------------------------------------------------------------------------
-- This file is here so GitHub thinks this is an Idris repo :D
--------------------------------------------------------------------------------

module Prelude.Nat

import Builtins

import Prelude.Algebra
import Prelude.Basics
import Prelude.Bool
import Prelude.Cast
import Prelude.Interfaces
import Prelude.Uninhabited

%access public export
%default total

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

-- name hints for interactive editing
%name Nat k,j,i,n,m

Uninhabited (Z = S n) where
  uninhabited Refl impossible

--------------------------------------------------------------------------------
-- Syntactic tests
--------------------------------------------------------------------------------

total isZero : Nat -> Bool
isZero Z     = True
isZero (S n) = False

total isSucc : Nat -> Bool
isSucc Z     = False
isSucc (S n) = True

--------------------------------------------------------------------------------
-- Basic arithmetic functions
--------------------------------------------------------------------------------

||| Add two natural numbers.
||| @ n the number to case-split on
||| @ m the other number
total plus : (n, m : Nat) -> Nat
plus Z right        = right
plus (S left) right = S (plus left right)

||| Multiply natural numbers
total mult : Nat -> Nat -> Nat
mult Z right        = Z
mult (S left) right = plus right $ mult left right

||| Convert an Integer to a Nat, mapping negative numbers to 0
fromIntegerNat : Integer -> Nat
fromIntegerNat 0 = Z
fromIntegerNat n =
  if (n > 0) then
    S (fromIntegerNat (assert_smaller n (n - 1)))
  else
    Z

||| Convert a Nat to an Integer
toIntegerNat : Nat -> Integer
toIntegerNat Z = 0
toIntegerNat (S k) = 1 + toIntegerNat k

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

||| Exponentiation of natural numbers
total power : Nat -> Nat -> Nat
power base Z       = S Z
power base (S exp) = mult base $ power base exp

hyper : Nat -> Nat -> Nat -> Nat
hyper Z        a b      = S b
hyper (S Z)    a Z      = a
hyper (S(S Z)) a Z      = Z
hyper n        a Z      = S Z
hyper (S pn)   a (S pb) = hyper pn a (hyper (S pn) a pb)

--------------------------------------------------------------------------------
-- Comparisons
--------------------------------------------------------------------------------

||| Proofs that `n` or `m` is not equal to Z
data NotBothZero : (n, m : Nat) -> Type where
  LeftIsNotZero  : NotBothZero (S n) m
  RightIsNotZero : NotBothZero n     (S m)

||| Proofs that `n` is less than or equal to `m`
||| @ n the smaller number
||| @ m the larger number
data LTE  : (n, m : Nat) -> Type where
  ||| Zero is the smallest Nat
  LTEZero : LTE Z    right
  ||| If n <= m, then n + 1 <= m + 1
  LTESucc : LTE left right -> LTE (S left) (S right)

Uninhabited (LTE (S n) Z) where
  uninhabited LTEZero impossible

||| Greater than or equal to
total GTE : Nat -> Nat -> Type
GTE left right = LTE right left

||| Strict less than
total LT : Nat -> Nat -> Type
LT left right = LTE (S left) right

||| Strict greater than
total GT : Nat -> Nat -> Type
GT left right = LT right left

||| A successor is never less than or equal zero
succNotLTEzero : Not (S m `LTE` Z)
succNotLTEzero LTEZero impossible

||| If two numbers are ordered, their predecessors are too
fromLteSucc : (S m `LTE` S n) -> (m `LTE` n)
fromLteSucc (LTESucc x) = x

||| A decision procedure for `LTE`
isLTE : (m, n : Nat) -> Dec (m `LTE` n)
isLTE Z n = Yes LTEZero
isLTE (S k) Z = No succNotLTEzero
isLTE (S k) (S j) with (isLTE k j)
  isLTE (S k) (S j) | (Yes prf) = Yes (LTESucc prf)
  isLTE (S k) (S j) | (No contra) = No (contra . fromLteSucc)

||| `LTE` is reflexive.
lteRefl : LTE n n
lteRefl {n = Z}   = LTEZero
lteRefl {n = S k} = LTESucc lteRefl

||| n < m implies n < m + 1
lteSuccRight : LTE n m -> LTE n (S m)
lteSuccRight LTEZero     = LTEZero
lteSuccRight (LTESucc x) = LTESucc (lteSuccRight x)

||| n + 1 < m implies n < m
lteSuccLeft : LTE (S n) m -> LTE n m
lteSuccLeft (LTESucc x) = lteSuccRight x

||| `LTE` is transitive
lteTransitive : LTE n m -> LTE m p -> LTE n p
lteTransitive LTEZero y = LTEZero
lteTransitive (LTESucc x) (LTESucc y) = LTESucc (lteTransitive x y)

lteAddRight : (n : Nat) -> LTE n (plus n m)
lteAddRight Z = LTEZero
lteAddRight (S k) = LTESucc (lteAddRight k)

||| Boolean test than one Nat is less than or equal to another
total lte : Nat -> Nat -> Bool
lte Z        right     = True
lte left     Z         = False
lte (S left) (S right) = lte left right

||| Boolean test than one Nat is greater than or equal to another
total gte : Nat -> Nat -> Bool
gte left right = lte right left

||| Boolean test than one Nat is strictly less than another
total lt : Nat -> Nat -> Bool
lt left right = lte (S left) right

||| Boolean test than one Nat is strictly greater than another
total gt : Nat -> Nat -> Bool
gt left right = lt right left

||| Find the least of two natural numbers
total minimum : Nat -> Nat -> Nat
minimum Z m = Z
minimum (S n) Z = Z
minimum (S n) (S m) = S (minimum n m)

||| Find the greatest of two natural numbers
total maximum : Nat -> Nat -> Nat
maximum Z m = m
maximum (S n) Z = S n
maximum (S n) (S m) = S (maximum n m)

||| Cast Nat to Int
||| Note that this can overflow
toIntNat : Nat -> Int
toIntNat n = prim__truncBigInt_Int (toIntegerNat n)

(-) : (m : Nat) -> (n : Nat) -> {auto smaller : LTE n m} -> Nat
(-) m n {smaller} = minus m n

--------------------------------------------------------------------------------
-- Interface implementations
--------------------------------------------------------------------------------

Eq Nat where
  Z == Z         = True
  (S l) == (S r) = l == r
  _ == _         = False

Cast Nat Integer where
  cast = toIntegerNat

Ord Nat where
  compare Z Z         = EQ
  compare Z (S k)     = LT
  compare (S k) Z     = GT
  compare (S x) (S y) = compare x y

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

  fromInteger = fromIntegerNat

MinBound Nat where
  minBound = Z

||| Casts negative `Integers` to 0.
Cast Integer Nat where
  cast = fromInteger

Cast String Nat where
    cast str = cast (the Integer (cast str))

||| A wrapper for Nat that specifies the semigroup and monoid implementations that use (*)
record Multiplicative where
  constructor GetMultiplicative
  _ : Nat

||| A wrapper for Nat that specifies the semigroup and monoid implementations that use (+)
record Additive where
  constructor GetAdditive
  _ : Nat

Semigroup Multiplicative where
  (<+>) left right = GetMultiplicative $ left' * right'
    where
      left'  : Nat
      left'  =
       case left of
          GetMultiplicative m => m

      right' : Nat
      right' =
        case right of
          GetMultiplicative m => m

Semigroup Additive where
  left <+> right = GetAdditive $ left' + right'
    where
      left'  : Nat
      left'  =
        case left of
          GetAdditive m => m

      right' : Nat
      right' =
        case right of
          GetAdditive m => m

Monoid Multiplicative where
  neutral = GetMultiplicative $ S Z

Monoid Additive where
  neutral = GetAdditive Z

||| Casts negative `Ints` to 0.
Cast Int Nat where
  cast i = fromInteger (cast i)

Cast Nat Int where
  cast = toIntNat

Cast Nat Double where
  cast = cast . toIntegerNat

--------------------------------------------------------------------------------
-- Auxilliary notions
--------------------------------------------------------------------------------

||| The predecessor of a natural number. `pred Z` is `Z`.
total pred : Nat -> Nat
pred Z     = Z
pred (S n) = n

--------------------------------------------------------------------------------
-- Fibonacci and factorial
--------------------------------------------------------------------------------

||| Fibonacci numbers
total fib : Nat -> Nat
fib Z         = Z
fib (S Z)     = S Z
fib (S (S n)) = fib (S n) + fib n

||| Factorial function
total fact : Nat -> Nat
fact Z     = S Z
fact (S n) = (S n) * fact n

--------------------------------------------------------------------------------
-- Division and modulus
--------------------------------------------------------------------------------

||| The proof that no successor of a natural number can be zero.
|||
||| ```idris example
||| modNatNZ 10 3 SIsNotZ
||| ```
SIsNotZ : {x: Nat} -> (S x = Z) -> Void
SIsNotZ Refl impossible

||| Modulus function where the divisor is not zero.
|||
||| ```idris example
||| modNatNZ 100 2 SIsNotZ
||| ```
modNatNZ : Nat -> (y: Nat) -> Not (y = Z) -> Nat
modNatNZ left Z         p = void (p Refl)
modNatNZ left (S right) _ = mod' left left right
  where
    total mod' : Nat -> Nat -> Nat -> Nat
    mod' Z        centre right = centre
    mod' (S left) centre right =
      if lte centre right then
        centre
      else
        mod' left (minus centre (S right)) right

partial
modNat : Nat -> Nat -> Nat
modNat left (S right) = modNatNZ left (S right) SIsNotZ

||| Division where the divisor is not zero.
|||
||| ```idris example
||| divNatNZ 100 2 SIsNotZ
||| ```
divNatNZ : Nat -> (y: Nat) -> Not (y = Z) -> Nat
divNatNZ left Z         p = void (p Refl)
divNatNZ left (S right) _ = div' left left right
  where
    total div' : Nat -> Nat -> Nat -> Nat
    div' Z        centre right = Z
    div' (S left) centre right =
      if lte centre right then
        Z
      else
        S (div' left (minus centre (S right)) right)

partial
divNat : Nat -> Nat -> Nat
divNat left (S right) = divNatNZ left (S right) SIsNotZ

divCeilNZ : Nat -> (y: Nat) -> Not (y = 0) -> Nat
divCeilNZ x y p = case (modNatNZ x y p) of
  Z   => divNatNZ x y p
  S _ => S (divNatNZ x y p)

partial
divCeil : Nat -> Nat -> Nat
divCeil x (S y) = divCeilNZ x (S y) SIsNotZ

partial
Integral Nat where
  div = divNat
  mod = modNat

log2NZ : (x: Nat) -> Not (x = Z) -> Nat
log2NZ Z         p = void (p Refl)
log2NZ (S Z)     _ = Z
log2NZ (S (S n)) _ = S (log2NZ (assert_smaller (S (S n)) (S (divNatNZ n 2 SIsNotZ))) SIsNotZ)

partial
log2 : Nat -> Nat
log2 (S n) = log2NZ (S n) SIsNotZ

--------------------------------------------------------------------------------
-- GCD and LCM
--------------------------------------------------------------------------------
gcd : (a: Nat) -> (b: Nat) -> .{auto ok: NotBothZero a b} -> Nat
gcd a Z     = a
gcd Z b     = b
gcd a (S b) = assert_total $ gcd (S b) (modNatNZ a (S b) SIsNotZ)

lcm : Nat -> Nat -> Nat
lcm _ Z     = Z
lcm Z _     = Z
lcm a (S b) = assert_total $ divNat (a * (S b)) (gcd a (S b))

--------------------------------------------------------------------------------
-- An informative comparison view
--------------------------------------------------------------------------------
data CmpNat : Nat -> Nat -> Type where
     CmpLT : (y : _) -> CmpNat x (x + S y)
     CmpEQ : CmpNat x x
     CmpGT : (x : _) -> CmpNat (y + S x) y

total cmp : (x, y : Nat) -> CmpNat x y
cmp Z Z     = CmpEQ
cmp Z (S k) = CmpLT _
cmp (S k) Z = CmpGT _
cmp (S x) (S y) with (cmp x y)
  cmp (S x) (S (x + (S k))) | CmpLT k = CmpLT k
  cmp (S x) (S x)           | CmpEQ   = CmpEQ
  cmp (S (y + (S k))) (S y) | CmpGT k = CmpGT k

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

-- Succ

||| S preserves equality
total eqSucc : (left : Nat) -> (right : Nat) -> (p : left = right) ->
  S left = S right
eqSucc left _ Refl = Refl

||| S is injective
total succInjective : (left : Nat) -> (right : Nat) -> (p : S left = S right) ->
  left = right
succInjective left _ Refl = Refl

-- Plus
total plusZeroLeftNeutral : (right : Nat) -> 0 + right = right
plusZeroLeftNeutral right = Refl

total plusZeroRightNeutral : (left : Nat) -> left + 0 = left
plusZeroRightNeutral Z     = Refl
plusZeroRightNeutral (S n) =
  let inductiveHypothesis = plusZeroRightNeutral n in
    rewrite inductiveHypothesis in Refl

total plusSuccRightSucc : (left : Nat) -> (right : Nat) ->
  S (left + right) = left + (S right)
plusSuccRightSucc Z right        = Refl
plusSuccRightSucc (S left) right =
  let inductiveHypothesis = plusSuccRightSucc left right in
    rewrite inductiveHypothesis in Refl

total plusCommutative : (left : Nat) -> (right : Nat) ->
  left + right = right + left
plusCommutative Z        right = rewrite plusZeroRightNeutral right in Refl
plusCommutative (S left) right =
  let inductiveHypothesis = plusCommutative left right in
    rewrite inductiveHypothesis in
      rewrite plusSuccRightSucc right left in Refl

total plusAssociative : (left : Nat) -> (centre : Nat) -> (right : Nat) ->
  left + (centre + right) = (left + centre) + right
plusAssociative Z        centre right = Refl
plusAssociative (S left) centre right =
  let inductiveHypothesis = plusAssociative left centre right in
    rewrite inductiveHypothesis in Refl

total plusConstantRight : (left : Nat) -> (right : Nat) -> (c : Nat) ->
  (p : left = right) -> left + c = right + c
plusConstantRight left _ c Refl = Refl

total plusConstantLeft : (left : Nat) -> (right : Nat) -> (c : Nat) ->
  (p : left = right) -> c + left = c + right
plusConstantLeft left _ c Refl = Refl

total plusOneSucc : (right : Nat) -> 1 + right = S right
plusOneSucc n = Refl

total plusLeftCancel : (left : Nat) -> (right : Nat) -> (right' : Nat) ->
  (p : left + right = left + right') -> right = right'
plusLeftCancel Z        right right' p = p
plusLeftCancel (S left) right right' p =
  let inductiveHypothesis = plusLeftCancel left right right' in
    inductiveHypothesis (succInjective _ _ p)

total plusRightCancel : (left : Nat) -> (left' : Nat) -> (right : Nat) ->
  (p : left + right = left' + right) -> left = left'
plusRightCancel left left' Z         p = rewrite sym (plusZeroRightNeutral left) in
                                         rewrite sym (plusZeroRightNeutral left') in
                                                 p
plusRightCancel left left' (S right) p =
  plusRightCancel left left' right
    (succInjective _ _ (rewrite plusSuccRightSucc left right in
                        rewrite plusSuccRightSucc left' right in p))

total plusLeftLeftRightZero : (left : Nat) -> (right : Nat) ->
  (p : left + right = left) -> right = Z
plusLeftLeftRightZero Z        right p = p
plusLeftLeftRightZero (S left) right p =
  plusLeftLeftRightZero left right (succInjective _ _ p)

-- Mult
total multZeroLeftZero : (right : Nat) -> Z * right = Z
multZeroLeftZero right = Refl

total multZeroRightZero : (left : Nat) -> left * Z = Z
multZeroRightZero Z        = Refl
multZeroRightZero (S left) = multZeroRightZero left

total multRightSuccPlus : (left : Nat) -> (right : Nat) ->
  left * (S right) = left + (left * right)
multRightSuccPlus Z        right = Refl
multRightSuccPlus (S left) right =
  let inductiveHypothesis = multRightSuccPlus left right in
    rewrite inductiveHypothesis in
    rewrite plusAssociative left right (mult left right) in
    rewrite plusAssociative right left (mult left right) in
    rewrite plusCommutative right left in
            Refl

total multLeftSuccPlus : (left : Nat) -> (right : Nat) ->
  (S left) * right = right + (left * right)
multLeftSuccPlus left right = Refl

total multCommutative : (left : Nat) -> (right : Nat) ->
  left * right = right * left
multCommutative Z right        = rewrite multZeroRightZero right in Refl
multCommutative (S left) right =
  let inductiveHypothesis = multCommutative left right in
      rewrite inductiveHypothesis in
      rewrite multRightSuccPlus right left in
              Refl

total multDistributesOverPlusRight : (left : Nat) -> (centre : Nat) -> (right : Nat) ->
  left * (centre + right) = (left * centre) + (left * right)
multDistributesOverPlusRight Z        centre right = Refl
multDistributesOverPlusRight (S left) centre right =
  let inductiveHypothesis = multDistributesOverPlusRight left centre right in
    rewrite inductiveHypothesis in
    rewrite plusAssociative (plus centre (mult left centre)) right (mult left right) in
    rewrite sym (plusAssociative centre (mult left centre) right) in
    rewrite plusCommutative (mult left centre) right in
    rewrite plusAssociative centre right (mult left centre) in
    rewrite plusAssociative (plus centre right) (mult left centre) (mult left right) in
            Refl

total multDistributesOverPlusLeft : (left : Nat) -> (centre : Nat) -> (right : Nat) ->
  (left + centre) * right = (left * right) + (centre * right)
multDistributesOverPlusLeft Z        centre right = Refl
multDistributesOverPlusLeft (S left) centre right =
  let inductiveHypothesis = multDistributesOverPlusLeft left centre right in
    rewrite inductiveHypothesis in
    rewrite plusAssociative right (mult left right) (mult centre right) in
            Refl

total multAssociative : (left : Nat) -> (centre : Nat) -> (right : Nat) ->
  left * (centre * right) = (left * centre) * right
multAssociative Z        centre right = Refl
multAssociative (S left) centre right =
  let inductiveHypothesis = multAssociative left centre right in
    rewrite inductiveHypothesis in
    rewrite multDistributesOverPlusLeft centre (mult left centre) right in
            Refl

total multOneLeftNeutral : (right : Nat) -> 1 * right = right
multOneLeftNeutral Z         = Refl
multOneLeftNeutral (S right) =
  let inductiveHypothesis = multOneLeftNeutral right in
    rewrite inductiveHypothesis in
            Refl

total multOneRightNeutral : (left : Nat) -> left * 1 = left
multOneRightNeutral Z        = Refl
multOneRightNeutral (S left) =
  let inductiveHypothesis = multOneRightNeutral left in
    rewrite inductiveHypothesis in
            Refl

-- Minus
total minusSuccSucc : (left : Nat) -> (right : Nat) ->
  minus (S left) (S right) = minus left right
minusSuccSucc left right = Refl

total minusZeroLeft : (right : Nat) -> minus 0 right = Z
minusZeroLeft right = Refl

total minusZeroRight : (left : Nat) -> minus left 0 = left
minusZeroRight Z        = Refl
minusZeroRight (S left) = Refl

total minusZeroN : (n : Nat) -> Z = minus n n
minusZeroN Z     = Refl
minusZeroN (S n) = minusZeroN n

total minusOneSuccN : (n : Nat) -> S Z = minus (S n) n
minusOneSuccN Z     = Refl
minusOneSuccN (S n) = minusOneSuccN n

total minusSuccOne : (n : Nat) -> minus (S n) 1 = n
minusSuccOne Z     = Refl
minusSuccOne (S n) = Refl

total minusPlusZero : (n : Nat) -> (m : Nat) -> minus n (n + m) = Z
minusPlusZero Z     m = Refl
minusPlusZero (S n) m = minusPlusZero n m

total minusMinusMinusPlus : (left : Nat) -> (centre : Nat) -> (right : Nat) ->
  minus (minus left centre) right = minus left (centre + right)
minusMinusMinusPlus Z        Z          right = Refl
minusMinusMinusPlus (S left) Z          right = Refl
minusMinusMinusPlus Z        (S centre) right = Refl
minusMinusMinusPlus (S left) (S centre) right =
  let inductiveHypothesis = minusMinusMinusPlus left centre right in
    rewrite inductiveHypothesis in
            Refl

total plusMinusLeftCancel : (left : Nat) -> (right : Nat) -> (right' : Nat) ->
  minus (left + right) (left + right') = minus right right'
plusMinusLeftCancel Z right right'        = Refl
plusMinusLeftCancel (S left) right right' =
  let inductiveHypothesis = plusMinusLeftCancel left right right' in
    rewrite inductiveHypothesis in
            Refl

total multDistributesOverMinusLeft : (left : Nat) -> (centre : Nat) -> (right : Nat) ->
  (minus left centre) * right = minus (left * right) (centre * right)
multDistributesOverMinusLeft Z        Z          right = Refl
multDistributesOverMinusLeft (S left) Z          right =
    rewrite (minusZeroRight (plus right (mult left right))) in Refl
multDistributesOverMinusLeft Z        (S centre) right = Refl
multDistributesOverMinusLeft (S left) (S centre) right =
  let inductiveHypothesis = multDistributesOverMinusLeft left centre right in
    rewrite inductiveHypothesis in
    rewrite plusMinusLeftCancel right (mult left right) (mult centre right) in
            Refl

total multDistributesOverMinusRight : (left : Nat) -> (centre : Nat) -> (right : Nat) ->
  left * (minus centre right) = minus (left * centre) (left * right)
multDistributesOverMinusRight left centre right =
    rewrite multCommutative left (minus centre right) in
    rewrite multDistributesOverMinusLeft centre right left in
    rewrite multCommutative centre left in
    rewrite multCommutative right left in
            Refl

-- Power
total powerSuccPowerLeft : (base : Nat) -> (exp : Nat) -> power base (S exp) =
  base * (power base exp)
powerSuccPowerLeft base exp = Refl

total multPowerPowerPlus : (base : Nat) -> (exp : Nat) -> (exp' : Nat) ->
  (power base exp) * (power base exp') = power base (exp + exp')
multPowerPowerPlus base Z       exp' =
    rewrite sym (plusZeroRightNeutral (power base exp')) in Refl
multPowerPowerPlus base (S exp) exp' =
  let inductiveHypothesis = multPowerPowerPlus base exp exp' in
    rewrite sym inductiveHypothesis in
    rewrite sym (multAssociative base (power base exp) (power base exp')) in
            Refl

total powerZeroOne : (base : Nat) -> power base 0 = S Z
powerZeroOne base = Refl

total powerOneNeutral : (base : Nat) -> power base 1 = base
powerOneNeutral Z        = Refl
powerOneNeutral (S base) =
  let inductiveHypothesis = powerOneNeutral base in
    rewrite inductiveHypothesis in Refl

total powerOneSuccOne : (exp : Nat) -> power 1 exp = S Z
powerOneSuccOne Z       = Refl
powerOneSuccOne (S exp) =
  let inductiveHypothesis = powerOneSuccOne exp in
    rewrite inductiveHypothesis in Refl

total powerSuccSuccMult : (base : Nat) -> power base 2 = mult base base
powerSuccSuccMult Z        = Refl
powerSuccSuccMult (S base) = rewrite multOneRightNeutral base in Refl

total powerPowerMultPower : (base : Nat) -> (exp : Nat) -> (exp' : Nat) ->
  power (power base exp) exp' = power base (exp * exp')
powerPowerMultPower base exp Z        = rewrite multZeroRightZero exp in Refl
powerPowerMultPower base exp (S exp') =
  let inductiveHypothesis = powerPowerMultPower base exp exp' in
    rewrite inductiveHypothesis in
    rewrite multRightSuccPlus exp exp' in
    rewrite sym (multPowerPowerPlus base exp (mult exp exp')) in
            Refl

-- Pred
total predSucc : (n : Nat) -> pred (S n) = n
predSucc n = Refl

total minusSuccPred : (left : Nat) -> (right : Nat) ->
  minus left (S right) = pred (minus left right)
minusSuccPred Z        right = Refl
minusSuccPred (S left) Z =
    rewrite minusZeroRight left in Refl
minusSuccPred (S left) (S right) =
  let inductiveHypothesis = minusSuccPred left right in
    rewrite inductiveHypothesis in Refl

-- ifThenElse
total ifThenElseSuccSucc : (cond : Bool) -> (t : Nat) -> (f : Nat) ->
  S (ifThenElse cond t f) = ifThenElse cond (S t) (S f)
ifThenElseSuccSucc True  t f = Refl
ifThenElseSuccSucc False t f = Refl

total ifThenElsePlusPlusLeft : (cond : Bool) -> (left : Nat) -> (t : Nat) -> (f : Nat) ->
  left + (ifThenElse cond t f) = ifThenElse cond (left + t) (left + f)
ifThenElsePlusPlusLeft True  left t f = Refl
ifThenElsePlusPlusLeft False left t f = Refl

total ifThenElsePlusPlusRight : (cond : Bool) -> (right : Nat) -> (t : Nat) -> (f : Nat) ->
  (ifThenElse cond t f) + right = ifThenElse cond (t + right) (f + right)
ifThenElsePlusPlusRight True  right t f = Refl
ifThenElsePlusPlusRight False right t f = Refl

total ifThenElseMultMultLeft : (cond : Bool) -> (left : Nat) -> (t : Nat) -> (f : Nat) ->
  left * (ifThenElse cond t f) = ifThenElse cond (left * t) (left * f)
ifThenElseMultMultLeft True  left t f = Refl
ifThenElseMultMultLeft False left t f = Refl

total ifThenElseMultMultRight : (cond : Bool) -> (right : Nat) -> (t : Nat) -> (f : Nat) ->
  (ifThenElse cond t f) * right = ifThenElse cond (t * right) (f * right)
ifThenElseMultMultRight True  right t f = Refl
ifThenElseMultMultRight False right t f = Refl

-- Orders
total lteNTrue : (n : Nat) -> lte n n = True
lteNTrue Z     = Refl
lteNTrue (S n) = lteNTrue n

total LTESuccZeroFalse : (n : Nat) -> lte (S n) Z = False
LTESuccZeroFalse Z     = Refl
LTESuccZeroFalse (S n) = Refl

-- Minimum and maximum
total maximumAssociative : (l,c,r : Nat) -> maximum l (maximum c r) = maximum (maximum l c) r
maximumAssociative Z c r = Refl
maximumAssociative (S k) Z r = Refl
maximumAssociative (S k) (S j) Z = Refl
maximumAssociative (S k) (S j) (S i) = rewrite maximumAssociative k j i in Refl

total maximumCommutative : (l, r : Nat) -> maximum l r = maximum r l
maximumCommutative Z Z = Refl
maximumCommutative Z (S k) = Refl
maximumCommutative (S k) Z = Refl
maximumCommutative (S k) (S j) = rewrite maximumCommutative k j in Refl

total maximumIdempotent : (n : Nat) -> maximum n n = n
maximumIdempotent Z = Refl
maximumIdempotent (S k) = cong (maximumIdempotent k)

total minimumAssociative : (l,c,r : Nat) -> minimum l (minimum c r) = minimum (minimum l c) r
minimumAssociative Z c r = Refl
minimumAssociative (S k) Z r = Refl
minimumAssociative (S k) (S j) Z = Refl
minimumAssociative (S k) (S j) (S i) = rewrite minimumAssociative k j i in Refl

total minimumCommutative : (l, r : Nat) -> minimum l r = minimum r l
minimumCommutative Z Z = Refl
minimumCommutative Z (S k) = Refl
minimumCommutative (S k) Z = Refl
minimumCommutative (S k) (S j) = rewrite minimumCommutative k j in Refl

total minimumIdempotent : (n : Nat) -> minimum n n = n
minimumIdempotent Z = Refl
minimumIdempotent (S k) = cong (minimumIdempotent k)

total minimumZeroZeroRight : (right : Nat) -> minimum 0 right = Z
minimumZeroZeroRight Z = Refl
minimumZeroZeroRight (S right) = minimumZeroZeroRight right

total minimumZeroZeroLeft : (left : Nat) -> minimum left 0 = Z
minimumZeroZeroLeft Z        = Refl
minimumZeroZeroLeft (S left) = Refl

total minimumSuccSucc : (left : Nat) -> (right : Nat) ->
  minimum (S left) (S right) = S (minimum left right)
minimumSuccSucc Z        Z         = Refl
minimumSuccSucc (S left) Z         = Refl
minimumSuccSucc Z        (S right) = Refl
minimumSuccSucc (S left) (S right) = Refl

total maximumZeroNRight : (right : Nat) -> maximum Z right = right
maximumZeroNRight Z         = Refl
maximumZeroNRight (S right) = Refl

total maximumZeroNLeft : (left : Nat) -> maximum left Z = left
maximumZeroNLeft Z        = Refl
maximumZeroNLeft (S left) = Refl

total maximumSuccSucc : (left : Nat) -> (right : Nat) ->
  S (maximum left right) = maximum (S left) (S right)
maximumSuccSucc Z        Z         = Refl
maximumSuccSucc (S left) Z         = Refl
maximumSuccSucc Z        (S right) = Refl
maximumSuccSucc (S left) (S right) = Refl

total sucMaxL : (l : Nat) -> maximum (S l) l = (S l)
sucMaxL Z = Refl
sucMaxL (S l) = cong (sucMaxL l)

total sucMaxR : (l : Nat) -> maximum l (S l) = (S l)
sucMaxR Z = Refl
sucMaxR (S l) = cong (sucMaxR l)

total sucMinL : (l : Nat) -> minimum (S l) l = l
sucMinL Z = Refl
sucMinL (S l) = cong (sucMinL l)

total sucMinR : (l : Nat) -> minimum l (S l) = l
sucMinR Z = Refl
sucMinR (S l) = cong (sucMinR l)

max_stars_repo_name: ajnavarro/language-dataset

max_issues_repo_name: ajnavarro/language-dataset

max_forks_repo_name: ajnavarro/language-dataset


text:
-- Axiom of (constructive) choice

ch : {0 r : a -> b -> Type} -> ((x : a) -> (y : b ** r x y)) -> (f : a -> b ** (x : a) -> r x (f x))
ch f = (\x => fst (f x) ** \x => let _ = True in snd (f x))

-- The dummy `let` above is needed for typecheck success in idris-0.3.0, to be removed when fixed.

ext: idr

max_stars_repo_name: buzden/idris-playground

max_issues_repo_name: buzden/idris-playground

max_forks_repo_name: buzden/idris-playground


text:
module Main

import Data.Vect
import Control.ST
import Control.ST.ImplicitCall
import TicTacToe

start : ST m Var [add (State (Game Start InPlay))]
start = do game <- new initGame
           pure game

status : (game : Var) -> ST m GameState [game ::: State (Game b st)]
status game = pure $ currentStatus !(read game)

grid : (game : Var) -> ST m Grid [game ::: State (Game b st)]
grid game = pure $ currentGrid !(read game)

board : {b : Board g p turn} -> (game : Var) -> ST m (Board g p turn) [game ::: State (Game b st)]
board game = pure $ currentBoard !(read game)

move : {b : Board g p turn}
    -> (pos : Position)
    -> (game : Var)
    -> {auto prf : Empty pos g}
    -> ST m GameState [game ::: State (Game b InPlay) :->
                          (\st' => State (Game (Turn pos b {prf = prf}) st'))]
move pos game = do g <- read game
                   let (st' ** g') = move pos g
                   write game g'
                   pure st'

inputPosition : ConsoleIO m => ST m (Maybe Position) []
inputPosition = do putStr "Input x position: "
                   x <- inputNat
                   putStr "Input y position: "
                   y <- inputNat
                   pure [MkPair px py | x' <- x, y' <- y, px <- natToFin x' 3, py <- natToFin y' 3]
  where
    inputNat : ConsoleIO m => ST m (Maybe Nat) []
    inputNat = do input <- getStr
                  if all isDigit (unpack input)
                     then pure . Just . cast $ input
                     else pure Nothing

inputPosLoop : ConsoleIO m => ST m Position []
inputPosLoop = do Just pos <- inputPosition
                    | Nothing => do putStrLn "Bad input"
                                    inputPosLoop
                  pure pos

ExistBoard : Type
ExistBoard = (g : Grid ** p : Player ** turn : Nat ** Board g p turn)

WholeGame : (ExistBoard, EndState) -> Type
WholeGame ((_ ** _ ** _ ** b), res) = State (Game b (Ended res))

loop : ConsoleIO m
    => (game : Var)
    -> {b : Board g p turn}
    -> ST m (ExistBoard, EndState)
            [game ::: State (Game b InPlay) :-> WholeGame]
loop game {b} {g} = do putStrLn $ Grid.show g
                       pos <- inputPosLoop
                       case isEmpty pos g of
                            Yes prf => do InPlay <- move pos game
                                            | Ended end => pure ((_ ** _ ** _ ** _), end)
                                          loop game
                            No contra => do putStrLn "Position already occupied"
                                            loop game

main : IO ()
main = run $ do game <- start
                ((g ** _ ** _ ** b), res) <- loop game
                putStrLn $ Grid.show g
                case res of
                     Draw => do putStrLn "DRAW!"
                                delete game
                     Won p => do print p
                                 putStrLn " is the WINNER!"
                                 delete game

max_stars_repo_name: ShinKage/DT-TicTacToe

max_issues_repo_name: ShinKage/DT-TicTacToe

max_forks_repo_name: ShinKage/DT-TicTacToe


text:
module Main

import Debug.Trace

{- Image -}

imageWidth : Nat
imageWidth = 256

imageHeight : Nat
imageHeight = 256

{- Render -}

main : IO ()
main =
  do
    _ <- fPutStr stdout $ "P3\n" ++ (show imageWidth) ++ " " ++ (show imageHeight) ++ "\n255\n"
    _ <- renderRows imageHeight
    pure ()

  where

    renderCells : (i : Nat) -> (j : Nat) -> IO (Either FileError ())
    renderCells Z _ = pure (Right ())
    renderCells (S i) j = do
      let i' : Nat = minus imageWidth (i + 1)
      let r : Double = (cast i') / (cast (minus imageWidth 1))
      let g : Double = (cast j) / (cast (minus imageHeight 1))
      let b : Double = 0.25

      let ir : Int = cast (255.99 * r)
      let ig : Int = cast (255.99 * g)
      let ib : Int = cast (255.99 * b)

      _ <- fPutStrLn stdout $ (show ir) ++ " " ++ (show ig) ++ " " ++ (show ib)

      renderCells i j

    renderRows : (j : Nat) -> IO (Either FileError ())
    renderRows Z = pure (Right ())
    renderRows (S j) = do
      _ <- trace ("Scanlines remaining: " ++ (show (j + 1))) $ pure ()
      _ <- renderCells imageWidth j
      renderRows j


text:
module LifeSMT

import Data.Vect
import src.SMTLib
import src.Tensor
import src.GridOps

pattern0 : Vect 6 (Vect 6 Int)
pattern0 = [[0, 0, 0, 0, 0, 0],
            [0, 0, 1, 0, 0, 0],
            [0, 0, 0, 1, 0, 0],
            [0, 1, 1, 1, 0, 0],
            [0, 0, 0, 0, 0, 0],
            [0, 0, 0, 0, 0, 0]]

pattern1 : Vect 6 (Vect 6 Int)
pattern1 = [[0, 0, 0, 0, 0, 0],
            [0, 0, 0, 0, 0, 0],
            [0, 1, 0, 1, 0, 0],
            [0, 0, 1, 1, 0, 0],
            [0, 0, 1, 0, 0, 0],
            [0, 0, 0, 0, 0, 0]]

lookup : Fin n -> Fin m -> List Dir ->  Vect n (Vect m (Expr (NumT IntT))) -> Expr (NumT IntT)
lookup n m ds xss = GridOps.lookup n m ds (int 0) xss

countNeighborhoods : Fin n -> Fin m -> Vect n (Vect m (Expr (NumT IntT))) -> Expr (NumT IntT)
countNeighborhoods n m xss with (toPos n, toPos m)
 countNeighborhoods n m xss | (First, First) = add [lookup n m [Left] xss, lookup n m [Up] xss, lookup n m [Up, Left] xss]
 countNeighborhoods n m xss | (Last, Last) = add [lookup n m [Right] xss, lookup n m [Down] xss, lookup n m [Down, Right] xss]
 countNeighborhoods n m xss | (First, Last) = add [lookup n m [Right] xss, lookup n m [Up] xss, lookup n m [Up, Right] xss]
 countNeighborhoods n m xss | (Last, First) = add [lookup n m [Left] xss, lookup n m [Down] xss, lookup n m [Down, Left] xss]
 countNeighborhoods n m xss | (First, _) = add [lookup n m [Left] xss, lookup n m [Right] xss, lookup n m [Up] xss,
                                                lookup n m [Up, Right] xss, lookup n m [Up, Left] xss]
 countNeighborhoods n m xss | (Last, _) = add [lookup n m [Left] xss, lookup n m [Right] xss, lookup n m [Down] xss,
                                               lookup n m [Down, Right] xss, lookup n m [Down, Left] xss]
 countNeighborhoods n m xss | (_, First) = add [lookup n m [Left] xss, lookup n m [Down] xss, lookup n m [Down, Left] xss,
                                                lookup n m [Up] xss, lookup n m [Up, Left] xss]
 countNeighborhoods n m xss | (_, Last) = add [lookup n m [Right] xss, lookup n m [Down] xss, lookup n m [Down, Right] xss,
                                               lookup n m [Up] xss, lookup n m [Up, Right] xss]
 countNeighborhoods n m xss | (_, _) = add [lookup n m [Left] xss, lookup n m [Right] xss, lookup n m [Down] xss,
                                            lookup n m [Up] xss, lookup n m [Down, Right] xss, lookup n m [Down, Left] xss,
                                            lookup n m [Up, Right] xss, lookup n m [Up, Left] xss]

rules : Vect n (Vect m (Expr (NumT IntT))) -> Vect n (Vect m (Expr (NumT IntT))) -> Vect n (Vect m (Expr (NumT IntT))) -> Expr BoolT
rules counters fromBoard toBoard = and $ concat $ tabulate (\i0 => tabulate (\i1 => rule i0 i1 counters fromBoard toBoard))
  where
    rule : Fin n -> Fin m -> Vect n (Vect m (Expr (NumT IntT))) -> Vect n (Vect m (Expr (NumT IntT))) -> Vect n (Vect m (Expr (NumT IntT))) -> Expr BoolT
    rule n m counters fromBoard toBoard = let c = index n m counters in
                                          let eqc = countNeighborhoods n m fromBoard == c in
                                          let from = index n m fromBoard in
                                          let eqf = from == (int 0) || from == (int 1) in
                                          let to = index n m toBoard in
                                          let eqt = to == (int 0) || to == (int 1) in
                                          let r = ite (from == (int 1))
                                                    (ite (c == (int 0) || c == (int 1))
                                                      (to == (int 0))
                                                      (ite (or [c == (int 4), c == (int 5), c == (int 6),
                                                                c == (int 7), c == (int 8)])
                                                        (to == (int 0))
                                                        (ite (or [c == (int 2), c == (int 3)])
                                                          (to == (int 1))
                                                          (bool False))))
                                                    (ite (c == (int 3))
                                                      (to == (int 1))
                                                      (to == (int 0))) in
                                          and [eqc, eqf, eqt, r]

validPattern : Vect n (Vect m Int) -> Vect n (Vect m (Expr (NumT IntT))) -> Expr BoolT
validPattern pattern board = and $ concat $ tabulate (\i0 => tabulate (\i1 => index i0 i1 board == (int $ index i0 i1 pattern)))

initBoard : Tensor [6, 6] String
initBoard = toTensor $ tabulate (\i0 => tabulate (\i1 => "x_" ++ show (finToNat i0) ++ "_" ++ show (finToNat i1)))

finalBoard : Tensor [6, 6] String
finalBoard = toTensor $ tabulate (\i0 => tabulate (\i1 => "y_" ++ show (finToNat i0) ++ "_" ++ show (finToNat i1)))

counters : Tensor [6, 6] String
counters = toTensor $ tabulate (\i0 => tabulate (\i1 => "c_" ++ show (finToNat i0) ++ "_" ++ show (finToNat i1)))

solver : Smt ()
solver = do initBoard <- declareVars initBoard (NumT IntT)
            finalBoard <- declareVars finalBoard (NumT IntT)
            counters <- declareVars counters (NumT IntT)
            assert $ rules (toVect counters) (toVect initBoard) (toVect finalBoard)
            assert $ validPattern pattern1 (toVect finalBoard)
            checkSat
            getModel
            end

test : IO ()
test = print solver

max_stars_repo_name: STELIORD/idris-snippets

max_issues_repo_name: stjordanis/idris-snippets

max_forks_repo_name: stjordanis/idris-snippets


text:
module Specdris.Expectations

import Specdris.Data.SpecResult
import Specdris.Core

%access export
%default total

||| Placeholder for the future test implementation. Is listed in the
||| final spec result.
pending : SpecResult
pending = Pending Nothing

||| Same as `pending`, just adds a more detailed description
|||
||| @ message description of what the spec case should test
pendingWith : (message : String) -> SpecResult
pendingWith message = Pending (Just message)

||| Checks if two elements are equal.
shouldBe : (Eq a, Show a) => (actual : a) -> (expected : a) -> SpecResult
shouldBe actual expected = if actual == expected then
                             Success
                           else
                             BinaryFailure actual expected "not equal"

infixr 7 ===

||| Checks if two elements are equal
(===) : (Eq a, Show a) => (actual : a) -> (expected : a) -> SpecResult
(===) = shouldBe

||| Checks if two element are unequal
shouldNotBe : (Eq a, Show a) => (actual : a) -> (expected : a) -> SpecResult
shouldNotBe actual expected = if actual /= expected then
                                Success
                              else
                                BinaryFailure actual expected "equal"

infixr 7 /==

||| Checks if two element are unequal
(/==) : (Eq a, Show a) => (actual : a) -> (expected : a) -> SpecResult
(/==) = shouldNotBe

||| Checks if the given element auf type `Bool` is `True`
shouldBeTrue : (actual : Bool) -> SpecResult
shouldBeTrue actual = actual === True

||| Checks if the given element auf type `Bool` is `False`
shouldBeFalse : (actual : Bool) -> SpecResult
shouldBeFalse actual = actual === False

||| Checks if the given element satisfies the predicate
shouldSatisfy : Show a => (actual : a) -> (pred : a -> Bool) -> SpecResult
shouldSatisfy actual pred = if pred actual then
                              Success
                            else
                              UnaryFailure actual "doesn't satisfy predicate"

||| Checks if the given `Maybe` element is `Just` and satisfies further expectations
shouldBeJust : Show a => (actual : Maybe a) -> (expectation : a -> SpecResult) -> SpecResult
shouldBeJust (Just a) expectation = expectation a
shouldBeJust {a} Nothing _        = UnaryFailure (Nothing {a}) "is not `Just`"

||| Checks if the given `Maybe` element is `Nothing`
shouldBeNothing : Show a => (actual: Maybe a) -> SpecResult
shouldBeNothing Nothing = Success
shouldBeNothing actual  = UnaryFailure actual "is not `Nothing`"

max_stars_repo_name: pheymann/specdris

max_issues_repo_name: pheymann/specdris

max_forks_repo_name: pheymann/specdris


text:
-- --------------------------------------------------------------- [ Error.idr ]
-- Module    : Error.idr
-- Copyright : (c) Jan de Muijnck-Hughes
-- License   : see LICENSE
-- --------------------------------------------------------------------- [ EOH ]
||| Common code for all DSML DSLs
module GRL.Lang.Common.Error

%access public export
-- ------------------------------------------------------------------ [ Errors ]

data GError : Type where
  NoFileError      : GError
  NoSuchFileError  : String -> GError
  ParserError      : String -> String -> GError
  NoSuchIdentError : String -> GError
  BadModelError    : GError

Show GError where
  show (NoFileError)            = "File Must Be specified"
  show (NoSuchFileError fn)     = unwords ["No such file:", show fn]
  show (ParserError fn err)     = unlines [unwords ["Unable to parse", show fn, "because:"], err]
  show (NoSuchIdentError ident) = unwords ["No such identifier:", show ident]
  show (BadModelError)          = "Bad Model"

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

max_stars_repo_name: jfdm/idris-grl

max_issues_repo_name: jfdm/idris-grl

max_forks_repo_name: jfdm/idris-grl


text:
-- -------------------------------------------------------------- [ Freyja.idr ]
-- Module    : Freyja.idr
-- Copyright : (c) Jan de Muijnck-Hughes
-- License   : see LICENSE
-- --------------------------------------------------------------------- [ EOH ]
module Sif.Pattern.Convert.Freyja

import Data.AVL.Dict
import Data.DList
import GRL.Lang.GLang

import XML.DOM

import Edda
import Edda.Reader.Org

import Freyja

import Sif.Types
import Sif.Pattern.Model
import Sif.Pattern.API

%access private

-- ------------------------------------------------------------------- [ Utils ]

inlines : String -> EddaString
inlines s =
  case readOrgInline s of
    Left err  => [Text "Error"]
    Right res => res

paras : Maybe String -> EddaBody
paras Nothing  = [Para (inlines "To Be Added")]
paras (Just s) =
  case readOrgBody s of
    Left err  => [Para (inlines $ show err)]
    Right res => res

-- ------------------------------------------------------------ [ Requirements ]

convertReq : REQUIREMENT impl d -> DPair RTy Requirement
convertReq r = (ty ** MkReq ty n d)
  where
    n : EddaString
    n = inlines (SifExpr.getTitle r)

    d : EddaBody
    d = paras (SifExpr.getDesc r)

    ty : RTy
    ty = SifExpr.getRTy r

convertProblem : PROBLEM impl d -> Problem
convertProblem p = MkProblem n d (snd rs)
  where
    n : EddaString
    n = inlines (SifExpr.getTitle p)

    d : EddaBody
    d = paras (SifExpr.getDesc p)

    rs : (rs' ** DList RTy Requirement rs')
    rs = fromLDP $ map (convertReq) (SifExpr.getReqs p)

-- ---------------------------------------------------------------- [ Solution ]

convertAffect : AFFECT impl d -> Affect
convertAffect a = MkAffect c (snd r) d
  where
    c : CValue
    c = SifExpr.getCValue a

    r : (DPair RTy Requirement)
    r = convertReq $ SifExpr.getReq a

    d : Maybe EddaBody
    d = case (SifExpr.getDesc a) of
          Nothing => Nothing
          d'      => Just $ paras d'

-- ------------------------------------------------------------------- [ Trait ]

convertTrait : TRAIT impl d -> DPair TTy Trait
convertTrait t = (ty ** MkTrait ty n d (SifExpr.getSValue t) as)
  where
    ty : TTy
    ty = (SifExpr.getTTy t)

    n : EddaString
    n = inlines (SifExpr.getTitle t)

    d : EddaBody
    d = paras (SifExpr.getDesc t)

    as : List Affect
    as = map (convertAffect) $ SifExpr.getAffects t

-- ---------------------------------------------------------------- [ Property ]

convertProperty : PROPERTY impl d -> Property
convertProperty p = MkProperty t d (snd ts)
  where
    t : EddaString
    t = inlines (SifExpr.getTitle p)

    d : EddaBody
    d = paras (SifExpr.getDesc p)

    ts : (ls ** DList TTy Trait ls)
    ts = fromLDP $ map convertTrait (SifExpr.getTraits p)

-- ---------------------------------------------------------------- [ Solution ]

convertSolution : SOLUTION impl d -> Solution
convertSolution s = MkSolution t d [ms,md] ps
  where
    t : EddaString
    t = inlines (SifExpr.getTitle s)

    d : EddaBody
    d = paras (SifExpr.getDesc s)

    ms : Model STRUCT
    ms = MkModel (inlines "Example Structure")
                 STRUCT
                 (paras Nothing)
                 "MODEL inserted here"

    md : Model DYN
    md = MkModel (inlines "Example Dynamic")
                 DYN
                 (paras Nothing)
                 "MODEL inserted here"

    ps : List Property
    ps = map (convertProperty) $ SifExpr.getProperties s

-- ------------------------------------------------------------------ [ Domain ]

convertDomain : SifDomain -> Context
convertDomain (MkDomain t d) = MkContext (inlines t) (paras d)

-- ----------------------------------------------------------------- [ Pattern ]

convertPattern : PATTERN impl d -> PatternDoc
convertPattern p = MkPDoc n d md c p' s e ss Nil
  where
    n : EddaString
    n = inlines (SifExpr.getTitle p)

    d : EddaBody
    d = paras $ SifExpr.getDesc p

    md : Metadata
    md = MkMData Nil Nil Nil Nil "nout" "nout" "nout" "nout"

    c : Context
    c = convertDomain (SifExpr.getDomain p)

    p' : Problem
    p' = convertProblem $ SifExpr.getProblem p

    s : Solution
    s = convertSolution $ SifExpr.getSolution p

    e : EddaBody
    e = paras Nothing

    ss : List Study
    ss = [MkStudy (inlines "To be determined") e e]

namespace Sif
  export
  toFreyja : PATTERN impl d -> PatternDoc
  toFreyja p = convertPattern p
-- --------------------------------------------------------------------- [ EOF ]

max_stars_repo_name: jfdm/sif-lang

max_issues_repo_name: jfdm/sif-lang

max_forks_repo_name: jfdm/sif-lang


text:
module Language.Elab.Deriving.ShowTest

import Language.Elab.Deriving.Show
%language ElabReflection

-- Testing of elaborations all on their own. (At bottom.)

export
data Foo1 : Type -> Type where
  Bor1 : Foo1 a

export
data Foo2 : Type -> Type where
  Bor2 : a -> Foo2 a

data Foo4 : Type -> Type -> Type where
  Bor4 : b -> Foo4 a b

data Foo5 : Type -> Type -> Type -> Type where
  Bor5 : a -> b -> c -> Foo5 a b c

-- NB c is never used, so Eq shouldn't be required for it
data Foo7 : Type -> Type -> Type -> Type where
  Zor7 : a -> Foo7 a b c
  Gor7 : b -> Foo7 a b c
  Nor7A : a -> b -> Foo7 a b c
  Nor7B : a -> b -> c -> Foo7 a b c
  Bor7 : Foo7 a b c

-- NB a is never used, so Eq shouldn't be required for it
data Foo7' : Type -> Type -> Type -> Type where
  Zor7' : c -> Foo7' a b c
  Gor7' : b -> Foo7' a b c
  Nor7' : b -> c -> Foo7' a b c
  Bor7' : Foo7' a b c

  -- we'll use our own nat for index experimentation
export
data MyNat : Type where
  MZ : MyNat
  MS : MyNat -> MyNat

data Foo6 : Type -> Type -> Type -> Nat -> Type where
  Zor6 : a -> b -> Foo6 a b c Z
  Gor6 : b -> Foo6 a b c (S k)
  Nor6A : a -> b -> c -> Foo6 a b c n
  Nor6B : a -> (0 _ : b) -> c -> Foo6 a b c n -- NB: 0 Use arg
  Bor6A : Foo6 a b c n
  Bor6B : Foo6 a b c n -> Foo6 a b c n
  Wah6 : a -> (n : Nat) -> Foo6 a b c n

export
data Foo6' : Type -> Type -> Type -> MyNat -> Type where
  Zor6'  : a -> b -> Foo6' a b c MZ
  Gor6A'  : b -> Foo6' a b c (MS k)
  Gor6B'  : (k : MyNat) -> b -> Foo6' a b c (MS k)
  Nor6A' : a -> b -> c -> Foo6' a b c n
  Nor6B' : a -> (0 _ : b) -> c -> Foo6' a b c n
  Bor6'  : Foo6' a b c n
  Wah6'  : a -> (n : MyNat) -> Foo6' a b c n
  Kah6'  : a -> (n : MyNat) -> (0 _ : c) -> Foo6' a b c n
  Pah6'  : a -> (n : MyNat) -> MyNat -> (0 _ : c) -> Foo6' a b c n
  -- Rah6'  : a -> (n : MyNat) -> Foo6' a b c n -> MyNat -> (0 _ : c) -> Foo6' a b c n -> Foo6' a b c n
  -- Gah6'  : {1 _ : a} -> (n : MyNat) -> MyNat -> (0 _ : c) -> Foo6' a b c n
  -- ^ another case to consider, what if I'm implicit but M1?
  -- Seems like an error would be appropriate there rather than showing
  -- implicits. Though showing implicits could be a flag in instance generation
  -- I guess.

-- eqImplFoo6'Fun (Wah6' 'c' MZ) (Wah6' 'c' MZ)
-- eqImplFoo6'Fun (Nor6A' {n=MZ} 'c' 'd' 'e')

-- eqImplFoo6Fun (Wah6 {b=Int} {c=String} 'c' (S Z)) (Wah6 'c' (S Z))

-- reference impl
-- NB We need to use n twice, Eq is not dependent, two values of `a` compared
-- against each other must have the same indices. Which follows since if they
-- don't they're obviously not equal.
-- if a con has no explicit, non-M0, non-index, vars then it's empty, and thus
-- vauously true to compare to itself. only explicit, non-M0, non-index vars need
-- to be compared. M0 values can't be used and index vars can't vary in an Eq
-- definition
eqFoo6 : (Eq a, Eq b, Eq c) => Foo6 a b c n -> Foo6 a b c n -> Bool
eqFoo6 (Zor6 x1 y1) (Zor6 x2 y2) = x1 == x2 && y1 == y2
eqFoo6 (Gor6 x1) (Gor6 x2) = x1 == x2
eqFoo6 (Nor6A x1 y1 z1) (Nor6A x2 y2 z2) = x1 == x2 && y1 == y2 && z1 == z2
eqFoo6 (Nor6B x1 _ z1) (Nor6B x2 _ z2) = x1 == x2 && z1 == z2
eqFoo6 Bor6A Bor6A = True
eqFoo6 (Bor6B x1) (Bor6B x2) = eqFoo6 x1 x2
-- we prefer to write this as x1 == x2, and we do so by declaring our Eq object
-- early, otherwise there's no instance for Foo6 to use == from
eqFoo6 (Wah6 x1 _) (Wah6 x2 _) = x1 == x2 -- indices do not differ
eqFoo6 _ _ = False
-- eqFoo6 {b=Int} {c=String} (Wah6 'c' (S Z)) (Wah6 'c' (S Z))

data FooN : MyNat -> Type -> Type where
  BorZ : b -> FooN MZ b
  BorS : b -> FooN (MS MZ) b
  BorNA : (k : MyNat) -> b -> FooN n b
  BorNB : (n : MyNat) -> b -> FooN n b

%runElab deriveShow Export  `{{MyNat}}
%runElab deriveShow Export `{{Foo1}}
%runElab deriveShow Export  `{{Foo2}}
%runElab deriveShow Private `{{Foo4}}
%runElab deriveShow Private `{{Foo5}}
%runElab deriveShow Private `{{Foo7}}
%runElab deriveShow Private `{{Foo7'}}
%runElab deriveShow Private `{{FooN}}
%runElab deriveShow Private `{{Foo6}}
%runElab deriveShow Export  `{{Foo6'}}

-- can check what's generated via
-- :printdef showImplFoo7'Fun

-- Will need to supply types if playing in the repl, e.g.:
-- show (Wah6' 'c' MZ {b=Char} {c=Int})


text:
module Heads

import Arith
import Data.Primitives.Views

data Face : Type where
     Heads : Face
     Tails : Face

coinFlips : (count : Nat) -> Stream Int -> List Face
coinFlips Z (value :: xs) = []
coinFlips (S k) (value :: xs) = getFace value :: coinFlips k xs
  where getFace : Int -> Face
        getFace x with (divides x 2)
          getFace ((2 * div) + rem) | (DivBy prf) = if rem == 0 then Heads else Tails

max_stars_repo_path: Chapter 11/Heads.idr

max_issues_repo_path: Chapter 11/Heads.idr

max_forks_repo_path: Chapter 11/Heads.idr


text:
module Data.Trichotomy

%default total

||| Trichotomy formalises the fact that three relations are mutually
||| exclusive. A value of type `Trichotomy lt m n` proofs, that
||| exactly one of the relations `lt m n`, `m === n`, or `lt n m` holds.
|||
||| All proofs held by a value of type `Trichotomous` are erased, so
||| at runtime such values get optimized to numbers 0, 1, or 2
||| respectively.
public export
data Trichotomy : (lt : a -> a -> Type) -> (a -> a -> Type) where
  LT :  {0 lt : a -> a -> Type}
     -> (0 _ : lt v w)
     -> (0 _ : Not (v === w))
     -> (0 _ : Not (lt w v))
     -> Trichotomy lt v w

  EQ :  {0 lt : a -> a -> Type}
     -> (0 _ : Not (lt v w))
     -> (0 _ : v === w)
     -> (0 _ : Not (lt w v))
     -> Trichotomy lt v w

  GT :  {0 lt : a -> a -> Type}
     -> (0 _ : Not (lt v w))
     -> (0 _ : Not (v === w))
     -> (0 _ : lt w v)
     -> Trichotomy lt v w

public export
Eq (Trichotomy lt m n) where
  LT _ _ _ == LT _ _ _ = True
  EQ _ _ _ == EQ _ _ _ = True
  GT _ _ _ == GT _ _ _ = True
  _        == _        = False

public export
Ord (Trichotomy lt m n) where
  compare (LT _ _ _) (LT _ _ _) = EQ
  compare (LT _ _ _) _          = LT
  compare _          (LT _ _ _) = GT
  compare (EQ _ _ _) (EQ _ _ _) = EQ
  compare (EQ _ _ _) _          = LT
  compare _          (EQ _ _ _) = GT
  compare (GT _ _ _) (GT _ _ _) = EQ

public export
Show (Trichotomy lt m n) where
  show (LT _ _ _) = "LT"
  show (EQ _ _ _) = "EQ"
  show (GT _ _ _) = "GT"

public export
toOrdering : Trichotomy lt m n -> Ordering
toOrdering (LT _ _ _) = LT
toOrdering (EQ _ _ _) = EQ
toOrdering (GT _ _ _) = GT


text:
module Main

main : IO ()
main = repl "\n> " reverse

max_stars_repo_name: curtisalexander/tdd-idris

max_issues_repo_name: curtisalexander/tdd-idris

max_forks_repo_name: curtisalexander/tdd-idris


text:
{-
42
4.2
it works!
True
00000000-0000-0000-0000-000000000000
VoidFunction : Void
exportedBoolToString : (p0 : Boolean) -> String
printMethod : (t : Type) -> (n : String) -> Void
take5 : (defaultValue : String) -> (flag : Boolean) -> (c : Char) -> (i : Int32) -> (d : Double) -> String
before exportedVoidIO
exported!
after exportedVoidIO
exportedBoolToStringIO True
exportedBoolToStringIO => True
Alan Kay
Kay, Alan
3
-}

module Main

import CIL.System.Reflection
import Data.Vect

%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.Double
  Max : Double -> Double -> CIL_IO Double
  Max = invoke SystemMathMax (Double -> Double -> CIL_IO Double)

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

  implementation 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"

GuidTy : CILTy
GuidTy = corlibTyVal "System.Guid"

Guid : Type
Guid = CIL $ GuidTy

implementation 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)

%inline
objectArrayFor : Vect _ Object -> CIL_IO ObjectArray
objectArrayFor xs = arrayOf CILTyObj xs

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

invokeStaticMethod : RuntimeType -> String -> Nullable ObjectArray -> CIL_IO (Maybe Object)
invokeStaticMethod type methodName args =
  nullable (pure Nothing) (\method => Just <$> Invoke method null args) !(type `GetMethod` methodName)

testExportedVoidFunction : RuntimeType -> CIL_IO ()
testExportedVoidFunction type = do
  putStrLn "before exportedVoidIO"
  invokeStaticMethod type "VoidFunction" null
  putStrLn "after exportedVoidIO"

testExportedBoolToStringIO : RuntimeType -> CIL_IO ()
testExportedBoolToStringIO type = do
  ret <- invokeStaticMethod type "exportedBoolToStringIO" (asNullable !(objectArrayFor [asObject True]))
  retString <- maybe (pure "ERROR") ToString ret
  putStrLn $ "exportedBoolToStringIO => " ++ retString

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
  pure $ 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

showParameter : ParameterInfo -> CIL_IO String
showParameter p = do
  n <- get_Name p
  t <- get_ParameterType p >>= get_Name
  pure $ "(" ++ n ++ " : " ++ t ++ ")"

showMethod : MethodInfo -> CIL_IO String
showMethod m = do
  name <- get_Name m
  ps   <- foldr (\p, acc => (:: acc) <$> showParameter p) (the (List _) []) !(GetParameters m)
  ret  <- get_ReturnType m >>= get_Name
  let sig = ps ++ [ret]
  pure $ name ++ " : " ++ (concat . intersperse " -> " $ sig)

printMethod : RuntimeType -> String -> CIL_IO ()
printMethod t n = do
  m <- t `GetMethod` n
  nullable (pure "method not found") showMethod m >>= putStrLn

testBoxingUnboxing : RuntimeType -> CIL_IO ()
testBoxingUnboxing type = do
  ret <- invokeStaticMethod type "exportedIncInt" (asNullable !(objectArrayFor [asObject 2]))
  maybe (pure "ERROR") ToString ret >>= putStrLn

main : CIL_IO ()
main = do
  testOverloadedStaticMethod
  testInstanceMethods
  testValueType

  asm <- GetExecutingAssembly
  type <- GetType asm "TheExports" True
  for_ (the (List _) ["VoidFunction", "exportedBoolToString", "printMethod", "take5"]) $
    printMethod 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
  pure $ show b

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

parameters (defaultValue: String, flag: Bool)

  take5 : Char -> Int -> Double -> String
  take5 c i d = if flag then defaultValue else show $ cast (ord c) + cast i + d

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 printMethod CILDefault $ -- export signature containing CIL type
  Fun take5 CILDefault
  End

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

max_stars_repo_name: timjs/iris-clean

max_issues_repo_name: timjs/iris-clean

max_forks_repo_name: timjs/iris-clean


text:
module Main

import Backprop
import Control.Algebra
import Control.Optics
import Data.List.Quantifiers
import Data.Nat
import Data.Num
import Data.String.Extra
import Data.Vect
import Debug.Trace
import Linear
import Linear.Backprop
import Linear.Math
import Linear.Random
import NN.Dense
import Utils.String

record Params where
  constructor MkParams
  dense1 : Dense 2 3 Double
  dense2 : Dense 3 1 Double

ldense1 : Simple Lens ? ?
ldense1 = lens dense1 $ \s, b => { dense1 := b } s

ldense2 : Simple Lens ? ?
ldense2 = lens dense2 $ \s, b => { dense2 := b } s

FromDouble Params where
  fromDouble x = MkParams (fromDouble x) (fromDouble x)

CanBack Params where
  zero = MkParams zero zero
  one = MkParams one one
  add (MkParams a1 a2) (MkParams b1 b2) = MkParams (add a1 b1) (add a2 b2)

Num Params where
  (+) = add
  MkParams a1 a2 * MkParams b1 b2 = MkParams (a1 * b1) (a2 * b2)
  fromInteger x = MkParams (fromInteger x) (fromInteger x)

Neg Params where
  MkParams a1 a2 - MkParams b1 b2 = MkParams (a1 - b1) (a2 - b2)
  negate (MkParams a1 a2) = MkParams (negate a1) (negate a2)

Show Params where
  show params = show_record "MkParams" [("dense1", show params.dense1), ("dense2", show params.dense2)]

model : {n : _} -> Node i Params -> Node i (T [n, 2] Double) -> Node i (T [n, 1] Double)
model p = sigmoid . apply (p ^. ldense2) . sigmoid . apply (p ^. ldense1)

loss : {a, n : _} -> Neg a => CanBack a => Floating a => (y : Node i (T [n, 1] a)) -> (y' : Node i (T [n, 1] a)) -> Node i a
loss y y' = asum $ asum $ square (y - y')

gd : {loss_t : _} -> (Neg params_t, Num params_t, CanBack params_t, CanBack loss_t, FromDouble params_t) => (loss_node : Node params_t loss_t) -> (params : params_t) -> (learning_rate : Double) -> (loss_t, params_t)
gd loss_node params alpha = let (loss, grads) = backprop loss_node params in (loss, params - fromDouble alpha * grads)

gdn : {loss_t : _} -> HasIO m => (Neg params_t, Show loss_t, Show params_t, Num params_t, CanBack params_t, CanBack loss_t, FromDouble params_t) => (iterations : Nat) -> (loss_node : Node params_t loss_t) -> (params : params_t) -> (learning_rate : Double) -> m params_t
gdn Z loss_node params alpha = pure params
gdn (S i) loss_node params alpha = do
  let (loss, params) = gd loss_node params alpha
  putStrLn $ "\{show i}: loss: \{show loss}"
  gdn i loss_node params alpha

main : IO ()
main = do
  putStrLn "begin"
  let x = the (T [_, _] Double) $ [[0, 0], [0, 1], [1, 0], [1, 1]]
  let y' = the (T [_, _] Double) $ [[0], [1], [1], [0]]
  params <- pure $ MkParams (MkDense !rand_m !rand_v) (MkDense !rand_m !rand_v)
  params <- gdn 100 (loss (model input (const x)) (const y')) params pi
  printLn "done"


text:
module Replica.App.Run.Dependencies

import Data.List
import Data.String

import Replica.Core.Types

%default total

public export
record TestPlan where
  constructor Plan
  now : List Test
  later : List Test
  skipped : List (String, Test)

export
displayPlan : TestPlan -> String
displayPlan x = unlines
  [ "Plan:"
  , "  Now: \{show $ map name x.now}"
  , "  Later: \{show $ map name x.later}"
  , "  Skipped: \{show $ map (name . snd) x.skipped}"]

public export
isReady : Test -> Bool
isReady = force . null . require

export
buildPlan : List Test -> TestPlan
buildPlan xs = let
  (now, later) = partition isReady xs
  in Plan now later []

export
validate : String -> TestPlan -> TestPlan
validate x y = let
  y' : TestPlan = record {later $= map (record {require $= filter (/= x)})} y
  (now', later') = partition isReady y'.later
  in record {now $= (++ now') . filter (not . (== x) . name), later = later'} y

export
fail : String -> TestPlan -> TestPlan
fail x y = let
  (skipped', later') = partition (elem x . require) y.later
  y' = record { now $= filter (not . (== x) . name)
              , later = later'
              , skipped $= (map (MkPair x) skipped' ++)} y
  in foldl (\tp, t => fail t.name $ assert_smaller y tp) y' skipped'

max_stars_repo_name: teto/REPLica

max_issues_repo_name: teto/REPLica

max_forks_repo_name: teto/REPLica


text:
module Types

import Logic

%access public export

%default total

data Tm : Type where
  Tru : Tm
  Fls : Tm
  Test : Tm -> Tm -> Tm -> Tm
  Zro : Tm
  Scc : Tm -> Tm
  Prd : Tm -> Tm
  IsZro : Tm -> Tm

data BValue : Tm -> Type where
  BV_Tru : BValue Tru
  BV_Fls : BValue Fls

data NValue : Tm -> Type where
  NV_Zro : NValue Zro
  NV_Scc : NValue t -> NValue (Scc t)

Value : (t : Tm) -> Type
Value t = Either (BValue t) (NValue t)

data Step : Tm -> Tm -> Type where
  ST_TestTru : Step (Test Tru t1 t2) t1
  ST_TestFls : Step (Test Fls t1 t2) t2
  ST_Test : Step t1 t1' -> Step (Test t1 t2 t3) (Test t1' t2 t3)
  ST_Scc : Step t1 t1' -> Step (Scc t1) (Scc t1')
  ST_PrdZro : Step (Prd Zro) Zro
  ST_PrdScc : NValue t1 -> Step (Prd (Scc t1)) t1
  ST_Prd : Step t1 t1' -> Step (Prd t1) (Prd t1')
  ST_IsZroZro : Step (IsZro Zro) Tru
  ST_IsZroScc : NValue t1 -> Step (IsZro (Scc t1)) Fls
  ST_IsZro : Step t1 t1' -> Step (IsZro t1) (IsZro t1')

Uninhabited (Step Tru _) where
  uninhabited ST_TestTru impossible
  uninhabited ST_TestFls impossible
  uninhabited (ST_Test _) impossible
  uninhabited (ST_Scc _) impossible
  uninhabited ST_PrdZro impossible
  uninhabited (ST_PrdScc _) impossible
  uninhabited (ST_Prd _) impossible
  uninhabited ST_IsZroZro impossible
  uninhabited (ST_IsZroScc _) impossible
  uninhabited (ST_IsZro _) impossible

Uninhabited (Step Fls _) where
  uninhabited ST_TestTru impossible
  uninhabited ST_TestFls impossible
  uninhabited (ST_Test _) impossible
  uninhabited (ST_Scc _) impossible
  uninhabited ST_PrdZro impossible
  uninhabited (ST_PrdScc _) impossible
  uninhabited (ST_Prd _) impossible
  uninhabited ST_IsZroZro impossible
  uninhabited (ST_IsZroScc _) impossible
  uninhabited (ST_IsZro _) impossible

Uninhabited (Step Zro _) where
  uninhabited ST_TestTru impossible
  uninhabited ST_TestFls impossible
  uninhabited (ST_Test _) impossible
  uninhabited (ST_Scc _) impossible
  uninhabited ST_PrdZro impossible
  uninhabited (ST_PrdScc _) impossible
  uninhabited (ST_Prd _) impossible
  uninhabited ST_IsZroZro impossible
  uninhabited (ST_IsZroScc _) impossible
  uninhabited (ST_IsZro _) impossible

infix 4 -+>

(-+>) : Tm -> Tm -> Type
(-+>) = Step

StepNormalForm : Tm -> Type
StepNormalForm = NormalForm Step

Stuck : (t : Tm) -> Type
Stuck t = (StepNormalForm t, Not (Value t))

some_term_is_stuck : (t : Tm ** Stuck t)
some_term_is_stuck = (IsZro Tru ** ( \(_ ** s) => case s of
                                       ST_IsZro ST_TestTru impossible
                                       ST_IsZro ST_TestFls impossible
                                       ST_IsZro (ST_Test _) impossible
                                       ST_IsZro (ST_Scc _) impossible
                                       ST_IsZro ST_PrdZro impossible
                                       ST_IsZro (ST_PrdScc _) impossible
                                       ST_IsZro (ST_Prd _) impossible
                                       ST_IsZro ST_IsZroZro impossible
                                       ST_IsZro (ST_IsZroScc _) impossible
                                       ST_IsZro (ST_IsZro _) impossible
                                   , \e => case e of
                                       Left BV_Tru impossible
                                       Left BV_Fls impossible
                                       Right NV_Zro impossible
                                       Right (NV_Scc _) impossible ))

value_is_nf : Value t -> StepNormalForm t
value_is_nf (Left BV_Tru) (_ ** s) = absurd s
value_is_nf (Left BV_Fls) (_ ** s) = absurd s
value_is_nf (Right NV_Zro) (_ ** s) = absurd s
value_is_nf (Right (NV_Scc nv)) (Scc t' ** ST_Scc s) =
  value_is_nf (Right nv) (t' ** s)

step_deterministic : Step x y1 -> Step x y2 -> y1 = y2
step_deterministic ST_TestTru ST_TestTru = Refl
step_deterministic ST_TestTru (ST_Test s) = absurd s
step_deterministic ST_TestFls ST_TestFls = Refl
step_deterministic ST_TestFls (ST_Test s) = absurd s
step_deterministic (ST_Test s) ST_TestTru = absurd s
step_deterministic (ST_Test s) ST_TestFls = absurd s
step_deterministic (ST_Test s1) (ST_Test s2) =
  rewrite step_deterministic s1 s2 in Refl
step_deterministic (ST_Scc s1) (ST_Scc s2) =
  rewrite step_deterministic s1 s2 in Refl
step_deterministic ST_PrdZro ST_PrdZro = Refl
step_deterministic ST_PrdZro (ST_Prd s) = absurd s
step_deterministic (ST_PrdScc _) (ST_PrdScc _) = Refl
step_deterministic (ST_PrdScc v) (ST_Prd (ST_Scc {t1'} s)) =
  absurd (value_is_nf (Right v) (t1' ** s))
step_deterministic (ST_Prd s) ST_PrdZro = absurd s
step_deterministic (ST_Prd (ST_Scc {t1'} s)) (ST_PrdScc v) =
  absurd (value_is_nf (Right v) (t1' ** s))
step_deterministic (ST_Prd s1) (ST_Prd s2) =
  rewrite step_deterministic s1 s2 in Refl
step_deterministic ST_IsZroZro ST_IsZroZro = Refl
step_deterministic ST_IsZroZro (ST_IsZro s) = absurd s
step_deterministic (ST_IsZroScc _) (ST_IsZroScc _) = Refl
step_deterministic (ST_IsZroScc v) (ST_IsZro (ST_Scc {t1'} s)) =
  absurd (value_is_nf (Right v) (t1' ** s))
step_deterministic (ST_IsZro s) ST_IsZroZro = absurd s
step_deterministic (ST_IsZro (ST_Scc {t1'} s)) (ST_IsZroScc v) =
  absurd (value_is_nf (Right v) (t1' ** s))
step_deterministic (ST_IsZro s1) (ST_IsZro s2) =
  rewrite step_deterministic s1 s2 in Refl

data Ty : Type where
  TyBool : Ty
  TyNat : Ty

data HasType : Tm -> Ty -> Type where
  T_Tru : Tru `HasType` TyBool
  T_Fls : Fls `HasType` TyBool
  T_Test : t1 `HasType` TyBool -> t2 `HasType` ty -> t3 `HasType` ty ->
           Test t1 t2 t3 `HasType` ty
  T_Zro : Zro `HasType` TyNat
  T_Scc : t `HasType` TyNat -> Scc t `HasType` TyNat
  T_Prd : t `HasType` TyNat -> Prd t `HasType` TyNat
  T_IsZro : t `HasType` TyNat -> IsZro t `HasType` TyBool

Uninhabited (Zro `HasType` TyBool) where
  uninhabited T_Tru impossible
  uninhabited T_Fls impossible
  uninhabited (T_Test _ _ _) impossible
  uninhabited T_Zro impossible
  uninhabited (T_Scc _) impossible
  uninhabited (T_Prd _) impossible
  uninhabited (T_IsZro _) impossible

Uninhabited (Scc _ `HasType` TyBool) where
  uninhabited T_Tru impossible
  uninhabited T_Fls impossible
  uninhabited (T_Test _ _ _) impossible
  uninhabited T_Zro impossible
  uninhabited (T_Scc _) impossible
  uninhabited (T_Prd _) impossible
  uninhabited (T_IsZro _) impossible

Uninhabited (Tru `HasType` TyNat) where
  uninhabited T_Tru impossible
  uninhabited T_Fls impossible
  uninhabited (T_Test _ _ _) impossible
  uninhabited T_Zro impossible
  uninhabited (T_Scc _) impossible
  uninhabited (T_Prd _) impossible
  uninhabited (T_IsZro _) impossible

Uninhabited (Fls `HasType` TyNat) where
  uninhabited T_Tru impossible
  uninhabited T_Fls impossible
  uninhabited (T_Test _ _ _) impossible
  uninhabited T_Zro impossible
  uninhabited (T_Scc _) impossible
  uninhabited (T_Prd _) impossible
  uninhabited (T_IsZro _) impossible

has_type_1 : Test Fls Zro (Scc Zro) `HasType` TyNat
has_type_1 = T_Test T_Fls T_Zro (T_Scc T_Zro)

has_type_not : Not (Test Fls Zro Tru `HasType` TyBool)
has_type_not (T_Test _ T_Tru _) impossible
has_type_not (T_Test _ T_Fls _) impossible
has_type_not (T_Test _ (T_Test _ _ _) _) impossible
has_type_not (T_Test _ T_Zro _) impossible
has_type_not (T_Test _ (T_Scc _) _) impossible
has_type_not (T_Test _ (T_Prd _) _) impossible
has_type_not (T_Test _ (T_IsZro _) _) impossible

scc_hastype_nat__hastype_nat : Scc t `HasType` TyNat -> t `HasType` TyNat
scc_hastype_nat__hastype_nat (T_Scc ty) = ty

bool_cannonical : t `HasType` TyBool -> Value t -> BValue t
bool_cannonical _ (Left bv) = bv
bool_cannonical ty (Right NV_Zro) = absurd ty
bool_cannonical ty (Right (NV_Scc _)) = absurd ty

nat_cannonical : t `HasType` TyNat -> Value t -> NValue t
nat_cannonical ty (Left BV_Tru) = absurd ty
nat_cannonical ty (Left BV_Fls) = absurd ty
nat_cannonical _ (Right bv) = bv

progress : t `HasType` ty -> Either (Value t) (t' ** t -+> t')
progress T_Tru = Left (Left BV_Tru)
progress T_Fls = Left (Left BV_Fls)
progress (T_Test {t2} {t3} ty1 ty2 ty3) = case progress ty1 of
  Left v => case bool_cannonical ty1 v of
    BV_Tru => Right (t2 ** ST_TestTru)
    BV_Fls => Right (t3 ** ST_TestFls)
  Right (t' ** s) => Right (Test t' t2 t3 ** ST_Test s)
progress T_Zro = Left (Right NV_Zro)
progress (T_Scc ty) = case progress ty of
  Left v => Left (Right (NV_Scc (nat_cannonical ty v)))
  Right (t' ** s) => Right (Scc t' ** ST_Scc s)
progress (T_Prd ty) = case progress ty of
  Left v => case nat_cannonical ty v of
    NV_Zro => Right (Zro ** ST_PrdZro)
    NV_Scc {t} nv => Right (t ** ST_PrdScc nv)
  Right (t' ** s) => Right (Prd t' ** ST_Prd s)
progress (T_IsZro ty) = case progress ty of
  Left v => case nat_cannonical ty v of
    NV_Zro => Right (Tru ** ST_IsZroZro)
    NV_Scc nv => Right (Fls ** ST_IsZroScc nv)
  Right (t' ** s) => Right (IsZro t' ** ST_IsZro s)

preservation : t `HasType` ty -> t -+> t' -> t' `HasType` ty
preservation T_Tru s = absurd s
preservation T_Fls s = absurd s
preservation (T_Test _ ty2 _) ST_TestTru = ty2
preservation (T_Test _ _ ty3) ST_TestFls = ty3
preservation (T_Test ty1 ty2 ty3) (ST_Test s) =
  T_Test (preservation ty1 s) ty2 ty3
preservation T_Zro s = absurd s
preservation (T_Scc ty) (ST_Scc s) = T_Scc (preservation ty s)
preservation (T_Prd ty) ST_PrdZro = ty
preservation (T_Prd (T_Scc ty)) (ST_PrdScc _) = ty
preservation (T_Prd ty) (ST_Prd s) = T_Prd (preservation ty s)
preservation (T_IsZro _) ST_IsZroZro = T_Tru
preservation (T_IsZro _) (ST_IsZroScc _) = T_Fls
preservation (T_IsZro ty) (ST_IsZro s) = T_IsZro (preservation ty s)

MultiStep : Relation Tm
MultiStep = Multi Step

infix 4 -+>*

(-+>*) : Relation Tm
(-+>*) = MultiStep

soundness : t `HasType` ty -> t -+>* t' -> Not (Stuck t')
soundness ht MultiRefl = case progress ht of
  Left v => \(_, p) => p v
  Right p => \(nf, _) => nf p
soundness ht (MultiStep once next) = soundness (preservation ht once) next

nvalue_hastype_nat : NValue t -> t `HasType` TyNat
nvalue_hastype_nat NV_Zro = T_Zro
nvalue_hastype_nat (NV_Scc v) = T_Scc (nvalue_hastype_nat v)

subject_expansion : (  t : Tm ** t' : Tm ** ty : Ty
                    ** (t -+> t', t' `HasType` ty, Not (t `HasType` ty)))
subject_expansion = (  Test Tru Zro Tru ** Zro ** TyNat
                    ** (ST_TestTru, T_Zro, \ty => case ty of
                                             T_Test _ _ ty3 => absurd ty3))


text:
module Toolkit.Data.List.Size

public export
data Size : List a -> Nat -> Type where
  Zero    : Size Nil Z
  PlusOne : Size       rest     k
         -> Size (e :: rest) (S k)

export
size' : (xs : List a) -> DPair Nat (Size xs)
size' [] = MkDPair Z Zero
size' (x :: xs) with (size' xs)
  size' (x :: xs) | (MkDPair k rest) = MkDPair (S k) (PlusOne rest)

export
size : (xs : List a) -> Size xs (length xs)
size [] = Zero
size (x :: xs) = PlusOne (size xs)

Uninhabited (Size Nil (S x)) where
  uninhabited Zero impossible
  uninhabited (PlusOne x) impossible

Uninhabited (Size (x::xs) Z) where
  uninhabited Zero impossible
  uninhabited (PlusOne x) impossible

export
hasSize : (xs : List a) -> (d : Nat) -> Dec (Size xs d)
hasSize xs d with (xs)
  hasSize xs 0 | [] = Yes Zero
  hasSize xs (S k) | [] = No absurd

  hasSize xs 0 | (x :: ys) = No absurd
  hasSize xs (S k) | (x :: ys) with (hasSize ys k)
    hasSize xs (S k) | (x :: ys) | (Yes prf) = Yes (PlusOne prf)
    hasSize xs (S k) | (x :: ys) | (No contra) = No (\(PlusOne y) => contra y)

-- [ EOF ]

max_stars_repo_name: gallais/linear-circuits

max_issues_repo_name: gallais/linear-circuits

max_forks_repo_name: gallais/linear-circuits


text:
module CUtils

import public System.FFI

libcutils : String -> String
libcutils x = "C:" <+> x <+> ",libidris2_cutils.so"

export
read_cstring : Ptr String -> String
read_cstring = prim__getString

export
nullanyptr : AnyPtr
nullanyptr = prim__getNullAnyPtr

export
remember : AnyPtr -> Ptr a
remember = prim__castPtr

export
nullptr : Ptr a
nullptr = remember nullanyptr

export
forget : Ptr a -> AnyPtr
forget = prim__forgetPtr

export
is_null : Ptr a -> Bool
is_null ptr = prim__nullPtr ptr > 0

export
cast : Ptr a -> Ptr b
cast = remember . forget

export
%foreign libcutils "sizeof_ptr"
sizeof_ptr : Int

export
%foreign libcutils "join_ptr"
prim__join_ptr : AnyPtr -> PrimIO AnyPtr

export
join_ptr : HasIO m => Ptr (Ptr a) -> m (Ptr a)
join_ptr ptr = do
  x <- primIO $ prim__join_ptr (forget ptr)
  pure $ remember x


text:
-- Was used for trying out graphics

record Circle where
    constructor MkCircle
    x, y, r : Int

record CircleMove where
    constructor MkCircleMove
    dx, dy : Int

updateCircle : Eff ()
    [ 'Circle     ::: STATE Circle
    , 'CircleMove ::: STATE CircleMove
    ]
updateCircle = do
    circle     <- 'Circle     :- get
    circleMove <- 'CircleMove :- get
    let (newCircle, newCircleMove) = moveCircle circle circleMove
    'Circle     :- put newCircle
    'CircleMove :- put newCircleMove
  where
    moveCircle : Circle -> CircleMove -> (Circle, CircleMove)
    moveCircle circle circleMove =
        let newCircle@(MkCircle cx cy cr) = record
                { x $= (+ dx circleMove)
                , y $= (+ dy circleMove)
                } circle
            newCircleMove = record
                { dx $= if cx < cr || cx > 640 - cr then (0 -) else (0 +)
                , dy $= if cy < cr || cy > 480 - cr then (0 -) else (0 +)
                } circleMove
        in (newCircle, newCircleMove)

max_stars_repo_name: artemohanjanyan/game-of-life

max_issues_repo_name: artemohanjanyan/game-of-life

max_forks_repo_name: artemohanjanyan/game-of-life


text:
module Parser.Lexer.Source

import public Parser.Lexer.Common

import Data.List1
import Data.List
import Data.Strings
import Data.String.Extra
import public Text.Bounded
import Text.PrettyPrint.Prettyprinter
import Text.PrettyPrint.Prettyprinter.Util

import Utils.Hex
import Utils.Octal
import Utils.String

import Core.Name

%default total

public export
data Token
  -- Literals
  = CharLit String
  | DoubleLit Double
  | IntegerLit Integer
  | StringLit String
  -- Identifiers
  | HoleIdent String
  | Ident String
  | DotSepIdent Namespace String -- ident.ident
  | DotIdent String               -- .ident
  | Symbol String
  -- Comments
  | Comment String
  | DocComment String
  -- Special
  | CGDirective String
  | EndInput
  | Keyword String
  | Pragma String
  | Unrecognised String

export
Show Token where
  -- Literals
  show (CharLit x) = "character " ++ show x
  show (DoubleLit x) = "double " ++ show x
  show (IntegerLit x) = "literal " ++ show x
  show (StringLit x) = "string " ++ show x
  -- Identifiers
  show (HoleIdent x) = "hole identifier " ++ x
  show (Ident x) = "identifier " ++ x
  show (DotSepIdent ns n) = "namespaced identifier " ++ show ns ++ "." ++ show n
  show (DotIdent x) = "dot+identifier " ++ x
  show (Symbol x) = "symbol " ++ x
  -- Comments
  show (Comment _) = "comment"
  show (DocComment c) = "doc comment: \"" ++ c ++ "\""
  -- Special
  show (CGDirective x) = "CGDirective " ++ x
  show EndInput = "end of input"
  show (Keyword x) = x
  show (Pragma x) = "pragma " ++ x
  show (Unrecognised x) = "Unrecognised " ++ x

export
Pretty Token where
  -- Literals
  pretty (CharLit x) = pretty "character" <++> squotes (pretty x)
  pretty (DoubleLit x) = pretty "double" <++> pretty x
  pretty (IntegerLit x) = pretty "literal" <++> pretty x
  pretty (StringLit x) = pretty "string" <++> dquotes (pretty x)
  -- Identifiers
  pretty (HoleIdent x) = reflow "hole identifier" <++> pretty x
  pretty (Ident x) = pretty "identifier" <++> pretty x
  pretty (DotSepIdent ns n) = reflow "namespaced identifier" <++> pretty ns <+> dot <+> pretty n
  pretty (DotIdent x) = pretty "dot+identifier" <++> pretty x
  pretty (Symbol x) = pretty "symbol" <++> pretty x
  -- Comments
  pretty (Comment _) = pretty "comment"
  pretty (DocComment c) = reflow "doc comment:" <++> dquotes (pretty c)
  -- Special
  pretty (CGDirective x) = pretty "CGDirective" <++> pretty x
  pretty EndInput = reflow "end of input"
  pretty (Keyword x) = pretty x
  pretty (Pragma x) = pretty "pragma" <++> pretty x
  pretty (Unrecognised x) = pretty "Unrecognised" <++> pretty x

mutual
  ||| The mutually defined functions represent different states in a
  ||| small automaton.
  ||| `toEndComment` is the default state and it will munch through
  ||| the input until we detect a special character (a dash, an
  ||| opening brace, or a double quote) and then switch to the
  ||| appropriate state.
  toEndComment : (k : Nat) -> Recognise (k /= 0)
  toEndComment Z = empty
  toEndComment (S k)
               = some (pred (\c => c /= '-' && c /= '{' && c /= '"'))
                        <+> toEndComment (S k)
             <|> is '{' <+> singleBrace k
             <|> is '-' <+> singleDash k
             <|> stringLit <+> toEndComment (S k)

  ||| After reading a single brace, we may either finish reading an
  ||| opening delimiter or ignore it (e.g. it could be an implicit
  ||| binder).
  singleBrace : (k : Nat) -> Lexer
  singleBrace k
     =  is '-' <+> many (is '-')    -- opening delimiter
               <+> singleDash (S k) -- handles the {----} special case
    <|> toEndComment (S k)          -- not a valid comment

  ||| After reading a single dash, we may either find another one,
  ||| meaning we may have started reading a line comment, or find
  ||| a closing brace meaning we have found a closing delimiter.
  singleDash : (k : Nat) -> Lexer
  singleDash k
     =  is '-' <+> doubleDash k    -- comment or closing delimiter
    <|> is '}' <+> toEndComment k  -- closing delimiter
    <|> toEndComment (S k)         -- not a valid comment

  ||| After reading a double dash, we are potentially reading a line
  ||| comment unless the series of uninterrupted dashes is ended with
  ||| a closing brace in which case it is a closing delimiter.
  doubleDash : (k : Nat) -> Lexer
  doubleDash k = many (is '-') <+> choice            -- absorb all dashes
    [ is '}' <+> toEndComment k                      -- closing delimiter
    , many (isNot '\n') <+> toEndComment (S k)       -- line comment
    ]

blockComment : Lexer
blockComment = is '{' <+> is '-' <+> toEndComment 1

docComment : Lexer
docComment = is '|' <+> is '|' <+> is '|' <+> many (isNot '\n')

holeIdent : Lexer
holeIdent = is '?' <+> identNormal

dotIdent : Lexer
dotIdent = is '.' <+> identNormal

pragma : Lexer
pragma = is '%' <+> identNormal

doubleLit : Lexer
doubleLit
    = digits <+> is '.' <+> digits <+> opt
           (is 'e' <+> opt (is '-' <|> is '+') <+> digits)

-- Do this as an entire token, because the contents will be processed by
-- a specific back end
cgDirective : Lexer
cgDirective
    = exact "%cg" <+>
      ((some space <+>
           some (pred isAlphaNum) <+> many space <+>
           is '{' <+> many (isNot '}') <+>
           is '}')
         <|> many (isNot '\n'))

mkDirective : String -> Token
mkDirective str = CGDirective (trim (substr 3 (length str) str))

-- Reserved words
keywords : List String
keywords = ["data", "module", "where", "let", "in", "do", "record",
            "auto", "default", "implicit", "mutual", "namespace",
            "parameters", "with", "impossible", "case", "of",
            "if", "then", "else", "forall", "rewrite",
            "using", "interface", "implementation", "open", "import",
            "public", "export", "private",
            "infixl", "infixr", "infix", "prefix",
            "total", "partial", "covering"]

-- Reserved words for internal syntax
special : List String
special = ["%lam", "%pi", "%imppi", "%let"]

-- Special symbols - things which can't be a prefix of another symbol, and
-- don't match 'validSymbol'
export
symbols : List String
symbols
    = [".(", -- for things such as Foo.Bar.(+)
       "@{",
       "[|", "|]",
       "(", ")", "{", "}}", "}", "[", "]", ",", ";", "_",
       "`(", "`{{", "`[", "`"]

export
isOpChar : Char -> Bool
isOpChar c = c `elem` (unpack ":!#$%&*+./<=>?@\\^|-~")

validSymbol : Lexer
validSymbol = some (pred isOpChar)

-- Valid symbols which have a special meaning so can't be operators
export
reservedSymbols : List String
reservedSymbols
    = symbols ++
      ["%", "\\", ":", "=", "|", "|||", "<-", "->", "=>", "?", "!",
       "&", "**", "..", "~"]

fromBinLit : String -> Integer
fromBinLit str
    = if length str <= 2
         then 0
         else let num = assert_total (strTail (strTail str)) in
                fromBin . reverse . map castBin . unpack $ num
    where
      castBin : Char -> Integer
      castBin '1' = 1; castBin _ = 0 -- This can only be '1' and '0' once lexed
      fromBin : List Integer -> Integer
      fromBin [] = 0
      fromBin (0 :: xs) = 2 * fromBin xs
      fromBin (1 :: xs) = 1 + (2 * fromBin xs)

fromHexLit : String -> Integer
fromHexLit str
  = if length str <= 2
       then 0
       else let num = assert_total (strTail (strTail str)) in
             case fromHex (reverse num) of
                  Nothing => 0 -- can't happen if the literal lexed correctly
                  Just n => cast n

fromOctLit : String -> Integer
fromOctLit str
  = if length str <= 2
       then 0
       else let num = assert_total (strTail (strTail str)) in
             case fromOct (reverse num) of
                  Nothing => 0 -- can't happen if the literal lexed correctly
                  Just n => cast n

rawTokens : TokenMap Token
rawTokens =
    [(comment, Comment),
     (blockComment, Comment),
     (docComment, DocComment . drop 3),
     (cgDirective, mkDirective),
     (holeIdent, \x => HoleIdent (assert_total (strTail x)))] ++
    map (\x => (exact x, Symbol)) symbols ++
    [(doubleLit, \x => DoubleLit (cast x)),
     (binLit, \x => IntegerLit (fromBinLit x)),
     (hexLit, \x => IntegerLit (fromHexLit x)),
     (octLit, \x => IntegerLit (fromOctLit x)),
     (digits, \x => IntegerLit (cast x)),
     (stringLit, \x => StringLit (stripQuotes x)),
     (charLit, \x => CharLit (stripQuotes x)),
     (dotIdent, \x => DotIdent (assert_total $ strTail x)),
     (namespacedIdent, parseNamespace),
     (identNormal, parseIdent),
     (pragma, \x => Pragma (assert_total $ strTail x)),
     (space, Comment),
     (validSymbol, Symbol),
     (symbol, Unrecognised)]
  where
    parseIdent : String -> Token
    parseIdent x = if x `elem` keywords then Keyword x
                   else Ident x
    parseNamespace : String -> Token
    parseNamespace ns = case mkNamespacedIdent ns of
                             (Nothing, ident) => parseIdent ident
                             (Just ns, n)     => DotSepIdent ns n

export
lexTo : (WithBounds Token -> Bool) ->
        String -> Either (Int, Int, String) (List (WithBounds Token))
lexTo pred str
    = case lexTo pred rawTokens str of
           -- Add the EndInput token so that we'll have a line and column
           -- number to read when storing spans in the file
           (tok, (l, c, "")) => Right (filter notComment tok ++
                                      [MkBounded EndInput False l c l c])
           (_, fail) => Left fail
    where
      notComment : WithBounds Token -> Bool
      notComment t = case t.val of
                          Comment _ => False
                          _ => True

export
lex : String -> Either (Int, Int, String) (List (WithBounds Token))
lex = lexTo (const False)