From df4af1af3b871ee7a960aea0d9f9ceec68e5ded3 Mon Sep 17 00:00:00 2001 From: Brian Huffman Date: Fri, 15 May 2020 07:30:48 -0700 Subject: [PATCH] Make `singleSubst` perform checks and return `Either` type. The old `singleSubst` has been renamed to `uncheckedSingleSubst`. Fixes #723. --- src/Cryptol/TypeCheck/Default.hs | 4 ++-- src/Cryptol/TypeCheck/Solver/Improve.hs | 14 +++++++----- src/Cryptol/TypeCheck/Subst.hs | 29 ++++++++++++++++++++----- src/Cryptol/TypeCheck/Unify.hs | 21 ++++++++++-------- 4 files changed, 46 insertions(+), 22 deletions(-) diff --git a/src/Cryptol/TypeCheck/Default.hs b/src/Cryptol/TypeCheck/Default.hs index e1305646..2331246a 100644 --- a/src/Cryptol/TypeCheck/Default.hs +++ b/src/Cryptol/TypeCheck/Default.hs @@ -9,7 +9,7 @@ import Control.Monad(guard) import Cryptol.TypeCheck.Type import Cryptol.TypeCheck.SimpType(tMax,tWidth) import Cryptol.TypeCheck.Error(Warning(..)) -import Cryptol.TypeCheck.Subst(Subst,apSubst,listSubst,substBinds,singleSubst) +import Cryptol.TypeCheck.Subst(Subst,apSubst,listSubst,substBinds,uncheckedSingleSubst) import Cryptol.TypeCheck.InferTypes(Goal,goal,Goals(..),goalsFromList) import Cryptol.TypeCheck.Solver.SMT(Solver,tryGetModel,shrinkModel) import Cryptol.Utils.Panic(panic) @@ -152,7 +152,7 @@ improveByDefaultingWithPure as ps = let ty = case ts of [] -> tNum (0::Int) _ -> foldr1 tMax ts - su1 = singleSubst x ty + su1 = uncheckedSingleSubst x ty in ( (x,ty) : [ (y,apSubst su1 t) | (y,t) <- yes ] , no -- We know that `x` does not appear here , otherFree -- We know that `x` did not appear here either diff --git a/src/Cryptol/TypeCheck/Solver/Improve.hs b/src/Cryptol/TypeCheck/Solver/Improve.hs index 5976e860..de0bd111 100644 --- a/src/Cryptol/TypeCheck/Solver/Improve.hs +++ b/src/Cryptol/TypeCheck/Solver/Improve.hs @@ -51,7 +51,7 @@ improveLit impSkol prop = (_,b) <- aSeq t a <- aTVar b unless impSkol $ guard (isFreeTV a) - let su = singleSubst a tBit + let su = uncheckedSingleSubst a tBit return (su, []) @@ -66,13 +66,15 @@ improveEq impSkol fins prop = where rewrite this other = do x <- aTVar this - guard (considerVar x && x `Set.notMember` fvs other) - return (singleSubst x other, []) + guard (considerVar x) + case singleSubst x other of + Left _ -> mzero + Right su -> return (su, []) <|> do (v,s) <- isSum this - guard (v `Set.notMember` fvs other) - return (singleSubst v (Mk.tSub other s), [ other >== s ]) - + case singleSubst v (Mk.tSub other s) of + Left _ -> mzero + Right su -> return (su, [ other >== s ]) isSum t = do (v,s) <- matches t (anAdd, aTVar, __) valid v s diff --git a/src/Cryptol/TypeCheck/Subst.hs b/src/Cryptol/TypeCheck/Subst.hs index 9dbcb458..158fe735 100644 --- a/src/Cryptol/TypeCheck/Subst.hs +++ b/src/Cryptol/TypeCheck/Subst.hs @@ -14,8 +14,10 @@ module Cryptol.TypeCheck.Subst ( Subst , emptySubst + , SubstError(..) , singleSubst , singleTParamSubst + , uncheckedSingleSubst , (@@) , defaultingSubst , listSubst @@ -75,20 +77,38 @@ emptySubst = , suDefaulting = False } -singleSubst :: TVar -> Type -> Subst -singleSubst v@(TVFree i _ _tps _) t = +-- | Reasons to reject a single-variable substitution. +data SubstError + = SubstRecursive + -- ^ 'TVar' maps to a type containing the same variable. + | SubstEscaped [TParam] + -- ^ 'TVar' maps to a type containing one or more out-of-scope bound variables. + +singleSubst :: TVar -> Type -> Either SubstError Subst +singleSubst x t + | x `Set.member` fvs t = Left SubstRecursive + | not (Set.null escaped) = Left (SubstEscaped (Set.toList escaped)) + | otherwise = Right (uncheckedSingleSubst x t) + where + escaped = + case x of + TVBound _ -> Set.empty + TVFree _ _ scope _ -> freeParams t `Set.difference` scope + +uncheckedSingleSubst :: TVar -> Type -> Subst +uncheckedSingleSubst v@(TVFree i _ _tps _) t = S { suFreeMap = IntMap.singleton i (v, t) , suBoundMap = IntMap.empty , suDefaulting = False } -singleSubst v@(TVBound tp) t = +uncheckedSingleSubst v@(TVBound tp) t = S { suFreeMap = IntMap.empty , suBoundMap = IntMap.singleton (tpUnique tp) (v, t) , suDefaulting = False } singleTParamSubst :: TParam -> Type -> Subst -singleTParamSubst tp t = singleSubst (TVBound tp) t +singleTParamSubst tp t = uncheckedSingleSubst (TVBound tp) t (@@) :: Subst -> Subst -> Subst s2 @@ s1 @@ -338,4 +358,3 @@ instance TVars DeclDef where instance TVars Module where apSubst su m = m { mDecls = apSubst su (mDecls m) } - diff --git a/src/Cryptol/TypeCheck/Unify.hs b/src/Cryptol/TypeCheck/Unify.hs index 53a57127..2513a264 100644 --- a/src/Cryptol/TypeCheck/Unify.hs +++ b/src/Cryptol/TypeCheck/Unify.hs @@ -111,14 +111,17 @@ bindVar v@(TVBound {}) t where k = kindOf v bindVar x@(TVFree _ _ xscope _) (TVar y@(TVFree _ _ yscope _)) - | xscope `Set.isProperSubsetOf` yscope = return (singleSubst y (TVar x), []) + | xscope `Set.isProperSubsetOf` yscope = + return (uncheckedSingleSubst y (TVar x), []) -bindVar x@(TVFree _ k inScope _d) t +bindVar x@(TVFree _ k _scope _d) t | not (k == kindOf t) = uniError $ UniKindMismatch k (kindOf t) - | recTy && k == KType = uniError $ UniRecursive x t - | not (Set.null escaped) = uniError $ UniNonPolyDepends x $ Set.toList escaped - | recTy = return (emptySubst, [TVar x =#= t]) - | otherwise = return (singleSubst x t, []) - where - escaped = freeParams t `Set.difference` inScope - recTy = x `Set.member` fvs t + | otherwise = + case singleSubst x t of + Left SubstRecursive + | k == KType -> uniError $ UniRecursive x t + | otherwise -> return (emptySubst, [TVar x =#= t]) + Left (SubstEscaped tps) -> + uniError $ UniNonPolyDepends x tps + Right su -> + return (su, [])