GaloisInc/cryptol
1
1
Fork 0
mirror of https://github.com/GaloisInc/cryptol.git synced 2024-12-15 02:01:39 +03:00
Code Issues Projects Releases Wiki Activity

Remove duplicated code for parsing/renaming/checking constraints.

Browse Source 
We now re-use the same code that is used to parse, rename, and
kind-check type expressions.
This commit is contained in:
Brian Huffman 2019-06-25 14:17:51 -07:00
parent f53c1f8777
commit a8552f58a6
5 changed files with 18 additions and 168 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

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

@ -35,7 +35,6 @@ import Cryptol.Prims.Syntax
import Cryptol.Parser.AST
import Cryptol.Parser.Position
import Cryptol.Parser.Selector(ppNestedSels,selName)
import Cryptol.TypeCheck.Type (TCon(..))
import Cryptol.Utils.Ident (packInfix)
import Cryptol.Utils.Panic (panic)
import Cryptol.Utils.PP
@ -559,47 +558,7 @@ instance Rename TParam where
return TParam { tpName = n, .. }
instance Rename Prop where
rename p = case p of
CFin t -> CFin <$> rename t
CEqual l r -> CEqual <$> rename l <*> rename r
CNeq l r -> CNeq <$> 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
-- here, we rename the type and then require that it produces something that
-- looks like a Prop
CType t -> translateProp =<< resolveTypeFixity t
translateProp :: Type PName -> RenameM (Prop Name)
translateProp ty = go ty
where
go t = case t of
TLocated t' r -> (`CLocated` r) <$> go t'
TApp (PC x) [l,r]
| PEqual <- x -> CEqual <$> rename l <*> rename r
| PNeq <- x -> CNeq <$> rename l <*> rename r
| PGeq <- x -> CGeq <$> rename l <*> rename r
TUser n [l,r]
| isLeq n -> CGeq <$> rename r <*> rename l
TUser n ts -> CUser <$> renameType n <*> traverse rename ts
-- record an error, but continue renaming to gather any other errors
_ ->
do record (InvalidConstraint ty)
CType <$> rename t
rename (CType t) = CType <$> rename t
-- | Check to see if this identifier is a reserved type/type-function.
isReserved :: PName -> Bool
@ -677,19 +636,25 @@ mkTInfix t op@(o2,f2) z =
case t of
TLocated t1 _ -> mkTInfix t1 op z
TUser op1 [x,y] | isLeq op1 -> doFixity (TUser op1) leqFixity x y
-- FIXME: This is a hack to implement an infix type constraint synonym:
-- type constraint x <= y = (y >= x)
-- It should be removed once we can define this in the Cryptol prelude.
TUser op1 [x,y] | isLeq op1 -> doFixity mkLeq leqFixity x y
TApp tc [x,y]
| Just pt <- primTyFromTC tc
, Just f1 <- primTyFixity pt -> doFixity (TApp tc) f1 x y
, Just f1 <- primTyFixity pt -> doFixity (mkBin tc) f1 x y
_ -> return (o2 t z)
where
mkLeq a b = TApp (PC PGeq) [b, a]
mkBin tc a b = TApp tc [a, b]
doFixity mk f1 x y =
case compareFixity f1 f2 of
FCLeft -> return (o2 t z)
FCRight -> do r <- mkTInfix y op z
return (mk [x,r])
return (mk x r)
-- As the fixity table is known, and this is a case where the fixity came
-- from that table, it's a real error if the fixities didn't work out.

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

@ -357,21 +357,9 @@ data Type n = TFun (Type n) (Type n) -- ^ @[8] -> [8]@
| TInfix (Type n) (Located n) Fixity (Type n) -- ^ @ ty + ty @
deriving (Eq, Show, Generic, NFData, Functor)
data Prop n = CFin (Type n) -- ^ @ fin x @
| CEqual (Type n) (Type n) -- ^ @ x == 10 @
| CNeq (Type n) (Type n) -- ^ @ x != 10 @
| CGeq (Type n) (Type n) -- ^ @ x >= 10 @
| CZero (Type n) -- ^ @ Zero a @
| CLogic (Type n) -- ^ @ Logic a @
| 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
deriving (Eq, Show, Generic, NFData, Functor)
-- | A 'Prop' is a 'Type' that represents a type constraint.
newtype Prop n = CType (Type n)
deriving (Eq, Show, Generic, NFData, Functor)
--------------------------------------------------------------------------------
@ -406,16 +394,6 @@ instance AddLoc (Type name) where
dropLoc (TLocated e _) = dropLoc e
dropLoc e = e
instance HasLoc (Prop name) where
getLoc (CLocated _ r) = Just r
getLoc _ = Nothing
instance AddLoc (Prop name) where
addLoc = CLocated
dropLoc (CLocated e _) = dropLoc e
dropLoc e = e
instance AddLoc (Pattern name) where
addLoc = PLocated
@ -851,22 +829,7 @@ instance PPName name => PP (Type name) where
isInfix _ = Nothing
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
CLiteral t1 t2 -> text "Literal" <+> ppPrec 4 t1 <+> ppPrec 4 t2
CEqual t1 t2 -> ppPrec 2 t1 <+> text "==" <+> ppPrec 2 t2
CNeq 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
ppPrec n (CType t) = ppPrec n t
--------------------------------------------------------------------------------
@ -1037,18 +1000,4 @@ instance NoPos (Type name) where
TInfix x y f z-> TInfix (noPos x) y f (noPos z)
instance NoPos (Prop name) where
noPos prop =
case prop of
CEqual x y -> CEqual (noPos x) (noPos y)
CNeq x y -> CNeq (noPos x) (noPos y)
CGeq x y -> CGeq (noPos x) (noPos y)
CFin x -> CFin (noPos x)
CZero x -> CZero (noPos x)
CLogic x -> CLogic (noPos x)
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)
noPos (CType t) = CType (noPos t)

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

@ -174,18 +174,6 @@ namesT vs = go
namesC :: Ord name => Set name -> Prop name -> Set name
namesC vs prop =
case prop of
CFin t -> namesT vs t
CEqual t1 t2 -> Set.union (namesT vs t1) (namesT vs t2)
CNeq t1 t2 -> Set.union (namesT vs t1) (namesT vs t2)
CGeq t1 t2 -> Set.union (namesT vs t1) (namesT vs t2)
CZero t -> namesT vs t
CLogic t -> namesT vs t
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
-- | The type names defined and used by a group of mutually recursive declarations.
@ -290,18 +278,6 @@ 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)
CNeq 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.

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

@ -548,8 +548,8 @@ mkProp ty =
props r t =
case t of
TInfix{} -> infixProp t
TUser f xs -> prefixProp r f xs
TInfix{} -> return [CType t]
TUser{} -> return [CType t]
TTuple ts -> concat `fmap` mapM (props r) ts
TParens t' -> props r t'
TLocated t' r' -> props r' t'
@ -566,32 +566,6 @@ mkProp ty =
where
err = errorMessage r "Invalid constraint"
-- we have to delay these until renaming, when we have the fixity table
-- present
infixProp t = return [CType t]
-- these can be translated right away
prefixProp r f xs
| i == zeroIdent, [x] <- xs = return [CLocated (CZero x) r]
| i == logicIdent, [x] <- xs = return [CLocated (CLogic x) r]
| i == arithIdent, [x] <- xs = return [CLocated (CArith x) r]
| 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, 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 ->
([Located Import], [TopDecl PName]) ->

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

@ -399,21 +399,7 @@ doCheckType ty k =
-- | Validate a parsed proposition.
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.CNeq t1 t2 -> tcon (PC PNeq) [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 ts -> checkTUser x ts (Just KProp)
P.CLocated p r1 -> kInRange r1 (checkProp p)
P.CType _ -> panic "checkProp" [ "Unexpected CType", show prop ]
checkProp (P.CType t) = doCheckType t (Just KProp)
-- | Check that a type has the expected kind.