From fc32ea9b2488f2918baf4e6c67e98e7d0f08521a Mon Sep 17 00:00:00 2001 From: Nicolas Abril Date: Fri, 8 Nov 2024 21:56:45 +0100 Subject: [PATCH 1/7] Add #Cons constructor syntax --- src/Kind/Parse.hs | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/src/Kind/Parse.hs b/src/Kind/Parse.hs index 409b5b27c..fdc26f630 100644 --- a/src/Kind/Parse.hs +++ b/src/Kind/Parse.hs @@ -617,6 +617,7 @@ parseSuffix term = guardChoice , (parseSuffEql term, discard $ string_skp "==") , (parseSuffPAR term, discard $ string_skp "&") , (parseSuffPar term, discard $ string_skp ",") + , (parseSuffCns term, discard $ string_skp ":") ] $ parseSuffVal term parseSuffArr :: Term -> Parser Term @@ -649,6 +650,12 @@ parseSuffPar fst = do snd <- parseTerm return $ Con "Pair" [(Nothing, fst), (Nothing, snd)] +parseSuffCns :: Term -> Parser Term +parseSuffCns head = do + P.try $ string_skp ":" + tail <- parseTerm + return $ Con "Cons" [(Nothing, head), (Nothing, tail)] + parseSuffVal :: Term -> Parser Term parseSuffVal term = return term From dfc9a67eaf726f7a99e023ca7287650fef6c1641 Mon Sep 17 00:00:00 2001 From: Nicolas Abril Date: Fri, 8 Nov 2024 21:57:15 +0100 Subject: [PATCH 2/7] Add #Cons pattern matching equation syntax sugar --- src/Kind/Parse.hs | 77 ++++++++++++++++++++++++++++++++--------------- 1 file changed, 52 insertions(+), 25 deletions(-) diff --git a/src/Kind/Parse.hs b/src/Kind/Parse.hs index fdc26f630..4f62da2e2 100644 --- a/src/Kind/Parse.hs +++ b/src/Kind/Parse.hs @@ -776,40 +776,67 @@ parseRule dep = do parsePattern :: Parser Pattern parsePattern = do P.notFollowedBy $ string_skp "with " - guardChoice - [ (parsePatternNat, discard $ string_skp "#" >> numeric_skp) - , (parsePatternLst, discard $ string_skp "[") - , (parsePatternCon, discard $ string_skp "#" <|> (name_skp >> string_skp "@")) - , (parsePatternTxt, discard $ string_skp "\"") - , (parsePatternPar, discard $ string_skp "(") - , (parsePatternSuc, discard $ numeric_skp >> char_skp '+') - , (parsePatternNum, discard $ numeric_skp) - , (parsePatternVar, discard $ name_skp) + pat <- guardChoice + [ (parsePatPrn, discard $ string_skp "(") + , (parsePatNat, discard $ string_skp "#" >> numeric_skp) + , (parsePatLst, discard $ string_skp "[") + , (parsePatCon, discard $ string_skp "#" <|> (name_skp >> string_skp "@")) + , (parsePatTxt, discard $ string_skp "\"") + , (parsePatSuc, discard $ numeric_skp >> char_skp '+') + , (parsePatNum, discard $ numeric_skp) + , (parsePatVar, discard $ name_skp) ] $ fail "Pattern-matching" + parsePatSuffix pat -parsePatternNat :: Parser Pattern -parsePatternNat = do +parsePatSuffix :: Pattern -> Parser Pattern +parsePatSuffix pat = P.choice + [ parsePatSuffPar pat + , parsePatSuffCns pat + , return pat + ] + +parsePatSuffPar :: Pattern -> Parser Pattern +parsePatSuffPar fst = do + P.try $ string_skp "," + snd <- parsePattern + return $ PCtr Nothing "Pair" [fst, snd] + +parsePatSuffCns :: Pattern -> Parser Pattern +parsePatSuffCns head = do + P.try $ string_skp ":" + tail <- parsePattern + return $ PCtr Nothing "Cons" [head, tail] + +parsePatPrn :: Parser Pattern +parsePatPrn = do + string_skp "(" + pat <- parsePattern + string_skp ")" + return pat + +parsePatNat :: Parser Pattern +parsePatNat = do char_skp '#' num <- numeric_skp let n = read num return $ (foldr (\_ acc -> PCtr Nothing "Succ" [acc]) (PCtr Nothing "Zero" []) [1..n]) -parsePatternLst :: Parser Pattern -parsePatternLst = do +parsePatLst :: Parser Pattern +parsePatLst = do char_skp '[' elems <- P.many parsePattern char_skp ']' return $ foldr (\x acc -> PCtr Nothing "Cons" [x, acc]) (PCtr Nothing "Nil" []) elems -parsePatternTxt :: Parser Pattern -parsePatternTxt = do +parsePatTxt :: Parser Pattern +parsePatTxt = do char '"' txt <- P.many parseTxtChr char '"' return $ foldr (\x acc -> PCtr Nothing "Cons" [PNum (toEnum (ord x)), acc]) (PCtr Nothing "Nil" []) txt -parsePatternPar :: Parser Pattern -parsePatternPar = do +parsePatPar :: Parser Pattern +parsePatPar = do char_skp '(' head <- parsePattern tail <- P.many $ do @@ -819,8 +846,8 @@ parsePatternPar = do let (init, last) = maybe ([], head) id (unsnoc (head : tail)) return $ foldr (\x acc -> PCtr Nothing "Pair" [x, acc]) last init -parsePatternCon :: Parser Pattern -parsePatternCon = do +parsePatCon :: Parser Pattern +parsePatCon = do name <- P.optionMaybe $ P.try $ do name <- name_skp char_skp '@' @@ -834,20 +861,20 @@ parsePatternCon = do return args return $ (PCtr name cnam args) -parsePatternNum :: Parser Pattern -parsePatternNum = do +parsePatNum :: Parser Pattern +parsePatNum = do num <- numeric_skp return $ (PNum (read num)) -parsePatternSuc :: Parser Pattern -parsePatternSuc = do +parsePatSuc :: Parser Pattern +parsePatSuc = do num <- numeric_skp char_skp '+' nam <- name_skp return $ (PSuc (read num) nam) -parsePatternVar :: Parser Pattern -parsePatternVar = do +parsePatVar :: Parser Pattern +parsePatVar = do name <- name_skp return $ (PVar name) From 8d0a1a5465d479d72fa4fdace3242d8814111e59 Mon Sep 17 00:00:00 2001 From: Nicolas Abril Date: Fri, 8 Nov 2024 22:46:20 +0100 Subject: [PATCH 3/7] Add Source location to terms created by 'with' equations --- src/Kind/Parse.hs | 21 +++++++++------------ 1 file changed, 9 insertions(+), 12 deletions(-) diff --git a/src/Kind/Parse.hs b/src/Kind/Parse.hs index 4f62da2e2..e618abaae 100644 --- a/src/Kind/Parse.hs +++ b/src/Kind/Parse.hs @@ -27,9 +27,8 @@ type Uses = [(String, String)] type PState = (String, Int, Uses) type Parser a = P.ParsecT String PState Identity a -- Types used for flattening pattern-matching equations -type Rule = ([Pattern], With) +type Rule = ([Pattern], Term) data Pattern = PVar String | PCtr (Maybe String) String [Pattern] | PNum Word64 | PSuc Word64 String -data With = WBod Term | WWit [Term] [Rule] -- Helper functions that consume trailing whitespace skip :: Parser () @@ -760,18 +759,18 @@ parseRule dep = do P.count dep $ char_skp '.' char_skp '|' pats <- P.many parsePattern - with <- P.choice - [ P.try $ do + body <- P.choice + [ withSrc $ P.try $ do string_skp "with " wth <- P.many1 $ P.notFollowedBy (char_skp '.') >> parseTerm rul <- P.many1 $ parseRule (dep + 1) - return $ WWit wth rul + return $ flattenWith dep wth rul , P.try $ do char_skp '=' body <- parseTerm - return $ WBod body + return body ] - return $ (pats, with) + return $ (pats, body) parsePattern :: Parser Pattern parsePattern = do @@ -1132,13 +1131,11 @@ parseNat = withSrc $ do -- Flattener for pattern matching equations flattenDef :: [Rule] -> Int -> Term flattenDef rules depth = - let (pats, with) = unzip rules - bods = map (flattenWith 0) with + let (pats, bods) = unzip rules in flattenRules pats bods depth -flattenWith :: Int -> With -> Term -flattenWith dep (WBod bod) = bod -flattenWith dep (WWit wth rul) = +flattenWith :: Int -> [Term] -> [Rule] -> Term +flattenWith dep wth rul = -- Wrap the 'with' arguments and patterns in Pairs since the type checker only takes one match argument. let wthA = foldr1 (\x acc -> Ann True (Con "Pair" [(Nothing, x), (Nothing, acc)]) (App (App (Ref "Pair") (Met 0 [])) (Met 0 []))) wth rulA = map (\(pat, wth) -> ([foldr1 (\x acc -> PCtr Nothing "Pair" [x, acc]) pat], wth)) rul From 5e6c1cdbe1aa29301c88354701b1d629139cb81c Mon Sep 17 00:00:00 2001 From: Nicolas Abril Date: Mon, 11 Nov 2024 12:11:04 +0100 Subject: [PATCH 4/7] Use '^' for Cons syntax sugar --- src/Kind/Parse.hs | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/Kind/Parse.hs b/src/Kind/Parse.hs index e618abaae..25a2b884b 100644 --- a/src/Kind/Parse.hs +++ b/src/Kind/Parse.hs @@ -616,7 +616,7 @@ parseSuffix term = guardChoice , (parseSuffEql term, discard $ string_skp "==") , (parseSuffPAR term, discard $ string_skp "&") , (parseSuffPar term, discard $ string_skp ",") - , (parseSuffCns term, discard $ string_skp ":") + , (parseSuffCns term, discard $ string_skp "^") ] $ parseSuffVal term parseSuffArr :: Term -> Parser Term @@ -651,7 +651,7 @@ parseSuffPar fst = do parseSuffCns :: Term -> Parser Term parseSuffCns head = do - P.try $ string_skp ":" + P.try $ string_skp "^" tail <- parseTerm return $ Con "Cons" [(Nothing, head), (Nothing, tail)] @@ -802,7 +802,7 @@ parsePatSuffPar fst = do parsePatSuffCns :: Pattern -> Parser Pattern parsePatSuffCns head = do - P.try $ string_skp ":" + P.try $ string_skp "^" tail <- parsePattern return $ PCtr Nothing "Cons" [head, tail] From 25005f0520b48976d1f73bde00b1d9e4d74e4d2f Mon Sep 17 00:00:00 2001 From: Nicolas Abril Date: Mon, 11 Nov 2024 13:05:26 +0100 Subject: [PATCH 5/7] Use ;; instead of ^ for Cons syntax sugar --- src/Kind/Parse.hs | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/Kind/Parse.hs b/src/Kind/Parse.hs index 25a2b884b..1a580d5c2 100644 --- a/src/Kind/Parse.hs +++ b/src/Kind/Parse.hs @@ -616,7 +616,7 @@ parseSuffix term = guardChoice , (parseSuffEql term, discard $ string_skp "==") , (parseSuffPAR term, discard $ string_skp "&") , (parseSuffPar term, discard $ string_skp ",") - , (parseSuffCns term, discard $ string_skp "^") + , (parseSuffCns term, discard $ string_skp ";;") ] $ parseSuffVal term parseSuffArr :: Term -> Parser Term @@ -651,7 +651,7 @@ parseSuffPar fst = do parseSuffCns :: Term -> Parser Term parseSuffCns head = do - P.try $ string_skp "^" + P.try $ string_skp ";;" tail <- parseTerm return $ Con "Cons" [(Nothing, head), (Nothing, tail)] @@ -802,7 +802,7 @@ parsePatSuffPar fst = do parsePatSuffCns :: Pattern -> Parser Pattern parsePatSuffCns head = do - P.try $ string_skp "^" + P.try $ string_skp ";;" tail <- parsePattern return $ PCtr Nothing "Cons" [head, tail] From 077ed662bd3abf868fbbbaf6473ac64f6e01f2b7 Mon Sep 17 00:00:00 2001 From: Nicolas Abril Date: Tue, 12 Nov 2024 22:54:56 +0100 Subject: [PATCH 6/7] Add source location to the equational pattern matching terms --- 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 1a580d5c2..070d7e2b6 100644 --- a/src/Kind/Parse.hs +++ b/src/Kind/Parse.hs @@ -743,7 +743,7 @@ parseDefFunSingle = do return val parseDefFunRules :: Parser Term -parseDefFunRules = do +parseDefFunRules = withSrc $ do rules <- P.many1 (parseRule 0) let flat = flattenDef rules 0 return From aae1cc607d32fb4c79e97b822f682347d5faea07 Mon Sep 17 00:00:00 2001 From: Nicolas Abril Date: Tue, 12 Nov 2024 22:55:13 +0100 Subject: [PATCH 7/7] Add IO read exec and args functions --- src/Kind/CompileJS.hs | 50 +++++++++++++++++++++++++++++++++++++++++-- 1 file changed, 48 insertions(+), 2 deletions(-) diff --git a/src/Kind/CompileJS.hs b/src/Kind/CompileJS.hs index af3651883..202dce586 100644 --- a/src/Kind/CompileJS.hs +++ b/src/Kind/CompileJS.hs @@ -446,6 +446,9 @@ ref book nam , "IO/print" , "IO/prompt" , "IO/swap" + , "IO/read" + , "IO/exec" + , "IO/args" ] -- JavaScript Codegen @@ -652,6 +655,25 @@ fnToJS book fnName ct@(getArguments -> (fnArgs, fnBody)) = do return $ concat [textStmt, "console.log(LIST_TO_JSTR(", textName, "));", doneStmt] "IO_PROMPT" -> do error $ "TODO" + "IO_READ" -> do + let [path] = appArgs + pathName <- fresh + pathStmt <- ctToJS False pathName path dep + let readStmt = concat + [ "try { var ", var, " = { $: 'Done', value: JSTR_TO_LIST(readFileSync(LIST_TO_JSTR(", pathName, "), 'utf8')) }; } " + , "catch (e) { var ", var, " = { $: 'Fail', error: e.message }; }" + ] + return $ concat [pathStmt, readStmt] + "IO_EXEC" -> do + let [cmd] = appArgs + cmdName <- fresh + cmdStmt <- ctToJS False cmdName cmd dep + retStmt <- set var $ concat ["JSTR_TO_LIST(execSync(LIST_TO_JSTR(", cmdName, ")).toString())"] + return $ concat [cmdStmt, retStmt] + "IO_ARGS" -> do + let [_] = appArgs + retStmt <- set var "process.argv.slice(2).map(x => JLIST_TO_LIST(x, JSTR_TO_LIST))" + return retStmt _ -> error $ "Unknown IO operation: " ++ name -- Normal Application else do @@ -780,6 +802,9 @@ fnToJS book fnName ct@(getArguments -> (fnArgs, fnBody)) = do prelude :: String prelude = unlines [ + "import { readFileSync } from 'fs';", + "import { execSync } from 'child_process';", + "", "function LIST_TO_JSTR(list) {", " try {", " let result = '';", @@ -803,6 +828,29 @@ prelude = unlines [ " return list;", "}", "", + "function LIST_TO_JLIST(list, decode) {", + " try {", + " let result = [];", + " let current = list;", + " while (current.$ === 'Cons') {", + " result += decode(current.head);", + " current = current.tail;", + " }", + " if (current.$ === 'Nil') {", + " return result;", + " }", + " } catch (e) {}", + " return list;", + "}", + "", + "function JLIST_TO_LIST(inp, encode) {", + " let out = {$: 'Nil'};", + " for (let i = inp.length - 1; i >= 0; i--) {", + " out = {$: 'Cons', head: encode(inp[i]), tail: out};", + " }", + " return out;", + "}", + "", "let MEMORY = new Map();", "function SWAP(key, val) {", " var old = MEMORY.get(key) || 0n;", @@ -951,8 +999,6 @@ rnCT (CRef nam) ctx = case lookup nam ctx of Just x -> x Nothing -> CRef nam -rnCT (CRef nam) ctx = - CHol nam rnCT (CLet (nam,typ) val bod) ctx = let typ' = rnCT typ ctx in let val' = rnCT val ctx in