From 16b3acd0cdaa1668129d6304200a58cc27a2c034 Mon Sep 17 00:00:00 2001 From: Eduardo Sandalo Porto Date: Thu, 7 Nov 2024 10:54:28 -0300 Subject: [PATCH 1/7] Add record update to the AST and parser --- src/Kind/Parse.hs | 23 +++++++++++++++++++++++ src/Kind/Type.hs | 3 +++ 2 files changed, 26 insertions(+) diff --git a/src/Kind/Parse.hs b/src/Kind/Parse.hs index bc0f4e826..fc87af0e3 100644 --- a/src/Kind/Parse.hs +++ b/src/Kind/Parse.hs @@ -172,6 +172,7 @@ parseTerm = (do , parseADT , parseNat , parseCon + , parseUpd , (parseUse parseTerm) , (parseLet parseTerm) , (parseGet parseTerm) @@ -303,6 +304,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 diff --git a/src/Kind/Type.hs b/src/Kind/Type.hs index 39c84cccd..0f02b27a4 100644 --- a/src/Kind/Type.hs +++ b/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)] From 5efec89976e5db6a2c9d90f571762053bd070f82 Mon Sep 17 00:00:00 2001 From: Eduardo Sandalo Porto Date: Fri, 8 Nov 2024 01:54:26 -0300 Subject: [PATCH 2/7] Add Upd checking --- src/Kind/Check.hs | 53 +++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 53 insertions(+) diff --git a/src/Kind/Check.hs b/src/Kind/Check.hs index 0569a0805..f0f6ebee1 100644 --- a/src/Kind/Check.hs +++ b/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,54 @@ 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) -> + case adtCts of + -- Exactly 1 constructor + [adtCts] -> do + let (Ctr _ cTel) = adtCts + let expectedFields = getFields cTel + 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 + _ -> 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 + getFields :: Tele -> [String] + getFields (TRet trm) = [] + getFields (TExt fld trm f) = fld : getFields (f trm) + + 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 From 950558b1ee69f7fc7f963e237742f81f62c5f907 Mon Sep 17 00:00:00 2001 From: Eduardo Sandalo Porto Date: Fri, 8 Nov 2024 01:54:56 -0300 Subject: [PATCH 3/7] Add Upd reducing --- src/Kind/Reduce.hs | 23 +++++++++++++++++++++++ src/Kind/Show.hs | 5 +++++ src/Kind/Util.hs | 1 + 3 files changed, 29 insertions(+) diff --git a/src/Kind/Reduce.hs b/src/Kind/Reduce.hs index ed2a03ae9..9fb6ad61f 100644 --- a/src/Kind/Reduce.hs +++ b/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,16 @@ 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 + -- Requires the original constructor to have been declared with its field names. + -- Updated fields must appear in the same order as the constructor's definition. + upd (Con cnam cargs) changes = Con cnam (updateArgs cargs changes) 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 + upd trm changes = trace (showTerm trm) $ Upd trm changes + -- Logging -- ------- @@ -181,6 +192,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 +304,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 +407,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) diff --git a/src/Kind/Show.hs b/src/Kind/Show.hs index 36203d050..facbfbb5d 100644 --- a/src/Kind/Show.hs +++ b/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', " }"] diff --git a/src/Kind/Util.hs b/src/Kind/Util.hs index 5d0bcf837..7d1facb94 100644 --- a/src/Kind/Util.hs +++ b/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) From 2652e3fb0b09f1607dab29435b3ef9dec96b02e2 Mon Sep 17 00:00:00 2001 From: Eduardo Sandalo Porto Date: Fri, 8 Nov 2024 02:51:38 -0300 Subject: [PATCH 4/7] Add Upd compilation to JS --- src/Kind/CompileJS.hs | 30 +++++++++++++++++++++++++++--- 1 file changed, 27 insertions(+), 3 deletions(-) diff --git a/src/Kind/CompileJS.hs b/src/Kind/CompileJS.hs index af3651883..07098c1e4 100644 --- a/src/Kind/CompileJS.hs +++ b/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,17 @@ 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 + setStmts <- forM fields $ \ (nm, tm) -> do + fldName <- fresh + fldStmt <- ctToJS False fldName tm dep + return $ fldStmt + return $ concat $ + [updStmt] ++ + setStmts ++ + [updName, "= {...", var, ", ", concatMap (\ (f,v) -> f ++ ": " ++ showCT v dep ++ ", ") fields ++ "};"] go (CMat val cses) = do let isRecord = length cses == 1 && not (any (\ (nm,_,_) -> nm == "_") cses) valName <- fresh @@ -859,6 +874,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 +962,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 +1057,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 From 0ee7253b4e00290973b4342bdf61984194107e1e Mon Sep 17 00:00:00 2001 From: Eduardo Sandalo Porto Date: Fri, 8 Nov 2024 11:15:43 -0300 Subject: [PATCH 5/7] Fix update syntax compilation to JS --- src/Kind/CompileJS.hs | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) diff --git a/src/Kind/CompileJS.hs b/src/Kind/CompileJS.hs index 07098c1e4..f033a975e 100644 --- a/src/Kind/CompileJS.hs +++ b/src/Kind/CompileJS.hs @@ -676,14 +676,16 @@ fnToJS book fnName ct@(getArguments -> (fnArgs, fnBody)) = do go (CUpd trm fields) = do updName <- fresh updStmt <- ctToJS False updName trm dep - setStmts <- forM fields $ \ (nm, tm) -> do + setVarsAndStmts <- forM fields $ \ (nm, tm) -> do fldName <- fresh fldStmt <- ctToJS False fldName tm dep - return $ fldStmt + return $ ((nm, fldName), fldStmt) + let (setVars, setStmts) = unzip setVarsAndStmts + let setVarsCode = concatMap (\(field, val) -> field ++ ": " ++ val ++ ", ") setVars return $ concat $ [updStmt] ++ setStmts ++ - [updName, "= {...", var, ", ", concatMap (\ (f,v) -> f ++ ": " ++ showCT v dep ++ ", ") fields ++ "};"] + [var, " = {...", updName, ", ", setVarsCode ++ "};"] go (CMat val cses) = do let isRecord = length cses == 1 && not (any (\ (nm,_,_) -> nm == "_") cses) valName <- fresh From a92d30570704ab852cd9bda17329e2645906d559 Mon Sep 17 00:00:00 2001 From: Eduardo Sandalo Porto Date: Fri, 8 Nov 2024 12:19:54 -0300 Subject: [PATCH 6/7] Have update syntax work on constructors defined in any way --- src/Kind/Check.hs | 45 +++++++++++++++++--------------------- src/Kind/Reduce.hs | 54 +++++++++++++++++++++++++++++++++++++++------- 2 files changed, 66 insertions(+), 33 deletions(-) diff --git a/src/Kind/Check.hs b/src/Kind/Check.hs index f0f6ebee1..e85779a21 100644 --- a/src/Kind/Check.hs +++ b/src/Kind/Check.hs @@ -300,35 +300,30 @@ check sus src term typx dep = debug ("check:" ++ (if sus then "* " else " ") ++ book <- envGetBook fill <- envGetFill case reduce book fill 2 typx of - (ADT adtScp adtCts adtTyp) -> - case adtCts of - -- Exactly 1 constructor - [adtCts] -> do - let (Ctr _ cTel) = adtCts - let expectedFields = getFields cTel - 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 - _ -> 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 + (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 - getFields :: Tele -> [String] - getFields (TRet trm) = [] - getFields (TExt fld trm f) = fld : getFields (f trm) - checkConstructor :: Maybe Cod -> [(String, Term)] -> Tele -> Int -> Env [(String, Term)] checkConstructor src [] (TRet ret) dep = do cmp src val ret typx dep diff --git a/src/Kind/Reduce.hs b/src/Kind/Reduce.hs index 9fb6ad61f..37419026a 100644 --- a/src/Kind/Reduce.hs +++ b/src/Kind/Reduce.hs @@ -130,14 +130,52 @@ 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 - -- Requires the original constructor to have been declared with its field names. - -- Updated fields must appear in the same order as the constructor's definition. - upd (Con cnam cargs) changes = Con cnam (updateArgs cargs changes) 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 + -- 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 From 49ce0e973dafcfd27074241c96ae8694ff258d48 Mon Sep 17 00:00:00 2001 From: Eduardo Sandalo Porto Date: Fri, 8 Nov 2024 12:25:35 -0300 Subject: [PATCH 7/7] Tiny parser change --- src/Kind/Parse.hs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Kind/Parse.hs b/src/Kind/Parse.hs index bcacfa0e8..7391ba33d 100644 --- a/src/Kind/Parse.hs +++ b/src/Kind/Parse.hs @@ -183,7 +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") + , (parseUpd, discard $ string_skp "record ") , ((parseUse parseTerm), discard $ string_skp "use ") , ((parseLet parseTerm), discard $ string_skp "let ") , ((parseGet parseTerm), discard $ string_skp "get ")