aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
-rw-r--r--editors/vim/syntax/bruijn.vim2
-rw-r--r--src/Helper.hs8
-rw-r--r--src/Parser.hs3
3 files changed, 11 insertions, 2 deletions
diff --git a/editors/vim/syntax/bruijn.vim b/editors/vim/syntax/bruijn.vim
index 6de2927..b7b2680 100644
--- a/editors/vim/syntax/bruijn.vim
+++ b/editors/vim/syntax/bruijn.vim
@@ -8,7 +8,7 @@ endif
syn match bruijnApplication /[()]/
syn match bruijnAbstraction /[[\]]/
syn match bruijnIndex /\([^0-9]\)\@<=\d\([^0-9]\)\@=/
-syn match bruijnNumber /([+-]\d\+[ubt]\?)/
+syn match bruijnNumber /([+-]\d\+[dubt]\?)/
syn match bruijnDefinition /^\t*\S\+/
syn match bruijnType /\( ⧗ \)\@<=.*$/
syn match bruijnTypeDelim / ⧗ /
diff --git a/src/Helper.hs b/src/Helper.hs
index 2b2e31c..f760597 100644
--- a/src/Helper.hs
+++ b/src/Helper.hs
@@ -328,6 +328,14 @@ decimalToUnary n | n < 0 = decimalToUnary 0
gen 0 = Bruijn 0
gen n' = Application (Bruijn 1) (gen (n' - 1))
+-- Decimal to De Bruijn encoding
+decimalToDeBruijn :: Integer -> Expression
+decimalToDeBruijn n | n < 0 = decimalToDeBruijn 0
+ | otherwise = gen n
+ where
+ gen 0 = Abstraction $ Bruijn $ fromInteger n
+ gen n' = Abstraction $ gen (n' - 1)
+
unaryToDecimal :: Expression -> Maybe String
unaryToDecimal e = do
res <- resolve e
diff --git a/src/Parser.hs b/src/Parser.hs
index 12214a0..470c18f 100644
--- a/src/Parser.hs
+++ b/src/Parser.hs
@@ -118,13 +118,14 @@ parseNumeral :: Parser Expression
parseNumeral = do
_ <- string "(" <?> "number start"
num <- number <?> "signed number"
- base <- try (oneOf "ubt") <|> return 't'
+ base <- try (oneOf "dubt") <|> return 't'
_ <- string ")" <?> "number end"
pure $ f base num
where
f 't' = decimalToTernary
f 'b' = decimalToBinary
f 'u' = decimalToUnary
+ f 'd' = decimalToDeBruijn
f _ = invalidProgramState
sign :: Parser (Integer -> Integer)
sign = (char '-' >> return negate) <|> (char '+' >> return id)