text:
module Prelude.Cast

import Builtin
import Prelude.Basics
import Prelude.Num
import Prelude.Types

%default total

-----------
-- CASTS --
-----------

-- Casts between primitives only here.  They might be lossy.

||| Interface for transforming an instance of a data type to another type.
public export
interface Cast from to where
  constructor MkCast
  ||| Perform a (potentially lossy!) cast operation.
  ||| @ orig The original type
  cast : (orig : from) -> to

export
Cast a a where
  cast = id

-- To String

export
Cast Int String where
  cast = prim__cast_IntString

export
Cast Integer String where
  cast = prim__cast_IntegerString

export
Cast Char String where
  cast = prim__cast_CharString

export
Cast Double String where
  cast = prim__cast_DoubleString

export
Cast Nat String where
  cast = cast . natToInteger

export
Cast Int8 String where
  cast = prim__cast_Int8String

export
Cast Int16 String where
  cast = prim__cast_Int16String

export
Cast Int32 String where
  cast = prim__cast_Int32String

export
Cast Int64 String where
  cast = prim__cast_Int64String

export
Cast Bits8 String where
  cast = prim__cast_Bits8String

export
Cast Bits16 String where
  cast = prim__cast_Bits16String

export
Cast Bits32 String where
  cast = prim__cast_Bits32String

export
Cast Bits64 String where
  cast = prim__cast_Bits64String

-- To Integer

export
Cast Int Integer where
  cast = prim__cast_IntInteger

export
Cast Char Integer where
  cast = prim__cast_CharInteger

export
Cast Double Integer where
  cast = prim__cast_DoubleInteger

export
Cast String Integer where
  cast = prim__cast_StringInteger

export
Cast Nat Integer where
  cast = natToInteger

export
Cast Bits8 Integer where
  cast = prim__cast_Bits8Integer

export
Cast Bits16 Integer where
  cast = prim__cast_Bits16Integer

export
Cast Bits32 Integer where
  cast = prim__cast_Bits32Integer

export
Cast Bits64 Integer where
  cast = prim__cast_Bits64Integer

export
Cast Int8 Integer where
  cast = prim__cast_Int8Integer

export
Cast Int16 Integer where
  cast = prim__cast_Int16Integer

export
Cast Int32 Integer where
  cast = prim__cast_Int32Integer

export
Cast Int64 Integer where
  cast = prim__cast_Int64Integer

-- To Int

export
Cast Integer Int where
  cast = prim__cast_IntegerInt

export
Cast Char Int where
  cast = prim__cast_CharInt

export
Cast Double Int where
  cast = prim__cast_DoubleInt

export
Cast String Int where
  cast = prim__cast_StringInt

export
Cast Nat Int where
  cast = fromInteger . natToInteger

export
Cast Bits8 Int where
  cast = prim__cast_Bits8Int

export
Cast Bits16 Int where
  cast = prim__cast_Bits16Int

export
Cast Bits32 Int where
  cast = prim__cast_Bits32Int

export
Cast Bits64 Int where
  cast = prim__cast_Bits64Int

export
Cast Int8 Int where
  cast = prim__cast_Int8Int

export
Cast Int16 Int where
  cast = prim__cast_Int16Int

export
Cast Int32 Int where
  cast = prim__cast_Int32Int

export
Cast Int64 Int where
  cast = prim__cast_Int64Int

-- To Char

export
Cast Int Char where
  cast = prim__cast_IntChar

export
Cast Integer Char where
  cast = prim__cast_IntegerChar

export
Cast Nat Char where
  cast = cast . natToInteger

export
Cast Bits8 Char where
  cast = prim__cast_Bits8Char

export
Cast Bits16 Char where
  cast = prim__cast_Bits16Char

export
Cast Bits32 Char where
  cast = prim__cast_Bits32Char

export
Cast Bits64 Char where
  cast = prim__cast_Bits64Char

export
Cast Int8 Char where
  cast = prim__cast_Int8Char

export
Cast Int16 Char where
  cast = prim__cast_Int16Char

export
Cast Int32 Char where
  cast = prim__cast_Int32Char

export
Cast Int64 Char where
  cast = prim__cast_Int64Char

-- To Double

export
Cast Int Double where
  cast = prim__cast_IntDouble

export
Cast Integer Double where
  cast = prim__cast_IntegerDouble

export
Cast String Double where
  cast = prim__cast_StringDouble

export
Cast Nat Double where
  cast = prim__cast_IntegerDouble . natToInteger

export
Cast Bits8 Double where
  cast = prim__cast_Bits8Double

export
Cast Bits16 Double where
  cast = prim__cast_Bits16Double

export
Cast Bits32 Double where
  cast = prim__cast_Bits32Double

export
Cast Bits64 Double where
  cast = prim__cast_Bits64Double

export
Cast Int8 Double where
  cast = prim__cast_Int8Double

export
Cast Int16 Double where
  cast = prim__cast_Int16Double

export
Cast Int32 Double where
  cast = prim__cast_Int32Double

export
Cast Int64 Double where
  cast = prim__cast_Int64Double

-- To Bits8

export
Cast Int Bits8 where
  cast = prim__cast_IntBits8

export
Cast Integer Bits8 where
  cast = prim__cast_IntegerBits8

export
Cast Bits16 Bits8 where
  cast = prim__cast_Bits16Bits8

export
Cast Bits32 Bits8 where
  cast = prim__cast_Bits32Bits8

export
Cast Bits64 Bits8 where
  cast = prim__cast_Bits64Bits8

export
Cast String Bits8 where
  cast = prim__cast_StringBits8

export
Cast Double Bits8 where
  cast = prim__cast_DoubleBits8

export
Cast Char Bits8 where
  cast = prim__cast_CharBits8

export
Cast Nat Bits8 where
  cast = cast . natToInteger

export
Cast Int8 Bits8 where
  cast = prim__cast_Int8Bits8

export
Cast Int16 Bits8 where
  cast = prim__cast_Int16Bits8

export
Cast Int32 Bits8 where
  cast = prim__cast_Int32Bits8

export
Cast Int64 Bits8 where
  cast = prim__cast_Int64Bits8

-- To Bits16

export
Cast Int Bits16 where
  cast = prim__cast_IntBits16

export
Cast Integer Bits16 where
  cast = prim__cast_IntegerBits16

export
Cast Bits8 Bits16 where
  cast = prim__cast_Bits8Bits16

export
Cast Bits32 Bits16 where
  cast = prim__cast_Bits32Bits16

export
Cast Bits64 Bits16 where
  cast = prim__cast_Bits64Bits16

export
Cast String Bits16 where
  cast = prim__cast_StringBits16

export
Cast Double Bits16 where
  cast = prim__cast_DoubleBits16

export
Cast Char Bits16 where
  cast = prim__cast_CharBits16

export
Cast Nat Bits16 where
  cast = cast . natToInteger

export
Cast Int8 Bits16 where
  cast = prim__cast_Int8Bits16

export
Cast Int16 Bits16 where
  cast = prim__cast_Int16Bits16

export
Cast Int32 Bits16 where
  cast = prim__cast_Int32Bits16

export
Cast Int64 Bits16 where
  cast = prim__cast_Int64Bits16

-- To Bits32

export
Cast Int Bits32 where
  cast = prim__cast_IntBits32

export
Cast Integer Bits32 where
  cast = prim__cast_IntegerBits32

export
Cast Bits8 Bits32 where
  cast = prim__cast_Bits8Bits32

export
Cast Bits16 Bits32 where
  cast = prim__cast_Bits16Bits32

export
Cast Bits64 Bits32 where
  cast = prim__cast_Bits64Bits32

export
Cast String Bits32 where
  cast = prim__cast_StringBits32

export
Cast Double Bits32 where
  cast = prim__cast_DoubleBits32

export
Cast Char Bits32 where
  cast = prim__cast_CharBits32

export
Cast Nat Bits32 where
  cast = cast . natToInteger

export
Cast Int8 Bits32 where
  cast = prim__cast_Int8Bits32

export
Cast Int16 Bits32 where
  cast = prim__cast_Int16Bits32

export
Cast Int32 Bits32 where
  cast = prim__cast_Int32Bits32

export
Cast Int64 Bits32 where
  cast = prim__cast_Int64Bits32

-- To Bits64

export
Cast Int Bits64 where
  cast = prim__cast_IntBits64

export
Cast Integer Bits64 where
  cast = prim__cast_IntegerBits64

export
Cast Bits8 Bits64 where
  cast = prim__cast_Bits8Bits64

export
Cast Bits16 Bits64 where
  cast = prim__cast_Bits16Bits64

export
Cast Bits32 Bits64 where
  cast = prim__cast_Bits32Bits64

export
Cast String Bits64 where
  cast = prim__cast_StringBits64

export
Cast Double Bits64 where
  cast = prim__cast_DoubleBits64

export
Cast Char Bits64 where
  cast = prim__cast_CharBits64

export
Cast Nat Bits64 where
  cast = cast . natToInteger

export
Cast Int8 Bits64 where
  cast = prim__cast_Int8Bits64

export
Cast Int16 Bits64 where
  cast = prim__cast_Int16Bits64

export
Cast Int32 Bits64 where
  cast = prim__cast_Int32Bits64

export
Cast Int64 Bits64 where
  cast = prim__cast_Int64Bits64

-- To Int8

export
Cast String Int8 where
  cast = prim__cast_StringInt8

export
Cast Double Int8 where
  cast = prim__cast_DoubleInt8

export
Cast Char Int8 where
  cast = prim__cast_CharInt8

export
Cast Int Int8 where
  cast = prim__cast_IntInt8

export
Cast Integer Int8 where
  cast = prim__cast_IntegerInt8

export
Cast Nat Int8 where
  cast = cast . natToInteger

export
Cast Bits8 Int8 where
  cast = prim__cast_Bits8Int8

export
Cast Bits16 Int8 where
  cast = prim__cast_Bits16Int8

export
Cast Bits32 Int8 where
  cast = prim__cast_Bits32Int8

export
Cast Bits64 Int8 where
  cast = prim__cast_Bits64Int8

export
Cast Int16 Int8 where
  cast = prim__cast_Int16Int8

export
Cast Int32 Int8 where
  cast = prim__cast_Int32Int8

export
Cast Int64 Int8 where
  cast = prim__cast_Int64Int8

-- To Int16

export
Cast String Int16 where
  cast = prim__cast_StringInt16

export
Cast Double Int16 where
  cast = prim__cast_DoubleInt16

export
Cast Char Int16 where
  cast = prim__cast_CharInt16

export
Cast Int Int16 where
  cast = prim__cast_IntInt16

export
Cast Integer Int16 where
  cast = prim__cast_IntegerInt16

export
Cast Nat Int16 where
  cast = cast . natToInteger

export
Cast Bits8 Int16 where
  cast = prim__cast_Bits8Int16

export
Cast Bits16 Int16 where
  cast = prim__cast_Bits16Int16

export
Cast Bits32 Int16 where
  cast = prim__cast_Bits32Int16

export
Cast Bits64 Int16 where
  cast = prim__cast_Bits64Int16

export
Cast Int8 Int16 where
  cast = prim__cast_Int8Int16

export
Cast Int32 Int16 where
  cast = prim__cast_Int32Int16

export
Cast Int64 Int16 where
  cast = prim__cast_Int64Int16

-- To Int32

export
Cast String Int32 where
  cast = prim__cast_StringInt32

export
Cast Double Int32 where
  cast = prim__cast_DoubleInt32

export
Cast Char Int32 where
  cast = prim__cast_CharInt32

export
Cast Int Int32 where
  cast = prim__cast_IntInt32

export
Cast Integer Int32 where
  cast = prim__cast_IntegerInt32

export
Cast Nat Int32 where
  cast = cast . natToInteger

export
Cast Bits8 Int32 where
  cast = prim__cast_Bits8Int32

export
Cast Bits16 Int32 where
  cast = prim__cast_Bits16Int32

export
Cast Bits32 Int32 where
  cast = prim__cast_Bits32Int32

export
Cast Bits64 Int32 where
  cast = prim__cast_Bits64Int32

export
Cast Int8 Int32 where
  cast = prim__cast_Int8Int32

export
Cast Int16 Int32 where
  cast = prim__cast_Int16Int32

export
Cast Int64 Int32 where
  cast = prim__cast_Int64Int32

-- To Int64

export
Cast String Int64 where
  cast = prim__cast_StringInt64

export
Cast Double Int64 where
  cast = prim__cast_DoubleInt64

export
Cast Char Int64 where
  cast = prim__cast_CharInt64

export
Cast Int Int64 where
  cast = prim__cast_IntInt64

export
Cast Integer Int64 where
  cast = prim__cast_IntegerInt64

export
Cast Nat Int64 where
  cast = cast . natToInteger

export
Cast Bits8 Int64 where
  cast = prim__cast_Bits8Int64

export
Cast Bits16 Int64 where
  cast = prim__cast_Bits16Int64

export
Cast Bits32 Int64 where
  cast = prim__cast_Bits32Int64

export
Cast Bits64 Int64 where
  cast = prim__cast_Bits64Int64

export
Cast Int8 Int64 where
  cast = prim__cast_Int8Int64

export
Cast Int16 Int64 where
  cast = prim__cast_Int16Int64

export
Cast Int32 Int64 where
  cast = prim__cast_Int32Int64

-- To Nat

export
Cast String Nat where
  cast = integerToNat . cast

export
Cast Double Nat where
  cast = integerToNat . cast

export
Cast Char Nat where
  cast = integerToNat . cast {to = Integer}

export
Cast Int Nat where
  cast = integerToNat . cast

export
Cast Integer Nat where
  cast = integerToNat

export
Cast Bits8 Nat where
  cast = integerToNat . cast {to = Integer}

export
Cast Bits16 Nat where
  cast = integerToNat . cast {to = Integer}

export
Cast Bits32 Nat where
  cast = integerToNat . cast {to = Integer}

export
Cast Bits64 Nat where
  cast = integerToNat . cast {to = Integer}

export
Cast Int8 Nat where
  cast = integerToNat . cast

export
Cast Int16 Nat where
  cast = integerToNat . cast

export
Cast Int32 Nat where
  cast = integerToNat . cast

export
Cast Int64 Nat where
  cast = integerToNat . cast


text:
module Main

import Test.Golden

%default covering

allTests : TestPool
allTests = MkTestPool []
  [ "test001", "test002"
  ]

main : IO ()
main = runner
  [ testPaths "effect" allTests
  ] where
    testPaths : String -> TestPool -> TestPool
    testPaths dir = record { testCases $= map ((dir ++ "/") ++) }

ext: idr


text:
module Data.List.Elem

import Decidable.Equality

%default total

--------------------------------------------------------------------------------
-- List membership proof
--------------------------------------------------------------------------------

||| A proof that some element is found in a list.
public export
data Elem : a -> List a -> Type where
     ||| A proof that the element is at the head of the list
     Here : Elem x (x :: xs)
     ||| A proof that the element is in the tail of the list
     There : Elem x xs -> Elem x (y :: xs)

export
Uninhabited (Here = There e) where
  uninhabited Refl impossible

export
Uninhabited (There e = Here) where
  uninhabited Refl impossible

export
thereInjective : {0 e1, e2 : Elem x xs} -> There e1 = There e2 -> e1 = e2
thereInjective Refl = Refl

export
DecEq (Elem x xs) where
  decEq Here Here = Yes Refl
  decEq Here (There later) = No absurd
  decEq (There later) Here = No absurd
  decEq (There this) (There that) with (decEq this that)
    decEq (There this) (There this) | Yes Refl  = Yes Refl
    decEq (There this) (There that) | No contra = No (contra . thereInjective)

export
Uninhabited (Elem {a} x []) where
  uninhabited Here impossible
  uninhabited (There p) impossible

||| An item not in the head and not in the tail is not in the list at all.
export
neitherHereNorThere : Not (x = y) -> Not (Elem x xs) -> Not (Elem x (y :: xs))
neitherHereNorThere xny _     Here        = xny Refl
neitherHereNorThere _   xnxs  (There xxs) = xnxs xxs

||| Check whether the given element is a member of the given list.
export
isElem : DecEq a => (x : a) -> (xs : List a) -> Dec (Elem x xs)
isElem x [] = No absurd
isElem x (y :: xs) with (decEq x y)
  isElem x (x :: xs) | Yes Refl = Yes Here
  isElem x (y :: xs) | No xny with (isElem x xs)
    isElem x (y :: xs) | No xny | Yes xxs = Yes (There xxs)
    isElem x (y :: xs) | No xny | No xnxs = No (neitherHereNorThere xny xnxs)

||| Remove the element at the given position.
public export
dropElem : (xs : List a) -> (p : Elem x xs) -> List a
dropElem (_ :: ys)  Here     = ys
dropElem (x :: ys) (There p) = x :: dropElem ys p

||| Erase the indices, returning the numeric position of the element
public export
elemToNat : Elem x xs -> Nat
elemToNat  Here     = Z
elemToNat (There p) = S (elemToNat p)

||| Find the element with a proof at a given position, if it is valid
public export
indexElem : Nat -> (xs : List a) -> Maybe (x ** Elem x xs)
indexElem  _    []        = Nothing
indexElem  Z    (y :: _)  = Just (y ** Here)
indexElem (S n) (_ :: ys) = map (\(x ** p) => (x ** There p)) (indexElem n ys)

||| Lift the membership proof to a mapped list
export
elemMap : (0 f : a -> b) -> Elem x xs -> Elem (f x) (map f xs)
elemMap f  Here      = Here
elemMap f (There el) = There $ elemMap f el


text:
import Data.Vect
import Data.Fin
import BoundedNat
import NatHelpers

%default total

Minion : Type

BoardSide : (size : Nat) -> Type
BoardSide size = Vect size (Maybe Minion)

data PlayerType = Fst | Snd

record PlayerHP where
  constructor MkPlayerHP
  maxHP : Nat
  armor : Nat
  bonusHP : Nat
  currentHitPoints : BoundedNat (maxHP + bonusHP)

dealDamage : (dmg : Nat) -> PlayerHP -> PlayerHP
dealDamage dmg (MkPlayerHP maxHP armor bonusHP currentHitPoints) =
  case subtract armor dmg of
       (Pos remainingArmor) => MkPlayerHP maxHP remainingArmor bonusHP currentHitPoints
       (Neg remainingDmg) => let diff = subtractBounded currentHitPoints remainingDmg in
                                 MkPlayerHP maxHP 0 bonusHP diff

InitialHP : (hp : Nat) -> PlayerHP
InitialHP hp = MkPlayerHP hp 0 0 (Val hp lteRightPlusZero)

regularHeal : (heal : Nat) -> PlayerHP -> PlayerHP
regularHeal heal (MkPlayerHP maxHP armor bonusHP currentHitPoints) =
  case boundedAdd currentHitPoints heal of
       Left overflow => MkPlayerHP maxHP armor bonusHP (Val maxHP (lteRightPlusNat maxHP))
       Right newHP => MkPlayerHP maxHP armor bonusHP newHP

alextrazaEffect : (newMax : Nat) -> PlayerHP -> PlayerHP
alextrazaEffect newMax (MkPlayerHP maxHP armor bonusHP currentHitPoints)  with (cmp newMax maxHP)
  -- new max is lower than the current max HP -> reduce the current amout of hp
  alextrazaEffect newMax (MkPlayerHP (newMax + (S y)) armor bonusHP currentHitPoints)  | (CmpLT y) =
    let upperBoundPrf = lteRightPlusLeft (lteRightPlusNat newMax) in
      MkPlayerHP (newMax + (S y)) armor bonusHP $ Val newMax upperBoundPrf
  -- new max is equal to the current max HP -> set current hp to max hp
  alextrazaEffect maxHP (MkPlayerHP maxHP armor bonusHP currentHitPoints)  | CmpEQ =
    MkPlayerHP maxHP armor bonusHP (Val maxHP $ lteRightPlusNat maxHP)
  -- new max is higher than current maxi HP -> keep max HP, add the extra amount of HP as bonus, set the current to bonus + max
  alextrazaEffect (maxHP + (S x)) (MkPlayerHP maxHP armor bonusHP currentHitPoints)  | (CmpGT x) =
    MkPlayerHP maxHP armor (S x) (Val (maxHP + (S x)) $ lteEq (maxHP + (S x)))

Card : Type

data Deck : (card : Type) -> Type where
  MkDeck : Vect n card -> Nat -> Deck card

-- Attempts to draw a card, returns the card and the new state of the deck.
-- Either the deck is empty and the overdraw count is returned, or the card is successfully drawn
drawCard : Deck card -> (Either Nat card, Deck card)
drawCard (MkDeck [] overDraw) = (Left (S overDraw), MkDeck [] (S overDraw))
drawCard (MkDeck (x :: xs) overDraw) = (Right x, MkDeck xs overDraw)

mutual

  record Player where
    constructor MkPlayer
    type : PlayerType
    hitPoints : PlayerHP
    heroPower : Hearthstone -> Hearthstone
    deck : Deck Card
    board : BoardSide 7

  record Hearthstone where
    constructor MkHearthstone
    turn : BoundedNat 50
    currentPlayer : Player
    opposingPlayer : Player


text:
module Determinism

import Step
import Term

%default total
%access export

stepDeterministic : {e1 : Term} -> {e2 : Term} -> {e3 : Term} ->
                    (Step e1 e2) -> (Step e1 e3) ->
                    e2 = e3
-- case split in the following order: (Step e1 e2), (Step e1 e3)
stepDeterministic (StApp1 st1) (StApp1 st2) =
  let ih = stepDeterministic st1 st2
  in congApp ih Refl
stepDeterministic (StApp1 st1) (StApp2 v2 st2) =
  absurd $ valueIrreducible _ v2 st1
stepDeterministic (StApp1 st1) (StBeta v2) impossible
--
stepDeterministic (StApp2 v1 _) (StApp1 st) =
  absurd $ valueIrreducible _ v1 st
stepDeterministic (StApp2 v1 st1) (StApp2 v2 st2) =
  let ih = stepDeterministic st1 st2
  in congApp Refl ih
stepDeterministic (StApp2 v1 st1) (StBeta v2) =
  absurd $ valueIrreducible _ v2 st1
--
stepDeterministic (StBeta v1) (StApp2 v2 st2) =
  absurd $ valueIrreducible _ v1 st2
stepDeterministic (StBeta v1) (StBeta _) = Refl

--
stepDeterministic (StRec st1) (StRec st2) =
  let ih = stepDeterministic st1 st2
  in congRec ih Refl Refl
stepDeterministic (StRec st1) StRecZero impossible
stepDeterministic (StRec st1) (StRecSucc v) =
  absurd $ valueIrreducible _ v st1
--
stepDeterministic StRecZero (StRec _) impossible
stepDeterministic StRecZero StRecZero = Refl
--
stepDeterministic (StRecSucc v) (StRec st) =
  absurd $ valueIrreducible _ v st
stepDeterministic (StRecSucc v) (StRecSucc _) = Refl
--
stepDeterministic (StSucc st1) (StSucc st2) =
  congSucc $ stepDeterministic st1 st2
--
stepDeterministic (StPred st1) (StPred st2) =
  congPred $ stepDeterministic st1 st2
stepDeterministic (StPred st1) StPredZero impossible
stepDeterministic (StPred st1) (StPredSucc v) =
  absurd $ valueIrreducible _ (VSucc v) st1
--
stepDeterministic StPredZero (StPred _) impossible
stepDeterministic StPredZero StPredZero = Refl
--
stepDeterministic (StPredSucc v1) (StPred st) =
  absurd $ valueIrreducible _ (VSucc v1) st
stepDeterministic (StPredSucc v1) (StPredSucc _) = Refl
--
stepDeterministic (StIfz st1) (StIfz st2) =
  let ih = stepDeterministic st1 st2
  in congIfz ih Refl Refl
stepDeterministic (StIfz st1) StIfzZero impossible
stepDeterministic (StIfz st1) (StIfzSucc v) =
  absurd $ valueIrreducible _ (VSucc v) st1
--
stepDeterministic StIfzZero (StIfz _) impossible
stepDeterministic StIfzZero StIfzZero = Refl
--
stepDeterministic (StIfzSucc v1) (StIfz st2) =
  absurd $ valueIrreducible _ (VSucc v1) st2
stepDeterministic (StIfzSucc v1) (StIfzSucc v2) = Refl

transStepDeterministic : (v2 : Value e2) -> (TransStep e1 e2) ->
                         (v3 : Value e3) -> (TransStep e1 e3) ->
                         e2 = e3
--
transStepDeterministic v2 (TStRefl e3) v3 (TStRefl e3) = Refl
--
transStepDeterministic v2 (TStRefl e2) v3 (TStTrans x y) =
  absurd $ valueIrreducible e2 v2 x
--
transStepDeterministic v2 (TStTrans x z) v3 (TStRefl e3) =
  absurd $ valueIrreducible e3 v3 x
--
transStepDeterministic {e2 = e2} v2 (TStTrans x z) v3 (TStTrans y w) =
  let eq = stepDeterministic x y
      z' = replace {P = \x => x} (cong {f = \e => TransStep e e2} eq) z
  in transStepDeterministic v2 z' v3 w

max_stars_repo_name: normanrink/PCF

max_issues_repo_name: normanrink/PCF

max_forks_repo_name: normanrink/PCF


text:
module Data.Compress.CRC

import Data.Compress.Utils.ConstantTable
import Data.Vect
import Data.Bits

crc_table : ConstantTable 256 Bits32
crc_table = from_vect
  [ 0x00000000, 0x77073096, 0xee0e612c, 0x990951ba, 0x076dc419, 0x706af48f
  , 0xe963a535, 0x9e6495a3, 0x0edb8832, 0x79dcb8a4, 0xe0d5e91e, 0x97d2d988
  , 0x09b64c2b, 0x7eb17cbd, 0xe7b82d07, 0x90bf1d91, 0x1db71064, 0x6ab020f2
  , 0xf3b97148, 0x84be41de, 0x1adad47d, 0x6ddde4eb, 0xf4d4b551, 0x83d385c7
  , 0x136c9856, 0x646ba8c0, 0xfd62f97a, 0x8a65c9ec, 0x14015c4f, 0x63066cd9
  , 0xfa0f3d63, 0x8d080df5, 0x3b6e20c8, 0x4c69105e, 0xd56041e4, 0xa2677172
  , 0x3c03e4d1, 0x4b04d447, 0xd20d85fd, 0xa50ab56b, 0x35b5a8fa, 0x42b2986c
  , 0xdbbbc9d6, 0xacbcf940, 0x32d86ce3, 0x45df5c75, 0xdcd60dcf, 0xabd13d59
  , 0x26d930ac, 0x51de003a, 0xc8d75180, 0xbfd06116, 0x21b4f4b5, 0x56b3c423
  , 0xcfba9599, 0xb8bda50f, 0x2802b89e, 0x5f058808, 0xc60cd9b2, 0xb10be924
  , 0x2f6f7c87, 0x58684c11, 0xc1611dab, 0xb6662d3d, 0x76dc4190, 0x01db7106
  , 0x98d220bc, 0xefd5102a, 0x71b18589, 0x06b6b51f, 0x9fbfe4a5, 0xe8b8d433
  , 0x7807c9a2, 0x0f00f934, 0x9609a88e, 0xe10e9818, 0x7f6a0dbb, 0x086d3d2d
  , 0x91646c97, 0xe6635c01, 0x6b6b51f4, 0x1c6c6162, 0x856530d8, 0xf262004e
  , 0x6c0695ed, 0x1b01a57b, 0x8208f4c1, 0xf50fc457, 0x65b0d9c6, 0x12b7e950
  , 0x8bbeb8ea, 0xfcb9887c, 0x62dd1ddf, 0x15da2d49, 0x8cd37cf3, 0xfbd44c65
  , 0x4db26158, 0x3ab551ce, 0xa3bc0074, 0xd4bb30e2, 0x4adfa541, 0x3dd895d7
  , 0xa4d1c46d, 0xd3d6f4fb, 0x4369e96a, 0x346ed9fc, 0xad678846, 0xda60b8d0
  , 0x44042d73, 0x33031de5, 0xaa0a4c5f, 0xdd0d7cc9, 0x5005713c, 0x270241aa
  , 0xbe0b1010, 0xc90c2086, 0x5768b525, 0x206f85b3, 0xb966d409, 0xce61e49f
  , 0x5edef90e, 0x29d9c998, 0xb0d09822, 0xc7d7a8b4, 0x59b33d17, 0x2eb40d81
  , 0xb7bd5c3b, 0xc0ba6cad, 0xedb88320, 0x9abfb3b6, 0x03b6e20c, 0x74b1d29a
  , 0xead54739, 0x9dd277af, 0x04db2615, 0x73dc1683, 0xe3630b12, 0x94643b84
  , 0x0d6d6a3e, 0x7a6a5aa8, 0xe40ecf0b, 0x9309ff9d, 0x0a00ae27, 0x7d079eb1
  , 0xf00f9344, 0x8708a3d2, 0x1e01f268, 0x6906c2fe, 0xf762575d, 0x806567cb
  , 0x196c3671, 0x6e6b06e7, 0xfed41b76, 0x89d32be0, 0x10da7a5a, 0x67dd4acc
  , 0xf9b9df6f, 0x8ebeeff9, 0x17b7be43, 0x60b08ed5, 0xd6d6a3e8, 0xa1d1937e
  , 0x38d8c2c4, 0x4fdff252, 0xd1bb67f1, 0xa6bc5767, 0x3fb506dd, 0x48b2364b
  , 0xd80d2bda, 0xaf0a1b4c, 0x36034af6, 0x41047a60, 0xdf60efc3, 0xa867df55
  , 0x316e8eef, 0x4669be79, 0xcb61b38c, 0xbc66831a, 0x256fd2a0, 0x5268e236
  , 0xcc0c7795, 0xbb0b4703, 0x220216b9, 0x5505262f, 0xc5ba3bbe, 0xb2bd0b28
  , 0x2bb45a92, 0x5cb36a04, 0xc2d7ffa7, 0xb5d0cf31, 0x2cd99e8b, 0x5bdeae1d
  , 0x9b64c2b0, 0xec63f226, 0x756aa39c, 0x026d930a, 0x9c0906a9, 0xeb0e363f
  , 0x72076785, 0x05005713, 0x95bf4a82, 0xe2b87a14, 0x7bb12bae, 0x0cb61b38
  , 0x92d28e9b, 0xe5d5be0d, 0x7cdcefb7, 0x0bdbdf21, 0x86d3d2d4, 0xf1d4e242
  , 0x68ddb3f8, 0x1fda836e, 0x81be16cd, 0xf6b9265b, 0x6fb077e1, 0x18b74777
  , 0x88085ae6, 0xff0f6a70, 0x66063bca, 0x11010b5c, 0x8f659eff, 0xf862ae69
  , 0x616bffd3, 0x166ccf45, 0xa00ae278, 0xd70dd2ee, 0x4e048354, 0x3903b3c2
  , 0xa7672661, 0xd06016f7, 0x4969474d, 0x3e6e77db, 0xaed16a4a, 0xd9d65adc
  , 0x40df0b66, 0x37d83bf0, 0xa9bcae53, 0xdebb9ec5, 0x47b2cf7f, 0x30b5ffe9
  , 0xbdbdf21c, 0xcabac28a, 0x53b39330, 0x24b4a3a6, 0xbad03605, 0xcdd70693
  , 0x54de5729, 0x23d967bf, 0xb3667a2e, 0xc4614ab8, 0x5d681b02, 0x2a6f2b94
  , 0xb40bbe37, 0xc30c8ea1, 0x5a05df1b, 0x2d02ef8d ]

export
update_crc32 : Bits32 -> List Bits8 -> Bits32
update_crc32 crc = complement . foldl (\crc,elem => xor (shiftR crc 8) (index_bits8 ((xor (cast crc) elem)) crc_table)) (complement crc)

export
crc32 : List Bits8 -> Bits32
crc32 = update_crc32 0


text:
import Data.List

data SplitList : List a -> Type where
     SplitNil : SplitList []
     SplitOne : SplitList [x]
     SplitPair : (lefts : List a) -> (rights : List a) ->
                 SplitList (lefts ++ rights)

total
splitList : (xs : List a) ->  SplitList xs
splitList xs = splitListHelp xs xs
  where
    splitListHelp : (counter : List a) -> (xs : List a) -> SplitList xs
    splitListHelp _ [] = SplitNil
    splitListHelp _ [x] = SplitOne
    splitListHelp (_ :: _ :: ys) (x :: xs)
       = case splitListHelp ys xs of
              SplitNil => SplitOne
              SplitOne {x=y} => SplitPair [x] [y]
              SplitPair lefts rights => SplitPair (x :: lefts) rights
    splitListHelp _ xs = SplitPair [] xs

mergeSort : Ord a => List a -> List a
mergeSort input with (splitList input)
  mergeSort [] | SplitNil = []
  mergeSort [x] | SplitOne = [x]
  mergeSort (lefts ++ rights) | (SplitPair lefts rights)
         = merge (mergeSort lefts) (mergeSort rights)


text:
module Main
import Data.Vect

import Poker.Hands
import Poker.Card
import Poker.InsertionSort
import Poker.Sorted
import Poker.ElemsAreSame

--=======================================================================================================
--=======================================================================================================
--Utility functions
--=======================================================================================================
--=======================================================================================================
parseCardValue: Char -> Either String Value
parseCardValue 'A' = Right Ace
parseCardValue 'K' = Right King
parseCardValue 'Q' = Right Queen
parseCardValue 'J' = Right Jack
parseCardValue '2' = Right (Pip 2)
parseCardValue '3' = Right (Pip 3)
parseCardValue '4' = Right (Pip 4)
parseCardValue '5' = Right (Pip 5)
parseCardValue '6' = Right (Pip 6)
parseCardValue '7' = Right (Pip 7)
parseCardValue '8' = Right (Pip 8)
parseCardValue '9' = Right (Pip 9)
parseCardValue 'T' = Right (Pip 10)
parseCardValue x = Left "Invalid value character"

parseCardSuit: Char -> Either String Suit
parseCardSuit 'C' = Right Clubs
parseCardSuit 'D' = Right Diamonds
parseCardSuit 'H' = Right Hearts
parseCardSuit 'S' = Right Spades
parseCardSuit x = Left "Invalid suit character"

||| Attempt to parse a single card description
parseCard: List Char -> Either String Card
parseCard [] = Left "Card description must be two characters"
parseCard (c1 :: c2 :: []) = (case parseCardValue c1 of
                                   (Left l) => Left l
                                   (Right value) => (case parseCardSuit c2 of
                                                      (Left l) => Left l
                                                      (Right suit) => Right (MkCard value suit) ))
parseCard xs = Left "Card description must be two characters"

parseHand': (input: List (List Char)) -> (aux: List Card) -> Either String (List Card)
parseHand' [] aux = Right aux
parseHand' (x :: xs) aux = case parseCard x of
                                (Left l) => Left l
                                (Right r) => parseHand' xs (r::aux)

parseHand: String -> Either String (Vect HAND_SIZE Card)
parseHand x = let unparsedCards = words' (unpack x) in
                (case parseHand' unparsedCards [] of
                     Left l => Left l
                     Right [x1, x2, x3, x4, x5] => Right [x1, x2, x3, x4, x5]
                     Right xs => Left "Wrong number of cards in hand")

parseEvalHand: String -> Either String (hand:(Vect HAND_SIZE Card) ** Hand hand)
parseEvalHand x = case parseHand x of
                       (Left l) => Left l
                       (Right r) => let (hand ** (sort_prf, elem_prf)) = insertSort r
                                        evaled = evalHand hand sort_prf in
                                        Right (hand ** evaled)
getHand: IO (Either String (hand:(Vect HAND_SIZE Card) ** Hand hand))
getHand = do
            putStrLn "Enter hand"
            cardsString <- getLine
            pure (parseEvalHand cardsString)

getComparison: IO ()
getComparison = do
      Right (h1 ** hand1) <- getHand | Left l => putStrLn l
      Right (h2 ** hand2) <- getHand | Left l => putStrLn l
      case compareHands hand1 hand2 of
          LT => putStrLn ("Player 2 wins with:" ++ (show hand2))
          EQ => putStrLn "Tie"
          GT => putStrLn ("Player 1 wins with:" ++ (show hand1))

main: IO ()
main = getComparison