separate inferType and checkType

doc/oplss.mng

@@ -1059,68 +1059,57 @@ that we can print warning messages.
 {[}Typecheck.hs{]}}
 
 Now that we have the type checking monad available, we can start our
-implementation. For flexibility \texttt{inferType} and \texttt{checkType} will
-\emph{both} be implemented by the same function, called \cd{tcTerm}.
+implementation. 
 
-\begin{verbatim}
-inferType :: Term -> TcMonad Type
-inferType t = tcTerm t Nothing
-
-checkType :: Term -> Type -> TcMonad ()
-checkType tm ty = void $ tcTerm tm (Just ty)
-\end{verbatim}
-
-The \texttt{tcTerm} function checks a term, producing its type. The
-second argument is \texttt{Nothing} in inference mode and an expected
-type in checking mode.
+The general structure of the \cd{inferType} function starts with a pattern
+match for the various syntactic forms. There are also several cases for
+practical reasons (annotations, source code positions, etc.) and a few cases
+for homework.  If the form of the term does not match any of the forms of the
+terms that we can synthesize types for, then the type checker produces an
+error.
 
 \begin{verbatim}
-tcTerm :: Term -> Maybe Type -> TcMonad Type
-\end{verbatim}
+inferType tm = case tm of 
+   (Var x) -> ...
 
-We combine these two functions into a single definition so that we can share
-code between checking and inference modes. While none of the expression forms
-of the core language can take advantage of this functionality, it is useful
-for some extensions to the language.
+   TyType -> ...
 
-The general structure of the \cd{tcTerm} function starts with a pattern match
-for the various syntactic forms in inference mode:
+   (TyPi tyA bnd) -> ...
 
-\begin{verbatim}
-tcTerm (Var x) Nothing = ...
-
-tcTerm TyType Nothing = ...
+   (App t1 t2) -> ...
 
-tcTerm (TyPi tyA bnd) Nothing = ...
+   (Ann tm ty) -> ...
 
-tcTerm (App t1 t2) Nothing = ...
+   ...
 
+   _ -> Env.err [DS "Must have a type for", DD tm] 
 \end{verbatim}
 
+For checking, the general form of the function also 
+
 Mixed in here, we also have a pattern for lambda expressions in checking
 mode:
 
 \begin{verbatim}
-tcTerm (Lam bnd) (Just (TyPi tyA bnd2)) = ...
-   -- pass in the Pi type for the lambda expression
-
-tcTerm (Lam _) (Just nf) =  -- checking mode wrong type
-   err [DS "Lambda expression has a function type, not ", DD nf]
+checkType tm ty = case tm of 
+  (Lam bnd) -> case ty of 
+     TyPi tyA bnd2 = ...
+        -- pass in the Pi type for the lambda expression
+     _ -> 
+       Env.err [DS "Lambda expression has a function type, not ", DD ty]
 \end{verbatim}
 
-There are also several cases for practical reasons (annotations, source code
-positions, etc.) and a few cases for homework.
-
-Finally, the last case covers all other forms of checking mode, by
-calling inference mode and making sure that the inferred type is equal
-to the checked type. This case is the implementation of \rref{c-infer}.
+Again there are several cases for practical reasons, plus cases for homework.
+Finally, the last case covers all other forms of checking mode, by calling
+inference mode and making sure that the inferred type is equal to the checked
+type. This case is the implementation of \rref{c-infer}.
 
 \begin{verbatim}
-tcTerm tm (Just ty) = do
- ty' <- inferType tm
- unless (Unbound.aeq ty' ty) $
-   err [DS "Types don't match", DD ty, DS "and", DD ty']
- return ty
+ -- c-infer
+ tm -> do
+      ty' <- inferType tm
+      unless (Unbound.aeq ty' ty) $ 
+         Env.err [DS "Types don't match", DD ty, DS "and", DD ty'] -}
 \end{verbatim}
 
 The function \texttt{aeq} ensures that the two types are alpha-equivalent. If
@@ -1419,12 +1408,12 @@ whnf :: Term -> TcMonad Term
 In \texttt{version2} of the \href{version2/src/TypeCheck.hs}{implementation},
 these functions are called in a few places:
 \begin{itemize}
-\item \texttt{equate} is called at the
-end of \texttt{tcTerm}
+\item \texttt{equate} is called at the end of \texttt{checkType} to make sure 
+that the annotate type matches the inferred type.
 \item \texttt{ensurePi} is called in the \texttt{App} case
-of \texttt{tcTerm}
-\item \texttt{whnf} is called in \texttt{checkType}, before the call to
-  \texttt{tcTerm}, to make sure that we are using the head form in checking
+of \texttt{inferType}
+\item \texttt{whnf} is called in \texttt{checkType}
+  to make sure that we are using the head form of the type in checking
   mode.
 \end{itemize}
 
@@ -1533,8 +1522,6 @@ For example, we can only type check the example below using the first (checking)
 \[ [[ |- \y. if y then (\x.x) else (\x. not x) <= Bool -> Bool -> Bool]] \]
 and we can only type check this next example using the second (inference) rule:
 \[ [[ x:Bool,y:Bool->Bool |- (if x then y else not) true => Bool ]] \]
-Fortunately, it is not difficult to implement our type checking function so that it implements both rules. Indeed, because \cd{tcTerm} combines both judgments into a single Haskell function in the implementation, it is possible to implement both 
-rules with the same code.
 
 However, note that we can strengthen the specification of the type checking
 rule for \cd{if} by making the result type \texttt{A} depend on whether the

full/pi-forall.cabal

@@ -21,7 +21,7 @@ common shared-properties
   default-language:
     GHC2021
   ghc-options:
-    -Wall -fno-warn-unused-matches -fno-warn-orphans -fno-warn-unused-top-binds -fno-warn-unused-imports -fno-warn-name-shadowing
+    -Wall -fno-warn-unused-matches -fno-warn-orphans -fno-warn-unused-top-binds -fno-warn-unused-imports -fno-warn-name-shadowing -Wno-unrecognised-pragmas
   default-extensions: 
     DefaultSignatures
     DeriveAnyClass

full/src/Environment.hs

@@ -9,7 +9,6 @@ module Environment
     lookupTy,
     lookupTyMaybe,
     lookupDef,
-    lookupRecDef,
     lookupHint ,
     lookupTCon,
     lookupDCon,
@@ -66,15 +65,15 @@ data SourceLocation where
 -- | Environment manipulation and accessing functions
 -- The context 'gamma' is a list
 data Env = Env
-  { -- | elaborated term and datatype declarations.
-    ctx :: [Decl],
+  { -- | elaborated term and datatype declarations
+    ctx :: [Entry],
     -- | how long the tail of "global" variables in the context is
     --    (used to supress printing those in error messages)
     globals :: Int,
-    -- | Type declarations (signatures): it's not safe to
+    -- | Type declarations: it's not safe to
     -- put these in the context until a corresponding term
     -- has been checked.
-    hints :: [Sig],
+    hints :: [Decl],
     -- | what part of the file we are in (for errors/warnings)
     sourceLocation :: [SourceLocation] 
   }
@@ -96,35 +95,35 @@ instance Disp Env where
   debugDisp e = vcat [debugDisp decl | decl <- ctx e]
 
 -- | Find a name's user supplied type signature.
-lookupHint :: (MonadReader Env m) => TName -> m (Maybe Sig)
+lookupHint :: (MonadReader Env m) => TName -> m (Maybe Decl)
 lookupHint v = do
   hints <- asks hints
-  return $ listToMaybe [ sig | sig <- hints, v == sigName sig]
+  return $ listToMaybe [ sig | sig <- hints, v == declName sig]
 
 -- | Find a name's type in the context.
 lookupTyMaybe ::
   (MonadReader Env m) =>
   TName ->
-  m (Maybe Sig)
+  m (Maybe Decl)
 lookupTyMaybe v = do
   ctx <- asks ctx
   return $ go ctx where
     go [] = Nothing
-    go (TypeSig sig : ctx)
-      | v == sigName sig = Just sig
+    go (TypeDecl sig : ctx)
+      | v == declName sig = Just sig
       | otherwise = go ctx 
-    go (Demote ep : ctx) = demoteSig ep <$> go ctx
+    go (Demote ep : ctx) = demoteDecl ep <$> go ctx
 
     go (_ : ctx) = go ctx
 
-demoteSig :: Epsilon -> Sig -> Sig
-demoteSig ep s = s { sigEp = min ep (sigEp s) }
+demoteDecl :: Epsilon -> Decl -> Decl
+demoteDecl ep s = s { declEp = min ep (declEp s) }
 
 
 -- | Find the type of a name specified in the context
 -- throwing an error if the name doesn't exist
 lookupTy ::
-  TName -> TcMonad Sig
+  TName -> TcMonad Decl
 lookupTy v =
   do
     x <- lookupTyMaybe v
@@ -147,14 +146,6 @@ lookupDef v = do
   ctx <- asks ctx
   return $ listToMaybe [a | Def v' a <- ctx, v == v']
 
-lookupRecDef ::
-  (MonadReader Env m) =>
-  TName ->
-  m (Maybe Term)
-lookupRecDef v = do
-  ctx <- asks ctx
-  return $ listToMaybe [a | RecDef v' a <- ctx, v == v']
-
 -- | Find a type constructor in the context
 lookupTCon ::
   (MonadReader Env m, MonadError Err m) =>
@@ -177,10 +168,6 @@ lookupTCon v = do
       if v == v'
         then return (delta, Just cs)
         else scanGamma g
-    scanGamma ((DataSig v' delta) : g) =
-      if v == v'
-        then return (delta, Nothing)
-        else scanGamma g
     scanGamma (_ : g) = scanGamma g
 
 -- | Find a data constructor in the context, returns a list of
@@ -200,7 +187,6 @@ lookupDConAll v = do
         Just c -> do
           more <- scanGamma g
           return $ (v', (delta, c)) :  more
-    scanGamma ((DataSig v' delta) : g) = scanGamma g
     scanGamma (_ : g) = scanGamma g
 
 -- | Given the name of a data constructor and the type that it should
@@ -231,17 +217,17 @@ lookupDCon c tname = do
 
 
 -- | Extend the context with a new binding
-extendCtx :: (MonadReader Env m) => Decl -> m a -> m a
+extendCtx :: (MonadReader Env m) => Entry -> m a -> m a
 extendCtx d =
   local (\m@Env{ctx = cs} -> m {ctx = d : cs})
 
 -- | Extend the context with a list of bindings
-extendCtxs :: (MonadReader Env m) => [Decl] -> m a -> m a
+extendCtxs :: (MonadReader Env m) => [Entry] -> m a -> m a
 extendCtxs ds =
   local (\m@Env {ctx = cs} -> m {ctx = ds ++ cs})
 
 -- | Extend the context with a list of bindings, marking them as "global"
-extendCtxsGlobal :: (MonadReader Env m) => [Decl] -> m a -> m a
+extendCtxsGlobal :: (MonadReader Env m) => [Entry] -> m a -> m a
 extendCtxsGlobal ds =
   local
     ( \m@Env {ctx = cs} ->
@@ -252,12 +238,12 @@ extendCtxsGlobal ds =
     )
 
 -- | Extend the context with a telescope
-extendCtxTele :: (MonadReader Env m, MonadIO m, MonadError Err m) => [Decl] -> m a -> m a
+extendCtxTele :: (MonadReader Env m, MonadIO m, MonadError Err m) => [Entry] -> m a -> m a
 extendCtxTele [] m = m
 extendCtxTele (Def x t2 : tele) m =
   extendCtx (Def x t2) $ extendCtxTele tele m
-extendCtxTele (TypeSig sig : tele) m =
-  extendCtx (TypeSig sig) $ extendCtxTele tele m
+extendCtxTele (TypeDecl sig : tele) m =
+  extendCtx (TypeDecl sig) $ extendCtxTele tele m
 extendCtxTele ( _ : tele) m = 
   err [DS "Invalid telescope ", DD tele]
 
@@ -273,11 +259,11 @@ extendCtxMods :: (MonadReader Env m) => [Module] -> m a -> m a
 extendCtxMods mods k = foldr extendCtxMod k mods
 
 -- | Get the complete current context
-getCtx :: MonadReader Env m => m [Decl]
+getCtx :: MonadReader Env m => m [Entry]
 getCtx = asks ctx
 
 -- | Get the prefix of the context that corresponds to local variables.
-getLocalCtx :: MonadReader Env m => m [Decl]
+getLocalCtx :: MonadReader Env m => m [Entry]
 getLocalCtx = do
   g <- asks ctx
   glen <- asks globals
@@ -293,7 +279,7 @@ getSourceLocation :: MonadReader Env m => m [SourceLocation]
 getSourceLocation = asks sourceLocation
 
 -- | Add a type hint
-extendHints :: (MonadReader Env m) => Sig -> m a -> m a
+extendHints :: (MonadReader Env m) => Decl -> m a -> m a
 extendHints h = local (\m@Env {hints = hs} -> m {hints = h : hs})
 
 -- | An error that should be reported to the user

full/src/Equal.hs

@@ -177,11 +177,7 @@ whnf (Var x) = do
   maybeDef <- Env.lookupDef x
   case maybeDef of 
     (Just d) -> whnf d 
-    _ -> do
-          maybeRecDef <- Env.lookupRecDef x 
-          case maybeRecDef of 
-            (Just d) -> whnf d
-            _ -> return (Var x)
+    _ -> return (Var x)
 
 whnf (App t1 t2) = do
   nf <- whnf t1 
@@ -235,7 +231,7 @@ whnf tm = return tm
 -- | 'Unify' the two terms, producing a list of Defs
 -- If there is an obvious mismatch, this function produces an error
 -- If either term is "ambiguous" just ignore.
-unify :: [TName] -> Term -> Term -> TcMonad [Decl]
+unify :: [TName] -> Term -> Term -> TcMonad [Entry]
 unify ns tx ty = do
   txnf <- whnf tx
   tynf <- whnf ty

full/src/Modules.hs

@@ -23,7 +23,7 @@ getModules
      [FilePath] -> String -> m [Module]
 getModules prefixes top = do
   toParse <- gatherModules prefixes [ModuleImport top]
-  flip evalStateT emptyConstructorNames $ mapM reparse toParse
+  flip evalStateT initialConstructorNames $ mapM reparse toParse
 
 
 data ModuleInfo = ModuleInfo {