| {-# OPTIONS --guarded #-} | |
| open import Agda.Primitive | |
| open import Relation.Binary.PropositionalEquality using (_≡_; refl; subst; sym; trans) | |
| open import Data.Unit using (⊤; tt) | |
| open import Data.Nat -- using (ℕ; _+_; suc; _<_) | |
| open import Data.Nat.Properties | |
| open import Data.Fin using (Fin; fromℕ; fromℕ<) | |
| open import Data.Vec using (Vec; lookup; []; _∷_; [_]; _++_; map) |
| {-# OPTIONS --cubical #-} | |
| open import Agda.Builtin.Cubical.Path | |
| open import Agda.Primitive.Cubical | |
| cong : ∀ {ℓ} {A : Set ℓ} {x y : A} {B : A → Set ℓ} (f : (a : A) → B a) (p : x ≡ y) | |
| → PathP (λ i → B (p i)) (f x) (f y) | |
| cong f p i = f (p i) | |
| open import Data.Nat |
| {-# LANGUAGE GADTs #-} | |
| import Control.Monad | |
| -- Note that Cmd values are perfectly "pure" values. There's nothing here that | |
| -- makes them impure. | |
| data Cmd a where | |
| PutStr :: String -> Cmd () | |
| PutStrLn :: String -> Cmd () | |
| ReadLn :: Cmd Int |
| {-# language | |
| BlockArguments | |
| , ConstraintKinds | |
| , ImplicitParams | |
| , LambdaCase | |
| , OverloadedStrings | |
| , PatternSynonyms | |
| , Strict | |
| , UnicodeSyntax | |
| #-} |
Every once in a while I investigate low-level backend options for PL-s, although so far I haven't actually written any such backend for my projects. Recently I've been looking at precise garbage collection in popular backends, and I've been (like on previous occasions) annoyed by limitations and compromises.
I was compelled to think about a system which accommodates precise relocating GC as much as possible. In one extreme configuration, described in this note, there
| module C : sig | |
| type t | |
| val empty : t | |
| val one : char -> t | |
| val union : t -> t -> t | |
| val inter : t -> t -> t | |
| val top : t | |
| val mem : char -> t -> bool | |
| val make : (char -> bool) -> t | |
| val equal : t -> t -> bool |
| //> using scala "3.3.0" | |
| import scala.util.boundary, boundary.break | |
| object Loops: | |
| type ExitToken = Unit { type Exit } | |
| type ContinueToken = Unit { type Continue } | |
| type Exit = boundary.Label[ExitToken] |
| {-# OPTIONS_GHC -Wno-unrecognised-pragmas #-} | |
| {-# HLINT ignore "Use list comprehension" #-} | |
| import Data.IORef ( IORef, newIORef, readIORef, writeIORef ) | |
| import GHC.IO ( unsafePerformIO ) | |
| import Control.Applicative ( Alternative(..) ) | |
| import Control.Monad ( when ) | |
| import Debug.Trace | |
| (* language definition *) | |
| type nom = string | |
| type bop = Add | Sub | Mul | |
| type typ = | |
| | Int | Arrow of typ * typ | Meta of meta | |
| and meta = meta_state ref | |
| and meta_state = | |
| | Solved of typ | |
| | Unsolved of nom (* keep name for pretty printing *) |
