mirror of
https://github.com/GaloisInc/cryptol.git
synced 2024-09-11 14:06:13 +03:00
Remove unused primitive type operator lengthFromThen.
This commit is contained in:
Brian Huffman
parent
24fb6c9511
commit
7ea4884fdd
@ -316,17 +316,6 @@
|
||||
)
|
||||
|
||||
|
||||
(define-fun cryLenFromThen ((x InfNat) (y InfNat) (z InfNat)) InfNat
|
||||
(ite (or (isErr x) (not (isFin x))
|
||||
(isErr y) (not (isFin y))
|
||||
(isErr z) (not (isFin z))
|
||||
(= (value x) (value y))) cryErr
|
||||
(ite (< (value y) (value x)) (cryLenFromThenTo x y (cryNat 0))
|
||||
(cryLenFromThenTo x y (cryNat (- (cryExpTable 2 (value z)) 1))))
|
||||
)
|
||||
)
|
||||
|
||||
|
||||
; ---
|
||||
|
||||
|
||||
|
||||
@ -142,7 +142,6 @@ evalTF f vs
|
||||
| TCMax <- f, [x,y] <- vs = nMax x y
|
||||
| TCCeilDiv <- f, [x,y] <- vs = mb $ nCeilDiv x y
|
||||
| TCCeilMod <- f, [x,y] <- vs = mb $ nCeilMod x y
|
||||
| TCLenFromThen <- f, [x,y,z] <- vs = mb $ nLenFromThen x y z
|
||||
| TCLenFromThenTo <- f, [x,y,z] <- vs = mb $ nLenFromThenTo x y z
|
||||
| otherwise = evalPanic "evalTF"
|
||||
["Unexpected type function:", show ty]
|
||||
|
||||
@ -632,9 +632,8 @@ type :: { Type PName
|
||||
|
||||
app_type :: { Type PName }
|
||||
-- : 'lg2' atype { at ($1,$2) $ TApp TCLg2 [$2] }
|
||||
-- | 'lengthFromThen' atype atype { at ($1,$3) $ TApp TCLenFromThen [$2,$3] }
|
||||
-- | 'lengthFromThenTo' atype atype
|
||||
-- atype { at ($1,$4) $ TApp TCLenFromThen [$2,$3,$4] }
|
||||
-- atype { at ($1,$4) $ TApp TCLenFromThenTo [$2,$3,$4] }
|
||||
-- | 'min' atype atype { at ($1,$3) $ TApp TCMin [$2,$3] }
|
||||
-- | 'max' atype atype { at ($1,$3) $ TApp TCMax [$2,$3] }
|
||||
|
||||
|
||||
@ -114,9 +114,6 @@ primTyList =
|
||||
, tInfix "%^" TF TCCeilMod (l 90)
|
||||
"How much we need to add to make a proper multiple of the second argument."
|
||||
|
||||
, tPrefix "lengthFromThen" TF TCLenFromThen
|
||||
"The length of an enumeration."
|
||||
|
||||
, tPrefix "lengthFromThenTo" TF TCLenFromThenTo
|
||||
"The length of an enumeration."
|
||||
]
|
||||
@ -244,12 +241,10 @@ instance HasKind TFun where
|
||||
TCCeilDiv -> KNum :-> KNum :-> KNum
|
||||
TCCeilMod -> KNum :-> KNum :-> KNum
|
||||
|
||||
TCLenFromThen -> KNum :-> KNum :-> KNum :-> KNum
|
||||
TCLenFromThenTo -> KNum :-> KNum :-> KNum :-> KNum
|
||||
|
||||
|
||||
|
||||
|
||||
-- | Type constants.
|
||||
data TCon = TC TC | PC PC | TF TFun | TError Kind TCErrorMessage
|
||||
deriving (Show, Eq, Ord, Generic, NFData)
|
||||
@ -325,9 +320,6 @@ data TFun
|
||||
| TCCeilMod -- ^ @ : Num -> Num -> Num @
|
||||
|
||||
-- Computing the lengths of explicit enumerations
|
||||
| TCLenFromThen -- ^ @ : Num -> Num -> Num -> Num@
|
||||
-- Example: @[ 1, 5 .. ] :: [lengthFromThen 1 5 b][b]@
|
||||
|
||||
| TCLenFromThenTo -- ^ @ : Num -> Num -> Num -> Num@
|
||||
-- Example: @[ 1, 5 .. 9 ] :: [lengthFromThenTo 1 5 9][b]@
|
||||
|
||||
@ -449,6 +441,4 @@ instance PP TFun where
|
||||
TCMax -> text "max"
|
||||
TCCeilDiv -> text "/^"
|
||||
TCCeilMod -> text "%^"
|
||||
|
||||
TCLenFromThen -> text "lengthFromThen"
|
||||
TCLenFromThenTo -> text "lengthFromThenTo"
|
||||
|
||||
@ -310,7 +310,6 @@ freshName n _ =
|
||||
-- TCWidth -> "width"
|
||||
-- TCMin -> "min"
|
||||
-- TCMax -> "max"
|
||||
-- TCLenFromThen -> "len_from_then"
|
||||
-- TCLenFromThenTo -> "len_from_then_to"
|
||||
-- showRecFld (nm,t) = showName nm : showT t
|
||||
|
||||
|
||||
@ -3,7 +3,7 @@ module Cryptol.TypeCheck.SimpType where
|
||||
|
||||
import Control.Applicative((<|>))
|
||||
import Cryptol.TypeCheck.Type hiding
|
||||
(tSub,tMul,tDiv,tMod,tExp,tMin,tCeilDiv,tCeilMod,tLenFromThen,tLenFromThenTo)
|
||||
(tSub,tMul,tDiv,tMod,tExp,tMin,tCeilDiv,tCeilMod,tLenFromThenTo)
|
||||
import Cryptol.TypeCheck.TypePat
|
||||
import Cryptol.TypeCheck.Solver.InfNat
|
||||
import Control.Monad(msum,guard)
|
||||
@ -41,7 +41,6 @@ tCon tc ts =
|
||||
(TCWidth, [x]) -> tWidth x
|
||||
(TCCeilDiv, [x, y]) -> tCeilDiv x y
|
||||
(TCCeilMod, [x, y]) -> tCeilMod x y
|
||||
(TCLenFromThen, [x, y, z]) -> tLenFromThen x y z
|
||||
(TCLenFromThenTo, [x, y, z]) -> tLenFromThenTo x y z
|
||||
_ -> TCon tc ts
|
||||
_ -> TCon tc ts
|
||||
@ -283,12 +282,6 @@ tWidth x
|
||||
| Just t <- tOp TCWidth (total (op1 nWidth)) [x] = t
|
||||
| otherwise = tf1 TCWidth x
|
||||
|
||||
tLenFromThen :: Type -> Type -> Type -> Type
|
||||
tLenFromThen x y z
|
||||
| Just t <- tOp TCLenFromThen (op3 nLenFromThen) [x,y,z] = t
|
||||
-- XXX: rules?
|
||||
| otherwise = tf3 TCLenFromThen x y z
|
||||
|
||||
tLenFromThenTo :: Type -> Type -> Type -> Type
|
||||
tLenFromThenTo x y z
|
||||
| Just t <- tOp TCLenFromThenTo (op3 nLenFromThenTo) [x,y,z] = t
|
||||
|
||||
@ -2,7 +2,7 @@
|
||||
module Cryptol.TypeCheck.SimpleSolver ( simplify , simplifyStep) where
|
||||
|
||||
import Cryptol.TypeCheck.Type hiding
|
||||
( tSub, tMul, tDiv, tMod, tExp, tMin, tLenFromThen, tLenFromThenTo)
|
||||
( tSub, tMul, tDiv, tMod, tExp, tMin, tLenFromThenTo)
|
||||
import Cryptol.TypeCheck.Solver.Types
|
||||
import Cryptol.TypeCheck.Solver.Numeric.Fin(cryIsFinType)
|
||||
import Cryptol.TypeCheck.Solver.Numeric(cryIsEqual, cryIsNotEqual, cryIsGeq)
|
||||
|
||||
@ -58,8 +58,6 @@ wfTypeFunction :: TFun -> [Type] -> [Prop]
|
||||
wfTypeFunction TCSub [a,b] = [ a >== b, pFin b]
|
||||
wfTypeFunction TCDiv [a,b] = [ b >== tOne, pFin a ]
|
||||
wfTypeFunction TCMod [a,b] = [ b >== tOne, pFin a ]
|
||||
wfTypeFunction TCLenFromThen [a,b,w] =
|
||||
[ pFin a, pFin b, pFin w, a =/= b, w >== tWidth a ]
|
||||
wfTypeFunction TCLenFromThenTo [a,b,c] = [ pFin a, pFin b, pFin c, a =/= b ]
|
||||
wfTypeFunction _ _ = []
|
||||
|
||||
|
||||
@ -159,28 +159,6 @@ nWidth Inf = Inf
|
||||
nWidth (Nat n) = Nat (widthInteger n)
|
||||
|
||||
|
||||
{- | @length ([ x, y .. ] : [_][w])@
|
||||
We don't check that the second element fits in `w` many bits as the
|
||||
second element may not be part of the list.
|
||||
For example, the length of @[ 0 .. ] : [_][0]@ is @nLenFromThen 0 1 0@,
|
||||
which should evaluate to 1. -}
|
||||
|
||||
|
||||
{- XXX: It would appear that the actual notation also requires `y` to fit in...
|
||||
It is not clear if that's a good idea. Consider, for example,
|
||||
|
||||
[ 1, 4 .., 2 ]
|
||||
|
||||
Cryptol infers that this list has one element, but it insists that the
|
||||
width of the elements be at least 3, to accommodate the 4.
|
||||
-}
|
||||
nLenFromThen :: Nat' -> Nat' -> Nat' -> Maybe Nat'
|
||||
nLenFromThen a@(Nat x) b@(Nat y) wi@(Nat w)
|
||||
| wi < nWidth a = Nothing
|
||||
| y > x = nLenFromThenTo a b (Nat (2^w - 1))
|
||||
| y < x = nLenFromThenTo a b (Nat 0)
|
||||
|
||||
nLenFromThen _ _ _ = Nothing
|
||||
|
||||
-- | @length [ x, y .. z ]@
|
||||
nLenFromThenTo :: Nat' -> Nat' -> Nat' -> Maybe Nat'
|
||||
@ -202,9 +180,6 @@ nLenFromThenTo _ _ _ = Nothing
|
||||
nLenFromThenTo x y z == 0
|
||||
case 1: x > y && z > x
|
||||
case 2: x <= y && z < x
|
||||
|
||||
nLenFromThen x y w == 0
|
||||
impossible
|
||||
-}
|
||||
|
||||
{- Note [Sequences of Length 1]
|
||||
@ -243,14 +218,6 @@ nLenFromThenTo _ _ _ = Nothing
|
||||
|
||||
case 2 summary: y > z, z >= x
|
||||
|
||||
------------------------
|
||||
|
||||
`nLenFromThen x y w == 1`
|
||||
| y > x = nLenFromThenTo x y (Nat (2^w - 1))
|
||||
| y < x = nLenFromThenTo x y (Nat 0)
|
||||
|
||||
y >= 2^w, y > x
|
||||
|
||||
-}
|
||||
|
||||
|
||||
|
||||
@ -88,7 +88,6 @@ cryIsFinType varInfo ty =
|
||||
(TCWidth, [t1]) -> SolvedIf [ pFin t1 ]
|
||||
(TCCeilDiv, [_,_]) -> SolvedIf []
|
||||
(TCCeilMod, [_,_]) -> SolvedIf []
|
||||
(TCLenFromThen,[_,_,_]) -> SolvedIf []
|
||||
(TCLenFromThenTo,[_,_,_]) -> SolvedIf []
|
||||
|
||||
_ -> Unsolved
|
||||
|
||||
@ -42,8 +42,6 @@ typeInterval varInfo = go
|
||||
(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)
|
||||
@ -344,17 +342,6 @@ iWidth i = Interval { iLower = nWidth (iLower i)
|
||||
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
|
||||
|
||||
@ -353,7 +353,6 @@ toSMT tvs ty = matchDefault (panic "toSMT" [ "Unexpected type", show ty ])
|
||||
, aWidth ~> "cryWidth"
|
||||
, aCeilDiv ~> "cryCeilDiv"
|
||||
, aCeilMod ~> "cryCeilMod"
|
||||
, aLenFromThen ~> "cryLenFromThen"
|
||||
, aLenFromThenTo ~> "cryLenFromThenTo"
|
||||
|
||||
, anError KNum ~> "cryErr"
|
||||
|
||||
@ -542,9 +542,6 @@ tCeilDiv = tf2 TCCeilDiv
|
||||
tCeilMod :: Type -> Type -> Type
|
||||
tCeilMod = tf2 TCCeilMod
|
||||
|
||||
tLenFromThen :: Type -> Type -> Type -> Type
|
||||
tLenFromThen = tf3 TCLenFromThen
|
||||
|
||||
tLenFromThenTo :: Type -> Type -> Type -> Type
|
||||
tLenFromThenTo = tf3 TCLenFromThenTo
|
||||
|
||||
@ -553,8 +550,6 @@ tLenFromThenTo = tf3 TCLenFromThenTo
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
-- Construction of constraints.
|
||||
|
||||
|
||||
@ -5,7 +5,7 @@ module Cryptol.TypeCheck.TypePat
|
||||
, aMin, aMax
|
||||
, aWidth
|
||||
, aCeilDiv, aCeilMod
|
||||
, aLenFromThen, aLenFromThenTo
|
||||
, aLenFromThenTo
|
||||
|
||||
, aLiteral, aLogic
|
||||
|
||||
@ -112,9 +112,6 @@ aCeilDiv = tf TCCeilDiv ar2
|
||||
aCeilMod :: Pat Type (Type,Type)
|
||||
aCeilMod = tf TCCeilMod ar2
|
||||
|
||||
aLenFromThen :: Pat Type (Type,Type,Type)
|
||||
aLenFromThen = tf TCLenFromThen ar3
|
||||
|
||||
aLenFromThenTo :: Pat Type (Type,Type,Type)
|
||||
aLenFromThenTo = tf TCLenFromThenTo ar3
|
||||
|
||||
|
||||
Loading…
Reference in New Issue
Block a user