From 2ca43b6350164a9f25fb4379cb2d04a956f219f1 Mon Sep 17 00:00:00 2001 From: Steve Dunham Date: Mon, 5 Jan 2026 20:52:35 -0800 Subject: [PATCH] Dependent records The projection functions needed `foo` -> `self .foo` in the types --- TODO.md | 4 ++- src/Data/List.newt | 7 +++++ src/Lib/Elab.newt | 6 ---- src/Lib/ProcessDecl.newt | 16 +++++++--- src/Lib/Syntax.newt | 67 +++++++++++++++++++++++++++++++++++++--- 5 files changed, 83 insertions(+), 17 deletions(-) create mode 100644 src/Data/List.newt diff --git a/TODO.md b/TODO.md index 9be6106..30617fa 100644 --- a/TODO.md +++ b/TODO.md @@ -1,6 +1,8 @@ ## TODO +- [ ] maybe add fat arrows, I keep wanting to type them, `{{...}}` is a little ugly +- [ ] get some names on add missing cases (if not too difficult) - [x] add optional types to case `case xxx : Maybe Int of ...` - [ ] "Expected keyword" at `\ a ->` should be error at the `->` - [x] Show Either @@ -19,7 +21,7 @@ - [ ] Delay checking - We have things like `foldr (\ x acc => case x : ...`, where the lambda doesn't have a good type, so we have to be explicit. If we could defer the checking of that expression until more things are solved, we might not need the annotation (e.g. checking the other arguments). Some `case` statements may have a similar situation. - One idea is to throw the checks onto some sort of TODO list and run whatever works. (I think Idris may have a heuristic where it checks arguments backwards in some cases.) -- [ ] Dependent records (I guess I missed that bit) +- [x] Dependent records (I guess I missed that bit) - [ ] Arguments on records - [ ] Add sugar for type aliases (maybe infer arguments) - Lean has this, we maybe could run infer on the RHS and call it a day? We would need a simple LHS, though. diff --git a/src/Data/List.newt b/src/Data/List.newt new file mode 100644 index 0000000..40e270f --- /dev/null +++ b/src/Data/List.newt @@ -0,0 +1,7 @@ +module Data.List + +import Prelude + +lookup : ∀ a b. {{Eq a}} → a → List (a × b) → Maybe b +lookup key Nil = Nothing +lookup key ((k,v) :: rest) = if k == key then Just v else lookup key rest diff --git a/src/Lib/Elab.newt b/src/Lib/Elab.newt index 6d65e38..661c28e 100644 --- a/src/Lib/Elab.newt +++ b/src/Lib/Elab.newt @@ -1597,12 +1597,6 @@ infer ctx (RLet fc nm ty v sc) = do (sc',scty) <- infer ctx' sc pure (Let fc nm v' sc', scty) -infer ctx (RAnn fc tm rty) = do - ty <- check ctx rty (VU fc) - vty <- eval ctx.env ty - tm <- check ctx tm vty - pure (tm, vty) - infer ctx (RLam _ (BI fc nm icit quant) tm) = do a <- freshMeta ctx fc (VU emptyFC) Normal >>= eval ctx.env let ctx' = extend ctx nm a diff --git a/src/Lib/ProcessDecl.newt b/src/Lib/ProcessDecl.newt index 82cd7b7..fc86566 100644 --- a/src/Lib/ProcessDecl.newt +++ b/src/Lib/ProcessDecl.newt @@ -498,7 +498,6 @@ processRecord ns recordFC nm tele cname decls = do let fields = getSigs decls let dcName = fromMaybe "Mk\{show 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 => case bi : BindInfo × Raw of (BI fc nm icit _, _) => RApp fc acc (RVar fc nm) icit) (RVar recordFC nm) tele let dcType = teleToPi (impTele tele) $ foldr (\ x acc => case x : FC × String × Raw of (fc, nm, ty) => RPi fc (BI fc nm Explicit Many) ty acc ) tail fields @@ -509,12 +508,17 @@ processRecord ns recordFC nm tele cname decls = do log 1 $ \ _ => "Decl:" log 1 $ \ _ => render 90 $ pretty decl processDecl ns decl - ignore $ for fields $ \case - (fc,name,ty) => do + -- pattern to peel out fields on LHS + let autoPat = foldl (\acc x => case x : FC × String × Raw of (fc,nm,ty) => RApp fc acc (RVar fc nm) Explicit) (RVar recordFC dcName) fields + processFields autoPat tail Nil fields + where + processFields : Raw → Raw → List (String × Raw) → List (FC × String × Raw) → M Unit + processFields _ _ _ Nil = pure MkUnit + processFields autoPat tail deps ((fc,name,ty) :: rest) = 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 x => case x : FC × String × Raw of (fc,nm,ty) => RApp fc acc (RVar fc nm) Explicit) (RVar recordFC dcName) fields + + let funType = substRaw deps $ teleToPi (impTele tele) $ RPi fc (BI fc "$self" Explicit Many) tail ty -- `.fieldName` let pname = "." ++ name @@ -526,6 +530,8 @@ processRecord ns recordFC nm tele cname decls = do processDecl ns $ TypeSig fc (pname :: Nil) funType processDecl ns pdecl setFlag (QN ns pname) fc Inline + let deps = ((name, RApp fc (RVar fc pname) (RVar fc "$self") Explicit) :: deps) + processFields autoPat tail deps rest -- currently mixfix registration is handled in the parser -- since we now run a decl at a time we could do it here. diff --git a/src/Lib/Syntax.newt b/src/Lib/Syntax.newt index c351a57..eeaf275 100644 --- a/src/Lib/Syntax.newt +++ b/src/Lib/Syntax.newt @@ -3,6 +3,7 @@ module Lib.Syntax import Prelude import Lib.Common import Data.String +import Data.List import Lib.Prettier import Lib.Types @@ -43,7 +44,6 @@ data Raw : U where RImpossible : (fc : FC) -> Raw RPi : (fc : FC) -> BindInfo -> (ty : Raw) -> (sc : Raw) -> Raw RLet : (fc : FC) -> (nm : Name) -> (ty : Raw) -> (v : Raw) -> (sc : Raw) -> Raw - RAnn : (fc : FC) -> (tm : Raw) -> (ty : Raw) -> Raw RLit : (fc : FC) -> Literal -> Raw RCase : (fc : FC) -> (scrut : Raw) -> (mty : Maybe Raw) -> (alts : List RCaseAlt) -> Raw RImplicit : (fc : FC) -> Raw @@ -63,7 +63,6 @@ instance HasFC Raw where getFC (RU fc) = fc getFC (RPi fc _ ty sc) = fc getFC (RLet fc nm ty v sc) = fc - getFC (RAnn fc tm ty) = fc getFC (RLit fc y) = fc getFC (RCase fc scrut mty alts) = fc getFC (RImplicit fc) = fc @@ -165,7 +164,6 @@ instance Show Raw where show (RHole _) = "?" show (RUpdateRec _ clauses tm) = foo ("RUpdateRec" :: show clauses :: show tm :: Nil) show (RVar _ name) = foo ("RVar" :: show name :: Nil) - show (RAnn _ t ty) = foo ( "RAnn" :: show t :: show ty :: Nil) show (RLit _ x) = foo ( "RLit" :: show x :: Nil) show (RLet _ x ty v scope) = foo ( "Let" :: show x :: " : " :: show ty :: " = " :: show v :: " in " :: show scope :: Nil) show (RPi _ bi y z) = foo ( "Pi" :: show bi :: show y :: show z :: Nil) @@ -224,8 +222,6 @@ instance Pretty Raw where par p 0 $ text "let" <+> text x <+> text ":" <+> asDoc p ty <+> text "=" <+> asDoc p v <+/> text "in" <+> asDoc p scope - -- does this exist? - asDoc p (RAnn _ x y) = text "TODO - Pretty RAnn" asDoc p (RLit _ lit) = pretty lit asDoc p (RCase _ x _ xs) = text "TODO - Pretty RCase" asDoc p (RImplicit _) = text "_" @@ -264,6 +260,67 @@ instance Pretty Decl where pretty (Instance _ _ _) = text "TODO pretty Instance" pretty (ShortData _ lhs sigs) = text "data" <+> pretty lhs <+> text "=" <+> pipeSep (map pretty sigs) +lhsNames : Raw → List String +lhsNames tm = case tm of + RVar fc n => n :: Nil + RAs _ n tm => n :: lhsNames tm + RApp _ t u _ => lhsNames t ++ lhsNames u + -- the rest have no names or don't occur on LHS + _ => Nil + +-- used for the projection type in dependent records, probably overkill, but maybe it will be useful elsewhere +-- TODO unit tests on substRaw +substRaw : List (String × Raw) → Raw → Raw +substRaw ss t = case t of + RVar fc n => fromMaybe t (lookup n ss) + (RUpdateRec fc uc target) => RUpdateRec fc (map substUC uc) (map (substRaw ss) target) + -- LHS only + (RAs fc nm t) => RAs fc nm (substRaw ss t) + (RIf fc c t e) => RIf fc (substRaw ss c) (substRaw ss t) (substRaw ss e) + (RLet fc nm ty v sc) => RLet fc nm (substRaw ss ty) (substRaw ss v) (substRaw ss sc) + (RPi fc info a b) => RPi fc info (substRaw ss a) (substRaw (filterBind info ss) b) + (RApp fc t u icit) => RApp fc (substRaw ss t) (substRaw ss u) icit + (RLam fc info sc) => RLam fc info (substRaw (filterBind info ss) sc) + -- FIXME shadowing + (RWhere fc ds body) => RWhere fc (map substDecl ds) (substRaw ss body) + (RDo fc stmts) => RDo fc (substStmts ss stmts) + (RCase fc scrut mdef alts) => RCase fc (substRaw ss scrut) (map (substRaw ss) mdef) (map substAlt alts) + -- Enumerate to force consideration of new cases + t@(RImpossible _) => t + t@(RU _) => t + t@(RHole fc) => t + t@(RImplicit fc) => t + t@(RLit _ _) => t + where + -- Need to handle shadowing! + filter : ∀ a. List String → List (String × a) → List (String × a) + filter nms Nil = Nil + filter nms (x@(a,b) :: xs) = if elem a nms then filter nms xs else x :: filter nms xs + + filterBind : ∀ a. BindInfo → List (String × a) → List (String × a) + filterBind (BI fc nm _ _) xs = filter (nm :: Nil) xs + + substUC : UpdateClause → UpdateClause + substUC (AssignField fc nm t) = AssignField fc nm (substRaw ss t) + substUC (ModifyField fc nm t) = ModifyField fc nm (substRaw ss t) + + substClause : Raw × Maybe Raw → Raw × Maybe Raw + substClause (a,b) = (substRaw ss a, map (substRaw ss) b) + + substDecl : Decl → Decl + substDecl (TypeSig fc nms ty) = TypeSig fc nms (substRaw ss ty) + substDecl (FunDef fc nm clauses) = FunDef fc nm $ map substClause clauses + substDecl d = d -- shouldn't happen + + substAlt : RCaseAlt → RCaseAlt + substAlt (MkAlt a b) = MkAlt (substRaw ss a) (map (substRaw (filter (lhsNames a) ss)) b) + + substStmts : List (String × Raw) → List DoStmt → List DoStmt + substStmts ss Nil = Nil + substStmts ss (DoExpr fc t :: rest) = DoExpr fc (substRaw ss t) :: substStmts ss rest + substStmts ss (DoArrow fc pat sc alts :: rest) = + DoArrow fc (substRaw ss pat) (substRaw ss sc) (map (substAlt) alts) :: substStmts (filter (lhsNames pat) ss) rest + substStmts ss (DoLet fc nm t :: rest) = DoLet fc nm (substRaw ss t) :: substStmts (filter (nm :: Nil) ss) rest instance Pretty Module where pretty (MkModule name imports decls) =