# MIT License, Copyright (c) 2024 Marvin Borner

# usage:
# write a file test.bruijn
# ```
# zero [[0]]
# inc [[[1 (2 1 0)]]]
# two inc (inc zero)
# four two two
# main four four
# ```
# run `cat test.bruijn | bruijn minibruijn.bruijn`

# This parser/interpreter works by parsing the input to the meta encoding
# (similar to Mogensen-Scott) and reducing it using its self-interpreter!
# Substituting the definitions is done *while parsing* using hashmaps

:import std/Char
:import std/Combinator .
:import std/List .
:import std/Meta
:import std/Monad/Parser .
:import std/Number/Conversion
:import std/Map
:import std/Result
:import std/String
:import std/Option

# meta encoding uses Church numerals instead of binary!
char→number (\Char.sub '0') → Conversion.binary→unary

# parses [a-z]+
identifier some (satisfy Char.alpha?)

# parses  *
spaces many (satisfy Char.space?)

# parses \n+
newlines some (satisfy (Char.eq? '\n'))

# parses between parentheses
parens between (char '(') (char ')')

# parses a single number (as number)
number char→number <$> (satisfy Char.numeric?)

error-identifier error-custom "identifier not found"

# T := [T]  # Abstraction
#    | T..T # Application
#    | (T)  # Parenthesized
#    | 0-9  # de Bruijn index
# identifiers ([a-z]*) just get looked up in the hashmap!
term [y [(foldl1 Meta.app) <$> (some (spaces *> singleton <* spaces))]]
	singleton abs <|> idx <|> def <|> (parens 0)
		abs Meta.abs <$> (between (char '[') (char ']') 0)
		idx Meta.idx <$> number
		def identifier >>= [lift-result (Option.result-or error-identifier lookup)]
			lookup String.#Map.lookup 0 2

:test (term Map.empty "()") (Result.err (error-compose (error-unexpected "(") (error-unexpected ")")))
:test (term Map.empty "[[0 1]]") (Result.ok [0 `[[(0 1)]] empty])
:test (term (String.#Map.insert "foo" `[[1]] Map.empty) "[foo 0]") (Result.ok [0 `[[[1]] 0] empty])

# parses an identifier, a term, and newlines to a hashmap insertion
block [[[String.#Map.insert 1 0 2]] <$> identifier <*> (term 0) <* newlines]

:test (block Map.empty "main [0]\n") (Result.ok [0 (String.#Map.insert "main" `[0] Map.empty) empty])
:test (block Map.empty "main ()\n") (Result.err (error-compose (error-unexpected "(") (error-unexpected ")")))

# iterates parsing of blocks starting with an empty hashmap until end
program y [[((block 0) >>= 1) <|> (eof *> (pure 0))]] Map.empty

# evaluates the main function of a program
main Meta.eval <$> ([String.#Map.lookup "main" 0 i i] <$> program) → [0 i i]