327 lines
7.4 KiB
Idris
327 lines
7.4 KiB
Idris
module Quox.Parser
|
||
|
||
import public Quox.Syntax.Qty.Three
|
||
import public Quox.Syntax
|
||
import public Quox.Lexer
|
||
|
||
import Data.Fin
|
||
import Data.Vect
|
||
import public Text.Parser
|
||
|
||
import Derive.Prelude
|
||
%hide TT.Name
|
||
|
||
%default total
|
||
%language ElabReflection
|
||
|
||
|
||
public export
|
||
0 Grammar : Bool -> Type -> Type
|
||
Grammar = Core.Grammar () Token
|
||
%hide Core.Grammar
|
||
|
||
|
||
public export
|
||
0 BName : Type
|
||
BName = Maybe BaseName
|
||
|
||
public export
|
||
0 PUniverse : Type
|
||
PUniverse = Nat
|
||
|
||
public export
|
||
0 PQty : Type
|
||
PQty = Three
|
||
|
||
namespace PDim
|
||
public export
|
||
data PDim = K DimConst | V BaseName
|
||
%runElab derive "PDim" [Eq, Ord, Show]
|
||
|
||
namespace PTerm
|
||
mutual
|
||
||| terms out of the parser with BVs and bidirectionality still tangled up
|
||
public export
|
||
data PTerm =
|
||
TYPE Nat
|
||
|
||
| Pi PQty BName PTerm PTerm
|
||
| Lam BName PTerm
|
||
| (:@) PTerm PTerm
|
||
|
||
| Sig BName PTerm PTerm
|
||
| Pair PTerm PTerm
|
||
| Case PQty PTerm (BName, PTerm) (PCaseBody)
|
||
|
||
| Enum (List TagVal)
|
||
| Tag TagVal
|
||
|
||
| Eq (BName, PTerm) PTerm PTerm
|
||
| DLam BName PTerm
|
||
| (:%) PTerm PDim
|
||
|
||
| V Name
|
||
| (:#) PTerm PTerm
|
||
|
||
public export
|
||
data PCaseBody =
|
||
CasePair (BName, BName) PTerm
|
||
| CaseEnum (List (TagVal, PTerm))
|
||
|
||
%runElab deriveMutual ["PTerm", "PCaseBody"] [Eq, Ord, Show]
|
||
|
||
private
|
||
data PArg = T PTerm | D PDim
|
||
%runElab derive "PArg" [Eq, Ord, Show]
|
||
|
||
|
||
private
|
||
apply : PTerm -> List PArg -> PTerm
|
||
apply = foldl $ \f, x => case x of T x => f :@ x; D p => f :% p
|
||
|
||
private
|
||
annotate : PTerm -> Maybe PTerm -> PTerm
|
||
annotate s a = maybe s (s :#) a
|
||
|
||
|
||
export
|
||
res : (str : String) -> (0 _ : IsReserved str) => Grammar True ()
|
||
res str = terminal "expecting \"\{str}\"" $
|
||
\x => guard $ x == R str
|
||
|
||
export
|
||
resC : (str : String) -> (0 _ : IsReserved str) => Grammar True ()
|
||
resC str = do res str; commit
|
||
|
||
|
||
parameters {default True commit : Bool}
|
||
private
|
||
maybeCommit : Grammar False ()
|
||
maybeCommit = when commit Core.commit
|
||
|
||
export
|
||
betweenR : {c : Bool} -> (op, cl : String) ->
|
||
(0 _ : IsReserved op) => (0 _ : IsReserved cl) =>
|
||
Grammar c a -> Grammar True a
|
||
betweenR o c p = res o *> maybeCommit *> p <* res c <* maybeCommit
|
||
|
||
export
|
||
parens, bracks, braces : {c : Bool} -> Grammar c a -> Grammar True a
|
||
parens = betweenR "(" ")"
|
||
bracks = betweenR "[" "]"
|
||
braces = betweenR "{" "}"
|
||
|
||
|
||
export
|
||
commaSep : {c : Bool} -> Grammar c a -> Grammar False (List a)
|
||
commaSep = sepEndBy (res ",")
|
||
-- don't commit because of the possible terminating ","
|
||
|
||
export
|
||
semiSep : {c : Bool} -> Grammar c a -> Grammar False (List a)
|
||
semiSep = sepEndBy (res ";")
|
||
|
||
export
|
||
commaSep1 : {c : Bool} -> Grammar c a -> Grammar c (List1 a)
|
||
commaSep1 = sepEndBy1 (res ",")
|
||
|
||
export
|
||
darr : Grammar True ()
|
||
darr = resC "⇒"
|
||
|
||
|
||
export
|
||
name : Grammar True Name
|
||
name = terminal "expecting name" $
|
||
\case I i => Just i; _ => Nothing
|
||
|
||
export
|
||
baseName : Grammar True BaseName
|
||
baseName = terminal "expecting unqualified name" $
|
||
\case I i => guard (null i.mods) $> i.base
|
||
_ => Nothing
|
||
|
||
export
|
||
nat : Grammar True Nat
|
||
nat = terminal "expecting natural number" $
|
||
\case N n => pure n; _ => Nothing
|
||
|
||
export
|
||
string : Grammar True String
|
||
string = terminal "expecting string literal" $
|
||
\case S s => pure s; _ => Nothing
|
||
|
||
export
|
||
tag : Grammar True String
|
||
tag = terminal "expecting tag constructor" $
|
||
\case T t => pure t; _ => Nothing
|
||
|
||
export
|
||
bareTag : Grammar True String
|
||
bareTag = string <|> [|toDots name|]
|
||
|
||
export
|
||
universe : Grammar True PUniverse
|
||
universe = terminal "expecting type universe" $
|
||
\case TYPE u => Just u; _ => Nothing
|
||
|
||
export
|
||
bname : Grammar True BName
|
||
bname = Nothing <$ res "_"
|
||
<|> [|Just baseName|]
|
||
|
||
export
|
||
zeroOne : (zero, one : a) -> Grammar True a
|
||
zeroOne zero one = terminal "expecting zero or one" $
|
||
\case N 0 => Just zero; N 1 => Just one; _ => Nothing
|
||
|
||
|
||
export covering
|
||
qty : Grammar True PQty
|
||
qty = zeroOne Zero One
|
||
<|> Any <$ res "ω"
|
||
<|> parens qty
|
||
|
||
private covering
|
||
qtys : Grammar False (List PQty)
|
||
qtys = option [] [|toList $ some qty <* res "·"|]
|
||
|
||
export
|
||
dimConst : Grammar True DimConst
|
||
dimConst = zeroOne Zero One
|
||
|
||
export covering
|
||
dim : Grammar True PDim
|
||
dim = [|V baseName|]
|
||
<|> [|K dimConst|]
|
||
<|> parens dim
|
||
|
||
private
|
||
0 PBinderHead : Nat -> Type
|
||
PBinderHead n = (Vect n PQty, BName, PTerm)
|
||
|
||
private
|
||
toVect : List a -> (n ** Vect n a)
|
||
toVect [] = (_ ** [])
|
||
toVect (x :: xs) = (_ ** x :: snd (toVect xs))
|
||
|
||
private
|
||
0 MakeBinder : Nat -> Type
|
||
MakeBinder n = (String, PBinderHead n -> PTerm -> PTerm)
|
||
|
||
private
|
||
makePi : MakeBinder 1
|
||
makePi = ("→", \([pi], x, s) => Pi pi x s)
|
||
|
||
private
|
||
makeSig : MakeBinder 0
|
||
makeSig = ("×", \([], x, s) => Sig x s)
|
||
|
||
private
|
||
plural : Nat -> a -> a -> a
|
||
plural 1 s p = s
|
||
plural _ s p = p
|
||
|
||
private
|
||
makeBinder : {m, n : Nat} -> MakeBinder m -> PBinderHead n -> PTerm ->
|
||
Grammar False PTerm
|
||
makeBinder (str, f) h t =
|
||
case decEq m n of
|
||
Yes Refl => pure $ f h t
|
||
No _ => fatalError
|
||
"'\{str}' expects \{show m} quantit\{plural m "y" "ies"}, got \{show n}"
|
||
|
||
private
|
||
binderInfix : Grammar True (n ** MakeBinder n)
|
||
binderInfix = res "→" $> (1 ** makePi)
|
||
<|> res "×" $> (0 ** makeSig)
|
||
|
||
private
|
||
lamIntro : Grammar True (BName -> PTerm -> PTerm)
|
||
lamIntro = Lam <$ resC "λ"
|
||
<|> DLam <$ resC "δ"
|
||
|
||
private covering
|
||
caseIntro : Grammar True PQty
|
||
caseIntro = resC "case1" $> One
|
||
<|> resC "caseω" $> Any
|
||
<|> resC "case" *> qty <* resC "·"
|
||
|
||
private
|
||
optNameBinder : Grammar False BName
|
||
optNameBinder = [|join $ optional $ bname <* darr|]
|
||
|
||
mutual
|
||
export covering
|
||
term : Grammar True PTerm
|
||
term = lamTerm
|
||
<|> caseTerm
|
||
<|> bindTerm
|
||
<|> [|annotate infixEqTerm (optional $ resC "∷" *> term)|]
|
||
|
||
private covering
|
||
lamTerm : Grammar True PTerm
|
||
lamTerm = flip . foldr <$> lamIntro <*> some bname <* darr <*> term
|
||
|
||
private covering
|
||
caseTerm : Grammar True PTerm
|
||
caseTerm =
|
||
[|Case caseIntro term
|
||
(resC "return" *> optBinderTerm)
|
||
(resC "of" *> braces caseBody)|]
|
||
|
||
private covering
|
||
caseBody : Grammar False PCaseBody
|
||
caseBody = [|CasePair (pairPat <* darr) (term <* optSemi)|]
|
||
<|> [|CaseEnum $ semiSep [|MkPair tag (darr *> term)|]|]
|
||
where
|
||
optSemi = ignore $ optional $ res ";"
|
||
pairPat = parens [|MkPair bname (resC "," *> bname)|]
|
||
|
||
private covering
|
||
bindTerm : Grammar True PTerm
|
||
bindTerm = do
|
||
bnd <- binderHead
|
||
inf <- binderInfix
|
||
body <- term
|
||
makeBinder (snd inf) (snd bnd) body
|
||
|
||
private covering
|
||
infixEqTerm : Grammar True PTerm
|
||
infixEqTerm = do
|
||
l <- appTerm
|
||
rty <- optional [|MkPair (resC "≡" *> term) (resC ":" *> appTerm)|]
|
||
pure $ maybe l (\rty => Eq (Nothing, snd rty) l (fst rty)) rty
|
||
|
||
private covering
|
||
appTerm : Grammar True PTerm
|
||
appTerm = resC "★" *> [|TYPE nat|]
|
||
<|> resC "Eq" *> [|Eq (bracks optBinderTerm) aTerm aTerm|]
|
||
<|> [|apply aTerm (many appArg)|]
|
||
|
||
private covering
|
||
appArg : Grammar True PArg
|
||
appArg = [|D $ resC "@" *> dim|]
|
||
<|> [|T aTerm|]
|
||
|
||
private covering
|
||
aTerm : Grammar True PTerm
|
||
aTerm = [|Enum $ braces $ commaSep bareTag|]
|
||
<|> [|TYPE universe|]
|
||
<|> [|V name|]
|
||
<|> [|Tag tag|]
|
||
<|> foldr1 Pair <$> parens (commaSep1 term)
|
||
|
||
private covering
|
||
binderHead : Grammar True (n ** PBinderHead n)
|
||
binderHead = parens {commit = False} $ do
|
||
qs <- [|toVect qtys|]
|
||
name <- bname
|
||
resC ":"
|
||
ty <- term
|
||
pure (_ ** (qs.snd, name, ty))
|
||
|
||
private covering
|
||
optBinderTerm : Grammar True (BName, PTerm)
|
||
optBinderTerm = [|MkPair optNameBinder term|]
|