dunham/newt
1
0
Fork 0
Code Issues Pull Requests Actions 1 Packages Projects Releases Wiki Activity

desugaring record implementation (TODO - dependency)

Browse Source
This commit is contained in:
Steve Dunham
2024-12-19 20:43:10 -08:00
parent 4289c5c6e8
commit f2c6b409fe
4 changed files with 84 additions and 25 deletions
Download Patch File Download Diff File Expand all files Collapse all files

1
TODO.md
View File

@@ -18,6 +18,7 @@ More comments in code! This is getting big enough that I need to re-find my bear
- need to flag internal functions to not search (or flag functions for search). I need to decide on syntax for this.
- for something like an `isEq` field in `Ord`, auto-search is picking up the function being defined.
- [ ] default implementations (use them if nothing is defined, where do we store them?) e.g. Ord compare, <, etc in Idris
- I may need to actually store some details on interfaces rather than reverse engineer from type.
- [x] syntax for negative integers
- [ ] White box tests in `test` directory
- [x] Put worker in iframe on safari

15
src/Lib/Parser.idr
View File

@@ -457,6 +457,19 @@ nakedBind = do
names <- some (withPos varname)
pure $ map (\(pos,name) => (BI pos name Explicit Many, RImplicit pos)) names
export
parseRecord : Parser Decl
parseRecord = do
fc <- getPos
keyword "record"
name <- uident
teles <- many $ ebind <|> nakedBind
keyword "where"
cname <- optional $ keyword "constructor" *> uident
decls <- startBlock $ manySame $ parseSig
pure $ Record fc name (join teles) cname decls
export
parseClass : Parser Decl
parseClass = do
@@ -487,7 +500,7 @@ export
parseDecl : Parser Decl
parseDecl = parseMixfix <|> parsePType <|> parsePFunc
<|> parseNorm <|> parseData <|> parseSig <|> parseDef
<|> parseClass <|> parseInstance
<|> parseClass <|> parseInstance <|> parseRecord
export

67
src/Lib/ProcessDecl.idr
View File

@@ -178,6 +178,21 @@ logMetas mstart = do
addError $ E fc $ unlines ([msg] ++ msgs ++ sols)
-- Used for Class and Record
getSigs : List Decl -> List (FC, String, Raw)
getSigs [] = []
getSigs ((TypeSig _ [] _) :: xs) = getSigs xs
getSigs ((TypeSig fc (nm :: nms) ty) :: xs) = (fc, nm, ty) :: getSigs xs
getSigs (_:: xs) = getSigs xs
teleToPi : Telescope -> Raw -> Raw
teleToPi [] end = end
teleToPi ((info, ty) :: tele) end = RPi (getFC info) info ty (teleToPi tele end)
impTele : Telescope -> Telescope
impTele tele = map (\(BI fc nm _ quant, ty) => (BI fc nm Implicit Zero, ty)) tele
export
processDecl : Decl -> M ()
@@ -273,6 +288,9 @@ processDecl (DCheck fc tm ty) = do
putStrLn " NFV \{pprint [] norm}"
processDecl (Class classFC nm tele decls) = do
-- REVIEW maybe we can leverage Record for this
-- a couple of catches, we don't want the dotted accessors and
-- the self argument should be an auto-implicit
putStrLn "-----"
putStrLn "Class \{nm}"
let fields = getSigs decls
@@ -280,7 +298,7 @@ processDecl (Class classFC nm tele decls) = do
let dcName = "Mk\{nm}"
let tcType = teleToPi tele (RU classFC)
let tail = foldl (\ acc, (BI fc nm icit _, _) => RApp fc acc (RVar fc nm) icit) (RVar classFC nm) tele
let dcType = teleToPi impTele $
let dcType = teleToPi (impTele tele) $
foldr (\(fc, nm, ty), acc => RPi fc (BI fc nm Explicit Many) ty acc ) tail fields
putStrLn "tcon type \{pretty tcType}"
@@ -290,7 +308,7 @@ processDecl (Class classFC nm tele decls) = do
putStrLn $ render 90 $ pretty decl
processDecl decl
for_ fields $ \ (fc,name,ty) => do
let funType = teleToPi impTele $ RPi fc (BI fc "_" Auto Many) tail ty
let funType = teleToPi (impTele tele) $ RPi fc (BI fc "_" Auto Many) tail ty
let autoPat = foldl (\acc, (fc,nm,ty) => RApp fc acc (RVar fc nm) Explicit) (RVar classFC dcName) fields
let lhs = foldl (\acc, (BI fc' nm icit quant, _) => RApp fc' acc (RVar fc' nm) Implicit) (RVar fc name) tele
let lhs = RApp classFC lhs autoPat Auto
@@ -300,20 +318,7 @@ processDecl (Class classFC nm tele decls) = do
putStrLn "\{pretty decl}"
processDecl $ TypeSig fc [name] funType
processDecl decl
where
getSigs : List Decl -> List (FC, String, Raw)
getSigs [] = []
getSigs ((TypeSig _ [] _) :: xs) = getSigs xs
getSigs ((TypeSig fc (nm :: nms) ty) :: xs) = (fc, nm, ty) :: getSigs xs
getSigs (_:: xs) = getSigs xs
impTele : Telescope
impTele = map (\(BI fc nm _ quant, ty) => (BI fc nm Implicit Zero, ty)) tele
teleToPi : Telescope -> Raw -> Raw
teleToPi [] end = end
teleToPi ((info, ty) :: tele) end = RPi (getFC info) info ty (teleToPi tele end)
processDecl (Instance instfc ty decls) = do
let decls = collectDecl decls
@@ -414,7 +419,6 @@ processDecl (Data fc nm ty cons) = do
putStrLn "Data \{nm}"
top <- get
mc <- readIORef top.metas
let mstart = length mc.metas
tyty <- check (mkCtx fc) ty (VU fc)
case lookup nm top of
Just (MkEntry _ name type Axiom) => do
@@ -449,3 +453,34 @@ processDecl (Data fc nm ty cons) = do
checkDeclType (U _) = pure ()
checkDeclType (Pi _ str icit rig t u) = checkDeclType u
checkDeclType _ = error fc "data type doesn't return U"
processDecl (Record recordFC nm tele cname decls) = do
putStrLn "-----"
putStrLn "Record"
let fields = getSigs decls
let dcName = fromMaybe "Mk\{nm}" cname
let tcType = teleToPi tele (RU recordFC)
-- REVIEW - I probably want to stick the telescope in front of the fields
let tail = foldl (\ acc, (BI fc nm icit _, _) => RApp fc acc (RVar fc nm) icit) (RVar recordFC nm) tele
let dcType = teleToPi (impTele tele) $
foldr (\(fc, nm, ty), acc => RPi fc (BI fc nm Explicit Many) ty acc ) tail fields
putStrLn "tcon type \{pretty tcType}"
putStrLn "dcon type \{pretty dcType}"
let decl = Data recordFC nm tcType [TypeSig recordFC [dcName] dcType]
putStrLn "Decl:"
putStrLn $ render 90 $ pretty decl
processDecl decl
for_ fields $ \ (fc,name,ty) => do
-- TODO dependency isn't handled yet
-- we'll need to replace stuff like `len` with `len self`.
let funType = teleToPi (impTele tele) $ RPi fc (BI fc "_" Explicit Many) tail ty
let autoPat = foldl (\acc, (fc,nm,ty) => RApp fc acc (RVar fc nm) Explicit) (RVar recordFC dcName) fields
let lhs = foldl (\acc, (BI fc' nm icit quant, _) => RApp fc' acc (RVar fc' nm) Implicit) (RVar fc name) tele
let lhs = RApp recordFC lhs autoPat Explicit
let decl = Def fc name [(lhs, (RVar fc name))]
putStrLn "\{name} : \{pretty funType}"
putStrLn "\{pretty decl}"
processDecl $ TypeSig fc [name] funType
processDecl decl

26
src/Lib/Syntax.idr
View File

@@ -125,6 +125,7 @@ data Decl
| PMixFix FC (List Name) Nat Fixity
| Class FC Name Telescope (List Decl)
| Instance FC Raw (List Decl)
| Record FC Name Telescope (Maybe Name) (List Decl)
public export
HasFC Decl where
@@ -137,6 +138,7 @@ HasFC Decl where
getFC (PMixFix x strs k y) = x
getFC (Class x str xs ys) = x
getFC (Instance x tm xs) = x
getFC (Record x str tm str1 xs) = x
public export
record Module where
@@ -169,6 +171,9 @@ Show Clause where
Show Import where
show (MkImport _ str) = foo ["MkImport", show str]
Show BindInfo where
show (BI _ nm icit quant) = foo ["BI", show nm, show icit, show quant]
-- this is for debugging, use pretty when possible
covering
Show Decl where
@@ -181,6 +186,7 @@ Show Decl where
show (PMixFix _ nms prec fix) = foo ["PMixFix", show nms, show prec, show fix]
show (Class _ nm tele decls) = foo ["Class", nm, "...", show $ map show decls]
show (Instance _ nm decls) = foo ["Instance", show nm, show $ map show decls]
show (Record _ nm tele nm1 decls) = foo ["Record", show nm, show tele, show nm1, show decls]
export covering
Show Module where
@@ -197,9 +203,6 @@ covering
Show RCaseAlt where
show (MkAlt x y)= foo ["MkAlt", show x, assert_total $ show y]
Show BindInfo where
show (BI _ name icit quant) = foo ["BI", show name, show icit, show quant]
covering
Show Raw where
show (RImplicit _) = "_"
@@ -233,16 +236,17 @@ Pretty Pattern where
pretty (PatWild _icit) = "_"
pretty (PatLit _ lit) = pretty lit
wrap : Icit -> Doc -> Doc
wrap Explicit x = text "(" ++ x ++ text ")"
wrap Implicit x = text "{" ++ x ++ text "}"
wrap Auto x = text "{{" ++ x ++ text "}}"
export
Pretty Raw where
pretty = asDoc 0
where
bindDoc : BindInfo -> Doc
bindDoc (BI _ nm icit quant) = ?rhs_0
wrap : Icit -> Doc -> Doc
wrap Explicit x = text "(" ++ x ++ text ")"
wrap Implicit x = text "{" ++ x ++ text "}"
wrap Auto x = text "{{" ++ x ++ text "}}"
par : Nat -> Nat -> Doc -> Doc
par p p' d = if p' < p then text "(" ++ d ++ text ")" else d
@@ -273,6 +277,9 @@ Pretty Raw where
asDoc p (RWhere _ dd b) = text "TODO pretty where"
asDoc p (RAs _ nm x) = text nm ++ "@(" ++ asDoc 0 x ++ ")"
prettyBind : (BindInfo, Raw) -> Doc
prettyBind (BI _ nm icit quant, ty) = wrap icit (text (show quant ++ nm) <+> text ":" <+> pretty ty)
export
Pretty Decl where
pretty (TypeSig _ nm ty) = spread (map text nm) <+> text ":" <+> nest 2 (pretty ty)
@@ -283,7 +290,10 @@ Pretty Decl where
pretty (PFunc _ nm [] ty src) = "pfunc" <+> text nm <+> ":" <+> nest 2 (pretty ty <+> ":=" <+/> text (show src))
pretty (PFunc _ nm uses ty src) = "pfunc" <+> text nm <+> "uses" <+> spread (map text uses) <+> ":" <+> nest 2 (pretty ty <+> ":=" <+/> text (show src))
pretty (PMixFix _ names prec fix) = text (show fix) <+> text (show prec) <+> spread (map text names)
pretty (Class _ _ _ _) = text "TODO pretty Class"
pretty (Record _ nm tele cname decls) = text "record" <+> text nm <+> ":" <+> spread (map prettyBind tele)
<+> (nest 2 $ text "where" </> stack (maybe empty (\ nm' => text "constructor" <+> text nm') cname :: map pretty decls))
pretty (Class _ nm tele decls) = text "class" <+> text nm <+> ":" <+> spread (map prettyBind tele)
<+> (nest 2 $ text "where" </> stack (map pretty decls))
pretty (Instance _ _ _) = text "TODO pretty Instance"
export