Something went wrong. Try again.
dependent-types proof-assistant
Something went wrong. Try again.
7.0 kB · 235 lines
Haskell
at main
123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142143144145146147148149150151152153154155156157158159160161162163164165166167168169170171172173174175176177178179180181182183184185186187188189190191192193194195196197198199200201202203204205206207208209210211212213214215216217218219220221222223224225226227228229230231232233234235236{-# options_ghc -Wno-orphans #-} -- specialize rules are "orphans"
module Parser where
import Prelude hiding (exp, pi)import FlatParse.Basic qualified as FPimport FlatParse.Minimal qualified as FPM
import Common hiding (empty, many, some, (<|>), debug, PiDomKind(..))
import Parser.Monadimport Presyntax
import Lexer (TokenKind(..), Token(..), pattern Token)import Lexer qualified as Lexer
----------------------------------------------------------------------------------------------------
{-# specialize noinline kindMustFollowCold @Exp #-}{-# specialize noinline kindMustFollowCold @(ParseList Bind) #-}{-# specialize noinline kindMustFollowCold @(ParseList Binders) #-}{-# specialize noinline kindMustFollowCold @(ParsePair Bind (ParseList Binders)) #-}
----------------------------------------------------------------------------------------------------
userName :: FP.Span -> Parser UserNameuserName sp = UserName (fpSpanToSpan sp) ! askSrc
pos :: FP.Pos -> Parser Pospos p = liftIO (fpPosToPosIO p)
lexicalError :: EmbedParseError a => FP.Span -> Parser alexicalError (FP.Span i j) = do i <- pos i j <- pos j pure $ embedParseError (PMNothing i) $ ParseError [PEILexicalError] i j j
----------------------------------------------------------------------------------------------------
makeNatLit :: FP.Pos -> FP.Pos -> Parser IntegermakeNatLit l r = do src <- srcToBs ! askSrc src <- pure $ FPM.unsafeSlice src (FP.Span l r) liftIO $ FPM.runParser FPM.anyAsciiDecimalInteger src >>= \case FPM.OK n _ -> pure n _ -> impossible
atom' :: Parser Expatom' = peek \fbk -> \case Token_ ERR sp -> lexicalError sp Token_ IDENT sp -> Var ! userName sp Token LPAR l _ -> (exp <!* [RPAR]) \t (FP.Span _ r) _ -> Paren ! pos l ∘ pure t ∘ pos r Token LZERO l r -> LZero ! pos l ∘ pos r Token LSUC l r -> LSuc ! pos l ∘ pos r Token FINLEVEL l r -> FinLevel ! pos l ∘ pos r Token UNDERSCORE l r -> PlsInfer ! pos l ∘ pos r Token NATLIT l r -> NatLit ! pos l ∘ makeNatLit l r ∘ pos r Token LMAX l r -> LMax ! pos l ∘ pos r _ -> empty
atom :: Parser Expatom = atom' `cut` ["atomic expression"]
proj' :: Parser Projproj' = peek \fbk -> \case Token_ ERR sp -> lexicalError sp Token_ IDENT sp -> PName ! userName sp _ -> empty
proj :: Parser Projproj = proj' `cut` ["field name"]
goProjs :: Exp -> Parser ExpgoProjs t = (proj <? DOT) (\x _ -> goProjs (Proj t x)) (\x -> pure (Proj t x))
projs :: Parser Expprojs = (atom <? DOT) (\t _ -> goProjs t) pure
projs' :: Parser Expprojs' = (atom' <? DOT) (\t _ -> goProjs t) pure
goSpine :: Parser SpinegoSpine = branch (kind' LBRACE) (\_ -> SApp ! (exp <! RBRACE) ∘ pure Impl ∘ goSpine) $ branch (projs' <|) (\t -> SApp t ! pure Expl ∘ goSpine) $ (SNil ! getPos)
infLevel :: FP.Pos -> Parser InfLevelinfLevel r = peek \fbk -> \case Token NATLIT l r -> OmegaPlus ! pos l ∘ makeNatLit l r ∘ pos r _ -> fbk $ OmegaPlusOmega ! pos r
spine :: Parser Expspine = peek \fbk -> \case Token Lexer.TYPE l r -> Type ! pos l ∘ projs Token BIGTYPE l r -> BigType ! pos l ∘ infLevel r _ -> fbk $ mkSpine ! projs ∘ goSpine
----------------------------------------------------------------------------------------------------
bind' :: Parser Bindbind' = peek \fbk -> \case Token_ IDENT sp -> BName ! userName sp Token_ ERR sp -> lexicalError sp Token UNDERSCORE l r -> BUnused ! pos l ∘ pos r _ -> empty
bind :: Parser Bindbind = bind' `cut` ["binder"]
explLamBinders :: Parser BindersexplLamBinders = Binders ! ((PLCons ! bind ∘ many bind') <! COLON) ∘ pure PDExpl ∘ (PMJust ! exp)
lamBinders' :: Parser BinderslamBinders' = peek \fbk -> \case Token LPAR _ _ -> explLamBinders <! RPAR Token LBRACE _ _ -> implBinders <! RBRACE _ -> fbk do x <- bind' pure $ Binders (PLSingle x) PDExpl (PMNothing (rightPos x))
lamBinders :: Parser BinderslamBinders = peek \fbk -> \case Token LPAR _ _ -> explLamBinders <! RPAR Token LBRACE _ _ -> implBinders <! RBRACE _ -> fbk do x <- bind pure $ Binders (PLSingle x) PDExpl (PMNothing (rightPos x))
explPiBinders' :: Parser BindersexplPiBinders' = do xs <- some bind' pd <- (PDExpl <$ kind' COLON) <|> (PDInfArg <$ kind' COLONBANG) a <- exp pure $ Binders xs PDExpl (PMJust a)
implBinders :: Parser BindersimplBinders = do x <- bind xs <- many bind' a <- branch (kind' COLON) -- TODO: can we recover to COLON? (\_ -> PMJust ! exp) (PMNothing ! getPos) pure $ Binders (PLCons x xs) PDImpl a
piBinders :: Parser BinderspiBinders = peek \fbk -> \case Token LPAR _ _ -> explPiBinders' <! RPAR Token LBRACE _ _ -> implBinders <! RBRACE _ -> empty
pi :: Parser Exppi = do l <- getPos many piBinders >>= \case PLNil _ -> (spine <?* [RARR, RARRBANG, RARR_UTF8, RARRBANG_UTF8]) (\t _ -> \case RARRBANG; RARRBANG_UTF8 -> FunBang l t ! (pi <|) RARR; RARR_UTF8 -> Fun l t ! (pi <|) _ -> impossible) pure bss -> do anyKindOf [RARR, RARR_UTF8] Pi l bss ! (pi <|)
lamBody :: FP.Pos -> Parser ExplamBody l = Lam ! pos l ∘ ((PLCons ! lamBinders ∘ many lamBinders') <! DOT) ∘ (exp <|)
exp :: Parser Expexp = peek \fbk -> \case Token BACKSLASH l _ -> lamBody l Token LAMBDA l _ -> lamBody l Token LET l r -> Let ! pos l ∘ (bind <! COLON) ∘ (exp <! RFATARR) ∘ (exp <! SEMI) ∘ (exp <|) _ -> fbk (pi <|)
-- topdef only nowtopDecl :: Parser TopDecltopDecl = do xbs <- (PPair ! bind ∘ many piBinders) <! COLON a <- exp <! RFATARR t <- (exp <|) pure $ TopDef xbs a t
topDecls :: Parser TopDeclstopDecls = (topDecl <? SEMI) (\d _ -> TDCons d ! (topDecls <|)) (\d -> pure $ TDCons d TDNil)
--------------------------------------------------------------------------------
testParse :: String -> IO ()testParse str = do let ?src = SrcNoFile (FP.strToUtf8 str) ts <- Lexer.lexSrc ?src putStrLn "TOKENS" putStrLn $ replicate 30 '-' Lexer.printTokens ts putStrLn "\nPARSE OUTPUT" putStrLn $ replicate 30 '-' runParserIO (eofMustFollow topDecls) ?src mempty ts >>= \case OK a _ -> pPrint a Fail -> putStrLn "Fail" Err e _ -> pPrint e
tst = testParse src
src :: Stringsrc = """ foo {A ? C : Type} (x y : A) : _ => foo.bar → Type bar (i j k : FinLevel) : Type (lmax i (lmax j k)) => _ """
src2 :: Stringsrc2 = """ foo : A => bar → baz
bar2 : B => let x : C => foo let y : F => bar a b c foo
brr : _ => (foo bar).x.y (type (lsuc lzero))
kkk : _ => type (lsuc 10) """
--------------------------------------------------------------------------------