From afac2cdb1384ba97c5fab2cd6df2c0b26cb7dce0 Mon Sep 17 00:00:00 2001 From: David Holland Date: Fri, 28 Jun 2024 12:07:57 -0400 Subject: [PATCH 1/9] Some tidying in SAWScript.AST --- src/SAWScript/AST.hs | 23 +++++++++++++++++++---- 1 file changed, 19 insertions(+), 4 deletions(-) diff --git a/src/SAWScript/AST.hs b/src/SAWScript/AST.hs index fee4aca481..344fa770b6 100644 --- a/src/SAWScript/AST.hs +++ b/src/SAWScript/AST.hs @@ -60,26 +60,41 @@ type Name = String -- }}} --- Expr Level {{{ +-- Location tracking {{{ + +-- +-- Type to wrap a thing with a position +-- +-- This is declared with record syntax to provide accessors/projection +-- functions; it is intended to be used positionally. +-- +data Located a = Located { + getVal :: a, -- the thing + getOrig :: Name, -- a name/string for it, where applicable + locatedPos :: Pos -- the position +} deriving (Functor, Foldable, Traversable) -data Located a = Located { getVal :: a, getOrig :: Name, locatedPos :: Pos } deriving (Functor, Foldable, Traversable) instance Show (Located a) where show (Located _ v p) = show v ++ " (" ++ show p ++ ")" instance Positioned (Located a) where getPos = locatedPos -type LName = Located Name - instance Eq a => Eq (Located a) where a == b = getVal a == getVal b instance Ord a => Ord (Located a) where compare a b = compare (getVal a) (getVal b) +type LName = Located Name + toLName :: Token Pos -> LName toLName p = Located (tokStr p) (tokStr p) (tokPos p) +-- }}} + +-- Expr Level {{{ + data Import = Import { iModule :: Either FilePath P.ModName , iAs :: Maybe P.ModName From 463f59ea67145aca71323a2bf3df99e9ce23de18 Mon Sep 17 00:00:00 2001 From: David Holland Date: Mon, 15 Jul 2024 21:15:18 -0400 Subject: [PATCH 2/9] Improve position tracking for expressions and patterns. Add positions to all expression and pattern nodes. Kill off the LExpr and LPattern expression and pattern cases that held just a position. The idea had been to always use the first enclosing such position. This doesn't provide accurate enough positions for type errors (in general for a type error you always want the exact expression you're complaining about, especially if you're printing spans of positions and not just line numbers), and, worse, with this approach it's hard to tell if any given position is the one you actually ought to be using. Fix up some of the position usage where prompted by the ensuing typing changes. Kill off the currentExprPos field of the local state monad in MGU.hs, which was for collecting the enclosing LExpr and is no longer needed. In pursuit of all this, add two ops to Position.hs: - leadingPos, which gets the empty (no span) position at the beginning of the position of something else, which can be used for deriving the position of implicit elements; - maxSpan', which is like maxSpan but works for (exactly) two Positioned objects of potentially heterogeneous type. This allows dropping a number of explicit calls to getPos in places where that's verbose and ugly. --- CHANGES.md | 5 + saw/SAWScript/REPL/Command.hs | 3 +- src/SAWScript/AST.hs | 111 ++++++------ src/SAWScript/AutoMatch.hs | 80 ++++----- src/SAWScript/Interpreter.hs | 142 ++++++++-------- src/SAWScript/MGU.hs | 306 ++++++++++++++++++---------------- src/SAWScript/Parser.y | 67 ++++---- src/SAWScript/Position.hs | 13 ++ 8 files changed, 400 insertions(+), 327 deletions(-) diff --git a/CHANGES.md b/CHANGES.md index 92a59c9728..fb94502805 100644 --- a/CHANGES.md +++ b/CHANGES.md @@ -6,6 +6,11 @@ allow taking `&str` slices. For more information, see the documentation in the [SAW manual](https://github.com/GaloisInc/saw-script/blob/master/doc/manual/manual.md#string-slices). +## Bug fixes + +* The locations printed with type errors (in particular) and other diagnostics + now have a much stronger connection with reality. + # Version 1.1 -- 2024-02-05 ## New Features diff --git a/saw/SAWScript/REPL/Command.hs b/saw/SAWScript/REPL/Command.hs index f7927bbffa..547756fdc3 100644 --- a/saw/SAWScript/REPL/Command.hs +++ b/saw/SAWScript/REPL/Command.hs @@ -161,7 +161,8 @@ typeOfCmd str expr <- case SAWScript.Parser.parseExpression tokens of Left err -> fail (show err) Right expr -> return expr - let decl = SS.Decl (getPos expr) (SS.PWild Nothing) Nothing expr + let pos = getPos expr + decl = SS.Decl pos (SS.PWild pos Nothing) Nothing expr rw <- getValueEnvironment ~(SS.Decl _pos _ (Just schema) _expr') <- either failTypecheck return $ checkDecl (rwTypes rw) (rwTypedef rw) decl diff --git a/src/SAWScript/AST.hs b/src/SAWScript/AST.hs index 344fa770b6..defc47bfd6 100644 --- a/src/SAWScript/AST.hs +++ b/src/SAWScript/AST.hs @@ -107,49 +107,60 @@ instance Positioned Import where data Expr -- Constants - = Bool Bool - | String String - | Int Integer + = Bool Pos Bool + | String Pos String + | Int Pos Integer | Code (Located String) | CType (Located String) -- Structures - | Array [Expr] - | Block [Stmt] - | Tuple [Expr] - | Record (Map Name Expr) + | Array Pos [Expr] + | Block Pos [Stmt] + | Tuple Pos [Expr] + | Record Pos (Map Name Expr) -- Accessors - | Index Expr Expr - | Lookup Expr Name - | TLookup Expr Integer + | Index Pos Expr Expr + | Lookup Pos Expr Name + | TLookup Pos Expr Integer -- LC | Var (Located Name) - | Function Pattern Expr - | Application Expr Expr + | Function Pos Pattern Expr + | Application Pos Expr Expr -- Sugar - | Let DeclGroup Expr - | TSig Expr Type - | IfThenElse Expr Expr Expr - -- Source locations - | LExpr Pos Expr - deriving (Eq, Show) + | Let Pos DeclGroup Expr + | TSig Pos Expr Type + | IfThenElse Pos Expr Expr Expr + deriving (Eq, Show) -- XXX eq? instance Positioned Expr where + getPos (Bool pos _) = pos + getPos (String pos _) = pos + getPos (Int pos _) = pos getPos (Code c) = getPos c getPos (CType t) = getPos t - getPos (LExpr site _) = site + getPos (Array pos _) = pos + getPos (Block pos _) = pos + getPos (Tuple pos _) = pos + getPos (Record pos _) = pos + getPos (Index pos _ _) = pos + getPos (Lookup pos _ _) = pos + getPos (TLookup pos _ _) = pos getPos (Var n) = getPos n - getPos _ = Unknown + getPos (Function pos _ _) = pos + getPos (Application pos _ _) = pos + getPos (Let pos _ _) = pos + getPos (TSig pos _ _) = pos + getPos (IfThenElse pos _ _ _) = pos data Pattern - = PWild (Maybe Type) - | PVar LName (Maybe Type) - | PTuple [Pattern] - | LPattern Pos Pattern - deriving (Eq, Show) + = PWild Pos (Maybe Type) + | PVar Pos LName (Maybe Type) + | PTuple Pos [Pattern] + deriving (Eq, Show) -- XXX Eq? instance Positioned Pattern where - getPos (LPattern pos _) = pos - getPos _ = Unknown + getPos (PWild pos _) = pos + getPos (PVar pos _ _) = pos + getPos (PTuple pos _) = pos data Stmt = StmtBind Pos Pattern (Maybe Type) Expr @@ -244,36 +255,36 @@ vcatWithSemi = PP.vcat . map (PP.<> PP.semi) instance Pretty Expr where pretty expr0 = case expr0 of - Bool b -> PP.viaShow b - String s -> PP.dquotes (PP.pretty s) - Int i -> PP.pretty i - Code ls -> PP.braces . PP.braces $ PP.pretty (getVal ls) + Bool _ b -> PP.viaShow b + String _ s -> PP.dquotes (PP.pretty s) + Int _ i -> PP.pretty i + Code ls -> PP.braces . PP.braces $ PP.pretty (getVal ls) CType (Located string _ _) -> PP.braces . PP.pretty $ "|" ++ string ++ "|" - Array xs -> PP.list (map PP.pretty xs) - Block stmts -> + Array _ xs -> PP.list (map PP.pretty xs) + Block _ stmts -> "do" PP.<+> PP.lbrace PP.<> PP.line' PP.<> (PP.indent 3 $ (PP.align . vcatWithSemi . map PP.pretty $ stmts)) PP.<> PP.line' PP.<> PP.rbrace - Tuple exprs -> PP.tupled (map PP.pretty exprs) - Record mapping -> + Tuple _ exprs -> PP.tupled (map PP.pretty exprs) + Record _ mapping -> PP.braces . (PP.space PP.<>) . (PP.<> PP.space) . PP.align . PP.sep . PP.punctuate PP.comma $ map (\(name, value) -> PP.pretty name PP.<+> "=" PP.<+> PP.pretty value) (Map.assocs mapping) - Index _ _ -> error "No concrete syntax for AST node 'Index'" - Lookup expr name -> PP.pretty expr PP.<> PP.dot PP.<> PP.pretty name - TLookup expr int -> PP.pretty expr PP.<> PP.dot PP.<> PP.pretty int + Index _ _ _ -> error "No concrete syntax for AST node 'Index'" + Lookup _ expr name -> PP.pretty expr PP.<> PP.dot PP.<> PP.pretty name + TLookup _ expr int -> PP.pretty expr PP.<> PP.dot PP.<> PP.pretty int Var (Located name _ _) -> PP.pretty name - Function pat expr -> + Function _ pat expr -> "\\" PP.<+> PP.pretty pat PP.<+> "->" PP.<+> PP.pretty expr -- FIXME, use precedence to minimize parentheses - Application f a -> PP.parens (PP.pretty f PP.<+> PP.pretty a) - Let (NonRecursive decl) expr -> + Application _ f a -> PP.parens (PP.pretty f PP.<+> PP.pretty a) + Let _ (NonRecursive decl) expr -> PP.fillSep [ "let" PP.<+> prettyDef decl , "in" PP.<+> PP.pretty expr ] - Let (Recursive decls) expr -> + Let _ (Recursive decls) expr -> PP.fillSep [ "let" PP.<+> PP.cat (PP.punctuate @@ -281,29 +292,27 @@ instance Pretty Expr where (map prettyDef decls)) , "in" PP.<+> PP.pretty expr ] - TSig expr typ -> PP.parens $ PP.pretty expr PP.<+> PP.colon PP.<+> pretty 0 typ - IfThenElse e1 e2 e3 -> + TSig _ expr typ -> PP.parens $ PP.pretty expr PP.<+> PP.colon PP.<+> pretty 0 typ + IfThenElse _ e1 e2 e3 -> "if" PP.<+> PP.pretty e1 PP.<+> "then" PP.<+> PP.pretty e2 PP.<+> "else" PP.<+> PP.pretty e3 - LExpr _ e -> PP.pretty e instance PrettyPrint Expr where pretty _ e = PP.pretty e instance Pretty Pattern where pretty pat = case pat of - PWild mType -> + PWild _ mType -> prettyMaybeTypedArg ("_", mType) - PVar (Located name _ _) mType -> + PVar _ (Located name _ _) mType -> prettyMaybeTypedArg (name, mType) - PTuple pats -> + PTuple _ pats -> PP.tupled (map PP.pretty pats) - LPattern _ pat' -> PP.pretty pat' instance Pretty Stmt where pretty = \case - StmtBind _ (PWild _leftType) _rightType expr -> + StmtBind _ (PWild _ _leftType) _rightType expr -> PP.pretty expr StmtBind _ pat _rightType expr -> PP.pretty pat PP.<+> "<-" PP.<+> PP.align (PP.pretty expr) @@ -360,7 +369,7 @@ prettyMaybeTypedArg (name,Just typ) = dissectLambda :: Expr -> ([Pattern], Expr) dissectLambda = \case - Function pat (dissectLambda -> (pats, expr)) -> (pat : pats, expr) + Function _ pat (dissectLambda -> (pats, expr)) -> (pat : pats, expr) expr -> ([], expr) pShow :: PrettyPrint a => a -> String diff --git a/src/SAWScript/AutoMatch.hs b/src/SAWScript/AutoMatch.hs index 23b86b825e..2e43e6b597 100644 --- a/src/SAWScript/AutoMatch.hs +++ b/src/SAWScript/AutoMatch.hs @@ -358,6 +358,10 @@ processResults (TaggedSourceFile leftLang leftFile) (TaggedSourceFile rightLang confirm "Execute generated script?") where + -- FUTURE: pass in the location that triggered this operation so + -- that if we run scripts of repl commands we can record where + -- it all came from. + triggerPos = PosInternal "generated by auto_match" nameLeft, nameRight, nameCenter :: String -> String -> String nameLeft str = (("left_" ++ str ++ "_") ++) @@ -370,20 +374,20 @@ processResults (TaggedSourceFile leftLang leftFile) (TaggedSourceFile rightLang returning boundName . tell $ case lang of Cryptol -> - [SAWScript.StmtBind Unknown (SAWScript.PVar boundName Nothing) Nothing - (SAWScript.Application - (SAWScript.Var . locate $ "cryptol_load") - (SAWScript.String file))] + [SAWScript.StmtBind triggerPos (SAWScript.PVar triggerPos boundName Nothing) Nothing + (SAWScript.Application triggerPos + (SAWScript.Var $ locate "cryptol_load") + (SAWScript.String triggerPos file))] LLVM -> - [SAWScript.StmtBind Unknown (SAWScript.PVar boundName Nothing) Nothing - (SAWScript.Application - (SAWScript.Var . locate $ "llvm_load_module") - (SAWScript.String file))] + [SAWScript.StmtBind triggerPos (SAWScript.PVar triggerPos boundName Nothing) Nothing + (SAWScript.Application triggerPos + (SAWScript.Var $ locate "llvm_load_module") + (SAWScript.String triggerPos file))] JVM -> - [SAWScript.StmtBind Unknown (SAWScript.PVar boundName Nothing) Nothing - (SAWScript.Application - (SAWScript.Var . locate $ "java_load_class") - (SAWScript.String $ dropExtension file))] + [SAWScript.StmtBind triggerPos (SAWScript.PVar triggerPos boundName Nothing) Nothing + (SAWScript.Application triggerPos + (SAWScript.Var $ locate "java_load_class") + (SAWScript.String triggerPos $ dropExtension file))] extractFunction :: (String -> String) -> SourceLanguage -> String -> SAWScript.LName -> ScriptWriter s tp (SAWScript.LName) extractFunction prefix lang function loadedModule = do @@ -391,26 +395,26 @@ processResults (TaggedSourceFile leftLang leftFile) (TaggedSourceFile rightLang returning boundName . tell $ case lang of Cryptol -> - [SAWScript.StmtBind Unknown (SAWScript.PVar boundName Nothing) Nothing - (SAWScript.Application - (SAWScript.Application - (SAWScript.Var . locate $ "cryptol_extract") + [SAWScript.StmtBind triggerPos (SAWScript.PVar triggerPos boundName Nothing) Nothing + (SAWScript.Application triggerPos + (SAWScript.Application triggerPos + (SAWScript.Var $ locate "cryptol_extract") (SAWScript.Var loadedModule)) - (SAWScript.String function))] + (SAWScript.String triggerPos function))] LLVM -> - [SAWScript.StmtBind Unknown (SAWScript.PVar boundName Nothing) Nothing - (SAWScript.Application - (SAWScript.Application - (SAWScript.Var . locate $ "llvm_extract") + [SAWScript.StmtBind triggerPos (SAWScript.PVar triggerPos boundName Nothing) Nothing + (SAWScript.Application triggerPos + (SAWScript.Application triggerPos + (SAWScript.Var $ locate "llvm_extract") (SAWScript.Var loadedModule)) - (SAWScript.String function))] + (SAWScript.String triggerPos function))] JVM -> - [SAWScript.StmtBind Unknown (SAWScript.PVar boundName Nothing) Nothing - (SAWScript.Application - (SAWScript.Application - (SAWScript.Var . locate $ "jvm_extract") + [SAWScript.StmtBind triggerPos (SAWScript.PVar triggerPos boundName Nothing) Nothing + (SAWScript.Application triggerPos + (SAWScript.Application triggerPos + (SAWScript.Var $ locate "jvm_extract") (SAWScript.Var loadedModule)) - (SAWScript.String function))] + (SAWScript.String triggerPos function))] equivalenceTheorem :: (String -> String) -> SAWScript.LName -> SAWScript.LName -> Assignments -> ScriptWriter s tp (SAWScript.LName) equivalenceTheorem prefix leftFunction rightFunction assigns = do @@ -422,7 +426,7 @@ processResults (TaggedSourceFile leftLang leftFile) (TaggedSourceFile rightLang name <- newNameWith (nameCenter (leftName ++ "_" ++ rightName)) return ((leftIndex, name), (rightIndex, name)) returning theoremName . tell $ - [SAWScript.StmtBind Unknown (SAWScript.PVar theoremName Nothing) Nothing . + [SAWScript.StmtBind triggerPos (SAWScript.PVar triggerPos theoremName Nothing) Nothing . SAWScript.Code . locate . show . Cryptol.ppPrec 0 . cryptolAbstractNamesSAW leftArgs . @@ -449,23 +453,23 @@ processResults (TaggedSourceFile leftLang leftFile) (TaggedSourceFile rightLang prove :: SAWScript.LName -> ScriptWriter s tp () prove theorem = tell $ - [SAWScript.StmtBind Unknown (SAWScript.PWild Nothing) Nothing - (SAWScript.Application - (SAWScript.Application - (SAWScript.Var . locate $ "prove_print") - (SAWScript.Var (locate "abc"))) + [SAWScript.StmtBind triggerPos (SAWScript.PWild triggerPos Nothing) Nothing + (SAWScript.Application triggerPos + (SAWScript.Application triggerPos + (SAWScript.Var $ locate "prove_print") + (SAWScript.Var $ locate "abc")) (SAWScript.Var theorem))] printString :: String -> ScriptWriter s tp () printString string = tell $ - [SAWScript.StmtBind Unknown (SAWScript.PWild Nothing) Nothing - (SAWScript.Application - (SAWScript.Var . locate $ "print") - (SAWScript.String string))] + [SAWScript.StmtBind triggerPos (SAWScript.PWild triggerPos Nothing) Nothing + (SAWScript.Application triggerPos + (SAWScript.Var $ locate "print") + (SAWScript.String triggerPos string))] locate :: String -> SAWScript.LName locate name = - SAWScript.Located name "" (PosInternal "generated by auto_match") + SAWScript.Located name "" triggerPos cryptolLocate :: String -> Cryptol.LPName cryptolLocate name = diff --git a/src/SAWScript/Interpreter.hs b/src/SAWScript/Interpreter.hs index f3518b221b..8b67168b6e 100644 --- a/src/SAWScript/Interpreter.hs +++ b/src/SAWScript/Interpreter.hs @@ -124,9 +124,9 @@ import qualified Lang.Crucible.FunctionHandle as Crucible bindPatternLocal :: SS.Pattern -> Maybe SS.Schema -> Value -> LocalEnv -> LocalEnv bindPatternLocal pat ms v env = case pat of - SS.PWild _ -> env - SS.PVar x mt -> extendLocal x (ms <|> (SS.tMono <$> mt)) Nothing v env - SS.PTuple ps -> + SS.PWild _pos _ -> env + SS.PVar _pos x mt -> extendLocal x (ms <|> (SS.tMono <$> mt)) Nothing v env + SS.PTuple _pos ps -> case v of VTuple vs -> foldr ($) env (zipWith3 bindPatternLocal ps mss vs) where mss = case ms of @@ -135,16 +135,15 @@ bindPatternLocal pat ms v env = -> [ Just (SS.Forall ks t) | t <- ts ] Just t -> error ("bindPatternLocal: expected tuple type " ++ show t) _ -> error "bindPatternLocal: expected tuple value" - SS.LPattern _ pat' -> bindPatternLocal pat' ms v env bindPatternEnv :: SS.Pattern -> Maybe SS.Schema -> Value -> TopLevelRW -> TopLevel TopLevelRW bindPatternEnv pat ms v env = case pat of - SS.PWild _ -> pure env - SS.PVar x mt -> + SS.PWild _pos _ -> pure env + SS.PVar _pos x mt -> do sc <- getSharedContext liftIO $ extendEnv sc x (ms <|> (SS.tMono <$> mt)) Nothing v env - SS.PTuple ps -> + SS.PTuple _pos ps -> case v of VTuple vs -> foldr (=<<) (pure env) (zipWith3 bindPatternEnv ps mss vs) where mss = case ms of @@ -153,7 +152,6 @@ bindPatternEnv pat ms v env = -> [ Just (SS.Forall ks t) | t <- ts ] Just t -> error ("bindPatternEnv: expected tuple type " ++ show t) _ -> error "bindPatternEnv: expected tuple value" - SS.LPattern _ pat' -> bindPatternEnv pat' ms v env -- Interpretation of SAWScript ------------------------------------------------- @@ -161,51 +159,50 @@ interpret :: SS.Expr -> TopLevel Value interpret expr = let ?fileReader = BS.readFile in case expr of - SS.Bool b -> return $ VBool b - SS.String s -> return $ VString (Text.pack s) - SS.Int z -> return $ VInteger z - SS.Code str -> do sc <- getSharedContext - cenv <- fmap rwCryptol getMergedEnv - --io $ putStrLn $ "Parsing code: " ++ show str - --showCryptolEnv' cenv - t <- io $ CEnv.parseTypedTerm sc cenv - $ locToInput str - return (toValue t) - SS.CType str -> do cenv <- fmap rwCryptol getMergedEnv - s <- io $ CEnv.parseSchema cenv - $ locToInput str - return (toValue s) - SS.Array es -> VArray <$> traverse interpret es - SS.Block stmts -> interpretStmts stmts - SS.Tuple es -> VTuple <$> traverse interpret es - SS.Record bs -> VRecord <$> traverse interpret bs - SS.Index e1 e2 -> do a <- interpret e1 - i <- interpret e2 - return (indexValue a i) - SS.Lookup e n -> do a <- interpret e - return (lookupValue a n) - SS.TLookup e i -> do a <- interpret e - return (tupleLookupValue a i) - SS.Var x -> do rw <- getMergedEnv - case Map.lookup x (rwValues rw) of - Nothing -> fail $ "unknown variable: " ++ SS.getVal x - Just v -> return (addTrace (show x) v) - SS.Function pat e -> do env <- getLocalEnv - let f v = withLocalEnv (bindPatternLocal pat Nothing v env) (interpret e) - return $ VLambda f - SS.Application e1 e2 -> do v1 <- interpret e1 - v2 <- interpret e2 - case v1 of - VLambda f -> f v2 - _ -> fail $ "interpret Application: " ++ show v1 - SS.Let dg e -> do env' <- interpretDeclGroup dg - withLocalEnv env' (interpret e) - SS.TSig e _ -> interpret e - SS.IfThenElse e1 e2 e3 -> do v1 <- interpret e1 - case v1 of - VBool b -> interpret (if b then e2 else e3) - _ -> fail $ "interpret IfThenElse: " ++ show v1 - SS.LExpr _ e -> interpret e + SS.Bool _ b -> return $ VBool b + SS.String _ s -> return $ VString (Text.pack s) + SS.Int _ z -> return $ VInteger z + SS.Code str -> do sc <- getSharedContext + cenv <- fmap rwCryptol getMergedEnv + --io $ putStrLn $ "Parsing code: " ++ show str + --showCryptolEnv' cenv + t <- io $ CEnv.parseTypedTerm sc cenv + $ locToInput str + return (toValue t) + SS.CType str -> do cenv <- fmap rwCryptol getMergedEnv + s <- io $ CEnv.parseSchema cenv + $ locToInput str + return (toValue s) + SS.Array _ es -> VArray <$> traverse interpret es + SS.Block _ stmts -> interpretStmts stmts + SS.Tuple _ es -> VTuple <$> traverse interpret es + SS.Record _ bs -> VRecord <$> traverse interpret bs + SS.Index _ e1 e2 -> do a <- interpret e1 + i <- interpret e2 + return (indexValue a i) + SS.Lookup _ e n -> do a <- interpret e + return (lookupValue a n) + SS.TLookup _ e i -> do a <- interpret e + return (tupleLookupValue a i) + SS.Var x -> do rw <- getMergedEnv + case Map.lookup x (rwValues rw) of + Nothing -> fail $ "unknown variable: " ++ SS.getVal x + Just v -> return (addTrace (show x) v) + SS.Function _ pat e -> do env <- getLocalEnv + let f v = withLocalEnv (bindPatternLocal pat Nothing v env) (interpret e) + return $ VLambda f + SS.Application _ e1 e2 -> do v1 <- interpret e1 + v2 <- interpret e2 + case v1 of + VLambda f -> f v2 + _ -> fail $ "interpret Application: " ++ show v1 + SS.Let _ dg e -> do env' <- interpretDeclGroup dg + withLocalEnv env' (interpret e) + SS.TSig _ e _ -> interpret e + SS.IfThenElse _ e1 e2 e3 -> do v1 <- interpret e1 + case v1 of + VBool b -> interpret (if b then e2 else e3) + _ -> fail $ "interpret IfThenElse: " ++ show v1 locToInput :: Located String -> CEnv.InputText locToInput l = CEnv.InputText { CEnv.inpText = getVal l @@ -229,9 +226,9 @@ interpretDecl env (SS.Decl _ pat mt expr) = do interpretFunction :: LocalEnv -> SS.Expr -> Value interpretFunction env expr = case expr of - SS.Function pat e -> VLambda f + SS.Function _ pat e -> VLambda f where f v = withLocalEnv (bindPatternLocal pat Nothing v env) (interpret e) - SS.TSig e _ -> interpretFunction env e + SS.TSig _ e _ -> interpretFunction env e _ -> error "interpretFunction: not a function" interpretDeclGroup :: SS.DeclGroup -> TopLevel LocalEnv @@ -247,15 +244,22 @@ interpretDeclGroup (SS.Recursive ds) = interpretStmts :: [SS.Stmt] -> TopLevel Value interpretStmts stmts = let ?fileReader = BS.readFile in + -- XXX are the uses of withPosition here suitable? not super clear case stmts of [] -> fail "empty block" - [SS.StmtBind pos (SS.PWild _) _ e] -> withPosition pos (interpret e) + [SS.StmtBind pos (SS.PWild _patpos _) _ e] -> withPosition pos (interpret e) SS.StmtBind pos pat _mcxt e : ss -> do env <- getLocalEnv v1 <- withPosition pos (interpret e) let f v = withLocalEnv (bindPatternLocal pat Nothing v env) (interpretStmts ss) bindValue pos v1 (VLambda f) - SS.StmtLet _ bs : ss -> interpret (SS.Let bs (SS.Block ss)) + SS.StmtLet pos bs : ss -> + -- Caution: the position pos is not the correct position for + -- the block ss. However, interpret on Block ignores the + -- position there, so all we need is a placeholder for it to + -- ignore. Therefore, don't take the trouble to compute the + -- correct position (the bounding box on the statements ss). + interpret (SS.Let pos bs (SS.Block pos ss)) SS.StmtCode _ s : ss -> do sc <- getSharedContext rw <- getMergedEnv @@ -284,17 +288,25 @@ processStmtBind :: SS.Expr -> m () processStmtBind printBinds pat _mc expr = do -- mx mt - let (mx, mt) = case pat of - SS.PWild t -> (Nothing, t) - SS.PVar x t -> (Just x, t) - _ -> (Nothing, Nothing) + -- Extract the variable and type from the pattern, if any. If there + -- isn't any single variable use "it". We seem to get here only for + -- statements typed at the repl, so it apparently isn't wrong to use + -- PosREPL. All the same I wonder if we'd be better off always using + -- the position from the pattern. (Experimentally, for the time being + -- at least it seems the position doesn't actually get used, e.g. for + -- type errors it ends up using some other arguably wrong position; + -- may need to come back later.) + -- XXX: it seems problematic to discard the type for a tuple binding... let it = SS.Located "it" "it" SS.PosREPL - let lname = maybe it id mx + let (lname, mt) = case pat of + SS.PWild _pos t -> (it, t) + SS.PVar _pos x t -> (x, t) + SS.PTuple _pos _pats -> (it, Nothing) ctx <- SS.tContext <$> getMonadContext let expr' = case mt of Nothing -> expr - Just t -> SS.TSig expr (SS.tBlock ctx t) - let decl = SS.Decl (SS.getPos expr) pat Nothing expr' + Just t -> SS.TSig (SS.maxSpan' expr t) expr (SS.tBlock ctx t) + let decl = SS.Decl (SS.maxSpan' pat expr') pat Nothing expr' rw <- liftTopLevel getMergedEnv let opts = rwPPOpts rw @@ -318,7 +330,7 @@ processStmtBind printBinds pat _mc expr = do -- mx mt -- Print non-unit result if it was not bound to a variable case pat of - SS.PWild _ | printBinds && not (isVUnit result) -> + SS.PWild _ _ | printBinds && not (isVUnit result) -> liftTopLevel $ do nenv <- io . scGetNamingEnv =<< getSharedContext printOutLnTop Info (showsPrecValue opts nenv 0 result "") diff --git a/src/SAWScript/MGU.hs b/src/SAWScript/MGU.hs index e64b56df99..a31b86e521 100644 --- a/src/SAWScript/MGU.hs +++ b/src/SAWScript/MGU.hs @@ -31,6 +31,7 @@ import Control.Monad.Reader import Control.Monad.State import Control.Monad.Identity import Data.Map (Map) +import Data.Either (partitionEithers) import qualified Data.Map as M import qualified Data.Set as S @@ -274,7 +275,6 @@ newtype TI a = TI { unTI :: ReaderT RO (StateT RW Identity) a } data RO = RO { typeEnv :: M.Map (Located Name) Schema , typedefEnv :: M.Map Name Type - , currentExprPos :: Pos } data RW = RW @@ -295,30 +295,48 @@ newTypeIndex = do newType :: TI Type newType = TyUnifyVar <$> newTypeIndex -withExprPos :: Pos -> TI a -> TI a -withExprPos p = local (\e -> e { currentExprPos = p }) - newTypePattern :: Pattern -> TI (Type, Pattern) newTypePattern pat = case pat of - PWild mt -> do t <- maybe newType return mt - return (t, PWild (Just t)) - PVar x mt -> do t <- maybe newType return mt - return (t, PVar x (Just t)) - PTuple ps -> do (ts, ps') <- unzip <$> mapM newTypePattern ps - return (tTuple ts, PTuple ps') - LPattern pos pat' -> withExprPos pos (newTypePattern pat') + PWild pos mt -> + do t <- maybe newType return mt + return (t, PWild pos (Just t)) + PVar pos x mt -> + do t <- maybe newType return mt + return (t, PVar pos x (Just t)) + PTuple pos ps -> + do (ts, ps') <- unzip <$> mapM newTypePattern ps + return (tTuple ts, PTuple pos ps') appSubstM :: AppSubst t => t -> TI t appSubstM t = do s <- TI $ gets subst return $ appSubst s t -recordError :: String -> TI () -recordError err = do pos <- currentExprPos <$> ask - TI $ modify $ \rw -> - rw { errors = (pos, err) : errors rw } +recordError :: Pos -> String -> TI () +recordError pos err = do + TI $ modify $ \rw -> rw { errors = (pos, err) : errors rw } +-- +-- Unify two types. +-- + +-- When typechecking an expression the first type argument (t1) should +-- be the type expected from the context, and the second (t2) should +-- be the type found in the expression appearing in that context. For +-- example, when checking the second argument of a function application +-- (Application _pos e1 e2) checking e1 gives rise to an expected type +-- for e2, so when unifying that with the result of checking e2 the +-- t1 argument should be the expected type arising from e1, the t2 +-- argument should be the type returned by checking e2, and the position +-- argument should be the position of e2 (not the position of the +-- enclosing apply node). If it doesn't work, the message generated +-- will be of the form "pos: found t2, expected t1". +-- +-- Other cases should pass the arguments analogously. As of this +-- writing some are definitely backwards. +-- +-- Further notes on error messages: -- -- The error message returned by mgu already prints the types at some -- length, so we don't need to print any of that again. @@ -329,7 +347,7 @@ recordError err = do pos <- currentExprPos <$> ask -- recognizable. -- -- The LName passed in is (at least in most cases) the name of the --- top-level binding the failure appears inside. Its position is +-- top-level binding the unification happens inside. Its position is -- therefore usually not where the problem is except in a very -- abstract sense and shouldn't be printed as if it's the error -- location. So tack it onto the end of everything. @@ -339,14 +357,14 @@ recordError err = do pos <- currentExprPos <$> ask -- it entirely, but that seems like a reasonable thing to do in the -- future given more clarity. -- -unify :: LName -> Type -> Type -> TI () -unify m t1 t2 = do +unify :: LName -> Type -> Pos -> Type -> TI () +unify m t1 pos t2 = do t1' <- appSubstM =<< instantiateM t1 t2' <- appSubstM =<< instantiateM t2 case mgu t1' t2' of Right s -> TI $ modify $ \rw -> rw { subst = s @@ subst rw } Left msgs -> - recordError $ unlines $ firstline : morelines' + recordError pos $ unlines $ firstline : morelines' where firstline = "Type mismatch." morelines = ppFailMGU msgs ++ ["within " ++ show m] @@ -375,22 +393,20 @@ bindPattern pat = bindSchemas bs patternBindings :: Pattern -> [(Located Name, Maybe Type)] patternBindings pat = case pat of - PWild _mt -> [] - PVar x mt -> [(x, mt)] - PTuple ps -> concatMap patternBindings ps - LPattern _ pat' -> patternBindings pat' + PWild _ _mt -> [] + PVar _ x mt -> [(x, mt)] + PTuple _ ps -> concatMap patternBindings ps bindPatternSchema :: Pattern -> Schema -> TI a -> TI a bindPatternSchema pat s@(Forall vs t) m = case pat of - PWild _ -> m - PVar n _ -> bindSchema n s m - PTuple ps -> + PWild _ _ -> m + PVar _ n _ -> bindSchema n s m + PTuple _ ps -> case unlocated t of TyCon (TupleCon _) ts -> foldr ($) m [ bindPatternSchema p (Forall vs t') | (p, t') <- zip ps ts ] _ -> m - LPattern pos pat' -> withExprPos pos (bindPatternSchema pat' s m) bindTypedef :: LName -> Type -> TI a -> TI a bindTypedef n t m = @@ -449,32 +465,30 @@ instance AppSubst Schema where instance AppSubst Expr where appSubst s expr = case expr of - TSig e t -> TSig (appSubst s e) (appSubst s t) - Bool _ -> expr - String _ -> expr - Int _ -> expr - Code _ -> expr - CType _ -> expr - Array es -> Array (appSubst s es) - Block bs -> Block (appSubst s bs) - Tuple es -> Tuple (appSubst s es) - Record fs -> Record (appSubst s fs) - Index ar ix -> Index (appSubst s ar) (appSubst s ix) - Lookup rec fld -> Lookup (appSubst s rec) fld - TLookup tpl idx -> TLookup (appSubst s tpl) idx - Var _ -> expr - Function pat body -> Function (appSubst s pat) (appSubst s body) - Application f v -> Application (appSubst s f) (appSubst s v) - Let dg e -> Let (appSubst s dg) (appSubst s e) - IfThenElse e e2 e3 -> IfThenElse (appSubst s e) (appSubst s e2) (appSubst s e3) - LExpr p e -> LExpr p (appSubst s e) + TSig pos e t -> TSig pos (appSubst s e) (appSubst s t) + Bool _ _ -> expr + String _ _ -> expr + Int _ _ -> expr + Code _ -> expr + CType _ -> expr + Array pos es -> Array pos (appSubst s es) + Block pos bs -> Block pos (appSubst s bs) + Tuple pos es -> Tuple pos (appSubst s es) + Record pos fs -> Record pos (appSubst s fs) + Index pos ar ix -> Index pos (appSubst s ar) (appSubst s ix) + Lookup pos rec fld -> Lookup pos (appSubst s rec) fld + TLookup pos tpl idx -> TLookup pos (appSubst s tpl) idx + Var _ -> expr + Function pos pat body -> Function pos (appSubst s pat) (appSubst s body) + Application pos f v -> Application pos (appSubst s f) (appSubst s v) + Let pos dg e -> Let pos (appSubst s dg) (appSubst s e) + IfThenElse pos e e2 e3 -> IfThenElse pos (appSubst s e) (appSubst s e2) (appSubst s e3) instance AppSubst Pattern where appSubst s pat = case pat of - PWild mt -> PWild (appSubst s mt) - PVar x mt -> PVar x (appSubst s mt) - PTuple ps -> PTuple (appSubst s ps) - LPattern _ pat' -> appSubst s pat' + PWild pos mt -> PWild pos (appSubst s mt) + PVar pos x mt -> PVar pos x (appSubst s mt) + PTuple pos ps -> PTuple pos (appSubst s ps) instance (Ord k, AppSubst a) => AppSubst (M.Map k a) where appSubst s = fmap (appSubst s) @@ -531,86 +545,86 @@ type OutStmt = Stmt inferE :: (LName, Expr) -> TI (OutExpr,Type) inferE (ln, expr) = case expr of - Bool b -> return (Bool b, tBool) - String s -> return (String s, tString) - Int i -> return (Int i, tInt) - Code s -> return (Code s, tTerm) - CType s -> return (CType s, tType) + Bool pos b -> return (Bool pos b, tBool) + String pos s -> return (String pos s, tString) + Int pos i -> return (Int pos i, tInt) + Code s -> return (Code s, tTerm) + CType s -> return (CType s, tType) - Array [] -> + Array pos [] -> do a <- newType - return (Array [], tArray a) + return (Array pos [], tArray a) - Array (e:es) -> + Array pos (e:es) -> do (e',t) <- inferE (ln, e) es' <- mapM (flip (checkE ln) t) es - return (Array (e':es'), tArray t) + return (Array pos (e':es'), tArray t) - Block bs -> + Block pos bs -> do ctx <- newType - (bs',t') <- inferStmts ln ctx bs - return (Block bs', tBlock ctx t') + (bs',t') <- inferStmts ln pos ctx bs + return (Block pos bs', tBlock ctx t') - Tuple es -> + Tuple pos es -> do (es',ts) <- unzip `fmap` mapM (inferE . (ln,)) es - return (Tuple es', tTuple ts) + return (Tuple pos es', tTuple ts) - Record fs -> + Record pos fs -> do (nes',nts) <- unzip `fmap` mapM (inferField ln) (M.toList fs) - return (Record (M.fromList nes'), TyRecord $ M.fromList nts) + return (Record pos (M.fromList nes'), TyRecord $ M.fromList nts) - Index ar ix -> + Index pos ar ix -> do (ar',at) <- inferE (ln,ar) ix' <- checkE ln ix tInt t <- newType - unify ln (tArray t) at - return (Index ar' ix', t) + unify ln (tArray t) (getPos ar') at + return (Index pos ar' ix', t) - Lookup e n -> + Lookup pos e n -> do (e1,t) <- inferE (ln, e) t1 <- appSubstM =<< instantiateM t elTy <- case unlocated t1 of TyRecord fs | Just ty <- M.lookup n fs -> return ty | otherwise -> - do recordError $ unlines + do recordError pos $ unlines [ "Selecting a missing field." , "Field name: " ++ n ] newType - _ -> do recordError $ unlines + _ -> do recordError pos $ unlines [ "Record lookup on non-record argument." , "Field name: " ++ n ] newType - return (Lookup e1 n, elTy) + return (Lookup pos e1 n, elTy) - TLookup e i -> + TLookup pos e i -> do (e1,t) <- inferE (ln,e) t1 <- appSubstM =<< instantiateM t elTy <- case unlocated t1 of TyCon (TupleCon n) tys | i < n -> return (tys !! fromIntegral i) | otherwise -> - do recordError $ unlines + do recordError pos $ unlines [ "Tuple index out of bounds." , "Given index " ++ show i ++ " is too large for tuple size of " ++ show n ] newType - _ -> do recordError $ unlines + _ -> do recordError pos $ unlines [ "Tuple lookup on non-tuple argument." , "Given index " ++ show i ] newType - return (TLookup e1 i, elTy) + return (TLookup pos e1 i, elTy) Var x -> do env <- TI $ asks typeEnv case M.lookup x env of Nothing -> do - recordError $ unlines + recordError (getPos x) $ unlines [ "Unbound variable: " ++ show x , "Note that some built-in commands are available only after running" , "either `enable_deprecated` or `enable_experimental`." @@ -621,43 +635,40 @@ inferE (ln, expr) = case expr of ts <- mapM (const newType) as return (Var x, instantiate (M.fromList (zip as ts)) t) - Function pat body -> + Function pos pat body -> do (pt, pat') <- newTypePattern pat (body', t) <- bindPattern pat' $ inferE (ln, body) - return (Function pat' body', tFun pt t) + return (Function pos pat' body', tFun pt t) - Application f v -> + Application pos f v -> do (v',fv) <- inferE (ln,v) t <- newType let ft = tFun fv t f' <- checkE ln f ft - return (Application f' v', t) + return (Application pos f' v', t) - Let dg body -> + Let pos dg body -> do dg' <- inferDeclGroup dg (body', t) <- bindDeclGroup dg' (inferE (ln, body)) - return (Let dg' body', t) + return (Let pos dg' body', t) - TSig e t -> + TSig _pos e t -> do t' <- checkKind t (e',t'') <- inferE (ln,e) - unify ln t' t'' + unify ln t' (getPos e') t'' return (e',t'') - IfThenElse e1 e2 e3 -> + IfThenElse pos e1 e2 e3 -> do e1' <- checkE ln e1 tBool (e2', t) <- inferE (ln, e2) e3' <- checkE ln e3 t - return (IfThenElse e1' e2' e3', t) - - LExpr p e -> - withExprPos p (inferE (ln, e)) + return (IfThenElse pos e1' e2' e3', t) checkE :: LName -> Expr -> Type -> TI OutExpr checkE m e t = do (e',t') <- inferE (m,e) - unify m t t' + unify m t (getPos e') t' return e' -- Take a struct field binding (name and expression) and return the @@ -677,79 +688,94 @@ inferDeclGroup (Recursive ds) = do ds' <- inferRecDecls ds return (Recursive ds') -inferStmts :: LName -> Type -> [Stmt] -> TI ([OutStmt], Type) +-- the passed-in position should be the position for the whole statement block +-- the first type argument (ctx) is ... XXX +inferStmts :: LName -> Pos -> Type -> [Stmt] -> TI ([OutStmt], Type) -inferStmts m _ctx [] = do - recordError ("do block must include at least one expression at " ++ show m) +inferStmts m pos _ctx [] = do + recordError pos ("do block must include at least one expression at " ++ show m) t <- newType return ([], t) -inferStmts m ctx [StmtBind pos (PWild mt) mc e] = do +inferStmts m _dopos ctx [StmtBind spos (PWild patpos mt) mc e] = do t <- maybe newType return mt e' <- checkE m e (tBlock ctx t) mc' <- case mc of Nothing -> return ctx Just ty -> do ty' <- checkKind ty - unify m ty ctx -- TODO: should this be ty'? + -- dholland 20240628 are the type arguments backwards? thought + -- so at first but now I'm not sure. Also I'm not sure this is + -- the right position to use. Where does mc come from? Is it a + -- source annotation? If so it should probably have its own + -- position. XXX + unify m ty (getPos e) ctx -- TODO: should this be ty'? return ty' - return ([StmtBind pos (PWild (Just t)) (Just mc') e'],t) + return ([StmtBind spos (PWild patpos (Just t)) (Just mc') e'],t) -inferStmts m _ [_] = do - recordError ("do block must end with expression at " ++ show m) +inferStmts m dopos _ [_] = do + recordError dopos ("do block must end with expression at " ++ show m) t <- newType return ([],t) -inferStmts m ctx (StmtBind pos pat mc e : more) = do +inferStmts m dopos ctx (StmtBind spos pat mc e : more) = do (pt, pat') <- newTypePattern pat e' <- checkE m e (tBlock ctx pt) mc' <- case mc of Nothing -> return ctx Just c -> do c' <- checkKind c - unify m c ctx + -- XXX same as above + unify m c (getPos e) ctx return c' - (more', t') <- bindPattern pat' $ inferStmts m ctx more + (more', t') <- bindPattern pat' $ inferStmts m dopos ctx more - return (StmtBind pos pat' (Just mc') e' : more', t') + return (StmtBind spos pat' (Just mc') e' : more', t') -inferStmts m ctx (StmtLet pos dg : more) = do +inferStmts m dopos ctx (StmtLet spos dg : more) = do dg' <- inferDeclGroup dg - (more', t) <- bindDeclGroup dg' (inferStmts m ctx more) - return (StmtLet pos dg' : more', t) + (more', t) <- bindDeclGroup dg' (inferStmts m dopos ctx more) + return (StmtLet spos dg' : more', t) -inferStmts m ctx (StmtCode pos s : more) = do - (more',t) <- inferStmts m ctx more - return (StmtCode pos s : more', t) +inferStmts m dopos ctx (StmtCode spos s : more) = do + (more',t) <- inferStmts m dopos ctx more + return (StmtCode spos s : more', t) -inferStmts m ctx (StmtImport pos imp : more) = do - (more', t) <- inferStmts m ctx more - return (StmtImport pos imp : more', t) +inferStmts m dopos ctx (StmtImport spos imp : more) = do + (more', t) <- inferStmts m dopos ctx more + return (StmtImport spos imp : more', t) -inferStmts m ctx (StmtTypedef pos name ty : more) = +inferStmts m dopos ctx (StmtTypedef spos name ty : more) = bindTypedef name ty $ do - (more', t) <- inferStmts m ctx more - return (StmtTypedef pos name ty : more', t) - -patternLNames :: Pattern -> [LName] -patternLNames pat = - case pat of - PWild _ -> [] - PVar n _ -> [n] - PTuple ps -> concatMap patternLNames ps - LPattern _ pat' -> patternLNames pat' + (more', t) <- inferStmts m dopos ctx more + return (StmtTypedef spos name ty : more', t) +-- Get the position and name of the first binding in a pattern, +-- for use as context info when printing messages. If there's a +-- real variable, prefer that (Right cases); otherwise take the +-- position of the first _ or () (Left cases). patternLName :: Pattern -> LName -patternLName pat = - case patternLNames pat of - (n : _) -> n - [] -> Located "_" "_" PosREPL +patternLName pat0 = + case visit pat0 of + Left pos -> Located "_" "_" pos + Right n -> n + where + visit pat = + case pat of + PWild pos _ -> Left pos + PVar _ n _ -> Right n + PTuple pos [] -> Left pos + PTuple allpos ps -> + case partitionEithers $ map visit ps of + (_, n : _) -> Right n + (pos : _, _) -> Left pos + _ -> Left allpos constrainTypeWithPattern :: LName -> Type -> Pattern -> TI () constrainTypeWithPattern ln t pat = do (pt, _pat') <- newTypePattern pat - unify ln t pt + unify ln t (getPos pat) pt inferDecl :: Decl -> TI Decl -inferDecl (Decl pos pat _ e) = withExprPos pos $ do +inferDecl (Decl pos pat _ e) = do let n = patternLName pat (e',t) <- inferE (n, e) constrainTypeWithPattern n t pat @@ -762,8 +788,8 @@ inferRecDecls ds = (_ts, pats') <- unzip <$> mapM newTypePattern pats (es, ts) <- fmap unzip $ flip (foldr bindPattern) pats' - $ sequence [ withExprPos pos $ inferE (patternLName p, e) - | Decl pos p _ e <- ds + $ sequence [ inferE (patternLName p, e) + | Decl _pos p _ e <- ds ] sequence_ $ zipWith (constrainTypeWithPattern (patternLName (head pats))) ts pats' ess <- generalize es ts @@ -799,26 +825,26 @@ checkKind = return checkDeclGroup :: Map LName Schema -> Map Name Type -> DeclGroup -> Either [(Pos, String)] DeclGroup checkDeclGroup env tenv dg = - case evalTIWithEnv env tenv (getPos dg) (inferDeclGroup dg) of + case evalTIWithEnv env tenv (inferDeclGroup dg) of Left errs -> Left errs Right dg' -> Right dg' checkDecl :: Map LName Schema -> Map Name Type -> Decl -> Either [(Pos, String)] Decl checkDecl env tenv decl = - case evalTIWithEnv env tenv (getPos decl) (inferDecl decl) of + case evalTIWithEnv env tenv (inferDecl decl) of Left errs -> Left errs Right decl' -> Right decl' -evalTIWithEnv :: Map LName Schema -> Map Name Type -> Pos -> TI a -> Either [(Pos, String)] a -evalTIWithEnv env tenv pos m = - case runTIWithEnv env tenv pos m of +evalTIWithEnv :: Map LName Schema -> Map Name Type -> TI a -> Either [(Pos, String)] a +evalTIWithEnv env tenv m = + case runTIWithEnv env tenv m of (res, _, []) -> Right res (_, _, errs) -> Left errs -runTIWithEnv :: Map LName Schema -> Map Name Type -> Pos -> TI a -> (a, Subst, [(Pos, String)]) -runTIWithEnv env tenv pos m = (a, subst rw, errors rw) +runTIWithEnv :: Map LName Schema -> Map Name Type -> TI a -> (a, Subst, [(Pos, String)]) +runTIWithEnv env tenv m = (a, subst rw, errors rw) where - m' = runReaderT (unTI m) (RO env tenv pos) + m' = runReaderT (unTI m) (RO env tenv) (a,rw) = runState m' emptyRW -- }}} diff --git a/src/SAWScript/Parser.y b/src/SAWScript/Parser.y index a52be8541b..07518ca456 100644 --- a/src/SAWScript/Parser.y +++ b/src/SAWScript/Parser.y @@ -138,8 +138,8 @@ mbImportSpec :: { (Maybe P.ImportSpec, Pos) } | {- empty -} { (Nothing, Unknown) } Stmt :: { Stmt } - : Expression { StmtBind (getPos $1) (PWild Nothing) Nothing $1 } - | AExpr '<-' Expression {% fmap (\x -> StmtBind (maxSpan [getPos x, getPos $3]) x Nothing $3) (toPattern $1) } + : Expression { StmtBind (getPos $1) (PWild (leadingPos $ getPos $1) Nothing) Nothing $1 } + | AExpr '<-' Expression {% fmap (\x -> StmtBind (maxSpan' x $3) x Nothing $3) (toPattern $1) } | 'rec' sepBy1(Declaration, 'and') { StmtLet (maxSpan [tokPos $1, maxSpan $2]) (Recursive $2) } | 'let' Declaration { StmtLet (maxSpan [tokPos $1, getPos $2]) (NonRecursive $2) } | 'let' Code { StmtCode (maxSpan [tokPos $1, getPos $2]) $2 } @@ -147,50 +147,50 @@ Stmt :: { Stmt } | 'typedef' name '=' Type { StmtTypedef (maxSpan [tokPos $1, getPos $4]) (toLName $2) $4 } Declaration :: { Decl } - : Arg list(Arg) '=' Expression { Decl (maxSpan [getPos $1, getPos $4]) $1 Nothing (buildFunction $2 $4) } + : Arg list(Arg) '=' Expression { Decl (maxSpan' $1 $4) $1 Nothing (buildFunction $2 $4) } | Arg list(Arg) ':' Type '=' Expression - { Decl (maxSpan [getPos $1, getPos $6]) $1 Nothing (buildFunction $2 (TSig $6 $4)) } + { Decl (maxSpan' $1 $6) $1 Nothing (buildFunction $2 (TSig (maxSpan' $4 $6) $6 $4)) } Pattern :: { Pattern } : Arg { $1 } - | name ':' Type { PVar (toLName $1) (Just $3) } + | name ':' Type { PVar (maxSpan [tokPos $1, getPos $3]) (toLName $1) (Just $3) } Arg :: { Pattern } - : name { LPattern (tokPos $1) (PVar (toLName $1) Nothing) } - | '(' ')' { LPattern (maxSpan [tokPos $1, tokPos $2]) (PTuple []) } - | '(' commas(Pattern) ')' { LPattern (maxSpan [tokPos $1, tokPos $3]) (case $2 of [p] -> p; _ -> PTuple $2) } + : name { PVar (tokPos $1) (toLName $1) Nothing } + | '(' ')' { PTuple (maxSpan [tokPos $1, tokPos $2]) [] } + | '(' commas(Pattern) ')' { case $2 of [p] -> p; _ -> PTuple (maxSpan [tokPos $1, tokPos $3]) $2 } Expression :: { Expr } : IExpr { $1 } - | IExpr ':' Type { TSig $1 $3 } + | IExpr ':' Type { TSig (maxSpan' $1 $3) $1 $3 } | '\\' list1(Arg) '->' Expression { buildFunction $2 $4 } - | 'let' Declaration 'in' Expression { Let (NonRecursive $2) $4 } + | 'let' Declaration 'in' Expression { Let (maxSpan [tokPos $1, getPos $4]) (NonRecursive $2) $4 } | 'rec' sepBy1(Declaration, 'and') - 'in' Expression { Let (Recursive $2) $4 } + 'in' Expression { Let (maxSpan [tokPos $1, getPos $4]) (Recursive $2) $4 } | 'if' Expression 'then' Expression - 'else' Expression { IfThenElse $2 $4 $6 } + 'else' Expression { IfThenElse (maxSpan [tokPos $1, getPos $6]) $2 $4 $6 } IExpr :: { Expr } : AExprs { $1 } AExprs :: { Expr } - : list1(AExpr) { LExpr (maxSpan $1) (buildApplication $1) } + : list1(AExpr) { buildApplication $1 } AExpr :: { Expr } -: '(' ')' { LExpr (maxSpan [tokPos $1, tokPos $2]) (Tuple []) } - | '[' ']' { LExpr (maxSpan [tokPos $1, tokPos $2]) (Array []) } - | string { LExpr (tokPos $1) (String (tokStr $1)) } - | Code { Code $1 } - | CType { CType $1 } - | num { LExpr (tokPos $1) (Int (tokNum $1)) } +: '(' ')' { Tuple (maxSpan [tokPos $1, tokPos $2]) [] } + | '[' ']' { Array (maxSpan [tokPos $1, tokPos $2]) [] } + | string { String (tokPos $1) (tokStr $1) } + | Code { Code $1 } + | CType { CType $1 } + | num { Int (tokPos $1) (tokNum $1) } | name { Var (Located (tokStr $1) (tokStr $1) (tokPos $1)) } - | '(' Expression ')' { LExpr (maxSpan [tokPos $1, tokPos $3]) $2 } - | '(' commas2(Expression) ')' { LExpr (maxSpan [tokPos $1, tokPos $3]) (Tuple $2) } - | '[' commas(Expression) ']' { LExpr (maxSpan [tokPos $1, tokPos $3]) (Array $2) } - | '{' commas(Field) '}' { LExpr (maxSpan [tokPos $1, tokPos $3]) (Record (Map.fromList $2)) } - | 'do' '{' termBy(Stmt, ';') '}' { LExpr (maxSpan [tokPos $1, tokPos $4]) (Block $3) } - | AExpr '.' name { LExpr (maxSpan [getPos $1, tokPos $3]) (Lookup $1 (tokStr $3)) } - | AExpr '.' num { LExpr (maxSpan [getPos $1, tokPos $3]) (TLookup $1 (tokNum $3)) } + | '(' Expression ')' { $2 } -- { Parens (maxSpan [tokPos $1, tokPos $3]) $2 } + | '(' commas2(Expression) ')' { Tuple (maxSpan [tokPos $1, tokPos $3]) $2 } + | '[' commas(Expression) ']' { Array (maxSpan [tokPos $1, tokPos $3]) $2 } + | '{' commas(Field) '}' { Record (maxSpan [tokPos $1, tokPos $3]) (Map.fromList $2) } + | 'do' '{' termBy(Stmt, ';') '}' { Block (maxSpan [tokPos $1, tokPos $4]) $3 } + | AExpr '.' name { Lookup (maxSpan [getPos $1, tokPos $3]) $1 (tokStr $3) } + | AExpr '.' num { TLookup (maxSpan [getPos $1, tokPos $3]) $1 (tokNum $3) } Code :: { Located String } : code { Located (tokStr $1) (tokStr $1) (tokPos $1) } @@ -328,19 +328,22 @@ parseError toks = case toks of [] -> Left UnexpectedEOF t : _ -> Left (UnexpectedToken t) +once :: Pattern -> Expr -> Expr +once pat e = Function (maxSpan' pat e) pat e buildFunction :: [Pattern] -> Expr -> Expr -buildFunction args e = foldr Function e args +buildFunction args e = + foldr {-(\pat e -> once pat e)-} once e args buildApplication :: [Expr] -> Expr -buildApplication = foldl1 (\e body -> Application e body) +buildApplication es = + foldl1 (\e body -> Application (maxSpan' e body) e body) es toPattern :: Expr -> Either ParseError Pattern toPattern expr = case expr of - Tuple es -> PTuple `fmap` mapM toPattern es - TSig (Var x) t -> return (PVar x (Just t)) - Var x -> return (PVar x Nothing) - LExpr pos e -> LPattern pos `fmap` toPattern e + Tuple pos es -> PTuple pos `fmap` mapM toPattern es + TSig pos (Var x) t -> return (PVar pos x (Just t)) + Var x -> return (PVar (getPos x) x Nothing) _ -> Left (InvalidPattern expr) } diff --git a/src/SAWScript/Position.hs b/src/SAWScript/Position.hs index ef7dfecf5b..b3229d9b2b 100644 --- a/src/SAWScript/Position.hs +++ b/src/SAWScript/Position.hs @@ -42,6 +42,7 @@ renderDoc :: PP.Doc ann -> String renderDoc doc = PP.renderString (PP.layoutPretty opts doc) where opts = PP.LayoutOptions (PP.AvailablePerLine 80 0.8) +-- This is not used, which is probably good because it seems odd endPos :: FilePath -> Pos endPos f = Range f 0 0 0 0 @@ -49,6 +50,12 @@ fmtPos :: Pos -> String -> String fmtPos p m = show p ++ ":\n" ++ m' where m' = intercalate "\n" . map (" " ++) . lines $ m +-- Get the empty position at the beginning of the position of something else. +leadingPos :: Pos -> Pos +leadingPos pos = case pos of + Range f l1 c1 _l2 _c2 -> Range f l1 c1 l1 c1 + _ -> pos + spanPos :: Pos -> Pos -> Pos spanPos (PosInternal str) _ = PosInternal str spanPos PosREPL _ = PosREPL @@ -118,9 +125,15 @@ class Positioned a where instance Positioned Pos where getPos p = p +-- Caution: if you write maxSpan (a, b) for heterogeneous types a and b, +-- it will typecheck but not actually work correctly. Either call getPos +-- first or use maxSpan' for this case. maxSpan :: (Functor t, Foldable t, Positioned a) => t a -> Pos maxSpan xs = foldr spanPos Unknown (fmap getPos xs) +maxSpan' :: (Positioned a, Positioned b) => a -> b -> Pos +maxSpan' x y = spanPos (getPos x) (getPos y) + -- WithPos ----------------------------------------------------------------- data WithPos a = WithPos { _wpPos :: Pos, _wpVal :: a } From 0299cff41b549619df4bb77df0da38bc2a634fb1 Mon Sep 17 00:00:00 2001 From: David Holland Date: Wed, 17 Jul 2024 13:14:38 -0400 Subject: [PATCH 3/9] Remove (derived) Eq instances on AST elements, except Type. These contain source positions, so derived Eq instances aren't in general going to produce the desired behavior. Leave the Eq instance on Type for the moment because it's used in the typechecker. This is going to require further attention. --- src/SAWScript/AST.hs | 16 ++++++++-------- 1 file changed, 8 insertions(+), 8 deletions(-) diff --git a/src/SAWScript/AST.hs b/src/SAWScript/AST.hs index defc47bfd6..d3f31328cc 100644 --- a/src/SAWScript/AST.hs +++ b/src/SAWScript/AST.hs @@ -100,7 +100,7 @@ data Import = Import , iAs :: Maybe P.ModName , iSpec :: Maybe P.ImportSpec , iPos :: Pos - } deriving (Eq, Show) + } deriving Show instance Positioned Import where getPos = iPos @@ -129,7 +129,7 @@ data Expr | Let Pos DeclGroup Expr | TSig Pos Expr Type | IfThenElse Pos Expr Expr Expr - deriving (Eq, Show) -- XXX eq? + deriving Show instance Positioned Expr where getPos (Bool pos _) = pos @@ -155,7 +155,7 @@ data Pattern = PWild Pos (Maybe Type) | PVar Pos LName (Maybe Type) | PTuple Pos [Pattern] - deriving (Eq, Show) -- XXX Eq? + deriving Show instance Positioned Pattern where getPos (PWild pos _) = pos @@ -168,7 +168,7 @@ data Stmt | StmtCode Pos (Located String) | StmtImport Pos Import | StmtTypedef Pos (Located String) Type - deriving (Eq, Show) + deriving Show instance Positioned Stmt where getPos (StmtBind pos _ _ _) = pos @@ -180,7 +180,7 @@ instance Positioned Stmt where data DeclGroup = Recursive [Decl] | NonRecursive Decl - deriving (Eq, Show) + deriving Show instance Positioned DeclGroup where getPos (Recursive ds) = maxSpan ds @@ -188,7 +188,7 @@ instance Positioned DeclGroup where data Decl = Decl { dPos :: Pos, dPat :: Pattern, dType :: Maybe Schema, dDef :: Expr } - deriving (Eq, Show) + deriving Show instance Positioned Decl where getPos = dPos @@ -214,7 +214,7 @@ data Type | TyUnifyVar TypeIndex -- ^ For internal typechecker use only | TySkolemVar Name TypeIndex -- ^ For internal typechecker use only | LType Pos Type - deriving (Eq,Show) + deriving (Show, Eq) instance Positioned Type where getPos (LType pos _) = pos @@ -241,7 +241,7 @@ data TyCon deriving (Eq, Show) data Schema = Forall [Name] Type - deriving (Eq, Show) + deriving Show -- }}} From 4b742e261d672eb39e60434a0d291c7343c5ff7b Mon Sep 17 00:00:00 2001 From: David Holland Date: Wed, 17 Jul 2024 19:42:56 -0400 Subject: [PATCH 4/9] Remove the Eq instance on Type. There were only two uses of it; provide matching-based alternatives for both, on the grounds that if we don't need an explicit Eq instance that specifically ignores position information it's better not to have to write one. The use in MGU handled peeling off any LType nodes; the one in Interpreter did not and was therefore potentially wrong... --- src/SAWScript/AST.hs | 16 +++++++++++++++- src/SAWScript/Interpreter.hs | 7 ++++--- src/SAWScript/MGU.hs | 3 ++- 3 files changed, 21 insertions(+), 5 deletions(-) diff --git a/src/SAWScript/AST.hs b/src/SAWScript/AST.hs index d3f31328cc..c98f90a356 100644 --- a/src/SAWScript/AST.hs +++ b/src/SAWScript/AST.hs @@ -33,6 +33,7 @@ module SAWScript.AST , tString, tTerm, tType, tBool, tInt, tAIG, tCFG , tJVMSpec, tLLVMSpec, tMIRSpec , tBlock, tContext, tVar + , isContext , PrettyPrint(..), pShow, commaSepAll, prettyWholeModule ) where @@ -214,7 +215,7 @@ data Type | TyUnifyVar TypeIndex -- ^ For internal typechecker use only | TySkolemVar Name TypeIndex -- ^ For internal typechecker use only | LType Pos Type - deriving (Show, Eq) + deriving Show instance Positioned Type where getPos (LType pos _) = pos @@ -509,3 +510,16 @@ tVar :: Name -> Type tVar n = TyVar n -- }}} + +-- Type Classifiers {{{ + +-- The idea is that calling these is/should be less messy than direct +-- pattern matching, and also help a little to avoid splattering the +-- internal representation of types all over the place. + +isContext :: Context -> Type -> Bool +isContext c ty = case ty of + TyCon (ContextCon c') [] | c' == c -> True + _ -> False + +-- }}} diff --git a/src/SAWScript/Interpreter.hs b/src/SAWScript/Interpreter.hs index 8b67168b6e..c85e4010d1 100644 --- a/src/SAWScript/Interpreter.hs +++ b/src/SAWScript/Interpreter.hs @@ -302,10 +302,11 @@ processStmtBind printBinds pat _mc expr = do -- mx mt SS.PWild _pos t -> (it, t) SS.PVar _pos x t -> (x, t) SS.PTuple _pos _pats -> (it, Nothing) - ctx <- SS.tContext <$> getMonadContext + ctx <- getMonadContext + let tyctx = SS.tContext ctx let expr' = case mt of Nothing -> expr - Just t -> SS.TSig (SS.maxSpan' expr t) expr (SS.tBlock ctx t) + Just t -> SS.TSig (SS.maxSpan' expr t) expr (SS.tBlock tyctx t) let decl = SS.Decl (SS.maxSpan' pat expr') pat Nothing expr' rw <- liftTopLevel getMergedEnv let opts = rwPPOpts rw @@ -320,7 +321,7 @@ processStmtBind printBinds pat _mc expr = do -- mx mt case schema of SS.Forall [] t -> case t of - SS.TyCon SS.BlockCon [c, t'] | c == ctx -> do + SS.TyCon SS.BlockCon [c, t'] | SS.isContext ctx c -> do result <- actionFromValue val return (result, t') _ -> return (val, t) diff --git a/src/SAWScript/MGU.hs b/src/SAWScript/MGU.hs index a31b86e521..ccd4f87c65 100644 --- a/src/SAWScript/MGU.hs +++ b/src/SAWScript/MGU.hs @@ -174,6 +174,7 @@ ppFailMGU (FailMGU start eflines lastfunlines) = mgu :: Type -> Type -> Either FailMGU Subst mgu (LType _ t) t2 = mgu t t2 mgu t1 (LType _ t) = mgu t1 t +mgu (TyUnifyVar i) (TyUnifyVar j) | i == j = return emptySubst mgu (TyUnifyVar i) t2 = bindVar i t2 mgu t1 (TyUnifyVar i) = bindVar i t1 mgu r1@(TyRecord ts1) r2@(TyRecord ts2) @@ -209,9 +210,9 @@ mgus (t1:ts1) (t2:ts2) = do mgus ts1 ts2 = failMGU' $ "Wrong number of arguments. Expected " ++ show (length ts1) ++ " but got " ++ show (length ts2) +-- Does not handle the case where t _is_ TyUnifyVar i; the caller handles that bindVar :: TypeIndex -> Type -> Either FailMGU Subst bindVar i t - | t == TyUnifyVar i = return emptySubst | i `S.member` unifyVars t = failMGU' "occurs check failMGUs" -- FIXME: error message | otherwise = return (singletonSubst i t) From 3cd149a1d88bbddca80349683f233306230515d9 Mon Sep 17 00:00:00 2001 From: David Holland Date: Wed, 17 Jul 2024 23:25:07 -0400 Subject: [PATCH 5/9] Update the literal "it" in Interpreter.hs. We concluded after discussion that using the more precise position from the pattern involved is preferable to using PosREPL, even though the name "it" is predicated on this coming from the repl. --- src/SAWScript/Interpreter.hs | 12 ++++-------- 1 file changed, 4 insertions(+), 8 deletions(-) diff --git a/src/SAWScript/Interpreter.hs b/src/SAWScript/Interpreter.hs index c85e4010d1..6b5c7b9f44 100644 --- a/src/SAWScript/Interpreter.hs +++ b/src/SAWScript/Interpreter.hs @@ -291,17 +291,13 @@ processStmtBind printBinds pat _mc expr = do -- mx mt -- Extract the variable and type from the pattern, if any. If there -- isn't any single variable use "it". We seem to get here only for -- statements typed at the repl, so it apparently isn't wrong to use - -- PosREPL. All the same I wonder if we'd be better off always using - -- the position from the pattern. (Experimentally, for the time being - -- at least it seems the position doesn't actually get used, e.g. for - -- type errors it ends up using some other arguably wrong position; - -- may need to come back later.) + -- "it". -- XXX: it seems problematic to discard the type for a tuple binding... - let it = SS.Located "it" "it" SS.PosREPL + let it pos = SS.Located "it" "it" pos let (lname, mt) = case pat of - SS.PWild _pos t -> (it, t) + SS.PWild pos t -> (it pos, t) SS.PVar _pos x t -> (x, t) - SS.PTuple _pos _pats -> (it, Nothing) + SS.PTuple pos _pats -> (it pos, Nothing) ctx <- getMonadContext let tyctx = SS.tContext ctx let expr' = case mt of From 3dcb3977b227df79234290a5521eca8701b182d8 Mon Sep 17 00:00:00 2001 From: David Holland Date: Thu, 18 Jul 2024 13:14:38 -0400 Subject: [PATCH 6/9] Complete half-finished change in Parser.y. --- src/SAWScript/Parser.y | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) diff --git a/src/SAWScript/Parser.y b/src/SAWScript/Parser.y index 07518ca456..5e240ff8e7 100644 --- a/src/SAWScript/Parser.y +++ b/src/SAWScript/Parser.y @@ -328,11 +328,12 @@ parseError toks = case toks of [] -> Left UnexpectedEOF t : _ -> Left (UnexpectedToken t) -once :: Pattern -> Expr -> Expr -once pat e = Function (maxSpan' pat e) pat e buildFunction :: [Pattern] -> Expr -> Expr buildFunction args e = - foldr {-(\pat e -> once pat e)-} once e args + let once :: Pattern -> Expr -> Expr + once pat e = Function (maxSpan' pat e) pat e + in + foldr once e args buildApplication :: [Expr] -> Expr buildApplication es = From bfcc7baeda6b9b50b1fb645c99159512fc45612d Mon Sep 17 00:00:00 2001 From: David Holland Date: Thu, 18 Jul 2024 13:21:06 -0400 Subject: [PATCH 7/9] Remove unused function endPos. --- src/SAWScript/Position.hs | 4 ---- 1 file changed, 4 deletions(-) diff --git a/src/SAWScript/Position.hs b/src/SAWScript/Position.hs index b3229d9b2b..091346e47f 100644 --- a/src/SAWScript/Position.hs +++ b/src/SAWScript/Position.hs @@ -42,10 +42,6 @@ renderDoc :: PP.Doc ann -> String renderDoc doc = PP.renderString (PP.layoutPretty opts doc) where opts = PP.LayoutOptions (PP.AvailablePerLine 80 0.8) --- This is not used, which is probably good because it seems odd -endPos :: FilePath -> Pos -endPos f = Range f 0 0 0 0 - fmtPos :: Pos -> String -> String fmtPos p m = show p ++ ":\n" ++ m' where m' = intercalate "\n" . map (" " ++) . lines $ m From 022f7ce8fed596449be93f9922c0ddf436d67c22 Mon Sep 17 00:00:00 2001 From: David Holland Date: Thu, 18 Jul 2024 19:47:23 -0400 Subject: [PATCH 8/9] Improve some of the comments. --- src/SAWScript/AST.hs | 6 +++++- src/SAWScript/MGU.hs | 2 +- src/SAWScript/Position.hs | 5 ++++- 3 files changed, 10 insertions(+), 3 deletions(-) diff --git a/src/SAWScript/AST.hs b/src/SAWScript/AST.hs index c98f90a356..6ce4b2274a 100644 --- a/src/SAWScript/AST.hs +++ b/src/SAWScript/AST.hs @@ -517,7 +517,11 @@ tVar n = TyVar n -- pattern matching, and also help a little to avoid splattering the -- internal representation of types all over the place. -isContext :: Context -> Type -> Bool +-- | Check if type 'ty' is a 'Context' type of context 'c'. +isContext :: + Context -- ^ The context 'c' to look for + -> Type -- ^ The type 'ty' to inspect + -> Bool isContext c ty = case ty of TyCon (ContextCon c') [] | c' == c -> True _ -> False diff --git a/src/SAWScript/MGU.hs b/src/SAWScript/MGU.hs index ccd4f87c65..7d97856e23 100644 --- a/src/SAWScript/MGU.hs +++ b/src/SAWScript/MGU.hs @@ -752,7 +752,7 @@ inferStmts m dopos ctx (StmtTypedef spos name ty : more) = -- Get the position and name of the first binding in a pattern, -- for use as context info when printing messages. If there's a -- real variable, prefer that (Right cases); otherwise take the --- position of the first _ or () (Left cases). +-- position of the first wildcard or empty tuple (Left cases). patternLName :: Pattern -> LName patternLName pat0 = case visit pat0 of diff --git a/src/SAWScript/Position.hs b/src/SAWScript/Position.hs index 091346e47f..1ca583399c 100644 --- a/src/SAWScript/Position.hs +++ b/src/SAWScript/Position.hs @@ -46,7 +46,10 @@ fmtPos :: Pos -> String -> String fmtPos p m = show p ++ ":\n" ++ m' where m' = intercalate "\n" . map (" " ++) . lines $ m --- Get the empty position at the beginning of the position of something else. +-- Get the empty position at the beginning of the position of +-- something else. This can be used to provide positions for implicit +-- elements, such as the not-physically-present wildcard in a +-- do-notation binding that doesn't bind anything. leadingPos :: Pos -> Pos leadingPos pos = case pos of Range f l1 c1 _l2 _c2 -> Range f l1 c1 l1 c1 From 2f5bb087c2301b8b928744c72d8367a2a9bb0e83 Mon Sep 17 00:00:00 2001 From: David Holland Date: Mon, 12 Aug 2024 17:09:13 -0400 Subject: [PATCH 9/9] Add a test for a type error that this branch improves. Also add a bunch of infrastructure -- the driver script for this is massively overkill for just this test but we expect this test to grow a lot of siblings in the not-too-distant future. --- intTests/support/test-and-diff.sh | 223 ++++++++++++++++++++++ intTests/test_type_errors/.gitignore | 3 + intTests/test_type_errors/err001.log.good | 10 + intTests/test_type_errors/err001.saw | 1 + intTests/test_type_errors/test.sh | 1 + 5 files changed, 238 insertions(+) create mode 100644 intTests/support/test-and-diff.sh create mode 100644 intTests/test_type_errors/.gitignore create mode 100644 intTests/test_type_errors/err001.log.good create mode 100644 intTests/test_type_errors/err001.saw create mode 100644 intTests/test_type_errors/test.sh diff --git a/intTests/support/test-and-diff.sh b/intTests/support/test-and-diff.sh new file mode 100644 index 0000000000..41affb9e33 --- /dev/null +++ b/intTests/support/test-and-diff.sh @@ -0,0 +1,223 @@ +# test-and-diff.sh: run SAW and diff the output against a reference +# copy. +# +# usage: sh ../support/test-and-diff.sh [verb] +# where verb is: +# test (default) do run-tests, show-diffs, check-diffs +# run-tests run all tests +# show-diffs print all (nonempty) diff outputs +# check-diffs exit 1 if there are any nonempty diff outputs +# good update reference outputs from the current run +# clean delete all results and intermediate output +# +# That is, the arguments are akin to make or similar tools. +# +# Note that this file is meant to be run/spawned/exec'd, not sourced. +# It should also be run explicitly with the shell so that the test +# suite is operable on Windows where #! doesn't work. +# +# This script will test all SAW files (*.saw) it finds in its current +# directory, as follows, assuming T.saw is one such file: +# - run "saw T.saw" +# - produce T.rawlog +# - produce T.log with timestamps stripped out +# - diff T.log against T.log.good to produce T.diff +# +# These steps are "run-tests". It will always run all tests before +# checking any of the outputs. If SAW itself fails (exits non-zero) +# that fact is logged, and if unexpected will cause a diff, but will +# not cause the test run to fail. This allows having tests that are +# expected to fail in SAW, which is important for e.g. checking error +# behavior. +# +# Note: don't write anything that relies on the existence of the +# .rawlog file; one hopes the need for it will eventually go away. +# +# Also note: this script assumes that all *.rawlog, *.log, and *.diff +# files it finds belong to it; they will be deleted at clean time. +# This prevents old outputs to hang around forever when the list of +# tests changes. +# +# It is fine to use this script when you have only one SAW script to +# test. The infrastructure for supporting multiple scripts does not +# cost much. +# +# There is, however, an expectation that if there are multiple scripts +# in one test directory, they are all fast. Having multiple scripts at +# once loses the ability to run them separately or address them +# directly from enclosing test infrastructure. We don't want that to +# incur significant costs or create aggravations. +# +# Note: we could, like make, not rerun tests whose output is newer +# than (all) their inputs. So far I haven't done this. As long as the +# scripts are all fast it probably doesn't matter. +# +# While I've written this script to be careful about spaces, spaces in +# filenames aren't supported. Don't do that; it just creates headaches +# for everyone. +# + +# Get the list of tests. +# +# Note that in some shells (and depending on settings) asking for +# *.saw when there aren't any will yield "*.saw" rather than +# generating an error. +TESTS= +for SCRIPT in *.saw; do + BASE=${SCRIPT%.saw} + TESTS="$TESTS $BASE" +done +if [ "$TESTS" = " *.saw" ] || [ "$TESTS" = " " ]; then + echo "$0: Found no files matching *.saw" 1>&2 + exit 1 +fi + +# Get the current directory, because we'll need to filter it out of +# the saw output. Be sure to get the real current directory. Because +# ksh's silly ideas about symlinks got stuffed into posix, pwd can lie +# and then what it prints won't be the same as what saw outputs. +# +# Don't use the variable PWD for this; it has magic semantics in the +# shell and, for the same reasons, may also lie. +# +# Bomb if the current directory includes a comma (just in case) so we +# can use comma as a delimiter in the seddery below. +CURDIR=$(pwd -P || pwd) +if echo "$CURDIR" | grep -q , >/dev/null; then + echo "$0: Your current directory name contains a comma." 1>&2 + echo "$0: I can't deal with that. Sorry..." 1>&2 + exit 1 +fi + +# shell function for the run-tests op +run-tests() { + for TEST in $TESTS; do + # Remove any existing test.log first as a precaution. This + # protects against misreading the results if the whole run + # gets killed before a new test.log gets produced. + rm -f $TEST.log + + # run the test + # (do not fail if saw does, instead log it) + echo "$SAW $TEST.saw" + $SAW $TEST.saw > $TEST.rawlog 2>&1 || echo FAILED >> $TEST.rawlog + + # Prune the timestamps from the log since they'll never match. + # We also need to shorten pathnames that contain the current + # directory, because saw feels the need to expand pathnames + # (see also saw-script #2082). + sed < $TEST.rawlog > $TEST.log ' + /^\[[0-9][0-9]:[0-9][0-9]:[0-9][0-9]\.[0-9][0-9][0-9]\] /{ + s/^..............// + } + s,'"$CURDIR"'/,, + ' + + # Check the output against the expected version. + # Note: because we (intentionally) aren't using set -e, we + # don't need to failure-protect this with || true. + # Send any errors from diff to the output so they get seen. + diff -u $TEST.log.good $TEST.log > $TEST.log.diff 2>&1 + done +} + +# shell function for the show-diffs op +show-diffs() { + # The easy way to do this is just "cat *.diff". While (as + # documented) above we assume all *.diff files belong to us, don't + # do things that way, because there isn't an analogous form for + # check-diffs. Thus if a stray nonempty *.diff file appeared it + # would show up in the show-diffs output but not cause check-diffs + # to fail, and that would be quite confusing. + # + # As long as the number of tests here isn't really excessive the + # shell iteration and resulting multiple cat processes won't cost + # enough to care about. + for TEST in $TESTS; do + cat $TEST.log.diff + done +} + +# shell function for the check-diffs op +check-diffs() { + for TEST in $TESTS; do + if [ -s $TEST.log.diff ]; then + cat 1>&2 <&2 + echo "$0: Cannot update reference outputs" 1>&2 + exit 1 + fi + done + + # now actually do it + if ! [ -f $TEST.log.good ] || \ + ! diff -q $TEST.log.good $TEST.log >/dev/null; then + echo "cp $TEST.log $TEST.log.good" + cp $TEST.log $TEST.log.good + fi +} + +# shell function for the clean op +clean() { + echo "rm -f *.rawlog *.log *.diff" + rm -f *.rawlog *.log *.diff +} + +# shell function for the test op +test() { + run-tests + show-diffs + check-diffs +} + +# run the requested operations +if [ $# = 0 ]; then + test +else + for VERB in "$@"; do + case "$VERB" in + test) + test + ;; + run-tests) + run-tests + ;; + show-diffs|show) # allow "show" as short form + show-diffs + ;; + check-diffs|check) # allow "check" as short form + check-diffs + ;; + good) + good + ;; + clean) + clean + ;; + *) + echo "$0: unknown action $VERB" 1>&2 + exit 1 + ;; + esac + done +fi + +# done +exit 0 diff --git a/intTests/test_type_errors/.gitignore b/intTests/test_type_errors/.gitignore new file mode 100644 index 0000000000..4619758def --- /dev/null +++ b/intTests/test_type_errors/.gitignore @@ -0,0 +1,3 @@ +*.rawlog +*.log +*.diff diff --git a/intTests/test_type_errors/err001.log.good b/intTests/test_type_errors/err001.log.good new file mode 100644 index 0000000000..b6dbe845b0 --- /dev/null +++ b/intTests/test_type_errors/err001.log.good @@ -0,0 +1,10 @@ + Loading file "err001.saw" + err001.saw:1:23-1:24: Type mismatch. + Mismatch of type constructors. Expected: String but got Int + + Expected: String + Found: Int + + within "foo" (err001.saw:1:5-1:8) + +FAILED diff --git a/intTests/test_type_errors/err001.saw b/intTests/test_type_errors/err001.saw new file mode 100644 index 0000000000..e83a7e9860 --- /dev/null +++ b/intTests/test_type_errors/err001.saw @@ -0,0 +1 @@ +let foo () : String = 3; diff --git a/intTests/test_type_errors/test.sh b/intTests/test_type_errors/test.sh new file mode 100644 index 0000000000..5fcd79d0a6 --- /dev/null +++ b/intTests/test_type_errors/test.sh @@ -0,0 +1 @@ +exec ${TEST_SHELL:-bash} ../support/test-and-diff.sh "$@"