phadej

cabal-version: 3.0
name: callback-exception
version: 0

executable problem
  build-depends: base
  include-dirs: include
  hs-source-dirs: src
  main-is: problem.hs

phadej

{-# LANGUAGE RankNTypes, ScopedTypeVariables #-}
{-# OPTIONS_GHC -Wall #-}
module Parts where

import Data.Kind

import Control.Applicative (liftA2)
import Data.Function

-- in blogs

phadej

module Staged where

open import Data.Nat using (ℕ; zero; suc)
open import Data.Empty using (⊥)
open import Relation.Binary.PropositionalEquality
open ≡-Reasoning

-- indices, we could open import Data.Fin renaming too.
-- probably should (so we get all the lemmas).
-- but for now it's defined inline.

phadej

Revision history for bug23034

0.1.0.0 -- YYYY-mm-dd

• First version. Released on an unsuspecting world.

phadej

{-# LANGUAGE ConstraintKinds       #-}
{-# LANGUAGE DeriveGeneric         #-}
{-# LANGUAGE FlexibleContexts      #-}
{-# LANGUAGE FlexibleInstances     #-}
{-# LANGUAGE GADTs                 #-}
{-# LANGUAGE KindSignatures        #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE RankNTypes            #-}
{-# LANGUAGE TypeApplications      #-}
{-# LANGUAGE TypeOperators         #-}

phadej

-- Normalization by evaluation for λ→2
-- Thorsten Altenkirch and Tarmo Uustalu (FLOPS
--
-- Agda translation by Oleg Grenrus
-- no proofs yet.

module Lambda2 where

open import Data.Nat using (ℕ; zero; suc; _+_; _*_)
import Data.Nat.Properties as ℕ

phadej

module Monotone where

open import Data.Nat using (ℕ; zero; suc; z≤n; s≤s)
open import Data.Nat.Properties using ()
open import Data.Fin using (Fin; zero; suc; _≤_)
open import Relation.Binary.PropositionalEquality

data Mono : ℕ → ℕ → Set where
  nil : ∀ {n} → Mono zero n
  new : ∀ {n m} → Mono n       m       → Mono (suc n) (suc m)

phadej

import Data.Coerce
import Data.Monoid

-- This combinator is based on ala' from Conor McBride's work on Epigram.
alaf :: (Coercible n o, Coercible n' o')
     => (o -> n) -> ((a -> n) -> b -> n') -> (a -> o) -> b -> o'
alaf _ = coerce

myfoldl :: Foldable t => (b -> a -> b) -> b -> t a -> b
myfoldl f z xs = alaf (Dual . Endo) foldMap (flip f) xs z

phadej

From 9f72a94762e730da15ada2147cd5a6ccb4f90406 Mon Sep 17 00:00:00 2001
From: Oleg Grenrus <[email protected]>
Date: Thu, 30 Dec 2021 21:04:11 +0200
Subject: [PATCH] PoC RecordDot

---
 compiler/GHC/Driver/Session.hs                |  3 ++
 compiler/GHC/Hs/Expr.hs                       |  2 +-
 compiler/GHC/HsToCore/Expr.hs                 |  4 +-
 compiler/GHC/Parser/Lexer.x                   | 14 ++---

phadej

import Debug.Trace (traceM)
import Data.String (IsString (..))

-- $setup
-- >>> :set -XOverloadedStrings

-- | A formatter.
--
-- The power of simple Haskell.
--