diff --git a/lib/Cryptol.cry b/lib/Cryptol.cry index f0918ff4..0dc05a07 100644 --- a/lib/Cryptol.cry +++ b/lib/Cryptol.cry @@ -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. diff --git a/src/Cryptol/ModuleSystem/Renamer.hs b/src/Cryptol/ModuleSystem/Renamer.hs index efb92f1d..de58cb08 100644 --- a/src/Cryptol/ModuleSystem/Renamer.hs +++ b/src/Cryptol/ModuleSystem/Renamer.hs @@ -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 diff --git a/src/Cryptol/Parser/AST.hs b/src/Cryptol/Parser/AST.hs index f2e861a6..f8a5bc84 100644 --- a/src/Cryptol/Parser/AST.hs +++ b/src/Cryptol/Parser/AST.hs @@ -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) diff --git a/src/Cryptol/Parser/Names.hs b/src/Cryptol/Parser/Names.hs index fd6ea001..55220b0b 100644 --- a/src/Cryptol/Parser/Names.hs +++ b/src/Cryptol/Parser/Names.hs @@ -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 diff --git a/src/Cryptol/Parser/ParserUtils.hs b/src/Cryptol/Parser/ParserUtils.hs index da9434e3..41fd8240 100644 --- a/src/Cryptol/Parser/ParserUtils.hs +++ b/src/Cryptol/Parser/ParserUtils.hs @@ -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 -> diff --git a/src/Cryptol/Prims/Eval.hs b/src/Cryptol/Prims/Eval.hs index 5b6b1fa4..7ddc4c07 100644 --- a/src/Cryptol/Prims/Eval.hs +++ b/src/Cryptol/Prims/Eval.hs @@ -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. diff --git a/src/Cryptol/TypeCheck/Infer.hs b/src/Cryptol/TypeCheck/Infer.hs index 40473cf1..60aaf80d 100644 --- a/src/Cryptol/TypeCheck/Infer.hs +++ b/src/Cryptol/TypeCheck/Infer.hs @@ -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 -> [ ] diff --git a/src/Cryptol/TypeCheck/Kind.hs b/src/Cryptol/TypeCheck/Kind.hs index 975a3b61..004983ab 100644 --- a/src/Cryptol/TypeCheck/Kind.hs +++ b/src/Cryptol/TypeCheck/Kind.hs @@ -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. diff --git a/src/Cryptol/TypeCheck/SimpleSolver.hs b/src/Cryptol/TypeCheck/SimpleSolver.hs index c82a9329..1ec6e995 100644 --- a/src/Cryptol/TypeCheck/SimpleSolver.hs +++ b/src/Cryptol/TypeCheck/SimpleSolver.hs @@ -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 diff --git a/src/Cryptol/TypeCheck/Solver/Class.hs b/src/Cryptol/TypeCheck/Solver/Class.hs index edd35087..576b28c9 100644 --- a/src/Cryptol/TypeCheck/Solver/Class.hs +++ b/src/Cryptol/TypeCheck/Solver/Class.hs @@ -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] diff --git a/src/Cryptol/TypeCheck/Type.hs b/src/Cryptol/TypeCheck/Type.hs index b04b104e..e9f702f0 100644 --- a/src/Cryptol/TypeCheck/Type.hs +++ b/src/Cryptol/TypeCheck/Type.hs @@ -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 "(&&)"