AndrasKovacs

{-# OPTIONS --postfix-projections --without-K #-}

-- Notes for https://www.youtube.com/watch?v=RXKRepPm0ps

-- checked with Agda 2.6.1 + stdlib 1.5

open import Data.Product renaming (proj₁ to ₁; proj₂ to ₂)
open import Relation.Binary.PropositionalEquality
  renaming (subst to tr; sym to infix 6 _⁻¹; trans to infixr 5 _◾_; cong to ap)
open import Data.Nat

AndrasKovacs

{-

-- Compiler: staging, memory layout control, etc  (small + self-hosting + useful soon)

-- Surface language:
   1. CBV + side effects (ML)
   2. CBV + typed effect system:
        - Eff monad
        - Eff monad, row of effects
           f : Int -> Eff [IO, Exc e, MutRef a, MutRef b] Int

AndrasKovacs

-- solution to https://github.com/effectfully/haskell-challenges/blob/master/h3-transform-typed/README.md

{-# LANGUAGE GADTs #-}

module Lib where

import           Data.Proxy
import           Data.Typeable

data Scheme a where

AndrasKovacs

-- Solution to challenge: https://github.com/effectfully/haskell-challenges/tree/master/force-elems
-- (Spoiler)

data EC = Elem | Con
data T a = T {ec :: !EC, unT :: a}

appEC :: EC -> (a -> b) -> a -> b
appEC Elem f a = f $! a
appEC Con  f a = f a

AndrasKovacs

{-# OPTIONS --without-K #-}

open import Data.Bool
open import Data.Product
open import Relation.Binary.PropositionalEquality
open import Data.Empty
open import Function

surj : {A B : Set} → (A → B) → Set
surj f = ∀ b → ∃ λ a → f a ≡ b

AndrasKovacs

{-# OPTIONS --rewriting #-}

module cont-cwf where

open import Agda.Builtin.Sigma
open import Agda.Builtin.Unit
open import Agda.Builtin.Bool
open import Agda.Builtin.Nat
open import Data.Empty
open import Relation.Binary.PropositionalEquality public using (_≡_; refl; trans; subst; cong)

AndrasKovacs

{-# language Strict, LambdaCase, BlockArguments #-}
{-# options_ghc -Wincomplete-patterns #-}

{-
Minimal demo of "glued" evaluation in the style of Olle Fredriksson:

  https://github.com/ollef/sixty

The main idea is that during elaboration, we need different evaluation

AndrasKovacs

{-# language Strict, BangPatterns #-}

data Tm = Var Int | App Tm Tm | Lam Tm | Fix Tm deriving (Show, Eq)
data Val = VVar Int | VApp Val Val | VLam [Val] Tm | VFix [Val] Tm

isCanonical :: Val -> Bool
isCanonical VLam{} = True
isCanonical _      = False

eval :: [Val] -> Tm -> Val

AndrasKovacs

open import Data.Unit
open import Data.Product

infixr 4 _⇒_ _*_ ⟨_,_⟩ _∘_

data Obj : Set where
  ∙    : Obj
  base : Obj
  _*_  : Obj → Obj → Obj

AndrasKovacs

{-# language Strict, TypeApplications, ScopedTypeVariables,
    PartialTypeSignatures, ViewPatterns #-}
{-# options_ghc -Wno-partial-type-signatures #-}

import qualified Data.Primitive.PrimArray as A
import GHC.Exts (IsList(..))
import Data.Bits
import Data.Word
import Control.Monad.ST.Strict