From 7e990efd365f0a52b7b4ffa8fc500f399d95c049 Mon Sep 17 00:00:00 2001
From: Rob Rix <robrix@github.com>
Date: Fri, 15 Mar 2024 10:55:23 -0400
Subject: [PATCH 01/59] Define a VM module.

---
 semantic-analysis/semantic-analysis.cabal | 1 +
 semantic-analysis/src/Analysis/VM.hs      | 2 ++
 2 files changed, 3 insertions(+)
 create mode 100644 semantic-analysis/src/Analysis/VM.hs

diff --git a/semantic-analysis/semantic-analysis.cabal b/semantic-analysis/semantic-analysis.cabal
index 058f47e232..9cc6771a6f 100644
--- a/semantic-analysis/semantic-analysis.cabal
+++ b/semantic-analysis/semantic-analysis.cabal
@@ -69,6 +69,7 @@ library
     Analysis.Project
     Analysis.Reference
     Analysis.Syntax
+    Analysis.VM
   build-depends:
     , aeson                        >= 1.4 && < 3
     , base                         >= 4.13 && < 5
diff --git a/semantic-analysis/src/Analysis/VM.hs b/semantic-analysis/src/Analysis/VM.hs
new file mode 100644
index 0000000000..c29ad06439
--- /dev/null
+++ b/semantic-analysis/src/Analysis/VM.hs
@@ -0,0 +1,2 @@
+module Analysis.VM
+() where

From 186ae4f2bc4367187098201433c5628407dfff3e Mon Sep 17 00:00:00 2001
From: Rob Rix <robrix@github.com>
Date: Fri, 15 Mar 2024 10:56:12 -0400
Subject: [PATCH 02/59] Re-export env & store effects.

---
 semantic-analysis/src/Analysis/VM.hs | 7 ++++++-
 1 file changed, 6 insertions(+), 1 deletion(-)

diff --git a/semantic-analysis/src/Analysis/VM.hs b/semantic-analysis/src/Analysis/VM.hs
index c29ad06439..04e39701ac 100644
--- a/semantic-analysis/src/Analysis/VM.hs
+++ b/semantic-analysis/src/Analysis/VM.hs
@@ -1,2 +1,7 @@
 module Analysis.VM
-() where
+( module Analysis.Effect.Env
+, module Analysis.Effect.Store
+) where
+
+import Analysis.Effect.Env
+import Analysis.Effect.Store

From 94b463e780bc46c7374cbc7ef91bf876cd89eda9 Mon Sep 17 00:00:00 2001
From: Rob Rix <robrix@github.com>
Date: Fri, 15 Mar 2024 10:57:47 -0400
Subject: [PATCH 03/59] Move let' & letrec into the VM module.

---
 semantic-analysis/src/Analysis/Syntax.hs | 22 +---------------------
 semantic-analysis/src/Analysis/VM.hs     | 24 +++++++++++++++++++++++-
 2 files changed, 24 insertions(+), 22 deletions(-)

diff --git a/semantic-analysis/src/Analysis/Syntax.hs b/semantic-analysis/src/Analysis/Syntax.hs
index 36655e4c25..d3aa308b23 100644
--- a/semantic-analysis/src/Analysis/Syntax.hs
+++ b/semantic-analysis/src/Analysis/Syntax.hs
@@ -13,9 +13,6 @@ module Analysis.Syntax
   -- * Abstract interpretation
 , eval0
 , eval
-  -- * Macro-expressible syntax
-, let'
-, letrec
   -- * Parsing
 , parseFile
 , parseGraph
@@ -27,11 +24,10 @@ module Analysis.Syntax
 
 import qualified Analysis.Carrier.Statement.State as S
 import           Analysis.Effect.Domain
-import           Analysis.Effect.Env (Env, bind, lookupEnv)
-import           Analysis.Effect.Store
 import           Analysis.File
 import           Analysis.Name (Name, name)
 import           Analysis.Reference as Ref
+import           Analysis.VM
 import           Control.Applicative (Alternative (..), liftA2, liftA3)
 import           Control.Carrier.Throw.Either (runThrow)
 import           Control.Effect.Labelled
@@ -128,22 +124,6 @@ eval eval = \case
   setSpan s r = r{ refSpan = s }
 
 
--- Macro-expressible syntax
-
-let' :: (Has (Env addr) sig m, HasLabelled Store (Store addr val) sig m) => Name -> val -> m a -> m a
-let' n v m = do
-  addr <- alloc n
-  addr .= v
-  bind n addr m
-
-letrec :: (Has (Env addr) sig m, HasLabelled Store (Store addr val) sig m) => Name -> m val -> m val
-letrec n m = do
-  addr <- alloc n
-  v <- bind n addr m
-  addr .= v
-  pure v
-
-
 -- Parsing
 
 parseFile :: (Has (Throw String) sig m, MonadIO m) => FilePath -> FilePath -> m (Source.Source, File Term)
diff --git a/semantic-analysis/src/Analysis/VM.hs b/semantic-analysis/src/Analysis/VM.hs
index 04e39701ac..59c3b9eae2 100644
--- a/semantic-analysis/src/Analysis/VM.hs
+++ b/semantic-analysis/src/Analysis/VM.hs
@@ -1,7 +1,29 @@
+{-# LANGUAGE FlexibleContexts #-}
 module Analysis.VM
-( module Analysis.Effect.Env
+( -- * Macro-expressible syntax
+  let'
+, letrec
+  -- * Re-exports
+, module Analysis.Effect.Env
 , module Analysis.Effect.Store
 ) where
 
 import Analysis.Effect.Env
 import Analysis.Effect.Store
+import Analysis.Name
+import Control.Effect.Labelled
+
+-- Macro-expressible syntax
+
+let' :: (Has (Env addr) sig m, HasLabelled Store (Store addr val) sig m) => Name -> val -> m a -> m a
+let' n v m = do
+  addr <- alloc n
+  addr .= v
+  bind n addr m
+
+letrec :: (Has (Env addr) sig m, HasLabelled Store (Store addr val) sig m) => Name -> m val -> m val
+letrec n m = do
+  addr <- alloc n
+  v <- bind n addr m
+  addr .= v
+  pure v

From 9df11b44e6a0d3dd151c5504ce267c7af7e80550 Mon Sep 17 00:00:00 2001
From: Rob Rix <robrix@github.com>
Date: Fri, 15 Mar 2024 11:00:34 -0400
Subject: [PATCH 04/59] Define a module for Python syntax.

---
 semantic-analysis/semantic-analysis.cabal       | 1 +
 semantic-analysis/src/Analysis/Syntax/Python.hs | 3 +++
 2 files changed, 4 insertions(+)
 create mode 100644 semantic-analysis/src/Analysis/Syntax/Python.hs

diff --git a/semantic-analysis/semantic-analysis.cabal b/semantic-analysis/semantic-analysis.cabal
index 9cc6771a6f..82545b3cb0 100644
--- a/semantic-analysis/semantic-analysis.cabal
+++ b/semantic-analysis/semantic-analysis.cabal
@@ -69,6 +69,7 @@ library
     Analysis.Project
     Analysis.Reference
     Analysis.Syntax
+    Analysis.Syntax.Python
     Analysis.VM
   build-depends:
     , aeson                        >= 1.4 && < 3
diff --git a/semantic-analysis/src/Analysis/Syntax/Python.hs b/semantic-analysis/src/Analysis/Syntax/Python.hs
new file mode 100644
index 0000000000..cf73f4a12f
--- /dev/null
+++ b/semantic-analysis/src/Analysis/Syntax/Python.hs
@@ -0,0 +1,3 @@
+-- | This belongs in @semantic-python@ instead of @semantic-analysis@, but for the sake of expedience…
+module Analysis.Syntax.Python
+() where

From 14cdce0d65720f3c70341b067cfb54a8477bcdfa Mon Sep 17 00:00:00 2001
From: Rob Rix <robrix@github.com>
Date: Fri, 15 Mar 2024 11:04:11 -0400
Subject: [PATCH 05/59] Move the Term type into its own module.

---
 semantic-analysis/src/Analysis/Syntax.hs      | 75 +--------------
 .../src/Analysis/Syntax/Python.hs             | 93 ++++++++++++++++++-
 2 files changed, 95 insertions(+), 73 deletions(-)

diff --git a/semantic-analysis/src/Analysis/Syntax.hs b/semantic-analysis/src/Analysis/Syntax.hs
index d3aa308b23..1de9750a61 100644
--- a/semantic-analysis/src/Analysis/Syntax.hs
+++ b/semantic-analysis/src/Analysis/Syntax.hs
@@ -25,8 +25,9 @@ module Analysis.Syntax
 import qualified Analysis.Carrier.Statement.State as S
 import           Analysis.Effect.Domain
 import           Analysis.File
-import           Analysis.Name (Name, name)
+import           Analysis.Name (name)
 import           Analysis.Reference as Ref
+import           Analysis.Syntax.Python
 import           Analysis.VM
 import           Control.Applicative (Alternative (..), liftA2, liftA3)
 import           Control.Carrier.Throw.Either (runThrow)
@@ -44,10 +45,9 @@ import           Data.Foldable (fold, foldl')
 import           Data.Function (fix)
 import qualified Data.IntMap as IntMap
 import           Data.List (sortOn)
-import           Data.List.NonEmpty (NonEmpty, fromList)
+import           Data.List.NonEmpty (fromList)
 import           Data.Maybe (listToMaybe)
 import           Data.Monoid (First (..))
-import qualified Data.Set as Set
 import           Data.String (IsString (..))
 import           Data.Text (Text)
 import qualified Data.Vector as V
@@ -55,75 +55,6 @@ import qualified Source.Source as Source
 import           Source.Span
 import           System.FilePath
 
-data Term
-  = Var Name
-  | Noop
-  | Iff Term Term Term
-  | Bool Bool
-  | String Text
-  | Throw Term
-  | Let Name Term Term
-  | Term :>> Term
-  | Import (NonEmpty Text)
-  | Function Name [Name] Term
-  | Call Term [Term]
-  | Locate Span Term
-  deriving (Eq, Ord, Show)
-
-infixl 1 :>>
-
-subterms :: Term -> Set.Set Term
-subterms t = Set.singleton t <> case t of
-  Var _          -> mempty
-  Noop           -> mempty
-  Iff c t e      -> subterms c <> subterms t <> subterms e
-  Bool _         -> mempty
-  String _       -> mempty
-  Throw t        -> subterms t
-  Let _ v b      -> subterms v <> subterms b
-  a :>> b        -> subterms a <> subterms b
-  Import _       -> mempty
-  Function _ _ b -> subterms b
-  Call f as      -> subterms f <> foldMap subterms as
-  Locate _ b     -> subterms b
-
-
--- Abstract interpretation
-
-eval0 :: (Has (Env addr) sig m, HasLabelled Store (Store addr val) sig m, Has (Dom val) sig m, Has (Reader Reference) sig m, Has S.Statement sig m) => Term -> m val
-eval0 = fix eval
-
-eval
-  :: (Has (Env addr) sig m, HasLabelled Store (Store addr val) sig m, Has (Dom val) sig m, Has (Reader Reference) sig m, Has S.Statement sig m)
-  => (Term -> m val)
-  -> (Term -> m val)
-eval eval = \case
-  Var n     -> lookupEnv n >>= maybe (dvar n) fetch
-  Noop      -> dunit
-  Iff c t e -> do
-    c' <- eval c
-    dif c' (eval t) (eval e)
-  Bool b    -> dbool b
-  String s  -> dstring s
-  Throw e   -> eval e >>= ddie
-  Let n v b -> do
-    v' <- eval v
-    let' n v' (eval b)
-  t :>> u   -> do
-    t' <- eval t
-    u' <- eval u
-    t' >>> u'
-  Import ns -> S.simport ns >> dunit
-  Function n ps b -> letrec n (dabs ps (foldr (\ (p, a) m -> let' p a m) (eval b) . zip ps))
-  Call f as -> do
-    f' <- eval f
-    as' <- traverse eval as
-    dapp f' as'
-  Locate s t -> local (setSpan s) (eval t)
-  where
-  setSpan s r = r{ refSpan = s }
-
-
 -- Parsing
 
 parseFile :: (Has (Throw String) sig m, MonadIO m) => FilePath -> FilePath -> m (Source.Source, File Term)
diff --git a/semantic-analysis/src/Analysis/Syntax/Python.hs b/semantic-analysis/src/Analysis/Syntax/Python.hs
index cf73f4a12f..6d3005512c 100644
--- a/semantic-analysis/src/Analysis/Syntax/Python.hs
+++ b/semantic-analysis/src/Analysis/Syntax/Python.hs
@@ -1,3 +1,94 @@
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE LambdaCase #-}
 -- | This belongs in @semantic-python@ instead of @semantic-analysis@, but for the sake of expedience…
 module Analysis.Syntax.Python
-() where
+( -- * Syntax
+  Term(..)
+, subterms
+  -- * Abstract interpretation
+, eval0
+, eval
+) where
+
+import           Analysis.Effect.Domain
+import qualified Analysis.Effect.Statement as S
+import           Analysis.Name
+import           Analysis.Reference
+import           Analysis.VM
+import           Control.Effect.Labelled
+import           Control.Effect.Reader
+import           Data.Function (fix)
+import           Data.List.NonEmpty (NonEmpty)
+import qualified Data.Set as Set
+import           Data.Text (Text)
+import           Source.Span (Span)
+
+-- Syntax
+
+data Term
+  = Var Name
+  | Noop
+  | Iff Term Term Term
+  | Bool Bool
+  | String Text
+  | Throw Term
+  | Let Name Term Term
+  | Term :>> Term
+  | Import (NonEmpty Text)
+  | Function Name [Name] Term
+  | Call Term [Term]
+  | Locate Span Term
+  deriving (Eq, Ord, Show)
+
+infixl 1 :>>
+
+subterms :: Term -> Set.Set Term
+subterms t = Set.singleton t <> case t of
+  Var _          -> mempty
+  Noop           -> mempty
+  Iff c t e      -> subterms c <> subterms t <> subterms e
+  Bool _         -> mempty
+  String _       -> mempty
+  Throw t        -> subterms t
+  Let _ v b      -> subterms v <> subterms b
+  a :>> b        -> subterms a <> subterms b
+  Import _       -> mempty
+  Function _ _ b -> subterms b
+  Call f as      -> subterms f <> foldMap subterms as
+  Locate _ b     -> subterms b
+
+
+-- Abstract interpretation
+
+eval0 :: (Has (Env addr) sig m, HasLabelled Store (Store addr val) sig m, Has (Dom val) sig m, Has (Reader Reference) sig m, Has S.Statement sig m) => Term -> m val
+eval0 = fix eval
+
+eval
+  :: (Has (Env addr) sig m, HasLabelled Store (Store addr val) sig m, Has (Dom val) sig m, Has (Reader Reference) sig m, Has S.Statement sig m)
+  => (Term -> m val)
+  -> (Term -> m val)
+eval eval = \case
+  Var n     -> lookupEnv n >>= maybe (dvar n) fetch
+  Noop      -> dunit
+  Iff c t e -> do
+    c' <- eval c
+    dif c' (eval t) (eval e)
+  Bool b    -> dbool b
+  String s  -> dstring s
+  Throw e   -> eval e >>= ddie
+  Let n v b -> do
+    v' <- eval v
+    let' n v' (eval b)
+  t :>> u   -> do
+    t' <- eval t
+    u' <- eval u
+    t' >>> u'
+  Import ns -> S.simport ns >> dunit
+  Function n ps b -> letrec n (dabs ps (foldr (\ (p, a) m -> let' p a m) (eval b) . zip ps))
+  Call f as -> do
+    f' <- eval f
+    as' <- traverse eval as
+    dapp f' as'
+  Locate s t -> local (setSpan s) (eval t)
+  where
+  setSpan s r = r{ refSpan = s }

From 25485ff897599cc55b2609e14e7b6b1ec08beab4 Mon Sep 17 00:00:00 2001
From: Rob Rix <robrix@github.com>
Date: Fri, 15 Mar 2024 11:07:33 -0400
Subject: [PATCH 06/59] :fire: re-exports.

---
 semantic-analysis/src/Analysis/Syntax.hs | 10 ++--------
 1 file changed, 2 insertions(+), 8 deletions(-)

diff --git a/semantic-analysis/src/Analysis/Syntax.hs b/semantic-analysis/src/Analysis/Syntax.hs
index 1de9750a61..0193a239f8 100644
--- a/semantic-analysis/src/Analysis/Syntax.hs
+++ b/semantic-analysis/src/Analysis/Syntax.hs
@@ -7,14 +7,8 @@
 {-# LANGUAGE TypeApplications #-}
 {-# LANGUAGE UndecidableInstances #-}
 module Analysis.Syntax
-( -- * Terms
-  Term(..)
-, subterms
-  -- * Abstract interpretation
-, eval0
-, eval
-  -- * Parsing
-, parseFile
+( -- * Parsing
+  parseFile
 , parseGraph
 , parseNode
   -- * Debugging

From fba6ecf1a79ba86ee923124cff46d6880614fb40 Mon Sep 17 00:00:00 2001
From: Rob Rix <robrix@github.com>
Date: Fri, 15 Mar 2024 11:08:20 -0400
Subject: [PATCH 07/59] :fire: all the JSON parsing stuff.

---
 semantic-analysis/semantic-analysis.cabal |   2 -
 semantic-analysis/src/Analysis/Syntax.hs  | 175 +---------------------
 2 files changed, 1 insertion(+), 176 deletions(-)

diff --git a/semantic-analysis/semantic-analysis.cabal b/semantic-analysis/semantic-analysis.cabal
index 82545b3cb0..9dfe388d9b 100644
--- a/semantic-analysis/semantic-analysis.cabal
+++ b/semantic-analysis/semantic-analysis.cabal
@@ -74,7 +74,6 @@ library
   build-depends:
     , aeson                        >= 1.4 && < 3
     , base                         >= 4.13 && < 5
-    , bytestring                   >= 0.10.8.2 && < 0.13
     , containers                  ^>= 0.6
     , filepath
     , fused-effects               ^>= 1.1
@@ -82,4 +81,3 @@ library
     , semantic-source             ^>= 0.2
     , text                        ^>= 1.2.3.1
     , transformers                ^>= 0.5
-    , vector                      ^>= 0.12.3
diff --git a/semantic-analysis/src/Analysis/Syntax.hs b/semantic-analysis/src/Analysis/Syntax.hs
index 0193a239f8..b9e91d818d 100644
--- a/semantic-analysis/src/Analysis/Syntax.hs
+++ b/semantic-analysis/src/Analysis/Syntax.hs
@@ -1,175 +1,2 @@
-{-# LANGUAGE ExistentialQuantification #-}
-{-# LANGUAGE FlexibleContexts #-}
-{-# LANGUAGE FlexibleInstances #-}
-{-# LANGUAGE LambdaCase #-}
-{-# LANGUAGE MultiParamTypeClasses #-}
-{-# LANGUAGE RankNTypes #-}
-{-# LANGUAGE TypeApplications #-}
-{-# LANGUAGE UndecidableInstances #-}
 module Analysis.Syntax
-( -- * Parsing
-  parseFile
-, parseGraph
-, parseNode
-  -- * Debugging
-, analyzeFile
-, parseToTerm
-) where
-
-import qualified Analysis.Carrier.Statement.State as S
-import           Analysis.Effect.Domain
-import           Analysis.File
-import           Analysis.Name (name)
-import           Analysis.Reference as Ref
-import           Analysis.Syntax.Python
-import           Analysis.VM
-import           Control.Applicative (Alternative (..), liftA2, liftA3)
-import           Control.Carrier.Throw.Either (runThrow)
-import           Control.Effect.Labelled
-import           Control.Effect.Reader
-import           Control.Effect.Throw (Throw, throwError)
-import           Control.Exception
-import           Control.Monad (guard)
-import           Control.Monad.IO.Class
-import qualified Data.Aeson as A
-import qualified Data.Aeson.Parser as A
-import qualified Data.Aeson.Types as A
-import qualified Data.ByteString.Lazy as B
-import           Data.Foldable (fold, foldl')
-import           Data.Function (fix)
-import qualified Data.IntMap as IntMap
-import           Data.List (sortOn)
-import           Data.List.NonEmpty (fromList)
-import           Data.Maybe (listToMaybe)
-import           Data.Monoid (First (..))
-import           Data.String (IsString (..))
-import           Data.Text (Text)
-import qualified Data.Vector as V
-import qualified Source.Source as Source
-import           Source.Span
-import           System.FilePath
-
--- Parsing
-
-parseFile :: (Has (Throw String) sig m, MonadIO m) => FilePath -> FilePath -> m (Source.Source, File Term)
-parseFile srcPath jsonPath = do
-  contents <- liftIO (B.readFile jsonPath)
-  -- FIXME: get this from the JSON itself (cf https://github.com/tree-sitter/tree-sitter-graph/issues/69)
-  let sourcePath = replaceExtensions jsonPath "py"
-  sourceContents <- Source.fromUTF8 . B.toStrict <$> liftIO (B.readFile srcPath)
-  let span = decrSpan (Source.totalSpan sourceContents)
-  case A.eitherDecodeWith A.json' (A.iparse parseGraph) contents of
-    Left  (_, err)       -> throwError err
-    Right (_, Nothing)   -> throwError "no root node found"
-    Right (_, Just root) -> pure (sourceContents, File (Reference sourcePath span) root)
-  where
-  decrSpan (Span (Pos sl sc) (Pos el ec)) = Span (Pos (sl - 1) (sc - 1)) (Pos (el - 1) (ec - 1))
-
-newtype Graph = Graph { terms :: IntMap.IntMap Term }
-
--- | Parse a @Value@ into an entire graph of terms, as well as a root node, if any exists.
-parseGraph :: A.Value -> A.Parser (Graph, Maybe Term)
-parseGraph = A.withArray "nodes" $ \ nodes -> do
-  (untied, First root) <- fold <$> traverse parseNode (V.toList nodes)
-  -- @untied@ is an intmap, where the keys are graph node IDs and the values are functions from the final graph to the representations of said graph nodes. Likewise, @root@ is a function of the same variety, wrapped in a @Maybe@.
-  --
-  -- We define @tied@ as the fixpoint of the former to yield the former as a graph of type @Graph@, and apply the latter to said graph to yield the entry point, if any, from which to evaluate.
-  let tied = fix (\ tied -> ($ Graph tied) <$> untied)
-  pure (Graph tied, ($ Graph tied) <$> root)
-
--- | Parse a node from a JSON @Value@ into a pair of a partial graph of unfixed terms and optionally an unfixed term representing the root node.
---
--- The partial graph is represented as an adjacency map relating node IDs to unfixed terms—terms which may make reference to a completed graph to find edges, and which therefore can't be inspected until the full graph is known.
-parseNode :: A.Value -> A.Parser (IntMap.IntMap (Graph -> Term), First (Graph -> Term))
-parseNode = A.withObject "node" $ \ o -> do
-  edges <- o A..: fromString "edges"
-  index <- o A..: fromString "id"
-  o A..: fromString "attrs" >>= A.withObject "attrs" (\ attrs -> do
-    ty <- attrs A..: fromString "type"
-    node <- parseTerm attrs edges ty
-    pure (IntMap.singleton index node, node <$ First (guard (ty == "module"))))
-
-parseTerm :: A.Object -> [A.Value] -> String -> A.Parser (Graph -> Term)
-parseTerm attrs edges = locate attrs . \case
-  "string"     -> const . String <$> attrs A..: fromString "text"
-  "true"       -> pure (const (Bool True))
-  "false"      -> pure (const (Bool False))
-  "throw"      -> fmap Throw <$> maybe empty resolve (listToMaybe edges)
-  "if"         -> liftA3 Iff <$> findEdgeNamed edges "condition" <*> findEdgeNamed edges "consequence" <*> findEdgeNamed edges "alternative" <|> pure (const Noop)
-  "block"      -> children edges
-  "module"     -> children edges
-  "identifier" -> const . Var . name <$> attrs A..: fromString "text"
-  "import"     -> const . Import . fromList . map snd . sortOn fst <$> traverse (resolveWith (const moduleNameComponent)) edges
-  "function"   -> liftA3 Function . pure . name <$> attrs A..: fromString "name" <*> pure (pure []) <*> findEdgeNamed edges "body"
-  "call"       -> liftA2 Call . const . Var . name <$> attrs A..: fromString "function" <*> (sequenceA <$> traverse resolve edges)
-  "noop"       -> pure (pure Noop)
-  t            -> A.parseFail ("unrecognized type: " <> t <> " attrs: " <> show attrs <> " edges: " <> show edges)
-
-findEdgeNamed :: (Foldable t, A.FromJSON a, Eq a) => t A.Value -> a -> A.Parser (Graph -> Term)
-findEdgeNamed edges name = foldMap (resolveWith (\ rep attrs -> attrs A..: fromString "type" >>= (rep <$) . guard . (== name))) edges
-
--- | Map a list of edges to a list of child nodes.
-children :: [A.Value] -> A.Parser (Graph -> Term)
-children edges = fmap chain . traverse snd . sortOn fst <$> traverse (resolveWith child) edges
-  where
-  child :: (Graph -> Term) -> A.Object -> A.Parser (Int, Graph -> Term)
-  child term attrs = (,) <$> attrs A..: fromString "index" <*> pure term
-
-  chain :: [Term] -> Term
-  chain []     = Noop
-  chain (t:ts) = foldl' (:>>) t ts
-
-moduleNameComponent :: A.Object -> A.Parser (Int, Text)
-moduleNameComponent attrs = (,) <$> attrs A..: fromString "index" <*> attrs A..: fromString "text"
-
-resolve :: A.Value -> A.Parser (Graph -> Term)
-resolve = resolveWith (const . pure)
-
-resolveWith :: ((Graph -> Term) -> A.Object -> A.Parser a) -> A.Value -> A.Parser a
-resolveWith f = resolveWith' (f . flip ((IntMap.!) . terms))
-
-resolveWith' :: (IntMap.Key -> A.Object -> A.Parser a) -> A.Value -> A.Parser a
-resolveWith' f = A.withObject "edge" (\ edge -> do
-  sink <- edge A..: fromString "sink"
-  attrs <- edge A..: fromString "attrs"
-  f sink attrs)
-
-locate :: A.Object -> A.Parser (Graph -> Term) -> A.Parser (Graph -> Term)
-locate attrs p = do
-  span <- span
-    <$> attrs A..:? fromString "start-line"
-    <*> attrs A..:? fromString "start-col"
-    <*> attrs A..:? fromString "end-line"
-    <*> attrs A..:? fromString "end-col"
-  t <- p
-  case span of
-    Nothing -> pure t
-    Just s  -> pure (Locate s <$> t)
-  where
-  span sl sc el ec = Span <$> (Pos <$> sl <*> sc) <*> (Pos <$> el <*> ec)
-
-
--- Debugging
-
-analyzeFile
-  :: (Algebra sig m, MonadIO m)
-  => FilePath
-  -> FilePath
-  -> (  forall term
-     .  Ord term
-     => (  forall sig m
-        .  (Has (Env addr) sig m, HasLabelled Store (Store addr val) sig m, Has (Dom val) sig m, Has (Reader Reference) sig m, Has S.Statement sig m)
-        => (term -> m val)
-        -> (term -> m val) )
-     -> Source.Source
-     -> File term
-     -> m b )
-  -> m b
-analyzeFile srcPath jsonPath analyze = do
-  (src, file) <- parseToTerm srcPath jsonPath
-  analyze eval src file
-
-parseToTerm :: (Algebra sig m, MonadIO m) => FilePath -> FilePath -> m (Source.Source, File Term)
-parseToTerm srcPath jsonPath = do
-  parsed <- runThrow @String (parseFile srcPath jsonPath)
-  either (liftIO . throwIO . ErrorCall) pure parsed
+() where

From f8a8f06f604c67b8b8335f8696cf40d6f67f8959 Mon Sep 17 00:00:00 2001
From: Rob Rix <robrix@github.com>
Date: Fri, 15 Mar 2024 11:17:39 -0400
Subject: [PATCH 08/59] Initial stab at ABT-style term representations.

---
 semantic-analysis/src/Analysis/Syntax.hs | 27 +++++++++++++++++++++++-
 1 file changed, 26 insertions(+), 1 deletion(-)

diff --git a/semantic-analysis/src/Analysis/Syntax.hs b/semantic-analysis/src/Analysis/Syntax.hs
index b9e91d818d..982430cafb 100644
--- a/semantic-analysis/src/Analysis/Syntax.hs
+++ b/semantic-analysis/src/Analysis/Syntax.hs
@@ -1,2 +1,27 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE KindSignatures #-}
+{-# LANGUAGE TypeOperators #-}
 module Analysis.Syntax
-() where
+( -- * Syntax
+  Term(..)
+  -- * Vectors
+, Vec(..)
+) where
+
+import Data.Kind (Type)
+import GHC.TypeLits (Natural, type (+))
+
+-- Syntax
+
+-- | (Currently) untyped term representations.
+data Term (sig :: Natural -> Type) where
+  (:$:) :: sig n -> Vec n (Term sig) -> Term sig
+
+
+-- Vectors
+
+-- FIXME: move this into its own module, or use a dependency, or something.
+data Vec (n :: Natural) a where
+  Nil :: Vec 0 a
+  Cons :: a -> Vec n a -> Vec (1 + n) a

From ef985dc71dd1e68c1636ceac48f4b83141d2fcc7 Mon Sep 17 00:00:00 2001
From: Rob Rix <robrix@github.com>
Date: Fri, 15 Mar 2024 11:20:06 -0400
Subject: [PATCH 09/59] Convert Vec to [].

---
 semantic-analysis/src/Analysis/Syntax.hs | 7 +++++++
 1 file changed, 7 insertions(+)

diff --git a/semantic-analysis/src/Analysis/Syntax.hs b/semantic-analysis/src/Analysis/Syntax.hs
index 982430cafb..00cf371ad4 100644
--- a/semantic-analysis/src/Analysis/Syntax.hs
+++ b/semantic-analysis/src/Analysis/Syntax.hs
@@ -1,12 +1,14 @@
 {-# LANGUAGE DataKinds #-}
 {-# LANGUAGE GADTs #-}
 {-# LANGUAGE KindSignatures #-}
+{-# LANGUAGE LambdaCase #-}
 {-# LANGUAGE TypeOperators #-}
 module Analysis.Syntax
 ( -- * Syntax
   Term(..)
   -- * Vectors
 , Vec(..)
+, toList
 ) where
 
 import Data.Kind (Type)
@@ -25,3 +27,8 @@ data Term (sig :: Natural -> Type) where
 data Vec (n :: Natural) a where
   Nil :: Vec 0 a
   Cons :: a -> Vec n a -> Vec (1 + n) a
+
+toList :: Vec n a -> [a]
+toList = \case
+  Nil -> []
+  Cons a as -> a : toList as

From 67c777964bed5f156ec0b0d3377fb9c1ae0a1d52 Mon Sep 17 00:00:00 2001
From: Rob Rix <robrix@github.com>
Date: Fri, 15 Mar 2024 11:42:04 -0400
Subject: [PATCH 10/59] Define a factored Python type.

---
 .../src/Analysis/Syntax/Python.hs             | 23 +++++++++++++++++++
 1 file changed, 23 insertions(+)

diff --git a/semantic-analysis/src/Analysis/Syntax/Python.hs b/semantic-analysis/src/Analysis/Syntax/Python.hs
index 6d3005512c..44b1c6614b 100644
--- a/semantic-analysis/src/Analysis/Syntax/Python.hs
+++ b/semantic-analysis/src/Analysis/Syntax/Python.hs
@@ -1,10 +1,14 @@
+{-# LANGUAGE DataKinds #-}
 {-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE KindSignatures #-}
 {-# LANGUAGE LambdaCase #-}
 -- | This belongs in @semantic-python@ instead of @semantic-analysis@, but for the sake of expedience…
 module Analysis.Syntax.Python
 ( -- * Syntax
   Term(..)
 , subterms
+, Python(..)
   -- * Abstract interpretation
 , eval0
 , eval
@@ -21,6 +25,7 @@ import           Data.Function (fix)
 import           Data.List.NonEmpty (NonEmpty)
 import qualified Data.Set as Set
 import           Data.Text (Text)
+import           GHC.TypeLits (Natural)
 import           Source.Span (Span)
 
 -- Syntax
@@ -58,6 +63,24 @@ subterms t = Set.singleton t <> case t of
   Locate _ b     -> subterms b
 
 
+data Python (arity :: Natural) where
+  Var' :: Name -> Python 0 -- FIXME: move this into @T.Term@.
+  Noop' :: Python 0
+  Iff' :: Python 3
+  Bool' :: Bool -> Python 0
+  String' :: Text -> Python 0
+  Throw' :: Python 1
+  (:>>>) :: Python 2
+  Import' :: NonEmpty Text -> Python 0
+  Function' :: Name -> [Name] -> Python 1
+  Call' :: Python 2 -- ^ Second should be an @ANil'@ or @ACons'@.
+  ANil' :: Python 0
+  ACons' :: Python 2 -- ^ Second should be an @ANil'@ or @ACons'@.
+  Locate' :: Span -> Python 1
+
+infixl 1 :>>>
+
+
 -- Abstract interpretation
 
 eval0 :: (Has (Env addr) sig m, HasLabelled Store (Store addr val) sig m, Has (Dom val) sig m, Has (Reader Reference) sig m, Has S.Statement sig m) => Term -> m val

From 54f32e95ed6040df29cede3daed4d1244c99e5d2 Mon Sep 17 00:00:00 2001
From: Rob Rix <robrix@github.com>
Date: Fri, 15 Mar 2024 11:42:18 -0400
Subject: [PATCH 11/59] Define a smart constructor for no-ops.

---
 semantic-analysis/src/Analysis/Syntax/Python.hs | 5 +++++
 1 file changed, 5 insertions(+)

diff --git a/semantic-analysis/src/Analysis/Syntax/Python.hs b/semantic-analysis/src/Analysis/Syntax/Python.hs
index 44b1c6614b..d29725aaf5 100644
--- a/semantic-analysis/src/Analysis/Syntax/Python.hs
+++ b/semantic-analysis/src/Analysis/Syntax/Python.hs
@@ -9,6 +9,7 @@ module Analysis.Syntax.Python
   Term(..)
 , subterms
 , Python(..)
+, noop
   -- * Abstract interpretation
 , eval0
 , eval
@@ -18,6 +19,7 @@ import           Analysis.Effect.Domain
 import qualified Analysis.Effect.Statement as S
 import           Analysis.Name
 import           Analysis.Reference
+import qualified Analysis.Syntax as T
 import           Analysis.VM
 import           Control.Effect.Labelled
 import           Control.Effect.Reader
@@ -80,6 +82,9 @@ data Python (arity :: Natural) where
 
 infixl 1 :>>>
 
+noop :: T.Term Python
+noop = Noop' T.:$: T.Nil
+
 
 -- Abstract interpretation
 

From 71073d78b06b66f4a77eeb80cd28891a843759c0 Mon Sep 17 00:00:00 2001
From: Rob Rix <robrix@github.com>
Date: Fri, 15 Mar 2024 11:48:20 -0400
Subject: [PATCH 12/59] Use inductive naturals.

---
 semantic-analysis/src/Analysis/Syntax.hs      | 25 ++++++++++++----
 .../src/Analysis/Syntax/Python.hs             | 29 +++++++++----------
 2 files changed, 33 insertions(+), 21 deletions(-)

diff --git a/semantic-analysis/src/Analysis/Syntax.hs b/semantic-analysis/src/Analysis/Syntax.hs
index 00cf371ad4..45f106a765 100644
--- a/semantic-analysis/src/Analysis/Syntax.hs
+++ b/semantic-analysis/src/Analysis/Syntax.hs
@@ -2,31 +2,44 @@
 {-# LANGUAGE GADTs #-}
 {-# LANGUAGE KindSignatures #-}
 {-# LANGUAGE LambdaCase #-}
-{-# LANGUAGE TypeOperators #-}
 module Analysis.Syntax
 ( -- * Syntax
   Term(..)
   -- * Vectors
+, Nat(..)
+, N0
+, N1
+, N2
+, N3
 , Vec(..)
 , toList
 ) where
 
 import Data.Kind (Type)
-import GHC.TypeLits (Natural, type (+))
 
 -- Syntax
 
 -- | (Currently) untyped term representations.
-data Term (sig :: Natural -> Type) where
+data Term (sig :: Nat -> Type) where
   (:$:) :: sig n -> Vec n (Term sig) -> Term sig
 
 
 -- Vectors
 
+data Nat
+  = Z
+  | S Nat
+  deriving (Eq, Ord, Show)
+
+type N0 = 'Z
+type N1 = 'S N0
+type N2 = 'S N1
+type N3 = 'S N2
+
 -- FIXME: move this into its own module, or use a dependency, or something.
-data Vec (n :: Natural) a where
-  Nil :: Vec 0 a
-  Cons :: a -> Vec n a -> Vec (1 + n) a
+data Vec (n :: Nat) a where
+  Nil :: Vec 'Z a
+  Cons :: a -> Vec n a -> Vec ('S n) a
 
 toList :: Vec n a -> [a]
 toList = \case
diff --git a/semantic-analysis/src/Analysis/Syntax/Python.hs b/semantic-analysis/src/Analysis/Syntax/Python.hs
index d29725aaf5..1017c94faa 100644
--- a/semantic-analysis/src/Analysis/Syntax/Python.hs
+++ b/semantic-analysis/src/Analysis/Syntax/Python.hs
@@ -27,7 +27,6 @@ import           Data.Function (fix)
 import           Data.List.NonEmpty (NonEmpty)
 import qualified Data.Set as Set
 import           Data.Text (Text)
-import           GHC.TypeLits (Natural)
 import           Source.Span (Span)
 
 -- Syntax
@@ -65,20 +64,20 @@ subterms t = Set.singleton t <> case t of
   Locate _ b     -> subterms b
 
 
-data Python (arity :: Natural) where
-  Var' :: Name -> Python 0 -- FIXME: move this into @T.Term@.
-  Noop' :: Python 0
-  Iff' :: Python 3
-  Bool' :: Bool -> Python 0
-  String' :: Text -> Python 0
-  Throw' :: Python 1
-  (:>>>) :: Python 2
-  Import' :: NonEmpty Text -> Python 0
-  Function' :: Name -> [Name] -> Python 1
-  Call' :: Python 2 -- ^ Second should be an @ANil'@ or @ACons'@.
-  ANil' :: Python 0
-  ACons' :: Python 2 -- ^ Second should be an @ANil'@ or @ACons'@.
-  Locate' :: Span -> Python 1
+data Python (arity :: T.Nat) where
+  Var' :: Name -> Python T.N0 -- FIXME: move this into @T.Term@.
+  Noop' :: Python T.N0
+  Iff' :: Python T.N3
+  Bool' :: Bool -> Python T.N0
+  String' :: Text -> Python T.N0
+  Throw' :: Python T.N1
+  (:>>>) :: Python T.N2
+  Import' :: NonEmpty Text -> Python T.N0
+  Function' :: Name -> [Name] -> Python T.N1
+  Call' :: Python T.N2 -- ^ Second should be an @ANil'@ or @ACons'@.
+  ANil' :: Python T.N0
+  ACons' :: Python T.N2 -- ^ Second should be an @ANil'@ or @ACons'@.
+  Locate' :: Span -> Python T.N1
 
 infixl 1 :>>>
 

From 138bea9c1431796b8f617398986e8636df44fac1 Mon Sep 17 00:00:00 2001
From: Rob Rix <robrix@github.com>
Date: Fri, 15 Mar 2024 11:49:23 -0400
Subject: [PATCH 13/59] Equate Vec.

---
 semantic-analysis/src/Analysis/Syntax.hs | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/semantic-analysis/src/Analysis/Syntax.hs b/semantic-analysis/src/Analysis/Syntax.hs
index 45f106a765..b625d00e82 100644
--- a/semantic-analysis/src/Analysis/Syntax.hs
+++ b/semantic-analysis/src/Analysis/Syntax.hs
@@ -41,6 +41,10 @@ data Vec (n :: Nat) a where
   Nil :: Vec 'Z a
   Cons :: a -> Vec n a -> Vec ('S n) a
 
+instance Eq a => Eq (Vec n a) where
+  Nil       == Nil       = True
+  Cons a as == Cons b bs = a == b && as == bs
+
 toList :: Vec n a -> [a]
 toList = \case
   Nil -> []

From b798092d5eda6b6093af045a4fa8c765a5cb55d4 Mon Sep 17 00:00:00 2001
From: Rob Rix <robrix@github.com>
Date: Fri, 15 Mar 2024 14:35:11 -0400
Subject: [PATCH 14/59] Go quantify a kite.

---
 semantic-analysis/src/Analysis/Syntax.hs | 31 +++++++++++++++++++++++-
 1 file changed, 30 insertions(+), 1 deletion(-)

diff --git a/semantic-analysis/src/Analysis/Syntax.hs b/semantic-analysis/src/Analysis/Syntax.hs
index b625d00e82..6dc80fe4b7 100644
--- a/semantic-analysis/src/Analysis/Syntax.hs
+++ b/semantic-analysis/src/Analysis/Syntax.hs
@@ -2,6 +2,10 @@
 {-# LANGUAGE GADTs #-}
 {-# LANGUAGE KindSignatures #-}
 {-# LANGUAGE LambdaCase #-}
+{-# LANGUAGE QuantifiedConstraints #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE UndecidableInstances #-}
 module Analysis.Syntax
 ( -- * Syntax
   Term(..)
@@ -15,13 +19,21 @@ module Analysis.Syntax
 , toList
 ) where
 
+import Control.Monad (guard)
 import Data.Kind (Type)
+import Data.Typeable
+import Unsafe.Coerce (unsafeCoerce)
 
 -- Syntax
 
 -- | (Currently) untyped term representations.
 data Term (sig :: Nat -> Type) where
-  (:$:) :: sig n -> Vec n (Term sig) -> Term sig
+  (:$:) :: KnownNat n => sig n -> Vec n (Term sig) -> Term sig
+
+instance (forall n . Eq (sig n)) => Eq (Term sig) where
+  a :$: as == b :$: bs = case sameNat a b of
+    Just Refl -> a == b && as == bs
+    _         -> False
 
 
 -- Vectors
@@ -36,6 +48,23 @@ type N1 = 'S N0
 type N2 = 'S N1
 type N3 = 'S N2
 
+
+-- | Reify 'Nat's back from type-level singletons.
+class KnownNat (n :: Nat) where
+  reifyNat :: proxy n -> Nat
+
+instance KnownNat 'Z where
+  reifyNat _ = Z
+
+instance KnownNat n => KnownNat ('S n) where
+  reifyNat _ = S (reifyNat (undefined :: proxy n))
+
+
+-- | Test the equality of type-level 'Nat's at runtime, generating a type-level equality if equal.
+sameNat :: forall a b proxy1 proxy2 . (KnownNat a, KnownNat b) => proxy1 a -> proxy2 b -> Maybe (a :~: b)
+sameNat a b = unsafeCoerce Refl <$ guard (reifyNat a == reifyNat b)
+
+
 -- FIXME: move this into its own module, or use a dependency, or something.
 data Vec (n :: Nat) a where
   Nil :: Vec 'Z a

From fc4e7e475cb3d95b96b17ab476253c22837e1d6f Mon Sep 17 00:00:00 2001
From: Rob Rix <robrix@github.com>
Date: Fri, 15 Mar 2024 14:37:18 -0400
Subject: [PATCH 15/59] Represent variables in the abstract trees.

---
 semantic-analysis/src/Analysis/Syntax.hs        | 9 ++++++---
 semantic-analysis/src/Analysis/Syntax/Python.hs | 3 +--
 2 files changed, 7 insertions(+), 5 deletions(-)

diff --git a/semantic-analysis/src/Analysis/Syntax.hs b/semantic-analysis/src/Analysis/Syntax.hs
index 6dc80fe4b7..ceab6cd956 100644
--- a/semantic-analysis/src/Analysis/Syntax.hs
+++ b/semantic-analysis/src/Analysis/Syntax.hs
@@ -27,13 +27,16 @@ import Unsafe.Coerce (unsafeCoerce)
 -- Syntax
 
 -- | (Currently) untyped term representations.
-data Term (sig :: Nat -> Type) where
-  (:$:) :: KnownNat n => sig n -> Vec n (Term sig) -> Term sig
+data Term (sig :: Nat -> Type) v where
+  Var  :: v -> Term sig v
+  (:$:) :: KnownNat n => sig n -> Vec n (Term sig v) -> Term sig v
 
-instance (forall n . Eq (sig n)) => Eq (Term sig) where
+instance (forall n . Eq (sig n), Eq v) => Eq (Term sig v) where
+  Var v1   == Var v2   = v1 == v2
   a :$: as == b :$: bs = case sameNat a b of
     Just Refl -> a == b && as == bs
     _         -> False
+  _        == _        = False
 
 
 -- Vectors
diff --git a/semantic-analysis/src/Analysis/Syntax/Python.hs b/semantic-analysis/src/Analysis/Syntax/Python.hs
index 1017c94faa..bcbce01711 100644
--- a/semantic-analysis/src/Analysis/Syntax/Python.hs
+++ b/semantic-analysis/src/Analysis/Syntax/Python.hs
@@ -65,7 +65,6 @@ subterms t = Set.singleton t <> case t of
 
 
 data Python (arity :: T.Nat) where
-  Var' :: Name -> Python T.N0 -- FIXME: move this into @T.Term@.
   Noop' :: Python T.N0
   Iff' :: Python T.N3
   Bool' :: Bool -> Python T.N0
@@ -81,7 +80,7 @@ data Python (arity :: T.Nat) where
 
 infixl 1 :>>>
 
-noop :: T.Term Python
+noop :: T.Term Python v
 noop = Noop' T.:$: T.Nil
 
 

From 076e967b98f59de36daa78771d80c5f90dd29f1f Mon Sep 17 00:00:00 2001
From: Rob Rix <robrix@github.com>
Date: Fri, 15 Mar 2024 14:43:54 -0400
Subject: [PATCH 16/59] Define an Ord instance for Vec.

---
 semantic-analysis/src/Analysis/Syntax.hs | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/semantic-analysis/src/Analysis/Syntax.hs b/semantic-analysis/src/Analysis/Syntax.hs
index ceab6cd956..5802d4cc19 100644
--- a/semantic-analysis/src/Analysis/Syntax.hs
+++ b/semantic-analysis/src/Analysis/Syntax.hs
@@ -77,6 +77,10 @@ instance Eq a => Eq (Vec n a) where
   Nil       == Nil       = True
   Cons a as == Cons b bs = a == b && as == bs
 
+instance Ord a => Ord (Vec n a) where
+  compare Nil         Nil         = EQ
+  compare (Cons a as) (Cons b bs) = a `compare` b <> as `compare` bs
+
 toList :: Vec n a -> [a]
 toList = \case
   Nil -> []

From 09c57edd633f266724ae60567258bf414a9b6dff Mon Sep 17 00:00:00 2001
From: Rob Rix <robrix@github.com>
Date: Fri, 15 Mar 2024 14:46:09 -0400
Subject: [PATCH 17/59] Define an Ord instance for Vec.

---
 semantic-analysis/src/Analysis/Syntax.hs | 8 ++++++++
 1 file changed, 8 insertions(+)

diff --git a/semantic-analysis/src/Analysis/Syntax.hs b/semantic-analysis/src/Analysis/Syntax.hs
index 5802d4cc19..7756f9ca51 100644
--- a/semantic-analysis/src/Analysis/Syntax.hs
+++ b/semantic-analysis/src/Analysis/Syntax.hs
@@ -38,6 +38,14 @@ instance (forall n . Eq (sig n), Eq v) => Eq (Term sig v) where
     _         -> False
   _        == _        = False
 
+instance (forall n . Ord (sig n), Ord v) => Ord (Term sig v) where
+  compare (Var v1)   (Var v2)   = compare v1 v2
+  compare (Var _)    _          = LT
+  compare (a :$: as) (b :$: bs) = case sameNat a b of
+    Just Refl -> compare a b <> compare as bs
+    _         -> reifyNat a `compare` reifyNat b -- lol
+  compare _          _          = GT
+
 
 -- Vectors
 

From 3987aa9f8961d8f14fea414242009e8a4f1375d5 Mon Sep 17 00:00:00 2001
From: Rob Rix <robrix@github.com>
Date: Fri, 15 Mar 2024 14:50:22 -0400
Subject: [PATCH 18/59] Define Foldable instances for Vec.

---
 semantic-analysis/src/Analysis/Syntax.hs | 8 ++++++++
 1 file changed, 8 insertions(+)

diff --git a/semantic-analysis/src/Analysis/Syntax.hs b/semantic-analysis/src/Analysis/Syntax.hs
index 7756f9ca51..60dc16e30c 100644
--- a/semantic-analysis/src/Analysis/Syntax.hs
+++ b/semantic-analysis/src/Analysis/Syntax.hs
@@ -1,4 +1,6 @@
 {-# LANGUAGE DataKinds #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE FlexibleInstances #-}
 {-# LANGUAGE GADTs #-}
 {-# LANGUAGE KindSignatures #-}
 {-# LANGUAGE LambdaCase #-}
@@ -89,6 +91,12 @@ instance Ord a => Ord (Vec n a) where
   compare Nil         Nil         = EQ
   compare (Cons a as) (Cons b bs) = a `compare` b <> as `compare` bs
 
+instance Foldable (Vec 'Z) where
+  foldMap _ _ = mempty
+
+instance Foldable (Vec n) => Foldable (Vec ('S n)) where
+  foldMap f (Cons a as) = f a <> foldMap f as
+
 toList :: Vec n a -> [a]
 toList = \case
   Nil -> []

From 22d693c4c22dc42f7a044cba0f9fd4e6c35f1766 Mon Sep 17 00:00:00 2001
From: Rob Rix <robrix@github.com>
Date: Fri, 15 Mar 2024 14:51:34 -0400
Subject: [PATCH 19/59] Simplify the Foldable instances.

---
 semantic-analysis/src/Analysis/Syntax.hs | 8 ++------
 1 file changed, 2 insertions(+), 6 deletions(-)

diff --git a/semantic-analysis/src/Analysis/Syntax.hs b/semantic-analysis/src/Analysis/Syntax.hs
index 60dc16e30c..b81ebc3f12 100644
--- a/semantic-analysis/src/Analysis/Syntax.hs
+++ b/semantic-analysis/src/Analysis/Syntax.hs
@@ -1,6 +1,4 @@
 {-# LANGUAGE DataKinds #-}
-{-# LANGUAGE FlexibleContexts #-}
-{-# LANGUAGE FlexibleInstances #-}
 {-# LANGUAGE GADTs #-}
 {-# LANGUAGE KindSignatures #-}
 {-# LANGUAGE LambdaCase #-}
@@ -91,10 +89,8 @@ instance Ord a => Ord (Vec n a) where
   compare Nil         Nil         = EQ
   compare (Cons a as) (Cons b bs) = a `compare` b <> as `compare` bs
 
-instance Foldable (Vec 'Z) where
-  foldMap _ _ = mempty
-
-instance Foldable (Vec n) => Foldable (Vec ('S n)) where
+instance Foldable (Vec n) where
+  foldMap _ Nil         = mempty
   foldMap f (Cons a as) = f a <> foldMap f as
 
 toList :: Vec n a -> [a]

From 6b25a7585c375c1c8f3575b4a085ff3e10c25fe2 Mon Sep 17 00:00:00 2001
From: Rob Rix <robrix@github.com>
Date: Fri, 15 Mar 2024 14:51:43 -0400
Subject: [PATCH 20/59] Spacing.

---
 semantic-analysis/src/Analysis/Syntax.hs | 1 +
 1 file changed, 1 insertion(+)

diff --git a/semantic-analysis/src/Analysis/Syntax.hs b/semantic-analysis/src/Analysis/Syntax.hs
index b81ebc3f12..afb6b2c357 100644
--- a/semantic-analysis/src/Analysis/Syntax.hs
+++ b/semantic-analysis/src/Analysis/Syntax.hs
@@ -93,6 +93,7 @@ instance Foldable (Vec n) where
   foldMap _ Nil         = mempty
   foldMap f (Cons a as) = f a <> foldMap f as
 
+
 toList :: Vec n a -> [a]
 toList = \case
   Nil -> []

From 175e81903e423ef7175f465cae83e2edd101d3f1 Mon Sep 17 00:00:00 2001
From: Rob Rix <robrix@github.com>
Date: Fri, 15 Mar 2024 14:52:59 -0400
Subject: [PATCH 21/59] Generic subterms.

@BekaValentine was right, it needs to include the argument. I have no idea what I was thinking.

Co-Authored-By: Rebecca Valentine <171941+BekaValentine@users.noreply.github.com>
---
 semantic-analysis/src/Analysis/Syntax.hs | 16 ++++++++++++----
 1 file changed, 12 insertions(+), 4 deletions(-)

diff --git a/semantic-analysis/src/Analysis/Syntax.hs b/semantic-analysis/src/Analysis/Syntax.hs
index afb6b2c357..a165599f1d 100644
--- a/semantic-analysis/src/Analysis/Syntax.hs
+++ b/semantic-analysis/src/Analysis/Syntax.hs
@@ -9,6 +9,7 @@
 module Analysis.Syntax
 ( -- * Syntax
   Term(..)
+, subterms
   -- * Vectors
 , Nat(..)
 , N0
@@ -19,10 +20,11 @@ module Analysis.Syntax
 , toList
 ) where
 
-import Control.Monad (guard)
-import Data.Kind (Type)
-import Data.Typeable
-import Unsafe.Coerce (unsafeCoerce)
+import           Control.Monad (guard)
+import           Data.Kind (Type)
+import qualified Data.Set as Set
+import           Data.Typeable
+import           Unsafe.Coerce (unsafeCoerce)
 
 -- Syntax
 
@@ -47,6 +49,12 @@ instance (forall n . Ord (sig n), Ord v) => Ord (Term sig v) where
   compare _          _          = GT
 
 
+subterms :: (forall n . Ord (sig n), Ord v) => Term sig v -> Set.Set (Term sig v)
+subterms t = case t of
+  Var _    -> Set.singleton t
+  _ :$: ts -> Set.insert t (foldMap subterms ts)
+
+
 -- Vectors
 
 data Nat

From 11b8caa386b75e1b3973d20dcc4b44811a210fa4 Mon Sep 17 00:00:00 2001
From: Rob Rix <robrix@github.com>
Date: Fri, 15 Mar 2024 14:54:51 -0400
Subject: [PATCH 22/59] An additional smart constructor.

---
 semantic-analysis/src/Analysis/Syntax/Python.hs | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/semantic-analysis/src/Analysis/Syntax/Python.hs b/semantic-analysis/src/Analysis/Syntax/Python.hs
index bcbce01711..ede4742d99 100644
--- a/semantic-analysis/src/Analysis/Syntax/Python.hs
+++ b/semantic-analysis/src/Analysis/Syntax/Python.hs
@@ -10,6 +10,7 @@ module Analysis.Syntax.Python
 , subterms
 , Python(..)
 , noop
+, iff
   -- * Abstract interpretation
 , eval0
 , eval
@@ -83,6 +84,9 @@ infixl 1 :>>>
 noop :: T.Term Python v
 noop = Noop' T.:$: T.Nil
 
+iff :: T.Term Python v -> T.Term Python v -> T.Term Python v -> T.Term Python v
+iff c t e = Iff' T.:$: T.Cons c (T.Cons t (T.Cons e T.Nil))
+
 
 -- Abstract interpretation
 

From 0a33a89d891da18b3db2b2844c7047d1617d567e Mon Sep 17 00:00:00 2001
From: Rob Rix <robrix@github.com>
Date: Fri, 15 Mar 2024 14:57:31 -0400
Subject: [PATCH 23/59] Define a pattern synonym for no-ops.

---
 semantic-analysis/src/Analysis/Syntax/Python.hs | 5 +++++
 1 file changed, 5 insertions(+)

diff --git a/semantic-analysis/src/Analysis/Syntax/Python.hs b/semantic-analysis/src/Analysis/Syntax/Python.hs
index ede4742d99..a944cd83c3 100644
--- a/semantic-analysis/src/Analysis/Syntax/Python.hs
+++ b/semantic-analysis/src/Analysis/Syntax/Python.hs
@@ -3,12 +3,14 @@
 {-# LANGUAGE GADTs #-}
 {-# LANGUAGE KindSignatures #-}
 {-# LANGUAGE LambdaCase #-}
+{-# LANGUAGE PatternSynonyms #-}
 -- | This belongs in @semantic-python@ instead of @semantic-analysis@, but for the sake of expedience…
 module Analysis.Syntax.Python
 ( -- * Syntax
   Term(..)
 , subterms
 , Python(..)
+, pattern Noop''
 , noop
 , iff
   -- * Abstract interpretation
@@ -81,6 +83,9 @@ data Python (arity :: T.Nat) where
 
 infixl 1 :>>>
 
+pattern Noop'' :: T.Term Python v
+pattern Noop'' <- Noop' T.:$: T.Nil
+
 noop :: T.Term Python v
 noop = Noop' T.:$: T.Nil
 

From d6263ff0ad8cfeb594f688f7fb5db11ef14feae7 Mon Sep 17 00:00:00 2001
From: Rob Rix <robrix@github.com>
Date: Fri, 15 Mar 2024 14:58:54 -0400
Subject: [PATCH 24/59] Define a pattern synonym for conditionals.

---
 semantic-analysis/src/Analysis/Syntax/Python.hs | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/semantic-analysis/src/Analysis/Syntax/Python.hs b/semantic-analysis/src/Analysis/Syntax/Python.hs
index a944cd83c3..32e40e606f 100644
--- a/semantic-analysis/src/Analysis/Syntax/Python.hs
+++ b/semantic-analysis/src/Analysis/Syntax/Python.hs
@@ -12,6 +12,7 @@ module Analysis.Syntax.Python
 , Python(..)
 , pattern Noop''
 , noop
+, pattern Iff''
 , iff
   -- * Abstract interpretation
 , eval0
@@ -89,6 +90,9 @@ pattern Noop'' <- Noop' T.:$: T.Nil
 noop :: T.Term Python v
 noop = Noop' T.:$: T.Nil
 
+pattern Iff'' :: T.Term Python v -> T.Term Python v -> T.Term Python v -> T.Term Python v
+pattern Iff'' c t e <- Iff' T.:$: T.Cons c (T.Cons t (T.Cons e T.Nil))
+
 iff :: T.Term Python v -> T.Term Python v -> T.Term Python v -> T.Term Python v
 iff c t e = Iff' T.:$: T.Cons c (T.Cons t (T.Cons e T.Nil))
 

From 45fa9a248c0fda4c2139cd73c0a422f59ecc3852 Mon Sep 17 00:00:00 2001
From: Rob Rix <robrix@github.com>
Date: Fri, 15 Mar 2024 15:01:03 -0400
Subject: [PATCH 25/59] :fire: the function constructors.

---
 semantic-analysis/src/Analysis/Syntax/Python.hs | 8 --------
 1 file changed, 8 deletions(-)

diff --git a/semantic-analysis/src/Analysis/Syntax/Python.hs b/semantic-analysis/src/Analysis/Syntax/Python.hs
index 32e40e606f..42d1093218 100644
--- a/semantic-analysis/src/Analysis/Syntax/Python.hs
+++ b/semantic-analysis/src/Analysis/Syntax/Python.hs
@@ -11,9 +11,7 @@ module Analysis.Syntax.Python
 , subterms
 , Python(..)
 , pattern Noop''
-, noop
 , pattern Iff''
-, iff
   -- * Abstract interpretation
 , eval0
 , eval
@@ -87,15 +85,9 @@ infixl 1 :>>>
 pattern Noop'' :: T.Term Python v
 pattern Noop'' <- Noop' T.:$: T.Nil
 
-noop :: T.Term Python v
-noop = Noop' T.:$: T.Nil
-
 pattern Iff'' :: T.Term Python v -> T.Term Python v -> T.Term Python v -> T.Term Python v
 pattern Iff'' c t e <- Iff' T.:$: T.Cons c (T.Cons t (T.Cons e T.Nil))
 
-iff :: T.Term Python v -> T.Term Python v -> T.Term Python v -> T.Term Python v
-iff c t e = Iff' T.:$: T.Cons c (T.Cons t (T.Cons e T.Nil))
-
 
 -- Abstract interpretation
 

From 1bfe2bbd6ae922d8d781106312bd0ab0a475a65e Mon Sep 17 00:00:00 2001
From: Rob Rix <robrix@github.com>
Date: Fri, 15 Mar 2024 15:01:48 -0400
Subject: [PATCH 26/59] Bool.

---
 semantic-analysis/src/Analysis/Syntax/Python.hs | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/semantic-analysis/src/Analysis/Syntax/Python.hs b/semantic-analysis/src/Analysis/Syntax/Python.hs
index 42d1093218..509e079b86 100644
--- a/semantic-analysis/src/Analysis/Syntax/Python.hs
+++ b/semantic-analysis/src/Analysis/Syntax/Python.hs
@@ -12,6 +12,7 @@ module Analysis.Syntax.Python
 , Python(..)
 , pattern Noop''
 , pattern Iff''
+, pattern Bool''
   -- * Abstract interpretation
 , eval0
 , eval
@@ -88,6 +89,9 @@ pattern Noop'' <- Noop' T.:$: T.Nil
 pattern Iff'' :: T.Term Python v -> T.Term Python v -> T.Term Python v -> T.Term Python v
 pattern Iff'' c t e <- Iff' T.:$: T.Cons c (T.Cons t (T.Cons e T.Nil))
 
+pattern Bool'' :: Bool -> T.Term Python v
+pattern Bool'' b <- Bool' b T.:$: T.Nil
+
 
 -- Abstract interpretation
 

From fef8e66d3653ab91890d6c99b4c3d8333aa1b03e Mon Sep 17 00:00:00 2001
From: Rob Rix <robrix@github.com>
Date: Fri, 15 Mar 2024 15:02:29 -0400
Subject: [PATCH 27/59] String.

---
 semantic-analysis/src/Analysis/Syntax/Python.hs | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/semantic-analysis/src/Analysis/Syntax/Python.hs b/semantic-analysis/src/Analysis/Syntax/Python.hs
index 509e079b86..641e3aeda5 100644
--- a/semantic-analysis/src/Analysis/Syntax/Python.hs
+++ b/semantic-analysis/src/Analysis/Syntax/Python.hs
@@ -13,6 +13,7 @@ module Analysis.Syntax.Python
 , pattern Noop''
 , pattern Iff''
 , pattern Bool''
+, pattern String''
   -- * Abstract interpretation
 , eval0
 , eval
@@ -92,6 +93,9 @@ pattern Iff'' c t e <- Iff' T.:$: T.Cons c (T.Cons t (T.Cons e T.Nil))
 pattern Bool'' :: Bool -> T.Term Python v
 pattern Bool'' b <- Bool' b T.:$: T.Nil
 
+pattern String'' :: Text -> T.Term Python v
+pattern String'' t <- String' t T.:$: T.Nil
+
 
 -- Abstract interpretation
 

From 155ecddd0995dc9c1d4676d1627e2a25fbfdf715 Mon Sep 17 00:00:00 2001
From: Rob Rix <robrix@github.com>
Date: Mon, 18 Mar 2024 11:26:30 -0400
Subject: [PATCH 28/59] Throw.

---
 semantic-analysis/src/Analysis/Syntax/Python.hs | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/semantic-analysis/src/Analysis/Syntax/Python.hs b/semantic-analysis/src/Analysis/Syntax/Python.hs
index 641e3aeda5..78b9a44c89 100644
--- a/semantic-analysis/src/Analysis/Syntax/Python.hs
+++ b/semantic-analysis/src/Analysis/Syntax/Python.hs
@@ -14,6 +14,7 @@ module Analysis.Syntax.Python
 , pattern Iff''
 , pattern Bool''
 , pattern String''
+, pattern Throw''
   -- * Abstract interpretation
 , eval0
 , eval
@@ -96,6 +97,9 @@ pattern Bool'' b <- Bool' b T.:$: T.Nil
 pattern String'' :: Text -> T.Term Python v
 pattern String'' t <- String' t T.:$: T.Nil
 
+pattern Throw'' :: T.Term Python v -> T.Term Python v
+pattern Throw'' e <- Throw' T.:$: T.Cons e T.Nil
+
 
 -- Abstract interpretation
 

From a59ff6e30d5434d66a16c4b46a7754fd4a2e9592 Mon Sep 17 00:00:00 2001
From: Rob Rix <robrix@github.com>
Date: Mon, 18 Mar 2024 11:28:00 -0400
Subject: [PATCH 29/59] Import.

---
 semantic-analysis/src/Analysis/Syntax/Python.hs | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/semantic-analysis/src/Analysis/Syntax/Python.hs b/semantic-analysis/src/Analysis/Syntax/Python.hs
index 78b9a44c89..7464c7dd6c 100644
--- a/semantic-analysis/src/Analysis/Syntax/Python.hs
+++ b/semantic-analysis/src/Analysis/Syntax/Python.hs
@@ -15,6 +15,7 @@ module Analysis.Syntax.Python
 , pattern Bool''
 , pattern String''
 , pattern Throw''
+, pattern Import''
   -- * Abstract interpretation
 , eval0
 , eval
@@ -100,6 +101,9 @@ pattern String'' t <- String' t T.:$: T.Nil
 pattern Throw'' :: T.Term Python v -> T.Term Python v
 pattern Throw'' e <- Throw' T.:$: T.Cons e T.Nil
 
+pattern Import'' :: NonEmpty Text -> T.Term Python v
+pattern Import'' i <- Import' i T.:$: T.Nil
+
 
 -- Abstract interpretation
 

From 42ab0be0e965a277fd0ae51fceb527109c6c0412 Mon Sep 17 00:00:00 2001
From: Rob Rix <robrix@github.com>
Date: Mon, 18 Mar 2024 11:29:25 -0400
Subject: [PATCH 30/59] Function.

---
 semantic-analysis/src/Analysis/Syntax/Python.hs | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/semantic-analysis/src/Analysis/Syntax/Python.hs b/semantic-analysis/src/Analysis/Syntax/Python.hs
index 7464c7dd6c..d22388de58 100644
--- a/semantic-analysis/src/Analysis/Syntax/Python.hs
+++ b/semantic-analysis/src/Analysis/Syntax/Python.hs
@@ -16,6 +16,7 @@ module Analysis.Syntax.Python
 , pattern String''
 , pattern Throw''
 , pattern Import''
+, pattern Function''
   -- * Abstract interpretation
 , eval0
 , eval
@@ -104,6 +105,9 @@ pattern Throw'' e <- Throw' T.:$: T.Cons e T.Nil
 pattern Import'' :: NonEmpty Text -> T.Term Python v
 pattern Import'' i <- Import' i T.:$: T.Nil
 
+pattern Function'' :: Name -> [Name] -> T.Term Python v -> T.Term Python v
+pattern Function'' n as b <- Function' n as T.:$: T.Cons b T.Nil
+
 
 -- Abstract interpretation
 

From dcf7d40f70bea02b0a5b54bf8a27962c9b7ca89d Mon Sep 17 00:00:00 2001
From: Rob Rix <robrix@github.com>
Date: Mon, 18 Mar 2024 12:06:48 -0400
Subject: [PATCH 31/59] Bidirectional.

---
 semantic-analysis/src/Analysis/Syntax/Python.hs | 14 +++++++-------
 1 file changed, 7 insertions(+), 7 deletions(-)

diff --git a/semantic-analysis/src/Analysis/Syntax/Python.hs b/semantic-analysis/src/Analysis/Syntax/Python.hs
index d22388de58..8ed3aa9cf1 100644
--- a/semantic-analysis/src/Analysis/Syntax/Python.hs
+++ b/semantic-analysis/src/Analysis/Syntax/Python.hs
@@ -88,25 +88,25 @@ data Python (arity :: T.Nat) where
 infixl 1 :>>>
 
 pattern Noop'' :: T.Term Python v
-pattern Noop'' <- Noop' T.:$: T.Nil
+pattern Noop'' = Noop' T.:$: T.Nil
 
 pattern Iff'' :: T.Term Python v -> T.Term Python v -> T.Term Python v -> T.Term Python v
-pattern Iff'' c t e <- Iff' T.:$: T.Cons c (T.Cons t (T.Cons e T.Nil))
+pattern Iff'' c t e = Iff' T.:$: T.Cons c (T.Cons t (T.Cons e T.Nil))
 
 pattern Bool'' :: Bool -> T.Term Python v
-pattern Bool'' b <- Bool' b T.:$: T.Nil
+pattern Bool'' b = Bool' b T.:$: T.Nil
 
 pattern String'' :: Text -> T.Term Python v
-pattern String'' t <- String' t T.:$: T.Nil
+pattern String'' t = String' t T.:$: T.Nil
 
 pattern Throw'' :: T.Term Python v -> T.Term Python v
-pattern Throw'' e <- Throw' T.:$: T.Cons e T.Nil
+pattern Throw'' e = Throw' T.:$: T.Cons e T.Nil
 
 pattern Import'' :: NonEmpty Text -> T.Term Python v
-pattern Import'' i <- Import' i T.:$: T.Nil
+pattern Import'' i = Import' i T.:$: T.Nil
 
 pattern Function'' :: Name -> [Name] -> T.Term Python v -> T.Term Python v
-pattern Function'' n as b <- Function' n as T.:$: T.Cons b T.Nil
+pattern Function'' n as b = Function' n as T.:$: T.Cons b T.Nil
 
 
 -- Abstract interpretation

From b6a9faea5dc26b331f2db0a3536b1ed0abbdb00c Mon Sep 17 00:00:00 2001
From: Rob Rix <robrix@github.com>
Date: Mon, 18 Mar 2024 12:11:38 -0400
Subject: [PATCH 32/59] Call.

---
 .../src/Analysis/Syntax/Python.hs             | 21 +++++++++++++++++++
 1 file changed, 21 insertions(+)

diff --git a/semantic-analysis/src/Analysis/Syntax/Python.hs b/semantic-analysis/src/Analysis/Syntax/Python.hs
index 8ed3aa9cf1..0d10cf5572 100644
--- a/semantic-analysis/src/Analysis/Syntax/Python.hs
+++ b/semantic-analysis/src/Analysis/Syntax/Python.hs
@@ -4,6 +4,7 @@
 {-# LANGUAGE KindSignatures #-}
 {-# LANGUAGE LambdaCase #-}
 {-# LANGUAGE PatternSynonyms #-}
+{-# LANGUAGE ViewPatterns #-}
 -- | This belongs in @semantic-python@ instead of @semantic-analysis@, but for the sake of expedience…
 module Analysis.Syntax.Python
 ( -- * Syntax
@@ -17,6 +18,7 @@ module Analysis.Syntax.Python
 , pattern Throw''
 , pattern Import''
 , pattern Function''
+, pattern Call''
   -- * Abstract interpretation
 , eval0
 , eval
@@ -108,6 +110,25 @@ pattern Import'' i = Import' i T.:$: T.Nil
 pattern Function'' :: Name -> [Name] -> T.Term Python v -> T.Term Python v
 pattern Function'' n as b = Function' n as T.:$: T.Cons b T.Nil
 
+pattern Call''
+  :: T.Term Python v
+  -> [T.Term Python v]
+  -> T.Term Python v
+pattern Call'' f as <- Call' T.:$: T.Cons f (T.Cons (fromArgs -> as) T.Nil)
+  where Call'' f as = Call' T.:$: T.Cons f (T.Cons (foldr ACons'' ANil'' as) T.Nil)
+
+fromArgs :: T.Term Python v -> [T.Term Python v]
+fromArgs = \case
+  ANil'' -> []
+  ACons'' a as -> a:fromArgs as
+  _ -> fail "unexpected constructor in spine of argument list"
+
+pattern ANil'' :: T.Term Python v
+pattern ANil'' = ANil' T.:$: T.Nil
+
+pattern ACons'' :: T.Term Python v -> T.Term Python v -> T.Term Python v
+pattern ACons'' a as = ACons' T.:$: T.Cons a (T.Cons as T.Nil)
+
 
 -- Abstract interpretation
 

From b19baf019b4808137c6b35548da82e42bcd46fae Mon Sep 17 00:00:00 2001
From: Rob Rix <robrix@github.com>
Date: Mon, 18 Mar 2024 12:27:03 -0400
Subject: [PATCH 33/59]  Locate.

---
 semantic-analysis/src/Analysis/Syntax/Python.hs | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/semantic-analysis/src/Analysis/Syntax/Python.hs b/semantic-analysis/src/Analysis/Syntax/Python.hs
index 0d10cf5572..de7cd506af 100644
--- a/semantic-analysis/src/Analysis/Syntax/Python.hs
+++ b/semantic-analysis/src/Analysis/Syntax/Python.hs
@@ -19,6 +19,7 @@ module Analysis.Syntax.Python
 , pattern Import''
 , pattern Function''
 , pattern Call''
+, pattern Locate''
   -- * Abstract interpretation
 , eval0
 , eval
@@ -129,6 +130,9 @@ pattern ANil'' = ANil' T.:$: T.Nil
 pattern ACons'' :: T.Term Python v -> T.Term Python v -> T.Term Python v
 pattern ACons'' a as = ACons' T.:$: T.Cons a (T.Cons as T.Nil)
 
+pattern Locate'' :: Span -> T.Term Python v -> T.Term Python v
+pattern Locate'' s t = Locate' s T.:$: T.Cons t T.Nil
+
 
 -- Abstract interpretation
 

From ed231118e1cdc8924574cc8bb79525e5899978ed Mon Sep 17 00:00:00 2001
From: Rob Rix <robrix@github.com>
Date: Mon, 18 Mar 2024 12:28:04 -0400
Subject: [PATCH 34/59] Completeness.

---
 semantic-analysis/src/Analysis/Syntax/Python.hs | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/semantic-analysis/src/Analysis/Syntax/Python.hs b/semantic-analysis/src/Analysis/Syntax/Python.hs
index de7cd506af..271f1ac614 100644
--- a/semantic-analysis/src/Analysis/Syntax/Python.hs
+++ b/semantic-analysis/src/Analysis/Syntax/Python.hs
@@ -133,6 +133,8 @@ pattern ACons'' a as = ACons' T.:$: T.Cons a (T.Cons as T.Nil)
 pattern Locate'' :: Span -> T.Term Python v -> T.Term Python v
 pattern Locate'' s t = Locate' s T.:$: T.Cons t T.Nil
 
+{-# COMPLETE Noop'', Iff'', Bool'', String'', Throw'', Import'', Function'', Call'', Locate'' #-}
+
 
 -- Abstract interpretation
 

From 948a5c77a2590452a610d5fa2b0110109515bd4e Mon Sep 17 00:00:00 2001
From: Rob Rix <robrix@github.com>
Date: Mon, 18 Mar 2024 12:29:59 -0400
Subject: [PATCH 35/59] Sequencing.

---
 semantic-analysis/src/Analysis/Syntax/Python.hs | 10 ++++++++--
 1 file changed, 8 insertions(+), 2 deletions(-)

diff --git a/semantic-analysis/src/Analysis/Syntax/Python.hs b/semantic-analysis/src/Analysis/Syntax/Python.hs
index 271f1ac614..e93bb2d945 100644
--- a/semantic-analysis/src/Analysis/Syntax/Python.hs
+++ b/semantic-analysis/src/Analysis/Syntax/Python.hs
@@ -16,6 +16,7 @@ module Analysis.Syntax.Python
 , pattern Bool''
 , pattern String''
 , pattern Throw''
+, pattern (:>>>>)
 , pattern Import''
 , pattern Function''
 , pattern Call''
@@ -25,7 +26,7 @@ module Analysis.Syntax.Python
 , eval
 ) where
 
-import           Analysis.Effect.Domain
+import           Analysis.Effect.Domain hiding ((:>>>))
 import qualified Analysis.Effect.Statement as S
 import           Analysis.Name
 import           Analysis.Reference
@@ -105,6 +106,11 @@ pattern String'' t = String' t T.:$: T.Nil
 pattern Throw'' :: T.Term Python v -> T.Term Python v
 pattern Throw'' e = Throw' T.:$: T.Cons e T.Nil
 
+pattern (:>>>>) :: T.Term Python v -> T.Term Python v -> T.Term Python v
+pattern s :>>>> t = (:>>>) T.:$: T.Cons s (T.Cons t T.Nil)
+
+infixl 1 :>>>>
+
 pattern Import'' :: NonEmpty Text -> T.Term Python v
 pattern Import'' i = Import' i T.:$: T.Nil
 
@@ -133,7 +139,7 @@ pattern ACons'' a as = ACons' T.:$: T.Cons a (T.Cons as T.Nil)
 pattern Locate'' :: Span -> T.Term Python v -> T.Term Python v
 pattern Locate'' s t = Locate' s T.:$: T.Cons t T.Nil
 
-{-# COMPLETE Noop'', Iff'', Bool'', String'', Throw'', Import'', Function'', Call'', Locate'' #-}
+{-# COMPLETE Noop'', Iff'', Bool'', String'', Throw'', (:>>>>), Import'', Function'', Call'', Locate'' #-}
 
 
 -- Abstract interpretation

From e1a6215ec4358f66e2c672026f6162a50e263014 Mon Sep 17 00:00:00 2001
From: Rob Rix <robrix@github.com>
Date: Mon, 18 Mar 2024 15:55:00 -0400
Subject: [PATCH 36/59] HLint.

---
 semantic-analysis/src/Analysis/Name.hs | 1 -
 1 file changed, 1 deletion(-)

diff --git a/semantic-analysis/src/Analysis/Name.hs b/semantic-analysis/src/Analysis/Name.hs
index aa28abdbf3..17f4914ccf 100644
--- a/semantic-analysis/src/Analysis/Name.hs
+++ b/semantic-analysis/src/Analysis/Name.hs
@@ -1,5 +1,4 @@
 {-# LANGUAGE FlexibleContexts #-}
-{-# LANGUAGE OverloadedStrings #-}
 module Analysis.Name
 ( Name
   -- * Constructors

From fecfa07f6cc32e8ee85621f61f627db8ab18e628 Mon Sep 17 00:00:00 2001
From: Rob Rix <robrix@github.com>
Date: Mon, 18 Mar 2024 15:58:13 -0400
Subject: [PATCH 37/59] Let.

---
 semantic-analysis/src/Analysis/Syntax/Python.hs | 7 ++++++-
 1 file changed, 6 insertions(+), 1 deletion(-)

diff --git a/semantic-analysis/src/Analysis/Syntax/Python.hs b/semantic-analysis/src/Analysis/Syntax/Python.hs
index e93bb2d945..567c074a92 100644
--- a/semantic-analysis/src/Analysis/Syntax/Python.hs
+++ b/semantic-analysis/src/Analysis/Syntax/Python.hs
@@ -16,6 +16,7 @@ module Analysis.Syntax.Python
 , pattern Bool''
 , pattern String''
 , pattern Throw''
+, pattern Let''
 , pattern (:>>>>)
 , pattern Import''
 , pattern Function''
@@ -81,6 +82,7 @@ data Python (arity :: T.Nat) where
   Bool' :: Bool -> Python T.N0
   String' :: Text -> Python T.N0
   Throw' :: Python T.N1
+  Let' :: Name -> Python T.N2
   (:>>>) :: Python T.N2
   Import' :: NonEmpty Text -> Python T.N0
   Function' :: Name -> [Name] -> Python T.N1
@@ -106,6 +108,9 @@ pattern String'' t = String' t T.:$: T.Nil
 pattern Throw'' :: T.Term Python v -> T.Term Python v
 pattern Throw'' e = Throw' T.:$: T.Cons e T.Nil
 
+pattern Let'' :: Name -> T.Term Python v -> T.Term Python v -> T.Term Python v
+pattern Let'' n v b = Let' n T.:$: T.Cons v (T.Cons b T.Nil)
+
 pattern (:>>>>) :: T.Term Python v -> T.Term Python v -> T.Term Python v
 pattern s :>>>> t = (:>>>) T.:$: T.Cons s (T.Cons t T.Nil)
 
@@ -139,7 +144,7 @@ pattern ACons'' a as = ACons' T.:$: T.Cons a (T.Cons as T.Nil)
 pattern Locate'' :: Span -> T.Term Python v -> T.Term Python v
 pattern Locate'' s t = Locate' s T.:$: T.Cons t T.Nil
 
-{-# COMPLETE Noop'', Iff'', Bool'', String'', Throw'', (:>>>>), Import'', Function'', Call'', Locate'' #-}
+{-# COMPLETE Noop'', Iff'', Bool'', String'', Throw'', Let'', (:>>>>), Import'', Function'', Call'', Locate'' #-}
 
 
 -- Abstract interpretation

From b9ba190c6a123e58800262d2fcafb12acd2398a1 Mon Sep 17 00:00:00 2001
From: Rob Rix <robrix@github.com>
Date: Mon, 18 Mar 2024 15:59:22 -0400
Subject: [PATCH 38/59] Port eval over.

---
 .../src/Analysis/Syntax/Python.hs             | 30 +++++++++----------
 1 file changed, 15 insertions(+), 15 deletions(-)

diff --git a/semantic-analysis/src/Analysis/Syntax/Python.hs b/semantic-analysis/src/Analysis/Syntax/Python.hs
index 567c074a92..c00a0a1628 100644
--- a/semantic-analysis/src/Analysis/Syntax/Python.hs
+++ b/semantic-analysis/src/Analysis/Syntax/Python.hs
@@ -149,35 +149,35 @@ pattern Locate'' s t = Locate' s T.:$: T.Cons t T.Nil
 
 -- Abstract interpretation
 
-eval0 :: (Has (Env addr) sig m, HasLabelled Store (Store addr val) sig m, Has (Dom val) sig m, Has (Reader Reference) sig m, Has S.Statement sig m) => Term -> m val
+eval0 :: (Has (Env addr) sig m, HasLabelled Store (Store addr val) sig m, Has (Dom val) sig m, Has (Reader Reference) sig m, Has S.Statement sig m) => T.Term Python Name -> m val
 eval0 = fix eval
 
 eval
   :: (Has (Env addr) sig m, HasLabelled Store (Store addr val) sig m, Has (Dom val) sig m, Has (Reader Reference) sig m, Has S.Statement sig m)
-  => (Term -> m val)
-  -> (Term -> m val)
+  => (T.Term Python Name -> m val)
+  -> (T.Term Python Name -> m val)
 eval eval = \case
-  Var n     -> lookupEnv n >>= maybe (dvar n) fetch
-  Noop      -> dunit
-  Iff c t e -> do
+  T.Var n     -> lookupEnv n >>= maybe (dvar n) fetch
+  Noop''      -> dunit
+  Iff'' c t e -> do
     c' <- eval c
     dif c' (eval t) (eval e)
-  Bool b    -> dbool b
-  String s  -> dstring s
-  Throw e   -> eval e >>= ddie
-  Let n v b -> do
+  Bool'' b    -> dbool b
+  String'' s  -> dstring s
+  Throw'' e   -> eval e >>= ddie
+  Let'' n v b -> do
     v' <- eval v
     let' n v' (eval b)
-  t :>> u   -> do
+  t :>>>> u   -> do
     t' <- eval t
     u' <- eval u
     t' >>> u'
-  Import ns -> S.simport ns >> dunit
-  Function n ps b -> letrec n (dabs ps (foldr (\ (p, a) m -> let' p a m) (eval b) . zip ps))
-  Call f as -> do
+  Import'' ns -> S.simport ns >> dunit
+  Function'' n ps b -> letrec n (dabs ps (foldr (\ (p, a) m -> let' p a m) (eval b) . zip ps))
+  Call'' f as -> do
     f' <- eval f
     as' <- traverse eval as
     dapp f' as'
-  Locate s t -> local (setSpan s) (eval t)
+  Locate'' s t -> local (setSpan s) (eval t)
   where
   setSpan s r = r{ refSpan = s }

From 692c3f2b40139e07ca6348e01bed0ab26ad1103c Mon Sep 17 00:00:00 2001
From: Rob Rix <robrix@github.com>
Date: Mon, 18 Mar 2024 16:03:39 -0400
Subject: [PATCH 39/59] :fire: Term.

---
 .../src/Analysis/Syntax/Python.hs             | 37 +------------------
 1 file changed, 1 insertion(+), 36 deletions(-)

diff --git a/semantic-analysis/src/Analysis/Syntax/Python.hs b/semantic-analysis/src/Analysis/Syntax/Python.hs
index c00a0a1628..a18decd34c 100644
--- a/semantic-analysis/src/Analysis/Syntax/Python.hs
+++ b/semantic-analysis/src/Analysis/Syntax/Python.hs
@@ -8,8 +8,7 @@
 -- | This belongs in @semantic-python@ instead of @semantic-analysis@, but for the sake of expedience…
 module Analysis.Syntax.Python
 ( -- * Syntax
-  Term(..)
-, subterms
+  T.Term(..)
 , Python(..)
 , pattern Noop''
 , pattern Iff''
@@ -37,45 +36,11 @@ import           Control.Effect.Labelled
 import           Control.Effect.Reader
 import           Data.Function (fix)
 import           Data.List.NonEmpty (NonEmpty)
-import qualified Data.Set as Set
 import           Data.Text (Text)
 import           Source.Span (Span)
 
 -- Syntax
 
-data Term
-  = Var Name
-  | Noop
-  | Iff Term Term Term
-  | Bool Bool
-  | String Text
-  | Throw Term
-  | Let Name Term Term
-  | Term :>> Term
-  | Import (NonEmpty Text)
-  | Function Name [Name] Term
-  | Call Term [Term]
-  | Locate Span Term
-  deriving (Eq, Ord, Show)
-
-infixl 1 :>>
-
-subterms :: Term -> Set.Set Term
-subterms t = Set.singleton t <> case t of
-  Var _          -> mempty
-  Noop           -> mempty
-  Iff c t e      -> subterms c <> subterms t <> subterms e
-  Bool _         -> mempty
-  String _       -> mempty
-  Throw t        -> subterms t
-  Let _ v b      -> subterms v <> subterms b
-  a :>> b        -> subterms a <> subterms b
-  Import _       -> mempty
-  Function _ _ b -> subterms b
-  Call f as      -> subterms f <> foldMap subterms as
-  Locate _ b     -> subterms b
-
-
 data Python (arity :: T.Nat) where
   Noop' :: Python T.N0
   Iff' :: Python T.N3

From e7c5928f730b53bcd3430e91edb61bc9d965da2c Mon Sep 17 00:00:00 2001
From: Rob Rix <robrix@github.com>
Date: Mon, 18 Mar 2024 16:04:51 -0400
Subject: [PATCH 40/59] Rename the synonyms to elide the primes.

---
 .../src/Analysis/Syntax/Python.hs             | 106 +++++++++---------
 1 file changed, 53 insertions(+), 53 deletions(-)

diff --git a/semantic-analysis/src/Analysis/Syntax/Python.hs b/semantic-analysis/src/Analysis/Syntax/Python.hs
index a18decd34c..e72578f308 100644
--- a/semantic-analysis/src/Analysis/Syntax/Python.hs
+++ b/semantic-analysis/src/Analysis/Syntax/Python.hs
@@ -10,17 +10,17 @@ module Analysis.Syntax.Python
 ( -- * Syntax
   T.Term(..)
 , Python(..)
-, pattern Noop''
-, pattern Iff''
-, pattern Bool''
-, pattern String''
-, pattern Throw''
-, pattern Let''
-, pattern (:>>>>)
-, pattern Import''
-, pattern Function''
-, pattern Call''
-, pattern Locate''
+, pattern Noop
+, pattern Iff
+, pattern Bool
+, pattern String
+, pattern Throw
+, pattern Let
+, pattern (:>>)
+, pattern Import
+, pattern Function
+, pattern Call
+, pattern Locate
   -- * Abstract interpretation
 , eval0
 , eval
@@ -58,58 +58,58 @@ data Python (arity :: T.Nat) where
 
 infixl 1 :>>>
 
-pattern Noop'' :: T.Term Python v
-pattern Noop'' = Noop' T.:$: T.Nil
+pattern Noop :: T.Term Python v
+pattern Noop = Noop' T.:$: T.Nil
 
-pattern Iff'' :: T.Term Python v -> T.Term Python v -> T.Term Python v -> T.Term Python v
-pattern Iff'' c t e = Iff' T.:$: T.Cons c (T.Cons t (T.Cons e T.Nil))
+pattern Iff :: T.Term Python v -> T.Term Python v -> T.Term Python v -> T.Term Python v
+pattern Iff c t e = Iff' T.:$: T.Cons c (T.Cons t (T.Cons e T.Nil))
 
-pattern Bool'' :: Bool -> T.Term Python v
-pattern Bool'' b = Bool' b T.:$: T.Nil
+pattern Bool :: Bool -> T.Term Python v
+pattern Bool b = Bool' b T.:$: T.Nil
 
-pattern String'' :: Text -> T.Term Python v
-pattern String'' t = String' t T.:$: T.Nil
+pattern String :: Text -> T.Term Python v
+pattern String t = String' t T.:$: T.Nil
 
-pattern Throw'' :: T.Term Python v -> T.Term Python v
-pattern Throw'' e = Throw' T.:$: T.Cons e T.Nil
+pattern Throw :: T.Term Python v -> T.Term Python v
+pattern Throw e = Throw' T.:$: T.Cons e T.Nil
 
-pattern Let'' :: Name -> T.Term Python v -> T.Term Python v -> T.Term Python v
-pattern Let'' n v b = Let' n T.:$: T.Cons v (T.Cons b T.Nil)
+pattern Let :: Name -> T.Term Python v -> T.Term Python v -> T.Term Python v
+pattern Let n v b = Let' n T.:$: T.Cons v (T.Cons b T.Nil)
 
-pattern (:>>>>) :: T.Term Python v -> T.Term Python v -> T.Term Python v
-pattern s :>>>> t = (:>>>) T.:$: T.Cons s (T.Cons t T.Nil)
+pattern (:>>) :: T.Term Python v -> T.Term Python v -> T.Term Python v
+pattern s :>> t = (:>>>) T.:$: T.Cons s (T.Cons t T.Nil)
 
-infixl 1 :>>>>
+infixl 1 :>>
 
-pattern Import'' :: NonEmpty Text -> T.Term Python v
-pattern Import'' i = Import' i T.:$: T.Nil
+pattern Import :: NonEmpty Text -> T.Term Python v
+pattern Import i = Import' i T.:$: T.Nil
 
-pattern Function'' :: Name -> [Name] -> T.Term Python v -> T.Term Python v
-pattern Function'' n as b = Function' n as T.:$: T.Cons b T.Nil
+pattern Function :: Name -> [Name] -> T.Term Python v -> T.Term Python v
+pattern Function n as b = Function' n as T.:$: T.Cons b T.Nil
 
-pattern Call''
+pattern Call
   :: T.Term Python v
   -> [T.Term Python v]
   -> T.Term Python v
-pattern Call'' f as <- Call' T.:$: T.Cons f (T.Cons (fromArgs -> as) T.Nil)
-  where Call'' f as = Call' T.:$: T.Cons f (T.Cons (foldr ACons'' ANil'' as) T.Nil)
+pattern Call f as <- Call' T.:$: T.Cons f (T.Cons (fromArgs -> as) T.Nil)
+  where Call f as = Call' T.:$: T.Cons f (T.Cons (foldr ACons ANil as) T.Nil)
 
 fromArgs :: T.Term Python v -> [T.Term Python v]
 fromArgs = \case
-  ANil'' -> []
-  ACons'' a as -> a:fromArgs as
+  ANil -> []
+  ACons a as -> a:fromArgs as
   _ -> fail "unexpected constructor in spine of argument list"
 
-pattern ANil'' :: T.Term Python v
-pattern ANil'' = ANil' T.:$: T.Nil
+pattern ANil :: T.Term Python v
+pattern ANil = ANil' T.:$: T.Nil
 
-pattern ACons'' :: T.Term Python v -> T.Term Python v -> T.Term Python v
-pattern ACons'' a as = ACons' T.:$: T.Cons a (T.Cons as T.Nil)
+pattern ACons :: T.Term Python v -> T.Term Python v -> T.Term Python v
+pattern ACons a as = ACons' T.:$: T.Cons a (T.Cons as T.Nil)
 
-pattern Locate'' :: Span -> T.Term Python v -> T.Term Python v
-pattern Locate'' s t = Locate' s T.:$: T.Cons t T.Nil
+pattern Locate :: Span -> T.Term Python v -> T.Term Python v
+pattern Locate s t = Locate' s T.:$: T.Cons t T.Nil
 
-{-# COMPLETE Noop'', Iff'', Bool'', String'', Throw'', Let'', (:>>>>), Import'', Function'', Call'', Locate'' #-}
+{-# COMPLETE Noop, Iff, Bool, String, Throw, Let, (:>>), Import, Function, Call, Locate #-}
 
 
 -- Abstract interpretation
@@ -123,26 +123,26 @@ eval
   -> (T.Term Python Name -> m val)
 eval eval = \case
   T.Var n     -> lookupEnv n >>= maybe (dvar n) fetch
-  Noop''      -> dunit
-  Iff'' c t e -> do
+  Noop      -> dunit
+  Iff c t e -> do
     c' <- eval c
     dif c' (eval t) (eval e)
-  Bool'' b    -> dbool b
-  String'' s  -> dstring s
-  Throw'' e   -> eval e >>= ddie
-  Let'' n v b -> do
+  Bool b    -> dbool b
+  String s  -> dstring s
+  Throw e   -> eval e >>= ddie
+  Let n v b -> do
     v' <- eval v
     let' n v' (eval b)
-  t :>>>> u   -> do
+  t :>> u   -> do
     t' <- eval t
     u' <- eval u
     t' >>> u'
-  Import'' ns -> S.simport ns >> dunit
-  Function'' n ps b -> letrec n (dabs ps (foldr (\ (p, a) m -> let' p a m) (eval b) . zip ps))
-  Call'' f as -> do
+  Import ns -> S.simport ns >> dunit
+  Function n ps b -> letrec n (dabs ps (foldr (\ (p, a) m -> let' p a m) (eval b) . zip ps))
+  Call f as -> do
     f' <- eval f
     as' <- traverse eval as
     dapp f' as'
-  Locate'' s t -> local (setSpan s) (eval t)
+  Locate s t -> local (setSpan s) (eval t)
   where
   setSpan s r = r{ refSpan = s }

From cdde997e619ab3f927c1d66d4934d3fc867d272d Mon Sep 17 00:00:00 2001
From: Rob Rix <robrix@github.com>
Date: Mon, 18 Mar 2024 16:05:10 -0400
Subject: [PATCH 41/59] Spacing.

---
 semantic-analysis/src/Analysis/Syntax/Python.hs | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/semantic-analysis/src/Analysis/Syntax/Python.hs b/semantic-analysis/src/Analysis/Syntax/Python.hs
index e72578f308..059e49a6d1 100644
--- a/semantic-analysis/src/Analysis/Syntax/Python.hs
+++ b/semantic-analysis/src/Analysis/Syntax/Python.hs
@@ -122,7 +122,7 @@ eval
   => (T.Term Python Name -> m val)
   -> (T.Term Python Name -> m val)
 eval eval = \case
-  T.Var n     -> lookupEnv n >>= maybe (dvar n) fetch
+  T.Var n   -> lookupEnv n >>= maybe (dvar n) fetch
   Noop      -> dunit
   Iff c t e -> do
     c' <- eval c

From be357c043a5f559ff701571877c1739f6ea2b0c9 Mon Sep 17 00:00:00 2001
From: Rob Rix <robrix@github.com>
Date: Mon, 18 Mar 2024 16:07:26 -0400
Subject: [PATCH 42/59] Define a synonym for Term.

---
 semantic-analysis/src/Analysis/Syntax/Python.hs | 10 ++++++----
 1 file changed, 6 insertions(+), 4 deletions(-)

diff --git a/semantic-analysis/src/Analysis/Syntax/Python.hs b/semantic-analysis/src/Analysis/Syntax/Python.hs
index 059e49a6d1..7f92f2bddd 100644
--- a/semantic-analysis/src/Analysis/Syntax/Python.hs
+++ b/semantic-analysis/src/Analysis/Syntax/Python.hs
@@ -8,7 +8,7 @@
 -- | This belongs in @semantic-python@ instead of @semantic-analysis@, but for the sake of expedience…
 module Analysis.Syntax.Python
 ( -- * Syntax
-  T.Term(..)
+  Term
 , Python(..)
 , pattern Noop
 , pattern Iff
@@ -41,6 +41,8 @@ import           Source.Span (Span)
 
 -- Syntax
 
+type Term = T.Term Python Name
+
 data Python (arity :: T.Nat) where
   Noop' :: Python T.N0
   Iff' :: Python T.N3
@@ -114,13 +116,13 @@ pattern Locate s t = Locate' s T.:$: T.Cons t T.Nil
 
 -- Abstract interpretation
 
-eval0 :: (Has (Env addr) sig m, HasLabelled Store (Store addr val) sig m, Has (Dom val) sig m, Has (Reader Reference) sig m, Has S.Statement sig m) => T.Term Python Name -> m val
+eval0 :: (Has (Env addr) sig m, HasLabelled Store (Store addr val) sig m, Has (Dom val) sig m, Has (Reader Reference) sig m, Has S.Statement sig m) => Term -> m val
 eval0 = fix eval
 
 eval
   :: (Has (Env addr) sig m, HasLabelled Store (Store addr val) sig m, Has (Dom val) sig m, Has (Reader Reference) sig m, Has S.Statement sig m)
-  => (T.Term Python Name -> m val)
-  -> (T.Term Python Name -> m val)
+  => (Term -> m val)
+  -> (Term -> m val)
 eval eval = \case
   T.Var n   -> lookupEnv n >>= maybe (dvar n) fetch
   Noop      -> dunit

From f96b14d07aee0276e100899f64cfab6d4f7691ec Mon Sep 17 00:00:00 2001
From: Rob Rix <robrix@github.com>
Date: Tue, 19 Mar 2024 10:48:50 -0400
Subject: [PATCH 43/59] Tone down the fancy.

---
 semantic-analysis/src/Analysis/Syntax.hs      | 38 +++++++++----------
 .../src/Analysis/Syntax/Python.hs             |  2 +-
 2 files changed, 19 insertions(+), 21 deletions(-)

diff --git a/semantic-analysis/src/Analysis/Syntax.hs b/semantic-analysis/src/Analysis/Syntax.hs
index a165599f1d..fa311d4e2a 100644
--- a/semantic-analysis/src/Analysis/Syntax.hs
+++ b/semantic-analysis/src/Analysis/Syntax.hs
@@ -1,4 +1,3 @@
-{-# LANGUAGE DataKinds #-}
 {-# LANGUAGE GADTs #-}
 {-# LANGUAGE KindSignatures #-}
 {-# LANGUAGE LambdaCase #-}
@@ -11,7 +10,8 @@ module Analysis.Syntax
   Term(..)
 , subterms
   -- * Vectors
-, Nat(..)
+, Z
+, S
 , N0
 , N1
 , N2
@@ -29,7 +29,7 @@ import           Unsafe.Coerce (unsafeCoerce)
 -- Syntax
 
 -- | (Currently) untyped term representations.
-data Term (sig :: Nat -> Type) v where
+data Term (sig :: Type -> Type) v where
   Var  :: v -> Term sig v
   (:$:) :: KnownNat n => sig n -> Vec n (Term sig v) -> Term sig v
 
@@ -57,26 +57,24 @@ subterms t = case t of
 
 -- Vectors
 
-data Nat
-  = Z
-  | S Nat
-  deriving (Eq, Ord, Show)
+data Z
+data S n
 
-type N0 = 'Z
-type N1 = 'S N0
-type N2 = 'S N1
-type N3 = 'S N2
+type N0 = Z
+type N1 = S N0
+type N2 = S N1
+type N3 = S N2
 
 
 -- | Reify 'Nat's back from type-level singletons.
-class KnownNat (n :: Nat) where
-  reifyNat :: proxy n -> Nat
+class KnownNat n where
+  reifyNat :: proxy n -> Int
 
-instance KnownNat 'Z where
-  reifyNat _ = Z
+instance KnownNat Z where
+  reifyNat _ = 0
 
-instance KnownNat n => KnownNat ('S n) where
-  reifyNat _ = S (reifyNat (undefined :: proxy n))
+instance KnownNat n => KnownNat (S n) where
+  reifyNat _ = 1 + reifyNat (undefined :: proxy n)
 
 
 -- | Test the equality of type-level 'Nat's at runtime, generating a type-level equality if equal.
@@ -85,9 +83,9 @@ sameNat a b = unsafeCoerce Refl <$ guard (reifyNat a == reifyNat b)
 
 
 -- FIXME: move this into its own module, or use a dependency, or something.
-data Vec (n :: Nat) a where
-  Nil :: Vec 'Z a
-  Cons :: a -> Vec n a -> Vec ('S n) a
+data Vec n a where
+  Nil :: Vec Z a
+  Cons :: a -> Vec n a -> Vec (S n) a
 
 instance Eq a => Eq (Vec n a) where
   Nil       == Nil       = True
diff --git a/semantic-analysis/src/Analysis/Syntax/Python.hs b/semantic-analysis/src/Analysis/Syntax/Python.hs
index 7f92f2bddd..fd7d14cbb9 100644
--- a/semantic-analysis/src/Analysis/Syntax/Python.hs
+++ b/semantic-analysis/src/Analysis/Syntax/Python.hs
@@ -43,7 +43,7 @@ import           Source.Span (Span)
 
 type Term = T.Term Python Name
 
-data Python (arity :: T.Nat) where
+data Python arity where
   Noop' :: Python T.N0
   Iff' :: Python T.N3
   Bool' :: Bool -> Python T.N0

From 6ea208f7f8c73ad33fd802bf7baafb8af13ab3ec Mon Sep 17 00:00:00 2001
From: Rob Rix <robrix@github.com>
Date: Tue, 19 Mar 2024 10:52:00 -0400
Subject: [PATCH 44/59] :fire: toList.

---
 semantic-analysis/src/Analysis/Syntax.hs | 8 --------
 1 file changed, 8 deletions(-)

diff --git a/semantic-analysis/src/Analysis/Syntax.hs b/semantic-analysis/src/Analysis/Syntax.hs
index fa311d4e2a..f547b887ec 100644
--- a/semantic-analysis/src/Analysis/Syntax.hs
+++ b/semantic-analysis/src/Analysis/Syntax.hs
@@ -1,6 +1,5 @@
 {-# LANGUAGE GADTs #-}
 {-# LANGUAGE KindSignatures #-}
-{-# LANGUAGE LambdaCase #-}
 {-# LANGUAGE QuantifiedConstraints #-}
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE TypeOperators #-}
@@ -17,7 +16,6 @@ module Analysis.Syntax
 , N2
 , N3
 , Vec(..)
-, toList
 ) where
 
 import           Control.Monad (guard)
@@ -98,9 +96,3 @@ instance Ord a => Ord (Vec n a) where
 instance Foldable (Vec n) where
   foldMap _ Nil         = mempty
   foldMap f (Cons a as) = f a <> foldMap f as
-
-
-toList :: Vec n a -> [a]
-toList = \case
-  Nil -> []
-  Cons a as -> a : toList as

From 02971162a53997e7d32f9ee7823b819b1e1e9701 Mon Sep 17 00:00:00 2001
From: Rob Rix <robrix@github.com>
Date: Tue, 19 Mar 2024 11:00:04 -0400
Subject: [PATCH 45/59] Dial the fancy even further back.

---
 semantic-analysis/src/Analysis/Syntax.hs | 45 +++++-------------------
 1 file changed, 9 insertions(+), 36 deletions(-)

diff --git a/semantic-analysis/src/Analysis/Syntax.hs b/semantic-analysis/src/Analysis/Syntax.hs
index f547b887ec..96c752b9d6 100644
--- a/semantic-analysis/src/Analysis/Syntax.hs
+++ b/semantic-analysis/src/Analysis/Syntax.hs
@@ -1,9 +1,4 @@
 {-# LANGUAGE GADTs #-}
-{-# LANGUAGE KindSignatures #-}
-{-# LANGUAGE QuantifiedConstraints #-}
-{-# LANGUAGE ScopedTypeVariables #-}
-{-# LANGUAGE TypeOperators #-}
-{-# LANGUAGE UndecidableInstances #-}
 module Analysis.Syntax
 ( -- * Syntax
   Term(..)
@@ -18,36 +13,30 @@ module Analysis.Syntax
 , Vec(..)
 ) where
 
-import           Control.Monad (guard)
-import           Data.Kind (Type)
+import           Data.Foldable (toList)
+import           Data.Functor.Classes
 import qualified Data.Set as Set
-import           Data.Typeable
-import           Unsafe.Coerce (unsafeCoerce)
 
 -- Syntax
 
 -- | (Currently) untyped term representations.
-data Term (sig :: Type -> Type) v where
+data Term sig v where
   Var  :: v -> Term sig v
-  (:$:) :: KnownNat n => sig n -> Vec n (Term sig v) -> Term sig v
+  (:$:) :: sig n -> Vec n (Term sig v) -> Term sig v
 
-instance (forall n . Eq (sig n), Eq v) => Eq (Term sig v) where
+instance (Eq1 sig, Eq v) => Eq (Term sig v) where
   Var v1   == Var v2   = v1 == v2
-  a :$: as == b :$: bs = case sameNat a b of
-    Just Refl -> a == b && as == bs
-    _         -> False
+  a :$: as == b :$: bs = liftEq (\ _ _ -> True) a b && toList as == toList bs
   _        == _        = False
 
-instance (forall n . Ord (sig n), Ord v) => Ord (Term sig v) where
+instance (Ord1 sig, Ord v) => Ord (Term sig v) where
   compare (Var v1)   (Var v2)   = compare v1 v2
   compare (Var _)    _          = LT
-  compare (a :$: as) (b :$: bs) = case sameNat a b of
-    Just Refl -> compare a b <> compare as bs
-    _         -> reifyNat a `compare` reifyNat b -- lol
+  compare (a :$: as) (b :$: bs) = liftCompare (\ _ _ -> EQ) a b <> compare (toList as) (toList bs)
   compare _          _          = GT
 
 
-subterms :: (forall n . Ord (sig n), Ord v) => Term sig v -> Set.Set (Term sig v)
+subterms :: (Ord1 sig, Ord v) => Term sig v -> Set.Set (Term sig v)
 subterms t = case t of
   Var _    -> Set.singleton t
   _ :$: ts -> Set.insert t (foldMap subterms ts)
@@ -64,22 +53,6 @@ type N2 = S N1
 type N3 = S N2
 
 
--- | Reify 'Nat's back from type-level singletons.
-class KnownNat n where
-  reifyNat :: proxy n -> Int
-
-instance KnownNat Z where
-  reifyNat _ = 0
-
-instance KnownNat n => KnownNat (S n) where
-  reifyNat _ = 1 + reifyNat (undefined :: proxy n)
-
-
--- | Test the equality of type-level 'Nat's at runtime, generating a type-level equality if equal.
-sameNat :: forall a b proxy1 proxy2 . (KnownNat a, KnownNat b) => proxy1 a -> proxy2 b -> Maybe (a :~: b)
-sameNat a b = unsafeCoerce Refl <$ guard (reifyNat a == reifyNat b)
-
-
 -- FIXME: move this into its own module, or use a dependency, or something.
 data Vec n a where
   Nil :: Vec Z a

From 4ed026b39ee88b0339326a0251ad3129c194bae1 Mon Sep 17 00:00:00 2001
From: Rob Rix <robrix@github.com>
Date: Tue, 19 Mar 2024 11:34:39 -0400
Subject: [PATCH 46/59] Define an Eq1 instance for Python.

---
 .../src/Analysis/Syntax/Python.hs             | 20 +++++++++++++++++++
 1 file changed, 20 insertions(+)

diff --git a/semantic-analysis/src/Analysis/Syntax/Python.hs b/semantic-analysis/src/Analysis/Syntax/Python.hs
index fd7d14cbb9..7761a0f145 100644
--- a/semantic-analysis/src/Analysis/Syntax/Python.hs
+++ b/semantic-analysis/src/Analysis/Syntax/Python.hs
@@ -35,6 +35,7 @@ import           Analysis.VM
 import           Control.Effect.Labelled
 import           Control.Effect.Reader
 import           Data.Function (fix)
+import           Data.Functor.Classes (Eq1 (..))
 import           Data.List.NonEmpty (NonEmpty)
 import           Data.Text (Text)
 import           Source.Span (Span)
@@ -114,6 +115,25 @@ pattern Locate s t = Locate' s T.:$: T.Cons t T.Nil
 {-# COMPLETE Noop, Iff, Bool, String, Throw, Let, (:>>), Import, Function, Call, Locate #-}
 
 
+instance Eq1 Python where
+  liftEq _ a b = case (a, b) of
+    (Noop', Noop')                       -> True
+    (Iff', Iff')                         -> True
+    (Bool' b1, Bool' b2)                 -> b1 == b2
+    (String' s1, String' s2)             -> s1 == s2
+    (Throw', Throw')                     -> True
+    (Let' n1, Let' n2)                   -> n1 == n2
+    ((:>>>), (:>>>))                     -> True
+    (Import' i1, Import' i2)             -> i1 == i2
+    (Function' n1 as1, Function' n2 as2) -> n1 == n2 && as1 == as2
+    (Call', Call')                       -> True
+    (ANil', ANil')                       -> True
+    (ACons', ACons')                     -> True
+    (Locate' s1, Locate' s2)             -> s1 == s2
+    _                                    -> False
+
+
+
 -- Abstract interpretation
 
 eval0 :: (Has (Env addr) sig m, HasLabelled Store (Store addr val) sig m, Has (Dom val) sig m, Has (Reader Reference) sig m, Has S.Statement sig m) => Term -> m val

From 5ccf3377d010777e260b21140437880322625ec1 Mon Sep 17 00:00:00 2001
From: Rob Rix <robrix@github.com>
Date: Tue, 19 Mar 2024 11:39:31 -0400
Subject: [PATCH 47/59] Define an Ord1 instance for Python.

---
 .../src/Analysis/Syntax/Python.hs             | 30 ++++++++++++++++++-
 1 file changed, 29 insertions(+), 1 deletion(-)

diff --git a/semantic-analysis/src/Analysis/Syntax/Python.hs b/semantic-analysis/src/Analysis/Syntax/Python.hs
index 7761a0f145..55034c7ee4 100644
--- a/semantic-analysis/src/Analysis/Syntax/Python.hs
+++ b/semantic-analysis/src/Analysis/Syntax/Python.hs
@@ -35,7 +35,7 @@ import           Analysis.VM
 import           Control.Effect.Labelled
 import           Control.Effect.Reader
 import           Data.Function (fix)
-import           Data.Functor.Classes (Eq1 (..))
+import           Data.Functor.Classes (Eq1 (..), Ord1 (..))
 import           Data.List.NonEmpty (NonEmpty)
 import           Data.Text (Text)
 import           Source.Span (Span)
@@ -132,6 +132,34 @@ instance Eq1 Python where
     (Locate' s1, Locate' s2)             -> s1 == s2
     _                                    -> False
 
+instance Ord1 Python where
+  liftCompare _ a b = case (a, b) of
+    (Noop', Noop')                       -> EQ
+    (Noop', _)                           -> LT
+    (Iff', Iff')                         -> EQ
+    (Iff', _)                            -> LT
+    (Bool' b1,  Bool' b2)                -> compare b1 b2
+    (Bool' _,  _)                        -> LT
+    (String' s1, String' s2)             -> compare s1 s2
+    (String' _, _)                       -> LT
+    (Throw', Throw')                     -> EQ
+    (Throw', _)                          -> LT
+    (Let' n1, Let' n2)                   -> compare n1 n2
+    (Let' _, _)                          -> LT
+    ((:>>>), (:>>>))                     -> EQ
+    ((:>>>), _)                          -> LT
+    (Import' i1, Import' i2)             -> compare i1 i2
+    (Import' _, _)                       -> LT
+    (Function' n1 as1, Function' n2 as2) -> compare n1 n2 <> compare as1 as2
+    (Function' _ _, _)                   -> LT
+    (Call', Call')                       -> EQ
+    (Call', _)                           -> LT
+    (ANil', ANil')                       -> EQ
+    (ANil', _)                           -> LT
+    (ACons', ACons')                     -> EQ
+    (ACons', _)                          -> LT
+    (Locate' s1, Locate' s2)             -> compare s1 s2
+    (Locate' _, _)                       -> LT
 
 
 -- Abstract interpretation

From 1df04e82f3f3ab8965eb2a3a71484f640d6cec63 Mon Sep 17 00:00:00 2001
From: Rob Rix <robrix@github.com>
Date: Tue, 19 Mar 2024 11:42:42 -0400
Subject: [PATCH 48/59] :fire: extensions.

---
 semantic-analysis/src/Analysis/Syntax/Python.hs | 2 --
 1 file changed, 2 deletions(-)

diff --git a/semantic-analysis/src/Analysis/Syntax/Python.hs b/semantic-analysis/src/Analysis/Syntax/Python.hs
index 55034c7ee4..f8af867716 100644
--- a/semantic-analysis/src/Analysis/Syntax/Python.hs
+++ b/semantic-analysis/src/Analysis/Syntax/Python.hs
@@ -1,7 +1,5 @@
-{-# LANGUAGE DataKinds #-}
 {-# LANGUAGE FlexibleContexts #-}
 {-# LANGUAGE GADTs #-}
-{-# LANGUAGE KindSignatures #-}
 {-# LANGUAGE LambdaCase #-}
 {-# LANGUAGE PatternSynonyms #-}
 {-# LANGUAGE ViewPatterns #-}

From 6812e35f73fba22a86cf316c1142c9c692661182 Mon Sep 17 00:00:00 2001
From: Rob Rix <robrix@github.com>
Date: Tue, 19 Mar 2024 11:52:30 -0400
Subject: [PATCH 49/59] Terms are free monads.

---
 semantic-analysis/src/Analysis/Syntax.hs      |  71 ++-----
 .../src/Analysis/Syntax/Python.hs             | 188 ++++--------------
 2 files changed, 53 insertions(+), 206 deletions(-)

diff --git a/semantic-analysis/src/Analysis/Syntax.hs b/semantic-analysis/src/Analysis/Syntax.hs
index 96c752b9d6..ebe36b7f40 100644
--- a/semantic-analysis/src/Analysis/Syntax.hs
+++ b/semantic-analysis/src/Analysis/Syntax.hs
@@ -1,71 +1,32 @@
-{-# LANGUAGE GADTs #-}
+{-# LANGUAGE QuantifiedConstraints #-}
 module Analysis.Syntax
 ( -- * Syntax
   Term(..)
 , subterms
-  -- * Vectors
-, Z
-, S
-, N0
-, N1
-, N2
-, N3
-, Vec(..)
 ) where
 
-import           Data.Foldable (toList)
-import           Data.Functor.Classes
 import qualified Data.Set as Set
 
 -- Syntax
 
 -- | (Currently) untyped term representations.
-data Term sig v where
-  Var  :: v -> Term sig v
-  (:$:) :: sig n -> Vec n (Term sig v) -> Term sig v
+data Term sig v
+  = Var v
+  | Term (sig (Term sig v))
 
-instance (Eq1 sig, Eq v) => Eq (Term sig v) where
-  Var v1   == Var v2   = v1 == v2
-  a :$: as == b :$: bs = liftEq (\ _ _ -> True) a b && toList as == toList bs
-  _        == _        = False
+instance (forall t . Eq t => Eq (sig t), Eq v) => Eq (Term sig v) where
+  Var v1   == Var v2 = v1 == v2
+  Term s1 == Term s2 = s1 == s2
+  _        == _      = False
 
-instance (Ord1 sig, Ord v) => Ord (Term sig v) where
-  compare (Var v1)   (Var v2)   = compare v1 v2
-  compare (Var _)    _          = LT
-  compare (a :$: as) (b :$: bs) = liftCompare (\ _ _ -> EQ) a b <> compare (toList as) (toList bs)
-  compare _          _          = GT
+instance (forall t . Eq t => Eq (sig t), forall t. Ord t => Ord (sig t), Ord v) => Ord (Term sig v) where
+  compare (Var v1)  (Var v2)  = compare v1 v2
+  compare (Var _)   _         = LT
+  compare (Term s1) (Term s2) = compare s1 s2
+  compare _          _        = GT
 
 
-subterms :: (Ord1 sig, Ord v) => Term sig v -> Set.Set (Term sig v)
+subterms :: (forall t . Eq t => Eq (sig t), forall t . Ord t => Ord (sig t), Ord v, Foldable sig) => Term sig v -> Set.Set (Term sig v)
 subterms t = case t of
-  Var _    -> Set.singleton t
-  _ :$: ts -> Set.insert t (foldMap subterms ts)
-
-
--- Vectors
-
-data Z
-data S n
-
-type N0 = Z
-type N1 = S N0
-type N2 = S N1
-type N3 = S N2
-
-
--- FIXME: move this into its own module, or use a dependency, or something.
-data Vec n a where
-  Nil :: Vec Z a
-  Cons :: a -> Vec n a -> Vec (S n) a
-
-instance Eq a => Eq (Vec n a) where
-  Nil       == Nil       = True
-  Cons a as == Cons b bs = a == b && as == bs
-
-instance Ord a => Ord (Vec n a) where
-  compare Nil         Nil         = EQ
-  compare (Cons a as) (Cons b bs) = a `compare` b <> as `compare` bs
-
-instance Foldable (Vec n) where
-  foldMap _ Nil         = mempty
-  foldMap f (Cons a as) = f a <> foldMap f as
+  Var _  -> Set.singleton t
+  Term s -> Set.insert t (foldMap subterms s)
diff --git a/semantic-analysis/src/Analysis/Syntax/Python.hs b/semantic-analysis/src/Analysis/Syntax/Python.hs
index f8af867716..f13a5dc360 100644
--- a/semantic-analysis/src/Analysis/Syntax/Python.hs
+++ b/semantic-analysis/src/Analysis/Syntax/Python.hs
@@ -1,24 +1,11 @@
+{-# LANGUAGE DeriveTraversable #-}
 {-# LANGUAGE FlexibleContexts #-}
-{-# LANGUAGE GADTs #-}
 {-# LANGUAGE LambdaCase #-}
-{-# LANGUAGE PatternSynonyms #-}
-{-# LANGUAGE ViewPatterns #-}
 -- | This belongs in @semantic-python@ instead of @semantic-analysis@, but for the sake of expedience…
 module Analysis.Syntax.Python
 ( -- * Syntax
   Term
 , Python(..)
-, pattern Noop
-, pattern Iff
-, pattern Bool
-, pattern String
-, pattern Throw
-, pattern Let
-, pattern (:>>)
-, pattern Import
-, pattern Function
-, pattern Call
-, pattern Locate
   -- * Abstract interpretation
 , eval0
 , eval
@@ -33,7 +20,6 @@ import           Analysis.VM
 import           Control.Effect.Labelled
 import           Control.Effect.Reader
 import           Data.Function (fix)
-import           Data.Functor.Classes (Eq1 (..), Ord1 (..))
 import           Data.List.NonEmpty (NonEmpty)
 import           Data.Text (Text)
 import           Source.Span (Span)
@@ -42,123 +28,22 @@ import           Source.Span (Span)
 
 type Term = T.Term Python Name
 
-data Python arity where
-  Noop' :: Python T.N0
-  Iff' :: Python T.N3
-  Bool' :: Bool -> Python T.N0
-  String' :: Text -> Python T.N0
-  Throw' :: Python T.N1
-  Let' :: Name -> Python T.N2
-  (:>>>) :: Python T.N2
-  Import' :: NonEmpty Text -> Python T.N0
-  Function' :: Name -> [Name] -> Python T.N1
-  Call' :: Python T.N2 -- ^ Second should be an @ANil'@ or @ACons'@.
-  ANil' :: Python T.N0
-  ACons' :: Python T.N2 -- ^ Second should be an @ANil'@ or @ACons'@.
-  Locate' :: Span -> Python T.N1
-
-infixl 1 :>>>
-
-pattern Noop :: T.Term Python v
-pattern Noop = Noop' T.:$: T.Nil
-
-pattern Iff :: T.Term Python v -> T.Term Python v -> T.Term Python v -> T.Term Python v
-pattern Iff c t e = Iff' T.:$: T.Cons c (T.Cons t (T.Cons e T.Nil))
-
-pattern Bool :: Bool -> T.Term Python v
-pattern Bool b = Bool' b T.:$: T.Nil
-
-pattern String :: Text -> T.Term Python v
-pattern String t = String' t T.:$: T.Nil
-
-pattern Throw :: T.Term Python v -> T.Term Python v
-pattern Throw e = Throw' T.:$: T.Cons e T.Nil
-
-pattern Let :: Name -> T.Term Python v -> T.Term Python v -> T.Term Python v
-pattern Let n v b = Let' n T.:$: T.Cons v (T.Cons b T.Nil)
-
-pattern (:>>) :: T.Term Python v -> T.Term Python v -> T.Term Python v
-pattern s :>> t = (:>>>) T.:$: T.Cons s (T.Cons t T.Nil)
+data Python t
+  = Noop
+  | Iff t t t
+  | Bool Bool
+  | String Text
+  | Throw t
+  | Let Name t t
+  | t :>> t
+  | Import (NonEmpty Text)
+  | Function Name [Name] t
+  | Call t [t]
+  | Locate Span t
+  deriving (Eq, Foldable, Functor, Ord, Show, Traversable)
 
 infixl 1 :>>
 
-pattern Import :: NonEmpty Text -> T.Term Python v
-pattern Import i = Import' i T.:$: T.Nil
-
-pattern Function :: Name -> [Name] -> T.Term Python v -> T.Term Python v
-pattern Function n as b = Function' n as T.:$: T.Cons b T.Nil
-
-pattern Call
-  :: T.Term Python v
-  -> [T.Term Python v]
-  -> T.Term Python v
-pattern Call f as <- Call' T.:$: T.Cons f (T.Cons (fromArgs -> as) T.Nil)
-  where Call f as = Call' T.:$: T.Cons f (T.Cons (foldr ACons ANil as) T.Nil)
-
-fromArgs :: T.Term Python v -> [T.Term Python v]
-fromArgs = \case
-  ANil -> []
-  ACons a as -> a:fromArgs as
-  _ -> fail "unexpected constructor in spine of argument list"
-
-pattern ANil :: T.Term Python v
-pattern ANil = ANil' T.:$: T.Nil
-
-pattern ACons :: T.Term Python v -> T.Term Python v -> T.Term Python v
-pattern ACons a as = ACons' T.:$: T.Cons a (T.Cons as T.Nil)
-
-pattern Locate :: Span -> T.Term Python v -> T.Term Python v
-pattern Locate s t = Locate' s T.:$: T.Cons t T.Nil
-
-{-# COMPLETE Noop, Iff, Bool, String, Throw, Let, (:>>), Import, Function, Call, Locate #-}
-
-
-instance Eq1 Python where
-  liftEq _ a b = case (a, b) of
-    (Noop', Noop')                       -> True
-    (Iff', Iff')                         -> True
-    (Bool' b1, Bool' b2)                 -> b1 == b2
-    (String' s1, String' s2)             -> s1 == s2
-    (Throw', Throw')                     -> True
-    (Let' n1, Let' n2)                   -> n1 == n2
-    ((:>>>), (:>>>))                     -> True
-    (Import' i1, Import' i2)             -> i1 == i2
-    (Function' n1 as1, Function' n2 as2) -> n1 == n2 && as1 == as2
-    (Call', Call')                       -> True
-    (ANil', ANil')                       -> True
-    (ACons', ACons')                     -> True
-    (Locate' s1, Locate' s2)             -> s1 == s2
-    _                                    -> False
-
-instance Ord1 Python where
-  liftCompare _ a b = case (a, b) of
-    (Noop', Noop')                       -> EQ
-    (Noop', _)                           -> LT
-    (Iff', Iff')                         -> EQ
-    (Iff', _)                            -> LT
-    (Bool' b1,  Bool' b2)                -> compare b1 b2
-    (Bool' _,  _)                        -> LT
-    (String' s1, String' s2)             -> compare s1 s2
-    (String' _, _)                       -> LT
-    (Throw', Throw')                     -> EQ
-    (Throw', _)                          -> LT
-    (Let' n1, Let' n2)                   -> compare n1 n2
-    (Let' _, _)                          -> LT
-    ((:>>>), (:>>>))                     -> EQ
-    ((:>>>), _)                          -> LT
-    (Import' i1, Import' i2)             -> compare i1 i2
-    (Import' _, _)                       -> LT
-    (Function' n1 as1, Function' n2 as2) -> compare n1 n2 <> compare as1 as2
-    (Function' _ _, _)                   -> LT
-    (Call', Call')                       -> EQ
-    (Call', _)                           -> LT
-    (ANil', ANil')                       -> EQ
-    (ANil', _)                           -> LT
-    (ACons', ACons')                     -> EQ
-    (ACons', _)                          -> LT
-    (Locate' s1, Locate' s2)             -> compare s1 s2
-    (Locate' _, _)                       -> LT
-
 
 -- Abstract interpretation
 
@@ -170,27 +55,28 @@ eval
   => (Term -> m val)
   -> (Term -> m val)
 eval eval = \case
-  T.Var n   -> lookupEnv n >>= maybe (dvar n) fetch
-  Noop      -> dunit
-  Iff c t e -> do
-    c' <- eval c
-    dif c' (eval t) (eval e)
-  Bool b    -> dbool b
-  String s  -> dstring s
-  Throw e   -> eval e >>= ddie
-  Let n v b -> do
-    v' <- eval v
-    let' n v' (eval b)
-  t :>> u   -> do
-    t' <- eval t
-    u' <- eval u
-    t' >>> u'
-  Import ns -> S.simport ns >> dunit
-  Function n ps b -> letrec n (dabs ps (foldr (\ (p, a) m -> let' p a m) (eval b) . zip ps))
-  Call f as -> do
-    f' <- eval f
-    as' <- traverse eval as
-    dapp f' as'
-  Locate s t -> local (setSpan s) (eval t)
+  T.Var n  -> lookupEnv n >>= maybe (dvar n) fetch
+  T.Term s -> case s of
+    Noop      -> dunit
+    Iff c t e -> do
+      c' <- eval c
+      dif c' (eval t) (eval e)
+    Bool b    -> dbool b
+    String s  -> dstring s
+    Throw e   -> eval e >>= ddie
+    Let n v b -> do
+      v' <- eval v
+      let' n v' (eval b)
+    t :>> u   -> do
+      t' <- eval t
+      u' <- eval u
+      t' >>> u'
+    Import ns -> S.simport ns >> dunit
+    Function n ps b -> letrec n (dabs ps (foldr (\ (p, a) m -> let' p a m) (eval b) . zip ps))
+    Call f as -> do
+      f' <- eval f
+      as' <- traverse eval as
+      dapp f' as'
+    Locate s t -> local (setSpan s) (eval t)
   where
   setSpan s r = r{ refSpan = s }

From ff22c0bd97ac28a27acd0b26d0a780a0f8843d09 Mon Sep 17 00:00:00 2001
From: Rob Rix <robrix@github.com>
Date: Tue, 19 Mar 2024 13:35:58 -0400
Subject: [PATCH 50/59] General fold over Terms.

---
 semantic-analysis/src/Analysis/Syntax.hs | 7 +++++++
 1 file changed, 7 insertions(+)

diff --git a/semantic-analysis/src/Analysis/Syntax.hs b/semantic-analysis/src/Analysis/Syntax.hs
index ebe36b7f40..8c6c52fa33 100644
--- a/semantic-analysis/src/Analysis/Syntax.hs
+++ b/semantic-analysis/src/Analysis/Syntax.hs
@@ -3,6 +3,7 @@ module Analysis.Syntax
 ( -- * Syntax
   Term(..)
 , subterms
+, foldTerm
 ) where
 
 import qualified Data.Set as Set
@@ -30,3 +31,9 @@ subterms :: (forall t . Eq t => Eq (sig t), forall t . Ord t => Ord (sig t), Ord
 subterms t = case t of
   Var _  -> Set.singleton t
   Term s -> Set.insert t (foldMap subterms s)
+
+foldTerm :: Functor sig => (v -> r) -> (sig r -> r) -> (Term sig v -> r)
+foldTerm var sig = go
+  where
+  go (Var v)  = var v
+  go (Term s) = sig (go <$> s)

From 3861c3889eef9a9374d3d3f2843fbe64e8609910 Mon Sep 17 00:00:00 2001
From: Rob Rix <robrix@github.com>
Date: Tue, 19 Mar 2024 13:46:16 -0400
Subject: [PATCH 51/59] Paramorphic fold.

---
 semantic-analysis/src/Analysis/Syntax.hs | 7 +++++++
 1 file changed, 7 insertions(+)

diff --git a/semantic-analysis/src/Analysis/Syntax.hs b/semantic-analysis/src/Analysis/Syntax.hs
index 8c6c52fa33..7757cabacb 100644
--- a/semantic-analysis/src/Analysis/Syntax.hs
+++ b/semantic-analysis/src/Analysis/Syntax.hs
@@ -4,6 +4,7 @@ module Analysis.Syntax
   Term(..)
 , subterms
 , foldTerm
+, paraTerm
 ) where
 
 import qualified Data.Set as Set
@@ -37,3 +38,9 @@ foldTerm var sig = go
   where
   go (Var v)  = var v
   go (Term s) = sig (go <$> s)
+
+paraTerm :: Functor sig => (v -> r) -> (sig (Term sig v, r) -> r) -> (Term sig v -> r)
+paraTerm var sig = go
+  where
+  go (Var v)  = var v
+  go (Term s) = sig ((,) <*> go <$> s)

From 050188ffcf9b8ec323940020eee678a63a787494 Mon Sep 17 00:00:00 2001
From: Rob Rix <robrix@github.com>
Date: Tue, 19 Mar 2024 14:42:10 -0400
Subject: [PATCH 52/59] Define subterms paramorphically.

---
 semantic-analysis/src/Analysis/Syntax.hs | 6 ++----
 1 file changed, 2 insertions(+), 4 deletions(-)

diff --git a/semantic-analysis/src/Analysis/Syntax.hs b/semantic-analysis/src/Analysis/Syntax.hs
index 7757cabacb..d2c4624aa2 100644
--- a/semantic-analysis/src/Analysis/Syntax.hs
+++ b/semantic-analysis/src/Analysis/Syntax.hs
@@ -28,10 +28,8 @@ instance (forall t . Eq t => Eq (sig t), forall t. Ord t => Ord (sig t), Ord v)
   compare _          _        = GT
 
 
-subterms :: (forall t . Eq t => Eq (sig t), forall t . Ord t => Ord (sig t), Ord v, Foldable sig) => Term sig v -> Set.Set (Term sig v)
-subterms t = case t of
-  Var _  -> Set.singleton t
-  Term s -> Set.insert t (foldMap subterms s)
+subterms :: (forall t . Eq t => Eq (sig t), forall t . Ord t => Ord (sig t), Ord v, Foldable sig, Functor sig) => Term sig v -> Set.Set (Term sig v)
+subterms = paraTerm (Set.singleton . Var) (foldMap (uncurry Set.insert))
 
 foldTerm :: Functor sig => (v -> r) -> (sig r -> r) -> (Term sig v -> r)
 foldTerm var sig = go

From c746f937705e7859506b6658379e3a561f21fde3 Mon Sep 17 00:00:00 2001
From: Rob Rix <robrix@github.com>
Date: Tue, 19 Mar 2024 14:45:20 -0400
Subject: [PATCH 53/59] Mendler-style recursion.

---
 semantic-analysis/src/Analysis/Syntax.hs | 8 ++++++++
 1 file changed, 8 insertions(+)

diff --git a/semantic-analysis/src/Analysis/Syntax.hs b/semantic-analysis/src/Analysis/Syntax.hs
index d2c4624aa2..2fb0112f90 100644
--- a/semantic-analysis/src/Analysis/Syntax.hs
+++ b/semantic-analysis/src/Analysis/Syntax.hs
@@ -1,10 +1,12 @@
 {-# LANGUAGE QuantifiedConstraints #-}
+{-# LANGUAGE RankNTypes #-}
 module Analysis.Syntax
 ( -- * Syntax
   Term(..)
 , subterms
 , foldTerm
 , paraTerm
+, mendlerTerm
 ) where
 
 import qualified Data.Set as Set
@@ -42,3 +44,9 @@ paraTerm var sig = go
   where
   go (Var v)  = var v
   go (Term s) = sig ((,) <*> go <$> s)
+
+mendlerTerm :: (v -> r) -> (forall r' . (r' -> r) -> sig r'-> r) -> (Term sig v -> r)
+mendlerTerm var sig = go
+  where
+  go (Var v)  = var v
+  go (Term s) = sig go s

From bcca57af9ca1c3fce84c9b09ced40e0bfadecdfb Mon Sep 17 00:00:00 2001
From: Rob Rix <robrix@github.com>
Date: Tue, 19 Mar 2024 14:46:43 -0400
Subject: [PATCH 54/59] Align.

---
 semantic-analysis/src/Analysis/Syntax.hs | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/semantic-analysis/src/Analysis/Syntax.hs b/semantic-analysis/src/Analysis/Syntax.hs
index 2fb0112f90..fecd21b32c 100644
--- a/semantic-analysis/src/Analysis/Syntax.hs
+++ b/semantic-analysis/src/Analysis/Syntax.hs
@@ -19,9 +19,9 @@ data Term sig v
   | Term (sig (Term sig v))
 
 instance (forall t . Eq t => Eq (sig t), Eq v) => Eq (Term sig v) where
-  Var v1   == Var v2 = v1 == v2
+  Var v1  == Var v2  = v1 == v2
   Term s1 == Term s2 = s1 == s2
-  _        == _      = False
+  _       == _       = False
 
 instance (forall t . Eq t => Eq (sig t), forall t. Ord t => Ord (sig t), Ord v) => Ord (Term sig v) where
   compare (Var v1)  (Var v2)  = compare v1 v2

From 07a5740e910100f912f3a8d766b4f25b80f93dce Mon Sep 17 00:00:00 2001
From: Rob Rix <robrix@github.com>
Date: Tue, 19 Mar 2024 14:50:45 -0400
Subject: [PATCH 55/59] Define foldTerm using mendlerTerm.

---
 semantic-analysis/src/Analysis/Syntax.hs | 5 +----
 1 file changed, 1 insertion(+), 4 deletions(-)

diff --git a/semantic-analysis/src/Analysis/Syntax.hs b/semantic-analysis/src/Analysis/Syntax.hs
index fecd21b32c..458ee663b2 100644
--- a/semantic-analysis/src/Analysis/Syntax.hs
+++ b/semantic-analysis/src/Analysis/Syntax.hs
@@ -34,10 +34,7 @@ subterms :: (forall t . Eq t => Eq (sig t), forall t . Ord t => Ord (sig t), Ord
 subterms = paraTerm (Set.singleton . Var) (foldMap (uncurry Set.insert))
 
 foldTerm :: Functor sig => (v -> r) -> (sig r -> r) -> (Term sig v -> r)
-foldTerm var sig = go
-  where
-  go (Var v)  = var v
-  go (Term s) = sig (go <$> s)
+foldTerm var sig = mendlerTerm var (\ k -> sig . fmap k)
 
 paraTerm :: Functor sig => (v -> r) -> (sig (Term sig v, r) -> r) -> (Term sig v -> r)
 paraTerm var sig = go

From 809ab74d192ded23bdc50b176ad8fae49d8232f2 Mon Sep 17 00:00:00 2001
From: Rob Rix <robrix@github.com>
Date: Tue, 19 Mar 2024 14:55:18 -0400
Subject: [PATCH 56/59] UndecidableInstances instead of QuantifiedConstraints.

I'd rather do this than fuss with CI for old versions of the compiler.
---
 semantic-analysis/src/Analysis/Syntax.hs | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/semantic-analysis/src/Analysis/Syntax.hs b/semantic-analysis/src/Analysis/Syntax.hs
index 458ee663b2..6e1f15abc7 100644
--- a/semantic-analysis/src/Analysis/Syntax.hs
+++ b/semantic-analysis/src/Analysis/Syntax.hs
@@ -1,5 +1,5 @@
-{-# LANGUAGE QuantifiedConstraints #-}
 {-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE UndecidableInstances #-}
 module Analysis.Syntax
 ( -- * Syntax
   Term(..)
@@ -18,19 +18,19 @@ data Term sig v
   = Var v
   | Term (sig (Term sig v))
 
-instance (forall t . Eq t => Eq (sig t), Eq v) => Eq (Term sig v) where
+instance (Eq (sig (Term sig v)), Eq v) => Eq (Term sig v) where
   Var v1  == Var v2  = v1 == v2
   Term s1 == Term s2 = s1 == s2
   _       == _       = False
 
-instance (forall t . Eq t => Eq (sig t), forall t. Ord t => Ord (sig t), Ord v) => Ord (Term sig v) where
+instance (Ord (sig (Term sig v)), Ord v) => Ord (Term sig v) where
   compare (Var v1)  (Var v2)  = compare v1 v2
   compare (Var _)   _         = LT
   compare (Term s1) (Term s2) = compare s1 s2
   compare _          _        = GT
 
 
-subterms :: (forall t . Eq t => Eq (sig t), forall t . Ord t => Ord (sig t), Ord v, Foldable sig, Functor sig) => Term sig v -> Set.Set (Term sig v)
+subterms :: (Ord (sig (Term sig v)), Ord v, Foldable sig, Functor sig) => Term sig v -> Set.Set (Term sig v)
 subterms = paraTerm (Set.singleton . Var) (foldMap (uncurry Set.insert))
 
 foldTerm :: Functor sig => (v -> r) -> (sig r -> r) -> (Term sig v -> r)

From d22bd1e603f74187c5bf57c562b3f851a6031b3d Mon Sep 17 00:00:00 2001
From: Rob Rix <robrix@github.com>
Date: Tue, 19 Mar 2024 14:58:02 -0400
Subject: [PATCH 57/59] Mendler-style paramorphism.

---
 semantic-analysis/src/Analysis/Syntax.hs | 7 +++++++
 1 file changed, 7 insertions(+)

diff --git a/semantic-analysis/src/Analysis/Syntax.hs b/semantic-analysis/src/Analysis/Syntax.hs
index 6e1f15abc7..bd9011fb35 100644
--- a/semantic-analysis/src/Analysis/Syntax.hs
+++ b/semantic-analysis/src/Analysis/Syntax.hs
@@ -7,6 +7,7 @@ module Analysis.Syntax
 , foldTerm
 , paraTerm
 , mendlerTerm
+, mendlerParaTerm
 ) where
 
 import qualified Data.Set as Set
@@ -47,3 +48,9 @@ mendlerTerm var sig = go
   where
   go (Var v)  = var v
   go (Term s) = sig go s
+
+mendlerParaTerm :: (v -> r) -> (forall r' . (r' -> (Term sig v, r)) -> sig r'-> r) -> (Term sig v -> r)
+mendlerParaTerm var sig = go
+  where
+  go (Var v)  = var v
+  go (Term s) = sig ((,) <*> go) s

From ad4dba658fe305b5ff7c55fb2b569cff7957ed0c Mon Sep 17 00:00:00 2001
From: Rob Rix <robrix@github.com>
Date: Tue, 19 Mar 2024 15:00:15 -0400
Subject: [PATCH 58/59] Define para using mendlerPara.

---
 semantic-analysis/src/Analysis/Syntax.hs | 5 +----
 1 file changed, 1 insertion(+), 4 deletions(-)

diff --git a/semantic-analysis/src/Analysis/Syntax.hs b/semantic-analysis/src/Analysis/Syntax.hs
index bd9011fb35..f0576259d2 100644
--- a/semantic-analysis/src/Analysis/Syntax.hs
+++ b/semantic-analysis/src/Analysis/Syntax.hs
@@ -38,10 +38,7 @@ foldTerm :: Functor sig => (v -> r) -> (sig r -> r) -> (Term sig v -> r)
 foldTerm var sig = mendlerTerm var (\ k -> sig . fmap k)
 
 paraTerm :: Functor sig => (v -> r) -> (sig (Term sig v, r) -> r) -> (Term sig v -> r)
-paraTerm var sig = go
-  where
-  go (Var v)  = var v
-  go (Term s) = sig ((,) <*> go <$> s)
+paraTerm var sig = mendlerParaTerm var (\ k -> sig . fmap k)
 
 mendlerTerm :: (v -> r) -> (forall r' . (r' -> r) -> sig r'-> r) -> (Term sig v -> r)
 mendlerTerm var sig = go

From 1d70d130a0a7be40164cd0d3e8a464801ff63e1f Mon Sep 17 00:00:00 2001
From: Rob Rix <robrix@github.com>
Date: Tue, 19 Mar 2024 15:01:07 -0400
Subject: [PATCH 59/59] Define subterms using mendlerPara.

:fire: that Functor constraint.
---
 semantic-analysis/src/Analysis/Syntax.hs | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/semantic-analysis/src/Analysis/Syntax.hs b/semantic-analysis/src/Analysis/Syntax.hs
index f0576259d2..35c3c4eead 100644
--- a/semantic-analysis/src/Analysis/Syntax.hs
+++ b/semantic-analysis/src/Analysis/Syntax.hs
@@ -31,8 +31,8 @@ instance (Ord (sig (Term sig v)), Ord v) => Ord (Term sig v) where
   compare _          _        = GT
 
 
-subterms :: (Ord (sig (Term sig v)), Ord v, Foldable sig, Functor sig) => Term sig v -> Set.Set (Term sig v)
-subterms = paraTerm (Set.singleton . Var) (foldMap (uncurry Set.insert))
+subterms :: (Ord (sig (Term sig v)), Ord v, Foldable sig) => Term sig v -> Set.Set (Term sig v)
+subterms = mendlerParaTerm (Set.singleton . Var) (\ k -> foldMap (uncurry Set.insert . k))
 
 foldTerm :: Functor sig => (v -> r) -> (sig r -> r) -> (Term sig v -> r)
 foldTerm var sig = mendlerTerm var (\ k -> sig . fmap k)