twee-lib 2.1.5 → 2.2
raw patch · 10 files changed
+97/−111 lines, 10 filessetup-changed
Files
- Setup.hs +0/−2
- Twee.hs +1/−2
- Twee/CP.hs +3/−3
- Twee/Index.hs +5/−1
- Twee/Join.hs +8/−8
- Twee/Proof.hs +62/−77
- Twee/Rule.hs +5/−5
- Twee/Term.hs +5/−1
- Twee/Term/Core.hs +5/−1
- twee-lib.cabal +3/−11
− Setup.hs
@@ -1,2 +0,0 @@-import Distribution.Simple-main = defaultMain
Twee.hs view
@@ -7,7 +7,7 @@ import qualified Twee.Rule as Rule import Twee.Equation import qualified Twee.Proof as Proof-import Twee.Proof(Proof, Axiom(..), Lemma(..), ProvedGoal(..), provedGoal, certify, derivation, symm)+import Twee.Proof(Axiom(..), Proof(..), ProvedGoal(..), provedGoal, certify, derivation, symm) import Twee.CP hiding (Config) import qualified Twee.CP as CP import Twee.Join hiding (Config, defaultConfig)@@ -300,7 +300,6 @@ instance Has (ActiveRule f) Depth where the = rule_depth instance f ~ g => Has (ActiveRule f) (Rule g) where the = rule_rule instance f ~ g => Has (ActiveRule f) (Proof g) where the = rule_proof-instance f ~ g => Has (ActiveRule f) (Lemma g) where the x = Lemma (the x) (the x) instance f ~ g => Has (ActiveRule f) (Positions g) where the = rule_positions newtype RuleId = RuleId Id deriving (Eq, Ord, Show, Num, Real, Integral, Enum)
Twee/CP.hs view
@@ -14,7 +14,7 @@ import Twee.Utils import Twee.Equation import qualified Twee.Proof as Proof-import Twee.Proof(Derivation, Lemma, congPath)+import Twee.Proof(Derivation, Proof, congPath) -- | The set of positions at which a term can have critical overlaps. data Positions f = NilP | ConsP {-# UNPACK #-} !Int !(Positions f)@@ -300,7 +300,7 @@ -- | Make a critical pair from two rules and an overlap. {-# INLINEABLE makeCriticalPair #-} makeCriticalPair ::- (Has a (Rule f), Has a (Lemma f), Has a Id, Function f) =>+ (Has a (Rule f), Has a (Proof f), Has a Id, Function f) => a -> a -> Overlap f -> Maybe (CriticalPair f) makeCriticalPair r1 r2 overlap@Overlap{..} | lessEq overlap_top t = Nothing@@ -318,7 +318,7 @@ {-# INLINEABLE overlapProof #-} overlapProof :: forall a f.- (Has a (Rule f), Has a (Lemma f), Has a Id) =>+ (Has a (Rule f), Has a (Proof f), Has a Id) => a -> a -> Overlap f -> Derivation f overlapProof left right Overlap{..} = Proof.symm (reductionProof (step left leftSub))
Twee/Index.hs view
@@ -5,9 +5,13 @@ -- the search term is an instance of the key, and return the corresponding -- values. -{-# LANGUAGE BangPatterns, RecordWildCards, OverloadedStrings, FlexibleContexts #-}+{-# LANGUAGE BangPatterns, RecordWildCards, OverloadedStrings, FlexibleContexts, CPP #-} -- We get some bogus warnings because of pattern synonyms. {-# OPTIONS_GHC -fno-warn-overlapping-patterns #-}+{-# OPTIONS_GHC -O2 -fmax-worker-args=100 #-}+#ifdef USE_LLVM+{-# OPTIONS_GHC -fllvm #-}+#endif module Twee.Index( Index, empty,
Twee/Join.hs view
@@ -5,7 +5,7 @@ import Twee.Base import Twee.Rule import Twee.Equation-import Twee.Proof(Lemma)+import Twee.Proof(Proof) import qualified Twee.Proof as Proof import Twee.CP hiding (Config) import Twee.Constraints@@ -33,7 +33,7 @@ {-# INLINEABLE joinCriticalPair #-} joinCriticalPair ::- (Function f, Has a (Rule f), Has a (Lemma f)) =>+ (Function f, Has a (Rule f), Has a (Proof f)) => Config -> Index f (Equation f) -> RuleIndex f a -> Maybe (Model f) -> -- A model to try before checking ground joinability@@ -67,7 +67,7 @@ {-# INLINEABLE step3 #-} {-# INLINEABLE allSteps #-} step1, step2, step3, allSteps ::- (Function f, Has a (Rule f), Has a (Lemma f)) =>+ (Function f, Has a (Rule f), Has a (Proof f)) => Config -> Index f (Equation f) -> RuleIndex f a -> CriticalPair f -> Maybe (CriticalPair f) allSteps config eqns idx cp = step1 config eqns idx cp >>=@@ -104,7 +104,7 @@ {-# INLINEABLE joinWith #-} joinWith ::- (Has a (Rule f), Has a (Lemma f)) =>+ (Has a (Rule f), Has a (Proof f)) => Index f (Equation f) -> RuleIndex f a -> (Term f -> Term f -> Resulting f) -> CriticalPair f -> Maybe (CriticalPair f) joinWith eqns idx reduce cp@CriticalPair{cp_eqn = lhs :=: rhs, ..} | subsumed eqns idx eqn = Nothing@@ -122,7 +122,7 @@ {-# INLINEABLE subsumed #-} subsumed ::- (Has a (Rule f), Has a (Lemma f)) =>+ (Has a (Rule f), Has a (Proof f)) => Index f (Equation f) -> RuleIndex f a -> Equation f -> Bool subsumed eqns idx (t :=: u) | t == u = True@@ -146,7 +146,7 @@ {-# INLINEABLE groundJoin #-} groundJoin ::- (Function f, Has a (Rule f), Has a (Lemma f)) =>+ (Function f, Has a (Rule f), Has a (Proof f)) => Config -> Index f (Equation f) -> RuleIndex f a -> [Branch f] -> CriticalPair f -> Either (Model f) [CriticalPair f] groundJoin config eqns idx ctx cp@CriticalPair{cp_eqn = t :=: u, ..} = case partitionEithers (map (solve (usort (atoms t ++ atoms u))) ctx) of@@ -158,7 +158,7 @@ {-# INLINEABLE groundJoinFrom #-} groundJoinFrom ::- (Function f, Has a (Rule f), Has a (Lemma f)) =>+ (Function f, Has a (Rule f), Has a (Proof f)) => Config -> Index f (Equation f) -> RuleIndex f a -> Model f -> [Branch f] -> CriticalPair f -> Either (Model f) [CriticalPair f] groundJoinFrom config@Config{..} eqns idx model ctx cp@CriticalPair{cp_eqn = t :=: u, ..} | not cfg_ground_join ||@@ -197,7 +197,7 @@ {-# INLINEABLE groundJoinFromMaybe #-} groundJoinFromMaybe ::- (Function f, Has a (Rule f), Has a (Lemma f)) =>+ (Function f, Has a (Rule f), Has a (Proof f)) => Config -> Index f (Equation f) -> RuleIndex f a -> Maybe (Model f) -> [Branch f] -> CriticalPair f -> Either (Model f) [CriticalPair f] groundJoinFromMaybe config eqns idx Nothing = groundJoin config eqns idx groundJoinFromMaybe config eqns idx (Just model) = groundJoinFrom config eqns idx model
Twee/Proof.hs view
@@ -2,7 +2,7 @@ {-# LANGUAGE TypeFamilies, PatternGuards, RecordWildCards, ScopedTypeVariables #-} module Twee.Proof( -- * Constructing proofs- Proof, Derivation(..), Lemma(..), Axiom(..),+ Proof, Derivation(..), Axiom(..), certify, equation, derivation, -- ** Smart constructors for derivations lemma, axiom, symm, trans, cong, congPath,@@ -37,13 +37,13 @@ Proof { equation :: !(Equation f), derivation :: !(Derivation f) }- deriving (Eq, Show)+ deriving Show -- | A derivation is an unchecked proof. It might be wrong! -- The way to check it is to call 'certify' to turn it into a 'Proof'. data Derivation f = -- | Apply an existing rule (with proof!) to the root of a term- UseLemma {-# UNPACK #-} !(Lemma f) !(Subst f)+ UseLemma {-# UNPACK #-} !(Proof f) !(Subst f) -- | Apply an axiom to the root of a term | UseAxiom {-# UNPACK #-} !(Axiom f) !(Subst f) -- | Reflexivity. @'Refl' t@ proves @t = t@.@@ -58,16 +58,6 @@ | Cong {-# UNPACK #-} !(Fun f) ![Derivation f] deriving (Eq, Show) --- | A lemma, which includes a proof.-data Lemma f =- Lemma {- -- | The id number of the lemma.- -- Has no semantic meaning; for convenience only.- lemma_id :: {-# UNPACK #-} !Id,- -- | A proof of the lemma.- lemma_proof :: !(Proof f) }- deriving Show- -- | An axiom, which comes without proof. data Axiom f = Axiom {@@ -95,8 +85,8 @@ Nothing -> error ("Invalid proof created!\n" ++ prettyShow p) Just eqn -> Proof eqn p where- check (UseLemma Lemma{..} sub) =- return (subst sub (equation lemma_proof))+ check (UseLemma proof sub) =+ return (subst sub (equation proof)) check (UseAxiom Axiom{..} sub) = return (subst sub axiom_eqn) check (Refl t) =@@ -124,14 +114,12 @@ ---------------------------------------------------------------------- -- Typeclass instances.-instance Eq (Lemma f) where+instance Eq (Proof f) where x == y = compare x y == EQ-instance Ord (Lemma f) where- compare =- comparing (\x ->- -- Don't look into lemma proofs when comparing derivations,- -- to avoid exponential blowup- (lemma_id x, equation (lemma_proof x)))+instance Ord (Proof f) where+ -- Don't look at the proof itself, to prevent exponential blowup+ -- when a proof contains UseLemma+ compare = comparing equation instance Symbolic (Derivation f) where type ConstantOf (Derivation f) = f@@ -150,10 +138,10 @@ subst_ sub (Cong f ps) = cong f (subst_ sub ps) instance Function f => Pretty (Proof f) where- pPrint = pPrintLemma defaultConfig prettyShow+ pPrint = pPrintLemma defaultConfig (prettyShow . axiom_number) (prettyShow . equation) instance PrettyTerm f => Pretty (Derivation f) where pPrint (UseLemma lemma sub) =- text "subst" <#> pPrintTuple [pPrint lemma, pPrint sub]+ text "subst" <#> pPrintTuple [text "lemma" <#> pPrint (equation lemma), pPrint sub] pPrint (UseAxiom axiom sub) = text "subst" <#> pPrintTuple [pPrint axiom, pPrint sub] pPrint (Refl t) =@@ -170,11 +158,6 @@ text "axiom" <#> pPrintTuple [pPrint axiom_number, text axiom_name, pPrint axiom_eqn] -instance PrettyTerm f => Pretty (Lemma f) where- pPrint Lemma{..} =- text "lemma" <#>- pPrintTuple [pPrint lemma_id, pPrint (equation lemma_proof)]- -- | Simplify a derivation. -- -- After simplification, a derivation has the following properties:@@ -182,25 +165,25 @@ -- * 'Symm' is pushed down next to 'Lemma' and 'Axiom' -- * 'Refl' only occurs inside 'Cong' or at the top level -- * 'Trans' is right-associated and is pushed inside 'Cong' if possible-simplify :: Minimal f => (Lemma f -> Maybe (Derivation f)) -> Derivation f -> Derivation f+simplify :: Minimal f => (Proof f -> Maybe (Derivation f)) -> Derivation f -> Derivation f simplify lem p = simp p where- simp p@(UseLemma lemma sub) =- case lem lemma of+ simp p@(UseLemma q sub) =+ case lem q of Nothing -> p- Just q ->+ Just r -> let -- Get rid of any variables that are not bound by sub -- (e.g., ones which only occur internally in q)- dead = usort (vars q) \\ substDomain sub- in simp (subst sub (erase dead q))+ dead = usort (vars r) \\ substDomain sub+ in simp (subst sub (erase dead r)) simp (Symm p) = symm (simp p) simp (Trans p q) = trans (simp p) (simp q) simp (Cong f ps) = cong f (map simp ps) simp p = p -lemma :: Lemma f -> Subst f -> Derivation f-lemma lem@Lemma{..} sub = UseLemma lem sub+lemma :: Proof f -> Subst f -> Derivation f+lemma p sub = UseLemma p sub axiom :: Axiom f -> Derivation f axiom ax@Axiom{..} =@@ -244,15 +227,15 @@ unRefl _ = Nothing -- | Find all lemmas which are used in a derivation.-usedLemmas :: Derivation f -> [Lemma f]+usedLemmas :: Derivation f -> [Proof f] usedLemmas p = map fst (usedLemmasAndSubsts p) -- | Find all lemmas which are used in a derivation, -- together with the substitutions used.-usedLemmasAndSubsts :: Derivation f -> [(Lemma f, Subst f)]+usedLemmasAndSubsts :: Derivation f -> [(Proof f, Subst f)] usedLemmasAndSubsts p = lem p [] where- lem (UseLemma lemma sub) = ((lemma, sub):)+ lem (UseLemma p sub) = ((p, sub):) lem (Symm p) = lem p lem (Trans p q) = lem p . lem q lem (Cong _ ps) = foldr (.) id (map lem ps)@@ -313,7 +296,7 @@ -- | The used axioms. pres_axioms :: [Axiom f], -- | The used lemmas.- pres_lemmas :: [Lemma f],+ pres_lemmas :: [Proof f], -- | The goals proved. pres_goals :: [ProvedGoal f] } deriving Show@@ -367,18 +350,19 @@ present config goals = -- First find all the used lemmas, then hand off to presentWithGoals presentWithGoals config goals- (used Set.empty (concatMap (usedLemmas . derivation . pg_proof) goals))+ (snd (used Set.empty (concatMap (usedLemmas . derivation . pg_proof) goals))) where- used lems [] = Set.elems lems+ used lems [] = (lems, []) used lems (x:xs) | x `Set.member` lems = used lems xs | otherwise =- used (Set.insert x lems)- (usedLemmas (derivation (lemma_proof x)) ++ xs)+ let (lems1, ys) = used (Set.insert x lems) (usedLemmas (derivation x))+ (lems2, zs) = used lems1 xs+ in (lems2, ys ++ [x] ++ zs) presentWithGoals :: Function f =>- Config -> [ProvedGoal f] -> [Lemma f] -> Presentation f+ Config -> [ProvedGoal f] -> [Proof f] -> Presentation f presentWithGoals config@Config{..} goals lemmas -- We inline a lemma if one of the following holds: -- * It only has one step@@ -392,11 +376,10 @@ let axioms = usort $ concatMap (usedAxioms . derivation . pg_proof) goals ++- concatMap (usedAxioms . derivation . lemma_proof) lemmas+ concatMap (usedAxioms . derivation) lemmas in Presentation axioms- [ lemma { lemma_proof = flattenProof lemma_proof }- | lemma@Lemma{..} <- lemmas ]+ (map flattenProof lemmas) [ decodeGoal (goal { pg_proof = flattenProof pg_proof }) | goal@ProvedGoal{..} <- goals ] @@ -408,8 +391,8 @@ [ decodeGoal (goal { pg_proof = certify $ simplify inline (derivation pg_proof) }) | goal@ProvedGoal{..} <- goals ] lemmas' =- [ Lemma n (certify $ simplify inline (derivation p))- | lemma@(Lemma n p) <- lemmas, not (lemma `Map.member` inlinings) ]+ [ certify $ simplify inline (derivation lemma)+ | lemma <- lemmas, not (lemma `Map.member` inlinings) ] in presentWithGoals config goals' lemmas' @@ -419,25 +402,26 @@ [ (lemma, p) | lemma <- lemmas, Just p <- [tryInline lemma]] - tryInline (Lemma n p)- | shouldInline n p = Just (derivation p)- tryInline (Lemma n p)+ tryInline p+ | shouldInline p = Just (derivation p)+ tryInline p -- Check for subsumption by an earlier lemma- | Just (Lemma m q) <- Map.lookup (canonicalise (t :=: u)) equations, m < n =+ | Just (m, q) <- Map.lookup (canonicalise (t :=: u)) equations, m < n = Just (subsume p (derivation q))- | Just (Lemma m q) <- Map.lookup (canonicalise (u :=: t)) equations, m < n =+ | Just (m, q) <- Map.lookup (canonicalise (u :=: t)) equations, m < n = Just (subsume p (Symm (derivation q))) where t :=: u = equation p+ Just (n, _) = Map.lookup (canonicalise (equation p)) equations tryInline _ = Nothing - shouldInline n p =+ shouldInline p = cfg_no_lemmas || oneStep (derivation p) || (not cfg_all_lemmas && (isJust (decodeEquality (eqn_lhs (equation p))) || isJust (decodeEquality (eqn_rhs (equation p))) ||- Map.lookup n uses == Just 1))+ Map.lookup p uses == Just 1)) subsume p q = -- Rename q so its variables match p's@@ -450,17 +434,17 @@ -- Record which lemma proves each equation equations = Map.fromList- [ (canonicalise (equation lemma_proof), lemma)- | lemma@Lemma{..} <- lemmas]+ [ (canonicalise (equation p), (i, p))+ | (i, p) <- zip [0..] lemmas] -- Count how many times each lemma is used uses = Map.fromListWith (+)- [ (lemma_id, 1)- | Lemma{..} <-+ [ (p, 1)+ | p <- concatMap usedLemmas (map (derivation . pg_proof) goals ++- map (derivation . lemma_proof) lemmas) ]+ map derivation lemmas) ] -- Check if a proof only has one step. -- Trans only occurs at the top level by this point.@@ -471,8 +455,8 @@ invisible (t :=: u) = show (pPrint t) == show (pPrint u) -- Pretty-print the proof of a single lemma.-pPrintLemma :: Function f => Config -> (Id -> String) -> Proof f -> Doc-pPrintLemma Config{..} lemmaName p =+pPrintLemma :: Function f => Config -> (Axiom f -> String) -> (Proof f -> String) -> Proof f -> Doc+pPrintLemma Config{..} axiomNum lemmaNum p = ppTerm (eqn_lhs (equation q)) $$ pp (derivation q) where q = flattenProof p@@ -496,10 +480,10 @@ text "and" <+> text (last xs) - ppLemma (Lemma{..}, sub) =- text "lemma" <+> text (lemmaName lemma_id) <#> showSubst sub- ppAxiom (Axiom{..}, sub) =- text "axiom" <+> pPrint axiom_number <+> parens (text axiom_name) <#> showSubst sub+ ppLemma (p, sub) =+ text "lemma" <+> text (lemmaNum p) <#> showSubst sub+ ppAxiom (axiom@Axiom{..}, sub) =+ text "axiom" <+> text (axiomNum axiom) <+> parens (text axiom_name) <#> showSubst sub showSubst sub | cfg_show_instances && not (null (substToList sub)) =@@ -575,11 +559,11 @@ pPrintPresentation :: forall f. Function f => Config -> Presentation f -> Doc pPrintPresentation config (Presentation axioms lemmas goals) = vcat $ intersperse (text "") $- vcat [ describeEquation "Axiom" (show n) (Just name) eqn- | Axiom n name eqn <- axioms,+ vcat [ describeEquation "Axiom" (axiomNum axiom) (Just name) eqn+ | axiom@(Axiom _ name eqn) <- axioms, not (invisible eqn) ]:- [ pp "Lemma" (num n) Nothing (equation p) emptySubst p- | Lemma n p <- lemmas,+ [ pp "Lemma" (lemmaNum p) Nothing (equation p) emptySubst p+ | p <- lemmas, not (invisible (equation p)) ] ++ [ pp "Goal" (show num) (Just pg_name) pg_goal_hint pg_witness_hint pg_proof | (num, ProvedGoal{..}) <- zip [1..] goals ]@@ -588,11 +572,12 @@ describeEquation kind n mname eqn $$ ppWitness witness $$ text "Proof:" $$- pPrintLemma config num p+ pPrintLemma config axiomNum lemmaNum p - num x = show (fromJust (Map.lookup x nums))- nums = Map.fromList (zip (map lemma_id lemmas) [n+1 ..])- n = maximum $ 0:map axiom_number axioms+ axiomNums = Map.fromList (zip axioms [1..])+ lemmaNums = Map.fromList (zip lemmas [length axioms+1..])+ axiomNum x = show (fromJust (Map.lookup x axiomNums))+ lemmaNum x = show (fromJust (Map.lookup x lemmaNums)) ppWitness sub | sub == emptySubst = pPrintEmpty
Twee/Rule.hs view
@@ -18,7 +18,7 @@ import Data.Ord import Twee.Equation import qualified Twee.Proof as Proof-import Twee.Proof(Derivation, Lemma(..))+import Twee.Proof(Derivation, Proof) import Data.Tuple --------------------------------------------------------------------------------@@ -229,7 +229,7 @@ -- | A multi-step rewrite proof @t ->* u@ data Reduction f = -- | Apply a single rewrite rule to the root of a term- Step {-# UNPACK #-} !(Lemma f) !(Rule f) !(Subst f)+ Step {-# UNPACK #-} !(Proof f) !(Rule f) !(Subst f) -- | Reflexivity | Refl {-# UNPACK #-} !(Term f) -- | Transivitity@@ -290,7 +290,7 @@ -- | Construct a basic rewrite step. {-# INLINE step #-}-step :: (Has a (Rule f), Has a (Lemma f)) => a -> Subst f -> Reduction f+step :: (Has a (Rule f), Has a (Proof f)) => a -> Subst f -> Reduction f step x sub = Step (the x) (the x) sub ----------------------------------------------------------------------@@ -420,14 +420,14 @@ -- | A strategy which rewrites using an index. {-# INLINE rewrite #-}-rewrite :: (Function f, Has a (Rule f), Has a (Lemma f)) => (Rule f -> Subst f -> Bool) -> Index f a -> Strategy f+rewrite :: (Function f, Has a (Rule f), Has a (Proof f)) => (Rule f -> Subst f -> Bool) -> Index f a -> Strategy f rewrite p rules t = do rule <- Index.approxMatches t rules tryRule p rule t -- | A strategy which applies one rule only. {-# INLINEABLE tryRule #-}-tryRule :: (Function f, Has a (Rule f), Has a (Lemma f)) => (Rule f -> Subst f -> Bool) -> a -> Strategy f+tryRule :: (Function f, Has a (Rule f), Has a (Proof f)) => (Rule f -> Subst f -> Bool) -> a -> Strategy f tryRule p rule t = do sub <- maybeToList (match (lhs (the rule)) t) guard (p (the rule) sub)
Twee/Term.hs view
@@ -13,7 +13,11 @@ -- * substitutions ('Substitution', 'Subst', 'subst'); -- * unification ('unify') and matching ('match'); -- * miscellaneous useful functions on terms.-{-# LANGUAGE BangPatterns, PatternSynonyms, ViewPatterns, TypeFamilies, OverloadedStrings, ScopedTypeVariables #-}+{-# LANGUAGE BangPatterns, PatternSynonyms, ViewPatterns, TypeFamilies, OverloadedStrings, ScopedTypeVariables, CPP #-}+{-# OPTIONS_GHC -O2 -fmax-worker-args=100 #-}+#ifdef USE_LLVM+{-# OPTIONS_GHC -fllvm #-}+#endif module Twee.Term( -- * Terms Term, pattern Var, pattern App, isApp, isVar, singleton, len,
Twee/Term/Core.hs view
@@ -3,7 +3,11 @@ -- and provides primitives for building higher-level stuff. {-# LANGUAGE CPP, PatternSynonyms, ViewPatterns, MagicHash, UnboxedTuples, BangPatterns,- RankNTypes, RecordWildCards, GeneralizedNewtypeDeriving #-}+ RankNTypes, RecordWildCards, GeneralizedNewtypeDeriving, CPP #-}+{-# OPTIONS_GHC -O2 -fmax-worker-args=100 #-}+#ifdef USE_LLVM+{-# OPTIONS_GHC -fllvm #-}+#endif module Twee.Term.Core where import Data.Primitive(sizeOf)
twee-lib.cabal view
@@ -1,5 +1,5 @@ name: twee-lib-version: 2.1.5+version: 2.2 synopsis: An equational theorem prover homepage: http://github.com/nick8325/twee license: BSD3@@ -29,14 +29,6 @@ location: git://github.com/nick8325/twee.git branch: master -flag static- description: Build a static binary.- default: False--flag static-cxx- description: Build a binary which statically links against libstdc++.- default: False- flag llvm description: Build using LLVM backend for faster code. default: False@@ -80,11 +72,11 @@ primitive >= 0.6.2.0, vector hs-source-dirs: .- ghc-options: -W -fno-warn-incomplete-patterns -O2 -fmax-worker-args=100+ ghc-options: -W -fno-warn-incomplete-patterns default-language: Haskell2010 if flag(llvm)- ghc-options: -fllvm+ cpp-options: -DUSE_LLVM if flag(bounds-checks) cpp-options: -DBOUNDS_CHECKS exposed-modules: