Skip to content

Instantly share code, notes, and snippets.

@cheery
cheery / SimplyDifficult.hs
Last active Feb 22, 2022
Dynamic pattern matching attempt
View SimplyDifficult.hs
{-# LANGUAGE TypeSynonymInstances, FlexibleInstances, MultiParamTypeClasses, GADTs, FlexibleContexts #-}
module SimplyDifficult where
-- This thing demonstrates dynamic pattern unification,
-- however the examples are too simple to verify that the unifier is
-- working correctly.
-- There were also a thing or two that were way too hard to implement.
-- I've omitted them.
View SimplyEasy.hs
module SimplyEasy where
-- From the paper: http://strictlypositive.org/Easy.pdf
-- An attempt to add case -statement.
-- Fails on typechecking a case.
data Name
= Const String
| Bound Int
| Unquoted Int
deriving (Show, Eq)
View continuations.py
from rpython.rlib.rstacklet import StackletThread
from rpython.rlib.objectmodel import specialize
import core
class SThread(StackletThread):
def __init__(self, config):
StackletThread.__init__(self, config)
self.cont = None
def get_sthread():
@cheery
cheery / ukanren.py
Last active Jan 29, 2022
ukanren with untested CHR
View ukanren.py
# -*- encoding: utf-8 -*-
class TermOrVar(object):
def to_str(self, rbp=0):
assert False
class Term(TermOrVar):
def __init__(self, name, args):
self.name = name
self.args = args
for arg in args:
View lam.agda
module lam where
open import Data.List
open import Data.Unit
open import Data.Empty
open import Data.Product
open import Data.Sum
data Ty : Set where
_⊗_ : Ty Ty Ty
View continuations.py
from rpython.rlib.rstacklet import StackletThread
from rpython.rlib.objectmodel import specialize
import core
class SThread(StackletThread):
def __init__(self, config):
StackletThread.__init__(self, config)
self.cont = None
def get_sthread():
View Regex2.agda
module Regex2 where
open import Function
open import Data.Bool
open import Data.Maybe
open import Data.Product
open import Data.Sum
open import Data.List as List
open import Data.Empty
open import Data.Unit
@cheery
cheery / FinMap.agda
Last active Dec 31, 2021
Parser in agda
View FinMap.agda
module FinMap where
open import Agda.Builtin.Equality
open import Relation.Binary.PropositionalEquality using (refl; cong; trans; subst; sym)
open import Data.Nat as ℕ using (ℕ; _<_; _≤_; suc; s≤s; z≤n)
open import Data.Nat.Properties using (≤-refl; +-comm; +-identityˡ; +-identityʳ; +-suc; 1+n≢0)
open import Data.Fin hiding (compare; _<_; _≤_)
open import Data.List
open import Data.Product
open import Data.Sum
View parsergen4.agda
module parsergen4 where
-- for troubleshooting, not a complete parser generator/parsing engine.
open import Agda.Builtin.Equality
open import Relation.Nullary using (Dec)
open import Data.Nat
open import Data.Fin hiding (_<_)
open import Data.Fin.Properties using (suc-injective)
open import Data.Vec hiding (_>>=_)
@cheery
cheery / Main.purs
Last active Aug 20, 2020
Record experiments with Paluh
View Main.purs
module Main where
import Prelude
import Effect (Effect)
import Data.Foldable (fold)
import TryPureScript (h1, h2, p, text, list, indent, link, render, code)
import Unsafe.Coerce (unsafeCoerce)
import Prim.RowList
import Prim.Row