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 <oleg.grenrus@iki.fi>
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.
--

phadej

Only in DBFunctor-0.1.2.1: cabal.project
Only in DBFunctor-0.1.2.1: dist-newstyle
Only in DBFunctor-0.1.2.1: .ghc.environment.x86_64-linux-8.6.5
diff -ur orig/DBFunctor-0.1.2.1/src/RTable/Core.hs DBFunctor-0.1.2.1/src/RTable/Core.hs
--- orig/DBFunctor-0.1.2.1/src/RTable/Core.hs	2021-05-23 18:03:12.000000000 +0300
+++ DBFunctor-0.1.2.1/src/RTable/Core.hs	2021-10-28 00:00:45.265149734 +0300
@@ -818,11 +818,6 @@
     -- anything else is just False
     _ == _ = False