justjoheinz

import shapeless._
import ops._
import coproduct._

object coproducttest {

  type U = Int :+: String :+: CNil

  type V = Double :+: List[Int] :+: CNil

justjoheinz

module Sandbox

import Data.Vect

||| zip to Vectors of the same size
||| using a proof that n=m
||| instead of zippy: Vect n e -> Vect n a -> Vect n (e,a)
zippy :  Vect n e -> Vect m a -> (n = m)-> Vect m (e,a)
zippy [] [] Refl = []
zippy  (x :: xs) (y :: ys) Refl =  (x, y) :: zippy xs ys Refl

justjoheinz

module Sandbox

import Data.Vect

||| zip to Vectors of the same size
||| using an implicit proof
||| instead of zippy: Vect n e -> Vect n a -> Vect n (e,a)
zippy :  Vect n e -> Vect m a -> {auto prf: n = m}-> Vect m (e,a)
zippy [] [] {prf} = []
zippy  (x :: xs) (y :: ys) {prf = Refl} =  (x, y) :: zippy xs ys

justjoheinz

module GCounter

import Data.Fin
import Data.Vect

||| GCounter is a Conflict Free Replicated Datatype.
||| For a definition, see https://en.wikipedia.org/wiki/Conflict-free_replicated_data_type
||| It provides update, query and merge operations.
||| merge is commutative, associative and idempotent.
data GCounter : Nat -> Type where

justjoheinz

import Data.Vect
import Data.Fin

%default total
%access public export

data Ty: Type where
    TyBool: Ty
    TyInt: Ty
    TyFun: Ty -> Ty -> Ty

justjoheinz

;; https://awkravchuk.itch.io/cl-fast-ecs/devlog/622054/gamedev-in-lisp-part-1-ecs-and-metalinguistic-abstraction
(in-package #:ecs_tutorial_sdl)

(define-constant +window-width+ 800)
(define-constant +window-height+ 600)

(define-constant +repl-update-interval+ 0.3d0)

(define-constant +font-path+ (namestring (asdf:system-relative-pathname :ecs_tutorial_sdl "Resources/inconsolata.ttf"))
  :test #'string=)