Gather some location info from parser

WIP

7 files changed, 367 insertions, 283 deletions

diff --git a/source/Checking.hs b/source/Checking.hs
index 449102f..63ab99c 100644
--- a/source/Checking.hs
+++ b/source/Checking.hs
@@ -391,9 +391,9 @@ checkAxiom (Axiom asms axiom) = addFactWithAsms asms axiom
 
 checkProof :: Proof -> Checking
 checkProof = \case
-    Qed JustificationEmpty->
+    Qed pos JustificationEmpty->
         tellTasks
-    Qed JustificationSetExt -> do
+    Qed pos JustificationSetExt -> do
         goals <- gets checkingGoals
         case goals of
             [goal] -> do
@@ -402,11 +402,11 @@ checkProof = \case
                 tellTasks
             [] -> pure ()
             _ -> throwWithMarker (MismatchedSetExt goals)
-    Qed (JustificationRef ms) ->
+    Qed pos (JustificationRef ms) ->
         byRef ms
-    Qed JustificationLocal ->
+    Qed pos JustificationLocal ->
         byAssumption
-    ByContradiction proof -> do
+    ByContradiction pos proof -> do
         goals <- gets checkingGoals
         case goals of
             [goal] -> do
@@ -414,11 +414,11 @@ checkProof = \case
                 byContradiction
                 checkProof proof
             _ -> throwWithMarker ByContradictionOnMultipleGoals
-    ByCase splits -> do
+    ByCase pos splits -> do
         for_ splits checkCase
         setGoals [makeDisjunction (caseOf <$> splits)]
         tellTasks
-    BySetInduction mx continue -> do
+    BySetInduction pos mx continue -> do
         goals <- gets checkingGoals
         case goals of
             Forall scope : goals' -> do
@@ -442,7 +442,7 @@ checkProof = \case
             _ -> do
                 m <- gets blockLabel
                 throwIO (BySetInductionSyntacticMismatch m)
-    ByOrdInduction continue -> do
+    ByOrdInduction pos continue -> do
         goals <- gets checkingGoals
         case goals of
             Forall scope : goals' -> case fromScope scope of
@@ -463,52 +463,52 @@ checkProof = \case
                     checkProof continue
                 _ -> error ("could not match transfinite induction with syntactic structure of the first goal: " <> show goals)
             _ -> error ("the first goal must be universally quantifier to apply transfinite induction: " <> show goals)
-    Assume phi continue -> do
+    Assume pos phi continue -> do
         goals' <- matchAssumptionWithGoal phi
         assume [Asm phi]
         setGoals goals'
         checkProof continue
-    Fix xs suchThat continue -> do
+    Fix pos xs suchThat continue -> do
         fixing xs
         checkProof case suchThat of
             Top -> continue
-            _ ->  Assume suchThat continue
-    Subclaim subclaim subproof continue -> do
+            _ ->  Assume pos suchThat continue
+    Subclaim pos subclaim subproof continue -> do
         locally (checkLemmaWithProof (Lemma [] subclaim) subproof)
         assume [Asm subclaim]
         checkProof continue
     Omitted -> do
         setGoals []
-    Suffices reduction by proof -> do
+    Suffices pos reduction by proof -> do
         goals <- gets checkingGoals
         setGoals [reduction `Implies` makeConjunction goals]
         justify by
         setGoals [reduction]
         checkProof proof
-    Take _witnesses _suchThat JustificationSetExt _continue ->
-        error "cannot justify existential statement with setext"
-    Take witnesses suchThat by continue -> locally do
+    Take pos _witnesses _suchThat JustificationSetExt _continue ->
+        error $ "Error at " <> show pos <> "\nCannot justify existential statement with setext"
+    Take pos witnesses suchThat by continue -> locally do
         goals <- gets checkingGoals
         setGoals [makeExists witnesses suchThat]
         justify by
         assume [Asm suchThat]
         setGoals goals
         checkProof continue
-    Have claim (JustificationRef ms) continue -> locally do
+    Have pos claim (JustificationRef ms) continue -> locally do
         goals <- gets checkingGoals
         setGoals [claim]
         byRef ms -- locally prove things with just refs and local assumptions
         assume [Asm claim]
         setGoals goals
         checkProof continue
-    Have claim JustificationLocal continue -> locally do
+    Have pos claim JustificationLocal continue -> locally do
         goals <- gets checkingGoals
         setGoals [claim]
         byAssumption -- locally prove things with just local assumptions
         assume [Asm claim]
         setGoals goals
         checkProof continue
-    Have claim by continue -> do
+    Have pos claim by continue -> do
         locally do
             goals <- gets checkingGoals
             claims <- case by of
@@ -522,7 +522,7 @@ checkProof = \case
             assume [Asm claim]
             setGoals goals
             checkProof continue
-    Define x t continue -> locally do
+    Define pos x t continue -> locally do
         assume [Asm case t of
             TermSep y yBound phi ->
                 makeForall [y] $
@@ -533,7 +533,7 @@ checkProof = \case
             _ -> Equals (TermVar x) t
             ]
         checkProof continue
-    DefineFunction funVar argVar valueExpr domExpr continue -> do
+    DefineFunction pos funVar argVar valueExpr domExpr continue -> do
         -- we're given f, x, e, d
         assume
             [ Asm (TermOp DomSymbol [TermVar funVar] `Equals` domExpr) -- dom(f) = d
@@ -542,11 +542,11 @@ checkProof = \case
             , Asm (relationNoun (TermVar funVar))
             ]
         checkProof continue
-    Calc quant calc continue -> do
+    Calc pos quant calc continue -> do
         checkCalc quant calc
         assume [Asm (calcResult quant calc)]
         checkProof continue
-    DefineFunctionLocal funVar argVar domVar ranExpr definitions continue -> do
+    DefineFunctionLocal pos funVar argVar domVar ranExpr definitions continue -> do
         -- We have f: X \to Y and x \mapsto ...
         -- definition is a nonempty list of (expresssion e, formula phi)
         -- such that f(x) =  e if phi(x)
diff --git a/source/Meaning.hs b/source/Meaning.hs
index 160640e..3bf2c9c 100644
--- a/source/Meaning.hs
+++ b/source/Meaning.hs
@@ -16,7 +16,7 @@ import Syntax.Internal (VarSymbol(..))
 import Syntax.Internal qualified as Sem
 import Syntax.LexicalPhrase (unsafeReadPhrase)
 import Syntax.Lexicon
-
+import Text.Megaparsec.Pos
 
 import Bound
 import Bound.Scope (abstractEither)
@@ -325,7 +325,7 @@ forEach vs'' stmts = do
 
 
 glossAdjL :: Raw.AdjL -> Gloss (Sem.Term -> Sem.Formula)
-glossAdjL (Raw.AdjL pat es) = do
+glossAdjL (Raw.AdjL pos pat es) = do
     (es', quantifies) <- unzip <$> glossTerm `each` es
     let quantify = compose $ reverse quantifies
     pure $ \t -> quantify $ Sem.FormulaAdj t pat es'
@@ -336,10 +336,10 @@ glossAdjL (Raw.AdjL pat es) = do
 -- the term representing the subject, hence the parameter 'Sem.Expr'.
 glossAdjR :: Raw.AdjR -> Gloss (Sem.Term -> Sem.Formula)
 glossAdjR = \case
-    Raw.AdjR pat [e] | pat == unsafeReadPhrase "equal to ?" -> do
+    Raw.AdjR pos pat [e] | pat == unsafeReadPhrase "equal to ?" -> do
         (e', quantify) <- glossTerm e
         pure $ \t -> quantify $ Sem.Equals t e'
-    Raw.AdjR pat es -> do
+    Raw.AdjR pos pat es -> do
         (es', quantifies) <- unzip <$> glossTerm `each` es
         let quantify = compose $ reverse quantifies
         pure $ \t -> quantify $ Sem.FormulaAdj t pat es'
@@ -348,10 +348,10 @@ glossAdjR = \case
 
 glossAdj :: Raw.AdjOf Raw.Term -> Gloss (Sem.ExprOf VarSymbol -> Sem.Formula)
 glossAdj adj = case adj of
-    Raw.Adj pat [e] | pat == unsafeReadPhrase "equal to ?" -> do
+    Raw.Adj pos pat [e] | pat == unsafeReadPhrase "equal to ?" -> do
         (e', quantify) <- glossTerm e
         pure $ \t -> quantify $ Sem.Equals t e'
-    Raw.Adj pat es -> do
+    Raw.Adj pos pat es -> do
         (es', quantifies) <- unzip <$> glossTerm `each` es
         let quantify = compose $ reverse quantifies
         pure $ \t -> quantify $ Sem.FormulaAdj t pat es'
@@ -367,7 +367,7 @@ glossVP = \case
 
 
 glossVerb :: Raw.Verb -> Gloss (Sem.Term -> Sem.Formula)
-glossVerb (Raw.Verb pat es) = do
+glossVerb (Raw.Verb pos pat es) = do
     (es', quantifies) <- unzip <$> glossTerm `each` es
     let quantify = compose $ reverse quantifies
     pure $ \ t -> quantify $ Sem.FormulaVerb t pat es'
@@ -384,7 +384,7 @@ glossNoun (Raw.Noun pat es) = do
 
 
 glossFun :: Raw.Fun -> Gloss (Sem.Term, Sem.Formula -> Sem.Formula)
-glossFun (Raw.Fun phrase es) = do
+glossFun (Raw.Fun pos phrase es) = do
     (es', quantifies) <- unzip <$> glossTerm `each` es
     let quantify = compose $ reverse quantifies
     pure (Sem.TermSymbol (Sem.SymbolFun phrase) es', quantify)
@@ -396,11 +396,11 @@ glossTerm = \case
         (, id) <$> glossExpr e
     Raw.TermFun f ->
         glossFun f
-    Raw.TermIota x stmt -> do
+    Raw.TermIota pos x stmt -> do
         stmt' <- glossStmt stmt
         _TODO "glossTerm TermIota"
         --pure (Sem.Iota x (abstract1 x stmt'), id)
-    Raw.TermQuantified quantifier np -> do
+    Raw.TermQuantified quantifier pos np -> do
         quantify <- glossQuantifier quantifier
         (mkConstraint, maySuchThat) <- glossNPMaybe np
         v <- freshVar
@@ -413,13 +413,13 @@ glossTerm = \case
 glossStmt :: Raw.Stmt -> Gloss Sem.Formula
 glossStmt = \case
     Raw.StmtFormula f -> glossFormula f
-    Raw.StmtNeg s -> Sem.Not <$> glossStmt s
+    Raw.StmtNeg pos s -> Sem.Not <$> glossStmt s
     Raw.StmtVerbPhrase ts vp -> do
         (ts', quantifies) <- NonEmpty.unzip <$> glossTerm `each` ts
         vp' <- glossVP vp
         let phi = Sem.makeConjunction (vp' <$> toList ts')
         pure (compose quantifies phi)
-    Raw.StmtNoun ts np -> do
+    Raw.StmtNoun pos ts np -> do
         (ts', quantifies) <- NonEmpty.unzip <$> glossTerm `each` ts
         (np', maySuchThat) <- glossNPMaybe np
         let andSuchThat phi = case maySuchThat of
@@ -427,19 +427,19 @@ glossStmt = \case
                 Nothing -> phi
             psi = Sem.makeConjunction (andSuchThat . np' <$> toList ts')
         pure (compose quantifies psi)
-    Raw.StmtStruct t sp -> do
+    Raw.StmtStruct pos t sp -> do
         (t', quantify) <- glossTerm t
         pure (quantify (Sem.TermSymbol (Sem.SymbolPredicate (Sem.PredicateNounStruct sp)) [t']))
-    Raw.StmtConnected conn s1 s2 -> glossConnective conn <*> glossStmt s1 <*> glossStmt s2
-    Raw.StmtQuantPhrase (Raw.QuantPhrase quantifier np) f -> do
+    Raw.StmtConnected conn mpos s1 s2 -> glossConnective conn <*> glossStmt s1 <*> glossStmt s2
+    Raw.StmtQuantPhrase pos (Raw.QuantPhrase quantifier np) f -> do
         (vars, constraints) <- glossNPList np
         f' <- glossStmt f
         quantify <- glossQuantifier quantifier
         pure (quantify vars [constraints] f')
-    Raw.StmtExists np -> do
+    Raw.StmtExists pos np -> do
         (vars, constraints) <- glossNPList np
         pure (Sem.makeExists vars constraints)
-    Raw.SymbolicQuantified quant vs bound suchThat have -> do
+    Raw.SymbolicQuantified pos quant vs bound suchThat have -> do
         quantify <- glossQuantifier quant
         bound' <- glossBound bound
         suchThatConstraints <- maybeToList <$> glossStmt `each` suchThat
@@ -547,11 +547,11 @@ glossLemma (Raw.Lemma asms f) = Sem.Lemma <$> glossAsms asms <*> glossStmt f
 glossDefn :: Raw.Defn -> Gloss Sem.Defn
 glossDefn = \case
     Raw.Defn asms h f -> glossDefnHead h <*> glossAsms asms <*> glossStmt f
-    Raw.DefnFun asms (Raw.Fun fun vs) _ e -> do
+    Raw.DefnFun asms (Raw.Fun pos fun vs) _ e -> do
         asms' <- glossAsms asms
         e' <- case e of
             -- TODO improve error handling or make grammar stricter
-            Raw.TermQuantified _ _ -> error $ "Quantified term in definition: " <> show e
+            Raw.TermQuantified _ p _ -> error $ "Quantified term in definition at" <> sourcePosPretty p <> " : " <> show e
             _ -> fst <$> glossTerm e
         pure $ Sem.DefnFun asms' fun vs e'
     Raw.DefnOp (Raw.SymbolPattern op vs) e ->
@@ -563,13 +563,13 @@ glossDefn = \case
 glossDefnHead :: Raw.DefnHead -> Gloss ([Sem.Asm] -> Sem.Formula -> Sem.Defn)
 glossDefnHead = \case
     -- TODO add info from NP.
-    Raw.DefnAdj _mnp v (Raw.Adj adj vs) -> do
+    Raw.DefnAdj _mnp v (Raw.Adj pos 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 verb vs) ->
+    Raw.DefnVerb _mnp v (Raw.Verb pos verb vs) ->
         pure $ \asms f -> Sem.DefnPredicate asms (Sem.PredicateVerb verb) (v :| vs) f
     Raw.DefnNoun v (Raw.Noun noun vs) ->
         pure $ \asms f -> Sem.DefnPredicate asms (Sem.PredicateNoun noun) (v :| vs) f
@@ -587,66 +587,66 @@ glossProof :: Raw.Proof -> Gloss Sem.Proof
 glossProof = \case
     Raw.Omitted ->
         pure Sem.Omitted
-    Raw.Qed by ->
-        pure (Sem.Qed by)
-    Raw.ByContradiction proof ->
-        Sem.ByContradiction <$> glossProof proof
-    Raw.BySetInduction mt proof ->
-        Sem.BySetInduction <$> mmt' <*> glossProof proof
+    Raw.Qed pos by ->
+        pure (Sem.Qed pos by)
+    Raw.ByContradiction pos proof ->
+        Sem.ByContradiction pos <$> glossProof proof
+    Raw.BySetInduction pos mt proof ->
+        Sem.BySetInduction pos <$> 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
-    Raw.ByOrdInduction proof ->
-        Sem.ByOrdInduction <$> glossProof proof
-    Raw.ByCase cases -> Sem.ByCase <$> glossCase `each` cases
-    Raw.Have _ms s by proof -> case s of
+    Raw.ByOrdInduction pos proof ->
+        Sem.ByOrdInduction pos <$> glossProof proof
+    Raw.ByCase pos cases -> Sem.ByCase pos <$> glossCase `each` cases
+    Raw.Have pos _ms s by proof -> case s of
         -- Pragmatics: an existential @Have@ implicitly
         -- introduces the witness and is interpreted as a @Take@ construct.
-        Raw.SymbolicExists vs bound suchThat -> do
+        Raw.SymbolicExists pos vs bound suchThat -> do
             bound' <- glossBound bound
             suchThat' <- glossStmt suchThat
             proof' <- glossProof proof
-            pure (Sem.Take vs (Sem.makeConjunction (suchThat' : bound' (toList vs))) by proof')
+            pure (Sem.Take pos vs (Sem.makeConjunction (suchThat' : bound' (toList vs))) by proof')
         _otherwise ->
-            Sem.Have <$> glossStmt s <*> pure by <*> glossProof proof
-    Raw.Assume stmt proof ->
-        Sem.Assume <$> glossStmt stmt <*> glossProof proof
-    Raw.FixSymbolic xs bound proof -> do
+            Sem.Have pos <$> glossStmt s <*> pure by <*> glossProof proof
+    Raw.Assume pos stmt proof ->
+        Sem.Assume pos <$> glossStmt stmt <*> glossProof proof
+    Raw.FixSymbolic pos xs bound proof -> do
         bound' <- glossBound bound
         proof' <- glossProof proof
-        pure (Sem.Fix xs (Sem.makeConjunction (bound' (toList xs))) proof')
-    Raw.FixSuchThat xs stmt proof -> do
+        pure (Sem.Fix pos xs (Sem.makeConjunction (bound' (toList xs))) proof')
+    Raw.FixSuchThat pos xs stmt proof -> do
         stmt' <- glossStmt stmt
         proof' <- glossProof proof
-        pure (Sem.Fix xs stmt' proof')
-    Raw.TakeVar vs bound suchThat by proof -> do
+        pure (Sem.Fix pos xs stmt' proof')
+    Raw.TakeVar pos vs bound suchThat by proof -> do
         bound' <- glossBound bound
         suchThat' <- glossStmt suchThat
         proof' <- glossProof proof
-        pure (Sem.Take vs (Sem.makeConjunction (suchThat' : bound' (toList vs))) by proof')
-    Raw.TakeNoun np by proof -> do
+        pure (Sem.Take pos vs (Sem.makeConjunction (suchThat' : bound' (toList vs))) by proof')
+    Raw.TakeNoun pos np by proof -> do
         (vs, constraints) <- glossNPList np
         proof' <- glossProof proof
-        pure $ Sem.Take vs constraints by proof'
-    Raw.Subclaim subclaim subproof proof ->
-        Sem.Subclaim <$> glossStmt subclaim <*> glossProof subproof <*> glossProof proof
-    Raw.Suffices reduction by proof ->
-        Sem.Suffices <$> glossStmt reduction <*> pure by <*> glossProof proof
-    Raw.Define var term proof ->
-        Sem.Define var <$> glossExpr term <*> glossProof proof
-    Raw.DefineFunction funVar argVar valueExpr domVar domExpr proof ->
+        pure $ Sem.Take pos vs constraints by proof'
+    Raw.Subclaim pos subclaim subproof proof ->
+        Sem.Subclaim pos <$> glossStmt subclaim <*> glossProof subproof <*> glossProof proof
+    Raw.Suffices pos reduction by proof ->
+        Sem.Suffices pos <$> glossStmt reduction <*> pure by <*> glossProof proof
+    Raw.Define pos var term proof ->
+        Sem.Define pos var <$> glossExpr term <*> glossProof proof
+    Raw.DefineFunction pos funVar argVar valueExpr domVar domExpr proof ->
         if domVar == argVar
-            then Sem.DefineFunction funVar argVar <$> glossExpr valueExpr <*> glossExpr domExpr <*> glossProof proof
+            then Sem.DefineFunction pos funVar argVar <$> glossExpr valueExpr <*> glossExpr domExpr <*> glossProof proof
             else error "mismatched variables in function definition."
 
-    Raw.DefineFunctionLocal funVar domVar ranExpr funVar2 argVar definitions proof -> do
+    Raw.DefineFunctionLocal pos funVar domVar ranExpr funVar2 argVar definitions proof -> do
         if funVar == funVar2
-            then Sem.DefineFunctionLocal funVar argVar domVar <$> glossExpr ranExpr <*> (glossLocalFunctionExprDef `each` definitions) <*> glossProof proof
+            then Sem.DefineFunctionLocal pos funVar argVar domVar <$> glossExpr ranExpr <*> (glossLocalFunctionExprDef `each` definitions) <*> glossProof proof
             else error "missmatched function names"
-    Raw.Calc calcQuant calc proof ->
-        Sem.Calc <$> glossCalcQuantifier calcQuant <*> glossCalc calc <*> glossProof proof
+    Raw.Calc pos calcQuant calc proof ->
+        Sem.Calc pos <$> glossCalcQuantifier calcQuant <*> glossCalc calc <*> glossProof proof
 
 glossCalcQuantifier :: Maybe Raw.CalcQuantifier -> Gloss Sem.CalcQuantifier
 glossCalcQuantifier Nothing = pure Sem.CalcUnquantified
@@ -680,9 +680,9 @@ glossCalc = \case
 
 glossSignature :: Raw.Signature -> Gloss Sem.Signature
 glossSignature sig = case sig of
-    Raw.SignatureAdj v (Raw.Adj adj vs) ->
+    Raw.SignatureAdj v (Raw.Adj pos adj vs) ->
         pure $ Sem.SignaturePredicate (Sem.PredicateAdj adj) (v :| vs)
-    Raw.SignatureVerb v (Raw.Verb verb vs) ->
+    Raw.SignatureVerb v (Raw.Verb pos verb vs) ->
         pure $ Sem.SignaturePredicate (Sem.PredicateVerb verb) (v :| vs)
     Raw.SignatureNoun v (Raw.Noun noun vs) ->
         pure $ Sem.SignaturePredicate (Sem.PredicateNoun noun) (v :| vs)
@@ -717,15 +717,15 @@ annotateCarrierFormula lbl = \case
 
 glossAbbreviation :: Raw.Abbreviation -> Gloss Sem.Abbreviation
 glossAbbreviation = \case
-    Raw.AbbreviationAdj x (Raw.Adj adj xs) stmt ->
+    Raw.AbbreviationAdj x (Raw.Adj pos adj xs) stmt ->
         makeAbbrStmt (Sem.SymbolPredicate (Sem.PredicateAdj adj)) (x : xs) stmt
-    Raw.AbbreviationVerb x (Raw.Verb verb xs) stmt ->
+    Raw.AbbreviationVerb x (Raw.Verb pos verb xs) stmt ->
         makeAbbrStmt (Sem.SymbolPredicate (Sem.PredicateVerb verb)) (x : xs) stmt
     Raw.AbbreviationNoun x (Raw.Noun noun xs) stmt ->
         makeAbbrStmt (Sem.SymbolPredicate (Sem.PredicateNoun noun)) (x : xs) stmt
     Raw.AbbreviationRel x rel params y stmt ->
         makeAbbrStmt (Sem.SymbolPredicate (Sem.PredicateRelation rel)) (params <> [x, y]) stmt
-    Raw.AbbreviationFun (Raw.Fun fun xs) t ->
+    Raw.AbbreviationFun (Raw.Fun pos fun xs) t ->
         makeAbbrTerm (Sem.SymbolFun fun) xs t
     Raw.AbbreviationEq (Raw.SymbolPattern op xs) e ->
         makeAbbrExpr (Sem.SymbolMixfix op) xs e
diff --git a/source/Report/Location.hs b/source/Report/Location.hs
new file mode 100644
index 0000000..bcc575e
--- /dev/null
+++ b/source/Report/Location.hs
@@ -0,0 +1,26 @@
+module Report.Location where
+
+import Base
+import Text.Megaparsec.Pos
+
+
+
+class Locatable a where
+    locate :: a -> SourcePos
+
+nowhere :: SourcePos
+nowhere = initialPos "Nowhere"
+
+instance Locatable SourcePos where
+    locate = id
+
+instance Locatable a => Locatable [a] where
+    locate []    = nowhere
+    locate (x:_) = locate x
+
+instance Locatable a => Locatable (Maybe a) where
+    locate Nothing  = nowhere
+    locate (Just x) = locate x
+
+instance Locatable a => Locatable (NonEmpty a) where
+    locate (x :| _) = locate x
diff --git a/source/Syntax/Abstract.hs b/source/Syntax/Abstract.hs
index ebbf9e9..00e43ca 100644
--- a/source/Syntax/Abstract.hs
+++ b/source/Syntax/Abstract.hs
@@ -3,7 +3,8 @@
 {-# LANGUAGE GADTs #-}
 {-# LANGUAGE NoImplicitPrelude #-}
 {-# LANGUAGE StandaloneDeriving #-}
-
+{-# LANGUAGE OverloadedRecordDot #-}
+{-# LANGUAGE DuplicateRecordFields #-}
 
 -- | Data types for the abstract syntax tree and helper functions
 -- for constructing the lexicon.
@@ -18,6 +19,7 @@ module Syntax.Abstract
 import Base
 import Syntax.LexicalPhrase (LexicalPhrase, SgPl(..), unsafeReadPhraseSgPl, unsafeReadPhrase)
 import Syntax.Token (Token(..))
+import Report.Location
 
 import Text.Earley.Mixfix (Holey)
 import Data.Text qualified as Text
@@ -32,6 +34,8 @@ data VarSymbol
 instance IsString VarSymbol where
     fromString v = NamedVar $ Text.pack v
 
+instance Locatable VarSymbol where
+    locate _ = nowhere -- TODO more info?
 
 data Expr
     = ExprVar VarSymbol
@@ -199,7 +203,7 @@ data Nameless a = Nameless deriving (Show, Eq, Ord)
 -- e.g. /@even@/, /@continuous@/, and /@σ-finite@/.
 type AdjL = AdjLOf Term
 data AdjLOf a
-    = AdjL LexicalPhrase [a]
+    = AdjL SourcePos LexicalPhrase [a]
     deriving (Show, Eq, Ord)
 
 
@@ -210,29 +214,32 @@ data AdjLOf a
 -- by an additional such-that phrase.
 type AdjR = AdjROf Term
 data AdjROf a
-    = AdjR LexicalPhrase [a]
+    = AdjR SourcePos LexicalPhrase [a]
     | AttrRThat VerbPhrase
     deriving (Show, Eq, Ord)
 
+instance Locatable (AdjROf a) where
+    locate (AdjR p _ _) = p
+    locate (AttrRThat vp) = nowhere -- TODO
 
 -- | Adjectives for parts of the AST where adjectives are not used
 -- to modify nouns and the L/R distinction does not matter, such as
 -- when then are used together with a copula (like /@n is even@/).
 type Adj = AdjOf Term
 data AdjOf a
-    = Adj LexicalPhrase [a]
+    = Adj SourcePos LexicalPhrase [a]
     deriving (Show, Eq, Ord)
 
 
 type Verb = VerbOf Term
 data VerbOf a
-    = Verb (SgPl LexicalPhrase) [a]
+    = Verb SourcePos (SgPl LexicalPhrase) [a]
     deriving (Show, Eq, Ord)
 
 
 type Fun = FunOf Term
 data FunOf a
-    = Fun (SgPl LexicalPhrase) [a]
+    = Fun {pos :: SourcePos, phrase :: SgPl LexicalPhrase, funArgs :: [a]}
     deriving (Show, Eq, Ord)
 
 
@@ -259,35 +266,49 @@ data Term
     -- ^ A symbolic expression.
     | TermFun Fun
     -- ^ Definite noun phrase, e.g. /@the derivative of $f$@/.
-    | TermIota VarSymbol Stmt
+    | TermIota SourcePos VarSymbol Stmt
     -- ^ Definite descriptor, e.g. /@an $x$ such that ...@//
-    | TermQuantified Quantifier (NounPhrase Maybe)
+    | TermQuantified Quantifier SourcePos (NounPhrase Maybe)
     -- ^ Indefinite quantified notion, e.g. /@every even integer that divides $k$ ...@/.
     deriving (Show, Eq, Ord)
 
+instance Locatable Term where
+    locate :: Term -> SourcePos
+    locate (TermExpr _) = nowhere -- TODO
+    locate (TermFun f) = f.pos
+    locate (TermIota p _ _) = p
+    locate (TermQuantified _ p _) = p
+
 
 data Stmt
-    = StmtFormula Formula -- ^ E.g.: /@We have \<Formula\>@/.
-    | StmtVerbPhrase (NonEmpty Term) VerbPhrase -- ^ E.g.: /@\<Term\> and \<Term\> \<verb\>@/.
-    | StmtNoun (NonEmpty Term) (NounPhrase Maybe) -- ^ E.g.: /@\<Term\> is a(n) \<NP\>@/.
-    | StmtStruct Term StructPhrase
-    | StmtNeg Stmt -- ^ E.g.: /@It is not the case that \<Stmt\>@/.
-    | StmtExists (NounPhrase []) -- ^ E.g.: /@There exists a(n) \<NP\>@/.
-    | StmtConnected Connective Stmt Stmt
-    | StmtQuantPhrase QuantPhrase Stmt
-    | SymbolicQuantified Quantifier (NonEmpty VarSymbol) Bound (Maybe Stmt) Stmt
+    = StmtFormula {formula :: Formula} -- ^ E.g.: /@We have \<Formula\>@/.
+    | StmtVerbPhrase {args :: NonEmpty Term, verb :: VerbPhrase} -- ^ E.g.: /@\<Term\> and \<Term\> \<verb\>@/.
+    | StmtNoun {pos :: SourcePos, args :: NonEmpty Term, noun :: (NounPhrase Maybe)} -- ^ E.g.: /@\<Term\> is a(n) \<NP\>@/.
+    | StmtStruct {pos :: SourcePos, arg :: Term, struct :: StructPhrase}
+    | StmtNeg {pos :: SourcePos, stmt :: Stmt} -- ^ E.g.: /@It is not the case that \<Stmt\>@/.
+    | StmtExists {pos :: SourcePos, np :: NounPhrase []} -- ^ E.g.: /@There exists a(n) \<NP\>@/.
+    | StmtConnected {conn :: Connective, mpos :: Maybe SourcePos, stmt1 :: Stmt, stmt2 :: Stmt}
+    | StmtQuantPhrase {pos :: SourcePos, qp :: QuantPhrase, stmt :: Stmt}
+    | SymbolicQuantified {pos :: SourcePos, quant :: Quantifier, xs :: NonEmpty VarSymbol, b :: Bound, suchThat :: Maybe Stmt, stmt :: Stmt}
     deriving (Show, Eq, Ord)
 
+instance Locatable Stmt where
+    locate :: Stmt -> SourcePos
+    locate (StmtFormula _) = nowhere -- TODO
+    locate StmtConnected{mpos = Nothing, stmt1 = s} = locate s
+    locate StmtVerbPhrase{args = a :| _} = locate a
+    locate s = s.pos
+
 data Bound = Unbounded | Bounded Sign Relation Expr deriving (Show, Eq, Ord)
 
-pattern SymbolicForall :: NonEmpty VarSymbol -> Bound -> Maybe Stmt -> Stmt -> Stmt
-pattern SymbolicForall vs bound suchThat have = SymbolicQuantified Universally vs bound suchThat have
+pattern SymbolicForall :: SourcePos -> NonEmpty VarSymbol -> Bound -> Maybe Stmt -> Stmt -> Stmt
+pattern SymbolicForall pos vs bound suchThat have = SymbolicQuantified pos Universally vs bound suchThat have
 
-pattern SymbolicExists :: NonEmpty VarSymbol -> Bound -> Stmt -> Stmt
-pattern SymbolicExists vs bound suchThat = SymbolicQuantified Existentially vs bound Nothing suchThat
+pattern SymbolicExists :: SourcePos -> NonEmpty VarSymbol -> Bound -> Stmt -> Stmt
+pattern SymbolicExists pos vs bound suchThat = SymbolicQuantified pos Existentially vs bound Nothing suchThat
 
-pattern SymbolicNotExists :: NonEmpty VarSymbol -> Bound -> Stmt -> Stmt
-pattern SymbolicNotExists vs bound suchThat = StmtNeg (SymbolicExists vs bound suchThat)
+makeSymbolicNotExists :: SourcePos -> NonEmpty VarSymbol -> Bound -> Stmt -> Stmt
+makeSymbolicNotExists p vs bound st = StmtNeg p (SymbolicExists p vs bound st)
 
 data Asm
     = AsmSuppose Stmt
@@ -344,32 +365,32 @@ data CalcQuantifier
 
 data Proof
     = Omitted
-    | Qed Justification
+    | Qed (Maybe SourcePos) Justification
     -- ^ Ends of a proof, leaving automation to discharge the current goal using the given justification.
-    | ByCase [Case]
-    | ByContradiction Proof
-    | BySetInduction (Maybe Term) Proof
+    | ByCase SourcePos [Case]
+    | ByContradiction SourcePos Proof
+    | BySetInduction SourcePos (Maybe Term) Proof
     -- ^ ∈-induction.
-    | ByOrdInduction Proof
+    | ByOrdInduction SourcePos Proof
     -- ^ Transfinite induction for ordinals.
-    | Assume Stmt Proof
-    | FixSymbolic (NonEmpty VarSymbol) Bound Proof
-    | FixSuchThat (NonEmpty VarSymbol) Stmt Proof
-    | Calc (Maybe CalcQuantifier) Calc Proof
+    | Assume SourcePos Stmt Proof
+    | FixSymbolic SourcePos (NonEmpty VarSymbol) Bound Proof
+    | FixSuchThat SourcePos (NonEmpty VarSymbol) Stmt Proof
+    | Calc SourcePos (Maybe CalcQuantifier) Calc Proof
     -- ^ Simplify goals that are implications or disjunctions.
-    | TakeVar (NonEmpty VarSymbol) Bound Stmt Justification Proof
-    | TakeNoun (NounPhrase []) Justification Proof
-    | Have (Maybe Stmt) Stmt Justification Proof
+    | TakeVar SourcePos (NonEmpty VarSymbol) Bound Stmt Justification Proof
+    | TakeNoun SourcePos (NounPhrase []) Justification Proof
+    | Have SourcePos (Maybe Stmt) Stmt Justification Proof
     -- ^ /@Since \<stmt\>, we have \<stmt\> by \<ref\>.@/
-    | Suffices Stmt Justification Proof
+    | Suffices SourcePos Stmt Justification Proof
     -- ^ /@It suffices to show that [...]. [...]@/
-    | Subclaim Stmt Proof Proof
+    | Subclaim SourcePos Stmt Proof Proof
     -- ^ A claim is a sublemma with its own proof:
     --  /@Show \<goal stmt\>. \<steps\>. \<continue other proof\>.@/
-    | Define VarSymbol Expr Proof
+    | Define SourcePos VarSymbol Expr Proof
     -- ^ Local definition.
     --
-    | DefineFunction VarSymbol VarSymbol Expr VarSymbol Expr Proof
+    | DefineFunction SourcePos VarSymbol VarSymbol Expr VarSymbol Expr Proof
     -- ^ Local function definition, e.g. /@Let $f(x) = e$ for $x\\in d$@/.
     -- The first 'VarSymbol' is the newly defined symbol, the second one is the argument.
     -- The first 'Expr' is the value, the final variable and expr specify a bound (the domain of the function).
@@ -377,7 +398,7 @@ data Proof
 
 
 
-    | DefineFunctionLocal VarSymbol VarSymbol Expr VarSymbol VarSymbol (NonEmpty (Expr, Formula)) Proof
+    | DefineFunctionLocal SourcePos VarSymbol VarSymbol Expr VarSymbol VarSymbol (NonEmpty (Expr, Formula)) Proof
     -- ^ Local function definition, but in this case we give the domain and target an the rules for $xs$ in some sub domains.
     --
     deriving (Show, Eq, Ord)
diff --git a/source/Syntax/Adapt.hs b/source/Syntax/Adapt.hs
index 77f80d6..fbfbdef 100644
--- a/source/Syntax/Adapt.hs
+++ b/source/Syntax/Adapt.hs
@@ -32,7 +32,7 @@ scanChunk ltoks =
         Located{startPos = pos, unLocated = BeginEnv "abbreviation"} : _ ->
             matchOrErr abbreviation "abbreviation" pos
         Located{startPos = pos, unLocated = (BeginEnv "struct")} :_ ->
-            matchOrErr struct "struct definition" pos
+            matchOrErr structRE "struct definition" pos
         Located{startPos = pos, unLocated = (BeginEnv "inductive")} :_ ->
             matchOrErr inductive "inductive definition" pos
         _ -> []
@@ -66,9 +66,9 @@ definition ::  RE Token [ScannedLexicalItem]
 definition = do
     sym (BeginEnv "definition")
     few notEndOfLexicalEnvToken
-    m <- label
+    m <- labelRE
     few anySym
-    lexicalItem <- head
+    lexicalItem <- headRE
     few anySym
     sym (EndEnv "definition")
     skipUntilNextLexicalEnv
@@ -78,9 +78,9 @@ abbreviation ::  RE Token [ScannedLexicalItem]
 abbreviation = do
     sym (BeginEnv "abbreviation")
     few anySym
-    m <- label
+    m <- labelRE
     few anySym
-    lexicalItem <- head
+    lexicalItem <- headRE
     few anySym
     sym (EndEnv "abbreviation")
     skipUntilNextLexicalEnv
@@ -90,9 +90,9 @@ signatureExtension ::  RE Token [ScannedLexicalItem]
 signatureExtension = do
     sym (BeginEnv "signature")
     few notEndOfLexicalEnvToken
-    m <- label
+    m <- labelRE
     few anySym
-    lexicalItem <- head
+    lexicalItem <- headRE
     few anySym
     sym (EndEnv "signature")
     skipUntilNextLexicalEnv
@@ -102,7 +102,7 @@ signatureExtensionAtom ::  RE Token [ScannedLexicalItem]
 signatureExtensionAtom = do
     sym (BeginEnv "signatureatom")
     few notEndOfLexicalEnvToken
-    m <- label
+    m <- labelRE
     few anySym
     lexicalItem <- sigPred
     few anySym
@@ -110,22 +110,22 @@ signatureExtensionAtom = do
     skipUntilNextLexicalEnv
     pure [lexicalItem m]
 
-label :: RE Token Marker
-label = msym \case
+labelRE :: RE Token Marker
+labelRE = msym \case
     Label m -> Just (Marker m)
     _ -> Nothing
 
 -- | 'RE' that matches the head of a definition.
-head :: RE Token (Marker -> ScannedLexicalItem)
+headRE :: RE Token (Marker -> ScannedLexicalItem)
 -- Note that @<|>@ is left biased for 'RE', so we can just
 -- place 'adj' before 'verb' and do not have to worry about
 -- overlapping patterns.
-head = ScanNoun <$> noun
-    <|> ScanAdj <$> adj
-    <|> ScanVerb <$> verb
-    <|> ScanFun <$> fun
-    <|> ScanRelationSymbol . fst <$> relationSymbol
-    <|> ScanFunctionSymbol <$> functionSymbol
+headRE = ScanNoun <$> nounRE
+    <|> ScanAdj <$> adjRE
+    <|> ScanVerb <$> verbRE
+    <|> ScanFun <$> funRE
+    <|> ScanRelationSymbol . fst <$> relationSymbolRE
+    <|> ScanFunctionSymbol <$> functionSymbolRE
     <|> ScanPrefixPredicate <$> prefixPredicate
 
 sigPred :: RE Token (Marker -> ScannedLexicalItem)
@@ -137,7 +137,7 @@ inductive :: RE Token [ScannedLexicalItem]
 inductive = do
     sym (BeginEnv "inductive")
     few notEndOfLexicalEnvToken
-    m <- label
+    m <- labelRE
     few anySym
     lexicalItem <- functionSymbolInductive
     few anySym
@@ -145,11 +145,11 @@ inductive = do
     skipUntilNextLexicalEnv
     pure [ScanFunctionSymbol lexicalItem m]
 
-struct :: RE Token [ScannedLexicalItem]
-struct = do
+structRE :: RE Token [ScannedLexicalItem]
+structRE = do
     sym (BeginEnv "struct")
     few anySym
-    m <- label
+    m <- labelRE
     few anySym
     lexicalItem <- ScanStructNoun . toLexicalPhrase <$> (an *> structPat <* math var)
     few anySym
@@ -172,20 +172,20 @@ structOp = do
     op <- math command
     pure (ScanStructOp op)
 
-noun :: RE Token LexicalPhrase
-noun = toLexicalPhrase <$> (math var *> is *> an *> pat <* iff)
+nounRE :: RE Token LexicalPhrase
+nounRE = toLexicalPhrase <$> (math var *> is *> an *> pat <* iff)
 
-adj :: RE Token LexicalPhrase
-adj = toLexicalPhrase <$> (math var *> is *> pat <* iff)
+adjRE :: RE Token LexicalPhrase
+adjRE = toLexicalPhrase <$> (math var *> is *> pat <* iff)
 
-verb :: RE Token LexicalPhrase
-verb = toLexicalPhrase <$> (math var *> pat <* iff)
+verbRE :: RE Token LexicalPhrase
+verbRE = toLexicalPhrase <$> (math var *> pat <* iff)
 
-fun :: RE Token LexicalPhrase
-fun = toLexicalPhrase <$> (the *> pat <* (is <|> comma))
+funRE :: RE Token LexicalPhrase
+funRE = toLexicalPhrase <$> (the *> pat <* (is <|> comma))
 
-relationSymbol :: RE Token (RelationSymbol, Int)
-relationSymbol = do
+relationSymbolRE :: RE Token (RelationSymbol, Int)
+relationSymbolRE = do
     beginMath
     var
     rel <- symbol
@@ -200,8 +200,8 @@ relationSymbol = do
             vars <- many (sym InvisibleBraceL *> var <* sym InvisibleBraceR)
             pure (length vars)
 
-functionSymbol :: RE Token FunctionSymbol
-functionSymbol = do
+functionSymbolRE :: RE Token FunctionSymbol
+functionSymbolRE = do
     sym (BeginEnv "math")
     toks <- few nonDefinitionKeyword
     sym (Symbol "=")
diff --git a/source/Syntax/Concrete.hs b/source/Syntax/Concrete.hs
index ada6227..00f0574 100644
--- a/source/Syntax/Concrete.hs
+++ b/source/Syntax/Concrete.hs
@@ -10,6 +10,7 @@ import Syntax.Abstract
 import Syntax.Concrete.Keywords
 import Syntax.Lexicon (Lexicon(..), lexiconAdjs, splitOnVariableSlot)
 import Syntax.Token
+import Report.Location
 
 import Data.HashSet qualified as HS
 import Data.List.NonEmpty qualified as NonEmpty
@@ -172,10 +173,10 @@ grammar lexicon@Lexicon{..} = mdo
 
     termExpr       <- rule $ TermExpr <$> math expr
     termFun        <- rule $ TermFun <$> (optional _the *> fun)
-    termIota       <- rule $ TermIota <$> (_the *> var) <* _suchThat <*> stmt
-    termAll        <- rule $ TermQuantified Universally <$> (_every *> nounPhraseMay)
-    termSome       <- rule $ TermQuantified Existentially <$> (_some *> nounPhraseMay)
-    termNo         <- rule $ TermQuantified Nonexistentially <$> (_no *> nounPhraseMay)
+    termIota       <- rule $ TermIota <$> _the <*> var <* _suchThat <*> stmt
+    termAll        <- rule $ TermQuantified Universally <$> _every <*> nounPhraseMay
+    termSome       <- rule $ TermQuantified Existentially <$> _some <*> nounPhraseMay
+    termNo         <- rule $ TermQuantified Nonexistentially <$> _no <*> nounPhraseMay
     termQuantified <- rule $ termAll <|> termSome <|> termNo
     term           <- rule $ termExpr <|> termFun <|> termQuantified <|> termIota
 
@@ -186,51 +187,79 @@ grammar lexicon@Lexicon{..} = mdo
     stmtVerbSg    <- rule $ StmtVerbPhrase <$> singletonTerm <*> verbPhraseSg
     stmtVerbPl    <-rule $ StmtVerbPhrase <$> andList1 term <*> verbPhrasePl
     stmtVerb      <- rule $ stmtVerbSg <|> stmtVerbPl
-    stmtNounIs    <- rule $ StmtNoun <$> singletonTerm <* _is <* _an <*> nounPhrase
-    stmtNounAre   <- rule $ StmtNoun <$> (nonemptyTerms <* _are) <*> nounPhrasePlMay
-    stmtNounIsNot <- rule $ StmtNeg <$> (StmtNoun <$> singletonTerm <* _is <* _not <* _an <*> nounPhrase)
-    stmtNounAreNot <- rule $ StmtNeg <$> (StmtNoun <$> nonemptyTerms <* (_are *> _not) <*> nounPhrasePlMay)
+    stmtNounIs    <- rule do
+        ts <- singletonTerm
+        np <- _is *> _an *> nounPhrase
+        pure let t :| _ = ts in (StmtNoun (locate t) ts np)
+    stmtNounAre   <- rule do
+        ts <- nonemptyTerms <* _are
+        np <- nounPhrasePlMay
+        pure let t :| _ = ts in (StmtNoun (locate t) ts np)
+    stmtNounIsNot <- rule do
+        ts <- singletonTerm
+        np <- _is *> _not *> _an *> nounPhrase
+        pure let t :| _ = ts in (StmtNeg (locate t) (StmtNoun (locate t) ts np))
+    stmtNounAreNot <- rule do
+        ts <- nonemptyTerms
+        np <- _are *> _not *> nounPhrasePlMay
+        pure let t :| _ = ts in (StmtNeg (locate t) (StmtNoun (locate t) ts np))
     stmtNoun      <- rule $ stmtNounIs <|> stmtNounIsNot <|> stmtNounAre <|> stmtNounAreNot
-    stmtStruct    <- rule $ StmtStruct <$> (term <* _is <* _an) <*> structNounNameless
-    stmtExists    <- rule $ StmtExists <$> (_exists *> _an *> nounPhrase')
-    stmtExist     <- rule $ StmtExists <$> (_exist *> nounPhrasePl)
-    stmtExistsNot <- rule $ StmtNeg . StmtExists <$> (_exists *> _no *> nounPhrase')
+    stmtStruct    <- rule do
+        t <- term
+        s <- _is *> _an *> structNounNameless
+        pure (StmtStruct (locate t) t s)
+    stmtExists    <- rule $ StmtExists <$> _exists <*> (_an *> nounPhrase')
+    stmtExist     <- rule $ StmtExists <$> _exist <*> nounPhrasePl
+    stmtExistsNot <- rule do
+        p <- _exists *> _no
+        np <- nounPhrase'
+        pure (StmtNeg p (StmtExists p np))
     stmtFormula   <- rule $ StmtFormula <$> math formula
-    stmtFormualNeg <- rule $ StmtNeg . StmtFormula <$> (_not *> math formula)
+    stmtFormualNeg <- rule do
+        p <- _not
+        phi <- math formula
+        pure (StmtNeg p (StmtFormula phi))
     stmtBot       <- rule $ StmtFormula (PropositionalConstant IsBottom) <$ _contradiction
     stmt'         <- rule $ stmtVerb <|> stmtNoun <|> stmtStruct <|> stmtFormula <|> stmtFormualNeg <|> stmtBot
-    stmtOr  <- rule $ stmt'   <|> (StmtConnected Disjunction <$> stmt'   <* _or  <*> stmt)
-    stmtAnd <- rule $ stmtOr  <|> (StmtConnected Conjunction <$> stmtOr  <* _and <*> stmt)
-    stmtIff <- rule $ stmtAnd <|> (StmtConnected Equivalence <$> stmtAnd <* _iff <*> stmt)
-    stmtIf  <- rule $ StmtConnected Implication <$> (_if *> stmt) <* optional _comma <* _then <*> stmt
-    stmtXor <- rule $ StmtConnected ExclusiveOr <$> (_either *> stmt) <* _or <*> stmt
-    stmtNor <- rule $ StmtConnected NegatedDisjunction <$> (_neither *> stmt) <* _nor <*> stmt
-    stmtNeg <- rule $ StmtNeg <$> (_itIsWrong *> stmt)
+    stmtOr  <- rule $ stmt'   <|> (StmtConnected Disjunction Nothing <$> stmt'   <* _or  <*> stmt)
+    stmtAnd <- rule $ stmtOr  <|> (StmtConnected Conjunction Nothing <$> stmtOr  <* _and <*> stmt)
+    stmtIff <- rule $ stmtAnd <|> (StmtConnected Equivalence Nothing <$> stmtAnd <* _iff <*> stmt)
+    stmtIf  <- rule $ StmtConnected Implication <$> (Just <$> _if) <*> stmt <* optional _comma <* _then <*> stmt
+    stmtXor <- rule $ StmtConnected ExclusiveOr <$> (Just <$>_either) <*> stmt <* _or <*> stmt
+    stmtNor <- rule $ StmtConnected NegatedDisjunction <$> (Just <$> _neither) <*> stmt <* _nor <*> stmt
+    stmtNeg <- rule $ StmtNeg <$> _itIsWrong <*> stmt
 
-    stmtQuantPhrase <- rule $ StmtQuantPhrase <$> (_for *> quant) <* optional _comma <* optional _have <*> stmt
+    stmtQuantPhrase <- rule $ StmtQuantPhrase <$> _for <*> quant <* optional _comma <* optional _have <*> stmt
 
     suchStmt <- rule $ _suchThat *> stmt <* optional _comma
 
    -- Symbolic quantifications with or without generalized bounds.
-    symbolicForall <- rule $ SymbolicForall
-        <$> ((_forAll <|> _forEvery) *> beginMath *> varSymbols)
-        <*> maybeBounded <* endMath
-        <*> optional suchStmt
-        <* optional _have <*> stmt
-    symbolicExists <- rule $ SymbolicExists
-        <$> ((_exists <|> _exist) *> beginMath *> varSymbols)
-        <*> maybeBounded <* endMath
-        <*> ((_suchThat *> stmt) <|> pure (StmtFormula (PropositionalConstant IsTop)))
-    symbolicNotExists <- rule $ SymbolicNotExists
-        <$> (_exists *> _no *> beginMath *> varSymbols)
-        <*> maybeBounded <* endMath
-        <* _suchThat <*> stmt
+    symbolicForall <- rule do
+        p <- _forAll <|> _forEvery
+        xs <- beginMath *> varSymbols
+        b <- maybeBounded <* endMath
+        ms <- optional suchStmt
+        s <- optional _have *> stmt
+        pure (SymbolicForall p xs b ms s)
+    symbolicExists <- rule do
+        p <- _exists <|> _exist
+        xs <- beginMath *> varSymbols
+        b <- maybeBounded <* endMath
+        s <- (_suchThat *> stmt) <|> pure (StmtFormula (PropositionalConstant IsTop))
+        pure (SymbolicExists p xs b s)
+    symbolicNotExists <- rule do
+        p <- _exists *> _no
+        xs <- beginMath *> varSymbols
+        b <- maybeBounded <* endMath
+        s <- _suchThat *> stmt
+        pure (makeSymbolicNotExists p xs b s)
     symbolicBound <- rule $ Bounded <$> relationSign <*> relation <*> expr
     maybeBounded <- rule (pure Unbounded <|> symbolicBound)
 
     symbolicQuantified <- rule $ symbolicForall <|> symbolicExists <|> symbolicNotExists
 
-    stmt <- rule $ asum [stmtNeg, stmtIf, stmtXor, stmtNor, stmtExists, stmtExist, stmtExistsNot, stmtQuantPhrase, stmtIff, symbolicQuantified] <?> "a statement"
+    stmt :: Prod r Text (Located Token) Stmt <- rule $ asum [stmtNeg, stmtIf, stmtXor, stmtNor, stmtExists, stmtExist, stmtExistsNot, stmtQuantPhrase, stmtIff, symbolicQuantified] <?> "a statement"
+
 
     asmLetIn        <- rule $ uncurry AsmLetIn <$> (_let *> math typing)
     asmLetNoun      <- rule $ AsmLetNoun <$> (_let *> fmap pure var <* (_be <|> _denote) <* _an) <*> nounPhrase
@@ -315,10 +344,10 @@ grammar lexicon@Lexicon{..} = mdo
     justificationLocal <- rule $ JustificationLocal <$ (_by *> (_assumption <|> _definition))
     justification <- rule (justificationSet <|> justificationRef <|> justificationLocal <|> pure JustificationEmpty)
 
-    trivial          <- rule $ Qed JustificationEmpty <$ _trivial <* _dot
+    trivial          <- rule $ Qed . Just <$> _trivial <* _dot <*> pure JustificationEmpty
     omitted          <- rule $ Omitted <$ _omitted <* _dot
-    qedJustified     <- rule $ Qed <$> (_follows *> justification <* _dot)
-    qed              <- rule $ qedJustified <|> trivial <|> omitted <|> pure (Qed JustificationEmpty)
+    qedJustified     <- rule $ Qed . Just <$> _follows <*> (justification <* _dot)
+    qed              <- rule $ qedJustified <|> trivial <|> omitted <|> pure (Qed Nothing JustificationEmpty)
 
     let alignedEq = symbol "&=" <?> "\"&=\""
     explanation <- rule $ (text justification) <|> pure JustificationEmpty
@@ -330,71 +359,56 @@ grammar lexicon@Lexicon{..} = mdo
     biconditionals <- rule $ Biconditionals <$> formula <*> (many1 biconditionalItem) <* optional _dot
 
 
-    calcQuantifier <- rule $ CalcQuantifier <$>
-        ((_forAll <|> _forEvery) *> beginMath *> varSymbols)
-        <*> maybeBounded <* endMath
-        <*> optional suchStmt
-        <* optional _have
+    calcQuantifier <- rule do
+        pos <- _forAll <|> _forEvery
+        xs <- beginMath *> varSymbols
+        mb <- maybeBounded <* endMath
+        st <- optional suchStmt
+        optional _have
+        pure (pos, CalcQuantifier xs mb st)
 
-    calc  <- rule $ Calc <$> optional calcQuantifier <*> align (equations <|> biconditionals) <*> proof
+    calc <- rule do
+        mquant <- optional calcQuantifier
+        psteps <- align (equations <|> biconditionals)
+        pf <- proof
+        pure let (pos2, steps) = psteps in case mquant of
+            Nothing -> Calc pos2 Nothing steps pf
+            Just (pos, q) -> Calc pos (Just q) steps pf
 
     caseOf           <- rule $ command "caseOf" *> token InvisibleBraceL *> stmt <* _dot <* token InvisibleBraceR
-    byCases          <- rule $ ByCase <$> env_ "byCase" (many1_ (Case <$> caseOf <*> proof))
-    byContradiction  <- rule $ ByContradiction <$ _suppose <* _not <* _dot <*> proof
-    bySetInduction   <- rule $ BySetInduction <$> proofBy (_in *> word "-induction" *> optional (word "on" *> term)) <*> proof
-    byOrdInduction   <- rule $ ByOrdInduction <$> proofBy (word "transfinite" *> word "induction" *> proof)
-    assume           <- rule $ Assume <$> (_suppose *> stmt <* _dot) <*> proof
-
-    fixSymbolic      <- rule $ FixSymbolic <$> (_fix *> beginMath *> varSymbols) <*> maybeBounded <* endMath <* _dot <*> proof
-    fixSuchThat      <- rule $ FixSuchThat <$> (_fix *> math varSymbols) <* _suchThat <*> stmt <* _dot <*> proof
+    byCases          <- rule $ uncurry ByCase <$> envPos_ "byCase" (many1_ (Case <$> caseOf <*> proof))
+    byContradiction  <- rule $ ByContradiction <$> _suppose <* _not <* _dot <*> proof
+    bySetInduction   <- rule $ uncurry BySetInduction <$> proofBy (_in *> word "-induction" *> optional (word "on" *> term)) <*> proof
+    byOrdInduction   <- rule $ uncurry ByOrdInduction <$> proofBy (word "transfinite" *> word "induction" *> proof)
+    assume           <- rule $ Assume <$> _suppose <*> (stmt <* _dot) <*> proof
+
+    fixSymbolic      <- rule $ FixSymbolic <$> _fix <*> (beginMath *> varSymbols) <*> maybeBounded <* endMath <* _dot <*> proof
+    fixSuchThat      <- rule $ FixSuchThat <$> _fix <*> math varSymbols <* _suchThat <*> stmt <* _dot <*> proof
     fix              <- rule $ fixSymbolic <|> fixSuchThat
 
-    takeVar          <- rule $ TakeVar <$> (_take *> beginMath *> varSymbols) <*> maybeBounded <* endMath <* _suchThat <*> stmt <*> justification <* _dot <*> proof
-    takeNoun         <- rule $ TakeNoun <$> (_take *> _an *> (nounPhrase' <|> nounPhrasePl)) <*> justification <* _dot <*> proof
+    takeVar          <- rule $ TakeVar <$> _take <*> (beginMath *> varSymbols) <*> maybeBounded <* endMath <* _suchThat <*> stmt <*> justification <* _dot <*> proof
+    takeNoun         <- rule $ TakeNoun <$> _take <*> (_an *> (nounPhrase' <|> nounPhrasePl)) <*> justification <* _dot <*> proof
     take             <- rule $ takeVar <|> takeNoun
-    suffices         <- rule $ Suffices <$> (_sufficesThat *> stmt) <*> (justification <* _dot) <*> proof
-    subclaim         <- rule $ Subclaim <$> (_show *> stmt <* _dot) <*> env_ "subproof" proof <*> proof
-    have             <- rule $ Have <$> optional (_since *> stmt <* _comma <* _have) <* optional _haveIntro <*> stmt <*> justification <* _dot <*> proof
-
-
-    define           <- rule $ Define <$> (_let *> beginMath *> varSymbol <* _eq) <*> expr <* endMath <* _dot <*> proof
-    defineFunction   <- rule $ DefineFunction <$> (_let *> beginMath *> varSymbol) <*> paren varSymbol <* _eq <*>  expr <* endMath <* _for <* beginMath <*> varSymbol <* _in <*> expr <* endMath <* _dot <*> proof
-
-
-
-
-
-
-    -- Define $f $\fromTo{X}{Y} such that,
-    -- Define function $f: X \to Y$,
-    -- \begin{align}
-    --      &x \mapsto 3*x      &,
-    --      &x \mapsto 4*k    &,    \forall k \in \N. x \in \Set{k}
-    -- \end{align}
-    --
+    suffices         <- rule $ Suffices <$> _sufficesThat <*> stmt <*> (justification <* _dot) <*> proof
+    subclaim         <- rule $ Subclaim <$> _show <*> (stmt <* _dot) <*> env_ "subproof" proof <*> proof
+    have             <- rule do
+        msince <- optional ((,) <$> _since <*> stmt <* _comma <* _have)
+        mpos <- optional _haveIntro
+        s <- stmt
+        j <- justification <* _dot
+        pf <- proof
+        pure
+            let pos = case (msince, mpos) of
+                    (Just (p, _), _) -> p
+                    (_, Just p) -> p
+                    _ -> locate s
+            in (Have pos (snd <$> msince) s j pf)
 
-    -- Follwing is the definition right now.
-    -- Define function $f: X \to Y$ such that,
-    -- \begin{cases}
-    --     1 & \text{if } x \in \mathbb{Q}\\
-    --     0 & \text{if } x \in \mathbb{R}\setminus\mathbb{Q}
-    --     3 & \text{else}
-    -- \end{cases}
 
-    functionDefineCase <- rule $ (,) <$> (optional _ampersand *> expr) <*> (_ampersand *> text _if *> formula)
-    defineFunctionLocal <-  rule    $ DefineFunctionLocal
-                                    <$> (_define *> beginMath *> varSymbol)           -- Define $ f
-                                    <*> (_colon *> varSymbol)                           -- : 'var' \to 'var'
-                                    <*> (_to *> expr <* endMath <* _suchThat)
-                                    -- <*> (_suchThat  *> align (many1 ((_ampersand *> varSymbol <* _mapsto) <*> exprApp <*> (_ampersand *> formula))))
-                                    -- <*> (_suchThat  *> align (many1 (varSymbol <* exprApp <*  formula)))
-                                    <*> (beginMath *> varSymbol) <*> (paren varSymbol <* _eq )
-                                    <*> cases (many1 functionDefineCase) <* endMath <* optional _dot
-                                    <*> proof
+    define           <- rule $ Define <$> _let <*> (beginMath *> varSymbol <* _eq) <*> expr <* endMath <* _dot <*> proof
+    defineFunction   <- rule $ DefineFunction <$> _let <*> (beginMath *> varSymbol) <*> paren varSymbol <* _eq <*>  expr <* endMath <* _for <* beginMath <*> varSymbol <* _in <*> expr <* endMath <* _dot <*> proof
 
-
-
-    proof            <- rule $ asum [byContradiction, byCases, bySetInduction, byOrdInduction, calc, subclaim, assume, fix, take, have, suffices, define, defineFunction, defineFunctionLocal, qed]
+    proof            <- rule $ asum [byContradiction, byCases, bySetInduction, byOrdInduction, calc, subclaim, assume, fix, take, have, suffices, define, defineFunction, qed]
 
 
     blockAxiom  <- rule $ uncurry3 BlockAxiom     <$> envPos  "axiom" axiom
@@ -412,9 +426,11 @@ grammar lexicon@Lexicon{..} = mdo
     pure block
 
 
-proofBy :: Prod r Text (Located Token) a -> Prod r Text (Located Token) a
-proofBy method = bracket $ word "proof" *> word "by" *> method
-
+proofBy :: Prod r Text (Located Token) a -> Prod r Text (Located Token) (SourcePos, a)
+proofBy method = bracket do
+    pos <- word "proof" *> word "by"
+    a <- method
+    pure (pos, a)
 
 lemmaEnv :: Prod r Text (Located Token) a -> Prod r Text (Located Token) (SourcePos, Marker, a)
 lemmaEnv content = asum
@@ -482,40 +498,58 @@ enumeratedMarked1 p = begin "enumerate" *> many1 ((,) <$> (command "item" *> lab
 -- instead of with specialized variants.
 --
 phraseOf
-    :: (pat -> [a] -> b)
+    :: forall pat a b r. Locatable a
+    => (SourcePos -> pat -> [a] -> b)
     -> Lexicon
     -> (Lexicon -> HashSet pat)
     -> (pat -> LexicalPhrase)
     -> Prod r Text (Located Token) a
     -> Prod r Text (Located Token) b
 phraseOf constr lexicon selector proj arg =
-    uncurry constr <$> asum (fmap make pats)
+    uncurry3 constr <$> asum (fmap make pats)
     where
+        pats :: [pat]
         pats = HS.toList (selector lexicon)
-        make pat = (\args -> (pat, args)) <$> go (proj pat)
+
+        make :: pat -> Prod r Text (Located Token) (SourcePos, pat, [a])
+        make pat = (\(pos, args) -> (pos, pat, args)) <$> goPos (proj pat)
+
+        goPos :: LexicalPhrase -> Prod r Text (Located Token) (SourcePos, [a])
+        goPos = \case
+            Just w : ws  -> (,) <$> tokenPos w <*> go ws
+            Nothing : ws -> do
+                a <- arg
+                rest <- go ws
+                pure (locate a, a : rest)
+            []           -> error "phraseOf.goPos: empty phrase"
+
+        go :: LexicalPhrase -> Prod r Text (Located Token) [a]
         go = \case
-            Just w : ws  -> token w *> go ws
-            Nothing : ws -> (:) <$> arg <*> go ws
+            Just w : ws  -> tokenPos w *> go ws
+            Nothing : ws -> do
+                a <- arg
+                rest <- go ws
+                pure (a : rest)
             []           -> pure []
 
-adjLOf :: Lexicon -> Prod r Text (Located Token) arg -> Prod r Text (Located Token) (AdjLOf arg)
+adjLOf :: Locatable arg => Lexicon -> Prod r Text (Located Token) arg -> Prod r Text (Located Token) (AdjLOf arg)
 adjLOf lexicon arg = phraseOf AdjL lexicon (HM.keysSet . lexiconAdjLs) id arg <?> "a left adjective"
 
-adjROf :: Lexicon -> Prod r Text (Located Token) arg -> Prod r Text (Located Token) (AdjROf arg)
+adjROf :: Locatable arg =>Lexicon -> Prod r Text (Located Token) arg -> Prod r Text (Located Token) (AdjROf arg)
 adjROf lexicon arg = phraseOf AdjR lexicon (HM.keysSet . lexiconAdjRs) id arg <?> "a right adjective"
 
-adjOf :: Lexicon -> Prod r Text (Located Token) arg -> Prod r Text (Located Token) (AdjOf arg)
+adjOf :: Locatable arg =>Lexicon -> Prod r Text (Located Token) arg -> Prod r Text (Located Token) (AdjOf arg)
 adjOf lexicon arg = phraseOf Adj lexicon (HM.keysSet . lexiconAdjs) id arg <?> "an adjective"
 
 verbOf
-    :: Lexicon
+    :: Locatable a => Lexicon
     -> (SgPl LexicalPhrase -> LexicalPhrase)
     -> Prod r Text (Located Token) a
     -> Prod r Text (Located Token) (VerbOf a)
 verbOf lexicon proj arg = phraseOf Verb lexicon (HM.keysSet . lexiconVerbs) proj arg
 
 funOf
-    :: Lexicon
+    :: Locatable a => Lexicon
     -> (SgPl LexicalPhrase -> LexicalPhrase)
     -> Prod r Text (Located Token) a
     -> Prod r Text (Located Token) (FunOf a)
@@ -524,7 +558,7 @@ funOf lexicon proj arg = phraseOf Fun lexicon (HM.keysSet . lexiconFuns) proj ar
 
 -- | A noun with a @t VarSymbol@ as name(s).
 nounOf
-    :: Lexicon
+    :: Locatable arg =>  Lexicon
     -> (SgPl LexicalPhrase -> LexicalPhrase)
     -> Prod r Text (Located Token) arg
     -> Prod r Text (Located Token) (t VarSymbol)
@@ -542,7 +576,7 @@ nounOf lexicon proj arg vars =
             []           -> pure []
 
 structNounOf
-    :: Lexicon
+    :: Locatable arg => Lexicon
     -> (SgPl LexicalPhrase -> LexicalPhrase)
     -> Prod r Text (Located Token) arg
     -> Prod r Text (Located Token) name
@@ -630,6 +664,9 @@ ref = terminal \ltok -> case unLocated ltok of
 math :: Prod r Text (Located Token) a -> Prod r Text (Located Token) a
 math body = beginMath *> body <* endMath
 
+mathPos :: Prod r Text (Located Token) a -> Prod r Text (Located Token) (SourcePos, a)
+mathPos body = (,) <$> beginMath <*> body <* endMath
+
 text :: Prod r Text (Located Token) a -> Prod r Text (Located Token) a
 text body = begin "text" *> body <* end "text" <?> "\"\\text{...}\""
 
@@ -649,8 +686,8 @@ brace body = token VisibleBraceL  *> body <* token VisibleBraceR <?> "\"\\{...\\
 group :: Prod r Text (Located Token) a -> Prod r Text (Located Token) a
 group body = token InvisibleBraceL *> body <* token InvisibleBraceR <?> "\"{...}\""
 
-align :: Prod r Text (Located Token) a -> Prod r Text (Located Token) a
-align body = begin "align*" *> body <* end "align*"
+align :: Prod r Text (Located Token) a -> Prod r Text (Located Token) (SourcePos, a)
+align body = (,) <$> begin "align*" <*> body <* end "align*"
 
 cases :: Prod r Text (Located Token) a -> Prod r Text (Located Token) a
 cases body = begin "cases" *> body <* end "cases"
diff --git a/source/Syntax/Internal.hs b/source/Syntax/Internal.hs
index 7089d74..73b41de 100644
--- a/source/Syntax/Internal.hs
+++ b/source/Syntax/Internal.hs
@@ -407,34 +407,34 @@ data Proof
     = Omitted
     -- ^ Ends a proof without further verification.
     -- This results in a “gap” in the formalization.
-    | Qed Justification
+    | Qed {mpos :: Maybe SourcePos, by :: Justification}
     -- ^ Ends of a proof, leaving automation to discharge the current goal using the given justification.
-    | ByContradiction Proof
+    | ByContradiction SourcePos Proof
     -- ^ Take the dual of the current goal as an assumption and
     -- set the goal to absurdity.
-    | BySetInduction (Maybe Term) Proof
+    | BySetInduction SourcePos (Maybe Term) Proof
     -- ^ ∈-induction.
-    | ByOrdInduction Proof
+    | ByOrdInduction SourcePos Proof
     -- ^ Transfinite induction for ordinals.
-    | Assume Formula Proof
+    | Assume SourcePos Formula Proof
     -- ^ Simplify goals that are implications or disjunctions.
-    | Fix (NonEmpty VarSymbol) Formula Proof
+    | Fix SourcePos (NonEmpty VarSymbol) Formula Proof
     -- ^ Simplify universal goals (with an optional bound or such that statement)
-    | Take (NonEmpty VarSymbol) Formula Justification Proof
+    | Take SourcePos (NonEmpty VarSymbol) Formula Justification Proof
     -- ^ Use existential assumptions.
-    | Suffices Formula Justification Proof
-    | ByCase [Case]
+    | Suffices SourcePos Formula Justification Proof
+    | ByCase SourcePos [Case]
     -- ^ Proof by case. Disjunction of the case hypotheses 'Case'
     -- must hold for this step to succeed. Each case starts a subproof,
     -- keeping the same goal but adding the case hypothesis as an assumption.
     -- Often this will be a classical split between /@P@/ and /@not P@/, in
     -- which case the proof that /@P or not P@/ holds is easy.
     --
-    | Have Formula Justification Proof
+    | Have SourcePos Formula Justification Proof
     -- ^ An affirmation, e.g.: /@We have \<stmt\> by \<ref\>@/.
     --
-    | Calc CalcQuantifier Calc Proof
-    | Subclaim Formula Proof Proof
+    | Calc SourcePos CalcQuantifier Calc Proof
+    | Subclaim SourcePos Formula Proof Proof
     -- ^ A claim is a sublemma with its own proof:
     --
     -- /@Show \<goal stmt\>. \<steps\>. \<continue other proof\>.@/
@@ -442,10 +442,10 @@ data Proof
     -- A successful first proof adds the claimed formula as an assumption
     -- for the remaining proof.
     --
-    | Define VarSymbol Term Proof
-    | DefineFunction VarSymbol VarSymbol Term Term Proof
+    | Define SourcePos VarSymbol Term Proof
+    | DefineFunction SourcePos VarSymbol VarSymbol Term Term Proof
 
-    | DefineFunctionLocal VarSymbol VarSymbol VarSymbol Term (NonEmpty (Term, Formula)) Proof
+    | DefineFunctionLocal SourcePos VarSymbol VarSymbol VarSymbol Term (NonEmpty (Term, Formula)) Proof
 
 deriving instance Show Proof
 deriving instance Eq   Proof