diff --git a/src/Lib/CompileJS.newt b/src/Lib/CompileJS.newt index 48655b5..da295bd 100644 --- a/src/Lib/CompileJS.newt +++ b/src/Lib/CompileJS.newt @@ -503,7 +503,7 @@ REVIEW could I avoid most of this by using `function` instead of arrow functions sortedNames : SortedMap QName CExp → List QName → List QName sortedNames defs names = - map snd $ filter (not ∘ fst) $ foldl (go Nil) Nil $ map (True,) names + map snd $ filter (not ∘ fst) $ foldl (go Nil) Nil $ map (_,_ True) names where getBody : CAlt → CExp getBody (CConAlt _ _ _ _ _ t) = t diff --git a/src/Lib/CompileScheme.newt b/src/Lib/CompileScheme.newt index 483aa4d..4668757 100644 --- a/src/Lib/CompileScheme.newt +++ b/src/Lib/CompileScheme.newt @@ -266,7 +266,7 @@ REVIEW could I avoid most of this by using `function` instead of arrow functions -- TODO factor out to CompilerCommon sortedNames : SortedMap QName CExp → List QName → List QName sortedNames defs names = - map snd $ filter (not ∘ fst) $ foldl (go Nil) Nil $ map (True,) names + map snd $ filter (not ∘ fst) $ foldl (go Nil) Nil $ map (_,_ True) names where getBody : CAlt → CExp getBody (CConAlt _ _ _ _ _ t) = t diff --git a/src/Lib/Elab.newt b/src/Lib/Elab.newt index 7aa5260..30a7eac 100644 --- a/src/Lib/Elab.newt +++ b/src/Lib/Elab.newt @@ -80,18 +80,6 @@ lookupDef ctx name = go 0 ctx.types ctx.env go ix ((nm, ty) :: xs) (v :: vs) = if nm == name then Just v else go (1 + ix) xs vs go ix _ _ = Nothing -expandList : FC → Maybe Raw → Raw -expandList fc Nothing = RVar fc "Nil" -expandList fc (Just t) = go fc t - where - cons : FC → Raw → Raw → Raw - cons fc t u = RApp fc (RApp fc (RVar fc "_::_") t Explicit) u Explicit - - go : FC → Raw → Raw - go fc (RApp fc' (RApp fc'' (RVar fc "_,_") t Explicit) u Explicit) = - cons fc t $ go fc u - go fc t = cons fc t (RVar fc "Nil") - forceMeta : Val -> M Val forceMeta (VMeta fc ix sp) = do meta <- lookupMeta ix @@ -989,7 +977,6 @@ mkPat (RAs fc as tm, icit) = do (PatCon fc icit nm args Nothing) => pure $ PatCon fc icit nm args (Just as) (PatCon fc icit nm args _) => error fc "Double as pattern \{show tm}" t => error fc "Can't put as on non-constructor \{show tm}" -mkPat (RList fc mt, icit) = mkPat (expandList fc mt, icit) mkPat (tm, icit) = do top <- getTop case splitArgs tm Nil of @@ -1551,8 +1538,6 @@ infer ctx (RVar fc nm) = go 0 ctx.types go i ((x, ty) :: xs) = if x == nm then pure (Bnd fc i, ty) else go (i + 1) xs -infer ctx (RList fc mt) = infer ctx $ expandList fc mt - infer ctx (RApp fc t u icit) = do -- If the app is explicit, add any necessary metas (icit, t, tty) <- case icit of diff --git a/src/Lib/Parser.newt b/src/Lib/Parser.newt index 9f27e40..854ff2a 100644 --- a/src/Lib/Parser.newt +++ b/src/Lib/Parser.newt @@ -41,10 +41,6 @@ dbraces pa = do symbol "}}" pure t - -optional : ∀ a. Parser a -> Parser (Maybe a) -optional pa = Just <$> pa <|> pure Nothing - stringLit : Parser Raw stringLit = do fc <- getPos @@ -98,25 +94,42 @@ lit = intLit <|> interpString <|> stringLit <|> charLit addPos : ∀ a. Parser a -> Parser (FC × a) addPos pa = _,_ <$> getPos <*> pa -asAtom : Parser Raw -asAtom = do - fc <- getPos - nm <- ident - asPat <- optional $ keyword "@" *> parenWrap typeExpr - case asPat of - Just exp => pure $ RAs fc nm exp - Nothing => pure $ RVar fc nm recordUpdate : Parser Raw +parseOp : Parser Raw listTypeExp : Parser Raw listTypeExp = do fc <- getPos symbol "[" - tm <- optional typeExpr + -- many of these though + tms <- sepBy' (symbol ",") parseOp + nilFC <- getPos symbol "]" - pure $ RList fc tm + pure $ expandList nilFC tms + where + cons : FC → Raw → Raw → Raw + cons fc t u = RApp fc (RApp fc (RVar fc "_::_") t Explicit) u Explicit + + expandList : FC → List Raw → Raw + expandList fc Nil = RVar fc "Nil" + expandList fc (x :: xs) = cons (getFC x) x $ expandList fc xs + + + +parenTypeExp' : Parser Raw +parenTypeExp' = do + pure MkUnit + t <- typeExpr + ts <- many $ keyword "," >> typeExpr + pure $ comma t ts + where + comma : Raw → List Raw → Raw + comma acc Nil = acc + comma acc (t :: ts) = + let fc = getFC t in + (RApp fc (RApp fc (RVar fc "_,_") acc Explicit) (comma t ts) Explicit) parenTypeExp : Parser Raw parenTypeExp = do @@ -126,9 +139,16 @@ parenTypeExp = do fc' <- getPos Nothing <- optional $ symbol ")" | Just tm => do pure $ RImpossible (fc + fc') - t <- typeExpr - symbol ")" - pure t + parenTypeExp' <* symbol ")" + +asAtom : Parser Raw +asAtom = do + fc <- getPos + nm <- ident + asPat <- optional $ keyword "@" *> parenTypeExp + case asPat of + Just exp => pure $ RAs fc nm exp + Nothing => pure $ RVar fc nm atom : Parser Raw atom = do @@ -168,9 +188,9 @@ recordUpdate = do pArg : Parser (Icit × FC × Raw) pArg = do fc <- getPos - (\x => Implicit, fc, x) <$> braces typeExpr - <|> (\x => Auto, fc, x) <$> dbraces typeExpr - <|> (\x => Explicit, fc, x) <$> atom + (\x => (Implicit, fc, x)) <$> braces typeExpr + <|> (\x => (Auto, fc, x)) <$> dbraces typeExpr + <|> (\x => (Explicit, fc, x)) <$> atom AppSpine : U AppSpine = List (Icit × FC × Raw) @@ -263,14 +283,14 @@ pratt ops prec stop left spine = do -parseOp : Parser Raw + parseOp = do fc <- getPos ops <- getOps hd <- atom rest <- many pArg (res, Nil) <- pratt ops 0 "" hd rest - | _ => fail "extra stuff" + | (res, xs) => fail "extra stuff \{show xs}" pure res letExpr : Parser Raw @@ -300,10 +320,10 @@ pLamArg = impArg <|> expArg where -- TODO - we're moving away from uppercase variables, but a test uses them impArg : Parser (Icit × String × Maybe Raw) - impArg = (Implicit, ) <$> braces (_,_ <$> (ident <|> uident) <*> optional (symbol ":" >> typeExpr)) + impArg = (_,_ Implicit ) <$> braces (_,_ <$> (ident <|> uident) <*> optional (symbol ":" >> typeExpr)) expArg : Parser (Icit × String × Maybe Raw) - expArg = (Explicit , ) <$> parenWrap (_,_ <$> ident <*> optional (symbol ":" >> typeExpr)) + expArg = (_,_ Explicit) <$> parenWrap (_,_ <$> ident <*> optional (symbol ":" >> typeExpr)) lamExpr : Parser Raw lamExpr = do @@ -353,7 +373,7 @@ caseLet = do -- look ahead so we can fall back to normal let fc <- getPos try (keyword "let" >> symbol "(") - pat <- typeExpr + pat <- parenTypeExp' symbol ")" keyword "=" sc <- typeExpr @@ -368,7 +388,7 @@ doCaseLet = do -- Maybe make it work like arrow? fc <- getPos try (keyword "let" >> symbol "(") - pat <- typeExpr + pat <- parenTypeExp' symbol ")" keyword "=" sc <- typeExpr diff --git a/src/Lib/Parser/Impl.newt b/src/Lib/Parser/Impl.newt index 9ac69b5..28ac1df 100644 --- a/src/Lib/Parser/Impl.newt +++ b/src/Lib/Parser/Impl.newt @@ -131,11 +131,20 @@ some p = do pure (x :: xs) many p = some p <|> pure Nil +optional : ∀ a. Parser a -> Parser (Maybe a) +optional pa = Just <$> pa <|> pure Nothing + -- one or more `a` seperated by `s` sepBy : ∀ s a. Parser s -> Parser a -> Parser (List a) sepBy s a = _::_ <$> a <*> many (s *> a) +-- zero or more `a` seperated by `s` +sepBy' : ∀ s a. Parser s -> Parser a -> Parser (List a) +sepBy' s a = do + Just x <- optional a | _ => pure Nil + xs <- many (s *> a) + pure $ x :: xs getPos : Parser FC getPos = P $ \last toks com ops indent => case toks of diff --git a/src/Lib/ProcessModule.newt b/src/Lib/ProcessModule.newt index 650b909..a25392f 100644 --- a/src/Lib/ProcessModule.newt +++ b/src/Lib/ProcessModule.newt @@ -181,7 +181,7 @@ invalidateModule modname = do in updateMap k (v :: prev) deps getDeps : String × ModContext → List (String × String) - getDeps (nm, mod) = map (nm , ) mod.modDeps + getDeps (nm, mod) = map (_,_ nm) mod.modDeps go : SortedMap String (List String) → List String → SortedMap String ModContext → SortedMap String ModContext go deps Nil mods = mods diff --git a/src/Lib/Syntax.newt b/src/Lib/Syntax.newt index fe280de..3760604 100644 --- a/src/Lib/Syntax.newt +++ b/src/Lib/Syntax.newt @@ -60,7 +60,6 @@ data Raw : U where -- has to be applied or we have to know its type as Foo → Foo to elaborate. -- I can bake the arg in here, or require an app in elab. RUpdateRec : (fc : FC) → List UpdateClause → Maybe Raw → Raw - RList : (fc : FC) → Maybe Raw → Raw instance HasFC Raw where getFC (RVar fc nm) = fc @@ -79,7 +78,6 @@ instance HasFC Raw where getFC (RAs fc _ _) = fc getFC (RUpdateRec fc _ _) = fc getFC (RImpossible fc) = fc - getFC (RList fc _) = fc data Import = MkImport FC (FC × Name) @@ -191,8 +189,6 @@ instance Pretty Raw where asDoc p (RWhere _ dd b) = text "TODO pretty RWhere" asDoc p (RAs _ nm x) = text nm ++ text "@(" ++ asDoc 0 x ++ text ")" asDoc p (RUpdateRec _ clauses tm) = text "{" <+> text "TODO RUpdateRec" <+> text "}" - asDoc p (RList _ (Just t)) = text "[" <+> asDoc p t <+> text "]" - asDoc p (RList _ Nothing) = text "[]" prettyBind : (BindInfo × Raw) -> Doc prettyBind (BI _ nm icit quant, ty) = wrap icit (text (show quant ++ nm) <+> text ":" <+> pretty ty) @@ -250,8 +246,7 @@ substRaw ss t = case t of (RWhere fc ds body) => RWhere fc (map substDecl ds) (substRaw ss body) (RDo fc stmts) => RDo fc (substStmts ss stmts) (RCase fc scrut mdef alts) => RCase fc (substRaw ss scrut) (map (substRaw ss) mdef) (map substAlt alts) - (RList fc (Just t)) => RList fc (Just $ substRaw ss t) - (RList fc Nothing) => RList fc Nothing + -- Enumerate to force consideration of new cases t@(RImpossible _) => t t@(RU _) => t diff --git a/src/Lib/Tokenizer.newt b/src/Lib/Tokenizer.newt index e490e33..fa36748 100644 --- a/src/Lib/Tokenizer.newt +++ b/src/Lib/Tokenizer.newt @@ -25,7 +25,7 @@ keywords = ("let" :: "in" :: "where" :: "case" :: "of" :: "data" :: "U" :: "do" "if" :: "then" :: "else" :: -- it would be nice to find a way to unkeyword "." so it could be -- used as an operator too - "$" :: "λ" :: "?" :: "@" :: "." :: + "$" :: "λ" :: "?" :: "@" :: "." :: "," :: "->" :: "→" :: ":" :: "=>" :: ":=" :: "$=" :: "=" :: "<-" :: "\\" :: "_" :: "|" :: Nil) @@ -101,7 +101,6 @@ rawTokenise ts@(TS sl sc toks chars) = case chars of rawTokenise (TS sl (sc + 1) (toks :< tok) cs) cs => Left $ E (MkFC "" (MkBounds sl sc sl (sc + 1))) "Expected '}'" - ',' :: cs => rawTokenise (TS sl (sc + 1) (toks :< mktok False sl (sc + 1) Ident ",") cs) '_' :: ',' :: '_' :: cs => rawTokenise (TS sl (sc + 3) (toks :< mktok False sl (sc + 3) MixFix "_,_") cs) '_' :: '.' :: '_' :: cs => rawTokenise (TS sl (sc + 3) (toks :< mktok False sl (sc + 3) MixFix "_._") cs) '\'' :: '\\' :: c :: '\'' :: cs => diff --git a/src/Prelude.newt b/src/Prelude.newt index c419793..7ca0520 100644 --- a/src/Prelude.newt +++ b/src/Prelude.newt @@ -88,7 +88,7 @@ xs <>< (y :: ys) = (xs :< y) <>< ys -- f $ a = f a infixr 8 _×_ -infixr 2 _,_ +infixr 2 _,_ -- deprecated decl, it is special now data a × b = (a,b) fst : ∀ a b. a × b → a diff --git a/tests/ListSugar.newt b/tests/ListSugar.newt index 323fb7d..6f7c226 100644 --- a/tests/ListSugar.newt +++ b/tests/ListSugar.newt @@ -6,6 +6,9 @@ import Prelude blah : List Int blah = [ 1, 2, 3] +pairs : List (Int × Int) +pairs = [ (1,2), (3,4)] + bar : List Int → Int bar [ ] = 0 bar [x] = 1