Skip to content

Commit

Permalink
Improved minibruijn and parser
Browse files Browse the repository at this point in the history
  • Loading branch information
marvinborner committed Oct 28, 2024
1 parent fe1fe57 commit 551cfb8
Show file tree
Hide file tree
Showing 4 changed files with 55 additions and 26 deletions.
65 changes: 41 additions & 24 deletions samples/fun/minibruijn.bruijn
Original file line number Diff line number Diff line change
@@ -1,4 +1,5 @@
# MIT License, Copyright (c) 2024 Marvin Borner

# usage:
# write a file test.bruijn
# ```
Expand All @@ -10,49 +11,65 @@
# ```
# run `cat test.bruijn | bruijn minibruijn.bruijn`

:import std/Char C
# 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 M
:import std/Meta
:import std/Monad/Parser .
:import std/Number/Conversion O
:import std/Map H
:import std/Result R
:import std/String S
: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 (\C.sub '0') → O.binary→unary
char→number (\Char.sub '0') → Conversion.binary→unary

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

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

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

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

number char→number <$> (satisfy C.numeric?)
# 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) # Parenthesised
# | (T) # Parenthesized
# | 0-9 # de Bruijn index
# identifiers ([a-z]*) just get looked up in the hashmap!
term [y [(foldl1 M.app) <$> (some (spaces *> singleton <* spaces))]]
term [y [(foldl1 Meta.app) <$> (some (spaces *> singleton <* spaces))]]
singleton abs <|> idx <|> def <|> (parens 0)
abs M.abs <$> (between (char '[') (char ']') 0)
idx M.idx <$> number
def [S.#H.lookup 0 2 i i] <$> identifier
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 H.empty "()") (R.err (error-compose (error-unexpected "(") (error-unexpected ")")))
:test (term H.empty "[[0 1]]") (R.ok [0 `[[(0 1)]] empty])
:test (term (S.#H.insert "foo" `[[1]] H.empty) "[foo 0]") (R.ok [0 `[[[1]] 0] empty])
: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])

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

:test (block H.empty "main [0]\n") (R.ok [0 (S.#H.insert "main" `[0] H.empty) empty])
:test (block H.empty "main ()\n") (R.err (error-compose (error-unexpected "(") (error-unexpected ")")))
: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 ")")))

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

main M.eval <$> ([S.#H.lookup "main" 0 i i] <$> program) → [0 i i]
# evaluates the main function of a program
main Meta.eval <$> ([String.#Map.lookup "main" 0 i i] <$> program) → [0 i i]
2 changes: 1 addition & 1 deletion src/Parser.hs
Original file line number Diff line number Diff line change
Expand Up @@ -385,7 +385,7 @@ parseImport :: Parser Command
parseImport = do
_ <- string ":import" <* sc <?> "import instruction"
path <- importPath
ns <- try (sc *> (namespace <|> string ".")) <|> (eof >> return "")
ns <- try (sc *> (namespace <|> string ".")) <|> return ""
pure $ Import (path ++ ".bruijn") ns

parseInput :: Parser Command
Expand Down
9 changes: 8 additions & 1 deletion std/Monad/Parser.bruijn
Original file line number Diff line number Diff line change
Expand Up @@ -34,6 +34,8 @@ map [[[R.map ok (1 0)]]] ⧗ (a → b) → (Parser a) → (Parser b)

…<$>… map

fail [[R.err 1]] ⧗ a → (Parser a)

pure [[R.ok (1 : 0)]] ⧗ a → (Parser a)

ap [[[R.apply (2 0) ok]]] ⧗ (Parser (a → b)) → (Parser a) → (Parser b)
Expand All @@ -50,7 +52,7 @@ string y [[0 [[[go]]] (pure [[0]])]] ⧗ String → (Parser a)

return pure ⧗ a → (Parser a)

bind [[[R.apply ok (2 0)]]] ⧗ (Parser a) → (a → (Parser b)) → (Parser a)
bind [[[R.apply (2 0) ok]]] ⧗ (Parser a) → (a → (Parser b)) → (Parser a)
ok &[[3 1 0]]

…>>=… bind
Expand All @@ -70,6 +72,11 @@ eof [0 [[[go]]] end] ⧗ (Parser a)
go R.err error-expected-end
end R.ok ([[0]] : [[0]])

lift-result [0 pure fail] ⧗ (Result a) → (Parser a)

:test (lift-result (R.ok "ok") "rst") (R.ok ("ok" : "rst"))
:test (lift-result (R.err "oh") "rst") (R.err "oh")

# =========================================================================== #
# most relevant functions are defined - we can now derive from Generic/Monad! #
# =========================================================================== #
Expand Down
5 changes: 5 additions & 0 deletions std/Option.bruijn
Original file line number Diff line number Diff line change
Expand Up @@ -45,3 +45,8 @@ apply [[1 none 0]] ⧗ (Option a) → (a → b) → c

:test (apply none [some ([[1]] 0)]) (none)
:test (apply (some [[0]]) [some ([[1]] 0)]) (some [[[0]]])

result-or [[0 [[0 3]] [[[1 2]]]]]

:test (result-or "fail" none) ([[0 "fail"]])
:test (result-or "fail" (some "ok")) ([[1 "ok"]])

0 comments on commit 551cfb8

Please sign in to comment.