bitmappergit

{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE BlockArguments #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE OverloadedLabels #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE TypeApplications #-}

bitmappergit

module Huggable where

swap :: (a, b) -> (b, a)
swap (a, b) = (b, a)

newtype Star f a b = Star { runStar :: a -> f b }
newtype Forget r a b = Forget { runForget :: a -> r }

class Profunctor p where
  dimap :: (a -> b) -> (c -> d) -> p b c -> p a d

bitmappergit

{-# LANGUAGE RankNTypes
           , BlockArguments
           , GADTs
           , MultiParamTypeClasses
           , OverloadedLabels
           , DataKinds
           , PolyKinds
           , FunctionalDependencies
           , AllowAmbiguousTypes
           , TypeApplications

bitmappergit

#include <stdio.h>
#include <stdbool.h>
#include <stdlib.h>
#include <gc.h>

typedef enum {
  APP,
  CON,
  COMB,
} tag_t;

bitmappergit

module 📕 where

open import Agda.Primitive
  renaming (Set to 💯; lsuc to 👆; lzero to 🔴; Level to 🏢)

data _🤝_ {🤣 : 🏢} {🇦 : 💯 🤣} (🇽 : 🇦) : 🇦 → 💯 🤣 where
  ✅ : 🇽 🤝 🇽

infix 4 _🤝_

bitmappergit

{-# LANGUAGE RankNTypes, BlockArguments #-}

module Lens
  ( Lens
  , MonoLens
  , view
  , (...)
  , over
  , set
  , lens

bitmappergit

use std::convert::TryInto;
use std::io::{BufRead, Read, Write};
use std::process::exit;

const IMAGE_SIZE: usize = 242000;
const NUM_DEVICES: usize = 2;
const TIB: usize = 1471;

type Cell = i32;

bitmappergit

module Glue

import StdEnv

:: Name :== String

:: Term
  = Loc Name
  | Top Name
  | App Term Term

bitmappergit

#include <stdio.h>
#include <stdbool.h>
#include <stdlib.h>
#include <gc.h>

typedef enum {
  APP,
  CON,
  COMB,
} tag_t;

bitmappergit

(* based on https://gist.github.com/AndrasKovacs/a0e0938113b193d6b9c1c0620d853784 *)

type name = string

datatype term
  = Loc of name
  | Top of name
  | App of term * term
  | Let of name * term * term
  | Lam of name * term