Initial implementation of record updates

Updates are converted to case blocks, so dependent field update works as
long as all the relevant fields are explicitly update.

Notes/implementation-notes.md

@@ -265,3 +265,17 @@ names defined in the inner namespace are explicitly exported. The visibility
 modifiers "export", "public export", and "private" control whether the name
 can be seen in any other namespace, and it's nothing to do with the file
 they're defined in at all.
+
+Records
+-------
+Records are part of TTImp (rather than the surface language). Elaborating a
+record declaration creates a data type and associated projection functions.
+Record setters are generated on demand while elaborating TTImp (in
+TTImp.Elab.Term and TTImp.Elab.Record). Setters are translated directly to
+'case' blocks, which means that update of dependent fields works as one might
+expect (i.e. it's safe as long as all of the fields are updated at the same
+time consistently).
+
+In TTImp, unlike in Idris 1, records are not implicitly put into their own
+namespace, but higher level languages (e.g. Idris itself) can do so explicitly
+themselves.

src/Core/AutoSearch.idr

@@ -186,7 +186,7 @@ searchNames loc defaults depth trying env ty topty defining []
 searchNames loc defaults depth trying env ty topty defining (n :: ns)
     = do gam <- get Ctxt
          let visns = mapMaybe (visible (gamma gam) (currentNS gam)) (n :: ns)
-         log 5 $ "Searching " ++ show (map fst visns) ++ " for " ++ show ty
+         log 2 $ "Searching " ++ show (map fst visns) ++ " for " ++ show ty
          let nfty = nf gam env ty
          exactlyOne loc env ty topty
             (map (searchName loc defaults depth trying env nfty topty defining) visns)
@@ -387,7 +387,8 @@ searchType loc defaults depth trying env defining topty ty
                                     (detArgs sd, globalHints sd, directHints sd, indirectHints sd)
                              let opens = filter (/=defining) allOpens
                              let cons = filter (/=defining) allCons
-                             log 5 $ "Hints for " ++ show n ++ " " ++ show defaults ++ " : " ++ show cons
+                             log 2 $ "Hints for " ++ show n ++ " " ++ show defaults ++ " : " ++ show cons
+                             log 2 $ "Chasers: " ++ show chasers
                              -- Solutions is either:
                              -- One of the locals
                              -- or *Exactly one* of the open hints

src/Core/Core.idr

@@ -36,6 +36,7 @@ data Error annot
     | AmbiguousElab annot (Env Term vars) (List (Term vars))
     | AmbiguousSearch annot (Env Term vars) (List (Term vars))
     | AllFailed (List (Maybe Name, Error annot))
+    | RecordTypeNeeded annot (Env Term vars)
     | InvalidImplicit annot (Env Term vars) Name (Term vars)
     | CantSolveGoal annot (Term [])
     | DeterminingArg annot Name (Env Term vars) (Term vars)
@@ -122,6 +123,8 @@ Show annot => Show (Error annot) where
   show (AmbiguousElab fc env ts) = show fc ++ ":Ambiguous elaboration " ++ show ts
   show (AmbiguousSearch fc env ts) = show fc ++ ":Ambiguous search " ++ show ts
   show (AllFailed ts) = "No successful elaboration: " ++ assert_total (show ts)
+  show (RecordTypeNeeded fc env)
+      = show fc ++ ":Can't infer type of record to update"
   show (InvalidImplicit fc env n tm) 
       = show fc ++ ":" ++ show n ++ " is not a valid implicit argument in " ++ show tm
   show (CantSolveGoal fc g) 
@@ -204,6 +207,7 @@ getAnnot (AmbiguousElab loc _ xs) = Just loc
 getAnnot (AmbiguousSearch loc _ xs) = Just loc
 getAnnot (AllFailed ((_, x) :: xs)) = getAnnot x
 getAnnot (AllFailed []) = Nothing
+getAnnot (RecordTypeNeeded loc _) = Just loc
 getAnnot (InvalidImplicit loc _ y tm) = Just loc
 getAnnot (CantSolveGoal loc tm) = Just loc
 getAnnot (DeterminingArg loc y env tm) = Just loc

src/Idris/Desugar.idr

@@ -116,8 +116,12 @@ mutual
   desugar side ps (PLocal fc xs scope) 
       = pure $ ILocal fc (concat !(traverse (desugarDecl ps) xs)) 
                          !(desugar side (definedIn xs ++ ps) scope)
+  desugar side ps (PApp pfc (PUpdate fc fs) rec)
+      = pure $ IUpdate pfc !(traverse (desugarUpdate side ps) fs)
+                           !(desugar side ps rec)
   desugar side ps (PUpdate fc fs)
-      = pure $ IUpdate fc !(traverse (desugarUpdate side ps) fs)
+      = desugar side ps (PLam fc RigW Explicit (MN "rec" 0) (PImplicit fc)
+                            (PApp fc (PUpdate fc fs) (PRef fc (MN "rec" 0))))
   desugar side ps (PApp fc x y) 
       = pure $ IApp fc !(desugar side ps x) !(desugar side ps y)
   desugar side ps (PImplicitApp fc x argn y) 

src/Idris/Error.idr

@@ -101,6 +101,8 @@ perror (AllFailed ts)
     allUndefined [(_, UndefinedName loc e)] = Just (UndefinedName loc e)
     allUndefined ((_, UndefinedName _ e) :: es) = allUndefined es
     allUndefined _ = Nothing
+perror (RecordTypeNeeded _ _)
+    = pure "Can't infer type for this record update"
 perror (InvalidImplicit _ env n tm)
     = pure $ show n ++ " is not a valid implicit argument in " ++ !(pshow env tm)
 perror (CantSolveGoal _ g)

src/Idris/Resugar.idr

@@ -163,9 +163,10 @@ mutual
       = do ds' <- traverse toPDecl ds
            sc' <- toPTerm startPrec sc
            bracket p startPrec (PLocal emptyFC (mapMaybe id ds') sc')
-  toPTerm p (IUpdate _ ds)
+  toPTerm p (IUpdate _ ds f)
       = do ds' <- traverse toPFieldUpdate ds
-           bracket p startPrec (PUpdate emptyFC ds')
+           f' <- toPTerm argPrec f
+           bracket p startPrec (PApp emptyFC (PUpdate emptyFC ds') f')
   toPTerm p tm@(IApp _ fn arg)
       = do arg' <- toPTerm argPrec arg
            app <- toPTermApp fn [(Nothing, arg')]

src/TTImp/CaseSplit.idr

@@ -87,7 +87,7 @@ findCons n lhs
               do defs <- get Ctxt
                  case findTyName defs [] n lhs of
                       Nothing => pure (SplitFail (CantSplitThis n 
-                                         ("Can't find name " ++ show n ++ " in LHS")))
+                                         ("Can't find type of " ++ show n ++ " in LHS")))
                       Just tyn =>
                           case lookupDefExact tyn (gamma defs) of
                                Just (TCon _ _ _ _ cons) => pure (OK (fn, tyn, cons))

src/TTImp/Elab/Record.idr

@@ -0,0 +1,163 @@
+module TTImp.Elab.Record
+
+import TTImp.TTImp
+import TTImp.Elab.Ambiguity
+import TTImp.Elab.Delayed
+import TTImp.Elab.Rewrite
+import public TTImp.Elab.State
+import TTImp.Reflect
+
+import Core.AutoSearch
+import Core.CaseTree
+import Core.Context
+import Core.Metadata
+import Core.Normalise
+import Core.Reflect
+import Core.TT
+import Core.Typecheck
+import Core.Unify
+
+import Data.List
+import Data.List.Views
+
+getRecordType : Env Term vars -> NF vars -> Maybe Name
+getRecordType env (NTCon n _ _ _) = Just n
+getRecordType env _ = Nothing
+
+data Rec : Type -> Type where
+     Field : String -> RawImp annot -> Rec annot -- field name on left, value on right
+     Constr : Name -> List (String, Rec annot) -> Rec annot
+
+toLHS : annot -> Rec annot -> RawImp annot
+toLHS loc (Field n _) = IBindVar loc n
+toLHS loc (Constr con args)
+    = let args' = map (\a => toLHS loc (snd a)) args in
+          apply (IVar loc con) args'
+
+toRHS : annot -> Rec annot -> RawImp annot
+toRHS loc (Field _ val) = val
+toRHS loc (Constr con args)
+    = let args' = map (\a => toRHS loc (snd a)) args in
+          apply (IVar loc con) args'
+
+findConName : Defs -> Name -> Maybe Name
+findConName defs tyn
+    = case lookupDefExact tyn (gamma defs) of
+           Just (TCon _ _ _ _ [con]) => Just con
+           _ => Nothing
+
+findFields : Defs -> Name -> Maybe (List (String, Maybe Name))
+findFields defs con
+    = case lookupTyExact con (gamma defs) of
+           Just t => Just (getExpNames (nf defs [] t))
+           _ => Nothing
+  where
+    getExpNames : NF [] -> List (String, Maybe Name)
+    getExpNames (NBind x (Pi _ p ty) sc)
+        = let rest = getExpNames (sc (toClosure defaultOpts [] Erased)) in
+              case p of
+                   Explicit => (nameRoot x, getRecordType [] ty) :: rest
+                   _ => rest
+    getExpNames _ = []
+
+genFieldName : {auto x : Ref Ctxt Defs} ->
+               String -> Core annot String
+genFieldName root
+    = do defs <- get Ctxt
+         put Ctxt (record { nextVar $= (+1) } defs)
+         pure (root ++ show (nextVar defs))
+
+-- There's probably a generic version of this in the prelude isn't
+-- there?
+replace : String -> Rec annot -> 
+          List (String, Rec annot) -> List (String, Rec annot)
+replace k v [] = []
+replace k v ((k', v') :: vs)
+    = if k == k' 
+         then ((k, v) :: vs)
+         else ((k', v') :: replace k v vs)
+
+findPath : {auto c : Ref Ctxt Defs} ->
+           annot -> List String -> Maybe Name -> 
+           (String -> RawImp annot) ->
+           Rec annot -> Core annot (Rec annot)
+findPath loc [] tyn val (Field lhs _) = pure (Field lhs (val lhs))
+findPath loc [] tyn val rec 
+   = throw (GenericMsg loc "Invalid record update")
+findPath loc (p :: ps) Nothing val (Field n v) 
+   = throw (GenericMsg loc (p ++ " is not part of a record type"))
+findPath loc (p :: ps) (Just tyn) val (Field n v) 
+   = do defs <- get Ctxt
+        let Just con = findConName defs tyn
+                 | Nothing => throw (GenericMsg loc "Can't find record constructor")
+        let Just fs = findFields defs con
+                 | Nothing => throw (GenericMsg loc "Can't find record fields")
+        args <- mkArgs fs
+        let rec' = Constr con args
+        findPath loc (p :: ps) (Just tyn) val rec'
+  where
+    mkArgs : List (String, Maybe Name) -> 
+             Core annot (List (String, Rec annot))
+    mkArgs [] = pure []
+    mkArgs ((p, _) :: ps)
+        = do fldn <- genFieldName p
+             args' <- mkArgs ps
+             pure ((p, Field fldn (IVar loc (UN fldn))) :: args')
+
+findPath loc (p :: ps) tyn val (Constr con args) 
+   = do let Just prec = lookup p args
+                 | Nothing => throw (GenericMsg loc ("Record type " ++ 
+                                       show tyn ++ " has no field " ++ p))
+        defs <- get Ctxt
+        let Just fs = findFields defs con
+                 | Nothing => pure (Constr con args)
+        let Just mfty = lookup p fs
+                 | Nothing => throw (GenericMsg loc ("Record type " ++ 
+                                       show tyn ++ " has no field " ++ p))
+        prec' <- findPath loc ps mfty val prec
+        pure (Constr con (replace p prec' args))
+
+getSides : {auto c : Ref Ctxt Defs} ->
+           annot -> IFieldUpdate annot -> Name -> RawImp annot -> Rec annot -> 
+           Core annot (Rec annot)
+getSides loc (ISetField path val) tyn orig rec 
+   -- update 'rec' so that 'path' is accessible on the lhs and rhs,
+   -- then set the path on the rhs to 'val'
+   = findPath loc path (Just tyn) (const val) rec
+getSides loc (ISetFieldApp path val) tyn orig rec 
+   = findPath loc path (Just tyn) (\n => apply val [IVar loc (UN n)]) rec
+ where
+   get : List String -> RawImp annot -> RawImp annot
+   get [] rec = rec
+   get (p :: ps) rec = get ps (IApp loc (IVar loc (UN p)) rec)
+
+getAllSides : {auto c : Ref Ctxt Defs} ->
+              annot -> List (IFieldUpdate annot) -> Name -> 
+              RawImp annot -> Rec annot -> 
+              Core annot (Rec annot)
+getAllSides loc [] tyn orig rec = pure rec
+getAllSides loc (u :: upds) tyn orig rec 
+    = getAllSides loc upds tyn orig !(getSides loc u tyn orig rec)
+
+export
+recUpdate : {auto c : Ref Ctxt Defs} -> 
+            {auto u : Ref UST (UState annot)} ->
+            {auto e : Ref EST (EState vars)} ->
+            {auto i : Ref ImpST (ImpState annot)} ->
+            {auto m : Ref Meta (Metadata annot)} ->
+            RigCount -> Elaborator annot ->
+            ElabInfo annot -> annot -> Env Term vars -> NestedNames vars -> 
+            List (IFieldUpdate annot) -> 
+            (rec : RawImp annot) -> (recty : Term vars) ->
+            Core annot (RawImp annot)
+recUpdate rigc process elabinfo loc env nest flds rec recty
+      = do defs <- get Ctxt
+           let Just rectyn = getRecordType env (nf defs env recty)
+                    | Nothing => throw (RecordTypeNeeded loc env)
+           fldn <- genFieldName "fld"
+           sides <- getAllSides loc flds rectyn rec (Field fldn (IVar loc (UN fldn)))
+           pure $ ICase loc rec (Implicit loc) [mkClause sides]
+  where
+    mkClause : Rec annot -> ImpClause annot
+    mkClause rec = PatClause loc (toLHS loc rec) (toRHS loc rec)
+

src/TTImp/Elab/Term.idr

@@ -4,6 +4,7 @@ import TTImp.TTImp
 import TTImp.Elab.Ambiguity
 import TTImp.Elab.Case
 import TTImp.Elab.Delayed
+import TTImp.Elab.Record
 import TTImp.Elab.Rewrite
 import public TTImp.Elab.State
 import TTImp.Reflect
@@ -99,6 +100,9 @@ mutual
   -- If there's local definitions, add implicits inside the block
   check rigc process elabinfo env nest tm@(ILocal loc fs sc) expected
       = checkImp rigc process elabinfo env nest tm expected
+  -- No implicits on record updates
+  check rigc process elabinfo env nest tm@(IUpdate loc fs rec) expected
+      = checkImp rigc process elabinfo env nest tm expected
   check rigc process elabinfo env nest tm@(ILet loc rig n ty val sc) expected
       = checkImp rigc process elabinfo env nest tm expected
   check rigc process elabinfo env nest tm_in exp 
@@ -141,7 +145,8 @@ mutual
   checkFnApp {vars} rigc process loc elabinfo env nest tm_in exp
       = do defs <- get Ctxt
            handle
-             (do (ctm, cty) <- check rigc process elabinfo env nest tm_in exp
+             (do log 10 $ "Checking " ++ show tm_in ++ " at " ++ show exp
+                 (ctm, cty) <- check rigc process elabinfo env nest tm_in exp
                  log 10 $ "Checked fnapp " ++ show (ctm, cty, exp)
                  let ctynf = nf defs env cty
                  case exp of
@@ -151,14 +156,14 @@ mutual
                  case nf defs env cty of
                       NTCon n _ _ _ =>
                           if isDelayType n defs
-                             then throw (InternalError "Need force!")
+                             then throw (InternalError "Force")
                              else checkExp rigc process loc elabinfo env nest
                                            ctm cty exp
                       _ => checkExp rigc process loc elabinfo env nest
                                     ctm cty exp)
              (\err =>
                   case err of
-                       InternalError _ =>
+                       InternalError "Force" =>
                            case forceName defs of
                                 Nothing => check rigc process elabinfo env nest tm_in Unknown
                                 Just fn =>
@@ -286,8 +291,15 @@ mutual
           checkCase rigc process elabinfo loc env nest scr scrty alts expected
   checkImp rigc process elabinfo env nest (ILocal loc nested scope) expected 
       = checkLocal rigc process elabinfo loc env nest nested scope expected
-  checkImp rigc process elabinfo env nest (IUpdate loc fs) expected
-      = throw (InternalError "record update not implemented")
+  checkImp rigc process elabinfo env nest (IUpdate loc fs rec) expected
+      = do recty <- case expected of
+                         FnType [] ret => pure ret
+                         _ => do (_, ty) <- checkImp rigc process elabinfo 
+                                                     env nest rec Unknown
+                                 pure ty
+           rcase <- recUpdate rigc process elabinfo loc env nest fs rec recty
+           log 5 $ "Record update: " ++ show rcase
+           check rigc process elabinfo env nest rcase expected
   checkImp {vars} rigc process elabinfo env nest (IApp loc fn arg) expected 
       = do -- Collect the implicits from the top level application first
            let (fn', args) = collectGivenImps fn

src/TTImp/TTImp.idr

@@ -52,7 +52,7 @@ mutual
        ICase : annot -> RawImp annot -> (ty : RawImp annot) ->
                List (ImpClause annot) -> RawImp annot
        ILocal : annot -> List (ImpDecl annot) -> RawImp annot -> RawImp annot
-       IUpdate : annot -> List (IFieldUpdate annot) -> RawImp annot
+       IUpdate : annot -> List (IFieldUpdate annot) -> RawImp annot -> RawImp annot
        IApp : annot -> 
               (fn : RawImp annot) -> (arg : RawImp annot) -> RawImp annot
        IImplicitApp : annot -> 
@@ -197,8 +197,8 @@ mutual
      = union (used ns sc) (usedCases ns xs)
   used ns (ILocal _ ds sc) 
      = union (usedDecls ns ds) (used ns sc)
-  used ns (IUpdate _ fs) 
-     = usedFields ns fs
+  used ns (IUpdate _ fs rec)
+     = union (usedFields ns fs) (used ns rec)
   used ns (IApp _ fn arg) 
      = union (used ns fn) (used ns arg)
   used ns (IImplicitApp _ fn _ arg)
@@ -285,7 +285,7 @@ getAnnot (ILam x _ _ _ _ _) = x
 getAnnot (ILet x _ _ _ _ _) = x
 getAnnot (ICase x _ _ _) = x
 getAnnot (ILocal x _ _) = x
-getAnnot (IUpdate x _) = x
+getAnnot (IUpdate x _ _) = x
 getAnnot (IApp x _ _) = x
 getAnnot (IImplicitApp x _ _ _) = x
 getAnnot (ISearch x _) = x
@@ -341,8 +341,8 @@ mutual
         = "(%case (" ++ show scr ++ ") " ++ show alts ++ ")"
     show (ILocal _ def scope)
         = "(%local (" ++ show def ++ ") " ++ show scope ++ ")"
-    show (IUpdate _ flds)
-        = "(%record " ++ showSep ", " (map show flds) ++ ")"
+    show (IUpdate _ flds rec)
+        = "(%record " ++ showSep ", " (map show flds) ++ " " ++ show rec ++ ")"
     show (IApp _ fn arg) 
         = "(" ++ show fn ++ " " ++ show arg ++ ")"
     show (IImplicitApp _ fn Nothing arg) 
@@ -669,8 +669,8 @@ mutual
         = do tag 4; toBuf b fc; toBuf b y; toBuf b ty; toBuf b xs
     toBuf b (ILocal fc xs sc) 
         = do tag 5; toBuf b fc; toBuf b xs; toBuf b sc
-    toBuf b (IUpdate fc fs) 
-        = do tag 6; toBuf b fc; toBuf b fs
+    toBuf b (IUpdate fc fs rec) 
+        = do tag 6; toBuf b fc; toBuf b fs; toBuf b rec
     toBuf b (IApp fc fn arg) 
         = do tag 7; toBuf b fc; toBuf b fn; toBuf b arg
     toBuf b (IImplicitApp fc fn y arg) 
@@ -732,7 +732,8 @@ mutual
                        xs <- fromBuf s b; sc <- fromBuf s b
                        pure (ILocal fc xs sc)
                6 => do fc <- fromBuf s b; fs <- fromBuf s b
-                       pure (IUpdate fc fs)
+                       rec <- fromBuf s b
+                       pure (IUpdate fc fs rec)
                7 => do fc <- fromBuf s b; fn <- fromBuf s b
                        arg <- fromBuf s b
                        pure (IApp fc fn arg)