more parser/FromParser stuff
- top level semicolons optional - type optional [the def will need to be an elim] - `load` statement - namespaces
This commit is contained in:
parent
cd63eb2c67
commit
c81aabcc14
10 changed files with 716 additions and 538 deletions
212
lib/Quox/Parser/FromParser.idr
Normal file
212
lib/Quox/Parser/FromParser.idr
Normal file
|
|
@ -0,0 +1,212 @@
|
|||
||| take freshly-parsed input, translate it to core, and check it
|
||||
module Quox.Parser.FromParser
|
||||
|
||||
import Quox.Parser.Syntax
|
||||
import Quox.Typechecker
|
||||
import Data.List
|
||||
|
||||
import public Control.Monad.Either
|
||||
import public Control.Monad.State
|
||||
import public Control.Monad.Reader
|
||||
|
||||
|
||||
public export
|
||||
data FromParserError =
|
||||
AnnotationNeeded PTerm
|
||||
| DuplicatesInEnum (List TagVal)
|
||||
| DimNotInScope PBaseName
|
||||
| QtyNotGlobal PQty
|
||||
| DimNameInTerm PBaseName
|
||||
|
||||
public export
|
||||
interface LoadFile m where
|
||||
loadFile : (file : String) -> m PTopLevel
|
||||
|
||||
public export
|
||||
0 CanError : (Type -> Type) -> Type
|
||||
CanError = MonadError FromParserError
|
||||
|
||||
public export
|
||||
0 HasNamespace : (Type -> Type) -> Type
|
||||
HasNamespace = MonadReader Mods
|
||||
|
||||
public export
|
||||
0 HasSeenFiles : (Type -> Type) -> Type
|
||||
HasSeenFiles = MonadState (SortedSet String)
|
||||
|
||||
public export
|
||||
0 FromParser : (Type -> Type) -> Type
|
||||
FromParser m = (CanError m, HasNamespace m, HasSeenFiles m)
|
||||
|
||||
|
||||
|
||||
parameters {auto _ : Functor m} (b : Var n -> m a) (f : PName -> m a)
|
||||
(xs : Context' BName n)
|
||||
private
|
||||
fromBaseName : PBaseName -> m a
|
||||
fromBaseName x = maybe (f $ MakePName [<] x) b $ Context.find (== Just x) xs
|
||||
|
||||
private
|
||||
fromName : PName -> m a
|
||||
fromName x = if null x.mods then fromBaseName x.base else f x
|
||||
|
||||
export
|
||||
fromPDimWith : CanError m =>
|
||||
Context' BName d -> PDim -> m (Dim d)
|
||||
fromPDimWith ds (K e) = pure $ K e
|
||||
fromPDimWith ds (V i) =
|
||||
fromBaseName (pure . B) (const $ throwError $ DimNotInScope i) ds i
|
||||
|
||||
private
|
||||
avoidDim : CanError m => Context' BName d -> PName -> m (Term q d n)
|
||||
avoidDim ds x =
|
||||
fromName (const $ throwError $ DimNameInTerm x.base)
|
||||
(pure . FT . fromPName) ds x
|
||||
|
||||
|
||||
mutual
|
||||
export
|
||||
fromPTermWith : CanError m =>
|
||||
Context' BName d -> Context' BName n ->
|
||||
PTerm -> m (Term Three d n)
|
||||
fromPTermWith ds ns t0 = case t0 of
|
||||
TYPE k =>
|
||||
pure $ TYPE $ k
|
||||
|
||||
Pi pi x s t =>
|
||||
Pi pi <$> fromPTermWith ds ns s
|
||||
<*> fromPTermTScope ds ns [x] t
|
||||
|
||||
Lam x s =>
|
||||
Lam <$> fromPTermTScope ds ns [x] s
|
||||
|
||||
s :@ t =>
|
||||
map E $ (:@) <$> fromPTermElim ds ns s <*> fromPTermWith ds ns t
|
||||
|
||||
Sig x s t =>
|
||||
Sig <$> fromPTermWith ds ns s <*> fromPTermTScope ds ns [x] t
|
||||
|
||||
Pair s t =>
|
||||
Pair <$> fromPTermWith ds ns s <*> fromPTermWith ds ns t
|
||||
|
||||
Case pi pair (r, ret) (CasePair (x, y) body) =>
|
||||
map E $ Base.CasePair pi
|
||||
<$> fromPTermElim ds ns pair
|
||||
<*> fromPTermTScope ds ns [r] ret
|
||||
<*> fromPTermTScope ds ns [x, y] body
|
||||
|
||||
Case pi tag (r, ret) (CaseEnum arms) =>
|
||||
map E $ Base.CaseEnum pi
|
||||
<$> fromPTermElim ds ns tag
|
||||
<*> fromPTermTScope ds ns [r] ret
|
||||
<*> assert_total fromPTermEnumArms ds ns arms
|
||||
|
||||
Enum strs =>
|
||||
let set = SortedSet.fromList strs in
|
||||
if length strs == length (SortedSet.toList set) then
|
||||
pure $ Enum set
|
||||
else
|
||||
throwError $ DuplicatesInEnum strs
|
||||
|
||||
Tag str => pure $ Tag str
|
||||
|
||||
Eq (i, ty) s t =>
|
||||
Eq <$> fromPTermDScope ds ns [i] ty
|
||||
<*> fromPTermWith ds ns s
|
||||
<*> fromPTermWith ds ns t
|
||||
|
||||
DLam i s =>
|
||||
DLam <$> fromPTermDScope ds ns [i] s
|
||||
|
||||
s :% p =>
|
||||
map E $ (:%) <$> fromPTermElim ds ns s <*> fromPDimWith ds p
|
||||
|
||||
V x =>
|
||||
fromName (pure . E . B) (avoidDim ds) ns x
|
||||
|
||||
s :# a =>
|
||||
map E $ (:#) <$> fromPTermWith ds ns s <*> fromPTermWith ds ns a
|
||||
|
||||
private
|
||||
fromPTermEnumArms : CanError m =>
|
||||
Context' BName d -> Context' BName n ->
|
||||
List (TagVal, PTerm) -> m (CaseEnumArms Three d n)
|
||||
fromPTermEnumArms ds ns =
|
||||
map SortedMap.fromList . traverse (traverse $ fromPTermWith ds ns)
|
||||
|
||||
private
|
||||
fromPTermElim : CanError m =>
|
||||
Context' BName d -> Context' BName n ->
|
||||
PTerm -> m (Elim Three d n)
|
||||
fromPTermElim ds ns e =
|
||||
case !(fromPTermWith ds ns e) of
|
||||
E e => pure e
|
||||
_ => throwError $ AnnotationNeeded e
|
||||
|
||||
-- [todo] use SN if the var is named but still unused
|
||||
private
|
||||
fromPTermTScope : {s : Nat} -> CanError m =>
|
||||
Context' BName d -> Context' BName n ->
|
||||
Vect s BName ->
|
||||
PTerm -> m (ScopeTermN s Three d n)
|
||||
fromPTermTScope ds ns xs t =
|
||||
if all isNothing xs then
|
||||
SN <$> fromPTermWith ds ns t
|
||||
else
|
||||
SY (map (maybe Unused UN) xs) <$> fromPTermWith ds (ns <>< xs) t
|
||||
|
||||
private
|
||||
fromPTermDScope : {s : Nat} -> CanError m =>
|
||||
Context' BName d -> Context' BName n ->
|
||||
Vect s BName ->
|
||||
PTerm -> m (DScopeTermN s Three d n)
|
||||
fromPTermDScope ds ns xs t =
|
||||
if all isNothing xs then
|
||||
SN <$> fromPTermWith ds ns t
|
||||
else
|
||||
SY (map (maybe Unused UN) xs) <$> fromPTermWith (ds <>< xs) ns t
|
||||
|
||||
|
||||
export %inline
|
||||
fromPTerm : CanError m => PTerm -> m (Term Three 0 0)
|
||||
fromPTerm = fromPTermWith [<] [<]
|
||||
|
||||
|
||||
export
|
||||
globalPQty : CanError m => (q : PQty) -> m (IsGlobal q)
|
||||
globalPQty pi = case isGlobal pi of
|
||||
Yes y => pure y
|
||||
No n => throwError $ QtyNotGlobal pi
|
||||
|
||||
|
||||
|
||||
-- -- [todo] extend substitutions so they can do this injection. that's the sort of
|
||||
-- -- thing they are for.
|
||||
-- export
|
||||
-- fromPDefinition : FromParser m => PDefinition -> m (Name, Definition Three)
|
||||
-- fromPDefinition (MkPDef {name, qty, type, term}) =
|
||||
-- pure (addMods !ask $ fromPName name, MkDef' {
|
||||
-- qty, qtyGlobal = !(globalPQty qty),
|
||||
-- type = T $ inject !(fromPTerm type),
|
||||
-- term = Just $ T $ inject !(fromPTerm term)
|
||||
-- })
|
||||
|
||||
|
||||
-- export
|
||||
-- fromPDecl : FromParser m => PDecl -> m (List (Name, Definition Three))
|
||||
-- fromPDecl (PDef def) = singleton <$> fromPDefinition def
|
||||
-- fromPDecl (PNs ns) = local (<+> ns.name) $
|
||||
-- concat <$> assert_total traverse fromPDecl ns.decls
|
||||
|
||||
|
||||
-- export covering
|
||||
-- fromPTopLevel : (FromParser m, LoadFile m) =>
|
||||
-- PTopLevel -> m (List (Name, Definition Three))
|
||||
-- fromPTopLevel (PD decl) = fromPDecl decl
|
||||
-- fromPTopLevel (PLoad file) =
|
||||
-- if contains file !get then
|
||||
-- pure []
|
||||
-- else do
|
||||
-- modify $ insert file
|
||||
-- t <- loadFile file
|
||||
-- fromPTopLevel t
|
||||
257
lib/Quox/Parser/Lexer.idr
Normal file
257
lib/Quox/Parser/Lexer.idr
Normal file
|
|
@ -0,0 +1,257 @@
|
|||
module Quox.Parser.Lexer
|
||||
|
||||
import Quox.CharExtra
|
||||
import Quox.Name
|
||||
import Data.String.Extra
|
||||
import Data.SortedMap
|
||||
import public Data.String -- for singleton to reduce in IsReserved
|
||||
import public Data.List.Elem
|
||||
import public Text.Lexer
|
||||
import public Text.Lexer.Tokenizer
|
||||
import Derive.Prelude
|
||||
%hide TT.Name
|
||||
|
||||
|
||||
%default total
|
||||
%language ElabReflection
|
||||
|
||||
|
||||
||| @ Reserved reserved token
|
||||
||| @ Name name, possibly qualified
|
||||
||| @ Nat nat literal
|
||||
||| @ String string literal
|
||||
||| @ Tag tag literal
|
||||
||| @ TYPE "Type" or "★" with subscript
|
||||
public export
|
||||
data Token =
|
||||
Reserved String
|
||||
| Name PName
|
||||
| Nat Nat
|
||||
| Str String
|
||||
| Tag String
|
||||
| TYPE Nat
|
||||
%runElab derive "Token" [Eq, Ord, Show]
|
||||
|
||||
-- token or whitespace
|
||||
public export
|
||||
0 TokenW : Type
|
||||
TokenW = Maybe Token
|
||||
|
||||
|
||||
public export
|
||||
record Error where
|
||||
constructor Err
|
||||
reason : StopReason
|
||||
line, col : Int
|
||||
||| `Nothing` if the error is at the end of the input
|
||||
char : Maybe Char
|
||||
%runElab derive "StopReason" [Eq, Ord, Show]
|
||||
%runElab derive "Error" [Eq, Ord, Show]
|
||||
|
||||
|
||||
private
|
||||
skip : Lexer -> Tokenizer TokenW
|
||||
skip t = match t $ const Nothing
|
||||
|
||||
private
|
||||
match : Lexer -> (String -> Token) -> Tokenizer TokenW
|
||||
match t f = Tokenizer.match t (Just . f)
|
||||
%hide Tokenizer.match
|
||||
|
||||
|
||||
export %inline
|
||||
syntaxChars : List Char
|
||||
syntaxChars = ['(', ')', '[', ']', '{', '}', '"', '\'', ',', '.', ';']
|
||||
|
||||
private
|
||||
stra, isSymCont : Char -> Bool
|
||||
isSymStart c = not (c `elem` syntaxChars) && isSymChar c
|
||||
isSymCont c = c == '\'' || isSymStart c
|
||||
|
||||
private
|
||||
idStart, idCont, idEnd, idContEnd : Lexer
|
||||
idStart = pred isIdStart
|
||||
idCont = pred isIdCont
|
||||
idEnd = pred $ \c => c `elem` unpack "?!#"
|
||||
idContEnd = idCont <|> idEnd
|
||||
|
||||
private
|
||||
symStart, symCont : Lexer
|
||||
symStart = pred isSymStart
|
||||
symCont = pred isSymCont
|
||||
|
||||
private
|
||||
baseNameL : Lexer
|
||||
baseNameL = idStart <+> many idCont <+> many idEnd
|
||||
<|> symStart <+> many symCont
|
||||
|
||||
private
|
||||
nameL : Lexer
|
||||
nameL = baseNameL <+> many (is '.' <+> baseNameL)
|
||||
|
||||
private
|
||||
name : Tokenizer TokenW
|
||||
name = match nameL $ Name . fromListP . split (== '.') . normalizeNfc
|
||||
|
||||
||| [todo] escapes other than `\"` and (accidentally) `\\`
|
||||
export
|
||||
fromStringLit : String -> String
|
||||
fromStringLit = pack . go . unpack . drop 1 . dropLast 1 where
|
||||
go : List Char -> List Char
|
||||
go [] = []
|
||||
go ['\\'] = ['\\'] -- i guess???
|
||||
go ('\\' :: c :: cs) = c :: go cs
|
||||
go (c :: cs) = c :: go cs
|
||||
|
||||
private
|
||||
string : Tokenizer TokenW
|
||||
string = match stringLit (Str . fromStringLit)
|
||||
|
||||
private
|
||||
nat : Tokenizer TokenW
|
||||
nat = match (some (range '0' '9')) (Nat . cast)
|
||||
|
||||
private
|
||||
tag : Tokenizer TokenW
|
||||
tag = match (is '\'' <+> nameL) (Tag . drop 1)
|
||||
<|> match (is '\'' <+> stringLit) (Tag . fromStringLit . drop 1)
|
||||
|
||||
|
||||
|
||||
private %inline
|
||||
fromSub : Char -> Char
|
||||
fromSub c = case c of
|
||||
'₀' => '0'; '₁' => '1'; '₂' => '2'; '₃' => '3'; '₄' => '4'
|
||||
'₅' => '5'; '₆' => '6'; '₇' => '7'; '₈' => '8'; '₉' => '9'; _ => c
|
||||
|
||||
private %inline
|
||||
subToNat : String -> Nat
|
||||
subToNat = cast . pack . map fromSub . unpack
|
||||
|
||||
|
||||
private
|
||||
universe : Tokenizer TokenW
|
||||
universe = universeWith "★" <|> universeWith "Type" where
|
||||
universeWith : String -> Tokenizer TokenW
|
||||
universeWith pfx =
|
||||
let len = length pfx in
|
||||
match (exact pfx <+> some (range '0' '9'))
|
||||
(TYPE . cast . drop len) <|>
|
||||
match (exact pfx <+> some (range '₀' '₉'))
|
||||
(TYPE . subToNat . drop len)
|
||||
|
||||
|
||||
private %inline
|
||||
choice : (xs : List (Tokenizer a)) -> (0 _ : NonEmpty xs) => Tokenizer a
|
||||
choice (t :: ts) = foldl (\a, b => a <|> b) t ts
|
||||
|
||||
|
||||
namespace Reserved
|
||||
||| description of a reserved symbol
|
||||
||| @ Word a reserved word (must not be followed by letters, digits, etc)
|
||||
||| @ Sym a reserved symbol (must not be followed by symbolic chars)
|
||||
||| @ Punc a character that doesn't show up in names (brackets, etc)
|
||||
public export
|
||||
data Reserved1 = Word String | Sym String | Punc Char
|
||||
%runElab derive "Reserved1" [Eq, Ord, Show]
|
||||
|
||||
||| description of a token that might have unicode & ascii-only aliases
|
||||
public export
|
||||
data Reserved = Only Reserved1 | Or Reserved1 Reserved1
|
||||
%runElab derive "Reserved" [Eq, Ord, Show]
|
||||
|
||||
public export
|
||||
Sym1, Word1 : String -> Reserved
|
||||
Sym1 = Only . Sym
|
||||
Word1 = Only . Word
|
||||
|
||||
public export
|
||||
Punc1 : Char -> Reserved
|
||||
Punc1 = Only . Punc
|
||||
|
||||
public export
|
||||
resString1 : Reserved1 -> String
|
||||
resString1 (Punc x) = singleton x
|
||||
resString1 (Word w) = w
|
||||
resString1 (Sym s) = s
|
||||
|
||||
||| return the representative string for a token description. if there are
|
||||
||| two, then it's the first one, which should be the full-unicode one
|
||||
public export
|
||||
resString : Reserved -> String
|
||||
resString (Only r) = resString1 r
|
||||
resString (r `Or` _) = resString1 r
|
||||
|
||||
private
|
||||
resTokenizer1 : Reserved1 -> String -> Tokenizer TokenW
|
||||
resTokenizer1 r str =
|
||||
let res : String -> Token := const $ Reserved str in
|
||||
case r of Word w => match (exact w <+> reject idContEnd) res
|
||||
Sym s => match (exact s <+> reject symCont) res
|
||||
Punc x => match (is x) res
|
||||
|
||||
||| match a reserved token
|
||||
export
|
||||
resTokenizer : Reserved -> Tokenizer TokenW
|
||||
resTokenizer (Only r) = resTokenizer1 r (resString1 r)
|
||||
resTokenizer (r `Or` s) =
|
||||
resTokenizer1 r (resString1 r) <|> resTokenizer1 s (resString1 r)
|
||||
|
||||
||| reserved words & symbols.
|
||||
||| the tokens recognised by ``a `Or` b`` will be `Reserved a`.
|
||||
||| e.g. `=>` in the input (if not part of a longer name)
|
||||
||| will be returned as `Reserved "⇒"`.
|
||||
public export
|
||||
reserved : List Reserved
|
||||
reserved =
|
||||
[Punc1 '(', Punc1 ')', Punc1 '[', Punc1 ']', Punc1 '{', Punc1 '}',
|
||||
Punc1 ',', Punc1 ';',
|
||||
Sym1 "@",
|
||||
Sym1 ":",
|
||||
Sym "⇒" `Or` Sym "=>",
|
||||
Sym "→" `Or` Sym "->",
|
||||
Sym "×" `Or` Sym "**",
|
||||
Sym "≡" `Or` Sym "==",
|
||||
Sym "∷" `Or` Sym "::",
|
||||
Sym "·" `Or` Punc '.',
|
||||
Word1 "case",
|
||||
Word1 "case1",
|
||||
Word "caseω" `Or` Word "case#",
|
||||
Word1 "return",
|
||||
Word1 "of",
|
||||
Word1 "_",
|
||||
Word1 "Eq",
|
||||
Word "λ" `Or` Word "fun",
|
||||
Word "δ" `Or` Word "dfun",
|
||||
Word "ω" `Or` Sym "#",
|
||||
Sym "★" `Or` Word "Type",
|
||||
Word1 "def",
|
||||
Word1 "def0",
|
||||
Word "defω" `Or` Word "def#",
|
||||
Sym "≔" `Or` Sym ":=",
|
||||
Word1 "load",
|
||||
Word1 "namespace"]
|
||||
|
||||
||| `IsReserved str` is true if `Reserved str` might actually show up in
|
||||
||| the token stream
|
||||
public export
|
||||
IsReserved : String -> Type
|
||||
IsReserved str = str `Elem` map resString reserved
|
||||
|
||||
export
|
||||
tokens : Tokenizer TokenW
|
||||
tokens = choice $
|
||||
map skip [pred isWhitespace,
|
||||
lineComment (exact "--" <+> reject symCont),
|
||||
blockComment (exact "{-") (exact "-}")] <+>
|
||||
[universe] <+> -- ★ᵢ takes precedence over bare ★
|
||||
map resTokenizer reserved <+>
|
||||
[nat, string, tag, name]
|
||||
|
||||
export
|
||||
lex : String -> Either Error (List (WithBounds Token))
|
||||
lex str =
|
||||
let (res, reason, line, col, str) = lex tokens str in
|
||||
case reason of
|
||||
EndInput => Right $ mapMaybe sequence res
|
||||
_ => Left $ Err {reason, line, col, char = index 0 str}
|
||||
328
lib/Quox/Parser/Parser.idr
Normal file
328
lib/Quox/Parser/Parser.idr
Normal file
|
|
@ -0,0 +1,328 @@
|
|||
module Quox.Parser.Parser
|
||||
|
||||
import public Quox.Parser.Lexer
|
||||
import public Quox.Parser.Syntax
|
||||
|
||||
import Data.Fin
|
||||
import Data.Vect
|
||||
import public Text.Parser
|
||||
|
||||
%default total
|
||||
|
||||
|
||||
public export
|
||||
0 Grammar : Bool -> Type -> Type
|
||||
Grammar = Core.Grammar () Token
|
||||
%hide Core.Grammar
|
||||
|
||||
|
||||
export
|
||||
res : (str : String) -> (0 _ : IsReserved str) => Grammar True ()
|
||||
res str = terminal "expecting \"\{str}\"" $
|
||||
\x => guard $ x == Reserved 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 PName
|
||||
name = terminal "expecting name" $
|
||||
\case Name i => Just i; _ => Nothing
|
||||
|
||||
export
|
||||
mods : Grammar True Mods
|
||||
mods = name <&> \n => n.mods :< n.base
|
||||
|
||||
export
|
||||
baseName : Grammar True String
|
||||
baseName = terminal "expecting unqualified name" $
|
||||
\case Name i => guard (null i.mods) $> i.base
|
||||
_ => Nothing
|
||||
|
||||
export
|
||||
nat : Grammar True Nat
|
||||
nat = terminal "expecting natural number" $
|
||||
\case Nat n => pure n; _ => Nothing
|
||||
|
||||
export
|
||||
string : Grammar True String
|
||||
string = terminal "expecting string literal" $
|
||||
\case Str s => pure s; _ => Nothing
|
||||
|
||||
export
|
||||
tag : Grammar True String
|
||||
tag = terminal "expecting tag constructor" $
|
||||
\case Tag t => pure t; _ => Nothing
|
||||
|
||||
export
|
||||
bareTag : Grammar True String
|
||||
bareTag = string <|> [|toDotsP 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 Nat 0 => Just zero; Nat 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
|
||||
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 _ =>
|
||||
let q = if m == 1 then "quantity" else "quantities" in
|
||||
fatalError "'\{str}' expects \{show m} \{q}, 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)|]
|
||||
where
|
||||
annotate : PTerm -> Maybe PTerm -> PTerm
|
||||
annotate s a = maybe s (s :#) a
|
||||
|
||||
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)|]
|
||||
where
|
||||
data PArg = TermArg PTerm | DimArg PDim
|
||||
|
||||
appArg : Grammar True PArg
|
||||
appArg = [|DimArg $ resC "@" *> dim|]
|
||||
<|> [|TermArg aTerm|]
|
||||
|
||||
apply : PTerm -> List PArg -> PTerm
|
||||
apply = foldl apply1 where
|
||||
apply1 : PTerm -> PArg -> PTerm
|
||||
apply1 f (TermArg x) = f :@ x
|
||||
apply1 f (DimArg p) = f :% p
|
||||
|
||||
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.fst ** (qs.snd, name, ty))
|
||||
|
||||
private covering
|
||||
optBinderTerm : Grammar True (BName, PTerm)
|
||||
optBinderTerm = [|MkPair optNameBinder term|]
|
||||
|
||||
|
||||
export covering
|
||||
defIntro : Grammar True PQty
|
||||
defIntro = Zero <$ resC "def0"
|
||||
<|> Any <$ resC "defω"
|
||||
<|> resC "def" *> option Any (qty <* resC "·")
|
||||
|
||||
export covering
|
||||
definition : Grammar True PDefinition
|
||||
definition =
|
||||
[|MkPDef defIntro name
|
||||
(optional (resC ":" *> term))
|
||||
(resC "≔" *> term)|]
|
||||
|
||||
export
|
||||
load : Grammar True String
|
||||
load = resC "load" *> string
|
||||
|
||||
mutual
|
||||
export covering
|
||||
namespace_ : Grammar True PNamespace
|
||||
namespace_ =
|
||||
[|MkPNamespace (resC "namespace" *> mods) (braces $ many decl)|]
|
||||
|
||||
export covering
|
||||
decl : Grammar True PDecl
|
||||
decl = [|PDef definition|]
|
||||
<|> [|PNs namespace_|]
|
||||
|
||||
export covering
|
||||
topLevel : Grammar True PTopLevel
|
||||
topLevel = [|PLoad load|]
|
||||
<|> [|PD decl|]
|
||||
|
||||
export covering
|
||||
input : Grammar False (List PTopLevel)
|
||||
input = skipSemis *> many (topLevel <* skipSemis)
|
||||
where skipSemis = ignore $ many $ resC ";"
|
||||
|
||||
|
||||
public export
|
||||
data Error =
|
||||
LexError Lexer.Error
|
||||
| ParseError (List1 (ParsingError Token))
|
||||
%hide Lexer.Error
|
||||
|
||||
export
|
||||
lexParseWith : {c : Bool} -> Grammar c a -> String -> Either Error a
|
||||
lexParseWith grm input = do
|
||||
toks <- mapFst LexError $ lex input
|
||||
bimap ParseError fst $ parse (grm <* eof) toks
|
||||
|
||||
export covering %inline
|
||||
lexParseInput : String -> Either Error (List PTopLevel)
|
||||
lexParseInput = lexParseWith input
|
||||
|
||||
export covering %inline
|
||||
lexParseTerm : String -> Either Error PTerm
|
||||
lexParseTerm = lexParseWith term
|
||||
|
|
@ -4,8 +4,6 @@ import public Quox.Syntax
|
|||
import public Quox.Syntax.Qty.Three
|
||||
import public Quox.Definition
|
||||
|
||||
import public Control.Monad.Either
|
||||
|
||||
import Derive.Prelude
|
||||
%hide TT.Name
|
||||
|
||||
|
|
@ -15,7 +13,7 @@ import Derive.Prelude
|
|||
|
||||
public export
|
||||
0 BName : Type
|
||||
BName = Maybe BaseName
|
||||
BName = Maybe String
|
||||
|
||||
public export
|
||||
0 PUniverse : Type
|
||||
|
|
@ -27,7 +25,7 @@ PQty = Three
|
|||
|
||||
namespace PDim
|
||||
public export
|
||||
data PDim = K DimConst | V BaseName
|
||||
data PDim = K DimConst | V PBaseName
|
||||
%name PDim p, q
|
||||
%runElab derive "PDim" [Eq, Ord, Show]
|
||||
|
||||
|
|
@ -53,7 +51,7 @@ namespace PTerm
|
|||
| DLam BName PTerm
|
||||
| (:%) PTerm PDim
|
||||
|
||||
| V Name
|
||||
| V PName
|
||||
| (:#) PTerm PTerm
|
||||
%name PTerm s, t
|
||||
|
||||
|
|
@ -70,15 +68,35 @@ public export
|
|||
record PDefinition where
|
||||
constructor MkPDef
|
||||
qty : PQty
|
||||
name : Name
|
||||
type : PTerm
|
||||
name : PName
|
||||
type : Maybe PTerm
|
||||
term : PTerm
|
||||
%name PDefinition def
|
||||
%runElab derive "PDefinition" [Eq, Ord, Show]
|
||||
|
||||
mutual
|
||||
public export
|
||||
record PNamespace where
|
||||
constructor MkPNamespace
|
||||
name : Mods
|
||||
decls : List PDecl
|
||||
%name PNamespace ns
|
||||
|
||||
public export
|
||||
data PDecl =
|
||||
PDef PDefinition
|
||||
| PNs PNamespace
|
||||
%name PDecl decl
|
||||
%runElab deriveMutual ["PNamespace", "PDecl"] [Eq, Ord, Show]
|
||||
|
||||
public export
|
||||
data PTopLevel = PD PDecl | PLoad String
|
||||
%name PTopLevel t
|
||||
%runElab derive "PTopLevel" [Eq, Ord, Show]
|
||||
|
||||
|
||||
export
|
||||
toPDimWith : Context' BaseName d -> Dim d -> PDim
|
||||
toPDimWith : Context' PBaseName d -> Dim d -> PDim
|
||||
toPDimWith ds (K e) = K e
|
||||
toPDimWith ds (B i) = V $ ds !!! i
|
||||
|
||||
|
|
@ -90,27 +108,30 @@ toPDim = toPDimWith [<]
|
|||
mutual
|
||||
namespace Term
|
||||
export
|
||||
toPTermWith : Context' BaseName d -> Context' BaseName n ->
|
||||
toPTermWith : Context' PBaseName d -> Context' PBaseName n ->
|
||||
Term Three d n -> PTerm
|
||||
toPTermWith ds ns t =
|
||||
let Element t _ = pushSubsts t in
|
||||
toPTermWith' ds ns t
|
||||
|
||||
private
|
||||
toPTermWith' : Context' BaseName d -> Context' BaseName n ->
|
||||
toPTermWith' : Context' PBaseName d -> Context' PBaseName n ->
|
||||
(t : Term Three d n) -> (0 _ : NotClo t) =>
|
||||
PTerm
|
||||
toPTermWith' ds ns s = case s of
|
||||
TYPE l =>
|
||||
TYPE l
|
||||
Pi qty arg (S [x] res) =>
|
||||
Pi qty (Just x) (toPTermWith ds ns arg)
|
||||
(toPTermWith ds (ns :< x) res.term)
|
||||
Pi qty (Just $ show x)
|
||||
(toPTermWith ds ns arg)
|
||||
(toPTermWith ds (ns :< baseStr x) res.term)
|
||||
Lam (S [x] body) =>
|
||||
Lam (Just x) $ toPTermWith ds (ns :< x) body.term
|
||||
Lam (Just $ show x) $
|
||||
toPTermWith ds (ns :< baseStr x) body.term
|
||||
Sig fst (S [x] snd) =>
|
||||
Sig (Just x) (toPTermWith ds ns fst)
|
||||
(toPTermWith ds (ns :< x) snd.term)
|
||||
Sig (Just $ show x)
|
||||
(toPTermWith ds ns fst)
|
||||
(toPTermWith ds (ns :< baseStr x) snd.term)
|
||||
Pair fst snd =>
|
||||
Pair (toPTermWith ds ns fst) (toPTermWith ds ns snd)
|
||||
Enum cases =>
|
||||
|
|
@ -118,40 +139,40 @@ mutual
|
|||
Tag tag =>
|
||||
Tag tag
|
||||
Eq (S [i] ty) l r =>
|
||||
Eq (Just i, toPTermWith (ds :< i) ns ty.term)
|
||||
Eq (Just $ show i, toPTermWith (ds :< baseStr i) ns ty.term)
|
||||
(toPTermWith ds ns l) (toPTermWith ds ns r)
|
||||
DLam (S [i] body) =>
|
||||
DLam (Just i) $ toPTermWith (ds :< i) ns body.term
|
||||
DLam (Just $ show i) $ toPTermWith (ds :< baseStr i) ns body.term
|
||||
E e =>
|
||||
toPTermWith ds ns e
|
||||
|
||||
namespace Elim
|
||||
export
|
||||
toPTermWith : Context' BaseName d -> Context' BaseName n ->
|
||||
toPTermWith : Context' PBaseName d -> Context' PBaseName n ->
|
||||
Elim Three d n -> PTerm
|
||||
toPTermWith ds ns e =
|
||||
let Element e _ = pushSubsts e in
|
||||
toPTermWith' ds ns e
|
||||
|
||||
private
|
||||
toPTermWith' : Context' BaseName d -> Context' BaseName n ->
|
||||
toPTermWith' : Context' PBaseName d -> Context' PBaseName n ->
|
||||
(e : Elim Three d n) -> (0 _ : NotClo e) =>
|
||||
PTerm
|
||||
toPTermWith' ds ns e = case e of
|
||||
F x =>
|
||||
V x
|
||||
V $ toPName x
|
||||
B i =>
|
||||
V $ unq $ ns !!! i
|
||||
V $ MakePName [<] $ ns !!! i
|
||||
fun :@ arg =>
|
||||
toPTermWith ds ns fun :@ toPTermWith ds ns arg
|
||||
CasePair qty pair (S [r] ret) (S [x, y] body) =>
|
||||
Case qty (toPTermWith ds ns pair)
|
||||
(Just r, toPTermWith ds (ns :< r) ret.term)
|
||||
(CasePair (Just x, Just y) $
|
||||
toPTermWith ds (ns :< x :< y) body.term)
|
||||
(Just $ show r, toPTermWith ds (ns :< baseStr r) ret.term)
|
||||
(CasePair (Just $ show x, Just $ show y) $
|
||||
toPTermWith ds (ns :< baseStr x :< baseStr y) body.term)
|
||||
CaseEnum qty tag (S [r] ret) arms =>
|
||||
Case qty (toPTermWith ds ns tag)
|
||||
(Just r, toPTermWith ds (ns :< r) ret.term)
|
||||
(Just $ show r, toPTermWith ds (ns :< baseStr r) ret.term)
|
||||
(CaseEnum $ mapSnd (toPTermWith ds ns) <$> SortedMap.toList arms)
|
||||
fun :% arg =>
|
||||
toPTermWith ds ns fun :% toPDimWith ds arg
|
||||
|
|
@ -167,172 +188,3 @@ namespace Elim
|
|||
export
|
||||
toPTerm : Elim Three 0 0 -> PTerm
|
||||
toPTerm = toPTermWith [<] [<]
|
||||
|
||||
|
||||
|
||||
public export
|
||||
data FromPTermError =
|
||||
AnnotationNeeded PTerm
|
||||
| DuplicatesInEnum (List TagVal)
|
||||
| DimNotInScope Name
|
||||
| QtyNotGlobal PQty
|
||||
| DimNameInTerm Name
|
||||
|
||||
public export
|
||||
FromPTerm : (Type -> Type) -> Type
|
||||
FromPTerm m = MonadError FromPTermError m
|
||||
|
||||
private
|
||||
extendVect : Telescope' a from to -> Vect n a -> Telescope' a from (n + to)
|
||||
extendVect tel [] = tel
|
||||
extendVect tel (x :: xs) {n = S n} =
|
||||
rewrite plusSuccRightSucc n to in
|
||||
extendVect (tel :< x) xs
|
||||
|
||||
|
||||
parameters {auto _ : FromPTerm m} (b : Var n -> m a) (f : Name -> m a)
|
||||
(xs : Context' BName n)
|
||||
private
|
||||
fromBaseName : BaseName -> m a
|
||||
fromBaseName x = maybe (f $ unq x) b $ Context.find (== Just x) xs
|
||||
|
||||
fromName : Name -> m a
|
||||
fromName x = if null x.mods then fromBaseName x.base else f x
|
||||
|
||||
export
|
||||
fromPDimWith : FromPTerm m =>
|
||||
Context' BName d -> PDim -> m (Dim d)
|
||||
fromPDimWith ds (K e) = pure $ K e
|
||||
fromPDimWith ds (V i) = fromBaseName (pure . B) (throwError . DimNotInScope) ds i
|
||||
|
||||
private
|
||||
avoidDim : FromPTerm m => Context' BName d -> Name -> m (Term q d n)
|
||||
avoidDim ds x =
|
||||
fromName (const $ throwError $ DimNameInTerm x) (pure . FT) ds x
|
||||
|
||||
|
||||
mutual
|
||||
export
|
||||
fromPTermWith : FromPTerm m =>
|
||||
Context' BName d -> Context' BName n ->
|
||||
PTerm -> m (Term Three d n)
|
||||
fromPTermWith ds ns t0 = case t0 of
|
||||
TYPE k =>
|
||||
pure $ TYPE $ k
|
||||
|
||||
Pi pi x s t =>
|
||||
Pi pi <$> fromPTermWith ds ns s
|
||||
<*> fromPTermTScope ds ns [x] t
|
||||
|
||||
Lam x s =>
|
||||
Lam <$> fromPTermTScope ds ns [x] s
|
||||
|
||||
s :@ t =>
|
||||
map E $ (:@) <$> fromPTermElim ds ns s <*> fromPTermWith ds ns t
|
||||
|
||||
Sig x s t =>
|
||||
Sig <$> fromPTermWith ds ns s <*> fromPTermTScope ds ns [x] t
|
||||
|
||||
Pair s t =>
|
||||
Pair <$> fromPTermWith ds ns s <*> fromPTermWith ds ns t
|
||||
|
||||
Case pi pair (r, ret) (CasePair (x, y) body) =>
|
||||
map E $ Base.CasePair pi
|
||||
<$> fromPTermElim ds ns pair
|
||||
<*> fromPTermTScope ds ns [r] ret
|
||||
<*> fromPTermTScope ds ns [x, y] body
|
||||
|
||||
Case pi tag (r, ret) (CaseEnum arms) =>
|
||||
map E $ Base.CaseEnum pi
|
||||
<$> fromPTermElim ds ns tag
|
||||
<*> fromPTermTScope ds ns [r] ret
|
||||
<*> assert_total fromPTermEnumArms ds ns arms
|
||||
|
||||
Enum strs =>
|
||||
let set = SortedSet.fromList strs in
|
||||
if length strs == length (SortedSet.toList set) then
|
||||
pure $ Enum set
|
||||
else
|
||||
throwError $ DuplicatesInEnum strs
|
||||
|
||||
Tag str => pure $ Tag str
|
||||
|
||||
Eq (i, ty) s t =>
|
||||
Eq <$> fromPTermDScope ds ns [i] ty
|
||||
<*> fromPTermWith ds ns s
|
||||
<*> fromPTermWith ds ns t
|
||||
|
||||
DLam i s =>
|
||||
DLam <$> fromPTermDScope ds ns [i] s
|
||||
|
||||
s :% p =>
|
||||
map E $ (:%) <$> fromPTermElim ds ns s <*> fromPDimWith ds p
|
||||
|
||||
V x =>
|
||||
fromName (pure . E . B) (avoidDim ds) ns x
|
||||
|
||||
s :# a =>
|
||||
map E $ (:#) <$> fromPTermWith ds ns s <*> fromPTermWith ds ns a
|
||||
|
||||
private
|
||||
fromPTermEnumArms : FromPTerm m =>
|
||||
Context' BName d -> Context' BName n ->
|
||||
List (TagVal, PTerm) -> m (CaseEnumArms Three d n)
|
||||
fromPTermEnumArms ds ns =
|
||||
map SortedMap.fromList . traverse (traverse $ fromPTermWith ds ns)
|
||||
|
||||
private
|
||||
fromPTermElim : FromPTerm m =>
|
||||
Context' BName d -> Context' BName n ->
|
||||
PTerm -> m (Elim Three d n)
|
||||
fromPTermElim ds ns e =
|
||||
case !(fromPTermWith ds ns e) of
|
||||
E e => pure e
|
||||
_ => throwError $ AnnotationNeeded e
|
||||
|
||||
-- [todo] use SN if the var is named but still unused
|
||||
private
|
||||
fromPTermTScope : {s : Nat} -> FromPTerm m =>
|
||||
Context' BName d -> Context' BName n ->
|
||||
Vect s BName ->
|
||||
PTerm -> m (ScopeTermN s Three d n)
|
||||
fromPTermTScope ds ns xs t =
|
||||
if all isNothing xs then
|
||||
SN <$> fromPTermWith ds ns t
|
||||
else
|
||||
SY (map (fromMaybe "_") xs) <$> fromPTermWith ds (extendVect ns xs) t
|
||||
|
||||
private
|
||||
fromPTermDScope : {s : Nat} -> FromPTerm m =>
|
||||
Context' BName d -> Context' BName n ->
|
||||
Vect s BName ->
|
||||
PTerm -> m (DScopeTermN s Three d n)
|
||||
fromPTermDScope ds ns xs t =
|
||||
if all isNothing xs then
|
||||
SN <$> fromPTermWith ds ns t
|
||||
else
|
||||
SY (map (fromMaybe "_") xs) <$> fromPTermWith (extendVect ds xs) ns t
|
||||
|
||||
|
||||
export %inline
|
||||
fromPTerm : FromPTerm m => PTerm -> m (Term Three 0 0)
|
||||
fromPTerm = fromPTermWith [<] [<]
|
||||
|
||||
|
||||
export
|
||||
globalPQty : FromPTerm m => (q : PQty) -> m (IsGlobal q)
|
||||
globalPQty pi = case isGlobal pi of
|
||||
Yes y => pure y
|
||||
No n => throwError $ QtyNotGlobal pi
|
||||
|
||||
|
||||
-- [todo] extend substitutions so they can do this injection. that's the sort of
|
||||
-- thing they are for.
|
||||
export
|
||||
fromPDefinition : FromPTerm m => PDefinition -> m (Name, Definition Three)
|
||||
fromPDefinition (MkPDef {name, qty, type, term}) =
|
||||
pure (name, MkDef' {
|
||||
qty, qtyGlobal = !(globalPQty qty),
|
||||
type = T $ inject !(fromPTerm type),
|
||||
term = Just $ T $ inject !(fromPTerm term)
|
||||
})
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue