alt-romes

{- cabal:
build-depends: base, random, containers
-}
{-# LANGUAGE GADTs, ViewPatterns, GHC2021 #-}
import Text.Printf
import Control.Monad (liftM, ap)
import Data.Function (on)
import Data.List (sort, minimumBy)
import System.Random
import qualified Data.Map as M

roboguy13

open import Data.Nat
open import Data.Nat.Properties
open import Relation.Binary.PropositionalEquality
open import Data.Product
open import Data.Sum
open import Relation.Nullary

module MonoidNat3 where

data Expr : Set where

Lysxia

module CoDebruijn where

open import Data.Product using (_×_; _,_; ∃-syntax)
open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl)

data Context : Set where
  O : Context
  1+_ : Context → Context

data Singleton : Context → Set where

TOTBWF

(** {1 Syntax} *)

(** Expressions. *)
type expr =
  | Var of cont * int
  (** Local references.

      Thorin is a "blockless" IR, so we can reference arguments of
      other nodes by adding a data dependency edge, which implicitly
      nests the two nodes. *)

rntz

type var = string
type term = Var of var
          | Lam of var * term
          | App of term * term
          | Fix of var * term   (* only used for functions *)
          | Lit of int

type value = Int of int
           | Fun of (value -> value)

rntz

import System.Environment (getArgs)

import Control.Monad (guard, forM_)

import System.Random (RandomGen)
import qualified System.Random as Random

import Data.Map.Strict (Map)
import qualified Data.Map.Strict as Map

TOTBWF

description
Inversion hell.

AndrasKovacs

Lightweight region memory management in a two-stage language

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

atennapel

-- Polarized lambda calculus to A-normal form
-- With eta-expansion and call-saturation

type Ix = Int
type Lvl = Int

data Ty = TInt
  deriving (Show)
data TFun = TFun [Ty] Ty
  deriving (Show)

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.