name changes for clarity

doc/oplss.mng

@@ -55,7 +55,7 @@ checker. They are based on lectures given at the \emph{Oregon Programming
   Languages Summer School} during July 2023 and derived from earlier lectures
 from summer schools during 2022, 2014 and 2013.
 
-\paragraph{What do I expect from you, dear reader?} This discussion assumes a
+\paragraph{What do I expect from you?} This discussion assumes a
 familiarity with the basics of the lambda calculus, including its standard
 operations (alpha-equivalence, substitution, evaluation) and the basics of
 type systems (especially their specification using inference rules). For
@@ -71,31 +71,30 @@ it. Installation instructions are available with the repository.
 \paragraph{What do these notes cover?}
 These notes are broken into several sections that incrementally build up the
 design and implementation of a type checker for a dependently-typed
-programming language. 
+programming language. This implementation itself is available in separate
+versions, each found in separate subdirectories of the repository.
 
 \begin{figure}[ht]
 \begin{center}
 \begin{tabular}{llll}
-Key feature & \pif version      & Section\\
+Key feature & \pif subdirectory & Section\\
 \hline
 Core system & \texttt{version1} & Sections~\ref{sec:simple}, \ref{sec:bidirectional}, and \ref{sec:implementation} \\
 Equality    & \texttt{version2} & Sections~\ref{sec:equality} and ~\ref{sec:pattern-matching}\\
 Irrelevance & \texttt{version3} & Section ~\ref{sec:irrelevance} \\
 Datatypes   & \texttt{full}     & Sections~\ref{sec:examples} and ~\ref{sec:datatypes} \\
 \end{tabular}
 \end{center}
-\caption{Connection between sections of the lecture notes and \pif versions}
+\caption{Connection between sections and \pif versions}
 \label{fig:impls}
 \end{figure}
 
-If you are looking at the repository, you will see that it includes several
-incrementally more expressive implementations of \pif in separate
-subdirectories. These implementations build on each other (each is an
-extension of the previous version) and are summarized in
-Figure~\ref{fig:impls}.  As you read each chapter, refer to its corresponding
-implementation to see how the features described in that chapter can be
-implemented. The directory \texttt{main} is the source of all of these
-implementations and contains the markup needed to generate the four versions.
+These implementations build on each other (each is an extension of the
+previous version) and are summarized in Figure~\ref{fig:impls}.  As you read
+each chapter, refer to its corresponding implementation to see how the
+features described in that chapter can be implemented. The directory
+\texttt{main} is the source of all of these implementations and contains the
+markup needed to generate the four versions.
 
 
 \begin{itemize}
@@ -642,9 +641,9 @@ Likewise, the case of the typing function for the $[[Type]]$ term is also
 straightforward. When we see the term $[[Type]]$, we know immediately that it
 is its own type.
 
-\begin{haskell}
-inferType Type ctx = Just Type
-\end{haskell}
+% \begin{haskell}
+% inferType TyType ctx = Just TyType
+% \end{haskell}
 
 The only stumbling block for the algorithm is \rref{t-lambda}. To type check a
 function, we need to type check its body when the context has been extended
@@ -910,7 +909,7 @@ language above, using the following datatype.
 data Term
 
   = -- | type of types  `Type`
-    Type
+    TyType
 
   | -- | variables  `x`
     Var TName
@@ -922,7 +921,7 @@ data Term
     App Term Term
 
   | -- | function types   `(x : A) -> B`
-    Pi Type (Unbound.Bind TName Type)
+    TyPi Type (Unbound.Bind TName Type)
 
   | -- | Annotated terms `( a : A )`
     Ann Term Type
@@ -933,8 +932,8 @@ data Term
 
 As you can see, variables are represented by names. \unbound's \cd{Bind}
 type constructor declares the scope of the bound variables. Both \cd{Lam}
-and \cd{Pi} bind a single variable in a \cd{Term}.  However, in a
-\cd{Pi} term, we also want to store the type $[[A]]$, the type of the bound
+and \cd{TyPi} bind a single variable in a \cd{Term}.  However, in a
+\cd{TyPi} term, we also want to store the type $[[A]]$, the type of the bound
 variable $[[x]]$.
 
 Because the syntax is all shared, a \cd{Type} is just another name for a
@@ -1090,9 +1089,9 @@ for the various syntactic forms in inference mode:
 \begin{verbatim}
 tcTerm (Var x) Nothing = ...
 
-tcTerm Type Nothing = ...
+tcTerm TyType Nothing = ...
 
-tcTerm (Pi tyA bnd) Nothing = ...
+tcTerm (TyPi tyA bnd) Nothing = ...
 
 tcTerm (App t1 t2) Nothing = ...
 
@@ -1102,7 +1101,7 @@ Mixed in here, we also have a pattern for lambda expressions in checking
 mode:
 
 \begin{verbatim}
-tcTerm (Lam bnd) (Just (Pi tyA bnd2)) = ...
+tcTerm (Lam bnd) (Just (TyPi tyA bnd2)) = ...
    -- pass in the Pi type for the lambda expression
 
 tcTerm (Lam _) (Just nf) =  -- checking mode wrong type
@@ -2168,10 +2167,10 @@ declaration to the syntax.\footnote{Some parts of this implementation have
 
 \begin{verbatim}
 -- | type constructor names
-type TCName = String
+type TyConName = String
 
 -- | data constructor names
-type DCName = String
+type DataConName = String
 
 -- | Declarations stored in the context
 data Decl =
@@ -2182,10 +2181,10 @@ data Decl =
     ...
 
   | -- | Datatype definition  `data T = ...`
-    Data TCName [ConstructorDef]
+    Data TyConName [ConstructorDef]
 
 -- | A Data constructor has a name and a telescope of arguments
-data ConstructorDef = ConstructorDef DCName Telescope
+data ConstructorDef = ConstructorDef DataConName Telescope
 
 -- | A telescope is a list of type declarations and definitions
 newtype Telescope = Telescope [Decl]
@@ -2324,7 +2323,7 @@ is as follows:
   Infer type of the scrutinee $[[a]]$ (\texttt{inferType})
 \item
   Make sure that the inferred type is some type constructor $[[T]]$
-  (\texttt{ensureTCon})
+  (\texttt{ensureTyCon})
 \item
   For each case alternative $[[pi]][[->]][[ai]]$:
 \begin{itemize}
@@ -2364,7 +2363,7 @@ can be referred to later in the telescope. For example, with parameters, we
 can implement $\Sigma$-types as a datatype, instead of making them primitive.
 
 \begin{piforall}
-data Sigma (A: Type) (B : A -> Type) : Type
+data TySigma (A: Type) (B : A -> Type) : Type
     Prod of (x:A) (B)
 \end{piforall}
 

full/src/Arbitrary.hs

@@ -6,7 +6,7 @@ module Arbitrary where
 
 import qualified Data.Set as Set
 import Test.QuickCheck
-    ( elements, frequency, sized, Arbitrary(arbitrary), Gen ) 
+    ( elements, frequency, sized, Arbitrary(arbitrary), Gen )
 import qualified Test.QuickCheck as QC
 import qualified Unbound.Generics.LocallyNameless as Unbound
 import Text.Parsec.Error ( ParseError )
@@ -18,18 +18,18 @@ import Parser ( testParser, expr )
 
 -- | Round trip property: a given term prints then parses to the same term.
 prop_roundtrip :: Term -> QC.Property
-prop_roundtrip tm = 
+prop_roundtrip tm =
     let str = render (disp tm) in
     case test_parseExpr str  of
         Left _ -> QC.counterexample ("*** Could not parse:\n" ++ str) False
         Right tm' -> QC.counterexample ("*** Round trip failure! Parsing:\n" ++ str ++ "\n*** results in\n" ++ show tm') (Unbound.aeq tm tm')
-           
+
 test_parseExpr :: String -> Either Text.Parsec.Error.ParseError Term
 test_parseExpr = testParser arbConstructorNames expr
 
 -- View random terms
 sampleTerms :: IO ()
-sampleTerms = QC.sample' (arbitrary :: Gen Term) >>= 
+sampleTerms = QC.sample' (arbitrary :: Gen Term) >>=
     mapM_ (putStrLn . render . disp)
 
 ---------------------------------------------------------------------------------------------------
@@ -49,42 +49,42 @@ genName = Unbound.string2Name <$> elements ["x", "y", "z", "x0" , "y0"]
 instance Arbitrary (Unbound.Name a) where
     arbitrary = genName
 
-tcNames :: [TCName]
+tcNames :: [TyConName]
 tcNames = ["T", "List", "Vec" ]
-dcNames :: [DCName]
+dcNames :: [DataConName]
 dcNames = ["K", "Nil", "Cons"]
 
 arbConstructorNames :: ConstructorNames
 arbConstructorNames = ConstructorNames (Set.fromList tcNames) (Set.fromList dcNames)
 
-genTCName :: Gen TCName
+genTCName :: Gen TyConName
 genTCName = elements tcNames
 
-genDCName :: Gen DCName
+genDCName :: Gen DataConName
 genDCName = elements dcNames
 
 
 -- * Core language
 
 -- Terms with no subterms
 base :: Gen Term
-base = elements [Type, TrustMe, PrintMe,
-                tyUnit, litUnit, tyBool, 
+base = elements [TyType, TrustMe, PrintMe,
+                tyUnit, litUnit, tyBool,
                 litTrue, litFalse, Refl  ]
-    where tyUnit = TCon "Unit" [] 
-          litUnit = DCon "()" [] 
-          tyBool = TCon "Bool" [] 
-          litTrue = DCon "True" [] 
-          litFalse = DCon "False" [] 
+    where tyUnit = TyCon "Unit" [] 
+          litUnit = DataCon "()" [] 
+          tyBool = TyCon "Bool" [] 
+          litTrue = DataCon "True" [] 
+          litFalse = DataCon "False" [] 
 
 -- Generate a random term
--- In the inner recursion, the bool prevents the generation of TCon/DCon applications 
+-- In the inner recursion, the bool prevents the generation of TyCon/DataCon applications 
 -- inside Apps --- we want these terms to be fully saturated.
 genTerm :: Int -> Gen Term
 genTerm n
     | n <= 1 = base
     | otherwise = go True n where
-        go b n0 = 
+        go b n0 =
             let n' = n0 `div` 2 in
             frequency [
               (1, Var <$> genName),
@@ -96,80 +96,80 @@ genTerm n
               (1, Subst <$> go True n' <*> go True n'),
               (1, Contra <$> go True n'),
 
-                            (if b then 1 else 0, TCon <$> genTCName <*> genArgs n'),
-              (if b then 1 else 0, DCon <$> genDCName <*> genArgs n'),
+                            (if b then 1 else 0, TyCon <$> genTCName <*> genArgs n'),
+              (if b then 1 else 0, DataCon <$> genDCName <*> genArgs n'),
               (1, Case <$> go True n' <*> genBoundedList 2 (genMatch n')),
 
               (1, base)
             ]
 
 genLam :: Int -> Gen Term
-genLam n = do 
+genLam n = do
     p <- genName
     ep <- arbitrary 
     b <- genTerm n
     return $ Lam ep (Unbound.bind p b)
 
 
 genPi :: Int -> Gen Term
-genPi n = do 
+genPi n = do
     p <- genName
     ep <- arbitrary 
     tyA <- genTerm n
     tyB <- genTerm n
-    return $ Pi ep tyA (Unbound.bind p tyB)
+    return $ TyPi ep tyA (Unbound.bind p tyB)
 
 genSigma :: Int -> Gen Term
 genSigma n = do
-    p <- genName 
+    p <- genName
     tyA <- genTerm n
     tyB <- genTerm n
-    return $ Sigma tyA (Unbound.bind p tyB)
+    return $ TySigma tyA (Unbound.bind p tyB)
 
-genLet :: Int -> Gen Term 
+genLet :: Int -> Gen Term
 genLet n = do
-    p <- genName 
+    p <- genName
     rhs <- genTerm n
     b <- genTerm n
     return $ Let rhs (Unbound.bind p b)
 
-genLetPair :: Int -> Gen Term 
+genLetPair :: Int -> Gen Term
 genLetPair n = do
-    p <- (,) <$> genName <*> genName 
+    p <- (,) <$> genName <*> genName
     a <- genTerm n
     b <- genTerm n
     return $ LetPair a (Unbound.bind p b)
 
 instance Arbitrary Arg where
     arbitrary = sized genArg
-    shrink (Arg ep tm) = 
+    shrink (Arg ep tm) =
         [ Arg ep tm' | tm' <- QC.shrink tm]
 
 genArg :: Int -> Gen Arg
 genArg n = Arg <$> arbitrary <*> genTerm (n `div` 2)
 
 genArgs :: Int -> Gen [Arg]
 genArgs n = genBoundedList 2 (genArg n)
-        
+
 instance Arbitrary Epsilon where
     arbitrary = elements [ Rel, Irr ]
 
 
 
 genPattern :: Int -> Gen Pattern
 genPattern n | n == 0 = PatVar <$> genName
-  | otherwise = frequency 
+  | otherwise = frequency
     [(1, PatVar <$> genName),
      (1, PatCon <$> genDCName <*> genPatArgs)]
-     where 
+     where
         n' = n `div` 2
         genPatArgs = genBoundedList 2 ( (,) <$> genPattern n' <*> arbitrary )
 
 genMatch :: Int -> Gen Match
 genMatch n = Match <$> (Unbound.bind <$> genPattern n <*> genTerm n)
 
 instance Arbitrary Pattern where
-    arbitrary = sized genPattern 
+    arbitrary = sized genPattern
     shrink (PatCon n pats) = map fst pats ++ [PatCon n pats' | pats' <- QC.shrink pats]
     shrink _ = []
 
@@ -182,24 +182,24 @@ instance Arbitrary Term where
     arbitrary = sized genTerm
 
     -- when QC finds a counterexample, it tries to shrink it to find a smaller one
-    shrink (App tm arg) = 
-        [tm, unArg arg] ++ [App tm' arg | tm' <- QC.shrink tm] 
+    shrink (App tm arg) =
+        [tm, unArg arg] ++ [App tm' arg | tm' <- QC.shrink tm]
                         ++ [App tm arg' | arg' <- QC.shrink arg]
 
     shrink (Lam ep bnd) = []
-    shrink (Pi ep tyA bnd) = [tyA]
+    shrink (TyPi ep tyA bnd) = [tyA]
     shrink (Let rhs bnd) = [rhs]
-    shrink (Sigma tyA bnd) = [tyA]
+    shrink (TySigma tyA bnd) = [tyA]
     shrink (TyEq a b) = [a,b] ++ [TyEq a' b | a' <- QC.shrink a] ++ [TyEq a b' | b' <- QC.shrink b]
     shrink (Subst a b) = [a,b] ++ [Subst a' b | a' <- QC.shrink a] ++ [Subst a b' | b' <- QC.shrink b]
-    shrink (Contra a) = [a] ++ [Contra a' | a' <- QC.shrink a]
+    shrink (Contra a) = a : [Contra a' | a' <- QC.shrink a]
 
-    shrink (TCon n as) = map unArg as ++ [TCon n as' | as' <- QC.shrink as]
-    shrink (DCon n as) = map unArg as ++ [DCon n as' | as' <- QC.shrink as]
+    shrink (TyCon n as) = map unArg as ++ [TyCon n as' | as' <- QC.shrink as]
+    shrink (DataCon n as) = map unArg as ++ [DataCon n as' | as' <- QC.shrink as]
     shrink (Case a ms) = [a] ++ [Case a' ms | a' <- QC.shrink a] ++ [Case a ms' | ms' <- QC.shrink ms]
 
     shrink _ = []
-       
+
 -------------------------------------------------------
 -- * General quickcheck utilities