diff --git a/.github/workflows/reference-docs.yml b/.github/workflows/reference-docs.yml deleted file mode 100644 index 47937a4b..00000000 --- a/.github/workflows/reference-docs.yml +++ /dev/null @@ -1,51 +0,0 @@ -name: Deploy reference docs to github pages - -on: - push: - branches: ["main"] - workflow_dispatch: - - -# Allow only one concurrent deployment, skipping runs queued between the run in-progress and latest queued. -# However, do NOT cancel in-progress runs as we want to allow these production deployments to complete. -concurrency: - group: "pages" - cancel-in-progress: false - -permissions: - contents: read - pages: write - id-token: write # required by the deploy-pages action for some reason - -jobs: - # Build job - build: - runs-on: ubuntu-latest - steps: - - name: checkout - uses: actions/checkout@v6 - - - name: install nix - uses: cachix/install-nix-action@v31 - with: - github_access_token: ${{ secrets.GITHUB_TOKEN }} - - - name: build with mdbook - run: nix shell --inputs-from . nixpkgs#mdbook -c mdbook build doc - - - name: upload pages artifact - uses: actions/upload-pages-artifact@v4 - with: - path: ./doc/book - - # Deployment job - deploy: - environment: - name: github-pages - url: ${{ steps.deployment.outputs.page_url }} - runs-on: ubuntu-latest - needs: build - steps: - - name: Deploy to GitHub Pages - id: deployment - uses: actions/deploy-pages@v4 diff --git a/doc/.gitignore b/doc/.gitignore deleted file mode 100644 index 7585238e..00000000 --- a/doc/.gitignore +++ /dev/null @@ -1 +0,0 @@ -book diff --git a/doc/book.toml b/doc/book.toml deleted file mode 100644 index 06bc22a4..00000000 --- a/doc/book.toml +++ /dev/null @@ -1,8 +0,0 @@ -[book] -authors = ["The Core Solidity Implementors"] -language = "en" -src = "src" -title = "The Core Solidity Reference" - -[output.html] -mathjax-support = true diff --git a/doc/src/README.md b/doc/src/README.md deleted file mode 100644 index e501955f..00000000 --- a/doc/src/README.md +++ /dev/null @@ -1,48 +0,0 @@ -# Introduction - -## Purpose and Audience - -Core Solidity is an update to the [Solidity](https://docs.soliditylang.org/en/latest/) programming -language. It both extends the language with new features (ADTs, Parametric polymorphism, -Typeclasses), and diverges from Classic Solidity in incompatible ways (most notably by removing -inheritance). This document targets compiler implementers, tooling developers, and language -researchers. It is a reference specification, not a tutorial. - -A prototype implementation exists at [`argotorg/solcore`](https://github.com/argotorg/solcore). The -implementation is a research prototype. It contains bugs, lacks optimizations, and will change. - -## Compilation Architecture - -Compilation proceeds by succesive translation between the following representations: - -1. **Core Solidity**: The user-facing language with all syntactic features. Supports higher-order - functions, pattern matching, type classes, and modules. This is a superset of SAIL, with all - additional language constructs being defined in terms of desugaring passes (syntactic - transformations) into SAIL. - -1. **SAIL**: A minimal first-order intermediate representation. All syntactic sugar has been - removed. Type classes are resolved to concrete instances. Polymorphic functions are specialized - to monomorphic versions. Pattern matching is compiled to simple case trees. - -1. **Hull**: A low-level representation close to Yul. Retains algebraic data types (binary sums and - products) but otherwise resembles Yul. Hull code is translated directly to Yul, which is then - compiled to EVM bytecode. - -1. **Yul**: The existing [Yul](https://docs.soliditylang.org/en/v0.8.35-pre.1/yul.html) assembly - language currently used in solc. Core Solidity is designed in a way that allows the use of - alternative or additional representations at this level in the future. - -Each transformation step simplifies the language and moves closer to the EVM execution model. - -## Document Structure - -- **Compilation Pipeline**: Describes the compilation pipeline and how representations relate -- **SAIL**: Specifies the desugared intermediate representation -- **Core Solidity**: Specifies the user-facing language features -- **Hull**: Specifies the low-level IR before Yul emission - -## Status - -This is a research prototype. The language design is not stable. Features may be added, removed, or -changed. The implementation has known bugs and missing functionality. Do not use this for production -systems. diff --git a/doc/src/SUMMARY.md b/doc/src/SUMMARY.md deleted file mode 100644 index e65b340e..00000000 --- a/doc/src/SUMMARY.md +++ /dev/null @@ -1,24 +0,0 @@ -# The Core Solidity Language Reference - -[Introduction](README.md) - -- [SAIL](sail/README.md) - - [Syntax](sail/syntax.md) - - [Builtins](sail/builtins.md) - - [Variable Declaration and Assignment](sail/variable-declaration-and-assignment.md) - - [Functions](sail/functions.md) - - [Assembly Blocks](sail/assembly.md) - - [Datatypes](sail/datatypes.md) - - [Parametric Polymorphism](sail/parametric-polymorphism.md) - - [Typeclasses](sail/typeclasses.md) - - [Modules](sail/modules.md) - - [Type Inference](sail/type-inference.md) -- [Core Solidity](core/README.md) - - [Lambda Functions](core/lambda-functions.md) - - [Numeric Types](core/numeric-types.md) - - [Arithmetic](core/arithmetic.md) - - [Data Locations](core/data-locations.md) - - [ABI Encoding / Decoding](core/abi-encoding-decoding.md) - - [Contracts](core/contracts.md) -- [Hull](hull/README.md) -- [Compilation Pipeline](compilation-pipeline.md) diff --git a/doc/src/compilation-pipeline.md b/doc/src/compilation-pipeline.md deleted file mode 100644 index 67a034b2..00000000 --- a/doc/src/compilation-pipeline.md +++ /dev/null @@ -1 +0,0 @@ -# Compilation Pipeline diff --git a/doc/src/core/README.md b/doc/src/core/README.md deleted file mode 100644 index 788c088f..00000000 --- a/doc/src/core/README.md +++ /dev/null @@ -1 +0,0 @@ -# Core Solidity diff --git a/doc/src/core/abi-encoding-decoding.md b/doc/src/core/abi-encoding-decoding.md deleted file mode 100644 index 7cb128b9..00000000 --- a/doc/src/core/abi-encoding-decoding.md +++ /dev/null @@ -1 +0,0 @@ -# ABI Encoding / Decoding diff --git a/doc/src/core/arithmetic.md b/doc/src/core/arithmetic.md deleted file mode 100644 index 3989dee0..00000000 --- a/doc/src/core/arithmetic.md +++ /dev/null @@ -1 +0,0 @@ -# Arithmetic diff --git a/doc/src/core/contracts.md b/doc/src/core/contracts.md deleted file mode 100644 index 97404c22..00000000 --- a/doc/src/core/contracts.md +++ /dev/null @@ -1 +0,0 @@ -# Contracts diff --git a/doc/src/core/data-locations.md b/doc/src/core/data-locations.md deleted file mode 100644 index 2266a893..00000000 --- a/doc/src/core/data-locations.md +++ /dev/null @@ -1 +0,0 @@ -# Data Locations diff --git a/doc/src/core/lambda-functions.md b/doc/src/core/lambda-functions.md deleted file mode 100644 index 91bbc850..00000000 --- a/doc/src/core/lambda-functions.md +++ /dev/null @@ -1 +0,0 @@ -# Lambda Functions diff --git a/doc/src/core/numeric-types.md b/doc/src/core/numeric-types.md deleted file mode 100644 index 02eaf53e..00000000 --- a/doc/src/core/numeric-types.md +++ /dev/null @@ -1 +0,0 @@ -# Numeric Types diff --git a/doc/src/hull/README.md b/doc/src/hull/README.md deleted file mode 100644 index 2d326773..00000000 --- a/doc/src/hull/README.md +++ /dev/null @@ -1,256 +0,0 @@ -# Hull - -## Introduction - -The Hull language is an intermediate step before Yul generation. It is basically Yul with algebraic -types (sums/products) - -### Naming - -Hull was initially named Core, but once it was decided that the whole language should be called -"Core Solidity", it was renamed to Hull. - -## Abstract syntax - -See `src/Language/Hull.hs` - -### Types - -```haskell -data Type - = TWord - | TBool - | TPair Type Type -- binary product, e.g. (word * word) - | TSum Type Type -- binary sum, e.g. (unit + word) - | TSumN [Type] -- n-ary sum - | TFun [Type] Type - | TUnit - | TNamed String Type -- named type, e.g. Option{unit + word} -``` - -### Expressions - -```haskell -data Expr - = EWord Integer - | EBool Bool - | EVar Name - | EPair Expr Expr - | EFst Expr - | ESnd Expr - | EInl Type Expr - | EInr Type Expr - | EInK Int Type Expr - | ECall Name [Expr] - | EUnit -``` - -Notes: - -- `EInl/EInr` are binary sum constructors (injections) -- `EInK k` represents k-th injection for n-ary sum -- all injections are annotated with target type, so we have for example - `inr(42)` -- n-ary products not implemented yet, but planned (they are simpler than sums) - -### Statements - -``` -data Stmt - = SAssign Expr Expr - | SAlloc Name Type - | SExpr Expr - | SAssembly [YulStmt] - | SReturn Expr - | SComment String - | SBlock [Stmt] - | SMatch Type Expr [Alt] - | SFunction Name [Arg] Type [Stmt] - | SRevert String - -data Arg = TArg Name Type -data Alt = Alt Con Name Stmt -data Con = CInl | CInr | CInK Int -``` - -Notes: - -- there are no control constructs yet, except call/return/revert; this is mostly because the surface - language does not have them either -- using comments can lead to problems, since Solidity seems to have no nested comments -- for `YulStmt`, see `src/Language/Yul.hs` -- as in Yul, there are no statement separators - -### Contracts - -Right now a contract consists of a name and a list of statements. This is definitely a temporary -solution. - -``` -data Contract = Contract { ccName :: Name, ccStmts :: [Stmt] } -``` - -## Concrete Syntax - -See `src/Language/Hull/Parser.hs` - -Although Hull is not meant to be written manually, it has concrete syntax, mostly for diagnostic -purposes. - -``` -Block = "{" hullStmt* "}" -Contract = "contract" identifier -Stmt = "let" identifier ":" Type - | "return" Expr - | match "<" Type ">" Expr "with" "{" Alt* "}" - | "function" identifier "(" Args? ")" "->" Type Block - | "assembly" YulBlock - | "revert" StringLiteral - | Expr ":=" Expr - | Expr - -Args = identifier : Type ("," Args)? -Alt = Con identifier "=>" Stmt -Con = "inl" | "inr" | "in" "(" integer ")" - -Expr = Con "<" Type ">" PrimaryExpr - | Project PrimaryExpr - | PrimaryExpr - -PrimaryExpr - = integer - | "true" - | "false" - | Tuple - | identifier "(" ExprList ")" - | identifier -Tuple = "(" ExprList ")" -ExprList = (Expr (, Expr)*)? -``` - -### Examples - -#### Option - -``` -contract Option { - function main () -> word { - return maybe$Word(0, inr(42)) - } - function maybe$Word (n : word, o : Option{unit + word}) -> word { - match o with { - inl $alt => { // None - return n - } - inr $alt => { // Some[var_1] - let var_2 : word - var_2 := $alt - return var_2 - } - } - } -} -``` - -#### Enumeration type - -``` -contract RGB { - function fromEnum (c : Color{unit + (unit + unit)}) -> word { - // match c with - match c with { - inl $alt => { // R - return 4 - } - inr $alt => match $alt with { - inl $alt => { // G - return 2 - } - inr $alt => { // B - return 42 - } - } - } - } - function main () -> word { - return fromEnum(inr(inr(()))) - } -} -``` - -## Problems - -Type annotation are helpful for code generation and seem to be necessary for compression, but they -lead to rather verbose syntax, e.g. - -``` -data Food = Curry | Beans | Other -data CFood = Red[Food] | Green[Food] | Nocolor - - function fromEnum(x : Food) { - match x { - | Curry => return 1; - | Beans => return 2; - | Other => return 3; - }; - } - - -contract Food { - function eat(x) { - match x { - | Red[f] => return f; - | Green[f] => return f; - | _ => Other; - }; - } - - function main() { - return fromEnum(eat(Green[Beans])); - } -} -``` - -yields the following Hull: - -``` -contract Food { - function eat (x : CFood{(Food{(unit + (unit + unit))} + (Food{(unit + (unit + unit))} + unit))}) -> Food{(unit + (unit + unit))} { - match x with { - inl $alt => { // Red[var_8] - let var_9 : Food{(unit + (unit + unit))} - var_9 := $alt - return var_9 - } - inr $alt => match<(Food{(unit + (unit + unit))} + unit)> $alt with { - inl $alt => { // Green[var_5] - let var_6 : Food{(unit + (unit + unit))} - var_6 := $alt - return var_6 - } - inr $alt => revert "no match for: Nocolor" - } - } - } - function fromEnum (x : Food{(unit + (unit + unit))}) -> word { - match x with { - inl $alt => { // Curry - return 1 - } - inr $alt => match<(unit + unit)> $alt with { - inl $alt => { // Beans - return 2 - } - inr $alt => { // Other - return 3 - } - } - } - } - function main () -> word { - return fromEnum(eat(inr(inl<(Food{(unit + (unit + unit))} + unit)>(inr(inl<(unit + unit)>(())))))) - } -} -``` - -On the other programs are not really meant to be read by humans. diff --git a/doc/src/sail/README.md b/doc/src/sail/README.md deleted file mode 100644 index f0ab39c8..00000000 --- a/doc/src/sail/README.md +++ /dev/null @@ -1 +0,0 @@ -# SAIL diff --git a/doc/src/sail/assembly.md b/doc/src/sail/assembly.md deleted file mode 100644 index 063e977f..00000000 --- a/doc/src/sail/assembly.md +++ /dev/null @@ -1 +0,0 @@ -# Assembly Blocks diff --git a/doc/src/sail/builtins.md b/doc/src/sail/builtins.md deleted file mode 100644 index d84e8040..00000000 --- a/doc/src/sail/builtins.md +++ /dev/null @@ -1 +0,0 @@ -# Builtins diff --git a/doc/src/sail/datatypes.md b/doc/src/sail/datatypes.md deleted file mode 100644 index 8a9dcef0..00000000 --- a/doc/src/sail/datatypes.md +++ /dev/null @@ -1 +0,0 @@ -# Datatypes diff --git a/doc/src/sail/functions.md b/doc/src/sail/functions.md deleted file mode 100644 index 0c5faf50..00000000 --- a/doc/src/sail/functions.md +++ /dev/null @@ -1 +0,0 @@ -# Functions diff --git a/doc/src/sail/modules.md b/doc/src/sail/modules.md deleted file mode 100644 index a55ecc05..00000000 --- a/doc/src/sail/modules.md +++ /dev/null @@ -1 +0,0 @@ -# Modules diff --git a/doc/src/sail/parametric-polymorphism.md b/doc/src/sail/parametric-polymorphism.md deleted file mode 100644 index 0118b7ed..00000000 --- a/doc/src/sail/parametric-polymorphism.md +++ /dev/null @@ -1 +0,0 @@ -# Parametric Polymorphism diff --git a/doc/src/sail/syntax.md b/doc/src/sail/syntax.md deleted file mode 100644 index 10d24690..00000000 --- a/doc/src/sail/syntax.md +++ /dev/null @@ -1 +0,0 @@ -# Syntax diff --git a/doc/src/sail/type-inference.md b/doc/src/sail/type-inference.md deleted file mode 100644 index 5496909e..00000000 --- a/doc/src/sail/type-inference.md +++ /dev/null @@ -1 +0,0 @@ -# Type Inference diff --git a/doc/src/sail/typeclasses.md b/doc/src/sail/typeclasses.md deleted file mode 100644 index ff847dd4..00000000 --- a/doc/src/sail/typeclasses.md +++ /dev/null @@ -1 +0,0 @@ -# Typeclasses diff --git a/doc/src/sail/variable-declaration-and-assignment.md b/doc/src/sail/variable-declaration-and-assignment.md deleted file mode 100644 index e17882d7..00000000 --- a/doc/src/sail/variable-declaration-and-assignment.md +++ /dev/null @@ -1 +0,0 @@ -# Variable Declaration and Assignment diff --git a/sol-core.cabal b/sol-core.cabal index 110f30c3..57170b3f 100644 --- a/sol-core.cabal +++ b/sol-core.cabal @@ -64,10 +64,10 @@ library Solcore.Backend.Mast Solcore.Backend.MastEval Solcore.Backend.Specialise + Solcore.Desugarer.DecisionTreeCompiler Solcore.Desugarer.FieldAccess Solcore.Desugarer.IfDesugarer Solcore.Desugarer.IndirectCall - Solcore.Desugarer.MatchCompiler Solcore.Desugarer.ReplaceWildcard Solcore.Desugarer.ContractDispatch Solcore.Desugarer.ReplaceFunTypeArgs @@ -160,6 +160,7 @@ test-suite sol-core-tests -- cabal-fmt: expand test -Main other-modules: Cases + MatchCompilerTests build-depends: , sol-core diff --git a/src/Solcore/Backend/EmitHull.hs b/src/Solcore/Backend/EmitHull.hs index 696a4d0a..dd1e3619 100644 --- a/src/Solcore/Backend/EmitHull.hs +++ b/src/Solcore/Backend/EmitHull.hs @@ -304,7 +304,12 @@ emitStmt (MastAsm as) = do -- an alternative might be to painstakingly rename all vars in the the assembly block subst <- gets ecSubst let yvars = getNames as - let unrolled = [Hull.SAssign (Hull.EVar (show v)) e | (v, e) <- Map.toList subst, Set.member v yvars] + let unrolled = + concat + [ [Hull.SAlloc (show v) Hull.TWord, Hull.SAssign (Hull.EVar (show v)) e] + | (v, e) <- Map.toList subst, + Set.member v yvars + ] pure $ unrolled ++ [Hull.SAssembly as] emitStmts :: [MastStmt] -> EM [Hull.Stmt] diff --git a/src/Solcore/Desugarer/DecisionTreeCompiler.hs b/src/Solcore/Desugarer/DecisionTreeCompiler.hs new file mode 100644 index 00000000..54e2bdd8 --- /dev/null +++ b/src/Solcore/Desugarer/DecisionTreeCompiler.hs @@ -0,0 +1,811 @@ +module Solcore.Desugarer.DecisionTreeCompiler where + +import Control.Monad +import Control.Monad.Except +import Control.Monad.Reader +import Control.Monad.State +import Control.Monad.Writer +import Data.Generics (everywhere, extT, mkT) +import Data.List +import Data.Map (Map) +import Data.Map qualified as Map +import Data.Maybe +import Data.Ord (comparing) +import Language.Yul (YulExp (..)) +import Solcore.Frontend.Pretty.SolcorePretty +import Solcore.Frontend.Syntax +import Solcore.Frontend.TypeInference.Id +import Solcore.Primitives.Primitives + +-- main function for pattern compilation + +matchCompiler :: CompUnit Id -> IO (Either String (CompUnit Id, [Warning])) +matchCompiler cunit = + do + result <- runCompilerM (initialTypeEnv cunit) (compile cunit) + case result of + Left err -> pure $ Left err + Right (unit', warns) -> do + let (nonExaustive, redundant) = partition isNonExaustive warns + if null nonExaustive + then + pure $ Right (unit', redundant) + else pure $ Left $ unlines $ map showWarning nonExaustive + +-- type class for the defining the pattern matching compilation +-- over the syntax tree + +class Compile a where + compile :: a -> CompilerM a + +instance (Compile a) => Compile [a] where + compile = mapM compile + +instance (Compile a) => Compile (Maybe a) where + compile Nothing = pure Nothing + compile (Just x) = Just <$> compile x + +instance Compile (CompUnit Id) where + compile (CompUnit imps ds) = + CompUnit imps <$> compile ds + +instance Compile (TopDecl Id) where + compile (TContr c) = + TContr <$> compile c + compile (TFunDef f) = + TFunDef <$> compile f + compile (TInstDef d) = + TInstDef <$> compile d + compile (TMutualDef ds) = + TMutualDef <$> compile ds + compile d = pure d + +instance Compile (Contract Id) where + compile (Contract n vs ds) = + Contract n vs + <$> local (\(te, ctx) -> (Map.union env' te, ctx ++ ["contract " ++ pretty n])) (compile ds) + where + ds' = [d | (CDataDecl d) <- ds] + env' = foldr addDataTyInfo Map.empty ds' + +instance Compile (ContractDecl Id) where + compile (CFunDecl d) = + CFunDecl <$> compile d + compile (CMutualDecl ds) = + CMutualDecl <$> compile ds + compile (CConstrDecl c) = + CConstrDecl <$> compile c + compile d = pure d + +instance Compile (Constructor Id) where + compile (Constructor ps bd) = + Constructor ps <$> compile bd + +instance Compile (FunDef Id) where + compile (FunDef sig bd) = + FunDef sig <$> pushCtx ("function " ++ pretty (sigName sig)) (compile bd) + +instance Compile (Stmt Id) where + compile (e1 := e2) = + (:=) <$> compile e1 <*> compile e2 + compile (Let v mt me) = + Let v mt <$> compile me + compile (StmtExp e) = + StmtExp <$> compile e + compile (Return e) = + Return <$> compile e + compile (If e1 bd1 bd2) = + If <$> compile e1 <*> compile bd1 <*> compile bd2 + compile s@(Asm _) = + pure s + compile (Match es eqns) = do + es' <- compile es + eqns' <- mapM compileEqn eqns + scrutTys <- mapM scrutineeType es' + let occs = [[i] | i <- [0 .. length es' - 1]] + occMap = Map.fromList (zip occs es') + matrix = map fst eqns' + actions = map snd eqns' + bacts = [([], a) | a <- actions] + matchDesc = "match (" ++ intercalate ", " (map pretty es') ++ ")" + pushCtx matchDesc $ do + ctx <- askWarnCtx + checkRedundancy ctx scrutTys matrix bacts + tree <- pushCtx matchDesc $ compileMatrix scrutTys occs matrix bacts + treeToStmt occMap tree + +compileEqn :: Equation Id -> CompilerM (Equation Id) +compileEqn (pats, stmts) = (pats,) <$> compile stmts + +compileMatrix :: + [Ty] -> + [Occurrence] -> + PatternMatrix -> + [BoundAction] -> + CompilerM DecisionTree +compileMatrix tys _ [] _ = do + pats <- mapM freshPat tys + ctx <- askWarnCtx + unless (null pats) $ tell [NonExhaustive ctx pats] + pure Fail +compileMatrix _tys occs (firstRow : _restRows) ((firstBinds, firstAct) : _restBacts) + | all isVarPat firstRow = do + let varBinds = [(v, occ) | (PVar v, occ) <- zip firstRow occs] + pure (Leaf (firstBinds ++ varBinds) firstAct) +compileMatrix tys occs matrix bacts = do + let col = selectColumn occs matrix + matrix' = map (reorderList col) matrix + occs' = reorderList col occs + tys' = reorderList col tys + case (tys', occs', matrix') of + (testTy : restTys, testOcc : restOccs, _) -> do + let firstCol = [p | (p : _) <- matrix'] + headCons = nub (mapMaybe patHeadCon firstCol) + headLits = nub (mapMaybe patHeadLit firstCol) + case (headCons, headLits) of + (c : cs, _) -> + buildConSwitch testOcc restOccs testTy restTys matrix' bacts (c : cs) + ([], ls@(_ : _)) -> + buildLitSwitch testOcc restOccs testTy restTys matrix' bacts ls + ([], []) -> + -- All wildcards after reordering: strip column and continue + compileMatrix restTys restOccs (defaultMatrix matrix') (defaultBoundActs testOcc matrix' bacts) + -- Unreachable: tys, occs, and matrix are parallel and all non-empty here + _ -> pure Fail + +buildConSwitch :: + Occurrence -> + [Occurrence] -> + Ty -> + [Ty] -> + PatternMatrix -> + [BoundAction] -> + [Id] -> + CompilerM DecisionTree +buildConSwitch testOcc restOccs _testTy restTys matrix bacts headCons = do + branches <- mapM buildBranch headCons + complete <- isComplete headCons + mDefault <- + if complete + then pure Nothing + else buildDefault + pure (Switch testOcc branches mDefault) + where + buildBranch k = do + info <- lookupConInfo (idName k) + let fieldTys = conFieldTypes info + newOccs = childOccs testOcc (length fieldTys) ++ restOccs + newTys = fieldTys ++ restTys + specBacts = specializedBoundActs k testOcc matrix bacts + rawPats = case [ps | (PCon k' ps : _) <- matrix, idName k' == idName k] of + (ps : _) -> ps + [] -> [] + -- Ensure srcPats are all PVar: PCon sub-patterns get a fresh variable + -- so conBranchToEqn can extend the occMap for child occurrences. + srcPats <- mapM ensureVar rawPats + specMat <- specialize k fieldTys matrix + subTree <- compileMatrix newTys newOccs specMat specBacts + pure (k, srcPats, subTree) + + -- Replace non-PVar patterns with fresh variables so that conBranchToEqn + -- can always extend the occMap for every child occurrence. + ensureVar p@(PVar _) = pure p + ensureVar p = freshPat (patTy p) + + patTy :: Pattern -> Ty + patTy (PVar i) = idType i + patTy (PCon k _) = snd (splitTy (idType k)) + patTy _ = word + + buildDefault = + let defMat = defaultMatrix matrix + defBacts = defaultBoundActs testOcc matrix bacts + in if null defMat + then do + witPats <- case headCons of + [] -> mapM freshPat restTys + (first : _) -> do + siblings <- siblingConstructors first + let headNames = map idName headCons + missing = filter (\s -> idName s `notElem` headNames) siblings + case missing of + (k : _) -> do + info <- lookupConInfo (idName k) + fieldPats <- mapM freshPat (conFieldTypes info) + restWit <- mapM freshPat restTys + pure (PCon k fieldPats : restWit) + [] -> mapM freshPat restTys + ctx <- askWarnCtx + tell [NonExhaustive ctx witPats] + pure (Just Fail) + else Just <$> compileMatrix restTys restOccs defMat defBacts + +buildLitSwitch :: + Occurrence -> + [Occurrence] -> + Ty -> + [Ty] -> + PatternMatrix -> + [BoundAction] -> + [Literal] -> + CompilerM DecisionTree +buildLitSwitch testOcc restOccs testTy restTys matrix bacts headLits = do + branches <- mapM buildBranch headLits + let defMat = defaultMatrix matrix + defBacts = defaultBoundActs testOcc matrix bacts + mDefault <- + if null defMat + then do + litWit <- freshPat testTy + restWit <- mapM freshPat restTys + ctx <- askWarnCtx + tell [NonExhaustive ctx (litWit : restWit)] + pure (Just Fail) + else Just <$> compileMatrix restTys restOccs defMat defBacts + pure (LitSwitch testOcc branches mDefault) + where + buildBranch lit = do + let specMat = specializeLit lit matrix + specBacts = litSpecializedBoundActs lit testOcc matrix bacts + (lit,) <$> compileMatrix restTys restOccs specMat specBacts + +instance Compile (Exp Id) where + compile v@(Var _) = + pure v + compile (Con c es) = + Con c <$> compile es + compile (FieldAccess me n) = + flip FieldAccess n <$> compile me + compile l@(Lit _) = + pure l + compile (Call me f es) = + Call <$> compile me <*> pure f <*> compile es + compile (Lam ps bd mt) = + Lam ps <$> pushCtx ("lambda (" ++ intercalate ", " (map pretty ps) ++ ")") (compile bd) <*> pure mt + compile (TyExp e t) = + flip TyExp t <$> compile e + compile (Cond e1 e2 e3) = + Cond <$> compile e1 <*> compile e2 <*> compile e3 + compile (Indexed e1 e2) = + Indexed <$> compile e1 <*> compile e2 + +instance Compile (Instance Id) where + compile (Instance d vs ps n ts t funs) = + Instance d vs ps n ts t + <$> pushCtx ("instance " ++ pretty t ++ " : " ++ pretty n) (compile funs) + +-- compiling a decision tree into a match + +-- Convert a decision tree to a statement body (list of statements). +-- Avoids wrapping multi-statement leaves in a fake Match node. +treeToBody :: OccMap -> DecisionTree -> CompilerM [Stmt Id] +treeToBody _ Fail = pure [] +treeToBody occMap (Leaf varBinds stmts) = do + subst <- buildSubst occMap varBinds + pure (map (substStmt subst) stmts) +treeToBody occMap tree = (: []) <$> treeToStmt occMap tree + +treeToStmt :: OccMap -> DecisionTree -> CompilerM (Stmt Id) +treeToStmt _ Fail = pure (Match [] []) +treeToStmt occMap (Leaf varBinds stmts) = do + subst <- buildSubst occMap varBinds + case map (substStmt subst) stmts of + [s] -> pure s + ss -> pure (Match [] [([], ss)]) +treeToStmt occMap (Switch occ branches mDef) = do + scrutinee <- occToExp occMap occ + eqns <- mapM (conBranchToEqn occMap occ) branches + defEqns <- case mDef of + Nothing -> pure [] + Just def -> do + body <- treeToBody occMap def + ty <- scrutineeType scrutinee + v <- freshPat ty + pure [([v], body)] + pure (Match [scrutinee] (eqns ++ defEqns)) +treeToStmt occMap (LitSwitch occ branches mDef) = do + scrutinee <- occToExp occMap occ + eqns <- mapM (litBranchToEqn occMap) branches + defEqns <- case mDef of + Nothing -> pure [] + Just def -> do + body <- treeToBody occMap def + ty <- scrutineeType scrutinee + v <- freshPat ty + pure [([v], body)] + pure (Match [scrutinee] (eqns ++ defEqns)) + +-- Build a substitution map from pattern variables to their occurrence expressions. +buildSubst :: OccMap -> [(Id, Occurrence)] -> CompilerM (Map Id (Exp Id)) +buildSubst occMap varBinds = do + pairs <- mapM (\(v, occ) -> (v,) <$> occToExp occMap occ) varBinds + pure (Map.fromList pairs) + +-- Substitute pattern variables in a statement using the given map. +-- Also substitutes YIdent names inside inline assembly blocks. +substStmt :: Map Id (Exp Id) -> Stmt Id -> Stmt Id +substStmt subst = everywhere (mkT goExp `extT` goYul) + where + goExp e@(Var v) = Map.findWithDefault e v subst + goExp e = e + goYul :: YulExp -> YulExp + goYul e@(YIdent n) = + case [v | (k, Var v) <- Map.toList subst, idName k == n] of + (v : _) -> YIdent (idName v) + [] -> e + goYul e = e + +occToExp :: OccMap -> Occurrence -> CompilerM (Exp Id) +occToExp occMap occ = + case Map.lookup occ occMap of + Just e -> pure e + Nothing -> throwError ("PANIC! occToExp: occurrence " ++ show occ ++ " not in map") + +conBranchToEqn :: OccMap -> Occurrence -> (Id, [Pattern], DecisionTree) -> CompilerM (PatternRow, Action) +conBranchToEqn occMap occ (k, srcPats, tree) = do + let childOccs' = [occ ++ [j] | j <- [0 .. length srcPats - 1]] + childExps = [Var fv | (PVar fv) <- srcPats] + occMap' = Map.union (Map.fromList (zip childOccs' childExps)) occMap + body <- treeToBody occMap' tree + pure ([PCon k srcPats], body) + +litBranchToEqn :: OccMap -> (Literal, DecisionTree) -> CompilerM (PatternRow, Action) +litBranchToEqn occMap (lit, tree) = do + body <- treeToBody occMap tree + pure ([PLit lit], body) + +-- definition of a monad + +-- Context attached to warnings: stack of pretty-printed descriptions of the +-- syntax nodes being traversed, from outermost to innermost. +type WarnCtx = [String] + +type CompilerM a = + ReaderT (TypeEnv, WarnCtx) (ExceptT String (WriterT [Warning] (StateT Int IO))) a + +runCompilerM :: TypeEnv -> CompilerM a -> IO (Either String (a, [Warning])) +runCompilerM env m = + do + ((r, ws), _) <- runStateT (runWriterT (runExceptT (runReaderT m (env, [])))) 0 + case r of + Left err -> pure $ Left err + Right t -> pure $ Right (t, ws) + +askTypeEnv :: CompilerM TypeEnv +askTypeEnv = asks fst + +askWarnCtx :: CompilerM WarnCtx +askWarnCtx = asks snd + +pushCtx :: String -> CompilerM a -> CompilerM a +pushCtx s = local (\(te, ctx) -> (te, ctx ++ [s])) + +lookupConInfo :: Name -> CompilerM ConInfo +lookupConInfo k = do + env <- askTypeEnv + case Map.lookup k env of + Just info -> pure info + Nothing -> undefinedConstructorError k + +siblingConstructors :: Id -> CompilerM [Id] +siblingConstructors k = do + env <- askTypeEnv + info <- lookupConInfo (idName k) + let rt = conReturnType info + pure [idFromInfo kid ci | (kid, ci) <- Map.toList env, conReturnType ci == rt] + +idFromInfo :: Name -> ConInfo -> Id +idFromInfo n info = + Id + n + ( funtype + (conFieldTypes info) + (conReturnType info) + ) + +inc :: CompilerM Int +inc = do + n <- get + put (n + 1) + pure n + +freshPat :: Ty -> CompilerM (Pat Id) +freshPat t = do + n <- inc + let v = Name $ "$v" ++ show n + pure (PVar (Id v t)) + +isComplete :: [Id] -> CompilerM Bool +isComplete [] = pure False +isComplete ks@(first : _) = do + siblings <- siblingConstructors first + let siblingNames = map idName siblings + ksNames = map idName ks + pure (null (siblingNames \\ ksNames)) + +-- some types used by the algorithm + +type Occurrence = [Int] + +type OccMap = Map Occurrence (Exp Id) + +type Action = [Stmt Id] + +-- Per-row accumulated bindings (var → occurrence) collected as PVar patterns +-- are consumed by specialization steps, paired with the row's action. +type BoundAction = ([(Id, Occurrence)], Action) + +type Pattern = Pat Id + +type PatternRow = [Pattern] + +type PatternMatrix = [PatternRow] + +data DecisionTree + = Leaf [(Id, Occurrence)] Action -- var-occ bindings to substitute before running action + | Fail + | Switch Occurrence [(Id, [Pattern], DecisionTree)] (Maybe DecisionTree) + | LitSwitch Occurrence [(Literal, DecisionTree)] (Maybe DecisionTree) + deriving (Eq, Show) + +-- data constructor information and environment + +type TypeEnv = Map Name ConInfo + +data ConInfo + = ConInfo + { conFieldTypes :: [Ty], + conReturnType :: Ty + } + deriving (Show) + +initialTypeEnv :: CompUnit Id -> TypeEnv +initialTypeEnv (CompUnit _ ds) = + foldr step primEnv ds + where + step (TDataDef dt) ac = addDataTyInfo dt ac + step (TMutualDef ds1) ac = foldr step ac ds1 + step _ ac = ac + +primEnv :: TypeEnv +primEnv = + Map.fromList + [ (unitName, unitConInfo), + (pairName, pairConInfo), + (inlName, inlConInfo), + (inrName, inrConInfo), + (trueName, trueConInfo), + (falseName, falseConInfo) + ] + +unitName :: Name +unitName = Name "()" + +unitConInfo :: ConInfo +unitConInfo = ConInfo [] unit + +pairName :: Name +pairName = Name "pair" + +pairConInfo :: ConInfo +pairConInfo = ConInfo [at, bt] (pair at bt) + +inlConInfo :: ConInfo +inlConInfo = ConInfo [at] (sumTy at bt) + +inrConInfo :: ConInfo +inrConInfo = ConInfo [bt] (sumTy at bt) + +trueConInfo :: ConInfo +trueConInfo = ConInfo [] boolTy + +falseConInfo :: ConInfo +falseConInfo = ConInfo [] boolTy + +addDataTyInfo :: DataTy -> TypeEnv -> TypeEnv +addDataTyInfo (DataTy n vs cons) env = + foldr (addConstructor res) env cons + where + res = TyCon n (map TyVar vs) + +addConstructor :: Ty -> Constr -> TypeEnv -> TypeEnv +addConstructor ty (Constr n ts) = + Map.insert n (ConInfo ts ty) + +-- matrix specialization + +specialize :: Id -> [Ty] -> PatternMatrix -> CompilerM PatternMatrix +specialize k fieldTys matrix = + do + pats <- mapM freshPat fieldTys + pure $ mapMaybe (specRow k pats) matrix + +specRow :: Id -> [Pattern] -> PatternRow -> Maybe PatternRow +specRow _ _ [] = Nothing +specRow k pats (p : rest) = + case p of + PCon k' ps + | idName k' == idName k -> Just (ps ++ rest) + | otherwise -> Nothing + PVar _ -> Just (pats ++ rest) + PLit _ -> Nothing + _ -> error "PANIC! Found wildcard in specRow" + +specializeLit :: Literal -> PatternMatrix -> PatternMatrix +specializeLit lit = mapMaybe specLitRow + where + specLitRow [] = Nothing + specLitRow (p : rest) = + case p of + PLit l + | l == lit -> Just rest + | otherwise -> Nothing + PVar _ -> Just rest + PCon _ _ -> Nothing + _ -> error "PANIC! Found wildcard in specializeLit" + +-- matrix definitions + +defaultMatrix :: PatternMatrix -> PatternMatrix +defaultMatrix = concatMap defaultRow + where + defaultRow [] = [] + defaultRow (p : rest) = + case p of + PVar _ -> [rest] + PCon _ _ -> [] + PLit _ -> [] + _ -> error "PANIC! Found wildcard in defaultMatrix" + +specializedBoundActs :: Id -> Occurrence -> PatternMatrix -> [BoundAction] -> [BoundAction] +specializedBoundActs k testOcc rows bacts = + [ (addVarBinding row binds, a) + | (row, (binds, a)) <- zip rows bacts, + rowMatchesCon row + ] + where + rowMatchesCon [] = False + rowMatchesCon (p : _) = case p of + PCon k' _ -> idName k' == idName k + PVar _ -> True + PLit _ -> False + PWildcard -> error "PANIC! Found wildcard in specializedBoundActs" + addVarBinding (PVar v : _) binds = binds ++ [(v, testOcc)] + addVarBinding _ binds = binds + +defaultBoundActs :: Occurrence -> PatternMatrix -> [BoundAction] -> [BoundAction] +defaultBoundActs testOcc rows bacts = + [ (addVarBinding row binds, a) + | (row, (binds, a)) <- zip rows bacts, + case row of + (p : _) -> isVarPat p + [] -> False + ] + where + addVarBinding (PVar v : _) binds = binds ++ [(v, testOcc)] + addVarBinding _ binds = binds + +litSpecializedBoundActs :: Literal -> Occurrence -> PatternMatrix -> [BoundAction] -> [BoundAction] +litSpecializedBoundActs lit testOcc rows bacts = + [ (addVarBinding row binds, a) + | (row, (binds, a)) <- zip rows bacts, + rowMatchesLit row + ] + where + rowMatchesLit [] = False + rowMatchesLit (p : _) = case p of + PLit l -> l == lit + PVar _ -> True + _ -> False + addVarBinding (PVar v : _) binds = binds ++ [(v, testOcc)] + addVarBinding _ binds = binds + +-- column selection heuristic + +necessityScore :: [Pattern] -> Int +necessityScore = length . filter (not . isVarPat) + +selectColumn :: [Occurrence] -> PatternMatrix -> Int +selectColumn _ [] = 0 +selectColumn occs matrix = + case map necessityScore (transpose matrix) of + [] -> 0 + scores -> + let best = maximum scores + candidates = [i | (i, s) <- zip [0 ..] scores, s == best] + rank i = length (occs !! i) + in minimumBy (comparing rank) candidates + +reorderList :: Int -> [a] -> [a] +reorderList i xs = + let (before, after) = splitAt i xs + in case after of + [] -> xs + (x : rest) -> x : before ++ rest + +childOccs :: Occurrence -> Int -> [Occurrence] +childOccs occ n = [occ ++ [j] | j <- [0 .. n - 1]] + +-- auxiliar functions + +scrutineeType :: Exp Id -> CompilerM Ty +scrutineeType (Var i) = pure (idType i) +scrutineeType (Con i _) = pure (snd (splitTy (idType i))) +scrutineeType (Lit (IntLit _)) = pure word +scrutineeType (Lit (StrLit _)) = pure string +scrutineeType (Call _ i _) = pure (snd (splitTy (idType i))) +scrutineeType (Lam args _body (Just tb)) = pure (funtype (map typeOfParam args) tb) +scrutineeType (Lam _ _ Nothing) = + throwError + "scrutineeType: lambda scrutinee has no return-type annotation" +scrutineeType (Cond _ _ e) = scrutineeType e +scrutineeType (TyExp _ ty) = pure ty +scrutineeType (FieldAccess _ n) = pure (idType n) +scrutineeType (Indexed earr _) = + do + tarr <- scrutineeType earr + case tarr of + (_ :-> tres) -> pure tres + _ -> + throwError + "scrutineeType: index expression scrutinee has no type annotation" + +typeOfParam :: Param Id -> Ty +typeOfParam (Typed i _t) = idType i +typeOfParam (Untyped i) = idType i + +isVarPat :: Pattern -> Bool +isVarPat (PVar _) = True +isVarPat _ = False + +patHeadCon :: Pattern -> Maybe Id +patHeadCon (PCon k _) = Just k +patHeadCon _ = Nothing + +patHeadLit :: Pattern -> Maybe Literal +patHeadLit (PLit l) = Just l +patHeadLit _ = Nothing + +-- redundancy checking (pre-pass over the original matrix) + +-- checkRedundancy ctx tys matrix bacts emits RedundantClause warnings +-- for every row that is not useful w.r.t. all the rows above it. +checkRedundancy :: WarnCtx -> [Ty] -> PatternMatrix -> [BoundAction] -> CompilerM () +checkRedundancy ctx tys matrix bacts = go [] (zip matrix bacts) + where + go _ [] = pure () + go prefix ((row, (_, act)) : rest) = do + useful <- isUseful tys prefix row + unless useful $ tell [RedundantClause ctx row act] + go (prefix ++ [row]) rest + +-- Maranget's U(P, q): returns True iff row q adds new coverage that no +-- row in the prefix matrix P already handles. +isUseful :: [Ty] -> PatternMatrix -> PatternRow -> CompilerM Bool +isUseful _ [] _ = pure True +isUseful _ _ [] = pure False +isUseful tys matrix (q1 : qRest) = + case q1 of + PCon k ps -> do + info <- lookupConInfo (idName k) + let fieldTys = conFieldTypes info + specMat <- specialize k fieldTys matrix + isUseful (fieldTys ++ drop 1 tys) specMat (ps ++ qRest) + PLit l -> + isUseful (drop 1 tys) (specializeLit l matrix) qRest + PVar _ -> + case tys of + [] -> pure False + (_ : restTys) -> do + let headCons = nub (mapMaybe patHeadCon [p | (p : _) <- matrix]) + complete <- if null headCons then pure False else isComplete headCons + if complete + then fmap or $ forM headCons $ \k -> do + info <- lookupConInfo (idName k) + let fieldTys = conFieldTypes info + freshFields <- mapM freshPat fieldTys + specMat <- specialize k fieldTys matrix + isUseful (fieldTys ++ restTys) specMat (freshFields ++ qRest) + else + isUseful restTys (defaultMatrix matrix) qRest + _ -> pure True -- PWildcard shouldn't appear after desugaring + +-- inhabitance checking (used for exhaustiveness) + +inhabitsM :: PatternMatrix -> [Ty] -> CompilerM (Maybe [Pattern]) +inhabitsM [] tys = Just <$> mapM freshPat tys +inhabitsM _ [] = pure Nothing +inhabitsM matrix (ty : restTys) = do + let firstCol = [p | (p : _) <- matrix] + headCons = nub (mapMaybe patHeadCon firstCol) + headLits = nub (mapMaybe patHeadLit firstCol) + case (headCons, headLits) of + (cs@(_ : _), _) -> inhabitsConCol matrix ty restTys cs + ([], _ : _) -> inhabitsLitCol matrix ty restTys + ([], []) -> do + r <- inhabitsM (defaultMatrix matrix) restTys + case r of + Nothing -> pure Nothing + Just restWit -> do + v <- freshPat ty + pure (Just (v : restWit)) + +inhabitsConCol :: PatternMatrix -> Ty -> [Ty] -> [Id] -> CompilerM (Maybe [Pattern]) +inhabitsConCol matrix _ty restTys headCons = + case headCons of + [] -> pure Nothing + (first : _) -> do + siblings <- siblingConstructors first + let headNames = map idName headCons + missingCons = filter (\s -> idName s `notElem` headNames) siblings + case missingCons of + (k : _) -> do + info <- lookupConInfo (idName k) + let fieldTys = conFieldTypes info + mRestWit <- inhabitsM (defaultMatrix matrix) restTys + sub <- mapM freshPat fieldTys + case mRestWit of + Nothing -> + pure Nothing + Just restWit -> + pure (Just (PCon k sub : restWit)) + [] -> + fmap msum $ mapM checkCon headCons + where + checkCon k = do + info <- lookupConInfo (idName k) + let fieldTys = conFieldTypes info + newTys = fieldTys ++ restTys + specMat <- specialize k fieldTys matrix + mWit <- inhabitsM specMat newTys + case mWit of + Nothing -> pure Nothing + Just wit -> do + let (fieldWit, restWit) = splitAt (length fieldTys) wit + pure (Just (PCon k fieldWit : restWit)) + +inhabitsLitCol :: PatternMatrix -> Ty -> [Ty] -> CompilerM (Maybe [Pattern]) +inhabitsLitCol matrix ty restTys = do + r <- inhabitsM (defaultMatrix matrix) restTys + case r of + Nothing -> pure Nothing + Just restWit -> do + v <- freshPat ty + pure (Just (v : restWit)) + +-- warnings + +data Warning + = RedundantClause WarnCtx PatternRow Action + | NonExhaustive WarnCtx [Pattern] + deriving (Eq, Show) + +isNonExaustive :: Warning -> Bool +isNonExaustive (NonExhaustive _ _) = True +isNonExaustive _ = False + +-- Pretty-print a warning + +showWarning :: Warning -> String +showWarning (RedundantClause ctx row blk) = + unwords ["Warning: Clause ", "(", pretty (row, blk), ") is redundant.", showWarnCtx ctx] +showWarning (NonExhaustive ctx pats) = + unwords ["Non-exhaustive pattern match. Missing case:", showRow $ nub pats, showWarnCtx ctx] + +showWarnCtx :: WarnCtx -> String +showWarnCtx [] = "" +showWarnCtx ctx = "\n in " ++ intercalate "\n in " (reverse ctx) + +showRow :: [Pattern] -> String +showRow = intercalate ", " . map pretty + +-- error messages + +undefinedConstructorError :: Name -> CompilerM a +undefinedConstructorError n = + throwError $ + unlines + [ "PANIC!", + "Constructor:" ++ pretty n, + "is not defined!" + ] diff --git a/src/Solcore/Desugarer/MatchCompiler.hs b/src/Solcore/Desugarer/MatchCompiler.hs deleted file mode 100644 index e2ca7607..00000000 --- a/src/Solcore/Desugarer/MatchCompiler.hs +++ /dev/null @@ -1,636 +0,0 @@ -module Solcore.Desugarer.MatchCompiler where - -import Control.Monad.Except -import Control.Monad.Reader -import Control.Monad.State -import Control.Monad.Writer -import Data.Either -import Data.List -import Data.List.NonEmpty qualified as L -import Language.Yul -import Solcore.Frontend.Syntax -import Solcore.Frontend.TypeInference.Id -import Solcore.Primitives.Primitives - -{- - Pattern matching compilation - ============================ - - This module implements the strategy to compile - complex pattern matching into simple over just - one pattern. Such structure can be used - for code generation. - - We follow the algorithm by Augustsson in: -https://link.springer.com/content/pdf/10.1007/3-540-15975-4_48.pdf - - -} - --- top level interface for the compiler - -matchCompiler :: CompUnit Id -> IO (Either String (CompUnit Id)) -matchCompiler (CompUnit imps ds) = - do - res <- mapM matchCompilerDecl (zip [0 ..] ds) - case partitionEithers res of - ([], cons') -> return $ Right $ CompUnit imps (concat cons') - (errs, _) -> return $ Left $ unlines errs - -matchCompilerDecl :: (Int, TopDecl Id) -> IO (Either String [TopDecl Id]) -matchCompilerDecl (_, TContr (Contract n vs ds)) = - do - res <- runCompilerM [n] (mapM compile ds) - case res of - (Left err, _) -> return $ Left err - (Right ds', fs) -> return $ Right [TContr (Contract n vs (ds' ++ map CFunDecl fs))] -matchCompilerDecl (i, d) = - do - let n = Name ("Global" ++ show i) - res <- runCompilerM [n] (compile d) - case res of - (Left err, _) -> return $ Left err - (Right ds', fs) -> - return $ Right (ds' : map TFunDef fs) - -class Compile a where - type Res a - compile :: a -> CompilerM (Res a) - -instance (Compile a) => Compile [a] where - type Res [a] = [Res a] - compile = mapM compile - -instance (Compile a) => Compile (Maybe a) where - type Res (Maybe a) = Maybe (Res a) - compile Nothing = return Nothing - compile (Just e) = Just <$> compile e - -instance Compile (TopDecl Id) where - type Res (TopDecl Id) = TopDecl Id - compile (TInstDef inst) = - TInstDef <$> compile inst - compile (TFunDef fun) = - TFunDef <$> compile fun - compile (TMutualDef ts) = - TMutualDef <$> compile ts - compile d = return d - -instance Compile (ContractDecl Id) where - type Res (ContractDecl Id) = ContractDecl Id - compile (CFunDecl fun) = - CFunDecl <$> compile fun - compile (CConstrDecl con) = - CConstrDecl <$> compile con - compile (CMutualDecl cs) = - CMutualDecl <$> compile cs - compile d = return d - -instance Compile (Instance Id) where - type Res (Instance Id) = Instance Id - compile (Instance d vs ps n ts m funs) = - Instance d vs ps n ts m <$> compile funs - -instance Compile (FunDef Id) where - type Res (FunDef Id) = FunDef Id - compile (FunDef sig bd) = - do - let n = sigName sig - bd' <- - local - (\ns -> ns ++ "_" ++ show n) - (compile bd) - return (FunDef sig (concat bd')) - -instance Compile (Constructor Id) where - type Res (Constructor Id) = Constructor Id - compile (Constructor ps bd) = - (Constructor ps . concat) <$> compile bd - -instance Compile (Stmt Id) where - type Res (Stmt Id) = [Stmt Id] - - compile (lhs := rhs) = - do - lhs' <- compile lhs - rhs' <- compile rhs - pure [lhs' := rhs'] - compile (Let v mt me) = - do - me' <- compile me - pure [Let v mt me'] - compile (StmtExp e) = - do - e' <- compile e - pure [StmtExp e'] - compile (Return e) = - do - e' <- compile e - pure [Return e'] - compile (Match es eqns) = - do - v <- matchError - let def = [StmtExp $ generateCall v [errorLit]] - matchCompilerM es def eqns - compile (If e blk1 blk2) = - do - blk1' <- compile blk1 - blk2' <- compile blk2 - pure [If e (concat blk1') (concat blk2')] - compile s = return [s] - -instance Compile (Exp Id) where - type Res (Exp Id) = Exp Id - - compile (Var v) = - pure (Var v) - compile (Con v es) = - Con v <$> compile es - compile (FieldAccess me v) = - flip FieldAccess v <$> compile me - compile (Call me v es) = - do - me' <- compile me - es' <- compile es - pure (Call me' v es') - compile (TyExp e ty) = - flip TyExp ty <$> compile e - compile (Cond e1 e2 e3) = - Cond <$> compile e1 <*> compile e2 <*> compile e3 - compile e = pure e - --- Algorithm main function - -matchCompilerM :: [Exp Id] -> [Stmt Id] -> Equations Id -> CompilerM [Stmt Id] --- first case: No remaining equations. We return the default body. -matchCompilerM _ d [] = do - return d --- second case: no scrutinee. Result is the body of the first equation. -matchCompilerM [] _ ((_, s1) : _) = do - return s1 -matchCompilerM es d eqns@(_ : _) - -- third case: all first patterns are variables - | allPatsStartsWithVars eqns = - thirdCase es d eqns - -- fourth case: constructors before variables (if any) - | hasConstrsBeforeVars eqns = - fourthCase es d eqns - -- fifth case: variable between two sets of constructors - | hasVarsBetweenConstrs eqns = - fifthCase es d eqns - | otherwise = - throwError "Panic! Impossible --- matchCompilerM" - --- Implementation of the third case. - -thirdCase :: [Exp Id] -> [Stmt Id] -> Equations Id -> CompilerM [Stmt Id] -thirdCase _ _ [] = - throwError "Panic! Impossible --- thirdCase." -thirdCase (e : es) d eqns = - do - Id n _ <- freshId - let vs = foldr (union . vars . L.head . L.fromList . fst) [] eqns - s = map (\vi -> (vi, n)) vs - eqns' = map (dropHeadPat s) eqns - t = typeOfExp e - res <- matchCompilerM es d eqns' - return (Let (Id n t) (Just t) (Just e) : res) - where - dropHeadPat :: Subst -> Equation Id -> Equation Id - dropHeadPat subst (_ : ps, ss) = (ps, apply subst ss) - dropHeadPat _ eqn = eqn -thirdCase [] _ _ = throwError "Panic! Impossible --- thirdCase with empty scrutinee." - -typeOfExp :: Exp Id -> Ty -typeOfExp (Var i) = idType i -typeOfExp (Con i []) = idType i -typeOfExp e@(Con i args) = go (idType i) args - where - go ty [] = ty - go (_ :-> u) (_ : as) = go u as - go _ _ = error $ "typeOfExp: " ++ show e -typeOfExp (Lit (IntLit _)) = word -- TyCon "Word" [] -typeOfExp (Call Nothing i _) = idType i -typeOfExp (Lam args _ (Just tb)) = funtype tas tb - where - tas = map paramTy args -typeOfExp e = error $ "typeOfExp: " ++ show e - -paramTy :: Param Id -> Ty -paramTy (Typed i _) = idType i -paramTy (Untyped i) = idType i - --- Implementation of the fourth case - -fourthCase :: [Exp Id] -> [Stmt Id] -> Equations Id -> CompilerM [Stmt Id] -fourthCase _ _ [] = - throwError "Panic! Impossible --- fourthCase." -fourthCase (e : es) d eqns = - do - let (cons, varEqns) = span isConstr eqns - cons' = sortBy compareConstr cons - defEqn <- eqnsForVars es d varEqns - let ss = stmtsFrom defEqn -- statements for the closest var match, - -- used for the default instruction semantics. - cons'' = groupByConstrHead cons' - conEqns <- mapM (eqnsForConstrs (e : es) d ss) cons'' - return [Match [e] (conEqns ++ defEqn)] - where - stmtsFrom [] = [] - stmtsFrom ((_, ss) : _) = ss -fourthCase [] _ _ = throwError "Panic! Impossible --- fourthCase with empty scrutinee." - -groupByConstrHead :: Equations Id -> [Equations Id] -groupByConstrHead = groupBy (\c c' -> compareConstr c c' == EQ) - -compareConstr :: Equation Id -> Equation Id -> Ordering -compareConstr ((PCon (Id n _) _) : _, _) ((PCon (Id n' _) _) : _, _) = - compare n n' -compareConstr _ _ = EQ - --- implementation of the fifth case - -fifthCase :: [Exp Id] -> [Stmt Id] -> Equations Id -> CompilerM [Stmt Id] -fifthCase [] _ [] = - throwError "Panic! Impossible --- fifthCase" -fifthCase es@(_ : _) d eqns@(_ : _) = - do - let eqnss = reverse $ splits isConstr eqns - case unsnoc eqnss of - Just (eqnGroups, tailEqns) -> do - d' <- generateFunctions es d eqnGroups - r <- matchCompilerM es d' tailEqns - addDefaultCase d' r - Nothing -> throwError "Panic! Impossible --- fifthCase" -fifthCase _ _ _ = throwError "Panic! Impossible --- fifthCase invalid inputs." - -addDefaultCase :: [Stmt Id] -> [Stmt Id] -> CompilerM [Stmt Id] -addDefaultCase _ [] = pure [] -addDefaultCase d [Match es eqn] = - do - pv <- freshPVar - pure [Match es (eqn ++ [([pv], d)])] -addDefaultCase _ [s] = pure [s] -addDefaultCase d (s : ss) = - do - ss' <- addDefaultCase d ss - pure (s : ss') - -hasVarsBetweenConstrs :: Equations Id -> Bool -hasVarsBetweenConstrs eqns = - length (splits isConstr eqns) >= 2 - -generateFunctions :: [Exp Id] -> [Stmt Id] -> [Equations Id] -> CompilerM [Stmt Id] -generateFunctions _ d [] = return d -generateFunctions es d (eqn : eqns) = - do - d' <- generateFunction es d eqn - generateFunctions es d' eqns - -generateFunction :: [Exp Id] -> [Stmt Id] -> Equations Id -> CompilerM [Stmt Id] -generateFunction es d eqn = - do - n <- newFunName - ss <- matchCompilerM es d eqn - let toParam paramId@(Id _ t) = Typed paramId t - vs = ids ss - let fd = FunDef (Signature [] [] n (map toParam vs) (Just (blockType ss))) ss - tell [fd] - v <- (TyVar . TVar) <$> freshName - return [StmtExp $ generateCall (Id n v) (Var <$> vs)] - -newFunName :: CompilerM Name -newFunName = - do - n <- inc - pre <- ask - return (Name $ "fun_" ++ pre ++ "_" ++ show n) - -eqnsForConstrs :: - [Exp Id] -> - [Stmt Id] -> - [Stmt Id] -> - Equations Id -> - CompilerM (Equation Id) -eqnsForConstrs (_ : es) d _ eqns@(((p : _), _) : _) = - do - (p', _, es') <- instantiatePat p - let eqns' = map dropHeadParam eqns - res <- matchCompilerM (es' ++ es) d eqns' - pure ([p'], res) -eqnsForConstrs _ _ _ _ = - throwError "Panic! Impossible --- eqnsForConstrs with invalid equations." - -dropHeadParam :: Equation Id -> Equation Id -dropHeadParam ((PCon _ ps' : ps), ss) = (ps' ++ ps, ss) -dropHeadParam x = x - -instantiatePat :: Pat Id -> CompilerM (Pat Id, [Pat Id], [Exp Id]) -instantiatePat p@(PLit _) = return (p, [], []) -instantiatePat p@(PVar _) = return (p, [], []) -instantiatePat PWildcard = return (PWildcard, [], []) -instantiatePat (PCon n ps) = - do - ns <- mapM (const freshName) ps - ts <- mapM tyFromPat ps - let vs = zipWith Id ns ts - return (PCon n (map PVar vs), ps, map Var vs) - -tyFromPat :: Pat Id -> CompilerM Ty -tyFromPat (PVar (Id _ t)) = pure t -tyFromPat (PLit _) = pure word -tyFromPat PWildcard = pure unit -tyFromPat (PCon (Id _ t) _) = - maybe err pure (retTy t) - where - err = throwError "Impossible! Should have return type!" - -eqnsForVars :: [Exp Id] -> [Stmt Id] -> Equations Id -> CompilerM (Equations Id) -eqnsForVars _ _ [] = return [] -eqnsForVars es d eqns = - do - v <- freshPVar - v' <- case vars v of - [x] -> pure x - _ -> throwError "Panic! Impossible --- eqnsForVars produced non-singleton vars." - let vs = foldr (union . vars . safeHead . fst) [] eqns - s = map (\vi -> (vi, v')) vs - eqns' = map (\(ps, ss) -> (ps, apply s ss)) eqns - ss' <- matchCompilerM es d eqns' - return [([v], ss')] - -safeHead :: [a] -> a -safeHead = L.head . L.fromList - -hasConstrsBeforeVars :: Equations Id -> Bool -hasConstrsBeforeVars eqns = - let (cs, vs) = span isConstr eqns - isVar ((PVar _) : _, _) = True - isVar _ = False - in (not $ null cs) && all isVar vs - -isConstr :: ([Pat Id], [Stmt Id]) -> Bool -isConstr ((PCon _ _) : _, _) = True -isConstr ((PLit _) : _, _) = True -isConstr _ = False - --- this function is safe because every call is --- guarded by allPatsStartsWithVars - -allPatsStartsWithVars :: Equations Id -> Bool -allPatsStartsWithVars = all startWithVar - where - startWithVar ((PVar _) : _, _) = True - startWithVar _ = False - --- substituting variables for pattern compilation - -type Subst = [(Name, Name)] - -class Apply a where - ids :: a -> [Id] - vars :: a -> [Name] - apply :: Subst -> a -> a - - vars = map idName . ids - -instance (Apply a) => Apply [a] where - apply s = map (apply s) - ids = foldr (union . ids) [] - -instance (Apply a) => Apply (Maybe a) where - apply _ Nothing = Nothing - apply s (Just x) = Just (apply s x) - - ids = maybe [] ids - -instance (Apply a, Apply b) => Apply (a, b) where - apply s (a, b) = (apply s a, apply s b) - ids (a, b) = ids a `union` ids b - -instance Apply (Stmt Id) where - apply s (e1 := e2) = - e1 := (apply s e2) - apply s (Let n t me) = - Let n t (apply s <$> me) - apply s (StmtExp e) = - StmtExp (apply s e) - apply s (Return e) = - Return (apply s e) - apply s (Match es eqns) = - Match (apply s es) (apply s eqns) - apply s (If e blk1 blk2) = - If (apply s e) (apply s blk1) (apply s blk2) - apply s (Asm yblk) = Asm (apply s yblk) - - ids (e1 := e2) = ids [e1, e2] - ids (Let n _ me) = [x | x <- ids me, n /= x] - ids (StmtExp e) = ids e - ids (Return e) = ids e - ids (If e blk1 blk2) = - ids e `union` ids blk1 `union` ids blk2 - ids (Match es eqns) = - ids es `union` vs' - where - vs' = ids bs \\ ids ps - (pss, bss) = unzip eqns - bs = concat bss - ps = concat pss - ids (Asm yblk) = ids yblk - -instance Apply YulStmt where - apply s (YBlock yblk) = - YBlock (apply s yblk) - apply s (YFun n yargs yret yblk) = - YFun n yargs yret (apply s yblk) - apply s (YLet ns me) = - YLet ns (apply s me) - apply s (YAssign ns e) = - YAssign ns (apply s e) - apply s (YIf e yblk) = - YIf (apply s e) (apply s yblk) - apply s (YSwitch e ycs ydf) = - YSwitch (apply s e) (apply s ycs) (apply s ydf) - apply s (YFor yblk1 e yblk2 yblk3) = - YFor - (apply s yblk1) - (apply s e) - (apply s yblk2) - (apply s yblk3) - apply s (YExp e) = - YExp (apply s e) - apply _ y = y - - ids (YBlock yblk) = ids yblk - ids (YFun _ _ _ yblk) = ids yblk - ids (YLet _ me) = ids me - ids (YAssign _ e) = ids e - ids (YIf e yblk) = ids e `union` ids yblk - ids (YSwitch e ycs ydf) = - ids e `union` ids ycs `union` ids ydf - ids (YFor yblk1 e yblk2 yblk3) = - ids yblk1 `union` ids e `union` ids yblk2 `union` ids yblk3 - ids (YExp e) = ids e - ids _ = [] - -instance Apply YulExp where - apply s (YCall n es) = - YCall n (apply s es) - apply s (YIdent n) = - YIdent (maybe n id (lookup n s)) - apply _ e = e - - ids (YCall _ es) = ids es - ids (YIdent n) = [Id n word] - ids _ = [] - -instance Apply YLiteral where - apply _ e = e - ids _ = [] - -instance Apply (Exp Id) where - apply s v@(Var (Id n t)) = - maybe v f (lookup n s) - where - f v1 = Var (Id v1 t) - apply s (Con n es) = - Con n (apply s es) - apply s (FieldAccess e n) = - FieldAccess (apply s e) n - apply _ e@(Lit _) = e - apply s (Call me n es) = - Call (apply s me) n (apply s es) - apply s (Lam args bd mt) = - Lam args (apply s bd) mt - apply s (TyExp e t) = TyExp (apply s e) t - apply s (Cond e1 e2 e3) = Cond (apply s e1) (apply s e2) (apply s e3) - apply s (Indexed e1 e2) = Indexed (apply s e1) (apply s e2) - - ids (Var n) = [n] - ids (Con _ es) = ids es - ids (FieldAccess e _) = ids e - ids (Call me _ es) = ids me `union` ids es - ids (Lam args bd _) = - ids bd \\ ids args - ids (TyExp e _) = ids e - ids _ = [] - -instance Apply (Param Id) where - apply _ p = p - - ids (Typed n _) = [n] - ids (Untyped n) = [n] - -instance Apply (Pat Id) where - apply _ p = p - - ids (PVar n) = [n] - ids (PCon _ ps) = foldr (union . ids) [] ps - ids _ = [] - --- infrastructure for the algorithm - -matchErrorCase :: CompilerM [Stmt Id] -matchErrorCase = - do - v <- matchError - return [StmtExp $ generateCall v [errorLit]] - -generateCall :: Id -> [Exp Id] -> Exp Id -generateCall = Call Nothing - -matchError :: CompilerM Id -matchError = - do - v <- (TyVar . TVar) <$> freshName - pure (Id (Name "revert") v) - -errorLit :: Exp Id -errorLit = Lit $ StrLit "Incomplete matching" - -splits :: (a -> Bool) -> [a] -> [[a]] -splits _ [] = [] -splits p xs = (ys ++ ws) : splits p ts - where - (ys, zs) = span p xs - (ws, ts) = span (not . p) zs - --- auxiliar functions which could be --- replaced by Trees that grow - -blockType :: [Stmt Id] -> Ty -blockType [] = unit -blockType ss = stmtType (last ss) - -stmtType :: Stmt Id -> Ty -stmtType (Return e) = - expType e -stmtType (StmtExp e) = - expType e -stmtType (Match _ eqns) = - eqnsType eqns -stmtType _ = unit - -expType :: Exp Id -> Ty -expType (Var (Id _ t)) = t -expType (Con (Id _ t) _) = - snd (splitTy t) -expType (FieldAccess _ (Id _ t)) = - t -expType (Call _ (Id _ t) _) = - snd (splitTy t) -expType (Lam _ _ (Just t)) = - t -expType (Lit l) = litType l -expType _ = error "Panic! MatchCompiler.expType" - -litType :: Literal -> Ty -litType _ = word - -eqnsType :: Equations Id -> Ty -eqnsType [] = unit -eqnsType ((_, ss) : _) = blockType ss - --- Compiler monad infra - -type CompilerM a = - ReaderT - String - ( ExceptT - String - ( WriterT - [FunDef Id] - (StateT Int IO) - ) - ) - a - -mkPrefix :: [Name] -> String -mkPrefix = intercalate "_" . map show - -inc :: CompilerM Int -inc = do - i <- get - put (i + 1) - return i - -freshName :: CompilerM Name -freshName = - do - n <- inc - return (Name ("var_" ++ show n)) - -freshId :: CompilerM Id -freshId = Id <$> freshName <*> freshTy - where - freshTy = (TyVar . TVar) <$> freshName - -freshExpVar :: CompilerM (Exp Id) -freshExpVar = - Var <$> freshId - -freshPVar :: CompilerM (Pat Id) -freshPVar = - PVar <$> freshId - -runCompilerM :: [Name] -> CompilerM a -> IO (Either String a, [FunDef Id]) -runCompilerM ns m = - evalStateT (runWriterT (runExceptT (runReaderT m (mkPrefix ns)))) 0 diff --git a/src/Solcore/Pipeline/SolcorePipeline.hs b/src/Solcore/Pipeline/SolcorePipeline.hs index 957728ed..970d0bd1 100644 --- a/src/Solcore/Pipeline/SolcorePipeline.hs +++ b/src/Solcore/Pipeline/SolcorePipeline.hs @@ -13,10 +13,10 @@ import Solcore.Backend.Mast () import Solcore.Backend.MastEval (defaultFuel, eliminateDeadCode, evalCompUnit) import Solcore.Backend.Specialise (specialiseCompUnit) import Solcore.Desugarer.ContractDispatch (contractDispatchDesugarer) +import Solcore.Desugarer.DecisionTreeCompiler (matchCompiler, showWarning) import Solcore.Desugarer.FieldAccess (fieldDesugarer) import Solcore.Desugarer.IfDesugarer (ifDesugarer) import Solcore.Desugarer.IndirectCall (indirectCall) -import Solcore.Desugarer.MatchCompiler (matchCompiler) import Solcore.Desugarer.ReplaceFunTypeArgs import Solcore.Desugarer.ReplaceWildcard (replaceWildcard) import Solcore.Frontend.Parser.SolcoreParser @@ -163,9 +163,12 @@ compile opts = runExceptT $ do matchless <- if noMatchCompiler then pure desugared - else ExceptT $ timeItNamed "Match compiler" $ matchCompiler desugared + else do + (ast, warns) <- ExceptT $ timeItNamed "Match compiler" $ matchCompiler desugared + when (verbose && not (null warns)) $ liftIO $ mapM_ (putStrLn . showWarning) warns + pure ast - let printMatch = (not $ noMatchCompiler) && (verbose || optDumpDS opts) + let printMatch = not noMatchCompiler && (verbose || optDumpDS opts) liftIO $ when printMatch $ do putStrLn "> Match compilation result:" putStrLn (pretty matchless) diff --git a/test/Cases.hs b/test/Cases.hs index 2c3eda18..423fc534 100644 --- a/test/Cases.hs +++ b/test/Cases.hs @@ -290,6 +290,11 @@ cases = runTestForFile "field-name-error.solc" caseFolder, runTestExpectingFailure "field-access.solc" caseFolder, runTestForFile "mod-example.solc" caseFolder, + runTestForFile "snds.solc" caseFolder, + runTestForFile "bool-elim.solc" caseFolder, + runTestForFile "catch-all.solc" caseFolder, + runTestForFile "redundant-match.solc" caseFolder, + runTestForFile "false-redundant-warning.solc" caseFolder, runTestForFile "proxy-desugar.solc" caseFolder, runTestForFile "invokable-issue.solc" caseFolder, runTestForFile "td.solc" caseFolder, @@ -302,7 +307,9 @@ cases = runTestForFile "instance-synonym.solc" caseFolder, runTestExpectingFailure "overlap-synonym-detected.solc" caseFolder, runTestExpectingFailure "overlap-synonym-missed-order.solc" caseFolder, - runTestExpectingFailure "overlap-synonym-missed-two-synonyms.solc" caseFolder + runTestExpectingFailure "overlap-synonym-missed-two-synonyms.solc" caseFolder, + runTestForFile "copytomem.solc" caseFolder, + runTestForFile "fresh-variable-shadowing.solc" caseFolder ] where caseFolder = "./test/examples/cases" diff --git a/test/Main.hs b/test/Main.hs index 175459cd..46f9aa23 100644 --- a/test/Main.hs +++ b/test/Main.hs @@ -1,6 +1,7 @@ module Main where import Cases +import MatchCompilerTests import Test.Tasty main :: IO () @@ -16,6 +17,6 @@ tests = spec, std, imports, - dispatches - -- , reduceTests + dispatches, + matchTests ] diff --git a/test/MatchCompilerTests.hs b/test/MatchCompilerTests.hs new file mode 100644 index 00000000..fff37b97 --- /dev/null +++ b/test/MatchCompilerTests.hs @@ -0,0 +1,815 @@ +module MatchCompilerTests where + +import Data.List (sort) +import Data.Map qualified as Map +import Solcore.Desugarer.DecisionTreeCompiler +import Solcore.Frontend.Pretty.SolcorePretty +import Solcore.Frontend.Syntax +import Solcore.Frontend.TypeInference.Id +import Solcore.Primitives.Primitives (at, bt, pair, sumTy) +import Test.Tasty +import Test.Tasty.HUnit + +matchTests :: TestTree +matchTests = + testGroup + "DecisionTreeCompiler" + [ testGroup + "compileMatrix" + [ test_emptyMatrix_isFail_andNonExhaustive, + test_singleVarRow_isLeaf_noWarnings, + test_redundantVarRow_emitsRedundantClause, + test_boolCompleteCover_noDefault_noWarnings, + test_boolIncompleteCover_defaultFail_nonExhaustive, + test_listCompleteCover_nestedSwitch_noWarnings, + test_twoColumn_completeCover_noWarnings, + test_litPats_withVarDefault_noWarnings, + test_litPats_noDefault_nonExhaustive, + test_unknownConstructor_isError + ], + testGroup + "treeToStmt" + [ test_treeToStmt_singleVar_substituted, + test_treeToStmt_multiColumn_varsBoundViaSpecialize + ], + testGroup + "redundancy warnings" + [ test_allVar_first_shadows_nonexhaustive_rest, + test_twoCol_noFalsePositive_partialOverlap, + test_twoCol_genuinelyRedundant_thirdRow, + test_singleCol_duplicateRow_warned + ], + testGroup + "non-exhaustive witness completeness" + [ test_twoCol_con_nonExh_witness_has_both_columns, + test_twoCol_lit_nonExh_witness_has_both_columns + ], + testGroup + "sibling set / missing-constructor witness" + [ test_nonExh_polyEnv_missingNil_witness_is_Nil, + test_nonExh_polyEnv_missingCons_witness_is_Cons + ], + testGroup + "inhabitsM correctness" + [ test_inhabitsM_wildcard_row_covers_all + ], + testGroup + "primEnv correctness" + [ test_pairConInfo_returnType_is_result_type, + test_inlConInfo_returnType_is_result_type, + test_inrConInfo_returnType_is_result_type + ] + ] + +runMatrix :: + TypeEnv -> + [Ty] -> + [Occurrence] -> + PatternMatrix -> + [Action] -> + IO (Either String (DecisionTree, [Warning])) +runMatrix env tys occs matrix acts = + runCompilerM env (compileMatrix tys occs matrix [([], a) | a <- acts]) + +-- Like runMatrix but also runs the redundancy pre-pass so RedundantClause +-- warnings are emitted (mirroring what compile (Match …) does end-to-end). +runMatrixFull :: + TypeEnv -> + [Ty] -> + [Occurrence] -> + PatternMatrix -> + [Action] -> + IO (Either String (DecisionTree, [Warning])) +runMatrixFull env tys occs matrix acts = + runCompilerM env $ do + ctx <- askWarnCtx + let bacts = [([], a) | a <- acts] + checkRedundancy ctx tys matrix bacts + compileMatrix tys occs matrix bacts + +-- Run compileMatrix then treeToStmt in one pass, returning the compiled statement. +runFull :: + TypeEnv -> + OccMap -> + [Ty] -> + [Occurrence] -> + PatternMatrix -> + [Action] -> + IO (Either String (Stmt Id, [Warning])) +runFull env occMap tys occs matrix acts = + runCompilerM env $ do + tree <- compileMatrix tys occs matrix [([], a) | a <- acts] + treeToStmt occMap tree + +assertRight :: + String -> + IO (Either String (DecisionTree, [Warning])) -> + (DecisionTree -> [Warning] -> Assertion) -> + Assertion +assertRight label act check = do + r <- act + case r of + Left err -> assertFailure (label ++ ": unexpected error: " ++ err) + Right (tree, ws) -> check tree ws + +assertLeft :: + String -> + IO (Either String (DecisionTree, [Warning])) -> + Assertion +assertLeft label act = do + r <- act + case r of + Left _ -> pure () + Right (tree, _) -> + assertFailure (label ++ ": expected error but got tree: " ++ show tree) + +isNonExh :: Warning -> Bool +isNonExh (NonExhaustive _ _) = True +isNonExh _ = False + +isRedundant :: Warning -> Bool +isRedundant (RedundantClause _ _ _) = True +isRedundant _ = False + +branchNames :: [(Id, [Pattern], DecisionTree)] -> [String] +branchNames bs = sort [nameOf (idName k) | (k, _, _) <- bs] + where + nameOf n = pretty n + +branchLits :: [(Literal, DecisionTree)] -> [Literal] +branchLits = map fst + +tyBool :: Ty +tyBool = TyCon (Name "Bool") [] + +tyList :: Ty +tyList = TyCon (Name "List") [tyBool] + +tyWord :: Ty +tyWord = TyCon (Name "word") [] + +idTrue :: Id +idTrue = Id (Name "True") (funtype [] tyBool) + +idFalse :: Id +idFalse = Id (Name "False") (funtype [] tyBool) + +idNil :: Id +idNil = Id (Name "Nil") (funtype [] tyList) + +idCons :: Id +idCons = Id (Name "Cons") (funtype [tyBool, tyList] tyList) + +-- Polymorphic list type, as addDataTyInfo produces for: data List a = Nil | Cons a (List a) +-- conReturnType stores TyCon "List" [TyVar "a"], NOT the concrete TyCon "List" [Bool]. +tyVarA :: Ty +tyVarA = TyVar (TVar (Name "a")) + +tyListPoly :: Ty +tyListPoly = TyCon (Name "List") [tyVarA] + +-- TypeEnv as initialTypeEnv/addDataTyInfo would build it (polymorphic return types). +polyListEnv :: TypeEnv +polyListEnv = + Map.fromList + [ (Name "Nil", ConInfo {conFieldTypes = [], conReturnType = tyListPoly}), + (Name "Cons", ConInfo {conFieldTypes = [tyVarA, tyListPoly], conReturnType = tyListPoly}) + ] + +-- Constructor Ids as the type-checker annotates them in patterns (concrete types). +idNilConcrete :: Id +idNilConcrete = Id (Name "Nil") tyList -- tyList = TyCon "List" [tyBool] + +idConsConcrete :: Id +idConsConcrete = Id (Name "Cons") (funtype [tyBool, tyList] tyList) + +patNilConcrete :: Pattern +patNilConcrete = PCon idNilConcrete [] + +patConsConcrete :: Pattern +patConsConcrete = + PCon + idConsConcrete + [ pvar "h" tyBool, + pvar "t" tyList + ] + +-- Type environments +boolEnv :: TypeEnv +boolEnv = + Map.fromList + [ (idName idTrue, ConInfo {conFieldTypes = [], conReturnType = tyBool}), + (idName idFalse, ConInfo {conFieldTypes = [], conReturnType = tyBool}) + ] + +listEnv :: TypeEnv +listEnv = + Map.fromList + [ (idName idNil, ConInfo {conFieldTypes = [], conReturnType = tyList}), + (idName idCons, ConInfo {conFieldTypes = [tyBool, tyList], conReturnType = tyList}) + ] + +patTrue :: Pattern +patTrue = PCon idTrue [] + +patFalse :: Pattern +patFalse = PCon idFalse [] + +patNil :: Pattern +patNil = PCon idNil [] + +patCons :: Pattern +patCons = + PCon + idCons + [ PVar (Id (Name "h") tyBool), + PVar (Id (Name "t") tyList) + ] + +pvar :: String -> Ty -> Pattern +pvar n ty = PVar (Id (Name n) ty) + +varBool :: Exp Id +varBool = Var (Id (Name "x") tyBool) + +varWord :: Exp Id +varWord = Var (Id (Name "n") tyWord) + +retVar :: String -> Ty -> Action +retVar n ty = [Return (Var (Id (Name n) ty))] + +actionA, actionB, actionC, actionD :: Action +actionA = retVar "a" tyBool +actionB = retVar "b" tyBool +actionC = retVar "c" tyBool +actionD = retVar "d" tyBool + +occ1 :: [Occurrence] +occ1 = [[0]] + +occ2 :: [Occurrence] +occ2 = [[0], [1]] + +-- 1. Empty matrix: no rows at all → Fail + NonExhaustive +test_emptyMatrix_isFail_andNonExhaustive :: TestTree +test_emptyMatrix_isFail_andNonExhaustive = + testCase "empty matrix -> Fail and one NonExhaustive warning" $ + assertRight "empty" (runMatrix boolEnv [tyBool] occ1 [] []) $ + \tree warns -> do + assertEqual "tree should be Fail" Fail tree + assertBool "should emit NonExhaustive warning" (any isNonExh warns) + +-- 2. Single all-variable row → Leaf, no warnings +test_singleVarRow_isLeaf_noWarnings :: TestTree +test_singleVarRow_isLeaf_noWarnings = + testCase "single variable row -> Leaf with no warnings" + $ assertRight + "single-var" + (runMatrix boolEnv [tyBool] occ1 [[pvar "x" tyBool]] [actionA]) + $ \tree warns -> do + case tree of + Leaf _ act' -> assertEqual "leaf action should be actionA" actionA act' + _ -> assertFailure ("expected Leaf, got: " ++ show tree) + assertBool "should have no warnings" (null warns) + +-- 3. All-var first row always fires; later rows are dead code → warned as unreachable +test_redundantVarRow_emitsRedundantClause :: TestTree +test_redundantVarRow_emitsRedundantClause = + testCase "all-var first row fires correctly; later rows are warned as unreachable" + $ assertRight + "redundant" + ( runMatrixFull + boolEnv + [tyBool] + occ1 + [[pvar "x" tyBool], [patTrue], [patFalse]] + [actionA, actionB, actionC] + ) + $ \tree warns -> do + case tree of + Leaf _ _ -> pure () + _ -> assertFailure ("expected Leaf for all-var first row, got: " ++ show tree) + let redundantActs = [act | RedundantClause _ _ act <- warns] + assertBool "True clause must be warned as unreachable" (actionB `elem` redundantActs) + assertBool "False clause must be warned as unreachable" (actionC `elem` redundantActs) + assertBool "first all-var row must not be warned as redundant" (actionA `notElem` redundantActs) + assertBool "should not emit NonExhaustive warning" (not (any isNonExh warns)) + +-- 4. Complete Bool cover → Switch with Nothing default, no warnings +test_boolCompleteCover_noDefault_noWarnings :: TestTree +test_boolCompleteCover_noDefault_noWarnings = + testCase "True+False cover -> Switch with no default and no warnings" + $ assertRight + "bool-complete" + ( runMatrix + boolEnv + [tyBool] + occ1 + [[patTrue], [patFalse]] + [actionA, actionB] + ) + $ \tree warns -> do + case tree of + Switch [0] branches Nothing -> do + assertEqual + "should have exactly True and False branches" + ["False", "True"] + (branchNames branches) + assertBool "should have no warnings" (null warns) + Switch _ _ (Just _) -> + assertFailure "complete cover must not have a default branch" + _ -> + assertFailure ("expected Switch, got: " ++ show tree) + +-- 5. Incomplete Bool cover → Switch with Just Fail default + NonExhaustive +test_boolIncompleteCover_defaultFail_nonExhaustive :: TestTree +test_boolIncompleteCover_defaultFail_nonExhaustive = + testCase "True-only cover -> Switch with Fail default and NonExhaustive warning" + $ assertRight + "bool-incomplete" + (runMatrix boolEnv [tyBool] occ1 [[patTrue]] [actionA]) + $ \tree warns -> do + case tree of + Switch [0] branches (Just Fail) -> do + assertEqual + "should only have the True branch" + ["True"] + (branchNames branches) + assertBool "should emit NonExhaustive warning" (any isNonExh warns) + _ -> + assertFailure ("expected Switch … (Just Fail), got: " ++ show tree) + +-- 6. Complete List cover (Nil + Cons) → Switch, no default, no warnings +test_listCompleteCover_nestedSwitch_noWarnings :: TestTree +test_listCompleteCover_nestedSwitch_noWarnings = + testCase "Nil + Cons cover -> Switch with no default and no warnings" + $ assertRight + "list-complete" + ( runMatrix + listEnv + [tyList] + occ1 + [[patNil], [patCons]] + [actionA, actionB] + ) + $ \tree warns -> do + case tree of + Switch [0] branches Nothing -> do + assertEqual + "should have exactly Cons and Nil branches" + ["Cons", "Nil"] + (branchNames branches) + assertBool "should have no warnings" (null warns) + _ -> + assertFailure ("expected Switch with two branches, got: " ++ show tree) + +-- 7. Two-column Bool×Bool complete matrix → no default at any level, no warnings +test_twoColumn_completeCover_noWarnings :: TestTree +test_twoColumn_completeCover_noWarnings = + testCase "Bool*Bool all-four-cases matrix -> no defaults, no warnings" + $ assertRight + "bool*bool" + ( runMatrix + boolEnv + [tyBool, tyBool] + occ2 + [ [patTrue, patTrue], + [patTrue, patFalse], + [patFalse, patTrue], + [patFalse, patFalse] + ] + [actionA, actionB, actionC, actionD] + ) + $ \tree warns -> do + case tree of + Switch _ outerBranches Nothing -> do + mapM_ (\(_, _, t) -> assertInnerHasNoDefault t) outerBranches + assertBool "should have no warnings" (null warns) + _ -> + assertFailure + ( "expected top-level Switch with no default, got: " + ++ show tree + ) + where + assertInnerHasNoDefault (Switch _ _ Nothing) = pure () + assertInnerHasNoDefault t = + assertFailure ("inner subtree should have no default branch, got: " ++ show t) + +-- 8. Literal patterns with a variable catch-all → LitSwitch with Leaf default, no warnings +test_litPats_withVarDefault_noWarnings :: TestTree +test_litPats_withVarDefault_noWarnings = + testCase "lit patterns with variable fallback -> LitSwitch with Leaf default, no warnings" + $ assertRight + "lit-default" + ( runMatrix + Map.empty + [tyWord] + occ1 + [[PLit (IntLit 0)], [PLit (IntLit 1)], [pvar "x" tyWord]] + [actionA, actionB, actionC] + ) + $ \tree warns -> do + case tree of + LitSwitch [0] branches (Just (Leaf _ defAct)) -> do + assertBool + "should have literal 0 branch" + (IntLit 0 `elem` branchLits branches) + assertBool + "should have literal 1 branch" + (IntLit 1 `elem` branchLits branches) + assertEqual "default leaf should be actionC" actionC defAct + assertBool "should have no warnings:" (null warns) + LitSwitch _ _ Nothing -> + assertFailure "expected a default branch for the variable catch-all" + _ -> + assertFailure ("expected LitSwitch, got: " ++ show tree) + +-- 9. Literal patterns without a catch-all → LitSwitch with Fail default + NonExhaustive +test_litPats_noDefault_nonExhaustive :: TestTree +test_litPats_noDefault_nonExhaustive = + testCase "lit patterns without catch-all -> LitSwitch with Fail default and NonExhaustive" + $ assertRight + "lit-no-default" + ( runMatrix + Map.empty + [tyWord] + occ1 + [[PLit (IntLit 0)], [PLit (IntLit 1)]] + [actionA, actionB] + ) + $ \tree warns -> do + case tree of + LitSwitch [0] branches (Just Fail) -> do + assertBool + "should have literal 0 branch" + (IntLit 0 `elem` branchLits branches) + assertBool + "should have literal 1 branch" + (IntLit 1 `elem` branchLits branches) + assertBool "should emit NonExhaustive warning" (any isNonExh warns) + _ -> + assertFailure ("expected LitSwitch … (Just Fail), got: " ++ show tree) + +-- 10. Constructor absent from the TypeEnv → Left error +test_unknownConstructor_isError :: TestTree +test_unknownConstructor_isError = + testCase "pattern constructor absent from TypeEnv -> Left error" $ + assertLeft + "unknown-con" + (runMatrix Map.empty [tyBool] occ1 [[patTrue]] [actionA]) + +-- Shared data for treeToStmt and inhabitsConCol tests + +varX :: Exp Id +varX = Var (Id (Name "x") tyBool) + +varY :: Exp Id +varY = Var (Id (Name "y") tyBool) + +-- Type environment with both List and Bool constructors +listBoolEnv :: TypeEnv +listBoolEnv = Map.union listEnv boolEnv + +-- 11. treeToStmt correctly substitutes a PVar with the scrutinee expression +-- +-- match y { | z => return z } +-- should compile to: return y +test_treeToStmt_singleVar_substituted :: TestTree +test_treeToStmt_singleVar_substituted = + testCase "treeToStmt: PVar in single-column all-var row is substituted by occurrence" $ do + let idZ = Id (Name "z") tyBool + occMap = Map.fromList [([0 :: Int], varY)] + r <- runFull boolEnv occMap [tyBool] [[0]] [[PVar idZ]] [[Return (Var idZ)]] + case r of + Left err -> assertFailure ("unexpected error: " ++ err) + Right (stmt, _) -> assertEqual "z should be substituted with y" (Return varY) stmt + +-- 12. treeToStmt correctly substitutes PVars bound through specialize and defaultMatrix +-- +-- match x, y { | True, z => return z; | z, w => return z } +-- +-- True branch: z is bound to occurrence [1] (= y) → return y +-- default branch: z is bound to occurrence [0] (= x) via defaultBoundActs → return x +test_treeToStmt_multiColumn_varsBoundViaSpecialize :: TestTree +test_treeToStmt_multiColumn_varsBoundViaSpecialize = + testCase "treeToStmt: PVars bound via specialize/defaultMatrix are correctly substituted" $ do + let idZ = Id (Name "z") tyBool + idW = Id (Name "w") tyBool + occMap = Map.fromList [([0 :: Int], varX), ([1], varY)] + matrix = [[patTrue, PVar idZ], [PVar idZ, PVar idW]] + retZ = [Return (Var idZ)] + r <- runFull boolEnv occMap [tyBool, tyBool] [[0], [1]] matrix [retZ, retZ] + case r of + Left err -> assertFailure ("unexpected error: " ++ err) + Right (stmt, _) -> case stmt of + Match [scrutinee] eqns -> do + assertEqual "scrutinee should be x" varX scrutinee + let trueBodys = [body | ([PCon k _], body) <- eqns, idName k == Name "True"] + let defBodys = [body | ([PVar _], body) <- eqns] + case trueBodys of + (tb : _) -> assertEqual "True branch: z substituted with y" [Return varY] tb + [] -> assertFailure "True branch not found in Match alts" + case defBodys of + (db : _) -> assertEqual "default branch: z substituted with x" [Return varX] db + [] -> assertFailure "default branch not found in Match alts" + _ -> assertFailure ("expected Match [x] …, got: " ++ show stmt) + +-- 13. Rows after a first all-var row are warned as unreachable even when they +-- are NOT exhaustive by themselves. +-- +-- match x { | z => return z; | True => return True; } +-- +-- The True clause is dead code: z catches everything first. This must be +-- warned as unreachable even though True alone does not cover the type. +test_allVar_first_shadows_nonexhaustive_rest :: TestTree +test_allVar_first_shadows_nonexhaustive_rest = + testCase "rows after first all-var row are unreachable even if not exhaustive" + $ assertRight + "catchall-shadows-partial" + ( runMatrixFull + boolEnv + [tyBool] + occ1 + [[pvar "z" tyBool], [patTrue]] + [actionA, actionB] + ) + $ \tree warns -> do + case tree of + Leaf _ _ -> pure () + _ -> assertFailure ("expected Leaf, got: " ++ show tree) + let redundantActs = [act | RedundantClause _ _ act <- warns] + assertBool "True clause must be warned as unreachable" (actionB `elem` redundantActs) + assertBool "first all-var row must not be warned" (actionA `notElem` redundantActs) + +-- 14. Two-column match: (True,z) / (w,True) / (a,b) +-- The rows after the first are NOT globally redundant: +-- row 1 fires for (False, True), row 2 fires for (False, False). +-- No RedundantClause warnings should be emitted. +test_twoCol_noFalsePositive_partialOverlap :: TestTree +test_twoCol_noFalsePositive_partialOverlap = + testCase "two-col: overlapping rows are not falsely warned as redundant" + $ assertRight + "two-col-no-false-pos" + ( runMatrixFull + boolEnv + [tyBool, tyBool] + occ2 + [ [patTrue, pvar "z" tyBool], + [pvar "w" tyBool, patTrue], + [pvar "a" tyBool, pvar "b" tyBool] + ] + [actionA, actionB, actionC] + ) + $ \_ warns -> do + let redundantActs = [act | RedundantClause _ _ act <- warns] + assertBool "row 1 (w,True) must NOT be warned as redundant" (actionB `notElem` redundantActs) + assertBool "row 2 (a,b) must NOT be warned as redundant" (actionC `notElem` redundantActs) + assertBool "no RedundantClause warnings at all" (null redundantActs) + +-- 15. Two-column match: genuinely redundant third row. +-- (True,True) / (False,True) / (z,True) — rows 0+1 cover all (x,True), +-- so row 2 is truly dead. +test_twoCol_genuinelyRedundant_thirdRow :: TestTree +test_twoCol_genuinelyRedundant_thirdRow = + testCase "two-col: third row subsumed by first two is genuinely warned" + $ assertRight + "two-col-true-pos" + ( runMatrixFull + boolEnv + [tyBool, tyBool] + occ2 + [ [patTrue, patTrue], + [patFalse, patTrue], + [pvar "z" tyBool, patTrue] + ] + [actionA, actionB, actionC] + ) + $ \_ warns -> do + let redundantActs = [act | RedundantClause _ _ act <- warns] + assertBool "row 2 (z,True) must be warned as redundant" (actionC `elem` redundantActs) + assertBool "row 0 must not be warned" (actionA `notElem` redundantActs) + assertBool "row 1 must not be warned" (actionB `notElem` redundantActs) + +-- 16. Single-column duplicate row: second True is redundant, False is not. +test_singleCol_duplicateRow_warned :: TestTree +test_singleCol_duplicateRow_warned = + testCase "single-col: exact duplicate constructor row is warned, later row is not" + $ assertRight + "dup-row" + ( runMatrixFull + boolEnv + [tyBool] + occ1 + [[patTrue], [patTrue], [patFalse]] + [actionA, actionB, actionC] + ) + $ \_ warns -> do + let redundantActs = [act | RedundantClause _ _ act <- warns] + assertBool "second True must be warned as redundant" (actionB `elem` redundantActs) + assertBool "False must not be warned as redundant" (actionC `notElem` redundantActs) + assertBool "first True must not be warned" (actionA `notElem` redundantActs) + +-- 17. Two-column constructor match with one missing constructor: +-- the NonExhaustive witness must cover BOTH columns, not just the +-- selected constructor column. +-- +-- match x, y { | True, z => ... } +-- Missing: (False, _) — witness should be [PCon False [], PVar _] +test_twoCol_con_nonExh_witness_has_both_columns :: TestTree +test_twoCol_con_nonExh_witness_has_both_columns = + testCase "two-col constructor: NonExhaustive witness covers both columns" + $ assertRight + "two-col-con-nonexh" + ( runMatrix + boolEnv + [tyBool, tyBool] + occ2 + [[patTrue, pvar "z" tyBool]] + [actionA] + ) + $ \_ warns -> do + let nonExhPats = [pats | NonExhaustive _ pats <- warns] + case nonExhPats of + [] -> assertFailure "expected a NonExhaustive warning" + (pats : _) -> do + assertEqual + "witness must have one pattern per scrutinee column (2)" + 2 + (length pats) + case pats of + (PCon k [] : _) -> + assertEqual "first pattern must be the missing constructor False" (Name "False") (idName k) + _ -> + assertFailure ("expected PCon False as first witness pattern, got: " ++ show pats) + +-- 18. Two-column literal match without a catch-all: +-- the NonExhaustive witness must cover BOTH columns, not just the +-- remaining (non-literal) column. +-- +-- match n, b { | 0, z => ... } +-- Missing: (_, _) — witness should be [PVar _, PVar _] +test_twoCol_lit_nonExh_witness_has_both_columns :: TestTree +test_twoCol_lit_nonExh_witness_has_both_columns = + testCase "two-col literal: NonExhaustive witness covers both columns" + $ assertRight + "two-col-lit-nonexh" + ( runMatrix + boolEnv + [tyWord, tyBool] + occ2 + [[PLit (IntLit 0), pvar "z" tyBool]] + [actionA] + ) + $ \_ warns -> do + let nonExhPats = [pats | NonExhaustive _ pats <- warns] + case nonExhPats of + [] -> assertFailure "expected a NonExhaustive warning" + (pats : _) -> + assertEqual + "witness must have one pattern per scrutinee column (2)" + 2 + (length pats) + +-- 19. inhabitsM: a matrix that has a wildcard row covering all columns is +-- exhaustive. The bug in 'inhabitsConCol' returns a false witness when +-- mRestWit = Nothing (the wildcard rows already cover every rest-column +-- value), instead of returning Nothing (= exhaustive). +-- +-- matrix: [ [True, True] -- row 0: covers (True, True) +-- , [z, w ] ] -- row 1: wildcard catches everything else +-- types: [Bool, Bool] +-- +-- The wildcard row 1 means the matrix IS exhaustive → Nothing. +-- Bug: inhabitsConCol finds missingCons=[False], computes +-- mRestWit = Nothing (wildcard covers restTys), but still emits +-- Just [PCon False [], $v]. +test_inhabitsM_wildcard_row_covers_all :: TestTree +test_inhabitsM_wildcard_row_covers_all = + testCase "inhabitsM: wildcard row makes matrix exhaustive → Nothing (no false witness)" $ do + let idZ = Id (Name "z") tyBool + idW = Id (Name "w") tyBool + matrix = + [ [patTrue, patTrue], + [PVar idZ, PVar idW] + ] + r <- runCompilerM boolEnv (inhabitsM matrix [tyBool, tyBool]) + case r of + Left err -> assertFailure ("unexpected error: " ++ err) + Right (mWit, _) -> + assertEqual + "wildcard row covers all patterns: inhabitsM should be Nothing" + Nothing + mWit + +-- 20. primEnv: pairConInfo.conReturnType stores pairTy at bt (the arrow type +-- at :-> bt :-> pair at bt) instead of the result type pair at bt. +-- Fix: ConInfo [at, bt] (pair at bt). +test_pairConInfo_returnType_is_result_type :: TestTree +test_pairConInfo_returnType_is_result_type = + testCase "pairConInfo: conReturnType should be pair at bt (result type, not arrow type)" $ + assertEqual + "conReturnType pairConInfo" + (pair at bt) + (conReturnType pairConInfo) + +-- 21. primEnv: inlConInfo.conReturnType stores inlTy at bt (the arrow type +-- at :-> sum at bt) instead of the result type sumTy at bt. +-- Fix: ConInfo [at] (sumTy at bt). +test_inlConInfo_returnType_is_result_type :: TestTree +test_inlConInfo_returnType_is_result_type = + testCase "inlConInfo: conReturnType should be sumTy at bt (result type, not arrow type)" $ + assertEqual + "conReturnType inlConInfo" + (sumTy at bt) + (conReturnType inlConInfo) + +-- 22. primEnv: inrConInfo.conReturnType stores inlTy at bt (wrong: uses inl +-- instead of inr, and stores the arrow type rather than the result type). +-- Fix: ConInfo [bt] (sumTy at bt). +test_inrConInfo_returnType_is_result_type :: TestTree +test_inrConInfo_returnType_is_result_type = + testCase "inrConInfo: conReturnType should be sumTy at bt (not inlTy at bt)" $ + assertEqual + "conReturnType inrConInfo" + (sumTy at bt) + (conReturnType inrConInfo) + +-- --------------------------------------------------------------------------- +-- Bug: `siblings \\ headCons` uses Eq Id (name + type). +-- +-- `siblingConstructors` builds Id values via `idFromInfo`, which uses the +-- TypeEnv's conReturnType. When the TypeEnv was built by `addDataTyInfo`, +-- conReturnType is polymorphic (e.g. TyCon "List" [TyVar "a"]). But the +-- constructor Ids in the pattern matrix come from the type-checker and carry +-- concrete types (e.g. TyCon "List" [Bool]). +-- +-- `siblings \\ headCons` therefore fails to remove any element of headCons +-- from siblings, so `missing` contains ALL sibling constructors instead of +-- just the absent ones. The first element of `missing` may then be a +-- constructor that IS already covered — producing a false or wrong witness. +-- +-- Fix: compare by name only: +-- let missing = filter (\s -> idName s `notElem` map idName headCons) siblings +-- --------------------------------------------------------------------------- + +-- 23. polyListEnv has polymorphic return types (as addDataTyInfo produces). +-- Matrix [[Cons h t]] on [List Bool] covers only Cons; Nil is missing. +-- siblings = [Cons_poly, Nil_poly]; headCons = [Cons_concrete]. +-- Bug: (\\) finds Cons_poly /= Cons_concrete → missing = [Cons_poly, Nil_poly]. +-- First missing = Cons_poly → witness says "Cons missing" — WRONG. +-- Fix: missing = [Nil_poly] → witness says "Nil missing" — CORRECT. +test_nonExh_polyEnv_missingNil_witness_is_Nil :: TestTree +test_nonExh_polyEnv_missingNil_witness_is_Nil = + testCase "poly TypeEnv: missing-constructor witness names Nil (not Cons) when Cons is covered" + $ assertRight + "poly-list-missing-nil" + ( runMatrix + polyListEnv + [tyList] + occ1 + [[patConsConcrete]] + [actionA] + ) + $ \_ warns -> do + let nonExhPats = [pats | NonExhaustive _ pats <- warns] + case nonExhPats of + [] -> assertFailure "expected a NonExhaustive warning" + (pats : _) -> case pats of + (PCon k _ : _) -> + assertEqual + "missing constructor should be Nil (Cons is covered)" + (Name "Nil") + (idName k) + _ -> + assertFailure ("expected PCon as first witness pattern, got: " ++ show pats) + +-- 24. Same environment, opposite case: matrix [[Nil]] covers only Nil; Cons is missing. +-- siblings = [Cons_poly, Nil_poly]; headCons = [Nil_concrete]. +-- Bug: (\\) finds Nil_poly /= Nil_concrete → missing = [Cons_poly, Nil_poly]. +-- First missing = Cons_poly → witness says "Cons missing" — happens to be correct +-- BY ACCIDENT (Cons is alphabetically first in Map.toList). +-- This test documents that the correct answer is Cons, and that the fix preserves it. +test_nonExh_polyEnv_missingCons_witness_is_Cons :: TestTree +test_nonExh_polyEnv_missingCons_witness_is_Cons = + testCase "poly TypeEnv: missing-constructor witness names Cons (not Nil) when Nil is covered" + $ assertRight + "poly-list-missing-cons" + ( runMatrix + polyListEnv + [tyList] + occ1 + [[patNilConcrete]] + [actionA] + ) + $ \_ warns -> do + let nonExhPats = [pats | NonExhaustive _ pats <- warns] + case nonExhPats of + [] -> assertFailure "expected a NonExhaustive warning" + (pats : _) -> case pats of + (PCon k _ : _) -> + assertEqual + "missing constructor should be Cons (Nil is covered)" + (Name "Cons") + (idName k) + _ -> + assertFailure ("expected PCon as first witness pattern, got: " ++ show pats) diff --git a/test/examples/cases/ListModule.solc b/test/examples/cases/ListModule.solc index 59a14c10..715e759b 100644 --- a/test/examples/cases/ListModule.solc +++ b/test/examples/cases/ListModule.solc @@ -3,19 +3,24 @@ contract ListModule { data Bool = True | False; - function zipWith (f,xs,ys) { + forall a b c . function zipWith (f : (a,b) -> c,xs : List(a),ys : List(b)) -> List(c) { match xs, ys { | Nil, Nil => return Nil ; | Cons(x1,xs1), Cons(y1,ys1) => return Cons(f(x1,y1), zipWith(f,xs1,ys1)) ; + | _ , _ => return Nil; } } - function foldr(f, v, xs) { + forall a b . function foldr(f : (a,b) -> b, v : b, xs : List(a)) -> b { match xs { | Nil => return v; | Cons(y,ys) => return f(y, foldr(f,v,ys)) ; } } + + function main () -> word { + return 0; + } } diff --git a/test/examples/cases/MatchCall.solc b/test/examples/cases/MatchCall.solc index b9b946a3..1412864f 100644 --- a/test/examples/cases/MatchCall.solc +++ b/test/examples/cases/MatchCall.solc @@ -8,6 +8,7 @@ contract MatchCall { function main() { match f() { | True => return 42; + | False => return 0; } } } diff --git a/test/examples/cases/Pair.solc b/test/examples/cases/Pair.solc index 836da609..c20e1b76 100644 --- a/test/examples/cases/Pair.solc +++ b/test/examples/cases/Pair.solc @@ -16,6 +16,12 @@ } } + function snds (p1, p2) { + match p1, p2 { + | (a,b) , (c,d) => return (b,d); + } + } + function curry(f,x,y) { return f((x,y)) ; } diff --git a/test/examples/cases/bool-elim.solc b/test/examples/cases/bool-elim.solc new file mode 100644 index 00000000..f9396c87 --- /dev/null +++ b/test/examples/cases/bool-elim.solc @@ -0,0 +1,14 @@ +data Bool = False | True; + + function second(x, y) { + match x, y { + | True, z => return z; + | False, z => return z; + } + } + +contract Second { + function main() -> word { + second(True, 42) + } +} diff --git a/test/examples/cases/catch-all.solc b/test/examples/cases/catch-all.solc new file mode 100644 index 00000000..3cd0dd36 --- /dev/null +++ b/test/examples/cases/catch-all.solc @@ -0,0 +1,14 @@ +data Bool = False | True; + +contract CatchAll { + function catchAll(x, y) -> Bool{ + match x, y { + | True, True => return True; + | z, w => return z; + } + } + + function main() -> Bool { + catchAll(True, False) + } +} diff --git a/test/examples/cases/copytomem.solc b/test/examples/cases/copytomem.solc new file mode 100644 index 00000000..b13ac736 --- /dev/null +++ b/test/examples/cases/copytomem.solc @@ -0,0 +1,7 @@ +data MemoryWordReader = MemoryWordReader(word); + +function copyToMem(reader:MemoryWordReader, dst:word, cnt: word) -> () { + match reader { + | MemoryWordReader(ptr) => assembly { mcopy(dst, ptr, cnt) } + } +} diff --git a/test/examples/cases/empty-asm.solc b/test/examples/cases/empty-asm.solc index 81e6307d..e8911fe2 100644 --- a/test/examples/cases/empty-asm.solc +++ b/test/examples/cases/empty-asm.solc @@ -4,5 +4,6 @@ function f(x : word) { let ret : word; assembly {} return ret; + | _ => return 0; } } diff --git a/test/examples/cases/false-redundant-warning.solc b/test/examples/cases/false-redundant-warning.solc new file mode 100644 index 00000000..9dbae5ff --- /dev/null +++ b/test/examples/cases/false-redundant-warning.solc @@ -0,0 +1,15 @@ +data Bool = False | True; + +function test(x, y) { + match x, y { + | True, z => return z; + | w, True => return w; + | a, b => return b; + } +} + +contract FalseRedundantWarning { + function main() -> Bool { + test(False, True) + } +} diff --git a/test/examples/cases/fresh-variable-shadowing.solc b/test/examples/cases/fresh-variable-shadowing.solc new file mode 100644 index 00000000..35d75fad --- /dev/null +++ b/test/examples/cases/fresh-variable-shadowing.solc @@ -0,0 +1,14 @@ +data Bool = False | True; + +function test(v0, p) { + match p { + | True => return False; + | z => return v0; + } +} + +contract FreshVariableShadowing { + function main() -> Bool { + test(True, False) + } +} diff --git a/test/examples/cases/join.solc b/test/examples/cases/join.solc index 3a20daa9..2e0386d6 100644 --- a/test/examples/cases/join.solc +++ b/test/examples/cases/join.solc @@ -14,6 +14,7 @@ contract Option { match mmx { | Some(Some(x)) => result = Some(x); | None => result = None; + | _ => result = None; } return result; } diff --git a/test/examples/cases/redundant-match.solc b/test/examples/cases/redundant-match.solc new file mode 100644 index 00000000..7d1d4a07 --- /dev/null +++ b/test/examples/cases/redundant-match.solc @@ -0,0 +1,13 @@ +data Bool = False | True; + + function f(x) { + match x { + | z => return z; + | True => return True; + | False => return False; + } + } + + contract Test { + function main() -> Bool { f(True) } + } diff --git a/test/examples/cases/snds.solc b/test/examples/cases/snds.solc new file mode 100644 index 00000000..6d25003a --- /dev/null +++ b/test/examples/cases/snds.solc @@ -0,0 +1,7 @@ + function snds (p1, p2) { + match p1, p2 { + | (a,b) , (c,d) => return (b,d); + } + } + + diff --git a/test/examples/cases/super-class.solc b/test/examples/cases/super-class.solc index dd85b793..c80f4af5 100644 --- a/test/examples/cases/super-class.solc +++ b/test/examples/cases/super-class.solc @@ -28,6 +28,7 @@ forall a . a : Eq => instance (List(a)) : Eq { | Nil, Nil => return True; | Cons(x,xs), Cons(y,ys) => return and(Eq.eq(x,y),Eq.eq(xs,ys)); + | _ , _ => return False; } } } diff --git a/test/examples/spec/034cojoin.solc b/test/examples/spec/034cojoin.solc index c77f07f9..e30ee48d 100644 --- a/test/examples/spec/034cojoin.solc +++ b/test/examples/spec/034cojoin.solc @@ -14,6 +14,7 @@ contract Option { let result = None; match mmx { | Some(Some(x)) => result = Some(x); + | Some(None) => result = None; | None => result = None; } return result; @@ -22,6 +23,7 @@ contract Option { function extract(mx) { match mx { | Some(x) => return x; + | None => return 0; } } diff --git a/test/examples/spec/037dwarves.solc b/test/examples/spec/037dwarves.solc index 8c12d410..dae322df 100644 --- a/test/examples/spec/037dwarves.solc +++ b/test/examples/spec/037dwarves.solc @@ -9,6 +9,7 @@ contract Dwarves { | Sleepy => return 3; | Bashful => return 4; | Happy => return 5; + | _ => return 0; } } diff --git a/test/examples/spec/903badassign.solc b/test/examples/spec/903badassign.solc index 933261d7..eae9a0b0 100644 --- a/test/examples/spec/903badassign.solc +++ b/test/examples/spec/903badassign.solc @@ -14,6 +14,7 @@ contract Option { let result = None; match mmx { | Some(Some(x)) => result = Some(x); + | Some(None) => result = None; | None => result = None; } return result;