GaloisInc/cryptol
1
1
Fork 0
mirror of https://github.com/GaloisInc/cryptol.git synced 2025-01-05 23:17:42 +03:00
Code Issues Projects Releases Wiki Activity

Introduce class Literal and generalize primitive demote to use it.

Browse Source 
demote : {val, a} Literal val a => a

instance (fin val) => Literal val Integer
instance (fin val, fin bits, bits >= width val) => Literal val [bits]
This commit is contained in:
Brian Huffman 2017-11-08 15:23:08 -08:00
parent 7e964aa1cd
commit 5eb67c0513
11 changed files with 106 additions and 65 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
lib/Cryptol.cry
View File

@ -8,7 +8,7 @@ module Cryptol where
/**
* The value corresponding to a numeric type.
*/
primitive demote : {val, bits} (fin val, fin bits, bits >= width val) => [bits]
primitive demote : {val, a} Literal val a => a
/**
* The integer value corresponding to a numeric type.

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

@ -520,13 +520,14 @@ instance Rename TParam where
instance Rename Prop where
rename p = case p of
CFin t -> CFin <$> rename t
CEqual l r -> CEqual <$> rename l <*> rename r
CGeq l r -> CGeq <$> rename l <*> rename r
CEqual l r -> CEqual <$> rename l <*> rename r
CGeq l r -> CGeq <$> rename l <*> rename r
CZero t -> CZero <$> rename t
CLogic t -> CLogic <$> rename t
CArith t -> CArith <$> rename t
CCmp t -> CCmp <$> rename t
CSignedCmp t -> CSignedCmp <$> rename t
CLiteral l r -> CLiteral <$> rename l <*> rename r
CUser qn ps -> CUser <$> renameType qn <*> traverse rename ps
CLocated p' r -> withLoc r
$ CLocated <$> rename p' <*> pure r

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

@ -383,6 +383,7 @@ data Prop n = CFin (Type n) -- ^ @ fin x @
| CArith (Type n) -- ^ @ Arith a @
| CCmp (Type n) -- ^ @ Cmp a @
| CSignedCmp (Type n) -- ^ @ SignedCmp a @
| CLiteral (Type n) (Type n)-- ^ @ Literal val a @
| CUser n [Type n] -- ^ Constraint synonym
| CLocated (Prop n) Range -- ^ Location information
| CType (Type n) -- ^ After parsing
@ -866,19 +867,19 @@ instance PPName name => PP (Type name) where
instance PPName name => PP (Prop name) where
ppPrec n prop =
case prop of
CFin t -> text "fin" <+> ppPrec 4 t
CZero t -> text "Zero" <+> ppPrec 4 t
CLogic t -> text "Logic" <+> ppPrec 4 t
CArith t -> text "Arith" <+> ppPrec 4 t
CCmp t -> text "Cmp" <+> ppPrec 4 t
CSignedCmp t -> text "SignedCmp" <+> ppPrec 4 t
CEqual t1 t2 -> ppPrec 2 t1 <+> text "==" <+> ppPrec 2 t2
CGeq t1 t2 -> ppPrec 2 t1 <+> text ">=" <+> ppPrec 2 t2
CUser f ts -> optParens (n > 2)
$ ppPrefixName f <+> fsep (map (ppPrec 4) ts)
CLocated c _ -> ppPrec n c
CType t -> ppPrec n t
CFin t -> text "fin" <+> ppPrec 4 t
CZero t -> text "Zero" <+> ppPrec 4 t
CLogic t -> text "Logic" <+> ppPrec 4 t
CArith t -> text "Arith" <+> ppPrec 4 t
CCmp t -> text "Cmp" <+> ppPrec 4 t
CSignedCmp t -> text "SignedCmp" <+> ppPrec 4 t
CLiteral t1 t2 -> text "Literal" <+> ppPrec 4 t1 <+> ppPrec 4 t2
CEqual t1 t2 -> ppPrec 2 t1 <+> text "==" <+> ppPrec 2 t2
CGeq t1 t2 -> ppPrec 2 t1 <+> text ">=" <+> ppPrec 2 t2
CUser f ts -> optParens (n > 2)
$ ppPrefixName f <+> fsep (map (ppPrec 4) ts)
CLocated c _ -> ppPrec n c
CType t -> ppPrec n t
--------------------------------------------------------------------------------
@ -1049,6 +1050,7 @@ instance NoPos (Prop name) where
CArith x -> CArith (noPos x)
CCmp x -> CCmp (noPos x)
CSignedCmp x -> CSignedCmp (noPos x)
CLiteral x y -> CLiteral (noPos x) (noPos y)
CUser x y -> CUser x (noPos y)
CLocated c _ -> noPos c
CType t -> CType (noPos t)

24
src/Cryptol/Parser/Names.hs
View File

@ -175,6 +175,7 @@ namesC vs prop =
CArith t -> namesT vs t
CCmp t -> namesT vs t
CSignedCmp t -> namesT vs t
CLiteral t1 t2-> Set.union (namesT vs t1) (namesT vs t2)
CUser x ts -> Set.insert x (Set.unions (map (namesT vs) ts))
CLocated p _ -> namesC vs p
CType t -> namesT vs t
@ -272,17 +273,18 @@ tnamesS (Forall params props ty _) =
tnamesC :: Ord name => Prop name -> Set name
tnamesC prop =
case prop of
CFin t -> tnamesT t
CEqual t1 t2 -> Set.union (tnamesT t1) (tnamesT t2)
CGeq t1 t2 -> Set.union (tnamesT t1) (tnamesT t2)
CZero t -> tnamesT t
CLogic t -> tnamesT t
CArith t -> tnamesT t
CCmp t -> tnamesT t
CSignedCmp t -> tnamesT t
CUser x ts -> Set.insert x (Set.unions (map tnamesT ts))
CLocated p _ -> tnamesC p
CType t -> tnamesT t
CFin t -> tnamesT t
CEqual t1 t2 -> Set.union (tnamesT t1) (tnamesT t2)
CGeq t1 t2 -> Set.union (tnamesT t1) (tnamesT t2)
CZero t -> tnamesT t
CLogic t -> tnamesT t
CArith t -> tnamesT t
CCmp t -> tnamesT t
CSignedCmp t -> tnamesT t
CLiteral t1 t2 -> Set.union (tnamesT t1) (tnamesT t2)
CUser x ts -> Set.insert x (Set.unions (map tnamesT ts))
CLocated p _ -> tnamesC p
CType t -> tnamesT t
-- | Compute the type synonyms/type variables used by a type.
tnamesT :: Ord name => Type name -> Set name

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

@ -482,17 +482,19 @@ mkProp ty =
| i == finIdent, [x] <- xs = return [CLocated (CFin x) r]
| i == cmpIdent, [x] <- xs = return [CLocated (CCmp x) r]
| i == signedCmpIdent, [x] <- xs = return [CLocated (CSignedCmp x) r]
| i == literalIdent, [x,y] <- xs = return [CLocated (CLiteral x y) r]
| otherwise = return [CLocated (CType (TUser f xs)) r]
where
i = getIdent f
zeroIdent, logicIdent, arithIdent, finIdent, cmpIdent, signedCmpIdent :: Ident
zeroIdent, logicIdent, arithIdent, finIdent, cmpIdent, signedCmpIdent, literalIdent :: Ident
zeroIdent = mkIdent "Zero"
logicIdent = mkIdent "Logic"
arithIdent = mkIdent "Arith"
finIdent = mkIdent "fin"
cmpIdent = mkIdent "Cmp"
signedCmpIdent = mkIdent "SignedCmp"
literalIdent = mkIdent "Literal"
-- | Make an ordinary module
mkModule :: Located ModName ->

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

@ -247,13 +247,14 @@ primTable = Map.fromList $ map (\(n, v) -> (mkIdent (T.pack n), v))
-- | Make a numeric constant.
ecDemoteV :: BitWord b w i => GenValue b w i
ecDemoteV = nlam $ \valT ->
nlam $ \bitT ->
case (valT, bitT) of
(Nat v, Nat bs) -> word bs v
tlam $ \ty ->
case (valT, ty) of
(Nat v, TVInteger) -> VInteger (integerLit v)
(Nat v, TVSeq bs TVBit) -> word bs v
_ -> evalPanic "Cryptol.Eval.Prim.evalConst"
["Unexpected Inf in constant."
, show valT
, show bitT
, show ty
]
-- | Make an integer constant.

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

@ -82,22 +82,23 @@ desugarLiteral fixDec lit =
do l <- curRange
demotePrim <- mkPrim "demote"
let named (x,y) = P.NamedInst
P.Named { name = Located l (packIdent x), value = P.TNum y }
P.Named { name = Located l (packIdent x), value = y }
demote fs = P.EAppT demotePrim (map named fs)
tBits n = P.TSeq (P.TNum n) P.TBit
return $ case lit of
P.ECNum num info ->
demote $ [ ("val", num) ] ++ case info of
P.BinLit n -> [ ("bits", 1 * toInteger n) ]
P.OctLit n -> [ ("bits", 3 * toInteger n) ]
P.HexLit n -> [ ("bits", 4 * toInteger n) ]
P.CharLit -> [ ("bits", 8 :: Integer) ]
demote $ [ ("val", P.TNum num) ] ++ case info of
P.BinLit n -> [ ("a", tBits (1 * toInteger n)) ]
P.OctLit n -> [ ("a", tBits (3 * toInteger n)) ]
P.HexLit n -> [ ("a", tBits (4 * toInteger n)) ]
P.CharLit -> [ ("a", tBits (8 :: Integer)) ]
P.DecLit
| fixDec -> if num == 0
then [ ("bits", 0)]
then [ ("a", tBits 0)]
else case genLog num 2 of
Just (x,_) -> [ ("bits", x + 1) ]
Just (x,_) -> [ ("a", tBits (x + 1)) ]
_ -> []
| otherwise -> [ ]
P.PolyLit _n -> [ ]

25
src/Cryptol/TypeCheck/Kind.hs
View File

@ -377,18 +377,19 @@ checkProp :: P.Prop Name -- ^ Proposition that need to be checked
-> KindM Type -- ^ Checked representation
checkProp prop =
case prop of
P.CFin t1 -> tcon (PC PFin) [t1] (Just KProp)
P.CEqual t1 t2 -> tcon (PC PEqual) [t1,t2] (Just KProp)
P.CGeq t1 t2 -> tcon (PC PGeq) [t1,t2] (Just KProp)
P.CZero t1 -> tcon (PC PZero) [t1] (Just KProp)
P.CLogic t1 -> tcon (PC PLogic) [t1] (Just KProp)
P.CArith t1 -> tcon (PC PArith) [t1] (Just KProp)
P.CCmp t1 -> tcon (PC PCmp) [t1] (Just KProp)
P.CSignedCmp t1 -> tcon (PC PSignedCmp) [t1] (Just KProp)
P.CUser x [] -> checkTyThing x (Just KProp)
P.CUser x ts -> tySyn False x ts (Just KProp)
P.CLocated p r1 -> kInRange r1 (checkProp p)
P.CType _ -> panic "checkProp" [ "Unexpected CType", show prop ]
P.CFin t1 -> tcon (PC PFin) [t1] (Just KProp)
P.CEqual t1 t2 -> tcon (PC PEqual) [t1,t2] (Just KProp)
P.CGeq t1 t2 -> tcon (PC PGeq) [t1,t2] (Just KProp)
P.CZero t1 -> tcon (PC PZero) [t1] (Just KProp)
P.CLogic t1 -> tcon (PC PLogic) [t1] (Just KProp)
P.CArith t1 -> tcon (PC PArith) [t1] (Just KProp)
P.CCmp t1 -> tcon (PC PCmp) [t1] (Just KProp)
P.CSignedCmp t1 -> tcon (PC PSignedCmp) [t1] (Just KProp)
P.CLiteral t1 t2 -> tcon (PC PLiteral) [t1,t2] (Just KProp)
P.CUser x [] -> checkTyThing x (Just KProp)
P.CUser x ts -> tySyn False x ts (Just KProp)
P.CLocated p r1 -> kInRange r1 (checkProp p)
P.CType _ -> panic "checkProp" [ "Unexpected CType", show prop ]
-- | Check that a type has the expected kind.

28
src/Cryptol/TypeCheck/SimpleSolver.hs
View File

@ -8,7 +8,8 @@ import Cryptol.TypeCheck.Solver.Types
import Cryptol.TypeCheck.Solver.Numeric.Fin(cryIsFinType)
import Cryptol.TypeCheck.Solver.Numeric(cryIsEqual, cryIsNotEqual, cryIsGeq)
import Cryptol.TypeCheck.Solver.Class
(solveZeroInst, solveLogicInst, solveArithInst, solveCmpInst, solveSignedCmpInst)
( solveZeroInst, solveLogicInst, solveArithInst, solveCmpInst
, solveSignedCmpInst, solveLiteralInst )
import Cryptol.Utils.Debug(ppTrace)
import Cryptol.TypeCheck.PP
@ -34,21 +35,22 @@ simplify ctxt p =
simplifyStep :: Ctxt -> Prop -> Solved
simplifyStep ctxt prop =
case tNoUser prop of
TCon (PC PTrue) [] -> SolvedIf []
TCon (PC PAnd) [l,r] -> SolvedIf [l,r]
TCon (PC PTrue) [] -> SolvedIf []
TCon (PC PAnd) [l,r] -> SolvedIf [l,r]
TCon (PC PZero) [ty] -> solveZeroInst ty
TCon (PC PLogic) [ty] -> solveLogicInst ty
TCon (PC PArith) [ty] -> solveArithInst ty
TCon (PC PCmp) [ty] -> solveCmpInst ty
TCon (PC PSignedCmp) [ty] -> solveSignedCmpInst ty
TCon (PC PZero) [ty] -> solveZeroInst ty
TCon (PC PLogic) [ty] -> solveLogicInst ty
TCon (PC PArith) [ty] -> solveArithInst ty
TCon (PC PCmp) [ty] -> solveCmpInst ty
TCon (PC PSignedCmp) [ty] -> solveSignedCmpInst ty
TCon (PC PLiteral) [t1,t2] -> solveLiteralInst t1 t2
TCon (PC PFin) [ty] -> cryIsFinType ctxt ty
TCon (PC PFin) [ty] -> cryIsFinType ctxt ty
TCon (PC PEqual) [t1,t2] -> cryIsEqual ctxt t1 t2
TCon (PC PNeq) [t1,t2] -> cryIsNotEqual ctxt t1 t2
TCon (PC PGeq) [t1,t2] -> cryIsGeq ctxt t1 t2
TCon (PC PEqual) [t1,t2] -> cryIsEqual ctxt t1 t2
TCon (PC PNeq) [t1,t2] -> cryIsNotEqual ctxt t1 t2
TCon (PC PGeq) [t1,t2] -> cryIsGeq ctxt t1 t2
_ -> Unsolved
_ -> Unsolved

17
src/Cryptol/TypeCheck/Solver/Class.hs
View File

@ -16,6 +16,7 @@ module Cryptol.TypeCheck.Solver.Class
, solveArithInst
, solveCmpInst
, solveSignedCmpInst
, solveLiteralInst
, expandProp
) where
@ -196,6 +197,22 @@ solveSignedCmpInst ty = case tNoUser ty of
_ -> Unsolved
-- | Solve Literal constraints.
solveLiteralInst :: Type -> Type -> Solved
solveLiteralInst n ty = case tNoUser ty of
-- SignedCmp Error -> fails
TCon (TError _ e) _ -> Unsolvable e
-- (fin val) => Literal val Integer
TCon (TC TCInteger) [] -> SolvedIf [ pFin n ]
-- (fin bits, bits => width n) => Literal n [bits]
TCon (TC TCSeq) [bits, TCon (TC TCBit) []] -> SolvedIf [ pFin n, pFin bits, bits >== tWidth n ]
_ -> Unsolved
-- | Add propositions that are implied by the given one.
-- The result contains the orignal proposition, and maybe some more.
expandProp :: Prop -> [Prop]

12
src/Cryptol/TypeCheck/Type.hs
View File

@ -142,6 +142,7 @@ data PC = PEqual -- ^ @_ == _@
| PArith -- ^ @Arith _@
| PCmp -- ^ @Cmp _@
| PSignedCmp -- ^ @SignedCmp _@
| PLiteral -- ^ @Literal _ _@
| PAnd -- ^ This is useful when simplifying things in place
| PTrue -- ^ Ditto
@ -239,6 +240,7 @@ instance HasKind PC where
PArith -> KType :-> KProp
PCmp -> KType :-> KProp
PSignedCmp -> KType :-> KProp
PLiteral -> KNum :-> KType :-> KProp
PAnd -> KProp :-> KProp :-> KProp
PTrue -> KProp
@ -483,6 +485,11 @@ pIsSignedCmp ty = case tNoUser ty of
TCon (PC PSignedCmp) [t1] -> Just t1
_ -> Nothing
pIsLiteral :: Prop -> Maybe (Type, Type)
pIsLiteral ty = case tNoUser ty of
TCon (PC PLiteral) [t1, t2] -> Just (t1, t2)
_ -> Nothing
pIsTrue :: Prop -> Bool
pIsTrue ty = case tNoUser ty of
TCon (PC PTrue) _ -> True
@ -644,6 +651,9 @@ pCmp t = TCon (PC PCmp) [t]
pSignedCmp :: Type -> Prop
pSignedCmp t = TCon (PC PSignedCmp) [t]
pLiteral :: Type -> Type -> Prop
pLiteral x y = TCon (PC PLiteral) [x, y]
-- | Make a greater-than-or-equal-to constraint.
(>==) :: Type -> Type -> Prop
x >== y = TCon (PC PGeq) [x,y]
@ -834,6 +844,7 @@ instance PP (WithNames Type) where
(PArith, [t1]) -> pp pc <+> go 4 t1
(PCmp, [t1]) -> pp pc <+> go 4 t1
(PSignedCmp, [t1]) -> pp pc <+> go 4 t1
(PLiteral, [t1,t2]) -> pp pc <+> go 4 t1 <+> go 4 t2
(_, _) -> pp pc <+> fsep (map (go 4) ts)
@ -905,6 +916,7 @@ instance PP PC where
PArith -> text "Arith"
PCmp -> text "Cmp"
PSignedCmp -> text "SignedCmp"
PLiteral -> text "Literal"
PTrue -> text "True"
PAnd -> text "(&&)"