AndrasKovacs

Require Import Coq.Unicode.Utf8.

(*
As far as I can tell, there is way more literature in Agda on datatype-generic
programming than in Coq. I think part of the reason is that the Agda literature
makes liberal use of induction-recursion and fancy termination/positivity
checking, to define fixpoints of functors. These features are not available in
Coq.

AndrasKovacs

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

{-|
Simple universe polymorphism. Features:

  - Non-first-class levels: there is a distinct Pi, lambda and application for
    levels. Levels are distinct from terms in syntax/values.
  - The surface language only allows abstraction over finite levels. Internally,

AndrasKovacs

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

infixr 3 _⇒_
infix  3 sort⇒_
infixl 2 _▶_
infix  2 _$_
infixr 4 _∷_ _∷'_

AndrasKovacs

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

infixr 3 _⇒_
infix 3 sort⇒_
infixl 2 _▶_
infixl 2 _$_ _$'_

AndrasKovacs

{-# language ScopedTypeVariables, RankNTypes, BlockArguments, TypeApplications,
    LambdaCase #-}

module Lib
    ( foldr
    ) where

import           Data.Foldable (foldl')
import           Prelude       hiding (foldr)

AndrasKovacs

{-# language Strict, LambdaCase, GADTs #-}
{-# options_ghc -Wincomplete-patterns -O2 #-}

import Gauge -- package gauge
import Control.Monad

data Op
  = Add
  | NotEq

AndrasKovacs

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

module UnivPoly where

import Data.Foldable
import Data.Maybe
import Data.String
import Debug.Trace

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