rntz

import bisect
from dataclasses import dataclass

class Bound:
    def to_bound(self): return self
    def __lt__(self, other):
        return self <= other and self != other
    def __le__(self, other):
        if isinstance(self, Init) or isinstance(other, Done): return True
        if isinstance(self, Done) or isinstance(other, Init): return False

rntz

-- A lower bound in a totally ordered key-space k; corresponds to some part of an
-- ordered sequence we can seek forward to.
data Bound k = Init | Atleast !k | Greater !k | Done deriving (Show, Eq)
instance Ord k => Ord (Bound k) where
  Init      <= _         = True
  _         <= Done      = True
  _         <= Init      = False
  Done      <= _         = False
  Atleast x <= Atleast y = x <= y
  Atleast x <= Greater y = x <= y

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