From 023e9e61ad2912fb805d924a068a8f09551fe991 Mon Sep 17 00:00:00 2001 From: Steve Dunham Date: Mon, 12 Aug 2024 11:54:08 -0700 Subject: [PATCH] codegen improvements --- newt/testcase.newt | 7 ++++++ src/Lib/Check.idr | 10 ++++++-- src/Lib/Compile.idr | 56 ++++++++++++++++++++++++------------------ src/Lib/CompileExp.idr | 18 ++++++-------- src/Lib/Types.idr | 2 +- 5 files changed, 55 insertions(+), 38 deletions(-) diff --git a/newt/testcase.newt b/newt/testcase.newt index 43277b3..7a9eb89 100644 --- a/newt/testcase.newt +++ b/newt/testcase.newt @@ -46,5 +46,12 @@ not = \ v => case v of True => False False => True + +not2 : Bool -> Bool +not2 = \ v => case v of + True => False + x => True + + data Void : U where diff --git a/src/Lib/Check.idr b/src/Lib/Check.idr index cc7a383..2cd5424 100644 --- a/src/Lib/Check.idr +++ b/src/Lib/Check.idr @@ -176,6 +176,11 @@ checkAlt scty ctx ty (MkAlt ptm body) = do (con, args) <- getArgs ptm [] debug "ALT con \{con} args \{show args}" let Just (MkEntry _ dcty (DCon arity _)) = lookup con !(get) + | Nothing => do + -- check body with con bound at scty against ty + let ctx' = extend ctx con scty + body' <- check ctx' body ty + pure $ CaseDefault body' | _ => error emptyFC "expected datacon, got \{con}" -- arity is wrong, but we actually need the type anyway @@ -218,7 +223,8 @@ checkAlt scty ctx ty (MkAlt ptm body) = do let var = VVar emptyFC (length ctx.env) [<] let ctx' = extend ctx nm a Lam emptyFC nm <$> go !(b $$ var) rest ctx' - go (VPi fc str Implicit a b) args ctx = do + + go (VPi _ str Implicit a b) args ctx = do debug "*** insert \{str}" let fc' = argsFC args let var = VVar fc' (length ctx.env) [<] @@ -226,7 +232,7 @@ checkAlt scty ctx ty (MkAlt ptm body) = do Lam fc' "_" <$> go !(b $$ var) args ctx' -- same deal with _ for name go (VPi fc str Explicit a b) ((fc', Implicit, nm) :: rest) ctx = do - error fc' "Implicit/Explicit mismatch \{show str} \{show nm}" + error fc' "Implicit/Explicit mismatch \{show str} at \{show nm}" go (VPi fc str icit x y) [] ctx = error emptyFC "Not enough arguments" -- nameless variable diff --git a/src/Lib/Compile.idr b/src/Lib/Compile.idr index d5ba251..2ce929a 100644 --- a/src/Lib/Compile.idr +++ b/src/Lib/Compile.idr @@ -1,3 +1,5 @@ +-- TODO fresh names + module Lib.Compile import Lib.Types @@ -9,6 +11,10 @@ data Kind = Plain | Return | Assign String data JSStmt : Kind -> Type +data JAlt : Type where + JConAlt : String -> JSStmt e -> JAlt + JDefAlt : JSStmt e -> JAlt + data JSExp : Type where LitArray : List JSExp -> JSExp LitObject : List (String, JSExp) -> JSExp @@ -28,7 +34,8 @@ data JSStmt : Kind -> Type where JReturn : JSExp -> JSStmt Return -- JAssign : (nm : String) -> JSExp -> JSStmt (Assign nm) -- TODO - switch to Nat tags - JCase : JSExp -> List (String, JSStmt a) -> Maybe (JSStmt a) -> JSStmt a + -- FIXME add e to JAlt (or just drop it?) + JCase : JSExp -> List JAlt -> JSStmt a -- throw can't be used JError : String -> JSStmt a @@ -70,22 +77,26 @@ termToJS env (CApp t args) f = termToJS env t (\ t' => argsToJS args [<] (\ args argsToJS (x :: xs) acc k = termToJS env x (\ x' => argsToJS xs (acc :< x') k) -termToJS env (CCase t alts def) f = +termToJS env (CCase t alts) f = -- need to assign the scrutinee to a variable (unless it is a var already?) -- and add (Bnd -> JSExpr map) -- TODO default case, let's drop the extra field. termToJS env t $ \case - (Var nm) => (JCase (Dot (Var nm) "tag") (map (termToJSAlt nm) alts) Nothing) - t' => + (Var nm) => (JCase (Dot (Var nm) "tag") (map (termToJSAlt nm) alts)) + t' => let nm = "sc$\{show $ length env}" in JSnoc (JConst nm t') - (JCase (Dot (Var nm) "tag") (map (termToJSAlt nm) alts) Nothing) + (JCase (Dot (Var nm) "tag") (map (termToJSAlt nm) alts)) where - termToJSAlt : String -> CAlt -> (String, JSStmt e) - termToJSAlt nm (CConAlt name args u) = - let env' = mkEnv nm 0 env args in - (name, termToJS env' u f) + termToJSAlt : String -> CAlt -> JAlt + termToJSAlt nm (CConAlt name args u) = JConAlt name (termToJS (mkEnv nm 0 env args) u f) + -- intentially reusing scrutinee name here + termToJSAlt nm (CDefAlt u) = JDefAlt (termToJS (Var nm :: env) u f) + label : JSExp -> (String -> JSStmt e) -> JSStmt e + label (Var nm) f = f nm + label t f = ?label_rhs + -- FIXME escape jsString : String -> Doc @@ -110,25 +121,22 @@ expToDoc JUndefined = text "undefined" expToDoc (Index obj ix) = expToDoc obj ++ "[" ++ expToDoc ix ++ "]" expToDoc (Dot obj nm) = expToDoc obj ++ "." ++ text nm -altToDoc : (String, JSStmt e) -> Doc --- line is an extra newline, but nest seems borken -altToDoc (nm, (JReturn exp)) = text "case" <+> jsString nm ++ ":" nest 2 (line ++ "return" <+> expToDoc exp) -altToDoc (nm, stmt) = text "case" <+> jsString nm ++ ":" nest 2 (line ++ stmtToDoc stmt text "break;") +caseBody : JSStmt e -> Doc +caseBody stmt@(JReturn x) = nest 2 (line ++ stmtToDoc stmt) +caseBody stmt = nest 2 (line ++ stmtToDoc stmt text "break;") + +altToDoc : JAlt -> Doc +altToDoc (JConAlt nm stmt) = text "case" <+> jsString nm ++ ":" ++ caseBody stmt +altToDoc (JDefAlt stmt) = text "default" ++ ":" ++ caseBody stmt stmtToDoc (JSnoc x y) = stmtToDoc x stmtToDoc y -stmtToDoc (JPlain x) = expToDoc x -stmtToDoc (JConst nm x) = text "const" <+> text nm <+> "=" <+/> expToDoc x -stmtToDoc (JReturn x) = text "return" <+> expToDoc x -stmtToDoc (JError str) = text "throw new Error(" ++ text str ++ ")" -stmtToDoc (JCase sc alts y) = +stmtToDoc (JPlain x) = expToDoc x ++ ";" +stmtToDoc (JConst nm x) = text "const" <+> text nm <+> "=" <+/> expToDoc x ++ ";" +stmtToDoc (JReturn x) = text "return" <+> expToDoc x ++ ";" +stmtToDoc (JError str) = text "throw new Error(" ++ text str ++ ");" +stmtToDoc (JCase sc alts) = text "switch (" ++ expToDoc sc ++ ")" <+> bracket "{" (stack $ map altToDoc alts) "}" --- FIXME - if the result is JSnoc, we get extra top level code --- If we make top level 0-arity values lazy, this won't happen --- function : String -> Tm -> Doc --- function nm tm = stmtToDoc $ termToJS [] tm (JConst nm) - - mkArgs : Nat -> List String -> List String mkArgs Z acc = acc mkArgs (S k) acc = mkArgs k ("h\{show k}" :: acc) diff --git a/src/Lib/CompileExp.idr b/src/Lib/CompileExp.idr index 4605467..f5386b1 100644 --- a/src/Lib/CompileExp.idr +++ b/src/Lib/CompileExp.idr @@ -16,6 +16,8 @@ data CExp : Type public export data CAlt : Type where CConAlt : String -> List String -> CExp -> CAlt + -- REVIEW keep var name? + CDefAlt : CExp -> CAlt -- literal data CExp : Type where @@ -25,7 +27,7 @@ data CExp : Type where CApp : CExp -> List CExp -> CExp -- TODO make DCon/TCon app separate so we can specialize -- U / Pi are compiled to type constructors - CCase : CExp -> List CAlt -> Maybe CExp -> CExp + CCase : CExp -> List CAlt -> CExp CRef : Name -> CExp CMeta : Nat -> CExp @@ -100,16 +102,10 @@ compileTerm (U _) = pure $ CRef "U" compileTerm (Pi _ nm icit t u) = pure $ CApp (CRef "PiType") [ !(compileTerm t), CLam nm !(compileTerm u)] compileTerm (Case _ t alts) = do t' <- compileTerm t - alts' <- catMaybes <$> traverse (\case - CaseDefault tm => pure Nothing - CaseCons nm args tm => pure $ Just $ CConAlt nm args !(compileTerm tm)) alts - def <- getDefault alts - pure $ CCase t' alts' def - where - getDefault : List CaseAlt -> M (Maybe CExp) - getDefault [] = pure Nothing - getDefault (CaseDefault u :: _) = Just <$> compileTerm u - getDefault (_ :: xs) = getDefault xs + alts' <- traverse (\case + CaseDefault tm => pure $ CDefAlt !(compileTerm tm) + CaseCons nm args tm => pure $ CConAlt nm args !(compileTerm tm)) alts + pure $ CCase t' alts' export diff --git a/src/Lib/Types.idr b/src/Lib/Types.idr index 05655e0..d64e21a 100644 --- a/src/Lib/Types.idr +++ b/src/Lib/Types.idr @@ -152,7 +152,7 @@ Pretty Tm where pretty (App _ t u) = text "(" <+> pretty t <+> pretty u <+> ")" pretty (U _) = "U" pretty (Pi _ str icit t u) = text "(" <+> text str <+> ":" <+> pretty t <+> ")" <+> "=>" <+> pretty u <+> ")" - pretty (Case _ _ _) = text "FIXME CASE" + pretty (Case _ _ _) = text "FIXME PRETTY CASE" -- public export -- data Closure : Nat -> Type