summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--source/Syntax/Adapt.hs24
1 files changed, 17 insertions, 7 deletions
diff --git a/source/Syntax/Adapt.hs b/source/Syntax/Adapt.hs
index 49796b4..b338d47 100644
--- a/source/Syntax/Adapt.hs
+++ b/source/Syntax/Adapt.hs
@@ -27,16 +27,14 @@ scanChunk ltoks =
in case ltoks of
Located{startPos = pos, unLocated = BeginEnv "definition"} : _ ->
matchOrErr definition "definition" pos
- Located{startPos = pos, unLocated = BeginEnv "signature"} : _ ->
- matchOrErr signaturePredicate "signature" pos
+ -- TODO Located{startPos = pos, unLocated = BeginEnv "signature"} : _ ->
+ -- matchOrErr signatureExtension "signature" pos
Located{startPos = pos, unLocated = BeginEnv "abbreviation"} : _ ->
matchOrErr abbreviation "abbreviation" pos
Located{startPos = pos, unLocated = (BeginEnv "struct")} :_ ->
matchOrErr struct "struct definition" pos
Located{startPos = pos, unLocated = (BeginEnv "inductive")} :_ ->
matchOrErr inductive "inductive definition" pos
- --Located{startPos = pos, unLocated = (BeginEnv "signature")} :_ ->
- -- matchOrErr signatureIntro "signature" pos
_ -> []
adaptChunks :: [[Located Token]] -> Lexicon -> Lexicon
@@ -88,18 +86,30 @@ abbreviation = do
skipUntilNextLexicalEnv
pure [lexicalItem m]
-signaturePredicate :: RE Token [ScannedLexicalItem]
-signaturePredicate = do
+signatureExtension :: RE Token [ScannedLexicalItem]
+signatureExtension = do
sym (BeginEnv "signature")
few notEndOfLexicalEnvToken
m <- label
few anySym
- lexicalItem <- sigPred
+ lexicalItem <- head
few anySym
sym (EndEnv "signature")
skipUntilNextLexicalEnv
pure [lexicalItem m]
+signatureExtensionAtom :: RE Token [ScannedLexicalItem]
+signatureExtensionAtom = do
+ sym (BeginEnv "signatureatom")
+ few notEndOfLexicalEnvToken
+ m <- label
+ few anySym
+ lexicalItem <- sigPred
+ few anySym
+ sym (EndEnv "signatureatom")
+ skipUntilNextLexicalEnv
+ pure [lexicalItem m]
+
label :: RE Token Marker
label = msym \case
Label m -> Just (Marker m)