dhaskell.lua

local function pretty_print(term)
	local introduced = {}
	local total = {}
	local function mark(seen, obj, from)
		if seen[obj] then
			introduced[obj] = from
		else
			seen[obj] = true
		end
	end
	local function search(term)
		if total[term] then
			return {[term] = true}
		else
			total[term] = true
			local variant = term.variant
			if variant == "con" then
				local seen = {}
				if not term.con.prim then
					for _, v in ipairs(term.args) do
						for k in pairs(search(v)) do
							mark(seen, k, term)
						end
					end
				end
				mark(seen, term, term)
				return seen
			elseif variant == "lambda" then
				local seen = search(term.term)
				mark(seen, term, term)
				return seen
			elseif variant == "apply" then
				local seen = search(term.fun)
				for k in pairs(search(term.arg)) do
					mark(seen, k, term)
				end
				mark(seen, term, term)
				return seen
			elseif variant == "case" then
				local seen = search(term.term)
				for _, v in pairs(term.cases) do
					for k in pairs(search(v.term)) do
						mark(seen, k, term)
					end
				end
				mark(seen, term, term)
				return seen
			elseif variant == "lookup" or variant == "stuck" then
				local seen = search(term.term)
				for _, v in pairs(term.witnesses) do
					for k in pairs(search(v)) do
						mark(seen, k, term)
					end
				end
				mark(seen, term, term)
				return seen
			else
				return {[term] = true}
			end
		end
	end
	search(term)

	local introducing = {}
	for k, v in pairs(introduced) do
		introducing[v] = introducing[v] or {}
		introducing[v][k] = true
	end
	search(term)
	local ind = 0
	local indices = {}

	local function parens(show, str)
		if show then
			return "(" .. str .. ")"
		else
			return str
		end
	end

	local serialize_rec
	local function serialize(term, p)
		local variant = term.variant
		if variant == "var" then
			return term.var
		elseif variant == "con" then
			if term.con.prim then
				return tostring(term.args) .. "#"
			elseif #term.args == 0 then
				return term.con.name
			else
				local args = {}
				for i, v in ipairs(term.args) do
					args[i] = serialize_rec(v, 4)
				end
				return parens(p > 3, term.con.name .. " " .. table.concat(args, " "))
			end
		elseif variant == "lambda" then
			return parens(p > 2, "\\" .. term.var .. " -> " .. serialize_rec(term.term, 2))
		elseif variant == "apply" then
			return parens(p > 3, serialize_rec(term.fun, 3) .. " " .. serialize_rec(term.arg, 4))
		elseif variant == "case" then
			local cases = {}
			for k, v in pairs(term.cases) do
				table.insert(cases, k.name .. (#v.vars == 0 and "" or " ") .. table.concat(v.vars, " ") .. " -> " .. serialize_rec(v.term, 3))
			end
			return parens(p > 2, "case@" .. term.type.name .. " " .. serialize_rec(term.term, 0) .. " of " .. table.concat(cases, "; "))
		elseif variant == "lookup" or variant == "stuck" then
			local witnesses = {}
			for i, v in ipairs(term.witnesses) do
				witnesses[i] = serialize_rec(v, 3)
			end
			return parens(p > 2, "\\(" .. term.class .. " " .. term.var .. ")" .. (variant == "stuck" and "@" or "") .. "[" .. table.concat(witnesses, "; ") .. "] -> " .. serialize_rec(term.term, 2))
		elseif variant == "prim" then
			return term.name .. "#"
		end
	end

	function serialize_rec(term, p)
		if indices[term] then
			return "%" .. indices[term]
		end
		if introducing[term] then
			local intros = {}
			for k in pairs(introducing[term]) do
				ind = ind + 1
				indices[k] = ind
				table.insert(intros, "%" .. ind .. " = " .. serialize(k, 0))
			end
			return parens(p > 2, "letrec " .. table.concat(intros, "; ") .. " in " .. (indices[term] and "%" .. indices[term] or serialize(term, 2)))
		else
			return serialize(term, p)
		end
	end
	return serialize_rec(term, 0)
end

local function replace_term(target, source)
	for k in pairs(target) do
		target[k] = nil
	end
	for k, v in pairs(source) do
		target[k] = v
	end
end

local function sub_inplace_rec(sub, terms)
	local seen = {}
	local function sub_inplace(sub, term)
		if not seen[term] then
			seen[term] = true
			local variant = term.variant
			if variant == "var" then
				local new_term = sub[term.var]
				if new_term then
					replace_term(term, new_term)
				end
			elseif variant == "con" and not term.con.prim then
				for i, v in ipairs(term.args) do
					term.args[i] = sub_inplace(sub, v)
				end
			elseif variant == "lambda" then
				local var = term.var
				local saved = sub[var]
				sub[var] = nil
				term.term = sub_inplace(sub, term.term)
				sub[var] = saved
			elseif variant == "apply" then
				term.fun = sub_inplace(sub, term.fun)
				term.arg = sub_inplace(sub, term.arg)
			elseif variant == "case" then
				local new_sub = {}
				term.term = sub_inplace(sub, term.term)
				for k, v in pairs(sub) do
					new_sub[k] = v
				end
				for _, v in pairs(term.cases) do
					local vars = v.vars
					for _, var in ipairs(vars) do
						new_sub[var] = nil
					end
					v.term = sub_inplace(new_sub, v.term)
					for _, var in ipairs(vars) do
						new_sub[var] = sub[var]
					end
				end
			elseif variant == "lookup" then
				for i, v in ipairs(term.witnesses) do
					term.witnesses[i] = sub_inplace(sub, v)
				end
				local var = term.var
				local saved = sub[var]
				sub[var] = nil
				term.term = sub_inplace(sub, term.term)
				sub[var] = saved
			elseif variant == "stuck" then
				for i, v in ipairs(term.witnesses) do
					term.witnesses[i] = sub_inplace(sub, v)
				end
				local var = term.var
				local saved = sub[var]
				sub[var] = nil
				term.term = sub_inplace(sub, term.term)
				sub[var] = saved
			end
		end
		return term
	end
	for term in pairs(terms) do
		sub_inplace(sub, term)
	end
end

local function substitute_rec(sub, term)
	local result = {}
	local function substitute(sub, term)
		if result[term] then
			return result[term]
		end
		local variant = term.variant
		if variant == "var" then
			local new_term = sub[term.var]
			if new_term then
				result[term] = new_term
			else
				result[term] = term
			end
		elseif variant == "con" and not term.con.prim then
			local args = {}
			local new_term = {variant = variant, con = term.con, args = args}
			result[term] = new_term
			for i, v in ipairs(term.args) do
				args[i] = substitute(sub, v)
			end
		elseif variant == "lambda" then
			local var = term.var
			local saved = sub[var]
			if saved then
				sub[var] = nil
				local new_term = {variant = variant, var = var}
				result[term] = new_term
				new_term.term = substitute_rec(sub, term.term)
				sub[var] = saved
			else
				local new_term = {variant = variant, var = var}
				result[term] = new_term
				new_term.term = substitute(sub, term.term)
			end
		elseif variant == "apply" then
			local new_term = {variant = variant}
			result[term] = new_term
			new_term.fun = substitute(sub, term.fun)
			new_term.arg = substitute(sub, term.arg)
		elseif variant == "case" then
			local cases = {}
			local new_term = {variant = variant, type = term.type, cases = cases}
			result[term] = new_term
			new_term.term = substitute(sub, term.term)
			local new_sub = {}
			for k, v in pairs(sub) do
				new_sub[k] = v
			end
			for con, v in pairs(term.cases) do
				local vars = v.vars
				local good = true
				for _, var in ipairs(vars) do
					new_sub[var] = nil
					if sub[var] then
						good = false
					end
				end
				if good then
					cases[con] = {vars = vars, term = substitute(sub, v.term)}
				else
					cases[con] = {vars = vars, term = substitute_rec(new_sub, v.term)}
				end
				for _, var in ipairs(vars) do
					new_sub[var] = sub[var]
				end
			end
		elseif variant == "lookup" or variant == "stuck" then
			local witnesses = {}
			local new_term = {variant = variant, class = term.class, var = term.var, witnesses = witnesses}
			result[term] = new_term
			local var = term.var
			local saved = sub[var]
			if saved then
				sub[var] = nil
				new_term.term = substitute_rec(sub, term.term)
				sub[var] = saved
			else
				new_term.term = substitute(sub, term.term)
			end
			for i, v in ipairs(term.witnesses) do
				witnesses[i] = substitute(sub, v)
			end
		else
			result[term] = term
		end
		return result[term]
	end
	return substitute(sub, term)
end

local function normal_form(classes, term, type)
	local variant = term.variant
	if variant == "apply" then
		local fun = term.fun
		normal_form(classes, fun)
		if fun.variant == "lambda" then
			replace_term(term, substitute_rec({[fun.var] = term.arg}, fun.term))
		elseif fun.variant == "prim" then
			replace_term(term, fun.fun(classes, term.arg))
		else
			error("Type error: " .. fun.variant .. " used as function")
		end
		return normal_form(classes, term, type)
	elseif variant == "case" then
		local t = term.term
		normal_form(classes, t)
		if t.variant == "con" then
			local case = term.cases[t.con]
			if not case then
				local cons = {}
				for k in pairs(term.cases) do
					table.insert(cons, k.name)
				end
				error("Pattern match failure: " .. t.con.name .. " not in {" .. table.concat(cons, ", ") .. "}")
			end
			local sub = {}
			for i, var in ipairs(case.vars) do
				sub[var] = t.args[i]
			end
			replace_term(term, substitute_rec(sub, case.term))
			return normal_form(classes, term, type)
		elseif t.variant == "stuck" then
			normal_form(classes, t, term.type)
			normal_form(classes, term, type)
		else
			error("Type error: " .. t.variant .. " used in a case expression")
		end
	elseif variant == "lookup" or variant == "stuck" then
		local class = classes[term.class]
		assert(class, "Class not found: " .. term.class)
		for _, witness in ipairs(term.witnesses) do
			normal_form(classes, witness)
			if witness.variant == "con" then
				dict = class[witness.con.type]
				if dict then
					replace_term(term, substitute_rec({[term.var] = dict}, term.term))
					return normal_form(classes, term)
				end
			end
		end
		if variant == "lookup" then
			error("Invalid class lookup")
		elseif type then
			local class = classes[term.class]
			assert(class, "Class not found: " .. term.class)
			local dict = class[type]
			assert(dict, "Class " .. term.class .. " does not include " .. type.name)
			replace_term(term, substitute_rec({[term.var] = dict}, term.term))
			return normal_form(classes, term, type)
		end
	end
end

local function tokenize(str)
	local keywords = {case = true, let = true, ["in"] = true, of = true, instance = true, data = true}
	local len = #str
	local i = 1
	local tokens = {n = 0}
	while i <= len do
		local ch = str:sub(i, i)
		if ch:match"%s" then
			i = i + 1
		elseif ch:match"[0-9.]" then
			local word
			word, i = str:match("^([0-9.e+-]+)()", i)
			tokens.n = tokens.n + 1
			tokens[tokens.n] = {token = "number", value = assert(tonumber(word), word .. " is not a number")}
		elseif ch:match"[a-z_]" then
			local word
			word, i = str:match("^([a-z_][a-zA-Z_0-9]*)()", i)
			tokens.n = tokens.n + 1
			tokens[tokens.n] = keywords[word] and {token = word} or {token = "var", id = word}
		elseif ch:match"[A-Z]" then
			local word
			word, i = str:match("^([A-Z][a-zA-Z_0-9]*)()", i)
			tokens.n = tokens.n + 1
			tokens[tokens.n] = {token = "con", id = word}
		elseif ch == "-" then
			if str:sub(i + 1, i + 1) == ">" then
				i = i + 2
				tokens.n = tokens.n + 1
				tokens[tokens.n] = {token = "->"}
			else
				i = i + 1
				tokens.n = tokens.n + 1
				tokens[tokens.n] = {token = ch}
			end
		else
			i = i + 1
			tokens.n = tokens.n + 1
			tokens[tokens.n] = {token = ch}
		end
	end
	return tokens
end

local parse_expr
local wrap_number
local function parse_unit(env, tokens, i)
	local tok = assert(tokens[i], "end of input").token
	if tok == "var" then
		return {variant = "var", var = tokens[i].id}, i + 1
	elseif tok == "con" then
		local con = env.cons[tokens[i].id]
		assert(con, "No constructor " .. tokens[i].id .. " found")
		local vars = {}
		for i = 1, con.arity do
			vars[i] = "%" .. i
		end
		local args = {}
		for i = 1, con.arity do
			args[i] = {variant = "var", var = vars[i]}
		end
		local term = {variant = "con", con = con, args = args}
		for i = con.arity, 1, -1 do
			term = {variant = "lambda", var = vars[i], term = term}
		end
		return term, i + 1
	elseif tok == "number" then
		return wrap_number(tokens[i].value), i + 1
	elseif tok == "\\" then
		local var = assert(tokens[i + 1], "\\ at end of input")
		local abstraction
		if var.token == "var" then
			assert(var.token == "var", "\\ should be followed by a var")
			i = i + 2
			abstraction = {variant = "lambda", var = var.id}
		elseif var.token == "(" then
			local class = assert(tokens[i + 2], "\\( at end of input")
			assert(class.token == "con", "\\( should be followed by class")
			local var = assert(tokens[i + 3], "\\(class at end of input")
			assert(var.token == "var", "\\(class should be followed by a var")
			assert(assert(tokens[i + 4], "\\(class var at end of input").token == ")", "\\(class var should be followed by )")
			i = i + 5
			local stuck = false
			if tokens[i] and tokens[i].token == "@" then
				stuck = true
				i = i + 1
			end
			assert(assert(tokens[i], "\\(class var) at end of input").token == "[", "\\(class var) should be followed by [")
			i = i + 1
			local witnesses = {}
			while tokens[i] and tokens[i].token ~= "]" do
				local term, ni = parse_expr(env, tokens, i)
				assert(term, "witness should be an expression")
				i = ni
				table.insert(witnesses, term)
				if tokens[i] and tokens[i].token == ";" then
					i = i + 1
				else
					break
				end
			end
			assert(assert(tokens[i], "unmatched [").token == "]", "unmatched [")
			i = i + 1
			abstraction = {variant = stuck and "stuck" or "lookup", class = class.id, witnesses = witnesses, var = var.id}
		end
		assert(assert(tokens[i], "abstraction at end of input").token == "->", "abstraction should be followed by ->")
		local term, ni = parse_expr(env, tokens, i + 1)
		assert(term, "abstraction should be followed by expression")
		abstraction.term = term
		return abstraction, ni
	elseif tok == "(" then
		local term, ni = parse_expr(env, tokens, i + 1)
		assert(assert(tokens[ni], "unmatched (").token == ")", "unmatched (")
		return term, ni + 1
	elseif tok == "case" then
		local type
		if tokens[i + 1] and tokens[i + 1].token == "@" then
			local tp = assert(tokens[i + 2], "case@ at end of input")
			assert(tp.token == "con", "case@ should be followed by type")
			type = env.types[tp.id]
			assert(type, "No type " .. tp.id .. " found")
			i = i + 2
		end
		local term, ni = parse_expr(env, tokens, i + 1)
		assert(term, "case should be followed by expression")
		assert(assert(tokens[ni], "unmatched case").token == "of", "case should be matched by of")
		assert(assert(tokens[ni + 1], "of at end of input").token == "{", "of should be followed by {")
		ni = ni + 2
		local cases = {}
		while tokens[ni] and tokens[ni].token == "con" do
			local con = env.cons[tokens[ni].id]
			assert(con, "No constructor " .. tokens[ni].id .. " found")
			local vars = {}
			ni = ni + 1
			while tokens[ni] and tokens[ni].token == "var" do
				table.insert(vars, tokens[ni].id)
				ni = ni + 1
			end
			assert(assert(tokens[ni], "match should be followed by ->").token == "->", "match should be followed by ->")
			local term, nni = parse_expr(env, tokens, ni + 1)
			assert(term, "match -> should be followed by expression")
			ni = nni
			cases[con] = {vars = vars, term = term}
			if tokens[ni] and tokens[ni].token == ";" then
				ni = ni + 1
			else
				break
			end
		end
		assert(assert(tokens[ni], "unmatched {").token == "}", "unmatched {")
		ni = ni + 1
		if not type then
			for k in pairs(cases) do
				type = k.type
				break
			end
		end
		return {variant = "case", type = type, term = term, cases = cases}, ni
	end
end

function parse_expr(env, tokens, i)
	local term, ni = parse_unit(env, tokens, i)
	assert(term, "expression should begin with unit")
	while tokens[ni] do
		local arg, nni = parse_unit(env, tokens, ni)
		if not arg then
			break
		end
		term = {variant = "apply", fun = term, arg = arg}
		ni = nni
	end
	return term, ni
end

function parse_decl(env, tokens, i)
	local tok = assert(tokens[i], "end of input").token
	if tok == "var" then
		local var = tokens[i].id
		i = i + 1
		local vars = {}
		while tokens[i] and tokens[i].token == "var" do
			table.insert(vars, tokens[i].id)
			i = i + 1
		end
		assert(assert(tokens[i], "declaration at end of input").token == "=", "declaration should be followed by =")
		local term, ni = parse_expr(env, tokens, i + 1)
		assert(term, "declaration should be followed by expression")
		for j = #vars, 1, -1 do
			term = {variant = "lambda", var = vars[j], term = term}
		end
		local places = {}
		for _, v in pairs(env.decls) do
			places[v] = true
		end
		for _, v in pairs(env.classes) do
			for _, v in pairs(v) do
				places[v] = true
			end
		end
		sub_inplace_rec({[var] = term}, places)
		env.decls[var] = term
		sub_inplace_rec(env.decls, {[term] = true})
		i = ni
	elseif tok == "data" then
		local tp = assert(tokens[i + 1], "data at end of input")
		assert(tp.token == "con", "data should be followed by type")
		assert(assert(tokens[i + 2], "data type at end of input").token == "=", "data type should be followed by =")
		i = i + 3
		local cons = {}
		local type = {name = tp.id, cons = cons}
		while tokens[i] and tokens[i].token == "con" do
			local con = tokens[i].id
			i = i + 1
			local arity = 0
			while tokens[i] and tokens[i].token == "var" do
				arity = arity + 1
				i = i + 1
			end
			table.insert(cons, {name = con, type = type, arity = arity})
			if tokens[i] and tokens[i].token == "|" then
				i = i + 1
			else
				break
			end
		end
		env.types[tp.id] = type
		for _, v in ipairs(cons) do
			env.cons[v.name] = v
		end
	elseif tok == "instance" then
		local class = assert(tokens[i + 1], "instance at end of input")
		assert(class.token == "con", "instance should be followed by class")
		local tp = assert(tokens[i + 2], "instance class at end of input")
		assert(tp.token == "con", "instance class should be followed by type")
		local type = env.types[tp.id]
		assert(type, "No type " .. tp.id .. " found")
		local dict, ni = parse_expr(env, tokens, i + 3)
		assert(dict, "instance class type should be followed by expression")
		sub_inplace_rec(env.decls, {[dict] = true})
		env.classes[class.id] = env.classes[class.id] or {}
		env.classes[class.id][type] = dict
		i = ni
	else
		error("Unexpected " .. tok)
	end
	if tokens[i] and tokens[i].token == ";" then
		i = i + 1
	end
	return i
end

local function load_decls(env, str)
	local tokens = tokenize(str)
	local i = 1
	while i <= #tokens do
		i = parse_decl(env, tokens, i)
	end
end

local function prim(name, fun)
	return {variant = "prim", name = name, fun = fun}
end

local NumberType = {name = "Number#"}
local NumberCon = {name = "N#", type = NumberType, prim = true}
NumberType.cons = NumberCon

function wrap_number(num)
	return {variant = "con", con = NumberCon, args = num}
end

local function get_number(cls, term)
	normal_form(cls, term, NumberType)
	assert(term.variant == "con", "Type error: " .. term.variant .. " used as number")
	assert(term.con == NumberCon, "Type error: " .. term.con.type.name .. " used as Number#")
	return term.args
end


local IOType = {name = "IO#"}
local IOCon = {name = "IO#", type = IOType, prim = true}
IOType.cons = IOCon

function wrap_io(fun)
	return {variant = "con", con = IOCon, args = fun}
end

local function get_io(cls, term)
	normal_form(cls, term, IOType)
	assert(term.variant == "con", "Type error: " .. term.variant .. " used as io")
	assert(term.con == IOCon, "Type error: " .. term.con.type.name .. " used as IO#")
	return term.args
end

local function evaluate(env, str)
	local tokens = tokenize(str)
	local term, i = parse_expr(env, tokens, 1)
	assert(i > #tokens, "garbage at end of input")
	sub_inplace_rec(env.decls, {[term] = true})
	normal_form(env.classes, term, IOType)
	if term.variant == "con" and term.con == IOCon then
		get_io(env.classes, term)(env.classes)
	else
		print(pretty_print(term))
	end
end

local env;
env = {
	types = {IO = IOType},
	cons = {},
	classes = {
		Show = {
			[NumberType] = prim("numShow", function(cls, str)
				return prim("numShow%", function(cls, term)
					local str = tostring(get_number(cls, str))
					for i = #str, 1, -1 do
						term = {variant = "con", con = env.cons.Cons, args = {{variant = "con", con = NumberCon, args = str:byte(i, i)}, term}}
					end
					return term
				end)
			end)
		},
		Eq = {
			[NumberType] = prim("numEq", function(cls, term)
				local a = get_number(cls, term)
				return prim("numEq%", function(cls, term)
					local b = get_number(cls, term)
					return {variant = "con", con = a == b and env.cons.True or env.cons.False, args = {}}
				end)
			end)
		}
	},
	decls = {
		dump = prim("dump", function(cls, term)
			print(pretty_print(term))
			return {variant = "lambda", var = "%", term = {variant = "var", var = "%"}}
		end),
		returnIO = prim("returnIO", function(cls, term)
			return wrap_io(function(cls) return term end)
		end),
		bindIO = prim("bindIO", function(cls, term)
			local k = get_io(cls, term)
			return prim("bindIO%", function(cls, term)
				return wrap_io(function(cls)
					local term = {variant = "apply", fun = term, arg = k(cls)}
					normal_form(cls, term)
					return get_io(cls, term)(cls)
				end)
			end)
		end),
		putChar = prim("putChar", function(cls, term)
			local code = get_number(cls, term)
			return wrap_io(function(cls)
				io.write(string.char(code))
				io.stdout:flush()
				return {variant = "con", con = env.cons.Unit, args = {}}
			end)
		end),
		getChar = wrap_io(function(cls)
			local ch = io.read(1)
			return wrap_number(ch:byte())
		end),
		numAdd = prim("numAdd", function(cls, a) return prim("numAdd%", function(cls, b) return wrap_number(get_number(cls, a) + get_number(cls, b)) end) end),
		numSub = prim("numSub", function(cls, a) return prim("numSub%", function(cls, b) return wrap_number(get_number(cls, a) - get_number(cls, b)) end) end),
		numMul = prim("numMul", function(cls, a) return prim("numMul%", function(cls, b) return wrap_number(get_number(cls, a) * get_number(cls, b)) end) end),
		numDiv = prim("numDiv", function(cls, a) return prim("numDiv%", function(cls, b) return wrap_number(get_number(cls, a) / get_number(cls, b)) end) end),
		numMod = prim("numMod", function(cls, a) return prim("numMod%", function(cls, b) return wrap_number(get_number(cls, a) % get_number(cls, b)) end) end),
		numExp = prim("numExp", function(cls, a) return prim("numExp%", function(cls, b) return wrap_number(get_number(cls, a) ^ get_number(cls, b)) end) end),
	}
}
load_decls(env, [[
id x = x;
const x y = x;
compose f g x = f (g x);
fix f = f (fix f);

data Unit = Unit;

data Bool = False | True;

if x y z = case x of {
		False -> z;
		True -> y;
	};

not x = if x False True;
and x y = if x y x;
or x y = if x x y;

eq x y = \(Eq eq)[x; y] -> eq x y;

instance Eq Unit
	\x -> \y -> case x of {
		Unit -> case y of {
			Unit -> True;
		};
	};

instance Eq Bool
	\x -> \y -> case x of {
		False -> case y of {
			False -> True;
			True -> False;
		};
		True -> case y of {
			False -> False;
			True -> True;
		};
	};

data Pair = Pair a b;
fst p = case p of {Pair x y -> x};
snd p = case p of {Pair x y -> y};

fmap f x = \(Functor fmap)@[x] -> fmap f x;

pure x = \(Applicative dict)@[] -> fst dict x;

ap f k = \(Applicative dict)@[f; k] -> snd dict f k;

bind k f = \(Monad bind)@[f; k] -> bind k f

data Identity = Identity x;

runIdentity x = case x of {Identity x -> x};

instance Functor Identity
	\f -> \x -> Identity (f (runIdentity x));

instance Applicative Identity
	Pair
		(\x -> Identity x)
		(\f -> \k -> Identity (runIdentity f (runIdentity k)));

data List = Nil | Cons x xs;

head xw = case xw of {Cons x xs -> x};

tail xw = case xw of {Cons x xs -> xs};

instance Functor List
	\f -> \xw -> case xw of {
		Nil -> Nil;
		Cons x xs -> Cons (f x) (fmap f xs);
	};

concat = \xw -> \ys -> case xw of {
		Nil -> ys;
		Cons x xs -> Cons x (concat xs ys);
	};

instance Applicative List
	Pair
		(\x -> Cons x Nil)
		(\fw -> \ks -> case fw of {
			Nil -> Nil;
			Cons f fs -> concat (fmap f ks) (ap fs ks);
		});

instance Monad List
	\kw -> \fs -> case kw of {
		Nil -> Nil;
		Cons k ks -> concat (fs k) (bind ks fs);
	};

instance Functor IO
	\f -> \x -> bindIO x (\x -> returnIO (f x))

instance Applicative IO
	Pair returnIO
		(\f -> \k -> bindIO f (\f -> bindIO k (\k -> returnIO (f k))));
		
instance Monad IO
	bindIO;

mapM f xw = case xw of {
		Nil -> pure Nil;
		Cons x xs -> bind (f x) (\x -> fmap (cons x) (mapM f xs));
	};

putStr xw = case xw of {
		Nil -> pure Unit;
		Cons x xs -> bind (putChar x) (\_ -> putStr xs);
	};

putStrLn xs = bind (putStr xs) (\_ -> putChar 10);

getLine = bind getChar (\c -> if (eq c 10) (pure Nil) (fmap (Cons c) getLine));

shows x rs = \(Show shows)[x] -> shows x rs;
show x = shows x Nil;

print = compose putStrLn show;

instance Show Unit
	\x -> \rs -> case x of {
		Unit -> Cons 85 (Cons 110 (Cons 105 (Cons 116 rs)));
	};

instance Show Bool
	\x -> \rs -> case x of {
		False -> Cons 70 (Cons 97 (Cons 108 (Cons 115 (Cons 101 rs))));
		True -> Cons 84 (Cons 114 (Cons 117 (Cons 101 rs)));
	};

instance Show List
	\x -> \rs -> case x of {
		Nil -> Cons 78 (Cons 105 (Cons 108 rs));
		Cons x xs -> Cons 40 (Cons 67 (Cons 111 (Cons 110 (Cons 115 (Cons 32 (shows x (Cons 32 (shows xs (Cons 41 rs)))))))));
	};

take n xs = if (eq n 0) Nil (case xs of {
		Nil -> Nil;
		Cons x xs -> Cons x (take (numSub n 1) xs);
	});

drop n xs = if (eq n 0) xs (case xs of {
		Nil -> Nil;
		Cons x xs -> drop (numSub n 1) xs;
	});

iterate f x = Cons x (iterate f (f x));

filter f xw = case xw of {
		Nil -> Nil;
		Cons x xs -> if (f x) (Cons x (filter f xs)) (filter f xs);
	};
]])
io.write"> "
io.stdout:flush()
for line in io.lines() do
	local succ, err = pcall(load_decls, env, line)
	if not succ then
		local succ2, err2 = pcall(evaluate, env, line)
		if not succ2 then
			print(err2)
		end
	end
	io.write"> "
	io.stdout:flush()
end