From 041521ab47538606b95a86273494774dad25f288 Mon Sep 17 00:00:00 2001 From: Steve Dunham Date: Sun, 16 Feb 2025 21:46:19 -0800 Subject: [PATCH] fix regressed error message for missing cases --- src/Lib/Compile.newt | 1 - src/Lib/CompileExp.newt | 3 --- src/Lib/Elab.newt | 10 +++++----- src/Lib/LiftWhere.newt | 2 +- src/Node.newt | 1 + 5 files changed, 7 insertions(+), 10 deletions(-) diff --git a/src/Lib/Compile.newt b/src/Lib/Compile.newt index 90f533b..38f36fa 100644 --- a/src/Lib/Compile.newt +++ b/src/Lib/Compile.newt @@ -286,7 +286,6 @@ maybeWrap stmt = Apply (JLam Nil stmt) Nil defToDoc : {{Ref2 Defs St}} → QName → Def → M Doc defToDoc name (Fn tm) = do debug $ \ _ => "compileFun \{render 90 $ pprint Nil tm}" - -- tm' <- erase Nil tm Nil ct <- compileFun tm let exp = maybeWrap $ termToJS emptyJSEnv ct JReturn pure $ text "const" <+> jsIdent (show name) <+> text "=" <+/> expToDoc exp ++ text ";" diff --git a/src/Lib/CompileExp.newt b/src/Lib/CompileExp.newt index 473719d..a0832f3 100644 --- a/src/Lib/CompileExp.newt +++ b/src/Lib/CompileExp.newt @@ -98,9 +98,6 @@ compileTerm tm@(App _ _ _) = case funArgs tm of (t@(Ref fc nm), args) => do args' <- traverse compileTerm args arity <- arityForName fc nm - top <- getTop - -- let (Just (MkEntry _ _ type _)) = lookup nm top - -- | Nothing => error fc "Undefined name \{show nm}" apply (CRef (show nm)) args' Lin arity (t, args) => do debug $ \ _ => "apply other \{render 90 $ pprint Nil t}" diff --git a/src/Lib/Elab.newt b/src/Lib/Elab.newt index ea27ad6..29c207f 100644 --- a/src/Lib/Elab.newt +++ b/src/Lib/Elab.newt @@ -1127,10 +1127,10 @@ buildLitCase ctx prob fc scnm scty lit = do cons <- rewriteConstraint cons Nil pure $ MkClause fc cons pats expr -buildDefault : Context → Problem → FC → String → M CaseAlt -buildDefault ctx prob fc scnm = do +buildDefault : Context → Problem → FC → String → List QName → M CaseAlt +buildDefault ctx prob fc scnm missing = do let defclauses = filter isDefault prob.clauses - when (length' defclauses == 0) $ \ _ => error fc "no default for literal slot on \{show scnm}" + when (length' defclauses == 0) $ \ _ => error fc "missing cases \{show missing} on \{show scnm}" CaseDefault <$> buildTree ctx (MkProb defclauses prob.ty) where isDefault : Clause -> Bool @@ -1253,9 +1253,9 @@ buildTree ctx prob@(MkProb ((MkClause fc constraints Nil expr) :: cs) ty) = do -- build a default case for missed constructors case miss' of Nil => pure $ Case fc sctm (mapMaybe id alts) - _ => do + missed => do -- ctx prob fc scnm - default <- buildDefault ctx prob fc scnm + default <- buildDefault ctx prob fc scnm (map fst missed) pure $ Case fc sctm (snoc alts' default) PatLit fc v => do diff --git a/src/Lib/LiftWhere.newt b/src/Lib/LiftWhere.newt index 3a6adcc..4783213 100644 --- a/src/Lib/LiftWhere.newt +++ b/src/Lib/LiftWhere.newt @@ -87,7 +87,7 @@ liftWhereFn (name, Fn tm) = do -- updateDef name fc type (Fn tm') liftWhereFn _ = pure MkUnit -liftWhere : {{Ref2 Defs St}} → M Unit +liftWhere : {{Ref2 Defs St}} → M Unit liftWhere = do defs <- getRef Defs ignore $ traverse liftWhereFn $ toList defs diff --git a/src/Node.newt b/src/Node.newt index 1419351..b24e6d6 100644 --- a/src/Node.newt +++ b/src/Node.newt @@ -2,6 +2,7 @@ module Node import Prelude +-- REVIEW - should this be IO (List String) pfunc getArgs uses (arrayToList) : List String := `Prelude_arrayToList(null, process.argv.slice(1))` pfunc readFile uses (MkIORes Left Right) : (fn : String) -> IO (Either String String) := `(fn) => (w) => { let fs = require('fs')