Merge pull request #627 from GaloisInc/infix-type

Infix type synonyms

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.
  */

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) (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)

src/Cryptol/ModuleSystem/Renamer.hs

@@ -35,11 +35,11 @@ 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
 
 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 +617,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'
@@ -635,19 +635,15 @@ 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]
       | Just pt <- primTyFromTC tc
       , 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 =
@@ -665,33 +661,22 @@ 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
   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.
@@ -993,20 +978,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
 

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) }

src/Cryptol/Parser/AST.hs

@@ -31,6 +31,10 @@ module Cryptol.Parser.AST
   , Kind(..)
   , Type(..)
   , Prop(..)
+  , tsName
+  , psName
+  , tsFixity
+  , psFixity
 
     -- * Declarations
   , Module(..)
@@ -182,12 +186,26 @@ 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
+
+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
@@ -599,11 +617,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 +938,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 =

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)))
 

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