From c0914c96df6046009c4a2d0b587ef781eb5a79db Mon Sep 17 00:00:00 2001 From: Brian Huffman Date: Wed, 26 Jun 2019 15:08:48 -0700 Subject: [PATCH 1/9] Add fixity field to TySyn and PropSyn datatypes. --- src/Cryptol/ModuleSystem/NamingEnv.hs | 4 ++-- src/Cryptol/ModuleSystem/Renamer.hs | 6 ++++-- src/Cryptol/Parser/AST.hs | 25 ++++++++++++++++++------- src/Cryptol/Parser/Names.hs | 12 ++++-------- src/Cryptol/Parser/ParserUtils.hs | 4 ++-- src/Cryptol/TypeCheck/Depends.hs | 14 +++++++------- src/Cryptol/TypeCheck/Kind.hs | 4 ++-- 7 files changed, 39 insertions(+), 30 deletions(-) diff --git a/src/Cryptol/ModuleSystem/NamingEnv.hs b/src/Cryptol/ModuleSystem/NamingEnv.hs index 7578dd924..89a15b2d3 100644 --- a/src/Cryptol/ModuleSystem/NamingEnv.hs +++ b/src/Cryptol/ModuleSystem/NamingEnv.hs @@ -369,8 +369,8 @@ instance BindsNames (InModule (Decl PName)) where DSignature ns _sig -> foldMap qualBind ns DPragma ns _p -> foldMap qualBind ns - DType (TySyn lqn _ _) -> qualType lqn - DProp (PropSyn lqn _ _) -> qualType lqn + DType syn -> qualType (tsName syn) + DProp syn -> qualType (psName syn) DLocated d' _ -> namingEnv (InModule pfx d') DPatBind _pat _e -> panic "ModuleSystem" ["Unexpected pattern binding"] DFixity{} -> panic "ModuleSystem" ["Unexpected fixity declaration"] diff --git a/src/Cryptol/ModuleSystem/Renamer.hs b/src/Cryptol/ModuleSystem/Renamer.hs index f9a9ba1c9..eb2b74e2f 100644 --- a/src/Cryptol/ModuleSystem/Renamer.hs +++ b/src/Cryptol/ModuleSystem/Renamer.hs @@ -993,20 +993,22 @@ instance Rename Match where MatchLet b -> shadowNamesNS b (MatchLet <$> rename b) instance Rename TySyn where - rename (TySyn n ps ty) = + rename (TySyn n f ps ty) = do when (isReserved (thing n)) (record (BoundReservedType (thing n) (getLoc n) (text "type synonym"))) shadowNames ps $ TySyn <$> rnLocated renameType n + <*> pure f <*> traverse rename ps <*> rename ty instance Rename PropSyn where - rename (PropSyn n ps cs) = + rename (PropSyn n f ps cs) = do when (isReserved (thing n)) (record (BoundReservedType (thing n) (getLoc n) (text "constraint synonym"))) shadowNames ps $ PropSyn <$> rnLocated renameType n + <*> pure f <*> traverse rename ps <*> traverse rename cs diff --git a/src/Cryptol/Parser/AST.hs b/src/Cryptol/Parser/AST.hs index 5199f4c5a..f4c0f3bfe 100644 --- a/src/Cryptol/Parser/AST.hs +++ b/src/Cryptol/Parser/AST.hs @@ -31,6 +31,8 @@ module Cryptol.Parser.AST , Kind(..) , Type(..) , Prop(..) + , tsName + , psName -- * Declarations , Module(..) @@ -182,12 +184,20 @@ data ImportSpec = Hiding [Ident] | Only [Ident] deriving (Eq, Show, Generic, NFData) -data TySyn n = TySyn (Located n) [TParam n] (Type n) +-- The 'Maybe Fixity' field is filled in by the NoPat pass. +data TySyn n = TySyn (Located n) (Maybe Fixity) [TParam n] (Type n) deriving (Eq, Show, Generic, NFData, Functor) -data PropSyn n = PropSyn (Located n) [TParam n] [Prop n] +-- The 'Maybe Fixity' field is filled in by the NoPat pass. +data PropSyn n = PropSyn (Located n) (Maybe Fixity) [TParam n] [Prop n] deriving (Eq, Show, Generic, NFData, Functor) +tsName :: TySyn name -> Located name +tsName (TySyn lqn _ _ _) = lqn + +psName :: PropSyn name -> Located name +psName (PropSyn lqn _ _ _) = lqn + {- | Bindings. Notes: * The parser does not associate type signatures and pragmas with @@ -599,11 +609,12 @@ instance (Show name, PPName name) => PP (BindDef name) where instance PPName name => PP (TySyn name) where - ppPrec _ (TySyn x xs t) = text "type" <+> ppL x <+> fsep (map (ppPrec 1) xs) - <+> text "=" <+> pp t + ppPrec _ (TySyn x _ xs t) = + text "type" <+> ppL x <+> fsep (map (ppPrec 1) xs) + <+> text "=" <+> pp t instance PPName name => PP (PropSyn name) where - ppPrec _ (PropSyn x xs ps) = + ppPrec _ (PropSyn x _ xs ps) = text "constraint" <+> ppL x <+> fsep (map (ppPrec 1) xs) <+> text "=" <+> parens (commaSep (map pp ps)) @@ -919,10 +930,10 @@ instance NoPos Pragma where instance NoPos (TySyn name) where - noPos (TySyn x y z) = TySyn (noPos x) (noPos y) (noPos z) + noPos (TySyn x f y z) = TySyn (noPos x) f (noPos y) (noPos z) instance NoPos (PropSyn name) where - noPos (PropSyn x y z) = PropSyn (noPos x) (noPos y) (noPos z) + noPos (PropSyn x f y z) = PropSyn (noPos x) f (noPos y) (noPos z) instance NoPos (Expr name) where noPos expr = diff --git a/src/Cryptol/Parser/Names.hs b/src/Cryptol/Parser/Names.hs index 6d4ae01d9..b5feaa1c3 100644 --- a/src/Cryptol/Parser/Names.hs +++ b/src/Cryptol/Parser/Names.hs @@ -57,12 +57,6 @@ allNamesD decl = DProp ps -> [psName ps] DLocated d _ -> allNamesD d -tsName :: TySyn name -> Located name -tsName (TySyn lqn _ _) = lqn - -psName :: PropSyn name -> Located name -psName (PropSyn lqn _ _) = lqn - -- | The names defined and used by a single binding. namesB :: Ord name => Bind name -> ([Located name], Set name) namesB b = ([bName b], boundNames (namesPs (bParams b)) (namesDef (thing (bDef b)))) @@ -193,8 +187,10 @@ tnamesD decl = DBind b -> ([], tnamesB b) DPatBind _ e -> ([], tnamesE e) DLocated d _ -> tnamesD d - DType (TySyn n ps t) -> ([n], Set.difference (tnamesT t) (Set.fromList (map tpName ps))) - DProp (PropSyn n ps cs) + DType (TySyn n _ ps t) + -> ([n], Set.difference (tnamesT t) + (Set.fromList (map tpName ps))) + DProp (PropSyn n _ ps cs) -> ([n], Set.difference (Set.unions (map tnamesC cs)) (Set.fromList (map tpName ps))) diff --git a/src/Cryptol/Parser/ParserUtils.hs b/src/Cryptol/Parser/ParserUtils.hs index 83fd9bed7..c055ab12d 100644 --- a/src/Cryptol/Parser/ParserUtils.hs +++ b/src/Cryptol/Parser/ParserUtils.hs @@ -377,7 +377,7 @@ mkTySyn ln ps b errorMessage (srcRange ln) "`width` is not a valid type synonym name." | otherwise = - return $ DType $ TySyn ln ps b + return $ DType $ TySyn ln Nothing ps b mkPropSyn :: Located PName -> [TParam PName] -> Type PName -> ParseM (Decl PName) mkPropSyn ln ps b @@ -385,7 +385,7 @@ mkPropSyn ln ps b errorMessage (srcRange ln) "`width` is not a valid constraint synonym name." | otherwise = - DProp . PropSyn ln ps . thing <$> mkProp b + DProp . PropSyn ln Nothing ps . thing <$> mkProp b polyTerm :: Range -> Integer -> Integer -> ParseM (Bool, Integer) polyTerm rng k p diff --git a/src/Cryptol/TypeCheck/Depends.hs b/src/Cryptol/TypeCheck/Depends.hs index ca66e1ff3..439485600 100644 --- a/src/Cryptol/TypeCheck/Depends.hs +++ b/src/Cryptol/TypeCheck/Depends.hs @@ -72,7 +72,7 @@ orderTyDecls ts = } ) - toMap vs ty@(TS (P.TySyn x as t) _) = + toMap vs ty@(TS (P.TySyn x _ as t) _) = (thing x , x { thing = (ty, Set.toList $ Set.difference (namesT vs t) @@ -80,18 +80,18 @@ orderTyDecls ts = } ) - toMap vs ty@(PS (P.PropSyn x as ps) _) = + toMap vs ty@(PS (P.PropSyn x _ as ps) _) = (thing x , x { thing = (ty, Set.toList $ Set.difference (Set.unions (map (namesC vs) ps)) (Set.fromList (map P.tpName as))) } ) - getN (TS (P.TySyn x _ _) _) = thing x - getN (PS (P.PropSyn x _ _) _) = thing x - getN (NT x _) = thing (P.nName x) - getN (AT x _) = thing (P.ptName x) - getN (PT x _) = thing (P.primTName x) + getN (TS x _) = thing (P.tsName x) + getN (PS x _) = thing (P.psName x) + getN (NT x _) = thing (P.nName x) + getN (AT x _) = thing (P.ptName x) + getN (PT x _) = thing (P.primTName x) check (AcyclicSCC x) = return [x] diff --git a/src/Cryptol/TypeCheck/Kind.hs b/src/Cryptol/TypeCheck/Kind.hs index efe414be4..b4dcb1523 100644 --- a/src/Cryptol/TypeCheck/Kind.hs +++ b/src/Cryptol/TypeCheck/Kind.hs @@ -75,7 +75,7 @@ checkParameterType a mbDoc = -- | Check a type-synonym declaration. checkTySyn :: P.TySyn Name -> Maybe String -> InferM TySyn -checkTySyn (P.TySyn x as t) mbD = +checkTySyn (P.TySyn x _ as t) mbD = do ((as1,t1),gs) <- collectGoals $ inRange (srcRange x) $ do r <- withTParams NoWildCards tySynParam as @@ -91,7 +91,7 @@ checkTySyn (P.TySyn x as t) mbD = -- | Check a constraint-synonym declaration. checkPropSyn :: P.PropSyn Name -> Maybe String -> InferM TySyn -checkPropSyn (P.PropSyn x as ps) mbD = +checkPropSyn (P.PropSyn x _ as ps) mbD = do ((as1,t1),gs) <- collectGoals $ inRange (srcRange x) $ do r <- withTParams NoWildCards propSynParam as From 019d2af088d8420f4179f73b79e3aa1aee1c7425 Mon Sep 17 00:00:00 2001 From: Brian Huffman Date: Wed, 26 Jun 2019 15:20:00 -0700 Subject: [PATCH 2/9] NoPat pass annotates type/constraint synonyms with fixities. --- src/Cryptol/Parser/NoPat.hs | 81 ++++++++++++++++++++++++------------- 1 file changed, 53 insertions(+), 28 deletions(-) diff --git a/src/Cryptol/Parser/NoPat.hs b/src/Cryptol/Parser/NoPat.hs index 8d782ccfe..e7fa6a8f7 100644 --- a/src/Cryptol/Parser/NoPat.hs +++ b/src/Cryptol/Parser/NoPat.hs @@ -245,8 +245,8 @@ noPatDs ds = let pragmaMap = Map.fromListWith (++) $ concatMap toPragma ds1 sigMap = Map.fromListWith (++) $ concatMap toSig ds1 fixMap = Map.fromListWith (++) $ concatMap toFixity ds1 - (ds2, (pMap,sMap,fMap,_)) <- runStateT (pragmaMap, sigMap, fixMap, Map.empty) - (annotDs ds1) + (ds2, (pMap,sMap,fMap,tMap,_)) <- + runStateT (pragmaMap, sigMap, fixMap, fixMap, Map.empty) (annotDs ds1) forM_ (Map.toList pMap) $ \(n,ps) -> forM_ ps $ \p -> recordError $ PragmaNoBind (p { thing = n }) (thing p) @@ -256,7 +256,9 @@ noPatDs ds = forM_ ss $ \s -> recordError $ SignatureNoBind (s { thing = n }) (thing s) - forM_ (Map.toList fMap) $ \(n,fs) -> + -- Generate an error if a fixity declaration is not used for + -- either a value-level or type-level operator. + forM_ (Map.toList (Map.intersection fMap tMap)) $ \(n,fs) -> forM_ fs $ \f -> recordError $ FixityNoBind f { thing = n } return ds2 @@ -273,8 +275,8 @@ noPatTopDs tds = fixMap = Map.fromListWith (++) $ concatMap toFixity allDecls docMap = Map.fromListWith (++) $ concatMap toDocs (decls tds) - (tds', (pMap,sMap,fMap,_)) <- runStateT (pragmaMap,sigMap,fixMap,docMap) - (annotTopDs desugared) + (tds', (pMap,sMap,fMap,tMap,_)) <- + runStateT (pragmaMap,sigMap,fixMap,fixMap,docMap) (annotTopDs desugared) forM_ (Map.toList pMap) $ \(n,ps) -> forM_ ps $ \p -> recordError $ PragmaNoBind (p { thing = n }) (thing p) @@ -284,7 +286,9 @@ noPatTopDs tds = forM_ ss $ \s -> recordError $ SignatureNoBind (s { thing = n }) (thing s) - forM_ (Map.toList fMap) $ \(n,fs) -> + -- Generate an error if a fixity declaration is not used for + -- either a value-level or type-level operator. + forM_ (Map.toList (Map.intersection fMap tMap)) $ \(n,fs) -> forM_ fs $ \f -> recordError $ FixityNoBind f { thing = n } return tds' @@ -311,7 +315,8 @@ noPatModule m = type AnnotMap = ( Map.Map PName [Located Pragma ] , Map.Map PName [Located (Schema PName)] - , Map.Map PName [Located Fixity ] + , Map.Map PName [Located Fixity ] -- for expressions + , Map.Map PName [Located Fixity ] -- for types , Map.Map PName [Located String ] ) @@ -340,14 +345,14 @@ annotTopDs tds = DParameterType {} -> (d :) <$> annotTopDs ds DParameterConstraint {} -> (d :) <$> annotTopDs ds DParameterFun p -> - do (ps,ss,fs,ds') <- get + do (ps,ss,fs,ts,ds') <- get let rm _ _ = Nothing name = thing (pfName p) case Map.updateLookupWithKey rm name fs of (Nothing,_) -> (d :) <$> annotTopDs ds (Just f,fs1) -> do mbF <- lift (checkFixs name f) - set (ps,ss,fs1,ds') + set (ps,ss,fs1,ts,ds') let p1 = p { pfFixity = mbF } (DParameterFun p1 :) <$> annotTopDs ds @@ -377,34 +382,54 @@ annotD decl = DFixity{} -> raise () DPragma {} -> raise () DPatBind {} -> raise () - DType {} -> return decl - DProp {} -> return decl + DType tysyn -> DType <$> lift (annotTySyn tysyn) + DProp propsyn -> DProp <$> lift (annotPropSyn propsyn) DLocated d r -> (`DLocated` r) <$> annotD d -- | Add pragma/signature annotations to a binding. annotB :: Bind PName -> StateT AnnotMap NoPatM (Bind PName) annotB Bind { .. } = - do (ps,ss,fs,ds) <- get + do (ps,ss,fs,ts,ds) <- get let name = thing bName remove _ _ = Nothing - case ( Map.updateLookupWithKey remove name ps - , Map.updateLookupWithKey remove name ss - , Map.updateLookupWithKey remove name fs - , Map.updateLookupWithKey remove name ds - ) of - ( (thisPs, pragmas1), (thisSigs, sigs1), (thisFixes, fixes1), (thisDocs, docs1)) -> - do s <- lift $ checkSigs name (jn thisSigs) - f <- lift $ checkFixs name (jn thisFixes) - d <- lift $ checkDocs name (jn thisDocs) - set (pragmas1,sigs1,fixes1,docs1) - return Bind { bSignature = s - , bPragmas = map thing (jn thisPs) ++ bPragmas - , bFixity = f - , bDoc = d - , .. - } + (thisPs , ps') = Map.updateLookupWithKey remove name ps + (thisSigs , ss') = Map.updateLookupWithKey remove name ss + (thisFixes , fs') = Map.updateLookupWithKey remove name fs + (thisDocs , ds') = Map.updateLookupWithKey remove name ds + s <- lift $ checkSigs name (jn thisSigs) + f <- lift $ checkFixs name (jn thisFixes) + d <- lift $ checkDocs name (jn thisDocs) + set (ps',ss',fs',ts,ds') + return Bind { bSignature = s + , bPragmas = map thing (jn thisPs) ++ bPragmas + , bFixity = f + , bDoc = d + , .. + } where jn x = concat (maybeToList x) +-- | Add fixity annotations to a type synonym binding. +annotTySyn :: TySyn PName -> StateT AnnotMap NoPatM (TySyn PName) +annotTySyn (TySyn ln _ params rhs) = + do (ps,ss,fs,ts,ds) <- get + let name = thing ln + remove _ _ = Nothing + (thisFixes, ts') = Map.updateLookupWithKey remove name ts + f <- lift $ checkFixs name (concat (maybeToList thisFixes)) + set (ps,ss,fs,ts',ds) + return (TySyn ln f params rhs) + +-- | Add fixity annotations to a constraint synonym binding. +annotPropSyn :: PropSyn PName -> StateT AnnotMap NoPatM (PropSyn PName) +annotPropSyn (PropSyn ln _ params rhs) = + do (ps,ss,fs,ts,ds) <- get + let name = thing ln + remove _ _ = Nothing + (thisFixes, ts') = Map.updateLookupWithKey remove name ts + f <- lift $ checkFixs name (concat (maybeToList thisFixes)) + set (ps,ss,fs,ts',ds) + return (PropSyn ln f params rhs) + -- | Check for multiple signatures. checkSigs :: PName -> [Located (Schema PName)] -> NoPatM (Maybe (Schema PName)) checkSigs _ [] = return Nothing From da1c509ffd06a9ab99514b9298643dadab4cfbf5 Mon Sep 17 00:00:00 2001 From: Brian Huffman Date: Wed, 26 Jun 2019 16:54:40 -0700 Subject: [PATCH 3/9] Propagate fixities from type declarations into the NamingEnv. --- src/Cryptol/ModuleSystem/NamingEnv.hs | 8 ++++---- src/Cryptol/Parser/AST.hs | 8 ++++++++ 2 files changed, 12 insertions(+), 4 deletions(-) diff --git a/src/Cryptol/ModuleSystem/NamingEnv.hs b/src/Cryptol/ModuleSystem/NamingEnv.hs index 89a15b2d3..3e6ac14c6 100644 --- a/src/Cryptol/ModuleSystem/NamingEnv.hs +++ b/src/Cryptol/ModuleSystem/NamingEnv.hs @@ -369,8 +369,8 @@ instance BindsNames (InModule (Decl PName)) where DSignature ns _sig -> foldMap qualBind ns DPragma ns _p -> foldMap qualBind ns - DType syn -> qualType (tsName syn) - DProp syn -> qualType (psName syn) + DType syn -> qualType (tsName syn) (tsFixity syn) + DProp syn -> qualType (psName syn) (psFixity syn) DLocated d' _ -> namingEnv (InModule pfx d') DPatBind _pat _e -> panic "ModuleSystem" ["Unexpected pattern binding"] DFixity{} -> panic "ModuleSystem" ["Unexpected fixity declaration"] @@ -383,6 +383,6 @@ instance BindsNames (InModule (Decl PName)) where do n <- mkName ln Nothing return (singletonE (thing ln) n) - qualType ln = BuildNamingEnv $ - do n <- mkName ln Nothing + qualType ln f = BuildNamingEnv $ + do n <- mkName ln f return (singletonT (thing ln) n) diff --git a/src/Cryptol/Parser/AST.hs b/src/Cryptol/Parser/AST.hs index f4c0f3bfe..365f4a693 100644 --- a/src/Cryptol/Parser/AST.hs +++ b/src/Cryptol/Parser/AST.hs @@ -33,6 +33,8 @@ module Cryptol.Parser.AST , Prop(..) , tsName , psName + , tsFixity + , psFixity -- * Declarations , Module(..) @@ -198,6 +200,12 @@ tsName (TySyn lqn _ _ _) = lqn psName :: PropSyn name -> Located name psName (PropSyn lqn _ _ _) = lqn +tsFixity :: TySyn name -> Maybe Fixity +tsFixity (TySyn _ f _ _) = f + +psFixity :: PropSyn name -> Maybe Fixity +psFixity (PropSyn _ f _ _) = f + {- | Bindings. Notes: * The parser does not associate type signatures and pragmas with From b54e4835ac88c3dec46cd259463c51492456241c Mon Sep 17 00:00:00 2001 From: Brian Huffman Date: Wed, 26 Jun 2019 17:29:55 -0700 Subject: [PATCH 4/9] Make kind checker accept TInfix constructors from the renamer. --- src/Cryptol/TypeCheck/Kind.hs | 4 +--- 1 file changed, 1 insertion(+), 3 deletions(-) diff --git a/src/Cryptol/TypeCheck/Kind.hs b/src/Cryptol/TypeCheck/Kind.hs index b4dcb1523..8c4ddc09e 100644 --- a/src/Cryptol/TypeCheck/Kind.hs +++ b/src/Cryptol/TypeCheck/Kind.hs @@ -385,9 +385,7 @@ doCheckType ty k = P.TParens t -> doCheckType t k - P.TInfix{} -> panic "KindCheck" - [ "TInfix not removed by the renamer", show ty ] - + P.TInfix t x _ u-> doCheckType (P.TUser (thing x) [t, u]) k where checkF f = do t <- kInRange (srcRange (name f)) From eadaf4473e384880e81090213fa5d36e2295c233 Mon Sep 17 00:00:00 2001 From: Brian Huffman Date: Wed, 26 Jun 2019 17:35:19 -0700 Subject: [PATCH 5/9] Add parser rules for infix type/constraint synonyms. --- src/Cryptol/Parser.y | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/src/Cryptol/Parser.y b/src/Cryptol/Parser.y index 9e4ec637c..bd9f5ccc3 100644 --- a/src/Cryptol/Parser.y +++ b/src/Cryptol/Parser.y @@ -303,11 +303,15 @@ decl :: { Decl PName } | 'type' name '=' type {% at ($1,$4) `fmap` mkTySyn $2 [] $4 } | 'type' name tysyn_params '=' type {% at ($1,$5) `fmap` mkTySyn $2 (reverse $3) $5 } + | 'type' tysyn_param op tysyn_param '=' type + {% at ($1,$6) `fmap` mkTySyn $3 [$2, $4] $6 } | 'type' 'constraint' name '=' type {% at ($2,$5) `fmap` mkPropSyn $3 [] $5 } | 'type' 'constraint' name tysyn_params '=' type {% at ($2,$6) `fmap` mkPropSyn $3 (reverse $4) $6 } + | 'type' 'constraint' tysyn_param op tysyn_param '=' type + {% at ($2,$7) `fmap` mkPropSyn $4 [$3, $5] $7 } | 'infixl' NUM ops {% mkFixity LeftAssoc $2 (reverse $3) } | 'infixr' NUM ops {% mkFixity RightAssoc $2 (reverse $3) } From fb86b1538c069a99b3e7ae5b06c6387b6a9ec7a8 Mon Sep 17 00:00:00 2001 From: Brian Huffman Date: Wed, 26 Jun 2019 17:36:46 -0700 Subject: [PATCH 6/9] Renamer looks up type operator fixities in the NamingEnv. Primitive infix type operators are looked up in a hard-coded table; everything else is looked up in the NamingEnv. --- src/Cryptol/ModuleSystem/Renamer.hs | 18 +++++++++++------- 1 file changed, 11 insertions(+), 7 deletions(-) diff --git a/src/Cryptol/ModuleSystem/Renamer.hs b/src/Cryptol/ModuleSystem/Renamer.hs index eb2b74e2f..c1254b688 100644 --- a/src/Cryptol/ModuleSystem/Renamer.hs +++ b/src/Cryptol/ModuleSystem/Renamer.hs @@ -40,6 +40,7 @@ import Cryptol.Utils.Panic (panic) import Cryptol.Utils.PP import Data.List(find) +import Data.Maybe (fromMaybe) import qualified Data.Foldable as F import Data.Map.Strict ( Map ) import qualified Data.Map.Strict as Map @@ -617,7 +618,7 @@ resolveTypeFixity = go TParens t' -> TParens <$> go t' TInfix a o _ b -> - do let op = lookupFixity o + do op <- lookupFixity o a' <- go a b' <- go b mkTInfix a' op b' @@ -640,6 +641,8 @@ mkTInfix t op@(o2,f2) z = -- 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 + TInfix x ln f1 y -> + doFixity (\a b -> TInfix a ln f1 b) f1 x y TApp tc [x,y] | Just pt <- primTyFromTC tc , Just f1 <- primTyFixity pt -> doFixity (mkBin tc) f1 x y @@ -665,15 +668,16 @@ mkTInfix t op@(o2,f2) z = -- | When possible, rewrite the type operator to a known constructor, otherwise -- return a 'TOp' that reconstructs the original term, and a default fixity. -lookupFixity :: Located PName -> (TOp,Fixity) +lookupFixity :: Located PName -> RenameM (TOp, Fixity) lookupFixity op = case lkp of - Just res -> res + Just res -> return res - -- unknown type operator, just use default fixity - -- NOTE: this works for the props defined above, as all other operators - -- are defined with a higher precedence. - Nothing -> (\x y -> TUser sym [x,y], Fixity NonAssoc 0) + -- Not a primitive type operator; look up fixity in naming environment + Nothing -> + do n <- renameType sym + let fi = fromMaybe defaultFixity (nameFixity n) + return (\x y -> TInfix x op fi y, fi) where sym = thing op From 17c47c4ac0a5f627bfbfb807fc75ac9979d8c282 Mon Sep 17 00:00:00 2001 From: Brian Huffman Date: Wed, 26 Jun 2019 17:54:40 -0700 Subject: [PATCH 7/9] Update type pretty-printer to handle infix type synonyms. --- src/Cryptol/TypeCheck/Type.hs | 20 +++++++++++++++----- 1 file changed, 15 insertions(+), 5 deletions(-) diff --git a/src/Cryptol/TypeCheck/Type.hs b/src/Cryptol/TypeCheck/Type.hs index d1343889b..e7a880c65 100644 --- a/src/Cryptol/TypeCheck/Type.hs +++ b/src/Cryptol/TypeCheck/Type.hs @@ -754,6 +754,10 @@ instance PP (WithNames Type) where TVar a -> ppWithNames nmMap a TRec fs -> braces $ fsep $ punctuate comma [ pp l <+> text ":" <+> go 0 t | (l,t) <- fs ] + + _ | Just tinf <- isTInfix ty0 -> optParens (prec > 2) + $ ppInfix 2 isTInfix tinf + TUser c [] _ -> pp c TUser c ts _ -> optParens (prec > 3) $ pp c <+> fsep (map (go 4) ts) -- TUser _ _ t -> ppPrec prec t -- optParens (prec > 3) $ pp c <+> fsep (map (go 4) ts) @@ -793,22 +797,28 @@ instance PP (WithNames Type) where (_, _) -> pp pc <+> fsep (map (go 4) ts) - _ | Just tinf <- isTInfix ty0 -> optParens (prec > 2) - $ ppInfix 2 isTInfix tinf - TCon f ts -> optParens (prec > 3) $ pp f <+> fsep (map (go 4) ts) where go p t = ppWithNamesPrec nmMap p t - isTInfix (WithNames (TCon (TF ieOp) [ieLeft',ieRight']) _) = + isTInfix (WithNames (TCon (TF tf) [ieLeft',ieRight']) _) = do let ieLeft = WithNames ieLeft' nmMap ieRight = WithNames ieRight' nmMap - pt <- primTyFromTF ieOp + pt <- primTyFromTF tf fi <- primTyFixity pt let ieAssoc = fAssoc fi iePrec = fLevel fi + ieOp = primTyIdent pt + return Infix { .. } + isTInfix (WithNames (TUser n [ieLeft',ieRight'] _) _) = + do let ieLeft = WithNames ieLeft' nmMap + ieRight = WithNames ieRight' nmMap + fi <- nameFixity n + let ieAssoc = fAssoc fi + iePrec = fLevel fi + ieOp = nameIdent n return Infix { .. } isTInfix _ = Nothing From 10da255fd18af7956b627e4863e29b14d6120d19 Mon Sep 17 00:00:00 2001 From: Brian Huffman Date: Wed, 26 Jun 2019 18:04:16 -0700 Subject: [PATCH 8/9] Re-implement infix type constraint (<=) as a constraint synonym. Also removed special-case hack for (<=) in the renamer. Also adapted test case output to account for the new prelude declaration. --- lib/Cryptol.cry | 5 +++++ src/Cryptol/ModuleSystem/Renamer.hs | 19 ------------------- tests/issues/T146.icry.stdout | 16 ++++++++-------- tests/issues/issue226.icry.stdout | 4 ++++ tests/issues/issue290v2.icry.stdout | 4 ++-- 5 files changed, 19 insertions(+), 29 deletions(-) diff --git a/lib/Cryptol.cry b/lib/Cryptol.cry index 78dcde991..b6c78554c 100644 --- a/lib/Cryptol.cry +++ b/lib/Cryptol.cry @@ -5,6 +5,11 @@ module Cryptol where +/** + * Assert that the first numeric type is less than or equal to the second. + */ +type constraint i <= j = (j >= i) + /** * The value corresponding to a numeric type. */ diff --git a/src/Cryptol/ModuleSystem/Renamer.hs b/src/Cryptol/ModuleSystem/Renamer.hs index c1254b688..6bc692a13 100644 --- a/src/Cryptol/ModuleSystem/Renamer.hs +++ b/src/Cryptol/ModuleSystem/Renamer.hs @@ -35,7 +35,6 @@ import Cryptol.Prims.Syntax import Cryptol.Parser.AST import Cryptol.Parser.Position import Cryptol.Parser.Selector(ppNestedSels,selName) -import Cryptol.Utils.Ident (packInfix) import Cryptol.Utils.Panic (panic) import Cryptol.Utils.PP @@ -636,11 +635,6 @@ mkTInfix :: Type PName -> (TOp,Fixity) -> Type PName -> RenameM (Type PName) mkTInfix t op@(o2,f2) z = case t of TLocated t1 _ -> mkTInfix t1 op z - - -- 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 TInfix x ln f1 y -> doFixity (\a b -> TInfix a ln f1 b) f1 x y TApp tc [x,y] @@ -650,7 +644,6 @@ mkTInfix t op@(o2,f2) z = _ -> 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 = @@ -684,18 +677,6 @@ lookupFixity op = lkp = do pt <- primTyFromPName (thing op) fi <- primTyFixity pt return (\x y -> TApp (primTyCon pt) [x,y], fi) - `mplus` - do guard (isLeq sym) - return (\x y -> TUser sym [x,y], leqFixity) - -leqFixity :: Fixity -leqFixity = Fixity NonAssoc 30 - -leqIdent :: Ident -leqIdent = packInfix "<=" - -isLeq :: PName -> Bool -isLeq x = getIdent x == leqIdent -- | Rename a binding. diff --git a/tests/issues/T146.icry.stdout b/tests/issues/T146.icry.stdout index 52b3c8e23..cb671f978 100644 --- a/tests/issues/T146.icry.stdout +++ b/tests/issues/T146.icry.stdout @@ -3,14 +3,14 @@ Loading module Cryptol Loading module Main [error] at ./T146.cry:1:18--6:10: - The type ?fv`868 is not sufficiently polymorphic. - It cannot depend on quantified variables: fv`852 + The type ?fv`870 is not sufficiently polymorphic. + It cannot depend on quantified variables: fv`854 where - ?fv`868 is type argument 'fv' of 'Main::ec_v1' at ./T146.cry:4:19--4:24 - fv`852 is signature variable 'fv' at ./T146.cry:11:10--11:12 + ?fv`870 is type argument 'fv' of 'Main::ec_v1' at ./T146.cry:4:19--4:24 + fv`854 is signature variable 'fv' at ./T146.cry:11:10--11:12 [error] at ./T146.cry:5:19--5:24: - The type ?fv`870 is not sufficiently polymorphic. - It cannot depend on quantified variables: fv`852 + The type ?fv`872 is not sufficiently polymorphic. + It cannot depend on quantified variables: fv`854 where - ?fv`870 is type argument 'fv' of 'Main::ec_v2' at ./T146.cry:5:19--5:24 - fv`852 is signature variable 'fv' at ./T146.cry:11:10--11:12 + ?fv`872 is type argument 'fv' of 'Main::ec_v2' at ./T146.cry:5:19--5:24 + fv`854 is signature variable 'fv' at ./T146.cry:11:10--11:12 diff --git a/tests/issues/issue226.icry.stdout b/tests/issues/issue226.icry.stdout index 482c91082..73aaf3a64 100644 --- a/tests/issues/issue226.icry.stdout +++ b/tests/issues/issue226.icry.stdout @@ -10,6 +10,10 @@ Type Synonyms type String n = [n][8] type Word n = [n] +Constraint Synonyms +=================== + type constraint (<=) i j = j >= i + Symbols ======= (==>) : Bit -> Bit -> Bit diff --git a/tests/issues/issue290v2.icry.stdout b/tests/issues/issue290v2.icry.stdout index 20c3d02e9..a25e2656c 100644 --- a/tests/issues/issue290v2.icry.stdout +++ b/tests/issues/issue290v2.icry.stdout @@ -4,9 +4,9 @@ Loading module Main [error] at ./issue290v2.cry:2:1--2:19: Unsolved constraints: - • n`849 == 1 + • n`851 == 1 arising from checking a pattern: type of 1st argument of Main::minMax at ./issue290v2.cry:2:8--2:11 where - n`849 is signature variable 'n' at ./issue290v2.cry:1:11--1:12 + n`851 is signature variable 'n' at ./issue290v2.cry:1:11--1:12 From 14d25e8f9a4fcba72b12e49c2dd360c9a8dee19e Mon Sep 17 00:00:00 2001 From: Brian Huffman Date: Wed, 26 Jun 2019 18:19:12 -0700 Subject: [PATCH 9/9] Fix pretty printing for infix type/constraint synonyms. --- src/Cryptol/TypeCheck/Type.hs | 10 +++++++--- tests/issues/issue226.icry.stdout | 2 +- 2 files changed, 8 insertions(+), 4 deletions(-) diff --git a/src/Cryptol/TypeCheck/Type.hs b/src/Cryptol/TypeCheck/Type.hs index e7a880c65..d6ab2b1ea 100644 --- a/src/Cryptol/TypeCheck/Type.hs +++ b/src/Cryptol/TypeCheck/Type.hs @@ -731,13 +731,17 @@ instance PP TySyn where instance PP (WithNames TySyn) where ppPrec _ (WithNames ts ns) = - text "type" <+> ctr <+> pp (tsName ts) <+> - sep (map (ppWithNames ns1) (tsParams ts)) <+> char '=' - <+> ppWithNames ns1 (tsDef ts) + text "type" <+> ctr <+> lhs <+> char '=' <+> ppWithNames ns1 (tsDef ts) where ns1 = addTNames (tsParams ts) ns ctr = case kindResult (kindOf ts) of KProp -> text "constraint" _ -> empty + n = tsName ts + lhs = case (nameFixity n, tsParams ts) of + (Just _, [x, y]) -> + ppWithNames ns1 x <+> pp (nameIdent n) <+> ppWithNames ns1 y + (_, ps) -> + pp n <+> sep (map (ppWithNames ns1) ps) instance PP Newtype where ppPrec = ppWithNamesPrec IntMap.empty diff --git a/tests/issues/issue226.icry.stdout b/tests/issues/issue226.icry.stdout index 73aaf3a64..f8555ed84 100644 --- a/tests/issues/issue226.icry.stdout +++ b/tests/issues/issue226.icry.stdout @@ -12,7 +12,7 @@ Type Synonyms Constraint Synonyms =================== - type constraint (<=) i j = j >= i + type constraint i <= j = j >= i Symbols =======