GaloisInc/cryptol
1
1
Fork 0
mirror of https://github.com/GaloisInc/cryptol.git synced 2024-11-28 09:23:04 +03:00
Code Issues Projects Releases Wiki Activity

Merge branch 'master' into feature/benchmarks

Browse Source
This commit is contained in:
Adam C. Foltzer 2015-08-14 16:11:49 -07:00
commit dce6f994e8
39 changed files with 1052 additions and 562 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

1
cryptol.cabal
View File

@ -122,6 +122,7 @@ library
Cryptol.TypeCheck.Solver.Class,
Cryptol.TypeCheck.Solver.Selector,
Cryptol.TypeCheck.Solver.Utils,
Cryptol.TypeCheck.Solver.Simplify,
Cryptol.TypeCheck.Solver.CrySAT,
Cryptol.TypeCheck.Solver.Numeric.AST,

52
src/Cryptol/Eval.hs
View File

@ -28,12 +28,12 @@ import Cryptol.Utils.Panic (panic)
import Cryptol.Utils.PP
import Cryptol.Prims.Eval
import Control.Applicative (pure, ZipList(..))
import qualified Data.Map as Map
import Data.Traversable (traverse)
#if __GLASGOW_HASKELL__ < 710
import Control.Applicative (Applicative(..))
import Data.Monoid (Monoid(..),mconcat)
import Data.Traversable (sequenceA)
#endif
-- Expression Evaluation -------------------------------------------------------
@ -168,31 +168,53 @@ evalSel env e sel = case sel of
-- List Comprehension Environments ---------------------------------------------
-- | A variation of the ZipList type from Control.Applicative, with a
-- separate constructor for pure values. This datatype is used to
-- represent the list of values that each variable takes on within a
-- list comprehension. The @Zip@ constructor is for bindings that take
-- different values at different positions in the list, while the
-- @Pure@ constructor is for bindings originating outside the list
-- comprehension, which have the same value for all list positions.
data ZList a = Pure a | Zip [a]
getZList :: ZList a -> [a]
getZList (Pure x) = repeat x
getZList (Zip xs) = xs
instance Functor ZList where
fmap f (Pure x) = Pure (f x)
fmap f (Zip xs) = Zip (map f xs)
instance Applicative ZList where
pure x = Pure x
Pure f <*> Pure x = Pure (f x)
Pure f <*> Zip xs = Zip (map f xs)
Zip fs <*> Pure x = Zip (map ($ x) fs)
Zip fs <*> Zip xs = Zip (zipWith ($) fs xs)
-- | Evaluation environments for list comprehensions: Each variable
-- name is bound to a list of values, one for each element in the list
-- comprehension. The Left constructor is for "pure" bindings
-- originating outside the list comprehension, which have the same
-- value for all list positions.
-- comprehension.
data ListEnv = ListEnv
{ leVars :: Map.Map QName (Either Value [Value])
{ leVars :: Map.Map QName (ZList Value)
, leTypes :: Map.Map TVar TValue
}
instance Monoid ListEnv where
mempty = ListEnv
{ leVars = Map.empty
, leTypes = Map.empty
{ leVars = Map.empty
, leTypes = Map.empty
}
mappend l r = ListEnv
{ leVars = Map.union (leVars l) (leVars r)
, leTypes = Map.union (leTypes l) (leTypes r)
{ leVars = Map.union (leVars l) (leVars r)
, leTypes = Map.union (leTypes l) (leTypes r)
}
toListEnv :: EvalEnv -> ListEnv
toListEnv e =
ListEnv
{ leVars = fmap Left (envVars e)
{ leVars = fmap Pure (envVars e)
, leTypes = envTypes e
}
@ -203,10 +225,10 @@ toListEnv e =
zipListEnv :: ListEnv -> [EvalEnv]
zipListEnv (ListEnv vm tm) =
[ EvalEnv { envVars = v, envTypes = tm }
| v <- getZipList (traverse (either pure ZipList) vm) ]
| v <- getZList (sequenceA vm) ]
bindVarList :: QName -> [Value] -> ListEnv -> ListEnv
bindVarList n vs lenv = lenv { leVars = Map.insert n (Right vs) (leVars lenv) }
bindVarList n vs lenv = lenv { leVars = Map.insert n (Zip vs) (leVars lenv) }
-- List Comprehensions ---------------------------------------------------------
@ -242,8 +264,8 @@ evalMatch lenv m = case m of
From n _ty expr -> bindVarList n (concat vss) lenv'
where
vss = [ fromSeq (evalExpr env expr) | env <- zipListEnv lenv ]
stutter (Left x) = Left x
stutter (Right xs) = Right [ x | (x, vs) <- zip xs vss, _ <- vs ]
stutter (Pure x) = Pure x
stutter (Zip xs) = Zip [ x | (x, vs) <- zip xs vss, _ <- vs ]
lenv' = lenv { leVars = fmap stutter (leVars lenv) }
-- XXX we don't currently evaluate these as though they could be recursive, as

4
src/Cryptol/ModuleSystem/Base.hs
View File

@ -204,7 +204,7 @@ importIfaces :: [P.Import] -> ModuleM IfaceDecls
importIfaces is = foldMap ifPublic `fmap` mapM importIface is
moduleFile :: ModName -> String -> FilePath
moduleFile (ModName ns) = addExtension (joinPath ns)
moduleFile n = addExtension (joinPath (P.unModName n))
-- | Discover a module.
findModule :: ModName -> ModuleM FilePath
@ -250,7 +250,7 @@ findFile path = do
possibleFiles paths = map (</> path) paths
preludeName :: P.ModName
preludeName = P.ModName ["Cryptol"]
preludeName = P.mkModName ["Cryptol"]
-- | Add the prelude to the import list if it's not already mentioned.
addPrelude :: P.Module -> P.Module

2
src/Cryptol/ModuleSystem/Monad.hs
View File

@ -316,7 +316,7 @@ loadingModule = loading . FromModule
-- | Push an "interactive" context onto the loading stack. A bit of a hack, as
-- it uses a faked module name
interactive :: ModuleM a -> ModuleM a
interactive = loadingModule (P.ModName ["<interactive>"])
interactive = loadingModule (P.mkModName ["<interactive>"])
loading :: ImportSource -> ModuleM a -> ModuleM a
loading src m = ModuleT $ do

31
src/Cryptol/ModuleSystem/Name.hs
View File

@ -4,15 +4,26 @@ module Cryptol.ModuleSystem.Name where
import GHC.Generics (Generic)
import Control.DeepSeq
import qualified Data.Text as Text
type Ident = Text.Text
pack :: String -> Ident
pack = Text.pack
unpack :: Ident -> String
unpack = Text.unpack
-- | Module names are just namespaces.
--
-- INVARIANT: the list of strings should never be empty in a valid module name.
newtype ModName = ModName [String]
newtype ModName = ModName [Ident]
deriving (Eq,Ord,Show,Generic)
instance NFData ModName
data Name = Name String
data Name = Name Ident
| NewName Pass Int
deriving (Eq,Ord,Show,Generic)
@ -23,10 +34,24 @@ data QName = QName (Maybe ModName) Name
instance NFData QName
unModName :: ModName -> [String]
unModName (ModName ns) = map unpack ns
mkModName :: [String] -> ModName
mkModName ns = ModName (map pack ns)
mkName :: String -> Name
mkName n = Name (pack n)
-- XXX It would be nice to also mark this as a name that doesn't need to be
-- resolved, if it's going to be created before renaming.
mkPrim :: String -> QName
mkPrim n = mkQual (ModName ["Cryptol"]) (Name n)
mkPrim n = mkQual (ModName [pack "Cryptol"]) (Name (pack n))
asPrim :: QName -> Maybe String
asPrim (QName (Just (ModName [m])) (Name n))
| m == pack "Cryptol" = Just (unpack n)
asPrim _ = Nothing
mkQual :: ModName -> Name -> QName
mkQual = QName . Just

26
src/Cryptol/ModuleSystem/Renamer.hs
View File

@ -381,10 +381,10 @@ translateProp ty = go =<< rnType True ty
TLocated t' r -> (`CLocated` r) <$> go t'
TUser (QName Nothing (Name p)) [l,r]
| p == "==" -> pure (CEqual l r)
| p == ">=" -> pure (CGeq l r)
| p == "<=" -> pure (CGeq r l)
TUser (QName Nothing p) [l,r]
| p == mkName "==" -> pure (CEqual l r)
| p == mkName ">=" -> pure (CGeq l r)
| p == mkName "<=" -> pure (CGeq r l)
_ ->
do record (InvalidConstraint ty)
@ -405,15 +405,15 @@ rnType isProp = go
TChar _ -> return t
TInf -> return t
TUser (QName Nothing (Name n)) ps
| n == "inf", null ps -> return TInf
| n == "Bit", null ps -> return TBit
TUser (QName Nothing n) ps
| n == mkName "inf", null ps -> return TInf
| n == mkName "Bit", null ps -> return TBit
| n == "min" -> TApp TCMin <$> traverse go ps
| n == "max" -> TApp TCMax <$> traverse go ps
| n == "lengthFromThen" -> TApp TCLenFromThen <$> traverse go ps
| n == "lengthFromThenTo" -> TApp TCLenFromThenTo <$> traverse go ps
| n == "width" -> TApp TCWidth <$> traverse go ps
| n == mkName "min" -> TApp TCMin <$> traverse go ps
| n == mkName "max" -> TApp TCMax <$> traverse go ps
| n == mkName "lengthFromThen" -> TApp TCLenFromThen <$> traverse go ps
| n == mkName "lengthFromThenTo" -> TApp TCLenFromThenTo <$> traverse go ps
| n == mkName "width" -> TApp TCWidth <$> traverse go ps
TUser qn ps -> TUser <$> renameType qn <*> traverse go ps
TApp f xs -> TApp f <$> traverse go xs
@ -470,7 +470,7 @@ mkTInfix t (op,_) z =
renameTypeOp :: Bool -> Located QName -> RenameM (TOp,Fixity)
renameTypeOp isProp op =
do let sym = unqual (thing op)
props = [ Name "==", Name ">=", Name "<=" ]
props = [ mkName "==", mkName ">=", mkName "<=" ]
lkp = do n <- Map.lookup (thing op) tfunNames
(fAssoc,fLevel) <- Map.lookup n tBinOpPrec
return (n,Fixity { .. })

34
src/Cryptol/Parser.y
View File

@ -150,7 +150,7 @@ vmodule :: { Module }
{ let { (is,ts) = $2
-- XXX make a location from is and ts
; modName = Located { srcRange = emptyRange
, thing = ModName ["Main"]
, thing = mkModName ["Main"]
}
} in Module modName is ts }
@ -377,25 +377,25 @@ iexpr :: { Expr }
expr10 :: { Expr }
: aexprs { mkEApp $1 }
| '-' expr10 %prec NEG { at ($1,$2) $ EApp (at $1 (EVar (mkUnqual (Name "negate")))) $2 }
| '~' expr10 { at ($1,$2) $ EApp (at $1 (EVar (mkUnqual (Name "complement")))) $2 }
| '-' expr10 %prec NEG { at ($1,$2) $ EApp (at $1 (EVar (mkUnqual (mkName "negate")))) $2 }
| '~' expr10 { at ($1,$2) $ EApp (at $1 (EVar (mkUnqual (mkName "complement")))) $2 }
qop :: { LQName }
: op { fmap mkUnqual $1 }
| QOP { let Token (Op (Other ns i)) _ = thing $1
in mkQual (ModName ns) (Name i) A.<$ $1 }
in mkQual (mkModName ns) (mkName i) A.<$ $1 }
op :: { LName }
: OP { let Token (Op (Other [] str)) _ = thing $1
in Name str A.<$ $1 }
in mkName str A.<$ $1 }
-- special cases for operators that are re-used elsewhere
| '*' { Located $1 $ Name "*" }
| '+' { Located $1 $ Name "+" }
| '-' { Located $1 $ Name "-" }
| '~' { Located $1 $ Name "~" }
| '^^' { Located $1 $ Name "^^" }
| '#' { Located $1 $ Name "#" }
| '*' { Located $1 $ mkName "*" }
| '+' { Located $1 $ mkName "+" }
| '-' { Located $1 $ mkName "-" }
| '~' { Located $1 $ mkName "~" }
| '^^' { Located $1 $ mkName "^^" }
| '#' { Located $1 $ mkName "#" }
ops :: { [LName] }
: op { [$1] }
@ -609,19 +609,19 @@ field_types :: { [Named Type] }
name :: { LName }
: IDENT { $1 { thing = getName $1 } }
| 'x' { Located { srcRange = $1, thing = Name "x" }}
| 'private' { Located { srcRange = $1, thing = Name "private" } }
| 'as' { Located { srcRange = $1, thing = Name "as" } }
| 'hiding' { Located { srcRange = $1, thing = Name "hiding" } }
| 'x' { Located { srcRange = $1, thing = mkName "x" }}
| 'private' { Located { srcRange = $1, thing = mkName "private" } }
| 'as' { Located { srcRange = $1, thing = mkName "as" } }
| 'hiding' { Located { srcRange = $1, thing = mkName "hiding" } }
modName :: { Located ModName }
: qname { mkModName $1 }
: qname { mkLModName $1 }
qname :: { Located QName }
: name { fmap mkUnqual $1 }
| QIDENT { let Token (Ident ns i) _ = thing $1
in mkQual (ModName ns) (Name i) A.<$ $1 }
in mkQual (mkModName ns) (mkName i) A.<$ $1 }
help_name :: { Located QName }
: qname { $1 }

7
src/Cryptol/Parser/AST.hs
View File

@ -6,6 +6,7 @@
-- Stability : provisional
-- Portability : portable
{-# LANGUAGE CPP #-}
{-# LANGUAGE Safe #-}
{-# LANGUAGE PatternGuards #-}
{-# LANGUAGE RecordWildCards #-}
@ -15,7 +16,7 @@
module Cryptol.Parser.AST
( -- * Names
ModName(..), {-splitNamespace, parseModName, nsChar,-} modRange
, QName(..), mkPrim, mkQual, mkUnqual, unqual
, QName(..), mkModName, unModName, mkName, mkPrim, asPrim, mkQual, mkUnqual, unqual
, Name(..)
, Named(..)
, Pass(..)
@ -689,8 +690,8 @@ wrap contextPrec myPrec doc = if myPrec < contextPrec then parens doc else doc
isPrefixOp :: Expr -> Maybe Doc
isPrefixOp (ELocated e _) = isPrefixOp e
isPrefixOp e@(EVar (QName Nothing (Name n))) | n == "-" = Just (pp e)
| n == "~" = Just (pp e)
isPrefixOp e@(EVar (QName Nothing n)) | n == mkName "-" = Just (pp e)
| n == mkName "~" = Just (pp e)
isPrefixOp _ = Nothing
isEApp :: Expr -> Maybe (Expr, Expr)

3
src/Cryptol/Parser/Lexer.x
View File

@ -55,7 +55,8 @@ $unitick = \x7
<comment> {
\*+\/ { endComent }
. { addToComment }
[^\*]+ { addToComment }
\* { addToComment }
\n { addToComment }
}

2
src/Cryptol/Parser/NoPat.hs
View File

@ -125,7 +125,7 @@ noPat pat =
r <- getRange
let qx = mkUnqual x
qtmp = mkUnqual tmp
prim = EVar (mkUnqual (Name "splitAt"))
prim = EVar (mkUnqual (mkName "splitAt"))
bTmp = simpleBind (Located r qtmp) (EApp prim (EVar qx))
b1 = sel a1 qtmp (TupleSel 0 (Just 2))
b2 = sel a2 qtmp (TupleSel 1 (Just 2))

22
src/Cryptol/Parser/ParserUtils.hs
View File

@ -114,8 +114,8 @@ errorMessage r x = P $ \_ _ _ -> Left (HappyErrorMsg r x)
customError :: String -> Located Token -> ParseM a
customError x t = P $ \_ _ _ -> Left (HappyErrorMsg (srcRange t) x)
mkModName :: LQName -> Located ModName
mkModName = fmap $ \ (QName mb (Name n)) ->
mkLModName :: LQName -> Located ModName
mkLModName = fmap $ \ (QName mb (Name n)) ->
case mb of
Just (ModName ns) -> ModName (ns ++ [n])
Nothing -> ModName [n]
@ -135,7 +135,7 @@ mkSchema xs ps t = Forall xs ps t Nothing
getName :: Located Token -> Name
getName l = case thing l of
Token (Ident [] x) _ -> Name x
Token (Ident [] x) _ -> mkName x
_ -> panic "[Parser] getName" ["not an Ident:", show l]
getNum :: Located Token -> Integer
@ -268,7 +268,7 @@ exprToNumT r expr =
-- It is used to represent anonymous type applications.
anonRecord :: Maybe Range -> [Type] -> Type
anonRecord ~(Just r) ts = TRecord (map toField ts)
where noName = Located { srcRange = r, thing = Name "" }
where noName = Located { srcRange = r, thing = mkName "" }
toField t = Named { name = noName, value = t }
exportDecl :: Maybe (Located String) -> ExportType -> Decl -> TopDecl
@ -289,18 +289,18 @@ changeExport e = map change
change td@Include{} = td
mkTypeInst :: Named Type -> TypeInst
mkTypeInst x | thing (name x) == Name "" = PosInst (value x)
| otherwise = NamedInst x
mkTypeInst x | thing (name x) == mkName "" = PosInst (value x)
| otherwise = NamedInst x
mkTParam :: Located Name -> Maybe Kind -> ParseM TParam
mkTParam Located { srcRange = rng, thing = n } k
| Name "width" <- n = errorMessage rng "`width` is not a valid type parameter name."
| n == mkName "width" = errorMessage rng "`width` is not a valid type parameter name."
| otherwise = return (TParam n k (Just rng))
mkTySyn :: Located Name -> [TParam] -> Type -> ParseM Decl
mkTySyn n ps b
| Name "width" <- thing n = errorMessage (srcRange n) "`width` is not a valid type synonym name."
| thing n == mkName "width" = errorMessage (srcRange n) "`width` is not a valid type synonym name."
| otherwise = return $ DType $ TySyn (fmap mkUnqual n) ps b
polyTerm :: Range -> Integer -> Integer -> ParseM (Bool, Integer)
@ -439,13 +439,13 @@ mkProp ty =
-- these can be translated right away
prefixProp r f xs =
case f of
QName Nothing (Name "Arith") | [x] <- xs ->
QName Nothing n | n == mkName "Arith", [x] <- xs ->
return [CLocated (CArith x) r]
QName Nothing (Name "fin") | [x] <- xs ->
QName Nothing n | n == mkName "fin", [x] <- xs ->
return [CLocated (CFin x) r]
QName Nothing (Name "Cmp") | [x] <- xs ->
QName Nothing n | n == mkName "Cmp", [x] <- xs ->
return [CLocated (CCmp x) r]
_ -> errorMessage r "Invalid constraint"

2
src/Cryptol/Parser/Utils.hs
View File

@ -21,7 +21,7 @@ translateExprToNumT :: Expr -> Maybe Type
translateExprToNumT expr =
case expr of
ELocated e r -> (`TLocated` r) `fmap` translateExprToNumT e
EVar (QName Nothing (Name "width")) -> mkFun TCWidth
EVar (QName Nothing n) | n == mkName "width" -> mkFun TCWidth
EVar x -> return (TUser x [])
ELit x -> cvtLit x
EApp e1 e2 -> do t1 <- translateExprToNumT e1

1
src/Cryptol/Prelude.hs
View File

@ -10,6 +10,7 @@
{-# LANGUAGE CPP #-}
{-# LANGUAGE QuasiQuotes #-}
{-# LANGUAGE OverloadedStrings #-}
module Cryptol.Prelude (writePreludeContents) where

9
src/Cryptol/Prims/Eval.hs
View File

@ -26,6 +26,7 @@ import Cryptol.Eval.Type(evalTF)
import Cryptol.Eval.Value
import Cryptol.Testing.Random (randomValue)
import Cryptol.Utils.Panic (panic)
import Cryptol.ModuleSystem.Name (Ident, pack)
import Data.List (sortBy,transpose,genericTake,genericReplicate,genericSplitAt,genericIndex)
import Data.Ord (comparing)
@ -83,14 +84,14 @@ instance Bits Bool where
-- Primitives ------------------------------------------------------------------
evalPrim :: Decl -> Value
evalPrim Decl { dName = QName (Just (ModName ["Cryptol"])) (Name prim), .. }
| Just val <- Map.lookup prim primTable = val
evalPrim Decl { dName = QName (Just m) (Name prim), .. }
| m == mkModName ["Cryptol"], Just val <- Map.lookup prim primTable = val
evalPrim Decl { .. } =
panic "Eval" [ "Unimplemented primitive", show dName ]
primTable :: Map.Map String Value
primTable = Map.fromList
primTable :: Map.Map Ident Value
primTable = Map.fromList $ map (\(n, v) -> (pack n, v))
[ ("+" , binary (arithBinary (liftBinArith (+))))
, ("-" , binary (arithBinary (liftBinArith (-))))
, ("*" , binary (arithBinary (liftBinArith (*))))

4
src/Cryptol/Prims/Syntax.hs
View File

@ -11,7 +11,7 @@ module Cryptol.Prims.Syntax
( TFun(..), tBinOpPrec, tfunNames
) where
import Cryptol.ModuleSystem.Name (QName,Name(Name),mkUnqual)
import Cryptol.ModuleSystem.Name (QName,Name(Name),mkUnqual,pack)
import Cryptol.Utils.PP
import qualified Data.Map as Map
@ -69,7 +69,7 @@ tfunNames = Map.fromList
, tprim "lengthFromThenTo" TCLenFromThenTo
]
where
tprim n p = (mkUnqual (Name n), p)
tprim n p = (mkUnqual (Name (pack n)), p)
instance PP TFun where
ppPrec _ tcon =

6
src/Cryptol/REPL/Command.hs
View File

@ -485,7 +485,7 @@ mkSolverResult :: String
-> (T.Type, T.Expr)
mkSolverResult thing result earg = (rty, re)
where
rName = T.Name "result"
rName = T.mkName "result"
rty = T.TRec $ [(rName, T.tBit )] ++ map fst argF
re = T.ERec $ [(rName, resultE)] ++ map snd argF
resultE = if result then T.eTrue else T.eFalse
@ -493,7 +493,7 @@ mkSolverResult thing result earg = (rty, re)
where
go [] fs _ = fs
go ((t, e):tes') fs n = go tes' (((argName, t), (argName, e)):fs) (n+1)
where argName = T.Name ("arg" ++ show n)
where argName = T.mkName ("arg" ++ show n)
argF = case earg of
Left ts -> mkArgs $ (map addError) ts
where addError t = (t, T.eError t ("no " ++ thing ++ " available"))
@ -839,7 +839,7 @@ replEvalExpr expr =
-- it to the current dynamic environment
bindItVariable :: T.Type -> T.Expr -> REPL ()
bindItVariable ty expr = do
let it = T.QName Nothing (P.Name "it")
let it = T.QName Nothing (P.mkName "it")
freshIt <- uniqify it
let dg = T.NonRecursive decl
schema = T.Forall { T.sVars = []

5
src/Cryptol/REPL/Monad.hs
View File

@ -10,6 +10,7 @@
{-# LANGUAGE DeriveDataTypeable #-}
{-# LANGUAGE RecordWildCards #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE ViewPatterns #-}
module Cryptol.REPL.Monad (
-- * REPL Monad
@ -351,7 +352,7 @@ getFocusedEnv = do
let (decls,names) = M.focusedEnv me
edecls = M.ifDecls dyDecls
-- is this QName something the user might actually type?
isShadowed (qn@(P.QName (Just (P.ModName ['#':_])) name), _) =
isShadowed (qn@(P.QName (Just (P.unModName -> ['#':_])) name), _) =
case Map.lookup localName neExprs of
Nothing -> False
Just uniqueNames -> isNamed uniqueNames
@ -422,7 +423,7 @@ uniqify :: P.QName -> REPL P.QName
uniqify (P.QName Nothing name) = do
i <- eNameSupply `fmap` getRW
modifyRW_ (\rw -> rw { eNameSupply = i+1 })
let modname' = P.ModName [ '#' : ("Uniq_" ++ show i) ]
let modname' = P.mkModName [ '#' : ("Uniq_" ++ show i) ]
return (P.QName (Just modname') name)
uniqify qn =
panic "[REPL] uniqify" ["tried to uniqify a qualified name: " ++ pretty qn]

11
src/Cryptol/Symbolic/Prims.hs
View File

@ -18,9 +18,10 @@ import Data.Ord (comparing)
import Cryptol.Eval.Value (BitWord(..))
import Cryptol.Prims.Eval (binary, unary, tlamN)
import Cryptol.Symbolic.Value
import Cryptol.TypeCheck.AST (ModName(..),QName(..),Name(..),Decl(..))
import Cryptol.TypeCheck.AST (QName(..),Name(..),Decl(..),mkModName,mkName)
import Cryptol.TypeCheck.Solver.InfNat(Nat'(..), nMul)
import Cryptol.Utils.Panic
import Cryptol.ModuleSystem.Name (Ident, pack)
import qualified Data.SBV.Dynamic as SBV
import qualified Data.Map as Map
@ -35,15 +36,15 @@ traverseSnd f (x, y) = (,) x <$> f y
-- Primitives ------------------------------------------------------------------
evalPrim :: Decl -> Value
evalPrim Decl { dName = QName (Just (ModName ["Cryptol"])) (Name prim), .. }
| Just val <- Map.lookup prim primTable = val
evalPrim Decl { dName = QName (Just m) (Name prim), .. }
| m == mkModName ["Cryptol"], Just val <- Map.lookup prim primTable = val
evalPrim Decl { .. } =
panic "Eval" [ "Unimplemented primitive", show dName ]
-- See also Cryptol.Prims.Eval.primTable
primTable :: Map.Map String Value
primTable = Map.fromList
primTable :: Map.Map Ident Value
primTable = Map.fromList $ map (\(n, v) -> (pack n, v))
[ ("True" , VBit SBV.svTrue)
, ("False" , VBit SBV.svFalse)
, ("demote" , ecDemoteV) -- Converts a numeric type into its corresponding value.

9
src/Cryptol/Transform/Specialize.hs
View File

@ -15,6 +15,7 @@ import Cryptol.TypeCheck.Subst
import qualified Cryptol.ModuleSystem as M
import qualified Cryptol.ModuleSystem.Env as M
import qualified Cryptol.ModuleSystem.Monad as M
import Cryptol.ModuleSystem.Name (unpack)
import Data.List (intercalate)
import Data.Map (Map)
@ -241,12 +242,12 @@ freshName (QName m name) tys = do
let go = if name' `elem` bNames
then loop (1 :: Integer)
else name'
return $ QName m (Name go)
return $ QName m (mkName go)
matchingBoundNames :: (Maybe ModName) -> SpecM [String]
matchingBoundNames m = do
qns <- allPublicQNames <$> liftSpecT M.getModuleEnv
return [ n | QName m' (Name n) <- qns , m == m' ]
return [ unpack n | QName m' (Name n) <- qns , m == m' ]
reifyName :: Name -> [Type] -> String
reifyName name tys = intercalate "_" (showName name : concatMap showT tys)
@ -287,9 +288,9 @@ reifyName name tys = intercalate "_" (showName name : concatMap showT tys)
TupleSel _ sig -> "tup" : maybe [] ((:[]) . show) sig
RecordSel x sig -> "rec" : showName x : map showName (maybe [] id sig)
ListSel _ sig -> "list" : maybe [] ((:[]) . show) sig
showName nm =
showName nm =
case nm of
Name s -> s
Name s -> unpack s
NewName _ n -> "x" ++ show n
showTF tf =
case tf of

2
src/Cryptol/TypeCheck.hs
View File

@ -68,7 +68,7 @@ tcExpr e0 inp = runInferM inp
_ -> do res <- inferBinds True False
[ P.Bind
{ P.bName = P.Located (inpRange inp)
$ mkUnqual (P.Name "(expression)")
$ mkUnqual (P.mkName "(expression)")
, P.bParams = []
, P.bDef = P.Located (inpRange inp) (P.DExpr expr)
, P.bPragmas = []

7
src/Cryptol/TypeCheck/AST.hs
View File

@ -14,7 +14,7 @@
module Cryptol.TypeCheck.AST
( module Cryptol.TypeCheck.AST
, TFun(..)
, Name(..), QName(..), mkUnqual, unqual
, Name(..), QName(..), mkModName, mkName, mkUnqual, unqual
, ModName(..)
, Selector(..)
, Import(..)
@ -25,12 +25,13 @@ module Cryptol.TypeCheck.AST
, Fixity(..)
) where
import Cryptol.ModuleSystem.Name (mkQual)
import Cryptol.ModuleSystem.Name (mkQual, mkName)
import Cryptol.Prims.Syntax
import Cryptol.Parser.AST ( Name(..), Selector(..),Pragma(..), ppSelector
, Import(..), ImportSpec(..), ExportType(..)
, ExportSpec(..), ModName(..), isExportedBind
, isExportedType, QName(..), mkUnqual, unqual
, mkModName
, Fixity(..) )
import Cryptol.Utils.Panic(panic)
import Cryptol.TypeCheck.PP
@ -435,7 +436,7 @@ tBit :: Type
tBit = TCon (TC TCBit) []
ePrim :: String -> Expr
ePrim n = EVar (mkQual (ModName ["Cryptol"]) (Name n))
ePrim n = EVar (mkQual (mkModName ["Cryptol"]) (mkName n))
eTrue :: Expr
eTrue = ePrim "True"

8
src/Cryptol/TypeCheck/Infer.hs
View File

@ -68,7 +68,7 @@ desugarLiteral :: Bool -> P.Literal -> InferM P.Expr
desugarLiteral fixDec lit =
do l <- curRange
let named (x,y) = P.NamedInst
P.Named { name = Located l (Name x), value = P.TNum y }
P.Named { name = Located l (mkName x), value = P.TNum y }
demote fs = P.EAppT (P.EVar (P.mkPrim "demote")) (map named fs)
return $ case lit of
@ -223,7 +223,7 @@ checkE expr tGoal =
lstT = totLen .-. tNum (1::Int)
appTys (P.EVar (P.mkPrim "fromTo"))
[ Located rng (Just (mkUnqual (Name x)), y)
[ Located rng (Just (mkUnqual (mkName x)), y)
| (x,y) <- [ ("first",fstT), ("last", lstT), ("bits", bit) ]
] tGoal
@ -244,7 +244,7 @@ checkE expr tGoal =
(P.EVar (P.mkPrim "fromThenTo"), [ ("next",t2), ("last",t3) ])
let e' = P.EAppT c
[ P.NamedInst P.Named { name = Located l (Name x), value = y }
[ P.NamedInst P.Named { name = Located l (mkName x), value = y }
| (x,y) <- ("first",t1) : fs
]
@ -305,7 +305,7 @@ checkE expr tGoal =
do l <- curRange
checkE (P.EAppT (P.EVar (P.mkPrim "demote"))
[P.NamedInst
P.Named { name = Located l (Name "val"), value = t }]) tGoal
P.Named { name = Located l (mkName "val"), value = t }]) tGoal
P.EFun ps e -> checkFun (text "anonymous function") ps e tGoal

3
src/Cryptol/TypeCheck/InferTypes.hs
View File

@ -11,6 +11,7 @@
{-# LANGUAGE Safe #-}
{-# LANGUAGE FlexibleInstances, FlexibleContexts #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE ViewPatterns #-}
module Cryptol.TypeCheck.InferTypes where
import Cryptol.TypeCheck.AST
@ -519,7 +520,7 @@ instance PP ConstraintSource where
ppUse :: Expr -> Doc
ppUse expr =
case expr of
EVar (QName (Just (ModName ["Cryptol"])) (Name prim))
EVar (P.asPrim -> Just prim)
| prim == "demote" -> text "literal or demoted expression"
| prim == "infFrom" -> text "infinite enumeration"
| prim == "infFromThen" -> text "infinite enumeration (with step)"

443
src/Cryptol/TypeCheck/Solve.hs
View File

@ -6,7 +6,7 @@
-- Stability : provisional
-- Portability : portable
{-# LANGUAGE PatternGuards, BangPatterns #-}
{-# LANGUAGE PatternGuards, BangPatterns, RecordWildCards #-}
{-# LANGUAGE Safe #-}
module Cryptol.TypeCheck.Solve
( simplifyAllConstraints
@ -21,11 +21,13 @@ module Cryptol.TypeCheck.Solve
import Cryptol.Parser.AST(LQName, thing)
import Cryptol.Parser.Position (emptyRange)
import Cryptol.TypeCheck.PP(pp)
import Cryptol.TypeCheck.AST
import Cryptol.TypeCheck.Monad
import Cryptol.TypeCheck.Subst
(apSubst,fvs,singleSubst,substToList, isEmptySubst,
emptySubst,Subst,listSubst, (@@), Subst)
emptySubst,Subst,listSubst, (@@), Subst,
apSubstMaybe)
import Cryptol.TypeCheck.Solver.Class
import Cryptol.TypeCheck.Solver.Selector(tryHasGoal)
import qualified Cryptol.TypeCheck.Solver.Numeric.AST as Num
@ -34,14 +36,15 @@ import qualified Cryptol.TypeCheck.Solver.Numeric.Simplify1 as Num
import qualified Cryptol.TypeCheck.Solver.Numeric.SimplifyExpr as Num
import qualified Cryptol.TypeCheck.Solver.CrySAT as Num
import Cryptol.TypeCheck.Solver.CrySAT (debugBlock, DebugLog(..))
import Cryptol.TypeCheck.Solver.Simplify
(Fins,tryRewritePropAsSubst)
import Cryptol.Utils.PP (text)
import Cryptol.Utils.Panic(panic)
import Cryptol.Utils.Misc(anyJust)
import Cryptol.Parser.Position(rCombs)
import Control.Monad (unless, guard)
import Data.Either(partitionEithers)
import Data.Maybe(catMaybes, fromMaybe)
import Data.Maybe(catMaybes, fromMaybe, mapMaybe)
import Data.Map ( Map )
import qualified Data.Map as Map
import Data.Set ( Set )
@ -80,30 +83,27 @@ wfType t =
--------------------------------------------------------------------------------
-- XXX at the moment, we try to solve class constraints before solving fin
-- constraints, as they could yield fin constraints. At some point, it would
-- probably be good to try solving all of these in one big loop.
simplifyAllConstraints :: InferM ()
simplifyAllConstraints =
do mapM_ tryHasGoal =<< getHasGoals
gs <- getGoals
cfg <- getSolverConfig
mb <- io (Num.withSolver cfg (`simpGoals` gs))
(mb,su) <- io (Num.withSolver cfg (`simpGoals'` gs))
extendSubst su
case mb of
Right (gs1,su) -> extendSubst su >> addGoals gs1
Left badGs -> mapM_ (recordError . UnsolvedGoal True) badGs
Right gs1 -> addGoals gs1
Left badGs -> mapM_ (recordError . UnsolvedGoal True) badGs
proveImplication :: LQName -> [TParam] -> [Prop] -> [Goal] -> InferM Subst
proveImplication lnam as ps gs =
do evars <- varsWithAsmps
cfg <- getSolverConfig
mbErr <- io (proveImplicationIO cfg lnam evars as ps gs)
(mbErr,su) <- io (proveImplicationIO cfg lnam evars as ps gs)
case mbErr of
Right (su,ws) ->
do mapM_ recordWarning ws
return su
Left err -> recordError err >> return emptySubst
Right ws -> mapM_ recordWarning ws
Left err -> recordError err
return su
proveImplicationIO :: SolverConfig
@ -113,25 +113,28 @@ proveImplicationIO :: SolverConfig
-> [TParam] -- ^ Type parameters
-> [Prop] -- ^ Assumed constraint
-> [Goal] -- ^ Collected constraints
-> IO (Either Error (Subst,[Warning]))
proveImplicationIO _ _ _ _ [] [] = return (Right (emptySubst,[]))
-> IO (Either Error [Warning], Subst)
proveImplicationIO _ _ _ _ [] [] = return (Right [], emptySubst)
proveImplicationIO cfg lname varsInEnv as ps gs =
Num.withSolver cfg $ \s ->
debugBlock s "proveImplicationIO" $
do debugBlock s "assumes" (debugLog s ps)
debugBlock s "shows" (debugLog s gs)
debugLog s "------------------"
debugLog s "1. ------------------"
_simpPs <- Num.assumeProps s ps
mbImps <- Num.check s
debugLog s "2. ------------------"
case mbImps of
Nothing ->
do debugLog s "(contradiction in assumptions)"
return $ Left $ UnusableFunction (thing lname) ps
return (Left $ UnusableFunction (thing lname) ps, emptySubst)
Just (imps,extra) ->
do let su = importImps imps
@ -145,28 +148,30 @@ proveImplicationIO cfg lname varsInEnv as ps gs =
: map (show . Num.ppProp) invalid )
let gs1 = filter ((`notElem` ps) . goal) gs0
mb <- simpGoals s (scs ++ gs1)
debugLog s "3. ---------------------"
(mb,su1) <- simpGoals' s (scs ++ gs1)
case mb of
Left badGs -> reportUnsolved badGs
Right ([],su1) -> return (Right (su1,[]))
Left badGs -> reportUnsolved badGs (su1 @@ su)
Right [] -> return (Right [], su1 @@ su)
Right (us,su1) ->
Right us ->
-- Last hope: try to default stuff
do let vs = Set.filter isFreeTV $ fvs $ map goal us
dVars = Set.toList (vs `Set.difference` varsInEnv)
(_,us1,su2,ws) <- improveByDefaultingWith s dVars us
case us1 of
[] -> return (Right (su2 @@ su1, ws))
_ -> reportUnsolved us1
[] -> return (Right ws, su2 @@ su1 @@ su)
_ -> reportUnsolved us1 (su2 @@ su1 @@ su)
where
reportUnsolved us =
return $ Left $ UnsolvedDelcayedCt
reportUnsolved us su =
return ( Left $ UnsolvedDelcayedCt
$ DelayedCt { dctSource = lname
, dctForall = as
, dctAsmps = ps
, dctGoals = us
}
}, su)
@ -177,161 +182,176 @@ numericRight g = case Num.exportProp (goal g) of
Just p -> Right (g, p)
Nothing -> Left g
_testSimpGoals :: IO ()
_testSimpGoals = Num.withSolver cfg $ \s ->
do mapM_ dump asmps
mapM_ (dump .goal) gs
_ <- Num.assumeProps s asmps
_mbImps <- Num.check s
mb <- simpGoals s gs
case mb of
Right _ -> debugLog s "End of test"
Left _ -> debugLog s "Impossible"
{- Constraints and satisfiability:
1. [Satisfiable] A collection of constraints is _satisfiable_, if there is an
assignment for the variables that make all constraints true.
2. [Valid] If a constraint is satisfiable for any assignment of its free
variables, then it is _valid_, and may be ommited.
3. [Partial] A constraint may _partial_, which means that under some
assignment it is neither true nor false. For example:
`x - y > 5` is true for `{ x = 15, y = 3 }`, it is false for
`{ x = 5, y = 4 }`, and it is neither for `{ x = 1, y = 2 }`.
Note that constraints that are always true or undefined are NOT
valid, as there are assignemntes for which they are not true.
An example of such constraint is `x - y >= 0`.
4. [Provability] Instead of thinking of three possible values for
satisfiability (i.e., true, false, and unknown), we could instead
think of asking: "Is constraint C provable". This essentailly
maps "true" to "true", and "false,unknown" to "false", if we
treat constraints with malformed parameters as unprovable.
-}
{-
The plan:
1. Start with a set of constraints, CS
2. Compute its well-defined closure, DS.
3. Simplify constraints: evaluate terms in constraints as much as possible
4. Solve: eliminate constraints that are true
5. Check for consistency
6. Compute improvements
7. For each type in the improvements, add well-defined constraints
8. Instentiate constraints with substitution
9. Goto 3
-}
simpGoals' :: Num.Solver -> [Goal] -> IO (Either [Goal] [Goal], Subst)
simpGoals' s gs0 = go emptySubst [] (wellFormed gs0 ++ gs0)
where
cfg = SolverConfig { solverPath = "cvc4"
, solverArgs = [ "--lang=smt2", "--incremental", "--rewrite-divk" ]
, solverVerbose = 1
}
-- Assumes that the well-formed constraints are themselves well-formed.
wellFormed gs = [ g { goal = p } | g <- gs, p <- wfType (goal g) ]
asmps = []
go su old [] = return (Right old, su)
go su old gs =
do gs1 <- simplifyConstraintTerms s gs
res <- solveConstraints s old gs1
case res of
Left err -> return (Left err, su)
Right gs2 ->
do let gs3 = gs2 ++ old
mb <- computeImprovements s gs3
case mb of
Left err -> return (Left err, su)
Right impSu ->
let (unchanged,changed) =
partitionEithers (map (applyImp impSu) gs3)
new = wellFormed changed
in go (impSu @@ su) unchanged (new ++ changed)
gs = map fakeGoal [ tv 0 =#= tMin (num 10) (tv 1)
, tv 1 =#= num 10
]
applyImp su g = case apSubstMaybe su (goal g) of
Nothing -> Left g
Just p -> Right g { goal = p }
fakeGoal p = Goal { goalSource = undefined, goalRange = undefined, goal = p }
tv n = TVar (TVFree n KNum Set.empty (text "test var"))
_btv n = TVar (TVBound n KNum)
num x = tNum (x :: Int)
{- Note:
It is good to consider the other goals when evaluating terms.
For example, consider the constraints:
dump a = do putStrLn "-------------------_"
case Num.exportProp a of
Just b -> do print $ Num.ppProp' $ Num.propToProp' b
putStrLn "-------------------"
Nothing -> print "can't export"
P (x * inf), x >= 1
We cannot simplify `x * inf` on its own, because we do not know if `x`
might be 0. However, in the contxt of `x >= 1`, we know that this is
impossible, and we can simplify the constraints to:
P inf, x >= 1
However, we should be careful to avoid circular reasoning, as we wouldn't
want to use the fact that `x >= 1` to simplify `x >= 1` to true.
-}
-- XXX: currently simplify individually
simplifyConstraintTerms :: Num.Solver -> [Goal] -> IO [Goal]
simplifyConstraintTerms s gs =
debugBlock s "Simplifying terms" $ return (map simpGoal gs)
where simpGoal g = g { goal = simpProp (goal g) }
{- | Try to simplify a bunch of goals.
Assumes that the substitution has been applied to the goals.
The result:
* Left gs: the original goals were contradictory; here a subset that
leads to the contradiction.
* Right (gs,su): here is the simplified set of goals,
and an improving substitution. -}
simpGoals :: Num.Solver -> [Goal] -> IO (Either [Goal] ([Goal],Subst))
simpGoals _ [] = return (Right ([],emptySubst))
simpGoals s gs0 =
debugBlock s "Simplifying goals" $
do debugBlock s "goals:" (debugLog s gs0)
case impossibleClass of
[] ->
case numCts of
[] -> do debugBlock s "After simplification (no numerics):"
$ debugLog s unsolvedClassCts
return $ Right (unsolvedClassCts, emptySubst)
_ -> solveNumCts
_ -> return (Left impossibleClass)
solveConstraints :: Num.Solver ->
[Goal] {- We may use these, but don't try to solve,
we already tried and failed. -} ->
[Goal] {- Need to solve these -} ->
IO (Either [Goal] [Goal])
-- ^ Left: contradiciting goals,
-- Right: goals that were not solved, or sub-goals
-- for solved goals. Does not include "old"
solveConstraints s otherGs gs0 =
debugBlock s "Solving constraints" $ solveClassCts [] [] gs0
where
(impossibleClass,unsolvedClassCts,numCts) = solveClassCts [] [] [] gs0
otherNumerics = [ g | Right g <- map numericRight otherGs ]
solveClassCts impossible unsolved numerics goals =
case goals of
[] -> (impossible, unsolved, numerics)
g : gs ->
case numericRight g of
Right n -> solveClassCts impossible unsolved (n : numerics) gs
Left c ->
case classStep c of
solveClassCts unsolvedClass numerics [] =
do unsolvedNum <- solveNumerics s otherNumerics numerics
return (Right (unsolvedClass ++ unsolvedNum))
Unsolvable ->
solveClassCts (g : impossible) unsolved numerics gs
Unsolved ->
solveClassCts impossible (g : unsolved) numerics gs
Solved Nothing subs ->
solveClassCts impossible unsolved numerics (subs ++ gs)
Solved (Just su) _ ->
panic "solveClassCts" [ "Unexpected substituion"
, show su ]
updCt prop g = case Num.importProp prop of
Just [g1] -> g { goal = g1 }
r -> panic "simpGoals" [ "Unexpected import results"
, show r
]
solveNumCts =
do mbOk <- Num.prepareConstraints s updCt numCts
case mbOk of
Left bad -> return (Left bad)
Right (nonDef,def,imps,wds) ->
-- XXX: What should we do with the extra props...
do let (su,extraProps) = importSplitImps imps
(sideConds,invalid) = importSideConds wds
solveClassCts unsolved numerics (g : gs) =
case numericRight g of
Right n -> solveClassCts unsolved (n : numerics) gs
Left c ->
case classStep c of
Unsolvable -> return (Left [g])
Unsolved -> solveClassCts (g : unsolved) numerics gs
Solved Nothing subs -> solveClassCts unsolved numerics (subs ++ gs)
Solved (Just su) _ -> panic "solveClassCts"
[ "Unexpected substituion", show su ]
inIfForm =
Num.ppProp' $
Num.propToProp' $
case def of
[] -> Num.PTrue
_ -> foldr1 (Num.:&&)
$ map Num.dpSimpExprProp def
solveNumerics :: Num.Solver ->
[(Goal,Num.Prop)] {- ^ Consult these -} ->
[(Goal,Num.Prop)] {- ^ Solve these -} ->
IO [Goal]
solveNumerics s consultGs solveGs =
Num.withScope s $
do _ <- Num.assumeProps s (map (goal . fst) consultGs)
Num.simplifyProps s (map Num.knownDefined solveGs)
def1 = eliminateSimpleGEQ def
toGoal =
case map Num.dpData def1 of
[] -> case gs0 of
g : _ -> \p -> g { goal = p }
[] -> panic "simplification"
[ "Goals out of no goals." ]
[g] -> \p -> g { goal = p }
gs -> \p ->
Goal { goalRange = rCombs (map goalRange gs)
, goalSource = CtImprovement
, goal = p }
computeImprovements :: Num.Solver -> [Goal] -> IO (Either [Goal] Subst)
computeImprovements s gs
-- Find things of the form: `x = t`. We might do some rewriting to put
-- it in this form, if needed.
| (x,t) : _ <- mapMaybe (improveByDefn fins) gs =
do let su = singleSubst x t
debugLog s ("Improve by definition: " ++ show (pp su))
return (Right su)
| otherwise =
debugBlock s "Computing improvements" $
do let nums = [ g | Right g <- map numericRight gs ]
res <- Num.withScope s $
do _ <- Num.assumeProps s (map (goal . fst) nums)
mb <- Num.check s
case mb of
Nothing -> return Nothing
Just (suish,_ps1) ->
let (su,_ps2) = importSplitImps suish
in return (Just su)
case res of
Just su -> return (Right su)
Nothing ->
do bad <- Num.minimizeContradictionSimpDef s
(map Num.knownDefined nums)
return (Left bad)
unless (null invalid) $
panic "simpGoals" ( "Unable to import required well-definedness constraints:"
: map (show . Num.ppProp) invalid )
where
if null nonDef
then do debugLog s "(all constraints are well-defined)"
debugBlock s "In If-form:" $
debugLog s inIfForm
-- XXX remove this once the interval analysis is done
fins = Set.fromList [ tv | Goal { .. } <- gs
, Just tv <- [ tIsVar =<< pIsFin goal ] ]
else debugBlock s "Non-well defined constratins:" $
debugLog s nonDef
def2 <- Num.simplifyProps s def1
let allCts = apSubst su $ map toGoal extraProps ++
nonDef ++
unsolvedClassCts ++
def2 ++
sideConds
improveByDefn :: Fins -> Goal -> Maybe (TVar,Type)
improveByDefn fins Goal { .. } =
do (var,ty) <- tryRewritePropAsSubst fins goal
return (var,simpType ty)
debugBlock s "After simplification:" $
do debugLog s allCts
debugLog s su
-- XXX: Apply subst to class constraints and go again?
return $ Right ( allCts, su )
-- | Import an improving substitutin (i.e., a bunch of equations)
@ -381,47 +401,6 @@ importSideConds = go [] []
{- | Simplify easy less-than-or-equal-to and equal-to goals.
Those are common with long lists of literals, so we have special handling
for them. In particular:
* Reduce goals of the form @(a >= k1, a >= k2, a >= k3, ...)@ to
@a >= max (k1, k2, k3, ...)@, when all the k's are constant.
* Eliminate goals of the form @ki >= k2@, when @k2@ is leq than @k1@.
* Eliminate goals of the form @a >= 0@.
NOTE: This assumes that the goals are well-defined.
-}
eliminateSimpleGEQ :: [Num.DefinedProp a] -> [Num.DefinedProp a]
eliminateSimpleGEQ = go Map.empty []
where
go geqs other (g : rest) =
case Num.dpSimpExprProp g of
Num.K a Num.:== Num.K b
| a == b -> go geqs other rest
_ Num.:>= Num.K (Num.Nat 0) ->
go geqs other rest
Num.K (Num.Nat k1) Num.:>= Num.K (Num.Nat k2)
| k1 >= k2 -> go geqs other rest
Num.Var v Num.:>= Num.K (Num.Nat k2) ->
go (addUpperBound v (k2,g) geqs) other rest
_ -> go geqs (g:other) rest
go geqs other [] = [ g | (_,g) <- Map.elems geqs ] ++ other
-- add in a possible upper bound for var
addUpperBound var g = Map.insertWith cmp var g
where
cmp a b | fst a > fst b = a
| otherwise = b
@ -486,9 +465,9 @@ improveByDefaultingWith s as ps =
su = listSubst defs
-- Do this to simplify the instantiated "fin" constraints.
mb <- simpGoals s (newOthers ++ others ++ apSubst su fins)
(mb,su1) <- simpGoals' s (newOthers ++ others ++ apSubst su fins)
case mb of
Right (gs1,su1) ->
Right gs1 ->
let warn (x,t) =
case x of
TVFree _ _ _ d -> DefaultingTo d t
@ -508,7 +487,7 @@ improveByDefaultingWith s as ps =
-- Something went wrong, don't default.
Left _ -> return (as,ps,emptySubst,[])
Left _ -> return (as,ps,su1 @@ su,[])
classify leqs fins others (prop : more) =
@ -583,11 +562,11 @@ defaultReplExpr cfg e s =
mbSubst <- tryGetModel cfg params (sProps s)
case mbSubst of
Just su ->
do res <- Num.withSolver cfg $ \so ->
simpGoals so (map (makeGoal su) (sProps s))
do (res,su1) <- Num.withSolver cfg $ \so ->
simpGoals' so (map (makeGoal su) (sProps s))
return $
case res of
Right ([],su1) | isEmptySubst su1 ->
Right [] | isEmptySubst su1 ->
do tys <- mapM (bindParam su) params
return (zip (sVars s) tys, appExpr tys)
_ -> Nothing
@ -627,6 +606,16 @@ tryGetModel cfg xs ps =
simpType :: Type -> Type
simpType ty = fromMaybe ty (simpTypeMaybe ty)
simpProp :: Prop -> Prop
simpProp p = case p of
TUser f ts q -> TUser f (map simpType ts) (simpProp q)
TCon c ts -> TCon c (map simpType ts)
TVar {} -> panic "simpProp" ["variable", show p]
TRec {} -> panic "simpProp" ["record", show p]
simpTypeMaybe :: Type -> Maybe Type
simpTypeMaybe ty =
case ty of
@ -647,3 +636,43 @@ simpTypeMaybe ty =
--------------------------------------------------------------------------------
_testSimpGoals :: IO ()
_testSimpGoals = Num.withSolver cfg $ \s ->
do mapM_ dump asmps
mapM_ (dump .goal) gs
_ <- Num.assumeProps s asmps
_mbImps <- Num.check s
(mb,_) <- simpGoals' s gs
case mb of
Right _ -> debugLog s "End of test"
Left _ -> debugLog s "Impossible"
where
cfg = SolverConfig { solverPath = "cvc4"
, solverArgs = [ "--lang=smt2", "--incremental", "--rewrite-divk" ]
, solverVerbose = 1
}
asmps = []
gs = map fakeGoal [ tv 0 =#= tMin (num 10) (tv 1)
, tv 1 =#= num 10
]
fakeGoal p = Goal { goalSource = undefined, goalRange = undefined, goal = p }
tv n = TVar (TVFree n KNum Set.empty (text "test var"))
_btv n = TVar (TVBound n KNum)
num x = tNum (x :: Int)
dump a = do putStrLn "-------------------_"
case Num.exportProp a of
Just b -> do print $ Num.ppProp' $ Num.propToProp' b
putStrLn "-------------------"
Nothing -> print "can't export"

203
src/Cryptol/TypeCheck/Solver/CrySAT.hs
View File

@ -18,7 +18,8 @@ module Cryptol.TypeCheck.Solver.CrySAT
, DefinedProp(..)
, debugBlock
, DebugLog(..)
, prepareConstraints
, knownDefined
, minimizeContradictionSimpDef
) where
import qualified Cryptol.TypeCheck.AST as Cry
@ -29,7 +30,6 @@ import Cryptol.TypeCheck.Solver.Numeric.AST
import Cryptol.TypeCheck.Solver.Numeric.ImportExport
import Cryptol.TypeCheck.Solver.Numeric.Defined
import Cryptol.TypeCheck.Solver.Numeric.Simplify
import Cryptol.TypeCheck.Solver.Numeric.SimplifyExpr(crySimpExpr)
import Cryptol.TypeCheck.Solver.Numeric.NonLin
import Cryptol.TypeCheck.Solver.Numeric.SMT
import Cryptol.Utils.PP -- ( Doc )
@ -37,8 +37,6 @@ import Cryptol.Utils.Panic ( panic )
import MonadLib
import Data.Maybe ( mapMaybe, fromMaybe )
import Data.Either ( partitionEithers )
import Data.List(nub)
import qualified Data.Map as Map
import Data.Foldable ( any, all )
import qualified Data.Set as Set
@ -74,6 +72,10 @@ data DefinedProp a = DefinedProp
terms because we want to import them back into Crytpol types. -}
}
knownDefined :: (a,Prop) -> DefinedProp a
knownDefined (a,p) = DefinedProp
{ dpData = a, dpSimpProp = simpProp p, dpSimpExprProp = p }
instance HasVars SimpProp where
apSubst su (SimpProp p) = do p1 <- apSubst su p
@ -81,106 +83,6 @@ instance HasVars SimpProp where
guard (p1 /= p2)
return (SimpProp p2)
apSubstDefinedProp :: (Prop -> a -> a) ->
Subst -> DefinedProp a -> Maybe (DefinedProp a)
apSubstDefinedProp updCt su DefinedProp { .. } =
do s1 <- apSubst su dpSimpProp
return $ case apSubst su dpSimpExprProp of
Nothing -> DefinedProp { dpSimpProp = s1, .. }
Just p1 -> DefinedProp { dpSimpProp = s1
, dpSimpExprProp = p1
, dpData = updCt p1 dpData
}
{- | Check if the given constraint is guaranteed to be well-defined.
This means that it cannot be instantiated in a way that would result in
undefined behaviour.
This estimate is consevative:
* if we return `Right`, then the property is definately well-defined
* if we return `Left`, then we don't know if the property is well-defined
If the property is well-defined, then we also simplify it.
-}
checkDefined1 :: Solver -> (Prop -> a -> a) ->
(a,Prop) -> IO (Either (a,Prop) (DefinedProp a))
checkDefined1 s updCt (ct,p) =
do proved <- prove s defCt
return $
if proved
then Right $
case crySimpPropExprMaybe p of
Nothing -> DefinedProp { dpData = ct
, dpSimpExprProp = p
, dpSimpProp = simpProp p
}
Just p' -> DefinedProp { dpData = updCt p' ct
, dpSimpExprProp = p'
, dpSimpProp = simpProp p'
}
else Left (ct,p)
where
SimpProp defCt = simpProp (cryDefinedProp p)
prepareConstraints ::
Solver -> (Prop -> a -> a) ->
[(a,Prop)] -> IO (Either [a] ([a], [DefinedProp a], Subst, [Prop]))
prepareConstraints s updCt cs =
do res <- mapM (checkDefined1 s updCt) cs
let (unknown,ok) = partitionEithers res
goStep1 unknown ok Map.empty []
where
getImps ok = withScope s $
do mapM_ (assert s . dpSimpProp) ok
check s
mapEither f = partitionEithers . map f
apSuUnk su (x,p) =
case apSubst su p of
Nothing -> Left (x,p)
Just p1 -> Right (updCt p1 x, p1)
apSuOk su p = case apSubstDefinedProp updCt su p of
Nothing -> Left p
Just p1 -> Right p1
apSubst' su x = fromMaybe x (apSubst su x)
goStep1 unknown ok su sgs =
do let (ok1, moreSu) = improveByDefnMany updCt ok
go unknown ok1 (composeSubst moreSu su) (map (apSubst' moreSu) sgs)
go unknown ok su sgs =
do mb <- getImps ok
case mb of
Nothing ->
do bad <- minimizeContradictionSimpDef s ok
return (Left bad)
Just (imps,subGoals)
| not (null okNew) -> goStep1 unknown (okNew ++ okOld) newSu newGs
| otherwise ->
do res <- mapM (checkDefined1 s updCt) unkNew
let (stillUnk,nowOk) = partitionEithers res
if null nowOk
then return (Right ( map fst (unkNew ++ unkOld)
, ok, newSu, newGs))
else goStep1 (stillUnk ++ unkOld) (nowOk ++ ok) newSu newGs
where (okOld, okNew) = mapEither (apSuOk imps) ok
(unkOld,unkNew) = mapEither (apSuUnk imps) unknown
newSu = composeSubst imps su
newGs = nub (subGoals ++ map (apSubst' su) sgs)
-- XXX: inefficient
@ -190,7 +92,7 @@ prepareConstraints s updCt cs =
simplifyProps :: Solver -> [DefinedProp a] -> IO [a]
simplifyProps s props =
debugBlock s "Simplifying properties" $
withScope s (go [] props)
withScope s (go [] (eliminateSimpleGEQ props))
where
go survived [] = return survived
@ -209,6 +111,51 @@ simplifyProps s props =
go (dpData p : survived) more
{- | Simplify easy less-than-or-equal-to and equal-to goals.
Those are common with long lists of literals, so we have special handling
for them. In particular:
* Reduce goals of the form @(a >= k1, a >= k2, a >= k3, ...)@ to
@a >= max (k1, k2, k3, ...)@, when all the k's are constant.
* Eliminate goals of the form @ki >= k2@, when @k2@ is leq than @k1@.
* Eliminate goals of the form @a >= 0@.
NOTE: This assumes that the goals are well-defined.
-}
eliminateSimpleGEQ :: [DefinedProp a] -> [DefinedProp a]
eliminateSimpleGEQ = go Map.empty []
where
go geqs other (g : rest) =
case dpSimpExprProp g of
K a :== K b
| a == b -> go geqs other rest
_ :>= K (Nat 0) ->
go geqs other rest
K (Nat k1) :>= K (Nat k2)
| k1 >= k2 -> go geqs other rest
Var v :>= K (Nat k2) ->
go (addUpperBound v (k2,g) geqs) other rest
_ -> go geqs (g:other) rest
go geqs other [] = [ g | (_,g) <- Map.elems geqs ] ++ other
-- add in a possible upper bound for var
addUpperBound var g = Map.insertWith cmp var g
where
cmp a b | fst a > fst b = a
| otherwise = b
-- | Add the given constraints as assumptions.
-- * We assume that the constraints are well-defined.
-- * Modifies the set of assumptions.
@ -249,52 +196,6 @@ minimizeContradictionSimpDef s ps = start [] ps
_ -> go bad (d : prev) more
improveByDefnMany :: (Prop -> a -> a) ->
[DefinedProp a] -> ([DefinedProp a], Subst)
improveByDefnMany updCt = go [] Map.empty
where
mbSu su x = case apSubstDefinedProp updCt su x of
Nothing -> Left x
Just y -> Right y
go todo su (p : ps) =
let p1 = fromMaybe p (apSubstDefinedProp updCt su p)
in case improveByDefn p1 of
Just (x,e) ->
go todo (composeSubst (Map.singleton x e) su) ps
-- `p` is solved, so ignore
Nothing -> go (p1 : todo) su ps
go todo su [] =
let (same,changed) = partitionEithers (map (mbSu su) todo)
in case changed of
[] -> (same, fmap crySimpExpr su)
_ -> go same su changed
{- | If we see an equation: `?x = e`, and:
* ?x is a unification variable
* `e` is "zonked" (substitution is fully applied)
* ?x does not appear in `e`.
then, we can improve `?x` to `e`.
-}
improveByDefn :: DefinedProp a -> Maybe (Name,Expr)
improveByDefn p =
case dpSimpExprProp p of
Var x :== e
| isUV x -> tryToBind x e
e :== Var x
| isUV x -> tryToBind x e
_ -> Nothing
where
tryToBind x e
| x `Set.member` cryExprFVS e = Nothing
| otherwise = Just (x,e)
isUV (UserName (Cry.TVFree {})) = True
isUV _ = False
{- | Attempt to find a substituion that, when applied, makes all of the
given properties hold. -}

20
src/Cryptol/TypeCheck/Solver/InfNat.hs
View File

@ -31,6 +31,26 @@ fromNat n' =
Nat i -> Just i
_ -> Nothing
--------------------------------------------------------------------------------
nEq :: Maybe Nat' -> Maybe Nat' -> Bool
nEq (Just x) (Just y) = x == y
nEq _ _ = False
nGt :: Maybe Nat' -> Maybe Nat' -> Bool
nGt (Just x) (Just y) = x > y
nGt _ _ = False
nFin :: Maybe Nat' -> Bool
nFin (Just x) = x /= Inf
nFin _ = False
--------------------------------------------------------------------------------
nAdd :: Nat' -> Nat' -> Nat'
nAdd Inf _ = Inf
nAdd _ Inf = Inf

76
src/Cryptol/TypeCheck/Solver/Numeric/Fin.hs Normal file
View File

@ -0,0 +1,76 @@
-- | Simplification of `fin` constraints.
module Cryptol.TypeCheck.Solver.Numeric.Fin where
import Data.Map (Map)
import Cryptol.TypeCheck.AST
import Cryptol.TypeCheck.InferTypes
import Cryptol.TypeCheck.Solver.Numeric.Interval
import Cryptol.TypeCheck.Solver.InfNat
cryIsFin :: Map TVar Interval -> Goal -> Solved
cryIsFin varInfo g =
case tNoUser (goal g) of
TCon (TC tc) [] | TCNum _ <- tc -> solved []
TCon (TF f) ts ->
case (f,ts) of
(TCAdd,[t1,t2]) -> solved [ pFin t1, pFin t2 ]
(TCSub,[t1,_ ]) -> solved [ pFin t1 ]
-- fin (x * y)
(TCMul,[t1,t2])
| iLower i1 >= Nat 1 && iIsFin i1 -> solved [ pFin t2 ]
| iLower i2 >= Nat 1 && iIsFin i2 -> solved [ pFin t1 ]
| iLower i1 >= Nat 1 &&
iLower i2 >= Nat 1 -> solved [ pFin t1, pFin t2 ]
| iIsFin i1 && iIsFin i2 -> solved []
where
i1 = typeInterval varInfo t1
i2 = typeInterval varInfo t2
(TCDiv, [t1,_]) -> solved [ pFin t1 ]
(TCMod, [_,_]) -> solved []
-- fin (x ^ y)
(TCExp, [t1,t2])
| iLower i1 == Inf -> solved [ t2 =#= tZero ]
| iLower i2 == Inf -> solved [ tOne >== t1 ]
| iLower i1 >= Nat 2 -> solved [ pFin t1, pFin t2 ]
| iLower i2 >= Nat 1 -> solved [ pFin t1, pFin t2 ]
| Just x <- iUpper i1, x <= Nat 1 -> solved []
| Just (Nat 0) <- iUpper i2 -> solved []
where
i1 = typeInterval varInfo t1
i2 = typeInterval varInfo t2
-- fin (min x y)
(TCMin, [t1,t2])
| iIsFin i1 -> solved []
| iIsFin i2 -> solved []
| Just x <- iUpper i1, x <= iLower i2 -> solved [ pFin t1 ]
| Just x <- iUpper i2, x <= iLower i1 -> solved [ pFin t2 ]
where
i1 = typeInterval varInfo t1
i2 = typeInterval varInfo t2
(TCMax, [t1,t2]) -> solved [ pFin t1, pFin t2 ]
(TCWidth, [t1]) -> solved [ pFin t1 ]
(TCLenFromThen,[_,_,_]) -> solved []
(TCLenFromThenTo,[_,_,_]) -> solved []
_ -> Unsolved
_ -> Unsolved
where
solved ps = Solved Nothing [ g { goal = p } | p <- ps ]

250
src/Cryptol/TypeCheck/Solver/Numeric/Interval.hs
View File

@ -1,17 +1,54 @@
module Solver.Numeric.Interval where
{-# LANGUAGE PatternGuards #-}
import Cryptol.TypeCheck.Solver.Numeric.AST
-- | An interval interpretation of types.
module Cryptol.TypeCheck.Solver.Numeric.Interval where
import Cryptol.TypeCheck.AST
import Cryptol.TypeCheck.Solver.InfNat
import Data.Maybe(fromMaybe)
import Data.Map ( Map )
import qualified Data.Map as Map
import Text.PrettyPrint
-- | Only meaningful for numeric types
typeInterval :: Map TVar Interval -> Type -> Interval
typeInterval varInfo = go
where
go ty =
case ty of
TUser _ _ t -> go t
TCon tc ts ->
case (tc, ts) of
(TC TCInf, []) -> iConst Inf
(TC (TCNum n), []) -> iConst (Nat n)
(TF TCAdd, [x,y]) -> iAdd (go x) (go y)
(TF TCSub, [x,y]) -> iSub (go x) (go y)
(TF TCMul, [x,y]) -> iMul (go x) (go y)
(TF TCDiv, [x,y]) -> iDiv (go x) (go y)
(TF TCMod, [x,y]) -> iMod (go x) (go y)
(TF TCExp, [x,y]) -> iExp (go x) (go y)
(TF TCWidth, [x]) -> iWidth (go x)
(TF TCMin, [x,y]) -> iMin (go x) (go y)
(TF TCMax, [x,y]) -> iMax (go x) (go y)
(TF TCLenFromThen, [x,y,z]) ->
iLenFromThen (go x) (go y) (go z)
(TF TCLenFromThenTo, [x,y,z]) ->
iLenFromThenTo (go x) (go y) (go z)
_ -> iAny
TVar x -> Map.findWithDefault iAny x varInfo
_ -> iAny
--------------------------------------------------------------------------------
data Interval = Interval
{ iLower :: Nat' -- ^ lower bound (inclusive)
, iUpper :: Maybe Nat'
-- ^ upper bound (inclusinve)
-- If there is no upper bound, than all *natural* numbers.
}
, iUpper :: Maybe Nat' -- ^ upper bound (inclusive)
-- If there is no upper bound,
-- than all *natural* numbers.
} deriving (Eq,Show)
ppInterval :: Interval -> Doc
ppInterval x = brackets (hsep [ pp (iLower x)
@ -23,6 +60,50 @@ ppInterval x = brackets (hsep [ pp (iLower x)
Inf -> text "inf"
iIsExact :: Interval -> Maybe Nat'
iIsExact i = if iUpper i == Just (iLower i) then Just (iLower i) else Nothing
iIsFin :: Interval -> Bool
iIsFin i = case iUpper i of
Just Inf -> False
_ -> True
-- | Returns 'True' when the intervals definitely overlap, and 'False'
-- otherwise.
iDisjoint :: Interval -> Interval -> Bool
iDisjoint
(Interval (Nat l1) (Just (Nat h1)))
(Interval (Nat l2) (Just (Nat h2))) =
or [ h1 > l2 && h1 < h2, l1 > l2 && l1 < h2 ]
iDisjoint _ _ = False
-- | Intersect two intervals, yielding a new one that describes the space where
-- they overlap. If the two intervals are disjoint, the result will be
-- 'Nothing'.
iIntersect :: Interval -> Interval -> Maybe Interval
iIntersect i j =
case (lower,upper) of
(Nat l, Just (Nat u)) | l < u -> ok
(Nat _, Just Inf) -> ok
(Nat _, Nothing) -> ok
(Inf, Just Inf) -> ok
_ -> Nothing
where
ok = Just (Interval lower upper)
lower = nMax (iLower i) (iLower j)
upper = case (iUpper i, iUpper j) of
(Just a, Just b) -> Just (nMin a b)
(Nothing,Nothing) -> Nothing
(Just l,Nothing) | l /= Inf -> Just l
(Nothing,Just r) | r /= Inf -> Just r
_ -> Nothing
-- | Any value
iAny :: Interval
iAny = Interval (Nat 0) (Just Inf)
@ -35,47 +116,144 @@ iAnyFin = Interval (Nat 0) Nothing
iConst :: Nat' -> Interval
iConst x = Interval x (Just x)
iAdd :: Interval -> Interval -> Interval
iAdd i j = Interval { iLower = nAdd (iLower i) (iLower j)
, iUpper = case (iUpper i, iUpper j) of
(Nothing, Nothing) -> Nothing
(Just x, Just y) -> Just (nAdd x y)
(Nothing, Just y) -> upper y
(Just x, Nothing) -> upper x
(Nothing, Nothing) -> Nothing
(Just x, Just y) -> Just (nAdd x y)
(Nothing, Just y) -> upper y
(Just x, Nothing) -> upper x
}
where
upper x = case x of
Inf -> Just Inf
_ -> Nothing
iSub :: Interval -> Interval -> Maybe Interval
iSub i j =
case iUpper i of
Nothing -> case iLower j of
Nat _ -> Just Interval { iLower = l, iUpper = Nothing }
Inf -> Nothing -- subtract infinitiy
Just n -> do u <- nSub n (iLower j)
return Interval { iLower = l, iUpper = Just u }
iMul :: Interval -> Interval -> Interval
iMul i j = Interval { iLower = nMul (iLower i) (iLower j)
, iUpper = case (iUpper i, iUpper j) of
(Nothing, Nothing) -> Nothing
(Just x, Just y) -> Just (nMul x y)
(Nothing, Just y) -> upper y
(Just x, Nothing) -> upper x
}
where
upper x = case x of
Inf -> Just Inf
Nat 0 -> Just (Nat 0)
_ -> Nothing
where l = fromMaybe (Nat 0) (nSub (iLower i) =<< iUpper j)
iExp :: Interval -> Interval -> Interval
iExp i j = Interval { iLower = nExp (iLower i) (iLower j)
, iUpper = case (iUpper i, iUpper j) of
(Nothing, Nothing) -> Nothing
(Just x, Just y) -> Just (nExp x y)
(Nothing, Just y) -> upperR y
(Just x, Nothing) -> upperL x
}
where
upperL x = case x of
Inf -> Just Inf
Nat 0 -> Just (Nat 0)
Nat 1 -> Just (Nat 1)
_ -> Nothing
upperR x = case x of
Inf -> Just Inf
Nat 0 -> Just (Nat 1)
_ -> Nothing
iMin :: Interval -> Interval -> Interval
iMin i j = Interval { iLower = nMin (iLower i) (iLower j)
, iUpper = case (iUpper i, iUpper j) of
(Nothing, Nothing) -> Nothing
(Just x, Just y) -> Just (nMin x y)
(Nothing, Just Inf) -> Nothing
(Nothing, Just y) -> Just y
(Just Inf, Nothing) -> Nothing
(Just x, Nothing) -> Just x
}
iMax :: Interval -> Interval -> Interval
iMax i j = Interval { iLower = nMax (iLower i) (iLower j)
, iUpper = case (iUpper i, iUpper j) of
(Nothing, Nothing) -> Nothing
(Just x, Just y) -> Just (nMax x y)
(Nothing, Just Inf) -> Just Inf
(Nothing, Just _) -> Nothing
(Just Inf, Nothing) -> Just Inf
(Just _, Nothing) -> Nothing
}
iSub :: Interval -> Interval -> Interval
iSub i j = Interval { iLower = lower, iUpper = upper }
where
lower = case iUpper j of
Nothing -> Nat 0
Just x -> case nSub (iLower i) x of
Nothing -> Nat 0
Just y -> y
upper = case iUpper i of
Nothing -> Nothing
Just x -> case nSub x (iLower j) of
Nothing -> Just Inf {- malformed subtraction -}
Just y -> Just y
iDiv :: Interval -> Interval -> Interval
iDiv i j = Interval { iLower = lower, iUpper = upper }
where
lower = case iUpper j of
Nothing -> Nat 0
Just x -> case nDiv (iLower i) x of
Nothing -> Nat 0 -- malformed division
Just y -> y
upper = case iUpper i of
Nothing -> Nothing
Just x -> case nDiv x (nMax (iLower i) (Nat 1)) of
Nothing -> Just Inf
Just y -> Just y
iMod :: Interval -> Interval -> Interval
iMod _ j = Interval { iLower = Nat 0, iUpper = upper }
where
upper = case iUpper j of
Just (Nat n) | n > 0 -> Just (Nat (n - 1))
_ -> Nothing
iWidth :: Interval -> Interval
iWidth i = Interval { iLower = nWidth (iLower i)
, iUpper = case iUpper i of
Nothing -> Nothing
Just n -> Just (nWidth n)
}
iLenFromThen :: Interval -> Interval -> Interval -> Interval
iLenFromThen i j w
| Just x <- iIsExact i, Just y <- iIsExact j, Just z <- iIsExact w
, Just r <- nLenFromThen x y z = iConst r
| otherwise =
case iUpper w of
Just (Nat n) ->
Interval { iLower = Nat 0, iUpper = Just (Nat (2^n - 1)) }
_ -> iAnyFin
iLenFromThenTo :: Interval -> Interval -> Interval -> Interval
iLenFromThenTo i j k
| Just x <- iIsExact i, Just y <- iIsExact j, Just z <- iIsExact k
, Just r <- nLenFromThenTo x y z = iConst r
| otherwise = iAnyFin
{-
data Expr = K Nat'
| Var Name
| Expr :+ Expr
| Expr :- Expr
| Expr :* Expr
| Div Expr Expr
| Mod Expr Expr
| Expr :^^ Expr
| Min Expr Expr
| Max Expr Expr
| Lg2 Expr
| Width Expr
| LenFromThen Expr Expr Expr
| LenFromThenTo Expr Expr Expr
-}

4
src/Cryptol/TypeCheck/Solver/Numeric/SMT.hs
View File

@ -450,12 +450,14 @@ cryCheckLinRel s logger x y p1 p2 =
| a < 0 = K (Nat b) :- K (Nat (negate a)) :* Var x
| otherwise = sumTerm (K (Nat a) :* Var x)
SMT.logMessage logger ("candidate: " ++ show (ppProp (Var y :==: expr)))
proved <- checkUnsat s
$ propToSmtLib $ crySimplify
$ Not $ Var y :==: expr
if not proved
then return Nothing
then SMT.logMessage logger "failed" >> return Nothing
else return (Just (expr,wellDefined expr)))
-- Try to get an example of another point, which is finite, and at

2
src/Cryptol/TypeCheck/Solver/Numeric/Simplify.hs
View File

@ -371,6 +371,8 @@ cryIsEq x y =
(K Inf, _) -> Not (Fin y)
(_, K Inf) -> Not (Fin x)
(Div x y, z) -> x :>= z :* y :&& (one :+ z) :* y :> x
(K (Nat n),_) | Just p <- cryIsNat False n y -> p
(_,K (Nat n)) | Just p <- cryIsNat False n x -> p

151
src/Cryptol/TypeCheck/Solver/Numeric/Simplify1.hs
View File

@ -18,6 +18,7 @@ module Cryptol.TypeCheck.Solver.Numeric.Simplify1 (propToProp', ppProp') where
import Cryptol.TypeCheck.Solver.Numeric.SimplifyExpr
(crySimpExpr, splitSum, normSum, Sign(..))
import Cryptol.TypeCheck.Solver.Numeric.AST
import Cryptol.TypeCheck.Solver.InfNat(genLog,rootExact)
import Cryptol.Utils.Misc ( anyJust )
import Cryptol.Utils.PP
@ -195,18 +196,19 @@ pAtom p = do a <- case p of
-- | Implementation of `==`
pEq :: Expr -> Expr -> I Bool
pEq x (K (Nat 0)) = pEq0 x
pEq x (K (Nat 1)) = pEq1 x
pEq (K (Nat 0)) y = pEq0 y
pEq (K (Nat 1)) y = pEq1 y
pEq x y = pIf (pInf x) (pInf y)
$ pAnd (pFin y) (pAtom (AEq x y))
pEq x (K (Nat n)) = pIsNat n x
pEq (K (Nat n)) y = pIsNat n y
pEq x y = pIf (pInf x) (pInf y) (pAnd (pFin y) (pAtom (AEq x y)))
-- | Implementation of `>=`
pGeq :: Expr -> Expr -> I Bool
pGeq x y = pIf (pInf x) pTrue
$ pIf (pFin y) (pAtom (AGt (x :+ one) y))
pFalse
pGeq x y = pIf (pInf x) pTrue (pAnd (pFin y) (pAtom (AGt (one :+ x) y)))
-- | Implementation `e1 > e2`.
pGt :: Expr -> Expr -> I Bool
pGt x y = pNot (pGeq y x)
-- | Implementation of `Fin`
pFin :: Expr -> I Bool
@ -235,62 +237,101 @@ pFin expr =
LenFromThen _ _ _ -> pTrue
LenFromThenTo _ _ _ -> pTrue
-- | Implementation `e1 > e2`.
pGt :: Expr -> Expr -> I Bool
pGt x y = pIf (pFin y) (pIf (pFin x) (pAtom (AGt x y)) pTrue) pFalse
-- | Implementation of `e == inf`
pInf :: Expr -> I Bool
pInf = pNot . pFin
-- | Special case: `e == 0`
pEq0 :: Expr -> I Bool
pEq0 expr =
pIsNat :: Integer -> Expr -> I Bool
pIsNat n expr =
case expr of
K Inf -> pFalse
K (Nat n) -> if n == 0 then pTrue else pFalse
Var _ -> pAnd (pFin expr) (pAtom (AEq expr zero))
t1 :+ t2 -> pAnd (pEq t1 zero) (pEq t2 zero)
t1 :- t2 -> pEq t1 t2
t1 :* t2 -> pOr (pEq t1 zero) (pEq t2 zero)
Div t1 t2 -> pGt t2 t1
Mod _ _ -> pAtom (AEq expr zero) -- or divides
t1 :^^ t2 -> pIf (pEq t2 zero) pFalse (pEq t1 zero)
Min t1 t2 -> pOr (pEq t1 zero) (pEq t2 zero)
Max t1 t2 -> pAnd (pEq t1 zero) (pEq t2 zero)
Width t1 -> pEq t1 zero
LenFromThen _ _ _ -> pFalse
LenFromThenTo x y z -> pIf (pGt x y) (pGt z x) (pGt x z)
K (Nat m) -> if m == n then pTrue else pFalse
Var _ -> nothing
-- | Special case: `e == 1`
pEq1 :: Expr -> I Bool
pEq1 expr =
case expr of
K Inf -> pFalse
K (Nat n) -> if n == 1 then pTrue else pFalse
Var _ -> pAnd (pFin expr) (pAtom (AEq expr one))
t1 :+ t2 -> pIf (pEq t1 zero) (pEq t2 one)
$ pIf (pEq t2 zero) (pEq t1 one) pFalse
t1 :- t2 -> pEq t1 (t2 :+ one)
t1 :* t2 -> pAnd (pEq t1 one) (pEq t2 one)
Div t1 t2 -> pAnd (pGt (two :* t2) t1) (pGeq t1 t2)
Mod _ _ -> pAtom (AEq expr one)
t1 :^^ t2 -> pOr (pEq t1 one) (pEq t2 zero)
K (Nat m) :+ e2 -> if n < m then pFalse
else pIsNat (n - m) e2
x :+ y
| n == 0 -> pAnd (pIsNat 0 x) (pIsNat 0 y)
| n == 1 -> pOr (pAnd (pIsNat 0 x) (pIsNat 1 y))
(pAnd (pIsNat 1 x) (pIsNat 0 y))
| otherwise -> nothing
Min t1 t2 -> pIf (pEq t1 one) (pGt t2 zero)
$ pIf (pEq t2 one) (pGt t1 zero)
pFalse
Max t1 t2 -> pIf (pEq t1 one) (pGt two t2)
$ pIf (pEq t2 one) (pGt two t1)
pFalse
e1 :- e2 -> pEq (K (Nat n) :+ e1) e2
Width t1 -> pEq t1 one
K (Nat m) :* e2 ->
if m == 0
then if n == 0 then pTrue else pFalse
else case divMod n m of
(q,r) -> if r == 0 then pIsNat q e2
else pFalse
e1 :* e2
| n == 0 -> pOr (pIsNat 0 e1) (pIsNat 0 e2)
| n == 1 -> pAnd (pIsNat 1 e1) (pIsNat 1 e2)
| otherwise -> nothing
-- See Note [Sequences of Length 1] in 'Cryptol.TypeCheck.Solver.InfNat'
LenFromThen x y w -> pAnd (pGt y x) (pGeq y (two :^^ w))
LenFromThenTo x y z -> pIf (pGt z y) (pGeq x z) (pGeq z x)
-- (x >= n * y) /\ ((n+1) * y > x)
Div x y -> pAnd (pGt (one :+ x) (K (Nat n) :* y))
(pGt (K (Nat (n + 1)) :* y) x)
Mod _ _ -> nothing
K (Nat m) :^^ y -> case genLog n m of
Just (a, exact) | exact -> pIsNat a y
_ -> pFalse
x :^^ K (Nat m) -> case rootExact n m of
Just a -> pIsNat a x
Nothing -> pFalse
x :^^ y
| n == 0 -> pAnd (pIsNat 0 x) (pGt y zero)
| n == 1 -> pOr (pIsNat 1 x) (pIsNat 0 y)
| otherwise -> nothing
Min x y
| n == 0 -> pOr (pIsNat 0 x) (pIsNat 0 y)
| otherwise -> pOr (pAnd (pIsNat n x) (pGt y (K (Nat (n - 1)))))
(pAnd (pIsNat n y) (pGt x (K (Nat (n - 1)))))
Max x y -> pOr (pAnd (pIsNat n x) (pGt (K (Nat (n + 1))) y))
(pAnd (pIsNat n y) (pGt (K (Nat (n + 1))) y))
Width x
| n == 0 -> pIsNat 0 x
| otherwise -> pAnd (pGt x (K (Nat (2^(n-1) - 1))))
(pGt (K (Nat (2 ^ n))) x)
{-
LenFromThen x y w
| n == 0 -> Just PFalse
-- See Note [Sequences of Length 1] in 'Cryptol.TypeCheck.Solver.InfNat'
| n == 1 -> Just (gt y x :&& gt (y :+ one) (two :^^ w))
| otherwise -> Nothing -- XXX: maybe some more?
-- See `nLenFromThenTo` in 'Cryptol.TypeCheck.Solver.InfNat'
LenFromThenTo x y z
| n == 0 -> Just ( gt x y :&& gt z x
:|| gt y x :&& gt x z
)
-- See Note [Sequences of Length 1] in 'Cryptol.TypeCheck.Solver.InfNat'
| n == 1 -> Just (gt z y :&& gt (x :+ one) z :||
gt y z :&& gt (z :+ one) x)
| otherwise -> Nothing -- XXX: maybe some more?
-}
where
nothing = pAnd (pFin expr) (pAtom (AEq expr (K (Nat n))))
pIsGtThanNat :: Integer -> Expr -> I Bool
pIsGtThanNat = undefined
pNatIsGtThan :: Integer -> Expr -> I Bool
pNatIsGtThan = undefined
--------------------------------------------------------------------------------

161
src/Cryptol/TypeCheck/Solver/Simplify.hs Normal file
View File

@ -0,0 +1,161 @@
{-# LANGUAGE RecordWildCards #-}
{-# LANGUAGE MultiWayIf #-}
module Cryptol.TypeCheck.Solver.Simplify (
Fins,
tryRewritePropAsSubst
) where
import Cryptol.Prims.Syntax (TFun(..))
import Cryptol.TypeCheck.AST (Type(..),Prop,TVar,pIsEq,isFreeTV,TCon(..))
import Cryptol.TypeCheck.Subst (fvs)
import Control.Monad (msum,guard,mzero)
import Data.Function (on)
import Data.List (sortBy)
import Data.Maybe (catMaybes,listToMaybe)
import qualified Data.Set as Set
-- | Type variables that are known to have a `fin` constraint. This set is used
-- to justify the addition of a subtraction on the rhs of an equality
-- constraint.
type Fins = Set.Set TVar
-- | When given an equality constraint, attempt to rewrite it to the form `?x =
-- ...`, by moving all occurrences of `?x` to the LHS, and any other variables
-- to the RHS. This will only work when there's only one unification variable
-- present in the prop.
tryRewritePropAsSubst :: Fins -> Prop -> Maybe (TVar,Type)
tryRewritePropAsSubst fins p =
do (x,y) <- pIsEq p
let vars = Set.toList (Set.filter isFreeTV (fvs p))
listToMaybe $ sortBy (flip compare `on` rank)
$ catMaybes [ tryRewriteEq fins var x y | var <- vars ]
-- | Rank a rewrite, favoring expressions that have fewer subtractions than
-- additions.
rank :: (TVar,Type) -> Int
rank (_,ty) = go ty
where
go (TCon (TF TCAdd) ts) = sum (map go ts) + 1
go (TCon (TF TCSub) ts) = sum (map go ts) - 1
go (TCon (TF TCMul) ts) = sum (map go ts) + 1
go (TCon (TF TCDiv) ts) = sum (map go ts) - 1
go (TCon _ ts) = sum (map go ts)
go _ = 0
-- | Rewrite an equation with respect to a unification variable ?x, into the
-- form `?x = t`. There are two interesting cases to consider (four with
-- symmetry):
--
-- * ?x = ty
-- * expr containing ?x = expr
--
-- In the first case, we just return the type variable and the type, but in the
-- second we try to rewrite the equation until it's in the form of the first
-- case.
tryRewriteEq :: Fins -> TVar -> Type -> Type -> Maybe (TVar,Type)
tryRewriteEq fins uvar l r =
msum [ do guard (uvarTy == l && uvar `Set.notMember` rfvs)
return (uvar, r)
, do guard (uvarTy == r && uvar `Set.notMember` lfvs)
return (uvar, l)
, do guard (uvar `Set.notMember` rfvs)
ty <- rewriteLHS fins uvar l r
return (uvar,ty)
, do guard (uvar `Set.notMember` lfvs)
ty <- rewriteLHS fins uvar r l
return (uvar,ty)
]
where
uvarTy = TVar uvar
lfvs = fvs l
rfvs = fvs r
-- | Check that a type contains only finite type variables.
allFin :: Fins -> Type -> Bool
allFin fins ty = fvs ty `Set.isSubsetOf` fins
-- | Rewrite an equality until the LHS is just `uvar`. Return the rewritten RHS.
--
-- There are a few interesting cases when rewriting the equality:
--
-- A o B = R when `uvar` is only present in A
-- A o B = R when `uvar` is only present in B
--
-- In the first case, as we only consider addition and subtraction, the
-- rewriting will continue on the left, after moving the `B` side to the RHS of
-- the equation. In the second case, if the operation is addition, the `A` side
-- will be moved to the RHS, with rewriting continuing in `B`. However, in the
-- case of subtraction, the `B` side is moved to the RHS, and rewriting
-- continues on the RHS instead.
--
-- In both cases, if the operation is addition, rewriting will only continue if
-- the operand being moved to the RHS is known to be finite. If this check was
-- not done, we would end up violating the well-definedness condition for
-- subtraction (for a, b: well defined (a - b) iff fin b).
rewriteLHS :: Fins -> TVar -> Type -> Type -> Maybe Type
rewriteLHS fins uvar = go
where
go (TVar tv) rhs | tv == uvar = return rhs
go (TCon (TF tf) [x,y]) rhs =
do let xfvs = fvs x
yfvs = fvs y
inX = Set.member uvar xfvs
inY = Set.member uvar yfvs
if | inX && inY -> mzero
| inX -> balanceR x tf y rhs
| inY -> balanceL x tf y rhs
| otherwise -> mzero
-- discard type synonyms, the rewriting will make them no longer apply
go (TUser _ _ l) rhs =
go l rhs
-- records won't work here.
go _ _ =
mzero
-- 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])
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
balanceL _ _ _ _ = mzero
-- guard that the type is finite
--
-- XXX this ignores things like `min x inf` where x is finite, and just
-- assumes that it won't work.
guardFin ty = guard (allFin fins ty)

22
src/Cryptol/TypeCheck/Subst.hs
View File

@ -23,6 +23,7 @@ import Cryptol.TypeCheck.AST
import Cryptol.TypeCheck.PP
import Cryptol.TypeCheck.TypeMap
import Cryptol.Utils.Panic(panic)
import Cryptol.Utils.Misc(anyJust)
data Subst = S { suMap :: Map.Map TVar Type, suDefaulting :: !Bool }
deriving Show
@ -94,6 +95,27 @@ instance FVS Schema where
where bound = Set.fromList (map tpVar as)
-- | Apply a substitution. Returns `Nothing` if nothing changed.
apSubstMaybe :: Subst -> Type -> Maybe Type
apSubstMaybe su ty =
case ty of
TCon t ts -> TCon t `fmap` anyJust (apSubstMaybe su) ts
TUser f ts t -> do t1 <- apSubstMaybe su t
return (TUser f (map (apSubst su) ts) t1)
TRec fs -> TRec `fmap` anyJust fld fs
where fld (x,t) = do t1 <- apSubstMaybe su t
return (x,t1)
TVar x ->
case Map.lookup x (suMap su) of
Just t -> Just $ if suDefaulting su
then apSubst (defaultingSubst emptySubst) t
else t
Nothing -> if suDefaulting su
then Just (defaultFreeVar x)
else Nothing
class TVars t where

1
src/Cryptol/TypeCheck/Unify.hs
View File

@ -6,6 +6,7 @@
-- Stability : provisional
-- Portability : portable
{-# LANGUAGE CPP #-}
{-# LANGUAGE Safe #-}
{-# LANGUAGE PatternGuards, ViewPatterns #-}
{-# LANGUAGE DeriveFunctor #-}

4
src/Cryptol/Utils/PP.hs
View File

@ -227,7 +227,7 @@ fixNameEnv :: NameEnv -> Doc -> Doc
fixNameEnv env (Doc f) = Doc (\_ -> f env)
instance PP ModName where
ppPrec _ (ModName ns) = hcat (punctuate (text "::") (map text ns))
ppPrec _ (ModName ns) = hcat (punctuate (text "::") (map (text . unpack) ns))
instance PP QName where
ppPrec _ qn = withNameEnv $ \ names ->
@ -236,7 +236,7 @@ instance PP QName where
in optParens isInfix (mbNs <> pp n)
instance PP Name where
ppPrec _ (Name x) = text x
ppPrec _ (Name x) = text (unpack x)
-- XXX: This may clash with user-specified names.
ppPrec _ (NewName p x) = text "__" <> passName p <> int x

4
tests/issues/issue058.icry.stdout
View File

@ -8,8 +8,8 @@ Loading module Main
for any type n
fin n
arising from
use of literal or demoted expression
at ./issue058.cry:4:15--4:16
use of expression (!=)
at ./issue058.cry:4:10--4:16
[error] at ./issue058.cry:7:1--7:17:
Failed to validate user-specified signature.
In the definition of 'Main::last', at ./issue058.cry:7:1--7:5:

2
tests/issues/issue198.icry.stdout
View File

@ -15,5 +15,5 @@ Loading module Main
Defaulting type parameter 'bits'
of literal or demoted expression
at ./simon.cry2:89:36--89:38
to max 6 (max (width (a`570 - 1)) (width a`569))
to max 6 (max (width a`569) (width (a`570 - 1)))
True

16
tests/issues/issue226.icry.stdout
View File

@ -13,8 +13,8 @@ Symbols
=======
(!) : {a, b, c} (fin a, fin c) => [a]b -> [c] -> b
(!!) : {a, b, c, d} (fin a, fin d) => [a]b -> [c][d] -> [c]b
(!=) : {a} (Cmp a) => a -> a -> Bool
(!==) : {a, b} (Cmp b) => (a -> b) -> (a -> b) -> a -> Bool
(!=) : {a} (Cmp a) => a -> a -> Bit
(!==) : {a, b} (Cmp b) => (a -> b) -> (a -> b) -> a -> Bit
(#) : {front, back,
a} (fin front) => [front]a -> [back]a -> [front + back]a
(%) : {a} (Arith a) => a -> a -> a
@ -23,14 +23,14 @@ Symbols
(+) : {a} (Arith a) => a -> a -> a
(-) : {a} (Arith a) => a -> a -> a
(/) : {a} (Arith a) => a -> a -> a
(<) : {a} (Cmp a) => a -> a -> Bool
(<) : {a} (Cmp a) => a -> a -> Bit
(<<) : {a, b, c} (fin b) => [a]c -> [b] -> [a]c
(<<<) : {a, b, c} (fin a, fin b) => [a]c -> [b] -> [a]c
(<=) : {a} (Cmp a) => a -> a -> Bool
(==) : {a} (Cmp a) => a -> a -> Bool
(===) : {a, b} (Cmp b) => (a -> b) -> (a -> b) -> a -> Bool
(>) : {a} (Cmp a) => a -> a -> Bool
(>=) : {a} (Cmp a) => a -> a -> Bool
(<=) : {a} (Cmp a) => a -> a -> Bit
(==) : {a} (Cmp a) => a -> a -> Bit
(===) : {a, b} (Cmp b) => (a -> b) -> (a -> b) -> a -> Bit
(>) : {a} (Cmp a) => a -> a -> Bit
(>=) : {a} (Cmp a) => a -> a -> Bit
(>>) : {a, b, c} (fin b) => [a]c -> [b] -> [a]c
(>>>) : {a, b, c} (fin a, fin b) => [a]c -> [b] -> [a]c
(@) : {a, b, c} (fin c) => [a]b -> [c] -> b

4
tests/mono-binds/test03.icry.stdout
View File

@ -9,8 +9,8 @@ test03::test = \{a} (fin a, a >= width a) ->
foo a <> <>
where
/* Not recursive */
foo : {b} (b >= width a, fin b) => [b]
foo = \{b} (b >= width a, fin b) -> Cryptol::demote a b <> <> <>
foo : {b} (fin b, b >= width a) => [b]
foo = \{b} (fin b, b >= width a) -> Cryptol::demote a b <> <> <>