andrevidela

extension Vector2D: Field {}

andrevidela

{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE ScopedTypeVariables#-}
{-# LANGUAGE TypeApplications#-}
{-# LANGUAGE TypeFamilies #-}

data ValueKind = First | Second deriving (Eq, Show)

andrevidela

atlantis-db/src/Atlantis/Database/Entities.hs:35:1: error:
    • No instance for (Read Hash)
        arising from the first field of ‘TransactionEntityKey’
          (type ‘Hash’)
      Possible fix:
        use a standalone 'deriving instance' declaration,
          so you can specify the instance context yourself
    • When deriving the instance for (Read (Key TransactionEntity))
   |
35 | share [mkPersist sqlSettings, mkMigrate "migrateTables"] [persistLowerCase|

andrevidela

atlantis-db/src/Atlantis/Database/Entities.hs:35:1: error:
    • No instance for (Read Hash)
        arising from the first field of ‘TransactionEntityKey’
          (type ‘Hash’)
      Possible fix:
        use a standalone 'deriving instance' declaration,
          so you can specify the instance context yourself
    • When deriving the instance for (Read (Key TransactionEntity))
   |
35 | share [mkPersist sqlSettings, mkMigrate "migrateTables"] [persistLowerCase|

andrevidela

%default total

data Prop = Var String 
          | Not Prop 
          | And Prop Prop 
          | Or Prop Prop 
          | Impl Prop Prop
          | Equiv Prop Prop

data Lit = Stmt String | Neg String

andrevidela

-- as long as there is a proof that a < b then we can build a Fin b
natToProvedFin : (n : Nat) -> (bound : Nat) -> {auto prf : LT n bound} -> Fin bound
natToProvedFin Z (S right) {prf=LTESucc x} = FZ
natToProvedFin (S k) (S right) {prf=LTESucc x} = FS $ natToProvedFin k right

record Numbers where
  constructor MkNumbers
  max : Nat
  bonus : Nat
  current : Fin (S (max + bonus))

andrevidela

mutual 
  
  tryGenOp : StackCmd () pre (S _) -> StackIO h
  tryGenOp x {pre} {h} = case decEq pre h of
                              (Yes Refl) => do x
                                               res <- Top
                                               PutStr (show res ++ "\n")
                                               stackCalc
                              (No contra) => do PutStr $ "not enough item on the stack, expected " ++

andrevidela

/// Partially applies the right argument of a binary function
func partialRightApply<A, B, C>(_ f: @escaping (A, B) -> C, arg rhs: B) -> (A) -> C {
    return {lhs in f(lhs, rhs)}
}

prefix operator >

prefix func > <T: Comparable>(rhs: T) -> (T) -> Bool {
    return partialRightApply(>, arg: rhs)
}

andrevidela

prefix operator ==

prefix func == <T: Equatable>(rhs: T) -> (T) -> Bool {
    return { lhs in lhs == rhs }
}

andrevidela

infix operator •

public func • <A, B, C>(f : @escaping (B) -> C, g : @escaping (A) -> B) -> (A) -> C {
    return { f(g($0)) }
}