AndrasKovacs

{- Question: https://stackoverflow.com/questions/79894235/can-we-prove-equal-subcases-have-equal-induction-hypotheses-in-recursion-princip
   I don't think this is possible without funext -}

module W-Ind {i j}(A : Set i)(B : A → Set j) where

open import Level
open import Relation.Binary.PropositionalEquality renaming (subst to tr; cong to ap)
open import Data.Product renaming (proj₁ to ₁; proj₂ to ₂)

postulate

AndrasKovacs

{-# language Strict, LambdaCase #-}

module ReasonableLC where

type Ix  = Int
type Lvl = Int

-- environment trimming, drops some entries
data Trim = Empty | Keep Trim | Drop Trim

AndrasKovacs

{-
Conor McBride's "classy hack" for getting HOAS notation for FOAS: https://mazzo.li/epilogue/index.html%3Fp=773.html
The following is a code-golfed version where we observe that by sprinkling some singletons
in the standard FOAS definition of terms, we get an equivalent definition (because singletons are
contractible) which supports HOAS notation directly.
-}

{-# OPTIONS --backtracking-instance-search #-}

open import Relation.Binary.PropositionalEquality

AndrasKovacs

{-# language DeriveFunctor, DeriveFoldable, RankNTypes, LambdaCase #-}

-- -- Breadth first

-- import Control.Applicative
-- import Control.Monad

-- data Tree a = Zero | One a | Node (Tree a) (Tree a)

AndrasKovacs

Comparing GHC Core for Parsley and flatparse for a simple s-expression parser. GHC 8.6.6, flatparse 0.5.2.1, parsley 2.0.0.1

Flatparse source:

{-# language TemplateHaskell #-}

module FP (runSexp) where

import FlatParse.Basic

AndrasKovacs

Lightweight region memory management in a two-stage language

• Intro
• Basics
  • Stage inference
• Regions
  • Bit-stealing
  • Using regions
• Eager regions

AndrasKovacs

Basic setup for formalizing elaboration

First attempts

Elaboration is, broadly speaking, taking user-written syntax and converting it to "core" syntax by filling in missing information and at the same time validating that the input is well-formed.

I haven't been fully happy with formalizations that I previously used, so I make a new attempt here. I focus on a minimal dependently typed case.

AndrasKovacs

{-# language
    BlockArguments
  , CPP
  , LambdaCase
  , MagicHash
  , PatternSynonyms
  , Strict
  , TypeApplications

AndrasKovacs

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

-- version 1, conversion is indexed over conversion
module IndexedConv where

  data Con  : Set
  data Ty   : Con → Set
  data Sub  : Con → Con → Set
  data Tm   : ∀ Γ → Ty Γ → Set
  data Con~ : Con → Con → Set

AndrasKovacs

{-# language
  BlockArguments
, ConstraintKinds
, ImplicitParams
, LambdaCase
, OverloadedStrings
, PatternSynonyms
, Strict
, UnicodeSyntax
#-}