diff --git a/src/Kind/Check.hs b/src/Kind/Check.hs index 0569a0805..e85779a21 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,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 diff --git a/src/Kind/CompileJS.hs b/src/Kind/CompileJS.hs index af3651883..f033a975e 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,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 diff --git a/src/Kind/Parse.hs b/src/Kind/Parse.hs index 409b5b27c..7391ba33d 100644 --- a/src/Kind/Parse.hs +++ b/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 diff --git a/src/Kind/Reduce.hs b/src/Kind/Reduce.hs index ed2a03ae9..37419026a 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,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) 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/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)] 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)