{{ message }}

Instantly share code, notes, and snippets.

# Ashok Menonamnn

• London, United Kingdom
Created Aug 2, 2016
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
Created Jul 25, 2016
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 _,_
Created Apr 28, 2016
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*))
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.
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
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 \]))
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)]
Created Jul 28, 2014
Solution to http://codekata.com/kata/kata06-anagrams/
View anagrams.rb
 require 'set' class AnagramDict include Enumerable def initialize @dict = {} end def put(word)
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
Created Mar 2, 2013
Solution to Facebook Programming Challenge Bar Game
View bar.cpp
 #include #include using namespace std; typedef pair pii; void game(); int main( int , char ** ) {
You can’t perform that action at this time.