More aggressive goal simplification.

This commit is contained in:
Iavor S. Diatchki 2017-01-31 14:12:53 -08:00
parent 12bb2c30c8
commit b788079244
13 changed files with 148 additions and 67 deletions

View File

@ -123,6 +123,7 @@ library
Cryptol.TypeCheck.TypeOf,
Cryptol.TypeCheck.Sanity,
Cryptol.TypeCheck.Solver.Types,
Cryptol.TypeCheck.Solver.InfNat,
Cryptol.TypeCheck.Solver.Class,
Cryptol.TypeCheck.Solver.Selector,

View File

@ -28,6 +28,7 @@ import Cryptol.ModuleSystem.Name (asPrim,nameLoc)
import Cryptol.TypeCheck.PP
import Cryptol.Utils.Ident (Ident,identText)
import Cryptol.Utils.Panic(panic)
import Cryptol.Utils.Misc(anyJust)
import qualified Data.Set as Set
import qualified Data.IntMap as IntMap
@ -46,20 +47,24 @@ data SolverConfig = SolverConfig
data VarType = ExtVar Schema -- ^ Known type
| CurSCC Expr Type -- ^ Part of current SCC
newtype Goals = Goals (TypeMap Goal)
-- XXX: Temporary, until we figure out:
-- 1. How to apply substitutions with normalization to the type Map
-- 2. What are the strictness requirements
-- (e.g., using Set results in a black hole)
newtype Goals = Goals [Goal] -- Goals (TypeMap Goal)
deriving (Show)
emptyGoals :: Goals
emptyGoals = Goals emptyTM
emptyGoals = Goals [] -- emptyTM
nullGoals :: Goals -> Bool
nullGoals (Goals tm) = nullTM tm
nullGoals (Goals tm) = null tm -- nullTM tm
fromGoals :: Goals -> [Goal]
fromGoals (Goals tm) = membersTM tm
fromGoals (Goals tm) = tm -- membersTM tm
insertGoal :: Goal -> Goals -> Goals
insertGoal g (Goals tm) = Goals (insertTM (goal g) g tm)
insertGoal g (Goals tm) = Goals (g : tm) -- (insertTM (goal g) g tm)
-- | Something that we need to find evidence for.
data Goal = Goal
@ -68,6 +73,12 @@ data Goal = Goal
, goal :: Prop -- ^ What needs to be proved
} deriving (Show, Generic, NFData)
instance Eq Goal where
x == y = goal x == goal y
instance Ord Goal where
compare x y = compare (goal x) (goal y)
data HasGoal = HasGoal
{ hasName :: !Int
, hasGoal :: Goal
@ -81,11 +92,6 @@ data DelayedCt = DelayedCt
, dctGoals :: [Goal]
} deriving (Show, Generic, NFData)
data Solved = SolvedIf [Prop] -- ^ Solved, assuming the sub-goals.
| Unsolved -- ^ We could not solve the goal.
| Unsolvable TCErrorMessage -- ^ The goal can never be solved.
deriving (Show)
data Warning = DefaultingKind (P.TParam Name) P.Kind
| DefaultingWildType P.Kind
| DefaultingTo Doc Type
@ -289,6 +295,17 @@ instance FVS DelayedCt where
-- values that remain, as applying the substitution to the keys will only ever
-- reduce the number of values that remain.
instance TVars Goals where
apSubst su (Goals gs) = case anyJust apG gs of
Nothing -> Goals gs
Just gs1 -> Goals $ concatMap norm gs1
where
norm g = [ g { goal = p } | p <- pSplitAnd (goal g) ]
apG g = mk g <$> apSubstMaybe su (goal g)
mk g p = g { goal = p }
{-
apSubst su (Goals gs) = Goals (Set.fromList . mapAp
apSubst su (Goals goals) =
Goals (mapWithKeyTM setGoal (apSubstTypeMapKeys su goals))
where
@ -298,6 +315,7 @@ instance TVars Goals where
setGoal key g = g { goalSource = apSubst su (goalSource g)
, goal = key
}
-}
instance TVars Goal where
apSubst su g = Goal { goalSource = apSubst su (goalSource g)
@ -559,9 +577,4 @@ instance PP (WithNames DelayedCt) where
ns1 = addTNames (dctForall d) names
instance PP Solved where
ppPrec _ res =
case res of
SolvedIf ps -> text "solved" $$ nest 2 (vcat (map pp ps))
Unsolved -> text "unsolved"
Unsolvable e -> text "unsolvable" <> colon <+> text (tcErrorMessage e)

View File

@ -5,19 +5,17 @@
-- Maintainer : cryptol@galois.com
-- Stability : provisional
-- Portability : portable
{-# LANGUAGE Trustworthy #-}
{-# LANGUAGE Safe #-}
{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE RecordWildCards #-}
{-# LANGUAGE RecursiveDo #-}
{-# LANGUAGE PatternGuards #-}
module Cryptol.TypeCheck.Monad
( module Cryptol.TypeCheck.Monad
, module Cryptol.TypeCheck.InferTypes
) where
import Debug.Trace
import Cryptol.ModuleSystem.Name (FreshM(..),Supply)
import Cryptol.Parser.Position
import qualified Cryptol.Parser.AST as P
@ -310,10 +308,13 @@ newGoal goalSource goal =
do goalRange <- curRange
return Goal { .. }
newGoals :: ConstraintSource -> [Prop] -> InferM ()
newGoals = newGoals' True
-- | Record some constraints that need to be solved.
-- The string explains where the constraints came from.
newGoals :: ConstraintSource -> [Prop] -> InferM ()
newGoals src ps = addGoals =<< mapM (newGoal src) ps
newGoals' :: Bool -> ConstraintSource -> [Prop] -> InferM ()
newGoals' simp src ps = addGoals' simp =<< mapM (newGoal src) ps
{- | The constraints are removed, and returned to the caller.
The substitution IS applied to them. -}
@ -322,17 +323,14 @@ getGoals =
do goals <- applySubst =<< IM (sets $ \s -> (iCts s, s { iCts = emptyGoals }))
return (fromGoals goals)
-- | Add a bunch of goals that need solving.
-- XXX: FOR SOME REASON WE CAN'T BE STRICT IN THE GOALS HERE. WHY IS THAT?
addGoals :: [Goal] -> InferM ()
addGoals = doAdd {- mapM_ simpG
where
simpG g = trace (show (pp (goal g)))
$ case Simple.simplify Map.empty [goal g] of
Left e -> recordError $ ErrorMsg $ text $ tcErrorMessage e
Right ps -> doAdd [ g { goal = p } | p <- ps ] -}
addGoals = addGoals' True
-- | Add a bunch of goals that need solving.
addGoals' :: Bool -> [Goal] -> InferM ()
addGoals' simp gs0
| simp = doAdd =<< simpGoals gs0
| otherwise = doAdd gs0
where
doAdd [] = return ()
doAdd gs = IM $ sets_ $ \s -> s { iCts = foldl (flip insertGoal) (iCts s) gs }
@ -355,6 +353,17 @@ collectGoals m =
-- set the type map directly
setGoals' gs = IM $ sets $ \ RW { .. } -> ((), RW { iCts = gs, .. })
simpGoal :: Goal -> InferM [Goal]
simpGoal g =
case Simple.simplify Map.empty (goal g) of
p | Just e <- tIsError p ->
do recordError $ ErrorMsg $ text $ tcErrorMessage e
return []
| ps <- pSplitAnd p -> return [ g { goal = pr } | pr <- ps ]
simpGoals :: [Goal] -> InferM [Goal]
simpGoals gs = concat <$> mapM simpGoal gs
{- | Record a constraint that when we select from the first type,
@ -729,6 +738,9 @@ kRecordWarning :: Warning -> KindM ()
kRecordWarning w = kInInferM $ recordWarning w
-- | Generate a fresh unification variable of the given kind.
-- NOTE: We do not simplify these, because we end up with bottom.
-- See `Kind.hs`
-- XXX: Perhaps we can avoid the recursion?
kNewType :: Doc -> Kind -> KindM Type
kNewType src k =
do tps <- KM $ do vs <- asks lazyTVars
@ -767,7 +779,7 @@ kInRange r (KM m) = KM $
return a
kNewGoals :: ConstraintSource -> [Prop] -> KindM ()
kNewGoals c ps = kInInferM $ newGoals c ps
kNewGoals c ps = kInInferM $ newGoals' False c ps
kInInferM :: InferM a -> KindM a
kInInferM m = KM $ lift $ lift m

View File

@ -1,9 +1,9 @@
module Cryptol.TypeCheck.SimpleSolver (simplify) where
module Cryptol.TypeCheck.SimpleSolver (simplify,simplifyStep) where
import Data.Map(Map)
import Cryptol.TypeCheck.Type
import Cryptol.TypeCheck.InferTypes(Solved(..))
import Cryptol.TypeCheck.Solver.Types
import Cryptol.TypeCheck.Solver.Numeric.Fin(cryIsFinType)
import Cryptol.TypeCheck.Solver.Numeric.Interval(Interval)
import Cryptol.TypeCheck.Solver.Numeric(cryIsEqual, cryIsNotEqual, cryIsGeq)
@ -11,18 +11,20 @@ import Cryptol.TypeCheck.Solver.Class(solveArithInst,solveCmpInst)
type Ctxt = Map TVar Interval
simplify :: Ctxt -> [Prop] -> Either TCErrorMessage [Prop]
simplify _ [] = Right []
simplify ctxt (p : ps) =
simplify :: Ctxt -> Prop -> Prop
simplify ctxt p =
case simplifyStep ctxt p of
Unsolvable e -> Left e
Unsolved -> fmap (p :) (simplify ctxt ps)
SolvedIf ps1 -> simplify ctxt (ps1 ++ ps)
Unsolvable e -> pError e
Unsolved -> p
SolvedIf ps -> pAnd (map (simplify ctxt) ps)
simplifyStep :: Ctxt -> Prop -> Solved
simplifyStep ctxt prop =
case tNoUser prop of
TCon (PC PTrue) [] -> SolvedIf []
TCon (PC PAnd) [l,r] -> SolvedIf [l,r]
TCon (PC PArith) [ty] -> solveArithInst ty
TCon (PC PCmp) [ty] -> solveCmpInst ty

View File

@ -27,8 +27,11 @@ import Cryptol.TypeCheck.Subst
(apSubst,fvs,singleSubst, isEmptySubst,
emptySubst,Subst,listSubst, (@@), Subst,
apSubstMaybe, substBinds)
import Cryptol.TypeCheck.Solver.Class
import qualified Cryptol.TypeCheck.SimpleSolver as Simplify
import Cryptol.TypeCheck.Solver.Types
import Cryptol.TypeCheck.Solver.Selector(tryHasGoal)
import qualified Cryptol.TypeCheck.Solver.Numeric.AST as Num
import qualified Cryptol.TypeCheck.Solver.Numeric.ImportExport as Num
import Cryptol.TypeCheck.Solver.Numeric.Interval (Interval)
@ -88,10 +91,9 @@ simplifyAllConstraints =
case gs of
[] -> return ()
_ ->
do r <- curRange
let n = length gs
io $ putStrLn $ "simplifyAllConstraints " ++ show (length gs) ++ " goals." ++ show r
if (n > 100) then io $ writeFile "GS" $ unlines $ map (show.pp.goal) gs else return ()
do -- r <- curRange
io $ putStrLn $ "simplifyAllConstraints " ++ show (length gs)
io $ putStrLn $ unlines [ " " ++ show (pp (goal g), pp (goalSource g)) | g <- gs ]
solver <- getSolver
(mb,su) <- io (simpGoals' solver gs)
extendSubst su
@ -292,7 +294,7 @@ solveConstraints s otherGs gs0 =
case Num.numericRight g of
Right n -> solveClassCts unsolved (n : numerics) gs
Left c ->
case classStep (goal c) of
case Simplify.simplifyStep Map.empty (goal c) of
Unsolvable _ -> return (Left [g])
Unsolved -> solveClassCts (g : unsolved) numerics gs
SolvedIf subs ->

View File

@ -16,8 +16,8 @@ module Cryptol.TypeCheck.Solver.Class
, expandProp
) where
import Cryptol.TypeCheck.AST
import Cryptol.TypeCheck.InferTypes(Solved(..))
import Cryptol.TypeCheck.Type
import Cryptol.TypeCheck.Solver.Types
-- | Solve class constraints.
-- If not, then we return 'Nothing'.

View File

@ -24,9 +24,10 @@ module Cryptol.TypeCheck.Solver.CrySAT
) where
import qualified Cryptol.TypeCheck.AST as Cry
import Cryptol.TypeCheck.InferTypes(Goal(..), SolverConfig(..), Solved(..))
import Cryptol.TypeCheck.InferTypes(Goal(..), SolverConfig(..))
import qualified Cryptol.TypeCheck.Subst as Cry
import Cryptol.TypeCheck.Solver.Types
import Cryptol.TypeCheck.Solver.Numeric.AST
import Cryptol.TypeCheck.Solver.Numeric.Fin
import Cryptol.TypeCheck.Solver.Numeric.ImportExport

View File

@ -5,9 +5,9 @@ module Cryptol.TypeCheck.Solver.Numeric
import Data.Map(Map)
import Cryptol.TypeCheck.Type
import Cryptol.TypeCheck.PP
import Cryptol.TypeCheck.InferTypes
import Cryptol.TypeCheck.Type
import Cryptol.TypeCheck.Solver.Types
import Cryptol.TypeCheck.Solver.InfNat
import Cryptol.TypeCheck.Solver.Numeric.Interval

View File

@ -13,8 +13,8 @@ module Cryptol.TypeCheck.Solver.Numeric.Fin where
import Data.Map (Map)
import Cryptol.TypeCheck.AST
import Cryptol.TypeCheck.InferTypes
import Cryptol.TypeCheck.Type
import Cryptol.TypeCheck.Solver.Types
import Cryptol.TypeCheck.Solver.Numeric.Interval
import Cryptol.TypeCheck.Solver.InfNat

View File

@ -14,8 +14,8 @@ module Cryptol.TypeCheck.Solver.Simplify (
) where
import Cryptol.Prims.Syntax (TFun(..))
import Cryptol.TypeCheck.AST (Type(..),Prop,TVar,pIsEq,isFreeTV,TCon(..))
import Cryptol.TypeCheck.Type(Type(..),Prop,TVar,TCon(..),TFun(..)
,pIsEq,isFreeTV,tAdd,tSub)
import Cryptol.TypeCheck.Solver.Numeric.Interval (Interval,iIsFin,typeInterval)
import Cryptol.TypeCheck.Subst (fvs)
@ -144,16 +144,16 @@ rewriteLHS fins uvar = go
-- invert the type function to balance the equation, when the variable occurs
-- on the LHS of the expression `x tf y`
balanceR x TCAdd y rhs = do guardFin y
go x (TCon (TF TCSub) [rhs,y])
balanceR x TCSub y rhs = go x (TCon (TF TCAdd) [rhs,y])
go x (tSub rhs y)
balanceR x TCSub y rhs = go x (tAdd rhs y)
balanceR _ _ _ _ = mzero
-- invert the type function to balance the equation, when the variable occurs
-- on the RHS of the expression `x tf y`
balanceL x TCAdd y rhs = do guardFin y
go y (TCon (TF TCSub) [rhs,x])
balanceL x TCSub y rhs = go (TCon (TF TCAdd) [rhs,y]) x
go y (tSub rhs x)
balanceL x TCSub y rhs = go (tAdd rhs y) x
balanceL _ _ _ _ = mzero

View File

@ -0,0 +1,16 @@
module Cryptol.TypeCheck.Solver.Types where
import Cryptol.TypeCheck.Type
import Cryptol.TypeCheck.PP
data Solved = SolvedIf [Prop] -- ^ Solved, assuming the sub-goals.
| Unsolved -- ^ We could not solve the goal.
| Unsolvable TCErrorMessage -- ^ The goal can never be solved.
deriving (Show)
instance PP Solved where
ppPrec _ res =
case res of
SolvedIf ps -> text "solved" $$ nest 2 (vcat (map pp ps))
Unsolved -> text "unsolved"
Unsolvable e -> text "unsolvable" <> colon <+> text (tcErrorMessage e)

View File

@ -38,6 +38,7 @@ import qualified Data.Set as Set
import Cryptol.TypeCheck.AST
import Cryptol.TypeCheck.PP
import Cryptol.TypeCheck.TypeMap
import Cryptol.TypeCheck.SimpleSolver
import Cryptol.Utils.Panic(panic)
import Cryptol.Utils.Misc(anyJust)
@ -58,7 +59,7 @@ s2 @@ s1 | Map.null (suMap s2) =
s1
else
s1{ suDefaulting = True }
s2 @@ s1 = S { suMap = Map.map (apSubst s2) (suMap s1) `Map.union` (suMap s2)
s2 @@ s1 = S { suMap = Map.map (apSubst s2) (suMap s1) `Map.union` suMap s2
, suDefaulting = suDefaulting s1 || suDefaulting s2
}
@ -134,6 +135,7 @@ apSubstMaybe su ty =
TCon t ts ->
do ss <- anyJust (apSubstMaybe su) ts
case t of
TF f ->
Just $!
case (f,ss) of
@ -150,7 +152,10 @@ apSubstMaybe su ty =
(TCLenFromThenTo,[t1,t2,t3]) -> tLenFromThenTo t1 t2 t3
_ -> panic "apSubstMaybe" ["Unexpected type function", show t]
PC _ -> Just $! simplify Map.empty (TCon t ss)
_ -> return (TCon t ss)
TUser f ts t -> do t1 <- apSubstMaybe su t
return (TUser f (map (apSubst su) ts) t1)
TRec fs -> TRec `fmap` anyJust fld fs

View File

@ -1,7 +1,8 @@
{-# Language Safe, DeriveGeneric, DeriveAnyClass, RecordWildCards #-}
{-# Language FlexibleInstances, FlexibleContexts #-}
{-# Language PatternGuards #-}
module Cryptol.TypeCheck.Type where
module Cryptol.TypeCheck.Type
(module Cryptol.TypeCheck.Type, TFun(..)) where
import GHC.Generics (Generic)
@ -47,8 +48,6 @@ data TParam = TParam { tpUnique :: !Int -- ^ Parameter identifier
deriving (Show, Generic, NFData)
-- | The internal representation of types.
-- These are assumed to be kind correct.
data Type = TCon TCon [Type]
@ -101,7 +100,8 @@ data PC = PEqual -- ^ @_ == _@
| PArith -- ^ @Arith _@
| PCmp -- ^ @Cmp _@
| PTrue -- ^ This is useful when simplifying things in place
| PAnd -- ^ This is useful when simplifying things in place
| PTrue -- ^ Ditto
deriving (Show, Eq, Ord, Generic, NFData)
-- | 1-1 constants.
@ -189,6 +189,7 @@ instance HasKind PC where
PHas _ -> KType :-> KType :-> KProp
PArith -> KType :-> KProp
PCmp -> KType :-> KProp
PAnd -> KProp :-> KProp :-> KProp
PTrue -> KProp
instance HasKind TFun where
@ -380,8 +381,10 @@ pIsCmp ty = case tNoUser ty of
TCon (PC PCmp) [t1] -> Just t1
_ -> Nothing
pIsTrue :: Prop -> Bool
pIsTrue ty = case tNoUser ty of
TCon (PC PTrue) _ -> True
_ -> False
--------------------------------------------------------------------------------
@ -554,8 +557,33 @@ pHas l ty fi = TCon (PC (PHas l)) [ty,fi]
pTrue :: Prop
pTrue = TCon (PC PTrue) []
pAnd :: [Prop] -> Prop
pAnd [] = pTrue
pAnd [x] = x
pAnd (x : xs)
| Just _ <- tIsError x = x
| pIsTrue x = rest
| Just _ <- tIsError rest = rest
| pIsTrue rest = x
| otherwise = TCon (PC PAnd) [x, rest]
where rest = pAnd xs
pSplitAnd :: Prop -> [Prop]
pSplitAnd p0 = go [p0]
where
go [] = []
go (q : qs) =
case tNoUser q of
TCon (PC PAnd) [l,r] -> go (l : r : qs)
TCon (PC PTrue) _ -> go qs
_ -> q : go qs
pFin :: Type -> Prop
pFin ty = TCon (PC PFin) [ty]
pFin ty =
case tNoUser ty of
TCon (TC (TCNum _)) _ -> pTrue
TCon (TC TCInf) _ -> pError (TCErrorMessage "`inf` is not finite.")
_ -> TCon (PC PFin) [ty]
-- | Make a malformed property.
pError :: TCErrorMessage -> Prop
@ -718,6 +746,7 @@ instance PP PC where
PArith -> text "Arith"
PCmp -> text "Cmp"
PTrue -> text "True"
PAnd -> text "(&&)"
instance PP TC where
ppPrec _ x =