path: root/source/Felix/Meaning.hs

{-# LANGUAGE ApplicativeDo #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE NoImplicitPrelude #-}
{-# LANGUAGE MultiWayIf #-}
{-# LANGUAGE TupleSections #-}


module Felix.Meaning where


import Base
import Felix.Syntax.Abstract (Sign(..))
import Felix.Syntax.Abstract qualified as Raw
import Felix.Syntax.Internal (VarSymbol(..), pattern FreshVar)
import Felix.Syntax.Internal qualified as Sem
import Felix.Syntax.LexicalPhrase (unsafeReadPhrase)
import Felix.Report.Location

import Bound
import Control.Monad.Except
import Control.Monad.State
import Data.List qualified as List
import Data.List.NonEmpty qualified as NonEmpty
import Data.Map qualified as Map
import Data.Set qualified as Set
import Control.Exception (Exception)


-- | The 'Gloss' monad. Basic elaboration, desugaring, and validation
-- computations take place in this monad, using 'ExceptT' to log
-- validation errors and 'State' to keep track of the surrounding context.
type Gloss = ExceptT GlossError (State GlossState)
-- This monad previously used 'ValidationT' for validation so that multiple
-- validation errors could be reported. Using only 'ExceptT' we fail immediately
-- on the first error. If we ever swich back to 'ValidateT' for error reporting,
-- then we should re-enable {-# OPTIONS_GHC -foptimal-applicative-do #-},
-- as 'ValidateT' can report more errors when used with applicative combinators.

-- These types are a private bridge to the current VarSymbol-based core.
newtype LocalId = LocalId Int
    deriving (Show, Eq, Ord)

data BinderTrivia = BinderTrivia
    { binderDisplayHint :: Maybe Text
    , binderDeclarationLocation :: Location
    } deriving (Show, Eq, Ord)

data ResolvedLocalRef
    = AmbientRef VarSymbol
    | LocalRef LocalId
    deriving (Show, Eq, Ord)

data H0ResolvedBinder = H0ResolvedBinder
    { h0BinderId :: LocalId
    , h0BinderTrivia :: BinderTrivia
    } deriving (Show, Eq, Ord)

data ResolvedBinderAdapterError
    = UnknownResolvedLocal LocalId
    | DuplicateResolvedLocalAssignment LocalId
    | ResolvedLocalTokenCollision LocalId VarSymbol
    deriving (Show, Eq, Ord)

-- | Errors that can be detected during glossing.
data GlossError
    = GlossDefnError Location DefnError Sem.Marker
    | GlossInductionError Location
    | GlossRelationExprWithParams Location
    | GlossRelationApplicationError Sem.RelationApplicationError
    | GlossDatatypeHeadError Location
    | GlossDatatypeClauseTargetError Location
    | GlossDatatypeConstructorError Location
    | DependentReplacementDomainNotSupported Location
    | QuantifiedTermRequiresResolvedContext Location
    | IotaTermNotSupported Location
    | DefiniteFunctionAssumptionNotSupported Location
    | GlossProofFunctionArgumentMismatch
        Location
        VarSymbol
        VarSymbol
    | GlossProofFunctionNameMismatch
        Location
        VarSymbol
        VarSymbol
    | GlossAbbreviationError
        Location
        Sem.Marker
        AbbreviationParameterError
    | DuplicateQuantifiedNounBinder
        Location
        Location
        Text
    | GlossResolvedBinderAdapterError
        Location
        ResolvedBinderAdapterError
    deriving (Eq, Ord)

data AbbreviationParameterError
    = DuplicateAbbreviationParameters (NonEmpty VarSymbol)
    | FreeAbbreviationBodyVariables (NonEmpty VarSymbol)
    deriving (Show, Eq, Ord)

instance Exception GlossError
instance Show GlossError where show = explainGlossError

explainGlossError :: GlossError -> String
explainGlossError = \case
    GlossDefnError loc defnError marker ->
        "Definition error at " <> prettyLocation loc <> " (in " <> show marker <> "): " <> case defnError of
            DefnWarnLhsFree xs ->
                "The variables " <> show xs <> " in the pattern being defined (definiendum) do not occur in the body of the definition (definiens). Remove them or use them in the body."
            DefnErrorLhsNotLinear ->
                "The left-hand side of the definition is not linear (a variable occurs multiple times)."
            DefnErrorLhsTypeFree ->
                "The defintion contains variables with no typing constraints or assumptions placed on them."
            DefnErrorRhsFree xs ->
                "The variables " <> show xs <> " on the right-hand side of the definition do not occurring on the left-hand side."
            DefnErrorQuantifiedRhsTerm ->
                "A quantified term cannot be the right-hand side of a functional definition."
    GlossInductionError loc ->
        "Error at " <> prettyLocation loc <> ": Induction over a non-variable is not supported."
    GlossRelationExprWithParams loc ->
        "Error at " <> prettyLocation loc <> ": A relation defined by an expression cannot have parameters."
    GlossRelationApplicationError
        (Sem.RelationParameterArityMismatch loc relation expected actual) ->
        "Relation "
            <> show (Sem.relationSymbolToken relation)
            <> " at "
            <> prettyLocation loc
            <> " expects "
            <> show (Sem.parameterArityValue expected)
            <> " parameter(s), but received "
            <> show (Sem.parameterArityValue actual)
            <> "."
    GlossDatatypeHeadError loc ->
        "Error at " <> prettyLocation loc <> ": A datatype head must be a constant symbolic term."
    GlossDatatypeClauseTargetError loc ->
        "Error at " <> prettyLocation loc <> ": Every datatype clause must target the datatype being defined."
    GlossDatatypeConstructorError loc ->
        "Error at " <> prettyLocation loc <> ": Datatype constructors must be symbolic terms with bare variable arguments."
    DependentReplacementDomainNotSupported loc ->
        "Error at "
            <> prettyLocation loc
            <> ": dependent replacement domains are not yet supported."
    QuantifiedTermRequiresResolvedContext loc ->
        "Error at "
            <> prettyLocation loc
            <> ": a quantified term requires a resolved binding context."
    IotaTermNotSupported loc ->
        "Error at "
            <> prettyLocation loc
            <> ": definite-description terms are not supported."
    DefiniteFunctionAssumptionNotSupported loc ->
        "Error at "
            <> prettyLocation loc
            <> ": definite-function assumptions are not supported."
    GlossProofFunctionArgumentMismatch loc valueArgument domainArgument ->
        "Function definition error at "
            <> prettyLocation loc
            <> ": value argument "
            <> show valueArgument
            <> " does not match domain argument "
            <> show domainArgument
            <> "."
    GlossProofFunctionNameMismatch loc declaredFunction definedFunction ->
        "Function definition error at "
            <> prettyLocation loc
            <> ": declared function "
            <> show declaredFunction
            <> " does not match defined function "
            <> show definedFunction
            <> "."
    GlossAbbreviationError loc marker abbreviationError ->
        "Abbreviation error at "
            <> prettyLocation loc
            <> " (in "
            <> show marker
            <> "): "
            <> case abbreviationError of
                DuplicateAbbreviationParameters variables ->
                    "The parameters "
                        <> show (NonEmpty.toList variables)
                        <> " occur more than once."
                FreeAbbreviationBodyVariables variables ->
                    "The body contains free variables not present in the head: "
                        <> show (NonEmpty.toList variables)
                        <> "."
    DuplicateQuantifiedNounBinder firstLocation secondLocation name ->
        "Quantified noun binder "
            <> show name
            <> " at "
            <> prettyLocation secondLocation
            <> " duplicates the overlapping binder at "
            <> prettyLocation firstLocation
            <> "."
    GlossResolvedBinderAdapterError location adapterError ->
        "Resolved binder adapter error at "
            <> prettyLocation location
            <> ": "
            <> case adapterError of
                UnknownResolvedLocal localId ->
                    "unknown local reference " <> show localId <> "."
                DuplicateResolvedLocalAssignment localId ->
                    "duplicate legacy assignment for " <> show localId <> "."
                ResolvedLocalTokenCollision localId token ->
                    "legacy token "
                        <> show token
                        <> " for "
                        <> show localId
                        <> " is not fresh."

liftRelationApplication
    :: Either Sem.RelationApplicationError a
    -> Gloss a
liftRelationApplication =
    either (throwError . GlossRelationApplicationError) pure

-- | Specialization of 'traverse' to 'Gloss'.
each :: (Traversable t) => (a -> Gloss b) -> t a -> Gloss (t b)
explain `each` as = traverse explain as
infix 7 `each` -- In particular, 'each' has precedence over '(<$>)'.

-- | Wellformedness check for definitions.
-- The following conditions need to be met.
--
-- * Variables occurring in the lexical phrases on the left side must be linear,
--   i.e. each variable can only occur once.
-- * The arguments of the lexical phrases must be variables, not complex terms.
--   This is statically guaranteed by the grammar.
-- * The optional typing noun may not have any free variables.
-- * The rhs side may not have any free variables not occurring on the lhs.
-- * If a variable on the lhs does not occur on the rhs, a warning should we issued.
--
isWellformedDefn :: Sem.Defn -> Either DefnError Sem.Defn
isWellformedDefn defn =
    if  | ls' /= ls -> Left DefnErrorLhsNotLinear
        | not (null rdiff) -> Left (DefnErrorRhsFree (toList rdiff))
        | not (null ldiff) -> case defn of
            Sem.DefnPredicate{} -> Left (DefnWarnLhsFree (toList ldiff))
            _ -> Right defn
        | otherwise -> Right defn
    where
        ls = lhsVars defn
        ls' = nubOrd ls
        rs = rhsVars defn
        (ldiff, rdiff) = symmetricDifferenceDecompose (Set.fromList ls') rs


lhsVars :: Sem.Defn -> [VarSymbol]
lhsVars = \case
    Sem.DefnPredicate _ _ vs _ -> toList vs
    Sem.DefnFun _ _ vs _ -> vs
    Sem.DefnOp _ vs _ -> vs

rhsVars :: Sem.Defn -> Set VarSymbol
rhsVars = \case
    Sem.DefnPredicate _ _ _ f -> Sem.freeVars f
    Sem.DefnFun _ _ _ e -> Sem.freeVars e
    Sem.DefnOp _ _ e -> Sem.freeVars e


-- | Validation errors for top-level definitions.
data DefnError
    = DefnWarnLhsFree [VarSymbol]
    | DefnErrorLhsNotLinear
    | DefnErrorLhsTypeFree
    | DefnErrorRhsFree [VarSymbol]
    | DefnErrorQuantifiedRhsTerm
    deriving (Show, Eq, Ord)


-- | Context for 'Gloss' computations.
data GlossState = GlossState
    { varCount :: Int
    -- ^ Counter for generating variables names for the output.
    , localCount :: Int
    -- ^ Counter for resolved quantified-noun binders.
    , localBinderTrivia :: Map LocalId BinderTrivia
    , legacyLocalTokens :: Map LocalId VarSymbol
    } deriving (Show, Eq)

freshVar :: Gloss VarSymbol
freshVar = do
    i <- gets varCount
    modify $ \s -> s {varCount = varCount s + 1}
    pure $ FreshVar i

type H0LexicalEnvironment = [H0ResolvedBinder]

type H0Expr = Sem.ExprOf ResolvedLocalRef

freshH0Binder
    :: Location
    -> Maybe VarSymbol
    -> Gloss H0ResolvedBinder
freshH0Binder termLocation writtenName = do
    nextLocal <- gets localCount
    let localId = LocalId nextLocal
        trivia = BinderTrivia
            { binderDisplayHint = writtenName >>= displayedVariableName
            , binderDeclarationLocation =
                maybe termLocation locate writtenName
            }
        binder = H0ResolvedBinder localId trivia
    modify \glossState ->
        glossState
            { localCount = nextLocal + 1
            , localBinderTrivia =
                Map.insert localId trivia (localBinderTrivia glossState)
            }
    pure binder
  where
    displayedVariableName = \case
        NamedVarAt _ name -> Just name
        FreshVarAt{} -> Nothing

pushH0Binder
    :: H0ResolvedBinder
    -> H0LexicalEnvironment
    -> H0LexicalEnvironment
pushH0Binder = (:)

resolveH0Reference
    :: H0LexicalEnvironment
    -> VarSymbol
    -> ResolvedLocalRef
resolveH0Reference environment variable = case variable of
    NamedVarAt _ name ->
        maybe
            (AmbientRef variable)
            (LocalRef . h0BinderId)
            (List.find hasDisplayName environment)
      where
        hasDisplayName binder =
            binderDisplayHint (h0BinderTrivia binder) == Just name
    FreshVarAt{} ->
        AmbientRef variable

resolveH0Expr
    :: H0LexicalEnvironment
    -> Sem.Expr
    -> H0Expr
resolveH0Expr environment =
    fmap (resolveH0Reference environment)

lowerH0Expr :: H0Expr -> Gloss Sem.Expr
lowerH0Expr =
    traverse \case
        AmbientRef variable ->
            pure variable
        LocalRef localId -> do
            trivia <- gets (Map.lookup localId . localBinderTrivia)
            throwError
                (GlossResolvedBinderAdapterError
                    (maybe Nowhere binderDeclarationLocation trivia)
                    (UnknownResolvedLocal localId))

abstractH0Binder
    :: H0ResolvedBinder
    -> H0Expr
    -> Gloss (Scope VarSymbol Sem.ExprOf ResolvedLocalRef)
abstractH0Binder binder body = do
    token <- allocateLegacyLocalToken binder body
    pure
        (abstract
            (\case
                LocalRef localId
                    | localId == h0BinderId binder ->
                        Just token
                _ ->
                    Nothing)
            body)

allocateLegacyLocalToken
    :: H0ResolvedBinder
    -> H0Expr
    -> Gloss VarSymbol
allocateLegacyLocalToken binder body = do
    assignments <- gets legacyLocalTokens
    case Map.lookup localId assignments of
        Just _ ->
            throwAdapterError
                (DuplicateResolvedLocalAssignment localId)
        Nothing -> do
            let ambientTokens =
                    Set.fromList
                        [ token
                        | AmbientRef token <- toList body
                        ]
                assignedTokens =
                    Set.fromList (Map.elems assignments)
                forbiddenTokens =
                    ambientTokens <> assignedTokens
            token <- freshTokenOutside forbiddenTokens
            if token `Set.member` forbiddenTokens
                then
                    throwAdapterError
                        (ResolvedLocalTokenCollision localId token)
                else do
                    modify \glossState ->
                        glossState
                            { legacyLocalTokens =
                                Map.insert
                                    localId
                                    token
                                    (legacyLocalTokens glossState)
                            }
                    pure token
  where
    localId = h0BinderId binder
    binderLocation =
        binderDeclarationLocation (h0BinderTrivia binder)
    throwAdapterError =
        throwError
            . GlossResolvedBinderAdapterError binderLocation

    freshTokenOutside forbidden = do
        candidate <- freshVar
        if candidate `Set.member` forbidden
            then freshTokenOutside forbidden
            else pure candidate

initialGlossState :: GlossState
initialGlossState = GlossState
    { varCount = 0
    , localCount = 0
    , localBinderTrivia = mempty
    , legacyLocalTokens = mempty
    }

glossStep :: GlossState -> Raw.Block -> Either GlossError (Sem.Block, GlossState)
glossStep glossState block = case runState (runExceptT (glossBlock block)) glossState of
    (Left err, _nextGlossState) -> Left err
    (Right glossedBlock, nextGlossState) -> Right (glossedBlock, nextGlossState)

meaning :: [Raw.Block] -> Either GlossError [Sem.Block]
meaning blocks = evalState (runExceptT (glossBlocks blocks)) initialGlossState

glossExpr :: Raw.Expr -> Gloss (Sem.ExprOf VarSymbol)
glossExpr = \case
    Raw.ExprVar v ->
        pure $ Sem.TermVar v
    Raw.ExprInteger loc n ->
        pure $ Sem.TermSymbol loc (Sem.SymbolInteger n) []
    Raw.ExprOp loc f es ->
        Sem.TermSymbol loc <$> pure (Sem.SymbolMixfix f) <*> (glossExpr `each` es)
    Raw.ExprStructOp _loc tok maybeLabel -> do
        maybeLabel' <- traverse glossExpr maybeLabel
        pure $ Sem.TermSymbolStruct tok maybeLabel'
    Raw.ExprSep _loc x t phi -> do
        t' <- glossExpr t
        phi' <- glossStmt phi
        pure (Sem.TermSep x t' (abstract1 x phi'))
    Raw.ExprReplacePred _loc y x xBound stmt -> do
        xBound' <- glossExpr xBound
        stmt' <- glossStmt stmt
        let toReplacementVar z = if
                | z == x -> Just Sem.ReplacementDomVar
                | z == y -> Just Sem.ReplacementRangeVar
                | otherwise -> Nothing
        let scope = abstract toReplacementVar stmt'
        pure (Sem.ReplacePred y x xBound' scope)
    Raw.ExprReplace _loc e bounds phi -> do
        e' <- glossExpr e
        bounds' <- glossReplaceBounds bounds
        let xs = fst <$> bounds'
        phi'' <- case phi of
            Just phi' -> glossStmt phi'
            Nothing -> pure Sem.Top
        let abstractBoundVars = abstract (\x -> List.find (== x) (toList xs))
        pure $ Sem.ReplaceFun bounds' (abstractBoundVars e') (abstractBoundVars phi'')
        where
            glossReplaceBounds
                :: NonEmpty (VarSymbol, Raw.Expr)
                -> Gloss (NonEmpty (VarSymbol, Sem.Term))
            glossReplaceBounds
                    ((firstBinder, firstDomain) :| remainingBounds) = do
                firstDomain' <- glossExpr firstDomain
                remainingBounds' <-
                    go (Set.singleton firstBinder) remainingBounds
                pure ((firstBinder, firstDomain') :| remainingBounds')
              where
                go
                    :: Set VarSymbol
                    -> [(VarSymbol, Raw.Expr)]
                    -> Gloss [(VarSymbol, Sem.Term)]
                go _precedingBinders [] = pure []
                go precedingBinders ((binder, domain) : laterBounds) = do
                    domain' <- glossExpr domain
                    -- Folding a glossed domain visits only free occurrences.
                    case List.find
                        (`Set.member` precedingBinders)
                        (toList domain') of
                        Just occurrence ->
                            throwError
                                (DependentReplacementDomainNotSupported
                                    (locate occurrence))
                        Nothing -> do
                            laterBounds' <-
                                go
                                    (Set.insert binder precedingBinders)
                                    laterBounds
                            pure ((binder, domain') : laterBounds')
    Raw.ExprFiniteSet loc es -> do
        es' <- glossExpr `each` es
        pure (Sem.finiteSet loc es')


glossFormula :: Raw.Formula -> Gloss (Sem.ExprOf VarSymbol)
glossFormula = \case
    Raw.FormulaChain ch ->
        glossChain ch
    Raw.Connected _loc conn phi psi ->
        glossConnective conn <*> glossFormula phi <*> glossFormula psi
    Raw.FormulaNeg loc f ->
        Sem.Not loc <$> glossFormula f
    Raw.FormulaPredicate loc predi _marker es ->
        Sem.Atomic loc <$> glossPrefixPredicate predi <*> glossExpr `each` toList es
    Raw.PropositionalConstant _loc c ->
        pure $ Sem.PropositionalConstant c
    Raw.FormulaQuantified _loc quantifier xs bound phi -> do
        bound' <- glossBound bound
        phi' <- glossFormula phi
        quantify <- glossQuantifier quantifier
        pure (quantify xs (bound' (toList xs)) phi')

glossChain :: Sem.Chain -> Gloss (Sem.ExprOf VarSymbol)
glossChain ch = Sem.makeConjunction <$> makeRels (conjuncts (splat ch))
    where
        -- | Separate each link of the chain into separate triples.
        splat :: Raw.Chain -> [(NonEmpty Raw.Expr, Sign, Raw.Relation, NonEmpty Raw.Expr)]
        splat = \case
            Raw.ChainBase es sign rel es'
                -> [(es, sign, rel, es')]
            Raw.ChainCons es sign rel ch'@(Raw.ChainBase es' _ _ _)
                -> (es, sign, rel, es') : splat ch'
            Raw.ChainCons es sign rel ch'@(Raw.ChainCons es' _ _ _)
                -> (es, sign, rel, es') : splat ch'

        -- | Take each triple and combine the lhs/rhs to make all the conjuncts.
        conjuncts :: [(NonEmpty Raw.Expr, Sign, Raw.Relation, NonEmpty Raw.Expr)] -> [(Sign, Raw.Relation, Raw.Expr, Raw.Expr)]
        conjuncts triples = do
            (e1s, sign, rel, e2s) <- triples
            e1 <- toList e1s
            e2 <- toList e2s
            pure (sign, rel, e1, e2)

        makeRels :: [(Sign, Raw.Relation, Raw.Expr, Raw.Expr)] -> Gloss [Sem.Formula]
        makeRels triples = for triples makeRel

        makeRel :: (Sign, Raw.Relation, Raw.Expr, Raw.Expr) -> Gloss Sem.Formula
        makeRel (sign, rel, e1, e2) = do
            e1' <- glossExpr e1
            e2' <- glossExpr e2
            case rel of
                Raw.Relation loc rel' params -> do
                    params' <- glossExpr `each` params
                    buildRelation <-
                        liftRelationApplication
                            (Sem.makeRelationApplication loc rel' params')
                    pure $ sign' loc $ buildRelation e1' e2'
                Raw.RelationExpr loc e -> do
                            e' <- glossExpr e
                            pure (sign' loc (Sem.IsElementOf loc (Sem.TermPair loc e1' e2') e'))
            where
                sign' = case sign of
                    Positive -> \_ -> id
                    Negative -> Sem.Not


glossPrefixPredicate :: Raw.PrefixPredicate -> Gloss Sem.Predicate
glossPrefixPredicate (Raw.PrefixPredicate symb _ar) = pure (Sem.PredicateSymbol symb)


glossNPNonEmpty :: Raw.NounPhrase NonEmpty -> Gloss (NonEmpty VarSymbol, Sem.Formula)
glossNPNonEmpty (Raw.NounPhrase leftAdjs noun vars rightAdjs maySuchThat) = do
    -- We interpret the noun as a predicate.
    noun' <- glossNoun noun
    -- Now we turn the noun and all its modifiers into statements.
    let typings = (\v' -> noun' (Sem.TermVar v')) <$> vars
    leftAdjs' <- forEach (toList vars) <$> glossAdjL `each` leftAdjs
    rightAdjs' <- forEach (toList vars) <$> glossAdjR `each` rightAdjs
    suchThat <- maybeToList <$> glossStmt `each` maySuchThat
    let constraints = toList typings <> leftAdjs' <> rightAdjs' <> suchThat
    pure (vars, Sem.makeConjunction constraints)


-- | If needed, we introduce a fresh variable to reduce this to the case @NounPhrase NonEmpty@.
glossNPList :: Raw.NounPhrase [] -> Gloss (NonEmpty VarSymbol, Sem.Formula)
glossNPList (Raw.NounPhrase leftAdjs noun vars rightAdjs maySuchThat) = do
    vars' <- case vars of
        [] -> (:| []) <$> freshVar
        v:vs -> pure (v :| vs)
    glossNPNonEmpty $ Raw.NounPhrase leftAdjs noun vars' rightAdjs maySuchThat

-- Returns a predicate for a term (the constraints) and the optional such-that clause.
-- We treat suchThat separately since multiple terms can share the same such-that clause.
glossNPMaybe ::  Raw.NounPhrase Maybe -> Gloss (Sem.Term -> Sem.Formula, Maybe Sem.Formula)
glossNPMaybe (Raw.NounPhrase leftAdjs noun mayVar rightAdjs maySuchThat) = do
    case mayVar of
        Nothing -> do
            glossNP leftAdjs noun rightAdjs maySuchThat
        Just v' -> do
            -- Next we desugar all the modifiers into statements.
            leftAdjs'    <- apply v' <$> glossAdjL `each` leftAdjs
            rightAdjs'   <- apply v' <$> glossAdjR `each` rightAdjs
            maySuchThat' <- glossStmt `each` maySuchThat
            let constraints = leftAdjs' <> rightAdjs'
            -- Finally we translate the noun itself.
            noun' <- glossNoun noun
            pure case constraints of
                [] -> (\t -> noun' t, maySuchThat')
                _  -> (\t -> noun' t `Sem.And` Sem.makeConjunction (eq t v' : constraints), maySuchThat')
            where
                eq t v = Sem.Equals Nowhere t (Sem.TermVar v)
                apply :: VarSymbol -> [Sem.Term -> Sem.Formula] -> [Sem.Formula]
                apply v stmts = [stmt (Sem.TermVar v) | stmt <- stmts]

-- | Gloss a noun without a variable name.
-- Returns a predicate for a term (the constraints) and the optional such-that clause.
-- We treat suchThat separately since multiple terms can share the same such-that clause.
glossNP :: [Raw.AdjL] -> Raw.Noun -> [Raw.AdjR] -> Maybe Raw.Stmt -> Gloss (Sem.Term -> Sem.ExprOf VarSymbol, Maybe Sem.Formula)
glossNP leftAdjs noun rightAdjs maySuchThat = do
    noun' <- glossNoun noun
    leftAdjs' <- glossAdjL `each` leftAdjs
    rightAdjs' <-  glossAdjR `each` rightAdjs
    maySuchThat' <- glossStmt `each` maySuchThat
    let constraints = [noun'] <> leftAdjs' <> rightAdjs'
    pure (\t -> Sem.makeConjunction (flap constraints t), maySuchThat')


-- | If we have a plural noun with multiple variables, then we need to desugar
-- adjectives to apply to each individual variable.
forEach :: Applicative t => t VarSymbol -> t (Sem.Term -> a) -> t a
forEach vs'' stmts = do
    v <- vs''
    stmt <- stmts
    pure $ stmt (Sem.TermVar v)


glossAdjL :: Raw.AdjL -> Gloss (Sem.Term -> Sem.Formula)
glossAdjL (Raw.AdjL loc pat es) = do
    (es', quantifies) <- unzip <$> glossTerm `each` es
    let quantify = compose $ reverse quantifies
    pure $ \t -> quantify $ Sem.FormulaAdj loc t pat es'


-- | Since we need to be able to remove negation in verb phrases,
-- we need to have 'Sem.Stmt' as the target. We do not yet have
-- the term representing the subject, hence the parameter 'Sem.Expr'.
glossAdjR :: Raw.AdjR -> Gloss (Sem.Term -> Sem.Formula)
glossAdjR = \case
    Raw.AdjR _loc pat [e] | pat == Raw.mkLexicalItem (unsafeReadPhrase "equal to ?") "eq" -> do
        (e', quantify) <- glossTerm e
        pure $ \t -> quantify $ Sem.Equals Nowhere t e'
    Raw.AdjR _loc pat es -> do
        (es', quantifies) <- unzip <$> glossTerm `each` es
        let quantify = compose $ reverse quantifies
        pure $ \t -> quantify $ Sem.FormulaAdj Nowhere t pat es'
    Raw.AttrRThat vp -> glossVP vp


glossAdj :: Raw.AdjOf Raw.Term -> Gloss (Sem.ExprOf VarSymbol -> Sem.Formula)
glossAdj adj = case adj of
    Raw.Adj loc pat [e] | pat == Raw.mkLexicalItem (unsafeReadPhrase "equal to ?") "eq" -> do
        (e', quantify) <- glossTerm e
        pure $ \t -> quantify $ Sem.Equals loc  t e'
    Raw.Adj loc pat es -> do
        (es', quantifies) <- unzip <$> glossTerm `each` es
        let quantify = compose $ reverse quantifies
        pure $ \t -> quantify $ Sem.FormulaAdj loc t pat es'

glossVP :: Raw.VerbPhrase -> Gloss (Sem.Term -> Sem.Formula)
glossVP = \case
    Raw.VPVerb verb -> glossVerb verb
    Raw.VPAdj adjs -> do
        mkAdjs <- glossAdj `each` toList adjs
        pure (\x -> Sem.makeConjunction [mkAdj x | mkAdj <- mkAdjs])
    Raw.VPVerbNot verb -> (Sem.Not Nowhere  .) <$> glossVerb verb
    Raw.VPAdjNot adjs -> (Sem.Not Nowhere .) <$> glossVP (Raw.VPAdj adjs)


glossVerb :: Raw.Verb -> Gloss (Sem.Term -> Sem.Formula)
glossVerb (Raw.Verb loc pat es) = do
    (es', quantifies) <- unzip <$> glossTerm `each` es
    let quantify = compose $ reverse quantifies
    pure $ \ t -> quantify $ Sem.FormulaVerb loc t pat es'


glossNoun :: Raw.Noun -> Gloss (Sem.Term -> Sem.Formula)
glossNoun (Raw.Noun loc pat es) = do
    (es', quantifies) <- unzip <$> glossTerm `each` es
    let quantify = compose $ reverse quantifies
    pure case Raw.sg (Raw.lexicalItemSgPlPhrase pat) of
        -- Everything is a set
        [Just (Sem.Word "set")] -> const Sem.Top
        _ -> \e' -> quantify (Sem.FormulaNoun loc e' pat es')


glossFun :: Raw.Fun -> Gloss (Sem.Term, Sem.Formula -> Sem.Formula)
glossFun (Raw.Fun loc phrase es) = do
    (es', quantifies) <- unzip <$> glossTerm `each` es
    let quantify = compose $ reverse quantifies
    pure (Sem.TermSymbol loc (Sem.SymbolFun phrase) es', quantify)


glossTerm :: Raw.Term -> Gloss (Sem.Term, Sem.Formula -> Sem.Formula)
glossTerm = \case
    Raw.TermExpr e ->
        (, id) <$> glossExpr e
    Raw.TermFun f ->
        glossFun f
    Raw.TermIota location _variable _statement ->
        rejectIotaTerm location
    Raw.TermQuantified _quantifier loc _nounPhrase ->
        throwError (QuantifiedTermRequiresResolvedContext loc)

rejectIotaTerm :: Location -> Gloss a
rejectIotaTerm =
    throwError . IotaTermNotSupported


data H0QuantifiedTerm = H0QuantifiedTerm
    { h0Quantifier :: Raw.Quantifier
    , h0QuantifiedBinder :: H0ResolvedBinder
    , h0QuantifiedConstraints :: [H0Expr]
    }

data H0TermPlan = H0TermPlan
    { h0TermExpression :: H0Expr
    , h0TermEnvironment :: H0LexicalEnvironment
    , h0TermQuantifiers :: [H0QuantifiedTerm]
    }

data H0TermsPlan = H0TermsPlan
    { h0TermExpressions :: [H0Expr]
    , h0TermsEnvironment :: H0LexicalEnvironment
    , h0TermsQuantifiers :: [H0QuantifiedTerm]
    }

glossH0Terms
    :: H0LexicalEnvironment
    -> [Raw.Term]
    -> Gloss H0TermsPlan
glossH0Terms initialEnvironment =
    go initialEnvironment mempty [] []
  where
    go environment _seenBinders expressions quantifiers [] =
        pure
            H0TermsPlan
                { h0TermExpressions = reverse expressions
                , h0TermsEnvironment = environment
                , h0TermsQuantifiers = reverse quantifiers
                }
    go environment seenBinders expressions quantifiers (term : terms) = do
        termPlan <- glossH0Term environment term
        nextSeenBinders <-
            foldM
                addSiblingBinder
                seenBinders
                (h0TermQuantifiers termPlan)
        go
            (h0TermEnvironment termPlan)
            nextSeenBinders
            (h0TermExpression termPlan : expressions)
            (reverse (h0TermQuantifiers termPlan) <> quantifiers)
            terms

    addSiblingBinder seenBinders quantifiedTerm =
        case binderDisplayHint binderTrivia of
            Nothing ->
                pure seenBinders
            Just displayName ->
                case Map.lookup displayName seenBinders of
                    Nothing ->
                        pure
                            (Map.insert
                                displayName
                                binderTrivia
                                seenBinders)
                    Just firstBinderTrivia ->
                        throwError
                            (DuplicateQuantifiedNounBinder
                                (binderDeclarationLocation
                                    firstBinderTrivia)
                                (binderDeclarationLocation
                                    binderTrivia)
                                displayName)
      where
        binderTrivia =
            h0BinderTrivia
                (h0QuantifiedBinder quantifiedTerm)

glossH0Term
    :: H0LexicalEnvironment
    -> Raw.Term
    -> Gloss H0TermPlan
glossH0Term environment = \case
    Raw.TermExpr expression -> do
        expression' <- resolveH0Expr environment <$> glossExpr expression
        pure
            H0TermPlan
                { h0TermExpression = expression'
                , h0TermEnvironment = environment
                , h0TermQuantifiers = []
                }
    Raw.TermFun (Raw.Fun location symbol arguments) -> do
        argumentsPlan <- glossH0Terms environment arguments
        pure
            H0TermPlan
                { h0TermExpression =
                    Sem.TermSymbol
                        location
                        (Sem.SymbolFun symbol)
                        (h0TermExpressions argumentsPlan)
                , h0TermEnvironment =
                    h0TermsEnvironment argumentsPlan
                , h0TermQuantifiers =
                    h0TermsQuantifiers argumentsPlan
                }
    Raw.TermIota location _variable _statement ->
        rejectIotaTerm location
    Raw.TermQuantified quantifier location nounPhrase -> do
        let writtenName = case nounPhrase of
                Raw.NounPhrase _ _ name _ _ -> name
        binder <- freshH0Binder location writtenName
        let nextEnvironment = pushH0Binder binder environment
            witness = Sem.TermVar (LocalRef (h0BinderId binder))
        constraints <-
            glossH0QuantifiedNoun
                nextEnvironment
                witness
                nounPhrase
        pure
            H0TermPlan
                { h0TermExpression = witness
                , h0TermEnvironment = nextEnvironment
                , h0TermQuantifiers =
                    [ H0QuantifiedTerm
                        { h0Quantifier = quantifier
                        , h0QuantifiedBinder = binder
                        , h0QuantifiedConstraints = constraints
                        }
                    ]
                }

applyH0Quantifiers
    :: [H0QuantifiedTerm]
    -> H0Expr
    -> Gloss H0Expr
applyH0Quantifiers quantifiers body =
    foldrM applyQuantifier body quantifiers
  where
    applyQuantifier quantifiedTerm continuation = do
        let constrainedBody =
                applyQuantifierConstraints
                    (h0Quantifier quantifiedTerm)
                    (h0QuantifiedConstraints quantifiedTerm)
                    continuation
        scope <-
            abstractH0Binder
                (h0QuantifiedBinder quantifiedTerm)
                constrainedBody
        pure case h0Quantifier quantifiedTerm of
            Raw.Universally ->
                Sem.Quantified Sem.Universally scope
            Raw.Existentially ->
                Sem.Quantified Sem.Existentially scope
            Raw.Nonexistentially ->
                Sem.Not
                    Nowhere
                    (Sem.Quantified Sem.Existentially scope)

glossH0QuantifiedNoun
    :: H0LexicalEnvironment
    -> H0Expr
    -> Raw.NounPhrase Maybe
    -> Gloss [H0Expr]
glossH0QuantifiedNoun
        environment
        witness
        (Raw.NounPhrase leftAdjectives noun _name rightAdjectives maySuchThat) = do
    nounConstraint <- glossH0Noun environment witness noun
    leftConstraints <-
        for leftAdjectives (glossH0AdjL environment witness)
    rightConstraints <-
        for rightAdjectives (glossH0AdjR environment witness)
    suchThatConstraint <-
        traverse (glossH0Stmt environment) maySuchThat
    pure
        ( maybeToList suchThatConstraint
            <> [ Sem.makeConjunction
                    ( nounConstraint
                        : leftConstraints
                        <> rightConstraints
                    )
               ]
        )

glossH0NPMaybe
    :: H0LexicalEnvironment
    -> H0Expr
    -> Raw.NounPhrase Maybe
    -> Gloss (H0Expr, Maybe H0Expr)
glossH0NPMaybe
        environment
        subject
        (Raw.NounPhrase leftAdjectives noun mayName rightAdjectives maySuchThat) = do
    nounConstraint <- glossH0Noun environment subject noun
    suchThatConstraint <-
        traverse (glossH0Stmt environment) maySuchThat
    case mayName of
        Nothing -> do
            leftConstraints <-
                for leftAdjectives (glossH0AdjL environment subject)
            rightConstraints <-
                for rightAdjectives (glossH0AdjR environment subject)
            pure
                ( Sem.makeConjunction
                    ( nounConstraint
                        : leftConstraints
                        <> rightConstraints
                    )
                , suchThatConstraint
                )
        Just name -> do
            let namedSubject =
                    Sem.TermVar
                        (resolveH0Reference environment name)
            leftConstraints <-
                for leftAdjectives
                    (glossH0AdjL environment namedSubject)
            rightConstraints <-
                for rightAdjectives
                    (glossH0AdjR environment namedSubject)
            let modifierConstraints =
                    leftConstraints <> rightConstraints
                constraint = case modifierConstraints of
                    [] ->
                        nounConstraint
                    _ ->
                        nounConstraint
                            `Sem.And`
                                Sem.makeConjunction
                                    ( Sem.Equals
                                        Nowhere
                                        subject
                                        namedSubject
                                        : modifierConstraints
                                    )
            pure (constraint, suchThatConstraint)

glossH0AdjL
    :: H0LexicalEnvironment
    -> H0Expr
    -> Raw.AdjL
    -> Gloss H0Expr
glossH0AdjL environment subject (Raw.AdjL location lexicalPattern arguments) = do
    argumentsPlan <- glossH0Terms environment arguments
    applyH0Quantifiers
        (h0TermsQuantifiers argumentsPlan)
        (Sem.FormulaAdj
            location
            subject
            lexicalPattern
            (h0TermExpressions argumentsPlan))

glossH0AdjR
    :: H0LexicalEnvironment
    -> H0Expr
    -> Raw.AdjR
    -> Gloss H0Expr
glossH0AdjR environment subject = \case
    Raw.AdjR _location lexicalPattern [argument]
        | lexicalPattern
            == Raw.mkLexicalItem
                (unsafeReadPhrase "equal to ?")
                "eq" -> do
                    argumentPlan <-
                        glossH0Term environment argument
                    applyH0Quantifiers
                        (h0TermQuantifiers argumentPlan)
                        (Sem.Equals
                            Nowhere
                            subject
                            (h0TermExpression argumentPlan))
    Raw.AdjR _location lexicalPattern arguments -> do
        argumentsPlan <- glossH0Terms environment arguments
        applyH0Quantifiers
            (h0TermsQuantifiers argumentsPlan)
            (Sem.FormulaAdj
                Nowhere
                subject
                lexicalPattern
                (h0TermExpressions argumentsPlan))
    Raw.AttrRThat verbPhrase ->
        glossH0VP environment subject verbPhrase

glossH0Adj
    :: H0LexicalEnvironment
    -> H0Expr
    -> Raw.Adj
    -> Gloss H0Expr
glossH0Adj environment subject = \case
    Raw.Adj location lexicalPattern [argument]
        | lexicalPattern
            == Raw.mkLexicalItem
                (unsafeReadPhrase "equal to ?")
                "eq" -> do
                    argumentPlan <-
                        glossH0Term environment argument
                    applyH0Quantifiers
                        (h0TermQuantifiers argumentPlan)
                        (Sem.Equals
                            location
                            subject
                            (h0TermExpression argumentPlan))
    Raw.Adj location lexicalPattern arguments -> do
        argumentsPlan <- glossH0Terms environment arguments
        applyH0Quantifiers
            (h0TermsQuantifiers argumentsPlan)
            (Sem.FormulaAdj
                location
                subject
                lexicalPattern
                (h0TermExpressions argumentsPlan))

glossH0VP
    :: H0LexicalEnvironment
    -> H0Expr
    -> Raw.VerbPhrase
    -> Gloss H0Expr
glossH0VP environment subject = \case
    Raw.VPVerb verb ->
        glossH0Verb environment subject verb
    Raw.VPAdj adjectives ->
        Sem.makeConjunction
            <$> for
                (toList adjectives)
                (glossH0Adj environment subject)
    Raw.VPVerbNot verb ->
        Sem.Not Nowhere
            <$> glossH0Verb environment subject verb
    Raw.VPAdjNot adjectives ->
        Sem.Not Nowhere
            <$> glossH0VP
                environment
                subject
                (Raw.VPAdj adjectives)

glossH0Verb
    :: H0LexicalEnvironment
    -> H0Expr
    -> Raw.Verb
    -> Gloss H0Expr
glossH0Verb environment subject (Raw.Verb location lexicalPattern arguments) = do
    argumentsPlan <- glossH0Terms environment arguments
    applyH0Quantifiers
        (h0TermsQuantifiers argumentsPlan)
        (Sem.FormulaVerb
            location
            subject
            lexicalPattern
            (h0TermExpressions argumentsPlan))

glossH0Noun
    :: H0LexicalEnvironment
    -> H0Expr
    -> Raw.Noun
    -> Gloss H0Expr
glossH0Noun environment subject (Raw.Noun location lexicalPattern arguments) = do
    argumentsPlan <- glossH0Terms environment arguments
    let constraint = case Raw.sg (Raw.lexicalItemSgPlPhrase lexicalPattern) of
            [Just (Sem.Word "set")] ->
                Sem.Top
            _ ->
                Sem.FormulaNoun
                    location
                    subject
                    lexicalPattern
                    (h0TermExpressions argumentsPlan)
    applyH0Quantifiers
        (h0TermsQuantifiers argumentsPlan)
        constraint



glossStmt :: Raw.Stmt -> Gloss Sem.Formula
glossStmt statement = do
    resolvedStatement <- glossH0Stmt [] statement
    lowerH0Expr resolvedStatement

glossH0Stmt
    :: H0LexicalEnvironment
    -> Raw.Stmt
    -> Gloss H0Expr
glossH0Stmt environment = \case
    Raw.StmtFormula formula ->
        resolveH0Expr environment <$> glossFormula formula
    Raw.StmtNeg location statement ->
        Sem.Not location <$> glossH0Stmt environment statement
    Raw.StmtVerbPhrase ts vp -> do
        termsPlan <- glossH0Terms environment (toList ts)
        statements <-
            for
                (h0TermExpressions termsPlan)
                (\term ->
                    glossH0VP
                        (h0TermsEnvironment termsPlan)
                        term
                        vp)
        applyH0Quantifiers
            (h0TermsQuantifiers termsPlan)
            (Sem.makeConjunction statements)
    Raw.StmtNoun ts np -> do
        termsPlan <- glossH0Terms environment (toList ts)
        statements <-
            for (h0TermExpressions termsPlan) \term -> do
                (nounConstraint, maySuchThat) <-
                    glossH0NPMaybe
                        (h0TermsEnvironment termsPlan)
                        term
                        np
                pure case maySuchThat of
                    Just suchThat ->
                        nounConstraint `Sem.And` suchThat
                    Nothing ->
                        nounConstraint
        applyH0Quantifiers
            (h0TermsQuantifiers termsPlan)
            (Sem.makeConjunction statements)
    Raw.StmtStruct t sp -> do
        termPlan <- glossH0Term environment t
        applyH0Quantifiers
            (h0TermQuantifiers termPlan)
            (Sem.TermSymbol
                (locate t)
                (Sem.SymbolPredicate
                    (Sem.PredicateNounStruct sp))
                [h0TermExpression termPlan])
    Raw.StmtConnected connective _location left right ->
        Sem.Connected connective
            <$> glossH0Stmt environment left
            <*> glossH0Stmt environment right
    Raw.StmtQuantPhrase _location (Raw.QuantPhrase quantifier np) statement -> do
        (vars, constraints) <- glossNPList np
        let nestedEnvironment =
                hideH0Binders vars environment
            constraints' =
                resolveH0Expr nestedEnvironment constraints
        statement' <-
            glossH0Stmt nestedEnvironment statement
        pure
            (quantifyH0Ambient
                quantifier
                vars
                [constraints']
                statement')
    Raw.StmtExists _location np -> do
        (vars, constraints) <- glossNPList np
        let nestedEnvironment =
                hideH0Binders vars environment
        pure
            (quantifyH0Ambient
                Raw.Existentially
                vars
                []
                (resolveH0Expr nestedEnvironment constraints))
    Raw.SymbolicQuantified _loc quant vs bound suchThat have -> do
        let nestedEnvironment =
                hideH0Binders vs environment
        bound' <- glossBound bound
        let boundConstraints =
                resolveH0Expr nestedEnvironment
                    <$> bound' (toList vs)
        suchThatConstraints <-
            maybeToList
                <$> traverse
                    (glossH0Stmt nestedEnvironment)
                    suchThat
        have' <- glossH0Stmt nestedEnvironment have
        pure
            (quantifyH0Ambient
                quant
                vs
                (boundConstraints <> suchThatConstraints)
                have')

-- Other binder forms stay on the legacy path and only mask outer H0 names.
hideH0Binders
    :: Foldable f
    => f VarSymbol
    -> H0LexicalEnvironment
    -> H0LexicalEnvironment
hideH0Binders variables =
    List.filter \binder ->
        maybe
            True
            (`Set.notMember` displayedNames)
            (binderDisplayHint (h0BinderTrivia binder))
  where
    displayedNames =
        Set.fromList
            [ name
            | NamedVarAt _ name <- toList variables
            ]

quantifyH0Ambient
    :: Foldable f
    => Raw.Quantifier
    -> f VarSymbol
    -> [H0Expr]
    -> H0Expr
    -> H0Expr
quantifyH0Ambient quantifier variables constraints body =
    case quantifier of
        Raw.Universally ->
            Sem.Quantified Sem.Universally scope
        Raw.Existentially ->
            Sem.Quantified Sem.Existentially scope
        Raw.Nonexistentially ->
            Sem.Not
                Nowhere
                (Sem.Quantified Sem.Existentially scope)
  where
    constrainedBody =
        applyQuantifierConstraints quantifier constraints body
    scope =
        abstract
            (\case
                AmbientRef variable
                    | variable `elem` variables ->
                        Just variable
                _ ->
                    Nothing)
            constrainedBody

-- | A bound applies to all listed variables. Note the use of '<**>'.
--
-- >>> ([1, 2, 3] <**> [(+ 10)]) == [11, 12, 13]
--
glossBound :: Raw.Bound -> Gloss ([VarSymbol] -> [Sem.Formula])
glossBound = \case
    Raw.Unbounded -> pure (const [])
    Raw.Bounded loc sign rel term -> do
        term' <- glossExpr term
        let sign' = case sign of
                Positive -> id
                Negative -> Sem.Not loc
        bound <- case rel of
            Raw.Relation loc' rel' params -> do
                params' <- glossExpr `each` params
                buildRelation <-
                    liftRelationApplication
                        (Sem.makeRelationApplication loc' rel' params')
                pure $ \v -> sign' $
                    buildRelation (Sem.TermVar v) term'
            Raw.RelationExpr loc' e -> do
                e' <- glossExpr e
                pure $ \v -> sign' $
                    Sem.IsElementOf loc' (Sem.TermPair loc' (Sem.TermVar v) term') e'
        pure \vs -> vs <**> [bound]


glossConnective :: Raw.Connective -> Gloss (Sem.Formula -> Sem.Formula -> Sem.Formula)
glossConnective conn = pure (Sem.Connected conn)


glossAsm :: Raw.Asm -> Gloss [Sem.Asm]
glossAsm = \case
    Raw.AsmSuppose s -> do
        s' <- glossStmt s
        pure [Sem.Asm s']
    Raw.AsmLetNoun vs np -> do
        (np', maySuchThat) <- glossNPMaybe np
        let f v = Sem.Asm (np' (Sem.TermVar v) )
        let suchThat = Sem.Asm <$> maybeToList maySuchThat
        pure (suchThat <> fmap f (toList vs))
    Raw.AsmLetIn vs e -> do
        e' <- glossExpr e
        let f v = Sem.Asm (Sem.IsElementOf Nowhere (Sem.TermVar v) e')
        pure $ fmap f (toList vs)
    Raw.AsmLetStruct structLabel structPhrase ->
        pure [Sem.AsmStruct structLabel structPhrase]
    Raw.AsmLetThe _variable fun ->
        throwError
            (DefiniteFunctionAssumptionNotSupported
                (locate fun))
    Raw.AsmLetEq x e -> do
        e' <- glossExpr e
        pure (Sem.Asm (Sem.Equals Nowhere (Sem.TermVar x) e') : [])


-- | A quantifier is interpreted as a quantification function that takes a nonempty list of variables,
-- a list of formulas expressing the constraints, and the formula to be quantified as arguments.
-- It then returns the quantification with the correct connective for the constraints.
glossQuantifier
    :: (Foldable t, Applicative f)
    => Raw.Quantifier
    -> f (t VarSymbol
    -> [Sem.ExprOf VarSymbol]
    -> Sem.Formula
    -> Sem.Formula)
glossQuantifier quantifier = pure quantify
    where
        quantify vs constraints body = case quantifier of
            Raw.Universally ->
                Sem.makeForall
                    vs
                    (applyQuantifierConstraints
                        quantifier
                        constraints
                        body)
            Raw.Existentially ->
                Sem.makeExists
                    vs
                    (applyQuantifierConstraints
                        quantifier
                        constraints
                        body)
            Raw.Nonexistentially ->
                Sem.Not
                    Nowhere
                    (Sem.makeExists
                        vs
                        (applyQuantifierConstraints
                            quantifier
                            constraints
                            body))

applyQuantifierConstraints
    :: Raw.Quantifier
    -> [Sem.ExprOf a]
    -> Sem.ExprOf a
    -> Sem.ExprOf a
applyQuantifierConstraints _quantifier [] body =
    body
applyQuantifierConstraints quantifier constraints body =
    case quantifier of
        Raw.Universally ->
            Sem.makeConjunction constraints `Sem.Implies` body
        Raw.Existentially ->
            Sem.makeConjunction constraints `Sem.And` body
        Raw.Nonexistentially ->
            Sem.makeConjunction constraints `Sem.And` body


glossAsms :: [Raw.Asm] -> Gloss [Sem.Asm]
glossAsms asms = do
    asms' <- glossAsm `each` asms
    pure $ concat asms'


glossAxiom :: Raw.Axiom -> Gloss Sem.Axiom
glossAxiom (Raw.Axiom asms f) = Sem.Axiom <$> glossAsms asms <*> glossStmt f


glossLemma :: Raw.Claim -> Gloss Sem.Lemma
glossLemma (Raw.Claim asms f) = Sem.Lemma <$> glossAsms asms <*> glossStmt f


glossDefn
    :: Location
    -> Sem.Marker
    -> Raw.Defn
    -> Gloss Sem.Defn
glossDefn blockLocation blockMarker = \case
    Raw.Defn asms h f ->
        glossDefnHead blockLocation h <*> glossAsms asms <*> glossStmt f
    Raw.DefnFun asms (Raw.Fun _loc fun vs) _ e -> do
        asms' <- glossAsms asms
        e' <- case e of
            Raw.TermQuantified _ loc _ ->
                throwError
                    (GlossDefnError
                        loc
                        DefnErrorQuantifiedRhsTerm
                        blockMarker)
            _ -> fst <$> glossTerm e
        pure $ Sem.DefnFun asms' fun vs e'
    Raw.DefnOp (Raw.SymbolPattern op vs) e ->
        Sem.DefnOp op vs <$> glossExpr e


-- | A definition head is interpreted as a builder of a definition,
-- depending on a previous assumptions and on a rhs.
glossDefnHead
    :: Location
    -> Raw.DefnHead
    -> Gloss ([Sem.Asm] -> Sem.Formula -> Sem.Defn)
glossDefnHead blockLocation = \case
    -- TODO add info from NP.
    Raw.DefnAdj _mnp v (Raw.Adj _loc adj vs) -> do
        pure $ \asms f -> Sem.DefnPredicate asms (Sem.PredicateAdj adj) (v :| vs) f
        --mnp' <- glossNPMaybe `each` mnp
        --pure $ case mnp' of
        --    Nothing  -> \asms f -> Sem.DefnPredicate asms (Sem.PredicateAdj adj') (v :| vs) f
        --    Just np' -> \asms f -> Sem.DefnPredicate asms (Sem.PredicateAdj adj') (v :| vs) (Sem.FormulaAnd (np' v) f)
    Raw.DefnVerb _mnp v (Raw.Verb _loc verb vs) ->
        pure $ \asms f -> Sem.DefnPredicate asms (Sem.PredicateVerb verb) (v :| vs) f
    Raw.DefnNoun v (Raw.Noun _loc noun vs) ->
        pure $ \asms f -> Sem.DefnPredicate asms (Sem.PredicateNoun noun) (v :| vs) f
    Raw.DefnRel v1 rel params v2 -> do
        liftRelationApplication
            (Sem.checkRelationParameterArity
                blockLocation
                rel
                params)
        pure \asms f ->
            let args = case params of
                    p : ps -> p :| (ps <> [v1, v2])
                    [] -> v1 :| [v2]
            in Sem.DefnPredicate asms (Sem.PredicateRelation rel) args f
    Raw.DefnSymbolicPredicate (Raw.PrefixPredicate symb _ar) _marker vs ->
        pure $ \asms f -> Sem.DefnPredicate asms (Sem.PredicateSymbol symb) vs f


glossProof :: Raw.Proof -> Gloss Sem.Proof
glossProof = \case
    Raw.Omitted loc ->
        pure (Sem.Omitted loc)
    Raw.Qed loc by ->
        pure (Sem.Qed loc by)
    Raw.Contradiction loc by ->
        pure (Sem.Contradiction loc by)
    Raw.ByContradiction loc proof ->
        Sem.ByContradiction loc <$> glossProof proof
    Raw.BySetInduction loc mt proof ->
        Sem.BySetInduction loc <$> mmt' <*> glossProof proof
            where
                mmt' = case mt of
                    Nothing -> pure Nothing
                    Just (Raw.TermExpr (Raw.ExprVar x)) -> pure (Just (Sem.TermVar x))
                    Just _t -> throwError (GlossInductionError loc)
    Raw.ByOrdInduction loc proof ->
        Sem.ByOrdInduction loc <$> glossProof proof
    Raw.ByCase loc cases -> Sem.ByCase loc <$> glossCase `each` cases
    Raw.Have loc _ms s by proof -> case s of
        -- Pragmatics: an existential @Have@ implicitly
        -- introduces the witness and is interpreted as a @Take@ construct.
        Raw.SymbolicExists _loc vs bound suchThat -> do
            bound' <- glossBound bound
            suchThat' <- glossStmt suchThat
            proof' <- glossProof proof
            pure (Sem.Take loc vs (Sem.makeConjunction (suchThat' : bound' (toList vs))) by proof')
        _otherwise ->
            Sem.Have loc <$> glossStmt s <*> pure by <*> glossProof proof
    Raw.Assume loc stmt proof ->
        Sem.Assume loc <$> glossStmt stmt <*> glossProof proof
    Raw.FixSymbolic loc xs bound proof -> do
        bound' <- glossBound bound
        proof' <- glossProof proof
        pure (Sem.Fix loc xs (Sem.makeConjunction (bound' (toList xs))) proof')
    Raw.FixSuchThat loc xs stmt proof -> do
        stmt' <- glossStmt stmt
        proof' <- glossProof proof
        pure (Sem.Fix loc xs stmt' proof')
    Raw.TakeVar loc vs bound suchThat by proof -> do
        bound' <- glossBound bound
        suchThat' <- glossStmt suchThat
        proof' <- glossProof proof
        pure (Sem.Take loc vs (Sem.makeConjunction (suchThat' : bound' (toList vs))) by proof')
    Raw.TakeNoun loc np by proof -> do
        (vs, constraints) <- glossNPList np
        proof' <- glossProof proof
        pure $ Sem.Take loc vs constraints by proof'
    Raw.Subclaim loc subclaim subproof proof ->
        Sem.Subclaim loc <$> glossStmt subclaim <*> glossProof subproof <*> glossProof proof
    Raw.Suffices loc reduction by proof ->
        Sem.Suffices loc <$> glossStmt reduction <*> pure by <*> glossProof proof
    Raw.Define loc var term proof ->
        Sem.Define loc var <$> glossExpr term <*> glossProof proof
    Raw.DefineFunction loc funVar argVar valueExpr domVar domExpr proof ->
        if domVar == argVar
            then Sem.DefineFunction loc funVar argVar <$> glossExpr valueExpr <*> glossExpr domExpr <*> glossProof proof
            else
                throwError
                    (GlossProofFunctionArgumentMismatch
                        loc
                        argVar
                        domVar)

    Raw.DefineFunctionLocal loc funVar domVar ranExpr funVar2 argVar definitions proof -> do
        if funVar == funVar2
            then Sem.DefineFunctionLocal loc funVar argVar domVar <$> glossExpr ranExpr <*> (glossLocalFunctionExprDef `each` definitions) <*> glossProof proof
            else
                throwError
                    (GlossProofFunctionNameMismatch
                        loc
                        funVar
                        funVar2)
    Raw.Calc loc calcQuant calc proof ->
        Sem.Calc loc <$> glossCalcQuantifier calcQuant <*> glossCalc calc <*> glossProof proof

glossCalcQuantifier :: Maybe Raw.CalcQuantifier -> Gloss Sem.CalcQuantifier
glossCalcQuantifier Nothing = pure Sem.CalcUnquantified
glossCalcQuantifier (Just (Raw.CalcQuantifier xs bound maySuchThat)) = do
    bound' <- glossBound bound
    maySuchThat' <- glossStmt `each` maySuchThat
    let constraints = bound' (toList xs) <> maybeToList maySuchThat'
    let calcGuard = case constraints of
            [] -> Nothing
            _ -> Just (Sem.makeConjunction constraints)
    pure (Sem.CalcForall xs calcGuard)

glossLocalFunctionExprDef :: (Raw.Expr, Raw.Formula) -> Gloss (Sem.Term, Sem.Formula)
glossLocalFunctionExprDef (definingExpression, localDomain) = do
    e <- glossExpr definingExpression
    d <- glossFormula localDomain
    pure (e,d)


glossCase :: Raw.Case -> Gloss Sem.Case
glossCase (Raw.Case caseOf proof) = Sem.Case <$> glossStmt caseOf <*> glossProof proof

glossCalc :: Raw.Calc -> Gloss Sem.Calc
glossCalc = \case
    Raw.Equation e eqns -> do
        e' <- glossExpr e
        eqns' <- (\(ei, ji) -> (,ji) <$> glossExpr ei) `each` eqns
        pure (Sem.Equation e' eqns')
    Raw.Biconditionals p ps -> do
        p' <- glossFormula p
        ps' <- (\(pi, ji) -> (,ji) <$> glossFormula pi) `each` ps
        pure (Sem.Biconditionals p' ps')

glossSignature :: Raw.Signature -> Gloss Sem.Signature
glossSignature sig = case sig of
    Raw.SignatureAdj v (Raw.Adj _loc adj vs) ->
        pure $ Sem.SignaturePredicate (Sem.PredicateAdj adj) (v :| vs)
    Raw.SignatureVerb v (Raw.Verb _loc verb vs) ->
        pure $ Sem.SignaturePredicate (Sem.PredicateVerb verb) (v :| vs)
    Raw.SignatureNoun v (Raw.Noun _loc noun vs) ->
        pure $ Sem.SignaturePredicate (Sem.PredicateNoun noun) (v :| vs)
    Raw.SignatureSymbolic (Raw.SymbolPattern op vs) np -> do
        (np', maySuchThat) <- glossNPMaybe np
        let andSuchThat phi = case maySuchThat of
                Just suchThat -> phi `Sem.And` suchThat
                Nothing -> phi
        let op' = Sem.TermOp Nowhere op (Sem.TermVar <$> vs)
        v <-  freshVar
        let v' = Sem.TermVar v
        pure $ Sem.SignatureFormula $ Sem.makeForall [v] ((Sem.Equals Nowhere  v' op') `Sem.Implies` andSuchThat (np' v'))


glossStructDefn :: Raw.StructDefn -> Gloss Sem.StructDefn
glossStructDefn (Raw.StructDefn phrase base carrier fixes assumes) = do
    assumes' <- (\(m, stmt) -> (m,) <$> glossStmt stmt) `each` assumes
    let base' = Set.fromList base
    let fixes' = Set.fromList fixes
    pure $ Sem.StructDefn phrase base' carrier fixes' assumes'


glossAbbreviation
    :: Location
    -> Sem.Marker
    -> Raw.Abbreviation
    -> Gloss Sem.Abbreviation
glossAbbreviation blockLocation blockMarker = \case
    Raw.AbbreviationAdj x (Raw.Adj _loc adj xs) stmt ->
        build
            (Sem.SymbolPredicate (Sem.PredicateAdj adj))
            (x : xs)
            (glossStmt stmt)
    Raw.AbbreviationVerb x (Raw.Verb _loc verb xs) stmt ->
        build
            (Sem.SymbolPredicate (Sem.PredicateVerb verb))
            (x : xs)
            (glossStmt stmt)
    Raw.AbbreviationNoun x (Raw.Noun _loc noun xs) stmt ->
        build
            (Sem.SymbolPredicate (Sem.PredicateNoun noun))
            (x : xs)
            (glossStmt stmt)
    Raw.AbbreviationRel x rel params y stmt -> do
        liftRelationApplication
            (Sem.checkRelationParameterArity
                blockLocation
                rel
                params)
        build
            (Sem.SymbolPredicate (Sem.PredicateRelation rel))
            (params <> [x, y])
            (glossStmt stmt)
    Raw.AbbreviationFun (Raw.Fun _loc fun xs) t ->
        build
            (Sem.SymbolFun fun)
            xs
            (fst <$> glossTerm t)
    Raw.AbbreviationEq (Raw.SymbolPattern op xs) e ->
        build
            (Sem.SymbolMixfix op)
            xs
            (glossExpr e)
  where
    build =
        makeAbbreviation blockLocation blockMarker

makeAbbreviation
    :: Location
    -> Sem.Marker
    -> Sem.Symbol
    -> [VarSymbol]
    -> Gloss Sem.Expr
    -> Gloss Sem.Abbreviation
makeAbbreviation blockLocation blockMarker symbol rawParameters elaborateBody = do
    parameters <-
        either
            (throwError
                . GlossAbbreviationError
                    blockLocation
                    blockMarker
                . DuplicateAbbreviationParameters)
            pure
            (validateAbbreviationParameters rawParameters)
    body <- elaborateBody
    scope <-
        either
            (throwError
                . GlossAbbreviationError
                    blockLocation
                    blockMarker
                . FreeAbbreviationBodyVariables)
            pure
            (abstractClosedAbbreviation parameters body)
    pure (Sem.Abbreviation symbol scope)
  where
    validateAbbreviationParameters
        :: [VarSymbol]
        -> Either
            (NonEmpty VarSymbol)
            (Map VarSymbol Int)
    validateAbbreviationParameters parameters =
        case NonEmpty.nonEmpty (duplicateParameters parameters) of
            Just duplicates ->
                Left duplicates
            Nothing ->
                Right (Map.fromList (zip parameters [0 ..]))

    abstractClosedAbbreviation
        :: Map VarSymbol Int
        -> Sem.Expr
        -> Either
            (NonEmpty VarSymbol)
            (Scope Int Sem.ExprOf Void)
    abstractClosedAbbreviation parameterIndices body =
        case NonEmpty.nonEmpty unknownVariables of
            Just variables ->
                Left variables
            Nothing ->
                case traverse bindParameter body of
                    Left variable ->
                        Left (variable :| [])
                    Right scopedBody ->
                        Right (toScope scopedBody)
      where
        unknownVariables =
            Set.toAscList
                ( Sem.freeVars body
                    `Set.difference`
                        Map.keysSet parameterIndices
                )

        bindParameter
            :: VarSymbol
            -> Either
                VarSymbol
                (Var Int Void)
        bindParameter variable =
            case Map.lookup variable parameterIndices of
                Nothing ->
                    Left variable
                Just parameterIndex ->
                    Right (B parameterIndex)

    duplicateParameters :: [VarSymbol] -> [VarSymbol]
    duplicateParameters =
        reverse . third . foldl' step (mempty, mempty, [])
      where
        step (seen, reported, duplicates) variable
            | variable `Set.notMember` seen =
                (Set.insert variable seen, reported, duplicates)
            | variable `Set.member` reported =
                (seen, reported, duplicates)
            | otherwise =
                ( seen
                , Set.insert variable reported
                , variable : duplicates
                )

        third (_seen, _reported, duplicates) =
            duplicates

glossInductive :: Raw.Inductive -> Gloss Sem.Inductive
glossInductive (Raw.Inductive (Raw.SymbolPattern symbol args) domain rules) =
    Sem.Inductive symbol args <$> glossExpr domain <*> (glossRule `each` rules)
    where
        glossRule (Raw.IntroRule phis psi) = Sem.IntroRule <$> (glossFormula `each` phis) <*> glossFormula psi

glossDatatype :: Raw.Datatype -> Gloss Sem.Datatype
glossDatatype rawDatatype = do
    let datatypeHeadExpr = Raw.datatypeHeadExpr rawDatatype
        rawClauses = Raw.datatypeClauses rawDatatype
    datatypeHead <- glossDatatypeHead datatypeHeadExpr
    datatypeClauses <- glossDatatypeClause datatypeHead `each` rawClauses
    pure (Sem.Datatype datatypeHead datatypeClauses)
    where
        glossDatatypeHead :: Raw.Expr -> Gloss Sem.SymbolPattern
        glossDatatypeHead expr = case expr of
            Raw.ExprOp _loc item [] ->
                pure (Sem.SymbolPattern item [])
            _ ->
                throwError (GlossDatatypeHeadError (locate expr))

        glossDatatypeClause :: Sem.SymbolPattern -> Raw.DatatypeClause -> Gloss Sem.DatatypeClause
        glossDatatypeClause datatypeHead rawClause = do
            let constructorExpr = Raw.datatypeClauseConstructorExpr rawClause
                targetExpr = Raw.datatypeClauseTargetExpr rawClause
                rawPremises = Raw.datatypeClausePremises rawClause
            datatypeTarget <- glossDatatypeHead targetExpr
            unless (datatypeTarget == datatypeHead) do
                throwError (GlossDatatypeClauseTargetError (locate targetExpr))
            datatypeClauseConstructor <- glossDatatypeConstructor constructorExpr
            datatypeClausePremises <- traverse glossDatatypePremise rawPremises
            pure (Sem.DatatypeClause datatypeClauseConstructor datatypeClausePremises)

        glossDatatypeConstructor :: Raw.Expr -> Gloss Sem.SymbolPattern
        glossDatatypeConstructor expr = case expr of
            Raw.ExprOp _loc item args -> do
                vars <- traverse glossConstructorArg args
                pure (Sem.SymbolPattern item vars)
            _ ->
                throwError (GlossDatatypeConstructorError (locate expr))

        glossConstructorArg :: Raw.Expr -> Gloss VarSymbol
        glossConstructorArg = \case
            Raw.ExprVar x -> pure x
            expr -> throwError (GlossDatatypeConstructorError (locate expr))

        glossDatatypePremise :: (VarSymbol, Raw.Expr) -> Gloss (VarSymbol, Sem.Expr)
        glossDatatypePremise (x, domain) =
            (x,) <$> glossExpr domain

glossBlock :: Raw.Block -> Gloss Sem.Block
glossBlock = \case
    Raw.BlockAxiom loc _title marker axiom ->
        Sem.BlockAxiom loc marker <$> glossAxiom axiom
    Raw.BlockClaim _claimKind loc _title marker lemma ->
        Sem.BlockLemma loc marker <$> glossLemma lemma
    Raw.BlockProof startLoc proof endLoc ->
        Sem.BlockProof startLoc endLoc <$> glossProof proof
    Raw.BlockDefn loc _title marker defn -> do
        defn' <- glossDefn loc marker defn
        whenLeft (isWellformedDefn defn') (\err -> throwError (GlossDefnError loc err marker))
        pure $ Sem.BlockDefn loc marker defn'
    Raw.BlockAbbr loc _title marker abbr ->
        Sem.BlockAbbr loc marker
            <$> glossAbbreviation loc marker abbr
    Raw.BlockSig loc _title marker asms sig ->
        Sem.BlockSig loc marker <$> glossAsms asms <*> glossSignature sig
    Raw.BlockStruct loc _title m structDefn ->
        Sem.BlockStruct loc m <$> glossStructDefn structDefn
    Raw.BlockData loc _title marker datatype ->
        Sem.BlockData loc marker <$> glossDatatype datatype
    Raw.BlockInductive loc _title marker ind ->
        Sem.BlockInductive loc marker <$> glossInductive ind


glossBlocks :: [Raw.Block] -> Gloss [Sem.Block]
glossBlocks blocks = glossBlock `each` blocks