diff --git a/CHANGELOG b/CHANGELOG
--- a/CHANGELOG
+++ b/CHANGELOG
@@ -1,9 +1,14 @@
+2023-03-07
+        * Version bump (3.14). (#422)
+        * Remove Copilot.Core.PrettyDot. (#409)
+        * Fix formatting error in CHANGELOG. (#414)
+        * Remove module space Copilot.Core.Interpret. (#410)
+        * Remove unused definitions from Copilot.Core.Type.Array. (#411)
+
 2023-01-07
         * Version bump (3.13). (#406)
         * Implement missing cases of type equality for arrays and structs.
           (#400)
-
-2022-12-27
         * Remove Copilot.Core.External. (#391)
         * Fix bug in definition of simpleType for Int8. (#393)
         * Hide module Copilot.Core.Type.Show. (#392)
diff --git a/copilot-core.cabal b/copilot-core.cabal
--- a/copilot-core.cabal
+++ b/copilot-core.cabal
@@ -1,6 +1,6 @@
 cabal-version:       >=1.10
 name:                copilot-core
-version:             3.13
+version:             3.14
 synopsis:            An intermediate representation for Copilot.
 description:
   Intermediate representation for Copilot.
@@ -49,20 +49,16 @@
 
     Copilot.Core
     Copilot.Core.Expr
-    Copilot.Core.Interpret
-    Copilot.Core.Interpret.Eval
     Copilot.Core.Operators
     Copilot.Core.Spec
     Copilot.Core.Type
     Copilot.Core.Type.Array
     Copilot.Core.Type.Equality
     Copilot.Core.PrettyPrint
-    Copilot.Core.PrettyDot
 
   other-modules:
 
     Copilot.Core.Error
-    Copilot.Core.Interpret.Render
     Copilot.Core.Type.Show
 
 test-suite unit-tests
diff --git a/src/Copilot/Core.hs b/src/Copilot/Core.hs
--- a/src/Copilot/Core.hs
+++ b/src/Copilot/Core.hs
@@ -16,8 +16,7 @@
 -- Electronic Notes in Theoretical Computer Science vol. 174, p. 23-39, 2007.
 --
 -- For examples of how to traverse a Copilot specification see
--- the source code of the interpreter
--- ("Copilot.Core.Interpret")
+-- the source code of the interpreter (@copilot-interpreter@)
 -- and the pretty-printer
 -- ("Copilot.Core.PrettyPrint").
 module Copilot.Core
diff --git a/src/Copilot/Core/Error.hs b/src/Copilot/Core/Error.hs
--- a/src/Copilot/Core/Error.hs
+++ b/src/Copilot/Core/Error.hs
@@ -5,7 +5,6 @@
 -- Copyright:   (c) 2011 National Institute of Aerospace / Galois, Inc.
 module Copilot.Core.Error
     ( impossible
-    , badUsage
     )
   where
 
@@ -19,8 +18,3 @@
     ++ ". Please file an issue at "
     ++ "https://github.com/Copilot-Language/copilot/issues"
     ++ "or email the maintainers at <ivan.perezdominguez@nasa.gov>"
-
--- | Report an error due to an error detected by Copilot (e.g., user error).
-badUsage :: String -- ^ Description of the error.
-         -> a
-badUsage msg = error $ "Copilot error: " ++ msg
diff --git a/src/Copilot/Core/Interpret.hs b/src/Copilot/Core/Interpret.hs
deleted file mode 100644
--- a/src/Copilot/Core/Interpret.hs
+++ /dev/null
@@ -1,35 +0,0 @@
--- The following warning is enabled in this module so that the import of
--- Copilot.Core.Interpret.Eval and Render do not give rise to warnings.
-{-# OPTIONS_GHC -fno-warn-deprecations #-}
-
--- Copyright © 2011 National Institute of Aerospace / Galois, Inc.
-
--- | An interpreter for Copilot specifications.
-
-{-# LANGUAGE Safe #-}
-
-module Copilot.Core.Interpret
-  {-# DEPRECATED "This module is deprecated in Copilot 3.11. Use copilot-interpreter instead." #-}
-  ( Format (..)
-  , interpret
-  ) where
-
-import Copilot.Core
-import Copilot.Core.Interpret.Eval
-import Copilot.Core.Interpret.Render
-import Copilot.Core.Type.Show        (ShowType (..))
-
--- | Output format for the results of a Copilot spec interpretation.
-data Format = Table | CSV
-
--- | Interpret a Copilot specification.
-interpret :: Format  -- ^ Format to be used for the output.
-          -> Int     -- ^ Number of steps to interpret.
-          -> Spec    -- ^ Specification to interpret.
-          -> String
-interpret format k spec =
-  case format of
-    Table -> renderAsTable e
-    CSV   -> renderAsCSV e
-  where
-    e = eval Haskell k spec
diff --git a/src/Copilot/Core/Interpret/Eval.hs b/src/Copilot/Core/Interpret/Eval.hs
deleted file mode 100644
--- a/src/Copilot/Core/Interpret/Eval.hs
+++ /dev/null
@@ -1,352 +0,0 @@
--- Copyright © 2011 National Institute of Aerospace / Galois, Inc.
-
--- | A tagless interpreter for Copilot specifications.
-
-{-# LANGUAGE BangPatterns       #-}
-{-# LANGUAGE DeriveDataTypeable #-}
-{-# LANGUAGE GADTs              #-}
-{-# LANGUAGE Safe               #-}
-
-module Copilot.Core.Interpret.Eval
-  {-# DEPRECATED "This module is deprecated in Copilot 3.11. Use copilot-interpreter instead." #-}
-  ( Env
-  , Output
-  , ExecTrace (..)
-  , eval
-  , ShowType (..)
-  ) where
-
-import Copilot.Core           (Expr (..), Field (..), Id, Name, Observer (..),
-                               Op1 (..), Op2 (..), Op3 (..), Spec, Stream (..),
-                               Trigger (..), Type (Struct), UExpr (..),
-                               arrayelems, specObservers, specStreams,
-                               specTriggers)
-import Copilot.Core.Error     (badUsage)
-import Copilot.Core.Type.Show (ShowType (..), showWithType)
-
-import           Prelude hiding (id)
-import qualified Prelude as P
-
-import Control.Exception (Exception, throw)
-import Data.Bits         (complement, shiftL, shiftR, xor, (.&.), (.|.))
-import Data.Dynamic      (Dynamic, fromDynamic, toDyn)
-import Data.List         (transpose)
-import Data.Maybe        (fromJust)
-import Data.Typeable     (Typeable)
-
--- | Exceptions that may be thrown during interpretation of a Copilot
--- specification.
-data InterpException
-  = ArrayWrongSize Name Int           -- ^ Extern array has incorrect size.
-  | ArrayIdxOutofBounds Name Int Int  -- ^ Index out-of-bounds exception.
-  | DivideByZero                      -- ^ Division by zero.
-  | NotEnoughValues Name Int          -- ^ For one or more streams, not enough
-                                      --   values are available to simulate the
-                                      --   number of steps requested.
-  | NoExtsInterp Name                 -- ^ One of the externs used by the
-                                      --   specification does not declare
-                                      --   sample values to be used during
-                                      --   simulation.
-  deriving Typeable
-
--- | Show a descriptive message of the exception.
-instance Show InterpException where
-  ---------------------------------------
-  show (ArrayWrongSize name expectedSize)                                      =
-    badUsage $ "in the environment for external array " ++ name
-      ++ ", we expect a list of length " ++ show expectedSize
-      ++ ", but the length of the array you supplied is of a different length."
-  ---------------------------------------
-  show (ArrayIdxOutofBounds name index size)                                   =
-    badUsage $ "in the environment for external array " ++ name
-      ++ ", you gave an index of " ++ show index
-      ++ " where the size of the array is " ++ show size ++ "; the size must "
-      ++ " be strictly greater than the index."
-  ---------------------------------------
-  show DivideByZero                                                            =
-    badUsage "divide by zero."
-  ---------------------------------------
-  show (NotEnoughValues name k)                                                =
-    badUsage $ "on the " ++ show k ++ "th iteration, we ran out of "
-      ++ "values for simulating the external element " ++ name ++ "."
-  ---------------------------------------
-  show (NoExtsInterp name)                                                     =
-    badUsage $ "in a call of external symbol " ++ name ++ ", you did not "
-      ++ "provide an expression for interpretation.  In your external "
-      ++ "declaration, you need to provide a 'Just strm', where 'strm' is "
-      ++ "some stream with which to simulate the function."
-  ---------------------------------------
-
--- | Allow throwing and catching 'InterpException' using Haskell's standard
--- exception mechanisms.
-instance Exception InterpException
-
--- | An environment that contains an association between (stream or extern)
--- names and their values.
-type Env nm = [(nm, Dynamic)]
-
--- | The simulation output is defined as a string. Different backends may
--- choose to format their results differently.
-type Output = String
-
--- | An execution trace, containing the traces associated to each individual
--- monitor trigger and observer.
-data ExecTrace = ExecTrace
-  { interpTriggers  :: [(String, [Maybe [Output]])]
-
-    -- ^ Map from trigger names to their optional output, which is a list of
-    -- strings representing their values. The output may be 'Nothing' if the
-    -- guard for the trigger was false. The order is important, since we
-    -- compare the arg lists between the interpreter and backends.
-
-  , interpObservers :: [(String, [Output])]
-    -- ^ Map from observer names to their outputs.
-  }
-  deriving Show
-
--- We could write this in a beautiful lazy style like above, but that creates a
--- space leak in the interpreter that is hard to fix while maintaining laziness.
--- We take a more brute-force appraoch below.
-
--- | Evaluate a specification for a number of steps.
-eval :: ShowType   -- ^ Show booleans as @0@\/@1@ (C) or @True@\/@False@
-                   --   (Haskell).
-     -> Int        -- ^ Number of steps to evaluate.
-     -> Spec       -- ^ Specification to evaluate.
-     -> ExecTrace
-eval showType k spec =
-
-  let initStrms = map initStrm (specStreams spec)             in
-
-  let strms = evalStreams k (specStreams spec) initStrms      in
-
-  let trigs = map (evalTrigger showType k strms)
-                  (specTriggers spec)                         in
-
-  let obsvs = map (evalObserver showType k strms)
-                  (specObservers spec)                        in
-
-  strms `seq` ExecTrace
-                { interpTriggers  =
-                    zip (map triggerName  (specTriggers  spec)) trigs
-                , interpObservers =
-                    zip (map observerName (specObservers spec)) obsvs
-                }
-
--- | An environment that contains an association between (stream or extern)
--- names and their values.
-type LocalEnv = [(Name, Dynamic)]
-
--- | Evaluate an expression for a number of steps, obtaining the value
--- of the sample at that time.
-evalExpr_ :: Typeable a => Int -> Expr a -> LocalEnv -> Env Id -> a
-evalExpr_ k e0 locs strms = case e0 of
-  Const _ x                          -> x
-  Drop t i id                        ->
-    let Just buff = lookup id strms >>= fromDynamic in
-    reverse buff !! (fromIntegral i + k)
-  Local t1 _ name e1 e2              ->
-    let x     = evalExpr_ k e1 locs strms in
-    let locs' = (name, toDyn x) : locs  in
-    x `seq` locs' `seq` evalExpr_ k e2  locs' strms
-  Var t name                         -> fromJust $ lookup name locs >>= fromDynamic
-  ExternVar _ name xs                -> evalExternVar k name xs
-  Op1 op e1                          ->
-    let ev1 = evalExpr_ k e1 locs strms in
-    let op1 = evalOp1 op                in
-    ev1 `seq` op1 `seq` op1 ev1
-  Op2 op e1 e2                       ->
-    let ev1 = evalExpr_ k e1 locs strms in
-    let ev2 = evalExpr_ k e2 locs strms in
-    let op2 = evalOp2 op                in
-    ev1 `seq` ev2 `seq` op2 `seq` op2 ev1 ev2
-  Op3 op e1 e2 e3                    ->
-    let ev1 = evalExpr_ k e1 locs strms in
-    let ev2 = evalExpr_ k e2 locs strms in
-    let ev3 = evalExpr_ k e3 locs strms in
-    let op3 = evalOp3 op                in
-    ev1 `seq` ev2 `seq` ev3 `seq` op3 `seq` op3 ev1 ev2 ev3
-  Label _ _ e1                         ->
-    let ev1 = evalExpr_ k e1 locs strms in
-    ev1
-
--- | Evaluate an extern stream for a number of steps, obtaining the value of
--- the sample at that time.
-evalExternVar :: Int -> Name -> Maybe [a] -> a
-evalExternVar k name exts =
-  case exts of
-    Nothing -> throw (NoExtsInterp name)
-    Just xs ->
-      case safeIndex k xs of
-        Nothing -> throw (NotEnoughValues name k)
-        Just x  -> x
-
--- | Evaluate an 'Copilot.Core.Operators.Op1' by producing an equivalent
--- Haskell function operating on the same types as the
--- 'Copilot.Core.Operators.Op1'.
-evalOp1 :: Op1 a b -> (a -> b)
-evalOp1 op = case op of
-    Not        -> P.not
-    Abs _      -> P.abs
-    Sign _     -> P.signum
-    Recip _    -> P.recip
-    Exp _      -> P.exp
-    Sqrt _     -> P.sqrt
-    Log _      -> P.log
-    Sin _      -> P.sin
-    Tan _      -> P.tan
-    Cos _      -> P.cos
-    Asin _     -> P.asin
-    Atan _     -> P.atan
-    Acos _     -> P.acos
-    Sinh _     -> P.sinh
-    Tanh _     -> P.tanh
-    Cosh _     -> P.cosh
-    Asinh _    -> P.asinh
-    Atanh _    -> P.atanh
-    Acosh _    -> P.acosh
-    Ceiling _  -> P.fromIntegral . idI . P.ceiling
-    Floor _    -> P.fromIntegral . idI . P.floor
-    BwNot _    -> complement
-    Cast _ _   -> P.fromIntegral
-    GetField (Struct _) _ f -> unfield . f
-  where
-    -- Used to help GHC pick a return type for ceiling/floor
-    idI :: Integer -> Integer
-    idI = P.id
-
-    -- Extract value from field
-    unfield (Field v) = v
-
--- | Evaluate an 'Copilot.Core.Operators.Op2' by producing an equivalent
--- Haskell function operating on the same types as the
--- 'Copilot.Core.Operators.Op2'.
-evalOp2 :: Op2 a b c -> (a -> b -> c)
-evalOp2 op = case op of
-  And          -> (&&)
-  Or           -> (||)
-  Add _        -> (+)
-  Sub _        -> (-)
-  Mul _        -> (*)
-  Mod _        -> (catchZero P.mod)
-  Div _        -> (catchZero P.quot)
-  Fdiv _       -> (P./)
-  Pow _        -> (P.**)
-  Logb _       -> P.logBase
-  Atan2 _      -> P.atan2
-  Eq _         -> (==)
-  Ne _         -> (/=)
-  Le _         -> (<=)
-  Ge _         -> (>=)
-  Lt _         -> (<)
-  Gt _         -> (>)
-  BwAnd _      -> (.&.)
-  BwOr  _      -> (.|.)
-  BwXor _      -> (xor)
-  BwShiftL _ _ -> ( \ !a !b -> shiftL a $! fromIntegral b )
-  BwShiftR _ _ -> ( \ !a !b -> shiftR a $! fromIntegral b )
-  Index    _   -> \xs n -> (arrayelems xs) !! (fromIntegral n)
-
--- | Apply a function to two numbers, so long as the second one is
--- not zero.
---
--- Used to detect attempts at dividing by zero and produce the appropriate
--- 'InterpException'.
-catchZero :: Integral a => (a -> a -> a) -> (a -> a -> a)
-catchZero _ _ 0 = throw DivideByZero
-catchZero f x y = f x y
-
--- | Evaluate an 'Copilot.Core.Operators.Op3' by producing an equivalent
--- Haskell function operating on the same types as the
--- 'Copilot.Core.Operators.Op3'.
-evalOp3 :: Op3 a b c d -> (a -> b -> c -> d)
-evalOp3 (Mux _) = \ !v !x !y -> if v then x else y
-
--- | Turn a stream into a key-value pair that can be added to an 'Env' for
--- simulation.
-initStrm :: Stream -> (Id, Dynamic)
-initStrm Stream { streamId       = id
-                , streamBuffer   = buffer
-                , streamExprType = t } =
-  (id, toDyn (reverse buffer))
-
--- | Evaluate several streams for a number of steps, producing the environment
--- at the end of the evaluation.
-evalStreams :: Int -> [Stream] -> Env Id -> Env Id
-evalStreams top specStrms initStrms =
-  -- XXX actually only need to compute until shortest stream is of length k
-  -- XXX this should just be a foldl' over [0,1..k]
-  evalStreams_ 0 initStrms
-  where
-  evalStreams_ :: Int -> Env Id -> Env Id
-  evalStreams_ k strms | k == top  = strms
-  evalStreams_ k strms | otherwise =
-    evalStreams_ (k+1) $! strms_
-    where
-    strms_ = map evalStream specStrms
-    evalStream Stream { streamId       = id
-                      , streamExpr     = e
-                      , streamExprType = t } =
-      let xs = fromJust $ lookup id strms >>= fromDynamic      in
-      let x  = evalExpr_ k e [] strms                          in
-      let ls = x `seq` (x:xs)                                  in
-      (id, toDyn ls)
-
--- | Evaluate a trigger for a number of steps.
-evalTrigger :: ShowType          -- ^ Show booleans as @0@/@1@ (C) or
-                                 --   @True@/@False@ (Haskell).
-            -> Int               -- ^ Number of steps to evaluate.
-            -> Env Id            -- ^ Environment to use with known
-                                 --   stream-value associations.
-            -> Trigger           -- ^ Trigger to evaluate.
-            -> [Maybe [Output]]
-evalTrigger showType k strms
-  Trigger
-    { triggerGuard = e
-    , triggerArgs  = args
-    } = map tag (zip bs vs)
-
-  where
-  tag :: (Bool, a) -> Maybe a
-  tag (True,  x) = Just x
-  tag (False, _) = Nothing
-
-  -- Is the guard true?
-  bs :: [Bool]
-  bs = evalExprs_ k e strms
-
-  -- The argument outputs.
-  vs :: [[Output]]
-  vs = if null args then replicate k []  -- might be 0 args.
-         else transpose $ map evalUExpr args
-
-  evalUExpr :: UExpr -> [Output]
-  evalUExpr (UExpr t e1) =
-    map (showWithType showType t) (evalExprs_ k e1 strms)
-
--- | Evaluate an observer for a number of steps.
-evalObserver :: ShowType  -- ^ Show booleans as @0@/@1@ (C) or @True@/@False@
-                          --   (Haskell).
-             -> Int       -- ^ Number of steps to evaluate.
-             -> Env Id    -- ^ Environment to use with known stream-value
-                          --   associations.
-             -> Observer  -- ^ Observer to evaluate.
-             -> [Output]
-evalObserver showType k strms
-  Observer
-    { observerExpr     = e
-    , observerExprType = t }
-  = map (showWithType showType t) (evalExprs_ k e strms)
-
--- | Evaluate an expression for a number of steps, producing a list with the
--- changing value of the expression until that time.
-evalExprs_ :: Typeable a => Int -> Expr a -> Env Id -> [a]
-evalExprs_ k e strms =
-  map (\i -> evalExpr_ i e [] strms) [0..(k-1)]
-
--- | Safe indexing (!!) on possibly infininite lists.
-safeIndex :: Int -> [a] -> Maybe a
-safeIndex i ls =
-  let ls' = take (i+1) ls in
-  if length ls' > i then Just (ls' !! i)
-    else Nothing
diff --git a/src/Copilot/Core/Interpret/Render.hs b/src/Copilot/Core/Interpret/Render.hs
deleted file mode 100644
--- a/src/Copilot/Core/Interpret/Render.hs
+++ /dev/null
@@ -1,127 +0,0 @@
--- The following warning is enabled in this module so that the import of
--- Copilot.Core.Interpret.Eval does not give rise to a warning.
-{-# OPTIONS_GHC -fno-warn-deprecations #-}
-
--- Copyright © 2011 National Institute of Aerospace / Galois, Inc.
-
--- | Pretty-print the results of a simulation.
-
-{-# LANGUAGE Safe #-}
-
-module Copilot.Core.Interpret.Render
-  {-# DEPRECATED "This module is deprecated in Copilot 3.11. Use copilot-interpreter instead." #-}
-  ( renderAsTable
-  , renderAsCSV
-  ) where
-
-import Data.List (intersperse, transpose, foldl')
-import Data.Maybe (catMaybes)
-import Copilot.Core.Interpret.Eval (Output, ExecTrace (..))
-import Text.PrettyPrint
-
-import Prelude hiding ((<>))
-
--- | Render an execution trace as a table, formatted to faciliate readability.
-renderAsTable :: ExecTrace -> String
-renderAsTable
-  ExecTrace
-    { interpTriggers  = trigs
-    , interpObservers = obsvs } = ( render
-                                  . asColumns
-                                  . transpose
-                                  . (:) (ppTriggerNames ++ ppObserverNames)
-                                  . transpose
-                                  ) (ppTriggerOutputs ++ ppObserverOutputs)
-     where
-
-     ppTriggerNames :: [Doc]
-     ppTriggerNames  = map (text . (++ ":")) (map fst trigs)
-
-     ppObserverNames :: [Doc]
-     ppObserverNames = map (text . (++ ":")) (map fst obsvs)
-
-     ppTriggerOutputs :: [[Doc]]
-     ppTriggerOutputs = map (map ppTriggerOutput) (map snd trigs)
-
-     ppTriggerOutput :: Maybe [Output] -> Doc
-     ppTriggerOutput (Just vs) = text $ "(" ++ concat (intersperse "," vs) ++ ")"
-     ppTriggerOutput Nothing   = text "--"
-
-     ppObserverOutputs :: [[Doc]]
-     ppObserverOutputs = map (map text) (map snd obsvs)
-
--- | Render an execution trace as using comma-separate value (CSV) format.
-renderAsCSV :: ExecTrace -> String
-renderAsCSV = render . unfold
-
--- | Pretty print all the steps of the execution trace and concatenate the
--- results.
-unfold :: ExecTrace -> Doc
-unfold r =
-  case step r of
-    (cs, Nothing) -> cs
-    (cs, Just r') -> cs $$ unfold r'
-
--- | Pretty print the state of the triggers, and provide a continuation
--- for the execution trace at the next point in time.
-step :: ExecTrace -> (Doc, Maybe ExecTrace)
-step ExecTrace
-       { interpTriggers  = trigs
-       } =
-  if null trigs then (empty, Nothing)
-    else (foldl' ($$) empty (text "#" : ppTriggerOutputs), tails)
-
-  where
-
-  ppTriggerOutputs :: [Doc]
-  ppTriggerOutputs =
-      catMaybes
-    . fmap ppTriggerOutput
-    . map (fmap head)
-    $ trigs
-
-  ppTriggerOutput :: (String, Maybe [Output]) -> Maybe Doc
-  ppTriggerOutput (_,  Nothing) = Nothing
-  ppTriggerOutput (cs, Just xs) = Just $
-    text cs <> text "," <>
-      (foldr (<>) empty . map text . intersperse ",") xs
-
-  tails :: Maybe ExecTrace
-  tails =
-    if any null (fmap (tail.snd) trigs)
-      then Nothing
-      else Just
-        ExecTrace
-          { interpTriggers  = map (fmap tail) trigs
-          , interpObservers = []
-          }
-
--- Copied from pretty-ncols because of incompatibility with newer GHC versions.
-asColumns :: [[Doc]] -> Doc
-asColumns = flip asColumnsWithBuff $ 1
-
-asColumnsWithBuff :: [[Doc]] -> Int -> Doc
-asColumnsWithBuff lls q = normalize
-        where
-          normalize = vcat $ map hsep
-                    $ map (\x -> pad (length x) longColumnLen empty x)
-                    $ pad' longEntryLen q
-                    $ transpose lls -- normalize column height
-          longColumnLen = maximum (map length lls)
-          longEntryLen = maximum $ map docLen (concat lls)
-
-docLen d = length $ render d
-
--- | Pad a string on the right to reach an expected length.
-pad :: Int -> Int -> a -> [a] -> [a]
-pad lx max b ls = ls ++ replicate (max - lx) b
-
--- | Pad a list of strings on the right with spaces.
-pad' :: Int      -- ^ Mininum number of spaces to add
-     -> Int      -- ^ Maximum number of spaces to add
-     -> [[Doc]]  -- ^ List of documents to pad
-     -> [[Doc]]
-pad' _ _ []       = []
-pad' mx q (ls:xs) = map buf ls : pad' mx q xs
-        where
-          buf x = x <> (hcat $ replicate q space) <> (hcat $ replicate (mx - (docLen x)) space)
diff --git a/src/Copilot/Core/PrettyDot.hs b/src/Copilot/Core/PrettyDot.hs
deleted file mode 100644
--- a/src/Copilot/Core/PrettyDot.hs
+++ /dev/null
@@ -1,306 +0,0 @@
--- Copyright © 2011 National Institute of Aerospace / Galois, Inc.
-
--- | A pretty printer for Copilot specifications as GraphViz/dot graphs.
-
-{-# LANGUAGE GADTs #-}
-{-# LANGUAGE Safe  #-}
-
-module Copilot.Core.PrettyDot
-  {-# DEPRECATED "This module is deprecated in Copilot 3.11." #-}
-  ( prettyPrintDot
-  , prettyPrintExprDot
-  ) where
-
-import Copilot.Core
-import Copilot.Core.Type.Show (showWithType, ShowType(..), showType)
-import Prelude hiding (id, (<>))
-import Text.PrettyPrint.HughesPJ
-import Data.List (intersperse)
-import Text.Printf
-
--- | Create a temporary/internal name from an extern variable name.
-mkExtTmpVar :: String -> String
-mkExtTmpVar = ("ext_" ++)
-
--- | Pretty print a Copilot Expression as a GraphViz graph part.
---
--- See the
--- <https://github.com/Copilot-Language/copilot-discussion/tree/master/TutorialAndDevGuide/DevGuide development guide> for details.
-ppExprDot :: Int       -- ^ Index or ID of the next node in the graph.
-          -> Int       -- ^ Index or ID of the parent node in the graph.
-          -> Bool      -- ^ Mark externs with the prefix @externV:@.
-          -> Expr a    -- ^ The expression to pretty print.
-          -> (Doc,Int)
-ppExprDot ii pere bb e0 = case e0 of
-  Const t x                  -> (text (printf "%s [label=\"const: %s\",color=red1, style=filled]\n" (show ii::String) ((showWithType Haskell t x)::String) )
-                  <> text (printf "%s -> %s\n" (show pere::String) (show ii::String)),ii+1)
-  Drop _ 0 id                -> (text (printf "%s [label=\"stream: %s\",color=crimson, style=filled]\n" (show ii::String) (show id::String) )
-                  <> text (printf "%s -> %s\n" (show pere::String) (show ii::String)),ii+1)
-  Drop _ i id                ->  (text (printf "%s [label=\"drop %s: \nstream: %s\",color=crimson, style=filled]\n" (show ii::String) (show i::String) (show id::String) )
-                  <> text (printf "%s -> %s\n" (show pere::String) (show ii::String)),ii+1)
-  ExternVar _ name _         -> (if bb
-                                   then (text (printf "%s [label=\"externV: %s\",color=cyan1, style=filled]\n" (show ii::String) (name::String)) <> text (printf "%s -> %s\n" (show pere::String) (show ii::String)))
-                                   else (text (printf "%s [label=\"%s\",color=cyan1, style=filled]\n" (show ii::String) (mkExtTmpVar name))      <> text (printf "%s -> %s\n" (show pere::String) (show ii::String)))
-                  ,ii+1)
-  Local _ _ name e1 e2       -> let (r1, i1) = ppExprDot (ii+2) (ii+1) bb e1
-                                in let (r2, i2) = ppExprDot (i1) ii bb e2
-                                in (text (printf "%s [label=\"local:\",color=blue, style=filled]\n" (show ii::String) )
-                  <> text (printf "%s -> %s\n" (show pere::String) (show ii::String))
-                  <> text (printf "%s [label=\"def: %s\",color=blue, style=filled]\n" ((show $ ii+1)::String) (name::String) )
-                  <> text (printf "%s -> %s\n" (show ii::String) (show $ ii+1::String))
-                  <> r1
-                  <> r2, i2)
-
-  Var _ name                 -> (text (printf "%s [label=\"var: %s\",color=blue, style=filled]\n" (show ii::String) (name::String) )
-                  <> text (printf "%s -> %s\n" (show pere::String) (show ii::String)),ii+1)
-
-  Op1 op e                   -> let (r1,i1) = ppExprDot (ii+1) ii bb e
-           in (text (printf "%s [label=\"op1: %s\",color=green4, style=filled]\n" (show ii::String) (ppOp1 op::String))
-                  <> text (printf "%s -> %s\n" (show pere::String) (show ii::String))
-                  <> r1,i1)
-
-  Op2 op e1 e2               -> let (r1,i1) = ppExprDot (ii+1) ii bb e1
-                                in let (r2,i2) = ppExprDot i1 ii bb e2
-           in (text (printf "%s [label=\"op2: %s\",color=green4, style=filled]\n" (show ii::String) (ppOp2 op::String))
-                  <> text (printf "%s -> %s\n" (show pere::String) (show ii::String))
-                  <> r1
-                  <> r2, i2)
-  Op3 op e1 e2 e3            -> let (r1,i1) = ppExprDot (ii+1) ii bb e1
-                                in let (r2,i2) = ppExprDot i1 ii bb e2
-                                in let (r3,i3) = ppExprDot i2 ii bb e3
-           in (text (printf "%s [label=\"op3: %s\",color=green4, style=filled]\n" (show ii::String) (ppOp3 op::String))
-                  <> text (printf "%s -> %s\n" (show pere::String) (show ii::String))
-                  <> r1
-                  <> r2
-                  <> r3, i3)
-
-  Label _ s e                -> let (r1,i1) = ppExprDot (ii+1) ii bb e
-           in (text (printf "%s [label=\"label: %s\",color=plum, style=filled]\n" (show ii::String) (s::String))
-                  <> text (printf "%s -> %s\n" (show pere::String) (show ii::String))
-                  <> r1,i1)
-
--- | Pretty print an untyped Copilot Expression as a graphiViz graph part.
---
--- See the
--- <https://github.com/Copilot-Language/copilot-discussion/tree/master/TutorialAndDevGuide/DevGuide development guide> for details.
-ppUExpr :: Int        -- ^ Index or ID of the next node in the graph.
-        -> Int        -- ^ Index or ID of the parent node in the graph.
-        -> Bool       -- ^ Mark externs with the prefix @externV:@.
-        -> UExpr      -- ^ The expression to pretty print.
-        -> (Doc, Int)
-ppUExpr i pere bb UExpr { uExprExpr = e0 } = ppExprDot i pere bb e0
-
--- | Pretty print a unary operator.
-ppOp1 :: Op1 a b -> String
-ppOp1 op = case op of
-  Not       -> "not"
-  Abs _     -> "abs"
-  Sign _    -> "signum"
-  Recip _   -> "recip"
-  Exp _     -> "exp"
-  Sqrt _    -> "sqrt"
-  Log _     -> "log"
-  Sin _     -> "sin"
-  Tan _     -> "tan"
-  Cos _     -> "cos"
-  Asin _    -> "asin"
-  Atan _    -> "atan"
-  Acos _    -> "acos"
-  Sinh _    -> "sinh"
-  Tanh _    -> "tanh"
-  Cosh _    -> "cosh"
-  Asinh _   -> "asinh"
-  Atanh _   -> "atanh"
-  Acosh _   -> "acosh"
-  Ceiling _ -> "ceiling"
-  Floor _   -> "floor"
-  BwNot _   -> "~"
-  Cast _ _  -> "(cast)"
-
--- | Pretty print a binary operator.
-ppOp2 :: Op2 a b c -> String
-ppOp2 op = case op of
-  And          -> "&&"
-  Or           -> "||"
-  Add      _   -> "+"
-  Sub      _   -> "-"
-  Mul      _   -> "*"
-  Div      _   -> "div"
-  Mod      _   -> "mod"
-  Fdiv     _   -> "/"
-  Pow      _   -> "**"
-  Logb     _   -> "logBase"
-  Atan2    _   -> "atan2"
-  Eq       _   -> "=="
-  Ne       _   -> "/="
-  Le       _   -> "<="
-  Ge       _   -> ">="
-  Lt       _   -> "<"
-  Gt       _   -> ">"
-  BwAnd    _   -> "&"
-  BwOr     _   -> "|"
-  BwXor    _   -> "^"
-  BwShiftL _ _ -> "<<"
-  BwShiftR _ _ -> ">>"
-
--- | Pretty print a ternary operator.
-ppOp3 :: Op3 a b c d -> String
-ppOp3 op = case op of
-  Mux _    -> "mux"
-
--- | Pretty print a stream as a GraphViz graph part.
-ppStream :: Int        -- ^ Index or ID of the next node in the graph.
-         -> Stream     -- ^ Stream to pretty print
-         -> (Doc, Int)
-ppStream i
-  Stream
-    { streamId       = id
-    , streamBuffer   = buffer
-    , streamExpr     = e
-    , streamExprType = t
-    }
-      =
-  (text (printf "%s [label=\"stream: %s\ntype: %s\",color=mediumblue, style=filled]\n" (show i::String) (show id::String) (showType t::String))
-    <> text (printf "%s [label=\"++\",color=yellow, style=filled]\n" ((show $ i+1)::String))
-    <> text (printf "%s -> %s\n" (show i::String) ((show $ i+1)::String))
-    <> text (printf "%s [label=\"[%s]\",color=green, style=filled]\n" ((show $ i+2)::String) ((concat $ intersperse "," $ map (showWithType Haskell t) buffer )) ::String)
-    <> text (printf "%s -> %s\n" (show (i+1)::String) ((show $ i+2)::String))
-    <> r1, i1)
-    where
-      (r1, i1) = ppExprDot (i+3) (i+1) True e
-
--- | Pretty print a trigger as a GraphViz graph part.
-ppTrigger :: Int        -- ^ Index or ID of the next node in the graph.
-          -> Trigger    -- ^ Trigger to pretty print
-          -> (Doc, Int)
-ppTrigger i
-  Trigger
-    { triggerName  = name
-    , triggerGuard = e
-    , triggerArgs  = args }
-  =  ( text (printf "%s [label=\"trigger: %s\",color=mediumblue, style=filled]\n" (show i::String) (name::String) )
-  <> text (printf "%s [label=\"guard\",color=yellow, style=filled]\n" ((show $ i+1)::String))
-  <> text (printf "%s -> %s\n" (show i::String) ((show $ i+1)::String))
-  <> r1
-  <> text (printf "%s [label=\"args\",color=yellow, style=filled]\n" (show i1::String))
-  <> text (printf "%s -> %s\n" (show i::String) (show i1::String))
-  <>  (vcat (r2))
-  ,i2)
-  where
-    (r1, i1) = ppExprDot (i+2) (i+1) True e
-    (r2, i2) = ppUExprL (i1+1) (i1) True args
-
--- | Pretty print a list of untyped Copilot Expressions as a GraphViz graph
--- part.
-ppUExprL :: Int           -- ^ Index or ID of the next node in the graph.
-         -> Int           -- ^ Index or ID of the parent node in the graph.
-         -> Bool          -- ^ Mark externs with the prefix @externV:@.
-         -> [UExpr]       -- ^ The list of expressions to pretty print.
-         -> ([Doc], Int)
-ppUExprL i _ _ [] = ([], i)
-
-ppUExprL i pere bb (a:b) = ((r1:r2), i2)
-  where
-    (r1, i1) = ppUExpr i pere bb a
-    (r2, i2) = ppUExprL i1 pere bb b
-
--- | Pretty print an observer as a GraphViz graph part.
-ppObserver :: Int         -- ^ Index or ID of the next node in the graph.
-           -> Observer    -- ^ Observer to pretty print
-           -> (Doc, Int)
-ppObserver i
-  Observer
-    { observerName     = name
-    , observerExpr     = e }
-  =
-  (text (printf "%s [label=\"observer: \n%s\",color=mediumblue, style=filled]\n" (show i::String) name::String)
-  <> r1, i1)
-  where
-    (r1, i1) = ppExprDot (i+1) i True e
-
--- | Pretty print a property as a GraphViz graph part.
-ppProperty :: Int         -- ^ Index or ID of the next node in the graph.
-           -> Property    -- ^ Property to pretty print
-           -> (Doc, Int)
-ppProperty i
-  Property
-    { propertyName     = name
-    , propertyExpr     = e }
-  =
-  (text (printf "%s [label=\"property: \n%s\",color=mediumblue, style=filled]\n" (show i::String) name::String)
-  <> r1, i1)
-  where
-    (r1, i1) = ppExprDot (i+1) i True e
-
--- | Pretty print a list of streams as a GraphViz graph part.
-ppStreamL :: Int        -- ^ Index or ID of the next node in the graph.
-          -> [Stream]   -- ^ List of streams to pretty print
-          -> (Doc, Int)
-ppStreamL i [] = (empty,i)
-
-ppStreamL i (a:b) = ((s1$$s2),(i2))
-  where
-    (s1,i1) = ppStream i a
-    (s2,i2) = ppStreamL i1 b
-
--- | Pretty print a list of triggers as a GraphViz graph part.
-ppTriggerL :: Int        -- ^ Index or ID of the next node in the graph.
-           -> [Trigger]  -- ^ List of triggers to pretty print
-           -> (Doc, Int)
-ppTriggerL i [] = (empty,i)
-
-ppTriggerL i (a:b) = ((s1$$s2),(i2))
-  where
-    (s1,i1) = ppTrigger i a
-    (s2,i2) = ppTriggerL i1 b
-
--- | Pretty print a list of observers as a GraphViz graph part.
-ppObserverL :: Int         -- ^ Index or ID of the next node in the graph.
-            -> [Observer]  -- ^ List of observers to pretty print
-            -> (Doc, Int)
-ppObserverL i [] = (empty,i)
-
-ppObserverL i (a:b) = ((s1$$s2),(i2))
-  where
-    (s1,i1) = ppObserver i a
-    (s2,i2) = ppObserverL i1 b
-
--- | Pretty print a list of properties as a GraphViz graph part.
-ppPropertyL :: Int         -- ^ Index or ID of the next node in the graph.
-            -> [Property]  -- ^ List of properties to pretty print
-            -> (Doc, Int)
-ppPropertyL i [] = (empty,i)
-
-ppPropertyL i (a:b) = ((s1$$s2),(i2))
-  where
-    (s1,i1) = ppProperty i a
-    (s2,i2) = ppPropertyL i1 b
-
--- | Pretty-print a Copilot specification as a GraphViz/dot graph.
-ppSpecDot :: Int        -- ^ Index or ID of the next node in the graph.
-          -> Spec       -- ^ Spec to pretty print.
-          -> (Doc, Int)
-ppSpecDot i spec =
-  ((aa $$ cs $$ ds $$ es $$ fs $$ bb),i4)
-  where
-    aa = text "digraph G {\nnode [shape=box]\n"
-    (cs, i1) = ppStreamL i    (specStreams    spec)
-    (ds, i2) = ppTriggerL i1  (specTriggers   spec)
-    (es, i3) = ppObserverL i2 (specObservers  spec)
-    (fs, i4) = ppPropertyL i3 (specProperties spec)
-    bb = text "\n}\n"
-
--- | Pretty-print a Copilot expression as a GraphViz/dot graph.
-prettyPrintExprDot :: Bool     -- ^ Mark externs with the prefix @externV:@.
-                   -> Expr a   -- ^ The expression to pretty print.
-                   -> String
-prettyPrintExprDot bb s = render rr
-  where
-    (r1, _) = ppExprDot 1 0 bb s
-    rr = text "digraph G {\nnode [shape=box]\n" $$ (text "0 [label=\"file: \n?????\",color=red, style=filled]\n") <> r1 $$ text "\n}\n"
-
--- | Pretty-print a Copilot specification as a GraphViz/dot graph.
-prettyPrintDot :: Spec -> String
-prettyPrintDot s = render r1
-  where
-    (r1, _) = ppSpecDot 0 s
diff --git a/src/Copilot/Core/Type/Array.hs b/src/Copilot/Core/Type/Array.hs
--- a/src/Copilot/Core/Type/Array.hs
+++ b/src/Copilot/Core/Type/Array.hs
@@ -1,11 +1,8 @@
-{-# LANGUAGE DataKinds             #-}
-{-# LANGUAGE FlexibleInstances     #-}
-{-# LANGUAGE GADTs                 #-}
-{-# LANGUAGE MultiParamTypeClasses #-}
-{-# LANGUAGE Safe                  #-}
-{-# LANGUAGE ScopedTypeVariables   #-}
-{-# LANGUAGE TypeFamilies          #-}
-{-# LANGUAGE TypeOperators         #-}
+{-# LANGUAGE DataKinds           #-}
+{-# LANGUAGE GADTs               #-}
+{-# LANGUAGE Safe                #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeFamilies        #-}
 
 -- |
 -- Copyright: (c) 2011 National Institute of Aerospace / Galois, Inc.
@@ -16,10 +13,6 @@
 module Copilot.Core.Type.Array
     ( Array
     , array
-    , flatten
-    , size
-    , Flatten
-    , InnerType
     , arrayelems
     )
   where
@@ -45,36 +38,6 @@
     typelen = fromIntegral $ natVal (Proxy :: Proxy n)
     errmsg = "Length of data (" ++ show datalen ++
              ") does not match length of type (" ++ show typelen ++ ")."
-
--- | Association between an array and the type of the elements it contains.
-{-# DEPRECATED InnerType "This type family is deprecated in Copilot 3.11." #-}
-type family InnerType x where
-  InnerType (Array _ x) = InnerType x
-  InnerType x           = x
-
--- | Flattening or conversion of arrays to lists.
-{-# DEPRECATED Flatten "This class is deprecated in Copilot 3.11." #-}
-{-# DEPRECATED flatten "This function is deprecated in Copilot 3.11." #-}
-class Flatten a b where
-  -- | Flatten an array to a list.
-  flatten :: Array n a -> [b]
-
--- | Flattening of plain arrays.
-instance Flatten a a where
-  flatten (Array xs) = xs
-
--- | Flattening of nested arrays.
-instance Flatten a b => Flatten (Array n a) b where
-  flatten (Array xss) = concat $ map flatten xss
-
--- | This instance is deprecated in Copilot 3.11.
-instance Foldable (Array n) where
-  foldr f base (Array xs) = foldr f base xs
-
--- | Total number of elements in a possibly nested array.
-{-# DEPRECATED size "This function is deprecated in Copilot 3.11." #-}
-size :: forall a n b. (Flatten a b, b ~ InnerType a) => Array n a -> Int
-size xs = length $ (flatten xs :: [b])
 
 -- | Return the elemts of an array.
 arrayelems :: Array n a -> [a]
diff --git a/tests/Test/Copilot/Core/Type/Array.hs b/tests/Test/Copilot/Core/Type/Array.hs
--- a/tests/Test/Copilot/Core/Type/Array.hs
+++ b/tests/Test/Copilot/Core/Type/Array.hs
@@ -13,7 +13,7 @@
                                              vectorOf)
 
 -- Internal imports: library modules being tested
-import Copilot.Core.Type.Array (Array, array, arrayelems, flatten, size)
+import Copilot.Core.Type.Array (Array, array, arrayelems)
 
 -- | All unit tests for copilot-core:Copilot.Core.Array.
 tests :: Test.Framework.Test
@@ -25,30 +25,6 @@
         (testArrayElemsLeft (Proxy :: Proxy 5))
     , testProperty "arrayElems . array (identity; 200)"
         (testArrayElemsLeft (Proxy :: Proxy 200))
-    , testProperty "arrayFlatten . array (identity; 0)"
-        (testArrayFlattenLeft (Proxy :: Proxy 0))
-    , testProperty "arrayFlatten . array (identity; 1)"
-        (testArrayFlattenLeft (Proxy :: Proxy 1))
-    , testProperty "arrayFlatten . array (identity; 2)"
-        (testArrayFlattenLeft (Proxy :: Proxy 2))
-    , testProperty "arrayFlatten . array (identity; 22)"
-        (testArrayFlattenLeft (Proxy :: Proxy 22))
-    , testProperty "arrayFlatten . array (identity; 50)"
-        (testArrayFlattenLeft (Proxy :: Proxy 50))
-    , testProperty "arrayFlatten . array (identity; nested; nested; 2x6)"
-        (testArrayFlattenNestedLeft (Proxy :: Proxy 2) (Proxy :: Proxy 6))
-    , testProperty "arrayFlatten . array (identity; nested; nested; 10x2)"
-        (testArrayFlattenNestedLeft (Proxy :: Proxy 10) (Proxy :: Proxy 2))
-    , testProperty "arrayFlatten . array (identity; nested; nested; 38x20)"
-        (testArrayFlattenNestedLeft (Proxy :: Proxy 38) (Proxy :: Proxy 20))
-    , testProperty "arrayFlatten . array (identity; nested; nested; 125x100)"
-        (testArrayFlattenNestedLeft (Proxy :: Proxy 125) (Proxy :: Proxy 100))
-    , testProperty "arraySize . array (identity; 0)"
-        (testArraySizeLeft (Proxy :: Proxy 0))
-    , testProperty "arraySize . array (identity; 45)"
-        (testArraySizeLeft (Proxy :: Proxy 45))
-    , testProperty "arraySize . array (identity; 100)"
-        (testArraySizeLeft (Proxy :: Proxy 100))
     ]
 
 -- * Individual tests
@@ -61,69 +37,6 @@
       let array' :: Array n Int64
           array' = array ls
       in arrayelems array' == ls
-
-  where
-
-    -- Generator for lists of Int64 of known length.
-    xsInt64 :: Gen [Int64]
-    xsInt64 = vectorOf (fromIntegral (natVal len)) arbitrary
-
--- | Test that building an array from a list and extracting the elements with
--- the function 'flatten' will result in the same list.
---
--- This test tests only plain arrays (no nesting).
-testArrayFlattenLeft :: forall n . KnownNat n => Proxy n -> Property
-testArrayFlattenLeft len =
-    forAll xsInt64 $ \ls ->
-      let array' :: Array n Int64
-          array' = array ls
-      in flatten array' == ls
-
-  where
-
-    -- Generator for lists of Int64 of known length.
-    xsInt64 :: Gen [Int64]
-    xsInt64 = vectorOf (fromIntegral (natVal len)) arbitrary
-
--- | Test that building a nested array of a known size and extracting the
--- elements with the function 'flatten' will result in a list with a size that
--- is the product of the sizes provided.
-testArrayFlattenNestedLeft :: forall n1 n2
-                           .  (KnownNat n1, KnownNat n2)
-                           => Proxy n1
-                           -> Proxy n2
-                           -> Property
-testArrayFlattenNestedLeft len1 len2 =
-    forAll xsArrays $ \array' ->
-      length (flatten array' :: [Int64]) == expectedSize
-
-  where
-
-    -- Expected size of the matrix / array.
-    expectedSize :: Int
-    expectedSize = fromIntegral $ natVal len1 * natVal len2
-
-    -- Generator for nested matrices of Int64 of known size.
-    xsArrays :: Gen (Array n1 (Array n2 Int64))
-    xsArrays =
-      array <$> vectorOf (fromIntegral (natVal len1)) xsArrayInt64
-
-    -- Generator for arrays of Int64 of known length.
-    xsArrayInt64 :: Gen (Array n2 Int64)
-    xsArrayInt64 = array <$> xsInt64
-
-    -- Generator for lists of Int64 of known length.
-    xsInt64 :: Gen [Int64]
-    xsInt64 = vectorOf (fromIntegral (natVal len2)) arbitrary
-
--- | Test that building an array from a list and calculating the size will
--- return the length of the list.
-testArraySizeLeft :: forall n . KnownNat n => Proxy n -> Property
-testArraySizeLeft len =
-    forAll xsInt64 $ \ls ->
-      let array' :: Array n Int64
-          array' = array ls
-      in size array' == length ls
 
   where