Skip to content

Commit

Permalink
Merge pull request #615 from HigherOrderCO/more-pattern-match-sugars
Browse files Browse the repository at this point in the history
`;;` as syntax sugar for `#Cons`; Show location on type error at term generated by `with`
  • Loading branch information
VictorTaelin authored Nov 15, 2024
2 parents 5db82a0 + aae1cc6 commit f56cd58
Show file tree
Hide file tree
Showing 2 changed files with 117 additions and 40 deletions.
50 changes: 48 additions & 2 deletions src/Kind/CompileJS.hs
Original file line number Diff line number Diff line change
Expand Up @@ -446,6 +446,9 @@ ref book nam
, "IO/print"
, "IO/prompt"
, "IO/swap"
, "IO/read"
, "IO/exec"
, "IO/args"
]

-- JavaScript Codegen
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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 = '';",
Expand All @@ -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;",
Expand Down Expand Up @@ -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
Expand Down
107 changes: 69 additions & 38 deletions src/Kind/Parse.hs
Original file line number Diff line number Diff line change
Expand Up @@ -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 ()
Expand Down Expand Up @@ -617,6 +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 ";;")
] $ parseSuffVal term

parseSuffArr :: Term -> Parser Term
Expand Down Expand Up @@ -649,6 +649,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

Expand Down Expand Up @@ -737,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
Expand All @@ -753,56 +759,83 @@ 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
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

parsePatSuffix :: Pattern -> Parser Pattern
parsePatSuffix pat = P.choice
[ parsePatSuffPar pat
, parsePatSuffCns pat
, return pat
]

parsePatternNat :: Parser Pattern
parsePatternNat = do
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
Expand All @@ -812,8 +845,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 '@'
Expand All @@ -827,20 +860,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)

Expand Down Expand Up @@ -1098,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
Expand Down

0 comments on commit f56cd58

Please sign in to comment.