mirror of
https://github.com/GaloisInc/cryptol.git
synced 2024-09-19 01:49:11 +03:00
Merge remote-tracking branch 'origin/master' into literal-class
# Conflicts: # tests/mono-binds/test04.icry.stdout # tests/regression/check01.icry.stdout # tests/regression/check16-tab.icry.stdout # tests/regression/check16.icry.stdout # tests/regression/check21.icry.stdout # tests/regression/check22.icry.stdout
This commit is contained in:
Iavor Diatchki
commit
e579113d05
@ -14,7 +14,14 @@ else
|
||||
TESTS=("$@")
|
||||
fi
|
||||
|
||||
CRY=$(find dist-newstyle -name cryptol -type f)
|
||||
GHC_VERSION=$(ghc --numeric-version)
|
||||
|
||||
if [ ${GHC_VERSION}x == "x" ]; then
|
||||
echo Failed to guess version of GHC.
|
||||
exit 1
|
||||
fi
|
||||
|
||||
CRY=$(find dist-newstyle -name cryptol -type f | grep $GHC_VERSION)
|
||||
|
||||
cabal new-run cryptol-test-runner -- -c $CRY --ignore-expected ${TESTS[*]}
|
||||
|
||||
|
||||
@ -51,7 +51,7 @@ subsumes _ _ = False
|
||||
|
||||
data Warning = DefaultingKind (P.TParam Name) P.Kind
|
||||
| DefaultingWildType P.Kind
|
||||
| DefaultingTo Doc Type
|
||||
| DefaultingTo TVarInfo Type
|
||||
deriving (Show, Generic, NFData)
|
||||
|
||||
-- | Various errors that might happen during type checking/inference
|
||||
@ -208,7 +208,7 @@ instance PP (WithNames Warning) where
|
||||
text "Assuming _ to have" <+> P.cppKind k
|
||||
|
||||
DefaultingTo d ty ->
|
||||
text "Defaulting" <+> d $$ text "to" <+> ppWithNames names ty
|
||||
text "Defaulting" <+> tvarDesc d $$ text "to" <+> ppWithNames names ty
|
||||
|
||||
instance PP (WithNames Error) where
|
||||
ppPrec _ (WithNames err names) =
|
||||
@ -297,7 +297,7 @@ instance PP (WithNames Error) where
|
||||
<+> text "is ambiguous.")
|
||||
$$ text "Arising from:"
|
||||
$$ nest 2 (vcat [ text "*" <+> var v | v <- vs ])
|
||||
where var (TVFree _ _ _ d) = d
|
||||
where var (TVFree _ _ _ d) = tvarDesc d
|
||||
var x = pp x
|
||||
|
||||
UndefinedTypeParameter x ->
|
||||
|
||||
@ -50,7 +50,8 @@ import Control.Monad(when,zipWithM,unless)
|
||||
|
||||
|
||||
inferModule :: P.Module Name -> InferM Module
|
||||
inferModule m = inferModuleK m return
|
||||
inferModule m =
|
||||
do inferModuleK m return
|
||||
|
||||
inferModuleK :: P.Module Name -> (Module -> InferM a) -> InferM a
|
||||
inferModuleK m continue =
|
||||
@ -683,7 +684,7 @@ generalize [] gs0 =
|
||||
|
||||
|
||||
generalize bs0 gs0 =
|
||||
do {- First, we apply the accumulating substituion to the goals
|
||||
do {- First, we apply the accumulating substitution to the goals
|
||||
and the inferred types, to ensure that we have the most up
|
||||
to date information. -}
|
||||
gs <- forM gs0 $ \g -> applySubst g
|
||||
@ -704,11 +705,11 @@ generalize bs0 gs0 =
|
||||
addGoals later -- these ones we keep around for to solve later
|
||||
|
||||
|
||||
{- Figure out what might be ambigious. We count something as
|
||||
{- Figure out what might be ambiguous. We count something as
|
||||
ambiguous if it is to be generalized, but does not appear in
|
||||
the any of the inferred types. Things like that of kind `*`
|
||||
are certainly ambiguous because we don't have any fancy type functions
|
||||
on them. However, things of kind `#` may not actually be mabiguos.
|
||||
on them. However, things of kind `#` may not actually be ambiguous.
|
||||
-}
|
||||
let (maybeAmbig, ambig) = partition ((KNum ==) . kindOf)
|
||||
$ Set.toList
|
||||
@ -718,13 +719,13 @@ generalize bs0 gs0 =
|
||||
|
||||
|
||||
{- See if we might be able to default some of the potentially ambiguous
|
||||
numeric vairables using the constraints that will be part of the
|
||||
numeric variables using the constraints that will be part of the
|
||||
newly generalized schema. Note that we only use the `here0` constrains
|
||||
as these should be the only ones that might mention the potentially
|
||||
ambiguous variable.
|
||||
|
||||
XXX: It is not clear if we should do this, or simply leave the
|
||||
variables as is. After all, they might not actually be ambiugous...
|
||||
variables as is. After all, they might not actually be ambiguous...
|
||||
-}
|
||||
let (as0,here1,defSu,ws) = improveByDefaultingWithPure maybeAmbig here0
|
||||
mapM_ recordWarning ws
|
||||
@ -740,7 +741,7 @@ generalize bs0 gs0 =
|
||||
|
||||
{- Finally, we replace free variables with bound ones, and fix-up
|
||||
the definitions as needed to reflect that we are now working
|
||||
with polymorphic things. For example, apply each occurance to the
|
||||
with polymorphic things. For example, apply each occurrence to the
|
||||
type parameters. -}
|
||||
totSu <- getSubst
|
||||
let
|
||||
@ -758,7 +759,7 @@ generalize bs0 gs0 =
|
||||
return (map genB bs)
|
||||
|
||||
|
||||
-- | Check a monomrphic binding.
|
||||
-- | Check a monomorphic binding.
|
||||
checkMonoB :: P.Bind Name -> Type -> InferM Decl
|
||||
checkMonoB b t =
|
||||
inRangeMb (getLoc b) $
|
||||
@ -803,44 +804,27 @@ checkSigB b (Forall as asmps0 t0, validSchema) = case thing (P.bDef b) of
|
||||
return e1
|
||||
cs <- applySubst cs0
|
||||
|
||||
let letGo qs c = Set.null (qs `Set.intersection` fvs (goal c))
|
||||
let findKeep vs keep todo =
|
||||
let stays (_,cvs) = not $ Set.null $ Set.intersection vs cvs
|
||||
(yes,perhaps) = partition stays todo
|
||||
(stayPs,newVars) = unzip yes
|
||||
in case stayPs of
|
||||
[] -> (keep,map fst todo)
|
||||
_ -> findKeep (Set.unions (vs:newVars)) (stayPs ++ keep) perhaps
|
||||
|
||||
splitPreds qs n ps =
|
||||
let (l,n1) = partition (letGo qs) ps
|
||||
in if null n1
|
||||
then (l,n)
|
||||
else splitPreds (fvs (map goal n1) `Set.union` qs) (n1 ++ n) l
|
||||
let (stay,leave) = findKeep (Set.fromList (map tpVar as)) []
|
||||
[ (c, fvs c) | c <- cs ]
|
||||
|
||||
(later0,now) = splitPreds (Set.fromList (map tpVar as)) [] cs
|
||||
addGoals leave
|
||||
|
||||
asmps1 <- applySubst asmps0
|
||||
|
||||
defSu1 <- proveImplication (Just (thing (P.bName b))) as asmps1 now
|
||||
let later = apSubst defSu1 later0
|
||||
asmps = apSubst defSu1 asmps1
|
||||
su <- proveImplication (Just (thing (P.bName b))) as asmps1 stay
|
||||
extendSubst su
|
||||
|
||||
-- Now we check for any remaining variables that are not mentioned
|
||||
-- in the environment. The plan is to try to default these to something
|
||||
-- reasonable.
|
||||
do let laterVs = fvs (map goal later)
|
||||
asmpVs <- varsWithAsmps
|
||||
let genVs = laterVs `Set.difference` asmpVs
|
||||
(maybeAmbig,ambig) = partition ((== KNum) . kindOf)
|
||||
(Set.toList genVs)
|
||||
when (not (null ambig)) $ recordError
|
||||
$ AmbiguousType [ thing (P.bName b) ] ambig
|
||||
|
||||
-- XXX: Uhm, why are we defaulting that 'later' things here?
|
||||
-- Surely this should be done later, when we solve them?
|
||||
let (_,newGs,defSu2,ws) = improveByDefaultingWithPure maybeAmbig later
|
||||
mapM_ recordWarning ws
|
||||
extendSubst defSu2
|
||||
addGoals newGs
|
||||
|
||||
su <- getSubst
|
||||
let su' = defSu1 @@ su
|
||||
t = apSubst su' t0
|
||||
e2 = apSubst su' e1
|
||||
let asmps = apSubst su asmps1
|
||||
t <- applySubst t0
|
||||
e2 <- applySubst e1
|
||||
|
||||
return Decl
|
||||
{ dName = thing (P.bName b)
|
||||
|
||||
@ -233,7 +233,7 @@ addTVarsDescs nm t d
|
||||
| otherwise = d $$ text "where" $$ vcat (map desc (Set.toList vs))
|
||||
where
|
||||
vs = Set.filter isFreeTV (fvs t)
|
||||
desc v@(TVFree _ _ _ x) = ppWithNames nm v <+> text "is" <+> x
|
||||
desc v@(TVFree _ _ _ x) = ppWithNames nm v <+> text "is" <+> tvarDesc x
|
||||
desc (TVBound {}) = empty
|
||||
|
||||
|
||||
|
||||
@ -23,7 +23,8 @@ import Cryptol.TypeCheck.AST
|
||||
import Cryptol.TypeCheck.Subst
|
||||
import Cryptol.TypeCheck.Unify(mgu, Result(..), UnificationError(..))
|
||||
import Cryptol.TypeCheck.InferTypes
|
||||
import Cryptol.TypeCheck.Error(Warning,Error(..),cleanupErrors)
|
||||
import Cryptol.TypeCheck.Error(Warning(..),Error(..),cleanupErrors)
|
||||
import Cryptol.TypeCheck.PP (brackets, commaSep)
|
||||
import qualified Cryptol.TypeCheck.SimpleSolver as Simple
|
||||
import qualified Cryptol.TypeCheck.Solver.SMT as SMT
|
||||
import Cryptol.Utils.PP(pp, ($$), (<+>), Doc, text, quotes)
|
||||
@ -309,7 +310,9 @@ recordError e =
|
||||
|
||||
recordWarning :: Warning -> InferM ()
|
||||
recordWarning w =
|
||||
do r <- curRange
|
||||
do r <- case w of
|
||||
DefaultingTo d _ -> return (tvarSource d)
|
||||
_ -> curRange
|
||||
IM $ sets_ $ \s -> s { iWarnings = (r,w) : iWarnings s }
|
||||
|
||||
getSolver :: InferM SMT.Solver
|
||||
@ -443,7 +446,8 @@ newTVar' src extraBound k =
|
||||
do r <- curRange
|
||||
bound <- getBoundInScope
|
||||
let vs = Set.union extraBound bound
|
||||
msg = src $$ text "at" <+> pp r
|
||||
msg = TVarInfo { tvarDesc = src $$ text "at" <+> pp r
|
||||
, tvarSource = r }
|
||||
newName $ \s -> let x = seedTVar s
|
||||
in (TVFree x k vs msg, s { seedTVar = x + 1 })
|
||||
|
||||
@ -501,7 +505,21 @@ getSubst = IM $ fmap iSubst get
|
||||
|
||||
-- | Add to the accumulated substitution.
|
||||
extendSubst :: Subst -> InferM ()
|
||||
extendSubst su = IM $ sets_ $ \s -> s { iSubst = su @@ iSubst s }
|
||||
extendSubst su =
|
||||
do IM $ sets_ $ \s -> s { iSubst = su @@ iSubst s }
|
||||
bound <- getBoundInScope
|
||||
let suBound = Set.filter isBoundTV (Set.unions (map (fvs . snd) (substToList su)))
|
||||
let escaped = Set.difference suBound bound
|
||||
if Set.null escaped then return () else
|
||||
panic "Cryptol.TypeCheck.Monad.extendSubst"
|
||||
[ "Escaped quantified variables:"
|
||||
, "Substitution: " ++ show (brackets (commaSep (map ppBinding su_binds)))
|
||||
, "Vars in scope: " ++ show (brackets (commaSep (map pp (Set.toList bound))))
|
||||
, "Escaped: " ++ show (brackets (commaSep (map pp (Set.toList escaped))))
|
||||
]
|
||||
where
|
||||
su_binds = substToList su
|
||||
ppBinding (v,x) = pp v <+> text ":=" <+> pp x
|
||||
|
||||
|
||||
-- | Variables that are either mentioned in the environment or in
|
||||
@ -603,6 +621,7 @@ getParamFuns = IM $ asks iParamFuns
|
||||
getParamTypes :: InferM (Map Name ModTParam)
|
||||
getParamTypes = IM $ asks iParamTypes
|
||||
|
||||
-- | Constraints on the module's parameters.
|
||||
getParamConstraints :: InferM [Located Prop]
|
||||
getParamConstraints = IM $ asks iParamConstraints
|
||||
|
||||
|
||||
@ -20,7 +20,7 @@ module Cryptol.TypeCheck.Solve
|
||||
) where
|
||||
|
||||
import Cryptol.Parser.Position(thing)
|
||||
import Cryptol.TypeCheck.PP(pp)
|
||||
import Cryptol.TypeCheck.PP -- (pp)
|
||||
import Cryptol.TypeCheck.AST
|
||||
import Cryptol.TypeCheck.Monad
|
||||
import Cryptol.TypeCheck.Default
|
||||
@ -182,16 +182,21 @@ simpHasGoals = go False [] =<< getHasGoals
|
||||
-- on the module's type parameters.
|
||||
proveModuleTopLevel :: InferM ()
|
||||
proveModuleTopLevel =
|
||||
do -- io $ putStrLn "Module top level"
|
||||
simplifyAllConstraints
|
||||
do simplifyAllConstraints
|
||||
gs <- getGoals
|
||||
let vs = Set.toList (Set.filter isFreeTV (fvs gs))
|
||||
(_,gs1,su1,ws) = improveByDefaultingWithPure vs gs
|
||||
extendSubst su1
|
||||
mapM_ recordWarning ws
|
||||
|
||||
cs <- getParamConstraints
|
||||
case cs of
|
||||
[] -> return ()
|
||||
_ -> do gs <- getGoals
|
||||
su <- proveImplication Nothing [] [] gs
|
||||
extendSubst su
|
||||
|
||||
[] -> addGoals gs1
|
||||
_ -> do su2 <- proveImplication Nothing [] [] gs1
|
||||
extendSubst su2
|
||||
|
||||
-- | Prove an implication, and return any improvements that we computed.
|
||||
-- Records errors, if any of the goals couldn't be solved.
|
||||
proveImplication :: Maybe Name -> [TParam] -> [Prop] -> [Goal] -> InferM Subst
|
||||
proveImplication lnam as ps gs =
|
||||
do evars <- varsWithAsmps
|
||||
@ -232,7 +237,8 @@ proveImplicationIO s f varsInEnv ps asmps0 gs0 =
|
||||
$ Set.difference (fvs (map goal gs3)) varsInEnv
|
||||
case improveByDefaultingWithPure free gs3 of
|
||||
(_,_,newSu,_)
|
||||
| isEmptySubst newSu -> return (err gs3, su) -- XXX: Old?
|
||||
| isEmptySubst newSu ->
|
||||
return (err gs3, su) -- XXX: Old?
|
||||
(_,newGs,newSu,ws) ->
|
||||
do let su1 = newSu @@ su
|
||||
(res1,su2) <- proveImplicationIO s f varsInEnv ps
|
||||
|
||||
@ -16,6 +16,7 @@ import Data.List(sortBy)
|
||||
import Data.Ord(comparing)
|
||||
|
||||
import Cryptol.Parser.Selector
|
||||
import Cryptol.Parser.Position(Range)
|
||||
import Cryptol.ModuleSystem.Name
|
||||
import Cryptol.Prims.Syntax
|
||||
import Cryptol.Utils.Ident (Ident)
|
||||
@ -112,14 +113,19 @@ data Type = TCon !TCon ![Type]
|
||||
|
||||
|
||||
-- | Type variables.
|
||||
data TVar = TVFree !Int Kind (Set TVar) Doc
|
||||
data TVar = TVFree !Int Kind (Set TVar) TVarInfo
|
||||
-- ^ Unique, kind, ids of bound type variables that are in scope
|
||||
-- The `Doc` is a description of how this type came to be.
|
||||
-- The last field gives us some infor for nicer warnings/errors.
|
||||
|
||||
|
||||
| TVBound {-# UNPACK #-} !TParam
|
||||
deriving (Show, Generic, NFData)
|
||||
|
||||
data TVarInfo = TVarInfo { tvarSource :: Range -- ^ Source code that gave rise
|
||||
, tvarDesc :: Doc -- ^ Description
|
||||
}
|
||||
deriving (Show, Generic, NFData)
|
||||
|
||||
|
||||
-- | The type is supposed to be of kind `KProp`
|
||||
type Prop = Type
|
||||
|
||||
@ -1,7 +1,7 @@
|
||||
Loading module Cryptol
|
||||
Loading module Cryptol
|
||||
Loading module Main
|
||||
[warning] at ./issue268.cry:2:1--2:74:
|
||||
[warning] at ./issue268.cry:2:61--2:65:
|
||||
Defaulting 2nd type parameter
|
||||
of expression drop
|
||||
at ./issue268.cry:2:61--2:65
|
||||
|
||||
@ -4,9 +4,9 @@ Loading module test04
|
||||
module test04
|
||||
import Cryptol
|
||||
/* Not recursive */
|
||||
test04::test : {a, b} (Literal 10 b) => a -> ((a, ()), (a, b))
|
||||
test04::test = \{a, b} (Literal 10 b) (a : a) ->
|
||||
(test04::f () (), test04::f b (Cryptol::demote 10 b <>))
|
||||
test04::test : {a, b} (b >= 4, fin b) => a -> ((a, ()), (a, [b]))
|
||||
test04::test = \{a, b} (b >= 4, fin b) (a : a) ->
|
||||
(test04::f () (), test04::f [b] (Cryptol::demote 10 b <> <>))
|
||||
where
|
||||
/* Not recursive */
|
||||
test04::f : {c} c -> (a, c)
|
||||
@ -16,10 +16,17 @@ test04::test = \{a, b} (Literal 10 b) (a : a) ->
|
||||
|
||||
Loading module Cryptol
|
||||
Loading module test04
|
||||
[warning] at ./test04.cry:3:19--3:21:
|
||||
Defaulting type parameter 'bits'
|
||||
of literal or demoted expression
|
||||
at ./test04.cry:3:19--3:21
|
||||
to 4
|
||||
|
||||
[error] at ./test04.cry:3:19--3:21:
|
||||
Unsolved constraints:
|
||||
Literal 10 ()
|
||||
arising from
|
||||
use of literal or demoted expression
|
||||
at ./test04.cry:3:19--3:21
|
||||
Type mismatch:
|
||||
Expected type: ()
|
||||
Inferred type: [?p33]
|
||||
where
|
||||
?p33 is type parameter 'bits'
|
||||
of literal or demoted expression
|
||||
at ./test04.cry:3:19--3:21
|
||||
|
||||
@ -48,7 +48,7 @@ Loading module test05
|
||||
[warning] at ./test05.cry:13:5--13:8
|
||||
This binding for foo shadows the existing binding from
|
||||
(at ./test05.cry:9:3--9:6, foo)
|
||||
[warning] at ./test05.cry:1:1--14:21:
|
||||
[warning] at ./test05.cry:14:11--14:21:
|
||||
Defaulting 1st type parameter
|
||||
of expression (#)
|
||||
at ./test05.cry:14:11--14:21
|
||||
|
||||
@ -1,12 +1,12 @@
|
||||
Loading module Cryptol
|
||||
Loading module Cryptol
|
||||
Loading module Main
|
||||
[warning] at :1:1--3:23:
|
||||
[warning] at ./unary-2.cry:3:22--3:23:
|
||||
Defaulting type parameter 'bits'
|
||||
of literal or demoted expression
|
||||
at ./unary-2.cry:3:22--3:23
|
||||
to 2
|
||||
[warning] at :1:1--3:23:
|
||||
[warning] at ./unary-2.cry:2:22--2:23:
|
||||
Defaulting type parameter 'bits'
|
||||
of literal or demoted expression
|
||||
at ./unary-2.cry:2:22--2:23
|
||||
|
||||
@ -1,31 +1,31 @@
|
||||
Loading module Cryptol
|
||||
Loading module Cryptol
|
||||
Loading module AES
|
||||
[warning] at ./AES.cry:147:1--150:39:
|
||||
Defaulting type parameter 'bits'
|
||||
of finite enumeration
|
||||
at ./AES.cry:147:36--147:51
|
||||
to 4
|
||||
[warning] at ./AES.cry:147:1--150:39:
|
||||
Defaulting type parameter 'bits'
|
||||
of literal or demoted expression
|
||||
at ./AES.cry:147:60--147:63
|
||||
to 4
|
||||
[warning] at ./AES.cry:124:1--129:31:
|
||||
Defaulting type parameter 'bits'
|
||||
of literal or demoted expression
|
||||
at ./AES.cry:127:32--127:33
|
||||
to 3
|
||||
[warning] at ./AES.cry:91:1--93:23:
|
||||
Defaulting type parameter 'bits'
|
||||
of finite enumeration
|
||||
at ./AES.cry:92:61--92:69
|
||||
to 2
|
||||
[warning] at ./AES.cry:86:1--88:20:
|
||||
[warning] at ./AES.cry:87:58--87:66:
|
||||
Defaulting type parameter 'bits'
|
||||
of finite enumeration
|
||||
at ./AES.cry:87:58--87:66
|
||||
to 2
|
||||
[warning] at ./AES.cry:92:61--92:69:
|
||||
Defaulting type parameter 'bits'
|
||||
of finite enumeration
|
||||
at ./AES.cry:92:61--92:69
|
||||
to 2
|
||||
[warning] at ./AES.cry:127:32--127:33:
|
||||
Defaulting type parameter 'bits'
|
||||
of literal or demoted expression
|
||||
at ./AES.cry:127:32--127:33
|
||||
to 3
|
||||
[warning] at ./AES.cry:147:36--147:51:
|
||||
Defaulting type parameter 'bits'
|
||||
of finite enumeration
|
||||
at ./AES.cry:147:36--147:51
|
||||
to 4
|
||||
[warning] at ./AES.cry:147:60--147:63:
|
||||
Defaulting type parameter 'bits'
|
||||
of literal or demoted expression
|
||||
at ./AES.cry:147:60--147:63
|
||||
to 4
|
||||
True
|
||||
True
|
||||
True
|
||||
|
||||
@ -1,10 +1,10 @@
|
||||
Loading module Cryptol
|
||||
Loading module Cryptol
|
||||
Loading module Main
|
||||
[warning] at ./check01.cry:2:1--2:27:
|
||||
Defaulting 4th type parameter
|
||||
of expression (@@)
|
||||
at ./check01.cry:2:5--2:27
|
||||
to max (width 19) (width 6)
|
||||
[warning] at ./check01.cry:2:24--2:26:
|
||||
Defaulting type parameter 'bits'
|
||||
of literal or demoted expression
|
||||
at ./check01.cry:2:24--2:26
|
||||
to 5
|
||||
[0x00000007, 0x00000014]
|
||||
True
|
||||
|
||||
@ -1,12 +1,12 @@
|
||||
Loading module Cryptol
|
||||
Loading module Cryptol
|
||||
Loading module Main
|
||||
[warning] at :1:1--3:25:
|
||||
[warning] at ./check02.cry:3:24--3:25:
|
||||
Defaulting type parameter 'bits'
|
||||
of literal or demoted expression
|
||||
at ./check02.cry:3:24--3:25
|
||||
to 1
|
||||
[warning] at <interactive>:1:1--1:18:
|
||||
[warning] at <interactive>:1:9--1:18:
|
||||
Defaulting type parameter 'bits'
|
||||
of finite enumeration
|
||||
at <interactive>:1:9--1:18
|
||||
|
||||
@ -1,7 +1,7 @@
|
||||
Loading module Cryptol
|
||||
Loading module Cryptol
|
||||
Loading module Main
|
||||
[warning] at <interactive>:1:1--1:22:
|
||||
[warning] at <interactive>:1:11--1:22:
|
||||
Defaulting type parameter 'bits'
|
||||
of finite enumeration
|
||||
at <interactive>:1:11--1:22
|
||||
@ -9,7 +9,7 @@ Loading module Main
|
||||
[0x00000000, 0x00000001, 0x00000002, 0x00000003, 0x00000004,
|
||||
0x00000005, 0x00000006, 0x00000007, 0x00000008, 0x00000009,
|
||||
0x0000000a]
|
||||
[warning] at <interactive>:1:1--1:23:
|
||||
[warning] at <interactive>:1:12--1:23:
|
||||
Defaulting type parameter 'bits'
|
||||
of finite enumeration
|
||||
at <interactive>:1:12--1:23
|
||||
|
||||
@ -1,17 +1,17 @@
|
||||
Loading module Cryptol
|
||||
Loading module Cryptol
|
||||
Loading module Main
|
||||
[warning] at :1:1--4:45:
|
||||
[warning] at ./check04.cry:4:21--4:29:
|
||||
Defaulting type parameter 'bits'
|
||||
of finite enumeration
|
||||
at ./check04.cry:4:21--4:29
|
||||
to 2
|
||||
[warning] at :1:1--4:45:
|
||||
[warning] at ./check04.cry:4:43--4:44:
|
||||
Defaulting type parameter 'bits'
|
||||
of literal or demoted expression
|
||||
at ./check04.cry:4:43--4:44
|
||||
to 2
|
||||
[warning] at <interactive>:1:1--1:21:
|
||||
[warning] at <interactive>:1:12--1:21:
|
||||
Defaulting type parameter 'bits'
|
||||
of finite enumeration
|
||||
at <interactive>:1:12--1:21
|
||||
|
||||
@ -1,17 +1,17 @@
|
||||
Loading module Cryptol
|
||||
Loading module Cryptol
|
||||
Loading module Main
|
||||
[warning] at :1:1--4:45:
|
||||
[warning] at ./check05.cry:4:21--4:29:
|
||||
Defaulting type parameter 'bits'
|
||||
of finite enumeration
|
||||
at ./check05.cry:4:21--4:29
|
||||
to 2
|
||||
[warning] at :1:1--4:45:
|
||||
[warning] at ./check05.cry:4:43--4:44:
|
||||
Defaulting type parameter 'bits'
|
||||
of literal or demoted expression
|
||||
at ./check05.cry:4:43--4:44
|
||||
to 2
|
||||
[warning] at <interactive>:1:1--1:21:
|
||||
[warning] at <interactive>:1:12--1:21:
|
||||
Defaulting type parameter 'bits'
|
||||
of finite enumeration
|
||||
at <interactive>:1:12--1:21
|
||||
|
||||
@ -1,17 +1,17 @@
|
||||
Loading module Cryptol
|
||||
Loading module Cryptol
|
||||
Loading module Main
|
||||
[warning] at :1:1--5:70:
|
||||
[warning] at ./check06.cry:5:24--5:32:
|
||||
Defaulting type parameter 'bits'
|
||||
of finite enumeration
|
||||
at ./check06.cry:5:24--5:32
|
||||
to 2
|
||||
[warning] at :1:1--5:70:
|
||||
[warning] at ./check06.cry:5:66--5:67:
|
||||
Defaulting type parameter 'bits'
|
||||
of literal or demoted expression
|
||||
at ./check06.cry:5:66--5:67
|
||||
to 2
|
||||
[warning] at <interactive>:1:1--1:24:
|
||||
[warning] at <interactive>:1:15--1:24:
|
||||
Defaulting type parameter 'bits'
|
||||
of finite enumeration
|
||||
at <interactive>:1:15--1:24
|
||||
|
||||
@ -1,42 +1,42 @@
|
||||
Loading module Cryptol
|
||||
Loading module Cryptol
|
||||
Loading module Main
|
||||
[warning] at :1:1--14:39:
|
||||
Defaulting type parameter 'bits'
|
||||
of literal or demoted expression
|
||||
at ./check07.cry:13:21--13:22
|
||||
to 1
|
||||
[warning] at :1:1--14:39:
|
||||
Defaulting type parameter 'bits'
|
||||
of finite enumeration
|
||||
at ./check07.cry:11:39--11:51
|
||||
to 4
|
||||
[warning] at ./check07.cry:7:1--7:56:
|
||||
[warning] at ./check07.cry:7:43--7:54:
|
||||
Defaulting type parameter 'bits'
|
||||
of finite enumeration
|
||||
at ./check07.cry:7:43--7:54
|
||||
to 6
|
||||
[warning] at :1:1--14:39:
|
||||
[warning] at ./check07.cry:13:21--13:22:
|
||||
Defaulting type parameter 'bits'
|
||||
of literal or demoted expression
|
||||
at ./check07.cry:13:21--13:22
|
||||
to 1
|
||||
[warning] at ./check07.cry:11:39--11:51:
|
||||
Defaulting type parameter 'bits'
|
||||
of finite enumeration
|
||||
at ./check07.cry:11:39--11:51
|
||||
to 4
|
||||
[warning] at ./check07.cry:5:37--5:49:
|
||||
Defaulting type parameter 'bits'
|
||||
of finite enumeration
|
||||
at ./check07.cry:5:37--5:49
|
||||
to 7
|
||||
[warning] at :1:1--14:39:
|
||||
[warning] at ./check07.cry:4:37--4:48:
|
||||
Defaulting type parameter 'bits'
|
||||
of finite enumeration
|
||||
at ./check07.cry:4:37--4:48
|
||||
to 6
|
||||
[warning] at :1:1--14:39:
|
||||
[warning] at ./check07.cry:3:37--3:65:
|
||||
Defaulting type parameter 'bits'
|
||||
of finite enumeration
|
||||
at ./check07.cry:3:37--3:65
|
||||
to 32
|
||||
[warning] at :1:1--14:39:
|
||||
[warning] at ./check07.cry:2:37--2:49:
|
||||
Defaulting type parameter 'bits'
|
||||
of finite enumeration
|
||||
at ./check07.cry:2:37--2:49
|
||||
to 7
|
||||
[warning] at :1:1--14:39:
|
||||
[warning] at ./check07.cry:1:37--1:48:
|
||||
Defaulting type parameter 'bits'
|
||||
of finite enumeration
|
||||
at ./check07.cry:1:37--1:48
|
||||
|
||||
@ -1,17 +1,17 @@
|
||||
Loading module Cryptol
|
||||
Loading module Cryptol
|
||||
Loading module Main
|
||||
[warning] at :1:1--7:45:
|
||||
[warning] at ./check08.cry:9:25--9:33:
|
||||
Defaulting type parameter 'bits'
|
||||
of finite enumeration
|
||||
at ./check08.cry:9:25--9:33
|
||||
to 3
|
||||
[warning] at :1:1--7:45:
|
||||
[warning] at ./check08.cry:7:16--7:24:
|
||||
Defaulting type parameter 'bits'
|
||||
of finite enumeration
|
||||
at ./check08.cry:7:16--7:24
|
||||
to 3
|
||||
[warning] at <interactive>:1:1--1:15:
|
||||
[warning] at <interactive>:1:7--1:15:
|
||||
Defaulting type parameter 'bits'
|
||||
of finite enumeration
|
||||
at <interactive>:1:7--1:15
|
||||
|
||||
@ -13,28 +13,28 @@ Loading module Main
|
||||
[warning] at ./check09.cry:23:5--23:7
|
||||
This binding for ss shadows the existing binding from
|
||||
(at ./check09.cry:5:1--5:3, ss)
|
||||
[warning] at ./check09.cry:17:1--30:54:
|
||||
[warning] at ./check09.cry:17:18--17:28:
|
||||
Defaulting type parameter 'bits'
|
||||
of finite enumeration
|
||||
at ./check09.cry:17:18--17:28
|
||||
to 3
|
||||
[warning] at :1:1--37:28:
|
||||
[warning] at ./check09.cry:13:18--13:26:
|
||||
Defaulting type parameter 'bits'
|
||||
of finite enumeration
|
||||
at ./check09.cry:13:18--13:26
|
||||
to 2
|
||||
[warning] at :1:1--37:28:
|
||||
[warning] at ./check09.cry:14:18--14:26:
|
||||
Defaulting type parameter 'bits'
|
||||
of finite enumeration
|
||||
at ./check09.cry:14:18--14:26
|
||||
to 2
|
||||
[warning] at <interactive>:1:1--1:15:
|
||||
[warning] at <interactive>:1:7--1:15:
|
||||
Defaulting type parameter 'bits'
|
||||
of finite enumeration
|
||||
at <interactive>:1:7--1:15
|
||||
to 2
|
||||
[0x00000008, 0x00004080, 0x00068c00, 0x00a22800]
|
||||
[warning] at <interactive>:1:1--1:15:
|
||||
[warning] at <interactive>:1:7--1:15:
|
||||
Defaulting type parameter 'bits'
|
||||
of finite enumeration
|
||||
at <interactive>:1:7--1:15
|
||||
|
||||
@ -1,12 +1,12 @@
|
||||
Loading module Cryptol
|
||||
Loading module Cryptol
|
||||
Loading module Main
|
||||
[warning] at :1:1--5:25:
|
||||
[warning] at ./check11.cry:3:10--3:19:
|
||||
Defaulting type parameter 'bits'
|
||||
of finite enumeration
|
||||
at ./check11.cry:3:10--3:19
|
||||
to 7
|
||||
[warning] at :1:1--5:25:
|
||||
[warning] at ./check11.cry:5:16--5:25:
|
||||
Defaulting type parameter 'bits'
|
||||
of finite enumeration
|
||||
at ./check11.cry:5:16--5:25
|
||||
|
||||
@ -1,7 +1,7 @@
|
||||
Loading module Cryptol
|
||||
Loading module Cryptol
|
||||
Loading module Main
|
||||
[warning] at :1:1--5:76:
|
||||
[warning] at ./check14.cry:5:73--5:74:
|
||||
Defaulting type parameter 'bits'
|
||||
of literal or demoted expression
|
||||
at ./check14.cry:5:73--5:74
|
||||
|
||||
@ -1,9 +1,9 @@
|
||||
Loading module Cryptol
|
||||
Loading module Cryptol
|
||||
Loading module Main
|
||||
[warning] at :1:1--4:17:
|
||||
Defaulting 1st type parameter
|
||||
of expression width
|
||||
at ./check16-tab.cry:1:11--1:16
|
||||
to max 4 (width 8)
|
||||
[warning] at ./check16-tab.cry:1:22--1:23:
|
||||
Defaulting type parameter 'bits'
|
||||
of literal or demoted expression
|
||||
at ./check16-tab.cry:1:22--1:23
|
||||
to 4
|
||||
True
|
||||
|
||||
@ -1,9 +1,9 @@
|
||||
Loading module Cryptol
|
||||
Loading module Cryptol
|
||||
Loading module Main
|
||||
[warning] at :1:1--4:13:
|
||||
Defaulting 1st type parameter
|
||||
of expression width
|
||||
at ./check16.cry:1:11--1:16
|
||||
to max 4 (width 8)
|
||||
[warning] at ./check16.cry:1:22--1:23:
|
||||
Defaulting type parameter 'bits'
|
||||
of literal or demoted expression
|
||||
at ./check16.cry:1:22--1:23
|
||||
to 4
|
||||
True
|
||||
|
||||
@ -1,7 +1,7 @@
|
||||
Loading module Cryptol
|
||||
Loading module Cryptol
|
||||
Loading module Main
|
||||
[warning] at :1:1--3:39:
|
||||
[warning] at ./check20.cry:3:31--3:33:
|
||||
Defaulting type parameter 'bits'
|
||||
of literal or demoted expression
|
||||
at ./check20.cry:3:31--3:33
|
||||
|
||||
@ -1,9 +1,9 @@
|
||||
Loading module Cryptol
|
||||
Loading module Cryptol
|
||||
Loading module Main
|
||||
[warning] at :1:1--7:63:
|
||||
Defaulting 1st type parameter
|
||||
of expression width
|
||||
at ./check21.cry:4:21--4:26
|
||||
to max 4 (width 1)
|
||||
[warning] at ./check21.cry:4:31--4:32:
|
||||
Defaulting type parameter 'bits'
|
||||
of literal or demoted expression
|
||||
at ./check21.cry:4:31--4:32
|
||||
to 4
|
||||
True
|
||||
|
||||
@ -1,9 +1,9 @@
|
||||
Loading module Cryptol
|
||||
Loading module Cryptol
|
||||
Loading module Main
|
||||
[warning] at :1:1--12:70:
|
||||
Defaulting 1st type parameter
|
||||
of expression width
|
||||
at ./check22.cry:3:21--3:26
|
||||
to max 4 (width 1)
|
||||
[warning] at ./check22.cry:3:31--3:32:
|
||||
Defaulting type parameter 'bits'
|
||||
of literal or demoted expression
|
||||
at ./check22.cry:3:31--3:32
|
||||
to 4
|
||||
True
|
||||
|
||||
@ -1,7 +1,7 @@
|
||||
Loading module Cryptol
|
||||
Loading module Cryptol
|
||||
Loading module Main
|
||||
[warning] at :1:1--4:82:
|
||||
[warning] at ./check24.cry:4:60--4:71:
|
||||
Defaulting type parameter 'bits'
|
||||
of finite enumeration
|
||||
at ./check24.cry:4:60--4:71
|
||||
|
||||
@ -4,12 +4,12 @@ Loading module check25
|
||||
[warning] at ./check25.cry:6:9--6:11
|
||||
This binding for tz shadows the existing binding from
|
||||
(at ./check25.cry:3:1--3:3, tz)
|
||||
[warning] at ./check25.cry:1:1--8:19:
|
||||
[warning] at ./check25.cry:8:17--8:19:
|
||||
Defaulting type parameter 'bits'
|
||||
of literal or demoted expression
|
||||
at ./check25.cry:8:17--8:19
|
||||
to 4
|
||||
[warning] at ./check25.cry:1:1--8:19:
|
||||
[warning] at ./check25.cry:6:14--6:16:
|
||||
Defaulting type parameter 'bits'
|
||||
of literal or demoted expression
|
||||
at ./check25.cry:6:14--6:16
|
||||
|
||||
@ -1,72 +1,72 @@
|
||||
Loading module Cryptol
|
||||
Loading module Cryptol
|
||||
Loading module Main
|
||||
[warning] at :1:1--13:43:
|
||||
[warning] at ./check26.cry:11:42--11:45:
|
||||
Defaulting 2nd type parameter
|
||||
of expression Main::xys
|
||||
at ./check26.cry:11:42--11:45
|
||||
to 4
|
||||
[warning] at :1:1--13:43:
|
||||
[warning] at ./check26.cry:8:31--8:34:
|
||||
Defaulting 2nd type parameter
|
||||
of expression Main::xys
|
||||
at ./check26.cry:8:31--8:34
|
||||
to 3
|
||||
[warning] at :1:1--13:43:
|
||||
[warning] at ./check26.cry:9:23--9:34:
|
||||
Defaulting type parameter 'bits'
|
||||
of finite enumeration
|
||||
at ./check26.cry:9:23--9:34
|
||||
to 4
|
||||
[warning] at :1:1--13:43:
|
||||
[warning] at ./check26.cry:9:41--9:51:
|
||||
Defaulting type parameter 'bits'
|
||||
of finite enumeration
|
||||
at ./check26.cry:9:41--9:51
|
||||
to 3
|
||||
[warning] at :1:1--13:43:
|
||||
[warning] at ./check26.cry:4:17--4:19:
|
||||
Defaulting 1st type parameter
|
||||
of expression Main::xy
|
||||
at ./check26.cry:4:17--4:19
|
||||
to 4
|
||||
[warning] at :1:1--13:43:
|
||||
[warning] at ./check26.cry:4:17--4:19:
|
||||
Defaulting 2nd type parameter
|
||||
of expression Main::xy
|
||||
at ./check26.cry:4:17--4:19
|
||||
to 5
|
||||
[warning] at :1:1--13:43:
|
||||
[warning] at ./check26.cry:4:23--4:25:
|
||||
Defaulting 2nd type parameter
|
||||
of expression Main::xy
|
||||
at ./check26.cry:4:23--4:25
|
||||
to 5
|
||||
[warning] at :1:1--13:43:
|
||||
[warning] at ./check26.cry:4:37--4:39:
|
||||
Defaulting 1st type parameter
|
||||
of expression Main::xy
|
||||
at ./check26.cry:4:37--4:39
|
||||
to 4
|
||||
[warning] at :1:1--13:43:
|
||||
[warning] at ./check26.cry:4:37--4:39:
|
||||
Defaulting 2nd type parameter
|
||||
of expression Main::xy
|
||||
at ./check26.cry:4:37--4:39
|
||||
to 5
|
||||
[warning] at :1:1--13:43:
|
||||
[warning] at ./check26.cry:4:43--4:45:
|
||||
Defaulting 1st type parameter
|
||||
of expression Main::xy
|
||||
at ./check26.cry:4:43--4:45
|
||||
to 4
|
||||
[warning] at :1:1--13:43:
|
||||
[warning] at ./check26.cry:5:17--5:19:
|
||||
Defaulting 2nd type parameter
|
||||
of expression Main::xy
|
||||
at ./check26.cry:5:17--5:19
|
||||
to 5
|
||||
[warning] at :1:1--13:43:
|
||||
[warning] at ./check26.cry:5:23--5:25:
|
||||
Defaulting type parameter 'bits'
|
||||
of literal or demoted expression
|
||||
at ./check26.cry:5:23--5:25
|
||||
to 4
|
||||
[warning] at :1:1--13:43:
|
||||
[warning] at ./check26.cry:5:35--5:37:
|
||||
Defaulting 1st type parameter
|
||||
of expression Main::xy
|
||||
at ./check26.cry:5:35--5:37
|
||||
to 4
|
||||
[warning] at :1:1--13:43:
|
||||
[warning] at ./check26.cry:5:41--5:43:
|
||||
Defaulting type parameter 'bits'
|
||||
of literal or demoted expression
|
||||
at ./check26.cry:5:41--5:43
|
||||
|
||||
@ -1,7 +1,7 @@
|
||||
Loading module Cryptol
|
||||
Loading module Cryptol
|
||||
Loading module Main
|
||||
[warning] at :1:1--2:42:
|
||||
[warning] at ./check28.cry:2:29--2:31:
|
||||
Defaulting 2nd type parameter
|
||||
of expression Main::xs
|
||||
at ./check28.cry:2:29--2:31
|
||||
|
||||
@ -6,14 +6,14 @@ Assuming a = 2
|
||||
Assuming a = 1
|
||||
Assuming b = 2
|
||||
{x = 0x1, y = 0x2}
|
||||
[warning] at <interactive>:1:1--1:22:
|
||||
[warning] at <interactive>:1:20--1:21:
|
||||
Defaulting type parameter 'bits'
|
||||
of literal or demoted expression
|
||||
at <interactive>:1:20--1:21
|
||||
to 2
|
||||
Assuming a = 1
|
||||
0x1
|
||||
[warning] at <interactive>:1:1--1:46:
|
||||
[warning] at <interactive>:1:42--1:44:
|
||||
Defaulting type parameter 'bits'
|
||||
of literal or demoted expression
|
||||
at <interactive>:1:42--1:44
|
||||
|
||||
@ -1,25 +1,25 @@
|
||||
Loading module Cryptol
|
||||
Loading module Cryptol
|
||||
Loading module Main
|
||||
[warning] at <interactive>:1:1--1:42:
|
||||
[warning] at <interactive>:1:11--1:19:
|
||||
Defaulting type parameter 'bits'
|
||||
of finite enumeration
|
||||
at <interactive>:1:11--1:19
|
||||
to max 4 (width 10)
|
||||
True
|
||||
[warning] at <interactive>:1:1--1:43:
|
||||
[warning] at <interactive>:1:11--1:20:
|
||||
Defaulting type parameter 'bits'
|
||||
of finite enumeration
|
||||
at <interactive>:1:11--1:20
|
||||
to max 4 (width 10)
|
||||
False
|
||||
[warning] at <interactive>:1:1--1:48:
|
||||
[warning] at <interactive>:1:11--1:25:
|
||||
Defaulting type parameter 'bits'
|
||||
of finite enumeration
|
||||
at <interactive>:1:11--1:25
|
||||
to max 7 (width 10)
|
||||
False
|
||||
[warning] at <interactive>:1:1--1:47:
|
||||
[warning] at <interactive>:1:11--1:24:
|
||||
Defaulting type parameter 'bits'
|
||||
of finite enumeration
|
||||
at <interactive>:1:11--1:24
|
||||
|
||||
@ -1,7 +1,7 @@
|
||||
Loading module Cryptol
|
||||
Assuming a = 4
|
||||
[0xb, 0xb, 0xb, 0xb, 0xb, 0xb, 0xb, 0xb, 0xb, 0xb]
|
||||
[warning] at <interactive>:1:1--1:68:
|
||||
[warning] at <interactive>:1:65--1:67:
|
||||
Defaulting type parameter 'bits'
|
||||
of finite enumeration
|
||||
at <interactive>:1:13--1:24
|
||||
|
||||
Loading…
Reference in New Issue
Block a user