Initial commit

1 files changed, 46 insertions, 0 deletions

diff --git a/source/Syntax/Chunk.hs b/source/Syntax/Chunk.hs
new file mode 100644
index 0000000..604ccf6
--- /dev/null
+++ b/source/Syntax/Chunk.hs
@@ -0,0 +1,46 @@
+module Syntax.Chunk where
+
+import Base
+import Syntax.Token
+
+import Data.List qualified as List
+
+
+-- LATER This is just a naïve implementation of token chunks.
+-- It and  the current tokenizer should probably be replaced by
+-- a more efficient implementation that does chunking
+-- directly while tokenizing.
+
+chunkify :: [Located Token] -> [[Located Token]]
+chunkify [] = []
+chunkify (tok : toks) = case unLocated tok of
+    BeginEnv env | isTopLevelEnv env ->
+        let (axiomToks, otherToks) = envBlock env toks
+        in  (tok : axiomToks) : chunkify otherToks
+    --
+    -- Skip all tokens outside of toplevel environments.
+    _ -> chunkify toks
+
+isTopLevelEnv :: Text -> Bool
+isTopLevelEnv env = env `elem`
+    [ "abbreviation"
+    , "axiom"
+    , "claim"
+    , "corollary"
+    , "datatype"
+    , "definition"
+    , "inductive"
+    , "lemma"
+    , "proof"
+    , "proposition"
+    , "signature"
+    , "struct"
+    , "theorem"
+    ]
+
+envBlock :: Text -> [Located Token] -> ([Located Token], [Located Token])
+envBlock env toks =
+    let (pre, post) = List.span (\tok -> unLocated tok /= EndEnv env) toks
+    in case post of
+        [] -> (pre, post)
+        endEnv : post' -> (pre ++ [endEnv], post')