Skip to content

Instantly share code, notes, and snippets.

Avatar

Ashok Menon amnn

View GitHub Profile
View RBTree.agda
module RBTree where
open import Agda.Primitive public
using (Level; lzero; lsuc; _⊔_)
data Σ {l k} (A : Set l) (B : A Set k) : Set (l ⊔ k) where
_,_ : (a : A) (b : B a) Σ A B
infixr 10 _,_
fst : {l k} {A : Set l} {B : A Set k} -> Σ A B -> A
View HList.agda
module HList where
open import Agda.Primitive public
using (Level; lzero; lsuc; _⊔_)
data Σ {l k} (A : Set l) (B : A -> Set k) : Set (l ⊔ k) where
_,_ : (a : A) -> (B a) -> Σ A B
infixr 3 _,_
View Fact.hs
module Fact where
fact :: Integer -> Integer
fact 0 = 1
fact n = n * fact (n-1)
factk :: Integer -> (Integer -> r) -> r
factk 0 k = k 1
factk n k = factk (n-1) (k . (n*))
@amnn
amnn / Huet.md
Last active Sep 26, 2020
Huet's Circular Unification Algorithm
View Huet.md

Based on Huet 1976, §5.7.2

Preliminaries

From earlier sections

  • V is a countably infinite set of variables.
  • C a finite set of constructors.
  • a : C -> Nat an arity function.
  • R : V -/-> Typ a partial environment function.
@amnn
amnn / grid.rb
Last active Sep 6, 2015
A class to print arbitrary Sudoku-style gride, given a list of numbers.
View grid.rb
# A class to print arbitrary Sudoku-style grids, given a list of numbers
# Author: Ashok Menon, 01/09/2015
class Array
def surround(delim)
"#{delim}#{join delim}#{delim}"
end
end
class Grid
@amnn
amnn / brainfuck.clj
Created Mar 10, 2015
Brainfuck interpreter written in Clojure
View brainfuck.clj
(ns brainfuck
(:refer-clojure :exclude [replace])
(:require [clojure.string :refer [join replace]]))
;;;;;; Parser ;;;;;;
(defn- wrap-outer-brackets
"Wrap string in square brackets so that its contents are read into a vector
by `read-string`."
[s] (str \[ s \]))
@amnn
amnn / earley.clj
Created Oct 9, 2014
Earley Parser in Clojure (Some helper functions are missing).
View earley.clj
(defn recogniser
"Returns the recogniser function for the grammar `g`."
[g]
(let [nullable? (nullable g)
g (null-free g)
init (initial-state (nullable? :S))]
(letfn [(consume-token [{:keys [index items] :as state} tok]
(loop [processed? #{}
items items
state (reset-state state)]
View anagrams.rb
require 'set'
class AnagramDict
include Enumerable
def initialize
@dict = {}
end
def put(word)
@amnn
amnn / Undo.hs
Last active Dec 19, 2015
Dirty Buffer Indicator with Undo/Redo support.
View Undo.hs
module Undo where
data Op = Edit | Undo | Redo | Load | Save deriving (Eq, Show)
type Str = [Op]
type State = (Int, Int, Int) -- ( Save point, Edit distance, Undo displacement )
valid :: State -> Bool
valid (s,e,u) = s >= 0 && e >= 0 && u <= 0 && s <= e && e+u >= 0
@amnn
amnn / bar.cpp
Created Mar 2, 2013
Solution to Facebook Programming Challenge Bar Game
View bar.cpp
#include <iostream>
#include <set>
using namespace std;
typedef pair<int,int> pii;
void game();
int main( int , char ** )
{
You can’t perform that action at this time.