From f2c6b409fe5a4d24cae40b230f19e01fc9115ad5 Mon Sep 17 00:00:00 2001 From: Steve Dunham Date: Thu, 19 Dec 2024 20:43:10 -0800 Subject: [PATCH] desugaring record implementation (TODO - dependency) --- TODO.md | 1 + src/Lib/Parser.idr | 15 ++++++++- src/Lib/ProcessDecl.idr | 67 +++++++++++++++++++++++++++++++---------- src/Lib/Syntax.idr | 26 +++++++++++----- 4 files changed, 84 insertions(+), 25 deletions(-) diff --git a/TODO.md b/TODO.md index b3d99f5..249ab3e 100644 --- a/TODO.md +++ b/TODO.md @@ -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 diff --git a/src/Lib/Parser.idr b/src/Lib/Parser.idr index 31a45ad..aae7366 100644 --- a/src/Lib/Parser.idr +++ b/src/Lib/Parser.idr @@ -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 diff --git a/src/Lib/ProcessDecl.idr b/src/Lib/ProcessDecl.idr index f7b6b46..b99cc05 100644 --- a/src/Lib/ProcessDecl.idr +++ b/src/Lib/ProcessDecl.idr @@ -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 diff --git a/src/Lib/Syntax.idr b/src/Lib/Syntax.idr index 81da8e0..44f7dd6 100644 --- a/src/Lib/Syntax.idr +++ b/src/Lib/Syntax.idr @@ -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