From c8b8b729ebb5b061b84341c04f7b6fbcbec81d4d Mon Sep 17 00:00:00 2001 From: Victor Taelin Date: Thu, 31 Oct 2024 11:37:32 -0300 Subject: [PATCH] native Map type Example: main : (Pair (Map U64) U64) = let map = { 1:10 2:20 | 0 } put old_val = new_map@map[1] := 100 #Pair{new_map old_val} Will: 1. set 'map[1]' to '100', assigning the result to the 'new_map' name 2. return the old value as 'old_val' (or the default, '0', if absent) The result is: Pair{{1:100 2:20 | 0} 10} We can also abbreviate it when the new name == the map name: main : (Pair (Map U64) U64) = let map = { 1:10 2:20 | 0 } put old = map[1] := 100 #Pair{map old} And we can omit 'old' when we don't need it: main : (Map U64) = let map = { 1:10 2:20 | 0 } put map[1] := 100 map There is also a 'get' operation, which just retrieves a value: main : U64 = let map = { 1:10 2:20 | 0 } get val = map[1] val --- src/Kind/Check.hs | 85 +++++++++++++++++++++++++++ src/Kind/CompileJS.hs | 132 ++++++++++++++++++++++++++++++++++++++++-- src/Kind/Equal.hs | 89 ++++++++++++++++++++++++++-- src/Kind/Parse.hs | 66 +++++++++++++++++---- src/Kind/Reduce.hs | 71 +++++++++++++++++++++++ src/Kind/Show.hs | 22 +++++++ src/Kind/Type.hs | 61 +++++++++++++------ src/Kind/Util.hs | 59 ++++++++++--------- 8 files changed, 516 insertions(+), 69 deletions(-) diff --git a/src/Kind/Check.hs b/src/Kind/Check.hs index 55c1a82c0..0d0f40ed4 100644 --- a/src/Kind/Check.hs +++ b/src/Kind/Check.hs @@ -116,6 +116,48 @@ infer sus src term dep = debug ("infer:" ++ (if sus then "* " else " ") ++ showT envLog (Error src (Ref "annotation") (Ref "switch") (Swi zer suc) dep) envFail + go (Map typ) = do + typA <- checkLater sus src typ Set dep + return $ Ann False (Map typA) Set + + go (KVs kvs dft) = do + dftA <- infer sus src dft dep + kvsA <- forM (IM.toList kvs) $ \(key, val ) -> do + valA <- check sus src val (getType dftA) dep + return (key, valA) + return $ Ann False (KVs (IM.fromList kvsA) dftA) (Map (getType dftA)) + + go (Get got nam map key bod) = do + mapA <- infer sus src map dep + book <- envGetBook + fill <- envGetFill + case reduce book fill 2 (getType mapA) of + (Map typ) -> do + let got_ann = Ann False (Var got dep) typ + let nam_ann = Ann False (Var nam dep) (Map typ) + keyA <- check sus src key U64 dep + bodA <- infer sus src (bod got_ann nam_ann) dep + return $ Ann False (Get got nam mapA keyA (\g m -> bodA)) (getType bodA) + otherwise -> do + envLog (Error src (Ref "Map") (getType mapA) (Get got nam map key bod) dep) + envFail + + go (Put got nam map key val bod) = do + mapA <- infer sus src map dep + book <- envGetBook + fill <- envGetFill + case reduce book fill 2 (getType mapA) of + (Map typ) -> do + valA <- check sus src val typ dep + let got_ann = Ann False (Var got dep) typ + let nam_ann = Ann False (Var nam dep) (Map typ) + keyA <- check sus src key U64 dep + bodA <- infer sus src (bod got_ann nam_ann) dep + return $ Ann False (Put got nam mapA keyA valA (\g m -> bodA)) (getType bodA) + otherwise -> do + envLog (Error src (Ref "Map") (getType mapA) (Put got nam map key val bod) dep) + envFail + go (Let nam val bod) = do valA <- infer sus src val dep bodA <- infer sus src (bod (Ann False (Var nam dep) (getType valA))) dep @@ -306,6 +348,49 @@ check sus src term typx dep = debug ("check:" ++ (if sus then "* " else " ") ++ otherwise -> infer sus src (Swi zer suc) dep otherwise -> infer sus src (Swi zer suc) dep + go (KVs kvs dft) = do + book <- envGetBook + fill <- envGetFill + case reduce book fill 2 typx of + (Map typ) -> do + dftA <- check sus src dft typ dep + kvsA <- forM (IM.toList kvs) $ \(key, val) -> do + valA <- check sus src val typ dep + return (key, valA) + return $ Ann False (KVs (IM.fromList kvsA) dftA) typx + otherwise -> infer sus src (KVs kvs dft) dep + + go (Get got nam map key bod) = do + mapA <- infer sus src map dep + book <- envGetBook + fill <- envGetFill + case reduce book fill 2 (getType mapA) of + (Map typ) -> do + let got_ann = Ann False (Var got dep) typ + let nam_ann = Ann False (Var nam dep) (Map typ) + keyA <- check sus src key U64 dep + bodA <- check sus src (bod got_ann nam_ann) typx dep + return $ Ann False (Get got nam mapA keyA (\g m -> bodA)) typx + otherwise -> do + envLog (Error src (Ref "Map") (getType mapA) (Get got nam map key bod) dep) + envFail + + go (Put got nam map key val bod) = do + mapA <- infer sus src map dep + book <- envGetBook + fill <- envGetFill + case reduce book fill 2 (getType mapA) of + (Map typ) -> do + valA <- check sus src val typ dep + let got_ann = Ann False (Var got dep) typ + let nam_ann = Ann False (Var nam dep) (Map typ) + keyA <- check sus src key U64 dep + bodA <- check sus src (bod got_ann nam_ann) typx dep + return $ Ann False (Put got nam mapA keyA valA (\g m -> bodA)) typx + otherwise -> do + envLog (Error src (Ref "Map") (getType mapA) (Put got nam map key val bod) dep) + envFail + go (Let nam val bod) = do valA <- infer sus src val dep bodA <- check sus src (bod (Ann False (Var nam dep) (getType valA))) typx dep diff --git a/src/Kind/CompileJS.hs b/src/Kind/CompileJS.hs index 467ea358a..e4b507379 100644 --- a/src/Kind/CompileJS.hs +++ b/src/Kind/CompileJS.hs @@ -1,6 +1,11 @@ --- Checker: +-- Type.hs: -- //./Type.hs// +-- FIXME: currently, the Map type will compile to a mutable map in JS, which +-- means we assume it is used linearly (no cloning). To improve this, we can add +-- a shallow-cloning operation for cloned maps, or use an immutable map. Adding +-- linearity checks to Kind would let us pick the best representation. + {-# LANGUAGE ViewPatterns #-} module Kind.CompileJS where @@ -43,6 +48,9 @@ data CT | CFlt Double | COp2 Oper CT CT | CSwi CT CT CT + | CKVs (IM.IntMap CT) CT + | CGet String String CT CT (CT -> CT -> CT) + | CPut String String CT CT CT (CT -> CT -> CT) | CLog CT CT | CVar String Int | CTxt String @@ -109,6 +117,23 @@ termToCT book fill term typx dep = bindCT (t2ct term typx dep) [] where let zer' = t2ct zer Nothing dep suc' = t2ct suc Nothing dep in CLam ("__" ++ show dep) $ \x -> CSwi x zer' suc' + go (Map typ) = + CNul + go (KVs kvs def) = + let kvs' = IM.map (\v -> t2ct v Nothing dep) kvs + def' = t2ct def Nothing dep + in CKVs kvs' def' + go (Get got nam map key bod) = + let map' = t2ct map Nothing dep + key' = t2ct key Nothing dep + bod' = \x y -> t2ct (bod (Var got dep) (Var nam dep)) Nothing (dep+2) + in CGet got nam map' key' bod' + go (Put got nam map key val bod) = + let map' = t2ct map Nothing dep + key' = t2ct key Nothing dep + 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) = @@ -191,6 +216,21 @@ removeUnreachables ct = go ct where zer' = go zer suc' = go suc in CSwi val' zer' suc' + go (CKVs kvs def) = + let kvs' = IM.map go kvs + def' = go def + in CKVs kvs' def' + go (CGet got nam map key bod) = + let map' = go map + key' = go key + bod' = \x y -> go (bod x y) + in CGet got nam map' key' bod' + go (CPut got nam map key val bod) = + let map' = go map + key' = go key + val' = go val + bod' = \x y -> go (bod x y) + in CPut got nam map' key' val' bod' go (CLog msg nxt) = let msg' = go msg nxt' = go nxt @@ -281,6 +321,9 @@ inline book ct = nf ct where go (CFlt val) = CFlt val go (COp2 opr fst snd) = COp2 opr (nf fst) (nf snd) go (CSwi val zer suc) = CSwi (nf val) (nf zer) (nf suc) + go (CKVs kvs def) = CKVs (IM.map nf kvs) (nf def) + go (CGet g n m k b) = CGet g n (nf m) (nf k) (\x y -> nf (b x y)) + go (CPut g n m k v b) = CPut g n (nf m) (nf k) (nf v) (\x y -> nf (b x y)) go (CLog msg nxt) = CLog (nf msg) (nf nxt) go (CVar nam idx) = CVar nam idx go (CTxt txt) = CTxt txt @@ -421,7 +464,9 @@ fnToJS book fnName (getArguments -> (fnArgs, fnBody)) = do -- Compiles a CT to JS ctToJS :: Bool -> Maybe String -> CT -> Int -> ST.State Int String - ctToJS tail var term dep = go (red book term) where + ctToJS tail var term dep = + trace ("COMPILE: " ++ showCT term 0) $ + go (red book term) where go CNul = ret var "null" go tm@(CLam nam bod) = do @@ -518,7 +563,7 @@ fnToJS book fnName (getArguments -> (fnArgs, fnBody)) = do else concat [valStmt, "switch (", valName, ".$) { ", unwords cases, " }"] case var of Just var -> return $ switch - Nothing -> ret var $ concat ["((B) => { var ", retName, ";", switch, " return ", retName, " })()"] + Nothing -> return $ concat ["((B) => { var ", retName, ";", switch, " return ", retName, " })()"] go (CSwi val zer suc) = do valName <- fresh valStmt <- ctToJS False (Just valName) val dep @@ -527,10 +572,52 @@ fnToJS book fnName (getArguments -> (fnArgs, fnBody)) = do Nothing -> fresh zerStmt <- ctToJS tail (Just retName) zer dep sucStmt <- ctToJS tail (Just retName) (CApp suc (COp2 SUB (CVar valName 0) (CNum 1))) dep - let ifelse = concat [valStmt, "if (", valName, " === 0n) { ", zerStmt, " } else { ", sucStmt, " }"] + let swiStmt = concat [valStmt, "if (", valName, " === 0n) { ", zerStmt, " } else { ", sucStmt, " }"] + case var of + Just var -> return $ swiStmt + Nothing -> return $ concat ["((C) => { var ", retName, ";", swiStmt, " return ", retName, " })()"] + go (CKVs kvs def) = do + retName <- case var of + Just var -> return var + Nothing -> fresh + dftStmt <- do + dftName <- fresh + dftStmt <- ctToJS False (Just dftName) def dep + return $ concat [dftStmt, retName, ".set(-1n, ", dftName, ");"] + kvStmts <- forM (IM.toList kvs) $ \(k, v) -> do + valName <- fresh + valStmt <- ctToJS False (Just valName) v dep + return $ concat [valStmt, retName, ".set(", show k, "n, ", valName, ");"] + let mapStmt = concat ["var ", retName, " = new Map();", unwords kvStmts, dftStmt] case var of - Just var -> return $ ifelse - Nothing -> ret var $ concat ["((C) => { var ", retName, ";", ifelse, " return ", retName, " })()"] + Just var -> return $ mapStmt + Nothing -> return $ concat ["((E) => {", mapStmt, "return ", retName, "})()"] + go (CGet got nam map key bod) = do + mapName <- fresh + mapStmt <- ctToJS False (Just mapName) map dep + keyName <- fresh + keyStmt <- ctToJS False (Just keyName) key dep + neoName <- fresh + gotName <- fresh + retStmt <- ctToJS tail var (bod (CVar gotName dep) (CVar neoName dep)) dep + let neoUid = nameToJS nam ++ "$" ++ show dep + let gotUid = nameToJS got ++ "$" ++ show dep + let gotStmt = concat ["var ", gotName, " = ", mapName, ".has(", keyName, ") ? ", mapName, ".get(", keyName, ") : ", mapName, ".get(-1n);"] + let neoStmt = concat ["var ", neoName, " = ", mapName, ";"] + return $ concat [mapStmt, keyStmt, gotStmt, retStmt] + go (CPut got nam map key val bod) = do + mapName <- fresh + mapStmt <- ctToJS False (Just mapName) map dep + keyName <- fresh + keyStmt <- ctToJS False (Just keyName) key dep + valName <- fresh + valStmt <- ctToJS False (Just valName) val dep + neoName <- fresh + gotName <- fresh + let gotStmt = concat ["var ", gotName, " = ", mapName, ".has(", keyName, ") ? ", mapName, ".get(", keyName, ") : ", mapName, ".get(-1n);"] + let neoStmt = concat ["var ", neoName, " = ", mapName, "; ", mapName, ".set(", keyName, ", ", valName, ");"] + retStmt <- ctToJS tail var (bod (CVar gotName dep) (CVar neoName dep)) dep + return $ concat [mapStmt, keyStmt, valStmt, gotStmt, neoStmt, retStmt] go (CRef nam) = ret var $ nameToJS nam go (CHol nam) = @@ -665,6 +752,21 @@ bindCT (CSwi val zer suc) ctx = let zer' = bindCT zer ctx in let suc' = bindCT suc ctx in CSwi val' zer' suc' +bindCT (CKVs kvs def) ctx = + let kvs' = IM.map (\v -> bindCT v ctx) kvs in + let def' = bindCT def ctx in + CKVs kvs' def' +bindCT (CGet got nam map key bod) ctx = + let map' = bindCT map ctx in + let key' = bindCT key ctx in + let bod' = \x y -> bindCT (bod (CVar got 0) (CVar nam 0)) ((nam, y) : (got, x) : ctx) in + CGet got nam map' key' bod' +bindCT (CPut got nam map key val bod) ctx = + let map' = bindCT map ctx in + let key' = bindCT key ctx in + let val' = bindCT val ctx in + let bod' = \x y -> bindCT (bod (CVar got 0) (CVar nam 0)) ((nam, y) : (got, x) : ctx) in + CPut got nam map' key' val' bod' bindCT (CLog msg nxt) ctx = let msg' = bindCT msg ctx in let nxt' = bindCT nxt ctx in @@ -718,6 +820,21 @@ rnCT (CSwi val zer suc) ctx = let zer' = rnCT zer ctx in let suc' = rnCT suc ctx in CSwi val' zer' suc' +rnCT (CKVs kvs def) ctx = + let kvs' = IM.map (\v -> rnCT v ctx) kvs in + let def' = rnCT def ctx in + CKVs kvs' def' +rnCT (CGet got nam map key bod) ctx = + let map' = rnCT map ctx in + let key' = rnCT key ctx in + let bod' = \x y -> rnCT (bod (CVar got 0) (CVar nam 0)) ((got, x) : (nam, y) : ctx) in + CGet got nam map' key' bod' +rnCT (CPut got nam map key val bod) ctx = + let map' = rnCT map ctx in + let key' = rnCT key ctx in + let val' = rnCT val ctx in + let bod' = \x y -> rnCT (bod (CVar got 0) (CVar nam 0)) ((got, x) : (nam, y) : ctx) in + CPut got nam map' key' val' bod' rnCT (CLog msg nxt) ctx = let msg' = rnCT msg ctx in let nxt' = rnCT nxt ctx in @@ -759,6 +876,9 @@ showCT (CNum val) dep = show val showCT (CFlt val) dep = show val showCT (COp2 opr fst snd) dep = "( " ++ showCT fst dep ++ " " ++ showCT snd dep ++ ")" showCT (CSwi val zer suc) dep = "switch " ++ showCT val dep ++ " {0:" ++ showCT zer dep ++ " _: " ++ showCT suc dep ++ "}" +showCT (CKVs kvs def) dep = "{" ++ unwords (map (\(k,v) -> show k ++ ":" ++ showCT v dep) (IM.toList kvs)) ++ " | " ++ showCT def dep ++ "}" +showCT (CGet g n m k b) dep = "get " ++ g ++ " = " ++ n ++ "@" ++ showCT m dep ++ "[" ++ showCT k dep ++ "] " ++ showCT (b (CVar g dep) (CVar n dep)) (dep+2) +showCT (CPut g n m k v b) dep = "put " ++ g ++ " = " ++ n ++ "@" ++ showCT m dep ++ "[" ++ showCT k dep ++ "] := " ++ showCT v dep ++ " " ++ showCT (b (CVar g dep) (CVar n dep)) (dep+2) showCT (CLog msg nxt) dep = "log(" ++ showCT msg dep ++ "," ++ showCT nxt dep ++ ")" showCT (CVar nam dep) _ = nam ++ "^" ++ show dep showCT (CTxt txt) dep = show txt diff --git a/src/Kind/Equal.hs b/src/Kind/Equal.hs index 595f7e747..c9ae3e457 100644 --- a/src/Kind/Equal.hs +++ b/src/Kind/Equal.hs @@ -66,10 +66,6 @@ identical a b dep = do identical a bVal dep go (ADT aScp aCts aTyp) (ADT bScp bCts bTyp) dep = do identical aTyp bTyp dep - -- iSlf <- zipWithM (\ax bx -> identical ax bx dep) aScp bScp - -- if and iSlf && length aCts == length bCts - -- then and <$> zipWithM goCtr aCts bCts - -- else return False go (Con aNam aArg) (Con bNam bArg) dep = do if aNam == bNam && length aArg == length bArg then and <$> zipWithM (\(_, aVal) (_, bVal) -> identical aVal bVal dep) aArg bArg @@ -126,6 +122,26 @@ identical a b dep = do iZer <- identical aZer bZer dep iSuc <- identical aSuc bSuc dep return (iZer && iSuc) + go (Map aTyp) (Map bTyp) dep = + identical aTyp bTyp dep + go (KVs aMap aDef) (KVs bMap bDef) dep = do + iDef <- identical aDef bDef dep + iMap <- flip mapM (IM.toList aMap) $ \ (aKey,aVal) -> + case IM.lookup aKey bMap of + Just bVal -> identical aVal bVal dep + Nothing -> return False + return (iDef && and iMap && IM.size aMap == IM.size bMap) + go (Get aGot aNam aMap aKey aBod) (Get bGot bNam bMap bKey bBod) dep = do + iMap <- identical aMap bMap dep + iKey <- identical aKey bKey dep + iBod <- identical (aBod (Var aGot dep) (Var aNam dep)) (bBod (Var bGot dep) (Var bNam dep)) (dep + 2) + return (iMap && iKey && iBod) + go (Put aGot aNam aMap aKey aVal aBod) (Put bGot bNam bMap bKey bVal bBod) dep = do + iMap <- identical aMap bMap dep + iKey <- identical aKey bKey dep + iVal <- identical aVal bVal dep + iBod <- identical (aBod (Var aGot dep) (Var aNam dep)) (bBod (Var bGot dep) (Var bNam dep)) (dep + 2) + return (iMap && iKey && iVal && iBod) go (Txt aTxt) (Txt bTxt) dep = return (aTxt == bTxt) go (Lst aLst) (Lst bLst) dep = @@ -202,6 +218,26 @@ similar a b dep = go a b dep where eZer <- equal aZer bZer dep eSuc <- equal aSuc bSuc dep return (eZer && eSuc) + go (Map aTyp) (Map bTyp) dep = do + equal aTyp bTyp dep + go (KVs aMap aDef) (KVs bMap bDef) dep = do + eDef <- equal aDef bDef dep + eMap <- flip mapM (IM.toList aMap) $ \ (aKey,aVal) -> + case IM.lookup aKey bMap of + Just bVal -> equal aVal bVal dep + Nothing -> return False + return (eDef && and eMap && IM.size aMap == IM.size bMap) + go (Get aGot aNam aMap aKey aBod) (Get bGot bNam bMap bKey bBod) dep = do + eMap <- equal aMap bMap dep + eKey <- equal aKey bKey dep + eBod <- equal (aBod (Var aGot dep) (Var aNam dep)) (bBod (Var bGot dep) (Var bNam dep)) (dep + 2) + return (eMap && eKey && eBod) + go (Put aGot aNam aMap aKey aVal aBod) (Put bGot bNam bMap bKey bVal bBod) dep = do + eMap <- equal aMap bMap dep + eKey <- equal aKey bKey dep + eVal <- equal aVal bVal dep + eBod <- equal (aBod (Var aGot dep) (Var aNam dep)) (bBod (Var bGot dep) (Var bNam dep)) (dep + 2) + return (eMap && eKey && eVal && eBod) go a b dep = identical a b dep goCtr (Ctr aCNm aTele) (Ctr bCNm bTele) = do @@ -322,6 +358,24 @@ occur book fill uid term dep = go term dep where let o_zer = go zer dep o_suc = go suc dep in o_zer || o_suc + go (Map typ) dep = + let o_typ = go typ dep + in o_typ + go (KVs map def) dep = + let o_map = any (\(_, x) -> go x dep) (IM.toList map) + o_def = go def dep + in o_map || o_def + go (Get got nam map key bod) dep = + let o_map = go map dep + o_key = go key dep + o_bod = go (bod (Var got dep) (Var nam dep)) (dep + 2) + in o_map || o_key || o_bod + go (Put got nam map key val bod) dep = + let o_map = go map dep + o_key = go key dep + o_val = go val dep + o_bod = go (bod (Var got dep) (Var nam dep)) (dep + 2) + in o_map || o_key || o_val || o_bod go (Src src val) dep = let o_val = go val dep in o_val @@ -415,6 +469,23 @@ same (Op2 aOpr aFst aSnd) (Op2 bOpr bFst bSnd) dep = same aFst bFst dep && same aSnd bSnd dep same (Swi aZer aSuc) (Swi bZer bSuc) dep = same aZer bZer dep && same aSuc bSuc dep +same (Map aTyp) (Map bTyp) dep = + same aTyp bTyp dep +same (KVs aMap aDef) (KVs bMap bDef) dep = + let sDef = same aDef bDef dep + sMap = IM.size aMap == IM.size bMap && and (map (\ (aKey,aVal) -> maybe False (\bVal -> same aVal bVal dep) (IM.lookup aKey bMap)) (IM.toList aMap)) + in sDef && sMap +same (Get aGot aNam aMap aKey aBod) (Get bGot bNam bMap bKey bBod) dep = + let sMap = same aMap bMap dep + sKey = same aKey bKey dep + sBod = same (aBod (Var aGot dep) (Var aNam dep)) (bBod (Var bGot dep) (Var bNam dep)) (dep + 2) + in sMap && sKey && sBod +same (Put aGot aNam aMap aKey aVal aBod) (Put bGot bNam bMap bKey bVal bBod) dep = + let sMap = same aMap bMap dep + sKey = same aKey bKey dep + sVal = same aVal bVal dep + sBod = same (aBod (Var aGot dep) (Var aNam dep)) (bBod (Var bGot dep) (Var bNam dep)) (dep + 2) + in sMap && sKey && sVal && sBod same (Txt aTxt) (Txt bTxt) dep = aTxt == bTxt same (Lst aLst) (Lst bLst) dep = @@ -465,8 +536,10 @@ subst lvl neo term = go term where go (Con nam arg) = Con nam (map (\(f, t) -> (f, go t)) arg) go (Mat cse) = Mat (map goCse cse) go (Swi zer suc) = Swi (go zer) (go suc) - go (Ref nam) = Ref nam - go (Let nam val bod) = Let nam (go val) (\x -> go (bod (Sub x))) + go (Map typ) = Map (go typ) + go (KVs map def) = KVs (IM.map go map) (go def) + go (Get g n m k b) = Get g n (go m) (go k) (\x y -> go (b x y)) + go (Put g n m k v b) = Put g n (go m) (go k) (go v) (\x y -> go (b x y)) go (Use nam val bod) = Use nam (go val) (\x -> go (bod (Sub x))) go (Met uid spn) = Met uid (map go spn) go (Log msg nxt) = Log (go msg) (go nxt) @@ -501,6 +574,10 @@ replace old neo term dep = if same old term dep then neo else go term where go (Con nam arg) = Con nam (map (\(f, t) -> (f, replace old neo t dep)) arg) go (Mat cse) = Mat (map goCse cse) go (Swi zer suc) = Swi (replace old neo zer dep) (replace old neo suc dep) + go (Map typ) = Map (replace old neo typ dep) + go (KVs map def) = KVs (IM.map (\x -> replace old neo x dep) map) (replace old neo def dep) + go (Get g n m k b) = Get g n (replace old neo m dep) (replace old neo k dep) (\x y -> replace old neo (b x y) (dep+2)) + go (Put g n m k v b) = Put g n (replace old neo m dep) (replace old neo k dep) (replace old neo v dep) (\x y -> replace old neo (b x y) (dep+2)) go (Ref nam) = Ref nam go (Let nam val bod) = Let nam (replace old neo val dep) (\x -> replace old neo (bod (Sub x)) (dep+1)) go (Use nam val bod) = Use nam (replace old neo val dep) (\x -> replace old neo (bod (Sub x)) (dep+1)) diff --git a/src/Kind/Parse.hs b/src/Kind/Parse.hs index 13561529d..f9ee4eec0 100644 --- a/src/Kind/Parse.hs +++ b/src/Kind/Parse.hs @@ -19,6 +19,7 @@ import System.Console.ANSI import Text.Parsec ((), (<|>), getPosition, sourceLine, sourceColumn, getState, setState) import Text.Parsec.Error (errorPos, errorMessages, showErrorMessages, ParseError, errorMessages, Message(..)) import qualified Control.Applicative as A +import qualified Data.IntMap.Strict as IM import qualified Data.Map.Strict as M import qualified Text.Parsec as P @@ -77,7 +78,7 @@ numeric :: Parser String numeric = do head <- P.satisfy (`elem` "0123456789") tail <- P.many (P.satisfy (`elem` "bx0123456789abcdefABCDEF_")) - return $ show (read (head : tail) :: Word64) + return $ show (read (filter (/= '_') (head : tail)) :: Word64) numeric_skp :: Parser String numeric_skp = numeric <* skip @@ -164,8 +165,8 @@ parseTerm = (do , parseLam , parseEra , parseOp2 + , parseMap , parseApp - , parseAnn , parseSlf , parseIns , parseADT @@ -173,10 +174,13 @@ parseTerm = (do , parseCon , (parseUse parseTerm) , (parseLet parseTerm) + , (parseGet parseTerm) + , (parsePut parseTerm) , parseIf , parseWhen , parseMatInl , parseSwiInl + , parseKVs , parseDo , parseSet , parseFloat @@ -227,15 +231,6 @@ parseApp = withSrc $ do char ')' return $ foldl (\f (era, a) -> App f a) fun args -parseAnn = withSrc $ do - char_skp '{' - val <- parseTerm - char_skp ':' - chk <- P.option False (char_skp ':' >> return True) - typ <- parseTerm - char '}' - return $ Ann chk val typ - parseSlf = withSrc $ do string_skp "$(" nam <- name_skp @@ -380,6 +375,55 @@ parseMat = withSrc $ do char '}' return $ Mat cse +-- TODO: implement the Map parsers +parseMap = withSrc $ do + P.try $ string_skp "(Map " + typ <- parseTerm + char ')' + return $ Map typ + +parseKVs = withSrc $ do + char_skp '{' + kvs <- P.many parseKV + char_skp '|' + dft <- parseTerm + char '}' + return $ KVs (IM.fromList kvs) dft + where + parseKV = do + key <- read <$> numeric_skp + char_skp ':' + val <- parseTerm + return (key, val) + +parseGet parseBody = withSrc $ do + P.try $ string_skp "get " + got <- name_skp + string_skp "=" + nam <- name_skp + map <- P.option (Ref nam) $ P.try $ char_skp '@' >> parseTerm + char_skp '[' + key <- parseTerm + char_skp ']' + bod <- parseBody + return $ Get got nam map key (\x y -> bod) + +parsePut parseBody = withSrc $ do + P.try $ string_skp "put " + got <- P.option "_" $ P.try $ do + got <- name_skp + string_skp "=" + return got + nam <- name_skp + map <- P.option (Ref nam) $ P.try $ char_skp '@' >> parseTerm + char_skp '[' + key <- parseTerm + char_skp ']' + string_skp ":=" + val <- parseTerm + bod <- parseBody + return $ Put got nam map key val (\x y -> bod) + parseRef = withSrc $ do name <- name (_, _, uses) <- P.getState diff --git a/src/Kind/Reduce.hs b/src/Kind/Reduce.hs index 359063abd..ee396c815 100644 --- a/src/Kind/Reduce.hs +++ b/src/Kind/Reduce.hs @@ -38,6 +38,8 @@ reduce book fill lv term = red term where red (Src src val) = red val red (Met uid spn) = met uid spn red (Log msg nxt) = log msg nxt + red (Get g n m k b) = get g n m k b + red (Put g n m k v b) = put g n m k v b red val = val app (Ref nam) arg | lv > 0 = app (ref nam) arg @@ -117,6 +119,20 @@ reduce book fill lv term = red term where log msg nxt = logMsg book fill lv msg msg nxt "" + get g n m k b = case (red k, red m) of + (Num k, KVs kvs d) -> case IM.lookup (fromIntegral k) kvs of + Just v -> red (b v (KVs kvs d)) + Nothing -> red (b d (KVs kvs d)) + _ -> Get g n m k b + + put g n m k v b = case (red k, red m) of + (Num k, KVs kvs d) -> case IM.lookup (fromIntegral k) kvs of + Just o -> red (b o (KVs (IM.insert (fromIntegral k) v kvs) d)) + Nothing -> red (b d (KVs (IM.insert (fromIntegral k) v kvs) d)) + _ -> Put g n m k v b + + + -- Logging -- ------- @@ -125,6 +141,7 @@ logMsg book fill lv msg' msg nxt txt = case (reduce book fill lv msg) of Con "Cons" [(_, head), (_, tail)] -> case (reduce book fill lv head) of Num chr -> logMsg book fill lv msg' tail nxt (txt ++ [toEnum (fromIntegral chr)]) + _ -> trace (">> " ++ (showTerm (normal book fill 1 msg' 0))) $ (reduce book fill lv nxt) Con "Nil" [] -> trace txt (reduce book fill lv nxt) _ -> @@ -194,6 +211,24 @@ normal book fill lv term dep = go (reduce book fill lv term) dep where let nf_fst = normal book fill lv fst dep in let nf_snd = normal book fill lv snd dep in Op2 opr nf_fst nf_snd + go (Map typ) dep = + let nf_typ = normal book fill lv typ dep in + Map nf_typ + go (KVs kvs def) dep = + let nf_kvs = IM.map (\x -> normal book fill lv x dep) kvs in + let nf_def = normal book fill lv def dep in + KVs nf_kvs nf_def + go (Get g n m k b) dep = + let nf_m = normal book fill lv m dep in + let nf_k = normal book fill lv k dep in + let nf_b = \v s -> normal book fill lv (b (Var g dep) (Var n dep)) (dep + 2) in + Get g n nf_m nf_k nf_b + go (Put g n m k v b) dep = + let nf_m = normal book fill lv m dep in + let nf_k = normal book fill lv k dep in + let nf_v = normal book fill lv v dep in + let nf_b = \o s -> normal book fill lv (b (Var g dep) (Var n dep)) (dep + 2) in + Put g n nf_m nf_k nf_v nf_b go (Txt val) dep = Txt val go (Lst val) dep = let nf_val = map (\x -> normal book fill lv x dep) val in @@ -265,6 +300,24 @@ bind (Swi zer suc) ctx = let zer' = bind zer ctx in let suc' = bind suc ctx in Swi zer' suc' +bind (Map typ) ctx = + let typ' = bind typ ctx in + Map typ' +bind (KVs kvs def) ctx = + let kvs' = IM.map (\x -> bind x ctx) kvs in + let def' = bind def ctx in + KVs kvs' def' +bind (Get g n m k b) ctx = + let m' = bind m ctx in + let k' = bind k ctx in + let b' = \v s -> bind (b v s) ((n, s) : (g, v) : ctx) in + Get g n m' k' b' +bind (Put g n m k v b) ctx = + let m' = bind m ctx in + let k' = bind k ctx in + let v' = bind v ctx in + let b' = \o s -> bind (b o s) ((n, s) : (g, o) : ctx) in + Put g n m' k' v' b' bind (Ref nam) ctx = case lookup nam ctx of Just x -> x @@ -346,6 +399,24 @@ genMetasGo (Swi zer suc) c = let (zer', c1) = genMetasGo zer c (suc', c2) = genMetasGo suc c1 in (Swi zer' suc', c2) +genMetasGo (Map typ) c = + let (typ', c1) = genMetasGo typ c + in (Map typ', c1) +genMetasGo (KVs kvs def) c = + let (def', c1) = genMetasGo def c + (kvs', c2) = foldr (\ (k, t) (acc, c') -> let (t', c'') = genMetasGo t c' in (IM.insert k t' acc, c'')) (IM.empty, c1) (IM.toList kvs) + in (KVs kvs' def', c2) +genMetasGo (Get g n m k b) c = + let (m', c1) = genMetasGo m c + (k', c2) = genMetasGo k c1 + (b', c3) = genMetasGo (b (Var g 0) (Var n 0)) c2 + in (Get g n m' k' (\_ _ -> b'), c3) +genMetasGo (Put g n m k v b) c = + let (m', c1) = genMetasGo m c + (k', c2) = genMetasGo k c1 + (v', c3) = genMetasGo v c2 + (b', c4) = genMetasGo (b (Var g 0) (Var n 0)) c3 + in (Put g n m' k' v' (\_ _ -> b'), c4) genMetasGo (Let nam val bod) c = let (val', c1) = genMetasGo val c (bod', c2) = genMetasGo (bod (Var nam 0)) c1 diff --git a/src/Kind/Show.hs b/src/Kind/Show.hs index fbbad46fa..36203d050 100644 --- a/src/Kind/Show.hs +++ b/src/Kind/Show.hs @@ -99,6 +99,28 @@ showTermGo small term dep = let zero' = showTermGo small zero dep succ' = showTermGo small succ dep in concat ["λ{ 0: ", zero', " _: ", succ', " }"] + Map typ -> + let typ' = showTermGo small typ dep + in concat ["(Map ", typ', ")"] + KVs kvs def -> + let kvs' = unwords (map (\(k, v) -> show k ++ ":" ++ showTermGo small v dep) (IM.toList kvs)) + def' = showTermGo small def dep + in concat ["{", kvs', " | ", def', "}"] + Get got nam map key bod -> + let got' = got + nam' = nam + map' = showTermGo small map dep + key' = showTermGo small key dep + bod' = showTermGo small (bod (Var got dep) (Var nam dep)) (dep + 2) + in concat ["get ", got', " = ", nam', "@", map', "[", key', "] ", bod'] + Put got nam map key val bod -> + let got' = got + nam' = nam + map' = showTermGo small map dep + key' = showTermGo small key dep + val' = showTermGo small val dep + bod' = showTermGo small (bod (Var got dep) (Var nam dep)) (dep + 2) + in concat ["put ", got', " = ", nam', "@", map', "[", key', "] := ", val', " ", bod'] Txt txt -> concat ["\"" , txt , "\""] Lst lst -> concat ["[", unwords (map (\x -> showTermGo small x dep) lst), "]"] Nat val -> concat ["#", (show val)] diff --git a/src/Kind/Type.hs b/src/Kind/Type.hs index ca58267d0..39c84cccd 100644 --- a/src/Kind/Type.hs +++ b/src/Kind/Type.hs @@ -9,63 +9,86 @@ import Data.Word (Word64) -- Kind's AST data Term - -- Product: ∀(x: A) B + -- Product: `∀(x: A) B` = All String Term (Term -> Term) - -- Lambda: λx f + -- Lambda: `λx f` | Lam String (Term -> Term) - -- Application: (fun arg) + -- Application: `(fun arg)` | App Term Term - -- Annotation: {x: T} + -- Annotation: `{x: T}` | Ann Bool Term Term - -- Self-Type: $(x: A) B + -- Self-Type: `$(x: A) B` | Slf String Term (Term -> Term) - -- Self-Inst: ~x + -- Self-Inst: `~x` | Ins Term - -- Datatype: "#[i0 i1...]{ #C0 Tele0 #C1 Tele1 ... } + -- Datatype: `#[i0 i1...]{ #C0 Tele0 #C1 Tele1 ... }` | ADT [Term] [Ctr] Term - -- Constructor: #CN { x0 x1 ... } + -- Constructor: `#CN { x0 x1 ... }` | Con String [(Maybe String, Term)] - -- Match: λ{ #C0:B0 #C1:B1 ... } + -- Lambda-Match: `λ{ #C0:B0 #C1:B1 ... }` | Mat [(String, Term)] - -- Top-Level Reference + -- Top-Level Reference: `Foo` | Ref String - -- Local let-definition + -- Local let-definition: `let x = val body` | Let String Term (Term -> Term) - -- Local use-definition + -- Local use-definition: `use x = val body` | Use String Term (Term -> Term) - -- Type : Type + -- Universe: `Set` | Set - -- U64 Type + -- U64 Type: `U64` | U64 - -- F64 Type + -- F64 Type: `F64` | F64 - -- U64 Value + -- U64 Value: `123` | Num Word64 - -- F64 Value + -- F64 Value: `1.5` | Flt Double - -- Binary Operation + -- Binary Operation: `(+ x y)` | Op2 Oper Term Term - -- U64 Elimination (updated to use splitting lambda) + -- U64 Elimination: `λ{ 0:A 1+p:B }` | Swi Term Term + -- Linear Map Type: `(Map T)` + | Map Term + + -- Linear Map Value: `{ k0:v0 k1:v1 ... | default }` + | KVs (IM.IntMap Term) Term + + -- Linear Map Getter: `get val = nam@map[key] bod` + -- - got is the name of the obtained value + -- - nam is the name of the map + -- - map is the value of the map + -- - key is the key to query + -- - bod is the continuation; receives the value and the same map + | Get String String Term Term (Term -> Term -> Term) + + -- Map Swapper: `put got = nam@map[key] := val body` + -- - got is the name of the old value + -- - nam is the name of the map + -- - map is the value of the map + -- - key is the key to swap + -- - val is the val to insert + -- - bod is the continuation; receives the old value and the changed map + | Put String String Term Term Term (Term -> Term -> Term) + -- Inspection Hole | Hol String [Term] diff --git a/src/Kind/Util.hs b/src/Kind/Util.hs index a268e0a48..9b8db0ac2 100644 --- a/src/Kind/Util.hs +++ b/src/Kind/Util.hs @@ -8,6 +8,7 @@ import Kind.Equal import Prelude hiding (LT, GT, EQ) +import qualified Data.IntMap.Strict as IM import qualified Data.Map.Strict as M import qualified Data.Set as S @@ -16,33 +17,37 @@ import Debug.Trace -- Gets dependencies of a term getDeps :: Term -> [String] getDeps term = case term of - Ref nam -> [nam] - All _ inp out -> getDeps inp ++ getDeps (out Set) - Lam _ bod -> getDeps (bod Set) - App fun arg -> getDeps fun ++ getDeps arg - Ann _ val typ -> getDeps val ++ getDeps typ - Slf _ typ bod -> getDeps typ ++ getDeps (bod Set) - Ins val -> getDeps val - ADT scp cts t -> concatMap getDeps scp ++ concatMap getDepsCtr cts ++ getDeps t - Con _ arg -> 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) - Op2 _ fst snd -> getDeps fst ++ getDeps snd - Swi zer suc -> getDeps zer ++ getDeps suc - Src _ val -> getDeps val - Hol _ args -> concatMap getDeps args - Met _ args -> concatMap getDeps args - Log msg nxt -> getDeps msg ++ getDeps nxt - Var _ _ -> [] - Set -> [] - U64 -> [] - F64 -> [] - Num _ -> [] - Flt _ -> [] - Txt _ -> [] - Lst elems -> concatMap getDeps elems - Nat _ -> [] + Ref nam -> [nam] + All _ inp out -> getDeps inp ++ getDeps (out Set) + Lam _ bod -> getDeps (bod Set) + App fun arg -> getDeps fun ++ getDeps arg + Ann _ val typ -> getDeps val ++ getDeps typ + Slf _ typ bod -> getDeps typ ++ getDeps (bod Set) + Ins val -> getDeps val + ADT scp cts t -> concatMap getDeps scp ++ concatMap getDepsCtr cts ++ getDeps t + Con _ arg -> 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) + Op2 _ fst snd -> getDeps fst ++ getDeps snd + Swi zer suc -> getDeps zer ++ getDeps suc + Map val -> getDeps val + KVs kvs def -> concatMap getDeps (IM.elems kvs) ++ getDeps def + Get _ _ m k b -> getDeps m ++ getDeps k ++ getDeps (b Set Set) + Put _ _ m k v b -> getDeps m ++ getDeps k ++ getDeps v ++ getDeps (b Set Set) + Src _ val -> getDeps val + Hol _ args -> concatMap getDeps args + Met _ args -> concatMap getDeps args + Log msg nxt -> getDeps msg ++ getDeps nxt + Var _ _ -> [] + Set -> [] + U64 -> [] + F64 -> [] + Num _ -> [] + Flt _ -> [] + Txt _ -> [] + Lst elems -> concatMap getDeps elems + Nat _ -> [] -- Gets dependencies of a constructor getDepsCtr :: Ctr -> [String]