No more rebindable syntax. Fixes #568.

When syntactic sugar for constants "negate", "complement" or "splitAt"
is used, the names of those primitives are now resolved during the
type checking phase. This makes them consistent with the handling of
other desugared primitives like "fromThen", etc.

src/Cryptol/ModuleSystem/Renamer.hs

@@ -34,7 +34,7 @@ import Cryptol.Prims.Syntax
 import Cryptol.Parser.AST
 import Cryptol.Parser.Position
 import Cryptol.TypeCheck.Type (TCon(..))
-import Cryptol.Utils.Ident (packInfix,packIdent)
+import Cryptol.Utils.Ident (packInfix)
 import Cryptol.Utils.Panic (panic)
 import Cryptol.Utils.PP
 
@@ -747,8 +747,9 @@ instance Rename Expr where
   rename expr = case expr of
     EVar n        -> EVar <$> renameVar n
     ELit l        -> return (ELit l)
-    ENeg e        -> rename (EApp (EVar (mkUnqual (packIdent "negate"))) e)
-    EComplement e -> rename (EApp (EVar (mkUnqual (packIdent "complement"))) e)
+    ENeg e        -> ENeg    <$> rename e
+    EComplement e -> EComplement
+                             <$> rename e
     ETuple es     -> ETuple  <$> traverse rename es
     ERecord fs    -> ERecord <$> traverse (rnNamed rename) fs
     ESel e' s     -> ESel    <$> rename e' <*> pure s
@@ -777,6 +778,7 @@ instance Rename Expr where
     ELocated e' r -> withLoc r
                    $ ELocated <$> rename e' <*> pure r
 
+    ESplit e      -> ESplit  <$> rename e
     EParens p     -> EParens <$> rename p
     EInfix x y _ z-> do op <- renameOp y
                         x' <- rename x

src/Cryptol/Parser/AST.hs

@@ -276,6 +276,7 @@ data Expr n   = EVar n                          -- ^ @ x @
               | EFun [Pattern n] (Expr n)       -- ^ @ \\x y -> x @
               | ELocated (Expr n) Range         -- ^ position annotation
 
+              | ESplit (Expr n)                 -- ^ @ splitAt x @ (Introduced by NoPat)
               | EParens (Expr n)                -- ^ @ (e)   @ (Removed by Fixity)
               | EInfix (Expr n) (Located n) Fixity (Expr n)-- ^ @ a + b @ (Removed by Fixity)
                 deriving (Eq, Show, Generic, NFData, Functor)
@@ -713,6 +714,8 @@ instance (Show name, PPName name) => PP (Expr name) where
 
       ELocated e _  -> ppPrec n e
 
+      ESplit e      -> wrap n 3 (text "splitAt" <+> ppPrec 4 e)
+
       EParens e -> parens (pp e)
 
       EInfix e1 op _ e2 -> wrap n 0 (pp e1 <+> ppInfixName (thing op) <+> pp e2)
@@ -939,6 +942,7 @@ instance NoPos (Expr name) where
       EFun x y      -> EFun     (noPos x) (noPos y)
       ELocated x _  -> noPos x
 
+      ESplit x      -> ESplit (noPos x)
       EParens e     -> EParens (noPos e)
       EInfix x y f z-> EInfix (noPos x) y f (noPos z)
 

src/Cryptol/Parser/Names.hs

@@ -100,6 +100,7 @@ namesE expr =
     EFun ps e     -> boundNames (namesPs ps) (namesE e)
     ELocated e _  -> namesE e
 
+    ESplit e      -> namesE e
     EParens e     -> namesE e
     EInfix a o _ b-> Set.insert (thing o) (Set.union (namesE a) (namesE b))
 
@@ -241,6 +242,7 @@ tnamesE expr =
     EFun ps e     -> Set.union (Set.unions (map tnamesP ps)) (tnamesE e)
     ELocated e _  -> tnamesE e
 
+    ESplit e      -> tnamesE e
     EParens e     -> tnamesE e
     EInfix a _ _ b-> Set.union (tnamesE a) (tnamesE b)
 

src/Cryptol/Parser/NoPat.hs

@@ -120,8 +120,7 @@ noPat pat =
          x <- newName
          tmp <- newName
          r <- getRange
-         let prim = EVar (mkUnqual (mkIdent "splitAt"))
-             bTmp = simpleBind (Located r tmp) (EApp prim (EVar x))
+         let bTmp = simpleBind (Located r tmp) (ESplit (EVar x))
              b1   = sel a1 tmp (TupleSel 0 (Just 2))
              b2   = sel a2 tmp (TupleSel 1 (Just 2))
          return (pVar r x, bTmp : b1 : b2 : ds1 ++ ds2)
@@ -166,6 +165,7 @@ noPatE expr =
                         return (EFun ps1 e1)
     ELocated e r1 -> ELocated <$> inRange r1 (noPatE e) <*> return r1
 
+    ESplit e      -> ESplit  <$> noPatE e
     EParens e     -> EParens <$> noPatE e
     EInfix x y f z-> EInfix  <$> noPatE x <*> pure y <*> pure f <*> noPatE z
 

src/Cryptol/TypeCheck/Infer.hs

@@ -145,10 +145,6 @@ appTys expr ts tGoal =
                    appTys e ts tGoal
 
 
-    P.ENeg {} -> panic "appTys" ["[bug] renamer bug", "unexpected ENeg" ]
-    P.EComplement {} ->
-      panic "appTys" ["[bug] renamer bug", "unexpected EComplement" ]
-
     P.EAppT e fs ->
       do ps <- mapM inferTyParam fs
          appTys e (ps ++ ts) tGoal
@@ -163,6 +159,9 @@ appTys expr ts tGoal =
     P.ELocated e r ->
       inRange r (appTys e ts tGoal)
 
+    P.ENeg        {} -> mono
+    P.EComplement {} -> mono
+
     P.ETuple    {} -> mono
     P.ERecord   {} -> mono
     P.ESel      {} -> mono
@@ -175,6 +174,7 @@ appTys expr ts tGoal =
     P.ETyped    {} -> mono
     P.ETypeVal  {} -> mono
     P.EFun      {} -> mono
+    P.ESplit    {} -> mono
 
     P.EParens e       -> appTys e ts tGoal
     P.EInfix a op _ b -> appTys (P.EVar (thing op) `P.EApp` a `P.EApp` b) ts tGoal
@@ -228,9 +228,13 @@ checkE expr tGoal =
          checkHasType t tGoal
          return e'
 
-    P.ENeg {} -> panic "checkE" ["[bug] renamer bug", "unexpected ENeg" ]
-    P.EComplement {} ->
-      panic "checkE" ["[bug] renamer bug", "unexpected EComplement" ]
+    P.ENeg e ->
+      do prim <- mkPrim "negate"
+         checkE (P.EApp prim e) tGoal
+
+    P.EComplement e ->
+      do prim <- mkPrim "complement"
+         checkE (P.EApp prim e) tGoal
 
     P.ELit l@(P.ECNum _ P.DecLit) ->
       do e <- desugarLiteral False l
@@ -382,6 +386,10 @@ checkE expr tGoal =
 
     P.ELocated e r  -> inRange r (checkE e tGoal)
 
+    P.ESplit e ->
+      do prim <- mkPrim "splitAt"
+         checkE (P.EApp prim e) tGoal
+
     P.EInfix a op _ b -> checkE (P.EVar (thing op) `P.EApp` a `P.EApp` b) tGoal
 
     P.EParens e -> checkE e tGoal