AndrasKovacs

{-# language Strict, BangPatterns, LambdaCase, ViewPatterns, OverloadedStrings #-}
{-# options_ghc -Wincomplete-patterns #-}

-- NbE with case commutation for sum types.

import Data.Maybe
import Data.String

type Name = String

AndrasKovacs

-- flatparse: hackage 0.1.1.1

-- example: smaltt (demo for fast elaborator): switching from megaparsec to flatparse would speed up more than 2x overall

-- 1 year ago:
--   parsec     : ridiculously slow, CPS implementation
--   attoparsec : (resumable, CPS), "high-performance" data parsing, binary parsing, not language parsing
--     fringe, modern:
--        parsnip: (unpublished on hackage) (by Kmett, on github) : really the high-performance raw data parsing (not language parsing)

AndrasKovacs

-- Agda 2.6.1, stdlib 1.5

open import Relation.Binary.PropositionalEquality
  renaming (sym to infix 6 _⁻¹; cong to ap; trans to infixr 5 _◾_; subst to tr)
open import Function

coe : ∀{i}{A B : Set i} → A ≡ B → A → B
coe refl a = a

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