Add record update syntax

src/Kind/Check.hs

@@ -13,6 +13,7 @@ import qualified Data.IntMap.Strict as IM
 import qualified Data.Map.Strict as M
 
 import Control.Monad (forM, forM_, unless, when)
+import Data.Foldable (find)
 import Debug.Trace
 
 -- Type-Checking
@@ -176,6 +177,10 @@ infer sus src term dep = debug ("infer:" ++ (if sus then "* " else " ") ++ showT
   go (Con nam arg) = do
     envLog (Error src (Ref "annotation") (Ref "constructor") (Con nam arg) dep)
     envFail
+
+  go (Upd trm args) = do
+    envLog (Error src (Ref "annotation") (Ref "record update") (Upd trm args) dep)
+    envFail
 
   go (Mat cse) = do
     envLog (Error src (Ref "annotation") (Ref "match") (Mat cse) dep)
@@ -291,6 +296,49 @@ check sus src term typx dep = debug ("check:" ++ (if sus then "* " else " ") ++
         envLog (Error src (Hol "arity_mismatch" []) (Hol "unknown_type" []) (Hol "constructor" []) dep)
         envFail
 
+  go val@(Upd trm arg) = do
+    book <- envGetBook
+    fill <- envGetFill
+    case reduce book fill 2 typx of
+      (ADT adtScp [adtCts] adtTyp) -> do
+        -- Exactly 1 constructor
+        let (Ctr _ cTel) = adtCts
+        let expectedFields = getTeleNames cTel 0 []
+        let wrongField = find (not . (`elem` expectedFields)) (map fst arg)
+        case wrongField of
+          Just fld -> do
+            envLog (Error src (Hol ("expected_one_of:" ++ show expectedFields) []) (Hol ("detected:" ++ fld) []) (Hol "unknown_field" []) dep)
+            envFail
+          Nothing -> pure ()
+
+        argA <- checkConstructor src arg cTel dep
+        return $ Ann False (Upd trm argA) typx
+
+      (ADT adtScp adtCts adtTyp) -> do
+        -- 0 or more than 1 constructors
+        envLog $ Error src
+          (Hol ("expected: 1 constructor") [])
+          (Hol ("detected: " ++ show (length adtCts) ++ " constructors") []) 
+          (Hol ("record_update_multiple_constructors") []) dep
+        envFail
+
+      otherwise -> infer sus src (Upd trm arg) dep
+    where
+      checkConstructor :: Maybe Cod -> [(String, Term)] -> Tele -> Int -> Env [(String, Term)]
+      checkConstructor src [] (TRet ret) dep = do
+        cmp src val ret typx dep
+        return []
+      checkConstructor src ((field, arg):args) (TExt nam inp bod) dep =
+        if field /= nam
+          then do
+            -- Constructors must be in order
+            checkConstructor src ((field, arg) : args) (bod arg) dep
+          else do
+            argA  <- check sus src arg inp dep
+            argsA <- checkConstructor src args (bod arg) (dep + 1)
+            return $ (field, argA) : argsA
+      checkConstructor src _ _ dep = return []
+
   go (Mat cse) = do
     book <- envGetBook
     fill <- envGetFill

src/Kind/CompileJS.hs

@@ -49,6 +49,7 @@ data CT
   | CLam (String,CT) (CT -> CT)
   | CApp CT CT
   | CCon String [(String, CT)]
+  | CUpd CT [(String, CT)]
   | CMat CT [(String, [(String,CT)], CT)]
   | CRef String
   | CHol String
@@ -117,6 +118,7 @@ termToCT book fill term typx dep = bindCT (t2ct term typx dep) [] where
             in CCon nam fields
           Nothing -> error $ "constructor-not-found:" ++ nam
         Nothing -> error $ "untyped-constructor"
+    go (Upd trm arg) = CUpd (t2ct trm Nothing dep) (map (\(f, t) -> (f, t2ct t Nothing dep)) arg)
     go (Mat cse) =
       case typx of
         Just typx -> case reduce book fill 2 typx of
@@ -158,8 +160,6 @@ termToCT book fill term typx dep = bindCT (t2ct term typx dep) [] where
           val' = t2ct val Nothing dep
           bod' = \x y -> t2ct (bod (Var got dep) (Var nam dep)) Nothing (dep+2)
       in CPut got nam map' key' val' bod'
-    go (All _ _ _) =
-      CNul
     go (Ref nam) =
       CRef nam
     go (Let nam val bod) =
@@ -245,6 +245,10 @@ removeUnreachables ct = go ct where
   go (CCon nam fields) =
     let fields' = map (\ (f,t) -> (f, go t)) fields
     in CCon nam fields'
+  go (CUpd trm fields) =
+    let trm' = go trm in
+    let fields' = map (\ (f,t) -> (f, go t)) fields
+    in CUpd trm' fields'
   go (CRef nam) = CRef nam
   go (CHol nam) = CHol nam
   go (CLet (nam,typ) val bod) =
@@ -369,7 +373,7 @@ inline book ct = nf ct where
     go (CLam (nam,inp) bod)     = CLam (nam, nf inp) (\x -> nf (bod x))
     go (CApp fun arg)           = CApp (nf fun) (nf arg)
     go (CCon nam fields)        = CCon nam (map (\ (f,t) -> (f, nf t)) fields)
-    go (CADT cts)               = CADT (map (\ (n,fs) -> (n, map (\ (fn,ft) -> (fn, nf ft)) fs)) cts)
+    go (CUpd trm fields)        = CUpd (nf trm) (map (\ (f,t) -> (f, nf t)) fields)
     go (CMat val cses)          = CMat (nf val) (map (\ (n,f,b) -> (n, map (\ (fn,ft) -> (fn, nf ft)) f, nf b)) cses)
     go (CRef nam)               = CRef nam
     go (CHol nam)               = CHol nam
@@ -669,6 +673,19 @@ fnToJS book fnName ct@(getArguments -> (fnArgs, fnBody)) = do
         setStmt <- return $ concat [var ++ "." ++ nm ++ " = " ++ fldName ++ ";"]
         return $ concat [fldStmt, setStmt]
       return $ concat $ [objStmt] ++ setStmts
+    go (CUpd trm fields) = do
+      updName <- fresh
+      updStmt <- ctToJS False updName trm dep
+      setVarsAndStmts <- forM fields $ \ (nm, tm) -> do
+        fldName <- fresh
+        fldStmt <- ctToJS False fldName tm dep
+        return $ ((nm, fldName), fldStmt)
+      let (setVars, setStmts) = unzip setVarsAndStmts
+      let setVarsCode = concatMap (\(field, val) -> field ++ ": " ++ val ++ ", ") setVars
+      return $ concat $
+        [updStmt] ++
+        setStmts ++
+        [var, " = {...", updName, ", ", setVarsCode ++ "};"]
     go (CMat val cses) = do
       let isRecord = length cses == 1 && not (any (\ (nm,_,_) -> nm == "_") cses)
       valName <- fresh
@@ -859,6 +876,10 @@ bindCT (CApp fun arg) ctx =
 bindCT (CCon nam arg) ctx =
   let arg' = map (\(f, x) -> (f, bindCT x ctx)) arg in
   CCon nam arg'
+bindCT (CUpd trm arg) ctx =
+  let trm' = bindCT trm ctx in
+  let arg' = map (\(f, x) -> (f, bindCT x ctx)) arg in
+  CUpd trm' arg'
 bindCT (CMat val cse) ctx =
   let val' = bindCT val ctx in
   let cse' = map (\(cn,fs,cb) -> (cn, fs, bindCT cb ctx)) cse in
@@ -943,6 +964,10 @@ rnCT (CApp fun arg) ctx =
 rnCT (CCon nam arg) ctx =
   let arg' = map (\(f, x) -> (f, rnCT x ctx)) arg in
   CCon nam arg'
+rnCT (CUpd trm arg) ctx =
+  let trm' = rnCT trm ctx in
+  let arg' = map (\(f, x) -> (f, rnCT x ctx)) arg in
+  CUpd trm' arg'
 rnCT (CMat val cse) ctx =
   let val' = rnCT val ctx in
   let cse' = map (\(cn,fs,cb) -> (cn, fs, rnCT cb ctx)) cse in
@@ -1034,6 +1059,7 @@ showCT (CLam (nam,inp) bod)     dep = "λ(" ++ nam ++ ": " ++ showCT inp dep ++
 showCT (CAll (nam,inp) bod)     dep = "∀(" ++ nam ++ ": " ++ showCT inp dep ++ "). " ++ showCT (bod (CVar nam dep)) (dep+1)
 showCT (CApp fun arg)           dep = "(" ++ showCT fun dep ++ " " ++ showCT arg dep ++ ")"
 showCT (CCon nam fields)        dep = "#" ++ nam ++ "{" ++ concatMap (\ (f,v) -> f ++ ":" ++ showCT v dep ++ " ") fields ++ "}"
+showCT (CUpd trm fields)        dep = "record " ++ showCT trm dep ++ "{" ++ concatMap (\ (f,v) -> f ++ ":" ++ showCT v dep ++ " ") fields ++ "}"
 showCT (CMat val cses)          dep = "match " ++ showCT val dep ++ " {" ++ concatMap (\(cn,fs,cb) -> "#" ++ cn ++ ":" ++ showCT cb dep ++ " ") cses ++ "}"
 showCT (CRef nam)               dep = nam
 showCT (CHol nam)               dep = nam

src/Kind/Parse.hs

@@ -183,6 +183,7 @@ parseTerm = do
     , (parseADT,             discard $ string_skp "#[" <|> string_skp "data[")
     , (parseNat,             discard $ string_skp "#" >> digit)
     , (parseCon,             discard $ string_skp "#" >> name)
+    , (parseUpd,             discard $ string_skp "record ")
     , ((parseUse parseTerm), discard $ string_skp "use ")
     , ((parseLet parseTerm), discard $ string_skp "let ")
     , ((parseGet parseTerm), discard $ string_skp "get ")
@@ -315,6 +316,28 @@ parseCon = withSrc $ do
     return args
   return $ Con nam args
 
+parseUpd = withSrc $ do
+  string_skp "record"
+  skip
+
+  term <- parseTerm
+  skip
+
+  args <- P.option [] $ P.try $ do
+    skip
+    char_skp '{'
+    args <- P.many $ do
+      P.notFollowedBy (char_skp '}')
+      name <- do
+        name <- name_skp
+        char_skp ':'
+        return name
+      term <- parseTerm
+      return (name, term)
+    char '}'
+    return args
+  return $ Upd term args
+
 parseMatCases :: Parser [(String, Term)]
 parseMatCases = do
   cse <- P.many $ P.try $ do

src/Kind/Reduce.hs

@@ -40,6 +40,7 @@ reduce book fill lv term = red term where
   red (Log msg nxt)     = log msg nxt
   red (Get g n m k b)   = get g n (red m) (red k) b
   red (Put g n m k v b) = put g n (red m) (red k) v b
+  red (Upd trm args)    = upd (reduce book fill lv trm) args
   red val               = val
 
   app (Ref nam)     arg | lv > 0 = app (ref nam) arg
@@ -129,6 +130,54 @@ reduce book fill lv term = red term where
     Nothing -> red (b d (KVs (IM.insert (fromIntegral k) v kvs) d))
   put g n m k v b = Put g n m k v b
 
+  -- Performance could be better if there was an earlier stage of compilation to force every constructor
+  -- to have its field names
+  upd (Con cnam cargs) changes = 
+    case findADT <$> (M.lookup cnam book) of
+      Just (ADT adtScp [adtCts] adtTyp) -> do
+        let (Ctr _ cTel) = adtCts
+        let fields = getFields cTel
+        let named = nameAllFields cargs fields
+        let updated = foldl' replace named changes
+        Con cnam (map (\(nam, trm) -> (Just nam, trm)) updated)
+      _ ->
+        error ("critical error: couldn't find ADT for: " ++ cnam)
+    where
+      updateArgs ((Just argName, argVal) : otherArgs) changes@((changeName, changeVal) : otherChanges) = 
+        if argName == changeName
+          then (Just argName, changeVal) : updateArgs otherArgs otherChanges
+          else (Just argName, argVal)    : updateArgs otherArgs changes
+      updateArgs args changes = args
+
+      findADT :: Term -> Term
+      findADT adt@(ADT _ _ _) = adt
+      findADT (Ann _ t _) = findADT t
+      findADT (Lam _ f) = findADT (f Set)
+      findADT (Src _ t) = findADT t
+      findADT trm = trm
+
+      getFields :: Tele -> [String]
+      getFields (TRet _) = []
+      getFields (TExt nam t f) = nam : getFields (f t)
+
+      nameAllFields :: [(Maybe String, Term)] -> [String] -> [(String, Term)]
+      nameAllFields ((Just thisName, term) : rest) (thatName : names) =
+        if thisName == thatName
+          then (thisName, term) : nameAllFields rest (thatName : names)
+          else (thisName, term) : nameAllFields rest names
+      nameAllFields ((Nothing, term) : rest) (thatName : names) =
+        (thatName, term) : nameAllFields rest names
+      nameAllFields [] _ = []
+
+      replace :: Eq a => [(a, b)] -> (a, b) -> [(a, b)]
+      replace [] _ = []
+      replace (cur@(curKey, curVal) : xs) (key, val) =
+        if curKey == key
+          then (key, val) : xs
+          else cur        : replace xs (key, val)
+
+  upd trm changes = trace (showTerm trm) $ Upd trm changes
+
 -- Logging
 -- -------
 
@@ -181,6 +230,10 @@ normal book fill lv term dep = go (reduce book fill lv term) dep where
   go (Con nam arg) dep =
     let nf_arg = map (\(f, t) -> (f, normal book fill lv t dep)) arg in
     Con nam nf_arg
+  go (Upd trm arg) dep =
+    let nf_trm = normal book fill lv trm dep in
+    let nf_arg = map (\(f, t) -> (f, normal book fill lv t dep)) arg in
+    Upd nf_trm nf_arg
   go (Mat cse) dep =
     let nf_cse = map (\(cnam, cbod) -> (cnam, normal book fill lv cbod dep)) cse in
     Mat nf_cse
@@ -289,6 +342,10 @@ bind (ADT scp cts typ) ctx =
 bind (Con nam arg) ctx =
   let arg' = map (\(f, x) -> (f, bind x ctx)) arg in
   Con nam arg'
+bind (Upd trm arg) ctx =
+  let trm' = bind trm ctx in
+  let arg' = map (\(n, x) -> (n, bind x ctx)) arg in
+  Upd trm' arg'
 bind (Mat cse) ctx =
   let cse' = map (\(cn,cb) -> (cn, bind cb ctx)) cse in
   Mat cse'
@@ -388,6 +445,10 @@ genMetasGo (ADT scp cts typ) c =
 genMetasGo (Con nam arg) c = 
   let (arg', c1) = foldr (\(f, t) (acc, c') -> let (t', c'') = genMetasGo t c' in ((f, t'):acc, c'')) ([], c) arg
   in (Con nam arg', c1)
+genMetasGo (Upd trm arg) c =
+  let (trm', c') = genMetasGo trm c in
+  let (arg', c1) = foldr (\(f, t) (acc, c') -> let (t', c'') = genMetasGo t c' in ((f, t'):acc, c'')) ([], c') arg
+  in (Upd trm' arg', c1)
 genMetasGo (Mat cse) c = 
   let (cse', c1) = foldr (\(cn, cb) (acc, c') -> let (cb', c'') = genMetasGo cb c' in ((cn, cb'):acc, c'')) ([], c) cse
   in (Mat cse', c1)

src/Kind/Show.hs

@@ -66,6 +66,11 @@ showTermGo small term dep =
           showArg (maybeField, term) = case maybeField of
             Just field -> field ++ ": " ++ showTermGo small term dep
             Nothing -> showTermGo small term dep
+      Upd trm arg ->
+        let arg' = unwords (map showArg arg)
+        in concat ["record", " ", showTermGo small trm dep, " ", "{", arg', "}"]
+        where
+          showArg (field, term) = field ++ ": " ++ showTermGo small term dep
       Mat cse ->
         let cse' = unwords (map (\(cnm, cbod) -> "#" ++ cnm ++ ": " ++ showTermGo small cbod dep) cse)
         in concat ["λ{ ", cse', " }"]

src/Kind/Type.hs

@@ -33,6 +33,9 @@ data Term
   -- Constructor: `#CN { x0 x1 ... }`
   | Con String [(Maybe String, Term)]
 
+  -- Record update syntax: `record x {a: 0 b: 1 ...}`
+  | Upd Term [(String, Term)]
+
   -- Lambda-Match: `λ{ #C0:B0 #C1:B1 ... }`
   | Mat [(String, Term)]
 

src/Kind/Util.hs

@@ -26,6 +26,7 @@ getDeps term = case term of
   Ins val         -> getDeps val
   ADT scp cts t   -> concatMap getDeps scp ++ concatMap getDepsCtr cts ++ getDeps t
   Con _ arg       -> concatMap (getDeps . snd) arg
+  Upd trm arg     -> getDeps trm ++ concatMap (getDeps . snd) arg
   Mat cse         -> concatMap (getDeps . snd) cse
   Let _ val bod   -> getDeps val ++ getDeps (bod Set)
   Use _ val bod   -> getDeps val ++ getDeps (bod Set)