intensional-datatys (empty) → 0.2.0.0
raw patch · 17 files changed
+2504/−0 lines, 17 filesdep +aesondep +basedep +containerssetup-changed
Dependencies added: aeson, base, containers, directory, extra, filepath, ghc, hashable, haskeline, intensional-datatys, mtl, unordered-containers
Files
- LICENSE +30/−0
- README.md +185/−0
- Setup.hs +2/−0
- benchmark/Benchmark.hs +66/−0
- intensional-datatys.cabal +119/−0
- profile/Profile.hs +81/−0
- src/Intensional.hs +235/−0
- src/Intensional/Constraints.hs +498/−0
- src/Intensional/Constructors.hs +130/−0
- src/Intensional/FromCore.hs +130/−0
- src/Intensional/Guard.hs +110/−0
- src/Intensional/InferCoreExpr.hs +301/−0
- src/Intensional/InferM.hs +247/−0
- src/Intensional/Scheme.hs +92/−0
- src/Intensional/Types.hs +180/−0
- src/Intensional/Ubiq.hs +18/−0
- test/PaperExamples.hs +80/−0
+ LICENSE view
@@ -0,0 +1,30 @@+Copyright Author name here (c) 2019++All rights reserved.++Redistribution and use in source and binary forms, with or without+modification, are permitted provided that the following conditions are met:++ * Redistributions of source code must retain the above copyright+ notice, this list of conditions and the following disclaimer.++ * Redistributions in binary form must reproduce the above+ copyright notice, this list of conditions and the following+ disclaimer in the documentation and/or other materials provided+ with the distribution.++ * Neither the name of Author name here nor the names of other+ contributors may be used to endorse or promote products derived+ from this software without specific prior written permission.++THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS+"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT+LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR+A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT+OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,+SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT+LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,+DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY+THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT+(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE+OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+ README.md view
@@ -0,0 +1,185 @@+# Intensional Datatype Refinement Checking++The pattern-match safety problem is to verify that a given functional program will never crash due to nonexhaustive+patterns in its function definitions. This tool is designed to verify pattern-match safety of Haskell programs.++Consider the following definition of formulas and disjunctive normal form (DNF) from [PaperExamples.hs](test/PaperExamples.hs):+````+ data Fm = + Lit L+ | Not Fm+ | And Fm Fm+ | Or Fm Fm+ | Imp Fm Fm++ distrib xss yss = List.nub [ List.union xs ys | xs <- xss, ys <- yss ]++ nnf2dnf (And p q) = distrib (nnf2dnf p) (nnf2dnf q)+ nnf2dnf (Or p q) = List.union (nnf2dnf p) (nnf2dnf q)+ nnf2dnf (Lit a) = [[a]]+ nnf2dnf _ = error "Impossible!"++ nnf' :: Fm -> Fm+ nnf' (And p q) = And (nnf' p) (nnf' q)+ nnf' (Or p q) = Or (nnf' p) (nnf' q)+ nnf' (Imp p q) = Or (Not (nnf' p)) (nnf' q) + nnf' (Not (Not p)) = nnf' p + nnf' (Not (And p q)) = Or (nnf' (Not p)) (nnf' (Not q))+ nnf' (Not (Or p q)) = And (nnf' (Not p)) (nnf' (Not q))+ nnf' (Not (Imp p q)) = And (nnf' p) (nnf' (Not q))+ nnf' (Not (Lit (Atom x))) = Lit (NegAtom x)+ nnf' (Not (Lit (NegAtom x))) = Lit (Atom x)+ nnf' (Lit (Atom x)) = Lit (Atom x)+ nnf' (Lit (NegAtom x)) = Lit (NegAtom x)++ dnf' = nnf2dnf . nnf'++````+The function ``nnf2dnf`` has only partial patterns, for example ``Imp p q`` is omitted, because it expects its argument to be in negation normal form and thus not contain any occurrences of ``Imp`` or ``Not``. However, the definition of ``dnf`` ensures that any input to ``nnf2dnf`` is of the correct form (assuming the definition of ``nnf'`` is correct). ++However, the definition of ``nnf'`` is not correct. Can you spot the error? Our tool can analyse how this program will behave at runtime and notices that ``nnf'`` can let a rogue ``Not`` through in some cases. In particular, the following use of ``dnf`` will result in the program crashing with a pattern-match exception:+````+ willCrash = + dnf' (Imp (Lit (Atom 1)) + (And (Lit (Atom 2)) + (Or (Lit (NegAtom 3)) (Lit (Atom 1)))))+````++When we try to compile this file with our plugin enabled, after a few milliseconds we get:++++The warning tells us that it is the ``Not`` created on line 60 that leaks out of the function (this is the ``Imp`` case of ``nnf``) and that the call on lines 73--76 (this is the definition of ``willCrash``) will cause that ``Not`` to reach the incomplete pattern match on lines 32--35 (this is the definition of ``nnf2dnf``).++On the other hand, the analysis also understands that the usage in the following definition will not exercise the faulty ``Imp`` case of ``nnf'`` and hence no warning is issued for this line of code:+````+ willNotCrash = dnf' (And (Lit (Atom 1)) (Lit (Atom 2)))+````++Internally, the tool is using a kind of refinement type system in order to statically approximate which constructors are flowing to which points of the program. The system is carefully designed so that inference is completely automatic and runs in time that is linear in the size of the program, but exponential in the underlying (Haskell) type of the program. In particular, it is exponential in the size of the datatype definitions, so the analysis may struggle if your program has very large datatypes. However, we have successfully analysed many large packages from Hackage (subject to the significant [limitations](#limitations) in the current implementation, discussed below).++The same example [file](test/PaperExamples.hs) also contains a non-faulty implementation ``nnf``. The type assigned to ``nnf`` describes a function that will never return a value built with ``Not`` or ``Implies`` (in fact the type is 'flow-sensitive' which means, in this case, that it says which constructors will be in the output given which constructors were in the input). Take a look at [Viewing the inferred types](#viewing-inferred-types) to see the type.++++## Usage++The tool is a plugin for GHC, and is integrated into the compilation pipeline. Since it depends on the GHC API directly, it is currently tied to GHC >= 8.6 and <=8.8.4 so first ensure you have a compatible version of the compiler.++### Invoke via GHC directly+To add the analysis to compilation using GHC directly from the command line, first install the ``intensional-datatys`` package from Hackage:+````+ $ cabal update+ Downloading the latest package list from hackage.haskell.org+ $ cabal install intensional-datatys+ Resolving dependencies...+````+Then use the flags ``-package intensional-datatys`` and ``-fplugin Intensional`` when invoking GHC as usual, e.g:+````+ $ ghc -package intensional-datatys -fplugin Intensional Main.hs+````+Optionally, add the flags detailed [here](#optional-ghc-flags) to the command line invocation to help the analysis efficiency or to view inferred types interactively.+++### Invoke via an (existing) Cabal project+To add this analysis as another stage to compilation for a Haskell project with a working cabal description+and access to Hackage:+ + 1. Add ``intensional-datatys`` to the ``build-depends`` field of the target that you want to analyse.+ 2. Add ``-fplugin Intensional`` to the ``ghc-options`` field+ 3. Optionally, add flags detailed [here](#optional-ghc-flags) to ``ghc-options`` to help the analysis efficiency or to view inferred types interactively.++### Interpreting the output +In the terminal you will find notifications of any warnings produced by the tool, which can be identified by the ``Intensional`` label in square brackets.++````+ test/PaperExamples.hs:(73,1)-(76,56): warning: [Intensional]+ Could not verify that ‘Not’ from test/PaperExamples.hs:60:21-34+ cannot reach the incomplete match at test/PaperExamples.hs:(32,1)-(35,39)+````++The warnings record instances where the tool *believes* there will be a pattern-match violation at runtime.+If there are no warnings, then the code has been verified as free from pattern-match safety violations at runtime, subject to the [limitations](#limitations) discussed below.++The first line of the warning gives the location of the error.+The second line of the warning gives a datatype constructor and the location in the source that the constructor is created.+The third line of the warning gives the location in the source code of an incomplete pattern.+The warning is being reported because, after analysing how the program will behave, the tool cannot exclude the possibility that the given incomplete pattern will not be matched to the given constructor at runtime, which result in an exception.+++### Optional GHC flags+ + We recommend the following additional flags which turn off inlining and other GHC optimisations whilst retaining strictness analysis.++ * ``-g``+ * ``-O0``+ * ``-fno-pre-inlining``+ * ``-funfolding-use-threshold=0``+ * ``-fno-ignore-interface-pragmas``+ * ``-fno-omit-interface-pragmas``+ + To view the types inferred for a module ``m`` or any module that ``m`` depends on, use the following flag and see section [Viewing Inferred Types](#viewing-inferred-types).++ * ``-fplugin-opt Intensional:m``+++## Limitations+As this is only a prototype tool, it's interface and deployment are not well developed! +In particular, many features of Haskell are not properly analysed, notably:+* Type classes+* GADTs+* Higher-ranked types++We do not analyse any code that is not from the home package (i.e. in the source files being compiled) and so we do not refine any types that are not defined in your program. For example, we do not track the control flow of ``Maybe`` or ``Bool``.++For efficiency, we do not allow empty refinements of single-constructor datatypes. This gives great savings when there are many newtypes, records and wrapper datatypes and are not a major concern of our work.++## Viewing inferred types+If the flag ``-fplugin-opt Intensional:m`` is used then, following the compilation of module ``m``, a very simple REPL will be presented from which you can issue commands to view inferred types of- or the GHC core associated with top-level functions.++* To view the type of a compiled module-level function ``f``, issue the command ``:t f``.+````+ Main> :t nnf+ nnf : forall X Y.inj_X Fm -> inj_Y Fm+ where+ [Imp] in X(Fm) ? Not <= X(Fm)+ [Imp] in X(Fm) ? Or <= Y(Fm)+ [Or] in X(Fm) ? Or <= Y(Fm)+ [And, Not] in X(Fm) ? Or <= Y(Fm)+ [And] in X(Fm) ? And <= Y(Fm)+ [Imp, Not] in X(Fm) ? And <= Y(Fm)+ [Not, Or] in X(Fm) ? And <= Y(Fm)+ [Lit, Not] in X(Fm), [NegAtom] in X(L) ? Lit <= Y(Fm)+ [Lit, Not] in X(Fm), [Atom] in X(L) ? Lit <= Y(Fm)+ [Lit] in X(Fm), [NegAtom] in X(L) ? Lit <= Y(Fm)+ [Lit] in X(Fm), [Atom] in X(L) ? Lit <= Y(Fm)+ [Lit, Not] in X(Fm), [NegAtom] in X(L) ? Atom <= Y(L)+ [Lit] in X(Fm), [Atom] in X(L) ? Atom <= Y(L)+ [Lit, Not] in X(Fm), [Atom] in X(L) ? NegAtom <= Y(L)+ [Lit] in X(Fm), [NegAtom] in X(L) ? NegAtom <= Y(L)+````+* To view the GHC Core associated with a module-level function ``f``, issue ``:c f``+````+ Main> :c dnf+ src<test/PaperExamples.hs:36:1-19>+ . @ Fm+ @ [[L]]+ @ Fm+ (src<test/PaperExamples.hs:36:7-13> nnf2dnf)+ (src<test/PaperExamples.hs:36:17-19> nnf)+````+* To resume compilation, issue ``:q ``.++Functions from module dependencies of ``m`` can also be queried by using their fully-qualified names.++ +## Troubleshooting ++* I get warnings about constructors created in typeclass functions that are not creating anything! + - See [limitations](#limitations), currently typeclass functions are overapproximated so the tool believes they return all constructors for the given type.++* I ran the tool and it seemed to compile without any warnings at all, but I was expecting some!+ - Are you sure that the source was actually compiled? The tool is part of the usual compilation pipeline, so if nothing changes in the source, GHC will not recompile the file.++* I can't seem to get the tool to work because of some Cabal dependency issues!+ - Perhaps you are not using GHC 8.8.3 or 8.8.4. Sorry about that, but the tool uses the GHC API directly, so the version is important.
+ Setup.hs view
@@ -0,0 +1,2 @@+import Distribution.Simple+main = defaultMain
+ benchmark/Benchmark.hs view
@@ -0,0 +1,66 @@+{-# LANGUAGE DeriveGeneric #-}++module Benchmark where++import System.Directory+import System.FilePath as Path+import Data.Aeson as Aeson+import Data.Map (Map)+import qualified Data.Map as Map+import qualified Data.List as List+import qualified Control.Monad as Monad+import GHC.Generics (Generic)+import qualified GHC.Generics as Generics+import Numeric (showFFloat)++import Intensional++emptyMark :: Benchmark+emptyMark = Benchmark [] 0 0 0 0 0 0++plusMark :: Benchmark -> Benchmark -> Benchmark+b `plusMark` c =+ b {+ avg = avg b + avg c,+ bigN = bigN b + bigN c,+ bigK = max (bigK b) (bigK c),+ bigD = max (bigD b) (bigD c),+ bigV = bigV b + bigV c,+ bigI = max (bigI b) (bigI c)+ }++summaryMark :: Map String Benchmark -> Benchmark+summaryMark = foldr plusMark emptyMark ++showMark :: Map String Benchmark -> String+showMark bm =+ unlines $ pre ++ titles : Map.foldrWithKey (\k v ss -> entry k v : ss) post bm+ where+ pre = ["\\begin{tabular}{|l|l|l|l|l|l|l|}", "\\hline"]+ titles = concat $ List.intersperse " & " ["Name", "N", "K", "V", "D", "I", "Time (ms)"] ++ ["\\\\\\hline"]+ entry n b = concat $ List.intersperse " & " [n, show $ bigN b, show $ bigK b, show $ bigV b, show $ bigD b, show $ bigI b, showFFloat (Just 2) (fromIntegral (avg b) / fromIntegral 1000000) ""] ++ ["\\\\\\hline"]+ post = ["\\end{tabular}"]++putMark :: FilePath -> Map String Benchmark -> IO ()+putMark fp bm = + writeFile fp (showMark bm)++convertMark :: FilePath -> IO ()+convertMark fp =+ do mbm <- decodeFileStrict fp+ case mbm of+ Nothing -> return ()+ Just bm -> putMark "test.tex" bm++summariseMarks :: FilePath -> IO ()+summariseMarks dir =+ withCurrentDirectory dir $+ do curDir <- getCurrentDirectory+ jsons <- filter ("json" `Path.isExtensionOf`) <$> listDirectory curDir+ Just bms <- sequence <$> mapM decodeFileStrict jsons+ -- associate the package names with summaries+ let summaries = + Map.fromList $ zipWith (\j bm -> (Path.dropExtension j, summaryMark bm)) jsons bms+ putMark "summary.tex" summaries+ Monad.zipWithM_ (\j bm -> putMark (Path.replaceExtension j ".tex") bm) jsons bms+
+ intensional-datatys.cabal view
@@ -0,0 +1,119 @@+cabal-version: 3.0++name: intensional-datatys+version: 0.2.0.0+synopsis: A GHC Core plugin for intensional datatype refinement checking+description: Please see the README on GitHub at <https://github.com/bristolpl/intensional-datatys#readme>+homepage: https://github.com/bristolpl/intensional-datatys#readme+bug-reports: https://github.com/bristolpl/intensional-datatys/issues+category: Language+author: Eddie Jones, Steven Ramsay+maintainer: ej16147@bristol.ac.uk, steven.ramsay@bristol.ac.uk+copyright: 2019 Eddie Jones, Steven Ramsay+license: BSD-3-Clause+license-file: LICENSE+build-type: Simple+extra-source-files:+ README.md++source-repository head+ type: git+ location: https://github.com/bristolpl/intensional-datatys++flag bbenchmarks+ description: Build the benchmark management script+ default: False+ manual: True++library+ exposed-modules:+ Intensional+ other-modules:+ Intensional.Types+ Intensional.Constructors+ Intensional.Constraints+ Intensional.Guard+ Intensional.Scheme+ Intensional.InferM+ Intensional.FromCore+ Intensional.InferCoreExpr+ Intensional.Ubiq+ hs-source-dirs:+ src+ cpp-options:+ -- -DDEBUG+ ghc-options:+ -Wall+ -Wcompat+ -Wincomplete-record-updates+ -Wincomplete-uni-patterns+ -Wredundant-constraints+ -Wnoncanonical-monad-instances+ build-depends:+ base >=4 && <5+ , ghc >=8.6.0 && <=8.8.4+ , extra ==1.7.4+ , containers ==0.6.2.1+ , unordered-containers ==0.2.11.0+ , mtl ==2.2.2+ , hashable ==1.3.0.0+ , aeson ==1.5.2.0+ , directory ==1.3.6.0+ , filepath ==1.4.2.1+ , haskeline ==0.7.5.0+ default-language: Haskell2010++test-suite test+ type: exitcode-stdio-1.0+ main-is: PaperExamples.hs+ hs-source-dirs:+ test+ ghc-options: + -g + -fno-pre-inlining + -funfolding-use-threshold=0 + -fno-ignore-interface-pragmas + -fno-omit-interface-pragmas+ -fplugin Intensional+ build-depends:+ base >=4 && <5+ , intensional-datatys+ default-language: Haskell2010++-- A library intended to be used from GHCI+-- to manage benchmarks for the associated paper+library benchmark+ if flag(bbenchmarks)+ buildable:True+ else+ buildable:False+ exposed-modules:+ Benchmark+ build-depends:+ base >=4+ , aeson ==1.5.2.0+ , containers ==0.6.2.1+ , intensional-datatys+ , filepath ==1.4.2.1+ , directory ==1.3.6.0+ hs-source-dirs:+ benchmark+ default-language: Haskell2010++-- Requires ghc 8.8+-- Needs manual tailoring to your+-- particular system, so disabled by+-- default.+executable profile+ ghc-options:+ buildable: False+ build-depends:+ base >=4 && <5+ , ghc >= 8.8+ , filepath ==1.4.2.1+ , directory ==1.3.6.0+ , intensional-datatys+ hs-source-dirs:+ profile+ main-is: Profile.hs+ default-language: Haskell2010
+ profile/Profile.hs view
@@ -0,0 +1,81 @@+module Main where++import Control.Monad+import Control.Monad.IO.Class+import DynFlags+import EnumSet+import GHC+import Intensional+import Plugins+import System.Directory+import System.Environment+import System.FilePath.Posix+import System.IO+import System.Timeout+import CmdLineParser++data Mode+ = Profile+ | BenchmarkInit+ | Benchmark+ deriving (Eq)++compileWithPlugin :: Mode -> IO ()+compileWithPlugin m = do+ args <- words <$> readFile "profile/self-args"+ runGhc (Just "/opt/ghc/8.8.3/lib/ghc-8.8.3") $ do+ df1 <- getSessionDynFlags+ (df2, leftover, ws) <-+ parseDynamicFlags+ df1+ { -- ghcLink = NoLink,+ -- optLevel = 0,+ -- enableTimeStats = m == Profile,+ -- generalFlags = fromList (Opt_ForceRecomp : [Opt_SccProfilingOn | m == Profile]),+ -- profAuto = if m == Profile then NoProfAuto else ProfAutoAll,+ staticPlugins =+ [ StaticPlugin+ ( PluginWithArgs+ plugin+ ( "suppress-output"+ : case m of+ Profile -> []+ Benchmark -> ["benchmark"]+ BenchmarkInit -> ["benchmark'"]+ )+ )+ ]+ }+ (map noLoc args)+ liftIO $ mapM_ (print . warnReason) ws+ setSessionDynFlags df2+ mapM ((`guessTarget` Nothing) . unLoc) leftover >>= setTargets+ void $ load LoadAllTargets++main :: IO ()+main = do+ args <- getArgs+ case args of+ ["-p", file] -> do+ -- requires +RTS -pj -l-au+ compileWithPlugin Profile+ renameFile "profile.prof" ("profile/" ++ takeBaseName file ++ ".prof")+ removeFile "profile.eventlog"+ ["-b"] -> benchmark+ -- listDirectory "test/XMonad" >>= benchmark . fmap ("test/XMonad/" ++)+ -- ("-b" : files) -> benchmark -- Run benchmarks on particular files+ _ -> putStrLn "Invalid command line argument!"+ where+ benchmark :: IO ()+ benchmark = do+ -- appendFile "benchmarks" ("Running: " ++ file ++ "\n")+ b <- timeout 10000000 (compileWithPlugin BenchmarkInit)+ case b of+ Nothing -> return ()+ Just _ -> loop 9+ loop 0 = return ()+ loop n = do+ b <- timeout 10000000 (compileWithPlugin Benchmark)+ case b of+ Nothing -> return ()+ Just _ -> loop (n - 1)
+ src/Intensional.hs view
@@ -0,0 +1,235 @@+{-# LANGUAGE BangPatterns #-}+{-# LANGUAGE DeriveGeneric #-}+{-# LANGUAGE LambdaCase #-}+{-# LANGUAGE ViewPatterns #-}++module Intensional (plugin, Benchmark(..)) where++import BinIface+import Binary+import Intensional.Constructors+import Intensional.Constraints+import Intensional.Types+import Control.Monad+import Data.Aeson+import qualified Data.Map as Map+import qualified Data.List as List+import GhcPlugins+import IfaceEnv+import IfaceSyn+import Intensional.InferCoreExpr+import Intensional.InferM+import System.CPUTime+import System.Directory+import TcIface+import TcRnMonad+import ToIface+import TyCoRep+import PprColour+import Pretty (Mode(..))+import OccName+import NameCache (OrigNameCache)+import GHC.Generics (Generic)+import System.IO+import qualified System.Console.Haskeline as Haskeline++{-|+ The GHC plugin is hardwired as @plugin@. +-}+plugin :: Plugin+plugin = + defaultPlugin {+ pluginRecompile = recomp, + installCoreToDos = install+ }+ where+ recomp cmd =+ return $ if "force" `elem` cmd then ForceRecompile else NoForceRecompile + todoPrefix cmd = [ + CoreDoStrictness, -- it is useful to know what is bottom for the purpose of pattern failures+ CoreDoPluginPass "Intensional" (inferGuts cmd)+ ]+ install cmd todo = return (todoPrefix cmd ++ todo)++{-|+ Given a module name @m@, @interfaceName m@ is the file path+ that will be written with the corresponding serialised typings.+-}+interfaceName :: ModuleName -> FilePath+interfaceName = ("interface/" ++) . moduleNameString++inferGuts :: [CommandLineOption] -> ModGuts -> CoreM ModGuts+inferGuts cmd guts@ModGuts {mg_deps = d, mg_module = m, mg_binds = p} = do+ when ("debug-core" `elem` cmd) $ pprTraceM "Core Source:" $ ppr p+ hask <- getHscEnv+ che <- getOrigNameCache + dflags <- getDynFlags + liftIO $ do+ -- Reload saved typeschemes+ let gbl =+ IfGblEnv { + if_doc = text "initIfaceLoad",+ if_rec_types = Nothing+ }+ env <- + initTcRnIf 'i' hask gbl (mkIfLclEnv m empty False) $ do+ cache <- mkNameCacheUpdater+ foldM+ ( \env (interfaceName -> m_name, _) -> do+ exists <- liftIO $ doesFileExist m_name+ if exists+ then do+ bh <- liftIO $ readBinMem m_name+ ictx <- liftIO $ Map.fromList <$> getWithUserData cache bh+ ctx <- mapM (mapM tcIfaceTyCon) ictx+ return (Map.union ctx env)+ else return env+ )+ Map.empty+ (dep_mods d)+ t0 <- getCPUTime+ -- Infer constraints+ let (!gamma, !errs, !stats) = runInferM (inferProg p) m env+ t1 <- getCPUTime+ when ("time" `elem` cmd) $+ recordBenchmarks (moduleNameString (moduleName m)) (t0, t1) stats+ -- Display type errors+ let printErrLn = + printSDocLn PageMode dflags stderr (setStyleColoured True $ defaultErrStyle dflags)+ mapM_ (\a -> when (m == modInfo a) $ printErrLn (showTypeError a)) errs+ -- Save typeschemes to interface file+ when (moduleNameString (moduleName m) `elem` cmd) $ + repl (gamma Prelude.<> env) m p che+ exist <- doesDirectoryExist "interface"+ unless exist (createDirectory "interface")+ bh <- openBinMem (1024 * 1024)+ putWithUserData+ (const $ return ())+ bh+ (Map.toList $ Map.filterWithKey (\k _ -> isExternalName k) (fmap toIfaceTyCon <$> gamma))+ writeBinMem bh (interfaceName (moduleName m))+ return guts++{-|+ When @cx@ is the type bindings for all the program so far and @md@+ is the currently processed module and @ch@ is GHC's name cache,+ @repl cx md ch@ is a read-eval-print-loop IO action, allowing the + user to inspect individual type bindings and output the raw core.+-}+repl :: Context -> Module -> CoreProgram -> OrigNameCache -> IO ()+repl cx md pr ch =+ Haskeline.runInputT Haskeline.defaultSettings loop+ where+ loop = + do mbInput <- Haskeline.getInputLine (modn ++ "> ") + case words <$> mbInput of+ Just [":q"] -> return ()+ Just [":c", strName] -> + do case mkName strName of+ Just n | Just e <- List.lookup n (map (\(x,y) -> (getName x, y)) $ flattenBinds pr) ->+ Haskeline.outputStrLn $ showSDocUnsafe $ ppr e+ _ -> return ()+ loop+ Just [":t", strName] ->+ do case mkName strName of+ Just n | Just ts <- Map.lookup n cx -> + Haskeline.outputStrLn $ showSDocUnsafe $ typingDoc n ts+ _ -> return ()+ loop+ _ -> loop+ typingDoc n ts = ppr n <+> colon <+> prpr (const empty) ts + modn = moduleNameString (moduleName md)+ mkName s = lookupOrigNameCache ch m n+ where + s' = reverse s+ (n', m') = Prelude.span (\c -> c /= '.') s'+ n = mkOccName OccName.varName (reverse n')+ m = if null m' then + md + else + md {moduleName = mkModuleName $ reverse (drop 1 m')}++++{-|+ Given a trivially unsat constraint @a@, @showTypeError a@ is the + message that we will print out to the user as an SDoc.+-}+showTypeError :: Atomic -> SDoc+showTypeError a =+ blankLine + $+$ (coloured (colBold Prelude.<> colWhiteFg) $ hang topLine 2 (hang msgLine1 2 msgLine2))+ $+$ blankLine+ where+ topLine = + (ppr $ spanInfo a) GhcPlugins.<> colon + <+> coloured (sWarning defaultScheme) (text "warning:")+ <+> lbrack GhcPlugins.<> coloured (sWarning defaultScheme) (text "Intensional") GhcPlugins.<> rbrack+ msgLine1 = + text "Could not verify that" <+> quotes (ppr $ left a) + <+> text "from" + <+> (ppr $ getLocation (left a)) + msgLine2 = text "cannot reach the incomplete match at"+ <+> (ppr $ getLocation (right a))++{-|+ Given a GHC interface tycon representation @iftc@,+ @tcIFaceTyCon iftc@ is the action that returns the original tycon.+-}+tcIfaceTyCon :: IfaceTyCon -> IfL TyCon+tcIfaceTyCon iftc = do+ e <- tcIfaceExpr (IfaceType (IfaceTyConApp iftc IA_Nil))+ case e of+ Type (TyConApp tc _) -> return tc+ _ -> pprPanic "TyCon has been corrupted!" (ppr e)++data Benchmark = + Benchmark { + times :: [Integer],+ avg :: Integer,+ bigN :: Int,+ bigK :: Int,+ bigD :: Int,+ bigV :: Int,+ bigI :: Int+ }+ deriving (Generic)++instance ToJSON Benchmark+instance FromJSON Benchmark++{-|+ Given the name of a benchmark @n@ and a beginning @t0@ and end + time @t1@ and statistics @ss@ on the run, @recordBenchmarks n (t0, t1) ss@+ is the IO action that writes the benchmark data to a JSON file.+-}+recordBenchmarks :: String -> (Integer, Integer) -> Stats -> IO ()+recordBenchmarks name (t0, t1) stats = do+ exist <- doesFileExist "benchmark.json"+ if exist+ then+ decodeFileStrict "benchmark.json" >>= \case+ Nothing ->+ encodeFile "benchmark.json" (Map.singleton name new)+ Just bs ->+ case Map.lookup name bs of+ Nothing ->+ encodeFile "benchmark.json" (Map.insert name new bs)+ Just bench -> do+ let bench' = updateAverage $ bench {times = (t1 - t0) : times bench}+ encodeFile "benchmark.json" (Map.insert name bench' bs)+ else encodeFile "benchmark.json" (Map.singleton name new)+ where+ updateAverage b =+ b {avg = sum (times b) `div` toInteger (length (times b))}+ new =+ Benchmark+ { + bigN = getN stats,+ bigD = getD stats,+ bigV = getV stats,+ bigK = getK stats,+ bigI = getI stats,+ times = [t1 - t0],+ avg = t1 - t0+ }
+ src/Intensional/Constraints.hs view
@@ -0,0 +1,498 @@+{-# OPTIONS_HADDOCK ignore-exports #-}+{-# OPTIONS_GHC -Wno-orphans #-} -- the Foldable instance for GHC.UniqFM is an orphan+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE DeriveFoldable #-}+{-# LANGUAGE DeriveFunctor #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE GADTs #-}++{-|+ Atomic constraints and sets of atomic constraints, represented as antichains. Saturation and restriction. +-}+module Intensional.Constraints+ ( + CInfo(..),+ modInfo,+ spanInfo,+ Atomic,+ Constraint (..),+ ConstraintSet,+ insert,+ guardWith,+ toList,+ fromList,+ isTriviallyUnsat,+ unsats,+ saturate,+ cexs,+ size,+ )+where++import Binary+import Data.Foldable+import Control.Monad.State (State)+import Data.Set (Set)+import qualified Data.Set as Set+import Data.Map.Strict (Map)+import qualified Data.Map.Strict as Map+import Data.IntMap (IntMap)+import Data.HashMap.Strict (HashMap)+import Data.IntSet (IntSet)+import qualified Control.Monad.State as State+import qualified Data.HashMap.Strict as HashMap+import qualified Data.IntMap as IntMap+import qualified Data.IntSet as IntSet+import qualified Data.Maybe as Maybe+import qualified GhcPlugins as GHC+import qualified Control.Monad as Monad++import Intensional.Ubiq+import Intensional.Types+import Intensional.Constructors+import Intensional.Guard (Guard)+import qualified Intensional.Guard as Guard++import Debug.Trace+++{-| + Type type of auxilliary information attached to + constraints @c@:++ * @prov c@ is the module in which the constraint was created+ * @span c@ is the originating location of the rhs of the constraint+ + INV: CInfo does not determine equality of constraints.+-}+data CInfo =+ CInfo {+ prov :: GHC.Module,+ sspn :: GHC.SrcSpan+ }+ deriving (Eq, Ord)++instance GHC.Outputable CInfo where+ ppr (CInfo _ sp) = GHC.ppr sp++instance Binary CInfo where+ put_ bh (CInfo m sp) = put_ bh m >> put_ bh sp + get bh = Monad.liftM2 CInfo (get bh) (get bh)+ ++{-|+ The type of constraints @c@ of shape @guard c@ ? @left c@ ⊆ @right c@ that originated from the + source at @srcSpan c@.+-}+type Atomic = Constraint 'L 'R++data Constraint l r+ = Constraint+ { left :: K l,+ right :: K r,+ guard :: Guard,+ cinfo :: CInfo+ }++instance Eq (Constraint l r) where+ -- Disregard info in comparison+ Constraint l r g _ == Constraint l' r' g' _ = l == l' && r == r' && g == g'++instance GHC.Outputable (Constraint l r) where+ ppr = prpr GHC.ppr++instance (Binary (K l), Binary (K r)) => Binary (Constraint l r) where+ put_ bh (Constraint l r g ss) = put_ bh l >> put_ bh r >> put_ bh g >> put_ bh ss+ get bh = Constraint <$> Binary.get bh <*> Binary.get bh <*> Binary.get bh <*> Binary.get bh++instance Refined (Constraint l r) where+ domain c = domain (left c) <> domain (right c) <> domain (guard c)+ rename x y c =+ c+ { left = rename x y (left c),+ right = rename x y (right c),+ guard = rename x y (guard c)+ }+ prpr m a = prpr m (guard a) GHC.<+> GHC.char '?' GHC.<+> prpr m (left a) GHC.<+> GHC.text "<=" GHC.<+> prpr m (right a)++modInfo :: Atomic -> GHC.Module+modInfo = prov . cinfo++spanInfo :: Atomic -> GHC.SrcSpan+spanInfo = sspn . cinfo++{-|+ Given an atomic constraint @a@, @isTriviallyUnsat a@ just if @a@ is of the form G ? k in {}.+-}+isTriviallyUnsat :: Atomic -> Bool+isTriviallyUnsat a =+ case (Guard.isEmpty (guard a), left a, right a) of+ (True, Con _ _, Set ks _) | GHC.isEmptyUniqSet ks -> True+ (_, _, _ ) -> False++headVar :: Atomic -> Maybe (Int, GHC.Name)+headVar a = + case right a of+ Dom (Inj x d) -> Just (x, d)+ Set _ _ -> Nothing+ _ -> error "Not possible!"++bodyVars :: Atomic -> Set (Int, GHC.Name) +bodyVars a = gVars <> lVars+ where+ gVars = Guard.typedVars (guard a)+ lVars = + case left a of+ Dom (Inj x d) -> Set.singleton (x, d)+ Con _ _ -> Set.empty+ _ -> error "Not possible!"++{-|+ Given two atomic constraints @a@ and @b@, @a `impliedBy` b@ just+ if @a@ and @b@ have the same body and the guard of @a@ is implied+ by the guard of @b@.+-}+impliedBy :: Atomic -> Atomic -> Bool+impliedBy a a' =+ left a == left a' && right a == right a' && guard a `Guard.impliedBy` guard a'++{-|+ Given an atomic constraint @a@, @tautology a@ just if @a@ is satisfied in + every assignment.+-}+tautology :: Atomic -> Bool+tautology a =+ case left a of+ Dom d ->+ case right a of+ Dom d' -> d == d'+ _ -> False+ Con k _ ->+ case right a of+ Dom (Inj x d) ->+ case Guard.lookup x d (guard a) of+ Just ks -> GHC.elementOfUniqSet k ks+ Nothing -> False+ Set ks _ -> GHC.elementOfUniqSet k ks+ _ -> error "[ERROR] Unexpected right atom"+++{-|+ When @m@ is the current module:+ Given atomic constraints @a@ and @b@, @resolve m a b@ is:++ * @Nothing@ if the resolvant of @a@ and @b@ is a tautology+ * @Just r@ otherwise, where @r@ is the resolvant as an atomic constraint+-}+resolve :: CInfo -> Atomic -> Atomic -> Maybe Atomic+resolve ci l r =+ -- simplify the the new constraint if it's body contains two literals+ case (left newR, right newR) of+ (Con k _, Set ks _) | GHC.elementOfUniqSet k ks -> Nothing+ (Con _ _, Set _ s) | otherwise -> Just (newR { right = Set mempty s})+ (_, _ ) -> Just newR+ where+ weaken x d y g = + -- weaken x(d) in g to y(d)+ case Guard.lookup x d g of+ Just ms | ks <- GHC.nonDetEltsUniqSet ms -> + Just (Guard.singleton ks y d <> Guard.deleteAll ks x d g)+ Nothing -> Nothing+ satisfy x d k g =+ -- satisfy x(d) in g by k+ case Guard.lookup x d g of+ Just ks | k `GHC.elementOfUniqSet` ks -> Just (Guard.delete k x d g)+ _ -> Nothing+ mbNewGuard = + -- create a new guard by modifying the old one according to+ -- saturation and weakening (ignoring l's guard, for now)+ case (left l, right l) of + (Dom (Inj y _), Dom (Inj x d)) -> weaken x d y (guard r)+ (Con k _, Dom (Inj x d)) -> satisfy x d k (guard r)+ (_, _ ) -> Nothing+ mbNewLeft = + -- apply transitivity, or not (ignoring l's guard, for now)+ case (right l, left r) of+ (Dom (Inj x d), Dom (Inj z d')) | z == x && d == d' -> Just (left l)+ (_, _ ) -> Nothing+ newR = + -- determine whether or not to attach a single copy of l's guards+ case (mbNewGuard, mbNewLeft) of+ (Just grd, Just lft) -> r { left = lft, guard = guard l <> grd, cinfo = ci }+ (Just grd, Nothing ) -> r { guard = guard l <> grd, cinfo = ci }+ (Nothing, Just lft) -> r { left = lft, guard = guard l <> guard r, cinfo = ci }+ (Nothing, Nothing ) -> r+ +-- We only use ConstraintSetF with Atomic so far, but it is worth making+-- this structure clear to derive Foldable etc+-- TODO: Remove these hashmaps in favour of IntMaps+data ConstraintSetF a+ = ConstraintSetF+ { + -- constraints of the form GS ? Y(d) <= Y(d)+ -- represented as X -> (d -> (Y -> GS)) + definiteVV :: IntMap (GHC.NameEnv (HashMap Int [a])),+ -- constraints of the form GS ? k in X(d)+ -- represented as X -> (d -> (k -> GS))+ definiteKV :: IntMap (GHC.NameEnv (HashMap GHC.Name [a])),+ -- constraints of the form G ? S1 <= {k1,...,km}+ -- represented as a list+ goal :: [a],+ -- a reverse lookup to find all those constraints+ -- that have a given sorted variable X(d) in front of+ -- the head (i.e. eligible for saturation on the right)+ revMap :: Map (Int, GHC.Name) [Atomic]+ }+ deriving (Eq, Functor, Foldable)++{-|+ The type of sets of constraints. + + We say that a set of constraints @cs@ is /reduced/ just if, + for all X, d, Y, k:+ @definiteVV cs X d Y@, @definiteKV cs X d k@ and @goal cs@+ are non-increasing lists wrt @impliedBy@.++ We say that a set of constraints @cs@ is an /antichain/ just if+ each of these lists are also non-decreasing.++ Most sets of constraints we process are reduced, but we allow+ non-reduced constraint sets to occur as a consequence of renaming+ of variables.++ Many sets of constraints are also antichains, + for example, when filtering a reduced constraint set one can+ guarantee the new constraint set will be an antichain by using+ @insert@ and constructing the new constraint set in the + reverse order. Constraint sets returned from saturation will + always be antichains.+-}+type ConstraintSet = ConstraintSetF Atomic++instance Foldable GHC.UniqFM where+ foldr = GHC.foldUFM ++{-|+ Given a list of atomic constraints @cs@, @fromList cs@ is+ largest antichain contained in @cs@+-}+fromList :: [Atomic] -> ConstraintSet+fromList = foldr insert empty++instance Semigroup ConstraintSet where+ cs <> ds = foldr insert ds cs++instance Monoid ConstraintSet where+ mempty = empty++instance GHC.Outputable ConstraintSet where+ ppr = prpr GHC.ppr++instance Binary ConstraintSet where+ put_ bh = put_ bh . toList+ get bh = fromList <$> get bh++instance Refined ConstraintSet where+ domain = foldMap domain+ rename x y = + -- this may create non-reduced constraint sets+ foldl' (\ds a -> unsafeInsert (rename x y a) ds) empty+ prpr m = foldr ((GHC.$$) . prpr m) GHC.empty+++{-|+ @empty@ is the empty constraint set+-}+empty :: ConstraintSet+empty =+ ConstraintSetF+ { + definiteVV = mempty,+ definiteKV = mempty,+ goal = [],+ revMap = mempty+ }++{-|+ Given a constraint set @cs@, @unsats cs@ is the constraint set + consisting of just those trivially unsatisfiable constraints in @cs@.+-}+unsats :: ConstraintSet -> ConstraintSet+unsats cs = + mempty { goal = filter isTriviallyUnsat (goal cs) }++{-| + When @cs@ is a constraint set, @size cs@ is its cardinality.+-}+size :: ConstraintSet -> Int+size = foldl' (\sz _ -> 1 + sz) 0++{-| + When @a@ is an atomic constraint and @cs@ a constraint set,+ @unsafeInsert a cs@ is the constraint set obtained by inserting+ @a@ into @cs@. + + Note: @unsafeInsert a cs@ may not be reduced even if @cs@ is.+-}+unsafeInsert :: Atomic -> ConstraintSet -> ConstraintSet+unsafeInsert a cs =+ fwd { revMap = Set.foldl' (\m (x,d) -> Map.insertWith (++) (x,d) [a] m) (revMap fwd) (bodyVars a) }+ where+ fwd = + case (left a, right a) of+ (Dom (Inj x _), Dom (Inj y yd)) ->+ let ne = IntMap.findWithDefault mempty y (definiteVV cs)+ hm = GHC.lookupWithDefaultUFM ne mempty yd+ as = HashMap.findWithDefault [] x hm+ in cs {definiteVV = IntMap.insert y (GHC.addToUFM ne yd (HashMap.insert x (a : as) hm)) (definiteVV cs)}+ (Con k _, Dom (Inj y yd)) ->+ let ne = IntMap.findWithDefault mempty y (definiteKV cs)+ hm = GHC.lookupWithDefaultUFM ne mempty yd+ as = HashMap.findWithDefault [] k hm+ in cs {definiteKV = IntMap.insert y (GHC.addToUFM ne yd (HashMap.insert k (a : as) hm)) (definiteKV cs)}+ (_, Set _ _) -> cs {goal = a : goal cs}+ (_, _) -> cs++{-| + When @a@ is an atomic constraint and @cs@ is a constraint antichain + @insert a cs@ is: + + * @Nothing@ just if @a@ is already implied by some constraint in @cs@.+ * @Just ds@ otherwise, where @ds@ is the constraint antichain obtained + by inserting @a@ into @cs@. Note: @ds@ may be smaller than @cs@.+-}+insert' :: Atomic -> ConstraintSet -> Maybe ConstraintSet+insert' a cs | not (tautology a) =+ case mbFwd of+ Just fwd -> Just $ fwd { revMap = Set.foldl' (\m (x,d) -> Map.insertWith (++) (x,d) [a] m) (revMap fwd) (bodyVars a) }+ Nothing -> Nothing+ where+ mbFwd = + case (left a, right a) of+ (Dom (Inj x _), Dom (Inj y yd)) ->+ let ne = IntMap.findWithDefault mempty y (definiteVV cs)+ hm = GHC.lookupWithDefaultUFM ne mempty yd+ as = HashMap.findWithDefault [] x hm+ in fmap (\as' -> cs {definiteVV = IntMap.insert y (GHC.addToUFM ne yd (HashMap.insert x as' hm)) (definiteVV cs)}) (maintain as)+ (Con k _, Dom (Inj y yd)) ->+ let ne = IntMap.findWithDefault mempty y (definiteKV cs)+ hm = GHC.lookupWithDefaultUFM ne mempty yd+ as = HashMap.findWithDefault [] k hm+ in fmap (\as' -> cs {definiteKV = IntMap.insert y (GHC.addToUFM ne yd (HashMap.insert k as' hm)) (definiteKV cs)}) (maintain as)+ (_, Set _ _) ->+ fmap (\as' -> cs {goal = as'}) (maintain (goal cs))+ (_, _) -> Nothing -- Ignore constraints concerning base types+ maintain ds =+ if any (a `impliedBy`) ds then Nothing else Just (a : ds)+insert' _ _ = Nothing++{-| + When @a@ is an atomic constraint and @cs@ is a constraint set+ @insert a cs@ is the constraint set obtained by inserting @a@+ into @cs@.++ If @cs@ is reduced then so is @insert a cs@. However, @insert a cs@ + may not be an antichain even when @cs@ is.+-}+insert :: Atomic -> ConstraintSet -> ConstraintSet+insert a cs = Maybe.fromMaybe cs (insert' a cs)++{-|+ When @g@ is a guard and @cs@ a set of constraints, @guardWith g cs@ is + the set of constraints obtained from @cs@ by appending @g@ to every guard+ of every constraint.+-}+guardWith :: Guard -> ConstraintSet -> ConstraintSet+guardWith g =+ foldl' (\ds a -> insert (a { guard = g <> guard a }) ds) mempty++{-|+ When @iface@ is a set of interface variables and @ci@ is the current ctx + and @cs@ is a constraint set, @saturate ci iface cs@ is the constraint set + obtained from @cs@ by saturation and restriction to @iface@.+-}+saturate :: CInfo -> IntSet -> ConstraintSet -> ConstraintSet+saturate ci iface cs = + es+ where+ ls = foldl' (\ms c -> if eligible iface c then unsafeInsert c ms else ms) mempty cs+ ds = snd $ State.execState (fix ci iface) (ls, cs)+ -- doing foldl with insert here will guarantee the result is an antichain+ es = foldl' (\fs a -> if domain a `IntSet.isSubsetOf` iface then insert a fs else fs) mempty ds+++{-|+ Given a set of interface variables @exts@ and a constraint @c@,+ @eligible exts c@ just if there are no interface variables in the+ head of @c@ and only interface variables elsewhere in @c@.++ (This means it is eligible to be used as the left-constraint in a+ resolution step.)+-}+eligible :: IntSet -> Atomic -> Bool+eligible exts c = + domain (guard c) `IntSet.isSubsetOf` exts + && domain (left c) `IntSet.isSubsetOf` exts+ && not (domain (right c) `IntSet.isSubsetOf` exts)++{-|+ Given some context @ci@ and constraints @cs@ attempt to build+ a model of @cs@. @cexs ci cs@ is the set of + trivially unsatisfiable constrants obtained from the candidate model.+-}+cexs :: CInfo -> ConstraintSet -> ConstraintSet +cexs ci = saturate ci mempty++{-| + When @exts@ is the set of interface variables and @ci@ is the current + ctx @fix ci exts@ is the stateful computation that transforms an + initial state @(ls, rs)@ where @ls@ are all unit constraints modulo + @exts@ and @ls@ is contained in @rs@, into a final state @(ls', rs')@ + in which @ls@ is empty and @rs'@ is the saturation of @rs@.+-}+fix :: CInfo -> IntSet -> State (ConstraintSet, ConstraintSet) ()+fix ci exts =+ do (ls, rs) <- State.get+ Monad.when debugging $ + traceM ("#ls = " ++ show (size ls) ++ ", #rs = " ++ show (size rs))+ Monad.unless (null ls) $ saturate1 ci exts >> fix ci exts++{-| + When @exts@ is a set of interface variables and @ci@ is the current ctx+ @saturate1 ci exts@ is the stateful computation that takes an initial state + @(ls, rs)@ consisting of a pair of constraint sets with @ls@ being unit + clauses modulo `exts` and @ls@ being contained in @rs@ to a final state + @(ls', rs')@ in which:++ * @ls'@ is those constraints in @rs'@ that are not in @rs@ and which + are unit modulo @exts@.+ * @rs'@ contains all the constraints obtained from @rs@ by resolving + on the left with each clauses from @ls@ once.+-}+saturate1 :: CInfo -> IntSet -> State (ConstraintSet, ConstraintSet) ()+saturate1 ci exts =+ do (ls, rs) <- State.get+ State.put (mempty, rs)+ Monad.forM_ ls $ \l ->+ do -- We immediately get the current state to allow+ -- for two left constraints to be applied to the+ -- same right constraint+ rs' <- State.gets snd+ -- This is guaranteed by varsAllExts+ case headVar l of+ Nothing -> error "impossible"+ Just (x,d) -> + Monad.forM_ (Map.findWithDefault [] (x,d) $ revMap rs') $ \r -> + addResolvant (resolve ci l r)+ where+ addResolvant Nothing = return ()+ addResolvant (Just r) =+ do (ls, rs) <- State.get+ case insert' r rs of+ Nothing -> return ()+ Just rs' -> + -- Insert the new constraint into ls only if it is a + -- unit clause modulo externals.+ State.put (if eligible exts r then insert r ls else ls, rs')+
+ src/Intensional/Constructors.hs view
@@ -0,0 +1,130 @@+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE KindSignatures #-}+{-# LANGUAGE LambdaCase #-}++-- The Hashable instances for Unique and Name are orphans+-- but should eventually be removed when hashtables are+-- replaced in the ConstraintSet representation.+{-# OPTIONS_GHC -Wno-orphans #-} ++module Intensional.Constructors+ ( Side (..),+ K (..),+ ConL,+ ConR,+ toAtomic,+ getLocation+ )+where++import Binary+import Data.Hashable+import GhcPlugins hiding (L)+import Intensional.Types+import Unique++instance Hashable Unique where+ hashWithSalt s = hashWithSalt s . getKey++instance Hashable Name where+ hashWithSalt s = hashWithSalt s . getUnique++data Side = L | R++-- A constructor set with a location tag+-- We include the srcSpan as part of the+-- identity so that multiple errors with +-- the same constructor in different program+-- locations are treated seperately.+data K (s :: Side) where+ Dom :: DataType Name -> K s+ Con :: Name -> SrcSpan -> K 'L+ Set :: UniqSet Name -> SrcSpan -> K 'R++type ConL = K 'L+type ConR = K 'R++-- Don't disregard location in comparison+-- i.e. distinguish between different sources+-- and sinks+instance Eq (K s) where+ Dom d == Dom d' = d == d'+ Con k l == Con k' l' = k == k' && l == l'+ Set s l == Set s' l' = s == s' && l == l'+ _ == _ = False++instance Hashable (K s) where+ hashWithSalt s (Dom d) = hashWithSalt s d+ hashWithSalt s (Con k _) = hashWithSalt s k+ hashWithSalt s (Set ks _) = hashWithSalt s (nonDetKeysUniqSet ks)++instance Outputable (K s) where+ ppr = prpr ppr++instance Binary (K 'L) where+ put_ bh (Dom d) = put_ bh False >> put_ bh d+ put_ bh (Con k l) = put_ bh True >> put_ bh k >> put_ bh l++ get bh =+ get bh >>= \case+ False -> Dom <$> get bh+ True -> Con <$> get bh <*> get bh++instance Binary (K 'R) where+ put_ bh (Dom d) = put_ bh False >> put_ bh d+ put_ bh (Set s l) = put_ bh True >> put_ bh (nonDetEltsUniqSet s) >> put_ bh l++ get bh =+ get bh >>= \case+ False -> Dom <$> get bh+ True -> do+ s <- mkUniqSet <$> get bh+ l <- get bh+ return (Set s l)++instance Refined (K l) where+ domain (Dom d) = domain d+ domain _ = mempty++ rename x y (Dom d) = Dom (rename x y d)+ rename _ _ s = s++ prpr m (Dom (Inj x d)) = m x GhcPlugins.<> parens (ppr d)+ prpr _ (Dom (Base _)) = error "Base in constraint."+ prpr _ (Con k _) = ppr k+ prpr _ (Set ks _) = hcat [char '{', pprWithBars ppr (nonDetEltsUniqSet ks), char '}']++{-|+ Assuming @k@ is either a @Con@ or @Set@ atom, + @getLocation k@ is the associated span.+-}+getLocation :: K a -> SrcSpan +getLocation (Con _ s) = s+getLocation (Set _ s) = s+getLocation _ = error "Dom constructors have no location."++-- Convert constraint to atomic form+toAtomic :: K l -> K r -> [(K 'L, K 'R)]+toAtomic (Dom d) (Dom d')+ | d == d' = []+ | otherwise = [(Dom d, Dom d')]+toAtomic (Dom d) (Con k l) =+ [(Dom d, Set (unitUniqSet k) l)]+toAtomic (Dom d) (Set ks l) =+ [(Dom d, Set ks l)]+toAtomic (Con k l) (Dom d) =+ [(Con k l, Dom d)]+toAtomic (Con k l) (Con k' l')+ | k == k' = []+ | otherwise = [(Con k l, Set emptyUniqSet l')]+toAtomic (Con k l) (Set ks l')+ | elementOfUniqSet k ks = []+ | otherwise = [(Con k l, Set emptyUniqSet l')]+toAtomic (Set ks l) (Dom d) =+ [(Con k l, Dom d) | k <- nonDetEltsUniqSet ks]+toAtomic (Set ks l) (Con k l') =+ [(Con k l, Set emptyUniqSet l') | k' <- nonDetEltsUniqSet ks, k' /= k]+toAtomic (Set ks l) (Set ks' l') =+ [(Con k l, Set emptyUniqSet l') | k <- nonDetEltsUniqSet ks, not (elementOfUniqSet k ks')]
+ src/Intensional/FromCore.hs view
@@ -0,0 +1,130 @@+{-# LANGUAGE LambdaCase #-}++module Intensional.FromCore+ ( freshCoreType,+ freshCoreScheme,+ fromCoreCons,+ consInstArgs,+ getVar,+ )+where++import Control.Monad.RWS+import qualified Data.IntSet as I+import qualified Data.Map as M+import GhcPlugins hiding ((<>), Expr (..), Type)+import Intensional.InferM+import Intensional.Scheme as Scheme+import ToIface+import qualified TyCoRep as Tcr+import Intensional.Types++-- A fresh monomorphic type+freshCoreType :: Tcr.Type -> InferM Type+freshCoreType = fromCore Nothing++-- A fresh polymorphic type+freshCoreScheme :: Tcr.Type -> InferM Scheme+freshCoreScheme = fromCoreScheme Nothing++-- The type of a constructor injected into a fresh refinement environment+fromCoreCons :: DataCon -> InferM Scheme+fromCoreCons k = do+ x <- fresh+ let d = dataConTyCon k+ b <- isIneligible d+ unless b $ do+ l <- asks inferLoc+ emitKD k l (Inj x d)+ fromCoreScheme (Just x) (dataConUserType k)++-- The argument types of an instantiated constructor+consInstArgs :: RVar -> [Type] -> DataCon -> InferM [Type]+consInstArgs x as k = mapM fromCoreInst (dataConRepArgTys k)+ where+ fromCoreInst :: Tcr.Type -> InferM Type+ fromCoreInst (Tcr.TyVarTy a) =+ case lookup a (zip (dataConUnivTyVars k) as) of+ Nothing -> return (Var (getName a))+ Just t -> return t+ fromCoreInst (Tcr.AppTy a b) = App <$> (fromCoreInst a) <*> (fromCoreInst b)+ fromCoreInst (Tcr.TyConApp d as')+ | isTypeSynonymTyCon d,+ Just (as'', s) <- synTyConDefn_maybe d =+ fromCoreInst (substTy (extendTvSubstList emptySubst (zip as'' as')) s) -- Instantiate type synonym arguments+ | isClassTyCon d = return Ambiguous -- Disregard type class evidence+ | otherwise =+ do b <- isIneligible d+ if b then Data (Base d) <$> (mapM fromCoreInst as') + else Data (Inj x d) <$> (mapM fromCoreInst as')+ fromCoreInst (Tcr.FunTy a b) = (:=>) <$> fromCoreInst a <*> fromCoreInst b+ fromCoreInst (Tcr.LitTy l) = return (Lit $ toIfaceTyLit l)+ fromCoreInst _ = return Ambiguous++-- Convert a monomorphic core type+fromCore :: Maybe RVar -> Tcr.Type -> InferM Type+fromCore _ (Tcr.TyVarTy a) = Var <$> getExternalName a+fromCore f (Tcr.AppTy a b) = liftM2 App (fromCore f a) (fromCore f b)+fromCore f (Tcr.TyConApp d as)+ | isTypeSynonymTyCon d,+ Just (as', s) <- synTyConDefn_maybe d =+ fromCore f (substTy (extendTvSubstList emptySubst (zip as' as)) s) -- Instantiate type synonyms+ | isClassTyCon d = return Ambiguous -- Disregard type class evidence+fromCore Nothing (Tcr.TyConApp d as) = do+ x <- fresh+ b <- isIneligible d+ if b then+ Data (Base d) <$> mapM (fromCore Nothing) as+ else+ Data (Inj x d) <$> mapM (fromCore Nothing) as+fromCore (Just x) (Tcr.TyConApp d as) = do+ b <- isIneligible d+ if b then+ Data (Base d) <$> mapM (fromCore (Just x)) as+ else+ Data (Inj x d) <$> mapM (fromCore (Just x)) as+fromCore f (Tcr.FunTy a b) = liftM2 (:=>) (fromCore f a) (fromCore f b)+fromCore _ (Tcr.LitTy l) = return $ Lit $ toIfaceTyLit l+fromCore _ _ = return Ambiguous -- Higher-ranked or impredicative types, casts and coercions++-- Convert a polymorphic core type+fromCoreScheme :: Maybe RVar -> Tcr.Type -> InferM Scheme+fromCoreScheme f (Tcr.ForAllTy b t) = do+ a <- getExternalName (Tcr.binderVar b)+ scheme <- fromCoreScheme f t+ return scheme {tyvars = a : tyvars scheme}+fromCoreScheme f (Tcr.FunTy a b) = do+ a' <- fromCore f a+ scheme <- fromCoreScheme f b -- Optimistically push arrows inside univiersal quantifier+ return scheme {body = a' :=> body scheme}+fromCoreScheme f t = Forall [] <$> fromCore f t++-- Lookup constrained variable and emit its constraints+getVar :: Var -> InferM Scheme+getVar v =+ asks (M.lookup (getName v) . varEnv) >>= \case+ Just scheme -> do+ -- Localise constraints+ fre_scheme <-+ foldM+ ( \s x -> do+ y <- fresh+ return (rename x y s)+ )+ (scheme {boundvs = mempty})+ (I.toList (boundvs scheme))+ -- Emit constriants associated with a variable+ tell (constraints fre_scheme)+ return fre_scheme {Scheme.constraints = mempty}+ Nothing -> do+ var_scheme <- freshCoreScheme $ varType v+ maximise True (body var_scheme)+ return var_scheme++-- Maximise/minimise a library type, i.e. assert every constructor occurs in covariant positions+maximise :: Bool -> Type -> InferM ()+maximise True (Data (Inj x d) _) = do+ l <- asks inferLoc+ mapM_ (\k -> emitKD k l (Inj x d)) $ tyConDataCons d+maximise b (x :=> y) = maximise (not b) x >> maximise b y+maximise _ _ = return ()
+ src/Intensional/Guard.hs view
@@ -0,0 +1,110 @@+module Intensional.Guard where++import qualified GhcPlugins as GHC+import Binary +import Data.Map (Map)+import Data.Set (Set)+import qualified Data.Map as Map+import qualified Data.Set as Set+import qualified Data.IntSet as IntSet+import qualified Data.IntMap as IntMap++import Intensional.Types+import Intensional.Constructors++-- data Named a = Named {toPair :: (GHC.Name, a)}+-- deriving (Eq, Functor)++-- instance Semigroup a => Semigroup (Named a) where+-- Named (n, ks1) <> Named (_, ks2) = Named (n, ks1 <> ks2)++-- instance GHC.Uniquable (Named a) where+-- getUnique (Named (n, _)) = GHC.getUnique n++-- instance Binary a => Binary (Named a) where+-- put_ bh = put_ bh . toPair+-- get bh = Named <$> Binary.get bh+++-- A set of simple inclusion constraints, i.e. k in X(d), grouped by X(d)+newtype Guard+ = Guard+ { + groups :: Map (RVar, GHC.Name) (GHC.UniqSet GHC.Name)+ }+ deriving (Eq)++instance Semigroup Guard where+ Guard g <> Guard g' = Guard (Map.unionWith GHC.unionUniqSets g g')++instance Monoid Guard where+ mempty = Guard mempty++instance GHC.Outputable Guard where+ ppr = prpr GHC.ppr++isEmpty :: Guard -> Bool+isEmpty (Guard g) = Map.null g++toList :: Guard -> [(Int, GHC.Name, GHC.Name)]+toList (Guard g) =+ [ (x, d, k) | ((x,d), ks) <- Map.toList g, k <- GHC.nonDetEltsUniqSet ks ]++fromList :: [(Int, GHC.Name, GHC.Name)] -> Guard+fromList = foldMap (\(x, d, k) -> singleton [k] x d)++typedVars :: Guard -> Set (RVar, GHC.Name)+typedVars (Guard g) = Map.keysSet g++instance Binary Guard where+ put_ bh = put_ bh . toList+ get bh = fromList <$> get bh++instance Refined Guard where+ domain (Guard g) = + Set.foldl' (\acc (x,_) -> IntSet.insert x acc) mempty (Map.keysSet g)++ rename x y (Guard g) =+ Guard (Map.foldrWithKey (\(z,d) ks m -> Map.insertWith GHC.unionUniqSets (if z == x then y else z, d) ks m) mempty g)++ prpr m (Guard g) = GHC.pprWithCommas pprGuardAtom guardList+ where+ pprGuardAtom ((x,d), ks) = GHC.hsep [GHC.ppr ks, GHC.text "in", prpr m (Dom (Inj x d))]+ guardList = fmap (\(x,y) -> (x, GHC.nonDetEltsUniqSet y)) (Map.toList g)++lookup :: RVar -> GHC.Name -> Guard -> Maybe (GHC.UniqSet GHC.Name)+lookup x d (Guard g) = Map.lookup (x,d) g++delete :: GHC.Name -> RVar -> GHC.Name -> Guard -> Guard+delete k x d (Guard g) = Guard (Map.alter del (x,d) g)+ where+ del Nothing = Nothing+ del (Just ks) =+ let ks' = GHC.delOneFromUniqSet ks k+ in if GHC.isEmptyUniqSet ks' then Nothing else Just ks'++deleteAll :: [GHC.Name] -> RVar -> GHC.Name -> Guard -> Guard+deleteAll ms x d (Guard g) = Guard (Map.alter del (x,d) g)+ where+ del Nothing = Nothing+ del (Just ks) =+ let ks' = GHC.delListFromUniqSet ks ms+ in if GHC.isEmptyUniqSet ks' then Nothing else Just ks'++-- A guard literal+-- Ignorning possibly trivial guards (e.g. 1-constructor types has already+-- happened in InferM.branch)+singleton :: [GHC.Name] -> RVar -> GHC.Name -> Guard+singleton ks x d =+ Guard (Map.singleton (x, d) (GHC.addListToUniqSet mempty ks))++-- guardsFromList :: [GHC.Name] -> DataType GHC.Name -> Guard+-- guardsFromList ks (Inj x d) = foldr (\k gs -> singleton k (Inj x d) <> gs) mempty ks++impliedBy :: Guard -> Guard -> Bool+impliedBy (Guard g) (Guard g') =+ Map.isSubmapOfBy keyInclusion g' g+ where+ keyInclusion u1 u2 =+ {-# SCC keyInclusion #-}+ IntMap.isSubmapOfBy (\_ _ -> True) (GHC.ufmToIntMap $ GHC.getUniqSet u1) (GHC.ufmToIntMap $ GHC.getUniqSet u2)
+ src/Intensional/InferCoreExpr.hs view
@@ -0,0 +1,301 @@+{-# LANGUAGE LambdaCase #-}++module Intensional.InferCoreExpr+ ( inferProg,+ )+where++import Intensional.Ubiq+import Control.Monad.Extra+import Control.Monad.RWS.Strict+import Control.Monad.State.Strict as State+import CoreArity+import qualified CoreSyn as Core+import Data.Bifunctor+import qualified Data.IntSet as I+import qualified Data.List as L+import qualified Data.Map as M+import Intensional.FromCore+import GhcPlugins hiding ((<>), Type)+import Intensional.InferM+import Pair+import Intensional.Scheme as Scheme+import Intensional.Guard as Guard+import Intensional.Types++import qualified Intensional.Constraints as Constraints++import Debug.Trace++{-|+ The type of subtype inference constraints that are accumulated+ during the subtype inference fixpoint algorithm.++ There is a 1-1 correspondence between this type and the type of+ atomic constraints, but the former contain more information+ (though this information could be determined by the context at+ great expense).+-}+type SubTyAtom = (Guard, RVar, RVar, TyCon)++{-|+ The type of elements of the frontier in the subtype inference fixpoint+ algorithm. There is an injection from this type into the typ of atomic+ constraints, but the inhabitants of this type additionally track the+ types used to instantiate the constructors of the datatype involved in+ the constraint. This additional information is needed to unfold the + frontier and look for successors.+-}+type SubTyFrontierAtom = (Guard, RVar, RVar, TyCon, [Type], [Type])++{-|+ The type of the subtype inference algorithm, i.e. a stateful fixed + point computation that must additionally draw upon the services of + the inference monad to deal with GHC types.+-}+type SubTyComputation = StateT ([SubTyFrontierAtom], [SubTyAtom]) InferM ()++{-|+ Given a pair of types @t1@ and @t2@, @inferSubType t1 t2@ is the action+ that emits constraints characterising @t1 <= t2@.++ Also emits statistics on the size of the input parameters to do with slices.+-}+inferSubType :: Type -> Type -> InferM ()+inferSubType t1 t2 = + do let ts = inferSubTypeStep t1 t2+ (_,cs) <- listen $+ forM_ ts $ \(x, y, d, as, as') ->+ do -- Entering a slice+ ds <- snd <$> State.execStateT inferSubTypeFix ([(mempty, x, y, d, as, as')],[(mempty, x, y, d)])+ -- Note how big it was for statistics+ noteD $ length (L.nub $ map (\(_,_,_,d') -> getName d') ds)+ -- Emit a constraint for each one+ forM_ ds $ \(gs, x', y', d') -> + censor (Constraints.guardWith gs) (emitDD (Inj x' d') (Inj y' d'))+ when debugging $ + do src <- asks inferLoc+ traceM ("[TRACE] Starting subtpe inference at " ++ traceSpan src)+ let sz = Constraints.size cs+ traceM ("[TRACE] The subtype proof at " ++ traceSpan src ++ " contributed " ++ show sz ++ " constraints.")++ where++ leq :: SubTyAtom -> SubTyAtom -> Bool+ leq (gs, x, y, d) (gs', x', y', d') =+ -- getName here is probably unnecessary, should look it up+ x == x' && y == y' && getName d == getName d' && gs' `Guard.impliedBy` gs+ + inferSubTypeFix :: SubTyComputation+ inferSubTypeFix = + do (frontier, acc) <-get+ unless (null frontier) $+ do put ([], acc)+ forM_ frontier $ \(gs, x, y, d, as, as') -> + do let dataCons = tyConDataCons d+ lift $ noteK (length dataCons)+ forM_ dataCons $ \k -> + do xtys <- lift $ consInstArgs x as k+ ytys <- lift $ consInstArgs y as' k+ let gs' = + if (isTrivial d) + then gs + else Guard.singleton [getName k] x (getName d) <> gs+ let ts = concat $ zipWith inferSubTypeStep xtys ytys+ forM_ ts $ \(x', y', d', bs, bs') ->+ do let new = (gs', x', y', d')+ let newF = (gs', x', y', d', bs, bs')+ (fr, ac) <- get+ unless (any (`leq` new) ac) $ put (newF:fr, new:ac)+ inferSubTypeFix+++ inferSubTypeStep :: Type -> Type -> [(RVar, RVar, TyCon, [Type], [Type])]+ inferSubTypeStep (Data (Inj x d) as) (Data (Inj y _) as') =+ [(x, y, d, as, as')]+ inferSubTypeStep (t11 :=> t12) (t21 :=> t22) =+ let ds1 = inferSubTypeStep t21 t11 + ds2 = inferSubTypeStep t12 t22+ in ds1 ++ ds2+ inferSubTypeStep (Data (Base _) as) (Data (Base _) as') =+ concat $ zipWith inferSubTypeStep as as'+ inferSubTypeStep _ _ = []++-- Infer constraints for a module+inferProg :: CoreProgram -> InferM Context+inferProg [] = return M.empty+inferProg (r : rs) =+ do let bs = map occName $ bindersOf r + ctx <- if any isDerivedOccName bs then return mempty else associate r+ ctxs <- putVars ctx (inferProg rs)+ return (ctxs <> ctx)++-- Infer a set of constraints and associate them to qualified type scheme+associate :: CoreBind -> InferM Context+associate r = + setLoc (UnhelpfulSpan (mkFastString ("Top level " ++ bindingNames))) doAssoc+ where + bindingNames = + show $ map (occNameString . occName) (bindersOf r)+ doAssoc =+ do when debugging $ traceM ("[TRACE] Begin inferring: " ++ bindingNames)+ env <- asks varEnv+ (ctx, cs) <- listen $ inferRec r+ let satAction s = + do cs' <- snd <$> (listen $ saturate (do { tell cs; return s }))+ -- Attempt to build a model and record counterexamples+ es <- cexs cs'+ return $ s { + boundvs = (domain cs' <> domain s) I.\\ domain env,+ Scheme.constraints = es <> cs'+ }+ -- add constraints to every type in the recursive group+ ctx' <- mapM satAction ctx+ -- note down any counterexamples+ let es = M.foldl' (\ss sch -> Scheme.unsats sch <> ss) mempty ctx'+ noteErrs es+ when debugging $ traceM ("[TRACE] End inferring: " ++ bindingNames) + incrN + return ctx'++-- Infer constraints for a mutually recursive binders+inferRec :: CoreBind -> InferM Context+inferRec (NonRec x e) = M.singleton (getName x) <$> infer e+inferRec (Rec xes) = do+ binds <-+ sequence+ $ M.fromList+ $ bimap+ getName+ ( \e -> do+ rec_scheme <- freshCoreScheme (exprType e)+ return (e, rec_scheme)+ )+ <$> xes+ -- Add binds for recursive calls+ putVars (fmap snd binds) $+ traverse+ ( \(e, rec_scheme) -> do+ scheme <- infer e+ -- Bound recursive calls+ -- Must be bidirectional for mututally recursive groups+ inferSubType (body scheme) (body rec_scheme)+ inferSubType (body rec_scheme) (body scheme)+ return scheme+ )+ binds++-- Infer constraints for a program expression+infer :: CoreExpr -> InferM Scheme+infer (Core.Var v) =+ -- Check if identifier is a constructor+ case isDataConId_maybe v of+ Just k+ -- Ignore typeclass evidence+ | isClassTyCon $ dataConTyCon k -> return (Forall [] Ambiguous)+ | otherwise -> fromCoreCons k+ Nothing -> getVar v+infer l@(Core.Lit _) = freshCoreScheme $ exprType l+infer (Core.App e1 (Core.Type e2)) = do+ t <- freshCoreType e2+ scheme <- infer e1+ case scheme of+ Forall (a : as) b ->+ return $ Forall as (subTyVar a t b) -- Type application+ Forall [] Ambiguous -> return (Forall [] Ambiguous)+ _ -> pprPanic "Type application to monotype!" (ppr (scheme, e2))+infer (Core.App e1 e2) =+ saturate+ ( infer e1 >>= \case+ Forall as Ambiguous -> Forall as Ambiguous <$ infer e2+ -- See FromCore 88 for the case when as /= []+ Forall as (t3 :=> t4) -> do+ t2 <- mono <$> infer e2+ inferSubType t2 t3+ return $ Forall as t4+ _ -> pprPanic "The expression has been given too many arguments!" $ ppr (exprType e1, exprType e2)+ )+infer (Core.Lam x e)+ | isTyVar x = do+ a <- getExternalName x+ infer e >>= \case+ Forall as t -> return $ Forall (a : as) t -- Type abstraction+ | otherwise = do+ t1 <- freshCoreType (varType x)+ putVar (getName x) (Forall [] t1) (infer e) >>= \case+ Forall as t2 -> return $ Forall as (t1 :=> t2)+infer (Core.Let b e) = saturate $ do+ ts <- associate b+ putVars ts $ infer e+infer (Core.Case e bind_e core_ret alts) = saturate $ do+ -- Fresh return type+ ret <- freshCoreType core_ret+ -- Infer expression on which to pattern match+ t0 <- mono <$> infer e+ -- Add the variable under scrutinee to scope+ putVar (getName bind_e) (Forall [] t0) $+ case t0 of+ Data dt as -> do+ ks <-+ mapMaybeM+ ( \case+ (Core.DataAlt k, xs, rhs)+ | not (isBottoming rhs) -> do+ -- Add constructor arguments introduced by the pattern+ y <- fresh -- only used in Base case of ts+ ts <- + case dt of + Inj x _ -> M.fromList . zip (fmap getName xs) <$> (map (Forall []) <$> (consInstArgs x as k))+ Base _ -> M.fromList . zip (fmap getName xs) <$> (map (Forall []) <$> (consInstArgs y as k))+ branchAny [k] dt $ do+ -- Ensure return type is valid+ ret_i <- mono <$> putVars ts (infer rhs)+ inferSubType ret_i ret+ -- Record constructorsc+ return (Just k)+ (Core.LitAlt _, _, rhs) + | not (isBottoming rhs) -> do+ -- Ensure return type is valid+ ret_i <- mono <$> infer rhs+ inferSubType ret_i ret+ -- Record constructors+ return Nothing+ _ -> return Nothing -- Skip defaults until all constructors have been seen+ )+ alts+ case findDefault alts of+ (_, Just rhs) | not (isBottoming rhs) ->+ -- Guard by unseen constructors+ branchAny (tyConDataCons (tyconOf dt) L.\\ ks) dt $ do+ -- Ensure return type is valid+ ret_i <- mono <$> infer rhs+ inferSubType ret_i ret+ _ | (Inj x d) <- dt -> do+ -- Ensure destructor is total if not nested+ l <- asks inferLoc+ emitDK (Inj x d) ks l+ _ -> return ()+ _ -> + mapM_+ ( \(_, xs, rhs) ->+ do -- Add constructor arguments introduced by the pattern+ ts <- sequence $ M.fromList $ zip (fmap getName xs) (fmap (freshCoreScheme . varType) xs)+ -- Ensure return type is valid+ ret_i <- mono <$> putVars ts (infer rhs)+ inferSubType ret_i ret+ )+ alts+ return (Forall [] ret)+infer (Core.Cast e g) = do+ _ <- infer e+ freshCoreScheme (pSnd $ coercionKind g)+infer (Core.Tick SourceNote {sourceSpan = s} e) = setLoc (RealSrcSpan s) $ infer e -- Track location in source text+infer (Core.Tick _ e) = infer e -- Ignore other ticks+infer (Core.Coercion g) = freshCoreScheme (pSnd $ coercionKind g)+infer (Core.Type t) = pprPanic "Unexpected type" (ppr t)++isBottoming :: CoreExpr -> Bool+isBottoming e =+ case exprBotStrictness_maybe e of+ Nothing -> exprIsBottom e+ Just (_, _) -> True
+ src/Intensional/InferM.hs view
@@ -0,0 +1,247 @@+{-# LANGUAGE FlexibleInstances #-}++module Intensional.InferM+ ( InferM,+ Context,+ InferEnv (..),+ Stats (..),+ runInferM,+ Intensional.InferM.saturate,+ branchAny,+ emitDD,+ emitDK,+ emitKD,+ fresh,+ putVar,+ putVars,+ setLoc,+ getExternalName,+ isTrivial,+ isIneligible,+ noteD,+ noteK,+ incrN,+ noteErrs,+ Intensional.InferM.cexs+ )+where++import Intensional.Constraints as Constraints+import Intensional.Constructors+import Control.Monad.RWS.Strict hiding (guard)+import qualified Data.IntSet as IntSet+import qualified Data.Map as M+import GhcPlugins hiding ((<>), singleton)+import Intensional.Scheme+import Intensional.Types+import Intensional.Ubiq+import Intensional.Guard++type InferM = RWS InferEnv ConstraintSet InferState++type Context = M.Map Name Scheme++data InferEnv+ = InferEnv+ { modName :: Module, -- The current module+ varEnv :: Context,+ inferLoc :: SrcSpan -- The current location in the source text+ }++data InferState = + InferState {+ maxK :: Int,+ maxD :: Int,+ maxI :: Int,+ cntN :: Int,+ rVar :: Int,+ errs :: ConstraintSet+ }++initState :: InferState+initState = InferState 0 0 0 0 0 mempty++noteK :: Int -> InferM ()+noteK x = modify (\s -> s { maxK = max x (maxK s) })++noteD :: Int -> InferM ()+noteD x = modify (\s -> s { maxD = max x (maxD s) })++noteI :: Int -> InferM ()+noteI x = modify (\s -> s { maxI = max x (maxI s) })++incrV :: InferM ()+incrV = modify (\s -> s { rVar = rVar s + 1 })++incrN :: InferM ()+incrN = modify (\s -> s { cntN = cntN s + 1 })++{-|+ Given a set of trivially unsatisfiable constraints @es@,+ @noteErrs es@ is the action that records them+ in the accumulating set in the inference state.+-}+noteErrs :: ConstraintSet -> InferM ()+noteErrs es = modify (\s -> s { errs = es <> errs s })++data Stats = + Stats {+ getK :: Int,+ getD :: Int,+ getV :: Int,+ getI :: Int,+ getN :: Int+ }++runInferM ::+ InferM a ->+ Module ->+ Context ->+ (a, [Atomic], Stats)+runInferM run mod_name init_env =+ let (a, s, _) = runRWS run (InferEnv mod_name init_env (UnhelpfulSpan (mkFastString "Nowhere"))) initState+ in (a, Constraints.toList (errs s), Stats (maxK s) (maxD s) (rVar s) (maxI s) (cntN s))++-- Transitively remove local constraints+saturate :: Refined a => InferM a -> InferM a+saturate ma = pass $+ do+ a <- ma+ env <- asks varEnv+ m <- asks modName+ src <- asks inferLoc+ let interface = domain a <> domain env+ noteI (IntSet.size interface)+ let fn cs =+ let ds = Constraints.saturate (CInfo m src) interface cs+ in if debugging then debugBracket a env src cs ds else ds+ return (a, fn)+ where+ debugBracket a env src cs ds =+ let asz = "type: " ++ show (IntSet.size $ domain a)+ esz = "env: " ++ show (IntSet.size $ domain env)+ csz = show (size cs)+ spn = traceSpan src+ tmsg = "#interface = (" ++ asz ++ " + " ++ esz ++ "), #constraints = " ++ csz+ ds' = trace ("[TRACE] BEGIN saturate at " ++ spn ++ ": " ++ tmsg) ds+ in ds' `seq` trace ("[TRACE] END saturate at " ++ spn ++ " saturated size: " ++ (show $ size ds)) ds++{-|+ Given a constraint set @cs@, @cexs cs@ is the inference action that+ attempts to build a model of @cs@ and returns the set of counterexamples.+-}+cexs :: ConstraintSet -> InferM ConstraintSet+cexs cs = + do m <- asks modName + src <- asks inferLoc + return $ Constraints.cexs (CInfo m src) cs++-- Check if a core datatype is ineligible for refinement+isIneligible :: TyCon -> InferM Bool+isIneligible tc = + do m <- asks modName+ return (not (homeOrBase m (getName tc)) || null (tyConDataCons tc))+ where+ homeOrBase m n =+ nameIsHomePackage m n ++ -- Previously we tried to include as much of base as possible by asking for specific modules+ -- but this is a little too coarse grain (e.g. GHC.Types will include Bool, but also Int):+ --+ -- vc|| ( not (nameIsFromExternalPackage baseUnitId n && nameIsFromExternalPackage primUnitId n)+ -- && case nameModule_maybe n of+ -- Nothing -> False+ -- Just (Module _ m) ->+ -- List.isPrefixOf "Prelude" (moduleNameString m)+ -- || List.isPrefixOf "Data" (moduleNameString m)+ -- || List.isPrefixOf "GHC.Base" (moduleNameString m)+ -- || List.isPrefixOf "GHC.Types" (moduleNameString m)+ -- )+ --+ -- a better approach would be, simply:+ -- strName = occNameString (getOccName tc)+ -- ...+ -- || strName == "Bool"+ -- || strName == "Maybe"++isTrivial :: TyCon -> Bool+isTrivial tc = (== 1) (length (tyConDataCons tc))++++{- + Given a list of data constructors @ks@, a datatype @Inj x d@ and an + inference action @m@, @branchAny ks (Inj x d) m@ is the inference action+ that consists of doing @m@ then guarding all emitted constraints+ by the requirement that @ks in x(d)@.+-}+branchAny :: [DataCon] -> DataType TyCon -> InferM a -> InferM a+branchAny _ (Base _) m = m+branchAny ks (Inj x d) m = + if (isTrivial d) then m else censor guardWithAll m+ where+ dn = getName d+ guardWithAll cs =+ foldMap (\k -> Constraints.guardWith (singleton [getName k] x dn) cs) ks++mkConFromCtx :: ConL -> ConR -> InferM Atomic+mkConFromCtx l r =+ do m <- asks modName+ s <- asks inferLoc+ return (Constraint l r mempty (CInfo m s))++emitDD :: DataType TyCon -> DataType TyCon -> InferM ()+emitDD (Inj x d) (Inj y _) = + unless (isTrivial d) $ + do a <- mkConFromCtx (Dom (Inj x dn)) (Dom (Inj y dn))+ tell (Constraints.fromList [a])+ where+ dn = getName d+emitDD _ _ = return ()++emitKD :: DataCon -> SrcSpan -> DataType TyCon -> InferM ()+emitKD k s (Inj x d) =+ unless (isTrivial d) $ + do a <- mkConFromCtx (Con kn s) (Dom (Inj x dn))+ tell (Constraints.fromList [a])+ where+ dn = getName d+ kn = getName k+emitKD _ _ _ = return ()++emitDK :: DataType TyCon -> [DataCon] -> SrcSpan -> InferM ()+emitDK (Inj x d) ks s =+ unless (isTrivial d || length (tyConDataCons d) == length ks) $ + do a <- mkConFromCtx (Dom (Inj x dn)) (Set ksn s)+ tell (Constraints.fromList [a])+ where+ dn = getName d+ ksn = mkUniqSet (map getName ks)+emitDK _ _ _ = return ()+++-- A fresh refinement variable+fresh :: InferM RVar+fresh = do+ i <- gets rVar+ incrV+ return i++-- Insert variables into environment+putVar :: Name -> Scheme -> InferM a -> InferM a+putVar n s = local (\env -> env {varEnv = M.insert n s (varEnv env)})++putVars :: Context -> InferM a -> InferM a+putVars ctx = local (\env -> env {varEnv = M.union ctx (varEnv env)})++-- Add source text location tick+setLoc :: SrcSpan -> InferM a -> InferM a+setLoc l = local (\env -> env {inferLoc = l})++-- Prepare name for interface+-- Should be used before all type variables+getExternalName :: NamedThing a => a -> InferM Name+getExternalName a = do+ let n = getName a+ mn <- asks modName+ return $ mkExternalName (nameUnique n) mn (nameOccName n) (nameSrcSpan n)
+ src/Intensional/Scheme.hs view
@@ -0,0 +1,92 @@+{-# LANGUAGE DeriveTraversable #-}+{-# LANGUAGE PatternSynonyms #-}++module Intensional.Scheme+ ( Scheme,+ SchemeGen (..),+ pattern Forall,+ mono,+ Intensional.Scheme.unsats+ )+where++import Binary+import Intensional.Constraints as Constraints+import qualified Data.IntSet as I+import qualified Data.IntMap as IntMap+import GhcPlugins +import Intensional.Types++type Scheme = SchemeGen TyCon++-- Constrained polymorphic types+data SchemeGen d+ = Scheme+ { tyvars :: [Name],+ boundvs :: Domain,+ body :: TypeGen d,+ constraints :: ConstraintSet+ }+ deriving (Functor, Foldable, Traversable)++{-# COMPLETE Forall #-}++pattern Forall :: [Name] -> TypeGen d -> SchemeGen d+pattern Forall as t <-+ Scheme as _ t _+ where+ Forall as t = Scheme as mempty t mempty++instance Outputable d => Outputable (SchemeGen d) where+ ppr = prpr ppr++instance Binary d => Binary (SchemeGen d) where+ put_ bh (Scheme as bs t cs) = put_ bh as >> put_ bh (I.toList bs) >> put_ bh t >> put_ bh cs++ get bh = Scheme <$> get bh <*> (I.fromList <$> get bh) <*> get bh <*> get bh++instance Outputable d => Refined (SchemeGen d) where+ domain s = (domain (body s) Prelude.<> domain (constraints s)) I.\\ boundvs s++ rename x y s+ | I.member x (boundvs s) = s+ | I.member y (boundvs s) = pprPanic "Alpha renaming of polymorphic types is not implemented!" $ ppr (x, y)+ | otherwise =+ Scheme+ { tyvars = tyvars s,+ boundvs = boundvs s,+ body = rename x y (body s),+ constraints = rename x y (constraints s)+ }+ + prpr _ scheme + | constraints scheme /= mempty =+ hang+ (hcat [pprTyQuant, pprConQuant, prpr varMap (body scheme)])+ 2+ (hang (text "where") 2 (prpr varMap (constraints scheme)))+ | otherwise = hcat [pprTyQuant, pprConQuant, prpr varMap (body scheme)]+ where+ numVars = I.size (boundvs scheme)+ varNames =+ if numVars > 3 then [ char 'X' GhcPlugins.<> int n | n <- [1..numVars] ] else [ char c | c <- ['X', 'Y', 'Z'] ]+ varMap = \x -> m IntMap.! x+ where m = IntMap.fromList $ zip (I.toAscList (boundvs scheme)) varNames+ pprTyQuant+ | null (tyvars scheme) = empty+ | otherwise = hcat [forAllLit <+> fsep (map ppr $ tyvars scheme), dot]+ pprConQuant+ | I.null (boundvs scheme) = empty+ | otherwise = hcat [forAllLit <+> fsep (map varMap $ I.toList (boundvs scheme)), dot]++-- Demand a monomorphic type+mono :: SchemeGen d -> TypeGen d+mono (Forall [] t) = t+mono _ = Ambiguous++{-|+ Given a scheme @s@, @unsats s@ is the constraint set containing+ just the trivially unsatisfiable constraints associated with @s@.+-}+unsats :: Scheme -> ConstraintSet+unsats s = Constraints.unsats (constraints s)
+ src/Intensional/Types.hs view
@@ -0,0 +1,180 @@+{-# LANGUAGE DeriveGeneric #-}+{-# LANGUAGE DeriveTraversable #-}+{-# LANGUAGE LambdaCase #-}++module Intensional.Types+ ( RVar,+ Domain,+ Refined (..),+ DataType (..),+ Type,+ TypeGen (..),+ -- inj,+ decompType,+ subTyVar,+ tyconOf,+ )+where++import Binary+import Data.Bifunctor+import Data.Hashable+import qualified Data.IntSet as I+import Data.Map (Map)+import GHC.Generics hiding (prec)+import GhcPlugins hiding ((<>), Expr (..), Type)+import IfaceType++type RVar = Int++type Domain = I.IntSet++-- The class of objects containing refinement variables+class Refined t where+ domain :: t -> Domain+ rename :: RVar -> RVar -> t -> t+ prpr :: (RVar -> SDoc) -> t -> SDoc++instance Refined b => Refined (Map a b) where+ domain = foldMap domain+ rename x y = fmap (rename x y)+ prpr m = foldr (($$) . prpr m) empty++-- A datatype identifier+-- d is TyCon, IfaceTyCon or Name+data DataType d+ = Base d+ | Inj RVar d -- Extended datatypes from the canonical environment+ deriving (Eq, Functor, Foldable, Generic, Traversable)++instance Hashable d => Hashable (DataType d)++instance Outputable d => Outputable (DataType d) where+ ppr = prpr ppr ++instance Binary d => Binary (DataType d) where+ put_ bh (Base d) = put_ bh False >> put_ bh d+ put_ bh (Inj x d) = put_ bh True >> put_ bh x >> put_ bh d+ get bh =+ get bh >>= \case+ False -> Base <$> get bh+ True -> Inj <$> get bh <*> get bh++instance Outputable d => Refined (DataType d) where+ domain (Base _) = I.empty+ domain (Inj x _) = I.singleton x++ rename x y (Inj z d)+ | x == z = Inj y d+ rename _ _ d = d++ prpr _ (Base d) = ppr d+ prpr m (Inj x d) = hcat [text "inj_", m x] <+> ppr d++-- Check if a core datatype contains covariant arguments+-- covariant :: TyCon -> Bool+-- covariant = all pos . concatMap dataConOrigArgTys . tyConDataCons+-- where+-- pos, neg :: Type -> Bool+-- pos (FunTy t1 t2) = neg t1 && pos t2+-- pos _ = True+-- neg (FunTy t1 t2) = pos t1 && neg t2+-- neg (TyConApp _ _) = False -- These cases are overapproximate+-- neg (TyVarTy _) = False+-- neg _ = True++++-- Get the tycon from a datatype+tyconOf :: DataType d -> d+tyconOf (Base d) = d+tyconOf (Inj _ d) = d++type Type = TypeGen TyCon++-- Monomorphic types parameterised by type constructors+data TypeGen d+ = Var Name+ | App (TypeGen d) (TypeGen d)+ | Data (DataType d) [TypeGen d]+ | TypeGen d :=> TypeGen d+ | Lit IfaceTyLit+ | Ambiguous -- Ambiguous hides higher-ranked types and casts+ deriving (Functor, Foldable, Traversable)++-- Clone of a Outputable Core.Type+instance Outputable d => Outputable (TypeGen d) where+ ppr = prpr ppr+ +instance Binary d => Binary (TypeGen d) where+ put_ bh (Var a) = put_ bh (0 :: Int) >> put_ bh a+ put_ bh (App a b) = put_ bh (1 :: Int) >> put_ bh a >> put_ bh b+ put_ bh (Data d as) = put_ bh (2 :: Int) >> put_ bh d >> put_ bh as+ put_ bh (a :=> b) = put_ bh (3 :: Int) >> put_ bh a >> put_ bh b+ put_ bh (Lit l) = put_ bh (4 :: Int) >> put_ bh l+ put_ bh Ambiguous = put_ bh (5 :: Int)++ get bh = do+ n <- get bh+ case n :: Int of+ 0 -> Var <$> get bh+ 1 -> App <$> get bh <*> get bh+ 2 -> Data <$> get bh <*> get bh+ 3 -> (:=>) <$> get bh <*> get bh+ 4 -> Lit <$> get bh+ 5 -> return Ambiguous+ _ -> pprPanic "Invalid binary file!" $ ppr n++instance Outputable d => Refined (TypeGen d) where+ domain (App a b) = domain a <> domain b+ domain (Data d as) = domain d <> foldMap domain as+ domain (a :=> b) = domain a <> domain b+ domain _ = mempty++ rename x y (App a b) = App (rename x y a) (rename x y b)+ rename x y (Data d as) = Data (rename x y d) (rename x y <$> as)+ rename x y (a :=> b) = rename x y a :=> rename x y b+ rename _ _ t = t++ prpr m = pprTy topPrec+ where+ pprTy :: Outputable d => PprPrec -> TypeGen d -> SDoc+ pprTy _ (Var a) = ppr a+ pprTy prec (App t1 t2) = hang (pprTy prec t1) 2 (pprTy appPrec t2)+ pprTy _ (Data d as) = hang (prpr m d) 2 $ sep [hcat [text "@", pprTy appPrec a] | a <- as]+ pprTy prec (t1 :=> t2) = maybeParen prec funPrec $ sep [pprTy funPrec t1, arrow, pprTy prec t2]+ pprTy _ (Lit l) = ppr l+ pprTy _ Ambiguous = text "<?>"++-- Inject a sort into a refinement environment+-- inj :: Int -> TypeGen d -> TypeGen d+-- inj _ (Var a) = Var a+-- inj x (App a b) = App (inj x a) (inj x b)+-- inj x (Data (Base b) as) = Data (Base b) (inj x <$> as)+-- inj x (Data (Inj _ d) as) = Data (Inj x d) (inj x <$> as)+-- inj x (a :=> b) = inj x a :=> inj x b+-- inj _ (Lit l) = Lit l+-- inj _ Ambiguous = Ambiguous++-- Decompose a functions into its arguments and eventual return type+decompType :: TypeGen d -> ([TypeGen d], TypeGen d)+decompType (a :=> b) = first (++ [a]) (decompType b)+decompType a = ([], a)++-- Type variable substitution+subTyVar :: Outputable d => Name -> TypeGen d -> TypeGen d -> TypeGen d+subTyVar a t (Var a')+ | a == a' = t+ | otherwise = Var a'+subTyVar a t (App x y) = applyType (subTyVar a t x) (subTyVar a t y)+subTyVar a t (Data d as) = Data d (subTyVar a t <$> as)+subTyVar a t (x :=> y) = subTyVar a t x :=> subTyVar a t y+subTyVar _ _ t = t++-- Unsaturated type application+applyType :: Outputable d => TypeGen d -> TypeGen d -> TypeGen d+applyType (Var a) t = App (Var a) t+applyType (App a b) t = App (App a b) t+applyType (Data d as) t = Data d (as ++ [t])+applyType Ambiguous _ = Ambiguous+applyType a b = pprPanic "The type is already saturated!" $ ppr (a, b)
+ src/Intensional/Ubiq.hs view
@@ -0,0 +1,18 @@+{-# LANGUAGE CPP #-}++module Intensional.Ubiq where++import qualified GhcPlugins as GHC++ -- Ubiquitous functions, they're found everywhere++debugging :: Bool+debugging = +#ifdef DEBUG+ True+#else+ False+#endif++traceSpan :: GHC.SrcSpan -> String+traceSpan s = GHC.showSDocUnsafe (GHC.ppr s)
+ test/PaperExamples.hs view
@@ -0,0 +1,80 @@+module Main where++import qualified Data.List as List++type P = Int++data L = Atom P | NegAtom P+ deriving Eq++data Fm = + Lit L+ | Not Fm+ | And Fm Fm+ | Or Fm Fm+ | Imp Fm Fm++nnf :: Fm -> Fm+nnf (And p q) = And (nnf p) (nnf q)+nnf (Or p q) = Or (nnf p) (nnf q)+nnf (Imp p q) = Or (nnf (Not p)) (nnf q) +nnf (Not (Not p)) = nnf p +nnf (Not (And p q)) = Or (nnf (Not p)) (nnf (Not q))+nnf (Not (Or p q)) = And (nnf (Not p)) (nnf (Not q))+nnf (Not (Imp p q)) = And (nnf p) (nnf (Not q))+nnf (Not (Lit (Atom x))) = Lit (NegAtom x)+nnf (Not (Lit (NegAtom x))) = Lit (Atom x)+nnf (Lit (Atom x)) = Lit (Atom x)+nnf (Lit (NegAtom x)) = Lit (NegAtom x)++distrib xss yss = List.nub [ List.union xs ys | xs <- xss, ys <- yss ]++nnf2dnf (And p q) = distrib (nnf2dnf p) (nnf2dnf q)+nnf2dnf (Or p q) = List.union (nnf2dnf p) (nnf2dnf q)+nnf2dnf (Lit a) = [[a]]+nnf2dnf _ = error "Impossible!"++dnf = nnf2dnf . nnf++k x y = x++data Arith = L Int | Plus | Mult+data Lam = Cst Arith | App Lam Lam | Abs (Lam -> Lam) | FVr String | BVr Int++lkup :: [(String,a)] -> String -> a+lkup ((s,x):ps) t = if s == t then x else lkup ps t++cloSub :: [(String, Lam)] -> Lam -> Lam+cloSub m (FVr s) = lkup m s+cloSub m (Cst c) = Cst c+cloSub m (App u v) = App (cloSub m u) (cloSub m v)++f :: Lam -> Lam+f x = k x (f (f x))++-- Bugs++nnf' :: Fm -> Fm+nnf' (And p q) = And (nnf' p) (nnf' q)+nnf' (Or p q) = Or (nnf' p) (nnf' q)+nnf' (Imp p q) = Or (Not (nnf' p)) (nnf' q) +nnf' (Not (Not p)) = nnf' p +nnf' (Not (And p q)) = Or (nnf' (Not p)) (nnf' (Not q))+nnf' (Not (Or p q)) = And (nnf' (Not p)) (nnf' (Not q))+nnf' (Not (Imp p q)) = And (nnf' p) (nnf' (Not q))+nnf' (Not (Lit (Atom x))) = Lit (NegAtom x)+nnf' (Not (Lit (NegAtom x))) = Lit (Atom x)+nnf' (Lit (Atom x)) = Lit (Atom x)+nnf' (Lit (NegAtom x)) = Lit (NegAtom x)++dnf' = nnf2dnf . nnf'++willNotCrash = dnf' (And (Lit (Atom 1)) (Lit (Atom 2)))+willCrash = + dnf' (Imp (Lit (Atom 1)) + (And (Lit (Atom 2)) + (Or (Lit (NegAtom 3)) (Lit (Atom 1)))))++main :: IO ()+main = return ()+