Dependent records

The projection functions needed `foo` -> `self .foo` in the types

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.

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

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

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
+  -- pattern to peel out fields on LHS
-    (fc,name,ty) => do
+  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.

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) =